SMTArith2.v 18.3 KB
Newer Older
1 2 3 4 5 6 7
(*
  Formalization of SMT Arithmetic for FloVer. Original author: Joachim Bard.
*)

Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Require Import Flover.Expressions.
Require Import Flover.Infra.ExpressionAbbrevs.
8
Require Import Flover.ExpressionSemantics.
9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42

Open Scope R.

(* list of all expr that can occur in SMT queries *)
(* alternative for SMTArith
Inductive SMTExpr : expr Q -> Prop :=
| ConstQ r : SMTExpr (Const REAL r)
| VarQ x : SMTExpr (Var Q x)
| UMinusQ e : SMTExpr e -> SMTExpr (Unop Neg e)
| PlusQ e1 e2 : SMTExpr e1 -> SMTExpr e2 -> SMTExpr (Binop Plus e1 e2)
| MinusQ e1 e2 : SMTExpr e1 -> SMTExpr e2 -> SMTExpr (Binop Sub e1 e2)
| TimesQ e1 e2 : SMTExpr e1 -> SMTExpr e2 -> SMTExpr (Binop Mult e1 e2)
| DivQ e1 e2 : SMTExpr e1 -> SMTExpr e2 -> SMTExpr (Binop Div e1 e2).
*)

Inductive SMTArith :=
| ConstQ (r: Q) : SMTArith
| VarQ (x: nat) : SMTArith
| UMinusQ (e: SMTArith) : SMTArith
| PlusQ (e1 e2: SMTArith) : SMTArith
| MinusQ (e1 e2: SMTArith) : SMTArith
| TimesQ (e1 e2: SMTArith) : SMTArith
| DivQ (e1 e2: SMTArith) : SMTArith.


Inductive SMTLogic :=
| LessQ (e1 e2: SMTArith) : SMTLogic
| LessEqQ (e1 e2: SMTArith) : SMTLogic
| EqualsQ (e1 e2: SMTArith) : SMTLogic
| TrueQ : SMTLogic
| NotQ (q: SMTLogic) : SMTLogic
| AndQ (q1 q2: SMTLogic) : SMTLogic
| OrQ (q1 q2: SMTLogic) : SMTLogic.

43 44
Definition FalseQ := NotQ TrueQ.

45 46 47 48 49 50 51 52 53 54 55 56
Definition getPrecond q :=
  match q with
  | AndQ p _ => Some p
  | _ => None
  end.

Definition getBound q :=
  match q with
  | AndQ _ (AndQ b _) => Some b
  | _ => None
  end.

57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105
(* TODO: broken (div by 0); remove it *)
Fixpoint evalArith (f: nat -> R) (e: SMTArith) : R :=
  match e with
  | ConstQ r => Q2R r
  | VarQ x => f x
  | UMinusQ e => - (evalArith f e)
  | PlusQ e1 e2 => (evalArith f e1) + (evalArith f e2)
  | MinusQ e1 e2 => (evalArith f e1) - (evalArith f e2)
  | TimesQ e1 e2 => (evalArith f e1) * (evalArith f e2)
  | DivQ e1 e2 => (evalArith f e1) / (evalArith f e2)
  end.

Fixpoint evalLogic (f: nat -> R) (q: SMTLogic) : Prop :=
  match q with
  | LessQ q1 q2 => (evalArith f q1) < (evalArith f q2)
  | LessEqQ q1 q2 => (evalArith f q1) <= (evalArith f q2)
  | EqualsQ q1 q2 => (evalArith f q1) = (evalArith f q2)
  | TrueQ => True
  | NotQ q => ~ (evalLogic f q)
  | AndQ q1 q2 => (evalLogic f q1) /\ (evalLogic f q2)
  | OrQ q1 q2 => (evalLogic f q1) \/ (evalLogic f q2)
  end.

Inductive eval_smt (E: env) : SMTArith -> R -> Prop :=
| VarQ_load x v : E x = Some v -> eval_smt E (VarQ x) v
| ConstQ_eval r : eval_smt E (ConstQ r) (Q2R r)
| UMinusQ_eval e v : eval_smt E e v -> eval_smt E (UMinusQ e) (- v)
| PlusQ_eval e1 e2 v1 v2 :
    eval_smt E e1 v1 -> eval_smt E e2 v2 -> eval_smt E (PlusQ e1 e2) (v1 + v2)
