proof Lemma which based on Fixpoint definitions

Question

Trying to prove following Lemma:

I have tried unfold nth_error and nth in the goal but I cannot figure out a way to tell Coq to break the Fixpoint definition of these two functions. I have also tried to induction on n and the lists but none of them was able to solve the problem since the items in list are irrelevant with each other. But this is obviously a correct Lemma, right now I feel it is un-provable, anyone can help me solve this problem? Much appreciated!

Lemma nth_error_nth :
  forall nodes1 (node : node) n,
    n < length nodes1 ->
    nth_error nodes1 n = Some (nth n nodes1 node).

SCappella SCappella · Accepted Answer · 2019-08-18T03:20:25

Your question should really be edited to include a Minimal, Reproducible Example so we don't need to guess what definitions you're using. I'm assuming you're using the standard library's List module and that node is simply some type. Without any more information, I'll just assume it's something like Variable node: Type.

To prove this lemma, induction on the list itself should work. You'll probably also need to do case analysis on n (try destruct n) since n_th and a few other things depend on whether n is 0 or not. If something seems like it might be impossible to prove, try strengthening the inductive hypothesis. This involves having more hypotheses in the goal when you use induction. You can accomplish this with revert or simply never intro the hypothesis in question.

You'll likely get some absurd hypotheses, like n < 0. You can use some the lemmas in PeanoNat.Nat to derive a contradiction from this. It might be helpful to use the Search vernacular. For example, Search (?n < 0). finds the lemma I referred to. There's also one step where you'll need to conclude m < n from S m < S n, which can be done with Lt.lt_S_n.

Just to get you started, here's the beginning of a proof.

Lemma nth_error_nth :
  forall nodes1 (node : node) n,
    n < (length nodes1) ->
    nth_error nodes1 n = Some (nth n nodes1 node).
Proof.
  (* we don't intro n since we'll need to apply
     the inductive hypothesis to two different values of n *)
  intros nodes1 node.
  induction nodes1 as [ | a nodes1 IH].

proof Lemma which based on Fixpoint definitions

1 Answers