coq - 如何在 Coq 中使用包含全称量词的假设？

Question

我是 Coq 的新手。我对以下证明感到困惑：

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.

结果显示：

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

使用 H0 和 H 的推论很明显，但我不知道如何使用 H0 来完成证明。非常感谢您的帮助！

Answer 1

由于已经有一段时间了，OP 还没有回应加莱的评论，我将在这里提出一个解决方案，希望它应该很容易在 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.