CODEWITHSUNDEEP
coqinduction
OrenIshShalom
OrenIshShalom

Reputation: 7102

Coq induction hypothesis is wrong

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

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

Upvotes: 0

Views: 557

Answers (1)

Yves
Yves

Reputation: 4236

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

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.

Upvotes: 2

Related Questions