Proof that uses mutual recursion

Stream: new members

[Vivek Rajesh Joshi]

In TPIL Chapter 8 (Induction and recursion), I'm not familiar with the format that is used in this proof regarding mutual recursion of Even and Odd. Can someone explain what the code means here, i.e. what does _, mean and how odd_succ is helping us here?

mutual
 inductive Even : Nat → Prop where
   | even_zero : Even 0
   | even_succ : ∀ n, Odd n → Even (n + 1)
 inductive Odd : Nat → Prop where
   | odd_succ : ∀ n, Even n → Odd (n + 1)
end
open Even Odd

theorem even_of_odd_succ : ∀ n, Odd (n + 1) → Even n
  | _, odd_succ n h => h

[Ruben Van de Velde]

This is "pattern matching". The underscore is used instead of a name when the name is not used or can be derived automatically. The comma separates parts of the pattern, so lean reads this as "take a natural number (from the ∀ n), and take a value of type Odd (n + 1) if it looks like odd_succ something something, and name the somethings n and h, and then the proof for this case is given after the =>

[Ruben Van de Velde]

Generally you'd have more than one alternative (starting with the | bar), but in this case Odd (n + 1) can only be constructed as odd_succ

[Ruben Van de Velde]

Compare with:

theorem even_of_odd_succ : ∀ n, Even n → Odd (n + 1)
  | 0, even_zero => sorry
  | n + 1, even_succ _ h => sorry

[Vivek Rajesh Joshi]

Got it, thanks :thumbs_up: