Блог

 (** **** 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
 

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

Дана цель со стрелой в ней,

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

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

 h :: filter test t = x :: lf
 

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