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: Oct 13 2024 at 01:02 UTC