Commit 06425929 authored by Joachim Bard's avatar Joachim Bard

moving testcases out of the way

parent defb76de
Require Import Flover.CertificateChecker.
Require Import Flover.SMTArith.
(* 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.
......@@ -77,16 +75,15 @@ Proof.
Qed.
Theorem RangeBound_e2_sound E Gamma v :
eval_precond (usedVars e2) E thePrecondition_fnc1
eval_precond E thePrecondition_fnc1
-> ~ eval_smt_logic E query
-> eval_expr E (toRTMap Gamma) (toREval (toRExp e2)) v REAL
-> v <= Q2R ((8201)#(2048)).
Proof.
intros H1 H2 H3.
rewrite e2_to_smt in H3.
eapply (RangeBound_high_sound (preQ:= prec_reorder) H1 _ _ _ H3).
eapply (RangeBound_high_sound (preQ:= prec_reorder) H1 _ _ H3).
Unshelve.
- set_tac.
- reflexivity.
- intros H. apply H2. apply prec_bound_correct.
destruct H as [Hp [Hb _]]. now constructor.
......
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