Coq诱导假说是错误的

Question

我试图在两个列表上证明一个简单的归纳，并且由于某种原因，Coq写入归纳假设是错误的。这是我的证明：

Lemma eqb_list_true_iff_left_to_right :
  forall A (eqb : A -> A -> bool),
    (forall a1 a2, eqb a1 a2 = true <-> a1 = a2) ->
    forall l1 l2, eqb_list eqb l1 l2 = true -> l1 = l2.
Proof.
  intros A eqb H1.
  induction l1 as [|a1 l1' IHl1'] eqn:E1.
  - induction l2 as [|a2 l2' IHl2'] eqn:E2.
    + reflexivity.
    + intros H2. simpl in H2. discriminate H2.
  - (* where did l1 = l1' come from ??? *)

以下是到达最后（注释）行时的假设和目标：

1 subgoal
A : Type
eqb : A -> A -> bool
H1 : forall a1 a2 : A, eqb a1 a2 = true <-> a1 = a2
l1 : list A
a1 : A
l1' : list A
E1 : l1 = a1 :: l1'
IHl1' : l1 = l1' ->
        forall l2 : list A, eqb_list eqb l1' l2 = true -> l1' = l2
______________________________________(1/1)
forall l2 : list A, eqb_list eqb (a1 :: l1') l2 = true -> a1 :: l1' = l2

显然，IHl1'涉及一个false -> _所以它没用。 l1 = l1'来自哪里???我在这里失踪了什么？谢谢！！

Answer 1

简短的回答：在eqn:E1的电话中删除induction l1。

该指令要求induction策略在声明中增加一个相等的归纳。但是如果你加上这样的相等，那么它就会出现在声明中，通过归纳证明，这会弄乱感应证据。