Гипотеза индукции Coq неверна - PullRequest
Новая
       27

Гипотеза индукции Coq неверна

0 голосов
/ 27 марта 2019

Я пытаюсь доказать простую индукцию в двух списках, и по какой-то причине 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' ???Что мне здесь не хватает ???Спасибо !!

1 Ответ

2 голосов
/ 27 марта 2019

Краткий ответ: уберите eqn:E1 в вызове induction l1.

Эта директива требует, чтобы тактика induction добавила равенство в утверждение, которое должно быть доказано по индукции.Но если вы добавите такое равенство, то оно появится в утверждении, которое будет доказано индукцией, и это испортит доказательство индукции.

...