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.
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
nth considers the number and the list.
You can try
unfold nth to see what the
match looks like
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: Sep 30 2023 at 06:01 UTC