proposition: Lemma beval_iff_bevalR : forall b bv, bevalR b bv <-> beval b = bv.
proof: Proof. Admitted. End AExp. Module aevalR_division. Inductive aexp : Type := | ANum : nat -> aexp | APlus : aexp -> aexp -> aexp | AMinus : aexp -> aexp -> aexp | AMult : aexp -> aexp -> aexp | ADiv : aexp -> aexp -> aexp. Reserved Notation "e '\\' n" (at level 50, left associativity). Inductive aevalR : aexp -> nat -> Prop := | E_ANum : forall (n:nat), (ANum n) \\ n | E_APlus : forall (a1 a2: aexp) (n1 n2 : nat), (a1 \\ n1) -> (a2 \\ n2) -> (APlus a1 a2) \\ (n1 + n2) | E_AMinus : forall (a1 a2: aexp) (n1 n2 : nat), (a1 \\ n1) -> (a2 \\ n2) -> (AMinus a1 a2) \\ (n1 - n2) | E_AMult : forall (a1 a2: aexp) (n1 n2 : nat), (a1 \\ n1) -> (a2 \\ n2) -> (AMult a1 a2) \\ (n1 * n2) | E_ADiv : forall (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 50, left associativity). Inductive aexp : Type := | AAny : aexp | ANum : nat -> aexp | APlus : aexp -> aexp -> aexp | AMinus : aexp -> aexp -> aexp | AMult : aexp -> aexp -> aexp. Inductive aevalR : aexp -> nat -> Prop := | E_Any : forall (n:nat), AAny \\ n | E_ANum : forall (n:nat), (ANum n) \\ n | E_APlus : forall (a1 a2: aexp) (n1 n2 : nat), (a1 \\ n1) -> (a2 \\ n2) -> (APlus a1 a2) \\ (n1 + n2) | E_AMinus : forall (a1 a2: aexp) (n1 n2 : nat), (a1 \\ n1) -> (a2 \\ n2) -> (AMinus a1 a2) \\ (n1 - n2) | E_AMult : forall (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. Definition empty_state : state := t_empty 0. Inductive aexp : Type := | ANum : nat -> aexp | AId : id -> aexp | APlus : aexp -> aexp -> aexp | AMinus : aexp -> aexp -> aexp | AMult : aexp -> aexp -> aexp. Definition W : id := Id "W". Definition X : id := Id "X". Definition Y : id := Id "Y". Definition Z : id := Id "Z". Inductive bexp : Type := | BTrue : bexp | BFalse : bexp | BEq : aexp -> aexp -> bexp | BLe : aexp -> aexp -> bexp | BNot : bexp -> bexp | BAnd : bexp -> bexp -> bexp. Fixpoint aeval (st : state) (a : aexp) : nat := match a with | ANum n => n | AId x => st x | APlus a1 a2 => (aeval st a1) + (aeval st a2) | AMinus a1 a2 => (aeval st a1) - (aeval st a2) | AMult a1 a2 => (aeval st a1) * (aeval st a2) end. Fixpoint beval (st : state) (b : bexp) : bool := match b with | BTrue => true | BFalse => false | BEq a1 a2 => beq_nat (aeval st a1) (aeval st a2) | BLe a1 a2 => leb (aeval st a1) (aeval st a2) | BNot b1 => negb (beval st b1) | BAnd b1 b2 => andb (beval st b1) (beval st b2) end. Example aexp1 : aeval (t_update empty_state X 5) (APlus (ANum 3) (AMult (AId X) (ANum 2))) = 13. Proof. reflexivity. Qed.
imports: Coq.Bool.Bool Coq.Arith.Arith Coq.Arith.EqNat Coq.omega.Omega Coq.Lists.List Coq.omega.Omega Maps