Fix minor issue in soundness proof

coq/CertificateChecker.v

@@ -48,9 +48,13 @@ Proof.
   destruct iv as [ivlo ivhi].
   rewrite absenv_eq; simpl.
   eapply validErrorbound_sound; eauto.
-  intros v v_in_empty.
-  rewrite NatSet.mem_spec in v_in_empty.
-  inversion v_in_empty.
+  - hnf. intros a in_diff.
+    rewrite NatSet.diff_spec in in_diff.
+    apply fVars_subset.
+    destruct in_diff; auto.
+  - intros v v_in_empty.
+    rewrite NatSet.mem_spec in v_in_empty.
+    inversion v_in_empty.
 Qed.
 
 Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) :=
@@ -64,6 +68,7 @@ Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P:
     (forall v, NatSet.mem v fVars= true ->
           exists vR, E1 v = Some vR /\
                 (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
+    NatSet.Subset (Commands.freeVars f) fVars ->
     ssaPrg f fVars outVars ->
     bstep (toRCmd f) E1 0 vR ->
     bstep (toRCmd f) E2 (Q2R machineEpsilon) vF ->
@@ -74,7 +79,7 @@ Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P:
    validator and the error bound validator.
 **)
 Proof.
-  intros E1 E2 outVars vR vF fVars approxE1E2 P_valid ssa_f eval_real eval_float
+  intros E1 E2 outVars vR vF fVars approxE1E2 P_valid fVars_subset ssa_f eval_real eval_float
          certificate_valid.
   unfold CertificateCheckerCmd in certificate_valid.
   rewrite <- andb_lazy_alt in certificate_valid.
@@ -92,11 +97,10 @@ Proof.
       destruct in_union as [in_fVars | in_empty]; try auto.
       inversion in_empty.
     + rewrite NatSet.union_spec; auto.
-  - hnf.
-    intros a in_set.
-    rewrite NatSet.diff_spec in in_set.
-    destruct in_set as [ in_set not_in_empty].
-    eapply ssa_subset_freeVars; eauto.
+  - hnf; intros a in_diff.
+    rewrite NatSet.diff_spec in in_diff.
+    destruct in_diff.
+    apply fVars_subset; auto.
   - intros v v_in_empty.
     rewrite NatSet.mem_spec in v_in_empty.
     inversion v_in_empty.