coq - 战术：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。其余的都是微不足道的。