Coq归纳假设是错误的 [英] Coq induction hypothesis is wrong

问题描述

我正在尝试在两个清单上证明一个简单的归纳法， 出于某种原因，Coq将归纳假设写错了. 这是我的证明:

I'm trying to prove a simple induction on two lists, and for some reason Coq writes the induction hypothesis wrong. Here is my proof:

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 ??? *)

以下是到达最后一行(注释)时的假设和目标:

And here are the hypotheses and goals when reaching the last (commented) line:

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'是哪里来的???我在这里想念什么???谢谢！

Obviously, IHl1' involves a false -> _ so it's useless. Where did the l1 = l1' come from??? What am I missing here??? Thanks!!

推荐答案

简短答案:删除对induction l1的调用中的eqn:E1.

Short answer: remove the eqn:E1 in the call to induction l1.

此指令要求induction策略在要通过归纳证明的语句中添加相等性.但是，如果添加这样的等式，则该陈述会出现在归纳证明中，从而弄乱了归纳证明.

This directive asks that the induction tactic adds an equality in the statement to be proved by induction. But if you add such an equality, then it appears in the statement to be proved by induction and this messes up the induction proof.

这篇关于Coq归纳假设是错误的的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！