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>

GuestWayncGuestWaync2017/12/22 00:44guest test post
<a href=" http://kioppoerk.com/ ">bbcode</a>
<a href="http://kioppoerk.com/">html</a>
http://kioppoerk.com/ simple

JerdulkJerdulk2018/01/28 01:59Homeopathic Amoxicillin For Pets <a href=http://tadalafbuy.com>cialis</a> Achat Kamagra Voir Le Profil Amoxicillin Tablets

KirhauhKirhauh2018/04/16 04:14Achat De Viagra En Belgique <a href=http://cialviag.com>canadian cialis</a> Overnight Meds Online