| MinusQ_eval e1 e2 v1 v2 :
    eval_smt E e1 v1 -> eval_smt E e2 v2 -> eval_smt E (MinusQ e1 e2) (v1 - v2)
| TimesQ_eval e1 e2 v1 v2 :
    eval_smt E e1 v1 -> eval_smt E e2 v2 -> eval_smt E (TimesQ e1 e2) (v1 * v2)
| 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
  | TrueQ => True
  | 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.

Lemma andq_assoc E q1 q2 q3 :
  eval_smt_logic E (AndQ q1 (AndQ q2 q3)) <-> eval_smt_logic E (AndQ (AndQ q1 q2) q3).
106
Proof. cbn. tauto. Qed.
107 108 109

Lemma andq_comm E q1 q2 :
  eval_smt_logic E (AndQ q1 q2) <-> eval_smt_logic E (AndQ q2 q1).
110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125
Proof. cbn. tauto. Qed.

Lemma not_eval_falseq E : ~ eval_smt_logic E FalseQ.
Proof. auto. Qed.

Fixpoint SMTArith2Expr (e: SMTArith) : expr Q :=
  match e with
  | ConstQ r => Expressions.Const REAL 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.

126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173
Lemma SMTArith2Expr_exact e : toREval (toRExp (SMTArith2Expr e)) = toRExp (SMTArith2Expr e).
Proof.
  induction e; cbn; auto; now rewrite ?IHe, ?IHe1, ?IHe2.
Qed.

Fixpoint smt_expr_eq (e: SMTArith) (e': expr Q) : bool :=
  match e, e' with
  | ConstQ r, Expressions.Const _ r' => Qeq_bool r r'
  | VarQ x, Var _ x' => beq_nat x x'
  | UMinusQ e, Unop Neg e' => smt_expr_eq e e'
  | PlusQ e1 e2, Binop Plus e1' e2' => (smt_expr_eq e1 e1') && (smt_expr_eq e2 e2')
  | MinusQ e1 e2, Binop Sub e1' e2' => (smt_expr_eq e1 e1') && (smt_expr_eq e2 e2')
  | TimesQ e1 e2, Binop Mult e1' e2' => (smt_expr_eq e1 e1') && (smt_expr_eq e2 e2')
  | DivQ e1 e2, Binop Div e1' e2' => (smt_expr_eq e1 e1') && (smt_expr_eq e2 e2')
  | _, _ => false
  end.

Lemma smt_expr_eq_sound e : smt_expr_eq e (SMTArith2Expr e) = true.
Proof.
  induction e; cbn; auto using Qeq_bool_refl, beq_nat_refl; intuition.
Qed.

Lemma eval_smt_expr_complete e e' :
  smt_expr_eq e e' = true -> toREval (toRExp e') = toRExp (SMTArith2Expr e).
