Commit 4e51542d authored by Joachim Bard's avatar Joachim Bard

simplified and clearified proofs for the testcase

parent f3c73937
......@@ -51,7 +51,6 @@ Definition bound :=
| _ => TrueQ
end.
Compute prec.
Lemma prec_bound_correct E :
eval_smt_logic E query <-> eval_smt_logic E (AndQ prec bound).
Proof.
......@@ -97,18 +96,25 @@ Proof.
+ apply IHe2. rewrite <- (toRTMap_eval_REAL _ H9). assumption.
Qed.
Lemma e2_to_smt : e2 = SMTArith2Expr (DivQ (PlusQ (VarQ 0) (VarQ 1)) (VarQ 1)).
Definition bound_expr :=
match bound with
| LessQ e (ConstQ r) => e
| LessQ (ConstQ r) e => e
| _ => ConstQ (0#1)
end.
Lemma e2_to_smt : e2 = SMTArith2Expr bound_expr.
Proof.
reflexivity.
Qed.
Lemma refute_bound E :
Lemma precond_bound_correct E :
eval_precond E thePrecondition_fnc1
-> ~ eval_smt_logic E query
-> ~ eval_smt_logic E (LessQ (ConstQ ((8201)#(2048))) (DivQ (PlusQ (VarQ 0) (VarQ 1)) (VarQ 1))).
-> eval_smt_logic E bound
-> eval_smt_logic E query.
Proof.
intros P unsatQ B.
apply unsatQ. apply prec_bound_correct.
intros P B.
apply prec_bound_correct.
constructor.
- eapply checkPre_pre_smt. 2: exact P.
reflexivity.
......@@ -121,10 +127,10 @@ Theorem RangeBound_e2_sound E Gamma v :
-> eval_expr E (toRTMap Gamma) (toREval (toRExp e2)) v REAL
-> v <= Q2R ((8201)#(2048)).
Proof.
intros Psound unsatQ e2v.
intros P nQ e2v.
rewrite e2_to_smt in e2v.
apply eval_expr_smt in e2v.
apply Rnot_lt_le. intros B.
eapply refute_bound. 1-2: eassumption.
eexists. exists v. repeat split. constructor. exact e2v. exact B.
apply nQ. apply precond_bound_correct. assumption.
do 2 eexists. repeat split; first [eassumption | constructor].
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