Commit bb57ac76 authored by Joachim Bard's avatar Joachim Bard
Browse files

simplifications

parent 71a45a2f
...@@ -603,9 +603,16 @@ Proof with try discriminate. ...@@ -603,9 +603,16 @@ Proof with try discriminate.
Qed. Qed.
*) *)
(*
Lemma checkPre_smt_pre E P q : Lemma checkPre_smt_pre E P q :
checkPre P q = true -> eval_smt_logic E q -> eval_precond E P. checkPre P q = true ->
eval_smt_logic E q ->
eval_precond E P.
Proof.
intros Heq Hq.
apply smt_to_pre_correct.
now apply (SMTLogic_eqb_sound _ _ _ Heq).
Qed.
(*
Proof with try discriminate. Proof with try discriminate.
unfold P_intv_sound, checkPre. unfold P_intv_sound, checkPre.
induction (FloverMap.elements P) as [|[e [lo hi]] l IHl] in q |- *. induction (FloverMap.elements P) as [|[e [lo hi]] l IHl] in q |- *.
...@@ -663,7 +670,7 @@ Proof. ...@@ -663,7 +670,7 @@ Proof.
apply Rnot_lt_le. intros B. apply Rnot_lt_le. intros B.
apply H2. eapply precond_bound_correct; eauto. apply H2. eapply precond_bound_correct; eauto.
split; cbn; auto. split; cbn; auto.
do 2 eexists. repeat split; first [eassumption | constructor]. exists v, (Q2R r). repeat split; auto. constructor.
Qed. Qed.
Lemma RangeBound_high_sound E P preQ e r Gamma v : Lemma RangeBound_high_sound E P preQ e r Gamma v :
...@@ -678,5 +685,5 @@ Proof. ...@@ -678,5 +685,5 @@ Proof.
apply Rnot_lt_le. intros B. apply Rnot_lt_le. intros B.
apply H2. eapply precond_bound_correct; eauto. apply H2. eapply precond_bound_correct; eauto.
split; cbn; auto. split; cbn; auto.
do 2 eexists. repeat split; first [eassumption | constructor]. exists (Q2R r), v. repeat split; auto. constructor.
Qed. 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