diff --git a/coq/Infra/Ltacs.v b/coq/Infra/Ltacs.v index f1e30edd91766fd130f285e64e4678d68bce160f..0fcf10be6fd0cb82865062504bf352eb44601b0a 100644 --- a/coq/Infra/Ltacs.v +++ b/coq/Infra/Ltacs.v @@ -21,11 +21,13 @@ Ltac canonize_Q_prop := match goal with | [ H: Qle_bool ?a ?b = true |- _] => rewrite Qle_bool_iff in H | [ H: Qleb ?a ?b = true |- _ ] => rewrite Qle_bool_iff in H + | [ H: Qeq_bool ?a ?b = true |- _] => rewrite Qeq_bool_iff in H end. Ltac canonize_Q_to_R := match goal with | [ H: (?a <= ?b)%Q |- _ ] => apply Qle_Rle in H + | [ H: (?a == ?b)%Q |- _ ] => apply Qeq_eqR in H | [ H: context [Q2R 0] |- _ ] => rewrite Q2R0_is_0 in H | [ |- context [Q2R 0] ] => rewrite Q2R0_is_0 end. @@ -44,51 +46,72 @@ Ltac Q2R_to_head_step := Ltac Q2R_to_head := repeat Q2R_to_head_step. -Ltac NatSet_simp hyp := - try rewrite NatSet.mem_spec in hyp; - try rewrite NatSet.equal_spec in hyp; - try rewrite NatSet.subset_spec in hyp; - try rewrite NatSet.empty_spec in hyp; - try rewrite NatSet.is_empty_spec in hyp; - try rewrite NatSet.add_spec in hyp; - try rewrite NatSet.remove_spec in hyp; - try rewrite NatSet.singleton_spec in hyp; - try rewrite NatSet.union_spec in hyp; - try rewrite NatSet.inter_spec in hyp; - try rewrite NatSet.diff_spec in hyp. - -Ltac NatSet_prop := - match goal with - | [ H : true = true |- _ ] => clear H; NatSet_prop - | [ H: ?T = true |- _ ] => NatSet_simp H; - (apply Is_true_eq_left in H; NatSet_prop; apply Is_true_eq_true in H) || NatSet_prop - | _ => try auto +Definition optionLift (X Y:Type) (v:option X) (f:X -> Y) (e:Y) := + match v with + |Some val => f val + | None => e end. -Ltac match_simpl := +Lemma optionLift_eq (X Y:Type) v (f:X -> Y) (e:Y): + match v with |Some val => f val | None => e end = optionLift X Y v f e. +Proof. + cbv; auto. +Qed. + +Lemma optionLift_cond X (a:bool) (b c :X): + (if a then b else c) = match a with |true => b |false => c end. +Proof. + cbv; auto. +Qed. + +Ltac remove_matches := rewrite optionLift_eq in *. + +Ltac remove_conds := rewrite <- andb_lazy_alt, optionLift_cond in *. + +Ltac match_factorize := match goal with - | [ H: ?t = ?u |- context [match ?t with _ => _ end]] => rewrite H; simpl + | [ H: ?t = ?u |- context [optionLift _ _ ?t _ _]] + => rewrite H; cbn + | [ H1: ?t = ?u, H2: context [optionLift _ _ ?t _ _] |- _ ] + => rewrite H1 in H2; cbn in H2 + | [ H: context [optionLift _ _ ?t _ _] |- _ ] + => destruct t eqn:?; cbn in H; try congruence + | [ |- context [optionLift _ _ ?t _ _] ] + => destruct t eqn:?; cbn; try congruence end. -Ltac destruct_if := +Ltac pair_factorize := match goal with - | [H: if ?c then ?a else ?b = _ |- _ ] => - case_eq ?c; - let name := fresh "cond" in - intros name; - rewrite name in *; - try congruence - | [H: _ |- if ?c then ?a else ?b = _] => - case_eq ?c; - let name := fresh "cond" in - intros name; - rewrite name in *; - try congruence - end. - -(* HOL4 Style patter matching tactics *) -Tactic Notation "lift " tactic(t) := - fun H => t H. + | [H: context[let (_, _) := ?p in _] |- _] => destruct p; cbn in H + end. + +Ltac match_simpl := + try remove_conds; + try remove_matches; + repeat match_factorize; + try pair_factorize. + +(* Ltac destruct_if := *) +(* match goal with *) +(* | [H: if ?c then ?a else ?b = _ |- _ ] => *) +(* case_eq ?c; *) +(* let name := fresh "cond" in *) +(* intros name; *) +(* rewrite name in *; *) +(* try congruence *) +(* | [H: _ |- if ?c then ?a else ?b = _] => *) +(* case_eq ?c; *) +(* let name := fresh "cond" in *) +(* intros name; *) +(* rewrite name in *; *) +(* try congruence *) +(* end. *) + +(* Ltac match_destr t:= *) +(* match goal with *) +(* | H: context [optionLift (DaisyMap.find ?k ?M) _ _] |- _ => *) +(* destruct (DaisyMap.find (elt:=intv * error) k M); idtac H *) +(* end. *) Tactic Notation "match_pat" open_constr(pat) tactic(t) := match goal with diff --git a/coq/Infra/NatSet.v b/coq/Infra/NatSet.v index fca6504bd9d907612e27cc00b2164fd4b44f4af5..72899be6f26cae366a57baa71255c10abe3e487e 100644 --- a/coq/Infra/NatSet.v +++ b/coq/Infra/NatSet.v @@ -72,24 +72,39 @@ Proof. destruct x_in_add as [ x_eq | [x_neq x_in_S]]; auto. Qed. -(** TODO: Merge with NatSet_prop tactic in Ltacs file **) -Ltac set_hnf_tac := +Ltac set_bool_to_prop := match goal with | [ H: NatSet.mem ?x _ = true |- _ ] => rewrite NatSet.mem_spec in H | [ H: NatSet.mem ?x _ = false |- _] => apply not_in_not_mem in H + | [ |- context [NatSet.mem ?x _]] => rewrite NatSet.mem_spec + end. + +Ltac solve_simple_sets := + match goal with + | [ H: NatSet.In ?x ?S1 |- NatSet.In ?x (NatSet.union ?S1 ?S2)] + => rewrite NatSet.union_spec; auto + end. + +Ltac set_hnf_tac := + match goal with | [ H: context [NatSet.In ?x (NatSet.diff ?A ?B)] |- _] => rewrite NatSet.diff_spec in H; destruct H | [ H: NatSet.Subset ?SA ?SB |- NatSet.In ?v ?SB] => apply H | [ H: NatSet.In ?x (NatSet.singleton ?y) |- _] => apply NatSetProps.Dec.F.singleton_1 in H | [ H: NatSet.In ?x NatSet.empty |- _ ] => inversion H | [ H: NatSet.In ?x (NatSet.union ?S1 ?S2) |- _ ] => rewrite NatSet.union_spec in H - | [ H: NatSet.In ?x (NatSet.add ?y ?S) |- _ ] => rewrite NatSet.add_spec_strong in H - | [ |- context [NatSet.mem ?x _]] => rewrite NatSet.mem_spec + | [ H: NatSet.In ?x (NatSet.add ?y ?S) |- _ ] => rewrite add_spec_strong in H | [ |- context [NatSet.In ?x (NatSet.union ?SA ?SB)]] => rewrite NatSet.union_spec | [ |- context [NatSet.In ?x (NatSet.diff ?A ?B)]] => rewrite NatSet.diff_spec | [ |- context [NatSet.In ?x (NatSet.singleton ?y)]] => rewrite NatSet.singleton_spec + | [ |- context [NatSet.In ?x (NatSet.remove ?y ?S)]] => rewrite NatSet.remove_spec + | [ |- context [NatSet.In ?x (NatSet.add ?y ?S)]] => rewrite NatSet.add_spec | [ |- context [NatSet.Subset ?SA ?SB]] => hnf; intros end. Ltac set_tac := - repeat set_hnf_tac; - simpl in *; try auto. + repeat set_bool_to_prop; + repeat solve_simple_sets; + repeat set_hnf_tac; + simpl in *; + repeat solve_simple_sets; + try auto. diff --git a/coq/IntervalValidation.v b/coq/IntervalValidation.v index 8448e78dee0f4fd30115ffe1097e0fb1db06aa84..15907a91d59993bd70a7f83b2e840823c486cfc6 100644 --- a/coq/IntervalValidation.v +++ b/coq/IntervalValidation.v @@ -105,24 +105,21 @@ Theorem ivbounds_approximatesPrecond_sound f A P dVars iv err: Proof. induction f; cbn; intros approx_true var var_in_fV find_A; set_tac. - subst. - rewrite find_A in *. + match_simpl. destruct (var mem dVars) eqn:?; set_tac; try congruence. andb_to_prop approx_true; unfold isSupersetIntv. apply andb_prop_intro; split; apply Is_true_eq_left; auto. - - destruct (DaisyMap.find (Unop u f) A) as [[iv_u err_u] | ] eqn:?; - try congruence. + - match_simpl. andb_to_prop approx_true. apply IHf; try auto. set_tac. - - destruct (DaisyMap.find (Binop b f1 f2) A) as [[iv_b err_b] | ] eqn:?; - try congruence. + - match_simpl. andb_to_prop approx_true. destruct H. + apply IHf1; try auto; set_tac. + apply IHf2; try auto; set_tac. - - destruct (DaisyMap.find (Downcast m f) A) as [[iv_m err_m] | ] eqn:?; - try congruence. + - match_simpl. andb_to_prop approx_true. apply IHf; try auto; set_tac. Qed. @@ -139,113 +136,116 @@ Proof. unfold IntervalArith.min4, min4; repeat rewrite Q2R_min; auto. Qed. -Ltac env_assert A e name := - assert (exists iv err, A e = (iv,err)) as name by (destruct (A e); repeat eexists; auto). - - Lemma validBoundsDiv_uneq_zero e1 e2 A P V ivlo_e2 ivhi_e2 err: - A e2 = ((ivlo_e2,ivhi_e2), err) -> + DaisyMap.find (elt:=intv * error) e2 A = Some ((ivlo_e2,ivhi_e2), err) -> validIntervalbounds (Binop Div e1 e2) A P V = true -> (ivhi_e2 < 0) \/ (0 < ivlo_e2). Proof. - intros A_eq validBounds. - unfold validIntervalbounds in validBounds. - env_assert A (Binop Div e1 e2) abs_div; destruct abs_div as [iv_div [err_div abs_div]]. - env_assert A e1 abs_e1; destruct abs_e1 as [iv_e1 [err_e1 abs_e1]]. - rewrite abs_div, abs_e1, A_eq in validBounds. - repeat (rewrite <- andb_lazy_alt in validBounds). - apply Is_true_eq_left in validBounds. - apply andb_prop_elim in validBounds. - destruct validBounds as [_ validBounds]; apply andb_prop_elim in validBounds. - destruct validBounds as [nodiv0 _]. - apply Is_true_eq_true in nodiv0. + intros A_eq validBounds; cbn in *. + match_simpl. + andb_to_prop validBounds. + repeat match_simpl. + andb_to_prop R. unfold isSupersetIntv in *; simpl in *. apply le_neq_bool_to_lt_prop; auto. Qed. +Definition dVars_range_valid (dVars:NatSet.t) (E:env) (A:analysisResult) :Prop := + forall v, NatSet.In v dVars -> + exists vR ivlo ivhi err, + E v = Some vR /\ + DaisyMap.find (Var Q v) A = Some ((ivlo, ivhi), err) /\ + (Q2R ivlo <= vR <= Q2R ivhi)%R. + +Definition fVars_P_sound (fVars:NatSet.t) (E:env) (P:precond) :Prop := + forall v, + NatSet.In v fVars -> + exists vR, E v = Some vR /\ + (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R. + +Definition vars_typed (S:NatSet.t) (Gamma: nat -> option mType) := + forall v, NatSet.In v S -> + exists m :mType, Gamma v = Some m. + Theorem validIntervalbounds_sound (f:exp Q) (A:analysisResult) (P:precond) fVars dVars (E:env) Gamma: validIntervalbounds f A P dVars = true -> - (forall v, NatSet.mem v dVars = true -> - exists vR, E v = Some vR /\ - (Q2R (fst (fst (A (Var Q v)))) <= vR <= Q2R (snd (fst (A (Var Q v)))))%R) -> + dVars_range_valid dVars E A -> NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars -> - (forall v, NatSet.mem v fVars = true -> - exists vR, E v = Some vR /\ - (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> - (forall v, NatSet.mem v (NatSet.union fVars dVars) = true -> - exists m :mType, Gamma v = Some m) -> - exists vR, eval_exp E (toRMap Gamma) (toREval (toRExp f)) vR M0 /\ - (Q2R (fst (fst (A f))) <= vR <= Q2R (snd (fst (A f))))%R. + fVars_P_sound fVars E P -> + vars_typed (NatSet.union fVars dVars) Gamma -> + exists ivlo ivhi err vR, + DaisyMap.find f A = Some ((ivlo, ivhi), err) /\ + eval_exp E (toRMap Gamma) (toREval (toRExp f)) vR M0 /\ + (Q2R ivlo <= vR <= Q2R ivhi)%R. Proof. induction f; intros valid_bounds valid_definedVars usedVars_subset valid_freeVars types_defined; - simpl in *. - - env_assert A (Var Q n) A_var. - destruct A_var as [iv_n [err_n A_var]]. - case_eq (NatSet.mem n dVars); intros dVars_case; - rewrite dVars_case, A_var in valid_bounds; simpl in *. - + destruct (valid_definedVars n) as [vR [env_valid bounds_valid]]; try auto. - eexists; split; simpl; try eauto. + cbn in *. + - match_simpl. + destruct (NatSet.mem n dVars) eqn:?; simpl in *. + + destruct (valid_definedVars n) + as [vR [ivlo_n [ivhi_n [err_n [env_valid [map_n bounds_valid]]]]]]; + try set_tac. + rewrite map_n in *. + inversion Heqo; subst. + exists ivlo_n, ivhi_n, e; eexists; split; [auto| split; try eauto ]. eapply Var_load; simpl; try auto. destruct (types_defined n) as [m type_m]; set_tac. match_simpl; auto. - + destruct (valid_freeVars n) as [vR [env_valid bounds_valid]]; set_tac; try auto. + + destruct (valid_freeVars n) as [vR [env_valid bounds_valid]]; + set_tac; try auto. assert (NatSet.In n fVars) by set_tac. - eexists; split; [econstructor | ]; eauto. - * destruct (types_defined n) as [m type_m]; set_tac. + andb_to_prop valid_bounds. + canonize_hyps; simpl in *. + exists (fst i), (snd i), e; eexists; split; + [destruct i; auto | split]. + * econstructor; try eauto. + destruct (types_defined n) as [m type_m]; set_tac. match_simpl; auto. - * andb_to_prop valid_bounds. - unfold Qleb in *. - canonize_hyps. - rewrite A_var. - simpl in *. - lra. - - exists (perturb (Q2R v) 0). - split; [econstructor; eauto; apply Rabs_0_equiv | ]. - env_assert A (Const m v) A_const; - destruct A_const as [iv_v [err_v A_const]]. - rewrite A_const in *; simpl in *. + * lra. + - match_simpl. andb_to_prop valid_bounds. - canonize_hyps. - simpl in *; unfold perturb; lra. - - env_assert A (Unop u f) A_unop; - destruct A_unop as [iv_u [err_u A_unop]]. - rewrite A_unop in *; simpl in *. - case_eq (validIntervalbounds f A P dVars); - intros case_bounds; rewrite case_bounds in *; try congruence. - env_assert A f A_f; - destruct A_f as [iv_f [ err_f A_f]]; rewrite A_f in *; simpl in *. - destruct IHf as [vF [eval_f valid_bounds_f]]; try auto. - destruct u. - + exists (evalUnop Neg vF); split; [econstructor; auto | ]. - (* TODO: Make lemma *) - unfold isSupersetIntv in valid_bounds; - andb_to_prop valid_bounds. - canonize_hyps. - simpl in *. + canonize_hyps; simpl in *. + exists (fst i), (snd i), e, (perturb (Q2R v) 0). + split; [destruct i; auto| split]. + + econstructor; try eauto. apply Rabs_0_equiv. + + unfold perturb; simpl; lra. + - match_simpl. + andb_to_prop valid_bounds. + match_simpl. + destruct IHf as [ivlo_f [ivhi_f [err_f [vF [iveq_f [eval_f valid_bounds_f]]]]]]; + try auto. + destruct u; try andb_to_prop R. + + exists (fst i), (snd i), e, (evalUnop Neg vF); split; + [destruct i; auto | split ; + [econstructor; eauto | ]]. + canonize_hyps; simpl in *. rewrite Q2R_opp in *. - lra. - + andb_to_prop valid_bounds. - rename L into nodiv0. + destruct valid_bounds_f. + inversion iveq_f; subst; simpl in *; lra. + + inversion iveq_f; subst; simpl in *. + rename L0 into nodiv0. apply le_neq_bool_to_lt_prop in nodiv0. - exists (perturb (evalUnop Inv vF) 0); split; [econstructor; eauto; try apply Rabs_0_equiv | ]. - * (* Absence of division by zero *) + exists (fst i), (snd i), e, (perturb (evalUnop Inv vF) 0); split; + [destruct i; auto | split]. + * econstructor; eauto; try apply Rabs_0_equiv. + (* Absence of division by zero *) hnf. destruct nodiv0 as [nodiv0 | nodiv0]; apply Qlt_Rlt in nodiv0; rewrite Q2R0_is_0 in nodiv0; lra. * canonize_hyps. - pose proof (interval_inversion_valid (Q2R (fst iv_f),(Q2R (snd iv_f))) (a :=vF)) as inv_valid. + pose proof (interval_inversion_valid ((Q2R ivlo_f),(Q2R ivhi_f)) (a :=vF)) as inv_valid. unfold invertInterval in inv_valid; simpl in *. rewrite delta_0_deterministic; [| rewrite Rbasic_fun.Rabs_R0; lra]. destruct inv_valid; try auto. { destruct nodiv0; rewrite <- Q2R0_is_0; [left | right]; apply Qlt_Rlt; auto. } { split; eapply Rle_trans. - - apply L0. + - apply L1. - rewrite Q2R_inv; try auto. destruct nodiv0; try lra. hnf; intros. - assert (0 < Q2R (snd iv_f))%R. + assert (0 < Q2R (ivhi_f))%R. { eapply Rlt_le_trans. apply Qlt_Rlt in H1. rewrite <- Q2R0_is_0. @@ -258,7 +258,7 @@ Proof. - rewrite <- Q2R_inv; try auto. hnf; intros. destruct nodiv0; try lra. - assert (Q2R (fst iv_f) < 0)%R. + assert (Q2R ivlo_f < 0)%R. { eapply Rle_lt_trans. Focus 2. rewrite <- Q2R0_is_0; @@ -267,58 +267,55 @@ Proof. } rewrite <- Q2R0_is_0 in H3. apply Rlt_Qlt in H3. lra. } - - env_assert A (Binop b f1 f2) A_b; - destruct A_b as [iv_b [err_b A_b]]. - env_assert A f1 A_f1; - destruct A_f1 as [iv_f1 [err_f1 A_f1]]. - env_assert A f2 A_f2; - destruct A_f2 as [iv_f2 [err_f2 A_f2]]. - rewrite A_b in *; simpl in *. + - match_simpl. andb_to_prop valid_bounds. - destruct IHf1 as [vF1 [eval_f1 valid_f1]]; try auto; set_tac. - destruct IHf2 as [vF2 [eval_f2 valid_f2]]; try auto; set_tac. - rewrite A_f1, A_f2 in *; simpl in *. + repeat match_simpl. + destruct IHf1 as [ivlo_f1 [ivhi_f1 [err1 [vF1 [env1 [eval_f1 valid_f1]]]]]]; + try auto; set_tac. + destruct IHf2 as [ivlo_f2 [ivhi_f2 [err2 [vF2 [env2 [eval_f2 valid_f2]]]]]]; + try auto; set_tac. assert (M0 = join M0 M0) as M0_join by (cbv; auto); rewrite M0_join. - exists (perturb (evalBinop b vF1 vF2) 0); + exists (fst i), (snd i), e, (perturb (evalBinop b vF1 vF2) 0); + split; [destruct i; auto | ]. + inversion env1; inversion env2; subst. destruct b; simpl in *. * split; [econstructor; try congruence; apply Rabs_0_equiv | ]. - pose proof (interval_addition_valid (Q2R (fst iv_f1),Q2R (snd iv_f1)) (Q2R (fst iv_f2), Q2R (snd iv_f2))) as valid_add. + pose proof (interval_addition_valid ((Q2R ivlo_f1), Q2R ivhi_f1) + (Q2R ivlo_f2, Q2R ivhi_f2)) as valid_add. specialize (valid_add vF1 vF2 valid_f1 valid_f2). unfold isSupersetIntv in R. andb_to_prop R. - canonize_hyps. - simpl in *. + canonize_hyps; simpl in *. repeat rewrite <- Q2R_plus in *; rewrite <- Q2R_min4, <- Q2R_max4 in *. - unfold perturb. - lra. + unfold perturb. lra. * split; [econstructor; try congruence; apply Rabs_0_equiv |]. - pose proof (interval_subtraction_valid (Q2R (fst iv_f1),Q2R (snd iv_f1)) (Q2R (fst iv_f2), Q2R (snd iv_f2))) as valid_sub. + pose proof (interval_subtraction_valid (Q2R ivlo_f1, Q2R ivhi_f1) + (Q2R ivlo_f2, Q2R ivhi_f2)) + as valid_sub. specialize (valid_sub vF1 vF2 valid_f1 valid_f2). unfold isSupersetIntv in R. andb_to_prop R. - canonize_hyps. - simpl in *. + canonize_hyps; simpl in *. repeat rewrite <- Q2R_opp in *; repeat rewrite <- Q2R_plus in *; rewrite <- Q2R_min4, <- Q2R_max4 in *. - unfold perturb. - lra. + unfold perturb; lra. * split; [ econstructor; try congruence; apply Rabs_0_equiv |]. - pose proof (interval_multiplication_valid (Q2R (fst iv_f1),Q2R (snd iv_f1)) (Q2R (fst iv_f2), Q2R (snd iv_f2))) as valid_mul. + pose proof (interval_multiplication_valid (Q2R ivlo_f1, Q2R ivhi_f1) + (Q2R ivlo_f2, Q2R ivhi_f2)) + as valid_mul. specialize (valid_mul vF1 vF2 valid_f1 valid_f2). unfold isSupersetIntv in R. andb_to_prop R. - canonize_hyps. - simpl in *. + canonize_hyps; simpl in *. repeat rewrite <- Q2R_mult in *; rewrite <- Q2R_min4, <- Q2R_max4 in *. - unfold perturb. - lra. + unfold perturb; lra. * andb_to_prop R. canonize_hyps. apply le_neq_bool_to_lt_prop in L. @@ -327,17 +324,20 @@ Proof. (* No division by zero proof *) { hnf; intros. destruct L as [L | L]; apply Qlt_Rlt in L; rewrite Q2R0_is_0 in L; lra. } - { pose proof (interval_division_valid (a:=vF1) (b:=vF2) (Q2R (fst iv_f1), Q2R (snd iv_f1)) (Q2R (fst iv_f2),Q2R (snd iv_f2))) as valid_div. + { pose proof (interval_division_valid (a:=vF1) (b:=vF2) + (Q2R ivlo_f1, Q2R ivhi_f1) + (Q2R ivlo_f2, Q2R ivhi_f2)) + as valid_div. simpl in *. destruct valid_div; try auto. - destruct L; rewrite <- Q2R0_is_0; [left | right]; apply Qlt_Rlt; auto. - - assert (~ snd iv_f2 == 0). + - assert (~ ivhi_f2 == 0). { hnf; intros. destruct L; try lra. - assert (0 < snd iv_f2) by (apply Rlt_Qlt; apply Qlt_Rlt in H2; lra). + assert (0 < ivhi_f2) by (apply Rlt_Qlt; apply Qlt_Rlt in H2; lra). lra. } - assert (~ fst iv_f2 == 0). + assert (~ ivlo_f2 == 0). { hnf; intros; destruct L; try lra. - assert (fst iv_f2 < 0) by (apply Rlt_Qlt; apply Qlt_Rlt in H3; lra). + assert (ivlo_f2 < 0) by (apply Rlt_Qlt; apply Qlt_Rlt in H3; lra). lra. } repeat (rewrite <- Q2R_inv in *; try auto). repeat rewrite <- Q2R_mult in *. @@ -345,18 +345,18 @@ Proof. unfold perturb. lra. } - - env_assert A (Downcast m f) A_d; - destruct A_d as [iv_d [err_d A_d]]; - env_assert A f A_f; - destruct A_f as [iv_f [err_f A_f]]; - rewrite A_d, A_f in *; simpl in *. + - match_simpl. andb_to_prop valid_bounds. - destruct IHf as [vF [eval_f valid_f]]; try auto. - exists (perturb vF 0). + match_simpl. + destruct IHf as [ivlo_f [ivhi_f [err_f [vF [env_f [eval_f valid_f]]]]]]; + try auto. + inversion env_f; subst. + exists (fst i), (snd i), e, (perturb vF 0). + split; [destruct i; try auto |]. split; [try econstructor; try eauto; try apply Rabs_0_equiv; unfold isMorePrecise; auto |]. - canonize_hyps. - unfold perturb; simpl in *. - lra. + unfold isSupersetIntv in *; andb_to_prop R. + canonize_hyps; simpl in *. + unfold perturb; lra. Qed. Lemma Rmap_updVars_comm Gamma n m: @@ -367,24 +367,6 @@ Proof. intros x; destruct (x =? n); try auto. Qed. -(* Lemma eval_exp_Rmap_updVars_comm e n Gamma E v: *) -(* eval_exp E (toRMap (updDefVars n M0 Gamma)) (toREval (toRExp e)) v M0 -> *) -(* eval_exp E (updDefVars n M0 (toRMap Gamma)) (toREval (toRExp e)) v M0. *) -(* Proof. *) -(* revert v; *) -(* induction e; intros * eval_e; inversion eval_e; subst; simpl in *; *) -(* auto. *) -(* - constructor; try auto. *) -(* erewrite test3; eauto. *) -(* - rewrite H2 in *. *) -(* apply M0_join_is_M0 in H2. *) -(* destruct H2; subst. *) -(* eauto. *) -(* - apply M0_least_precision in H1; subst. *) -(* econstructor; try eauto. *) -(* apply isMorePrecise_refl. *) -(* Qed. *) - Lemma swap_Gamma_eval_exp e E vR m Gamma1 Gamma2: (forall n, Gamma1 n = Gamma2 n) -> eval_exp E Gamma1 e vR m -> @@ -418,95 +400,78 @@ Proof. Qed. Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult) Gamma: - forall E fVars dVars outVars elo ehi err P, + forall E fVars dVars outVars P, ssa f (NatSet.union fVars dVars) outVars -> - (forall v, NatSet.mem v dVars = true -> - exists vR, E v = Some vR /\ - (Q2R (fst (fst (A (Var Q v)))) <= vR <= Q2R (snd (fst (A (Var Q v)))))%R) -> - (forall v, NatSet.mem v fVars = true -> - exists vR, E v = Some vR /\ - (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> - (forall v, NatSet.mem v (NatSet.union fVars dVars) = true -> - exists m :mType, Gamma v = Some m) -> + dVars_range_valid dVars E A -> + fVars_P_sound fVars E P -> + vars_typed (NatSet.union fVars dVars) Gamma -> NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars -> validIntervalboundsCmd f A P dVars = true -> - A (getRetExp f) = ((elo, ehi), err) -> - exists vR, + exists elo ehi err vR, + DaisyMap.find (getRetExp f) A = Some ((elo, ehi), err) /\ bstep (toREvalCmd (toRCmd f)) E (toRMap Gamma) vR M0 /\ (Q2R elo <= vR <= Q2R ehi)%R. Proof. revert Gamma. induction f; - intros * ssa_f dVars_sound fVars_valid types_valid usedVars_subset valid_bounds_f A_f. - - inversion ssa_f; subst. - unfold validIntervalboundsCmd in valid_bounds_f. - andb_to_prop valid_bounds_f. + intros * ssa_f dVars_sound fVars_valid types_valid usedVars_subset valid_bounds_f; + cbn in *. + - repeat match_simpl. andb_to_prop valid_bounds_f. inversion ssa_f; subst. - pose proof (validIntervalbounds_sound e A P E Gamma (fVars:=fVars) L) as validIV_e. - destruct validIV_e as [v [eval_e valid_bounds_e]]; try auto. - { simpl in usedVars_subset. - hnf. intros a in_usedVars. - apply usedVars_subset. - rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec. - rewrite NatSet.diff_spec in in_usedVars. - destruct in_usedVars as [ in_usedVars not_dVar]. - repeat split; try auto. + canonize_hyps. + pose proof (validIntervalbounds_sound e (Gamma:=Gamma) (E:=E) (fVars:=fVars) L) as validIV_e. + destruct validIV_e as [v_lo [v_hi [err_v [v [find_v [eval_e valid_bounds_e]]]]]]; + try auto. + { set_tac. repeat split; auto. hnf; intros; subst. set_tac. } + rewrite find_v in *; inversion Heqo; subst. specialize (IHf (updDefVars n M0 Gamma) (updEnv n v E) fVars (NatSet.add n dVars)). assert (NatSet.Equal (NatSet.add n (NatSet.union fVars dVars)) (NatSet.union fVars (NatSet.add n dVars))). - + hnf. intros a; split; intros in_set. - * rewrite NatSet.add_spec, NatSet.union_spec in in_set. - rewrite NatSet.union_spec, NatSet.add_spec. - destruct in_set as [P1 | [ P2 | P3]]; auto. - * rewrite NatSet.add_spec, NatSet.union_spec. - rewrite NatSet.union_spec, NatSet.add_spec in in_set. - destruct in_set as [P1 | [ P2 | P3]]; auto. - + edestruct IHf as [vR [eval_f valid_bounds_f]]; try eauto. + + hnf. intros a; split; intros in_set; set_tac. + * destruct in_set as [ ? | [? ?]]; try auto; set_tac. + destruct H0; auto. + * destruct in_set as [? | ?]; try auto; set_tac. + destruct H as [? | [? ?]]; auto. + + edestruct IHf as [ivlo_f [ivhi_f [err_f [vR [env_f [eval_f valid_bounds_f]]]]]]; + try eauto. eapply ssa_equal_set. symmetry in H. apply H. apply H7. * intros v0 mem_v0. unfold updEnv. case_eq (v0 =? n); intros v0_eq. { rename R1 into eq_lo; rename R0 into eq_hi. - apply Qeq_bool_iff in eq_lo; - apply Qeq_eqR in eq_lo. - apply Qeq_bool_iff in eq_hi; - apply Qeq_eqR in eq_hi. rewrite Nat.eqb_eq in v0_eq; subst. - rewrite <- eq_lo, <- eq_hi. - exists v; split; auto. } - { apply dVars_sound. rewrite NatSet.mem_spec. - rewrite NatSet.mem_spec in mem_v0. - rewrite NatSet.add_spec in mem_v0. - destruct mem_v0; try auto. + exists v; eexists; eexists; eexists; repeat split; try eauto; lra. } + { apply dVars_sound. + set_tac. + destruct mem_v0 as [? | [? ?]]; try auto. rewrite Nat.eqb_neq in v0_eq. - exfalso; apply v0_eq; auto. } + congruence. } * intros v0 mem_fVars. unfold updEnv. case_eq (v0 =? n); intros case_v0; auto. rewrite Nat.eqb_eq in case_v0; subst. - assert (NatSet.mem n (NatSet.union fVars dVars) = true) as in_union. - { rewrite NatSet.mem_spec, NatSet.union_spec; rewrite <- NatSet.mem_spec; auto. } - { rewrite in_union in *; congruence. } + assert (NatSet.In n (NatSet.union fVars dVars)) as in_union by set_tac. + exfalso; set_tac. apply H6; set_tac; auto. * intros x x_contained. set_tac. - rewrite NatSet.union_spec in x_contained. destruct x_contained as [x_free | x_def]. - { destruct (types_valid x) as [m_x Gamma_x]; set_tac. + { destruct (types_valid x) as [m_x Gamma_x]; try set_tac. exists m_x. unfold updDefVars. case_eq (x =? n); intros eq_case; try auto. rewrite Nat.eqb_eq in eq_case. subst. exfalso; apply H6; set_tac. } - { rewrite NatSet.add_spec in x_def. + { set_tac. destruct x_def as [x_n | x_def]; subst. - exists M0; unfold updDefVars; rewrite Nat.eqb_refl; auto. - - destruct (types_valid x) as [m_x Gamma_x]; set_tac. - exists m_x. - unfold updDefVars; case_eq (x =? n); intros eq_case; try auto. - rewrite Nat.eqb_eq in eq_case; subst. - exfalso; apply H6; set_tac. } + - destruct x_def. destruct (types_valid x) as [m_x Gamma_x]. + + rewrite NatSet.union_spec; auto. + + exists m_x. + unfold updDefVars; case_eq (x =? n); intros eq_case; try auto. + rewrite Nat.eqb_eq in eq_case; subst. + congruence. } * clear L R1 R0 R IHf. hnf. intros a a_freeVar. rewrite NatSet.diff_spec in a_freeVar. @@ -521,12 +486,12 @@ Proof. { hnf; intros a_dVar. apply a_no_dVar. rewrite NatSet.add_spec; auto. } - * simpl. exists vR; split; [econstructor; eauto | auto]. + * simpl. exists ivlo_f, ivhi_f, err_f, vR; repeat split; try auto; try lra. + econstructor; try eauto. eapply swap_Gamma_bstep with (Gamma1 := toRMap (updDefVars n M0 Gamma)) ; try eauto. intros n1; erewrite Rmap_updVars_comm; eauto. - unfold validIntervalboundsCmd in valid_bounds_f. - pose proof (validIntervalbounds_sound e A P E Gamma valid_bounds_f dVars_sound usedVars_subset) as valid_iv_e. - destruct valid_iv_e as [vR [eval_e valid_e]]; try auto. - simpl in *; rewrite A_f in *; simpl in *. - exists vR; split; [econstructor; eauto | auto]. + pose proof (validIntervalbounds_sound e (E:=E) (Gamma:=Gamma) valid_bounds_f dVars_sound usedVars_subset) as valid_iv_e. + destruct valid_iv_e as [?[?[?[? [? [? ?]]]]]]; try auto. + simpl in *. repeat eexists; repeat split; try eauto; [econstructor; eauto| | ]; lra. Qed. \ No newline at end of file