Konstantin Solomatov avatar Konstantin Solomatov committed f0604bb

Working through Imp.v

Comments (0)

Files changed (1)

 
     We'll see many examples of these in the proofs below. *)
 
-(** Kostik **)
-
 (* ####################################################### *)
 (** * Evaluation as a Relation *)
 
        try apply IHa1; try apply IHa2; reflexivity. 
 Qed.
 
+(** Kostik **)
+
 (** **** Exercise: 2 stars, optional (bevalR) *)
 (** Write a relation [bevalR] in the same style as
     [aevalR], and prove that it is equivalent to [beval].*)
 
-(* 
-Inductive bevalR:
-(* FILL IN HERE *)
+Inductive bevalR : bexp -> bool -> Prop :=
+  | E_BTrue : bevalR BTrue true
+  | E_BFalse : bevalR BFalse false
+  | E_BEq : forall e1 e2 v1 v2, e1 || v1 -> e2 || v2 -> bevalR (BEq e1 e2) (beq_nat v1 v2)
+  | E_BLe : forall e1 e2 v1 v2, e1 || v1 -> e2 || v2 -> bevalR (BLe e1 e2) (ble_nat v1 v2)
+  | E_BNot : forall e1 v1, bevalR e1 v1 -> bevalR (BNot e1) (negb v1)
+  | E_BAnd : forall e1 e2 v1 v2, bevalR e1 v1 -> bevalR e2 v2 -> bevalR (BAnd e1 e2) (andb v1 v2).
+
+Theorem bevalREq : forall e b,
+  bevalR e b <-> beval e = b.
+Proof.
+  split. 
+  Case "->". intros H. induction H; 
+    (* E_BTrue and E_BFalse *) try (reflexivity);
+    (* E_BEq E_BLe *) 
+      try (
+        simpl; apply aeval_iff_aevalR in H; apply aeval_iff_aevalR in H0; subst; reflexivity).
+    SCase "E_BNot". simpl. rewrite IHbevalR. reflexivity.
+    SCase "E_BAnd". simpl. rewrite IHbevalR1. rewrite IHbevalR2. reflexivity.
+  Case "<-". 
+    generalize dependent b. 
+    induction e; intros.
+    SCase "E_BTrue". simpl in H. subst. constructor.
+    SCase "E_BFalse". simpl in H. subst. constructor. 
+    SCase "E_BEq". simpl in H. subst. constructor. 
+      apply aeval_iff_aevalR. reflexivity.
+      apply aeval_iff_aevalR. reflexivity.
+    SCase "E_BLe". simpl in H. subst. constructor. 
+      apply aeval_iff_aevalR. reflexivity.
+      apply aeval_iff_aevalR. reflexivity. 
+    SCase "E_BNot". simpl in H. subst. constructor. apply IHe. reflexivity.
+    SCase "E_BAnd". simpl in H. subst. constructor. 
+      apply IHe1. reflexivity.
+      apply IHe2. reflexivity.
+Qed.
 (** [] *)
-*)
 
 (** For the definitions of evaluation for arithmetic and boolean
     expressions, the choice of whether to use functional or relational
     evaluation are greatly preferable to functional ones, as we'll see
     shortly. *)
 
+(** Kostik **)
+
 (* ####################################################### *)
 (** ** Inference Rule Notation *)
 
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.