Commit 42fa192a authored by Joachim Bard's avatar Joachim Bard

minor changes to SMTArith2.v and adjusting testcases

parent 68a14034
......@@ -491,7 +491,7 @@ Qed.
Lemma RangeBound_low_sound E P preQ e r Gamma v :
eval_precond E P
-> checkPre P preQ = true
-> ~ eval_smt_logic E (AndQ preQ (LessQ e (ConstQ r)))
-> ~ eval_smt_logic E (AndQ preQ (AndQ (LessQ e (ConstQ r)) TrueQ))
-> eval_expr E (toRTMap Gamma) (toREval (toRExp (SMTArith2Expr e))) v REAL
-> Q2R r <= v.
Proof.
......@@ -499,13 +499,14 @@ Proof.
apply eval_expr_smt in H4.
apply Rnot_lt_le. intros B.
apply H3. eapply precond_bound_correct; eauto.
split; cbn; auto.
do 2 eexists. repeat split; first [eassumption | constructor].
Qed.
Lemma RangeBound_high_sound E P preQ e r Gamma v :
eval_precond E P
-> checkPre P preQ = true
-> ~ eval_smt_logic E (AndQ preQ (LessQ (ConstQ r) e))
-> ~ eval_smt_logic E (AndQ preQ (AndQ (LessQ (ConstQ r) e) TrueQ))
-> eval_expr E (toRTMap Gamma) (toREval (toRExp (SMTArith2Expr e))) v REAL
-> v <= Q2R r.
Proof.
......@@ -513,5 +514,6 @@ Proof.
apply eval_expr_smt in H4.
apply Rnot_lt_le. intros B.
apply H3. eapply precond_bound_correct; eauto.
split; cbn; auto.
do 2 eexists. repeat split; first [eassumption | constructor].
Qed.
......@@ -95,5 +95,6 @@ Proof.
eapply (RangeBound_high_sound (preQ:= prec) H1 _ _ H3).
Unshelve.
- reflexivity.
- intros H. apply H2. apply prec_bound_correct. exact H.
- intros H. apply H2. apply prec_bound_correct. destruct H as [Hp [Hb _]].
now constructor.
Qed.
Require Import Flover.CertificateChecker.
Require Import Flover.SMTArith2.
Require Import Flover.SMTValidation.
(* Require Import Flover.SMTValidation. *)
Definition C12 :expr Q := Const M64 ((1657)#(5)).
Definition C34 :expr Q := Const M64 ((3)#(5)).
Definition T2 :expr Q := Var Q 2.
......@@ -29,8 +29,10 @@ FloverMap.add e10 (( (-26688776647036775)#(193898302136352), (-156700)#(5322249)
Definition querymap_doppler :=
FloverMap.add e10 ((AndQ (AndQ (LessEqQ (VarQ 1) (ConstQ ((20000)#(1)))) (AndQ (LessEqQ (ConstQ ((-30)#(1))) (VarQ 2)) (AndQ (LessEqQ (ConstQ ((20)#(1))) (VarQ 1)) (AndQ (LessEqQ (ConstQ ((-100)#(1))) (VarQ 0)) (AndQ (LessEqQ (VarQ 0) (ConstQ ((100)#(1)))) (AndQ (LessEqQ (VarQ 2) (ConstQ ((50)#(1)))) TrueQ)))))) (AndQ (LessQ (DivQ (TimesQ (UMinusQ (PlusQ (ConstQ ((1657)#(5))) (TimesQ (ConstQ ((3)#(5))) (VarQ 2)))) (VarQ 1)) (TimesQ (PlusQ (PlusQ (ConstQ ((1657)#(5))) (TimesQ (ConstQ ((3)#(5))) (VarQ 2))) (VarQ 0)) (PlusQ (PlusQ (ConstQ ((1657)#(5))) (TimesQ (ConstQ ((3)#(5))) (VarQ 2))) (VarQ 0)))) (ConstQ ((-26688776647036775)#(193898302136352)))) TrueQ)), FalseQ) (FloverMap.empty (SMTLogic * SMTLogic)).
(*
Theorem test_validation :
validSMTIntervalbounds e10 absenv_doppler thePrecondition_doppler querymap_doppler NatSet.empty = true.
Proof.
cbv.
Abort.
*)
Require Import Flover.CertificateChecker.
Require Import Flover.SMTArith2.
Require Import Flover.SMTValidation.
(* Require Import Flover.SMTValidation. *)
Definition x0 :expr Q := Var Q 0.
Definition y1 :expr Q := Var Q 1.
Definition e1 :expr Q := Binop Plus x0 y1.
......@@ -22,11 +22,13 @@ FloverMap.add e5 (( (29)#(10), (75821)#(10240)), (316565750324396041763684170206
Definition querymap_fnc1 :=
FloverMap.add e2 (FalseQ, (AndQ (AndQ (LessEqQ (VarQ 0) (ConstQ ((6)#(1)))) (AndQ (LessEqQ (VarQ 1) (ConstQ ((8)#(1)))) (AndQ (LessEqQ (ConstQ ((-3)#(1))) (VarQ 0)) (AndQ (LessEqQ (ConstQ ((2)#(1))) (VarQ 1)) TrueQ)))) (AndQ (LessQ (ConstQ ((8201)#(2048))) (DivQ (PlusQ (VarQ 0) (VarQ 1)) (VarQ 1))) TrueQ))) (FloverMap.empty (SMTLogic * SMTLogic)).
(*
Theorem test_validation :
validSMTIntervalbounds e5 absenv_fnc1 thePrecondition_fnc1 querymap_fnc1 NatSet.empty = true.
Proof.
cbv.
Abort.
*)
Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Require Import RealRangeArith.
......@@ -87,5 +89,6 @@ Proof.
eapply (RangeBound_high_sound (preQ:= prec_reorder) H1 _ _ H3).
Unshelve.
- reflexivity.
- intros H. apply H2. apply prec_bound_correct. exact H.
- intros H. apply H2. apply prec_bound_correct.
destruct H as [Hp [Hb _]]. now 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