Commit 9cb08b00 authored by Joachim Bard's avatar Joachim Bard

fixing more admits

parent 87d71951
......@@ -276,7 +276,7 @@ Lemma meps_0_deterministic (f:expr R) (E:env) Gamma DeltaMap:
eval_expr E (toRTMap Gamma) DeltaMap (toREval f) v2 REAL ->
v1 = v2.
Proof.
induction f;
induction f in E |- *;
intros v1 v2 ev1 ev2.
- inversion ev1; inversion ev2; subst.
rewrite H1 in H6.
......@@ -284,9 +284,9 @@ Proof.
- inversion ev1; inversion ev2; subst.
simpl in *; subst; auto.
- inversion ev1; inversion ev2; subst; try congruence.
+ rewrite (IHf v0 v3); [ auto | |];
+ rewrite (IHf E v0 v3); [ auto | |];
destruct m, m0; cbn in *; congruence.
+ cbn in *. Flover_compute; rewrite (IHf v0 v3); [auto | | ];
+ cbn in *. Flover_compute; rewrite (IHf E v0 v3); [auto | | ];
destruct m, m0; cbn in *; congruence.
- inversion ev1; inversion ev2; subst.
assert (m0 = REAL) by (eapply toRTMap_eval_REAL; eauto).
......@@ -294,8 +294,8 @@ Proof.
assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m2 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst.
rewrite (IHf1 v0 v4); try auto.
rewrite (IHf2 v3 v5); try auto.
rewrite (IHf1 E v0 v4); try auto.
rewrite (IHf2 E v3 v5); try auto.
- inversion ev1; inversion ev2; subst.
assert (m0 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
......@@ -304,15 +304,35 @@ Proof.
assert (m4 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m5 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst.
rewrite (IHf1 v0 v5); try auto.
rewrite (IHf2 v3 v6); try auto.
rewrite (IHf3 v4 v7); try auto.
rewrite (IHf1 E v0 v5); try auto.
rewrite (IHf2 E v3 v6); try auto.
rewrite (IHf3 E v4 v7); try auto.
- inversion ev1; inversion ev2; subst.
apply REAL_least_precision in H3;
apply REAL_least_precision in H11; subst.
rewrite (IHf v0 v3); try auto.
rewrite (IHf E v0 v3); try auto.
- inversion ev1; inversion ev2.
assert (v0 = v3) by (eapply IHf1; eauto).
subst.
eapply IHf2; eauto.
- inversion ev1; inversion ev2; subst.
Admitted.
+ assert (m2 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m4 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst.
eapply IHf2; eauto.
+ assert (m0 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst. exfalso. apply H6.
eapply IHf1; eauto.
+ assert (m0 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst. exfalso. apply H17.
eapply IHf1; eauto.
+ assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m5 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst.
eapply IHf3; eauto.
Qed.
(**
Helping lemmas. Needed in soundness proof.
......@@ -436,7 +456,29 @@ Proof.
eauto;
hnf; intros; eapply no_usedVar;
set_tac.
Admitted.
- eapply Let_dist; eauto;
[ eapply IHe1; eauto; intros ?; apply no_usedVar; set_tac |].
destruct (n =? x) eqn: Heqx.
+ eapply eval_eq_env; try eassumption.
intros y. unfold updEnv. destruct (y =? n) eqn: Heqy; auto.
apply beq_nat_true in Heqx. subst. now rewrite Heqy.
+ eapply eval_eq_env; [|eapply IHe2; eauto].
instantiate (1 := v_new); instantiate (1 := x).
* intros y. unfold updEnv. destruct (y =? n) eqn: Heqy; auto.
apply beq_nat_true in Heqy. subst. now rewrite Heqx.
* intros ?. apply no_usedVar. set_tac.
right. apply beq_nat_false in Heqx. auto.
- eapply Cond_then; eauto;
[ eapply IHe1 | eapply IHe2];
eauto;
hnf; intros; eapply no_usedVar;
set_tac.
- eapply Cond_else; eauto;
[ eapply IHe1 | eapply IHe3];
eauto;
hnf; intros; eapply no_usedVar;
set_tac.
Qed.
Lemma eval_expr_det_ignore_bind2 e:
forall x v v_new m Gamma E DeltaMap,
......@@ -468,14 +510,35 @@ Proof.
eauto;
hnf; intros; eapply no_usedVar;
set_tac.
Admitted.
- eapply Let_dist; eauto;
[ eapply IHe1; eauto; intros ?; apply no_usedVar; set_tac |].
destruct (n =? x) eqn: Heqx.
+ eapply eval_eq_env; try eassumption.
intros y. unfold updEnv. destruct (y =? n) eqn: Heqy; auto.
apply beq_nat_true in Heqx. subst. now rewrite Heqy.
+ eapply IHe2. instantiate (1 := v_new); instantiate (1 := x).
* eapply eval_eq_env; try eassumption.
intros y. unfold updEnv. destruct (y =? n) eqn: Heqy; auto.
apply beq_nat_true in Heqy. subst. now rewrite Heqx.
* intros ?. apply no_usedVar. set_tac.
right. apply beq_nat_false in Heqx. auto.
- eapply Cond_then; eauto;
[ eapply IHe1 | eapply IHe2];
eauto;
hnf; intros; eapply no_usedVar;
set_tac.
- eapply Cond_else; eauto;
[ eapply IHe1 | eapply IHe3];
eauto;
hnf; intros; eapply no_usedVar;
set_tac.
Qed.
Lemma swap_Gamma_eval_expr e E vR m Gamma1 Gamma2 DeltaMap:
(forall e, Gamma1 e = Gamma2 e) ->
eval_expr E Gamma1 DeltaMap e vR m ->
eval_expr E Gamma2 DeltaMap e vR m.
Proof.
(*
revert E vR Gamma1 Gamma2 DeltaMap m;
induction e; intros * Gamma_eq eval_e;
inversion eval_e; subst; simpl in *;
......@@ -485,10 +548,12 @@ Proof.
| eapply Unop_inv'
| eapply Binop_dist'
| eapply Fma_dist'
| eapply Downcast_dist' ]; try eauto;
| eapply Downcast_dist'
| eapply Let_dist
| eapply Cond_then
| eapply Cond_else ]; try eauto;
rewrite <- Gamma_eq; auto.
*)
Admitted.
Qed.
Lemma Rmap_updVars_comm Gamma n m:
forall x,
......@@ -503,8 +568,8 @@ Lemma eval_expr_functional E Gamma DeltaMap e v1 v2 m:
eval_expr E Gamma DeltaMap e v2 m ->
v1 = v2.
Proof.
revert v1 v2 m.
induction e; intros v1 v2 m__FP Heval1 Heval2.
revert E v1 v2 m.
induction e; intros E v1 v2 m__FP Heval1 Heval2.
- inversion Heval1; inversion Heval2; subst.
now replace v1 with v2 by congruence.
- inversion Heval1; inversion Heval2; subst.
......@@ -527,14 +592,22 @@ Proof.
replace delta with delta0 by congruence.
f_equal; f_equal; eapply IHe; eauto;
erewrite Gamma_det; eauto.
Admitted.
- inversion Heval1; inversion Heval2; subst.
replace v0 with v3 in * by (eapply IHe1; eauto).
eapply IHe2; eauto.
- inversion Heval1; inversion Heval2; subst.
+ eapply IHe2; erewrite Gamma_det; eauto.
+ exfalso. apply H6. eapply IHe1; eauto. erewrite Gamma_det; eauto.
+ exfalso. apply H17. eapply IHe1; eauto. erewrite Gamma_det; eauto.
+ eapply IHe3; erewrite Gamma_det; eauto.
Qed.
Lemma real_eval_expr_ignores_delta_map (f:expr R) (E:env) Gamma:
forall v1 DeltaMap,
eval_expr E (toRTMap Gamma) DeltaMap (toREval f) v1 REAL ->
eval_expr E (toRTMap Gamma) DeltaMapR (toREval f) v1 REAL.
Proof.
induction f; unfold DeltaMapR;
induction f in E |- *; unfold DeltaMapR;
intros v1 DeltaMap ev1.
- inversion ev1; subst.
constructor; auto.
......@@ -544,18 +617,18 @@ Proof.
apply Rabs_0_impl_eq in H3; f_equal; now symmetry.
- inversion ev1; subst; try congruence.
+ unfold isCompat in H2; destruct m; cbn in H2; try congruence; clear H2.
specialize (IHf _ _ H5).
specialize (IHf _ _ _ H5).
eapply Unop_neg'; eauto.
+ unfold isCompat in H3; destruct m; cbn in H3; try congruence; clear H3.
specialize (IHf _ _ H5).
specialize (IHf _ _ _ H5).
eapply Unop_inv'; eauto.
apply Rabs_0_impl_eq in H4; f_equal; now symmetry.
- inversion ev1; subst.
assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m2 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst.
specialize (IHf1 _ _ H6).
specialize (IHf2 _ _ H9).
specialize (IHf1 _ _ _ H6).
specialize (IHf2 _ _ _ H9).
eapply Binop_dist'; eauto.
apply Rabs_0_impl_eq in H5; f_equal; now symmetry.
- inversion ev1; subst.
......@@ -563,18 +636,19 @@ Proof.
assert (m2 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst.
specialize (IHf1 _ _ H6).
specialize (IHf2 _ _ H9).
specialize (IHf3 _ _ H10).
specialize (IHf1 _ _ _ H6).
specialize (IHf2 _ _ _ H9).
specialize (IHf3 _ _ _ H10).
eapply Fma_dist'; eauto.
apply Rabs_0_impl_eq in H5; f_equal; now symmetry.
- inversion ev1; subst.
apply REAL_least_precision in H3; subst.
specialize (IHf _ _ H6).
specialize (IHf _ _ _ H6).
eapply Downcast_dist'; eauto.
+ trivial.
+ apply Rabs_0_impl_eq in H4; f_equal; now symmetry.
- admit.
- inversion ev1; subst.
econstructor; eauto. rewrite Rabs_R0. cbn. lra.
- inversion ev1; subst.
+ assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m2 = REAL) by (eapply toRTMap_eval_REAL; eauto).
......@@ -586,4 +660,4 @@ Proof.
subst.
eapply Cond_else; eauto.
cbn. rewrite Rabs_R0. lra.
Admitted.
Qed.
This diff is collapsed.
......@@ -46,7 +46,20 @@ Proof.
apply N.compare_eq in Heq; subst.
rewrite N.eqb_refl, Pos.eqb_refl in *.
destruct e5; congruence.
Admitted.
- apply Pos.compare_eq in e7.
apply N.compare_eq in Heq.
now subst.
- cbn in *.
rewrite Pos.eqb_compare in e3.
rewrite N.eqb_compare in e3.
rewrite Heq, e7 in e3.
discriminate.
- cbn in *.
rewrite Pos.eqb_compare in e3.
rewrite N.eqb_compare in e3.
rewrite Heq, e7 in e3.
discriminate.
Qed.
Lemma Qcompare_Rcompare q1 q2:
Qcompare q1 q2 = Rcompare (Q2R q1) (Q2R q2).
......@@ -70,7 +83,7 @@ Lemma QcompareExp_RcompareExp e1 e2:
Q_orderedExps.exprCompare e1 e2 = R_orderedExps.exprCompare (toRExp e1) (toRExp e2).
Proof.
functional induction (Q_orderedExps.exprCompare e1 e2); simpl in *; try auto; try congruence;
try rewrite e3;
try rewrite e3; try rewrite e4;
try rewrite <- IHc, e6; try auto.
- destruct (Qcompare v1 v2) eqn:q_comp; rewrite Qcompare_Rcompare in q_comp; auto.
- rewrite e6; auto.
......@@ -88,12 +101,12 @@ Proof.
- rewrite e5, e8; auto.
- rewrite e5, e8; auto.
- rewrite e5, e8; auto.
- rewrite <- IHc, e4; auto.
- rewrite <- IHc, e4; auto.
- rewrite <- IHc, e4; auto.
- rewrite e6; auto.
- rewrite e6; auto.
- rewrite e6; auto.
- rewrite <- IHc, e5; auto.
- rewrite <- IHc, e5; auto.
- rewrite <- IHc, e5; auto.
- rewrite e7; auto.
- rewrite e7; auto.
- rewrite e7; auto.
- rewrite <- IHc, <- IHc0, e3, e4; auto.
- rewrite <- IHc, <- IHc0, e3, e4; auto.
- rewrite <- IHc, <- IHc0, e3, e4; auto.
......@@ -165,13 +178,27 @@ Proof.
congruence.
+ apply N.compare_eq in Heq; subst.
rewrite N.eqb_refl in H; congruence.
- specialize (IHc e4).
- specialize (IHc e5).
specialize (IHc0 Heq).
apply NatSet.eq_leibniz in IHc.
apply NatSet.eq_leibniz in IHc0.
simpl.
rewrite IHc, IHc0.
Admitted.
apply nat_compare_eq in e4.
now rewrite IHc, IHc0, e4.
- cbn in *.
rewrite Pos.eqb_compare in e3.
rewrite N.eqb_compare in e3.
rewrite Heq, e7 in e3.
discriminate.
- 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.
Qed.
Lemma freeVars_toREval_toRExp_compat e:
freeVars (toREval (toRExp e)) = freeVars e.
......@@ -437,8 +464,14 @@ Proof.
- 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.
- rewrite e4, IHc, IHc0; auto.
- cbn in *.
rewrite Pos.eqb_compare in e3.
rewrite N.eqb_compare in e3.
rewrite H, e7 in e3.
discriminate.
- rewrite IHc, IHc0; auto.
Admitted.
Qed.
Lemma no_cycle_unop e:
forall u, Q_orderedExps.exprCompare e (Unop u e) <> Eq.
......
......@@ -3,7 +3,8 @@
Used in soundness proofs for error bound validator.
**)
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.Qreals.
Require Import Flover.Infra.Abbrevs Flover.Infra.RealSimps.
Require Import Flover.Infra.Abbrevs Flover.Infra.RealSimps Flover.IntervalArithQ
Flover.Infra.RealRationalProps.
(**
Define validity of an interval, requiring that the lower bound is less than or equal to the upper bound.
......@@ -103,6 +104,18 @@ Proof.
+ apply (Rle_trans _ (Rmax b (Rmax c d)) _); auto. apply Rmax_r.
Qed.
Corollary Q2R_max4 a b c d:
Q2R (IntervalArithQ.max4 a b c d) = max4 (Q2R a) (Q2R b) (Q2R c) (Q2R d).
Proof.
unfold IntervalArithQ.max4, max4; repeat rewrite Q2R_max; auto.
Qed.
Corollary Q2R_min4 a b c d:
Q2R (IntervalArithQ.min4 a b c d) = min4 (Q2R a) (Q2R b) (Q2R c) (Q2R d).
Proof.
unfold IntervalArithQ.min4, min4; repeat rewrite Q2R_min; auto.
Qed.
(**
Asbtract interval update function, parametric by actual operator applied.
**)
......
......@@ -102,15 +102,17 @@ Fixpoint validIntervalbounds (e:expr Q) (A:analysisResult) (P: FloverMap.t intv)
else
false
| Let _ x e1 e2 =>
match FloverMap.find e1 A, FloverMap.find (Var Q x) A with
| Some ((e_lo,e_hi), _), Some ((x_lo, x_hi), _) =>
if (validIntervalbounds e1 A P validVars &&
Qeq_bool (e_lo) (x_lo) &&
Qeq_bool (e_hi) (x_hi))
then validIntervalbounds e2 A P (NatSet.add x validVars)
else false
| _, _ => false
end
if validIntervalbounds e1 A P validVars &&
validIntervalbounds e2 A P (NatSet.add x validVars)
then
match FloverMap.find e1 A, FloverMap.find (Var Q x) A, FloverMap.find e2 A with
| Some ((e_lo,e_hi), _), Some ((x_lo, x_hi), _), Some (iv2, _) =>
Qeq_bool (e_lo) (x_lo) &&
Qeq_bool (e_hi) (x_hi) &&
isSupersetIntv iv2 intv
| _, _, _ => false
end
else false
| Cond f1 f2 f3 => false
(*
if ((validIntervalbounds f1 A P validVars) &&
......@@ -128,18 +130,6 @@ Fixpoint validIntervalbounds (e:expr Q) (A:analysisResult) (P: FloverMap.t intv)
end
end.
Corollary Q2R_max4 a b c d:
Q2R (IntervalArithQ.max4 a b c d) = max4 (Q2R a) (Q2R b) (Q2R c) (Q2R d).
Proof.
unfold IntervalArithQ.max4, max4; repeat rewrite Q2R_max; auto.
Qed.
Corollary Q2R_min4 a b c d:
Q2R (IntervalArithQ.min4 a b c d) = min4 (Q2R a) (Q2R b) (Q2R c) (Q2R d).
Proof.
unfold IntervalArith.min4, min4; repeat rewrite Q2R_min; auto.
Qed.
Lemma validBoundsDiv_uneq_zero e1 e2 A P V ivlo_e2 ivhi_e2 err:
FloverMap.find (elt:=intv * error) e2 A = Some ((ivlo_e2,ivhi_e2), err) ->
validIntervalbounds (Binop Div e1 e2) A P V = true ->
......@@ -400,53 +390,56 @@ Proof.
cbn; rewrite Rabs_R0. lra.
- destruct types_defined
as [mG [find_mG [[validt_f1 [validt_f2 valid_join]] valid_exec]]].
Flover_compute; try congruence.
inversion ssa_f; subst.
canonize_hyps.
assert (validRanges f1 A E (toRTMap (toRExpMap Gamma))) as valid_f1
by (Flover_compute; try congruence; eapply IHf1; eauto; set_tac).
split; [split;auto|].
+ intros. Flover_compute.
pose proof (validRanges_single _ _ _ _ valid_f1) as valid_single_f1.
destruct valid_single_f1 as [iv_f1 [err_v [v [find_v [eval_f1 valid_bounds_f1]]]]].
eapply IHf2; eauto.
* eapply ssa_equal_set; eauto. admit.
* intros v0 mem_v0.
pose proof (validRanges_single _ _ _ _ valid_f1) as valid_single_f1.
destruct valid_single_f1 as [iv_f1 [err_f1 [v [find_v [eval_f1 valid_bounds_f1]]]]].
rewrite find_v in *; inversion Heqo0; subst.
assert (validRanges f2 A (updEnv n v E) (toRTMap (toRExpMap Gamma))) as valid_f2.
{ eapply IHf2; eauto.
- eapply ssa_equal_set; eauto.
intros x. split; set_tac; intros; tauto.
- intros v0 mem_v0.
unfold updEnv.
case_eq (v0 =? n); intros v0_eq.
{ rename R1 into eq_lo;
rename R0 into eq_hi.
+ rename L1 into eq_lo;
rename R into eq_hi.
rewrite Nat.eqb_eq in v0_eq; subst.
canonize_hyps.
admit.
(*
assert (vR = v) by (eapply meps_0_deterministic; eauto); subst.
exists v, iv_f1. eexists.
repeat split; try lra.
*)
}
{ apply valid_definedVars.
exists v; eexists; eexists. repeat split; eauto; simpl in *; lra.
+ apply valid_definedVars.
set_tac.
destruct mem_v0 as [? | [? ?]]; try auto.
rewrite Nat.eqb_neq in v0_eq.
congruence. }
* intros x x_contained.
congruence.
- intros x x_contained.
set_tac.
repeat split; try auto.
{ right. split; auto. intros Heq; subst. apply H1; set_tac. }
{ hnf; intros. apply H1; set_tac. }
* hnf. intros x ? ?.
repeat split; auto.
+ right. split; auto. hnf; intros. apply H0; set_tac.
+ hnf; intros. apply H0; set_tac.
- hnf. intros x ? ?.
unfold updEnv.
case_eq (x =? n); intros case_x; auto.
rewrite Nat.eqb_eq in case_x. subst.
set_tac.
assert (NatSet.In n fVars) as in_free
by (apply preVars_free; eapply preIntvVars_sound; eauto).
(* by (destruct (fVars_valid n iv); auto; set_tac). *)
exfalso. apply H5. set_tac.
+ Flover_compute.
kill_trivial_exists.
admit.
exfalso. apply H5. set_tac. }
repeat split; auto.
+ intros vR ?.
assert (vR = v) by (eapply meps_0_deterministic; eauto); now subst.
+ apply validRanges_single in valid_f2.
destruct valid_f2 as [? [? [v2 [find_v2 [? ?]]]]].
rewrite find_v2 in *; inversion Heqo2; subst.
cbn in *.
eexists. eexists. exists v2.
repeat split; eauto; try lra.
econstructor; eauto; try reflexivity.
rewrite Rabs_R0. cbn; lra.
- Flover_compute. congruence.
Admitted.
Qed.
(*
Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult):
......
......@@ -179,7 +179,8 @@ Lemma validRanges_eq_compat (e1: expr Q) e2 A E Gamma:
Proof.
intros Heq.
unfold Q_orderedExps.eq in Heq.
functional induction (Q_orderedExps.exprCompare e1 e2); try congruence.
revert E.
functional induction (Q_orderedExps.exprCompare e1 e2); intros E; try congruence.
- simpl.
intros [_ validr1].
repeat split; auto.
......@@ -210,7 +211,7 @@ Proof.
+ 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).
specialize (IHc Heq E validsub1).
split; auto.
destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
exists iv, err, vR.
......@@ -225,8 +226,8 @@ Proof.
simpl.
rewrite e5; auto.
- intros valid1; destruct valid1 as [[_ [validsub1 validsub1']] validr1].
specialize (IHc e6 validsub1).
specialize (IHc0 Heq validsub1').
specialize (IHc e6 E validsub1).
specialize (IHc0 Heq E validsub1').
repeat split; auto; try congruence.
destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
exists iv, err, vR.
......@@ -241,8 +242,8 @@ Proof.
simpl.
rewrite Heq, e6; auto.
- intros valid1; destruct valid1 as [[_ [validsub1 validsub1']] validr1].
specialize (IHc e6 validsub1).
specialize (IHc0 Heq validsub1').
specialize (IHc e6 E validsub1).
specialize (IHc0 Heq E validsub1').
repeat split; auto; try congruence.
destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
exists iv, err, vR.
......@@ -257,8 +258,8 @@ Proof.
simpl.
rewrite Heq, e6; auto.
- intros valid1; destruct valid1 as [[_ [validsub1 validsub1']] validr1].
specialize (IHc e6 validsub1).
specialize (IHc0 Heq validsub1').
specialize (IHc e6 E validsub1).
specialize (IHc0 Heq E validsub1').
repeat split; auto; try congruence.
destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
exists iv, err, vR.
......@@ -273,8 +274,8 @@ Proof.
simpl.
rewrite Heq, e6; auto.
- intros valid1; destruct valid1 as [[Hdiv [validsub1 validsub1']] validr1].
specialize (IHc e6 validsub1).
specialize (IHc0 Heq validsub1').
specialize (IHc e6 E validsub1).
specialize (IHc0 Heq E validsub1').
repeat split; auto.
{
intros Hrefl; specialize (Hdiv Hrefl).
......@@ -296,9 +297,9 @@ Proof.
simpl.
rewrite Heq, e6; auto.
- intros valid1; destruct valid1 as [[validsub1 [validsub1' validsub1'']] validr1].
specialize (IHc e3 validsub1).
specialize (IHc0 e4 validsub1').
specialize (IHc1 Heq validsub1'').
specialize (IHc e3 E validsub1).
specialize (IHc0 e4 E validsub1').
specialize (IHc1 Heq E validsub1'').
repeat split; auto; try congruence.
destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
exists iv, err, vR.
......@@ -313,7 +314,7 @@ Proof.
simpl.
rewrite Heq, e3, e4; auto.
- intros valid1; destruct valid1 as [validsub1 validr1].
specialize (IHc Heq validsub1).
specialize (IHc Heq E validsub1).
split; auto.
destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
exists iv, err, vR.
......@@ -334,7 +335,50 @@ Proof.
congruence.
+ apply N.compare_eq in Heq; subst.
rewrite N.eqb_refl in *; congruence.
Admitted.
- intros valid1; destruct valid1 as [[validsub1 validsub2] validr1].
destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
apply nat_compare_eq in e4; subst.
repeat split; auto.
+ intros v ?.
eapply IHc0; eauto.
apply validsub2.
erewrite expr_compare_eq_eval_compat; eauto.
+ exists iv, err, vR.
intuition.
* rewrite <- Hfind.
symmetry.
apply FloverMapFacts.P.F.find_o.
simpl.
rewrite e3, e5.
rewrite Nat.compare_refl; auto.
* erewrite expr_compare_eq_eval_compat; eauto.
rewrite Q_orderedExps.exprCompare_eq_sym.
simpl.
rewrite e3, e5.
rewrite Nat.compare_refl; auto.
- cbn in * |-.
rewrite Pos.eqb_compare in e3.
rewrite N.eqb_compare in e3.
rewrite Heq, e7 in e3.
discriminate.
- intros valid1; destruct valid1 as [[validsub1 [validsub1' validsub1'']] validr1].
specialize (IHc e3 E validsub1).
specialize (IHc0 e4 E validsub1').
specialize (IHc1 Heq E 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 e3, e4, Heq; auto.
+ erewrite expr_compare_eq_eval_compat; eauto.
rewrite Q_orderedExps.exprCompare_eq_sym.
simpl.
rewrite Heq, e3, e4; auto.
Qed.
Lemma validRanges_ssa_extension (e: expr Q) (e' : expr Q) A E Gamma
vR' m n c fVars dVars outVars:
......
......@@ -8,15 +8,15 @@ From Flover
From Coq Require Export QArith.QArith.
From Flover
Require Export IntervalValidation SMTArith
Require Export IntervalValidation SMTArith SMTValidation
RealRangeArith Infra.ExpressionAbbrevs.
Definition RangeValidator e A (P: precond) (Qmap: usedQueries) dVars :=
validIntervalbounds e A (fst P) dVars.
(*
if
validIntervalbounds e A (fst P) dVars
then true
else validSMTIntervalbounds e A P Qmap (fun _ => None) dVars.
(*
else match validAffineBounds e A (fst P) dVars (FloverMap.empty (affine_form Q)) 1 with
| Some _ => true
| None => validSMTIntervalbounds e A P Qmap (fun _ => None) dVars
......@@ -43,7 +43,8 @@ Proof.
- destruct pre_valid. eapply validIntervalbounds_sound; eauto.
revert preVars_free. apply NatSetProps.subset_trans.
unfold preVars. apply NatSetProps.union_subset_1.
- cbn in *. congruence.
- cbn in *. rewrite Hivcheck in range_valid.
eapply validSMTIntervalbounds_sound; eauto; congruence.
(*
intros range_valid dVars_valid affine_dVars_valid types_valid pre_valid unsat_qs.
unfold RangeValidator in *.
......
This diff is collapsed.
......@@ -426,7 +426,37 @@ Proof.
[ | destruct (morePrecise m1 m && true) eqn:?; try congruence];
unfold_addMono; try eauto;
by_monotonicity find_akk Hmem.
Admitted.
- destruct (mTypeEq m m1) eqn:?; try congruence. type_conv; subst.
unfold_addMono.
eapply IHe2; eauto.
replace t0 with (FloverMap.add (Var Q n) m1 t) by congruence.
rewrite map_find_add.
destruct (Q_orderedExps.compare (Var Q n) e) eqn:?; eauto.
assert (FloverMap.find (Var Q n) akk = Some m0)
as in_akk
by (erewrite FloverMapFacts.P.F.find_o; eauto).
eapply IHe1 in in_akk; eauto.
congruence.
- destruct (mTypeEq m m1) eqn:?; congruence.
- destruct (mTypeEq m m1) eqn:?; congruence.
- destruct (isFixedPointB m1 && isFixedPointB m2) eqn:?;
try congruence;
destruct (morePrecise m1 m3 && morePrecise m2 m3) eqn:?;
try congruence;
unfold_addMono; try eauto;
by_monotonicity find_akk Hmem.
- destruct (isFixedPointB m1 && isFixedPointB m2) eqn:?;
try congruence;
destruct (morePrecise m1 m3 && morePrecise m2 m3) eqn:?;
try congruence;
unfold_addMono; try eauto;
by_monotonicity find_akk Hmem.
- destruct (isFixedPointB m1 && isFixedPointB m2) eqn:?;
try congruence;
unfold_addMono; try eauto;
by_monotonicity find_akk Hmem.