manually proving bounds on an example using queries

coq/SMTArith.v

@@ -3,6 +3,7 @@
 *)
 
 Require Import Coq.Reals.Reals Coq.QArith.Qreals.
+Require Import Flover.Expressions.
 
 Open Scope R.
 
@@ -44,3 +45,91 @@ Fixpoint evalLogic (f: nat -> R) (q: SMTLogic) : Prop :=
   | AndQ q1 q2 => (evalLogic f q1) /\ (evalLogic f q2)
   | OrQ q1 q2 => (evalLogic f q1) \/ (evalLogic f q2)
   end.
+
+Definition unsat q := forall f, ~ evalLogic f q.
+
+Section Test.
+
+  (* the following defs are copied from the certificate *)
+  Definition query := AndQ (LessQ (ConstQ ((8201)#(2048))) (DivQ (PlusQ (VarQ 0) (VarQ 1)) (VarQ 1)))
+ (AndQ (LessEqQ (VarQ 1) (ConstQ ((8)#(1)))) (AndQ (LessEqQ (ConstQ ((-3)#(1))) (VarQ 0)) (AndQ (LessEqQ (ConstQ ((2)#(1))) (VarQ 1)) (LessEqQ (VarQ 0) (ConstQ ((6)#(1))))))).
+  Definition preC :=
+    (AndQ (LessEqQ (VarQ 1) (ConstQ ((8)#(1)))) (AndQ (LessEqQ (ConstQ ((-3)#(1))) (VarQ 0)) (AndQ (LessEqQ (ConstQ ((2)#(1))) (VarQ 1)) (LessEqQ (VarQ 0) (ConstQ ((6)#(1))))))).
+  Definition bound := (LessQ (ConstQ ((8201)#(2048))) (DivQ (PlusQ (VarQ 0) (VarQ 1)) (VarQ 1))).
+  Print bound.
+  Definition q := AndQ bound preC.
+  Arguments bound : simpl never.
+  Arguments preC : simpl never.
+
+  Lemma test0 : (forall f, evalLogic f preC) -> unsat q -> unsat bound.
+  Proof.
+    intros P nq f H.
+    apply (nq f). 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.
+  Proof.
+    intros f H. unfold preC. cbn. repeat split.
+    - apply (H 1%nat).
+    - apply (H 0%nat).
+    - apply (H 1%nat).
+    - apply (H 0%nat).
+  Qed.
+
+  Lemma test2 : (forall f, forall n, evalPrecond f preC' n) -> unsat q -> unsat bound.
+  Proof.
+    intros H. apply test0. intros f. apply test1. apply H.
+  Qed.
+
+  Definition get_bound q :=
+    match q with
+    | 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).
+  Proof.
+    unfold query, bound. cbn. intros validP unsatQ f validB.
+    apply (unsatQ f). cbn.
+    split; [exact validB | clear unsatQ validB ].
+    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))).
+  Proof.
+    intros unsatB f. cbn.
+    specialize (unsatB f). cbn in unsatB.
+    now apply Rnot_lt_le.
+  Qed.
+
+
+End Test.
+
+Fixpoint SMTArith2Expr (e: SMTArith) : expr Q.
+  eapply(match e with
+   | ConstQ r => Const _ r
+   | VarQ x => Var Q x
+   | UMinusQ e0 => Unop Neg (SMTArith2Expr e0)
+   | PlusQ e1 e2 => Binop Plus (SMTArith2Expr e1) (SMTArith2Expr e2)
+   | MinusQ e1 e2 => Binop Sub (SMTArith2Expr e1) (SMTArith2Expr e2)
+   | TimesQ e1 e2 => Binop Mult (SMTArith2Expr e1) (SMTArith2Expr e2)
+   | DivQ e1 e2 => Binop Div (SMTArith2Expr e1) (SMTArith2Expr e2)
+   end).
+Abort.
+
+Fixpoint SMTLogic2Expr (e: SMTLogic) : expr Q.
+Abort.
+(* TODO: how to get expr? *)
+
+(* list of all Expr that can occur in SMT queries *)
+(* Inductive SMTQuery : Prop :=. *)