Stream: Coq users

Topic: Newbie proving basic lemma on nth


view this post on Zulip 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?

view this post on Zulip Valéry Croizier (Jul 17 2020 at 22:32):

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

view this post on Zulip Valéry Croizier (Jul 17 2020 at 22:37):

Same problem.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Jul 17 2020 at 23:28):

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

view this post on Zulip 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.

view this post on Zulip Yannick Zakowski (Jul 17 2020 at 23:30):

Oh, too slow, my bad :)

view this post on Zulip 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: Jan 29 2023 at 01:02 UTC