Commit c5d1888c authored by Joachim Bard's avatar Joachim Bard

finally finishing proof of SMT checker function

parent 448e732c
......@@ -255,38 +255,9 @@ Definition eval_precond E (P: FloverMap.t intv) :=
*)
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)).
*)
forall e x iv, List.In (e, iv) (FloverMap.elements P)
-> (FloverMapFacts.P.F.eqb (Var Q x) e = true)
-> exists vR: R, E x = Some vR /\ Q2R (fst iv) <= vR <= Q2R (snd iv).
Definition addVarConstraint (el: expr Q * intv) q :=
match el with
......@@ -304,17 +275,18 @@ Proof.
induction (FloverMap.elements P) as [|[e [lo hi]] l IHl].
- intros. cbn. auto.
- intros H. cbn.
destruct e; try (apply IHl; intros; apply H; right; auto).
destruct e; try (apply IHl; intros e' x iv inl Heq; apply (H e'); cbn; auto).
repeat split.
+ 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'].
cbn. auto.
exists v, (Q2R hi). repeat split. 3: tauto. 1-2: constructor. tauto.
+ apply IHl. intros x iv inl. apply H. right. exact inl.
+ destruct (H (Var Q n) n (lo, hi)) as [v H']; cbn; auto.
* now rewrite eqb_cmp_eq, Q_orderedExps.exprCompare_refl.
* exists (Q2R lo), v. repeat split. 3: tauto. 1-2: constructor. tauto.
+ destruct (H (Var Q n) n (lo, hi)) as [v H']; cbn; auto.
* now rewrite eqb_cmp_eq, Q_orderedExps.exprCompare_refl.
* exists v, (Q2R hi). repeat split. 3: tauto. 1-2: constructor. tauto.
+ apply IHl. intros e x iv inl Heq. apply (H e); cbn; auto.
Qed.
(*
Lemma smt_to_pre_correct E P :
eval_smt_logic E (precond2SMT P) -> eval_precond E P.
Proof.
......@@ -334,6 +306,7 @@ Proof.
destruct e; cbn in H; auto.
apply H.
Qed.
*)
(* checker for precondition *)
Fixpoint checkPrelist (lP: list (FloverMap.key * intv)) q : bool :=
......@@ -416,7 +389,9 @@ Proof with try discriminate.
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 e as [x| | | | |].
all: cbn; try (intros H0 H1; apply IHl; auto; intros e' x iv Hin Heq;
apply (H1 e'); auto).
destruct q as [? ?|? ?|? ?| |?|q1 q2|? ?]...
intros chk H.
destruct q1 as [? ?|e1 e2|? ?| |?|? ?|? ?]...
......@@ -424,24 +399,26 @@ Proof with try discriminate.
destruct q2 as [? ?|? ?|? ?| |?|q1 q2|? ?]...
destruct q1 as [? ?|e1 e2|? ?| |?|? ?|? ?]...
destruct e1 as [|z| | | | |]... destruct e2 as [r'| | | | | |]...
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].
apply andb_prop in chk. destruct chk as [chk4 chk3].
apply andb_prop in chk as [chk chk0].
apply andb_prop in chk as [chk chk1].
apply andb_prop in chk as [chk chk2].
apply andb_prop in chk as [chk4 chk3].
apply beq_nat_true in chk4. apply beq_nat_true in chk3.
apply Qeq_bool_eq in chk2. apply Qeq_bool_eq in chk1.
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]]].
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]]].
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.
+ destruct (H (Var Q x) x (lo, hi)) as [v [H0 [H1 H2]]]; cbn; 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 (Var Q x) x (lo, hi)) as [v [H0 [H1 H2]]]; cbn; 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; auto.
intros. apply (H e); auto.
Qed.
(*
Lemma checkPre_smt_pre E P q :
checkPre P q = true -> eval_smt_logic E q -> eval_precond E P.
Proof with try discriminate.
......@@ -476,6 +453,7 @@ Proof with try discriminate.
+ apply andb_prop in chk. destruct chk as [chk chk0].
apply (IHl _ chk0); tauto.
Qed.
*)
Lemma precond_bound_correct E P preQ bound :
eval_precond E P
......
......@@ -226,8 +226,10 @@ Proof.
eapply toRExpMap_some in find_m; cbn; eauto.
match_simpl; auto.
+ Flover_compute.
destruct (valid_precond n i0) as [vR [env_valid bounds_valid]].
admit.
rewrite FloverMapFacts.P.F.elements_o in Heqo0.
apply findA_find in Heqo0 as [e' [? ?]].
apply find_some in H as [? ?].
destruct (valid_precond e' n i0) as [vR [env_valid bounds_valid]]; auto.
assert (NatSet.In n fVars) by set_tac.
canonize_hyps.
kill_trivial_exists.
......@@ -421,4 +423,4 @@ Proof.
try lra; try auto.
canonize_hyps.
cbn in *; lra.
Abort.
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