ソフトウェアの基礎 Poly_J さらなる演習問題

extra.v

Inductive list (X:Type) := nil:list X | cons:X -> list X -> list X.
Implicit Arguments nil [[X]].
Implicit Arguments cons [[X]].
Notation "[ ]" := nil.
Notation "[ x , .. , y ]" := (cons x .. (cons y nil) ..).
Notation "x :: xs" := (cons x xs).

Fixpoint append {X:Type} (xs:list X) (ys:list X) :list X :=
  match xs with
    | nil => ys
    | x :: xs' => x :: append xs' ys
  end.

Notation "xs ++ ys" := (append xs ys).

Fixpoint len {X:Type} (xs:list X) :nat :=
  match xs with
    | [] => O
    | _ :: xs' => S (len xs')
  end.


Fixpoint foldl {X Y:Type} (f:Y -> X -> Y) (y:Y) (xs:list X) :Y :=
  match xs with
    | [] => y
    | x :: xs' => foldl f (f y x) xs'
  end.

Example test_foldl0: foldl plus 0 [] = 0.
Proof. reflexivity. Qed.
Example test_foldl1: foldl (fun xs y => y::xs) [] [1] = [1].
Proof. reflexivity. Qed.
Example test_foldl2: foldl (fun xs y => y::xs) [] [1,2,3] = [3,2,1].
Proof. reflexivity. Qed.

Fixpoint foldr {X Y:Type} (f:X -> Y -> Y) (y:Y) (xs:list X) :Y :=
  match xs with
    | [] => y
    | x :: xs' => f x (foldr f y xs')
  end.

Example test_foldr0: foldr cons [] [1] = [1].
Proof. reflexivity. Qed.
Example test_foldr1: foldr cons [] [1,2,3] = [1,2,3].
Proof. reflexivity. Qed.

Definition foldr_len {X:Type} :list X -> nat :=
  foldr (fun _ n => S n) 0.
Example test_foldr_len0: foldr_len [1] = 1. reflexivity. Qed.
Example test_foldr_len1: foldr_len [1,2,3] = 3. reflexivity. Qed.

Theorem foldr_len_correct:
  forall (X:Type) (xs:list X), foldr_len xs = len xs.
Proof.
  intros.
  induction xs as [|x xs'].
  reflexivity.
  simpl.
  rewrite <- IHxs'.
  unfold foldr_len.
  simpl.
  reflexivity.
Qed.

Definition foldl_len {X:Type} :list X -> nat :=
  foldl (fun n _ => S n) 0.
Example test_foldl_len0: foldl_len [1] = 1. reflexivity. Qed.
Example test_foldl_len1: foldl_len [1,2,3] = 3. reflexivity. Qed.

(* Theorem foldl_len_correct: *)
(*   forall (X:Type) (xs:list X), foldl_len xs = len xs. *)

Fixpoint map {X Y:Type} (f:X->Y) (xs:list X) :list Y :=
  match xs with
    | [] => []
    | x :: xs' => f x :: map f xs'
  end.

Fixpoint beq_nat (n m:nat) :bool :=
  match n,m with
    | O,O => true
    | S n', S m' => beq_nat n' m'
    | _, _ => false
  end.

Definition foldr_map {X Y:Type} (f:X->Y) (xs:list X) :list Y :=
  foldr (fun x ys => f x :: ys) [] xs.
Example test_foldr_map: foldr_map (beq_nat 2) [1,2] = [false,true].
Proof. reflexivity. Qed.

Theorem fold_map_correct:
  forall (X Y:Type) (f:X->Y) (xs:list X), foldr_map f xs = map f xs.
Proof.
  intros.
  induction xs as [|x xs'].
  reflexivity.
  simpl.
  rewrite <- IHxs'.
  unfold foldr_map.
  simpl.
  reflexivity.
Qed.

(* Inductive mumble:Type := a:mumble|b:mumble->nat->mumble|c:mumble. *)
(* Inductive grumble (X:Type) :Type := d:mumble -> grumble X | e:X->grumble X. *)

(* Check e bool true. *)

(* Inductive baz:Type := x:baz->baz|y:baz->bool->baz. *)

Fixpoint evenb (n:nat) :bool :=
  match n with
    | O => true
    | S (S n') => evenb n'
    | _ => false
end.

Fixpoint negb (b:bool) :bool :=
  match b with
    | true => false
    | _ => true
  end.

Definition oddb (n:nat) := negb (evenb n).

Definition andb (b c:bool) :=
  match b,c with
    | true, true => true
    | _, _ => false
  end.
Notation "x && y" := (andb x y).


Definition forallb {X:Type} (p:X -> bool) (xs:list X) :bool :=
  foldr (fun x b => p x && b) true xs.
Example test_forallb_oddb: forallb oddb [1,3,5,7,9] = true.
Proof. reflexivity. Qed.
Example test_forallb_negb: forallb negb [false, false] = true.
Proof. reflexivity. Qed.
Example test_forallb_evenb: forallb evenb [0,2,4,5] = false.
Proof. reflexivity. Qed.
Example test_forallb_nil: forallb (beq_nat 5) [] = true.
Proof. reflexivity. Qed.

Fixpoint existsb {X:Type} (p:X->bool) (xs:list X) :bool :=
  match xs with
    | [] => false
    | (x::xs') => if p x then true else existsb p xs'
  end.

Example test_existb_eq5: existsb (beq_nat 5) [0,2,3,6] = false.
Proof. reflexivity. Qed.

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

Example test_existb'_eq5: existsb' (beq_nat 5) [0,2,3,6] = false.
Proof. simpl. reflexivity. Qed.

Example test_existb'_and: existsb' (andb true) [true,true,true] = true.
Proof. reflexivity. Qed.

Example test_existb'_odd: existsb' oddb [1,0,0,3] = true.
Proof. reflexivity. Qed.

Example test_existb'_nil: existsb' evenb [] = false.
Proof. reflexivity. Qed.

Example test_existb_and: existsb (andb true) [true,true,true] = true.
Proof. reflexivity. Qed.

Example test_existb_odd: existsb oddb [1,0,0,3] = true.
Proof. reflexivity. Qed.

Example test_existb_nil: existsb evenb [] = false.
Proof. reflexivity. Qed.

Theorem existsb'_down:
  forall (X:Type) (p:X->bool) (x:X) (xs:list X),
    p x = false -> existsb' p (x :: xs) = existsb' p xs.
Proof.
  intros.
  induction xs as [|y ys'].
  simpl.
  unfold existsb'.
  simpl.
  unfold forallb.
  simpl.
  rewrite -> H.
  reflexivity.
  unfold existsb'.
  unfold forallb.
  simpl.
  rewrite -> H.
  simpl.
  destruct (negb (p y)).
  simpl.
  destruct (  foldr (fun (x0 : X) (b : bool) => negb (p x0) && b) true ys').
  reflexivity.
  reflexivity.
  reflexivity.
Qed.


Theorem existsb_equality:
  forall (X:Type) (p:X->bool) (xs:list X),
    existsb p xs = existsb' p xs.
Proof.
  intros.
  induction xs as [|x xs'].
  reflexivity.
  simpl.
  remember (p x).
  destruct b.
  (* b = true *)
  unfold existsb'.
  unfold forallb.
  simpl.
  rewrite <- Heqb.
  reflexivity.
  (* b = false *)
  symmetry in Heqb.
  apply existsb'_down with (xs:=xs') in Heqb.
  rewrite -> Heqb.
  assumption.
Qed.