From 99d6ff3cc0b7282e90f5f3345162b6c0c74e4cf2 Mon Sep 17 00:00:00 2001 From: Heiko Becker Date: Thu, 5 Jan 2017 16:24:57 +0100 Subject: [PATCH] Simplify a coq proof --- coq/IntervalValidation.v | 40 ++++++++++++++++------------------------ 1 file changed, 16 insertions(+), 24 deletions(-) diff --git a/coq/IntervalValidation.v b/coq/IntervalValidation.v index 527f526..ffc32f6 100644 --- a/coq/IntervalValidation.v +++ b/coq/IntervalValidation.v @@ -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. -- GitLab