Skip to content

GitLab

Commit 3eb5483d authored by Heiko Becker's avatar Heiko Becker
Browse files

WIP for IVs

parent 129566e2
Hide whitespace changes
Inline Side-by-side
Showing with 111 additions and 86 deletions
coq/Infra/RealRationalProps.v
View file @ 3eb5483d
......@@ -6,12 +6,13 @@ Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Q
Require Import Coq.Reals.Reals Coq.micromega.Psatz.
Require Import Daisy.Infra.RationalSimps Daisy.Infra.Abbrevs Daisy.Expressions Daisy.IntervalArith.
Fixpoint toRExp (e:exp Q) :=
match e with
Fixpoint toRExp (f:exp Q) :=
match f with
|Var _ v => Var R v
|Param _ v => Param R v
|Const n => Const (Q2R n)
|Binop b e1 e2 => Binop b (toRExp e1) (toRExp e2)
|Unop o f1 => Unop o (toRExp f1)
|Binop o f1 f2 => Binop o (toRExp f1) (toRExp f2)
end.
Lemma Q2R0_is_0:
......
coq/IntervalValidation.v
View file @ 3eb5483d
......@@ -11,49 +11,54 @@ Require Import Daisy.Infra.ExpressionAbbrevs Daisy.IntervalArithQ Daisy.Interval
Import Lists.List.ListNotations.
Fixpoint freeVars (V:Type) (e:exp V) : list nat:=
match e with
Fixpoint freeVars (V:Type) (f:exp V) : list nat:=
match f with
|Const n => []
|Var _ v => []
|Param _ v => [v]
|Binop b e1 e2 => (freeVars V e1) ++ (freeVars V e2)
|Unop o f1 => freeVars V f1
|Binop o f1 f2 => (freeVars V f1) ++ (freeVars V f2)
end.
Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):=
let (intv, _) := absenv e in
match e with
| Var _ v => false
| Param _ v =>
isSupersetIntv (P v) intv
| Const n =>
isSupersetIntv (n,n) intv
| Binop b e1 e2 =>
let rec := andb (validIntervalbounds e1 absenv P) (validIntervalbounds e2 absenv P) in
let (iv1,_) := absenv e1 in
let (iv2,_) := absenv e2 in
let opres :=
match b with
| Plus =>
let new_iv := addIntv iv1 iv2 in
isSupersetIntv new_iv intv
| Sub =>
let new_iv := subtractIntv iv1 iv2 in
isSupersetIntv new_iv intv
| Mult =>
let new_iv := multIntv iv1 iv2 in
isSupersetIntv new_iv intv
| Div => false
end
in
andb rec opres
end.
Fixpoint validIntervalbounds (f:exp Q) (absenv:analysisResult) (P:precond):=
let (intv, _) := absenv f in
match f with
| Var _ v => false
| Param _ v =>
isSupersetIntv (P v) intv
| Const n =>
isSupersetIntv (n,n) intv
| Unop o f1 =>
let rec := validIntervalbounds f1 absenv P in
let (iv1, _) := absenv f1 in
let new_iv :=
match o with
| Neg => negateIntv iv1
| Inv => invertIntv iv1
end
in
andb rec (isSupersetIntv new_iv intv)
| Binop o f1 f2 =>
let rec := andb (validIntervalbounds f1 absenv P) (validIntervalbounds f2 absenv P) in
let (iv1,_) := absenv f1 in
let (iv2,_) := absenv f2 in
let new_iv :=
match o with
| Plus => addIntv iv1 iv2
| Sub => subtractIntv iv1 iv2
| Mult => multIntv iv1 iv2
| Div => divideIntv iv1 iv2
end
in
andb rec (isSupersetIntv new_iv intv)
end.
Theorem ivbounds_approximatesPrecond_sound e absenv P:
validIntervalbounds e absenv P = true ->
forall v, In v (freeVars Q e) ->
Theorem ivbounds_approximatesPrecond_sound f absenv P:
validIntervalbounds f absenv P = true ->
forall v, In v (freeVars Q f) ->
Is_true(isSupersetIntv (P v) (fst (absenv (Param Q v)))).
Proof.
induction e; unfold validIntervalbounds.
induction f; unfold validIntervalbounds.
- intros approx_true v v_in_fV; simpl in *; contradiction.
- intros approx_true v v_in_fV; simpl in *.
unfold isSupersetIntv.
......@@ -63,23 +68,30 @@ Proof.
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_unary_true v v_in_fV.
unfold freeVars in v_in_fV.
apply Is_true_eq_left in approx_unary_true.
destruct (absenv (Unop u f)); destruct (absenv f); simpl in *.
apply andb_prop_elim in approx_unary_true.
destruct approx_unary_true.
apply IHf; try auto.
apply Is_true_eq_true; auto.
- intros approx_bin_true v v_in_fV.
unfold freeVars in v_in_fV.
apply in_app_or in v_in_fV.
apply Is_true_eq_left in approx_bin_true.
destruct (absenv (Binop b e1 e2)); destruct (absenv e1); destruct (absenv e2); simpl in *.
destruct (absenv (Binop b f1 f2)); destruct (absenv f1); destruct (absenv f2); simpl in *.
apply andb_prop_elim in approx_bin_true.
destruct approx_bin_true.
apply andb_prop_elim in H.
destruct H.
destruct v_in_fV as [v_in_fV_e1 | v_in_fV_e2].
+ apply IHe1; auto.
destruct v_in_fV as [v_in_fV_f1 | v_in_fV_f2].
+ apply IHf1; auto.
apply Is_true_eq_true; auto.
+ apply IHe2; auto.
+ apply IHf2; auto.
apply Is_true_eq_true; auto.
Qed.
Corollary Q2R_max4 a b c d:
Q2R (IntervalArithQ.max4 a b c d) = max4 (Q2R a) (Q2R b) (Q2R c) (Q2R d).
Proof.
......@@ -95,38 +107,33 @@ Qed.
Ltac env_assert absenv e name :=
assert (exists iv err, absenv e = (iv,err)) as name by (destruct (absenv e); repeat eexists; auto).
Theorem validIntervalbounds_sound (e:exp Q):
forall (absenv:analysisResult) (P:precond) cenv vR,
precondValidForExec P cenv ->
validIntervalbounds e absenv P = true ->
eval_exp 0%R cenv (toRExp e) vR ->
(Q2R (fst (fst(absenv e))) <= vR <= Q2R (snd (fst (absenv e))))%R.
Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) cenv:
forall vR,
precondValidForExec P cenv ->
validIntervalbounds f absenv P = true ->
eval_exp 0%R cenv (toRExp f) vR ->
(Q2R (fst (fst(absenv f))) <= vR <= Q2R (snd (fst (absenv f))))%R.
Proof.
induction e.
- intros absenv P cenv vR precond_valid valid_bounds eval_e.
induction f.
- intros vR precond_valid valid_bounds eval_f.
pose proof (ivbounds_approximatesPrecond_sound (Var Q n) absenv P valid_bounds) as env_approx_p.
unfold validIntervalbounds in valid_bounds.
destruct (absenv (Var Q n)); inversion valid_bounds.
- intros absenv P cenv vR precond_valid valid_bounds eval_e.
- intros vR precond_valid valid_bounds eval_f.
pose proof (ivbounds_approximatesPrecond_sound (Param Q n) absenv P valid_bounds) as env_approx_p.
unfold validIntervalbounds in valid_bounds.
assert (exists intv err, absenv (Param Q n) = (intv,err))
as absenv_n
by (destruct (absenv (Param Q n)); repeat eexists; auto).
destruct absenv_n as [intv [err absenv_n]].
case_eq (absenv (Param Q n)).
intros intv err absenv_n.
rewrite absenv_n in valid_bounds.
unfold precondValidForExec in precond_valid.
specialize (env_approx_p n).
assert (exists ivlo ivhi, P n = (ivlo, ivhi)) as p_n
by (destruct (P n); repeat eexists; auto).
destruct p_n as [ivlo [ivhi p_n]].
case_eq (P n); intros ivlo ivhi p_n.
unfold isSupersetIntv, freeVars in env_approx_p.
assert (In n (n::nil)) by (unfold In; auto).
specialize (env_approx_p H).
assert (In n (n::nil)) as n_in_n by (unfold In; auto).
specialize (env_approx_p n_in_n).
rewrite p_n, absenv_n in env_approx_p.
specialize (precond_valid n); rewrite p_n in precond_valid.
inversion eval_e; subst.
rewrite absenv_n; simpl.
inversion eval_f; subst.
rewrite perturb_0_val; auto.
destruct intv as [abslo abshi]; simpl in *.
apply andb_prop_elim in env_approx_p.
......@@ -143,15 +150,14 @@ Proof.
+ eapply Rle_trans.
apply env_le_ivhi.
apply ivhi_le_abshi.
- intros absenv P cenv vR valid_precond valid_bounds eval_e.
- intros vR valid_precond valid_bounds eval_f.
pose proof (ivbounds_approximatesPrecond_sound (Const v) absenv P valid_bounds) as env_approx_p.
unfold validIntervalbounds in valid_bounds.
destruct (absenv (Const v)) as [intv err].
simpl.
destruct (absenv (Const v)) as [intv err]; simpl.
apply Is_true_eq_left in valid_bounds.
apply andb_prop_elim in valid_bounds.
destruct valid_bounds as [valid_lo valid_hi].
inversion eval_e; subst.
inversion eval_f; subst.
rewrite perturb_0_val; auto.
unfold contained; simpl.
split.
......@@ -163,32 +169,50 @@ Proof.
unfold Qleb in *.
apply Qle_bool_iff in valid_hi.
apply Qle_Rle in valid_hi; auto.
- intros absenv P cenv vR valid_precond valid_bounds eval_e;
inversion eval_e; subst.
pose proof (ivbounds_approximatesPrecond_sound (Binop b e1 e2) absenv P valid_bounds) as env_approx_p.
rewrite perturb_0_val in eval_e; auto.
- intros vR valid_precond valid_bounds eval_f;
pose proof (ivbounds_approximatesPrecond_sound (Unop u f) absenv P valid_bounds) as env_approx_p.
case_eq (absenv (Unop u f)); intros intv err absenv_unop.
destruct intv as [unop_lo unop_hi]; simpl.
unfold validIntervalbounds in valid_bounds.
rewrite absenv_unop in valid_bounds.
case_eq (absenv f); intros intv_f err_f absenv_f.
rewrite absenv_f in valid_bounds.
apply Is_true_eq_left in valid_bounds.
apply andb_prop_elim in valid_bounds.
destruct valid_bounds as [valid_rec valid_unop].
apply Is_true_eq_true in valid_rec.
inversion eval_f; subst.
+ specialize (IHf v1 valid_precond valid_rec H2).
rewrite absenv_f in IHf; simpl in IHf.
(** By monotonicity of negation **)
admit.
+ specialize (IHf v1 valid_precond valid_rec H3).
rewrite absenv_f in IHf; simpl in IHf.
(* By monotonicity of inversion of IV *)
admit.
- intros vR valid_precond valid_bounds eval_f; inversion eval_f; subst.
pose proof (ivbounds_approximatesPrecond_sound (Binop b f1 f2) absenv P valid_bounds) as env_approx_p.
rewrite perturb_0_val in eval_f; auto.
rewrite perturb_0_val; auto.
simpl in valid_bounds.
env_assert absenv (Binop b e1 e2) absenv_bin.
env_assert absenv e1 absenv_e1.
env_assert absenv e2 absenv_e2.
destruct absenv_bin as [iv [err absenv_bin]]; rewrite absenv_bin in valid_bounds; rewrite absenv_bin.
destruct absenv_e1 as [iv1 [err1 absenv_e1]]; rewrite absenv_e1 in valid_bounds.
destruct absenv_e2 as [iv2 [err2 absenv_e2]]; rewrite absenv_e2 in valid_bounds.
case_eq (absenv (Binop b f1 f2)); intros iv err absenv_bin.
case_eq (absenv f1); intros iv1 err1 absenv_f1.
case_eq (absenv f2); intros iv2 err2 absenv_f2.
rewrite absenv_bin, absenv_f1, absenv_f2 in valid_bounds.
apply Is_true_eq_left in valid_bounds.
apply andb_prop_elim in valid_bounds.
destruct valid_bounds as [valid_rec valid_bin].
apply andb_prop_elim in valid_rec.
destruct valid_rec as [valid_e1 valid_e2].
apply Is_true_eq_true in valid_e1; apply Is_true_eq_true in valid_e2.
specialize (IHe1 absenv P cenv v1 valid_precond valid_e1 H4);
specialize (IHe2 absenv P cenv v2 valid_precond valid_e2 H5).
rewrite absenv_e1 in IHe1.
rewrite absenv_e2 in IHe2.
specialize (IHf1 v1 valid_precond valid_e1 H4);
specialize (IHf2 v2 valid_precond valid_e2 H5).
rewrite absenv_f1 in IHf1.
rewrite absenv_f2 in IHf2.
destruct b; simpl in *.
+ pose proof (additionIsValid (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_add.
unfold validIntervalAdd in valid_add.
specialize (valid_add v1 v2 IHe1 IHe2).
specialize (valid_add v1 v2 IHf1 IHf2).
unfold contained in valid_add.
unfold isSupersetIntv in valid_bin.
apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi].
......@@ -212,7 +236,7 @@ Proof.
rewrite <- Q2R_max4 in valid_add_hi.
unfold absIvUpd; auto. }
+ pose proof (subtractionIsValid (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_sub.
specialize (valid_sub v1 v2 IHe1 IHe2).
specialize (valid_sub v1 v2 IHf1 IHf2).
unfold contained in valid_sub.
unfold isSupersetIntv in valid_bin.
apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi].
......@@ -238,7 +262,7 @@ Proof.
rewrite <- Q2R_max4 in valid_sub_hi.
unfold absIvUpd; auto.
+ pose proof (interval_multiplication_valid (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_mul.
specialize (valid_mul v1 v2 IHe1 IHe2).
specialize (valid_mul v1 v2 IHf1 IHf2).
unfold contained in valid_mul.
unfold isSupersetIntv in valid_bin.
apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi].
......@@ -261,5 +285,5 @@ Proof.
repeat rewrite <- Q2R_mult in valid_mul_hi.
rewrite <- Q2R_max4 in valid_mul_hi.
unfold absIvUpd; auto.
+ contradiction.
Qed.
\ No newline at end of file
+ admit.
Admitted.
\ No newline at end of file
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