Тактика: filter_exercise

Question

(** **** Exercise: 3 stars, advanced (filter_exercise)

    This one is a bit challenging.  Pay attention to the form of your
    induction hypothesis. *)

Theorem filter_exercise : forall (X : Type) (test : X -> bool)
                             (x : X) (l lf : list X),
     filter test l = x :: lf ->
     test x = true.
Proof.
  intros X test x l lf. induction l as [| h t].
  - simpl. intros H. discriminate H.
  - simpl. destruct (test h) eqn:E.
    +

Вот что я получил так далеко:

X : Type
test : X -> bool
x, h : X
t, lf : list X
IHt : filter test t = x :: lf -> test x = true
E : test h = true
============================
h :: filter test t = x :: lf -> test x = true

И вот я застрял. Что такого особенного в гипотезе индукции, на которую я должен обратить внимание?

Answer 1

Учитывая цель со стрелкой в ​​нем,

h :: filter test t = x :: lf -> test x = true
                             ^^

естественным следующим шагом является intros предпосылка. Новая предпосылка

h :: filter test t = x :: lf

подразумевает, что компоненты :: соответственно равны т.е. h = x а также filter test t = lf, который можно извлечь с помощью inversion, Остальное тривиально.