## Stream: Coq users

### Topic: Newbie proving basic lemma on nth

#### Valéry Croizier (Jul 17 2020 at 22:28):

`Lemma nth_succ (a n : nat) (l : list nat) : nth (n+1) (a::l) 0 = 1 + nth n l 0.`
I'd like in vain to destruct the first nth keeping the second intact. How to prove this?

#### Valéry Croizier (Jul 17 2020 at 22:32):

Oops. Was meant to be `nth (n+1) (a::l) 0 = nth n l 0`.

Same problem.

#### Valéry Croizier (Jul 17 2020 at 23:13):

I have tried some double-induction on `l` and then `n` and always end up with goals like `match n with | 0 | _ => 0 end = 0` which look so obvious but still can't find the right tactic.

#### Simon Hudon (Jul 17 2020 at 23:28):

Your proof doesn't need any induction. I believe you may be getting stuck because `n + 1` does not translate to a constructor applied to a variable but `1+n` does. Try `Search (_ + 1).` to find a way to rewrite it into `S _`. That will help because the `match` in `nth` considers the number and the list.

#### Simon Hudon (Jul 17 2020 at 23:28):

You can try `unfold nth` to see what the `match` looks like

#### Yannick Zakowski (Jul 17 2020 at 23:30):

Hello.
The main problem is that the addition over naturals is defined by recursion on the first argument, so that `n + 1` does not reduce. If it were to reduce to a term of the form `S m`, then `nth` itself could reduce, and would reduce to the right hand side.
A complete proof is therefore simply: `rewrite <- peano_naturals.S_nat_plus_1; reflexivity`
The first rewrite replace `n + 1` by `S n`, and then after reduction terms are identical on both side, hence `reflexivity` solves it.

#### Yannick Zakowski (Jul 17 2020 at 23:30):

Oh, too slow, my bad :)

#### Valéry Croizier (Jul 18 2020 at 00:14):

So, I replaced n + 1 with 1 + n earlier in the proof and `reflexivity` solves it. :+1:

Last updated: Jun 18 2024 at 22:01 UTC