PreconditionValidation.v 1.9 KB
Newer Older
Heiko Becker's avatar
Heiko Becker committed
1 2 3
(**
Precondition agreement checker and its soundness proof
**)
4
Require Import Coq.Reals.Reals Coq.Lists.List Coq.QArith.QArith.
5
Require Import Flover.Infra.Abbrevs Flover.Expressions Flover.Infra.RationalSimps Flover.Infra.ExpressionAbbrevs Flover.IntervalArithQ.
6 7 8 9 10 11

Import Lists.List.ListNotations.

Fixpoint freeVars (V:Type) (e:exp V) : list nat:=
  match e with
  |Const n => []
12 13
  |Var _ v => []
  |Param _ v => [v]
14 15 16 17 18 19
  |Binop b e1 e2 => (freeVars V e1) ++ (freeVars V e2)
  end.

Fixpoint approximatesPrecond (e:exp Q) (absenv:analysisResult) (P:precond) :=
  match e with
  |Const n => true
20 21
  |Var _ v => true
  |Param _ v =>
Heiko Becker's avatar
Heiko Becker committed
22
   let (vprelo, vprehi) := P v in
23 24 25 26 27 28 29 30 31 32 33
   let (iv,err) := absenv (Param Q v) in
   let (vlo,vhi) := iv in
   andb (Qleb vlo vprelo) (Qleb vprehi vhi)
  |Binop b e1 e2 => andb (approximatesPrecond e1 absenv P) (approximatesPrecond e2 absenv P)
  end.

Theorem approximatesPrecond_sound e absenv P:
  approximatesPrecond e absenv P = true ->
  forall v, In v (freeVars Q e) ->
       Is_true(isSupersetIntv (P v) (fst (absenv (Param Q v)))).
Proof.
Heiko Becker's avatar
Heiko Becker committed
34
  induction e; unfold approximatesPrecond.
35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56
  - intros approx_true v v_in_fV; simpl in *; contradiction.
  - intros approx_true v v_in_fV; simpl in *.
    unfold isSupersetIntv.
    destruct v_in_fV; try contradiction.
    subst.
    destruct (P v); destruct (absenv (Param Q v)); simpl in *.
    destruct i; simpl in *.
    apply Is_true_eq_left in approx_true; auto.
  - intros approx_true v0 v_in_fV; simpl in *; contradiction.
  - intros approx_bin_true v v_in_fV.
    unfold freeVars in v_in_fV.
    apply in_app_or in v_in_fV.
    unfold approximatesPrecond in approx_bin_true.
    apply Is_true_eq_left in approx_bin_true.
    apply andb_prop_elim in approx_bin_true.
    destruct approx_bin_true.
    destruct v_in_fV as [v_in_fV_e1 | v_in_fV_e2].
    + apply IHe1; auto.
      apply Is_true_eq_true; auto.
    + apply IHe2; auto.
      apply Is_true_eq_true; auto.
Qed.