Valéry Croizier (Jul 17 2020 at 22:28): 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.
Valéry Croizier (Jul 17 2020 at 22:37):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: Apr 20 2024 at 08:02 UTC