How to define mutual inductive sentences in Lean?

Question

I am trying to use the syntax for inductive data types, but it received an error message , mutually inductive types must compile into a basic inductive type with a dependent exception .

Below is an example of my attempt to define even and odd sentences for natural numbers

 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) 

Also a related question: what is the syntax for defining mutually recursive functions? I can't seem to find it anywhere in the docs.

Answer 1

I think Lean automatically tries to create even.rec and odd.rec to work with Type , not Prop . But this does not work, because Lean separates the logical world ( Prop ) and the computing world ( Type ). In other words, we can destroy a logical term (proof) only to create a logical term. Note that your example will work if you made even and odd type ℕ → Type .

The Coq proof helper, which is a connected system, automatically processes this situation, creating two (rather weak and impractical) induction principles, but, of course, does not generate common recursors.

There is a workaround described in this Lean wiki article . This involves writing quite a few templates. Let me give an example of how this can be done for this case.

First of all, we collect mutual inductive types into an inductive family. We add a boolean index representing uniformity:

 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) 

Next, we define some abbreviations for simulating mutually inductive types:

 -- 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 no def odd.z : odd 1 := even_odd.zo def odd.n (n : ℕ) (e : even n): odd (n + 1) := even_odd.no ne 

Now let's look at our own principles of induction:

 -- 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 

It is better to make the Ce : ℕ → Prop parameter Ce : ℕ → Prop even.induction_on implicit, but for some reason Lean cannot output it (see the lemma at the end, where we must explicitly pass Ce , otherwise Lean infers Ce not relevant to our goal). The situation is symmetrical with odd.induction_on .

What is the syntax for defining mutually recursive functions?

As explained in this lean user thread , support for mutually recursive functions is very limited:

there is no support for arbitrary mutually recursive functions, but there is support for a very simple case. After defining mutually recursive types, we can define mutually recursive functions that “mirror” the structure of these types.

You can find an example in this thread. But, again, we can simulate mutually recursive functions using the same add-to-switch approach. Let mutually recursive Boolean predicates evenb and 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 

Here is an example of how to use all of the above. Let a simple lemma be proved:

 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)