Commit 4730f8a8 authored by Heiko Becker's avatar Heiko Becker

Merge branch 'affine_arithmetic' of gitlab.mpi-sws.org:AVA/FloVer into affine_arithmetic

parents 8c58a841 539a03bf
This diff is collapsed.
......@@ -22,93 +22,153 @@ Fixpoint validErrorboundAA (e:expr Q) (* analyzed expression *)
(dVars:NatSet.t) (* let-bound variables encountered previously *)
(currNoise: nat) (* current maximal noise term *)
(errMap:FloverMap.t (affine_form Q)) (* previously seen affine polys *)
:option (FloverMap.t (affine_form Q) * nat) :=
olet m := FloverMap.find e typeMap in
olet dRes := FloverMap.find e A in
let (intv, err) := dRes in
(* Error bounds are intervals symmetric at 0 --> the bound must be positive here *)
if (negb (Qleb 0 err))
then None
else
(* We have already checked a subexpression *)
if (FloverMap.mem e errMap)
then Some (errMap, currNoise)
: option (FloverMap.t (affine_form Q) * nat) :=
(* (* case analysis for the expression *) *)
(* if (FloverMap.mem e errMap) then *)
(* (* We have already checked a subexpression *) *)
(* Some (errMap, currNoise) *)
(* else *)
olet m := FloverMap.find e typeMap in
olet dRes := FloverMap.find e A in
let (intv, err) := dRes in
(* Error bounds are intervals symmetric at 0 --> the bound must be positive here *)
if (negb (Qleb 0 err))
then None
else
(* case analysis for the expression *)
match e with
| Var _ x =>
match e with
| Var _ x =>
if (NatSet.mem x dVars)
then Some (errMap, currNoise) (* previously checked defined variable *)
else
(* Build an affine polynomial *)
let errNew := computeErrorQ (maxAbs intv) m in
let af := fromIntv (mkIntv (-errNew) errNew) currNoise in
if (Qleb errNew err)
then Some (FloverMap.add e af errMap, (currNoise+1)%nat)
else None
| Expressions.Const m v =>
(* Build an affine polynomial *)
let errNew := computeErrorQ (maxAbs intv) m in
let af := fromIntv (mkIntv (-errNew) errNew) currNoise in
if (Qleb errNew err)
then Some (FloverMap.add e af errMap, (currNoise+1)%nat)
else None
| Expressions.Const m v =>
let errNew := computeErrorQ (maxAbs intv) m in
let af := fromIntv (mkIntv (-errNew) errNew) currNoise in
if (Qleb errNew err)
then Some (FloverMap.add (elt:=affine_form Q) e af errMap, (currNoise+1)%nat)
else None
| Unop Neg e1 =>
| Unop Neg e1 =>
olet res := validErrorboundAA e1 typeMap A dVars currNoise errMap in
let (newErrorMap, maxNoise) := res in
olet afPolye1 := FloverMap.find e1 newErrorMap in
match FloverMap.find e1 A with
| Some (iv_e1, err1) =>
if (Qeq_bool err err1)
then Some (FloverMap.add e afPolye1 newErrorMap, maxNoise)
else None
| None => None
end
| Unop Inv e1 => None
| Binop b e1 e2 =>
olet res1 := validErrorboundAA e1 typeMap A dVars currNoise errMap in
let (newErrorMap1, maxNoise1) := res1 in
olet res2 := validErrorboundAA e2 typeMap A dVars maxNoise1 newErrorMap1 in
let (newErrorMap2, maxNoise2) := res2 in
(* Error polynomial for e1 *)
olet afPolye1 := FloverMap.find e1 newErrorMap2 in
(* Error polynomial for e2 *)
olet afPolye2 := FloverMap.find e2 newErrorMap2 in
(* Analysis results for e1, e2 *)
match FloverMap.find e1 A, FloverMap.find e2 A with
| None, _ => None
| _, None => None
| Some (ive1, err1), Some (ive2, err2) =>
let errIve1 := widenIntv ive1 err1 in
let errIve2 := widenIntv ive2 err2 in
match b with
| Plus =>
let actualRange := (addIntv errIve1 errIve2) in
let errNew := computeErrorQ (maxAbs actualRange) m in
let errPoly := plus_aff
(plus_aff afPolye1 afPolye2)
(fromIntv (mkIntv (-errNew) errNew) maxNoise2) in
let errVal := maxAbs (toIntv errPoly) in
if (Qleb errVal err)
then Some (FloverMap.add e errPoly newErrorMap2, (maxNoise2 + 1)%nat)
else None
| Sub =>
let mAbs := (maxAbs (subtractIntv errIve1 errIve2)) in
let errNew := computeErrorQ mAbs m in
let errPoly := plus_aff
(subtract_aff afPolye1 afPolye2)
(fromIntv (mkIntv (-errNew) errNew) maxNoise2) in
let errVal := maxAbs (toIntv errPoly) in
if (Qleb errVal err)
then Some (FloverMap.add e errPoly newErrorMap2, (maxNoise2 + 1)%nat)
let (newErrorMap, maxNoise) := res in
olet afPolye1 := FloverMap.find e1 newErrorMap in
match FloverMap.find e1 A with
| Some (iv_e1, err1) =>
if (Qeq_bool err err1)
then Some (FloverMap.add e afPolye1 newErrorMap, maxNoise)
else None
| Mult =>
| None => None
end
| Unop Inv e1 => None
| Binop b e1 e2 =>
olet res1 := validErrorboundAA e1 typeMap A dVars currNoise errMap in
let (newErrorMap1, maxNoise1) := res1 in
olet res2 := validErrorboundAA e2 typeMap A dVars maxNoise1 newErrorMap1 in
let (newErrorMap2, maxNoise2) := res2 in
(* Error polynomial for e1 *)
olet afPolye1 := FloverMap.find e1 newErrorMap2 in
(* Error polynomial for e2 *)
olet afPolye2 := FloverMap.find e2 newErrorMap2 in
(* Analysis results for e1, e2 *)
match FloverMap.find e1 A, FloverMap.find e2 A with
| None, _ => None
| _, None => None
| Some (ive1, err1), Some (ive2, err2) =>
let errIve1 := widenIntv ive1 err1 in
let errIve2 := widenIntv ive2 err2 in
match b with
| Plus =>
let actualRange := (addIntv errIve1 errIve2) in
let errNew := computeErrorQ (maxAbs actualRange) m in
let errPoly := plus_aff
(plus_aff afPolye1 afPolye2)
(fromIntv (mkIntv (-errNew) errNew) maxNoise2) in
let errVal := maxAbs (toIntv errPoly) in
if (Qleb errVal err)
then Some (FloverMap.add e errPoly newErrorMap2, (maxNoise2 + 1)%nat)
else None
| Sub =>
let mAbs := (maxAbs (subtractIntv errIve1 errIve2)) in
let errNew := computeErrorQ mAbs m in
let errPoly := plus_aff
(subtract_aff afPolye1 afPolye2)
(fromIntv (mkIntv (-errNew) errNew) maxNoise2) in
let errVal := maxAbs (toIntv errPoly) in
if (Qleb errVal err)
then Some (FloverMap.add e errPoly newErrorMap2, (maxNoise2 + 1)%nat)
else None
| Mult =>
let aaRangee1 := fromIntv ive1 maxNoise2 in
let aaRangee2 := fromIntv ive2 (maxNoise2 + 1) in
let propError := plus_aff
(plus_aff (mult_aff aaRangee1 afPolye2 (maxNoise2 + 2))
(mult_aff aaRangee2 afPolye1 (maxNoise2 + 3) ))
(mult_aff afPolye1 afPolye2 (maxNoise2 + 4)) in
let mAbs := (maxAbs (multIntv errIve1 errIve2)) in
let errNew := computeErrorQ mAbs m in
let errPoly := plus_aff propError
(fromIntv (mkIntv (-errNew) errNew) (maxNoise2 + 5)) in
let errVal := maxAbs (toIntv errPoly) in
if (Qleb errVal err)
then Some (FloverMap.add e errPoly newErrorMap2, (maxNoise2 + 6)%nat)
else None
| Div =>
if (((Qleb (ivhi errIve2) 0) && (negb (Qeq_bool (ivhi errIve2) 0))) ||
((Qleb 0 (ivlo errIve2)) && (negb (Qeq_bool (ivlo errIve2) 0))))
then
let aaRangee1 := fromIntv ive1 maxNoise2 in
let invertede2 := invertIntv ive2 in
let aaRangeInve2 := fromIntv invertede2 (maxNoise2 + 1) in
let invertedErre2 := inverse_aff afPolye2 (maxNoise2 + 2) (* TODO invert *) in
let propError := plus_aff
(plus_aff (mult_aff aaRangee1 invertedErre2 (maxNoise2 + 3))
(mult_aff aaRangeInve2 afPolye1 (maxNoise2 + 4)))
(mult_aff afPolye1 invertedErre2 (maxNoise2 + 5)) in
let mAbs := (maxAbs (divideIntv errIve1 errIve2)) in
let errNew := computeErrorQ mAbs m in
let errPoly := plus_aff propError
(fromIntv (mkIntv (-errNew) errNew) (maxNoise2 + 6)) in
let errVal := maxAbs (toIntv errPoly) in
if (Qleb errVal err)
then Some (FloverMap.add e errPoly newErrorMap2, (maxNoise2 + 7)%nat)
else None
else None
end
end
| Fma e1 e2 e3 =>
olet res1 := validErrorboundAA e1 typeMap A dVars currNoise errMap in
let (newErrorMap1, maxNoise1) := res1 in
olet res2 := validErrorboundAA e2 typeMap A dVars maxNoise1 newErrorMap1 in
let (newErrorMap2, maxNoise2) := res2 in
olet res3 := validErrorboundAA e3 typeMap A dVars maxNoise2 newErrorMap2 in
let (newErrorMap3, maxNoise3) := res3 in
(* Error polynomial for e1 *)
olet afPolye1 := FloverMap.find e1 newErrorMap3 in
(* Error polynomial for e2 *)
olet afPolye2 := FloverMap.find e2 newErrorMap3 in
(* Error polynomial for e2 *)
olet afPolye3 := FloverMap.find e3 newErrorMap3 in
match FloverMap.find e1 A, FloverMap.find e2 A, FloverMap.find e3 A with
| None, _, _ => None
| _, None, _ => None
| _, _, None => None
| Some (ive1, err1), Some (ive2, err2), Some (ive3, err3) =>
let errIve1 := widenIntv ive1 err1 in
let errIve2 := widenIntv ive2 err2 in
let errIve3 := widenIntv ive3 err3 in
let aaRangee1 := fromIntv ive1 maxNoise2 in
let aaRangee2 := fromIntv ive2 (maxNoise2 + 1) in
let propError := plus_aff
(plus_aff (mult_aff aaRangee1 afPolye2 (maxNoise2 + 2))
(mult_aff aaRangee2 afPolye1 (maxNoise2 + 3) ))
(mult_aff afPolye1 afPolye2 (maxNoise2 + 4)) in
let mAbs := (maxAbs (multIntv errIve1 errIve2)) in
(plus_aff
(plus_aff (mult_aff aaRangee1 afPolye2 (maxNoise2 + 2))
(mult_aff aaRangee2 afPolye1 (maxNoise2 + 3) ))
(mult_aff afPolye1 afPolye2 (maxNoise2 + 4)))
afPolye3 in
let mAbs := (maxAbs (addIntv (multIntv errIve1 errIve2) errIve3)) in
let errNew := computeErrorQ mAbs m in
let errPoly := plus_aff propError
(fromIntv (mkIntv (-errNew) errNew) (maxNoise2 + 5)) in
......@@ -116,84 +176,24 @@ Fixpoint validErrorboundAA (e:expr Q) (* analyzed expression *)
if (Qleb errVal err)
then Some (FloverMap.add e errPoly newErrorMap2, (maxNoise2 + 6)%nat)
else None
| Div =>
if (((Qleb (ivhi errIve2) 0) && (negb (Qeq_bool (ivhi errIve2) 0))) ||
((Qleb 0 (ivlo errIve2)) && (negb (Qeq_bool (ivlo errIve2) 0))))
then
let aaRangee1 := fromIntv ive1 maxNoise2 in
let invertede2 := invertIntv ive2 in
let aaRangeInve2 := fromIntv invertede2 (maxNoise2 + 1) in
let invertedErre2 := inverse_aff afPolye2 (maxNoise2 + 2) (* TODO invert *) in
let propError := plus_aff
(plus_aff (mult_aff aaRangee1 invertedErre2 (maxNoise2 + 3))
(mult_aff aaRangeInve2 afPolye1 (maxNoise2 + 4)))
(mult_aff afPolye1 invertedErre2 (maxNoise2 + 5)) in
let mAbs := (maxAbs (divideIntv errIve1 errIve2)) in
let errNew := computeErrorQ mAbs m in
let errPoly := plus_aff propError
(fromIntv (mkIntv (-errNew) errNew) (maxNoise2 + 6)) in
let errVal := maxAbs (toIntv errPoly) in
if (Qleb errVal err)
then Some (FloverMap.add e errPoly newErrorMap2, (maxNoise2 + 7)%nat)
else None
else None
end
end
| Fma e1 e2 e3 =>
end
| Downcast m e1 =>
olet res1 := validErrorboundAA e1 typeMap A dVars currNoise errMap in
let (newErrorMap1, maxNoise1) := res1 in
olet res2 := validErrorboundAA e2 typeMap A dVars maxNoise1 newErrorMap1 in
let (newErrorMap2, maxNoise2) := res2 in
olet res3 := validErrorboundAA e3 typeMap A dVars maxNoise2 newErrorMap2 in
let (newErrorMap3, maxNoise3) := res3 in
(* Error polynomial for e1 *)
olet afPolye1 := FloverMap.find e1 newErrorMap3 in
(* Error polynomial for e2 *)
olet afPolye2 := FloverMap.find e2 newErrorMap3 in
(* Error polynomial for e2 *)
olet afPolye3 := FloverMap.find e3 newErrorMap3 in
match FloverMap.find e1 A, FloverMap.find e2 A, FloverMap.find e3 A with
| None, _, _ => None
| _, None, _ => None
| _, _, None => None
| Some (ive1, err1), Some (ive2, err2), Some (ive3, err3) =>
let errIve1 := widenIntv ive1 err1 in
let errIve2 := widenIntv ive2 err2 in
let errIve3 := widenIntv ive3 err3 in
let aaRangee1 := fromIntv ive1 maxNoise2 in
let aaRangee2 := fromIntv ive2 (maxNoise2 + 1) in
let propError := plus_aff
(plus_aff
(plus_aff (mult_aff aaRangee1 afPolye2 (maxNoise2 + 2))
(mult_aff aaRangee2 afPolye1 (maxNoise2 + 3) ))
(mult_aff afPolye1 afPolye2 (maxNoise2 + 4)))
afPolye3 in
let mAbs := (maxAbs (addIntv (multIntv errIve1 errIve2) errIve3)) in
let errNew := computeErrorQ mAbs m in
let errPoly := plus_aff propError
(fromIntv (mkIntv (-errNew) errNew) (maxNoise2 + 5)) in
let (newErrorMap1, maxNoise1) := res1 in
(* Error polynomial for e1 *)
olet afPolye1 := FloverMap.find e1 newErrorMap1 in
olet aRes := FloverMap.find e1 A in
let (ive1, err1) := aRes in
let errIve1 := widenIntv ive1 err1 in
let mAbs := maxAbs errIve1 in
let newErr := computeErrorQ mAbs m in
let errPoly := plus_aff afPolye1
(fromIntv (mkIntv (-newErr) newErr) maxNoise1) in
let errVal := maxAbs (toIntv errPoly) in
if (Qleb errVal err)
then Some (FloverMap.add e errPoly newErrorMap2, (maxNoise2 + 6)%nat)
then Some (FloverMap.add e errPoly newErrorMap1, (maxNoise1 + 1)%nat)
else None
end
| Downcast m e1 =>
olet res1 := validErrorboundAA e1 typeMap A dVars currNoise errMap in
let (newErrorMap1, maxNoise1) := res1 in
(* Error polynomial for e1 *)
olet afPolye1 := FloverMap.find e1 newErrorMap1 in
olet aRes := FloverMap.find e1 A in
let (ive1, err1) := aRes in
let errIve1 := widenIntv ive1 err1 in
let mAbs := maxAbs errIve1 in
let newErr := computeErrorQ mAbs m in
let errPoly := plus_aff afPolye1
(fromIntv (mkIntv (-newErr) newErr) maxNoise1) in
let errVal := maxAbs (toIntv errPoly) in
if (Qleb errVal err)
then Some (FloverMap.add e errPoly newErrorMap1, (maxNoise1 + 1)%nat)
else None
end.
end.
(** Error bound command validator **)
Fixpoint validErrorboundAACmd (f:cmd Q) (* analyzed cmd with let's *)
......@@ -202,7 +202,7 @@ Fixpoint validErrorboundAACmd (f:cmd Q) (* analyzed cmd with let's *)
(dVars:NatSet.t) (* let-bound variables encountered previously *)
(currNoise: nat) (* current maximal noise term *)
(errMap:FloverMap.t (affine_form Q)) (* previously seen affine polys *)
:option (FloverMap.t (affine_form Q) * nat) :=
: option (FloverMap.t (affine_form Q) * nat) :=
match f with
|Let m x e g =>
olet res1 := validErrorboundAA e typeMap A dVars currNoise errMap in
......@@ -231,6 +231,8 @@ Fixpoint validErrorboundAACmd (f:cmd Q) (* analyzed cmd with let's *)
(* let mAbs := maxAbs (toIntv af) in *)
(* (Rabs (vR - vF) <= (Q2R mAbs))%R. *)
(* Theorem validErrorboundAA_sound e: *)
(* forall E1 E2 P Gamma defVars nR A elo ehi tMap fVars dVars currNoise maxNoise initMap resMap M1, *)
(* (forall e vR, *)
......
......@@ -484,6 +484,14 @@ Proof.
hnf; intros; eapply no_usedVar;
set_tac.
Qed.
Lemma Rmap_updVars_comm Gamma n m:
forall x,
updDefVars n REAL (toRMap Gamma) x = toRMap (updDefVars n m Gamma) x.
Proof.
unfold updDefVars, toRMap; simpl.
intros x; destruct (x =? n); try auto.
Qed.
(*
(**
Analogous lemma for unary expressions.
......
......@@ -89,6 +89,70 @@ Proof.
- rewrite e5, e8; auto.
Qed.
Lemma usedVars_eq_compat e1 e2:
Q_orderedExps.eq e1 e2 ->
NatSet.eq (usedVars e1) (usedVars e2).
Proof.
intros Heq.
unfold Q_orderedExps.eq in Heq.
functional induction (Q_orderedExps.exprCompare e1 e2); try congruence.
- apply Nat.compare_eq in Heq.
now rewrite Heq.
- now set_tac.
- simpl.
reflexivity.
- set_tac.
- specialize (IHc e6).
specialize (IHc0 Heq).
apply NatSet.eq_leibniz in IHc.
apply NatSet.eq_leibniz in IHc0.
simpl.
now rewrite IHc, IHc0.
- specialize (IHc e6).
specialize (IHc0 Heq).
apply NatSet.eq_leibniz in IHc.
apply NatSet.eq_leibniz in IHc0.
simpl.
now rewrite IHc, IHc0.
- specialize (IHc e6).
specialize (IHc0 Heq).
apply NatSet.eq_leibniz in IHc.
apply NatSet.eq_leibniz in IHc0.
simpl.
now rewrite IHc, IHc0.
- specialize (IHc e6).
specialize (IHc0 Heq).
apply NatSet.eq_leibniz in IHc.
apply NatSet.eq_leibniz in IHc0.
simpl.
now rewrite IHc, IHc0.
- specialize (IHc e3).
specialize (IHc0 e4).
specialize (IHc1 Heq).
apply NatSet.eq_leibniz in IHc.
apply NatSet.eq_leibniz in IHc0.
apply NatSet.eq_leibniz in IHc1.
simpl.
now rewrite IHc, IHc0, IHc1.
- simpl.
now apply IHc.
- simpl in e5.
rewrite andb_false_iff in e5.
destruct e5.
+ apply Ndec.Pcompare_Peqb in e8.
congruence.
+ apply N.compare_eq in Heq; subst.
rewrite N.eqb_refl in H; congruence.
Qed.
Lemma usedVars_toREval_toRExp_compat e:
usedVars (toREval (toRExp e)) = usedVars e.
Proof.
induction e; simpl; set_tac.
- now rewrite IHe1, IHe2.
- now rewrite IHe1, IHe2, IHe3.
Qed.
Module FloverMap := FMapAVL.Make(legacy_OrderedQExps).
Module FloverMapFacts := OrdProperties (FloverMap).
......@@ -132,6 +196,18 @@ Proof.
auto.
Qed.
Lemma contained_flover_map_none (V: Type) (e: expr Q) (expmap1: FloverMap.t V) expmap2:
contained_flover_map expmap1 expmap2 ->
FloverMap.find e expmap2 = None ->
FloverMap.find e expmap1 = None.
Proof.
intros cont Hfound1.
unfold contained_flover_map in cont.
destruct (FloverMap.find e expmap1) eqn: Heq; auto.
apply cont in Heq.
congruence.
Qed.
Definition toRBMap (bMap:FloverMap.t N) : expr R -> option N :=
let elements := FloverMap.elements (elt:=N) bMap in
fun (e:expr R) =>
......
......@@ -70,6 +70,25 @@ Proof.
destruct x_in_add as [ x_eq | [x_neq x_in_S]]; auto.
Qed.
Lemma subset_diff_to_subset_union s1 s2 s3:
NatSet.Subset (s1 -- s3) s2 ->
NatSet.Subset s1 (NatSet.union s2 s3).
Proof.
intros diff.
hnf in diff |-*.
intros a Hin1.
specialize (diff a).
destruct (NatSet.mem a s3) eqn: Hmem.
- rewrite NatSet.mem_spec in Hmem.
rewrite NatSet.union_spec.
now right.
- apply not_in_not_mem in Hmem.
rewrite NatSet.union_spec.
left.
apply diff.
apply NatSetProps.Dec.F.diff_3; auto.
Qed.
Ltac set_bool_to_prop :=
match goal with
| [ H: NatSet.mem ?x _ = true |- _ ] => rewrite NatSet.mem_spec in H
......
......@@ -373,14 +373,6 @@ Proof.
simpl in *; lra.
Qed.
Lemma Rmap_updVars_comm Gamma n m:
forall x,
updDefVars n REAL (toRMap Gamma) x = toRMap (updDefVars n m Gamma) x.
Proof.
unfold updDefVars, toRMap; simpl.
intros x; destruct (x =? n); try auto.
Qed.
Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult):
forall Gamma E fVars dVars outVars P fBits,
ssa f (NatSet.union fVars dVars) outVars ->
......
From Coq
Require Import QArith.QArith QArith.Qreals QArith.Qminmax micromega.Psatz.
Require Import QArith.QArith QArith.Qreals QArith.Qminmax micromega.Psatz Recdef.
From Flover
Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps
Infra.Ltacs Infra.RealSimps Typing IntervalArithQ IntervalArith Commands.
Infra.Ltacs Infra.RealSimps Typing ssaPrgs IntervalArithQ IntervalArith Commands.
Definition dVars_range_valid (dVars:NatSet.t) (E:env) (A:analysisResult) :Prop :=
forall v, NatSet.In v dVars ->
......@@ -155,4 +155,243 @@ Proof.
* eapply swap_Gamma_eval_expr with (Gamma1 := toRMap Gamma2); eauto.
- destruct valid1.
eapply validRanges_swap; eauto.
Qed.
\ No newline at end of file
Qed.
Lemma validRanges_eq_compat (e1: expr Q) e2 A E Gamma fBits:
Q_orderedExps.eq e1 e2 ->
validRanges e1 A E Gamma fBits ->
validRanges e2 A E Gamma fBits.
Proof.
intros Heq.
unfold Q_orderedExps.eq in Heq.
functional induction (Q_orderedExps.exprCompare e1 e2); try congruence.
- simpl.
intros [_ validr1].
repeat split; auto.
destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
exists iv, err, vR.
apply Nat.compare_eq in Heq.
rewrite <- Heq.
intuition.
- intros [_ validr1].
repeat split; auto.
destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
exists iv, err, vR.
intuition.
+ rewrite <- Hfind.
symmetry.
apply FloverMapFacts.P.F.find_o.
unfold Q_orderedExps.exprCompare.
rewrite e3; auto.
+ erewrite expr_compare_eq_eval_compat; eauto.
rewrite Q_orderedExps.exprCompare_eq_sym.
simpl.
rewrite e3; auto.
- simpl in e3.
rewrite andb_false_iff in e3.
destruct e3.
+ apply Ndec.Pcompare_Peqb in e6.
congruence.
+ apply N.compare_eq in Heq; subst.
rewrite N.eqb_refl in H; congruence.
- intros valid1; destruct valid1 as [validsub1 validr1].
specialize (IHc Heq validsub1).
split; auto.
destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
exists iv, err, vR.
intuition.
+ rewrite <- Hfind.
symmetry.
apply FloverMapFacts.P.F.find_o.
simpl.
rewrite e5; auto.
+ erewrite expr_compare_eq_eval_compat; eauto.
rewrite Q_orderedExps.exprCompare_eq_sym.
simpl.
rewrite e5; auto.
- intros valid1; destruct valid1 as [[_ [validsub1 validsub1']] validr1].
specialize (IHc e6 validsub1).
specialize (IHc0 Heq validsub1').
repeat split; auto; try congruence.
destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
exists iv, err, vR.
intuition.
+ rewrite <- Hfind.
symmetry.
apply FloverMapFacts.P.F.find_o.
simpl.
rewrite e6; auto.
+ erewrite expr_compare_eq_eval_compat; eauto.
rewrite Q_orderedExps.exprCompare_eq_sym.
simpl.
rewrite Heq, e6; auto.
- intros valid1; destruct valid1 as [[_ [validsub1 validsub1']] validr1].
specialize (IHc e6 validsub1).
specialize (IHc0 Heq validsub1').
repeat split; auto; try congruence.
destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
exists iv, err, vR.
intuition.
+ rewrite <- Hfind.
symmetry.
apply FloverMapFacts.P.F.find_o.
simpl.
rewrite e6; auto.
+ erewrite expr_compare_eq_eval_compat; eauto.
rewrite Q_orderedExps.exprCompare_eq_sym.
simpl.
rewrite Heq, e6; auto.
- intros valid1; destruct valid1 as [[_ [validsub1 validsub1']] validr1].
specialize (IHc e6 validsub1).
specialize (IHc0 Heq validsub1').
repeat split; auto; try congruence.
destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
exists iv, err, vR.
intuition.
+ rewrite <- Hfind.
symmetry.
apply FloverMapFacts.P.F.find_o.
simpl.
rewrite e6; auto.