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

Require Import Coq.Reals.Reals Coq.QArith.Qreals.
6
Require Import Flover.Expressions.
Joachim Bard's avatar
Joachim Bard committed
7
Require Import Flover.Infra.ExpressionAbbrevs.
Joachim Bard's avatar
Joachim Bard committed
8
Require Import Flover.ExpressionSemantics.
9
Require Import Flover.Commands.
10
Require Import Flover.Infra.Ltacs.
11
Require Import Flover.RealRangeArith.
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28

Open Scope R.

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
Joachim Bard's avatar
Joachim Bard committed
29
| TrueQ : SMTLogic
30
31
32
33
| NotQ (q: SMTLogic) : SMTLogic
| AndQ (q1 q2: SMTLogic) : SMTLogic
| OrQ (q1 q2: SMTLogic) : SMTLogic.

Joachim Bard's avatar
Joachim Bard committed
34
35
36
37
38
39
40
41
42
43
44
45
46
47
Definition FalseQ := NotQ TrueQ.

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.

48
49
50
51
52
53
54
55
56
57
58
59
60
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).

61
62
63
64
65
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
Joachim Bard's avatar
Joachim Bard committed
66
  | TrueQ => True
67
68
69
70
71
  | 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.

Joachim Bard's avatar
Joachim Bard committed
72
73
74
75
76
77
78
79
80
81
82
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).
Proof. cbn. tauto. Qed.

Lemma andq_comm E q1 q2 :
  eval_smt_logic E (AndQ q1 q2) <-> eval_smt_logic E (AndQ q2 q1).
Proof. cbn. tauto. Qed.

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

83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
Fixpoint SMTArith_eqb e e' : bool :=
  match e, e' with
  | ConstQ r, ConstQ r' => Qeq_bool r r'
  | VarQ x, VarQ x' => beq_nat x x'
  | UMinusQ e, UMinusQ e' => SMTArith_eqb e e'
  | PlusQ e1 e2, PlusQ e1' e2' => SMTArith_eqb e1 e1' && SMTArith_eqb e2 e2'
  | MinusQ e1 e2, MinusQ e1' e2' => SMTArith_eqb e1 e1' && SMTArith_eqb e2 e2'
  | TimesQ e1 e2, TimesQ e1' e2' => SMTArith_eqb e1 e1' && SMTArith_eqb e2 e2'
  | DivQ e1 e2, DivQ e1' e2' => SMTArith_eqb e1 e1' && SMTArith_eqb e2 e2'
  | _, _ => false
  end.

Fixpoint SMTLogic_eqb q q' : bool :=
  match q, q' with
  | LessQ q1 q2, LessQ q1' q2' => SMTArith_eqb q1 q1' && SMTArith_eqb q2 q2'
  | LessEqQ q1 q2, LessEqQ q1' q2' => SMTArith_eqb q1 q1' && SMTArith_eqb q2 q2'
  | EqualsQ q1 q2, EqualsQ q1' q2' => SMTArith_eqb q1 q1' && SMTArith_eqb q2 q2'
  | TrueQ, TrueQ => true
  | NotQ q, NotQ q' => SMTLogic_eqb q q'
  | AndQ q1 q2, AndQ q1' q2' => SMTLogic_eqb q1 q1' && SMTLogic_eqb q2 q2'
  | OrQ q1 q2, OrQ q1' q2' => SMTLogic_eqb q1 q1' && SMTLogic_eqb q2 q2'
  | _, _ => false
  end.

Joachim Bard's avatar
Joachim Bard committed
107
108
109
110
111
112
113
114
115
116
117
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.

118
119
120
121
122
123
124
125
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
174
175
176
177
178
179
180
181
Lemma SMTArith_eqb_refl e : SMTArith_eqb e e = true.
Proof.
  induction e; cbn; try rewrite IHe1, IHe2; auto using Qeq_bool_refl, Nat.eqb_refl.
Qed.

