proposition: Lemma beval_iff_bevalR : forall b bv, b ==>b bv <-> beval b = bv.
proof: Proof. Admitted. End AExp. Module aevalR_division. Inductive aexp : Type := | ANum (n : nat) | APlus (a1 a2 : aexp) | AMinus (a1 a2 : aexp) | AMult (a1 a2 : aexp) | ADiv (a1 a2 : aexp). Reserved Notation "e '==>' n" (at level 90, left associativity). Inductive aevalR : aexp -> nat -> Prop := | E_ANum (n : nat) : (ANum n) ==> n | E_APlus (a1 a2 : aexp) (n1 n2 : nat) : (a1 ==> n1) -> (a2 ==> n2) -> (APlus a1 a2) ==> (n1 + n2) | E_AMinus (a1 a2 : aexp) (n1 n2 : nat) : (a1 ==> n1) -> (a2 ==> n2) -> (AMinus a1 a2) ==> (n1 - n2) | E_AMult (a1 a2 : aexp) (n1 n2 : nat) : (a1 ==> n1) -> (a2 ==> n2) -> (AMult a1 a2) ==> (n1 * n2) | E_ADiv (a1 a2 : aexp) (n1 n2 n3 : nat) : (a1 ==> n1) -> (a2 ==> n2) -> (n2 > 0) -> (mult n2 n3 = n1) -> (ADiv a1 a2) ==> n3 where "a '==>' n" := (aevalR a n) : type_scope. End aevalR_division. Module aevalR_extended. Reserved Notation "e '==>' n" (at level 90, left associativity). Inductive aexp : Type := | AAny | ANum (n : nat) | APlus (a1 a2 : aexp) | AMinus (a1 a2 : aexp) | AMult (a1 a2 : aexp). Inductive aevalR : aexp -> nat -> Prop := | E_Any (n : nat) : AAny ==> n | E_ANum (n : nat) : (ANum n) ==> n | E_APlus (a1 a2 : aexp) (n1 n2 : nat) : (a1 ==> n1) -> (a2 ==> n2) -> (APlus a1 a2) ==> (n1 + n2) | E_AMinus (a1 a2 : aexp) (n1 n2 : nat) : (a1 ==> n1) -> (a2 ==> n2) -> (AMinus a1 a2) ==> (n1 - n2) | E_AMult (a1 a2 : aexp) (n1 n2 : nat) : (a1 ==> n1) -> (a2 ==> n2) -> (AMult a1 a2) ==> (n1 * n2) where "a '==>' n" := (aevalR a n) : type_scope. End aevalR_extended. Definition state := total_map nat. Inductive aexp : Type := | ANum (n : nat) | AId (x : string) | APlus (a1 a2 : aexp) | AMinus (a1 a2 : aexp) | AMult (a1 a2 : aexp). Definition W : string := "W". Definition X : string := "X". Definition Y : string := "Y". Definition Z : string := "Z". Inductive bexp : Type := | BTrue | BFalse | BEq (a1 a2 : aexp) | BNeq (a1 a2 : aexp) | BLe (a1 a2 : aexp) | BGt (a1 a2 : aexp) | BNot (b : bexp) | BAnd (b1 b2 : bexp). Coercion AId : string >-> aexp. Coercion ANum : nat >-> aexp. Declare Custom Entry com. Declare Scope com_scope. Notation "<{ e }>" := e (at level 0, e custom com at level 99) : com_scope. Notation "( x )" := x (in custom com, x at level 99) : com_scope. Notation "x" := x (in custom com at level 0, x constr at level 0) : com_scope. Notation "f x .. y" := (.. (f x) .. y) (in custom com at level 0, only parsing, f constr at level 0, x constr at level 9, y constr at level 9) : com_scope. Notation "x + y" := (APlus x y) (in custom com at level 50, left associativity). Notation "x - y" := (AMinus x y) (in custom com at level 50, left associativity). Notation "x * y" := (AMult x y) (in custom com at level 40, left associativity). Notation "'true'" := true (at level 1). Notation "'true'" := BTrue (in custom com at level 0). Notation "'false'" := false (at level 1). Notation "'false'" := BFalse (in custom com at level 0). Notation "x <= y" := (BLe x y) (in custom com at level 70, no associativity). Notation "x > y" := (BGt x y) (in custom com at level 70, no associativity). Notation "x = y" := (BEq x y) (in custom com at level 70, no associativity). Notation "x <> y" := (BNeq x y) (in custom com at level 70, no associativity). Notation "x && y" := (BAnd x y) (in custom com at level 80, left associativity). Notation "'~' b" := (BNot b) (in custom com at level 75, right associativity). Open Scope com_scope. Definition example_aexp : aexp := <{ 3 + (X * 2) }>. Definition example_bexp : bexp := <{ true && ~(X <= 4) }>. Fixpoint aeval (st : state) (a : aexp) : nat := match a with | ANum n => n | AId x => st x | <{a1 + a2}> => (aeval st a1) + (aeval st a2) | <{a1 - a2}> => (aeval st a1) - (aeval st a2) | <{a1 * a2}> => (aeval st a1) * (aeval st a2) end. Fixpoint beval (st : state) (b : bexp) : bool := match b with | <{true}> => true | <{false}> => false | <{a1 = a2}> => (aeval st a1) =? (aeval st a2) | <{a1 <> a2}> => negb ((aeval st a1) =? (aeval st a2)) | <{a1 <= a2}> => (aeval st a1) <=? (aeval st a2) | <{a1 > a2}> => negb ((aeval st a1) <=? (aeval st a2)) | <{~ b1}> => negb (beval st b1) | <{b1 && b2}> => andb (beval st b1) (beval st b2) end. Definition empty_st := (_ !-> 0). Notation "x '!->' v" := (x !-> v ; empty_st) (at level 100). Example aexp1 : aeval (X !-> 5) <{ 3 + (X * 2) }> = 13. Proof. reflexivity. Qed.
imports: Coq(Bool.Bool) Coq(Init.Nat) Coq(Arith.Arith) Coq(Arith.EqNat) Coq(Lia) Coq(Lists.List) Coq(Strings.String) LF(Maps)