Progress cmd proof

coq/ErrorValidationAA.v

@@ -236,8 +236,11 @@ Fixpoint validErrorboundAACmd (f: cmd Q) (* analyzed cmd with let's *)
     match FloverMap.find e A, FloverMap.find (Var Q x) A with
     | Some (iv_e, err_e), Some (iv_x, err_x) =>
       if Qeq_bool err_e err_x then
-          validErrorboundAACmd g typeMap A (NatSet.add x dVars) maxNoise1
-                              (FloverMap.add (Var Q x) afPolye errMap1)
+        match FloverMap.find (Var Q x) errMap1 with
+        | Some _ => None
+        | None => validErrorboundAACmd g typeMap A (NatSet.add x dVars) maxNoise1
+                                      (FloverMap.add (Var Q x) afPolye errMap1)
+        end
       else
           None
     | _,_ => None
@@ -4172,6 +4175,134 @@ Proof.
     destruct p as (variv, varerr).
     destruct (Qeq_bool suberr varerr) eqn: Heqerr;
       cbn in Hvalidbounds; [|congruence].
+    destruct (FloverMap.find (Var Q n) subexpr_map) eqn: Hvarnew;
+      cbn in Hvalidbounds; [congruence|].
+    inversion Hssa; subst.
+    cbn in Hsubset.
+    assert (NatSet.Subset (usedVars e -- dVars) fVars) as Hsubs.
+    { set_tac. repeat split; auto.
+      hnf; intros; subst.
+      set_tac. }
+    pose proof (validErrorboundAA_sound e) as Hvalid__e.
+    inversion Heval__R; subst.
+    destruct Htypes as ((? & ? & ? & ? & ? & ?) & ?).
+    destruct Hrange as ((? & ?) & ?).
+    specialize Hvalid__e as (((v__FP & m__FP & Heval__e) & Hcheckedex__e) & Hvalidall__e); eauto.
+    assert (NatSet.Equal (NatSet.add n (NatSet.union fVars dVars))
+                         (NatSet.union fVars (NatSet.add n dVars))) as Hseteq.
+    {
+      hnf. intros ?; split; intros in_set; set_tac.
+      - destruct in_set as [ ? | [? ?]]; try auto; set_tac.
+        destruct H14; auto.
+      - destruct in_set as [? | ?]; try auto; set_tac.
+        destruct H13 as [? | [? ?]]; auto.
+    }
+    assert (ssa c (fVars ∪ (NatSet.add n dVars)) outVars) as Hssa'.
+    {
+      eapply ssa_equal_set; symmetry in Hseteq.
+      exact Hseteq.
+      assumption.
+    }
+    assert (NatSet.Subset (freeVars c -- NatSet.add n dVars) fVars) as Hsubset'.
+    {
+      hnf. intros ? a_freeVar.
+      rewrite NatSet.diff_spec in a_freeVar.
+      destruct a_freeVar as [a_freeVar a_no_dVar].
+      apply Hsubset.
+      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. }
+    }
+    specialize (Hvalidall__e v__FP m__FP Heval__e) as (af__e & err__e & noise_map2 & ? & ? & ? & ? & ? & ? &
+                                               ? & Hiv & ? & Hevals & Hcheckedall__e).
+    rewrite Qeq_bool_iff in Heqerr.
+    apply Qeq_eqR in Heqerr.
+    assert (approxEnv (updEnv n v E1) (toRExpMap Gamma) A fVars
+                      (NatSet.add n dVars) (updEnv n v__FP E2)).
+    {
+      eapply approxUpdBound; eauto.
+      - eapply toRExpMap_some; eauto.
+        simpl; auto.
+      - apply Rle_trans with (r2:= err__e); try lra.
+        apply to_interval_containment in Hevals.
+        rewrite Hiv in Hevals.
+        cbn in Hevals.
+        now apply Rabs_le.
+    }
+    specialize (H9 v (eval_det_eval_nondet H10)).
+    assert (affine_dVars_error_valid (updEnv n v E1) (updEnv n v__FP E2) A Gamma DeltaMap
+                                     (NatSet.add n dVars) noise_map2 subnoise
+                                     (FloverMap.add (Var Q n) a subexpr_map)).
+    {
+      unfold affine_dVars_error_valid.
+      intros v' Hinv'.
+      destruct (v' =? n) eqn:Heq.
+      - unfold checked_error_expressions, updEnv.
+        intros v__R' v__FP' m__FP' iv__A' err__A' Heval__R' Heval__FP' Hcert'.
+        rewrite Nat.eqb_eq in Heq; subst.
+        inversion Heval__R'; subst.
+        inversion Heval__FP'; subst.
+        unfold updEnv in H24, H26.
+        rewrite Nat.eqb_refl in H24, H26.
+        inversion H24; inversion H26; subst.
+        exists af__e, err__e.
+        intuition.
+        + rewrite FloverMapFacts.P.F.add_eq_o; [congruence|].
+          apply Q_orderedExps.exprCompare_refl.
+        + replace err__A' with varerr by congruence.
+          now rewrite <- Heqerr.
+      - pose proof Heq as Heq'.
+        rewrite Nat.eqb_neq in Heq.
+        apply NatSetProps.FM.add_3 in Hinv'; auto.
+        move Hdvars at bottom.
+        specialize (Hdvars v' Hinv').
+        unfold checked_error_expressions in Hdvars |-*.
+        intros v__R' v__FP' m__FP' iv__A' err__A' Heval__R' Heval__FP' Hcert'.
+        specialize Hdvars as (af' & err__af' & Hfresh' & Hnoisemap1' & Hcertvar' & Herr' &
+                              Hiv' & Herrvar' & Hevals'); eauto.
+        + inversion Heval__R'; subst.
+          unfold updEnv in H24.
+          rewrite Heq' in H24.
+          constructor; eauto.
+        + inversion Heval__FP'; subst.
+          unfold updEnv in H24.
+          rewrite Heq' in H24.
+          constructor; eauto.
+        + exists af', err__af'.
+          repeat split; eauto using fresh_monotonic, af_evals_map_extension.
+          rewrite FloverMapFacts.P.F.add_neq_o; [now apply H13|].
+          cbn; intros Heq''.
+          apply nat_compare_eq in Heq''.
+          auto.
+    }
+    rewrite <- FloverMapFacts.P.F.not_find_in_iff in Hvarnew.
+    specialize IHc with (dVars := NatSet.add n dVars) as (IHex & _); eauto.
+    + lia.
+    + intros e' Hin.
+      destruct (q_expr_eq_dec (Var Q n) e') as [Heqe'|Hneqe'].
+      * rewrite FloverMapFacts.P.F.In_iff in Hvarnew; eauto.
+        specialize (flover_map_el_eq_extension Hvarnew Hin) as [Heq Heqexp].
+        rewrite Heqexp.
+        exists v__FP, m.
+        constructor; auto.
+        1: eapply toRExpMap_some with (e := Var Q n); eauto.
+        unfold updEnv.
+        now rewrite <- beq_nat_refl.
+      * rewrite FloverMapFacts.P.F.add_neq_in_iff in Hin; auto.
+        {
+          destruct (flover_map_in_dec e' expr_map1) as [Hin1|Hnin1].
+          - move Hcheckedex at bottom.
+            specialize (Hcheckedex _ Hin1).
+            destruct Hcheckedex as (vfp & mfp & Hevalfp).
+            exists vfp, mfp.
+            eapply eval_expr_det_ssa_extension; eauto.
+        }
     admit.
   - inversion Heval__R; subst.
     edestruct (validErrorboundAA_sound e) as (((v__FP & m__FP & Hex) & Hcheckedex') & _); eauto;

coq/ExpressionSemanticsDeterministic.v

@@ -5,7 +5,7 @@ From Flover.Infra
      Require Import RealRationalProps RationalSimps Ltacs.
 
 From Flover
-     Require Import ExpressionSemantics.
+     Require Import ExpressionSemantics ssaPrgs.
 
 From Flover.Infra
      Require Export ExpressionAbbrevs.
@@ -344,7 +344,7 @@ Proof.
   rewrite <- (H n); auto.
 Qed.
 
-Lemma eval_expr_det_ignore_bind_det e:
+Lemma eval_expr_det_ignore_bind e:
   forall x v m Gamma E DeltaMap,
     eval_expr_det E Gamma DeltaMap e v m ->
     ~ NatSet.In x (usedVars e) ->
@@ -533,3 +533,16 @@ Proof.
     + trivial.
     + apply Rabs_0_impl_eq in H3; f_equal; now symmetry.
 Qed.
+
+Lemma eval_expr_det_ssa_extension (e: expr R) (e' : expr Q) E Gamma DeltaMap
+      v v' m__e m n c fVars dVars outVars:
+  ssa (Let m__e n e' c) (fVars ∪ dVars) outVars ->
+  NatSet.Subset (usedVars e) (fVars ∪ dVars) ->
+  ~ (n ∈ fVars ∪ dVars) ->
+  eval_expr_det E Gamma DeltaMap e v m ->
+  eval_expr_det (updEnv n v' E) Gamma DeltaMap e v m.
+Proof.
+  intros Hssa Hsub Hnotin Heval.
+  eapply eval_expr_det_ignore_bind; [auto |].
+  edestruct ssa_inv_let; eauto.
+Qed.