Lemma SMTLogic_eqb_refl q : SMTLogic_eqb q q = true.
Proof.
  induction q; cbn; try rewrite IHq1, IHq2; auto; now rewrite ?SMTArith_eqb_refl.
Qed.

Lemma SMTArith_eqb_sym e e' : SMTArith_eqb e e' = SMTArith_eqb e' e.
Proof.
  induction e in e' |- *; destruct e'; cbn; auto using Qeq_bool_comm, Nat.eqb_sym;
    try (rewrite IHe1, IHe2; reflexivity).
Qed.

Lemma SMTArith_eqb_sound E e e' v :
  SMTArith_eqb e e' = true ->
  eval_smt E e v ->
  eval_smt E e' v.
Proof.
  induction e in e', v |- *; destruct e'; cbn; try discriminate.
  - intros Heq H. inversion H; subst. apply Qeq_bool_eq, Qeq_eqR in Heq.
    rewrite Heq. constructor.
  - intros Heq H. apply beq_nat_true in Heq. inversion H; subst.
    now constructor.
  - intros Heq H. inversion H; subst. constructor. auto.
  - intros Heq H. andb_to_prop Heq. inversion H; subst.
    constructor; auto.
  - intros Heq H. andb_to_prop Heq. inversion H; subst.
    constructor; auto.
  - intros Heq H. andb_to_prop Heq. inversion H; subst.
    constructor; auto.
  - intros Heq H. andb_to_prop Heq. inversion H; subst.
    constructor; auto.
Qed.

Lemma SMTLogic_eqb_sound E q q' :
  SMTLogic_eqb q q' = true ->
  eval_smt_logic E q <-> eval_smt_logic E q'.