Proof.
  induction e in e' |- *; destruct e'; cbn; try discriminate.
  - intros H. apply Qeq_bool_eq in H. apply Qeq_eqR in H. now rewrite H.
  - intros H. apply beq_nat_true in H. now rewrite H.
  - destruct u; [intuition | discriminate].
    now rewrite (IHe e').
  - destruct b; try discriminate.
    intros H. apply andb_prop in H as [H1 H2].
    rewrite <- (IHe1 e'1); auto.
    now rewrite <- (IHe2 e'2).
  - destruct b; try discriminate.
    intros H. apply andb_prop in H as [H1 H2].
    rewrite <- (IHe1 e'1); auto.
    now rewrite <- (IHe2 e'2).
  - destruct b; try discriminate.
    intros H. apply andb_prop in H as [H1 H2].
    rewrite <- (IHe1 e'1); auto.
    now rewrite <- (IHe2 e'2).
  - destruct b; try discriminate.
    intros H. apply andb_prop in H as [H1 H2].
    rewrite <- (IHe1 e'1); auto.
    now rewrite <- (IHe2 e'2).
Qed.

174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193
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 Gamma e v :
  eval_expr E (toRTMap Gamma) (toREval (toRExp (SMTArith2Expr e))) v REAL
  -> eval_smt E e v.
194
Proof.
195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210
  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. rewrite <- (toRTMap_eval_REAL _ H6). assumption.
    + apply IHe2. rewrite <- (toRTMap_eval_REAL _ H9). assumption.
  - inversion H. cbn. constructor.
    + apply IHe1. rewrite <- (toRTMap_eval_REAL _ H6). assumption.
    + apply IHe2. rewrite <- (toRTMap_eval_REAL _ H9). assumption.
  - inversion H. cbn. constructor.
    + apply IHe1. rewrite <- (toRTMap_eval_REAL _ H6). assumption.
    + apply IHe2. rewrite <- (toRTMap_eval_REAL _ H9). assumption.
  - inversion H. cbn. constructor; auto.
    + apply IHe1. rewrite <- (toRTMap_eval_REAL _ H6). assumption.
    + apply IHe2. rewrite <- (toRTMap_eval_REAL _ H9). assumption.
211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250
Qed.

Fixpoint varsSMT (e: SMTArith) :=
  match e with
  | VarQ x => {{x}}
  | ConstQ _ => NatSet.empty
  | UMinusQ e => varsSMT e
  | PlusQ e1 e2 => varsSMT e1  varsSMT e2
  | MinusQ e1 e2 => varsSMT e1  varsSMT e2
  | TimesQ e1 e2 => varsSMT e1  varsSMT e2
  | DivQ e1 e2 => varsSMT e1  varsSMT e2
  end.

Fixpoint varsLogic (q: SMTLogic) :=
  match q with
  | LessQ e1 e2 => varsSMT e1  varsSMT e2
  | LessEqQ e1 e2 => varsSMT e1  varsSMT e2
  | EqualsQ e1 e2 => varsSMT e1  varsSMT e2
  | TrueQ => NatSet.empty
  | NotQ q => varsLogic q
  | AndQ q1 q2 => varsLogic q1  varsLogic q2
  | OrQ q1 q2 => varsLogic q1  varsLogic 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)
| LessEqQ_eval e1 e2 v1 v2 :
    eval_smt E e1 v1 -> eval_smt E e2 v2 -> v1 <= v2 -> eval_smt_logic E (LessEqQ e1 e2)
| EqualsQ_eval e1 e2 v1 v2 :
    eval_smt E e1 v1 -> eval_smt E e2 v2 -> v1 = v2 -> eval_smt_logic E (EqualsQ e1 e2)
(* | NotQ_eval q : ~ (eval_smt_logic E q) -> eval_smt_logic E (NotQ q) *)
| AndQ_eval q1 q2 :
    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).
*)

251
(*
252
Definition eval_precond E (P: FloverMap.t intv) :=
253 254 255 256 257
  forall x iv, FloverMap.find (Var Q x) P = Some iv
             -> exists vR: R, E x = Some vR /\ Q2R (fst iv) <= vR <= Q2R (snd iv).
*)

Definition eval_precond E (P: FloverMap.t intv) :=
258 259 260
  forall e x iv, List.In (e, iv) (FloverMap.elements P)
            -> (FloverMapFacts.P.F.eqb (Var Q x) e = true)
            -> exists vR: R, E x = Some vR /\ Q2R (fst iv) <= vR <= Q2R (snd iv).
261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277

Definition addVarConstraint (el: expr Q * intv) q :=
  match el with
  | (Var _ x, (lo, hi)) => AndQ (LessEqQ (ConstQ lo) (VarQ x)) (AndQ (LessEqQ (VarQ x) (ConstQ hi)) q)
  | _ => q
  end.

Definition precond2SMT (P: FloverMap.t intv) :=
  List.fold_right addVarConstraint TrueQ (FloverMap.elements P).

Lemma pre_to_smt_correct E P :
  eval_precond E P -> eval_smt_logic E (precond2SMT P).
Proof.
  unfold eval_precond, precond2SMT.
  induction (FloverMap.elements P) as [|[e [lo hi]] l IHl].
  - intros. cbn. auto.
  - intros H. cbn.
278
    destruct e; try (apply IHl; intros e' x iv inl Heq; apply (H e'); cbn; auto).
279
    repeat split.
280 281 282 283 284 285 286
    + destruct (H (Var Q n) n (lo, hi)) as [v H']; cbn; auto.
      * now rewrite eqb_cmp_eq, Q_orderedExps.exprCompare_refl.
      * exists (Q2R lo), v. repeat split. 3: tauto. 1-2: constructor. tauto.
    + destruct (H (Var Q n) n (lo, hi)) as [v H']; cbn; auto.
      * now rewrite eqb_cmp_eq, Q_orderedExps.exprCompare_refl.
      * exists v, (Q2R hi). repeat split. 3: tauto. 1-2: constructor. tauto.
    + apply IHl. intros e x iv inl Heq. apply (H e); cbn; auto.
287 288
Qed.

289
(*
290 291 292 293 294 295
Lemma smt_to_pre_correct E P :
  eval_smt_logic E (precond2SMT P) -> eval_precond E P.
Proof.
  unfold precond2SMT, eval_precond.
  induction (FloverMap.elements P) as [|? l IHl].
  - cbn. tauto.
296
  - cbn. intros H x [lo hi] [hd | inl].
297 298 299 300 301 302 303 304 305 306 307 308
    + subst. cbn in H. destruct H as [H1 [H2 H3]].
      destruct H1 as [v1 [v2 H1]].
      exists v2. repeat split; destruct H1 as [lov1 [xv2 leq]].
      * inversion xv2. now subst.
      * inversion lov1. now subst.
      * destruct H2 as [v1' [v2' [xv1' [hiv2' leq']]]].
        inversion xv1'. inversion hiv2'. inversion xv2. subst.
        assert (eq: v2 = v1') by congruence. now rewrite eq.
    + apply IHl; auto. destruct a as [e [lo' hi']].
      destruct e; cbn in H; auto.
      apply H.
Qed.
309
*)
310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373

(* checker for precondition *)
Fixpoint checkPrelist (lP: list (FloverMap.key * intv)) q : bool :=
  match lP, q with
  | List.nil, TrueQ => true
  | List.cons (Var _ x, (lo, hi)) lP', AndQ (LessEqQ (ConstQ lo') (VarQ y)) (AndQ (LessEqQ (VarQ z) (ConstQ hi')) q') => (x =? y) && (x =? z) && Qeq_bool lo lo' && Qeq_bool hi hi' && checkPrelist lP' q'
  | List.cons (Var _ x, _) _, _ => false
  | List.cons el lP', _ => checkPrelist lP' q
  | _, _ => false
  end.

Lemma checkPrelist_LessQ lP e1 e2 : checkPrelist lP (LessQ e1 e2) = false.
Proof.
  induction lP as [|[e [lo hi]] l IHl]; auto.
  destruct e; auto.
Qed.

Lemma checkPrelist_LessEqQ lP e1 e2 : checkPrelist lP (LessEqQ e1 e2) = false.
Proof.
  induction lP as [|[e [lo hi]] l IHl]; auto.
  destruct e; auto.
Qed.

Lemma checkPrelist_EqualsQ lP e1 e2 : checkPrelist lP (EqualsQ e1 e2) = false.
Proof.
  induction lP as [|[e [lo hi]] l IHl]; auto.
  destruct e; auto.
Qed.

Lemma checkPrelist_NotQ lP q : checkPrelist lP (NotQ q) = false.
Proof.
  induction lP as [|[e [lo hi]] l IHl]; auto.
  destruct e; auto.
Qed.

Lemma checkPrelist_OrQ lP q1 q2 : checkPrelist lP (OrQ q1 q2) = false.
Proof.
  induction lP as [|[e [lo hi]] l IHl]; auto.
  destruct e; auto.
Qed.

(*
Lemma checkPrelist_inv lP q :
  checkPrelist lP q = true
  -> q = TrueQ \/ exists y z lo hi q', q = AndQ (LessEqQ (ConstQ lo) (VarQ y)) (AndQ (LessEqQ (VarQ z) (ConstQ hi)) q').
Proof.
  induction lP as [|[e [lo hi]] l IHl].
  - destruct q; cbn; intros H; try discriminate H. auto.
  - destruct e, q; cbn; intros H'; eauto.
    do 2 match goal with | [ q : SMTLogic |- _ ] => destruct q end; cbn; eauto.
    + destruct e0, e3; cbn.
Abort.
*)

Definition checkPre P q := checkPrelist (FloverMap.elements P) q.

Lemma checkPre_precond P : checkPre P (precond2SMT P) = true.
Proof.
  unfold precond2SMT, checkPre.
  induction (FloverMap.elements P) as [|[e [lo hi]] l IHl]; cbn; [reflexivity |].
  destruct e; cbn; auto.
  now rewrite Nat.eqb_refl, !Qeq_bool_refl, IHl.
Qed.

374 375 376 377 378 379 380 381 382 383 384 385
(*
Lemma convert_eval_precond E P :
  eval_precond E P <-> forall (x : nat) (iv : intv),
SetoidList.findA (FloverMapFacts.P.F.eqb (Var Q x)) (FloverMap.elements (elt:=intv) P) = Some iv ->
exists vR : R, E x = Some vR /\ Q2R (fst iv) <= vR <= Q2R (snd iv).
Proof.
  unfold eval_precond. split.
  - intros H x iv. rewrite <- FloverMapFacts.P.F.elements_o. auto.
  - intros H x iv. rewrite FloverMapFacts.P.F.elements_o. auto.
Qed.
*)

386 387 388
Lemma checkPre_pre_smt E P q :
  checkPre P q = true -> eval_precond E P -> eval_smt_logic E q.
Proof with try discriminate.
389
  unfold checkPre, eval_precond.
390 391
  induction (FloverMap.elements P) as [|[e [lo hi]] l IHl] in q |- *.
  - destruct q; cbn; intros chk... now auto.
392 393 394
  - destruct e as [x| | | | |].
    all: cbn; try (intros H0 H1; apply IHl; auto; intros e' x iv Hin Heq;
      apply (H1 e'); auto).
395 396
    destruct q as [? ?|? ?|? ?| |?|q1 q2|? ?]...
    intros chk H.
397
    destruct q1 as [? ?|e1 e2|? ?| |?|? ?|? ?]...
398 399 400 401
    destruct e1 as [r| | | | | |]... destruct e2 as [|y| | | | |]...
    destruct q2 as [? ?|? ?|? ?| |?|q1 q2|? ?]...
    destruct q1 as [? ?|e1 e2|? ?| |?|? ?|? ?]...
    destruct e1 as [|z| | | | |]... destruct e2 as [r'| | | | | |]...
402 403 404 405
    apply andb_prop in chk as [chk chk0].
    apply andb_prop in chk as [chk chk1].
    apply andb_prop in chk as [chk chk2].
    apply andb_prop in chk as [chk4 chk3].
406 407 408 409 410
    apply beq_nat_true in chk4. apply beq_nat_true in chk3.
    apply Qeq_bool_eq in chk2. apply Qeq_bool_eq in chk1.
    rewrite <- chk3, <- chk4.
    apply Qeq_sym in chk2. apply Qeq_sym in chk1.
    repeat split.
411 412 413 414 415 416
    + destruct (H (Var Q x) x (lo, hi)) as [v [H0 [H1 H2]]]; cbn; auto.
      * now rewrite eqb_cmp_eq, Q_orderedExps.exprCompare_refl.
      * exists (Q2R r), v. repeat split; try now constructor. erewrite Qeq_eqR; now eauto.
    + destruct (H (Var Q x) x (lo, hi)) as [v [H0 [H1 H2]]]; cbn; auto.
      * now rewrite eqb_cmp_eq, Q_orderedExps.exprCompare_refl.
      * exists v, (Q2R r'). repeat split; try now constructor. erewrite Qeq_eqR; now eauto.
417
    + apply IHl; auto.
418
      intros. apply (H e); auto.
419 420
Qed.

421
(*
422 423 424 425 426 427 428
Lemma checkPre_smt_pre E P q :
  checkPre P q = true -> eval_smt_logic E q -> eval_precond E P.
Proof with try discriminate.
  unfold eval_precond, checkPre.
  induction (FloverMap.elements P) as [|[e [lo hi]] l IHl] in q |- *.
  - destruct q; cbn; intros chk; try discriminate. tauto.
  - destruct e as [x| | | | |];
429
      try (intros chk H ? ? [?|?]; [discriminate| apply (IHl _ chk); auto]).
430 431 432 433 434 435
    destruct q as [? ?|? ?|? ?| |?|q1 q2|? ?]...
    destruct q1 as [? ?|e1 e2|? ?| |?|? ?|? ?]...
    destruct e1 as [r| | | | | |]... destruct e2 as [|y| | | | |]...
    destruct q2 as [? ?|? ?|? ?| |?|q1 q2|? ?]...
    destruct q1 as [? ?|e1 e2|? ?| |?|? ?|? ?]...
    destruct e1 as [|z| | | | |]... destruct e2 as [r'| | | | | |]...
436
    cbn. intros chk H x' [lo' hi'] [eq|inl].
437 438 439 440 441 442 443 444 445 446 447 448 449 450
    + apply andb_prop in chk. destruct chk as [chk chk0].
      apply andb_prop in chk. destruct chk as [chk chk1].
      apply andb_prop in chk. destruct chk as [chk chk2].
      apply andb_prop in chk. destruct chk as [chk4 chk3].
      apply beq_nat_true in chk4. apply beq_nat_true in chk3.
      apply Qeq_bool_eq in chk2. apply Qeq_bool_eq in chk1.
      destruct H as [[v1 [v2 [H1 [H2 H3]]]] [[v1' [v2' [H1' [H2' H3']]]] H]].
      symmetry in chk4. symmetry in chk3.
      assert (x' = x) by congruence.
      assert (lo' = lo) by congruence.
      assert (hi' = hi) by congruence.
      subst.
      inversion H1. inversion H2. inversion H1'. inversion H2'.
      assert (v2 = v1') by congruence.
451
      subst. cbn. rewrite (Qeq_eqR _ _ chk2). rewrite (Qeq_eqR _ _ chk1).
452 453 454 455
      exists v1'. repeat split; auto.
    + apply andb_prop in chk. destruct chk as [chk chk0].
      apply (IHl _ chk0); tauto.
Qed.
456
*)
457 458 459 460 461 462 463 464 465 466 467 468 469 470 471

Lemma precond_bound_correct E P preQ bound :
  eval_precond E P
  -> checkPre P preQ = true
  -> eval_smt_logic E bound
  -> eval_smt_logic E (AndQ preQ bound).
Proof.
  intros H1 H2 H3.
  split; auto.
  eapply checkPre_pre_smt; eauto.
Qed.

Lemma RangeBound_low_sound E P preQ e r Gamma v :
  eval_precond E P
  -> checkPre P preQ = true
472
  -> ~ eval_smt_logic E (AndQ preQ (AndQ (LessQ e (ConstQ r)) TrueQ))
473 474 475 476 477 478 479
  -> eval_expr E (toRTMap Gamma) (toREval (toRExp (SMTArith2Expr e))) v REAL
  -> Q2R r <= v.
Proof.
  intros H1 H2 H3 H4.
  apply eval_expr_smt in H4.
  apply Rnot_lt_le. intros B.
  apply H3. eapply precond_bound_correct; eauto.
480
  split; cbn; auto.
481 482 483 484 485 486
  do 2 eexists. repeat split; first [eassumption | constructor].
Qed.

Lemma RangeBound_high_sound E P preQ e r Gamma v :
  eval_precond E P
  -> checkPre P preQ = true
487
  -> ~ eval_smt_logic E (AndQ preQ (AndQ (LessQ (ConstQ r) e) TrueQ))
488 489 490 491 492 493 494
  -> eval_expr E (toRTMap Gamma) (toREval (toRExp (SMTArith2Expr e))) v REAL
  -> v <= Q2R r.
Proof.
  intros H1 H2 H3 H4.
  apply eval_expr_smt in H4.
  apply Rnot_lt_le. intros B.
  apply H3. eapply precond_bound_correct; eauto.
495
  split; cbn; auto.
496
  do 2 eexists. repeat split; first [eassumption | constructor].
497
Qed.