Commit 99d6ff3c authored by Heiko Becker's avatar Heiko Becker

Simplify a coq proof

parent f677adf0
......@@ -24,33 +24,31 @@ 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
| Unop o f1 =>
let rec := validIntervalbounds f1 absenv P in
let (iv1, _) := absenv f1 in
| Param _ v => isSupersetIntv (P v) intv
| Const n => isSupersetIntv (n,n) intv
| Unop o f =>
let rec := validIntervalbounds f absenv P in
let (iv, _) := absenv f in
let opres :=
match o with
| Neg =>
let new_iv := negateIntv iv1 in
let new_iv := negateIntv iv in
isSupersetIntv new_iv intv
| Inv =>
let nodiv0 := orb
(andb (Qleb (ivhi iv1) 0) (negb (Qeq_bool (ivhi iv1) 0)))
(andb (Qleb 0 (ivlo iv1)) (negb (Qeq_bool (ivlo iv1) 0))) in
let new_iv := invertIntv iv1 in
(andb (Qleb (ivhi iv) 0) (negb (Qeq_bool (ivhi iv) 0)))
(andb (Qleb 0 (ivlo iv)) (negb (Qeq_bool (ivlo iv) 0))) in
let new_iv := invertIntv iv in
andb (isSupersetIntv new_iv intv) nodiv0
end
in
andb rec opres
| 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
| Binop op 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 opres :=
match b with
match op with
| Plus =>
let new_iv := addIntv iv1 iv2 in
isSupersetIntv new_iv intv
......@@ -79,11 +77,9 @@ Proof.
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.
destruct v_in_fV; try contradiction.
subst.
destruct (P v); destruct (absenv (Param Q v)); simpl in *.
destruct i; simpl in *.
destruct (absenv (Param Q v)); 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.
......@@ -152,7 +148,6 @@ Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond)
Proof.
induction f.
- intros vR 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 vR valid_bounds eval_f.
......@@ -181,7 +176,6 @@ Proof.
apply Qle_Rle in abslo_le_ivlo; apply Qle_Rle in ivhi_le_abshi.
split; lra.
- intros vR 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.
apply Is_true_eq_left in valid_bounds.
......@@ -199,8 +193,7 @@ Proof.
unfold Qleb in *.
apply Qle_bool_iff in valid_hi.
apply Qle_Rle in valid_hi; auto.
- intros vR valid_bounds eval_f;
pose proof (ivbounds_approximatesPrecond_sound (Unop u f) absenv P valid_bounds) as env_approx_p.
- intros vR valid_bounds eval_f.
case_eq (absenv (Unop u f)); intros intv err absenv_unop.
destruct intv as [unop_lo unop_hi]; simpl.
unfold validIntervalbounds in valid_bounds.
......@@ -299,7 +292,6 @@ Proof.
apply Rlt_Qlt in nodiv0_pos; apply Rle_Qle in H2; lra.
}
- intros vR 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 delta_0_deterministic in eval_f; auto.
rewrite delta_0_deterministic; auto.
simpl in valid_bounds.
......
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