Commits

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 *)