Change toRTMap to toRExpMap to make function purpose clearer, fix broken...

Change toRTMap to toRExpMap to make function purpose clearer, fix broken proofs up until ErrorBounds.v

coq/CertificateChecker.v

@@ -31,7 +31,7 @@ Definition CertificateChecker (e:expr Q) (absenv:analysisResult)
 Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P
         defVars:
   forall (E1 E2:env),
-    approxEnv E1 (toRTMap defVars) absenv (usedVars e) NatSet.empty E2 ->
+    approxEnv E1 (toRExpMap defVars) absenv (usedVars e) NatSet.empty E2 ->
     (forall v, NatSet.In v (Expressions.usedVars e) ->
           exists vR, E1 v = Some vR /\
                 (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
@@ -70,8 +70,8 @@ Proof.
   { hnf; intros a in_empty.
     set_tac. }
   rename R into validFPRanges.
-  assert (validRanges e absenv E1 (toRTMap defVars)) as valid_e.
-  { eapply (RangeValidator_sound e (dVars:=NatSet.empty) (A:=absenv) (P:=P) (Gamma:=toRTMap defVars) (E:=E1));
+  assert (validRanges e absenv E1 (toRExpMap defVars)) as valid_e.
+  { eapply (RangeValidator_sound e (dVars:=NatSet.empty) (A:=absenv) (P:=P) (Gamma:=toRExpMap defVars) (E:=E1));
       auto. }
   pose proof (validRanges_single _ _ _ _ _ valid_e) as valid_single;
     destruct valid_single as [iv_e [ err_e [vR [ map_e [eval_real real_bounds_e]]]]].

coq/ErrorValidation.v

@@ -151,15 +151,15 @@ Qed.
 
 Lemma validErrorboundCorrectVariable_eval E1 E2 A (v:nat) e nR nlo nhi fVars
       dVars Gamma exprTypes:
-    eval_expr E1 (toRMap (toRTMap Gamma)) (toREval (toRExp (Var Q v))) nR REAL ->
+    eval_expr E1 (toRMap (toRExpMap Gamma)) (toREval (toRExp (Var Q v))) nR REAL ->
     validTypes (Var Q v) Gamma ->
-    approxEnv E1 (toRTMap Gamma) A fVars dVars E2 ->
-    validRanges (Var Q v) A E1 (toRTMap Gamma) ->
+    approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
+    validRanges (Var Q v) A E1 (toRExpMap Gamma) ->
     validErrorbound (Var Q v) exprTypes A dVars = true ->
     NatSet.Subset (NatSet.diff (usedVars (Var Q v)) dVars) fVars ->
     FloverMap.find (Var Q v) A = Some ((nlo, nhi), e) ->
     exists nF m,
-    eval_expr E2 (toRTMap Gamma) (toRExp (Var Q v)) nF m.
+    eval_expr E2 (toRExpMap Gamma) (toRExp (Var Q v)) nF m.
 Proof.
   intros eval_real typing_ok approxCEnv bounds_valid error_valid v_sound A_var.
   apply validRanges_single in bounds_valid.
@@ -180,11 +180,11 @@ Admitted.
 
 Lemma validErrorboundCorrectVariable:
   forall E1 E2 A (v:nat) e nR nF mF nlo nhi fVars dVars exprTypes,
-    eval_expr E1 (toRMap (toRTMap exprTypes)) (toREval (toRExp (Var Q v))) nR REAL ->
-    eval_expr E2 (toRTMap exprTypes) (toRExp (Var Q v)) nF mF ->
-    approxEnv E1 (toRTMap exprTypes) A fVars dVars E2 ->
+    eval_expr E1 (toRMap (toRExpMap exprTypes)) (toREval (toRExp (Var Q v))) nR REAL ->
+    eval_expr E2 (toRExpMap exprTypes) (toRExp (Var Q v)) nF mF ->
+    approxEnv E1 (toRExpMap exprTypes) A fVars dVars E2 ->
     validTypes (Var Q v) (exprTypes) ->
-    validRanges (Var Q v) A E1 (toRTMap exprTypes) ->
+    validRanges (Var Q v) A E1 (toRExpMap exprTypes) ->
     validErrorbound (Var Q v) exprTypes A dVars = true ->
     NatSet.Subset (NatSet.diff (usedVars (Var Q v)) dVars) fVars ->
     FloverMap.find (Var Q v) A = Some ((nlo, nhi), e) ->
@@ -215,7 +215,7 @@ Proof.
     repeat destr_factorize.
     rewrite computeErrorQ_computeErrorR in error_valid.
     eapply Rle_trans; eauto.
-    assert (m = mF) by admit; subst. (* comes from toRTMap... *)
+    assert (m = mF) by admit; subst. (* comes from toRExpMap... *)
     rewrite <- maxAbs_impl_RmaxAbs.
     apply computeErrorR_up.
     apply contained_leq_maxAbs.
@@ -223,10 +223,10 @@ Proof.
 Admitted.
 
 Lemma validErrorboundCorrectConstant_eval E1 E2 m n nR Gamma:
-    eval_expr E1 (toRMap (toRTMap Gamma)) (toREval (toRExp (Const m n))) nR REAL ->
+    eval_expr E1 (toRMap (toRExpMap Gamma)) (toREval (toRExp (Const m n))) nR REAL ->
     validTypes (Const m n) Gamma ->
     exists nF m',
-      eval_expr E2 (toRTMap Gamma) (toRExp (Const m n)) nF m'.
+      eval_expr E2 (toRExpMap Gamma) (toRExp (Const m n)) nF m'.
 Proof.
   intros eval_real typing_ok.
   simpl in *.
@@ -288,13 +288,13 @@ Qed.
 Lemma validErrorboundCorrectAddition E1 E2 A
       (e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
       (alo ahi e1lo e1hi e2lo e2hi:Q) dVars m m1 m2 Gamma:
-  eval_expr E1 (toRMap (toRTMap Gamma)) (toREval (toRExp e1)) nR1 REAL ->
-  eval_expr E1 (toRMap (toRTMap Gamma)) (toREval (toRExp e2)) nR2 REAL ->
-  eval_expr E1 (toRMap (toRTMap Gamma)) (toREval (toRExp (Binop Plus e1 e2))) nR REAL ->
-  eval_expr E2 (toRTMap Gamma) (toRExp e1) nF1 m1 ->
-  eval_expr E2 (toRTMap Gamma) (toRExp e2) nF2 m2 ->
+  eval_expr E1 (toRMap (toRExpMap Gamma)) (toREval (toRExp e1)) nR1 REAL ->
+  eval_expr E1 (toRMap (toRExpMap Gamma)) (toREval (toRExp e2)) nR2 REAL ->
+  eval_expr E1 (toRMap (toRExpMap Gamma)) (toREval (toRExp (Binop Plus e1 e2))) nR REAL ->
+  eval_expr E2 (toRExpMap Gamma) (toRExp e1) nF1 m1 ->
+  eval_expr E2 (toRExpMap Gamma) (toRExp e2) nF2 m2 ->
   eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
-           (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 (toRTMap Gamma)))
+           (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 (toRExpMap Gamma)))
            (toRExp (Binop Plus (Var Q 1) (Var Q 2))) nF m ->
   validTypes (Binop Plus e1 e2) Gamma ->
   validErrorbound (Binop Plus e1 e2) Gamma A dVars = true ->
@@ -2111,16 +2111,16 @@ Qed.
 Theorem validErrorbound_sound (e:expr Q):
   forall E1 E2 fVars dVars A nR err elo ehi Gamma,
     validTypes e Gamma ->
-    approxEnv E1 (toRTMap Gamma) A fVars dVars E2 ->
+    approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
     NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars ->
-    eval_expr E1 (toRMap (toRTMap Gamma)) (toREval (toRExp e)) nR REAL ->
+    eval_expr E1 (toRMap (toRExpMap Gamma)) (toREval (toRExp e)) nR REAL ->
     validErrorbound e Gamma A dVars = true ->
-    validRanges e A E1 (toRTMap Gamma) ->
+    validRanges e A E1 (toRExpMap Gamma) ->
     FloverMap.find e A = Some ((elo,ehi),err) ->
     (exists nF m,
-      eval_expr E2 (toRTMap Gamma) (toRExp e) nF m) /\
+      eval_expr E2 (toRExpMap Gamma) (toRExp e) nF m) /\
     (forall nF m,
-        eval_expr E2 (toRTMap Gamma) (toRExp e) nF m ->
+        eval_expr E2 (toRExpMap Gamma) (toRExp e) nF m ->
     (Rabs (nR - nF) <= (Q2R err))%R).
 Proof.
   revert e; induction e;

coq/ExpressionSemantics.v

@@ -40,7 +40,6 @@ Inductive eval_expr (E:env)
     E x = Some v ->
     eval_expr E Gamma (Var R x) v m
 | Const_dist m n delta:
-    Gamma (Const m n) = Some m ->
     Rabs delta <= mTypeToR m ->
     eval_expr E Gamma (Const m n) (perturb n m delta) m
 | Unop_neg m mN f1 v1:
@@ -88,7 +87,6 @@ Hint Constructors eval_expr.
 Lemma Const_dist' m n delta v m' E Gamma:
   Rle (Rabs delta) (mTypeToR m') ->
   v = perturb n m delta ->
-  Gamma (Const m n) = Some m ->
   m' = m ->
   eval_expr E Gamma (Const m n) v m'.
 Proof.
@@ -171,24 +169,49 @@ Qed.
 
 Hint Resolve Fma_dist'.
 
-Lemma Gamma_def e E Gamma v m:
-  eval_expr E Gamma e v m ->
-  Gamma e = Some m.
+Lemma Gamma_det e E Gamma v1 v2 m1 m2:
+  eval_expr E Gamma e v1 m1 ->
+  eval_expr E Gamma e v2 m2 ->
+  m1 = m2.
 Proof.
-  destruct e; intros * eval_e; inversion eval_e; subst; auto.
+  induction e; intros * eval_e1 eval_e2;
+    inversion eval_e1; subst;
+      inversion eval_e2; subst; try auto;
+        match goal with
+        | [H1: Gamma ?e = Some ?m1, H2: Gamma ?e = Some ?m2 |- _ ] =>
+          rewrite H1 in H2; inversion H2; subst
+        end;
+        auto.
 Qed.
 
 Lemma toRMap_eval_REAL f:
-  forall v E Gamma m, eval_expr E (toRMap Gamma) (toREval f) v m -> m = REAL.
+  forall v E Gamma m, eval_expr E (toRTMap Gamma) (toREval f) v m -> m = REAL.
 Proof.
-  induction f; intros * eval_f; inversion eval_f; subst;
+  induction f; intros * eval_f; inversion eval_f; subst.
   repeat
     match goal with
-    | H: context[toRMap _ _] |- _ => unfold toRMap in H
+    | H: context[toRTMap _ _] |- _ => unfold toRTMap in H
     | H: context[match ?Gamma ?v with | _ => _ end ] |- _ => destruct (Gamma v) eqn:?
     | H: Some ?m1 = Some ?m2 |- _ => inversion H; try auto
     | H: None = Some ?m |- _ => inversion H
     end; try auto.
+  - auto.
+  - rewrite (IHf _ _ _ _ H5) in H2.
+    unfold isCompat in H2.
+    destruct m; type_conv; subst; try congruence; auto.
+  - rewrite (IHf _ _ _ _ H4) in H2.
+    unfold isCompat in H2.
+    destruct m; type_conv; subst; try congruence; auto.
+  - rewrite (IHf1 _ _ _ _ H5) in H3.
+    rewrite (IHf2 _ _ _ _ H8) in H3.
+    unfold isJoin in H3; simpl in H3.
+    destruct m; try congruence; auto.
+  - rewrite (IHf1 _ _ _ _ H5) in H3.
+    rewrite (IHf2 _ _ _ _ H8) in H3.
+    rewrite (IHf3 _ _ _ _ H9) in H3.
+    unfold isJoin3 in H3; simpl in H3.
+    destruct m; try congruence; auto.
+  - auto.
 Qed.
 
 (**
@@ -207,8 +230,8 @@ Evaluation with 0 as machine epsilon is deterministic
 **)
 Lemma meps_0_deterministic (f:expr R) (E:env) Gamma:
   forall v1 v2,
-  eval_expr E (toRMap Gamma) (toREval f) v1 REAL ->
-  eval_expr E (toRMap Gamma) (toREval f) v2 REAL ->
+  eval_expr E (toRTMap Gamma) (toREval f) v1 REAL ->
+  eval_expr E (toRTMap Gamma) (toREval f) v2 REAL ->
   v1 = v2.
 Proof.
   induction f;
@@ -268,13 +291,18 @@ Proof.
   intros no_div_zero err_v eval_f1 eval_f2 eval_float.
   inversion eval_float; subst.
   rewrite H2 in *.
-  eapply Gamma_def in eval_f1; eapply Gamma_def in H6.
-  rewrite H6 in eval_f1; inversion eval_f1; subst.
-  eapply Gamma_def in eval_f2; eapply Gamma_def in H8;
-    rewrite H8 in eval_f2; inversion eval_f2; subst.
+  repeat
+    (match goal with
+     | [H1: eval_expr ?E ?Gamma ?f ?v1 ?m1, H2: eval_expr ?E ?Gamma ?f ?v2 ?m2 |- _] =>
+       assert (m1 = m2)
+         by (eapply Gamma_det; eauto);
+       revert H1 H2
+     end); intros; subst.
   eapply Binop_dist' with (v1:=v1) (v2:=v2) (delta:=delta); try eauto.
-  unfold updDefVars.
-  unfold R_orderedExps.compare; rewrite R_orderedExps.exprCompare_refl; auto.
+  - eapply Var_load; eauto.
+  - eapply Var_load; eauto.
+  - unfold updDefVars.
+    unfold R_orderedExps.compare; rewrite R_orderedExps.exprCompare_refl; auto.
 Qed.
 
 Lemma fma_unfolding f1 f2 f3 E v1 v2 v3 m1 m2 m3 m Gamma delta:
@@ -295,8 +323,7 @@ Proof.
     (match goal with
      | [H1: eval_expr ?E ?Gamma ?f ?v1 ?m1, H2: eval_expr ?E ?Gamma ?f ?v2 ?m2 |- _] =>
        assert (m1 = m2)
-         by (eapply Gamma_def in H1; eapply Gamma_def in H2;
-             rewrite H2 in H1; inversion H1; subst; auto);
+         by (eapply Gamma_det; eauto);
        revert H1 H2
      end).
   intros; subst.

coq/FPRangeValidator.v

@@ -70,10 +70,10 @@ Ltac prove_fprangeval m v L1 R:=
 
 Theorem FPRangeValidator_sound:
   forall (e:expr Q) E1 E2 Gamma v m A fVars dVars,
-  approxEnv E1 (toRTMap Gamma) A fVars dVars E2 ->
-  eval_expr E2 (toRTMap Gamma) (toRExp e) v m ->
+  approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
+  eval_expr E2 (toRExpMap Gamma) (toRExp e) v m ->
   validTypes e Gamma ->
-  validRanges e A E1 (toRTMap Gamma) ->
+  validRanges e A E1 (toRExpMap Gamma) ->
   validErrorbound e Gamma A dVars = true ->
   FPRangeValidator e A Gamma dVars = true ->
   NatSet.Subset (NatSet.diff (usedVars e) dVars) fVars ->

coq/Infra/ExpressionAbbrevs.v

@@ -48,19 +48,20 @@ Proof.
     destruct e5; congruence.
 Qed.
 
-Lemma Qcompare_Rcompare q1 q2 c:
-  Qcompare q1 q2 = c ->
-  Rcompare (Q2R q1) (Q2R q2) = c.
+Lemma Qcompare_Rcompare q1 q2:
+  Qcompare q1 q2 = Rcompare (Q2R q1) (Q2R q2).
 Proof.
-  intros q_check; destruct c.
+  destruct (Qcompare q1 q2) eqn:q_check.
   - rewrite <- Qeq_alt in q_check.
     apply Qeq_eqR in q_check.
     rewrite q_check in *.
     rewrite R_orderedExps.V_orderedFacts.compare_refl in *; auto.
   - rewrite <- Qlt_alt in q_check.
     apply Qlt_Rlt in q_check.
+    symmetry.
     rewrite R_orderedExps.V_orderedFacts.compare_lt_iff; auto.
   - rewrite <- Qgt_alt in q_check.
+    symmetry.
     rewrite R_orderedExps.V_orderedFacts.compare_gt_iff.
     auto using Qlt_Rlt.
 Qed.
@@ -71,7 +72,7 @@ Proof.
   functional induction (Q_orderedExps.exprCompare e1 e2); simpl in *; try auto; try congruence;
     try rewrite e3;
   try rewrite <- IHc, e6; try auto.
-  - destruct (Qcompare v1 v2) eqn:q_comp; apply Qcompare_Rcompare in q_comp; auto.
+  - destruct (Qcompare v1 v2) eqn:q_comp; rewrite Qcompare_Rcompare in q_comp; auto.
   - rewrite e6; auto.
   - rewrite e6; auto.
   - rewrite e6; auto.
@@ -89,6 +90,16 @@ Proof.
   - rewrite e5, e8; auto.
 Qed.
 
+(* Lemma QcompareExp_toREvalcompare e1 e2: *)
+(*   Q_orderedExps.exprCompare e1 e2 = R_orderedExps.exprCompare (toREval (toRExp e1)) (toREval (toRExp e2)). *)
+(* Proof. *)
+(*   functional induction (Q_orderedExps.exprCompare e1 e2); *)
+(*     try auto; try congruence. *)
+(*   - rewrite Qcompare_Rcompare; auto. *)
+(*   - simpl in *; congruence. *)
+(*   - simpl in *; congruence. *)
+(*   -  *)
+
 Lemma usedVars_eq_compat e1 e2:
   Q_orderedExps.eq e1 e2 ->
   NatSet.eq (usedVars e1) (usedVars e2).
@@ -208,13 +219,27 @@ Proof.
   congruence.
 Qed.
 
-Definition toRTMap (tMap:FloverMap.t mType) : expr R -> option mType :=
+Definition toRExpMap (tMap:FloverMap.t mType) : expr R -> option mType :=
   let elements := FloverMap.elements (elt:=mType) tMap in
   fun (e:expr R) =>
-    olet p := findA (fun p => match R_orderedExps.compare e (toRExp p) with
-                   | Eq => true |_ => false end) elements in
+    olet p := findA
+                (fun p => match R_orderedExps.compare e (toRExp p) with
+                       | Eq => true |_ => false end)
+                elements
+      in
         Some p.
 
+Definition toRTMap (Gamma:expr R -> option mType) :expr R -> option mType :=
+  fun (e:expr R) =>
+    match e with
+    | Var _ _ =>
+     match Gamma e with
+     |Some m => Some REAL
+     | _ => None
+     end
+    | _ => Some REAL
+    end.
+
 Definition updDefVars  (e:expr R) (m:mType) Gamma :=
   fun eNew =>
     match R_orderedExps.compare eNew e with
@@ -256,7 +281,7 @@ Proof.
   induction l; intros f_eq find1; simpl in *; try congruence.
   destruct a.
   destruct (f1 a) eqn:?.
-  - rewrite <- f_eq; rewrite Heqb0; congruence.
+  - rewrite <- f_eq; rewrite Heqb0; auto.
   - rewrite <- f_eq; rewrite Heqb0.
     apply IHl; auto.
 Qed.
@@ -273,14 +298,14 @@ Proof.
     apply IHl; auto.
 Qed.
 
-Lemma toRTMap_some tMap e e2 m:
+Lemma toRExpMap_some tMap e e2 m:
   e2 = toRExp e ->
   FloverMap.find e tMap = Some m ->
-  toRTMap tMap e2 = Some m.
+  toRExpMap tMap e2 = Some m.
 Proof.
   intros ? find_Q; subst.
   rewrite  FloverMapFacts.P.F.elements_o in find_Q.
-  unfold toRTMap.
+  unfold toRExpMap.
   unfold optionBind.
   erewrite <- findA_swap2 with (f1 := FloverMapFacts.P.F.eqb e).
   - rewrite find_Q; auto.
@@ -291,12 +316,12 @@ Proof.
     destruct (Q_orderedExps.exprCompare e k) eqn:q_comp; auto.
 Qed.
 
-Lemma toRTMap_find_map tMap e m:
-  toRTMap tMap (toRExp e) = Some m ->
+Lemma toRExpMap_find_map tMap e m:
+  toRExpMap tMap (toRExp e) = Some m ->
   FloverMap.find e tMap = Some m.
 Proof.
   intros RTMap_def.
-  unfold toRTMap, optionBind in *.
+  unfold toRExpMap, optionBind in *.
   Flover_compute.
   inversion RTMap_def; subst.
   rewrite FloverMapFacts.P.F.elements_o.
@@ -308,19 +333,72 @@ Proof.
   destruct (Q_orderedExps.exprCompare e k) eqn:q_comp; auto.
 Qed.
 
-Lemma toRTMap_some_cases tMap e1 e2 m1 m2:
-  toRTMap (FloverMap.add e1 m1 tMap) (toRExp e2) = Some m2 ->
-  (R_orderedExps.exprCompare (toRExp e1) (toRExp e2) = Eq /\ m1 = m2) \/ toRTMap tMap (toRExp e2) = Some m2.
+Lemma toRExpMap_some_cases tMap e1 e2 m1 m2:
+  toRExpMap (FloverMap.add e1 m1 tMap) (toRExp e2) = Some m2 ->
+  (R_orderedExps.exprCompare (toRExp e1) (toRExp e2) = Eq /\ m1 = m2) \/ toRExpMap tMap (toRExp e2) = Some m2.
 Proof.
   intros map_def.
-  apply toRTMap_find_map in map_def.
+  apply toRExpMap_find_map in map_def.
   rewrite FloverMapFacts.P.F.add_o in map_def.
   destruct (FloverMap.E.eq_dec e1 e2) eqn:?.
   - left. inversion map_def; split; try auto.
     rewrite <- QcompareExp_RcompareExp; auto.
-  - right. eauto using toRTMap_some.
+  - right. eauto using toRExpMap_some.
+Qed.
+
+Lemma eqb_cmp_eq e1 e2:
+  FloverMapFacts.P.F.eqb e1 e2 = match Q_orderedExps.exprCompare e1 e2 with
+                                 | Eq => true
+                                 | _ => false end.
+Proof.
+  unfold FloverMapFacts.P.F.eqb, FloverMapFacts.P.F.eq_dec.
+  destruct (Q_orderedExps.exprCompare e1 e2) eqn:q_comp; auto.
 Qed.
 
+Lemma Q_compare_eq_Rcompare_eq e1 e2:
+  Q_orderedExps.exprCompare e1 e2 = Eq ->
+  R_orderedExps.exprCompare (toREval (toRExp e1)) (toREval (toRExp e2)) = Eq.
+Proof.
+  functional induction (Q_orderedExps.exprCompare e1 e2);
+    simpl in *; try congruence;
+      intros;
+      try eauto.
+  - rewrite <- Qcompare_Rcompare; auto.
+  - apply Pos.compare_eq in e6; subst.
+    apply N.compare_eq in H; subst.
+    rewrite Pos.eqb_refl, N.eqb_refl in e3; simpl in *; congruence.
+  - rewrite IHc, e5; auto.
+  - rewrite IHc; auto.
+  - rewrite IHc, IHc0; auto.
+  - rewrite IHc, IHc0; auto.
+  - rewrite IHc, IHc0; auto.
+  - rewrite IHc, IHc0; auto.
+  - apply Pos.compare_eq in e8; subst.
+    apply N.compare_eq in H; subst.
+    rewrite Pos.eqb_refl, N.eqb_refl in e5; simpl in *; congruence.
+Qed.
+
+(*
+Lemma toRExpMap_toRTMap e Gamma m:
+  toRExpMap Gamma (toRExp e) = Some m ->
+  toRTMap Gamma (toREval (toRExp e)) = Some REAL.
+Proof.
+  intros map_def.
+  unfold toRTMap.
+  apply toRExpMap_find_map in map_def.
+  Flover_compute.
+  rewrite FloverMapFacts.P.F.elements_o in map_def.
+  erewrite findA_swap2 with
+      (f2 := FloverMapFacts.P.F.eqb e) in Heqo; try congruence.
+  intros. unfold R_orderedExps.compare.
+  rewrite eqb_cmp_eq.
+  clear map_def Heqo.
+  destruct (Q_orderedExps.exprCompare e k) eqn:?.
+  unfold FloverMapFacts.P.F.eqb, FloverMapFacts.P.F.eq_dec.
+  rewrite <- QcompareExp_RcompareExp.
+  destruct (Q_orderedExps.exprCompare e k) eqn:q_comp; auto.
+*)
+
 (**
 We treat a function mapping an exprression arguing on fractions as value type
 to pairs of intervals on rationals and rational errors as the analysis result

coq/IntervalValidation.v

@@ -5,12 +5,19 @@
     The computation is done using our formalized interval arithmetic.
     The function is used in CertificateChecker.v to build the full checker.
 **)
-Require Import Coq.QArith.QArith Coq.QArith.Qreals QArith.Qminmax Coq.Lists.List Coq.micromega.Psatz.
-Require Import Flover.Infra.Abbrevs Flover.Infra.RationalSimps Flover.Infra.RealRationalProps.
-Require Import Flover.Infra.Ltacs Flover.Infra.RealSimps Flover.TypeValidator.
-Require Export Flover.IntervalArithQ Flover.IntervalArith Flover.ssaPrgs Flover.RealRangeArith.
+From Coq
+     Require Import QArith.QArith QArith.Qreals QArith.Qminmax Lists.List
+     micromega.Psatz.
 
-Fixpoint validIntervalbounds (e:expr Q) (A:analysisResult) (P:precond) (validVars:NatSet.t) :bool:=
+From Flover
+     Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps
+     Infra.Ltacs Infra.RealSimps TypeValidator.
+
+From Flover
+     Require Export IntervalArithQ IntervalArith ssaPrgs RealRangeArith.
+
+Fixpoint validIntervalbounds (e:expr Q) (A:analysisResult) (P:precond)
+         (validVars:NatSet.t) :bool:=
   match FloverMap.find e A with
   | None => false
   | Some (intv, _) =>
@@ -85,7 +92,6 @@ Fixpoint validIntervalbounds (e:expr Q) (A:analysisResult) (P:precond) (validVar
         match FloverMap.find f1 A with
         | None => false
         | Some (iv1, _) =>
-        (* TODO: intv = iv1 might be a hard constraint... *)
         (isSupersetIntv intv iv1) && (isSupersetIntv iv1 intv)
         end
       else
@@ -93,7 +99,8 @@ Fixpoint validIntervalbounds (e:expr Q) (A:analysisResult) (P:precond) (validVar
        end
   end.
 
-Fixpoint validIntervalboundsCmd (f:cmd Q) (A:analysisResult) (P:precond) (validVars:NatSet.t) :bool:=
+Fixpoint validIntervalboundsCmd (f:cmd Q) (A:analysisResult) (P:precond)
+         (validVars:NatSet.t) :bool:=
   match f with
   | Let m x e g =>
     match FloverMap.find e A, FloverMap.find (Var Q x) A with
@@ -133,15 +140,15 @@ Qed.
 
 Theorem validIntervalbounds_sound (f:expr Q) (A:analysisResult) (P:precond)
         fVars dVars (E:env) Gamma:
-    validIntervalbounds f A P dVars = true ->
-    dVars_range_valid dVars E A ->
-    NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars ->
-    fVars_P_sound fVars E P ->
-    validTypes f Gamma ->
-    validRanges f A E (toRTMap Gamma).
+  validIntervalbounds f A P dVars = true ->
+  dVars_range_valid dVars E A ->
+  NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars ->
+  fVars_P_sound fVars E P ->
+  validTypes f Gamma ->
+  validRanges f A E (toRTMap (toRExpMap Gamma)).
 Proof.
   induction f;
-    intros valid_bounds valid_definedVars usedVars_subset valid_freeVars;
+    intros valid_bounds valid_definedVars usedVars_subset valid_freeVars types_defined;
     cbn in *.
   - Flover_compute.
     split; try auto.
@@ -153,10 +160,10 @@ Proof.
       inversion Heqo; subst.
       kill_trivial_exists.
       eexists; split; [auto| split; try eauto ].
-      (* eapply Var_load; simpl; try auto. *)
-      (* destruct (types_defined n) as [m type_m]; *)
-      (*   set_tac. *)
-      (* match_simpl; auto. *)
+      eapply Var_load; simpl; try auto.
+      destruct (types_defined) as [m [find_m _]].
+      eapply toRExpMap_some in  find_m; simpl; eauto.
+      match_simpl; auto.
     + destruct (valid_freeVars n) as [vR [env_valid bounds_valid]];
         set_tac; try auto.
       assert (NatSet.In n fVars) by set_tac.
@@ -165,22 +172,22 @@ Proof.
       kill_trivial_exists.
       eexists; split; [auto | split].
       * econstructor; try eauto.
-        (*
-        destruct (types_defined n) as [m type_m];
-          set_tac.
-        match_simpl; auto. *)
+        destruct (types_defined) as [m [find_m _]].
+        eapply toRExpMap_some in find_m; simpl; eauto.
+        match_simpl; auto.
       * lra.
   - split; [auto |].
     Flover_compute; canonize_hyps; simpl in *.
     kill_trivial_exists.
     exists (perturb (Q2R v) REAL 0).
     split; [eauto| split].
-    + econstructor; try eauto. cbn. rewrite Rabs_R0; lra.
+    + econstructor; try eauto.
+      cbn. rewrite Rabs_R0; lra.
     + unfold perturb; simpl; lra.
   - Flover_compute; simpl in *; try congruence.
-    unfold validRanges in IHf.
-    assert (validRanges f A E (fun x => Some REAL)) as valid_e.
-    { apply IHf; auto. }
+    assert (validRanges f A E (toRTMap (toRExpMap Gamma))) as valid_e.
+    { apply IHf; try auto.
+      destruct types_defined as [? [? [[? ?] ?]]]; auto. }
     split; try auto.
     apply validRanges_single in valid_e.
     destruct valid_e as [iv_f [err_f [vF [iveq_f [eval_f valid_bounds_f]]]]].
@@ -206,7 +213,9 @@ Proof.
         { hnf. destruct nodiv0 as [nodiv0 | nodiv0]; apply Qlt_Rlt in nodiv0;
                rewrite Q2R0_is_0 in nodiv0; lra. }
       * canonize_hyps.
-        pose proof (interval_inversion_valid ((Q2R (fst iv_f)),(Q2R (snd iv_f))) (a :=vF)) as inv_valid.
+        pose proof (interval_inversion_valid ((Q2R (fst iv_f)),(Q2R (snd iv_f)))
+                                             (a :=vF))
+          as inv_valid.
          unfold invertInterval in inv_valid; simpl in *.
          destruct inv_valid; try auto.
          { destruct nodiv0; rewrite <- Q2R0_is_0; [left | right]; apply Qlt_Rlt; auto. }
@@ -229,17 +238,17 @@ Proof.
              hnf; intros.
              destruct nodiv0; try lra.
              assert (Q2R (fst iv_f) < 0)%R.
-             { eapply Rle_lt_trans.
-               Focus 2.
-               rewrite <- Q2R0_is_0;
-                 apply Qlt_Rlt in H2; apply H2.
-               lra.
-             }
+             { rewrite <- Q2R0_is_0.