include NotQ in eval of queries, adjust testcase; no open proofs

coq/SMTArith.v

@@ -72,6 +72,18 @@ Inductive eval_smt (E: env) : SMTArith -> R -> Prop :=
 | DivQ_eval e1 e2 v1 v2 :
     v2 <> 0 -> eval_smt E e1 v1 -> eval_smt E e2 v2 -> eval_smt E (DivQ e1 e2) (v1 / v2).
 
+Fixpoint eval_smt_logic (E: env) (q: SMTLogic) : Prop :=
+  match q with
+  | LessQ e1 e2 => exists v1 v2, eval_smt E e1 v1 /\ eval_smt E e2 v2 /\ v1 < v2
+  | LessEqQ e1 e2 => exists v1 v2, eval_smt E e1 v1 /\ eval_smt E e2 v2 /\ v1 <= v2
+  | EqualsQ e1 e2 => exists v, eval_smt E e1 v /\ eval_smt E e2 v
+  | NotQ q => ~ (eval_smt_logic E q)
+  | AndQ q1 q2 => eval_smt_logic E q1 /\ eval_smt_logic E q2
+  | OrQ q1 q2 => eval_smt_logic E q1 \/ eval_smt_logic E q2
+  end.
+
+(*
+(* Does not work for NotQ *)
 Inductive eval_smt_logic (E: env) : SMTLogic -> Prop :=
 | LessQ_eval e1 e2 v1 v2 :
     eval_smt E e1 v1 -> eval_smt E e2 v2 -> v1 < v2 -> eval_smt_logic E (LessQ e1 e2)
@@ -84,6 +96,7 @@ Inductive eval_smt_logic (E: env) : SMTLogic -> Prop :=
     eval_smt_logic E q1 -> eval_smt_logic E q2 -> eval_smt_logic E (AndQ q1 q2)
 | OrQ_eval_l q1 q2 : eval_smt_logic E q1 -> eval_smt_logic E (OrQ q1 q2)
 | OrQ_eval_r q1 q2 : eval_smt_logic E q2 -> eval_smt_logic E (OrQ q1 q2).
+*)
 
 Fixpoint SMTArith2Expr (e: SMTArith) : expr Q :=
   match e with

coq/smt_bottom_up.v

@@ -49,8 +49,8 @@ Proof with try (right; apply Rabs_R0).
     apply (Binop_dist (m1:= REAL) (m2:=REAL)); auto...
 Qed.
 
-Lemma eval_expr_smt E e v :
-  eval_expr E (fun _ => Some REAL) (toREval (toRExp (SMTArith2Expr e))) v REAL
+Lemma eval_expr_smt E Gamma e v :
+  eval_expr E (toRTMap Gamma) (toREval (toRExp (SMTArith2Expr e))) v REAL
   -> eval_smt E e v.
 Proof.
   induction e in v |- *; cbn; intros H.
@@ -58,24 +58,25 @@ Proof.
   - inversion H. cbn. constructor; auto.
   - inversion H. cbn. constructor. destruct m; try discriminate. auto.
   - inversion H. cbn. constructor.
-    + apply IHe1. admit.
-    + apply IHe2. admit.
+    + apply IHe1. rewrite <- (toRTMap_eval_REAL _ H6). assumption.
+    + apply IHe2. rewrite <- (toRTMap_eval_REAL _ H9). assumption.
   - inversion H. cbn. constructor.
-    + apply IHe1. admit.
-    + apply IHe2. admit.
+    + apply IHe1. rewrite <- (toRTMap_eval_REAL _ H6). assumption.
+    + apply IHe2. rewrite <- (toRTMap_eval_REAL _ H9). assumption.
   - inversion H. cbn. constructor.
-    + apply IHe1. admit.
-    + apply IHe2. admit.
+    + apply IHe1. rewrite <- (toRTMap_eval_REAL _ H6). assumption.
+    + apply IHe2. rewrite <- (toRTMap_eval_REAL _ H9). assumption.
   - inversion H. cbn. constructor; auto.
-    + apply IHe1. admit.
-    + apply IHe2. admit.
-Admitted.
+    + apply IHe1. rewrite <- (toRTMap_eval_REAL _ H6). assumption.
+    + apply IHe2. rewrite <- (toRTMap_eval_REAL _ H9). assumption.
+Qed.
 
 Lemma e2_to_smt : e2 = SMTArith2Expr (DivQ (PlusQ (VarQ 0) (VarQ 1)) (VarQ 1)).
 Proof.
   reflexivity.
 Qed.
 
+(*
 Lemma refute_bound E :
   fVars_P_sound (usedVars e2) E thePrecondition_fnc1
   -> ~ eval_smt_logic E query
@@ -93,11 +94,30 @@ Proof.
   - destruct (P 0%nat) as [v1 [H0 H1]]. now cbn; set_tac.
     eapply LessEqQ_eval. 1-2: constructor; eauto. apply H1.
 Qed.
+*)
 
-Theorem RangeBound_e2_sound E v :
+Lemma refute_bound E :
   fVars_P_sound (usedVars e2) E thePrecondition_fnc1
   -> ~ eval_smt_logic E query
-  -> eval_expr E (fun _ => Some REAL) (toREval (toRExp e2)) v REAL
+  -> ~ eval_smt_logic E (LessQ (ConstQ ((8201)#(2048))) (DivQ (PlusQ (VarQ 0) (VarQ 1)) (VarQ 1))).
+Proof.
+  intros P unsatQ B.
+  apply unsatQ. cbn. repeat split.
+  - exact B.
+  - destruct (P 1%nat) as [v1 [H0 H1]]. now cbn; set_tac.
+    exists v1. eexists. repeat split. 1-2: now constructor. apply H1.
+  - destruct (P 0%nat) as [v1 [H0 H1]]. now cbn; set_tac.
+    eexists. exists v1. repeat split. 1-2: now constructor. apply H1.
+  - destruct (P 1%nat) as [v1 [H0 H1]]. now cbn; set_tac.
+    eexists. exists v1. repeat split. 1-2: now constructor. apply H1.
+  - destruct (P 0%nat) as [v1 [H0 H1]]. now cbn; set_tac.
+    exists v1. eexists. repeat split. 1-2: now constructor. apply H1.
+Qed.
+
+Theorem RangeBound_e2_sound E Gamma v :
+  fVars_P_sound (usedVars e2) E thePrecondition_fnc1
+  -> ~ eval_smt_logic E query
+  -> eval_expr E (toRTMap Gamma) (toREval (toRExp e2)) v REAL
   -> v <= Q2R ((8201)#(2048)).
 Proof.
   intros Psound unsatQ e2v.
@@ -105,7 +125,5 @@ Proof.
   apply eval_expr_smt in e2v.
   apply Rnot_lt_le. intros B.
   eapply refute_bound. 1-2: eassumption.
-  eapply LessQ_eval. 3: exact B. constructor. assumption.
+  eexists. exists v. repeat split. constructor. exact e2v. exact B.
 Qed.
-
-Print Assumptions RangeBound_e2_sound.