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.

Ex 3.2

Inductive binop : Set :=
| Plus
| Times.

Definition var := nat.

Inductive exp : Set :=
| Const : nat -> exp
| Binop : binop -> exp -> exp -> exp
| Var   : var   -> exp.

Definition binopDenote (b : binop) : nat -> nat -> nat :=
  match b with
    | Plus => plus
    | Times => mult
  end.

Fixpoint expDenote (assign : var -> nat) (e : exp) : nat :=
  match e with
    | Const n => n
    | Binop b e1 e2 => (binopDenote b) (expDenote assign e1) (expDenote assign e2)
    |  Var v  => assign v
  end.

Fixpoint const_fold (e : exp) : exp :=
  match e with
    | Binop b e1 e2 =>
      match (const_fold e1, const_fold e2) with
        | (Const x, Const y) => Const ((binopDenote b) x y)
        | (x,y) => Binop b x y
      end
    | _ => e
  end.

Theorem preserve : forall e assign,
  expDenote assign e = expDenote assign (const_fold e).
Proof.
intros.
induction e; simpl; try tauto.
rewrite IHe1, IHe2.
destruct (const_fold e1); destruct (const_fold e2); reflexivity.
Qed.

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