How to define mutual inductive propositions in Lean?

Question

I try using the syntax for inductive datatypes but it got an error message "mutually inductive types must compile to basic inductive type with dependent elimination".

Below is an example of my attempt to define propositions even and odd on 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 documented anywhere.

Answer 1

I think Lean is automatically trying to create the recursors even.rec and odd.rec to work with Type, not Prop. But that doesn't work because Lean separates the logical world (Prop) and computational world (Type). In other words, we can destruct a logical term (proof) only to produce a logical term. Observe, that your example would work if you made even and odd of type ℕ → Type.

The Coq proof assistant, which is a related system, handles this situation automatically by creating two (rather weak and impractical) induction principles, but it doesn't generate the general recursors, of course.

There is a workaround, described in this Lean wiki article. It involves writing quite a lot of boilerplate. Let me give an example how it could be done for this case.

First of all, we compile the mutual inductive types into an inductive family. We add a boolean index representing evenness:

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

Now, let's roll out our own induction principles:

-- 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'd be better to make the Ce : ℕ → Prop parameter of even.induction_on implicit, but for some reason Lean can't infer it (see the lemma at the end, where we have to pass Ce explicitly, otherwise Lean infers Ce not related 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 restricted:

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

You can find an example in that thread. But, again, we can simulate mutually recursive functions using the same add-a-switching-parameter approach. Let's simulate 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 all of the above can be used. Let's prove a simple lemma:

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)