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.

DannyApenoDannyApeno2017/06/20 22:43Attention Required! | Cloudflare
<a href=http://acheterdufrance.com/>Show more>>></a>

TimothyTeNTimothyTeN2017/07/01 23:47301 Moved Permanently
<a href=https://www.viagrapascherfr.com/>Click here>>></a>