Porting one last proof

coq/IntervalValidation.v

@@ -174,7 +174,6 @@ Qed.
     
 Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) fVars dVars (E:env) defVars:
   forall vR,
-(*    validType Gamma f m -> *)
     validIntervalbounds f absenv P dVars = true ->
     (forall v, NatSet.mem v dVars = true ->
           exists vR, E v = Some vR /\
@@ -525,100 +524,95 @@ Proof.
     apply Is_true_eq_true in vI1; auto.
 Qed.
 
-(* Unused, proof not up-to-date *)
-(* Theorem validIntervalboundsCmd_sound (f:cmd Q) (absenv:analysisResult): *)
-(*   forall E vR fVars dVars outVars elo ehi err P, *)
-(*     ssaPrg f (NatSet.union fVars dVars) outVars -> *)
-(*     bstep (toREvalCmd (toRCmd f)) E vR M0  -> *)
-(*     (forall v m, NatSet.mem v dVars = true -> *)
-(*           exists vR, *)
-(*             E v = Some (vR, m) /\ *)
-(*             (Q2R (fst (fst (absenv (Var Q m v)))) <= vR <= Q2R (snd (fst (absenv (Var Q m v)))))%R) -> *)
-(*     (forall v m, NatSet.mem v fVars = true -> *)
-(*           exists vR, *)
-(*             E v = Some (vR, m) /\ *)
-(*             (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> *)
-(*     NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars -> *)
-(*     validIntervalboundsCmd f  absenv P dVars = true -> *)
-(*     absenv (getRetExp f) = ((elo, ehi), err) -> *)
-(*     (Q2R elo <=  vR <= Q2R ehi)%R. *)
-(* Proof. *)
-(*   induction f; *)
-(*     intros *  ssa_f eval_f dVars_sound fVars_valid usedVars_subset valid_bounds_f absenv_f. *)
-(*   - inversion ssa_f; subst. *)
-(*     inversion eval_f; subst. *)
-(*     unfold validIntervalboundsCmd in valid_bounds_f. *)
-(*     andb_to_prop valid_bounds_f. *)
-(*     inversion ssa_f; subst. *)
-(*     specialize (IHf (updEnv n m v E) vR fVars (NatSet.add n dVars)). *)
-(*     eapply IHf; eauto. *)
-(*     + assert (NatSet.Equal (NatSet.add n (NatSet.union fVars dVars)) (NatSet.union fVars (NatSet.add n dVars))). *)
-(*       * hnf. intros a; split; intros in_set. *)
-(*         { rewrite NatSet.add_spec, NatSet.union_spec in in_set. *)
-(*           rewrite NatSet.union_spec, NatSet.add_spec. *)
-(*           destruct in_set as [P1 | [ P2 | P3]]; auto. } *)
-(*         { rewrite NatSet.add_spec, NatSet.union_spec. *)
-(*           rewrite NatSet.union_spec, NatSet.add_spec in in_set. *)
-(*           destruct in_set as [P1 | [ P2 | P3]]; auto. } *)
-(*       * eapply ssa_equal_set; eauto. *)
-(*         symmetry; eauto. *)
-(*     + admit. *)
-(*     + *)
-(*       intros v0 m0 mem_v0. *)
-(*       unfold updEnv. *)
-(*       case_eq (v0 =? n); intros v0_eq. *)
-(*       * rename R1 into eq_lo; *)
-(*           rename R0 into eq_hi. *)
-(*         apply Qeq_bool_iff in eq_lo; *)
-(*           apply Qeq_eqR in eq_lo. *)
-(*         apply Qeq_bool_iff in eq_hi; *)
-(*           apply Qeq_eqR in eq_hi. *)
-(*         rewrite Nat.eqb_eq in v0_eq; subst. *)
-(*         rewrite <- eq_lo, <- eq_hi. *)
-(*         exists v; split; auto. *)
-(*         eapply validIntervalbounds_sound; eauto. *)
-(*         simpl in usedVars_subset. *)
-(*         hnf. intros a in_usedVars. *)
-(*         apply usedVars_subset. *)
-(*         rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec. *)
-(*         rewrite NatSet.diff_spec in in_usedVars. *)
-(*         destruct in_usedVars as [ in_usedVars not_dVar]. *)
-(*         repeat split; try auto. *)
-(*         { hnf; intros; subst. *)
-(*           specialize (H5 n in_usedVars). *)
-(*           rewrite <- NatSet.mem_spec in H5. *)
-(*           rewrite H5 in H6; congruence. } *)
-(*       * apply dVars_sound. rewrite NatSet.mem_spec. *)
-(*         rewrite NatSet.mem_spec in mem_v0. *)
-(*         rewrite NatSet.add_spec in mem_v0. *)
-(*         destruct mem_v0; try auto. *)
-(*         rewrite Nat.eqb_neq in v0_eq. *)
-(*         exfalso; apply v0_eq; auto. *)
-(*     + intros v0 mem_fVars. *)
-(*       unfold updEnv. *)
-(*       case_eq (v0 =? n); intros case_v0; auto. *)
-(*       rewrite Nat.eqb_eq in case_v0; subst. *)
-(*       assert (NatSet.mem n (NatSet.union fVars dVars) = true) as in_union. *)
-(*       * rewrite NatSet.mem_spec, NatSet.union_spec; rewrite <- NatSet.mem_spec; auto. *)
-(*       * rewrite in_union in *; congruence. *)
-(*     + clear L R1 R0 R IHf. *)
-(*       hnf. intros a a_freeVar. *)
-(*       rewrite NatSet.diff_spec in a_freeVar. *)
-(*       destruct a_freeVar as [a_freeVar a_no_dVar]. *)
-(*       apply usedVars_subset. *)
-(*       simpl. *)
-(*       rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec. *)
-(*       repeat split; try auto. *)
-(*       * hnf; intros; subst. *)
-(*         apply a_no_dVar. *)
-(*         rewrite NatSet.add_spec; auto. *)
-(*       * hnf; intros a_dVar. *)
-(*         apply a_no_dVar. *)
-(*         rewrite NatSet.add_spec; auto. *)
-(*   - unfold validIntervalboundsCmd in valid_bounds_f. *)
-(*     inversion eval_f; subst. *)
-(*     unfold updEnv. *)
-(*     assert (Q2R (fst (fst (absenv (erasure e)))) <= vR <= Q2R (snd (fst (absenv (erasure e)))))%R. *)
-(*     + simpl in valid_bounds_f; eapply validIntervalbounds_sound; eauto. *)
-(*     + simpl in *. rewrite absenv_f in *; auto. *)
-(* Qed. *)
+Theorem validIntervalboundsCmd_sound (f:cmd Q) (absenv:analysisResult) defVars:
+  forall E vR fVars dVars outVars elo ehi err P,
+    ssa f (NatSet.union fVars dVars) outVars ->
+    bstep (toREvalCmd (toRCmd f)) E (toREvalVars defVars) vR M0  ->
+    (forall v, NatSet.mem v dVars = true ->
+          exists vR, E v = Some vR /\
+            (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R) ->
+    (forall v, NatSet.mem v fVars = true ->
+          exists vR, E v = Some vR /\
+            (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
+    NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
+    validIntervalboundsCmd f absenv P dVars = true ->
+    absenv (getRetExp f) = ((elo, ehi), err) ->
+    (Q2R elo <=  vR <= Q2R ehi)%R.
+Proof.
+  induction f;
+    intros *  ssa_f eval_f dVars_sound fVars_valid usedVars_subset valid_bounds_f absenv_f.
+  - inversion ssa_f; subst.
+    inversion eval_f; subst.
+    unfold validIntervalboundsCmd in valid_bounds_f.
+    andb_to_prop valid_bounds_f.
+    inversion ssa_f; subst.
+    specialize (IHf (updEnv n v E) vR fVars (NatSet.add n dVars)).
+    eapply IHf; eauto.
+    + assert (NatSet.Equal (NatSet.add n (NatSet.union fVars dVars)) (NatSet.union fVars (NatSet.add n dVars))).
+      * hnf. intros a; split; intros in_set.
+        { rewrite NatSet.add_spec, NatSet.union_spec in in_set.
+          rewrite NatSet.union_spec, NatSet.add_spec.
+          destruct in_set as [P1 | [ P2 | P3]]; auto. }
+        { rewrite NatSet.add_spec, NatSet.union_spec.
+          rewrite NatSet.union_spec, NatSet.add_spec in in_set.
+          destruct in_set as [P1 | [ P2 | P3]]; auto. }
+      * eapply ssa_equal_set; eauto.
+        symmetry; eauto.
+    + intros v0 mem_v0.
+      unfold updEnv.
+      case_eq (v0 =? n); intros v0_eq.
+      * rename R1 into eq_lo;
+          rename R0 into eq_hi.
+        apply Qeq_bool_iff in eq_lo;
+          apply Qeq_eqR in eq_lo.
+        apply Qeq_bool_iff in eq_hi;
+          apply Qeq_eqR in eq_hi.
+        rewrite Nat.eqb_eq in v0_eq; subst.
+        rewrite <- eq_lo, <- eq_hi.
+        exists v; split; auto.
+        eapply validIntervalbounds_sound; eauto.
+        simpl in usedVars_subset.
+        hnf. intros a in_usedVars.
+        apply usedVars_subset.
+        rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
+        rewrite NatSet.diff_spec in in_usedVars.
+        destruct in_usedVars as [ in_usedVars not_dVar].
+        repeat split; try auto.
+        { hnf; intros; subst.
+          specialize (H5 n in_usedVars).
+          rewrite <- NatSet.mem_spec in H5.
+          rewrite H5 in H6; congruence. }
+      * apply dVars_sound. rewrite NatSet.mem_spec.
+        rewrite NatSet.mem_spec in mem_v0.
+        rewrite NatSet.add_spec in mem_v0.
+        destruct mem_v0; try auto.
+        rewrite Nat.eqb_neq in v0_eq.
+        exfalso; apply v0_eq; auto.
+    + intros v0 mem_fVars.
+      unfold updEnv.
+      case_eq (v0 =? n); intros case_v0; auto.
+      rewrite Nat.eqb_eq in case_v0; subst.
+      assert (NatSet.mem n (NatSet.union fVars dVars) = true) as in_union.
+      * rewrite NatSet.mem_spec, NatSet.union_spec; rewrite <- NatSet.mem_spec; auto.
+      * rewrite in_union in *; congruence.
+    + clear L R1 R0 R IHf.
+      hnf. intros a a_freeVar.
+      rewrite NatSet.diff_spec in a_freeVar.
+      destruct a_freeVar as [a_freeVar a_no_dVar].
+      apply usedVars_subset.
+      simpl.
+      rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
+      repeat split; try auto.
+      * hnf; intros; subst.
+        apply a_no_dVar.
+        rewrite NatSet.add_spec; auto.
+      * hnf; intros a_dVar.
+        apply a_no_dVar.
+        rewrite NatSet.add_spec; auto.
+  - unfold validIntervalboundsCmd in valid_bounds_f.
+    inversion eval_f; subst.
+    simpl in absenv_f.
+    assert (Q2R (fst (fst (absenv e))) <= vR <= Q2R (snd (fst (absenv e))))%R.
+    + simpl in valid_bounds_f; eapply validIntervalbounds_sound; eauto.
+    + simpl in *. rewrite absenv_f in *; auto.
+Qed.