## Stream: new members

### Topic: Pattern matching and recursion

#### Martin C. Martin (Aug 18 2022 at 13:39):

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 (Aug 18 2022 at 13:40):

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 (Aug 18 2022 at 14:03):

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

#### Martin C. Martin (Aug 18 2022 at 14:11):

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

#### Patrick Johnson (Aug 18 2022 at 14:32):

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


Last updated: Dec 20 2023 at 11:08 UTC