0

I'm new to Coq. I'm confused about the proof below:

Lemma nth_eq : forall {A} (l1 l2 : list A),
length l1 = length l2 ->
(forall d k, nth k l1 d = nth k l2 d) ->l1 = l2.
Proof.
  intros.

The result shows:

1 subgoal
A : Type
l1, l2 : list A
H : length l1 = length l2
H0 : forall (d : A) (k : nat), nth k l1 d = nth k l2 d
______________________________________(1/1)
l1 = l2

The inference is obvious by using H0 and H but I don't know how to use H0 to finish the proof. Thank you very much for your help!

Coneain
  • 198
  • 12
  • 1
    Did you try `induction` ? – Vinz Jun 16 '17 at 09:55
  • yes. But it didn't work unless I transform H0 into other form. – Coneain Jun 16 '17 at 10:13
  • I'd recommend looking at [this question](https://stackoverflow.com/q/43332924/2747511) and the comments under it. But `H0` is not a real problem here, you need to generalize your induction hypothesis for the proof to go through. – Anton Trunov Jun 16 '17 at 10:43
  • 1
    How would you prove this theorem using pen and paper only? "Obvious" is not a really satisfactory answer. – gallais Jun 16 '17 at 12:44

1 Answers1

1

Since it's been a while and the OP hasn't responded to the comment by gallais, I'll put a solution here which should hopefully be easy to follow stepping through the proof in an IDE.

Require Import List.

Lemma nth_eq : forall {A} (l1 l2 : list A),
length l1 = length l2 ->
(forall d k, nth k l1 d = nth k l2 d) ->l1 = l2.
Proof.
(* shortcut to the below:
   induction l1; destruct l2; try discriminate 1.
   will eliminate two of the cases for you *)
induction l1; destruct l2.
+ reflexivity.
+ discriminate 1.
+ discriminate 1.
+ intros. f_equal.
  - specialize H0 with (d := a) (k := 0). simpl in H0. assumption.
  - apply IHl1.
    * simpl in H. injection H. trivial.
    * intros. specialize H0 with (d := d) (k := S k). simpl in H0.
      assumption.
Qed.
Daniel Schepler
  • 3,043
  • 14
  • 20