Hatena::Groupcoq

mzpの日記

2010-06-26

Ex 3.1

Inductive truth := Yes | No | Maybe.

Definition not (t : truth) :=
  match t with
    | Yes => No
    | No  => Yes
    | Maybe => Maybe
  end.

Definition and (t1 t2 : truth) :=
  match (t1,t2) with
    | (Yes,Yes) => Yes
    | (No,No) => No
    | _   => Maybe
  end.

Definition or (t1 t2 : truth) :=
  match (t1,t2) with
    | (Yes,_)  => Yes
    | (_,Yes)  => Yes
    | (No,No)  => No
    | _ => Maybe
  end.

Lemma and_comm : forall (t1 t2 t3 : truth),
  and t1 (and t2 t3) = and (and t1 t2) t3.
Proof.
intros.
destruct t1; destruct t2; destruct t3; simpl; try tauto.
Qed.

Lemma or_dist_r : forall (t1 t2 t3 : truth),
  and t1 (or t2 t3) = or (and t1 t2) (and t1 t3).
Proof.
intros.
destruct t1; destruct t2; destruct t3; simpl; try tauto.
Qed.

Lemma or_dist_l : forall (t1 t2 t3 : truth),
  and (or t1 t2) t3 = or (and t1 t3) (and t2 t3).
Proof.
intros.
destruct t1; destruct t2; destruct t3; simpl; try tauto.
Qed.