Commit e48791c8 authored by Joachim Bard's avatar Joachim Bard

different versions of eval_precond

parent 32ed187d
......@@ -248,9 +248,45 @@ Inductive eval_smt_logic (E: env) : SMTLogic -> Prop :=
| OrQ_eval_r q1 q2 : eval_smt_logic E q2 -> eval_smt_logic E (OrQ q1 q2).
*)
(*
Definition eval_precond E (P: FloverMap.t intv) :=
forall x lo hi, (List.In (Var Q x, (lo, hi)) (FloverMap.elements P))
-> exists vR: R, E x = Some vR /\ Q2R lo <= vR <= Q2R hi.
forall x iv, FloverMap.find (Var Q x) P = Some iv
-> exists vR: R, E x = Some vR /\ Q2R (fst iv) <= vR <= Q2R (snd iv).
*)
Definition eval_precond E (P: FloverMap.t intv) :=
forall x iv, List.In (Var Q x, iv) (FloverMap.elements P)
-> exists vR: R, E x = Some vR /\ Q2R (fst iv) <= vR <= Q2R (snd iv).
(*
Lemma find_elements X m k (x: X) :
FloverMap.find k m = Some x -> List.In (k, x) (FloverMap.elements m).
Proof.
destruct m. induction this; try discriminate.
cbn. rewrite FloverMap.Raw.Proofs.elements_app.
inversion is_bst. intros ?. apply List.in_or_app.
destruct (legacy_OrderedQExps.compare k k0).
- left. now apply (IHthis1 H3).
- right. left. assert (e = x) by congruence. subst. admit.
- right. right. now apply (IHthis2 H5).
Admitted.
Lemma eval_precond_equiv E P : eval_precond E P <-> eval_precond_list E P.
Proof.
split.
- intros H x iv H'. apply H. admit.
- intros H x iv H'. apply H. now apply find_elements.
Admitted.
*)
(*
Definition eval_precond_fVars (fVars:NatSet.t) (E:env) (P: FloverMap.t intv) :=
forall v iv,
NatSet.In v fVars ->
FloverMap.find (Var Q v) P = Some iv ->
exists vR, E v = Some vR /\
(Q2R (fst iv) <= vR <= Q2R (snd iv)).
*)
Definition addVarConstraint (el: expr Q * intv) q :=
match el with
......@@ -270,13 +306,13 @@ Proof.
- intros H. cbn.
destruct e; try (apply IHl; intros; apply H; right; auto).
repeat split.
+ destruct (H n lo hi) as [v H'].
+ destruct (H n (lo, hi)) as [v H'].
cbn. auto.
exists (Q2R lo), v. repeat split. 3: tauto. 1-2: constructor. tauto.
+ destruct (H n lo hi) as [v H'].
+ destruct (H n (lo, hi)) as [v H'].
cbn. auto.
exists v, (Q2R hi). repeat split. 3: tauto. 1-2: constructor. tauto.
+ apply IHl. intros x lo' hi' inl. apply H. right. exact inl.
+ apply IHl. intros x iv inl. apply H. right. exact inl.
Qed.
Lemma smt_to_pre_correct E P :
......@@ -285,7 +321,7 @@ Proof.
unfold precond2SMT, eval_precond.
induction (FloverMap.elements P) as [|? l IHl].
- cbn. tauto.
- cbn. intros H x lo hi [hd | inl].
- cbn. intros H x [lo hi] [hd | inl].
+ subst. cbn in H. destruct H as [H1 [H2 H3]].
destruct H1 as [v1 [v2 H1]].
exists v2. repeat split; destruct H1 as [lov1 [xv2 leq]].
......@@ -362,16 +398,28 @@ Proof.
now rewrite Nat.eqb_refl, !Qeq_bool_refl, IHl.
Qed.
(*
Lemma convert_eval_precond E P :
eval_precond E P <-> forall (x : nat) (iv : intv),
SetoidList.findA (FloverMapFacts.P.F.eqb (Var Q x)) (FloverMap.elements (elt:=intv) P) = Some iv ->
exists vR : R, E x = Some vR /\ Q2R (fst iv) <= vR <= Q2R (snd iv).
Proof.
unfold eval_precond. split.
- intros H x iv. rewrite <- FloverMapFacts.P.F.elements_o. auto.
- intros H x iv. rewrite FloverMapFacts.P.F.elements_o. auto.
Qed.
*)
Lemma checkPre_pre_smt E P q :
checkPre P q = true -> eval_precond E P -> eval_smt_logic E q.
Proof with try discriminate.
unfold eval_precond, checkPre.
unfold checkPre, eval_precond.
induction (FloverMap.elements P) as [|[e [lo hi]] l IHl] in q |- *.
- destruct q; cbn; intros chk... now auto.
- destruct e as [x| | | | |]; cbn; auto.
destruct q as [? ?|? ?|? ?| |?|q1 q2|? ?]...
intros chk H.
destruct q1 as [? ?|e1 e2|? ?| |?|? ?|? ?]; try now apply (IHl (AndQ _ _)).
destruct q1 as [? ?|e1 e2|? ?| |?|? ?|? ?]...
destruct e1 as [r| | | | | |]... destruct e2 as [|y| | | | |]...
destruct q2 as [? ?|? ?|? ?| |?|q1 q2|? ?]...
destruct q1 as [? ?|e1 e2|? ?| |?|? ?|? ?]...
......@@ -385,11 +433,13 @@ Proof with try discriminate.
rewrite <- chk3, <- chk4.
apply Qeq_sym in chk2. apply Qeq_sym in chk1.
repeat split.
+ destruct (H x lo hi) as [v [H0 [H1 H2]]]; auto.
+ destruct (H x (lo, hi)) as [v [H0 [H1 H2]]].
1: auto. (* now rewrite eqb_cmp_eq, Q_orderedExps.exprCompare_refl. *)
exists (Q2R r), v. repeat split; try now constructor. erewrite Qeq_eqR; now eauto.
+ destruct (H x lo hi) as [v [H0 [H1 H2]]]; auto.
+ destruct (H x (lo, hi)) as [v [H0 [H1 H2]]].
1: auto. (* now rewrite eqb_cmp_eq, Q_orderedExps.exprCompare_refl. *)
exists v, (Q2R r'). repeat split; try now constructor. erewrite Qeq_eqR; now eauto.
+ apply IHl; now auto.
+ apply IHl; auto.
Qed.
Lemma checkPre_smt_pre E P q :
......@@ -399,14 +449,14 @@ Proof with try discriminate.
induction (FloverMap.elements P) as [|[e [lo hi]] l IHl] in q |- *.
- destruct q; cbn; intros chk; try discriminate. tauto.
- destruct e as [x| | | | |];
try (intros chk H ? ? ? [?|?]; [discriminate| apply (IHl _ chk); auto]).
try (intros chk H ? ? [?|?]; [discriminate| apply (IHl _ chk); auto]).
destruct q as [? ?|? ?|? ?| |?|q1 q2|? ?]...
destruct q1 as [? ?|e1 e2|? ?| |?|? ?|? ?]...
destruct e1 as [r| | | | | |]... destruct e2 as [|y| | | | |]...
destruct q2 as [? ?|? ?|? ?| |?|q1 q2|? ?]...
destruct q1 as [? ?|e1 e2|? ?| |?|? ?|? ?]...
destruct e1 as [|z| | | | |]... destruct e2 as [r'| | | | | |]...
cbn. intros chk H x' lo' hi' [eq|inl].
cbn. intros chk H x' [lo' hi'] [eq|inl].
+ apply andb_prop in chk. destruct chk as [chk chk0].
apply andb_prop in chk. destruct chk as [chk chk1].
apply andb_prop in chk. destruct chk as [chk chk2].
......@@ -421,7 +471,7 @@ Proof with try discriminate.
subst.
inversion H1. inversion H2. inversion H1'. inversion H2'.
assert (v2 = v1') by congruence.
subst. rewrite (Qeq_eqR _ _ chk2). rewrite (Qeq_eqR _ _ chk1).
subst. cbn. rewrite (Qeq_eqR _ _ chk2). rewrite (Qeq_eqR _ _ chk1).
exists v1'. repeat split; auto.
+ apply andb_prop in chk. destruct chk as [chk chk0].
apply (IHl _ chk0); tauto.
......@@ -464,4 +514,4 @@ Proof.
apply Rnot_lt_le. intros B.
apply H3. eapply precond_bound_correct; eauto.
do 2 eexists. repeat split; first [eassumption | constructor].
Qed.
\ No newline at end of file
Qed.
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