Hatena::Groupcoq

mzpの日記

 | 

2010-06-26

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>

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

 |