帰納的データ型の構文を使用しようとしましたが、エラーメッセージがあります。「相互誘導型は従属型除外型の基本誘導型にコンパイルする必要があります」相互再帰関数を定義するための構文は何ですか：以下希薄で相互誘導的命題を定義する方法は？
はまた、自然数
mutual inductive even, odd
with even: ℕ → Prop
| z: even 0
| n: ∀ n, odd n → even (n + 1)
with odd: ℕ → Prop
| z: odd 1
| n: ∀ n, even n → odd (n + 1)
に関連する質問を提案evenとoddを定義する私の試みの一例ですか？私はそれがどこにでも書かれているとは思えない。
私はLeanが自動的に再帰子even.recとodd.recを作成しようとしていると思って、PropではなくTypeではないと思っています。しかし、Leanは論理世界（Prop）と計算世界（Type）を分離しているため、これは機能しません。言い換えれば、論理的な用語を生成するためにのみ、論理的な用語（証明）を破棄することができます。たとえば、evenとoddがℕ → Typeの場合、あなたの例がうまくいくことに注意してください。
関連システムであるCoqプルーフアシスタントは、2つの（弱く実用的ではない）誘導原理を作成することでこの状況を自動的に処理しますが、一般的な再帰を生成しません。
このLean wiki articleに記載されている回避策があります。かなりの定型文を書くことになります。このケースでどのようにできるかを例に挙げてみましょう。
最初に、相互誘導型を誘導型にコンパイルします。我々は、相互誘導種類をシミュレートするために、いくつかの略語を定義し、
inductive even_odd: bool → ℕ → Prop
| ze: even_odd tt 0
| ne: ∀ n, even_odd ff n → even_odd tt (n + 1)
| zo: even_odd ff 1
| no: ∀ n, even_odd tt n → even_odd ff (n + 1)
次：
-- types
def even := even_odd tt
def odd := even_odd ff
-- constructors
def even.z : even 0 := even_odd.ze
def even.n (n : ℕ) (o : odd n): even (n + 1) := even_odd.ne n o
def odd.z : odd 1 := even_odd.zo
def odd.n (n : ℕ) (e : even n): odd (n + 1) := even_odd.no n e
それでは、私たち自身の誘導の原則をロールアウトしてみましょう：
-- induction principles
def even.induction_on {n : ℕ} (ev : even n) (Ce : ℕ → Prop) (Co : ℕ → Prop)
(ce0 : Ce 0) (stepe : ∀ n : ℕ, Co n → Ce (n + 1))
(co1 : Co 1) (stepo : ∀ n : ℕ, Ce n → Co (n + 1)) : Ce n :=
@even_odd.rec (λ (switch : bool), bool.rec_on switch Co Ce)
ce0 (λ n _ co, stepe n co)
co1 (λ n _ ce, stepo n ce)
tt n ev
def odd.induction_on {n : ℕ} (od : odd n) (Co : ℕ → Prop) (Ce : ℕ → Prop)
(ce0 : Ce 0) (stepe : ∀ n : ℕ, Co n → Ce (n + 1))
(co1 : Co 1) (stepo : ∀ n : ℕ, Ce n → Co (n + 1)) :=
@even_odd.rec (λ (switch : bool), bool.rec_on switch Co Ce)
ce0 (λ n _ co, stepe n co)
co1 (λ n _ ce, stepo n ce)
ff n od
のパラメータを暗黙のうちにeven.induction_onのパラメータにするほうがよいでしょうが、何らかの理由でLeanがそれを推測することはできません（最後の補題を参照してください。私たちはCeを明示的に渡さなければなりません。そうでなければ、LeanはCeの私たちの目標に関係しません。状況はodd.induction_onと対称です。
どのような相互再帰関数を定義するための構文ですか？
としては相互に再帰的な機能のサポートが非常に制限され、このlean-user threadで説明：
任意相互再帰関数のサポートはありませんが、非常に単純なケースのためのサポートがあります。 相互再帰型を定義した後、これらの型の構造を「反映」する相互再帰関数を定義することができます。
このスレッドでは、例を見つけることができます。しかし、やはり、同じadd-a-switching-parameterアプローチを使用して、相互再帰関数をシミュレートすることができます。のは、相互再帰的なブール述語evenbとoddbをシミュレートしてみましょう：ここ
def even_oddb : bool → ℕ → bool
| tt 0 := tt
| tt (n + 1) := even_oddb ff n
| ff 0 := ff
| ff (n + 1) := even_oddb tt n
def evenb := even_oddb tt
def oddb := even_oddb ff
は、上記のすべてを使用することができる方法の一例です。簡単な補助定理を証明しましょう：
lemma even_implies_evenb (n : ℕ) : even n -> evenb n = tt :=
assume ev : even n,
even.induction_on ev (λ n, evenb n = tt) (λ n, oddb n = tt)
rfl
(λ (n : ℕ) (IH : oddb n = tt), IH)
rfl
(λ (n : ℕ) (IH : evenb n = tt), IH)