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

简答：删除对induction l1的调用中的eqn:E1。

该指令要求induction 策略在要通过归纳证明的语句中添加相等性。但是如果你添加这样一个等式，那么它就会出现在要通过归纳证明的陈述中，这会破坏归纳证明。