Commit 61a5e249 authored by Heiko Becker's avatar Heiko Becker

Fix admits in RealRangeArith

parent 2fe03457
......@@ -3,7 +3,8 @@ From Coq
From Flover
Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps
Infra.Ltacs Infra.RealSimps TypeValidator ssaPrgs IntervalArithQ IntervalArith Commands.
Infra.Ltacs Infra.RealSimps TypeValidator ssaPrgs IntervalArithQ
IntervalArith Commands.
Definition dVars_range_valid (dVars:NatSet.t) (E:env) (A:analysisResult) :Prop :=
forall v, NatSet.In v dVars ->
......@@ -60,24 +61,24 @@ Proof.
destruct e; intros [_ valid_e]; simpl in *; try auto.
Qed.
(* Lemma validRanges_swap Gamma1 Gamma2: *)
(* forall e A E fBits, *)
(* (forall n, (toRMap Gamma1) n = toRMap (Gamma2) n) -> *)
(* validRanges e A E Gamma1 fBits -> *)
(* validRanges e A E Gamma2 fBits. *)
(* Proof. *)
(* induction e; intros * Gamma_swap valid1; simpl in *; try (split; auto); *)
(* try ( *)
(* destruct valid1 as [_ [? [? [? [? [? ?]]]]]]; *)
(* repeat eexists; eauto; *)
(* [eapply swap_Gamma_eval_expr with (Gamma1 := (toRMap Gamma1)); eauto | *)
(* lra | *)
(* lra]). *)
(* - destruct valid1; auto. *)
(* - destruct valid1 as [[? [? ?]] ?]; auto. *)
(* - destruct valid1 as [[? [? ?]] ?]; auto. *)
(* - destruct valid1; auto. *)
(* Qed. *)
Lemma validRanges_swap Gamma1 Gamma2:
forall e A E,
(forall n, (toRMap Gamma1) n = toRMap (Gamma2) n) ->
validRanges e A E Gamma1 ->
validRanges e A E Gamma2.
Proof.
induction e; intros * Gamma_swap valid1; simpl in *; try (split; auto);
try (
destruct valid1 as [_ [? [? [? [? [? ?]]]]]];
repeat eexists; eauto;
[eapply swap_Gamma_eval_expr with (Gamma1 := (toRMap Gamma1)); eauto |
lra |
lra]).
- destruct valid1; auto.
- destruct valid1 as [[? [? ?]] ?]; auto.
- destruct valid1 as [[? [? ?]] ?]; auto.
- destruct valid1; auto.
Qed.
Fixpoint validRangesCmd (f:cmd Q) A E Gamma {struct f} : Prop :=
match f with
......@@ -102,12 +103,12 @@ Proof.
destruct f; simpl in *; intros [ _ valid_f]; auto.
Qed.
(*
Lemma validRangesCmd_swap:
forall f A E Gamma1 Gamma2 fBits,
forall f A E Gamma1 Gamma2,
(forall n, (toRMap Gamma1) n = toRMap (Gamma2) n) ->
validRangesCmd f A E Gamma1 fBits ->
validRangesCmd f A E Gamma2 fBits.
validRangesCmd f A E Gamma1 ->
validRangesCmd f A E Gamma2.
Proof.
induction f; intros * Gamma_swap valid1; simpl in *; try (split; auto);
try (
......@@ -120,12 +121,11 @@ Proof.
+ eapply validRanges_swap; eauto.
+ intros. eapply IHf; [ | eapply valid_all_exec].
* intros x. unfold updDefVars.
destruct (x =? n) eqn:?; auto.
destruct (R_orderedExps.compare x (Var R n)) eqn:?; auto.
* eapply swap_Gamma_eval_expr with (Gamma1 := toRMap Gamma2); eauto.
- destruct valid1.
eapply validRanges_swap; eauto.
Qed.
*)
Lemma validRanges_eq_compat (e1: expr Q) e2 A E Gamma:
Q_orderedExps.eq e1 e2 ->
......@@ -303,24 +303,15 @@ Proof.
- split; auto.
destruct Hranges as [_ [iv [err [vR Hranges]]]].
exists iv, err, vR; intuition.
admit.
(* eapply swap_Gamma_eval_expr. *)
(* eapply Rmap_updVars_comm. *)
(* eapply eval_expr_ssa_extension; try eassumption. *)
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.
admit.
- admit.
- admit.
- admit.
- admit.
Admitted.
(*
(*
eapply swap_Gamma_eval_expr.
eapply Rmap_updVars_comm.
eapply eval_expr_ssa_extension; try eassumption. *)
eapply eval_expr_ssa_extension; try eassumption.
- simpl in Hsub.
destruct Hranges as [Hunopranges Hranges].
specialize (IHe Hsub Hunopranges).
......@@ -373,5 +364,4 @@ Admitted.
eapply Rmap_updVars_comm.
eapply eval_expr_ssa_extension; try eassumption.
rewrite usedVars_toREval_toRExp_compat; auto.
Qed.
*)
\ No newline at end of file
Qed.
\ No newline at end of file
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