83 lines
1.6 KiB
Coq
83 lines
1.6 KiB
Coq
(* http://adam.chlipala.net/cpdt/ex/exercises.pdf *)
|
|
|
|
|
|
(* ** 0.1 *)
|
|
|
|
Inductive truth : Type := Yes | No | Maybe.
|
|
|
|
Definition tnot (a: truth) : truth :=
|
|
match a with
|
|
| Yes => No
|
|
| No => Yes
|
|
| Maybe => Maybe
|
|
end.
|
|
|
|
Definition tor (a b: truth) : truth :=
|
|
match a, b with
|
|
| Yes, _ => Yes
|
|
| _, Yes => Yes
|
|
| Maybe, _ => Maybe
|
|
| _, Maybe => Maybe
|
|
| No, No => No
|
|
end.
|
|
|
|
Definition tand (a b: truth) : truth :=
|
|
match a, b with
|
|
| Yes, Yes => Yes
|
|
| No, _ => No
|
|
| _, No => No
|
|
| Maybe, _ => Maybe
|
|
| _, Maybe => Maybe
|
|
end.
|
|
|
|
(* [tand] is commutative *)
|
|
Theorem tand_comm: forall a b c:truth,
|
|
tand (tand a b) c = tand a (tand b c).
|
|
Proof.
|
|
intros a b c.
|
|
induction a; induction b; induction c; trivial.
|
|
Qed.
|
|
|
|
(* [tand] distributes over [tor] *)
|
|
Theorem tand_distr: forall a b c:truth,
|
|
tand a (tor b c) = tor (tand a b) (tand a c).
|
|
Proof.
|
|
intros a b c.
|
|
induction a; induction b; induction c; trivial.
|
|
Qed.
|
|
|
|
(* ** 0.2 *)
|
|
|
|
Require List.
|
|
|
|
Inductive slist {A:Type}: Type :=
|
|
| SNil: slist
|
|
| SCons: A -> slist
|
|
| SApp: slist -> slist -> slist.
|
|
Arguments slist: clear implicits.
|
|
|
|
(*
|
|
Definition sapp {A:Type} (a b:slist A): slist A :=
|
|
match a, b with
|
|
| SNil, _ => b
|
|
| _, SNil => a
|
|
| _, _ => SCons a b
|
|
end.
|
|
*)
|
|
|
|
Fixpoint flatten {A:Type} (a:slist A) : list A :=
|
|
match a with
|
|
| SNil => List.nil
|
|
| SCons x => List.cons x List.nil
|
|
| SApp x y => List.app (flatten x) (flatten y)
|
|
end.
|
|
|
|
Theorem flatten_app_distr {A:Type}: forall a b:slist A,
|
|
flatten (SApp a b) = List.app (flatten a) (flatten b).
|
|
Proof.
|
|
intros a b.
|
|
induction a; induction b; trivial.
|
|
Qed.
|
|
|
|
(* ** 0.3 *)
|