# softwareFoundations

committed f0604bb

Working through Imp.v

# Imp.v

` `
`     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.