Commit 112ec621 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Move auxiliary lemmas from AffineValidation to more appropriate places

parent ad80ecfc
This diff is collapsed.
......@@ -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) =>
......
......@@ -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.
+ erewrite expr_compare_eq_eval_compat; eauto.
rewrite Q_orderedExps.exprCompare_eq_sym.
simpl.
rewrite Heq, e6; auto.
- intros valid1; destruct valid1 as [[Hdiv [validsub1 validsub1']] validr1].
specialize (IHc e6 validsub1).
specialize (IHc0 Heq validsub1').
repeat split; auto.
{
intros Hrefl; specialize (Hdiv Hrefl).
intros iv2 err Hfind.
erewrite FloverMapFacts.P.F.find_o with (y := e12) in Hfind.
eapply Hdiv; eauto.
now rewrite Q_orderedExps.exprCompare_eq_sym.
}
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' validsub1'']] validr1].
specialize (IHc e3 validsub1).
specialize (IHc0 e4 validsub1').
specialize (IHc1 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 e3, e4, Heq; auto.
+ erewrite expr_compare_eq_eval_compat; eauto.
rewrite Q_orderedExps.exprCompare_eq_sym.
simpl.
rewrite Heq, e3, e4; auto.
- 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.
- 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 *; congruence.
Qed.
Lemma validRanges_ssa_extension (e: expr Q) (e' : expr Q) A E Gamma fBits vR' m n c fVars dVars outVars:
ssa (Let m n e' c) (fVars dVars) outVars ->
NatSet.Subset (usedVars e) (fVars dVars) ->
~ (n fVars dVars) ->
validRanges e A E Gamma fBits ->
validRanges e A (updEnv n vR' E) (updDefVars n REAL Gamma) fBits.
Proof.
intros Hssa Hsub Hnotin Hranges.
induction e.
- split; auto.
destruct Hranges as [_ [iv [err [vR Hranges]]]].
exists iv, err, vR; intuition.
eapply swap_Gamma_eval_expr.
eapply Rmap_updVars_comm.
eapply eval_expr_ssa_extension; try eassumption.
- split; auto.
destruct Hranges as [_ [iv [err [vR Hranges]]]].
exists iv, err, vR; intuition.
eapply swap_Gamma_eval_expr.
eapply Rmap_updVars_comm.
eapply eval_expr_ssa_extension; try eassumption.
- simpl in Hsub.
destruct Hranges as [Hunopranges Hranges].
specialize (IHe Hsub Hunopranges).
split; auto.
destruct Hranges as [iv [err [vR Hranges]]].
exists iv, err, vR; intuition.
eapply swap_Gamma_eval_expr.
eapply Rmap_updVars_comm.
eapply eval_expr_ssa_extension; try eassumption.
rewrite usedVars_toREval_toRExp_compat; auto.
- simpl in Hsub.
assert (NatSet.Subset (usedVars e1) (fVars dVars)) as Hsub1 by set_tac.
assert (NatSet.Subset (usedVars e2) (fVars dVars)) as Hsub2 by (clear Hsub1; set_tac).
destruct Hranges as [[Hdiv [Hranges1 Hranges2]] Hranges].
specialize (IHe1 Hsub1 Hranges1).
specialize (IHe2 Hsub2 Hranges2).
simpl.
repeat split; auto.
destruct Hranges as [iv [err [vR Hranges]]].
exists iv, err, vR; intuition.
eapply swap_Gamma_eval_expr.
eapply Rmap_updVars_comm.
eapply eval_expr_ssa_extension; try eassumption.
simpl.
repeat rewrite usedVars_toREval_toRExp_compat; auto.
- simpl in Hsub.
assert (NatSet.Subset (usedVars e1) (fVars dVars)) as Hsub1 by set_tac.
assert (NatSet.Subset (usedVars e2) (fVars dVars)) as Hsub2 by (clear Hsub1; set_tac).
assert (NatSet.Subset (usedVars e3) (fVars dVars)) as Hsub3 by (clear Hsub1 Hsub2; set_tac).
destruct Hranges as [[Hranges1 [Hranges2 Hranges3]] Hranges].
specialize (IHe1 Hsub1 Hranges1).
specialize (IHe2 Hsub2 Hranges2).
specialize (IHe3 Hsub3 Hranges3).
simpl.
repeat split; auto.
destruct Hranges as [iv [err [vR Hranges]]].
exists iv, err, vR; intuition.
eapply swap_Gamma_eval_expr.
eapply Rmap_updVars_comm.
eapply eval_expr_ssa_extension; try eassumption.
simpl.
repeat rewrite usedVars_toREval_toRExp_compat; auto.
- simpl in Hsub.
destruct Hranges as [Hranges' Hranges].
specialize (IHe Hsub Hranges').
split; auto.
destruct Hranges as [iv [err [vR Hranges]]].
exists iv, err, vR; intuition.
eapply swap_Gamma_eval_expr.
eapply Rmap_updVars_comm.
eapply eval_expr_ssa_extension; try eassumption.
rewrite usedVars_toREval_toRExp_compat; auto.
Qed.
......@@ -45,8 +45,8 @@ Proof.
assert (1 > 0)%nat as Hinoise by omega.
eassert (forall n : nat, (n >= 1)%nat -> imap n = None) as Himap by trivial.
assert (NatSet.Subset (usedVars e -- dVars) (usedVars e)) as Hsubset by set_tac.
assert (affine_fVars_P_sound (usedVars e) E P) as HfVars by exact H2.
assert (affine_vars_typed (usedVars e dVars) Gamma) as Hvarstyped
assert (fVars_P_sound (usedVars e) E P) as HfVars by exact H2.
assert (vars_typed (usedVars e dVars) Gamma) as Hvarstyped
by exact H3.
specialize (sound_affine e A P (usedVars e) dVars E Gamma fBits
exprAfs noise iexpmap inoise imap
......@@ -95,8 +95,8 @@ Proof.
congruence).
assert (1 > 0)%nat as Hinoise by omega.
eassert (forall n : nat, (n >= 1)%nat -> imap n = None) as Himap by trivial.
assert (affine_fVars_P_sound fVars E P) as HfVars by exact H2.
assert (affine_vars_typed (fVars dVars) Gamma) as Hvarstyped
assert (fVars_P_sound fVars E P) as HfVars by exact H2.
assert (vars_typed (fVars dVars) Gamma) as Hvarstyped
by exact H3.
specialize (sound_affine f A P fBits fVars dVars outVars E Gamma
exprAfs noise iexpmap inoise imap
......
......@@ -210,6 +210,18 @@ Proof.
set_tac.
Qed.
Lemma eval_expr_ssa_extension (e: expr R) (e' : expr Q) E Gamma fBits vR vR' m n c fVars dVars outVars:
ssa (Let m n e' c) (fVars dVars) outVars ->
NatSet.Subset (usedVars e) (fVars dVars) ->
~ (n fVars dVars) ->
eval_expr E Gamma fBits e vR REAL ->
eval_expr (updEnv n vR' E) (updDefVars n REAL Gamma) fBits e vR REAL.
Proof.
intros Hssa Hsub Hnotin Heval.
eapply eval_expr_ignore_bind; [auto |].
edestruct ssa_inv_let; eauto.
Qed.
(*
Lemma shadowing_free_rewriting_expr e v E1 E2 defVars:
(forall n, E1 n = E2 n)->
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment