Schedule/ProofCafe_21

演習問題 fold_map

演習問題 forall_exists_challenge


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

Fixpoint existsb {X : Type} (f: X -> bool) (l: list X) : bool :=
  match l with
    | nil => false
    | x :: xs' => orb (f x) (existsb f xs')
  end.

Definition existsb' {X : Type} (f: X -> bool) (l: list X) : bool :=
  negb (forallb (fun x => negb (f x)) l).

Require Import Bool.

Theorem forall_exists_challenge:
  forall (A : Type) (p : A -> bool) xs, existsb p xs = existsb' p xs.
Proof.
  intros A p xs.
  induction xs.
    reflexivity.

    unfold existsb'.
    simpl.
    rewrite negb_andb.
    rewrite negb_involutive.
    rewrite IHxs.
    unfold existsb'.
    reflexivity.
Qed.

練習問題 (gen_dep_practice)