Commit fbef6bd9 authored by Joachim Bard's avatar Joachim Bard

fixing statements in testSMTArith.v

parent 22be0d1c
......@@ -68,5 +68,3 @@ Fixpoint SMTArith2Expr (e: SMTArith) : expr Q :=
| TimesQ e1 e2 => Binop Mult (SMTArith2Expr e1) (SMTArith2Expr e2)
| DivQ e1 e2 => Binop Div (SMTArith2Expr e1) (SMTArith2Expr e2)
end.
Definition unsat q := forall f, ~ evalLogic f q.
......@@ -25,6 +25,8 @@ FloverMap.add e5 (nil) (FloverMap.add C34 (nil) (FloverMap.add e2 ((cons (AndQ (
Section Test.
Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Require Import Flover.Expressions.
Require Import RealRangeArith.
Require Import IntervalArithQ.
Open Scope R.
......@@ -43,22 +45,19 @@ Section Test.
Arguments bound : simpl never.
Arguments preC : simpl never.
Lemma test0 : (forall f, evalLogic f preC) -> unsat q -> unsat bound.
Lemma test0 : forall f, evalLogic f preC -> ~ evalLogic f q -> ~ evalLogic f bound.
Proof.
intros P nq f H.
apply (nq f). cbn. auto.
intros f P nq B.
apply nq. cbn. auto.
Qed.
Definition preC' n :=
if n =? 0 then ( (-3)#(1), (6)#(1)) else if n =? 1 then ( (2)#(1), (8)#(1)) else (0#1,0#1).
(* this (or similar) might be already defined somewhere *)
Definition evalPrecond f (P: precond) n :=
match P n with
|(lo, hi) => (Q2R lo <= f n) /\ (f n <= Q2R hi)
end.
Lemma test1 : forall f, (forall n, evalPrecond f preC' n) -> evalLogic f preC.
Lemma test1 : forall f, (forall n, evalPrecond f thePrecondition_fnc1 n) -> evalLogic f preC.
Proof.
intros f H. unfold preC. cbn. repeat split.
- apply (H 1%nat).
......@@ -67,9 +66,9 @@ Section Test.
- apply (H 0%nat).
Qed.
Lemma test2 : (forall f, forall n, evalPrecond f preC' n) -> unsat q -> unsat bound.
Lemma test2 : forall f, (forall n, evalPrecond f thePrecondition_fnc1 n) -> ~ evalLogic f q -> ~ evalLogic f bound.
Proof.
intros H. apply test0. intros f. apply test1. apply H.
intros f H. apply test0. apply test1. apply H.
Qed.
Definition get_bound q :=
......@@ -77,21 +76,19 @@ Section Test.
| AndQ b _ => b (* only works if the bound is at the left *)
| _ => q (* FAIL: q has not the right format *)
end.
Lemma test3 : (forall f, forall n, evalPrecond f preC' n) -> unsat query -> unsat (get_bound query).
Lemma test3 : forall f, (forall n, evalPrecond f thePrecondition_fnc1 n) -> ~ evalLogic f query -> ~ evalLogic f (get_bound query).
Proof.
unfold query, bound. cbn. intros validP unsatQ f validB.
apply (unsatQ f). cbn.
unfold query, bound. cbn. intros f validP unsatQ validB.
apply unsatQ.
split; [exact validB | clear unsatQ validB ].
repeat split; first [now apply (validP _ 0%nat) | now apply (validP _ 1%nat)].
repeat split; first [now apply (validP 0%nat) | now apply (validP 1%nat)].
Qed.
Lemma test4 :
unsat (get_bound query) -> forall f, evalLogic f (LessEqQ (DivQ (PlusQ (VarQ 0) (VarQ 1)) (VarQ 1)) (ConstQ (8201 # 2048))).
forall f, ~ evalLogic f (get_bound query) -> evalLogic f (LessEqQ (DivQ (PlusQ (VarQ 0) (VarQ 1)) (VarQ 1)) (ConstQ (8201 # 2048))).
Proof.
intros unsatB f. cbn.
specialize (unsatB f). cbn in unsatB.
now apply Rnot_lt_le.
cbn. intros f unsatB. now apply Rnot_lt_le.
Qed.
Lemma test5 : e2 = SMTArith2Expr (DivQ (PlusQ (VarQ 0) (VarQ 1)) (VarQ 1)).
......@@ -99,6 +96,18 @@ Section Test.
reflexivity.
Qed.
(*
Print eval_expr.
Print env.
Print toREval.
Print option.
Print mTypeToR.
Print toRExp.
Print fVars_P_sound.
Print toRTMap.
Print toRExpMap.
*)
(* Lemma bound_e2 : eval_expr _ _ (toRExp e2). *)
End Test.
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