Pattern matching and recursion

Stream: new members

[Martin C. Martin]

The mathlib style is to provide the arguments to a theorem as a parameter, like this:
theorem my_zero_add (n : ℕ) : 0 + n
However, this means they're not immediately available to the pattern matcher, i.e. you can't start your proof with |. You can use a match ... with, but how do I access the inductive hypothesis? This fails with "unknown identifier 'my_zero_add'":

theorem my_zero_add (n : ℕ) : 0 + n = n :=
match n with
| 0 := rfl
| (n + 1) := congr_arg nat.succ (my_zero_add n)

[Martin C. Martin]

If I add n as an explicit argument, instead of a parameter, everything is unicorns and rainbows:

theorem my_zero_add' : ∀ n : ℕ, 0 + n = n
| 0 := rfl
| (n + 1) := congr_arg nat.succ (my_zero_add' n)

[Reid Barton]

mathlib style is to use the my_zero_add' form when required/useful.

[Martin C. Martin]

Thanks. So we let the details of the proof affect the way the theorem is stated & used?

[Patrick Johnson]

Martin C. Martin said:

So we let the details of the proof affect the way the theorem is stated & used?

The statements of the both theorems are identical, because theorem parameters are translated to universal quantifiers.

theorem my_zero_add (n : ℕ) : 0 + n = n := sorry
theorem my_zero_add' : ∀ (n : ℕ), 0 + n = n := sorry

#check my_zero_add  -- ∀ (n : ℕ), 0 + n = n
#check my_zero_add' -- ∀ (n : ℕ), 0 + n = n