Proof.
  induction q in q' |- *; destruct q'; cbn; try discriminate.
  - intros H. andb_to_prop H.
    split; intros [v1 [v2 [H1 [H2 H3]]]]; exists v1, v2; repeat split;
      eauto using SMTArith_eqb_sound.
    all: rewrite SMTArith_eqb_sym in L, R; eauto using SMTArith_eqb_sound.
  - intros H. andb_to_prop H.
    split; intros [v1 [v2 [H1 [H2 H3]]]]; exists v1, v2; repeat split;
      eauto using SMTArith_eqb_sound.
    all: rewrite SMTArith_eqb_sym in L, R; eauto using SMTArith_eqb_sound.
  - intros H. andb_to_prop H.
    split; intros [v [H1 H2]]; exists v; repeat split;
      eauto using SMTArith_eqb_sound.
    all: rewrite SMTArith_eqb_sym in L, R; eauto using SMTArith_eqb_sound.
  - tauto.
  - intros Heq. split; intros nH H; now apply nH, (IHq q').
  - intros H. andb_to_prop H. split; intros [H1 H2]; split.
    all: try now apply (IHq1 _ L).
    all: now apply (IHq2 _ R).
  - intros H. andb_to_prop H. split; intros [H1 | H2].
    all: try (left; now apply (IHq1 _ L)).
    all: right; now apply (IHq2 _ R).
Qed.

Joachim Bard's avatar
Joachim Bard committed
182
183
184
185
186
187
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 :=
188
189
190
191
  match e', e with
  | Expressions.Const _ r', ConstQ r => Qeq_bool r r'
  | Var _ x', VarQ x => beq_nat x x'
  | Unop Neg e', UMinusQ e => smt_expr_eq e e'
Joachim Bard's avatar
Joachim Bard committed
192
  | Unop Inv e', DivQ (ConstQ (1#1)) e => smt_expr_eq e e'
193
194
195
196
  | Binop Plus e1' e2', PlusQ e1 e2 => (smt_expr_eq e1 e1') && (smt_expr_eq e2 e2')
  | Binop Sub e1' e2', MinusQ e1 e2 => (smt_expr_eq e1 e1') && (smt_expr_eq e2 e2')
  | Binop Mult e1' e2', TimesQ e1 e2 => (smt_expr_eq e1 e1') && (smt_expr_eq e2 e2')
  | Binop Div e1' e2', DivQ e1 e2 => (smt_expr_eq e1 e1') && (smt_expr_eq e2 e2')
Joachim Bard's avatar
Joachim Bard committed
197
  | Fma e1' e2' e3', PlusQ (TimesQ e1 e2) e3 =>
198
199
    smt_expr_eq e1 e1' && smt_expr_eq e2 e2' && smt_expr_eq e3 e3'
  | Downcast _ e', _ => smt_expr_eq e e'
Joachim Bard's avatar
Joachim Bard committed
200
201
202
203
204
205
206
207
  | _, _ => 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.

208
209
210
211
Lemma eval_smt_expr_complete E Gamma v e e' :
  smt_expr_eq e e' = true ->
  eval_expr E (toRTMap Gamma) DeltaMapR (toREval (toRExp e')) v REAL ->
  eval_expr E (toRTMap Gamma) DeltaMapR (toRExp (SMTArith2Expr e)) v REAL.
Joachim Bard's avatar
Joachim Bard committed
212
Proof.
213
214
215
216
217
  induction e' in e, v |- *.
  - destruct e; try discriminate. intros H. apply beq_nat_true in H. now rewrite H.
  - destruct e; try discriminate. intros H. apply Qeq_bool_eq in H.
    apply Qeq_eqR in H. cbn. now rewrite H.
  - destruct e, u; try discriminate.
Joachim Bard's avatar
Joachim Bard committed
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
    + intros Heq H.
      inversion H; subst.
      econstructor; eauto.
      destruct m; try discriminate.
      eapply IHe'; auto.
    + destruct e1; try discriminate.
      destruct r as [n d].
      destruct n; try discriminate.
      destruct p; try discriminate.
      destruct d; try discriminate.
      cbn. intros Heq H.
      inversion H; subst.
      destruct m; try discriminate.
      eapply Binop_dist'; eauto.
      cbn.
      rewrite RMicromega.IQR_1.
      apply RealSimps.inv_eq_1_div.
235
236
237
238
239
240
241
242
  - intros Heq H.
    inversion H; subst.
    assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
    assert (m2 = REAL) by (eapply toRTMap_eval_REAL; eauto).
    subst.
    destruct e, b; cbn; try discriminate; andb_to_prop Heq.
    all: eapply (Binop_dist' (v1:=v1) (v2:=v2)); eauto.
  - destruct e; try discriminate.
Joachim Bard's avatar
Joachim Bard committed
243
    destruct e1; try discriminate.
244
    intros Heq H. andb_to_prop Heq.
Joachim Bard's avatar
Joachim Bard committed
245
    fold smt_expr_eq in *.
246
247
248
249
    inversion H; subst.
    assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
    assert (m2 = REAL) by (eapply toRTMap_eval_REAL; eauto).
    assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto).
Joachim Bard's avatar
Joachim Bard committed
250
251
252
253
    subst. unfold evalFma. cbn.
    eapply (Binop_dist' (m1:=REAL) (m2:=REAL) (v1:=v1 * v2) (v2:= v3));
      try discriminate; eauto.
    eapply (Binop_dist' (m1:=REAL) (m2:=REAL) (v1:=v1) (v2:=v2)); eauto.
254
255
256
257
258
    discriminate.
  - cbn. intros Heq H.
    inversion H; subst.
    destruct m1; try discriminate.
    now apply IHe'.
Joachim Bard's avatar
Joachim Bard committed
259
260
261
Qed.

Lemma eval_smt_expr E e v :
262
263
  eval_smt E e v ->
  eval_expr E (fun _ => Some REAL) DeltaMapR (toRExp (SMTArith2Expr e)) v REAL.
Joachim Bard's avatar
Joachim Bard committed
264
265
266
Proof with try (right; apply Rabs_R0).
  induction 1.
  - now constructor.
267
  - rewrite <- (delta_0_deterministic (Q2R r) REAL 0)... constructor... auto.
268
  - apply (Unop_neg (m:= REAL)); auto.
Joachim Bard's avatar
Joachim Bard committed
269
270
271
272
273
274
275
276
277
278
279
  - 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 :
280
  eval_expr E (toRTMap Gamma) DeltaMapR (toREval (toRExp (SMTArith2Expr e))) v REAL
Joachim Bard's avatar
Joachim Bard committed
281
282
283
284
285
286
287
  -> 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.
288
289
290
291
292
293
    + apply IHe1.
      match_pat (eval_expr _ _ _ (toREval (toRExp (SMTArith2Expr e1))) _ _)
                (fun H => rewrite <- (toRTMap_eval_REAL _ H)). assumption.
    + apply IHe2.
      match_pat (eval_expr _ _ _ (toREval (toRExp (SMTArith2Expr e2))) _ _)
                (fun H => rewrite <- (toRTMap_eval_REAL _ H)). assumption.
Joachim Bard's avatar
Joachim Bard committed
294
  - inversion H. cbn. constructor.
295
296
297
298
299
300
    + apply IHe1.
      match_pat (eval_expr _ _ _ (toREval (toRExp (SMTArith2Expr e1))) _ _)
                (fun H => rewrite <- (toRTMap_eval_REAL _ H)). assumption.
    + apply IHe2.
      match_pat (eval_expr _ _ _ (toREval (toRExp (SMTArith2Expr e2))) _ _)
                (fun H => rewrite <- (toRTMap_eval_REAL _ H)). assumption.
Joachim Bard's avatar
Joachim Bard committed
301
  - inversion H. cbn. constructor.
302
303
304
305
306
307
    + apply IHe1.
      match_pat (eval_expr _ _ _ (toREval (toRExp (SMTArith2Expr e1))) _ _)
                (fun H => rewrite <- (toRTMap_eval_REAL _ H)). assumption.
    + apply IHe2.
      match_pat (eval_expr _ _ _ (toREval (toRExp (SMTArith2Expr e2))) _ _)
                (fun H => rewrite <- (toRTMap_eval_REAL _ H)). assumption.
Joachim Bard's avatar
Joachim Bard committed
308
  - inversion H. cbn. constructor; auto.
309
310
311
312
313
314
    + apply IHe1.
      match_pat (eval_expr _ _ _ (toREval (toRExp (SMTArith2Expr e1))) _ _)
                (fun H => rewrite <- (toRTMap_eval_REAL _ H)). assumption.
    + apply IHe2.
      match_pat (eval_expr _ _ _ (toREval (toRExp (SMTArith2Expr e2))) _ _)
                (fun H => rewrite <- (toRTMap_eval_REAL _ H)). assumption.
Joachim Bard's avatar
Joachim Bard committed
315
316
Qed.

Joachim Bard's avatar
Joachim Bard committed
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
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
Joachim Bard's avatar
Joachim Bard committed
333
  | TrueQ => NatSet.empty
Joachim Bard's avatar
Joachim Bard committed
334
335
336
337
338
  | NotQ q => varsLogic q
  | AndQ q1 q2 => varsLogic q1  varsLogic q2
  | OrQ q1 q2 => varsLogic q1  varsLogic q2
  end.

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
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
Lemma eval_smt_updEnv x v r E e :
  ~ (x  varsSMT e) ->
  eval_smt E e v <-> eval_smt (updEnv x r E) e v.
Proof.
  induction e in v |- *; intros Hx.
  - split; intros H; inversion H; subst; constructor.
  - split; intros H; inversion H; subst; constructor.
    + unfold updEnv. cbn in Hx. case_eq (x0 =? x); auto.
      intros Heq. exfalso. apply Hx. set_tac. symmetry. now apply beq_nat_true.
    + unfold updEnv in *. cbn in Hx. case_eq (x0 =? x); intros Heq; rewrite Heq in *; auto.
      exfalso. apply Hx. set_tac. symmetry. now apply beq_nat_true.
  - split; intros H; inversion H; subst; constructor; apply IHe; auto.
  - split; intros H; inversion H; subst; constructor.
    all: try apply IHe1; auto.
    all: try apply IHe2; auto.
    all: intros ?; apply Hx; cbn; set_tac.
  - split; intros H; inversion H; subst; constructor.
    all: try apply IHe1; auto.
    all: try apply IHe2; auto.
    all: intros ?; apply Hx; cbn; set_tac.
  - split; intros H; inversion H; subst; constructor.
    all: try apply IHe1; auto.
    all: try apply IHe2; auto.
    all: intros ?; apply Hx; cbn; set_tac.
  - split; intros H; inversion H; subst; constructor.
    all: try apply IHe1; auto.
    all: try apply IHe2; auto.
    all: intros ?; apply Hx; cbn; set_tac.
Qed.

Lemma eval_smt_logic_updEnv x v E q :
  ~ (x  varsLogic q) ->
  eval_smt_logic E q <-> eval_smt_logic (updEnv x v E) q.
Proof.
  intros H. induction q; cbn.
  - split; intros [v1 [v2 [H1 [H2 H3]]]]; exists v1, v2; repeat split; auto.
    all: try apply eval_smt_updEnv; auto.
    all: try eapply eval_smt_updEnv; eauto.
    all: try (intros ?; apply H; cbn; set_tac).
  - split; intros [v1 [v2 [H1 [H2 H3]]]]; exists v1, v2; repeat split; auto.
    all: try apply eval_smt_updEnv; auto.
    all: try eapply eval_smt_updEnv; eauto.
    all: try (intros ?; apply H; cbn; set_tac).
  - split; intros [v' [H1 H2]]; exists v'; repeat split; auto.
    all: try apply eval_smt_updEnv; auto.
    all: try eapply eval_smt_updEnv; eauto.
    all: try (intros ?; apply H; cbn; set_tac).
  - tauto.
  - split; intros H1 H2; apply H1; apply IHq; auto.
  - split; intros [H1 H2]; split.
    all: try apply IHq1; auto.
    all: try apply IHq2; auto.
    all: intros Hx; apply H; cbn; set_tac.
  - split; (intros [H1 | H2]; [left | right]).
    all: try apply IHq1; auto.
    all: try apply IHq2; auto.
    all: intros Hx; apply H; cbn; set_tac.
Qed.

Definition precond : Type := precondIntv * SMTLogic.

Definition preVars (P: precond) := preIntvVars (fst P)  varsLogic (snd P).

Definition eval_precond E (P: precond) :=
  P_intv_sound E (fst P) /\ eval_smt_logic E (snd P).

Lemma eval_precond_updEnv E x v P :
  eval_precond E P ->
  ~ (x  preVars P) ->
  eval_precond (updEnv x v E) P.
Proof.
  unfold preVars. destruct P as [Piv C]. cbn. intros [HPiv HC] H. split.
  - unfold P_intv_sound in *.
    intros y iv inl. destruct (HPiv y iv) as [r [H1 H2]]; auto.
    exists r. split; auto. unfold updEnv. case_eq (y =? x); intros Heq; auto.
    exfalso. apply H. set_tac. left. apply beq_nat_true in Heq. subst.
    eapply preIntvVars_sound. eauto.
  - apply eval_smt_logic_updEnv; auto. intros ?. apply H. set_tac.
Qed.

Definition usedQueries : Type := FloverMap.t (SMTLogic * SMTLogic).

Joachim Bard's avatar
Joachim Bard committed
421
Definition unsat_queries qMap :=
422
423
  forall E e ql qh, FloverMap.find e qMap = Some (ql, qh) ->
               ~ eval_smt_logic E ql /\ ~ eval_smt_logic E qh.
424

Joachim Bard's avatar
Joachim Bard committed
425
426
427
428
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
Joachim Bard's avatar
Joachim Bard committed
429
430
  end.

Joachim Bard's avatar
Joachim Bard committed
431
Definition precond2SMT (P: precond) :=
432
  List.fold_right addVarConstraint (snd P) (FloverMap.elements (fst P)).
Joachim Bard's avatar
Joachim Bard committed
433

Joachim Bard's avatar
cleanup    
Joachim Bard committed
434
435
Lemma pre_to_smt_correct E P :
  eval_precond E P -> eval_smt_logic E (precond2SMT P).
Joachim Bard's avatar
Joachim Bard committed
436
Proof.
437
438
439
  unfold eval_precond, P_intv_sound, precond2SMT.
  destruct P as [intvs q]. cbn.
  induction (FloverMap.elements intvs) as [|[e [lo hi]] l IHl].
440
  - intros. now cbn.
441
442
  - intros [H Hq]. cbn.
    destruct e; try (apply IHl; split; auto; intros x iv inl; apply H; cbn; auto).
Joachim Bard's avatar
Joachim Bard committed
443
    repeat split.
Joachim Bard's avatar
cleanup    
Joachim Bard committed
444
    + destruct (H n (lo, hi)) as [v [? ?]]; cbn; auto.
445
      exists (Q2R lo), v. repeat split; try now constructor. tauto.
Joachim Bard's avatar
cleanup    
Joachim Bard committed
446
    + destruct (H n (lo, hi)) as [v [? ?]]; cbn; auto.
447
      exists v, (Q2R hi). repeat split; try now constructor. tauto.
448
    + apply IHl. split; auto. intros x iv inl. apply H; cbn; auto.
Joachim Bard's avatar
cleanup    
Joachim Bard committed
449
Qed.
Joachim Bard's avatar
Joachim Bard committed
450
451
452
453

Lemma smt_to_pre_correct E P :
  eval_smt_logic E (precond2SMT P) -> eval_precond E P.
Proof.
454
455
456
457
458
  unfold precond2SMT, eval_precond, P_intv_sound.
  destruct P as [intvs q]. cbn.
  induction (FloverMap.elements intvs) as [|p l IHl]; try (cbn; tauto).
  cbn. intros H. split.
  - intros x [lo hi] [hd | inl].
Joachim Bard's avatar
Joachim Bard committed
459
460
461
462
463
464
465
466
    + 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.
467
    + apply IHl; auto. destruct p as [e [lo' hi']].
Joachim Bard's avatar
Joachim Bard committed
468
469
      destruct e; cbn in H; auto.
      apply H.
470
471
  - destruct p as [e [lo hi]]. destruct e; try now apply IHl.
      cbn in H. tauto.
Joachim Bard's avatar
Joachim Bard committed
472
473
474
Qed.

(* checker for precondition *)
475
Fixpoint checkPrelist (lP: list (FloverMap.key * intv)) C q : bool :=
Joachim Bard's avatar
Joachim Bard committed
476
  match lP, q with
477
478
  | List.nil, _ => SMTLogic_eqb C q
  | 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' C q'
Joachim Bard's avatar
Joachim Bard committed
479
  | List.cons (Var _ x, _) _, _ => false
480
  | List.cons el lP', _ => checkPrelist lP' C q
Joachim Bard's avatar
Joachim Bard committed
481
482
  end.

483
484
(*
Lemma checkPrelist_LessQ lP C e1 e2 : checkPrelist lP C (LessQ e1 e2) = false.
Joachim Bard's avatar
Joachim Bard committed
485
Proof.
Joachim Bard's avatar
Joachim Bard committed
486
487
  induction lP as [|[e [lo hi]] l IHl]; auto.
  destruct e; auto.
Joachim Bard's avatar
Joachim Bard committed
488
489
Qed.

Joachim Bard's avatar
Joachim Bard committed
490
Lemma checkPrelist_LessEqQ lP e1 e2 : checkPrelist lP (LessEqQ e1 e2) = false.
Joachim Bard's avatar
Joachim Bard committed
491
Proof.
Joachim Bard's avatar
Joachim Bard committed
492
493
  induction lP as [|[e [lo hi]] l IHl]; auto.
  destruct e; auto.
Joachim Bard's avatar
Joachim Bard committed
494
495
Qed.

Joachim Bard's avatar
Joachim Bard committed
496
Lemma checkPrelist_EqualsQ lP e1 e2 : checkPrelist lP (EqualsQ e1 e2) = false.
Joachim Bard's avatar
Joachim Bard committed
497
Proof.
Joachim Bard's avatar
Joachim Bard committed
498
499
500
501
502
  induction lP as [|[e [lo hi]] l IHl]; auto.
  destruct e; auto.
Qed.

Lemma checkPrelist_NotQ lP q : checkPrelist lP (NotQ q) = false.
Joachim Bard's avatar
Joachim Bard committed
503
Proof.
Joachim Bard's avatar
Joachim Bard committed
504
505
506
  induction lP as [|[e [lo hi]] l IHl]; auto.
  destruct e; auto.
Qed.
Joachim Bard's avatar
Joachim Bard committed
507

Joachim Bard's avatar
Joachim Bard committed
508
509
510
511
512
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.
513
*)
Joachim Bard's avatar
Joachim Bard committed
514

515
Definition checkPre (P: precond) q := checkPrelist (FloverMap.elements (fst P)) (snd P) q.
Joachim Bard's avatar
Joachim Bard committed
516

Joachim Bard's avatar
Joachim Bard committed
517
518
519
Lemma checkPre_precond P : checkPre P (precond2SMT P) = true.
Proof.
  unfold precond2SMT, checkPre.
520
521
522
523
524
  destruct P as [Piv C]. cbn.
  induction (FloverMap.elements Piv) as [|[e [lo hi]] l IHl]; cbn. 
  - apply SMTLogic_eqb_refl.
  - destruct e; cbn; auto.
    now rewrite Nat.eqb_refl, !Qeq_bool_refl, IHl.
Joachim Bard's avatar
Joachim Bard committed
525
Qed.
Joachim Bard's avatar
Joachim Bard committed
526

527
Lemma checkPre_pre_smt E P q :
528
  checkPre P q = true ->
529
  eval_precond E P ->
530
  eval_smt_logic E q.
Joachim Bard's avatar
Joachim Bard committed
531
Proof with try discriminate.
532
533
534
535
  unfold checkPre, eval_precond, P_intv_sound.
  destruct P as [Piv C]. cbn.
  induction (FloverMap.elements Piv) as [|[e [lo hi]] l IHl] in q |- *.
  - cbn. intros Heq [_ H]. now apply (SMTLogic_eqb_sound _ C).
Joachim Bard's avatar
Joachim Bard committed
536
  - destruct e as [x| | | | |].
537
    2-6: (cbn; intros Heq [H1 H2]; apply IHl; auto).
538
    cbn.
Joachim Bard's avatar
Joachim Bard committed
539
540
541
542
543
544
    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'| | | | | |]...
545
    intros chk [H HC].
Joachim Bard's avatar
Joachim Bard committed
546
547
548
549
550
551
552
553
    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].
    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.
554
    (* assert (x  fVars) as fx by (subst; set_tac; set_tac). *)
Joachim Bard's avatar
Joachim Bard committed
555
    repeat split.
556
    + destruct (H x (lo, hi)) as [v [H0 [H1 H2]]]; cbn; auto.
Joachim Bard's avatar
Joachim Bard committed
557
      exists (Q2R r), v. repeat split; try now constructor. erewrite Qeq_eqR; now eauto.
558
    + destruct (H x (lo, hi)) as [v [H0 [H1 H2]]]; cbn; auto.
Joachim Bard's avatar
Joachim Bard committed
559
      exists v, (Q2R r'). repeat split; try now constructor. erewrite Qeq_eqR; now eauto.
560
    + apply IHl; auto.
Joachim Bard's avatar
Joachim Bard committed
561
562
Qed.

563
(*
Joachim Bard's avatar
Joachim Bard committed
564
565
566
Lemma checkPre_smt_pre E P q :
  checkPre P q = true -> eval_smt_logic E q -> eval_precond E P.
Proof with try discriminate.
567
  unfold P_intv_sound, checkPre.
Joachim Bard's avatar
Joachim Bard committed
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
  induction (FloverMap.elements P) as [|[e [lo hi]] l IHl] in q |- *.
  - destruct q; cbn; intros chk; try discriminate. tauto.
  - destruct e as [x| | | | |];
      try (intros chk H ? ? [?|?]; [discriminate| apply (IHl _ chk); auto]).
    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'| | | | | |]...
    cbn. intros chk H x' [lo' hi'] [eq|inl].
    + 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.
      subst. cbn. rewrite (Qeq_eqR _ _ chk2). rewrite (Qeq_eqR _ _ chk1).
      exists v1'. repeat split; auto.
    + apply andb_prop in chk. destruct chk as [chk chk0].
      apply (IHl _ chk0); tauto.
Qed.
598
*)
Joachim Bard's avatar
Joachim Bard committed
599

600
Lemma precond_bound_correct E P preQ bound :
601
602
603
604
  eval_precond E P ->
  checkPre P preQ = true ->
  eval_smt_logic E bound ->
  eval_smt_logic E (AndQ preQ bound).
Joachim Bard's avatar
Joachim Bard committed
605
Proof.
606
  intros.
Joachim Bard's avatar
Joachim Bard committed
607
608
609
610
  split; auto.
  eapply checkPre_pre_smt; eauto.
Qed.

611
Lemma RangeBound_low_sound E P preQ e r Gamma v :
612
613
614
615
616
  eval_precond E P ->
  checkPre P preQ = true ->
  ~ eval_smt_logic E (AndQ preQ (AndQ (LessQ e (ConstQ r)) TrueQ)) ->
  eval_expr E (toRTMap Gamma) DeltaMapR (toREval (toRExp (SMTArith2Expr e))) v REAL ->
  Q2R r <= v.
Joachim Bard's avatar
Joachim Bard committed
617
Proof.
618
619
  intros H0 H1 H2 H3.
  apply eval_expr_smt in H3.
Joachim Bard's avatar
Joachim Bard committed
620
  apply Rnot_lt_le. intros B.
621
  apply H2. eapply precond_bound_correct; eauto.
Joachim Bard's avatar
Joachim Bard committed
622
623
624
625
  split; cbn; auto.
  do 2 eexists. repeat split; first [eassumption | constructor].
Qed.

626
Lemma RangeBound_high_sound E P preQ e r Gamma v :
627
628
629
630
631
  eval_precond E P ->
  checkPre P preQ = true ->
  ~ eval_smt_logic E (AndQ preQ (AndQ (LessQ (ConstQ r) e) TrueQ)) ->
  eval_expr E (toRTMap Gamma) DeltaMapR (toREval (toRExp (SMTArith2Expr e))) v REAL ->
  v <= Q2R r.
Joachim Bard's avatar
Joachim Bard committed
632
Proof.
633
634
  intros H0 H1 H2 H3.
  apply eval_expr_smt in H3.
Joachim Bard's avatar
Joachim Bard committed
635
  apply Rnot_lt_le. intros B.
636
  apply H2. eapply precond_bound_correct; eauto.
Joachim Bard's avatar
Joachim Bard committed
637
638
639
  split; cbn; auto.
  do 2 eexists. repeat split; first [eassumption | constructor].
Qed.