Fix admitted goals in CertificateChecker.v

coq/CertificateChecker.v

@@ -13,7 +13,9 @@ Require Export Daisy.Infra.ExpressionAbbrevs.
 
 (** Certificate checking function **)
 Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
-  andb (validIntervalbounds e absenv P NatSet.empty) (validErrorbound e absenv NatSet.empty).
+  if (validIntervalbounds e absenv P NatSet.empty)
+  then (validErrorbound e absenv NatSet.empty)
+  else false.
 
 (**
    Soundness proof for the certificate checker.
@@ -22,10 +24,11 @@ Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
 **)
 Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P:
   forall (E1 E2:env) (vR:R) (vF:R) fVars,
-    (forall v, NatSet.mem v (Expressions.freeVars e)= true ->
+    approxEnv E1 absenv fVars NatSet.empty E2 ->
+    (forall v, NatSet.mem v fVars = true ->
           exists vR, E1 v = Some vR /\
                 (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
-    approxEnv E1 absenv fVars NatSet.empty E2 ->
+    NatSet.Subset (Expressions.freeVars e) fVars ->
     eval_exp 0%R E1 (toRExp e) vR ->
     eval_exp (Q2R machineEpsilon) E2 (toRExp e) vF ->
     CertificateChecker e absenv P = true ->
@@ -35,32 +38,32 @@ Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P:
    validator and the error bound validator.
 **)
 Proof.
-  intros VarEnv1 VarEnv2 ParamEnv vR vF P_valid approxC1C2 eval_real eval_float certificate_valid.
+  intros E1 E2 vR vF fVars approxE1E2 P_valid fVars_subset eval_real eval_float
+         certificate_valid.
   unfold CertificateChecker in certificate_valid.
+  rewrite <- andb_lazy_alt in certificate_valid.
   andb_to_prop certificate_valid.
-  assert (exists iv err, absenv e = (iv,err)) by (destruct (absenv e); repeat eexists).
-  destruct H as [iv [err absenv_eq]].
-  assert (exists ivlo ivhi, iv = (ivlo, ivhi)) by (destruct iv; repeat eexists).
-  destruct H as [ivlo [ ivhi iv_eq]].
-  subst; rewrite absenv_eq in *; simpl in *.
-  eapply (validErrorbound_sound); eauto.
+  env_assert absenv e env_e.
+  destruct env_e as [iv [err absenv_eq]].
+  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.
-  hnf in v_in_empty.
   inversion v_in_empty.
-  admit.
-Admitted.
+Qed.
 
 Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) :=
-  andb (validIntervalboundsCmd f absenv P NatSet.empty)
-       (validErrorboundCmd f absenv NatSet.empty).
+  if (validIntervalboundsCmd f absenv P NatSet.empty)
+  then (validErrorboundCmd f absenv NatSet.empty)
+  else false.
 
 Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P:
   forall (E1 E2:env) outVars vR vF fVars,
+    approxEnv E1 absenv fVars NatSet.empty E2 ->
     (forall v, NatSet.mem v fVars= true ->
           exists vR, E1 v = Some vR /\
                 (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
-    approxEnv E1 absenv fVars NatSet.empty E2 ->
     ssaPrg f fVars outVars ->
     bstep (toRCmd f) E1 0 vR ->
     bstep (toRCmd f) E2 (Q2R machineEpsilon) vF ->
@@ -71,21 +74,21 @@ 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 P_valid approxC1C2 ssa_f eval_real eval_float
+  intros E1 E2 outVars vR vF fVars approxE1E2 P_valid ssa_f eval_real eval_float
          certificate_valid.
   unfold CertificateCheckerCmd in certificate_valid.
+  rewrite <- andb_lazy_alt in certificate_valid.
   andb_to_prop certificate_valid.
-  assert (exists iv err, absenv (getRetExp f) = (iv,err)) by (destruct (absenv (getRetExp f)); repeat eexists).
-  destruct H as [iv [err absenv_eq]].
-  assert (exists ivlo ivhi, iv = (ivlo, ivhi)) by (destruct iv; repeat eexists).
-  destruct H as [ivlo [ ivhi iv_eq]].
-  subst; rewrite absenv_eq in *; simpl in *.
+  env_assert absenv (getRetExp f) env_f.
+  destruct env_f as [iv [err absenv_eq]].
+  destruct iv as [ivlo ivhi].
+  rewrite absenv_eq; simpl.
   eapply (validErrorboundCmd_sound); eauto.
   - hnf.
     intros a; split; intros in_set.
     + rewrite NatSet.union_spec in in_set.
-      destruct in_set; try auto.
-      inversion H.
+      destruct in_set as [in_fV | in_empty]; try auto.
+      inversion in_empty.
     + rewrite NatSet.union_spec; auto.
   - intros v v_in_empty.
     rewrite NatSet.mem_spec in v_in_empty.