Commit 7ca212cb authored by Heiko Becker's avatar Heiko Becker

Define type erasure for Q exps in IV validation file, needed to obtain soundness properties

parent 5a48c033
...@@ -78,17 +78,26 @@ Fixpoint validIntervalboundsCmd (f:cmd Q) (absenv:analysisResult) (P:precond) (v ...@@ -78,17 +78,26 @@ Fixpoint validIntervalboundsCmd (f:cmd Q) (absenv:analysisResult) (P:precond) (v
validIntervalbounds e absenv P validVars validIntervalbounds e absenv P validVars
end. end.
Fixpoint erasure (e:exp Q) :exp Q :=
match e with
|Var _ m x => Var Q M0 x
|Unop u e => Unop u (erasure e)
|Binop b e1 e2 => Binop b (erasure e1) (erasure e2)
|Downcast _ e => Downcast M0 (erasure e)
|_ => e
end.
Theorem ivbounds_approximatesPrecond_sound f absenv P V: Theorem ivbounds_approximatesPrecond_sound f absenv P V:
validIntervalbounds f absenv P V = true -> validIntervalbounds (erasure f) absenv P V = true ->
forall v, NatSet.In v (NatSet.diff (Expressions.usedVars f) V) -> forall v, NatSet.In v (NatSet.diff (Expressions.usedVars f) V) ->
Is_true(isSupersetIntv (P v) (fst (absenv (Var Q v)))). Is_true(isSupersetIntv (P v) (fst (absenv (Var Q M0 v)))).
Proof. Proof.
induction f; unfold validIntervalbounds. induction f; unfold validIntervalbounds.
- intros approx_true v v_in_fV; simpl in *. - simpl. intros approx_true v v_in_fV; simpl in *.
rewrite NatSet.diff_spec in v_in_fV. rewrite NatSet.diff_spec in v_in_fV.
rewrite NatSet.singleton_spec in v_in_fV; rewrite NatSet.singleton_spec in v_in_fV;
destruct v_in_fV; subst. destruct v_in_fV; subst.
destruct (absenv (Var Q n)); simpl in *. destruct (absenv (Var Q M0 n)); simpl in *.
case_eq (NatSet.mem n V); intros case_mem; case_eq (NatSet.mem n V); intros case_mem;
rewrite case_mem in approx_true; simpl in *. rewrite case_mem in approx_true; simpl in *.
+ rewrite NatSet.mem_spec in case_mem. + rewrite NatSet.mem_spec in case_mem.
...@@ -101,7 +110,8 @@ Proof. ...@@ -101,7 +110,8 @@ Proof.
- intros approx_unary_true v v_in_fV. - intros approx_unary_true v v_in_fV.
unfold usedVars in v_in_fV. unfold usedVars in v_in_fV.
apply Is_true_eq_left in approx_unary_true. apply Is_true_eq_left in approx_unary_true.
destruct (absenv (Unop u f)); destruct (absenv f); simpl in *. simpl in *.
destruct (absenv (Unop u (erasure f))); destruct (absenv (erasure f)); simpl in *.
apply andb_prop_elim in approx_unary_true. apply andb_prop_elim in approx_unary_true.
destruct approx_unary_true. destruct approx_unary_true.
apply IHf; try auto. apply IHf; try auto.
...@@ -112,7 +122,9 @@ Proof. ...@@ -112,7 +122,9 @@ Proof.
destruct v_in_fV as [ v_in_fV v_not_in_V]. destruct v_in_fV as [ v_in_fV v_not_in_V].
rewrite NatSet.union_spec in v_in_fV. rewrite NatSet.union_spec in v_in_fV.
apply Is_true_eq_left in approx_bin_true. apply Is_true_eq_left in approx_bin_true.
destruct (absenv (Binop b f1 f2)); destruct (absenv f1); destruct (absenv f2); simpl in *. simpl in *.
destruct (absenv (Binop b (erasure f1) (erasure f2))); destruct (absenv (erasure f1));
destruct (absenv (erasure f2)); simpl in *.
apply andb_prop_elim in approx_bin_true. apply andb_prop_elim in approx_bin_true.
destruct approx_bin_true. destruct approx_bin_true.
apply andb_prop_elim in H. apply andb_prop_elim in H.
...@@ -124,7 +136,8 @@ Proof. ...@@ -124,7 +136,8 @@ Proof.
+ apply IHf2; auto. + apply IHf2; auto.
apply Is_true_eq_true; auto. apply Is_true_eq_true; auto.
rewrite NatSet.diff_spec; split; auto. rewrite NatSet.diff_spec; split; auto.
Qed. - admit.
Admitted.
Corollary Q2R_max4 a b c d: Corollary Q2R_max4 a b c d:
Q2R (IntervalArithQ.max4 a b c d) = max4 (Q2R a) (Q2R b) (Q2R c) (Q2R d). Q2R (IntervalArithQ.max4 a b c d) = max4 (Q2R a) (Q2R b) (Q2R c) (Q2R d).
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment