From 8c1d93485bbcc56b862c4f7fc2b7737fbbad3333 Mon Sep 17 00:00:00 2001 From: Heiko Becker Date: Thu, 29 Jun 2017 08:46:21 +0200 Subject: [PATCH] Rework typing to get the semantics and typing work closer together. Using this new typing, prove the stronger soundness statement, moving the evaluation to the conclusion of the theorems. --- coq/CertificateChecker.v | 89 ++-- coq/Commands.v | 7 +- coq/Environments.v | 116 ++++- coq/ErrorBounds.v | 42 +- coq/ErrorValidation.v | 840 +++++++++++++++------------------- coq/Expressions.v | 331 ++++++++------ coq/Infra/Ltacs.v | 36 +- coq/Infra/MachineType.v | 252 ++++------ coq/Infra/NatSet.v | 62 ++- coq/Infra/RationalSimps.v | 7 +- coq/Infra/RealRationalProps.v | 29 +- coq/Infra/RealSimps.v | 9 + coq/IntervalArith.v | 79 ++-- coq/IntervalArithQ.v | 7 +- coq/IntervalValidation.v | 750 ++++++++++++++---------------- coq/Typing.v | 194 ++++---- coq/ssaPrgs.v | 10 +- 17 files changed, 1427 insertions(+), 1433 deletions(-) diff --git a/coq/CertificateChecker.v b/coq/CertificateChecker.v index b08819e..8e618bd 100644 --- a/coq/CertificateChecker.v +++ b/coq/CertificateChecker.v @@ -25,22 +25,25 @@ Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) (def the real valued execution respects the precondition. **) Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P defVars: - forall (E1 E2:env) (vR:R) (vF:R) fVars m, - approxEnv E1 defVars absenv fVars NatSet.empty E2 -> - (forall v, NatSet.mem v fVars = true -> + forall (E1 E2:env), + approxEnv E1 defVars absenv (usedVars e) NatSet.empty E2 -> + (forall v, NatSet.mem v (Expressions.usedVars e) = true -> exists vR, E1 v = Some vR /\ (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> - NatSet.Subset (Expressions.usedVars e) fVars -> - eval_exp E1 (toREvalVars defVars) (toREval (toRExp e)) vR M0 -> - eval_exp E2 defVars (toRExp e) vF m -> + (forall v, (v) mem (usedVars e) = true -> + exists m : mType, + defVars v = Some m) -> CertificateChecker e absenv P defVars = true -> + exists vR vF m, + eval_exp E1 (toRMap defVars) (toREval (toRExp e)) vR M0 /\ + eval_exp E2 defVars (toRExp e) vF m /\ (Rabs (vR - vF) <= Q2R (snd (absenv e)))%R. (** The proofs is a simple composition of the soundness proofs for the range validator and the error bound validator. **) Proof. - intros * approxE1E2 P_valid fVars_subset eval_real eval_float certificate_valid. + intros * approxE1E2 P_valid types_defined certificate_valid. unfold CertificateChecker in certificate_valid. rewrite <- andb_lazy_alt in certificate_valid. andb_to_prop certificate_valid. @@ -48,14 +51,23 @@ Proof. destruct env_e as [iv [err absenv_eq]]. destruct iv as [ivlo ivhi]. rewrite absenv_eq; simpl. - eapply validErrorbound_sound; eauto. - - hnf. intros a in_diff. - rewrite NatSet.diff_spec in in_diff. - apply fVars_subset. - destruct in_diff; auto. - - intros v v_in_empty. + pose proof (NatSetProps.empty_union_2 (Expressions.usedVars e) NatSet.empty_spec) as union_empty. + hnf in union_empty. + assert (forall v1, (v1) mem (Expressions.usedVars e ∪ NatSet.empty) = true -> + exists m0 : mType, defVars v1 = Some m0). + { intros; eapply types_defined. + rewrite NatSet.mem_spec in *. + rewrite <- union_empty; eauto. } + assert (NatSet.Subset (usedVars e -- NatSet.empty) (Expressions.usedVars e)). + { hnf; intros a in_empty. + set_tac. } + assert (forall v, (v) mem (NatSet.empty) = true -> exists vR : R, E1 v = Some vR /\ (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R). + { intros v v_in_empty. rewrite NatSet.mem_spec in v_in_empty. - inversion v_in_empty. + inversion v_in_empty. } + edestruct validIntervalbounds_sound as [vR [eval_real real_bounds_e]]; eauto. + destruct (validErrorbound_sound e P (typeMap defVars e) L approxE1E2 H0 eval_real R0 L0 H1 P_valid H absenv_eq) as [vF [mF [eval_float err_bounded]]]; auto. + exists vR; exists vF; exists mF; split; auto. Qed. Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) defVars:= @@ -66,21 +78,25 @@ Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) d else false. Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P defVars: - forall (E1 E2:env) vR vF m, + forall (E1 E2:env), approxEnv E1 defVars absenv (freeVars f) NatSet.empty E2 -> (forall v, NatSet.mem v (freeVars f)= true -> exists vR, E1 v = Some vR /\ (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> - bstep (toREvalCmd (toRCmd f)) E1 (toREvalVars defVars) vR M0 -> - bstep (toRCmd f) E2 defVars vF m -> + (forall v, (v) mem (freeVars f) = true -> + exists m : mType, + defVars v = Some m) -> CertificateCheckerCmd f absenv P defVars = true -> + exists vR vF m, + bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR M0 /\ + bstep (toRCmd f) E2 defVars vF m /\ (Rabs (vR - vF) <= Q2R (snd (absenv (getRetExp f))))%R. (** The proofs is a simple composition of the soundness proofs for the range validator and the error bound validator. **) Proof. - intros * approxE1E2 P_valid eval_real eval_float certificate_valid. + intros * approxE1E2 P_valid types_defined certificate_valid. unfold CertificateCheckerCmd in certificate_valid. repeat rewrite <- andb_lazy_alt in certificate_valid. andb_to_prop certificate_valid. @@ -89,20 +105,25 @@ Proof. env_assert absenv (getRetExp f) env_f. destruct env_f as [iv [err absenv_eq]]. destruct iv as [ivlo ivhi]. + assert (ssa f (freeVars f ∪ NatSet.empty) outVars) as ssa_valid. + { eapply ssa_equal_set; try eauto. + apply NatSetProps.empty_union_2. + apply NatSet.empty_spec. } + assert (forall v, (v) mem (NatSet.empty) = true -> + exists vR : R, + E1 v = Some vR /\ (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R) as no_dVars_valid. + { intros v v_in_empty. + set_tac. inversion v_in_empty. } + assert (forall v, (v) mem (freeVars f ∪ NatSet.empty) = true -> + exists m : mType, defVars v = Some m) as types_valid. + { intros v v_mem; apply types_defined. + set_tac. rewrite NatSet.union_spec in v_mem. + destruct v_mem; try auto. + inversion H. } + assert (NatSet.Subset (freeVars f -- NatSet.empty) (freeVars f)) + as freeVars_contained by set_tac. + edestruct (validIntervalboundsCmd_sound) as [vR [eval_real bounded_real_f]] ; eauto. rewrite absenv_eq; simpl. - eapply (validErrorboundCmd_sound); eauto. - - instantiate (1 := outVars). - eapply ssa_equal_set; try eauto. - hnf. - intros a; split; intros in_union. - + rewrite NatSet.union_spec in in_union. - destruct in_union as [in_fVars | in_empty]; try auto. - inversion in_empty. - + rewrite NatSet.union_spec; auto. - - hnf; intros a in_diff. - rewrite NatSet.diff_spec in in_diff. - destruct in_diff; auto. - - intros v v_in_empty. - rewrite NatSet.mem_spec in v_in_empty. - inversion v_in_empty. -Qed.y + edestruct (validErrorboundCmd_sound) as [vF [mF [eval_float bounded_float]]]; eauto. + exists vR; exists vF; exists mF; split; auto. +Qed. \ No newline at end of file diff --git a/coq/Commands.v b/coq/Commands.v index fee65fa..c78d46c 100644 --- a/coq/Commands.v +++ b/coq/Commands.v @@ -51,16 +51,13 @@ Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop := **) Inductive bstep : cmd R -> env -> (nat -> option mType) -> R -> mType -> Prop := let_b m m' x e s E v res defVars: - eval_exp E defVars e v m -> - defVars x = Some m -> - bstep s (updEnv x v E) defVars res m' -> + eval_exp E defVars e v m -> + bstep s (updEnv x v E) (updDefVars x m defVars) res m' -> bstep (Let m x e s) E defVars res m' |ret_b m e E v defVars: eval_exp E defVars e v m -> bstep (Ret e) E defVars v m. - - (** The free variables of a command are all used variables of expressions without the let bound variables diff --git a/coq/Environments.v b/coq/Environments.v index f6b2d96..ae6f787 100644 --- a/coq/Environments.v +++ b/coq/Environments.v @@ -17,15 +17,14 @@ Inductive approxEnv : env -> (nat -> option mType) -> analysisResult -> NatSet.t approxEnv emptyEnv defVars A NatSet.empty NatSet.empty emptyEnv |approxUpdFree E1 E2 defVars A v1 v2 x fVars dVars m: approxEnv E1 defVars A fVars dVars E2 -> - defVars x = Some m -> - (Rabs (v1 - v2) <= (Rabs v1) * Q2R (meps m))%R -> + (Rabs (v1 - v2) <= (Rabs v1) * Q2R (mTypeToQ m))%R -> NatSet.mem x (NatSet.union fVars dVars) = false -> - approxEnv (updEnv x v1 E1) defVars A (NatSet.add x fVars) dVars (updEnv x v2 E2) -|approxUpdBound E1 E2 defVars A v1 v2 x fVars dVars: + approxEnv (updEnv x v1 E1) (updDefVars x m defVars) A (NatSet.add x fVars) dVars (updEnv x v2 E2) +|approxUpdBound E1 E2 defVars A v1 v2 x fVars dVars m: approxEnv E1 defVars A fVars dVars E2 -> (Rabs (v1 - v2) <= Q2R (snd (A (Var Q x))))%R -> NatSet.mem x (NatSet.union fVars dVars) = false -> - approxEnv (updEnv x v1 E1) defVars A fVars (NatSet.add x dVars) (updEnv x v2 E2). + approxEnv (updEnv x v1 E1) (updDefVars x m defVars) A fVars (NatSet.add x dVars) (updEnv x v2 E2). (* Inductive approxParams :env -> env -> Prop := *) (* |approxParamRefl: *) @@ -34,3 +33,110 @@ Inductive approxEnv : env -> (nat -> option mType) -> analysisResult -> NatSet.t (* approxParams E1 E2 -> *) (* (Rabs (v1 - v2) <= Q2R (meps m))%R -> *) (* approxParams (updEnv x M0 v1 E1) (updEnv x m v2 E2). *) + +Section RelationProperties. + + Variable (x:nat) (v:R) (E1 E2:env) (Gamma:nat -> option mType) (A:analysisResult) (fVars dVars: NatSet.t). + + Hypothesis approxEnvs: approxEnv E1 Gamma A fVars dVars E2. + +Lemma approxEnv_gives_value: + E1 x = Some v -> + NatSet.In x (NatSet.union fVars dVars) -> + exists v', + E2 x = Some v'. +Proof. + induction approxEnvs; + intros E1_def x_valid. + - unfold emptyEnv in E1_def; simpl in E1_def. congruence. + - unfold updEnv in *. + case_eq (x =? x0); intros eq_case; rewrite eq_case in *. + + eexists; eauto. + + eapply IHa; auto. + set_tac. + rewrite NatSet.union_spec in x_valid. + destruct x_valid; set_tac. + rewrite NatSet.add_spec in H1. + destruct H1; subst; try auto. + rewrite Nat.eqb_refl in eq_case; congruence. + - unfold updEnv in *. + case_eq (x =? x0); intros eq_case; rewrite eq_case in *. + + eexists; eauto. + + eapply IHa; auto. + set_tac. + rewrite NatSet.union_spec in x_valid. + destruct x_valid; set_tac. + rewrite NatSet.add_spec in H1. + destruct H1; subst; try auto. + rewrite Nat.eqb_refl in eq_case; congruence. +Qed. + +Arguments mTypeToQ _ : simpl nomatch. + +Lemma approxEnv_fVar_bounded v2 m: + E1 x = Some v -> + E2 x = Some v2 -> + NatSet.In x fVars -> + Gamma x = Some m -> + (Rabs (v - v2) <= (Rabs v) * Q2R (mTypeToQ m))%R. +Proof. + induction approxEnvs; + intros E1_def E2_def x_free x_typed. + - unfold emptyEnv in *; simpl in *; congruence. + - set_tac. + rewrite add_spec_strong in x_free. + destruct x_free as [x_x0 | [x_neq x_free]]; subst. + + unfold updEnv in *; + rewrite Nat.eqb_refl in *; simpl in *. + unfold updDefVars in x_typed. + rewrite Nat.eqb_refl in x_typed. + inversion x_typed; subst. + inversion E1_def; inversion E2_def; subst; auto. + + unfold updEnv in *; simpl in *. + rewrite <- Nat.eqb_neq in x_neq. + rewrite x_neq in *; simpl in *. + unfold updDefVars in x_typed; rewrite x_neq in x_typed. + apply IHa; auto. + - assert (x =? x0 = false) as x_x0_neq. + { rewrite Nat.eqb_neq; hnf; intros; subst. + set_tac. + apply H0. + set_tac. } + unfold updEnv in *; rewrite x_x0_neq in *. + apply IHa; auto. + unfold updDefVars in x_typed; + rewrite x_x0_neq in x_typed; auto. +Qed. + +Lemma approxEnv_dVar_bounded v2 m: + E1 x = Some v -> + E2 x = Some v2 -> + NatSet.In x dVars -> + Gamma x = Some m -> + (Rabs (v - v2) <= Q2R (snd (A (Var Q x))))%R. +Proof. + induction approxEnvs; + intros E1_def E2_def x_def x_typed. + - unfold emptyEnv in *; simpl in *; congruence. + - assert (x =? x0 = false) as x_x0_neq. + { rewrite Nat.eqb_neq; hnf; intros; subst. + set_tac. + apply H0; set_tac. + } + unfold updEnv in *; rewrite x_x0_neq in *. + unfold updDefVars in x_typed; rewrite x_x0_neq in x_typed. + apply IHa; auto. + - set_tac. + rewrite add_spec_strong in x_def. + destruct x_def as [x_x0 | [x_neq x_def]]; subst. + + unfold updEnv in *; + rewrite Nat.eqb_refl in *; simpl in *. + inversion E1_def; inversion E2_def; subst; auto. + + unfold updEnv in *; simpl in *. + rewrite <- Nat.eqb_neq in x_neq. + rewrite x_neq in *; simpl in *. + unfold updDefVars in x_typed; rewrite x_neq in x_typed. + apply IHa; auto. +Qed. + +End RelationProperties. \ No newline at end of file diff --git a/coq/ErrorBounds.v b/coq/ErrorBounds.v index fced5c2..d5f82f9 100644 --- a/coq/ErrorBounds.v +++ b/coq/ErrorBounds.v @@ -9,9 +9,9 @@ Require Import Daisy.Environments Daisy.Infra.ExpressionAbbrevs. Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (m:mType) defVars: - eval_exp E1 (toREvalVars defVars) (Const M0 n) nR M0 -> + eval_exp E1 (toRMap defVars) (Const M0 n) nR M0 -> eval_exp E2 defVars (Const m n) nF m -> - (Rabs (nR - nF) <= Rabs n * (Q2R (meps m)))%R. + (Rabs (nR - nF) <= Rabs n * (Q2R (mTypeToQ m)))%R. Proof. intros eval_real eval_float. inversion eval_real; subst. @@ -20,24 +20,24 @@ Proof. unfold perturb; simpl. rewrite Rabs_err_simpl, Rabs_mult. apply Rmult_le_compat_l; [apply Rabs_pos | auto]. - simpl (meps M0) in *. + simpl (mTypeToQ M0) in *. apply (Rle_trans _ (Q2R 0) _); try auto. rewrite Q2R0_is_0; lra. Qed. Lemma add_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R) (vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q) (m m1 m2:mType) defVars: - eval_exp E1 (toREvalVars defVars) (toREval (toRExp e1)) e1R M0 -> + eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 -> eval_exp E2 defVars (toRExp e1) e1F m1-> - eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) e2R M0 -> + eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 -> eval_exp E2 defVars (toRExp e2) e2F m2 -> - eval_exp E1 (toREvalVars defVars) (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR M0 -> + eval_exp E1 (toRMap defVars) (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR M0 -> eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (updDefVars 2 m2 (updDefVars 1 m1 defVars)) (Binop Plus (Var R 1) (Var R 2)) vF m -> (Rabs (e1R - e1F) <= Q2R err1)%R -> (Rabs (e2R - e2F) <= Q2R err2)%R -> - (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + (Rabs (e1F + e2F) * (Q2R (meps m))))%R. + (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + (Rabs (e1F + e2F) * (Q2R (mTypeToQ m))))%R. Proof. intros e1_real e1_float e2_real e2_float plus_real plus_float bound_e1 bound_e2. (* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *) @@ -94,17 +94,17 @@ Qed. **) Lemma subtract_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R) (vR:R) (vF:R) (E1 E2:env) err1 err2 (m m1 m2:mType) defVars: - eval_exp E1 (toREvalVars defVars) (toREval (toRExp e1)) e1R M0 -> + eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 -> eval_exp E2 defVars (toRExp e1) e1F m1 -> - eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) e2R M0 -> + eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 -> eval_exp E2 defVars (toRExp e2) e2F m2 -> - eval_exp E1 (toREvalVars defVars) (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR M0 -> + eval_exp E1 (toRMap defVars) (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR M0 -> eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (updDefVars 2 m2 (updDefVars 1 m1 defVars)) (Binop Sub (Var R 1) (Var R 2)) vF m -> (Rabs (e1R - e1F) <= Q2R err1)%R -> (Rabs (e2R - e2F) <= Q2R err2)%R -> - (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + ((Rabs (e1F - e2F)) * (Q2R (meps m))))%R. + (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + ((Rabs (e1F - e2F)) * (Q2R (mTypeToQ m))))%R. Proof. intros e1_real e1_float e2_real e2_float sub_real sub_float bound_e1 bound_e2. (* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *) @@ -155,15 +155,15 @@ Qed. Lemma mult_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R) (vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars: - eval_exp E1 (toREvalVars defVars) (toREval (toRExp e1)) e1R M0 -> + eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 -> eval_exp E2 defVars (toRExp e1) e1F m1 -> - eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) e2R M0 -> + eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 -> eval_exp E2 defVars (toRExp e2) e2F m2 -> - eval_exp E1 (toREvalVars defVars) (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR M0 -> + eval_exp E1 (toRMap defVars) (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR M0 -> eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (updDefVars 2 m2 (updDefVars 1 m1 defVars)) (Binop Mult (Var R 1) (Var R 2)) vF m -> - (Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R (meps m)))%R. + (Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R (mTypeToQ m)))%R. Proof. intros e1_real e1_float e2_real e2_float mult_real mult_float. (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *) @@ -206,15 +206,15 @@ Qed. Lemma div_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R) (vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars: - eval_exp E1 (toREvalVars defVars) (toREval (toRExp e1)) e1R M0 -> + eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 -> eval_exp E2 defVars (toRExp e1) e1F m1 -> - eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) e2R M0 -> + eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 -> eval_exp E2 defVars (toRExp e2) e2F m2 -> - eval_exp E1 (toREvalVars defVars) (toREval (Binop Div (toRExp e1) (toRExp e2))) vR M0 -> + eval_exp E1 (toRMap defVars) (toREval (Binop Div (toRExp e1) (toRExp e2))) vR M0 -> eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (updDefVars 2 m2 (updDefVars 1 m1 defVars)) (Binop Div (Var R 1) (Var R 2)) vF m -> - (Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R (meps m)))%R. + (Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R (mTypeToQ m)))%R. Proof. intros e1_real e1_float e2_real e2_float div_real div_float. (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *) @@ -433,13 +433,13 @@ Proof. Qed. Lemma round_abs_err_bounded (e:exp R) (nR nF1 nF:R) (E1 E2: env) (err:R) (machineEpsilon m:mType) defVars: - eval_exp E1 (toREvalVars defVars) (toREval e) nR M0 -> + eval_exp E1 (toRMap defVars) (toREval e) nR M0 -> eval_exp E2 defVars e nF1 m -> eval_exp (updEnv 1 nF1 emptyEnv) (updDefVars 1 m defVars) (toRExp (Downcast machineEpsilon (Var Q 1))) nF machineEpsilon-> (Rabs (nR - nF1) <= err)%R -> - (Rabs (nR - nF) <= err + (Rabs nF1) * Q2R (meps machineEpsilon))%R. + (Rabs (nR - nF) <= err + (Rabs nF1) * Q2R (mTypeToQ machineEpsilon))%R. Proof. intros eval_real eval_float eval_float_rnd err_bounded. replace (nR - nF)%R with ((nR - nF1) + (nF1 - nF))%R by lra. diff --git a/coq/ErrorValidation.v b/coq/ErrorValidation.v index edf05d4..0faba43 100644 --- a/coq/ErrorValidation.v +++ b/coq/ErrorValidation.v @@ -6,7 +6,7 @@ encoded in the analysis result. The validator is used in the file CertificateChecker.v to build the complete checker. **) -Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals Coq.Lists.List. +Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals. Require Import Coq.micromega.Psatz Coq.Reals.Reals. Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps Daisy.Infra.RealSimps Daisy.Infra.Ltacs. Require Import Daisy.Environments Daisy.IntervalValidation Daisy.Typing Daisy.ErrorBounds. @@ -24,9 +24,9 @@ Fixpoint validErrorbound (e:exp Q) (typeMap:exp Q -> option mType) (absenv:analy |Var _ v => if (NatSet.mem v dVars) then true - else (Qleb (maxAbs intv * (meps m)) err) + else (Qleb (maxAbs intv * (mTypeToQ m)) err) |Const _ n => - Qleb (maxAbs intv * (meps m)) err + Qleb (maxAbs intv * (mTypeToQ m)) err |Unop Neg e1 => if (validErrorbound e1 typeMap absenv dVars) then Qeq_bool err (snd (absenv e1)) @@ -43,11 +43,11 @@ Fixpoint validErrorbound (e:exp Q) (typeMap:exp Q -> option mType) (absenv:analy let upperBoundE2 := maxAbs ive2 in match b with | Plus => - Qleb (err1 + err2 + (maxAbs (addIntv errIve1 errIve2)) * (meps m)) err + Qleb (err1 + err2 + (maxAbs (addIntv errIve1 errIve2)) * (mTypeToQ m)) err | Sub => - Qleb (err1 + err2 + (maxAbs (subtractIntv errIve1 errIve2)) * (meps m)) err + Qleb (err1 + err2 + (maxAbs (subtractIntv errIve1 errIve2)) * (mTypeToQ m)) err | Mult => - Qleb ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbs (multIntv errIve1 errIve2)) * (meps m)) err + Qleb ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbs (multIntv errIve1 errIve2)) * (mTypeToQ m)) err | Div => if (((Qleb (ivhi errIve2) 0) && (negb (Qeq_bool (ivhi errIve2) 0))) || ((Qleb 0 (ivlo errIve2)) && (negb (Qeq_bool (ivlo errIve2) 0)))) @@ -55,20 +55,22 @@ Fixpoint validErrorbound (e:exp Q) (typeMap:exp Q -> option mType) (absenv:analy let upperBoundInvE2 := maxAbs (invertIntv ive2) in let minAbsIve2 := minAbs (errIve2) in let errInv := (1 / (minAbsIve2 * minAbsIve2)) * err2 in - Qleb ((upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbs (divideIntv errIve1 errIve2)) * (meps m)) err + Qleb ((upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbs (divideIntv errIve1 errIve2)) * (mTypeToQ m)) err else false end else false |Downcast m1 e1 => - let (ive1, err1) := absenv e1 in - let rec := validErrorbound e1 typeMap absenv dVars in - let errIve1 := widenIntv ive1 err1 in - andb rec (Qleb (err1 + maxAbs errIve1 * (meps m1)) err) + if validErrorbound e1 typeMap absenv dVars + then + let (ive1, err1) := absenv e1 in + let errIve1 := widenIntv ive1 err1 in + (Qleb (err1 + maxAbs errIve1 * (mTypeToQ m1)) err) + else + false end else false end. - (** Error bound command validator **) Fixpoint validErrorboundCmd (f:cmd Q) (typeMap:exp Q -> option mType) (env:analysisResult) (dVars:NatSet.t) {struct f} : bool := match f with @@ -109,15 +111,16 @@ Proof. + destruct (tmap (Downcast m e));inversion validErrorbound_e. Qed. +Arguments mTypeToQ _ :simpl nomatch. Lemma validErrorboundCorrectVariable: - forall E1 E2 absenv (v:nat) nR nF e nlo nhi P fVars dVars m Gamma defVars, - typeCheck (Var Q v) defVars Gamma = true -> - approxEnv E1 defVars absenv fVars dVars E2 -> - eval_exp E1 (toREvalVars defVars) (toREval (toRExp (Var Q v))) nR M0 -> - eval_exp E2 defVars (toRExp (Var Q v)) nF m -> + forall E1 E2 absenv (v:nat) e nR nlo nhi P fVars dVars Gamma expTypes, + eval_exp E1 (toRMap Gamma) (toREval (toRExp (Var Q v))) nR M0 -> + typeCheck (Var Q v) Gamma expTypes = true -> + approxEnv E1 Gamma absenv fVars dVars E2 -> validIntervalbounds (Var Q v) absenv P dVars = true -> - validErrorbound (Var Q v) Gamma absenv dVars = true -> + validErrorbound (Var Q v) expTypes absenv dVars = true -> + NatSet.Subset (NatSet.diff (usedVars (Var Q v)) dVars) fVars -> (forall v1, NatSet.mem v1 dVars = true -> exists r, E1 v1 = Some r /\ @@ -125,194 +128,118 @@ Lemma validErrorboundCorrectVariable: (forall v1, NatSet.mem v1 fVars= true -> exists r, E1 v1 = Some r /\ (Q2R (fst (P v1)) <= r <= Q2R (snd (P v1)))%R) -> + (forall v1 : NatSet.elt, + NatSet.mem v1 (NatSet.union fVars dVars) = true -> + exists m0 : mType, Gamma v1 = Some m0) -> absenv (Var Q v) = ((nlo, nhi), e) -> + exists nF m, + eval_exp E2 Gamma (toRExp (Var Q v)) nF m /\ (Rabs (nR - nF) <= (Q2R e))%R. Proof. - intros * typing_ok approxCEnv eval_real eval_float bounds_valid error_valid dVars_sound P_valid absenv_var. - simpl in eval_real; inversion eval_real; inversion eval_float; subst. - rename H1 into E1_v; - rename H6 into E2_v. - simpl in error_valid. - rewrite absenv_var in error_valid; simpl in error_valid; subst. - case_eq (Gamma (Var Q v)); intros; rewrite H in error_valid; [ | inversion error_valid]. - rewrite <- andb_lazy_alt in error_valid. + intros * eval_real typing_ok approxCEnv bounds_valid error_valid v_sound dVars_sound P_valid types_valid absenv_var. + eapply validIntervalbounds_sound in bounds_valid; eauto. + destruct bounds_valid as [nR2 [eval_real2 bounds_valid]]. + assert (nR2 = nR) by (eapply meps_0_deterministic; eauto); + subst. + simpl in eval_real; inversion eval_real; subst. + rename H1 into E1_v. + simpl in *. + assert (exists m, Gamma v = Some m) as v_has_type. + { destruct (expTypes (Var Q v)); try congruence. + case_eq (Gamma v); intros * gamma_v; + rewrite gamma_v in *; eauto. } + destruct v_has_type as [m type_v]. + assert (exists nF, eval_exp E2 Gamma (Var R v) nF m) as eval_float. + { destruct (approxEnv_gives_value approxCEnv E1_v); try eauto. + set_tac. + case_eq (NatSet.mem v dVars); intros v_case; set_tac. + left; apply v_sound. + apply NatSetProps.FM.diff_3; set_tac. } + destruct eval_float as [nF eval_float]. + repeat eexists; try eauto. + rewrite absenv_var in error_valid; simpl in error_valid. + case_eq (expTypes (Var Q v)); + intros * expType_v; rewrite expType_v in *; try congruence. + rewrite type_v in *; simpl in *. + rewrite mTypeEq_compat_eq in typing_ok; subst. andb_to_prop error_valid. rename L into error_pos. rename R into error_valid. - (* induction on the approximation relation to do a case distinction on whether - we argue currently about a free or a let bound variable *) - induction approxCEnv. - (* empty environment case, contradiction *) - - unfold emptyEnv in *; simpl in *. - congruence. - - unfold updEnv in *; simpl in *. - case_eq (v =? x); intros eq_case; rewrite eq_case in *. - + rewrite Nat.eqb_eq in eq_case; subst. - assert (NatSet.mem x dVars = false) as x_not_bound. - * case_eq (NatSet.mem x dVars); intros case_mem; try auto. - rewrite NatSet.mem_spec in case_mem. - assert (NatSet.In x (NatSet.union fVars dVars)) - as x_in_union by (rewrite NatSet.union_spec; auto). - rewrite <- NatSet.mem_spec in x_in_union. - rewrite x_in_union in *. - congruence. - * rewrite x_not_bound in error_valid. - inversion E1_v; inversion E2_v; subst. - eapply Rle_trans; try eauto. - apply Qle_bool_iff in error_valid. - apply Qle_Rle in error_valid. - eapply Rle_trans; eauto. - rewrite Q2R_mult. - rewrite H5 in H1; inversion H1; subst. - rewrite H,H5 in typing_ok; apply EquivEqBoolEq in typing_ok; subst. - clear H5 H3. - apply Rmult_le_compat_r. - { apply meps_posR. } - { rewrite <- maxAbs_impl_RmaxAbs. - apply contained_leq_maxAbs. - unfold contained; simpl. - assert ((toRExp (Var Q x)) = Var R x) by (simpl; auto). - rewrite <- H3 in eval_float. - pose proof (validIntervalbounds_sound (Var Q x) A P (E:=fun y : nat => if y =? x then Some nR else E1 y) (vR:=nR) defVars bounds_valid (fVars := (NatSet.add x fVars))) as valid_bounds_prf. - rewrite absenv_var in valid_bounds_prf; simpl in valid_bounds_prf. - apply valid_bounds_prf; try auto. - - intros v v_mem_diff. - rewrite NatSet.diff_spec, NatSet.singleton_spec in v_mem_diff. - destruct v_mem_diff as [v_eq v_no_dVar]. - subst. - rewrite NatSet.add_spec; auto. } - + apply IHapproxCEnv; try auto. - * constructor; auto. - * constructor; auto. - * intros v0 mem_dVars. - specialize (dVars_sound v0 mem_dVars). - destruct dVars_sound as [vR0 iv_sound_val]. - case_eq (v0 =? x); intros case_mem; - rewrite case_mem in iv_sound_val; simpl in iv_sound_val. - { rewrite Nat.eqb_eq in case_mem; subst. - rewrite NatSet.mem_spec in mem_dVars. - assert (NatSet.In x (NatSet.union fVars dVars)) - as x_in_union by (rewrite NatSet.union_spec; auto). - rewrite <- NatSet.mem_spec in x_in_union; - rewrite x_in_union in *; congruence. } - { exists vR0. split; auto; destruct iv_sound_val as [E1_v0 iv_sound_val]; auto. } - * intros v0 v0_fVar. - assert (NatSet.mem v0 (NatSet.add x fVars) = true) - as v0_in_add by (rewrite NatSet.mem_spec, NatSet.add_spec; rewrite NatSet.mem_spec in v0_fVar; auto). - specialize (P_valid v0 v0_in_add). - case_eq (v0 =? x); intros case_v0; rewrite case_v0 in *; try auto. - rewrite Nat.eqb_eq in case_v0; subst. - assert (NatSet.mem x (NatSet.union fVars dVars) = true) - as x_in_union - by (rewrite NatSet.mem_spec, NatSet.union_spec; rewrite NatSet.mem_spec in v0_fVar; auto). - rewrite x_in_union in *; congruence. - - unfold updEnv in E1_v, E2_v; simpl in *. - case_eq (v =? x); intros eq_case; rewrite eq_case in *. - + rewrite Nat.eqb_eq in eq_case; subst. - inversion E1_v; inversion E2_v; subst. - rewrite absenv_var in *; auto. - + apply IHapproxCEnv; try auto. - * constructor; auto. - * constructor; auto. - * rewrite absenv_var. - case_eq (NatSet.mem v dVars); - intros case_dVars; rewrite case_dVars in *; simpl in *; try auto. - assert (NatSet.mem v (NatSet.add x dVars) = false) as not_in_add. - { case_eq (NatSet.mem v (NatSet.add x dVars)); - intros case_add; rewrite case_add in *; simpl in *; try auto. - - rewrite NatSet.mem_spec in case_add. - rewrite NatSet.add_spec in case_add. - destruct case_add as [v_eq_x | v_dVar]; subst. - + rewrite Nat.eqb_neq in eq_case. exfalso; apply eq_case; auto. - + rewrite <- NatSet.mem_spec in v_dVar. rewrite v_dVar in case_dVars. - inversion case_dVars. } - { rewrite absenv_var in bounds_valid. rewrite not_in_add in bounds_valid. - auto. } - * rewrite absenv_var in bounds_valid; simpl in *. - case_eq (NatSet.mem v dVars); - intros case_dVars; rewrite case_dVars in *; simpl in *; try auto. - assert (NatSet.mem v (NatSet.add x dVars) = false) as not_in_add. - { case_eq (NatSet.mem v (NatSet.add x dVars)); - intros case_add; rewrite case_add in *; simpl in *; try auto. - - rewrite NatSet.mem_spec in case_add. - rewrite NatSet.add_spec in case_add. - destruct case_add as [v_eq_x | v_dVar]; subst. - + rewrite Nat.eqb_neq in eq_case. exfalso; apply eq_case; auto. - + rewrite <- NatSet.mem_spec in v_dVar. rewrite v_dVar in case_dVars. - inversion case_dVars. } - { rewrite not_in_add in error_valid; auto. } - * intros v0 mem_dVars. - specialize (dVars_sound v0). - rewrite absenv_var in *; simpl in *. - rewrite NatSet.mem_spec in mem_dVars. - assert (NatSet.In v0 (NatSet.add x dVars)) as v0_in_add. - { rewrite NatSet.add_spec. right; auto. } - { rewrite <- NatSet.mem_spec in v0_in_add. - specialize (dVars_sound v0_in_add). - destruct dVars_sound as [vR0 [val_def iv_sound_val]]. - exists vR0; split; auto. - unfold updEnv in val_def; simpl in val_def. - case_eq (v0 =? x); intros case_mem; - rewrite case_mem in val_def; simpl in val_def. - - rewrite Nat.eqb_eq in case_mem; subst. - apply (NatSetProps.Dec.F.union_3 fVars) in mem_dVars. - rewrite <- NatSet.mem_spec in mem_dVars. - rewrite mem_dVars in *; congruence. - - auto. } - * rewrite absenv_var in bounds_valid. - intros v0 v0_fVar. - specialize (P_valid v0 v0_fVar). - unfold updEnv in P_valid; simpl in *. - case_eq (v0 =? x); intros case_v0; rewrite case_v0 in *; try auto. - rewrite Nat.eqb_eq in case_v0; subst. - assert (NatSet.mem x (NatSet.union fVars dVars) = true) - as x_in_union - by (rewrite NatSet.mem_spec, NatSet.union_spec; rewrite NatSet.mem_spec in v0_fVar; auto). - rewrite x_in_union in *; congruence. + inversion eval_float; subst. + case_eq (v mem dVars); [intros v_dVar | intros v_fVar]. + - rewrite v_dVar in *; simpl in *. + rewrite NatSet.mem_spec in v_dVar. + pose proof (approxEnv_dVar_bounded approxCEnv E1_v H2 v_dVar H1). + rewrite absenv_var in *; simpl in *; auto. + - rewrite v_fVar in *; simpl in *. + apply not_in_not_mem in v_fVar. + assert (v ∈ fVars) as v_in_fVars by set_tac. + pose proof (approxEnv_fVar_bounded approxCEnv E1_v H2 v_in_fVars H1). + eapply Rle_trans. + apply H. + canonize_hyps. + rewrite Q2R_mult in error_valid. + rewrite <- maxAbs_impl_RmaxAbs in error_valid. + eapply Rle_trans; eauto. + eapply Rmult_le_compat_r. + + apply mTypeToQ_pos_R. + + rewrite absenv_var in *; simpl in *. + destruct bounds_valid as [valid_lo valid_hi]. + apply RmaxAbs; eauto. Qed. -Lemma validErrorboundCorrectConstant: - forall E1 E2 absenv (n:Q) nR nF e nlo nhi dVars m Gamma defVars, - eval_exp E1 (toREvalVars defVars) (toREval (toRExp (Const m n))) nR M0 -> - eval_exp E2 defVars (toRExp (Const m n)) nF m -> +Lemma validErrorboundCorrectConstant E1 E2 absenv m n nR e nlo nhi dVars Gamma defVars: + eval_exp E1 (toRMap defVars) (toREval (toRExp (Const m n))) nR M0 -> typeCheck (Const m n) defVars Gamma = true -> validErrorbound (Const m n) Gamma absenv dVars = true -> (Q2R nlo <= nR <= Q2R nhi)%R -> absenv (Const m n) = ((nlo,nhi),e) -> + exists nF m', + eval_exp E2 defVars (toRExp (Const m n)) nF m' /\ (Rabs (nR - nF) <= (Q2R e))%R. Proof. - intros * eval_real eval_float subexpr_ok error_valid intv_valid absenv_const. + intros eval_real subexpr_ok error_valid intv_valid absenv_const. + assert (eval_exp E2 defVars (toRExp (Const m n)) (perturb (Q2R n) (Q2R (mTypeToQ m))) m) as eval_float. + { constructor. rewrite Rabs_eq_Qabs. + apply Qle_Rle. + rewrite Qabs_pos; try lra. + apply mTypeToQ_pos_Q. } + exists (perturb (Q2R n) (Q2R (mTypeToQ m))); + exists m. + split; try auto. eapply Rle_trans. simpl in eval_real,eval_float. eapply const_abs_err_bounded; eauto. unfold validErrorbound in error_valid. rewrite absenv_const in *; simpl in *. - case_eq (Gamma (Const m n)); intros; rewrite H in error_valid; [ | inversion error_valid ]. + case_eq (Gamma (Const m n)); intros * type_const; + rewrite type_const in error_valid; [ | inversion error_valid ]. andb_to_prop error_valid. rename R into error_valid. inversion eval_real; subst. - simpl in H3; rewrite Q2R0_is_0 in H3. - rewrite delta_0_deterministic in *; auto. + simpl in *; rewrite Q2R0_is_0 in *. + rewrite delta_0_deterministic in intv_valid; auto. apply Qle_bool_iff in error_valid. apply Qle_Rle in error_valid. destruct intv_valid. eapply Rle_trans. - eapply Rmult_le_compat_r. - apply meps_posR. + apply mTypeToQ_pos_R. apply RmaxAbs; eauto. - rewrite Q2R_mult in error_valid. rewrite <- maxAbs_impl_RmaxAbs in error_valid; auto. inversion subexpr_ok; subst. - rewrite H in H4. apply EquivEqBoolEq in H4; subst; auto. + rewrite type_const in *. + apply mTypeEq_compat_eq in H3; subst; auto. Qed. Lemma validErrorboundCorrectAddition E1 E2 absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) (alo ahi e1lo e1hi e2lo e2hi:Q) dVars m m1 m2 Gamma defVars: - m = computeJoin m1 m2 -> - eval_exp E1 (toREvalVars defVars) (toREval (toRExp e1)) nR1 M0 -> - eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) nR2 M0 -> - eval_exp E1 (toREvalVars defVars) (toREval (toRExp (Binop Plus e1 e2))) nR M0 -> + m = join m1 m2 -> + eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) nR1 M0 -> + eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) nR2 M0 -> + eval_exp E1 (toRMap defVars) (toREval (toRExp (Binop Plus e1 e2))) nR M0 -> eval_exp E2 defVars (toRExp e1) nF1 m1 -> eval_exp E2 defVars (toRExp e2) nF2 m2 -> eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) @@ -343,7 +270,7 @@ Proof. case_eq (Gamma e1); intros; rewrite H0 in subexpr_ok; [ | inversion subexpr_ok ]. case_eq (Gamma e2); intros; rewrite H1 in subexpr_ok; [ | inversion subexpr_ok ]. andb_to_prop subexpr_ok. - apply EquivEqBoolEq in L0; subst. + apply mTypeEq_compat_eq in L0; subst. pose proof (typingSoundnessExp _ _ R0 e1_float). pose proof (typingSoundnessExp _ _ R e2_float). rewrite H0 in H2; rewrite H1 in H3; inversion H2; inversion H3; subst. @@ -353,7 +280,7 @@ Proof. eapply Rle_trans. apply Rplus_le_compat_l. eapply Rmult_le_compat_r. - apply meps_posR. + apply mTypeToQ_pos_R. Focus 2. rewrite Qle_bool_iff in valid_error. apply Qle_Rle in valid_error. @@ -374,11 +301,11 @@ Proof. assert (ivhi iv = ivh) by (rewrite iv_unf; auto). rewrite <- H0, <- H1. assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto. - pose proof (distance_gives_iv (a:=nR1) _ contained_intv1 err1_bounded). + pose proof (distance_gives_iv (a:=nR1) _ (Q2R e1lo, Q2R e1hi) contained_intv1 err1_bounded). assert (contained nR2 (Q2R e2lo, Q2R e2hi)) as contained_intv2 by auto. - pose proof (distance_gives_iv (a:=nR2) _ contained_intv2 err2_bounded). - pose proof (IntervalArith.interval_addition_valid H2 H3). - unfold IntervalArith.contained in H4. + pose proof (distance_gives_iv (a:=nR2) _ (Q2R e2lo, Q2R e2hi) contained_intv2 err2_bounded). + pose proof (IntervalArith.interval_addition_valid _ _ H2 H3). + simpl in *. destruct H4. subst; simpl in *. apply RmaxAbs; simpl. @@ -393,10 +320,10 @@ Qed. Lemma validErrorboundCorrectSubtraction E1 E2 absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars: - m = computeJoin m1 m2 -> - eval_exp E1 (toREvalVars defVars) (toREval (toRExp e1)) nR1 M0 -> - eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) nR2 M0 -> - eval_exp E1 (toREvalVars defVars) (toREval (toRExp (Binop Sub e1 e2))) nR M0 -> + m = join m1 m2 -> + eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) nR1 M0 -> + eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) nR2 M0 -> + eval_exp E1 (toRMap defVars) (toREval (toRExp (Binop Sub e1 e2))) nR M0 -> eval_exp E2 defVars (toRExp e1) nF1 m1-> eval_exp E2 defVars (toRExp e2) nF2 m2 -> eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) @@ -425,7 +352,7 @@ Proof. case_eq (Gamma e1); intros; rewrite H0 in subexpr_ok; [ | inversion subexpr_ok ]. case_eq (Gamma e2); intros; rewrite H1 in subexpr_ok; [ | inversion subexpr_ok ]. andb_to_prop subexpr_ok. - apply EquivEqBoolEq in L0; subst. + apply mTypeEq_compat_eq in L0; subst. pose proof (typingSoundnessExp _ _ R0 e1_float). pose proof (typingSoundnessExp _ _ R e2_float). rewrite H0 in H2; rewrite H1 in H3; inversion H2; inversion H3; subst. @@ -443,7 +370,7 @@ Proof. eapply Rle_trans. apply Rplus_le_compat_l. eapply Rmult_le_compat_r. - apply meps_posR. + apply mTypeToQ_pos_R. Focus 2. apply valid_error. remember (subtractIntv (widenIntv (e1lo, e1hi) err1) (widenIntv (e2lo, e2hi) err2)) as iv. @@ -455,11 +382,11 @@ Proof. assert (ivhi iv = ivh) by (rewrite iv_unf; auto). rewrite <- H0, <- H1. assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto. - pose proof (distance_gives_iv (a:=nR1) _ contained_intv1 err1_bounded). + pose proof (distance_gives_iv (a:=nR1) _ _ contained_intv1 err1_bounded). assert (contained nR2 (Q2R e2lo, Q2R e2hi)) as contained_intv2 by auto. - pose proof (distance_gives_iv (a:=nR2) _ contained_intv2 err2_bounded). - pose proof (IntervalArith.interval_subtraction_valid H2 H3). - unfold IntervalArith.contained in H4. + pose proof (distance_gives_iv (a:=nR2) _ _ contained_intv2 err2_bounded). + pose proof (IntervalArith.interval_subtraction_valid _ _ H2 H3). + simpl in *. destruct H4. subst; simpl in *. apply RmaxAbs; simpl. @@ -480,10 +407,10 @@ Qed. Lemma validErrorboundCorrectMult E1 E2 absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars: - m = computeJoin m1 m2 -> - eval_exp E1 (toREvalVars defVars) (toREval (toRExp e1)) nR1 M0 -> - eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) nR2 M0 -> - eval_exp E1 (toREvalVars defVars) (toREval (toRExp (Binop Mult e1 e2))) nR M0 -> + m = join m1 m2 -> + eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) nR1 M0 -> + eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) nR2 M0 -> + eval_exp E1 (toRMap defVars) (toREval (toRExp (Binop Mult e1 e2))) nR M0 -> eval_exp E2 defVars (toRExp e1) nF1 m1 -> eval_exp E2 defVars (toRExp e2) nF2 m2 -> eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) @@ -512,7 +439,7 @@ Proof. case_eq (Gamma e1); intros; rewrite H0 in subexpr_ok; [ | inversion subexpr_ok ]. case_eq (Gamma e2); intros; rewrite H1 in subexpr_ok; [ | inversion subexpr_ok ]. andb_to_prop subexpr_ok. - apply EquivEqBoolEq in L0; subst. + apply mTypeEq_compat_eq in L0; subst. pose proof (typingSoundnessExp _ _ R0 e1_float). pose proof (typingSoundnessExp _ _ R e2_float). rewrite H0 in H2; rewrite H1 in H3; inversion H2; inversion H3; subst. @@ -521,7 +448,7 @@ Proof. rename R2 into valid_error. assert (0 <= Q2R err1)%R as err1_pos by (eapply (err_always_positive e1 Gamma absenv dVars); eauto). assert (0 <= Q2R err2)%R as err2_pos by (eapply (err_always_positive e2 Gamma absenv dVars); eauto). - clear R L1. + clear R1 L1. apply Qle_bool_iff in valid_error. apply Qle_Rle in valid_error. repeat rewrite Q2R_plus in valid_error. @@ -539,16 +466,16 @@ Proof. (* Before doing case distinction, prove bounds that will be used many times: *) assert (nR1 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi))%R as upperBound_nR1 - by (apply contained_leq_maxAbs_val; unfold contained; auto). + by (apply contained_leq_maxAbs_val; auto). assert (nR2 <= RmaxAbsFun (Q2R e2lo, Q2R e2hi))%R as upperBound_nR2 - by (apply contained_leq_maxAbs_val; unfold contained; auto). + by (apply contained_leq_maxAbs_val; auto). assert (-nR1 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi))%R as upperBound_Ropp_nR1 - by (apply contained_leq_maxAbs_neg_val; unfold contained; auto). + by (apply contained_leq_maxAbs_neg_val; auto). assert (- nR2 <= RmaxAbsFun (Q2R e2lo, Q2R e2hi))%R as upperBound_Ropp_nR2 - by (apply contained_leq_maxAbs_neg_val; unfold contained; auto). + by (apply contained_leq_maxAbs_neg_val; auto). assert (nR1 * Q2R err2 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2)%R as bound_nR1 by (apply Rmult_le_compat_r; auto). assert (- nR1 * Q2R err2 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2)%R @@ -997,15 +924,15 @@ Proof. assert (ivhi iv = ivh) by (rewrite iv_unf; auto). rewrite <- H0, <- H1. assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto. - pose proof (distance_gives_iv (a:=nR1) _ contained_intv1 err1_bounded). + pose proof (distance_gives_iv (a:=nR1) _ _ contained_intv1 err1_bounded). assert (contained nR2 (Q2R e2lo, Q2R e2hi)) as contained_intv2 by auto. - pose proof (distance_gives_iv (a:=nR2) _ contained_intv2 err2_bounded). - pose proof (IntervalArith.interval_multiplication_valid H2 H3). - unfold IntervalArith.contained in H4. + pose proof (distance_gives_iv (a:=nR2) _ _ contained_intv2 err2_bounded). + pose proof (IntervalArith.interval_multiplication_valid _ _ H2 H3). + simpl in *. destruct H4. unfold RmaxAbsFun. apply Rmult_le_compat_r. - apply meps_posR. + apply mTypeToQ_pos_R. apply RmaxAbs; subst; simpl in *. + rewrite Q2R_min4. repeat rewrite Q2R_mult; @@ -1020,10 +947,10 @@ Qed. Lemma validErrorboundCorrectDiv E1 E2 absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars: - m = computeJoin m1 m2 -> - eval_exp E1 (toREvalVars defVars) (toREval (toRExp e1)) nR1 M0 -> - eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) nR2 M0 -> - eval_exp E1 (toREvalVars defVars) (toREval (toRExp (Binop Div e1 e2))) nR M0 -> + m = join m1 m2 -> + eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) nR1 M0 -> + eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) nR2 M0 -> + eval_exp E1 (toRMap defVars) (toREval (toRExp (Binop Div e1 e2))) nR M0 -> eval_exp E2 defVars (toRExp e1) nF1 m1 -> eval_exp E2 defVars (toRExp e2) nF2 m2 -> eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) @@ -1053,7 +980,7 @@ Proof. case_eq (Gamma e1); intros; rewrite H0 in subexpr_ok; [ | inversion subexpr_ok ]. case_eq (Gamma e2); intros; rewrite H1 in subexpr_ok; [ | inversion subexpr_ok ]. andb_to_prop subexpr_ok. - apply EquivEqBoolEq in L0; subst. + apply mTypeEq_compat_eq in L0; subst. pose proof (typingSoundnessExp _ _ R0 e1_float). pose proof (typingSoundnessExp _ _ R e2_float). rewrite H0 in H2; rewrite H1 in H3; inversion H2; inversion H3; subst. @@ -1062,9 +989,9 @@ Proof. rename R3 into valid_error. rename L0 into no_div_zero_float. assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto. - pose proof (distance_gives_iv (a:=nR1) _ contained_intv1 err1_bounded). + pose proof (distance_gives_iv (a:=nR1) _ _ contained_intv1 err1_bounded). assert (contained nR2 (Q2R e2lo, Q2R e2hi)) as contained_intv2 by auto. - pose proof (distance_gives_iv (a:=nR2) _ contained_intv2 err2_bounded). + pose proof (distance_gives_iv (a:=nR2) _ _ contained_intv2 err2_bounded). assert (0 <= Q2R err1)%R as err1_pos by (eapply (err_always_positive e1 Gamma absenv); eauto). assert (0 <= Q2R err2)%R as err2_pos by (eapply (err_always_positive e2 Gamma absenv); eauto). apply Qle_bool_iff in valid_error. @@ -1091,26 +1018,26 @@ Proof. + clear absenv_e1 absenv_e2 valid_error eval_float eval_real e1_float e1_real e2_float e2_real absenv_div E1 E2 alo ahi nR nF e L. - unfold IntervalArith.contained, widenInterval in *. + unfold widenInterval in *. simpl in *. rewrite Q2R_plus, Q2R_minus in no_div_zero_float. assert (Q2R e2lo - Q2R err2 = 0 -> False)%R by (apply (lt_or_gt_neq_zero_lo _ (Q2R e2hi + Q2R err2)); try auto; lra). assert (Q2R e2hi + Q2R err2 = 0 -> False)%R by (apply (lt_or_gt_neq_zero_hi (Q2R e2lo - Q2R err2)); try auto; lra). - pose proof (interval_inversion_valid (iv:=(Q2R e2lo,Q2R e2hi)) no_div_zero_real_R valid_bounds_e2) as valid_bounds_inv_e2. + pose proof (interval_inversion_valid (Q2R e2lo,Q2R e2hi) no_div_zero_real_R valid_bounds_e2) as valid_bounds_inv_e2. clear no_div_zero_real_R. (* Before doing case distinction, prove bounds that will be used many times: *) assert (nR1 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi))%R as upperBound_nR1 - by (apply contained_leq_maxAbs_val; unfold contained; auto). + by (apply contained_leq_maxAbs_val; auto). assert (/ nR2 <= RmaxAbsFun (invertInterval (Q2R e2lo, Q2R e2hi)))%R as upperBound_nR2 - by (apply contained_leq_maxAbs_val; unfold contained; auto). + by (apply contained_leq_maxAbs_val; auto). assert (-nR1 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi))%R as upperBound_Ropp_nR1 - by (apply contained_leq_maxAbs_neg_val; unfold contained; auto). + by (apply contained_leq_maxAbs_neg_val; auto). assert (- / nR2 <= RmaxAbsFun (invertInterval (Q2R e2lo, Q2R e2hi)))%R as upperBound_Ropp_nR2 - by (apply contained_leq_maxAbs_neg_val; unfold contained; auto). + by (apply contained_leq_maxAbs_neg_val; auto). assert (nR1 * Q2R err2 <= RmaxAbsFun (Q2R e1lo, Q2R e1hi) * Q2R err2)%R as bound_nR1 by (apply Rmult_le_compat_r; auto). @@ -1119,11 +1046,11 @@ Proof. by (apply Rmult_le_compat_r; auto). unfold invertInterval in *; simpl in upperBound_nR2, upperBound_Ropp_nR2. (* Case distinction for the divisor range - positive or negative in float and real valued execution *) + positive or negative in float and real valued execution *) destruct no_div_zero_real as [ real_iv_neg | real_iv_pos]; destruct no_div_zero_float as [float_iv_neg | float_iv_pos]. (* The range of the divisor lies in the range from -infinity until 0 *) - * unfold widenIntv in *; unfold IntervalArith.contained in *; simpl in *. + * unfold widenIntv in *; simpl in *. rewrite <- Q2R_plus in float_iv_neg. rewrite <- Q2R0_is_0 in float_iv_neg. rewrite <- Q2R0_is_0 in real_iv_neg. @@ -1551,12 +1478,12 @@ Proof. { apply Rmult_le_compat_r; try lra. repeat (rewrite Q2R_inv; try auto). } } - * unfold widenIntv in *; unfold IntervalArith.contained in *; simpl in *. + * unfold widenIntv in *; simpl in *. exfalso. assert (Q2R e2lo - Q2R err2 <= Q2R e2hi)%R by lra. assert (Q2R e2hi < Q2R e2lo - Q2R err2)%R by (apply (Rlt_trans _ 0 _); auto). lra. - * unfold widenIntv in *; unfold IntervalArith.contained in *; simpl in *. + * unfold widenIntv in *; simpl in *. exfalso. assert (Q2R e2lo <= Q2R e2hi + Q2R err2)%R by lra. assert (Q2R e2hi + Q2R err2 < Q2R e2lo)%R as hierr_lt_lo by (apply (Rlt_trans _ 0 _); auto). @@ -1888,8 +1815,8 @@ Proof. assert (IVhi (widenInterval (Q2R e2lo, Q2R e2hi) (Q2R err2)) < 0 \/ 0 < IVlo (widenInterval (Q2R e2lo, Q2R e2hi) (Q2R err2)))%R as no_div_zero_widen by (unfold widenInterval in *; simpl in *; rewrite Q2R_plus, Q2R_minus in no_div_zero_float; auto). - pose proof (IntervalArith.interval_division_valid no_div_zero_widen H0 H1) as valid_div_float. - unfold IntervalArith.contained, widenInterval in *; simpl in *. + pose proof (IntervalArith.interval_division_valid _ _ no_div_zero_widen H0 H1) as valid_div_float. + unfold widenInterval in *; simpl in *. assert (e2lo - err2 == 0 -> False). * hnf; intros. destruct no_div_zero_float as [float_iv | float_iv]; rewrite <- Q2R0_is_0 in float_iv; apply Rlt_Qlt in float_iv; try lra. @@ -1905,7 +1832,7 @@ Proof. { destruct valid_div_float. unfold RmaxAbsFun. apply Rmult_le_compat_r. - apply meps_posR. + apply mTypeToQ_pos_R. rewrite <- maxAbs_impl_RmaxAbs. unfold RmaxAbsFun. apply RmaxAbs; subst; simpl in *. @@ -1919,7 +1846,7 @@ Proof. repeat rewrite Q2R_minus. repeat rewrite Q2R_plus; auto. } - apply le_neq_bool_to_lt_prop in no_div_zero_float. - unfold IntervalArith.contained, widenInterval in *; simpl in *. + unfold widenInterval in *; simpl in *. assert (e2lo - err2 == 0 -> False). + hnf; intros. destruct no_div_zero_float as [float_iv | float_iv]; try lra. @@ -1950,7 +1877,7 @@ Qed. Lemma validErrorboundCorrectRounding E1 E2 absenv (e: exp Q) (nR nF nF1: R) (err err':error) (elo ehi alo ahi: Q) dVars (m: mType) (machineEpsilon:mType) Gamma defVars: - eval_exp E1 (toREvalVars defVars) (toREval (toRExp e)) nR M0 -> + eval_exp E1 (toRMap defVars) (toREval (toRExp e)) nR M0 -> eval_exp E2 defVars (toRExp e) nF1 m -> eval_exp (updEnv 1 nF1 emptyEnv) (updDefVars 1 m defVars) @@ -1971,26 +1898,24 @@ Proof. simpl in subexpr_ok; rewrite H in subexpr_ok. case_eq (Gamma e); intros; rewrite H0 in subexpr_ok; [ | inversion subexpr_ok ]. andb_to_prop subexpr_ok. - apply EquivEqBoolEq in L0; subst. + apply mTypeEq_compat_eq in L0; subst. andb_to_prop valid_error. simpl in *. eapply Rle_trans. eapply round_abs_err_bounded; eauto. - assert (contained nR (Q2R elo, Q2R ehi)) as valid_intv_c by (unfold contained; auto). - pose proof (distance_gives_iv _ valid_intv_c err_bounded) as dgi. - unfold IntervalArith.contained in dgi. + assert (contained nR (Q2R elo, Q2R ehi)) as valid_intv_c by (auto). + pose proof (distance_gives_iv _ _ valid_intv_c err_bounded) as dgi. destruct dgi as [dgi1 dgi2]; simpl in dgi1; simpl in dgi2. - apply (Rle_trans _ (Q2R err + Q2R (maxAbs (widenIntv (elo, ehi) err)) * Q2R (meps m0)) _). + apply (Rle_trans _ (Q2R err + Q2R (maxAbs (widenIntv (elo, ehi) err)) * Q2R (mTypeToQ m0)) _). + apply Rplus_le_compat_l. apply Rmult_le_compat_r. * rewrite <- Q2R0_is_0. apply Qle_Rle. - apply meps_pos. + apply mTypeToQ_pos_Q. * remember (widenIntv (elo, ehi) err) as iv_widen. destruct iv_widen as [eloR ehiR]. rewrite <- maxAbs_impl_RmaxAbs. apply contained_leq_maxAbs. - unfold IntervalArith.contained; simpl. unfold widenIntv in Heqiv_widen; simpl in Heqiv_widen. inversion Heqiv_widen. rewrite Q2R_minus. @@ -2009,12 +1934,11 @@ Qed. Each case requires the application of one of the soundness lemmata proven before **) Theorem validErrorbound_sound (e:exp Q): - forall E1 E2 fVars dVars absenv nR nF err P elo ehi m Gamma defVars, + forall E1 E2 fVars dVars absenv nR err P elo ehi Gamma defVars, typeCheck e defVars Gamma = true -> approxEnv E1 defVars absenv fVars dVars E2 -> NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars -> - eval_exp E1 (toREvalVars defVars) (toREval (toRExp e)) nR M0 -> - eval_exp E2 defVars (toRExp e) nF m -> + eval_exp E1 (toRMap defVars) (toREval (toRExp e)) nR M0 -> validErrorbound e Gamma absenv dVars = true -> validIntervalbounds e absenv P dVars = true -> (forall v1, NatSet.mem v1 dVars = true -> @@ -2023,32 +1947,35 @@ Theorem validErrorbound_sound (e:exp Q): (forall v, NatSet.mem v fVars= true -> exists vR, E1 v = Some vR /\ (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> + (forall v1 : NatSet.elt, (v1) mem (fVars ∪ dVars) = true -> + exists m0 : mType, defVars v1 = Some m0) -> absenv e = ((elo,ehi),err) -> - (Rabs (nR - nF) <= (Q2R err))%R. + exists nF m, + eval_exp E2 defVars (toRExp e) nF m /\ + (Rabs (nR - nF) <= (Q2R err))%R. Proof. revert e; induction e; - (intros * typing_ok approxCEnv fVars_subset eval_real eval_float valid_error valid_intv valid_dVars P_valid absenv_eq). + intros * typing_ok approxCEnv fVars_subset eval_real valid_error valid_intv + valid_dVars P_valid vars_wellTyped absenv_eq. - inversion typing_ok; subst. - eapply validErrorboundCorrectVariable; try eauto. + eapply validErrorboundCorrectVariable; eauto. - inversion typing_ok; subst. case_eq (Gamma (Const m v)); intros; rewrite H in H0; [ | inversion H0 ]. - apply EquivEqBoolEq in H0; subst. - assert (eval_exp E2 defVars (toRExp (Const m1 v)) nF m1) by - (inversion eval_float; subst; econstructor; eauto). + apply mTypeEq_compat_eq in H0; subst. eapply validErrorboundCorrectConstant; eauto. - + simpl in valid_intv. - rewrite absenv_eq in valid_intv. - simpl in eval_real; inversion eval_real; subst. - simpl in H4; rewrite Q2R0_is_0 in H4. - rewrite delta_0_deterministic; auto. - unfold isSupersetIntv in valid_intv; apply andb_true_iff in valid_intv; destruct valid_intv. - simpl in H,H0. - split; auto. - * apply Qle_bool_iff in H1. apply (Qle_Rle _ _ H1). - * apply Qle_bool_iff in H2. apply (Qle_Rle _ _ H2). + simpl in valid_intv. + rewrite absenv_eq in valid_intv. + simpl in eval_real; inversion eval_real; subst. + simpl in *; rewrite Q2R0_is_0 in H3. + rewrite delta_0_deterministic; auto. + unfold isSupersetIntv in valid_intv; apply andb_true_iff in valid_intv; destruct valid_intv. + canonize_hyps. + simpl in H0,H1. + split; auto. - unfold validErrorbound in valid_error. rewrite absenv_eq in valid_error. - case_eq (Gamma (Unop u e)); intros; rewrite H in valid_error; [ | inversion valid_error ]. + case_eq (Gamma (Unop u e)); intros * type_unop; + rewrite type_unop in valid_error; [ | inversion valid_error ]. andb_to_prop valid_error. destruct u; try congruence. env_assert absenv e absenv_e. @@ -2060,23 +1987,21 @@ Proof. rewrite R. destruct iv as [e_lo e_hi]. inversion eval_real; subst. - inversion eval_float; subst. - unfold evalUnop. - apply bound_flip_sub. - eapply IHe; eauto. + destruct (IHe E1 E2 fVars dVars absenv v1 err_e P e_lo e_hi Gamma defVars) as [nF [mF [eval_float valid_bounds_e]]]; + eauto. + simpl in typing_ok. - rewrite H in typing_ok. - case_eq (Gamma e); intros; rewrite H0 in typing_ok; [ | inversion typing_ok ]. + rewrite type_unop in typing_ok. + case_eq (Gamma e); intros * type_e; rewrite type_e in typing_ok; [ | inversion typing_ok ]. andb_to_prop typing_ok; auto. + simpl in valid_intv. rewrite absenv_eq in valid_intv; andb_to_prop valid_intv. auto. - + instantiate (1 := e_hi). - instantiate (1 := e_lo). + + exists (evalUnop Neg nF); exists mF. + simpl. + split; try eauto. + apply bound_flip_sub. rewrite absenv_e; auto. - pose proof (ivbounds_approximatesPrecond_sound (Binop b e1 e2) absenv P valid_intv) as env_approx_p. - assert (typing_copy := typing_ok). - assert (valid_error_copy := valid_error). simpl in valid_error. env_assert absenv e1 absenv_e1. env_assert absenv e2 absenv_e2. @@ -2088,163 +2013,145 @@ Proof. iv_assert iv2 iv_e2. destruct iv_e2 as [ivlo2 [ivhi2 iv_e2]]. rewrite iv_e2 in absenv_e2. - rewrite absenv_eq, absenv_e1, absenv_e2 in valid_error. - case_eq (Gamma (Binop b e1 e2)); intros; rewrite H in valid_error; [ | inversion valid_error ]. - simpl in typing_ok. rewrite H in typing_ok. - case_eq (Gamma e1); intros; rewrite H0 in typing_ok; [ | inversion typing_ok ]. - case_eq (Gamma e2); intros; rewrite H1 in typing_ok; [ | inversion typing_ok ]. - andb_to_prop typing_ok. apply EquivEqBoolEq in L0; subst. + subst; simpl in *. + rewrite absenv_eq, absenv_e1, absenv_e2 in *. + case_eq (Gamma (Binop b e1 e2)); + intros * type_b; rewrite type_b in valid_error; [ | inversion valid_error ]. + rewrite type_b in typing_ok; simpl in typing_ok. + case_eq (Gamma e1); + intros * type_e1; rewrite type_e1 in typing_ok; [ | inversion typing_ok ]. + case_eq (Gamma e2); + intros * type_e2; rewrite type_e2 in typing_ok; [ | inversion typing_ok ]. + andb_to_prop typing_ok. + apply mTypeEq_compat_eq in L0; subst. andb_to_prop valid_error. simpl in valid_intv. - rewrite absenv_eq, absenv_e1, absenv_e2 in valid_intv. andb_to_prop valid_intv. inversion eval_real; subst. - destruct m0; destruct m3; inversion H5; clear H5. - apply binary_unfolding in eval_float. - destruct eval_float as [vF1 [vF2 [ mF1 [mF2 [joinF12 [eval_e1 [eval_e2 eval_float ]]]]]]]. - simpl in *. - pose proof (validIntervalbounds_sound e1 absenv P (vR:=v1) defVars L2 valid_dVars (fVars:=fVars)) - as valid_bounds_e1. - rewrite absenv_e1 in valid_bounds_e1. - pose proof (validIntervalbounds_sound e2 absenv P (vR:=v2) defVars R4 valid_dVars (fVars:=fVars)) - as valid_bounds_e2. - rewrite absenv_e2 in valid_bounds_e2; + apply M0_join_is_M0 in H2. + destruct H2; subst. + destruct (IHe1 E1 E2 fVars dVars absenv v1 err1 P ivlo1 ivhi1 Gamma defVars) + as [vF1 [mF1 [eval_float_e1 bounded_e1]]]; + try auto; set_tac. + destruct (IHe2 E1 E2 fVars dVars absenv v2 err2 P ivlo2 ivhi2 Gamma defVars) + as [vF2 [mF2 [eval_float_e2 bounded_e2]]]; + try auto; set_tac. + destruct (validIntervalbounds_sound _ _ _ E1 defVars L2 (fVars := fVars) (dVars:=dVars)) + as [v1' [eval_real_e1 bounds_e1]]; + try auto; set_tac. + rewrite absenv_e1 in bounds_e1. + pose proof (meps_0_deterministic _ eval_real_e1 H5); subst. clear H5. + destruct (validIntervalbounds_sound _ _ _ E1 defVars R4 (fVars:= fVars) (dVars:=dVars)) + as [v2' [eval_real_e2 bounds_e2]]; + try auto; set_tac. + rewrite absenv_e2 in bounds_e2; simpl in *. + pose proof (meps_0_deterministic _ eval_real_e2 H6); subst; clear H6. + assert (b = Div -> ~ (vF2 = 0)%R) as no_div_zero. + { intros; subst; simpl in *. + andb_to_prop R2. + apply le_neq_bool_to_lt_prop in L0. + assert (contained vF1 (widenInterval (Q2R ivlo1, Q2R ivhi1) (Q2R err1))) + as bounds_float_e1. + { eapply distance_gives_iv; simpl; + try eauto. } + assert (contained vF2 (widenInterval (Q2R ivlo2, Q2R ivhi2) (Q2R err2))) + as bounds_float_e2. + { eapply distance_gives_iv; simpl; + try eauto. } simpl in *. - assert (Rabs (v1 - vF1) <= Q2R err1 /\ Rabs (v2 - vF2) <= Q2R err2)%R. - + split. - * eapply IHe1; eauto. - { hnf. intros a in_diff. - rewrite NatSet.diff_spec in in_diff. - apply fVars_subset. - destruct in_diff. - rewrite NatSet.diff_spec, NatSet.union_spec. - split; auto. } - * eapply IHe2; eauto. - { hnf. intros a in_diff. - rewrite NatSet.diff_spec in in_diff. - apply fVars_subset. - destruct in_diff. - rewrite NatSet.diff_spec, NatSet.union_spec. - split; auto. } - + assert ((Q2R ivlo1 <= v1 <= Q2R ivhi1) /\ (Q2R ivlo2 <= v2 <= Q2R ivhi2))%R. - * split. - { apply valid_bounds_e1; try auto. - hnf. intros a in_diff. - rewrite NatSet.diff_spec in in_diff. - destruct in_diff as [in_freeVars no_dVar]. - apply fVars_subset. - rewrite NatSet.diff_spec, NatSet.union_spec. - split; try auto. } - { apply valid_bounds_e2; try auto. - hnf. intros a in_diff. - rewrite NatSet.diff_spec in in_diff. - destruct in_diff as [in_freeVars no_dVar]. - apply fVars_subset. - rewrite NatSet.diff_spec, NatSet.union_spec. - split; try auto. } - * destruct H2, H3. destruct b. - { eapply (validErrorboundCorrectAddition (e1:=e1) absenv); eauto. - simpl; apply valid_error_copy. } - { eapply (validErrorboundCorrectSubtraction (e1:=e1) absenv); eauto. - simpl; apply valid_error_copy. } - { eapply (validErrorboundCorrectMult (e1 := e1) absenv); eauto. - simpl; apply valid_error_copy. } - { eapply (validErrorboundCorrectDiv (e1 := e1) absenv); eauto. - - simpl; apply valid_error_copy. - - case_eq (Qleb ivhi2 0 && negb (Qeq_bool ivhi2 0) || Qleb 0 ivlo2 && negb (Qeq_bool ivlo2 0)); intros; - rewrite H7 in R3; inversion R3. - auto. } - - unfold validErrorbound in valid_error. - rewrite absenv_eq in valid_error. - case_eq (Gamma (Downcast m e)); intros; rewrite H in valid_error; [ | inversion valid_error ]. + hnf; intro; subst. + rewrite <- Q2R0_is_0 in bounds_float_e2. + destruct L0 as [nodivzero | nodivzero]; apply Qlt_Rlt in nodivzero; try rewrite Q2R_plus in *; try rewrite Q2R_minus in *; try lra. + } + assert (eval_exp E2 defVars (Binop b (toRExp e1) (toRExp e2)) (perturb (evalBinop b vF1 vF2) (Q2R (mTypeToQ (join mF1 mF2)))) (join mF1 mF2)) + as eval_float. + { econstructor; eauto. + rewrite Rabs_right; try lra. + apply Rle_ge. + apply mTypeToQ_pos_R. + } + exists (perturb (evalBinop b vF1 vF2) (Q2R (mTypeToQ (join mF1 mF2)))); + exists (join mF1 mF2); split; [auto | ]. + apply binary_unfolding in eval_float; try auto. + destruct b. + + eapply (validErrorboundCorrectAddition (e1:=e1) absenv); eauto. + * simpl. + rewrite type_b. + rewrite type_e1. + rewrite type_e2. + rewrite mTypeEq_refl, R0, R; auto. + * simpl. + rewrite absenv_eq. + rewrite type_b. + rewrite L, L1, R1; simpl. + rewrite absenv_e1, absenv_e2. + auto. + + eapply (validErrorboundCorrectSubtraction (e1:=e1) absenv); eauto. + * simpl; rewrite type_b, type_e1, type_e2, mTypeEq_refl, R0, R; auto. + * simpl; rewrite absenv_eq, type_b, L, L1, R1; simpl. + rewrite absenv_e1, absenv_e2; auto. + + eapply (validErrorboundCorrectMult (e1 := e1) absenv); eauto. + * simpl; rewrite type_b, type_e1, type_e2, mTypeEq_refl, R0, R; auto. + * simpl; rewrite absenv_eq, type_b, L, L1, R1; simpl. + rewrite absenv_e1, absenv_e2; auto. + + eapply (validErrorboundCorrectDiv (e1 := e1) absenv); eauto. + * simpl; rewrite type_b, type_e1, type_e2, mTypeEq_refl, R0, R; auto. + * simpl; rewrite absenv_eq, type_b, L, L1, R1; simpl. + rewrite absenv_e1, absenv_e2; auto. + * andb_to_prop R3; auto. + - env_assert absenv e absenv_e. + destruct absenv_e as [iv [err_e absenv_e]]. + iv_assert iv iv_e. + destruct iv_e as [ivlo_e [ivhi_e iv_e]]. + rewrite iv_e in absenv_e. + subst; simpl in *. + rewrite absenv_eq, absenv_e in *. + case_eq (Gamma (Downcast m e)); + intros * type_b; rewrite type_b in valid_error; [ | inversion valid_error ]. + rewrite type_b in typing_ok; simpl in typing_ok. + case_eq (Gamma e); + intros * type_e; rewrite type_e in typing_ok; [ | inversion typing_ok ]. + andb_to_prop typing_ok. + apply mTypeEq_compat_eq in L0; subst. andb_to_prop valid_error. - simpl in valid_intv; rewrite absenv_eq in valid_intv. - remember (absenv e) as absenv_e; destruct absenv_e as [ive1 err1]. - andb_to_prop R. + simpl in valid_intv. andb_to_prop valid_intv. - inversion eval_float; subst. - simpl in eval_real. - eapply (validErrorboundCorrectRounding absenv e dVars Gamma eval_real H6); eauto. - + econstructor; eauto. - constructor; auto. - + simpl. - rewrite absenv_eq. - rewrite H. - rewrite L. - rewrite <- Heqabsenv_e. - apply andb_true_iff; split; auto. - + instantiate (1:=(snd ive1)). - instantiate (1:=(fst ive1)). - simpl in eval_real. - simpl in typing_ok. - simpl in fVars_subset. - inversion typing_ok; subst. - pose proof (validIntervalbounds_sound e absenv P (fVars:=fVars) (dVars:=dVars) (E:=E1) defVars L1 (vR:=nR) valid_dVars fVars_subset P_valid eval_real) as vIB_e. - rewrite <- Heqabsenv_e in vIB_e. - simpl in vIB_e; auto. - + assert (absenv e = (fst ive1, snd ive1, err1)) by (destruct ive1; simpl; auto). - apply H0. - + eapply IHe; eauto. - * simpl in typing_ok. - rewrite H in typing_ok. - case_eq (Gamma e); intros; rewrite H0 in typing_ok; [ | inversion typing_ok ]. - andb_to_prop typing_ok. - auto. - * assert (absenv e = (fst ive1, snd ive1, err1)) by (destruct ive1; simpl; auto). - apply H0. + inversion eval_real; subst. + apply M0_least_precision in H1. + subst. + destruct (IHe E1 E2 fVars dVars absenv v1 err_e P ivlo_e ivhi_e Gamma defVars) + as [vF [mF [eval_float_e bounded_e]]]; + try auto; set_tac. + pose proof (typingSoundnessExp _ _ R eval_float_e). + rewrite H in type_e; inversion type_e; subst. + destruct (validIntervalbounds_sound _ _ _ E1 defVars L1 (fVars := fVars) (dVars:=dVars)) + as [v1' [eval_real_e bounds_e]]; + try auto; set_tac. + rewrite absenv_e in bounds_e. + pose proof (meps_0_deterministic _ eval_real_e H4); subst. clear H4. + exists (perturb vF (Q2R (mTypeToQ m0))); + exists m0. + split; [econstructor; eauto |]. + + rewrite Rabs_right; try lra. + auto using Rle_ge, mTypeToQ_pos_R. + + rewrite Q2R0_is_0 in *. rewrite (delta_0_deterministic _ delta) in *; try auto. + eapply validErrorboundCorrectRounding; eauto. + * econstructor; eauto. + rewrite Rabs_right; try lra. + auto using Rle_ge, mTypeToQ_pos_R. + * simpl. rewrite type_b, H. + rewrite mTypeEq_refl, R0, R; auto. + * simpl. rewrite absenv_eq, absenv_e, type_b, L; simpl. + rewrite L0; auto. Qed. -(* Lemma validErrorbound_subset e tmap absenv dVars dVars': *) -(* validErrorbound e tmap absenv dVars = true -> *) -(* NatSet.Subset dVars dVars' -> *) -(* validErrorbound e tmap absenv dVars' = true. *) -(* Proof. *) -(* induction e; intros validBound_e_dV subset_dV; simpl in *; try auto. *) -(* - destruct (absenv (Var Q n)); simpl in *. *) -(* case_eq (tmap (Var Q n)); intros; rewrite H in validBound_e_dV; [ | inversion validBound_e_dV ]. *) -(* andb_to_prop validBound_e_dV. *) -(* apply Is_true_eq_true; apply andb_prop_intro; split. *) -(* + apply Is_true_eq_left in L; auto. *) -(* + case_eq (NatSet.mem n dVars); *) -(* intros case_mem; rewrite case_mem in *; simpl in *. *) -(* * hnf in subset_dV. *) -(* rewrite NatSet.mem_spec in case_mem. *) -(* specialize (subset_dV n case_mem). *) -(* rewrite <- NatSet.mem_spec in subset_dV. *) -(* rewrite subset_dV. *) -(* apply Is_true_eq_left; auto. *) -(* * case_eq (NatSet.mem n dVars'); intros case_mem'; *) -(* apply Is_true_eq_left; auto. *) -(* - destruct (absenv (Binop b e1 e2)); simpl in *. *) -(* case_eq (tmap (Binop b e1 e2)); intros; rewrite H in validBound_e_dV; [ | inversion validBound_e_dV ]. *) -(* rewrite <- andb_lazy_alt in *. *) -(* andb_to_prop validBound_e_dV. *) -(* rewrite andb_true_iff; split; try auto. *) -(* destruct (absenv e1); destruct (absenv e2). *) -(* rewrite <- andb_lazy_alt. *) -(* rewrite andb_true_iff; split; try auto. *) -(* repeat (rewrite andb_true_iff; split); auto. *) -(* - destruct (absenv (Downcast m e)); simpl in *. *) -(* case_eq (tmap (Downcast m e)); intros; rewrite H in validBound_e_dV; [ | inversion validBound_e_dV ]. *) -(* andb_to_prop validBound_e_dV. *) -(* rewrite <- andb_lazy_alt. *) -(* rewrite L; simpl. *) -(* destruct (absenv e); simpl in *. *) -(* apply andb_true_iff in R; destruct R. *) -(* apply andb_true_iff; split. *) -(* + apply IHe; auto. *) -(* + auto. *) -(* Qed. *) - - Theorem validErrorboundCmd_sound (f:cmd Q) (absenv:analysisResult): - forall E1 E2 outVars fVars dVars vR vF elo ehi err P m Gamma defVars, + forall E1 E2 outVars fVars dVars vR elo ehi err P Gamma defVars, typeCheckCmd f defVars Gamma = true -> approxEnv E1 defVars absenv fVars dVars E2 -> ssa f (NatSet.union fVars dVars) outVars -> NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars -> - bstep (toREvalCmd (toRCmd f)) E1 (toREvalVars defVars) vR M0 -> - bstep (toRCmd f) E2 defVars vF m -> + bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR M0 -> validErrorboundCmd f Gamma absenv dVars = true -> validIntervalboundsCmd f absenv P dVars = true -> (forall v1, NatSet.mem v1 dVars = true -> @@ -2253,20 +2160,38 @@ Theorem validErrorboundCmd_sound (f:cmd Q) (absenv:analysisResult): (forall v, NatSet.mem v fVars= true -> exists vR, E1 v = Some vR /\ (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> + (forall v1, (v1) mem (fVars ∪ dVars) = true -> + exists m0 : mType, + defVars v1 = Some m0) -> absenv (getRetExp f) = ((elo,ehi),err) -> + exists vF m, + bstep (toRCmd f) E2 defVars vF m /\ (Rabs (vR - vF) <= (Q2R err))%R. Proof. induction f; - intros * type_f approxc1c2 ssa_f freeVars_subset eval_real eval_float valid_bounds valid_intv fVars_sound P_valid absenv_res. - - simpl in eval_real, eval_float. - inversion eval_float; inversion eval_real; subst. + intros * type_f approxc1c2 ssa_f freeVars_subset eval_real valid_bounds valid_intv fVars_sound P_valid types_defined absenv_res. + - simpl in eval_real; inversion eval_real; subst. inversion ssa_f; subst. - assert (approxEnv (updEnv n v0 E1) defVars absenv fVars (NatSet.add n dVars) (updEnv n v E2)). + andb_to_prop valid_bounds. + andb_to_prop type_f. + andb_to_prop valid_intv. + env_assert absenv e absenv_e. + destruct absenv_e as [iv_e [err_e absenv_e]]. + iv_assert iv_e iv_eq. + destruct iv_eq as [ivlo_e [ivhi_e iv_eq]]. + rewrite iv_eq in *. + simpl in freeVars_subset. + assert (NatSet.Subset (usedVars e -- dVars) fVars) as valid_varset. + { set_tac. + split; try auto. + rewrite NatSet.remove_spec. + split; try set_tac. + hnf; intros; subst; set_tac. } + eapply validErrorbound_sound with (err := err_e) (elo := ivlo_e) (ehi:= ivhi_e) in L0; eauto. + destruct L0 as [vF [mF [eval_float_e bounded_e]]]. + assert (approxEnv (updEnv n v E1) (updDefVars n mF defVars) absenv fVars (NatSet.add n dVars) (updEnv n vF E2)). + eapply approxUpdBound; try auto. - * unfold validErrorboundCmd in valid_bounds. - andb_to_prop valid_bounds. - rename L0 into validErrorbound_e. - rewrite Qeq_bool_iff in R0. + * rewrite Qeq_bool_iff in R0. assert (snd (absenv (Var Q n)) == snd (absenv (Var Q n))) by apply Qeq_refl. pose proof (Qleb_comp _ _ R0 _ _ H). assert (Qle (snd (absenv e)) (snd (absenv (Var Q n)))). @@ -2275,52 +2200,20 @@ Proof. rewrite Qle_bool_iff. apply Qle_lteq. right. - inversion type_f; subst. auto. } + auto. } { apply Qle_Rle in H1. eapply Rle_trans. Focus 2. apply H1. - env_assert absenv e absenv_e. - destruct absenv_e as [iv [err_e absenv_e]]. - destruct iv. - eapply validErrorbound_sound; eauto. - - simpl in type_f. - case_eq (Gamma (Var Q n)); intros; rewrite H2 in type_f; [ | inversion type_f ]. - case_eq (Gamma e); intros; rewrite H3 in type_f; [ | inversion type_f ]. - andb_to_prop type_f. - auto. - - hnf. intros a a_in_diff. - apply freeVars_subset. - rewrite NatSet.diff_spec in *. - simpl. - destruct a_in_diff. - split; try auto. - rewrite NatSet.remove_spec, NatSet.union_spec. - split; try auto. - hnf; intros; subst. - specialize (H5 n H2). - rewrite <- NatSet.mem_spec in H5. - rewrite H5 in *; congruence. - - simpl in valid_intv. - andb_to_prop valid_intv. - assumption. - - instantiate (1 := q0). instantiate (1 := q). - rewrite absenv_e; auto. } - + simpl in valid_bounds. - andb_to_prop valid_bounds. - rename L0 into validbound_e; - rename R0 into var_bound_eq_e; + rewrite absenv_e; auto. } + + rename R0 into var_bound_eq_e; rename R into valid_rec. - simpl in valid_intv; - andb_to_prop valid_intv. - eapply (IHf (updEnv n v0 E1) (updEnv n v E2) _ _ _ vR vF elo ehi err P); eauto. - * simpl in type_f. - case_eq (Gamma (Var Q n)); intros; rewrite H0 in type_f; [ | inversion type_f ]. - case_eq (Gamma e); intros; rewrite H1 in type_f; [ | inversion type_f ]. - andb_to_prop type_f. - auto. - * instantiate (1 := outVars). - eapply ssa_equal_set; eauto. + pose proof (typingSoundnessExp _ _ L eval_float_e). + rewrite H0 in *; simpl in *. + andb_to_prop R1. + rewrite mTypeEq_compat_eq in L0; symmetry in L0; subst. + destruct (IHf (updEnv n v E1) (updEnv n vF E2) outVars fVars (NatSet.add n dVars) vR elo ehi err P Gamma (updDefVars n mF defVars)) as [vF_res [m_res [step_res bounded_res]]]; eauto. + * eapply ssa_equal_set; eauto. hnf. intros a; split; intros in_set. { rewrite NatSet.add_spec, NatSet.union_spec; rewrite NatSet.union_spec, NatSet.add_spec in in_set. @@ -2335,31 +2228,22 @@ Proof. simpl. rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec. split; try auto. + * eapply test4 with (Gamma1 := updDefVars n M0 (toRMap defVars)); eauto using test3. * intros v1 v1_mem. unfold updEnv. case_eq (v1 =? n); intros v1_eq. - { rename R1 into eq_lo; - rename R0 into eq_hi. + { rename R4 into eq_lo; + rename R3 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. - inversion type_f; subst. apply Nat.eqb_eq in v1_eq; subst. - exists v0; split; try auto. + exists v; split; try auto. rewrite <- eq_lo, <- eq_hi. - eapply validIntervalbounds_sound; eauto. - hnf. intros a a_mem_diff. - rewrite NatSet.diff_spec in a_mem_diff. - destruct a_mem_diff as [a_mem_freeVars a_no_dVar]. - apply freeVars_subset. - simpl. rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec. - split; try auto. - split; try auto. - hnf; intros; subst. - specialize (H5 n a_mem_freeVars). - rewrite <- NatSet.mem_spec in H5. - rewrite H5 in *; congruence. } + destruct (validIntervalbounds_sound e absenv _ E1 defVars L1 (fVars:=fVars)) as [vR_e [eval_real_e bounded_real_e]]; eauto. + pose proof (meps_0_deterministic _ eval_real_e H7); subst. + auto. } { rewrite NatSet.mem_spec in v1_mem. rewrite NatSet.add_spec in v1_mem. rewrite Nat.eqb_neq in v1_eq. @@ -2377,12 +2261,20 @@ Proof. by (rewrite NatSet.mem_spec in *; rewrite NatSet.union_spec; auto). rewrite <- NatSet.mem_spec in in_union. rewrite in_union in *; congruence. - - inversion eval_real; inversion eval_float; subst. + * intros v1 v1_mem; set_tac. + unfold updDefVars. + case_eq (v1 =? n); intros case_v1; try rewrite case_v1 in *; try eauto. + apply types_defined; set_tac. + rewrite NatSet.union_spec in v1_mem; destruct v1_mem as [v_fVar | v_dVar]; try auto. + rewrite NatSet.add_spec in v_dVar. destruct v_dVar; try auto. + subst; rewrite Nat.eqb_refl in case_v1; congruence. + * exists vF_res; exists m_res; split; try auto. + clear IHf P_valid fVars_sound R2 R4 R3 valid_rec absenv_res. + econstructor; eauto. + - inversion eval_real; subst. unfold updEnv; simpl. unfold validErrorboundCmd in valid_bounds. - simpl in valid_intv. - env_assert absenv e absenv_e. - destruct absenv_e as [iv [err_e absenv_e]]. - destruct iv. - eapply validErrorbound_sound; eauto. + simpl in *. + edestruct validErrorbound_sound as [vF [mF [eval_e bounded_e]]]; eauto. + exists vF; exists mF; split; [econstructor |]; eauto. Qed. \ No newline at end of file diff --git a/coq/Expressions.v b/coq/Expressions.v index a013257..c54ffa2 100644 --- a/coq/Expressions.v +++ b/coq/Expressions.v @@ -1,9 +1,12 @@ (** Formalization of the base expression language for the daisy framework **) -Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.Qreals. -Require Import Daisy.Infra.RealRationalProps Daisy.Infra.RationalSimps Daisy.Infra.Ltacs. -Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet Daisy.IntervalArithQ Daisy.IntervalArith Daisy.Infra.MachineType. +Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith + Coq.QArith.Qreals. +Require Import Daisy.Infra.RealRationalProps Daisy.Infra.RationalSimps + Daisy.Infra.Ltacs. +Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet + Daisy.IntervalArithQ Daisy.IntervalArith Daisy.Infra.MachineType. (** Expressions will use binary operators. @@ -11,7 +14,7 @@ Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet Dais **) Inductive binop : Type := Plus | Sub | Mult | Div. -Definition binopEqBool (b1:binop) (b2:binop) := +Definition binopEq (b1:binop) (b2:binop) := match b1, b2 with | Plus, Plus => true | Sub, Sub => true @@ -32,16 +35,25 @@ Definition evalBinop (o:binop) (v1:R) (v2:R) := | Div => Rdiv v1 v2 end. -Lemma binopEqBool_refl b: - binopEqBool b b = true. +Lemma binopEq_refl b: + binopEq b b = true. Proof. case b; auto. Qed. -Lemma binopEqBool_prop b1 b2: - binopEqBool b1 b2 = true <-> b1 = b2. +Lemma binopEq_compat_eq b1 b2: + binopEq b1 b2 = true <-> b1 = b2. Proof. - split; case b1; case b2; intros; simpl in *; try congruence; auto. + split; case b1; case b2; intros; simpl in *; congruence. +Qed. + +Lemma binopEq_compat_eq_false b1 b2: + binopEq b1 b2 = false <-> ~ (b1 = b2). +Proof. + split; intros neq. + - hnf; intros; subst. rewrite binopEq_refl in neq. + congruence. + - destruct b1; destruct b2; cbv; congruence. Qed. (** @@ -50,23 +62,23 @@ Qed. **) Inductive unop: Type := Neg | Inv. -Definition unopEqBool (o1:unop) (o2:unop) := +Definition unopEq (o1:unop) (o2:unop) := match o1, o2 with | Neg, Neg => true | Inv, Inv => true | _ , _ => false end. -Lemma unopEqBool_refl b: - unopEqBool b b = true. +Lemma unopEq_refl b: + unopEq b b = true. Proof. case b; auto. Qed. -Lemma unopEqBool_prop b1 b2: - unopEqBool b1 b2 = true <-> b1 = b2. +Lemma unopEq_compat_eq b1 b2: + unopEq b1 b2 = true <-> b1 = b2. Proof. - split; case b1; case b2; intros; simpl in *; try congruence; auto. + split; case b1; case b2; intros; simpl in *; congruence. Qed. (** @@ -94,54 +106,58 @@ Inductive exp (V:Type): Type := Boolean equality function on expressions. Used in certificates to define the analysis result as function **) -Fixpoint expEqBool (e1:exp Q) (e2:exp Q) := +Fixpoint expEq (e1:exp Q) (e2:exp Q) := match e1, e2 with | Var _ v1, Var _ v2 => (v1 =? v2) - | Const m1 n1, Const m2 n2 => andb (mTypeEqBool m1 m2) (Qeq_bool n1 n2) - | Unop o1 e11, Unop o2 e22 => andb (unopEqBool o1 o2) (expEqBool e11 e22) - | Binop o1 e11 e12, Binop o2 e21 e22 => andb (binopEqBool o1 o2) (andb (expEqBool e11 e21) (expEqBool e12 e22)) - | Downcast m1 f1, Downcast m2 f2 => andb (mTypeEqBool m1 m2) (expEqBool f1 f2) + | Const m1 n1, Const m2 n2 => + (mTypeEq m1 m2) && (Qeq_bool n1 n2) + | Unop o1 e11, Unop o2 e22 => + (unopEq o1 o2) && (expEq e11 e22) + | Binop o1 e11 e12, Binop o2 e21 e22 => + (binopEq o1 o2) && (expEq e11 e21) && (expEq e12 e22) + | Downcast m1 f1, Downcast m2 f2 => + (mTypeEq m1 m2) && (expEq f1 f2) | _, _ => false end. -Lemma expEqBool_refl e: - expEqBool e e = true. +Lemma expEq_refl e: + expEq e e = true. Proof. - induction e; try (apply andb_true_iff; split); simpl in *; auto; try (apply EquivEqBoolEq; auto). + induction e; try (apply andb_true_iff; split); simpl in *; auto . - symmetry; apply beq_nat_refl. + - apply mTypeEq_refl. - apply Qeq_bool_iff; lra. - case u; auto. - case b; auto. - - apply andb_true_iff; split. - apply IHe1. apply IHe2. + - apply mTypeEq_refl. Qed. -Lemma expEqBool_sym e e': - expEqBool e e' = expEqBool e' e. +Lemma expEq_sym e e': + expEq e e' = expEq e' e. Proof. revert e'. induction e; intros e'; destruct e'; simpl; try auto. - - apply beq_nat_sym. + - apply Nat.eqb_sym. - f_equal. - + apply mTypeEqBool_sym; auto. + + apply mTypeEq_sym; auto. + apply Qeq_bool_sym. - f_equal. + destruct u; auto. + apply IHe. - f_equal. - + destruct b; auto. + f_equal. + * destruct b; auto. * apply IHe1. - * apply IHe2. + + apply IHe2. - f_equal. - + apply mTypeEqBool_sym; auto. + + apply mTypeEq_sym; auto. + apply IHe. Qed. -Lemma expEqBool_trans e f g: - expEqBool e f = true -> - expEqBool f g = true -> - expEqBool e g = true. +Lemma expEq_trans e f g: + expEq e f = true -> + expEq f g = true -> + expEq e g = true. Proof. revert e f g; induction e; destruct f; intros g eq1 eq2; @@ -150,25 +166,24 @@ Proof. subst; try auto. - andb_to_prop eq1; andb_to_prop eq2. - apply EquivEqBoolEq in L. - apply EquivEqBoolEq in L0; subst. - rewrite mTypeEqBool_refl; simpl. + rewrite mTypeEq_compat_eq in L, L0; subst. + rewrite mTypeEq_refl; simpl. rewrite Qeq_bool_iff in *; lra. - andb_to_prop eq1; andb_to_prop eq2. - rewrite unopEqBool_prop in *; subst. - rewrite unopEqBool_refl; simpl. + rewrite unopEq_compat_eq in *; subst. + rewrite unopEq_refl; simpl. eapply IHe; eauto. - andb_to_prop eq1; andb_to_prop eq2. - rewrite binopEqBool_prop in *; subst. - rewrite binopEqBool_refl; simpl. + rewrite binopEq_compat_eq in *; subst. + rewrite binopEq_refl; simpl. apply andb_true_iff. split; [eapply IHe1; eauto | eapply IHe2; eauto]. - andb_to_prop eq1; andb_to_prop eq2. - rewrite EquivEqBoolEq in *; subst. - rewrite mTypeEqBool_refl; simpl. + rewrite mTypeEq_compat_eq in *; subst. + rewrite mTypeEq_refl; simpl. eapply IHe; eauto. Qed. @@ -187,54 +202,126 @@ Fixpoint toREval (e:exp R) := | Const _ n => Const M0 n | Unop o e1 => Unop o (toREval e1) | Binop o e1 e2 => Binop o (toREval e1) (toREval e2) - | Downcast _ e1 => (toREval e1) + | Downcast _ e1 => Downcast M0 (toREval e1) end. -Fixpoint toREvalVars (d:nat -> option mType) (n:nat) := +Definition toRMap (d:nat -> option mType) (n:nat) := match d n with | Some m => Some M0 | None => None end. +Arguments toRMap _ _/. + (** Define a perturbation function to ease writing of basic definitions **) Definition perturb (r:R) (e:R) := (r * (1 + e))%R. +Hint Unfold perturb. + (** Define expression evaluation relation parametric by an "error" epsilon. The result value expresses float computations according to the IEEE standard, using a perturbation of the real valued computation by (1 + delta), where |delta| <= machine epsilon. **) -Inductive eval_exp (E:env) (defVars: nat -> option mType) :(exp R) -> R -> mType -> Prop := +Inductive eval_exp (E:env) (Gamma: nat -> option mType) :(exp R) -> R -> mType -> Prop := | Var_load m x v: - defVars x = Some m -> + Gamma x = Some m -> E x = Some v -> - eval_exp E defVars (Var R x) v m + eval_exp E Gamma (Var R x) v m | Const_dist m n delta: - Rle (Rabs delta) (Q2R (meps m)) -> - eval_exp E defVars (Const m n) (perturb n delta) m + Rle (Rabs delta) (Q2R (mTypeToQ m)) -> + eval_exp E Gamma (Const m n) (perturb n delta) m | Unop_neg m f1 v1: - eval_exp E defVars f1 v1 m -> - eval_exp E defVars (Unop Neg f1) (evalUnop Neg v1) m + eval_exp E Gamma f1 v1 m -> + eval_exp E Gamma (Unop Neg f1) (evalUnop Neg v1) m | Unop_inv m f1 v1 delta: - Rle (Rabs delta) (Q2R (meps m)) -> - eval_exp E defVars f1 v1 m -> - eval_exp E defVars (Unop Inv f1) (perturb (evalUnop Inv v1) delta) m + Rle (Rabs delta) (Q2R (mTypeToQ m)) -> + eval_exp E Gamma f1 v1 m -> + (~ v1 = 0)%R -> + eval_exp E Gamma (Unop Inv f1) (perturb (evalUnop Inv v1) delta) m | Downcast_dist m m1 f1 v1 delta: (* Downcast expression f1 (evaluating to machine type m1), to a machine type m, less precise than m1.*) isMorePrecise m1 m = true -> - Rle (Rabs delta) (Q2R (meps m)) -> - eval_exp E defVars f1 v1 m1 -> - eval_exp E defVars (Downcast m f1) (perturb v1 delta) m + Rle (Rabs delta) (Q2R (mTypeToQ m)) -> + eval_exp E Gamma f1 v1 m1 -> + eval_exp E Gamma (Downcast m f1) (perturb v1 delta) m | Binop_dist m1 m2 op f1 f2 v1 v2 delta: - Rle (Rabs delta) (Q2R (meps (computeJoin m1 m2))) -> - eval_exp E defVars f1 v1 m1 -> - eval_exp E defVars f2 v2 m2 -> + Rle (Rabs delta) (Q2R (mTypeToQ (join m1 m2))) -> + eval_exp E Gamma f1 v1 m1 -> + eval_exp E Gamma f2 v2 m2 -> ((op = Div) -> (~ v2 = 0)%R) -> - eval_exp E defVars (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta) (computeJoin m1 m2). + eval_exp E Gamma (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta) (join m1 m2). + +Hint Constructors eval_exp. + +(** + Show some simpler rule lemmata +**) +Lemma Const_dist' m n delta v m' E Gamma: + Rle (Rabs delta) (Q2R (mTypeToQ m)) -> + v = perturb n delta -> + m' = m -> + eval_exp E Gamma (Const m n) v m'. +Proof. + intros; subst; auto. +Qed. + +Hint Resolve Const_dist'. + +Lemma Unop_neg' m f1 v1 v m' E Gamma: + eval_exp E Gamma f1 v1 m -> + v = evalUnop Neg v1 -> + m' = m -> + eval_exp E Gamma (Unop Neg f1) (evalUnop Neg v1) m'. +Proof. + intros; subst; auto. +Qed. + +Hint Resolve Unop_neg'. + +Lemma Unop_inv' m f1 v1 delta v m' E Gamma: + Rle (Rabs delta) (Q2R (mTypeToQ m)) -> + eval_exp E Gamma f1 v1 m -> + (~ v1 = 0)%R -> + v = perturb (evalUnop Inv v1) delta -> + m' = m -> + eval_exp E Gamma (Unop Inv f1) v m'. +Proof. + intros; subst; auto. +Qed. + +Hint Resolve Unop_inv'. + +Lemma Downcast_dist' m m1 f1 v1 delta v m' E Gamma: + isMorePrecise m1 m = true -> + Rle (Rabs delta) (Q2R (mTypeToQ m)) -> + eval_exp E Gamma f1 v1 m1 -> + v = (perturb v1 delta) -> + m' = m -> + eval_exp E Gamma (Downcast m f1) v m'. +Proof. + intros; subst; eauto. +Qed. + +Hint Resolve Downcast_dist'. + +Lemma Binop_dist' m1 m2 op f1 f2 v1 v2 delta v m' E Gamma: + Rle (Rabs delta) (Q2R (mTypeToQ m')) -> + eval_exp E Gamma f1 v1 m1 -> + eval_exp E Gamma f2 v2 m2 -> + ((op = Div) -> (~ v2 = 0)%R) -> + v = perturb (evalBinop op v1 v2) delta -> + m' = join m1 m2 -> + eval_exp E Gamma (Binop op f1 f2) v m'. +Proof. + intros; subst; auto. +Qed. + +Hint Resolve Binop_dist'. (** Define the set of "used" variables of an expression to be the set of variables @@ -257,67 +344,48 @@ Lemma delta_0_deterministic (v:R) (delta:R): perturb v delta = v. Proof. intros abs_0; apply Rabs_0_impl_eq in abs_0; subst. - unfold perturb. - lra. + unfold perturb. lra. Qed. -(* TODO: need of `general` case? *) -Lemma general_meps_0_deterministic (f:exp R) (E:env) defVars: - forall v1 v2 m1, - m1 = M0 -> - eval_exp E defVars (toREval f) v1 m1 -> - eval_exp E defVars (toREval f) v2 M0 -> - v1 = v2. -Proof. - induction f; intros * m10_eq eval_v1 eval_v2. - - inversion eval_v1; inversion eval_v2; subst; auto; - try repeat (repeat rewrite delta_0_deterministic; simpl in *; rewrite Q2R0_is_0 in *; subst; auto); simpl. - rewrite H6 in H1; inversion H1; subst; auto. - - inversion eval_v1; inversion eval_v2; subst; auto; - try repeat (repeat rewrite delta_0_deterministic; simpl in *; rewrite Q2R0_is_0 in *; subst; auto); simpl. - - inversion eval_v1; inversion eval_v2; subst; auto; - try repeat (repeat rewrite delta_0_deterministic; simpl in *; rewrite Q2R0_is_0 in *; subst; auto); simpl. - + apply Ropp_eq_compat. apply (IHf v0 v3 M0); auto. - + inversion H4. - + inversion H5. - + rewrite (IHf v0 v3 M0); auto. - - inversion eval_v1; inversion eval_v2; subst; auto; - try repeat (repeat rewrite delta_0_deterministic; simpl in *; rewrite Q2R0_is_0 in *; subst; auto); simpl. - destruct m0; destruct m2; inversion H5. - destruct m3; destruct m4; inversion H11. - simpl in *. - rewrite (IHf1 v0 v4 M0); auto. - rewrite (IHf2 v5 v3 M0); auto. - rewrite Q2R0_is_0 in H2,H12. - rewrite delta_0_deterministic; auto. - rewrite delta_0_deterministic; auto. - - simpl toREval in eval_v1. - simpl toREval in eval_v2. - apply (IHf v1 v2 m1); auto. -Qed. - -(* Lemma rnd_0_deterministic f E m v: *) -(* eval_exp E (toREval (Downcast m f)) v M0 <-> *) -(* eval_exp E (toREval f) v M0. *) -(* Proof. *) -(* split; intros. *) -(* - simpl in H. auto. *) -(* - simpl; auto. *) -(* Qed. *) - - (** Evaluation with 0 as machine epsilon is deterministic **) -Lemma meps_0_deterministic (f:exp R) (E:env) defVars: +Lemma meps_0_deterministic (f:exp R) (E:env) Gamma: forall v1 v2, - eval_exp E defVars (toREval f) v1 M0 -> - eval_exp E defVars (toREval f) v2 M0 -> + eval_exp E Gamma (toREval f) v1 M0 -> + eval_exp E Gamma (toREval f) v2 M0 -> v1 = v2. Proof. - intros v1 v2 ev1 ev2. - assert (M0 = M0) by auto. - apply (general_meps_0_deterministic f H ev1 ev2). + induction f; + intros v1 v2 ev1 ev2. + - inversion ev1; inversion ev2; subst. + rewrite H1 in H6. + inversion H6; auto. + - inversion ev1; inversion ev2; subst. + simpl in *. + rewrite Q2R0_is_0 in *; + repeat (rewrite delta_0_deterministic; try auto). + - inversion ev1; inversion ev2; subst; try congruence. + + rewrite (IHf v0 v3); eauto. + + rewrite (IHf v0 v3); eauto. + simpl in *. + rewrite Q2R0_is_0 in *; + repeat (rewrite delta_0_deterministic; try auto). + - inversion ev1; inversion ev2; subst. + apply M0_join_is_M0 in H11; apply M0_join_is_M0 in H2. + destruct H2, H11; subst. + rewrite (IHf1 v0 v4); try auto. + rewrite (IHf2 v3 v5); try auto. + simpl in *. + rewrite Q2R0_is_0 in *. + repeat (rewrite delta_0_deterministic; try auto). + - inversion ev1; inversion ev2; subst. + apply M0_least_precision in H1; + apply M0_least_precision in H7; subst. + rewrite (IHf v0 v3); try auto. + simpl in *. + rewrite Q2R0_is_0 in *. + repeat (rewrite delta_0_deterministic; try auto). Qed. (** @@ -326,24 +394,19 @@ For each evaluation of using an arbitrary epsilon, we can replace it by evaluating the subexpressions and then binding the result values to different variables in the Environment. **) -Lemma binary_unfolding b f1 f2 m E vF defVars: - eval_exp E defVars (Binop b f1 f2) vF m -> - exists vF1 vF2 m1 m2, - m = computeJoin m1 m2 /\ - eval_exp E defVars f1 vF1 m1 /\ - eval_exp E defVars f2 vF2 m2 /\ - eval_exp (updEnv 2 vF2 (updEnv 1 vF1 emptyEnv)) - (updDefVars 2 m2 (updDefVars 1 m1 defVars)) - (Binop b (Var R 1) (Var R 2)) vF m. +Lemma binary_unfolding b f1 f2 E v1 v2 m1 m2 Gamma: + (b = Div -> ~(v2 = 0 )%R) -> + eval_exp E Gamma f1 v1 m1 -> + eval_exp E Gamma f2 v2 m2 -> + eval_exp E Gamma (Binop b f1 f2) (perturb (evalBinop b v1 v2) (Q2R (mTypeToQ (join m1 m2)))) (join m1 m2) -> + eval_exp (updEnv 2 v2 (updEnv 1 v1 emptyEnv)) + (updDefVars 2 m2 (updDefVars 1 m1 Gamma)) + (Binop b (Var R 1) (Var R 2)) (perturb (evalBinop b v1 v2) (Q2R (mTypeToQ (join m1 m2)))) (join m1 m2). Proof. - intros eval_float. - inversion eval_float; subst. - exists v1 ; exists v2; exists m1; exists m2; repeat split; try auto. - eapply Binop_dist; eauto. - - pose proof (isMorePrecise_refl m1). - eapply Var_load; eauto. - - pose proof (isMorePrecise_refl m2). - eapply Var_load; eauto. + intros no_div_zero eval_f1 eval_f2 eval_float. + econstructor; try auto. + rewrite Rabs_right; try lra. + auto using Rle_ge, mTypeToQ_pos_R. Qed. (* diff --git a/coq/Infra/Ltacs.v b/coq/Infra/Ltacs.v index fdd0c30..e1c1255 100644 --- a/coq/Infra/Ltacs.v +++ b/coq/Infra/Ltacs.v @@ -1,6 +1,6 @@ (** Ltac definitions **) -Require Import Coq.Bool.Bool Coq.Reals.Reals. -Require Import Daisy.Infra.RealSimps Daisy.Infra.NatSet. +Require Import Coq.Bool.Bool Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qreals. +Require Import Daisy.Infra.RealSimps Daisy.Infra.NatSet Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps. Ltac iv_assert iv name:= assert (exists ivlo ivhi, iv = (ivlo, ivhi)) as name by (destruct iv; repeat eexists; auto). @@ -17,6 +17,21 @@ Ltac andb_to_prop H := try andb_to_prop Left; try andb_to_prop Right. +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 + end. + +Ltac canonize_Q_to_R := + match goal with + | [ H: (?a <= ?b)%Q |- _ ] => apply Qle_Rle in H + | [ H: context [Q2R 0] |- _ ] => rewrite Q2R0_is_0 in H + | [ |- context [Q2R 0] ] => rewrite Q2R0_is_0 + end. + +Ltac canonize_hyps := repeat canonize_Q_prop; repeat canonize_Q_to_R. + Ltac NatSet_simp hyp := try rewrite NatSet.mem_spec in hyp; try rewrite NatSet.equal_spec in hyp; @@ -36,4 +51,19 @@ Ltac 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 - end. \ No newline at end of file + end. + +Ltac match_simpl := + match goal with + | [ H: ?t = ?u |- context [match ?t with _ => _ end]] => rewrite H; simpl + end. + +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 + end . diff --git a/coq/Infra/MachineType.v b/coq/Infra/MachineType.v index c1e18b1..a89f9ca 100644 --- a/coq/Infra/MachineType.v +++ b/coq/Infra/MachineType.v @@ -1,13 +1,22 @@ -Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals. -Require Import Coq.Reals.Reals Coq.micromega.Psatz. +(** + Implementation of machine-precision as a datatype for mixed-precision computations + + @author: Raphael Monat + @maintainer: Heiko Becker + **) +Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs + Coq.QArith.Qreals Coq.Reals.Reals Coq.micromega.Psatz. +Require Import Daisy.Infra.RealRationalProps. (** - Define machine types, and some tool functions. Needed for the - mixed-precision part, to be able to define a rounding operator. + Define machine precision as datatype **) Inductive mType: Type := M0 | M32 | M64 | M128 | M256. -Definition meps (e:mType) : Q := +(** + Injection of machine types into Q +**) +Definition mTypeToQ (e:mType) :Q := match e with | M0 => 0 | M32 => (Qpower (2#1) (Zneg 24)) @@ -18,34 +27,26 @@ Definition meps (e:mType) : Q := | M256 => (Qpower (2#1) (Zneg 211)) end. -Lemma meps_pos : - forall e, 0 <= meps e. +Arguments mTypeToQ _/. + +Lemma mTypeToQ_pos_Q: + forall e, 0 <= mTypeToQ e. Proof. intro e. - case_eq e; intro; simpl meps; apply Qle_bool_iff; auto. + case_eq e; intro; + simpl mTypeToQ; apply Qle_bool_iff; auto. Qed. -Lemma meps_posR : - forall e, (0 <= Q2R (meps e))%R. +Lemma mTypeToQ_pos_R : + forall e, (0 <= Q2R (mTypeToQ e))%R. Proof. intro. - assert (Q2R 0 = 0%R) by (unfold Q2R; simpl; lra). - rewrite <- H. + rewrite <- Q2R0_is_0. apply Qle_Rle. - apply meps_pos. + apply mTypeToQ_pos_Q. Qed. -(* Definition mTypeEqBool (m1:mType) (m2:mType) := *) -(* Qeq_bool (meps m1) (meps m2). *) - -(* TODO: unused? *) -(* Theorem eq_mType_dec: forall (m1 m2:mType), {m1 = m2} + {m1 <> m2}. *) -(* Proof. *) -(* intros. *) -(* case_eq m1; intros; case_eq m2; intros; auto; right; intro; inversion H1. *) -(* Qed. *) - -Definition mTypeEqBool (m1:mType) (m2:mType) := +Definition mTypeEq (m1:mType) (m2:mType) := match m1, m2 with | M0, M0 => true | M32, M32 => true @@ -55,179 +56,82 @@ Definition mTypeEqBool (m1:mType) (m2:mType) := | _, _ => false end. -Lemma mTypeEqBool_sym (m1:mType) (m2:mType): - forall b, mTypeEqBool m1 m2 = b -> mTypeEqBool m2 m1 = b. +Lemma mTypeEq_compat_eq(m1:mType) (m2:mType): + mTypeEq m1 m2 = true <-> m1 = m2. Proof. - intros. - destruct b, m1, m2; simpl; cbv; auto. + split; intros eq_case; + case_eq m1; intros m1_case; + case_eq m2; intros m2_case; subst; + try congruence; try auto; + cbv in eq_case; inversion eq_case. Qed. -Lemma mTypeEqBool_refl (m:mType): - mTypeEqBool m m = true. +Lemma mTypeEq_refl (m:mType): + mTypeEq m m = true. Proof. - intros. destruct m; cbv; auto. + intros. rewrite mTypeEq_compat_eq; auto. Qed. - -(* Definition mTypeEqComp (m1:mType) (m2:mType) := *) -(* Qeq_bool (meps m1) (meps m2). *) - -(* Lemma EquivBoolComp (m1:mType) (m2:mType): *) -(* mTypeEqBool m1 m2 = true <-> mTypeEqComp m1 m2 = true. *) -(* Proof. *) -(* split; intros. *) -(* - case_eq m1; intros; case_eq m2; intros; auto; try rewrite H0 in H; rewrite H1 in H; cbv; auto. *) -(* - case_eq m1; intros; case_eq m2; intros; auto; try rewrite H0 in H; rewrite H1 in H; unfold mTypeEqComp in H; cbv in H; inversion H. *) -(* Qed. *) - -Lemma EquivEqBoolEq (m1:mType) (m2:mType): - mTypeEqBool m1 m2 = true <-> m1 = m2. +Lemma mTypeEq_compat_eq_false (m1:mType) (m2:mType): + mTypeEq m1 m2 = false <-> ~(m1 = m2). Proof. - split; intros; case_eq m1; intros; case_eq m2; intros; auto; rewrite H0 in H; rewrite H1 in H; cbv in H; inversion H; auto. + split; intros eq_case. + - hnf; intros; subst. rewrite mTypeEq_refl in eq_case. + congruence. + - case_eq m1; intros; case_eq m2; intros; subst; cbv; congruence. Qed. - -(* Definition mTypeEq: relation mType := *) -(* fun m1 m2 => Qeq (meps m1) (meps m2). *) - - -(* Instance mTypeEquivalence: Equivalence mTypeEq. *) -(* Proof. *) -(* split; intros. *) -(* - intro. apply Qeq_refl. *) -(* - intros a b eq. apply Qeq_sym. auto. *) -(* - intros a b c eq1 eq2. eapply Qeq_trans; eauto. *) -(* Qed. *) - - -(* Lemma mTypeEquivs (m1:mType) (m2:mType): *) -(* mTypeEqBool m1 m2 = true <-> mTypeEq m1 m2. *) -(* Proof. *) -(* split; unfold mTypeEqBool; unfold mTypeEq; apply Qeq_bool_iff. *) -(* Qed. *) - -Definition isMorePrecise (m1:mType) (m2:mType) := - (* check if m1 is more precise than m2, i.e. if the epsilon of m1 is *) - (* smaller than the epsilon of m2 *) - if (mTypeEqBool m2 M0) then - true - else if (mTypeEqBool m1 M0) then - mTypeEqBool m2 M0 - else - Qle_bool (meps m1) (meps m2). - -(** - Check if m1 is a more precise floating point type, meaning that the corresponding machine epsilon is less. - Special Case m0, which must be the bottom element. -**) -Definition isMorePrecise' (m1:mType) (m2:mType) := - match m2, m1 with - |M0, _ => true - |M32, M0 => false - |M32, _ => true - |M64, M0 | M64, M32 => false - |M64, _ => true - |M128, M128 => true - |M128, M256 => true - |M256, M256 => true - |_, _ => false - end. - -(* Lemma ismoreprec_rw m1 m2: *) -(* forall b, isMorePrecise m1 m2 = b <-> isMorePrecise' m1 m2 = b. *) -(* Admitted. *) - -Lemma isMorePrecise_refl (m1:mType) : - isMorePrecise m1 m1 = true. +Lemma mTypeEq_sym (m1:mType) (m2:mType): + forall b, mTypeEq m1 m2 = b -> mTypeEq m2 m1 = b. Proof. - unfold isMorePrecise; simpl. - case_eq (mTypeEqBool m1 M0); intro hyp; [ auto | apply Qle_bool_iff; apply Qle_refl ]. + intros. + destruct b; + [rewrite mTypeEq_compat_eq in * | rewrite mTypeEq_compat_eq_false in *]; + auto. Qed. -(* Definition isMorePrecise_rel (m1:mType) (m2:mType) := *) -(* Qle (meps m1) (meps m2). *) - - -Definition computeJoin (m1:mType) (m2:mType) := - if (isMorePrecise m1 m2) then m1 else m2. - - -(* Everything below is unused? *) -Definition isJoinOf (m:mType) (m1:mType) (m2:mType) := - (* is m the join of m1 and m2 ?*) - if (isMorePrecise m1 m2) then - mTypeEqBool m m1 - else - mTypeEqBool m m2. - -Lemma ifisMorePreciseM0 (m:mType) : - isMorePrecise M0 m = true -> m = M0. -Proof. - intro. - unfold isMorePrecise in H. - case_eq (mTypeEqBool m M0); intros; rewrite H0 in H; auto. - - apply EquivEqBoolEq in H0; auto. - - assert (mTypeEqBool M0 M0 = true) by (apply EquivEqBoolEq; auto). - rewrite H1 in H. - inversion H. -Qed. +(** + Check if machine precision m1 is more precise than machine precision m2. + M0 is real-valued evaluation, hence the most precise. + All others are compared by + mTypeToQ m1 <= mTypeToQ m2 + **) +Definition isMorePrecise (m1:mType) (m2:mType) := + Qle_bool (mTypeToQ m1) (mTypeToQ m2). -Lemma ifM0isJoin_l (m:mType) (m1:mType) (m2:mType) : - m = M0 -> isJoinOf m m1 m2 = true -> m1 = M0. +Lemma isMorePrecise_refl (m:mType) : + isMorePrecise m m = true. Proof. - intros H0 H. - unfold isJoinOf in H. - case_eq (isMorePrecise m1 m2); intro Hyp; rewrite Hyp in H; simpl in H; rewrite H0 in H; subst. - - case_eq m1; intros; auto; unfold isMorePrecise in Hyp; rewrite H0 in H; compute in H; inversion H. - - unfold isMorePrecise in Hyp. - apply EquivEqBoolEq in H; symmetry in H; apply EquivEqBoolEq in H. - rewrite H in Hyp; inversion Hyp. + unfold isMorePrecise; simpl. + apply Qle_bool_iff; lra. Qed. - -Lemma ifM0isJoin_r (m:mType) (m1:mType) (m2:mType) : - m = M0 -> isJoinOf m m1 m2 = true -> m2 = M0. +Lemma M0_least_precision (m:mType) : + isMorePrecise m M0 = true -> m = M0. Proof. - intros H0 H. - unfold isJoinOf in H. - case_eq (isMorePrecise m1 m2); intro Hyp; rewrite Hyp in H; simpl in H; rewrite H0 in H; subst. - - apply EquivEqBoolEq in H. rewrite <- H in Hyp; subst. - unfold isMorePrecise in Hyp. - case_eq (mTypeEqBool m2 M0); intros; auto; rewrite H in Hyp. - apply EquivEqBoolEq in H; auto. - case_eq (mTypeEqBool M0 M0); intros; auto; rewrite H0 in Hyp. - inversion Hyp. - unfold mTypeEqBool in H0; inversion H0. - - apply EquivEqBoolEq in H; auto. + intro m_morePrecise. + unfold isMorePrecise in *. + destruct m; cbv in m_morePrecise; congruence. Qed. -Lemma ifM0isJoin (m1:mType) (m2:mType): - isJoinOf M0 m1 m2 = true -> m1 = M0 /\ m2 = M0. +Lemma M0_lower_bound (m:mType) : + isMorePrecise M0 m = true. Proof. - assert (M0 = M0) by auto. - intros; split. - - apply (ifM0isJoin_l M0 m1 m2); auto. - - apply (ifM0isJoin_r M0 m1 m2); auto. + destruct m; unfold isMorePrecise; cbv; auto. Qed. -Lemma computeJoinIsJoin (m1:mType) (m2:mType) : - isJoinOf (computeJoin m1 m2) m1 m2 = true. -Proof. - remember (computeJoin m1 m2) as m. - unfold isJoinOf. - unfold computeJoin in Heqm. - case_eq (isMorePrecise m1 m2); intros; auto; - rewrite H in Heqm; - rewrite Heqm; - apply EquivEqBoolEq; auto. -Qed. +(** + Function computing the join of two precisions, this is the most precise type, + in which evaluation has to be performed, e.g. addition of 32 and 64 bit floats + has to happen in 64 bits +**) +Definition join (m1:mType) (m2:mType) := + if (isMorePrecise m1 m2) then m2 else m1. -Lemma isJoinComputeJoin (M:mType) (m1:mType) (m2:mType) : - isJoinOf M m1 m2 = true -> - M = computeJoin m1 m2. +Lemma M0_join_is_M0 m1 m2: + join m1 m2 = M0 -> m1 = M0 /\ m2 = M0. Proof. + unfold join. intros. - unfold computeJoin. - unfold isJoinOf in H. - case_eq (isMorePrecise m1 m2); intros; auto; rewrite H0 in H; apply EquivEqBoolEq; auto. + destruct m1, m2; simpl in *; cbv in *; try congruence; try auto. Qed. \ No newline at end of file diff --git a/coq/Infra/NatSet.v b/coq/Infra/NatSet.v index 873cc23..b3647aa 100644 --- a/coq/Infra/NatSet.v +++ b/coq/Infra/NatSet.v @@ -30,4 +30,64 @@ End OWL. Module NatSet := MakeWithLeibniz OWL. -Module NatSetProps := WPropertiesOn OWL NatSet. \ No newline at end of file +Module NatSetProps := WPropertiesOn OWL NatSet. + +Notation "S1 ∪ S2" := (NatSet.union S1 S2) (at level 80, right associativity). + +Notation "'{{' x '}}'" := (NatSet.singleton x) (at level 0, no associativity). + +Notation "S1 -- S2" := (NatSet.diff S1 S2) (at level 80, right associativity). + +Notation "x 'mem' S" := (NatSet.mem x S) (at level 0, no associativity). + +Notation "x '∈' S" := (NatSet.In x S) (at level 100, no associativity). + +Check (forall x S, x ∈ S -- {{x}}). + +Lemma not_in_not_mem: + forall n S, + NatSet.mem n S = false -> + ~ NatSet.In n S. +Proof. + intros * not_mem; hnf; intros not_in. + rewrite <- NatSet.mem_spec in not_in; + rewrite not_in in *; + congruence. +Qed. + +(** TODO: Merge with NatSet_prop tactic in Ltacs file **) +Ltac set_hnf_tac := + match goal with + | [ H: NatSet.mem ?x _ = true |- _ ] => rewrite NatSet.mem_spec in H; set_hnf_tac + | [ H: NatSet.mem ?x _ = false |- _] => apply not_in_not_mem in H; set_hnf_tac + | [ |- context [NatSet.mem ?x _]] => rewrite NatSet.mem_spec; set_hnf_tac + | [ |- context [NatSet.In ?x (NatSet.union ?SA ?SB)]] => rewrite NatSet.union_spec; set_hnf_tac + | [ |- context [NatSet.In ?x (NatSet.diff ?A ?B)]] => rewrite NatSet.diff_spec; set_hnf_tac + | [ H: context [NatSet.In ?x (NatSet.diff ?A ?B)] |- _] => rewrite NatSet.diff_spec in H; destruct H; set_hnf_tac + | [ |- context [NatSet.In ?x (NatSet.singleton ?y)]] => rewrite NatSet.singleton_spec + | [ |- context [NatSet.Subset ?SA ?SB]] => hnf; intros; set_hnf_tac + | [ H: NatSet.Subset ?SA ?SB |- NatSet.In ?v ?SB] => apply H; set_hnf_tac + | _ => idtac + end. + +Ltac set_tac := + set_hnf_tac; + simpl in *; try auto. + + +Lemma add_spec_strong: + forall x y S, + (x ∈ (NatSet.add y S)) <-> x = y \/ ((~ (x = y)) /\ (x ∈ S)). +Proof. + split; intros x_in_add. + - rewrite NatSet.add_spec in x_in_add. + case_eq (Nat.eqb x y); intros x_eq_case. + + left; apply Nat.eqb_eq; auto. + + right; destruct x_in_add as [x_eq | x_in_S]; subst. + * rewrite Nat.eqb_refl in x_eq_case; congruence. + * split; try auto. + hnf; intros; subst. + rewrite Nat.eqb_refl in x_eq_case; congruence. + - rewrite NatSet.add_spec. + destruct x_in_add as [ x_eq | [x_neq x_in_S]]; auto. +Qed. diff --git a/coq/Infra/RationalSimps.v b/coq/Infra/RationalSimps.v index 1493ad0..dd6b9de 100644 --- a/coq/Infra/RationalSimps.v +++ b/coq/Infra/RationalSimps.v @@ -3,17 +3,16 @@ **) Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs. Require Import Coq.micromega.Psatz. -Require Import Daisy.Infra.Abbrevs Daisy.Infra.Ltacs. -Definition Qleb :=Qle_bool. +Definition Qleb := Qle_bool. Definition Qeqb := Qeq_bool. (* Definition machineEpsilon := (1#(2^53)). *) -Definition maxAbs (iv:intv) := +Definition maxAbs (iv:Q*Q) := Qmax (Qabs (fst iv)) (Qabs (snd iv)). -Definition minAbs (iv:intv) := +Definition minAbs (iv:Q*Q) := Qmin (Qabs (fst iv)) (Qabs (snd iv)). Lemma maxAbs_pointIntv a: diff --git a/coq/Infra/RealRationalProps.v b/coq/Infra/RealRationalProps.v index 9241731..e5c5073 100644 --- a/coq/Infra/RealRationalProps.v +++ b/coq/Infra/RealRationalProps.v @@ -2,26 +2,9 @@ Some rewriting properties for translating between rationals and real numbers. These are used in the soundness proofs since we want to have the final theorem on the real valued evaluation. **) -Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals. -Require Import Coq.Reals.Reals Coq.micromega.Psatz. -Require Import Daisy.Infra.RationalSimps Daisy.Infra.Abbrevs. -Require Import Daisy.IntervalArith Daisy.Infra.RealSimps. - -(* TODO: Move me *) -Lemma beq_nat_sym a b: - beq_nat a b = beq_nat b a. -Proof. - case_eq (a =? b); intros. - - apply beq_nat_true in H. - rewrite H. - apply beq_nat_refl. - - apply beq_nat_false in H. - case_eq (b =? a); intros. - + apply beq_nat_true in H0. - rewrite H0 in H. - auto. - + auto. -Qed. +Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs + Coq.QArith.Qreals Coq.Reals.Reals Coq.micromega.Psatz. +Require Import Daisy.Infra.RationalSimps Daisy.Infra.RealSimps. Lemma Q2R0_is_0: Q2R 0 = 0%R. @@ -160,4 +143,10 @@ Lemma Q_case_div_to_R_case_div a b: (Q2R b < 0 \/ 0 < Q2R a)%R. Proof. intros [le | gr]; [left | right]; rewrite <- Q2R0_is_0; apply Qlt_Rlt; auto. +Qed. + +Lemma Rabs_0_equiv: + (Rbasic_fun.Rabs 0 <= Q2R 0)%R. +Proof. + rewrite Q2R0_is_0, Rbasic_fun.Rabs_R0; lra. Qed. \ No newline at end of file diff --git a/coq/Infra/RealSimps.v b/coq/Infra/RealSimps.v index f670b82..75c31cf 100644 --- a/coq/Infra/RealSimps.v +++ b/coq/Infra/RealSimps.v @@ -4,6 +4,15 @@ Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.Setoids.Setoid. +(** Define the maxAbs function on R and prove some minor properties of it. +TODO: Make use of IVLO and IVhi + **) +Definition RmaxAbsFun (iv:R * R) := + Rmax (Rabs (fst iv)) (Rabs (snd iv)). + +Definition RminAbsFun (iv: R * R) := + Rmin (Rabs (fst iv)) (Rabs (snd iv)). + Lemma Rsub_eq_Ropp_Rplus (a:R) (b:R) : (a - b = a + (- b))%R. Proof. diff --git a/coq/IntervalArith.v b/coq/IntervalArith.v index f74e273..c23d203 100644 --- a/coq/IntervalArith.v +++ b/coq/IntervalArith.v @@ -4,28 +4,37 @@ **) Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.Qreals. Require Import Daisy.Infra.Abbrevs Daisy.Infra.RealSimps. + (** Define validity of an interval, requiring that the lower bound is less than or equal to the upper bound. Containement is defined such that if x is contained in the interval, it must lie between the lower and upper bound. **) -Definition valid (intv:interval) :Prop := +Notation valid intv := (IVlo intv <= IVhi intv)%R. -Definition contained (x:R) (intv:interval) := +Notation contained x intv := (IVlo intv <= x <= IVhi intv)%R. Lemma contained_implies_valid (a:R) (iv:interval) : contained a iv -> valid iv. Proof. - unfold contained, valid; intros inIntv; apply (Rle_trans _ a _); destruct inIntv; auto. + intros inIntv; apply (Rle_trans _ a _); destruct inIntv; auto. Qed. (** Subset definition; when an interval is a subinterval of another **) -Definition isSupersetInterval (iv1:interval) (iv2:interval) := - (IVlo iv2 <= IVlo iv1)%R /\ (IVhi iv1 <= IVhi iv2)%R. +Notation isSupersetInterval iv1 iv2 := + ((IVlo iv2 <= IVlo iv1)%R /\ (IVhi iv1 <= IVhi iv2)%R). + +Lemma contained_superset a iv1 iv2: + contained a iv1 -> + isSupersetInterval iv1 iv2 -> + contained a iv2. +Proof. + intros; simpl in *. lra. +Qed. Definition pointInterval (x:R) := mkInterval x x. @@ -34,32 +43,13 @@ Lemma contained_implies_subset (a:R) (iv:interval): isSupersetInterval (pointInterval a) iv. Proof. intros containedIntv. - unfold contained, isSupersetInterval, pointInterval in *; destruct containedIntv; split; auto. + unfold pointInterval in *; destruct containedIntv; split; auto. Qed. -(** - Definition of validity conditions for interval operations, Addition, Subtraction, Multiplication and Division - **) -Definition validIntervalAdd (iv1:interval) (iv2:interval) (iv3:interval) := - forall a b, contained a iv1 -> contained b iv2 -> - contained (a + b) iv3. - -Definition validIntervalSub (iv1:interval) (iv2:interval) (iv3:interval) := - forall a b, contained a iv1 -> contained b iv2 -> - contained (a - b) iv3. - -Definition validIntervalMult (iv1:interval) (iv2:interval) (iv3:interval) := - forall a b, contained a iv1 -> contained b iv2 -> - contained (a * b) iv3. - -Definition validIntervalDiv (iv1:interval) (iv2:interval) (iv3:interval) := - forall a b, contained a iv1 -> contained b iv2 -> - contained (a / b) iv3. - Lemma validPointInterval (a:R) : contained a (pointInterval a). Proof. - unfold contained; split; simpl; apply Req_le; auto. + split; simpl; apply Req_le; auto. Qed. (** @@ -135,7 +125,7 @@ Definition negateInterval (iv:interval) := mkInterval (- IVhi iv) (- IVlo iv). Lemma interval_negation_valid (iv:interval) (a:R) : contained a iv -> contained (- a) (negateInterval iv). Proof. - unfold contained; destruct iv as [ivlo ivhi]; simpl; intros [ivlo_le_a a_le_ivhi]. + destruct iv as [ivlo ivhi]; simpl; intros [ivlo_le_a a_le_ivhi]. split; apply Ropp_ge_le_contravar; apply Rle_ge; auto. Qed. @@ -144,7 +134,7 @@ Definition invertInterval (iv:interval) := mkInterval (/ IVhi iv) (/ IVlo iv). Lemma interval_inversion_valid (iv:interval) (a:R) : (IVhi iv < 0 \/ 0 < IVlo iv -> contained a iv -> contained (/ a) (invertInterval iv))%R. Proof. - unfold contained; destruct iv as [ivlo ivhi]; simpl; + destruct iv as [ivlo ivhi]; simpl; intros [ivhi_lt_zero | zero_lt_ivlo]; intros [ivlo_le_a a_le_ivhi]; assert (ivlo <= ivhi)%R by (eapply Rle_trans; eauto); split. @@ -167,12 +157,12 @@ Qed. Definition addInterval (iv1:interval) (iv2:interval) := absIntvUpd Rplus iv1 iv2. -Lemma interval_addition_valid iv1 iv2: - validIntervalAdd iv1 iv2 (addInterval iv1 iv2). +Lemma interval_addition_valid iv1 iv2 a b: + contained a iv1 -> + contained b iv2 -> + contained (a + b) (addInterval iv1 iv2). Proof. - unfold validIntervalAdd. - intros a b. - unfold contained, addInterval, absIntvUpd, min4, max4. + unfold addInterval, absIntvUpd, min4, max4. intros [lo_leq_a a_leq_hi] [lo_leq_b b_leq_hi]. simpl; split. (** Lower Bound **) @@ -190,11 +180,12 @@ Qed. Definition subtractInterval (iv1:interval) (iv2:interval) := addInterval iv1 (negateInterval iv2). -Corollary interval_subtraction_valid iv1 iv2: - validIntervalSub iv1 iv2 (subtractInterval iv1 iv2). +Corollary interval_subtraction_valid iv1 iv2 a b: + contained a iv1 -> + contained b iv2 -> + contained (a - b) (subtractInterval iv1 iv2). Proof. unfold subtractInterval. - intros a b. intros contained_1 contained_iv2. rewrite Rsub_eq_Ropp_Rplus. apply interval_addition_valid; auto. @@ -214,7 +205,7 @@ Lemma interval_multiplication_valid (iv1:interval) (iv2:interval) (a:R) (b:R) : contained b iv2 -> contained (a * b) (multInterval iv1 iv2). Proof. - unfold contained, multInterval, absIntvUpd, IVlo, IVhi. + unfold multInterval, absIntvUpd, IVlo, IVhi. destruct iv1 as [ivlo1 ivhi1]; destruct iv2 as [ivlo2 ivhi2]; simpl. intros [lo_leq_a a_leq_hi] [lo_leq_b b_leq_hi]. pose proof (min4_correct (ivlo1 * ivlo2) (ivlo1 * ivhi2) (ivhi1 * ivlo2) (ivhi1 * ivhi2)) @@ -295,22 +286,13 @@ Proof. apply interval_inversion_valid; auto. Qed. -(** Define the maxAbs function on R and prove some minor properties of it. -TODO: Make use of IVLO and IVhi - **) -Definition RmaxAbsFun (iv:interval) := - Rmax (Rabs (fst iv)) (Rabs (snd iv)). - -Definition RminAbsFun (iv:interval) := - Rmin (Rabs (fst iv)) (Rabs (snd iv)). - Lemma contained_leq_maxAbs a iv: contained a iv -> (Rabs a <= RmaxAbsFun iv)%R. Proof. intros contained_a. unfold RmaxAbsFun. - unfold contained in contained_a; simpl in contained_a; destruct contained_a. + simpl in contained_a; destruct contained_a. eapply RmaxAbs; auto. Qed. @@ -342,14 +324,13 @@ Lemma distance_gives_iv a b e iv: (Rabs (a - b) <= e)%R -> contained b (widenInterval iv e). Proof. - intros contained_a abs_le; unfold contained in *; simpl in *. + intros contained_a abs_le; simpl in *. destruct contained_a as [lo_a a_hi]. rewrite Rabs_minus_sym in abs_le. unfold Rabs in abs_le. destruct Rcase_abs in abs_le; try lra. Qed. - Lemma minAbs_positive_iv_is_lo a b: (0 < a)%R -> (a <= b)%R -> diff --git a/coq/IntervalArithQ.v b/coq/IntervalArithQ.v index 24be82c..1bb4cac 100644 --- a/coq/IntervalArithQ.v +++ b/coq/IntervalArithQ.v @@ -5,6 +5,7 @@ Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.micromega.Psatz. Require Import Coq.ZArith.ZArith. Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps. + (** Define validity of an intv, requiring that the lower bound is less than or equal to the upper bound. Containement is defined such that if x is contained in the intv, it must lie between the lower and upper bound. @@ -302,8 +303,8 @@ Proof. + apply Qlt_le_weak in q. destruct (Qlt_le_dec ivhi2 0). * apply Qlt_le_weak in q0. - pose proof (Qmult_le_compat_neg_l q b_leq_hi) as ahi2_leq_ab. - pose proof (Qmult_le_compat_neg_l q0 a_leq_hi) as hihi_leq_ahi2. + pose proof (Qmult_le_compat_neg_l _ _ _ q b_leq_hi) as ahi2_leq_ab. + pose proof (Qmult_le_compat_neg_l _ _ _ q0 a_leq_hi) as hihi_leq_ahi2. eapply Qle_trans. apply leq_hihi. rewrite Qmult_comm. eapply Qle_trans. apply hihi_leq_ahi2. @@ -324,7 +325,7 @@ Proof. rewrite Qmult_comm. eapply Qle_trans. apply Qlt_le_weak in q0. - apply (Qmult_le_compat_neg_l q0 a_leq_hi). + apply (Qmult_le_compat_neg_l _ _ _ q0 a_leq_hi). rewrite Qmult_comm. setoid_rewrite Qmult_comm at 1 2. eapply (Qmult_le_compat_r _ _ a); auto. diff --git a/coq/IntervalValidation.v b/coq/IntervalValidation.v index 9b6df85..116f660 100644 --- a/coq/IntervalValidation.v +++ b/coq/IntervalValidation.v @@ -61,9 +61,13 @@ Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond) (vali end else false | Downcast _ f1 => - let (iv1, _) := absenv f1 in - andb (validIntervalbounds f1 absenv P validVars) (andb (isSupersetIntv intv iv1) (isSupersetIntv iv1 intv)) - (* TODO: intv = iv1 might be a hard constraint... *) + if (validIntervalbounds f1 absenv P validVars) + then + let (iv1, _) := absenv f1 in + (* TODO: intv = iv1 might be a hard constraint... *) + (isSupersetIntv intv iv1) && (isSupersetIntv iv1 intv) + else + false end. Fixpoint validIntervalboundsCmd (f:cmd Q) (absenv:analysisResult) (P:precond) (validVars:NatSet.t) :bool:= @@ -170,9 +174,8 @@ Proof. apply le_neq_bool_to_lt_prop; auto. Qed. - -Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) fVars dVars (E:env) defVars: - forall vR, +Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) + fVars dVars (E:env) Gamma: validIntervalbounds f absenv P dVars = true -> (forall v, NatSet.mem v dVars = true -> exists vR, E v = Some vR /\ @@ -181,437 +184,360 @@ Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) (forall v, NatSet.mem v fVars = true -> exists vR, E v = Some vR /\ (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> - eval_exp E (toREvalVars defVars) (toREval (toRExp f)) vR M0 -> - (Q2R (fst (fst (absenv f))) <= vR <= Q2R (snd (fst (absenv f))))%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 (absenv f))) <= vR <= Q2R (snd (fst (absenv f))))%R. Proof. - induction f; intros vR valid_bounds valid_definedVars usedVars_subset valid_usedVars eval_f. - - unfold validIntervalbounds in valid_bounds. - env_assert absenv (Var Q n) absenv_var. - destruct absenv_var as [ iv [err absenv_var]]. - specialize (valid_usedVars n). - simpl; rewrite absenv_var in *; simpl in *. - inversion eval_f; subst. - case_eq (NatSet.mem n dVars); intros case_mem; rewrite case_mem in *; simpl in *. - + specialize (valid_definedVars n case_mem). - destruct valid_definedVars as [vR' [E_n_eq [gamma_n iv_n]]]. - rewrite H1 in E_n_eq; inversion E_n_eq; subst. - rewrite absenv_var in *; auto. - + repeat (rewrite delta_0_deterministic in *; try auto). - unfold isSupersetIntv in valid_bounds. - andb_to_prop valid_bounds. - apply Qle_bool_iff in L0; - apply Qle_bool_iff in R0. - apply Qle_Rle in L0; - apply Qle_Rle in R0. - simpl in *. - assert (NatSet.mem n fVars = true) as in_fVars. - * assert (NatSet.In n (NatSet.singleton n)) - as in_singleton by (rewrite NatSet.singleton_spec; auto). - rewrite NatSet.mem_spec. - hnf in usedVars_subset. - apply usedVars_subset. - rewrite NatSet.diff_spec, NatSet.singleton_spec. - split; try auto. - hnf; intros in_dVars. - rewrite <- NatSet.mem_spec in in_dVars. - rewrite in_dVars in case_mem; congruence. - * specialize (valid_usedVars in_fVars); - destruct valid_usedVars as [vR' [vR_def P_valid]]. - rewrite vR_def in H1; inversion H1; subst. + induction f; + intros valid_bounds valid_definedVars usedVars_subset valid_freeVars types_defined; + simpl in *. + - env_assert absenv (Var Q n) absenv_var. + destruct absenv_var as [iv_n [err_n absenv_var]]. + case_eq (NatSet.mem n dVars); intros dVars_case; + rewrite dVars_case, absenv_var in valid_bounds; simpl in *. + + destruct (valid_definedVars n) as [vR [env_valid bounds_valid]]; try auto. + eexists; split; simpl; 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. + assert (NatSet.In n fVars) by set_tac. + eexists; split; [econstructor | ]; 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 absenv_var. + simpl in *. lra. - - unfold validIntervalbounds in valid_bounds. - simpl in *; destruct (absenv (Const m v)) as [intv err]; simpl in *. - 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_f; subst. - rewrite delta_0_deterministic; auto. - unfold contained; simpl. - split. - + apply Is_true_eq_true in valid_lo. - unfold Qleb in *. - apply Qle_bool_iff in valid_lo. - apply Qle_Rle in valid_lo; auto. - + apply Is_true_eq_true in valid_hi. - unfold Qleb in *. - apply Qle_bool_iff in valid_hi. - apply Qle_Rle in valid_hi; auto. - + simpl in H2; rewrite Q2R0_is_0 in H2; auto. - - case_eq (absenv (Unop u f)); intros intv err absenv_unop. - destruct intv as [unop_lo unop_hi]; simpl. - unfold validIntervalbounds in valid_bounds. - simpl 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_rec valid_definedVars usedVars_subset valid_usedVars H3). - rewrite absenv_f in IHf; simpl in IHf. - (* TODO: Make lemma *) - unfold isSupersetIntv in valid_unop. - apply andb_prop_elim in valid_unop. - destruct valid_unop as [valid_lo valid_hi]. - apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi. - apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi. - pose proof (interval_negation_valid (iv :=(Q2R (fst intv_f),(Q2R (snd intv_f)))) (a :=v1)) as negation_valid. - unfold contained, negateInterval in negation_valid; simpl in *. - apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi. - destruct IHf. - split. - * eapply Rle_trans. apply valid_lo. - rewrite Q2R_opp; lra. - * eapply Rle_trans. - Focus 2. apply valid_hi. - rewrite Q2R_opp; lra. - + specialize (IHf v1 valid_rec valid_definedVars usedVars_subset valid_usedVars H4). - rewrite absenv_f in IHf; simpl in IHf. - apply andb_prop_elim in valid_unop. - destruct valid_unop as [nodiv0 valid_unop]. + - exists (perturb (Q2R v) 0). + split; [econstructor; eauto; apply Rabs_0_equiv | ]. + env_assert absenv (Const m v) absenv_const; + destruct absenv_const as [iv_v [err_v absenv_const]]. + rewrite absenv_const in *; simpl in *. + andb_to_prop valid_bounds. + canonize_hyps. + simpl in *; unfold perturb; lra. + - env_assert absenv (Unop u f) absenv_unop; + destruct absenv_unop as [iv_u [err_u absenv_unop]]. + rewrite absenv_unop in *; simpl in *. + case_eq (validIntervalbounds f absenv P dVars); + intros case_bounds; rewrite case_bounds in *; try congruence. + env_assert absenv f absenv_f; + destruct absenv_f as [iv_f [ err_f absenv_f]]; rewrite absenv_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_unop. - apply andb_prop_elim in valid_unop. - destruct valid_unop as [valid_lo valid_hi]. - apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi. - apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi. - assert ((Q2R (ivhi intv_f) < 0)%R \/ (0 < Q2R (ivlo intv_f))%R) as nodiv0_prop. - * apply Is_true_eq_true in nodiv0. - apply le_neq_bool_to_lt_prop in nodiv0. - destruct nodiv0. - { left; rewrite <- Q2R0_is_0; apply Qlt_Rlt; auto. } - { right; rewrite <- Q2R0_is_0; apply Qlt_Rlt; auto. } - * pose proof (interval_inversion_valid (iv :=(Q2R (fst intv_f),(Q2R (snd intv_f)))) (a :=v1)) as inv_valid. - unfold contained, invertInterval in inv_valid; simpl in *. - apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi. - destruct IHf. - rewrite delta_0_deterministic; auto. - unfold perturb; split. - { eapply Rle_trans. apply valid_lo. - destruct nodiv0_prop as [nodiv0_neg | nodiv0_pos]. - (* TODO: Extract lemma maybe *) - - assert (0 < - (Q2R (snd intv_f)))%R as negation_pos by lra. - assert (- (Q2R (snd intv_f)) <= - v1)%R as negation_flipped_hi by lra. - apply Rinv_le_contravar in negation_flipped_hi; try auto. - rewrite <- Ropp_inv_permute in negation_flipped_hi; try lra. - rewrite <- Ropp_inv_permute in negation_flipped_hi; try lra. - apply Ropp_le_contravar in negation_flipped_hi. - repeat rewrite Ropp_involutive in negation_flipped_hi; - rewrite Q2R_inv; auto. - hnf; intros is_0. - rewrite <- Q2R0_is_0 in nodiv0_neg. - apply Rlt_Qlt in nodiv0_neg; lra. - - rewrite Q2R_inv. - apply Rinv_le_contravar; try lra. - hnf; intros is_0. - assert (Q2R (fst intv_f) <= Q2R (snd intv_f))%R by lra. - rewrite <- Q2R0_is_0 in nodiv0_pos. - apply Rlt_Qlt in nodiv0_pos; apply Rle_Qle in H2; lra. - } - { eapply Rle_trans. - Focus 2. apply valid_hi. - destruct nodiv0_prop as [nodiv0_neg | nodiv0_pos]. - - assert (Q2R (fst intv_f) < 0)%R as fst_lt_0 by lra. - assert (0 < - (Q2R (fst intv_f)))%R as negation_pos by lra. - assert (- v1 <= - (Q2R (fst intv_f)))%R as negation_flipped_lo by lra. - apply Rinv_le_contravar in negation_flipped_lo; try auto. - rewrite <- Ropp_inv_permute in negation_flipped_lo; try lra. - rewrite <- Ropp_inv_permute in negation_flipped_lo; try lra. - apply Ropp_le_contravar in negation_flipped_lo. - repeat rewrite Ropp_involutive in negation_flipped_lo; - rewrite Q2R_inv; auto. - hnf; intros is_0. - rewrite <- Q2R0_is_0 in negation_pos. - rewrite <- Q2R_opp in negation_pos. - apply Rlt_Qlt in negation_pos; lra. - assert (0 < - (Q2R (snd intv_f)))%R by lra. + unfold isSupersetIntv in valid_bounds; + andb_to_prop valid_bounds. + canonize_hyps. + simpl in *. + rewrite Q2R_opp in *. + lra. + + andb_to_prop valid_bounds. + rename L 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 *) + 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. + 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. + - rewrite Q2R_inv; try auto. + destruct nodiv0; try lra. + hnf; intros. + assert (0 < Q2R (snd iv_f))%R. + { eapply Rlt_le_trans. + apply Qlt_Rlt in H1. + rewrite <- Q2R0_is_0. + apply H1. lra. + } + rewrite <- Q2R0_is_0 in H3. + apply Rlt_Qlt in H3. lra. - - rewrite Q2R_inv. - apply Rinv_le_contravar; try lra. - hnf; intros is_0. - assert (Q2R (fst intv_f) <= Q2R (snd intv_f))%R by lra. - rewrite <- Q2R0_is_0 in nodiv0_pos. - apply Rlt_Qlt in nodiv0_pos; apply Rle_Qle in H2; lra. - } - { rewrite Q2R0_is_0 in H1; auto. } + - apply H0. + - rewrite <- Q2R_inv; try auto. + hnf; intros. + destruct nodiv0; try lra. + assert (Q2R (fst iv_f) < 0)%R. + { eapply Rle_lt_trans. + Focus 2. + rewrite <- Q2R0_is_0; + apply Qlt_Rlt in H2; apply H2. + lra. + } + rewrite <- Q2R0_is_0 in H3. + apply Rlt_Qlt in H3. lra. } + - env_assert absenv (Binop b f1 f2) absenv_b; + destruct absenv_b as [iv_b [err_b absenv_b]]. + env_assert absenv f1 absenv_f1; + destruct absenv_f1 as [iv_f1 [err_f1 absenv_f1]]. + env_assert absenv f2 absenv_f2; + destruct absenv_f2 as [iv_f2 [err_f2 absenv_f2]]. + rewrite absenv_b in *; simpl in *. + 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 absenv_f1, absenv_f2 in *; simpl in *. + assert (M0 = join M0 M0) as M0_join by (cbv; auto); + rewrite M0_join. + exists (perturb (evalBinop b vF1 vF2) 0); + 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. + specialize (valid_add vF1 vF2 valid_f1 valid_f2). + unfold isSupersetIntv in R. + andb_to_prop R. + canonize_hyps. + simpl in *. + repeat rewrite <- Q2R_plus in *; + rewrite <- Q2R_min4, <- Q2R_max4 in *. + 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. + specialize (valid_sub vF1 vF2 valid_f1 valid_f2). + unfold isSupersetIntv in R. + andb_to_prop R. + canonize_hyps. + simpl in *. + repeat rewrite <- Q2R_opp in *; + repeat rewrite <- Q2R_plus in *; + rewrite <- Q2R_min4, <- Q2R_max4 in *. + 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. + specialize (valid_mul vF1 vF2 valid_f1 valid_f2). + unfold isSupersetIntv in R. + andb_to_prop R. + canonize_hyps. + simpl in *. + repeat rewrite <- Q2R_mult in *; + rewrite <- Q2R_min4, <- Q2R_max4 in *. + unfold perturb. + lra. + * andb_to_prop R. + canonize_hyps. + apply le_neq_bool_to_lt_prop in L. + split; + [ econstructor; try congruence; try apply Rabs_0_equiv | ]. + (* 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. + simpl in *. + destruct valid_div; try auto. + - destruct L; rewrite <- Q2R0_is_0; [left | right]; apply Qlt_Rlt; auto. + - assert (~ snd iv_f2 == 0). + { hnf; intros. destruct L; try lra. + assert (0 < snd iv_f2) by (apply Rlt_Qlt; apply Qlt_Rlt in H2; lra). + lra. } + assert (~ fst iv_f2 == 0). + { hnf; intros; destruct L; try lra. + assert (fst iv_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 *. + rewrite <- Q2R_min4, <- Q2R_max4 in *. + unfold perturb. + lra. + } + - env_assert absenv (Downcast m f) absenv_d; + destruct absenv_d as [iv_d [err_d absenv_d]]; + env_assert absenv f absenv_f; + destruct absenv_f as [iv_f [err_f absenv_f]]; + rewrite absenv_d, absenv_f in *; simpl in *. + andb_to_prop valid_bounds. + destruct IHf as [vF [eval_f valid_f]]; try auto. + exists (perturb vF 0). + split; [try econstructor; try eauto; try apply Rabs_0_equiv; unfold isMorePrecise; auto |]. + canonize_hyps. + unfold perturb; simpl in *. + lra. +Qed. + +Lemma test3 Gamma n m: + forall x, + updDefVars n M0 (toRMap Gamma) x = toRMap (updDefVars n m Gamma) x. +Proof. + unfold updDefVars, toRMap; simpl. + intros x; destruct (x =? n); try auto. +Qed. + +Lemma test2 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 test5 e E vR m Gamma1 Gamma2: + (forall n, Gamma1 n = Gamma2 n) -> + eval_exp E Gamma1 e vR m -> + eval_exp E Gamma2 e vR m. +Proof. + revert E vR Gamma1 Gamma2 m; + induction e; intros * Gamma_eq eval_e; + inversion eval_e; subst; simpl in *; + try eauto. + apply Var_load; try auto. + rewrite <- Gamma_eq; auto. +Qed. + +Lemma test4 f E vR m Gamma1 Gamma2 : + (forall n, Gamma1 n = Gamma2 n) -> + bstep f E Gamma1 vR m -> + bstep f E Gamma2 vR m. +Proof. + revert E Gamma1 Gamma2; + induction f; intros * Gamma_eq eval_f. - inversion eval_f; subst. - rewrite delta_0_deterministic in eval_f; auto. - rewrite delta_0_deterministic; auto. - simpl 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. - simpl. - 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. - destruct m1; destruct m2; cbv in H2; inversion H2. - specialize (IHf1 v1 valid_e1 valid_definedVars). - specialize (IHf2 v2 valid_e2 valid_definedVars). - rewrite absenv_f1 in IHf1. - rewrite absenv_f2 in IHf2. - assert ((Q2R (fst (fst (iv1, err1))) <= v1 <= Q2R (snd (fst (iv1, err1))))%R) as valid_bounds_e1. - + apply IHf1; try auto. - intros v in_diff_e1. - apply usedVars_subset. - simpl. rewrite NatSet.diff_spec,NatSet.union_spec. - rewrite NatSet.diff_spec in in_diff_e1. - destruct in_diff_e1 as [ in_usedVars not_dVar]. - split; try auto. - + assert (Q2R (fst (fst (iv2, err2))) <= v2 <= Q2R (snd (fst (iv2, err2))))%R as valid_bounds_e2. - * apply IHf2; try auto. - intros v in_diff_e2. - apply usedVars_subset. - simpl. rewrite NatSet.diff_spec, NatSet.union_spec. - rewrite NatSet.diff_spec in in_diff_e2. - destruct in_diff_e2; split; auto. - * destruct b; simpl in *. - { pose proof (interval_addition_valid (iv1 :=(Q2R (fst iv1),Q2R (snd iv1))) (iv2 :=(Q2R (fst iv2), Q2R (snd iv2)))) as valid_add. - unfold validIntervalAdd in valid_add. - specialize (valid_add v1 v2 valid_bounds_e1 valid_bounds_e2). - 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]. - apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi. - apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi. - apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi. - destruct valid_add as [valid_add_lo valid_add_hi]. - split. - - eapply Rle_trans. apply valid_lo. - unfold ivlo. unfold addIntv. - simpl in valid_add_lo. - repeat rewrite <- Q2R_plus in valid_add_lo. - rewrite <- Q2R_min4 in valid_add_lo. - unfold absIvUpd; auto. - - eapply Rle_trans. - Focus 2. - apply valid_hi. - unfold ivlo, addIntv. - simpl in valid_add_hi. - repeat rewrite <- Q2R_plus in valid_add_hi. - rewrite <- Q2R_max4 in valid_add_hi. - unfold absIvUpd; auto. } - { pose proof (interval_subtraction_valid (iv1 := (Q2R (fst iv1),Q2R (snd iv1))) (iv2 :=(Q2R (fst iv2), Q2R (snd iv2)))) as valid_sub. - specialize (valid_sub v1 v2 valid_bounds_e1 valid_bounds_e2). - 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]. - apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi. - apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi. - apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi. - destruct valid_sub as [valid_sub_lo valid_sub_hi]. - split. - - eapply Rle_trans. - apply valid_lo. - unfold ivlo. unfold subtractIntv. - simpl in valid_sub_lo. - repeat rewrite <- Rsub_eq_Ropp_Rplus in valid_sub_lo. - repeat rewrite <- Q2R_minus in valid_sub_lo. - rewrite <- Q2R_min4 in valid_sub_lo. - unfold absIvUpd; auto. - - eapply Rle_trans. - Focus 2. - apply valid_hi. - unfold ivlo, addIntv. - simpl in valid_sub_hi. - repeat rewrite <- Rsub_eq_Ropp_Rplus in valid_sub_hi. - repeat rewrite <- Q2R_minus in valid_sub_hi. - rewrite <- Q2R_max4 in valid_sub_hi. - unfold absIvUpd; auto. } - { pose proof (interval_multiplication_valid (iv1 :=(Q2R (fst iv1),Q2R (snd iv1))) (iv2:=(Q2R (fst iv2), Q2R (snd iv2)))) as valid_mul. - specialize (valid_mul v1 v2 valid_bounds_e1 valid_bounds_e2). - 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]. - apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi. - apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi. - apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi. - destruct valid_mul as [valid_mul_lo valid_mul_hi]. - split. - - eapply Rle_trans. - apply valid_lo. - unfold ivlo. unfold multIntv. - simpl in valid_mul_lo. - repeat rewrite <- Q2R_mult in valid_mul_lo. - rewrite <- Q2R_min4 in valid_mul_lo. - unfold absIvUpd; auto. - - eapply Rle_trans. - Focus 2. - apply valid_hi. - unfold ivlo, addIntv. - simpl in valid_mul_hi. - repeat rewrite <- Q2R_mult in valid_mul_hi. - rewrite <- Q2R_max4 in valid_mul_hi. - unfold absIvUpd; auto. } - { pose proof (interval_division_valid (a:=v1) (b:=v2) (iv1:=(Q2R (fst iv1), Q2R (snd iv1))) (iv2:=(Q2R (fst iv2),Q2R (snd iv2)))) as valid_div. - rewrite <- andb_lazy_alt in valid_bin. - unfold contained in valid_div. - unfold isSupersetIntv in valid_bin. - apply andb_prop_elim in valid_bin; destruct valid_bin as [nodiv0 valid_bin]. - (** CONTINUE **) - apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi]. - apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi. - apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi. - apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi. - apply orb_prop_elim in nodiv0. - assert (snd iv2 < 0 \/ 0 < fst iv2). - - destruct nodiv0 as [lt_0 | lt_0]; - apply andb_prop_elim in lt_0; destruct lt_0 as [le_0 neq_0]; - apply Is_true_eq_true in le_0; apply Is_true_eq_true in neq_0; - apply negb_true_iff in neq_0; apply Qeq_bool_neq in neq_0; - rewrite Qle_bool_iff in le_0; - rewrite Qle_lteq in le_0; destruct le_0 as [lt_0 | eq_0]; - [ | exfalso; apply neq_0; auto | | exfalso; apply neq_0; symmetry; auto]; auto. - - destruct valid_div as [valid_div_lo valid_div_hi]; simpl; try auto. - + rewrite <- Q2R0_is_0. - destruct H; [left | right]; apply Qlt_Rlt; auto. - + unfold divideInterval, IVlo, IVhi in valid_div_lo, valid_div_hi. - simpl in *. - assert (Q2R (fst iv2) <= (Q2R (snd iv2)))%R by lra. - assert (~ snd iv2 == 0). - * destruct H; try lra. - hnf; intros ivhi2_0. - apply Rle_Qle in H0. - rewrite ivhi2_0 in H0. - lra. - * assert (~ fst iv2 == 0). - { destruct H; try lra. - hnf; intros ivlo2_0. - apply Rle_Qle in H0. - rewrite ivlo2_0 in H0. - lra. } - { split. - - eapply Rle_trans. apply valid_lo. - unfold ivlo. unfold multIntv. - simpl in valid_div_lo. - rewrite <- Q2R_inv in valid_div_lo; [ | auto]. - rewrite <- Q2R_inv in valid_div_lo; [ | auto]. - repeat rewrite <- Q2R_mult in valid_div_lo. - rewrite <- Q2R_min4 in valid_div_lo; auto. - - eapply Rle_trans. - Focus 2. - apply valid_hi. - simpl in valid_div_hi. - rewrite <- Q2R_inv in valid_div_hi; [ | auto]. - rewrite <- Q2R_inv in valid_div_hi; [ | auto]. - repeat rewrite <- Q2R_mult in valid_div_hi. - rewrite <- Q2R_max4 in valid_div_hi; auto. } } - + destruct m1; destruct m2; inversion H2. - simpl in H3; rewrite Q2R0_is_0 in H3; auto. - + destruct m1; destruct m2; inversion H2. - simpl in H3; rewrite Q2R0_is_0 in H3; auto. - - unfold validIntervalbounds in valid_bounds. - simpl in *; destruct (absenv (Downcast m f)); destruct (absenv f); simpl in *. - apply Is_true_eq_left in valid_bounds. - apply andb_prop_elim in valid_bounds. - destruct valid_bounds as [vI1 vI2]. - apply andb_prop_elim in vI2. - destruct vI2 as [vI2 vI2']. - apply Is_true_eq_true in vI2. - apply Is_true_eq_true in vI2'. - assert (isEqIntv i i0) as Eq by (apply supIntvAntisym; auto). - destruct Eq as [Eqlo Eqhi]. - simpl in *. - apply Qeq_eqR in Eqlo; rewrite Eqlo. - apply Qeq_eqR in Eqhi; rewrite Eqhi. - eapply IHf; try eauto. - apply Is_true_eq_true in vI1; auto. + econstructor; try eauto. + + eapply test5; eauto. + + apply (IHf _ (updDefVars n m0 Gamma1) _); try eauto. + intros n1. + unfold updDefVars. + case (n1 =? n); auto. + - inversion eval_f; subst. + econstructor; try eauto. + eapply test5; eauto. Qed. -Theorem validIntervalboundsCmd_sound (f:cmd Q) (absenv:analysisResult) defVars: - forall E vR fVars dVars outVars elo ehi err P, +Theorem validIntervalboundsCmd_sound (f:cmd Q) (absenv:analysisResult) Gamma: + forall E fVars dVars outVars elo ehi err P, ssa f (NatSet.union fVars dVars) outVars -> - bstep (toREvalCmd (toRCmd f)) E (toREvalVars defVars) vR M0 -> (forall v, NatSet.mem v dVars = true -> exists vR, E v = Some vR /\ (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (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) -> NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars -> validIntervalboundsCmd f absenv P dVars = true -> absenv (getRetExp f) = ((elo, ehi), err) -> - (Q2R elo <= vR <= Q2R ehi)%R. + exists vR, + bstep (toREvalCmd (toRCmd f)) E (toRMap Gamma) vR M0 /\ + (Q2R elo <= vR <= Q2R ehi)%R. Proof. + revert Gamma. induction f; - intros * ssa_f eval_f dVars_sound fVars_valid usedVars_subset valid_bounds_f absenv_f. + intros * ssa_f dVars_sound fVars_valid types_valid usedVars_subset valid_bounds_f absenv_f. - inversion ssa_f; subst. - inversion eval_f; subst. unfold validIntervalboundsCmd in valid_bounds_f. andb_to_prop valid_bounds_f. inversion ssa_f; subst. - specialize (IHf (updEnv n v E) vR fVars (NatSet.add n dVars)). - eapply IHf; eauto. - + 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. } - * eapply ssa_equal_set; eauto. - symmetry; eauto. - + 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. - eapply validIntervalbounds_sound; eauto. - simpl in usedVars_subset. - hnf. intros a in_usedVars. + pose proof (validIntervalbounds_sound e absenv 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. + hnf; intros; subst. + set_tac. } + 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. + { 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. + rewrite Nat.eqb_neq in v0_eq. + exfalso; apply v0_eq; auto. } + * 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. } + * 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. + 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. + 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. } + * clear L R1 R0 R IHf. + hnf. intros a a_freeVar. + rewrite NatSet.diff_spec in a_freeVar. + destruct a_freeVar as [a_freeVar a_no_dVar]. apply usedVars_subset. + simpl. 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. { hnf; intros; subst. - specialize (H5 n in_usedVars). - rewrite <- NatSet.mem_spec in H5. - rewrite H5 in H6; congruence. } - * 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. - rewrite Nat.eqb_neq in v0_eq. - exfalso; apply v0_eq; auto. - + 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. - + clear L R1 R0 R IHf. - hnf. intros a a_freeVar. - rewrite NatSet.diff_spec in a_freeVar. - destruct a_freeVar as [a_freeVar a_no_dVar]. - apply usedVars_subset. - simpl. - rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec. - repeat split; try auto. - * hnf; intros; subst. - apply a_no_dVar. - rewrite NatSet.add_spec; auto. - * hnf; intros a_dVar. - apply a_no_dVar. - rewrite NatSet.add_spec; auto. + apply a_no_dVar. + rewrite NatSet.add_spec; auto. } + { hnf; intros a_dVar. + apply a_no_dVar. + rewrite NatSet.add_spec; auto. } + * simpl. exists vR; split; [econstructor; eauto | auto]. + eapply test4 with (Gamma1 := toRMap (updDefVars n M0 Gamma)) ; try eauto. + intros n1; rewrite <- test3; auto. - unfold validIntervalboundsCmd in valid_bounds_f. - inversion eval_f; subst. - simpl in absenv_f. - assert (Q2R (fst (fst (absenv e))) <= vR <= Q2R (snd (fst (absenv e))))%R. - + simpl in valid_bounds_f; eapply validIntervalbounds_sound; eauto. - + simpl in *. rewrite absenv_f in *; auto. -Qed. + pose proof (validIntervalbounds_sound e absenv 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 absenv_f in *; simpl in *. + exists vR; split; [econstructor; eauto | auto]. +Qed. \ No newline at end of file diff --git a/coq/Typing.v b/coq/Typing.v index d46e712..914492e 100644 --- a/coq/Typing.v +++ b/coq/Typing.v @@ -2,131 +2,144 @@ Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith. Require Import Daisy.Infra.RealRationalProps Daisy.Expressions Daisy.Infra.Ltacs Daisy.Commands Daisy.ssaPrgs Daisy.Infra.RationalSimps. Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet Daisy.IntervalArithQ Daisy.IntervalArith Daisy.Infra.MachineType. -Fixpoint typeExpression (V:Type) (defVars:nat -> option mType) (e:exp V) : option mType := +Fixpoint typeExpression (V:Type) (Gamma:nat -> option mType) (e:exp V) : option mType := match e with - | Var _ v => defVars v + | Var _ v => Gamma v | Const m n => Some m - | Unop u e1 => typeExpression defVars e1 + | Unop u e1 => typeExpression Gamma e1 | Binop b e1 e2 => - let tm1 := typeExpression defVars e1 in - let tm2 := typeExpression defVars e2 in + let tm1 := typeExpression Gamma e1 in + let tm2 := typeExpression Gamma e2 in match tm1, tm2 with - | Some m1, Some m2 => Some (computeJoin m1 m2) + | Some m1, Some m2 => Some (join m1 m2) | _, _=> None end | Downcast m e1 => - let tm1 := typeExpression defVars e1 in + let tm1 := typeExpression Gamma e1 in match tm1 with |Some m1 => if (isMorePrecise m1 m) then Some m else None |_ => None end end. -Fixpoint typeMap (defVars:nat -> option mType) (e:exp Q) (e': exp Q) : option mType := +Fixpoint typeMap (Gamma:nat -> option mType) (e:exp Q) (e': exp Q) : option mType := match e with - | Var _ v => if expEqBool e e' then defVars v else None - | Const m n => if expEqBool e e' then Some m else None - | Unop u e1 => if expEqBool e e' then typeExpression defVars e else typeMap defVars e1 e' - | Binop b e1 e2 => if expEqBool e e' then typeExpression defVars e + | Var _ v => if expEq e e' then Gamma v else None + | Const m n => if expEq e e' then Some m else None + | Unop u e1 => if expEq e e' then typeExpression Gamma e else typeMap Gamma e1 e' + | Binop b e1 e2 => if expEq e e' then typeExpression Gamma e else - match (typeMap defVars e1 e'), (typeMap defVars e2 e') with - | Some m1, Some m2 => if (mTypeEqBool m1 m2) then Some m1 else None + match (typeMap Gamma e1 e'), (typeMap Gamma e2 e') with + | Some m1, Some m2 => if (mTypeEq m1 m2) then Some m1 else None | Some m1, None => Some m1 | None, Some m2 => Some m2 | None, None => None end - | Downcast m e1 => if expEqBool e e' then typeExpression defVars (Downcast m e1) else typeMap defVars e1 e' + | Downcast m e1 => if expEq e e' then typeExpression Gamma (Downcast m e1) else typeMap Gamma e1 e' end. -Fixpoint typeCmd (defVars:nat -> option mType) (f:cmd Q): option mType := +Fixpoint typeCmd (Gamma:nat -> option mType) (f:cmd Q): option mType := match f with - |Let m n e c => match typeExpression defVars e with - |Some m' => if isMorePrecise m m' then typeCmd defVars c + |Let m n e c => match typeExpression Gamma e with + |Some m' => if isMorePrecise m m' then typeCmd Gamma c else None |None => None end - |Ret e => typeExpression defVars e + |Ret e => typeExpression Gamma e end. -Fixpoint typeMapCmd (defVars:nat -> option mType) (f:cmd Q) (f':exp Q) : option mType := +Fixpoint typeMapCmd (Gamma:nat -> option mType) (f:cmd Q) (f':exp Q) : option mType := match f with - |Let m n e c => if expEqBool f' (Var Q n) then - match defVars n with + |Let m n e c => if expEq f' (Var Q n) then + match Gamma n with | Some m' => if isMorePrecise m m' then Some m else None | None => None end else - let te := typeMap defVars e in - let tc := typeMapCmd defVars c in + let te := typeMap Gamma e in + let tc := typeMapCmd Gamma c in match (te f'), (tc f') with - |Some m1, Some m2 => if mTypeEqBool m1 m2 then Some m1 else None + |Some m1, Some m2 => if mTypeEq m1 m2 then Some m1 else None |Some m1, None => Some m1 |None, Some m2 => Some m2 |None, None => None end - |Ret e => (typeMap defVars e) f' + |Ret e => (typeMap Gamma e) f' end. -Fixpoint typeCheck (e:exp Q) (defVars:nat -> option mType) (tMap: exp Q -> option mType) : bool := +Fixpoint typeCheck (e:exp Q) (Gamma:nat -> option mType) (tMap: exp Q -> option mType) : bool := match e with - | Var _ v => match tMap e, defVars v with - | Some m, Some m' => mTypeEqBool m m' + | Var _ v => match tMap e, Gamma v with + | Some m, Some m' => mTypeEq m m' | _, _ => false end | Const m n => match tMap e with - | Some m' => mTypeEqBool m m' + | Some m' => mTypeEq m m' | None => false end | Unop u e1 => match tMap e with | Some m => match tMap e1 with - | Some m' => mTypeEqBool m m' && typeCheck e1 defVars tMap + | Some m' => mTypeEq m m' && typeCheck e1 Gamma tMap | None => false end | None => false end | Binop b e1 e2 => match tMap e, tMap e1, tMap e2 with | Some m, Some m1, Some m2 => - mTypeEqBool m (computeJoin m1 m2) - && typeCheck e1 defVars tMap - && typeCheck e2 defVars tMap + mTypeEq m (join m1 m2) + && typeCheck e1 Gamma tMap + && typeCheck e2 Gamma tMap | _, _, _ => false end | Downcast m e1 => match tMap e, tMap e1 with - | Some m', Some m1 => mTypeEqBool m m' && isMorePrecise m1 m && typeCheck e1 defVars tMap + | Some m', Some m1 => mTypeEq m m' && isMorePrecise m1 m && typeCheck e1 Gamma tMap | _, _ => false end end. -Fixpoint typeCheckCmd (c:cmd Q) (defVars:nat -> option mType) (tMap:exp Q -> option mType) : bool := +Fixpoint typeCheckCmd (c:cmd Q) (Gamma:nat -> option mType) (tMap:exp Q -> option mType) : bool := match c with - | Let m x e g => match tMap (Var Q x), tMap e with - | Some mx, Some me => (mTypeEqBool mx m) && (isMorePrecise mx me) && typeCheck e defVars tMap && typeCheckCmd g defVars tMap - | _, _ => false - end - | Ret e => typeCheck e defVars tMap + | Let m x e g => if typeCheck e Gamma tMap + then + match tMap e with + | Some me => mTypeEq me m && typeCheckCmd g (updDefVars x me Gamma) tMap + | _ => false + end + else + false + | Ret e => typeCheck e Gamma tMap end. -(* Lemma eqTypeExpression e m defVars: *) -(* typeMap defVars e e = Some m <-> typeExpression defVars e = Some m. *) +(* Fixpoint typeCheckCmd (c:cmd Q) (Gamma:nat -> option mType) (tMap:exp Q -> option mType) : bool := *) +(* match c with *) +(* | Let m x e g => match tMap (Var Q x), tMap e with *) +(* | Some mx, Some me => (mTypeEq mx m) && (isMorePrecise mx me) && typeCheck e Gamma tMap && typeCheckCmd g Gamma tMap *) +(* | _, _ => false *) +(* end *) +(* | Ret e => typeCheck e Gamma tMap *) +(* end. *) + +(* Lemma eqTypeExpression e m Gamma: *) +(* typeMap Gamma e e = Some m <-> typeExpression Gamma e = Some m. *) (* Proof. *) -(* revert m defVars; induction e; intros. *) +(* revert m Gamma; induction e; intros. *) (* - split; intros. *) (* + simpl in *. *) (* rewrite <- beq_nat_refl in H; simpl in H; auto. *) (* + simpl in *. *) (* rewrite <- beq_nat_refl; simpl; auto. *) (* - split; intros; simpl in *. *) -(* + rewrite mTypeEqBool_refl,Qeq_bool_refl in H; simpl in H; auto. *) -(* + rewrite mTypeEqBool_refl,Qeq_bool_refl; simpl; auto. *) +(* + rewrite mTypeEq_refl,Qeq_bool_refl in H; simpl in H; auto. *) +(* + rewrite mTypeEq_refl,Qeq_bool_refl; simpl; auto. *) (* - split; intros; simpl in *. *) -(* + rewrite unopEqBool_refl,expEqBool_refl in H; simpl in H; auto. *) -(* + rewrite unopEqBool_refl,expEqBool_refl; simpl; auto. *) +(* + rewrite unopEqBool_refl,expEq_refl in H; simpl in H; auto. *) +(* + rewrite unopEqBool_refl,expEq_refl; simpl; auto. *) (* - split; intros; simpl in *. *) -(* + rewrite binopEqBool_refl,expEqBool_refl,expEqBool_refl in H; simpl in H; auto. *) -(* + rewrite binopEqBool_refl,expEqBool_refl,expEqBool_refl; simpl; auto. *) +(* + rewrite binopEqBool_refl,expEq_refl,expEq_refl in H; simpl in H; auto. *) +(* + rewrite binopEqBool_refl,expEq_refl,expEq_refl; simpl; auto. *) (* - split; intros; simpl in *. *) -(* + rewrite mTypeEqBool_refl,expEqBool_refl in H; simpl in H; auto. *) -(* + rewrite mTypeEqBool_refl,expEqBool_refl; simpl; auto. *) +(* + rewrite mTypeEq_refl,expEq_refl in H; simpl in H; auto. *) +(* + rewrite mTypeEq_refl,expEq_refl; simpl; auto. *) (* Qed. *) (* Definition Gamma_stronger (Gamma1 Gamma2: exp Q -> option mType):= *) @@ -143,10 +156,10 @@ Fixpoint typeCheckCmd (c:cmd Q) (defVars:nat -> option mType) (tMap:exp Q -> opt (* Qed. *) -(* Lemma Gamma_strengthening e Gamma1 Gamma2 defVars: *) +(* Lemma Gamma_strengthening e Gamma1 Gamma2 Gamma: *) (* Gamma_stronger Gamma1 Gamma2 -> *) -(* typeCheck e defVars Gamma1 = true -> *) -(* typeCheck e defVars Gamma2 = true. *) +(* typeCheck e Gamma Gamma1 = true -> *) +(* typeCheck e Gamma Gamma2 = true. *) (* Proof. *) (* revert Gamma1 Gamma2; induction e; intros. *) (* - simpl in *. *) @@ -162,9 +175,9 @@ Fixpoint typeCheckCmd (c:cmd Q) (defVars:nat -> option mType) (tMap:exp Q -> opt (* rewrite (H _ _ H1). *) (* case_eq (Gamma1 e); intros; rewrite H2 in H0; [ | inversion H0 ]. *) (* apply andb_true_iff in H0; destruct H0. *) -(* apply EquivEqBoolEq in H0; subst. *) +(* apply mTypeEq_compat_eq in H0; subst. *) (* rewrite (H _ _ H2). *) -(* rewrite mTypeEqBool_refl; simpl. *) +(* rewrite mTypeEq_refl; simpl. *) (* eapply IHe; eauto. *) (* - simpl in *. *) (* case_eq (Gamma1 (Binop b e1 e2)); intros; rewrite H1 in H0; [ | inversion H0 ]. *) @@ -186,27 +199,27 @@ Fixpoint typeCheckCmd (c:cmd Q) (defVars:nat -> option mType) (tMap:exp Q -> opt (* Qed. *) -Theorem typingSoundnessExp e defVars E: - forall v m Gamma, - typeCheck e defVars Gamma = true -> - eval_exp E defVars (toRExp e) v m -> - Gamma e = Some m. +Theorem typingSoundnessExp Gamma E: + forall e v m expTypes, + typeCheck e Gamma expTypes = true -> + eval_exp E Gamma (toRExp e) v m -> + expTypes e = Some m. Proof. - revert e; induction e; intros * typechecks evals. + induction e; intros * typechecks evals. - simpl in typechecks. inversion evals; subst. rewrite H0 in typechecks. - case_eq (Gamma (Var Q n)); intros; rewrite H in typechecks; [ | inversion typechecks ]. - apply EquivEqBoolEq in typechecks; subst; auto. + case_eq (expTypes (Var Q n)); intros; rewrite H in typechecks; [ | inversion typechecks ]. + apply mTypeEq_compat_eq in typechecks; subst; auto. - simpl in typechecks. inversion evals; subst. - case_eq (Gamma (Const m0 v)); intros; rewrite H in typechecks; [ | inversion typechecks ]. - apply EquivEqBoolEq in typechecks; subst; auto. + case_eq (expTypes (Const m0 v)); intros; rewrite H in typechecks; [ | inversion typechecks ]. + apply mTypeEq_compat_eq in typechecks; subst; auto. - simpl in typechecks. - case_eq (Gamma (Unop u e)); intros; rewrite H in typechecks; [ | inversion typechecks ]. - case_eq (Gamma e); intros; rewrite H0 in typechecks; [ | inversion typechecks ]. + case_eq (expTypes (Unop u e)); intros; rewrite H in typechecks; [ | inversion typechecks ]. + case_eq (expTypes e); intros; rewrite H0 in typechecks; [ | inversion typechecks ]. apply andb_true_iff in typechecks; destruct typechecks. - apply EquivEqBoolEq in H1; subst. + apply mTypeEq_compat_eq in H1; subst. inversion evals; subst. + rewrite <- H0. eapply IHe; eauto. @@ -214,38 +227,41 @@ Proof. eapply IHe; eauto. - inversion evals; subst. simpl in typechecks. - case_eq (Gamma (Binop b e1 e2)); intros; rewrite H in typechecks; [ | inversion typechecks ]. - case_eq (Gamma e1); intros; rewrite H0 in typechecks; [ | inversion typechecks ]. - case_eq (Gamma e2); intros; rewrite H1 in typechecks; [ | inversion typechecks ]. + case_eq (expTypes (Binop b e1 e2)); intros; rewrite H in typechecks; [ | inversion typechecks ]. + case_eq (expTypes e1); intros; rewrite H0 in typechecks; [ | inversion typechecks ]. + case_eq (expTypes e2); intros; rewrite H1 in typechecks; [ | inversion typechecks ]. andb_to_prop typechecks. - apply EquivEqBoolEq in L0; subst. - assert (Gamma e1 = Some m1) by (eapply IHe1; eauto). - assert (Gamma e2 = Some m2) by (eapply IHe2; eauto). + apply mTypeEq_compat_eq in L0; subst. + assert (expTypes e1 = Some m1) by (eapply IHe1; eauto). + assert (expTypes e2 = Some m2) by (eapply IHe2; eauto). rewrite H0 in H4. rewrite H1 in H5. inversion H4; inversion H5; subst; auto. - simpl in typechecks. - case_eq (Gamma (Downcast m e)); intros; rewrite H in typechecks; [ | inversion typechecks ]. - case_eq (Gamma e); intros; rewrite H0 in typechecks; [ | inversion typechecks ]. + case_eq (expTypes (Downcast m e)); intros; rewrite H in typechecks; [ | inversion typechecks ]. + case_eq (expTypes e); intros; rewrite H0 in typechecks; [ | inversion typechecks ]. andb_to_prop typechecks. - apply EquivEqBoolEq in L0; subst. + apply mTypeEq_compat_eq in L0; subst. inversion evals; subst. auto. Qed. -Theorem typingSoundnessCmd c defVars E v m Gamma: - typeCheckCmd c defVars Gamma = true -> - bstep (toRCmd c) E defVars v m -> - Gamma (getRetExp c) = Some m. +Theorem typingSoundnessCmd c Gamma E v m expTypes: + typeCheckCmd c Gamma expTypes = true -> + bstep (toRCmd c) E Gamma v m -> + expTypes (getRetExp c) = Some m. Proof. - revert E defVars; induction c; intros * tc bc. + revert Gamma E expTypes; induction c; intros * tc bc. - simpl in tc. - case_eq (Gamma (Var Q n)); intros; rewrite H in tc; [ | inversion tc ]. - case_eq (Gamma e); intros; rewrite H0 in tc; [ | inversion tc ]. + inversion bc; subst. andb_to_prop tc. - apply EquivEqBoolEq in L; subst. + assert (expTypes e = Some m0) + as e_type_m0 + by (eapply typingSoundnessExp; eauto). + specialize (IHc (updDefVars n m0 Gamma) (updEnv n v0 E)). simpl. - inversion bc; subst. - eapply IHc; eauto. + rewrite e_type_m0 in R. + andb_to_prop R. + apply IHc; auto. - simpl in *. inversion bc; subst. eapply typingSoundnessExp; eauto. diff --git a/coq/ssaPrgs.v b/coq/ssaPrgs.v index 0580620..b04e1c5 100644 --- a/coq/ssaPrgs.v +++ b/coq/ssaPrgs.v @@ -197,7 +197,7 @@ Proof. case_eq (n =? y); auto. Qed. - +(* Lemma shadowing_free_rewriting_exp e v E1 E2 defVars: (forall n, E1 n = E2 n)-> eval_exp E1 defVars (toREval e) v M0 <-> @@ -218,8 +218,8 @@ Proof. + erewrite IHe; eauto. + erewrite <- IHe; eauto. + erewrite <- IHe; eauto. - - split; intros eval_Binop; inversion eval_Binop; subst; econstructor; eauto; - destruct m1; destruct m2; inversion H2; + - split; intros eval_Binop; inversion eval_Binop; subst; econstructor; eauto. + destruct m1; destruct m2; inversion H2. try (erewrite IHe1; eauto); try (erewrite IHe2; eauto); auto. - split; intros eval_Downcast; simpl; simpl in eval_Downcast; erewrite IHe; eauto. @@ -275,7 +275,7 @@ Proof. rewrite <- NatSet.mem_spec in valid_vars. rewrite valid_vars in *; congruence. + econstructor; eauto. - rewrite H; auto. + rewrite H; auto. - inversion eval_e; subst; constructor; auto. - inversion eval_e; subst; econstructor; eauto. - simpl in valid_vars. @@ -301,7 +301,7 @@ Fixpoint exp_subst (e:exp Q) x e_new := |Downcast m e1 => Downcast m (exp_subst e1 x e_new) | e => e end. - +*) (* Lemma exp_subst_correct e e_sub E x v v_res defVars: *) (* eval_exp E defVars (toREval (toRExp e_sub)) v M0 -> *) (* eval_exp (updEnv x v E) defVars (toREval (toRExp e)) v_res M0 <-> *) -- GitLab