Software Foundations

MoreLogic.v

練習問題。all_forallb

ようやっと、Coqで仕様を記述し、証明する。という本来の目的のモノが出てくる。

問題は、「仕様とは何か？」ということが分かってないことだが。

とりあえず、allを以下のように書く。これはこれで間違ってはいない・・・と思うんだが。

Inductive all (X : Type) (P : X -> Prop) : list X -> Prop :=
 | all_nil  : all X P []
 | all_cons : forall (x:X) (l: list X), all X P l -> all X P (x::l).

これで、forallbの仕様を書け。とは言われても。

Definition TestPTrue {X:Type} (test : X -> bool) (x : X) : Prop :=
 test x = true.

Fixpoint forallb {X : Type} (test : X -> bool) (l : list X) : bool :=
  match l with
    | [] => true
    | x :: l' => andb (test x) (forallb test l')
  end.

Theorem all_forallb_1 : forall (X : Type)(test : X -> bool)(l : list X),
  all X (TestPTrue test) l -> forallb test l = true.
Proof.

こんな感じか。証明は出来てない。
そもそも test xがfalseになるものがある場合、どう仕様を書けばいいのか。