# Zulip Chat Archive

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