testcase: proving bound by hand; 1 open lemma

coq/smt_bottom_up.v

+Require Import Flover.CertificateChecker.
+Require Import Flover.SMTArith.
+Definition x0 :expr Q := Var Q 0.
+Definition y1 :expr Q := Var Q 1.
+Definition e1 :expr Q := Binop Plus x0 y1.
+Definition e2 :expr Q := Binop Div e1 y1.
+Definition C34 :expr Q := Const M64 ((17)#(5)).
+Definition e5 :expr Q := Binop Plus e2 C34.
+Definition Rete5 := Ret e5.
+
+
+Definition defVars_fnc1 :FloverMap.t mType :=
+(FloverMap.add (Var Q 1) (M64) (FloverMap.add (Var Q 0) (M64) (FloverMap.empty mType))).
+
+
+Definition thePrecondition_fnc1:precond := fun (n:nat) =>
+if n =? 0 then ( (-3)#(1), (6)#(1)) else if n =? 1 then ( (2)#(1), (8)#(1)) else (0#1,0#1).
+
+Definition absenv_fnc1 :analysisResult := Eval compute in
+FloverMap.add e5 (( (29)#(10), (75821)#(10240)), (31656575032439604176368417020690028172637826983022229834977068248762132258095105)#(4767828205180598627806767057994257910674911537412415567148097160036817151091933841114427031552)) (FloverMap.add C34 (( (17)#(5), (17)#(5)), (17)#(45035996273704960)) (FloverMap.add e2 (( (-1)#(2), (8201)#(2048)), (2879632975312110162723860570159105251222262341380356792653971457)#(529335265084873566077879553980951356026419978008369989458181366086188773933056)) (FloverMap.add y1 (( (2)#(1), (8)#(1)), (1)#(1125899906842624)) (FloverMap.add e1 (( (-1)#(1), (14)#(1)), (126100789566373895)#(40564819207303340847894502572032)) (FloverMap.add y1 (( (2)#(1), (8)#(1)), (1)#(1125899906842624)) (FloverMap.add x0 (( (-3)#(1), (6)#(1)), (3)#(4503599627370496)) (FloverMap.empty (intv * error)))))))).
+
+Definition querymap_fnc1 := Eval compute in
+FloverMap.add e5 (nil) (FloverMap.add C34 (nil) (FloverMap.add e2 ((cons (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)))))))) nil)) (FloverMap.add y1 (nil) (FloverMap.add e1 (nil) (FloverMap.add y1 (nil) (FloverMap.add x0 (nil) (FloverMap.empty (list SMTLogic)))))))).
+
+Require Import Coq.Reals.Reals Coq.QArith.Qreals.
+Require Import RealRangeArith.
+Require Import Flover.Expressions.
+
+Definition query :=
+      match FloverMap.find e2 querymap_fnc1 with
+      | Some (List.cons q _) => q
+      | _ => EqualsQ (ConstQ (0#1)) (ConstQ (1#1)) (* 0 == 1 *)
+      end.
+
+Lemma eval_smt_expr E e v :
+  eval_smt E e v -> eval_expr E (fun _ => Some REAL) (toRExp (SMTArith2Expr e)) v REAL.
+Proof with try (right; apply Rabs_R0).
+  induction 1.
+  - now constructor.
+  - rewrite <- (delta_0_deterministic _ REAL 0)... constructor...
+  - rewrite <- (delta_0_deterministic _ REAL 0)... apply (Unop_neg (m:= REAL)); auto.
+  - rewrite <- (delta_0_deterministic _ REAL 0)...
+    apply (Binop_dist (m1:= REAL) (m2:=REAL)); auto... discriminate.
+  - rewrite <- (delta_0_deterministic _ REAL 0)...
+    apply (Binop_dist (m1:= REAL) (m2:=REAL)); auto... discriminate.
+  - rewrite <- (delta_0_deterministic _ REAL 0)...
+    apply (Binop_dist (m1:= REAL) (m2:=REAL)); auto... discriminate.
+  - rewrite <- (delta_0_deterministic _ REAL 0)...
+    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
+  -> eval_smt E e v.
+Proof.
+  induction e in v |- *; cbn; intros H.
+  - inversion H. cbn. constructor.
+  - inversion H. cbn. constructor; auto.
+  - inversion H. cbn. constructor. destruct m; try discriminate. auto.
+  - inversion H. cbn. constructor.
+    + apply IHe1. admit.
+    + apply IHe2. admit.
+  - inversion H. cbn. constructor.
+    + apply IHe1. admit.
+    + apply IHe2. admit.
+  - inversion H. cbn. constructor.
+    + apply IHe1. admit.
+    + apply IHe2. admit.
+  - inversion H. cbn. constructor; auto.
+    + apply IHe1. admit.
+    + apply IHe2. admit.
+Admitted.
+
+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
+  -> ~ 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 constructor.
+  - exact B.
+  - destruct (P 1%nat) as [v1 [H0 H1]]. now cbn; set_tac.
+    eapply LessEqQ_eval. 1-2: constructor; eauto. apply H1.
+  - destruct (P 0%nat) as [v1 [H0 H1]]. now cbn; set_tac.
+    eapply LessEqQ_eval. 1-2: constructor; eauto. apply H1.
+  - destruct (P 1%nat) as [v1 [H0 H1]]. now cbn; set_tac.
+    eapply LessEqQ_eval. 1-2: constructor; eauto. apply H1.
+  - 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 :
+  fVars_P_sound (usedVars e2) E thePrecondition_fnc1
+  -> ~ eval_smt_logic E query
+  -> eval_expr E (fun _ => Some REAL) (toREval (toRExp e2)) v REAL
+  -> v <= Q2R ((8201)#(2048)).
+Proof.
+  intros Psound unsatQ e2v.
+  rewrite e2_to_smt in e2v.
+  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.
+Qed.
+
+Print Assumptions RangeBound_e2_sound.