`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?

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

.

Same problem.

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.

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.

You can try `unfold nth`

to see what the `match`

looks like

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.

Oh, too slow, my bad :)

So, I replaced n + 1 with 1 + n earlier in the proof and `reflexivity`

solves it. :+1:

Last updated: Jan 29 2023 at 01:02 UTC