diff --git a/coq/CertificateChecker.v b/coq/CertificateChecker.v index 5c9734c2af48a21f3b8a88bf626052796f61d851..d8631ddcd72a161de699ce1dc84e559f94cf513c 100644 --- a/coq/CertificateChecker.v +++ b/coq/CertificateChecker.v @@ -6,7 +6,7 @@ **) Require Import Coq.Reals.Reals Coq.QArith.Qreals. Require Import Daisy.Infra.RealSimps Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps Daisy.Infra.Ltacs. -Require Import Daisy.IntervalValidation Daisy.ErrorValidation Daisy.Environments. +Require Import Daisy.IntervalValidation Daisy.ErrorValidation Daisy.Environments Daisy.Typing. Require Export Coq.QArith.QArith. Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Commands. @@ -14,7 +14,7 @@ Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Commands. (** Certificate checking function **) Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) := if (validIntervalbounds e absenv P NatSet.empty) - then (validErrorbound e absenv NatSet.empty) + then (validErrorbound e (fun (e:exp Q) => typeExpression e) absenv NatSet.empty) else false. (** @@ -23,14 +23,14 @@ Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) := the real valued execution respects the precondition. **) Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P: - forall (E1 E2:env) (vR:R) (vF:R) fVars, + forall (E1 E2:env) (vR:R) (vF:R) fVars m, approxEnv E1 absenv fVars NatSet.empty E2 -> (forall v, NatSet.mem v fVars = true -> - exists vR, E1 v = Some vR /\ + exists vR, E1 v = Some (vR, M0) /\ (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> - NatSet.Subset (usedVars e) fVars -> - eval_exp 0%R E1 (toRExp e) vR -> - eval_exp (Q2R machineEpsilon) E2 (toRExp e) vF -> + NatSet.Subset (Expressions.usedVars e) fVars -> + eval_exp E1 (toREval (toRExp e)) vR M0 -> + eval_exp E2 (toRExp e) vF m -> CertificateChecker e absenv P = true -> (Rabs (vR - vF) <= Q2R (snd (absenv e)))%R. (** @@ -38,8 +38,7 @@ Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P: validator and the error bound validator. **) Proof. - intros E1 E2 vR vF fVars approxE1E2 P_valid fVars_subset eval_real eval_float - certificate_valid. + intros * approxE1E2 P_valid fVars_subset eval_real eval_float certificate_valid. unfold CertificateChecker in certificate_valid. rewrite <- andb_lazy_alt in certificate_valid. andb_to_prop certificate_valid. @@ -48,30 +47,32 @@ Proof. destruct iv as [ivlo ivhi]. rewrite absenv_eq; simpl. eapply validErrorbound_sound; eauto. + - admit. (*eapply validTypeMap; 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. + - intros v m0 v_in_empty. rewrite NatSet.mem_spec in v_in_empty. inversion v_in_empty. -Qed. +Admitted. +(* Qed. *) Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) := if (validIntervalboundsCmd f absenv P NatSet.empty) - then (validErrorboundCmd f absenv NatSet.empty) + then (validErrorboundCmd f (fun e => typeExpression e) absenv NatSet.empty) else false. Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P: - forall (E1 E2:env) outVars vR vF fVars, + forall (E1 E2:env) outVars vR vF fVars m, approxEnv E1 absenv fVars NatSet.empty E2 -> (forall v, NatSet.mem v fVars= true -> - exists vR, E1 v = Some vR /\ + exists vR, E1 v = Some (vR, M0) /\ (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> NatSet.Subset (Commands.freeVars f) fVars -> ssa f fVars outVars -> - bstep (toRCmd f) E1 0 vR -> - bstep (toRCmd f) E2 (Q2R machineEpsilon) vF -> + bstep (toREvalCmd (toRCmd f)) E1 vR M0 -> + bstep (toRCmd f) E2 vF m -> CertificateCheckerCmd f absenv P = true -> (Rabs (vR - vF) <= Q2R (snd (absenv (getRetExp f))))%R. (** @@ -79,7 +80,7 @@ Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P: validator and the error bound validator. **) Proof. - intros E1 E2 outVars vR vF fVars approxE1E2 P_valid fVars_subset ssa_f eval_real eval_float + intros * approxE1E2 P_valid fVars_subset ssa_f eval_real eval_float certificate_valid. unfold CertificateCheckerCmd in certificate_valid. rewrite <- andb_lazy_alt in certificate_valid. @@ -89,6 +90,7 @@ Proof. destruct iv as [ivlo ivhi]. rewrite absenv_eq; simpl. eapply (validErrorboundCmd_sound); eauto. + - admit. (* eapply typeMapCmdValid; eauto.*) - instantiate (1 := outVars). eapply ssa_equal_set; try eauto. hnf. @@ -101,7 +103,7 @@ Proof. rewrite NatSet.diff_spec in in_diff. destruct in_diff. apply fVars_subset; auto. - - intros v v_in_empty. + - intros v m1 v_in_empty. rewrite NatSet.mem_spec in v_in_empty. inversion v_in_empty. -Qed. +Admitted. \ No newline at end of file diff --git a/coq/Commands.v b/coq/Commands.v index 7ccc418b770515a7444503c928210e199562b2c9..3a1950b361fc5aa57e82b1e311a228a95bf9dd02 100644 --- a/coq/Commands.v +++ b/coq/Commands.v @@ -2,6 +2,7 @@ Formalization of the Abstract Syntax Tree of a subset used in the Daisy framework **) Require Import Coq.Reals.Reals Coq.QArith.QArith. +Require Import Daisy.Expressions. Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Infra.NatSet. (** @@ -10,21 +11,67 @@ Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Infra.NatSet. Only assignments and return statement **) Inductive cmd (V:Type) :Type := -Let: nat -> exp V -> cmd V -> cmd V +Let: mType -> nat -> exp V -> cmd V -> cmd V | Ret: exp V -> cmd V. +Fixpoint getRetExp (V:Type) (f:cmd V) := + match f with + |Let m x e g => getRetExp g + | Ret e => e + end. + + +Fixpoint toRCmd (f:cmd Q) := + match f with + |Let m x e g => Let m x (toRExp e) (toRCmd g) + |Ret e => Ret (toRExp e) + end. + +Fixpoint toREvalCmd (f:cmd R) := + match f with + |Let m x e g => Let M0 x (toREval e) (toREvalCmd g) + |Ret e => Ret (toREval e) + end. + + +(*| Nop: cmd V. *) + +(* +UNUSED! + Small Step semantics for Daisy language +Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop := + let_s x e s E v eps: + eval_exp eps E e v -> + sstep (Let x e s) E eps s (updEnv x v E) + |ret_s e E v eps: + eval_exp eps E e v -> + sstep (Ret e) E eps (Nop R) (updEnv 0 v E). + *) + (** Define big step semantics for the Daisy language, terminating on a "returned" result value **) -Inductive bstep : cmd R -> env -> R -> R -> Prop := - let_b x e s E v eps res: - eval_exp eps E e v -> - bstep s (updEnv x v E) eps res -> - bstep (Let x e s) E eps res - |ret_b e E v eps: - eval_exp eps E e v -> - bstep (Ret e) E eps v. + +(* meaning of this -> mType ??? *) +(* Inductive bstep : cmd R -> env -> R -> mType -> Prop := *) +(* let_b m x e s E v res: *) +(* eval_exp E e v m -> *) +(* bstep s (updEnv x m v E) res m -> *) +(* bstep (Let m x e s) E res m *) +(* |ret_b m e E v: *) +(* eval_exp E e v m -> *) +(* bstep (Ret e) E v m. *) +Inductive bstep : cmd R -> env -> R -> mType -> Prop := + let_b m m' x e s E v res: + eval_exp E e v m -> + bstep s (updEnv x m v E) res m' -> + bstep (Let m x e s) E res m' + |ret_b m e E v: + eval_exp E e v m -> + bstep (Ret e) E v m. + + (** The free variables of a command are all used variables of expressions @@ -32,8 +79,8 @@ Inductive bstep : cmd R -> env -> R -> R -> Prop := **) Fixpoint freeVars V (f:cmd V) :NatSet.t := match f with - | Let x e g => NatSet.remove x (NatSet.union (usedVars e) (freeVars g)) - | Ret e => usedVars e + | Let _ x e1 g => NatSet.remove x (NatSet.union (Expressions.usedVars e1) (freeVars g)) + | Ret e => Expressions.usedVars e end. (** @@ -41,7 +88,7 @@ Fixpoint freeVars V (f:cmd V) :NatSet.t := **) Fixpoint definedVars V (f:cmd V) :NatSet.t := match f with - | Let x _ g => NatSet.add x (definedVars g) + | Let _ x _ g => NatSet.add x (definedVars g) | Ret _ => NatSet.empty end. @@ -51,6 +98,6 @@ Fixpoint definedVars V (f:cmd V) :NatSet.t := **) Fixpoint liveVars V (f:cmd V) :NatSet.t := match f with - | Let _ e g => NatSet.union (usedVars e) (liveVars g) + | Let _ _ e g => NatSet.union (usedVars e) (liveVars g) | Ret e => usedVars e end. \ No newline at end of file diff --git a/coq/Environments.v b/coq/Environments.v index 8c11f49049e34997a0ef92cff1a88dc33a74660e..8dd37a2046515a832ac412b325c2c55d1ed0173b 100644 --- a/coq/Environments.v +++ b/coq/Environments.v @@ -15,21 +15,21 @@ expression may yield different values for different machine epsilons Inductive approxEnv : env -> analysisResult -> NatSet.t -> NatSet.t -> env -> Prop := |approxRefl A: approxEnv emptyEnv A NatSet.empty NatSet.empty emptyEnv -|approxUpdFree E1 E2 A v1 v2 x fVars dVars: +|approxUpdFree E1 E2 A v1 v2 x fVars dVars m: approxEnv E1 A fVars dVars E2 -> - (Rabs (v1 - v2) <= Rabs v1 * Q2R machineEpsilon)%R -> + (Rabs (v1 - v2) <= (Rabs v1) * Q2R (meps m))%R -> NatSet.mem x (NatSet.union fVars dVars) = false -> - approxEnv (updEnv x v1 E1) A (NatSet.add x fVars) dVars (updEnv x v2 E2) -|approxUpdBound E1 E2 A v1 v2 x fVars dVars: + approxEnv (updEnv x M0 v1 E1) A (NatSet.add x fVars) dVars (updEnv x m v2 E2) +|approxUpdBound E1 E2 A v1 v2 x fVars dVars m: approxEnv E1 A fVars dVars E2 -> - (Rabs (v1 - v2) <= Q2R (snd (A (Var Q x))))%R -> + (Rabs (v1 - v2) <= Q2R (snd (A (Var Q m x))))%R -> NatSet.mem x (NatSet.union fVars dVars) = false -> - approxEnv (updEnv x v1 E1) A fVars (NatSet.add x dVars) (updEnv x v2 E2). + approxEnv (updEnv x M0 v1 E1) A fVars (NatSet.add x dVars) (updEnv x m v2 E2). -Inductive approxParams :env -> R -> env -> Prop := -|approxParamRefl eps: - approxParams emptyEnv eps emptyEnv -|approxParamUpd E1 E2 eps x v1 v2 : - approxParams E1 eps E2 -> - (Rabs (v1 - v2) <= eps)%R -> - approxParams (updEnv x v1 E1) eps (updEnv x v2 E2). +Inductive approxParams :env -> env -> Prop := +|approxParamRefl: + approxParams emptyEnv emptyEnv +|approxParamUpd E1 E2 m x v1 v2 : + approxParams E1 E2 -> + (Rabs (v1 - v2) <= Q2R (meps m))%R -> + approxParams (updEnv x M0 v1 E1) (updEnv x m v2 E2). diff --git a/coq/ErrorBounds.v b/coq/ErrorBounds.v index e03b368e1f8ce0d4f42bbf0998e0f02b058f15d4..204dffff21344dd3559657c62bc5be5f864c95fe 100644 --- a/coq/ErrorBounds.v +++ b/coq/ErrorBounds.v @@ -7,10 +7,10 @@ Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith. Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealSimps Daisy.Infra.RealRationalProps. Require Import Daisy.Environments Daisy.Infra.ExpressionAbbrevs. -Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (absenv:analysisResult): - eval_exp 0%R E1 (Const n) nR -> - eval_exp (Q2R machineEpsilon) E2 (Const n) nF -> - (Rabs (nR - nF) <= Rabs n * (Q2R machineEpsilon))%R. +Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (absenv:analysisResult) (m:mType): + eval_exp E1 (Const M0 n) nR M0 -> + eval_exp E2 (Const m n) nF m -> + (Rabs (nR - nF) <= Rabs n * (Q2R (meps m)))%R. Proof. intros eval_real eval_float. inversion eval_real; subst. @@ -19,6 +19,9 @@ Proof. unfold perturb; simpl. rewrite Rabs_err_simpl, Rabs_mult. apply Rmult_le_compat_l; [apply Rabs_pos | auto]. + simpl (meps M0) in *. + apply (Rle_trans _ (Q2R 0) _); try auto. + rewrite Q2R0_is_0; lra. Qed. (* @@ -42,39 +45,41 @@ 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): - eval_exp 0%R E1 (toRExp e1) e1R -> - eval_exp (Q2R machineEpsilon) E2 (toRExp e1) e1F -> - eval_exp 0%R E1 (toRExp e2) e2R -> - eval_exp (Q2R machineEpsilon) E2 (toRExp e2) e2F -> - eval_exp 0%R E1 (Binop Plus (toRExp e1) (toRExp e2)) vR -> - eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (Binop Plus (Var R 1) (Var R 2)) vF -> + (vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q) (m m1 m2:mType): + eval_exp E1 (toREval (toRExp e1)) e1R M0 -> + eval_exp E2 (toRExp e1) e1F m1-> + eval_exp E1 (toREval (toRExp e2)) e2R M0 -> + eval_exp E2 (toRExp e2) e2F m2 -> + eval_exp E1 (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR M0 -> + eval_exp (updEnv 2 m2 e2F (updEnv 1 m1 e1F emptyEnv)) (Binop Plus (Var R m1 1) (Var R m2 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 machineEpsilon)))%R. + (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + (Rabs (e1F + e2F) * (Q2R (meps 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 *) inversion plus_real; subst. + destruct m0; destruct m3; inversion H2; + simpl in H3; rewrite Q2R0_is_0 in H3; auto. rewrite delta_0_deterministic in plus_real; auto. rewrite (delta_0_deterministic (evalBinop Plus v1 v2) delta); auto. unfold evalBinop in *; simpl in *. - clear delta H2. - rewrite (meps_0_deterministic H3 e1_real); - rewrite (meps_0_deterministic H5 e2_real). - rewrite (meps_0_deterministic H3 e1_real) in plus_real. - rewrite (meps_0_deterministic H5 e2_real) in plus_real. - clear H3 H5 H6 v1 v2. + clear delta H3. + rewrite (meps_0_deterministic (toRExp e1) H5 e1_real); + rewrite (meps_0_deterministic (toRExp e2) H6 e2_real). + rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in plus_real. + rewrite (meps_0_deterministic (toRExp e2) H6 e2_real) in plus_real. + clear H5 H6 H7 v1 v2. (* Now unfold the float valued evaluation to get the deltas we need for the inequality *) inversion plus_float; subst. unfold perturb; simpl. - inversion H3; subst; inversion H5; subst. + inversion H4; subst; inversion H7; subst. unfold updEnv; simpl. - unfold updEnv in H0,H1; simpl in *. - symmetry in H0, H1. - inversion H0; inversion H1; subst. + unfold updEnv in H6,H9; simpl in *. + symmetry in H6,H9. + inversion H6; inversion H9; subst. (* We have now obtained all necessary values from the evaluations --> remove them for readability *) - clear plus_float H3 H5 plus_real e1_real e1_float e2_real e2_float H0 H1. + clear plus_float H4 H7 plus_real e1_real e1_float e2_real e2_float H8 H6 H9. repeat rewrite Rmult_plus_distr_l. rewrite Rmult_1_r. rewrite Rsub_eq_Ropp_Rplus. @@ -97,7 +102,7 @@ Proof. eapply Rle_trans. eapply Rmult_le_compat_l. apply Rabs_pos. - apply H2. + apply H3. apply Req_le; auto. Qed. @@ -105,39 +110,41 @@ Qed. Copy-Paste proof with minor differences, was easier then manipulating the evaluations and then applying the lemma **) 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: - eval_exp 0%R E1 (toRExp e1) e1R -> - eval_exp (Q2R machineEpsilon) E2 (toRExp e1) e1F -> - eval_exp 0%R E1 (toRExp e2) e2R -> - eval_exp (Q2R machineEpsilon) E2 (toRExp e2) e2F -> - eval_exp 0%R E1 (Binop Sub (toRExp e1) (toRExp e2)) vR -> - eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (Binop Sub (Var R 1) (Var R 2)) vF -> + (e2F:R) (vR:R) (vF:R) (E1 E2:env) err1 err2 (m m1 m2:mType): + eval_exp E1 (toREval (toRExp e1)) e1R M0 -> + eval_exp E2 (toRExp e1) e1F m1 -> + eval_exp E1 (toREval (toRExp e2)) e2R M0 -> + eval_exp E2 (toRExp e2) e2F m2 -> + eval_exp E1 (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR M0 -> + eval_exp (updEnv 2 m2 e2F (updEnv 1 m1 e1F emptyEnv)) (Binop Sub (Var R m1 1) (Var R m2 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 machineEpsilon)))%R. + (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + ((Rabs (e1F - e2F)) * (Q2R (meps 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 *) - inversion sub_real; subst. + inversion sub_real; subst; + destruct m0; destruct m3; inversion H2; + simpl in H3; rewrite Q2R0_is_0 in H3; auto. rewrite delta_0_deterministic in sub_real; auto. rewrite delta_0_deterministic; auto. unfold evalBinop in *; simpl in *. - clear delta H2. - rewrite (meps_0_deterministic H3 e1_real); - rewrite (meps_0_deterministic H5 e2_real). - rewrite (meps_0_deterministic H3 e1_real) in sub_real. - rewrite (meps_0_deterministic H5 e2_real) in sub_real. - clear H3 H5 H6 v1 v2. + clear delta H3. + rewrite (meps_0_deterministic (toRExp e1) H5 e1_real); + rewrite (meps_0_deterministic (toRExp e2) H6 e2_real). + rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in sub_real. + rewrite (meps_0_deterministic (toRExp e2) H6 e2_real) in sub_real. + clear H5 H6 H7 v1 v2. (* Now unfold the float valued evaluation to get the deltas we need for the inequality *) inversion sub_float; subst. unfold perturb; simpl. - inversion H3; subst; inversion H5; subst. + inversion H4; subst; inversion H7; subst. unfold updEnv; simpl. - symmetry in H0, H1. - unfold updEnv in H0, H1; simpl in H0, H1. - inversion H0; inversion H1; subst. + symmetry in H6, H9. + unfold updEnv in H6, H9; simpl in H6, H9. + inversion H6; inversion H9; subst. (* We have now obtained all necessary values from the evaluations --> remove them for readability *) - clear sub_float H3 H5 sub_real e1_real e1_float e2_real e2_float H0 H1. + clear sub_float H4 H7 sub_real e1_real e1_float e2_real e2_float H6 H9 H8. repeat rewrite Rmult_plus_distr_l. rewrite Rmult_1_r. repeat rewrite Rsub_eq_Ropp_Rplus. @@ -161,36 +168,37 @@ Proof. 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): - eval_exp 0%R E1 (toRExp e1) e1R -> - eval_exp (Q2R machineEpsilon) E2 (toRExp e1) e1F -> - eval_exp 0%R E1 (toRExp e2) e2R -> - eval_exp (Q2R machineEpsilon) E2 (toRExp e2) e2F -> - eval_exp 0%R E1 (Binop Mult (toRExp e1) (toRExp e2)) vR -> - eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (Binop Mult (Var R 1) (Var R 2)) vF -> - (Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R machineEpsilon))%R. + (vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType): + eval_exp E1 (toREval (toRExp e1)) e1R M0 -> + eval_exp E2 (toRExp e1) e1F m1 -> + eval_exp E1 (toREval (toRExp e2)) e2R M0 -> + eval_exp E2 (toRExp e2) e2F m2 -> + eval_exp E1 (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR M0 -> + eval_exp (updEnv 2 m2 e2F (updEnv 1 m1 e1F emptyEnv)) (Binop Mult (Var R m1 1) (Var R m2 2)) vF m-> + (Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R (meps 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 *) - inversion mult_real; subst. + inversion mult_real; subst; + destruct m0; destruct m3; inversion H2; + simpl in H3; rewrite Q2R0_is_0 in H3; auto. rewrite delta_0_deterministic in mult_real; auto. rewrite delta_0_deterministic; auto. unfold evalBinop in *; simpl in *. - clear delta H2. - rewrite (meps_0_deterministic H3 e1_real); - rewrite (meps_0_deterministic H5 e2_real). - rewrite (meps_0_deterministic H3 e1_real) in mult_real. - rewrite (meps_0_deterministic H5 e2_real) in mult_real. - clear H3 H5 H6 v1 v2. + clear delta H3. + rewrite (meps_0_deterministic (toRExp e1) H5 e1_real); + rewrite (meps_0_deterministic (toRExp e2) H6 e2_real). + rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in mult_real. + rewrite (meps_0_deterministic (toRExp e2) H6 e2_real) in mult_real. + clear H5 H6 v1 v2 H7 H2. (* Now unfold the float valued evaluation to get the deltas we need for the inequality *) inversion mult_float; subst. unfold perturb; simpl. - inversion H3; subst; inversion H5; subst. - symmetry in H0, H1; + inversion H3; subst; inversion H6; subst. unfold updEnv in *; simpl in *. - inversion H0; inversion H1; subst. + inversion H5; inversion H8; subst. (* We have now obtained all necessary values from the evaluations --> remove them for readability *) - clear mult_float H3 H5 mult_real e1_real e1_float e2_real e2_float H0 H1. + clear mult_float H7 H8 mult_real e1_real e1_float e2_real e2_float H5 H8. repeat rewrite Rmult_plus_distr_l. rewrite Rmult_1_r. rewrite Rsub_eq_Ropp_Rplus. @@ -208,36 +216,37 @@ Proof. 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): - eval_exp 0%R E1 (toRExp e1) e1R -> - eval_exp (Q2R machineEpsilon) E2 (toRExp e1) e1F -> - eval_exp 0%R E1 (toRExp e2) e2R -> - eval_exp (Q2R machineEpsilon) E2 (toRExp e2) e2F -> - eval_exp 0%R E1 (Binop Div (toRExp e1) (toRExp e2)) vR -> - eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (Binop Div (Var R 1) (Var R 2)) vF -> - (Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R machineEpsilon))%R. + (vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType): + eval_exp E1 (toREval (toRExp e1)) e1R M0 -> + eval_exp E2 (toRExp e1) e1F m1 -> + eval_exp E1 (toREval (toRExp e2)) e2R M0 -> + eval_exp E2 (toRExp e2) e2F m2 -> + eval_exp E1 (toREval (Binop Div (toRExp e1) (toRExp e2))) vR M0 -> + eval_exp (updEnv 2 m2 e2F (updEnv 1 m1 e1F emptyEnv)) (Binop Div (Var R m1 1) (Var R m2 2)) vF m -> + (Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R (meps 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 *) - inversion div_real; subst. + inversion div_real; subst; + destruct m0; destruct m3; inversion H2; + simpl in H3; rewrite Q2R0_is_0 in H3; auto. rewrite delta_0_deterministic in div_real; auto. rewrite delta_0_deterministic; auto. unfold evalBinop in *; simpl in *. - clear delta H2. - rewrite (meps_0_deterministic H3 e1_real); - rewrite (meps_0_deterministic H5 e2_real). - rewrite (meps_0_deterministic H3 e1_real) in div_real. - rewrite (meps_0_deterministic H5 e2_real) in div_real. - clear H3 H5 H6 v1 v2. + clear delta H3 H2. + rewrite (meps_0_deterministic (toRExp e1) H5 e1_real); + rewrite (meps_0_deterministic (toRExp e2) H6 e2_real). + rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in div_real. + rewrite (meps_0_deterministic (toRExp e2) H6 e2_real) in div_real. + (* clear H5 H6 v1 v2. *) (* Now unfold the float valued evaluation to get the deltas we need for the inequality *) inversion div_float; subst. unfold perturb; simpl. - inversion H3; subst; inversion H5; subst. - symmetry in H0, H1; + inversion H3; subst; inversion H9; subst. unfold updEnv in *; simpl in *. - inversion H0; inversion H1; subst. + inversion H8; inversion H11; subst. (* We have now obtained all necessary values from the evaluations --> remove them for readability *) - clear div_float H3 H5 div_real e1_real e1_float e2_real e2_float H0 H1. + clear div_float H8 H11 div_real e1_real e1_float e2_real e2_float. repeat rewrite Rmult_plus_distr_l. rewrite Rmult_1_r. rewrite Rsub_eq_Ropp_Rplus. @@ -431,3 +440,29 @@ Proof. auto. rewrite Q2R0_is_0; auto. Qed. + +Lemma round_abs_err_bounded (e:exp R) (nR nF1 nF:R) (E1 E2: env) (err:R) (machineEpsilon m:mType): + eval_exp E1 (toREval e) nR M0 -> + eval_exp E2 e nF1 m -> + eval_exp (updEnv 1 m nF1 emptyEnv) (toRExp (Downcast machineEpsilon (Var Q m 1))) nF machineEpsilon-> + (Rabs (nR - nF1) <= err)%R -> + (Rabs (nR - nF) <= err + (Rabs nF1) * Q2R (meps 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. + eapply Rle_trans. + apply (Rabs_triang (nR - nF1) (nF1 - nF)). + apply (Rle_trans _ (err + Rabs (nF1 - nF)) _). + - apply Rplus_le_compat_r; assumption. + - apply Rplus_le_compat_l. + inversion eval_float_rnd; subst. + inversion H5; subst. + inversion H7. + unfold perturb; simpl. + replace (v1 - v1 * (1 + delta))%R with (- (v1 * delta))%R by lra. + replace (Rabs (-(v1*delta))) with (Rabs (v1*delta)) by (symmetry; apply Rabs_Ropp). + rewrite Rabs_mult. + apply Rmult_le_compat_l. + + apply Rabs_pos. + + auto. +Qed. diff --git a/coq/ErrorValidation.v b/coq/ErrorValidation.v index b2aa09101a0c200b461042dfaf2c91fcccde3b9a..f0aac13657462f1e24cfd6fb1ea325592669024e 100644 --- a/coq/ErrorValidation.v +++ b/coq/ErrorValidation.v @@ -9,63 +9,70 @@ Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals Coq.Lists.List. 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.ErrorBounds. +Require Import Daisy.Environments Daisy.IntervalValidation Daisy.Typing Daisy.ErrorBounds. (** Error bound validator **) -Fixpoint validErrorbound (e:exp Q) (absenv:analysisResult) (dVars:NatSet.t):= +Fixpoint validErrorbound (e:exp Q) (typeMap:exp Q -> option mType) (absenv:analysisResult) (dVars:NatSet.t):= let (intv, err) := (absenv e) in - if (Qleb 0 err) - then - match e with - |Var _ v => - if (NatSet.mem v dVars) - then true - else (Qleb (maxAbs intv * RationalSimps.machineEpsilon) err) - |Const n => - Qleb (maxAbs intv * RationalSimps.machineEpsilon) err - |Unop Neg e => - if (validErrorbound e absenv dVars) - then Qeq_bool err (snd (absenv e)) - else false - |Unop Inv e => false - |Binop b e1 e2 => - if ((validErrorbound e1 absenv dVars) && (validErrorbound e2 absenv dVars)) - then - let (ive1, err1) := absenv e1 in - let (ive2, err2) := absenv e2 in - let errIve1 := widenIntv ive1 err1 in - let errIve2 := widenIntv ive2 err2 in - let upperBoundE1 := maxAbs ive1 in - let upperBoundE2 := maxAbs ive2 in - match b with - | Plus => - Qleb (err1 + err2 + (maxAbs (addIntv errIve1 errIve2)) * machineEpsilon) err - | Sub => - Qleb (err1 + err2 + (maxAbs (subtractIntv errIve1 errIve2)) * machineEpsilon) err - | Mult => - Qleb ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbs (multIntv errIve1 errIve2)) * machineEpsilon) err - | Div => - if (((Qleb (ivhi errIve2) 0) && (negb (Qeq_bool (ivhi errIve2) 0))) || - ((Qleb 0 (ivlo errIve2)) && (negb (Qeq_bool (ivlo errIve2) 0)))) - then - 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)) * machineEpsilon) err - else false - end - else false - end - else false. + let mopt := typeMap e in + match mopt with + | None => false + | Some m => + if (Qleb 0 err) + then + match e with + |Var _ _ v => + if (NatSet.mem v dVars) + then true + else (Qleb (maxAbs intv * (meps m)) err) + |Const _ n => + Qleb (maxAbs intv * (meps m)) err + |Unop _ _ => false + |Binop b e1 e2 => + if ((validErrorbound e1 typeMap absenv dVars) && (validErrorbound e2 typeMap absenv dVars)) + then + let (ive1, err1) := absenv e1 in + let (ive2, err2) := absenv e2 in + let errIve1 := widenIntv ive1 err1 in + let errIve2 := widenIntv ive2 err2 in + let upperBoundE1 := maxAbs ive1 in + let upperBoundE2 := maxAbs ive2 in + match b with + | Plus => + Qleb (err1 + err2 + (maxAbs (addIntv errIve1 errIve2)) * (meps m)) err + | Sub => + Qleb (err1 + err2 + (maxAbs (subtractIntv errIve1 errIve2)) * (meps m)) err + | Mult => + Qleb ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbs (multIntv errIve1 errIve2)) * (meps m)) err + | Div => + if (((Qleb (ivhi errIve2) 0) && (negb (Qeq_bool (ivhi errIve2) 0))) || + ((Qleb 0 (ivlo errIve2)) && (negb (Qeq_bool (ivlo errIve2) 0)))) + then + 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 + 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) + end + else false + end. + (** Error bound command validator **) -Fixpoint validErrorboundCmd (f:cmd Q) (env:analysisResult) (dVars:NatSet.t) {struct f} : bool := +Fixpoint validErrorboundCmd (f:cmd Q) (typeMap:exp Q -> option mType) (env:analysisResult) (dVars:NatSet.t) {struct f} : bool := match f with - |Let x e g => - if ((validErrorbound e env dVars) && (Qeq_bool (snd (env e)) (snd (env (Var Q x))))) - then validErrorboundCmd g env (NatSet.add x dVars) + |Let m x e g => + if ((validErrorbound e typeMap env dVars) && (Qeq_bool (snd (env e)) (snd (env (Var Q m x))))) + then validErrorboundCmd g typeMap env (NatSet.add x dVars) else false - |Ret e => validErrorbound e env dVars + |Ret e => validErrorbound e typeMap env dVars end. (** @@ -73,48 +80,70 @@ Fixpoint validErrorboundCmd (f:cmd Q) (env:analysisResult) (dVars:NatSet.t) {str This lemma enables us to deduce from each run of the validator the invariant that when it succeeds, the errors must be positive. **) -Lemma err_always_positive e (absenv:analysisResult) iv err dVars: - validErrorbound e absenv dVars = true -> +Lemma err_always_positive e tmap (absenv:analysisResult) iv err dVars: + validErrorbound e tmap absenv dVars = true -> (iv,err) = absenv e -> (0 <= Q2R err)%R. Proof. - destruct e;intros validErrorbound_e absenv_e; + destruct e; intros validErrorbound_e absenv_e; unfold validErrorbound in validErrorbound_e; - rewrite <- absenv_e in validErrorbound_e; simpl in *; - andb_to_prop validErrorbound_e. - - apply Qle_bool_iff in L; apply Qle_Rle in L; rewrite Q2R0_is_0 in L; auto. - - apply Qle_bool_iff in L; apply Qle_Rle in L; rewrite Q2R0_is_0 in L; auto. - - destruct u; simpl in *; try congruence. - andb_to_prop R. - apply Qle_bool_iff in L; apply Qle_Rle in L; rewrite Q2R0_is_0 in L; auto. - - apply Qle_bool_iff in L; apply Qle_Rle in L; rewrite Q2R0_is_0 in L; auto. + rewrite <- absenv_e in validErrorbound_e; simpl in *. + - case_eq (Qleb 0 err); intros; auto; rewrite H in validErrorbound_e. + + apply Qle_bool_iff,Qle_Rle in H; rewrite Q2R0_is_0 in H; auto. + + destruct (tmap (Var Q m n)); inversion validErrorbound_e. + - case_eq (Qleb 0 err); intros; auto; rewrite H in validErrorbound_e. + + apply Qle_bool_iff,Qle_Rle in H; rewrite Q2R0_is_0 in H; auto. + + destruct (tmap (Const m q)); inversion validErrorbound_e. + - case_eq (Qleb 0 err); intros; auto; rewrite H in validErrorbound_e. + + apply Qle_bool_iff,Qle_Rle in H; rewrite Q2R0_is_0 in H; auto. + + destruct (tmap (Unop u e)); inversion validErrorbound_e. + - case_eq (Qleb 0 err); intros; auto; rewrite H in validErrorbound_e. + + apply Qle_bool_iff, Qle_Rle in H; rewrite Q2R0_is_0 in H; auto. + + destruct (tmap (Binop b e1 e2));inversion validErrorbound_e. + - case_eq (Qleb 0 err); intros; auto; rewrite H in validErrorbound_e. + + apply Qle_bool_iff, Qle_Rle in H; rewrite Q2R0_is_0 in H; auto. + + destruct (tmap (Downcast m e));inversion validErrorbound_e. Qed. + Lemma validErrorboundCorrectVariable: - forall E1 E2 absenv (v:nat) nR nF e nlo nhi P fVars dVars, + forall E1 E2 absenv (v:nat) nR nF e nlo nhi P fVars dVars m Gamma, + validType Gamma (Var Q m v) m -> approxEnv E1 absenv fVars dVars E2 -> - eval_exp 0%R E1 (toRExp (Var Q v)) nR -> - eval_exp (Q2R machineEpsilon) E2 (toRExp (Var Q v)) nF -> - validIntervalbounds (Var Q v) absenv P dVars = true -> - validErrorbound (Var Q v) absenv dVars = true -> - (forall v, - NatSet.mem v dVars = true -> - exists r : R, - E1 v = Some r /\ - (Q2R (fst (fst (absenv (Var Q v)))) <= r <= Q2R (snd (fst (absenv (Var Q v)))))%R) -> - (forall v, NatSet.mem v fVars= true -> - exists r, E1 v = Some r /\ - (Q2R (fst (P v)) <= r <= Q2R (snd (P v)))%R) -> - absenv (Var Q v) = ((nlo, nhi), e) -> + eval_exp E1 (toREval (toRExp (Var Q m v))) nR M0 -> + eval_exp E2 (toRExp (Var Q m v)) nF m -> + validIntervalbounds (Var Q m v) absenv P dVars = true -> + validErrorbound (Var Q m v) Gamma absenv dVars = true -> + (forall v1 m1, + NatSet.mem v1 dVars = true -> + exists r mv1, + E1 v1 = Some (r, M0) /\ Gamma (Var Q mv1 v1) = Some m1 /\ + (Q2R (fst (fst (absenv (Var Q m1 v1)))) <= r <= Q2R (snd (fst (absenv (Var Q m1 v1)))))%R) -> + (forall v1, NatSet.mem v1 fVars= true -> + exists r, E1 v1 = Some (r, M0) /\ + (Q2R (fst (P v1)) <= r <= Q2R (snd (P v1)))%R) -> + absenv (Var Q m v) = ((nlo, nhi), e) -> (Rabs (nR - nF) <= (Q2R e))%R. Proof. - intros E1 E2 absenv v nR nF e nlo nhi P fVars dVars approxCEnv eval_real - eval_float bounds_valid error_valid dVars_sound P_valid absenv_var. - inversion eval_real; inversion eval_float; subst. - rename H0 into E1_v; - rename H3 into E2_v. + 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 H2 into E1_v; + rename H7 into E2_v. + (* assert ((typeExpression (Var Q m v)) (Var Q m v) = Some m) as tEv. *) + (* unfold typeExpression. unfold expEqBool. *) + (* case_eq (mTypeEqBool m m && (v =? v)); intros; auto. *) + (* apply andb_false_iff in H. destruct H. assert (mTypeEqBool m m = true) by (apply EquivEqBoolEq; auto). *) + (* congruence. *) + (* assert (v =? v = true) by (apply beq_nat_true_iff; auto). *) + (* congruence. *) simpl in error_valid. - rewrite absenv_var in error_valid; simpl in error_valid. + rewrite absenv_var in error_valid; simpl in error_valid; subst. + case_eq (Gamma (Var Q m v)); intros; rewrite H in error_valid; [ | inversion error_valid]. + + (* assert (mTypeEqBool m m && (v =? v) = true). *) + (* apply andb_true_iff; split; [ rewrite EquivEqBoolEq | apply beq_nat_true_iff ]; auto. *) + + (* rewrite H in error_valid. *) rewrite <- andb_lazy_alt in error_valid. andb_to_prop error_valid. rename L into error_pos. @@ -137,41 +166,45 @@ Proof. rewrite x_in_union in *. congruence. * rewrite x_not_bound in error_valid. - inversion E1_v; inversion E2_v; - subst. + 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. + inversion typing_ok; subst. + rewrite H in H5; inversion H5; subst. + clear H5 H3. apply Rmult_le_compat_r. - { apply mEps_geq_zero. } + { apply inj_eps_posR. } { rewrite <- maxAbs_impl_RmaxAbs. apply contained_leq_maxAbs. unfold contained; simpl. - pose proof (validIntervalbounds_sound (Var Q x) A P (E:=fun y : nat => if y =? x then Some nR else E1 y) (vR:=nR) bounds_valid (fVars := (NatSet.add x fVars))) as valid_bounds_prf. + assert ((toRExp (Var Q m x)) = Var R m x) by (simpl; auto). + rewrite <- H2 in eval_float. + pose proof (validIntervalbounds_sound A P (E:=fun y : nat => if y =? x then Some (nR, M0) else E1 y) (vR:=nR) typing_ok 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. } + - 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 [val_def iv_sound_val]]. + * intros v0 m2 (*overVar*) mem_dVars (*isSubExpr*). + specialize (dVars_sound v0 m2 (*overVar*) mem_dVars (*isSubExpr*)). + destruct dVars_sound as [vR0 [mR0 iv_sound_val]]. case_eq (v0 =? x); intros case_mem; - rewrite case_mem in val_def; simpl in val_def. + 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. } + { exists vR0, mR0; 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). @@ -217,14 +250,16 @@ Proof. + 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. + * intros v0 m2 (*overVar*) mem_dVars (*isSubExpr*). + specialize (dVars_sound v0 m2 (*overVar*)). 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 v0_in_add). - destruct dVars_sound as [vR0 [val_def iv_sound_val]]. + specialize (dVars_sound v0_in_add). + destruct dVars_sound as [vR0 [mR0 [val_def iv_sound_val]]]. + exists vR0, mR0; 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. @@ -232,7 +267,7 @@ Proof. apply (NatSetProps.Dec.F.union_3 fVars) in mem_dVars. rewrite <- NatSet.mem_spec in mem_dVars. rewrite mem_dVars in *; congruence. - - exists vR0; split; auto. } + - auto. } * rewrite absenv_var in bounds_valid. intros v0 v0_fVar. specialize (P_valid v0 v0_fVar). @@ -246,106 +281,52 @@ Proof. Qed. Lemma validErrorboundCorrectConstant: - forall E1 E2 absenv (n:Q) nR nF e nlo nhi dVars, - eval_exp 0%R E1 (Const (Q2R n)) nR -> - eval_exp (Q2R (RationalSimps.machineEpsilon)) E2 (Const (Q2R n)) nF -> - validErrorbound (Const n) absenv dVars = true -> + forall E1 E2 absenv (n:Q) nR nF e nlo nhi dVars m Gamma, + eval_exp E1 (toREval (toRExp (Const m n))) nR M0 -> + eval_exp E2 (toRExp (Const m n)) nF m -> + validType Gamma (Const m n) m -> + validErrorbound (Const m n) Gamma absenv dVars = true -> (Q2R nlo <= nR <= Q2R nhi)%R -> - absenv (Const n) = ((nlo,nhi),e) -> + absenv (Const m n) = ((nlo,nhi),e) -> (Rabs (nR - nF) <= (Q2R e))%R. Proof. - intros E1 E2 absenv n nR nF e nlo nhi dVars - eval_real eval_float error_valid intv_valid absenv_const. + intros * eval_real eval_float subexpr_ok error_valid intv_valid absenv_const. 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 ]. 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. 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_geq_zero. + apply inj_eps_posR. apply RmaxAbs; eauto. - rewrite Q2R_mult in error_valid. rewrite <- maxAbs_impl_RmaxAbs in error_valid; auto. + inversion subexpr_ok; subst. + rewrite H in H6; inversion H6; subst; auto. Qed. -(* -Lemma validErrorboundCorrectParam: - forall E1 E2 absenv (v:nat) nR nF e P plo phi, - eval_exp 0%R E1 P (toRExp (Param Q v)) nR -> - eval_exp (Q2R RationalSimps.machineEpsilon) E2 P (toRExp (Param Q v)) nF -> - validErrorbound (Param Q v) absenv = true -> - (Q2R plo <= nR <= Q2R phi)%R -> - (forall n : nat, NatSet.In n (Expressions.freeVars (Param Q v)) -> - Is_true (isSupersetIntv (P n) (fst (absenv (Param Q n))))) -> - absenv (Param Q v) = ((plo,phi),e) -> - (Rabs (nR - nF) <= (Q2R e))%R. -Proof. - intros E1 E2 absenv v nR nF e P plo phi - eval_real eval_float error_valid intv_valid absenv_approx_p absenv_param. - inversion eval_real; subst. - rewrite delta_0_deterministic in *; auto. - unfold validErrorbound in error_valid. - rewrite absenv_param in error_valid. - specialize (absenv_approx_p v). - assert (exists ivlo ivhi, (ivlo,ivhi) = P v) by (destruct (P v) as [ivlo ivhi]; repeat eexists). - destruct H as [ivlo [ivhi P_eq]]. - rewrite <- P_eq in absenv_approx_p, H4. - rewrite absenv_param in absenv_approx_p. - unfold freeVars in absenv_approx_p; simpl in absenv_approx_p. - assert (v = v \/ False) by auto. - specialize (absenv_approx_p H). - unfold isSupersetIntv in absenv_approx_p. - apply andb_prop_elim in absenv_approx_p. - destruct absenv_approx_p as [plo_le_ivlo ivhi_le_phi]. - apply Is_true_eq_true, Qle_bool_iff in plo_le_ivlo. - apply Is_true_eq_true, Qle_bool_iff in ivhi_le_phi. - simpl in H4; destruct H4. - apply Qle_Rle in plo_le_ivlo; apply Qle_Rle in ivhi_le_phi. - andb_to_prop error_valid. - rename R into error_valid. - apply Qle_bool_iff in error_valid. - apply Qle_Rle in error_valid. - rewrite Q2R_mult in error_valid. - eapply Rle_trans;[ | apply error_valid]. - simpl in *. - inversion eval_float; subst. - unfold perturb; simpl. - assert (Q2R plo <= v0)%R as lower_bound_v0 by lra. - assert (v0 <= Q2R phi)%R as upper_bound_v0 by lra. - rewrite Rsub_eq_Ropp_Rplus. - eapply Rle_trans. - apply Rabs_triang. - eapply Rle_trans. - apply Rplus_le_compat. - apply RmaxAbs. - apply lower_bound_v0. - apply upper_bound_v0. - rewrite Rmult_plus_distr_l. - rewrite Rmult_1_r. - apply Rmult_le_compat_r;try (apply Rabs_pos). - apply mEps_geq_zero. - rewrite <- maxAbs_impl_RmaxAbs. - destruct intv_valid. - eapply RmaxAbs; 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: - eval_exp 0%R E1 (toRExp e1) nR1 -> - eval_exp 0%R E1 (toRExp e2) nR2 -> - eval_exp 0%R E1 (toRExp (Binop Plus e1 e2)) nR -> - eval_exp (Q2R RationalSimps.machineEpsilon) E2 (toRExp e1) nF1 -> - eval_exp (Q2R RationalSimps.machineEpsilon) E2 (toRExp e2) nF2 -> - eval_exp (Q2R RationalSimps.machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) (toRExp (Binop Plus (Var Q 1) (Var Q 2))) nF -> - validErrorbound (Binop Plus e1 e2) absenv dVars = true -> + (alo ahi e1lo e1hi e2lo e2hi:Q) dVars m m1 m2 Gamma: + m = computeJoin m1 m2 -> + eval_exp E1 (toREval (toRExp e1)) nR1 M0 -> + eval_exp E1 (toREval (toRExp e2)) nR2 M0 -> + eval_exp E1 (toREval (toRExp (Binop Plus e1 e2))) nR M0 -> + eval_exp E2 (toRExp e1) nF1 m1 -> + eval_exp E2 (toRExp e2) nF2 m2 -> + eval_exp (updEnv 2 m2 nF2 (updEnv 1 m1 nF1 emptyEnv)) (toRExp (Binop Plus (Var Q m1 1) (Var Q m2 2))) nF m -> + validType Gamma (Binop Plus e1 e2) m -> + validErrorbound (Binop Plus e1 e2) Gamma absenv dVars = true -> (Q2R e1lo <= nR1 <= Q2R e1hi)%R -> (Q2R e2lo <= nR2 <= Q2R e2hi)%R -> absenv e1 = ((e1lo,e1hi),err1) -> @@ -355,21 +336,29 @@ Lemma validErrorboundCorrectAddition E1 E2 absenv (Rabs (nR2 - nF2) <= (Q2R err2))%R -> (Rabs (nR - nF) <= (Q2R e))%R. Proof. - intros e1_real e2_real eval_real e1_float e2_float eval_float - valid_error valid_intv1 valid_intv2 absenv_e1 absenv_e2 absenv_add + intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float + subexpr_ok valid_error valid_intv1 valid_intv2 absenv_e1 absenv_e2 absenv_add err1_bounded err2_bounded. eapply Rle_trans. eapply (add_abs_err_bounded e1 e2); try eauto. - unfold validErrorbound in valid_error at 1. - rewrite absenv_add, absenv_e1, absenv_e2 in valid_error. + unfold validErrorbound in valid_error. + rewrite absenv_add,absenv_e1,absenv_e2 in valid_error. + (* assert (typeExpression (Binop Plus e1 e2) (Binop Plus e1 e2) = Some m) as type_add. *) + (* { simpl typeExpression; repeat rewrite expEqBool_refl; simpl. *) + (* pose proof (typeExpressionIsSound _ e1_float) as type_e1. *) + (* pose proof (typeExpressionIsSound _ e2_float) as type_e2. *) + (* rewrite type_e1,type_e2. *) + (* rewrite mIsJoin; auto. } *) + case_eq (Gamma (Binop Plus e1 e2)); intros; rewrite H in valid_error; [ | inversion valid_error ]. + inversion subexpr_ok; subst. rewrite H in H7; inversion H7; subst. clear m4 m5 H3 H4 H7 H6. andb_to_prop valid_error. rename R0 into valid_error. eapply Rle_trans. apply Rplus_le_compat_l. eapply Rmult_le_compat_r. - apply mEps_geq_zero. + apply inj_eps_posR. Focus 2. rewrite Qle_bool_iff in valid_error. apply Qle_Rle in valid_error. @@ -388,14 +377,14 @@ Proof. rewrite <- maxAbs_impl_RmaxAbs. assert (ivlo iv = ivl) by (rewrite iv_unf; auto). assert (ivhi iv = ivh) by (rewrite iv_unf; auto). - rewrite <- H, <- H0. + 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). 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 H1 H2). - unfold IntervalArith.contained in H3. - destruct H3. + pose proof (IntervalArith.interval_addition_valid H2 H3). + unfold IntervalArith.contained in H4. + destruct H4. subst; simpl in *. apply RmaxAbs; simpl. - rewrite Q2R_min4. @@ -408,14 +397,16 @@ 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: - eval_exp 0%R E1 (toRExp e1) nR1 -> - eval_exp 0%R E1 (toRExp e2) nR2 -> - eval_exp 0%R E1 (toRExp (Binop Sub e1 e2)) nR -> - eval_exp (Q2R RationalSimps.machineEpsilon) E2 (toRExp e1) nF1 -> - eval_exp (Q2R RationalSimps.machineEpsilon) E2 (toRExp e2) nF2 -> - eval_exp (Q2R RationalSimps.machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) (toRExp (Binop Sub (Var Q 1) (Var Q 2))) nF -> - validErrorbound (Binop Sub e1 e2) absenv dVars = true -> + (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma: + m = computeJoin m1 m2 -> + eval_exp E1 (toREval (toRExp e1)) nR1 M0 -> + eval_exp E1 (toREval (toRExp e2)) nR2 M0 -> + eval_exp E1 (toREval (toRExp (Binop Sub e1 e2))) nR M0 -> + eval_exp E2 (toRExp e1) nF1 m1-> + eval_exp E2 (toRExp e2) nF2 m2 -> + eval_exp (updEnv 2 m2 nF2 (updEnv 1 m1 nF1 emptyEnv)) (toRExp (Binop Sub (Var Q m1 1) (Var Q m2 2))) nF m -> + validType Gamma (Binop Sub e1 e2) m -> + validErrorbound (Binop Sub e1 e2) Gamma absenv dVars = true -> (Q2R e1lo <= nR1 <= Q2R e1hi)%R -> (Q2R e2lo <= nR2 <= Q2R e2hi)%R -> absenv e1 = ((e1lo,e1hi),err1) -> @@ -425,21 +416,15 @@ Lemma validErrorboundCorrectSubtraction E1 E2 absenv (Rabs (nR2 - nF2) <= (Q2R err2))%R -> (Rabs (nR - nF) <= (Q2R e))%R. Proof. - intros e1_real e2_real eval_real e1_float e2_float eval_float - valid_error valid_intv1 valid_intv2 absenv_e1 absenv_e2 absenv_sub + intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float + subexpr_ok valid_error valid_intv1 valid_intv2 absenv_e1 absenv_e2 absenv_sub err1_bounded err2_bounded. eapply Rle_trans. - eapply subtract_abs_err_bounded. - apply e1_real. - apply e1_float. - apply e2_real. - apply e2_float. - apply eval_real. - apply eval_float. - apply err1_bounded. - apply err2_bounded. - unfold validErrorbound in valid_error at 1. - rewrite absenv_sub, absenv_e1, absenv_e2 in valid_error. + eapply (subtract_abs_err_bounded e1 e2); try eauto. + unfold validErrorbound in valid_error. + rewrite absenv_sub,absenv_e1,absenv_e2 in valid_error. + case_eq (Gamma (Binop Sub e1 e2)); intros; rewrite H in valid_error; [ | inversion valid_error ]. + inversion subexpr_ok; subst. rewrite H in H7; inversion H7; subst. clear m4 m5 H3 H4 H7 H6. andb_to_prop valid_error. rename R0 into valid_error. apply Qle_bool_iff in valid_error. @@ -453,7 +438,7 @@ Proof. eapply Rle_trans. apply Rplus_le_compat_l. eapply Rmult_le_compat_r. - apply mEps_geq_zero. + apply inj_eps_posR. Focus 2. apply valid_error. remember (subtractIntv (widenIntv (e1lo, e1hi) err1) (widenIntv (e2lo, e2hi) err2)) as iv. @@ -463,14 +448,14 @@ Proof. rewrite <- maxAbs_impl_RmaxAbs. assert (ivlo iv = ivl) by (rewrite iv_unf; auto). assert (ivhi iv = ivh) by (rewrite iv_unf; auto). - rewrite <- H, <- H0. + 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). 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 H1 H2). - unfold IntervalArith.contained in H3. - destruct H3. + pose proof (IntervalArith.interval_subtraction_valid H2 H3). + unfold IntervalArith.contained in H4. + destruct H4. subst; simpl in *. apply RmaxAbs; simpl. - rewrite Q2R_min4. @@ -489,14 +474,16 @@ 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: - eval_exp 0%R E1 (toRExp e1) nR1 -> - eval_exp 0%R E1 (toRExp e2) nR2 -> - eval_exp 0%R E1 (toRExp (Binop Mult e1 e2)) nR -> - eval_exp (Q2R RationalSimps.machineEpsilon) E2 (toRExp e1) nF1 -> - eval_exp (Q2R RationalSimps.machineEpsilon) E2 (toRExp e2) nF2 -> - eval_exp (Q2R RationalSimps.machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) (toRExp (Binop Mult (Var Q 1) (Var Q 2))) nF -> - validErrorbound (Binop Mult e1 e2) absenv dVars = true -> + (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma: + m = computeJoin m1 m2 -> + eval_exp E1 (toREval (toRExp e1)) nR1 M0 -> + eval_exp E1 (toREval (toRExp e2)) nR2 M0 -> + eval_exp E1 (toREval (toRExp (Binop Mult e1 e2))) nR M0 -> + eval_exp E2 (toRExp e1) nF1 m1 -> + eval_exp E2 (toRExp e2) nF2 m2 -> + eval_exp (updEnv 2 m2 nF2 (updEnv 1 m1 nF1 emptyEnv)) (toRExp (Binop Mult (Var Q m1 1) (Var Q m2 2))) nF m -> + validType Gamma (Binop Mult e1 e2) m -> + validErrorbound (Binop Mult e1 e2) Gamma absenv dVars = true -> (Q2R e1lo <= nR1 <= Q2R e1hi)%R -> (Q2R e2lo <= nR2 <= Q2R e2hi)%R -> absenv e1 = ((e1lo,e1hi),err1) -> @@ -506,17 +493,19 @@ Lemma validErrorboundCorrectMult E1 E2 absenv (Rabs (nR2 - nF2) <= (Q2R err2))%R -> (Rabs (nR - nF) <= (Q2R e))%R. Proof. - intros e1_real e2_real eval_real e1_float e2_float eval_float - valid_error valid_e1 valid_e2 absenv_e1 absenv_e2 absenv_mult + intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float + subexpr_ok valid_error valid_e1 valid_e2 absenv_e1 absenv_e2 absenv_mult err1_bounded err2_bounded. eapply Rle_trans. eapply (mult_abs_err_bounded e1 e2); eauto. - unfold validErrorbound in valid_error at 1. - rewrite absenv_mult, absenv_e1, absenv_e2 in valid_error. + unfold validErrorbound in valid_error. + rewrite absenv_mult,absenv_e1,absenv_e2 in valid_error. + case_eq (Gamma (Binop Mult e1 e2)); intros; rewrite H in valid_error; [ | inversion valid_error ]. + inversion subexpr_ok; subst. rewrite H in H7; inversion H7; subst. clear m4 m5 H3 H4 H7 H6. andb_to_prop valid_error. rename R0 into valid_error. - assert (0 <= Q2R err1)%R as err1_pos by (eapply (err_always_positive e1 absenv dVars); eauto). - assert (0 <= Q2R err2)%R as err2_pos by (eapply (err_always_positive e2 absenv dVars); eauto). + 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. apply Qle_bool_iff in valid_error. apply Qle_Rle in valid_error. @@ -581,19 +570,19 @@ Proof. eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_l; auto. - apply H0. + apply H1. destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. - apply H. + apply H0. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. hnf. left; auto. assert (nR1 <= nF1)%R by lra. - apply H1. + apply H2. lra. } { @@ -602,12 +591,12 @@ Proof. eapply Rmult_le_compat_neg_l. hnf. left; auto. assert (nR2 < nF2)%R by lra. - apply Rlt_le in H1; apply H1. + apply Rlt_le in H2; apply H2. destruct (Rle_lt_dec 0 nR2). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. - apply H. + apply H0. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. @@ -615,7 +604,7 @@ Proof. eapply Rmult_le_compat_neg_l. hnf. left; auto. assert (nR1 < nF1)%R by lra. - apply Rlt_le in H1; apply H1. + apply Rlt_le in H2; apply H2. lra. } * rewrite Rsub_eq_Ropp_Rplus. @@ -626,12 +615,12 @@ Proof. eapply Rplus_le_compat_l. eapply Rmult_le_compat_l; auto. assert (- nF2 <= - nR2)%R by lra. - apply H1. + apply H2. destruct (Rle_lt_dec 0 (- nR2)). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. - apply H. + apply H0. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. @@ -639,7 +628,7 @@ Proof. eapply Rmult_le_compat_neg_l. hnf. left; auto. assert (nR1 < nF1)%R by lra. - apply Rlt_le in H1; apply H1. + apply Rlt_le in H2; apply H2. lra. } { @@ -652,22 +641,22 @@ Proof. apply Rle_ge. rewrite Ropp_0. hnf. left; auto. - apply H0. + apply H1. destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. assert (- nF1 <= -nR1)%R by lra. - apply H1. + apply H2. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. hnf. left; auto. - apply Ropp_le_ge_contravar in H. - apply Rge_le in H. - apply H. + apply Ropp_le_ge_contravar in H0. + apply Rge_le in H0. + apply H0. lra. } + rewrite Rsub_eq_Ropp_Rplus in err1_bounded, err2_bounded. @@ -684,19 +673,19 @@ Proof. eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_l; auto. - apply H0. + apply H1. destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. - apply H. + apply H0. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. hnf. left; auto. assert (nR1 <= nF1)%R by lra. - apply H1. + apply H2. lra. } { @@ -705,15 +694,15 @@ Proof. eapply Rmult_le_compat_neg_l. hnf. left; auto. assert (- nF2 <= - (nR2 - Q2R err2))%R by lra. - apply Ropp_le_ge_contravar in H1. - repeat rewrite Ropp_involutive in H1. - apply Rge_le in H1. - apply H1. + apply Ropp_le_ge_contravar in H2. + repeat rewrite Ropp_involutive in H2. + apply Rge_le in H2. + apply H2. destruct (Rle_lt_dec 0 (nR2 - Q2R err2)). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. - apply H. + apply H0. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. @@ -721,7 +710,7 @@ Proof. eapply Rmult_le_compat_neg_l. hnf. left; auto. assert (nR1 < nF1)%R by lra. - apply Rlt_le in H1; apply H1. + apply Rlt_le in H2; apply H2. lra. } * rewrite Rsub_eq_Ropp_Rplus. @@ -732,12 +721,12 @@ Proof. eapply Rplus_le_compat_l. eapply Rmult_le_compat_l; auto. assert (- nF2 <= - nR2 + Q2R err2)%R by lra. - apply H1. + apply H2. destruct (Rle_lt_dec 0 (- nR2 + Q2R err2)). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. - apply H. + apply H0. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. @@ -745,7 +734,7 @@ Proof. eapply Rmult_le_compat_neg_l. hnf. left; auto. assert (nR1 < nF1)%R by lra. - apply Rlt_le in H1; apply H1. + apply Rlt_le in H2; apply H2. lra. } { @@ -758,22 +747,22 @@ Proof. apply Rle_ge. rewrite Ropp_0. hnf. left; auto. - apply H0. + apply H1. destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. assert (- nF1 <= -nR1)%R by lra. - apply H1. + apply H2. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. hnf. left; auto. - apply Ropp_le_ge_contravar in H. - apply Rge_le in H. - apply H. + apply Ropp_le_ge_contravar in H0. + apply Rge_le in H0. + apply H0. lra. } + rewrite Rsub_eq_Ropp_Rplus in err1_bounded, err2_bounded. @@ -790,22 +779,22 @@ Proof. eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_l; auto. - apply H0. + apply H1. destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. - apply H. + apply H0. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. hnf. left; auto. assert (- nF1 <= - (nR1 - Q2R err1))%R by lra. - apply Ropp_le_ge_contravar in H1. - repeat rewrite Ropp_involutive in H1. - apply Rge_le in H1. - apply H1. + apply Ropp_le_ge_contravar in H2. + repeat rewrite Ropp_involutive in H2. + apply Rge_le in H2. + apply H2. lra. } { @@ -814,12 +803,12 @@ Proof. eapply Rmult_le_compat_neg_l. hnf. left; auto. assert (nR2 < nF2)%R by lra. - apply Rlt_le in H1; apply H1. + apply Rlt_le in H2; apply H2. destruct (Rle_lt_dec 0 nR2). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. - apply H. + apply H0. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. @@ -827,10 +816,10 @@ Proof. eapply Rmult_le_compat_neg_l. hnf. left; auto. assert (- nF1 <= - (nR1 - Q2R err1))%R by lra. - apply Ropp_le_ge_contravar in H1. - repeat rewrite Ropp_involutive in H1. - apply Rge_le in H1. - apply H1. + apply Ropp_le_ge_contravar in H2. + repeat rewrite Ropp_involutive in H2. + apply Rge_le in H2. + apply H2. lra. } * rewrite Rsub_eq_Ropp_Rplus. @@ -841,12 +830,12 @@ Proof. eapply Rplus_le_compat_l. eapply Rmult_le_compat_l; auto. assert (- nF2 <= - nR2)%R by lra. - apply H1. + apply H2. destruct (Rle_lt_dec 0 (- nR2)). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. - apply H. + apply H0. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. @@ -854,10 +843,10 @@ Proof. eapply Rmult_le_compat_neg_l. hnf. left; auto. assert (- nF1 <= - (nR1 - Q2R err1))%R by lra. - apply Ropp_le_ge_contravar in H1. - repeat rewrite Ropp_involutive in H1. - apply Rge_le in H1. - apply H1. + apply Ropp_le_ge_contravar in H2. + repeat rewrite Ropp_involutive in H2. + apply Rge_le in H2. + apply H2. lra. } { @@ -866,21 +855,21 @@ Proof. eapply Rplus_le_compat_l. eapply Rmult_le_compat_l. lra. - apply H0. + apply H1. destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. assert (- nF1 <= - (nR1 - Q2R err1))%R by lra. - apply H1. + apply H2. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l; try lra. - apply Ropp_le_ge_contravar in H. - apply Rge_le in H. - apply H. + apply Ropp_le_ge_contravar in H0. + apply Rge_le in H0. + apply H0. lra. } (* All positive *) @@ -895,19 +884,19 @@ Proof. eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_l; auto. - apply H0. + apply H1. destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. - apply H. + apply H0. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. hnf. left; auto. assert (nR1 - Q2R err1 <= nF1)%R by lra. - apply H1. + apply H2. lra. } { @@ -916,12 +905,12 @@ Proof. eapply Rmult_le_compat_neg_l. hnf. left; auto. assert (nR2 - Q2R err2 <= nF2)%R by lra. - apply H1. + apply H2. destruct (Rle_lt_dec 0 (nR2 - Q2R err2)). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. - apply H. + apply H0. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. @@ -929,7 +918,7 @@ Proof. eapply Rmult_le_compat_neg_l. lra. assert (nR1 - Q2R err1 <= nF1)%R by lra. - apply H1. + apply H2. lra. } * rewrite Rsub_eq_Ropp_Rplus. @@ -940,12 +929,12 @@ Proof. eapply Rplus_le_compat_l. eapply Rmult_le_compat_l; auto. assert (- nF2 <= Q2R err2 - nR2)%R by lra. - apply H1. + apply H2. destruct (Rle_lt_dec 0 (Q2R err2 - nR2)). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. - apply H. + apply H0. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. @@ -953,7 +942,7 @@ Proof. eapply Rmult_le_compat_neg_l. lra. assert (nR1 - Q2R err1 <= nF1)%R by lra. - apply H1. + apply H2. lra. } { @@ -966,22 +955,22 @@ Proof. apply Rle_ge. rewrite Ropp_0. lra. - apply H0. + apply H1. destruct (Rle_lt_dec 0 (Q2R err2 + nR2)). - eapply Rle_trans. eapply Rplus_le_compat_l. eapply Rmult_le_compat_r; auto. assert (- nF1 <= Q2R err1 - nR1)%R by lra. - apply H1. + apply H2. lra. - eapply Rle_trans. eapply Rplus_le_compat_l. rewrite Rmult_comm. eapply Rmult_le_compat_neg_l. lra. - apply Ropp_le_ge_contravar in H. - apply Rge_le in H. - apply H. + apply Ropp_le_ge_contravar in H0. + apply Rge_le in H0. + apply H0. lra. } - remember (multIntv (widenIntv (e1lo, e1hi) err1) (widenIntv (e2lo, e2hi) err2)) as iv. @@ -991,17 +980,17 @@ Proof. rewrite <- maxAbs_impl_RmaxAbs. assert (ivlo iv = ivl) by (rewrite iv_unf; auto). assert (ivhi iv = ivh) by (rewrite iv_unf; auto). - rewrite <- H, <- H0. + 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). 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 H1 H2). - unfold IntervalArith.contained in H3. - destruct H3. + pose proof (IntervalArith.interval_multiplication_valid H2 H3). + unfold IntervalArith.contained in H4. + destruct H4. unfold RmaxAbsFun. apply Rmult_le_compat_r. - apply mEps_geq_zero. + apply inj_eps_posR. apply RmaxAbs; subst; simpl in *. + rewrite Q2R_min4. repeat rewrite Q2R_mult; @@ -1015,14 +1004,16 @@ 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: - eval_exp 0%R E1 (toRExp e1) nR1 -> - eval_exp 0%R E1 (toRExp e2) nR2 -> - eval_exp 0%R E1 (toRExp (Binop Div e1 e2)) nR -> - eval_exp (Q2R RationalSimps.machineEpsilon) E2 (toRExp e1) nF1 -> - eval_exp (Q2R RationalSimps.machineEpsilon) E2 (toRExp e2) nF2 -> - eval_exp (Q2R RationalSimps.machineEpsilon) (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) (toRExp (Binop Div (Var Q 1) (Var Q 2))) nF -> - validErrorbound (Binop Div e1 e2) absenv dVars = true -> + (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma: + m = computeJoin m1 m2 -> + eval_exp E1 (toREval (toRExp e1)) nR1 M0 -> + eval_exp E1 (toREval (toRExp e2)) nR2 M0 -> + eval_exp E1 (toREval (toRExp (Binop Div e1 e2))) nR M0 -> + eval_exp E2 (toRExp e1) nF1 m1 -> + eval_exp E2 (toRExp e2) nF2 m2 -> + eval_exp (updEnv 2 m2 nF2 (updEnv 1 m1 nF1 emptyEnv)) (toRExp (Binop Div (Var Q m1 1) (Var Q m2 2))) nF m -> + validType Gamma (Binop Div e1 e2) m -> + validErrorbound (Binop Div e1 e2) Gamma absenv dVars = true -> (Q2R e1lo <= nR1 <= Q2R e1hi)%R -> (Q2R e2lo <= nR2 <= Q2R e2hi)%R -> (Qleb e2hi 0 && negb (Qeq_bool e2hi 0) || Qleb 0 e2lo && negb (Qeq_bool e2lo 0) = true) -> @@ -1033,16 +1024,19 @@ Lemma validErrorboundCorrectDiv E1 E2 absenv (Rabs (nR2 - nF2) <= (Q2R err2))%R -> (Rabs (nR - nF) <= (Q2R e))%R. Proof. - intros e1_real e2_real eval_real e1_float e2_float eval_float - valid_error valid_bounds_e1 valid_bounds_e2 no_div_zero_real absenv_e1 + intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float + subexpr_ok valid_error valid_bounds_e1 valid_bounds_e2 no_div_zero_real absenv_e1 absenv_e2 absenv_div err1_bounded err2_bounded. eapply Rle_trans. eapply (div_abs_err_bounded e1 e2); eauto. - unfold validErrorbound in valid_error at 1. - rewrite absenv_div, absenv_e1, absenv_e2 in valid_error. + unfold validErrorbound in valid_error. + rewrite absenv_div,absenv_e1,absenv_e2 in valid_error. + case_eq (Gamma (Binop Div e1 e2)); intros; rewrite H in valid_error; [ | inversion valid_error ]. + inversion subexpr_ok; subst. rewrite H in H7; inversion H7; subst. clear m4 m5 H3 H4 H7 H6. + rename H into type_binop. andb_to_prop valid_error. - assert (validErrorbound e1 absenv dVars = true) as valid_err_e1 by auto; - assert (validErrorbound e2 absenv dVars = true) as valid_err_e2 by auto. + assert (validErrorbound e1 Gamma absenv dVars = true) as valid_err_e1 by auto; + assert (validErrorbound e2 Gamma absenv dVars = true) as valid_err_e2 by auto. clear L1 R. rename R1 into valid_error. rename L0 into no_div_zero_float. @@ -1050,8 +1044,8 @@ Proof. 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). - assert (0 <= Q2R err1)%R as err1_pos by (eapply (err_always_positive e1 absenv); eauto). - assert (0 <= Q2R err2)%R as err2_pos by (eapply (err_always_positive e2 absenv); eauto). + 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. apply Qle_Rle in valid_error. repeat rewrite Q2R_plus in valid_error. @@ -1075,7 +1069,7 @@ Proof. (* Error Propagation proof *) + clear absenv_e1 absenv_e2 valid_error eval_float eval_real e1_float e1_real e2_float e2_real absenv_div - valid_err_e1 valid_err_e2 E1 E2 absenv alo ahi nR nF e1 e2 e L. + valid_err_e1 valid_err_e2 E1 E2 absenv alo ahi nR nF e1 e2 e L subexpr_ok type_binop. unfold IntervalArith.contained, widenInterval in *. simpl in *. rewrite Q2R_plus, Q2R_minus in no_div_zero_float. @@ -1536,7 +1530,6 @@ Proof. { apply Rmult_le_compat_r; try lra. repeat (rewrite Q2R_inv; try auto). } } - * unfold widenIntv in *; unfold IntervalArith.contained in *; simpl in *. exfalso. assert (Q2R e2lo - Q2R err2 <= Q2R e2hi)%R by lra. @@ -1891,7 +1884,7 @@ Proof. { destruct valid_div_float. unfold RmaxAbsFun. apply Rmult_le_compat_r. - apply mEps_geq_zero. + apply inj_eps_posR. rewrite <- maxAbs_impl_RmaxAbs. unfold RmaxAbsFun. apply RmaxAbs; subst; simpl in *. @@ -1934,60 +1927,122 @@ Proof. rewrite (Qmult_inj_r) in H3; auto. } 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: + eval_exp E1 (toREval (toRExp e)) nR M0 -> + eval_exp E2 (toRExp e) nF1 m -> + eval_exp (updEnv 1 m nF1 emptyEnv) (toRExp (Downcast machineEpsilon (Var Q m 1))) nF machineEpsilon -> + validType Gamma (Downcast machineEpsilon e) machineEpsilon -> + validErrorbound (Downcast machineEpsilon e) Gamma absenv dVars = true -> + (Q2R elo <= nR <= Q2R ehi)%R -> + absenv e = ((elo, ehi), err) -> + absenv (Downcast machineEpsilon e) = ((alo, ahi), err') -> + (Rabs (nR - nF1) <= (Q2R err))%R -> + (Rabs (nR - nF) <= (Q2R err'))%R. +Proof. + intros eval_real eval_float eval_float_rnd subexpr_ok valid_error valid_intv absenv_e absenv_rnd err_bounded. + unfold validErrorbound in valid_error. + rewrite absenv_rnd in valid_error. + rewrite absenv_e in valid_error. + case_eq (Gamma (Downcast machineEpsilon e)); intros; rewrite H in valid_error; [ | inversion valid_error ]. + inversion subexpr_ok; subst. rewrite H in H5; inversion H5; symmetry in H5; subst. clear m2 H2 H3 H5. + + (* pose proof (typingBinopDet _ _ _ _ type_mult H). 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. + destruct dgi as [dgi1 dgi2]; simpl in dgi1; simpl in dgi2. + apply (Rle_trans _ (Q2R err + Q2R (maxAbs (widenIntv (elo, ehi) err)) * Q2R (meps machineEpsilon)) _). + + apply Rplus_le_compat_l. + apply Rmult_le_compat_r. + * rewrite <- Q2R0_is_0. + apply Qle_Rle. + apply inj_eps_pos. + * 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. + rewrite Q2R_plus. + split; assumption. + + apply Qle_bool_iff in R0. + rewrite <- Q2R_mult. + rewrite <- Q2R_plus. + apply Qle_Rle. + assumption. +Qed. + +Lemma test E e v m m' Gamma: + eval_exp E (toRExp e) v m -> + validType Gamma e m' -> + m = m'. +Proof. + revert v m m'; induction e; intros * eval_e vt_e. + - inversion eval_e; subst; inversion vt_e; subst; auto. + - inversion eval_e; subst; inversion vt_e; subst; auto. + - inversion vt_e; subst; auto; inversion eval_e; subst. + + eapply IHe; eauto. + + eapply IHe; eauto. + - inversion vt_e; subst; inversion eval_e; subst; try auto. + assert (m0 = m1) by (eapply IHe1; eauto). + assert (m3 = m2) by (eapply IHe2; eauto). + subst; simpl; auto. + - inversion vt_e; subst; inversion eval_e; subst; auto. +Qed. + (** Soundness theorem for the error bound validator. Proof is by induction on the expression e. 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, + forall E1 E2 fVars dVars absenv nR nF err P elo ehi m Gamma, + validType Gamma e m -> approxEnv E1 absenv fVars dVars E2 -> - NatSet.Subset (NatSet.diff (usedVars e) dVars) fVars -> - eval_exp 0%R E1 (toRExp e) nR -> - eval_exp (Q2R RationalSimps.machineEpsilon) E2 (toRExp e) nF -> - validErrorbound e absenv dVars = true -> + NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars -> + eval_exp E1 (toREval (toRExp e)) nR M0 -> + eval_exp E2 (toRExp e) nF m -> + validErrorbound e Gamma absenv dVars = true -> validIntervalbounds e absenv P dVars = true -> - (forall v : NatSet.elt, NatSet.mem v dVars = true -> - exists vr, E1 v = Some vr /\ - (Q2R (fst (fst (absenv (Var Q v)))) <= vr <= Q2R (snd (fst (absenv (Var Q v)))))%R) -> + (forall v1 m1, NatSet.mem v1 dVars = true -> + exists vr mv1, E1 v1 = Some (vr, M0) /\ Gamma (Var Q mv1 v1) = Some m1 /\ + (Q2R (fst (fst (absenv (Var Q m1 v1)))) <= vr <= Q2R (snd (fst (absenv (Var Q m1 v1)))))%R) -> (forall v, NatSet.mem v fVars= true -> - exists vR, E1 v = Some vR /\ + exists vR, E1 v = Some (vR, M0) /\ (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> absenv e = ((elo,ehi),err) -> (Rabs (nR - nF) <= (Q2R err))%R. Proof. - induction e; - try (intros E1 E2 fVars dVars absenv nR nF err P elo ehi; - intros approxCEnv fVars_subset eval_real eval_float valid_error valid_intv valid_dVars P_valid absenv_eq). - - eapply validErrorboundCorrectVariable; eauto. - - pose proof (validIntervalbounds_sound (Const v) absenv P (vR:=nR) valid_intv valid_dVars (fVars:=fVars)) - as bounds_valid. + revert e; induction e; + (intros * typing_ok approxCEnv fVars_subset eval_real eval_float valid_error valid_intv valid_dVars P_valid absenv_eq). + - inversion typing_ok; subst. + eapply validErrorboundCorrectVariable; try eauto. + - inversion typing_ok; subst. eapply validErrorboundCorrectConstant; eauto. - rewrite absenv_eq in *; simpl in *; auto. + + simpl in valid_intv. + rewrite absenv_eq in valid_intv. + simpl in eval_real; inversion eval_real; subst. + simpl in H3; 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. + simpl in H,H0. + split; auto. + * apply Qle_bool_iff in H. apply (Qle_Rle _ _ H). + * apply Qle_bool_iff in H0. apply (Qle_Rle _ _ H0). - 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 ]. andb_to_prop valid_error. - destruct u; try congruence. - env_assert absenv e absenv_e. - destruct absenv_e as [iv [err_e absenv_e]]. - rename R into valid_error. - andb_to_prop valid_error. - apply Qeq_bool_iff in R. - apply Qeq_eqR in R. - 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. - simpl in valid_intv. - rewrite absenv_eq in valid_intv; andb_to_prop valid_intv. - auto. - instantiate (1 := e_hi). - instantiate (1 := e_lo). - rewrite absenv_e; auto. - - pose proof (ivbounds_approximatesPrecond_sound (Binop b e1 e2) absenv P valid_intv) as env_approx_p. + inversion R. + - pose proof (ivbounds_approximatesPrecond_sound (f:=(Binop b e1 e2)) absenv P (Gamma:=Gamma) valid_intv) as env_approx_p. + assert (valid_error_copy := valid_error). simpl in valid_error. env_assert absenv e1 absenv_e1. env_assert absenv e2 absenv_e2. @@ -2000,39 +2055,60 @@ Proof. 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 ]. + (* pose proof (expEqBool_refl (Binop b e1 e2)); simpl in H; rewrite H in valid_error. *) + assert(m0 = m) by (inversion typing_ok; subst; rewrite H in H7; inversion H7; subst; auto); 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. apply binary_unfolding in eval_float. - destruct eval_float as [vF1 [vF2 [ eval_vF1 [eval_vF2 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) L2 valid_dVars (fVars:=fVars)) + destruct m1; destruct m2; inversion H3. + inversion typing_ok; subst. + assert (mF1 = m1) as m1eq by (eapply test; eauto). + assert (mF2 = m2) as m2eq by (eapply test; eauto). + symmetry in m1eq,m2eq; subst. + pose proof (validIntervalbounds_sound absenv P (vR:=v1) H5 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) R2 valid_dVars (fVars:=fVars)) + pose proof (validIntervalbounds_sound absenv P (vR:=v2) H9 R2 valid_dVars (fVars:=fVars)) as valid_bounds_e2. rewrite absenv_e2 in valid_bounds_e2; 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. + { 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. } + (* { destruct eval_float as [eval_e1 [eval_e2 eval_binop]]. *) + (* pose proof (typeExpressionIsSound _ eval_e1). *) + (* rewrite te1 in H0; inversion H0; subst; auto. } *) + (* { unfold isSubExpression in subexpr_ok. *) + (* simpl in subexpr_ok. *) + (* pose proof (subexpr_unfolding _ _ _ _ subexpr_ok) as [subexpr_e1 subexpr_e2]. *) + (* auto. } *) * eapply IHe2; eauto. - hnf. intros a in_diff. + { 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. - + destruct H. - assert ((Q2R ivlo1 <= v1 <= Q2R ivhi1) /\ (Q2R ivlo2 <= v2 <= Q2R ivhi2))%R. + split; auto. } + (* { destruct eval_float as [eval_e1 [eval_e2 eval_binop]]. *) + (* pose proof (typeExpressionIsSound _ eval_e2). *) + (* rewrite te2 in H0; inversion H0; subst; auto. } *) + (* { unfold isSubExpression in subexpr_ok. *) + (* simpl in subexpr_ok. *) + (* pose proof (subexpr_unfolding _ _ _ _ subexpr_ok) as [subexpr_e1 subexpr_e2]. *) + (* 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. @@ -2048,100 +2124,239 @@ Proof. apply fVars_subset. rewrite NatSet.diff_spec, NatSet.union_spec. split; try auto. } - * destruct H1. destruct b. + * (*destruct m1; destruct m2; inversion H3.*) + destruct H0, H1, H. destruct b. { eapply (validErrorboundCorrectAddition (e1:=e1) absenv); eauto. - unfold validErrorbound. - rewrite absenv_eq, absenv_e1, absenv_e2; simpl. - apply Is_true_eq_true. - apply andb_prop_intro; split. - - apply Is_true_eq_left in L. auto. - - apply andb_prop_intro. - split; try auto. - apply andb_prop_intro. - split; apply Is_true_eq_left; try auto. - apply L1. - apply R. - apply Is_true_eq_left; apply R0. } + simpl; apply valid_error_copy. (*TODO: something cleaner... *) } + (* unfold validErrorbound. *) + (* rewrite absenv_eq, absenv_e1, absenv_e2; simpl. *) + (* apply Is_true_eq_true. *) + (* apply andb_prop_intro; split. *) + (* - apply Is_true_eq_left in L. auto. *) + (* - apply andb_prop_intro. *) + (* split; try auto. *) + (* apply andb_prop_intro. *) + (* split; apply Is_true_eq_left; try auto. *) + (* apply L1. *) + (* apply R. *) + (* apply Is_true_eq_left; apply R0. } *) { eapply (validErrorboundCorrectSubtraction (e1:=e1) absenv); eauto. - unfold validErrorbound. - rewrite absenv_eq, absenv_e1, absenv_e2; simpl. - apply Is_true_eq_true. - apply andb_prop_intro; split. - - apply Is_true_eq_left in L. auto. - - apply andb_prop_intro. - split; try auto. - apply andb_prop_intro. - split; apply Is_true_eq_left; try auto. - apply L1. - apply R. - apply Is_true_eq_left; apply R0. } + simpl; apply valid_error_copy. } + (* unfold validErrorbound. *) + (* rewrite absenv_eq, absenv_e1, absenv_e2; simpl. *) + (* apply Is_true_eq_true. *) + (* apply andb_prop_intro; split. *) + (* - apply Is_true_eq_left in L. auto. *) + (* - apply andb_prop_intro. *) + (* split; try auto. *) + (* apply andb_prop_intro. *) + (* split; apply Is_true_eq_left; try auto. *) + (* apply L1. *) + (* apply R. *) + (* apply Is_true_eq_left; apply R0. } *) { eapply (validErrorboundCorrectMult (e1 := e1) absenv); eauto. - unfold validErrorbound. - rewrite absenv_eq, absenv_e1, absenv_e2; simpl. - apply Is_true_eq_true. - apply andb_prop_intro; split. - - apply Is_true_eq_left in L. auto. - - apply andb_prop_intro. - split; try auto. - apply andb_prop_intro. - split; apply Is_true_eq_left; try auto. - apply L1. - apply R. - apply Is_true_eq_left; apply R0. } + simpl; apply valid_error_copy. } + (* unfold validErrorbound. *) + (* rewrite absenv_eq, absenv_e1, absenv_e2; simpl. *) + (* apply Is_true_eq_true. *) + (* apply andb_prop_intro; split. *) + (* - apply Is_true_eq_left in L. auto. *) + (* - apply andb_prop_intro. *) + (* split; try auto. *) + (* apply andb_prop_intro. *) + (* split; apply Is_true_eq_left; try auto. *) + (* apply L1. *) + (* apply R. *) + (* apply Is_true_eq_left; apply R0. } *) { eapply (validErrorboundCorrectDiv (e1 := e1) absenv); eauto. - unfold validErrorbound. - rewrite absenv_eq, absenv_e1, absenv_e2; simpl. - apply Is_true_eq_true. - apply andb_prop_intro; split. - - apply Is_true_eq_left in L. auto. - - apply andb_prop_intro. - split; try auto. - apply andb_prop_intro. - split; apply Is_true_eq_left; try auto. - apply L1. - apply R. - apply Is_true_eq_left; apply R0. - - andb_to_prop R1; auto. } + - 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 H in R1; inversion R1. + auto. } + (* unfold validErrorbound. *) + (* rewrite absenv_eq, absenv_e1, absenv_e2; simpl. *) + (* apply Is_true_eq_true. *) + (* apply andb_prop_intro; split. *) + (* - apply Is_true_eq_left in L. auto. *) + (* - apply andb_prop_intro. *) + (* split; try auto. *) + (* apply andb_prop_intro. *) + (* split; apply Is_true_eq_left; try auto. *) + (* apply L1. *) + (* apply R. *) + (* apply Is_true_eq_left; apply R0. *) + (* - andb_to_prop R1; 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 ]. + 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. + andb_to_prop valid_intv. + inversion eval_float; subst. + simpl in eval_real. + eapply (validErrorboundCorrectRounding absenv dVars 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. + (* case_eq (typeExpression e e); intros; rewrite H1 in typing_ok; [ | inversion typing_ok ]. *) + (* case_eq (isMorePrecise m m0); intros; rewrite H4 in typing_ok; inversion typing_ok; subst. *) + (* assert ((forall (v : NatSet.elt) (m : mType), *) + (* NatSet.mem v dVars = true -> *) + (* typeExpression e (Var Q m v) = Some m -> *) + (* exists vR : Rdefinitions.R, *) + (* E1 v = Some (vR, M0) /\ *) + (* (Q2R (fst (fst (absenv (Var Q m v)))) <= vR <= Q2R (snd (fst (absenv (Var Q m v)))))%R)). *) + (* { intros v_a m_a natset_a te_a. *) + (* pose proof (typedIsSubExpr _ _ te_a) as subexpr_a. *) + (* specialize (valid_dVars e v_a m_a natset_a te_a). *) + (* apply valid_dVars. } *) + simpl in fVars_subset. + inversion typing_ok; subst. + pose proof (validIntervalbounds_sound absenv P (fVars:=fVars) (dVars:=dVars) (E:=E1) H4 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. + * inversion typing_ok; subst. + assert (m3 = m2) by (eapply test; eauto). + subst; auto. + * assert (absenv e = (fst ive1, snd ive1, err1)) by (destruct ive1; simpl; auto). + apply H0. 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 m n)); simpl in *. + case_eq (tmap (Var Q m 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. + + +(* Lemma soundnessTypeCmd f n m0 m1 fV dV oV: *) +(* ssaPrg f (NatSet.union fV dV) oV -> *) +(* (typeExpressionCmd f) (Var Q m1 n) = Some m1 -> *) +(* (typeExpressionCmd f) (Var Q m0 n) = Some m0 -> *) +(* m1 = m0. *) +(* Proof. *) +(* revert f; induction f; intros. *) +(* - simpl in H0,H1. *) +(* case_eq (n =? n0); intros; rewrite H2 in H0, H1. *) +(* + admit. *) +(* + rewrite andb_false_r in H0, H1. *) +(* case_eq (typeExpression e (Var Q m1 n)); intros; case_eq (typeExpression e (Var Q m0 n)); intros; rewrite H3 in H0; rewrite H4 in H1. *) +(* * case_eq (typeExpressionCmd f (Var Q m1 n)); intros; case_eq (typeExpressionCmd f (Var Q m0 n)); intros; rewrite H5 in H0; rewrite H6 in H1. *) +(* { *) + +(* } *) + +(* case_eq (mTypeEqBool m1 m); intros; case_eq (mTypeEqBool m0 m); intros; rewrite H3 in H0; rewrite H in H1. *) +(* + *) + + + +(* Fixpoint cmdEqBool (f f': cmd Q): bool := *) +(* match f, f' with *) +(* |Let m1 n1 e1 c1, Let m2 n2 e2 c2 => *) +(* (mTypeEqBool m1 m2) && (n1 =? n2) && (expEqBool e1 e2) && (cmdEqBool c1 c2) *) +(* |Ret e1, Ret e2 => expEqBool e1 e2 *) +(* |_, _ => false *) +(* end. *) + +(* Fixpoint isSubCmd (f':cmd Q) (f:cmd Q): bool := *) +(* let rec := match f with *) +(* |Let m n e c => isSubCmd f' c *) +(* |Ret e => false *) +(* end *) +(* in *) +(* orb (cmdEqBool f f') rec. *) + + + Theorem validErrorboundCmd_sound (f:cmd Q) (absenv:analysisResult): - forall E1 E2 outVars fVars dVars vR vF elo ehi err P, + forall E1 E2 outVars fVars dVars vR vF elo ehi err P m Gamma, + validTypeCmd Gamma f m -> approxEnv E1 absenv fVars dVars E2 -> ssa f (NatSet.union fVars dVars) outVars -> NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars -> - bstep (toRCmd f) E1 0%R vR -> - bstep (toRCmd f) E2 (Q2R RationalSimps.machineEpsilon) vF -> - validErrorboundCmd f absenv dVars = true -> + bstep (toREvalCmd (toRCmd f)) E1 vR M0 -> + bstep (toRCmd f) E2 vF m -> + validErrorboundCmd f Gamma absenv dVars = true -> validIntervalboundsCmd f absenv P dVars = true -> - (forall v : NatSet.elt, NatSet.mem v dVars = true -> - exists vR, E1 v = Some vR /\ - (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R) -> + (forall v1 m1, NatSet.mem v1 dVars = true -> + exists vR mv1, E1 v1 = Some (vR, M0) /\ Gamma (Var Q mv1 v1) = Some m1 /\ + (Q2R (fst (fst (absenv (Var Q m1 v1)))) <= vR <= Q2R (snd (fst (absenv (Var Q m1 v1)))))%R) -> (forall v, NatSet.mem v fVars= true -> - exists vR, E1 v = Some vR /\ + exists vR, E1 v = Some (vR, M0) /\ (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> absenv (getRetExp f) = ((elo,ehi),err) -> (Rabs (vR - vF) <= (Q2R err))%R. Proof. induction f; - intros E1 E2 outVars fVars dVars vR vF elo ehi err P; - intros approxc1c2 ssa_f freeVars_subset eval_real eval_float valid_bounds valid_intv fVars_sound P_valid absenv_res. + intros * type_f approxc1c2 ssa_f freeVars_subset eval_real eval_float (*issubcmd_ok*) valid_bounds valid_intv fVars_sound P_valid absenv_res. - simpl in eval_real, eval_float. - inversion eval_real; inversion eval_float; subst. + inversion eval_float; inversion eval_real; subst. inversion ssa_f; subst. - assert (approxEnv (updEnv n v E1) absenv fVars (NatSet.add n dVars) (updEnv n v0 E2)). + assert (approxEnv (updEnv n M0 v0 E1) absenv fVars (NatSet.add n dVars) (updEnv n m v 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. - assert (snd (absenv (Var Q n)) == snd (absenv (Var Q n))) by apply Qeq_refl. + assert (snd (absenv (Var Q m n)) == snd (absenv (Var Q m n))) by apply Qeq_refl. pose proof (Qleb_comp _ _ R0 _ _ H). - assert (Qle (snd (absenv e)) (snd (absenv (Var Q n)))). + assert (Qle (snd (absenv e)) (snd (absenv (Var Q m n)))). { rewrite <- Qle_bool_iff. rewrite H0. rewrite Qle_bool_iff. apply Qle_lteq. - right. auto. } + right. + inversion type_f; subst. auto. } { apply Qle_Rle in H1. eapply Rle_trans. Focus 2. @@ -2150,6 +2365,7 @@ Proof. destruct absenv_e as [iv [err_e absenv_e]]. destruct iv. eapply validErrorbound_sound; eauto. + - inversion type_f; subst; auto. - hnf. intros a a_in_diff. apply freeVars_subset. rewrite NatSet.diff_spec in *. @@ -2159,9 +2375,9 @@ Proof. rewrite NatSet.remove_spec, NatSet.union_spec. split; try auto. hnf; intros; subst. - specialize (H2 n H3). - rewrite <- NatSet.mem_spec in H2. - rewrite H2 in *; congruence. + specialize (H5 n H2). + rewrite <- NatSet.mem_spec in H5. + rewrite H5 in *; congruence. - simpl in valid_intv. andb_to_prop valid_intv. assumption. @@ -2189,7 +2405,8 @@ Proof. rename R into valid_rec. simpl in valid_intv; andb_to_prop valid_intv. - eapply (IHf (updEnv n v E1) (updEnv n v0 E2) _ _ _ vR vF elo ehi err P); eauto. + eapply (IHf (updEnv n M0 v0 E1) (updEnv n m v E2) _ _ _ vR vF elo ehi err P); eauto. + * inversion type_f; subst; auto. * instantiate (1 := outVars). eapply ssa_equal_set; eauto. hnf. intros a; split; intros in_set. @@ -2206,7 +2423,7 @@ Proof. simpl. rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec. split; try auto. - * intros v1 v1_mem. + * intros v1 m1 v1_mem. unfold updEnv. case_eq (v1 =? n); intros v1_eq. { rename R1 into eq_lo; @@ -2215,27 +2432,30 @@ Proof. 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. - rewrite <- eq_lo, <- eq_hi. - exists v; split; try auto. - 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 (H2 n a_mem_freeVars). - rewrite <- NatSet.mem_spec in H2. - rewrite H2 in *; congruence. } + exists v0, m; split; try split; try auto; assert (m1 = m) by admit; subst. + - inversion H11; subst; 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. } { rewrite NatSet.mem_spec in v1_mem. rewrite NatSet.add_spec in v1_mem. rewrite Nat.eqb_neq in v1_eq. destruct v1_mem. - exfalso; apply v1_eq; auto. - - apply fVars_sound. rewrite NatSet.mem_spec; auto. } + - apply fVars_sound ; try auto. + rewrite NatSet.mem_spec; auto. } * intros v1 mem_fVars. specialize (P_valid v1 mem_fVars). unfold updEnv. @@ -2254,4 +2474,5 @@ Proof. destruct absenv_e as [iv [err_e absenv_e]]. destruct iv. eapply validErrorbound_sound; eauto. -Qed. \ No newline at end of file + inversion type_f; subst; auto. +Admitted. \ No newline at end of file diff --git a/coq/Expressions.v b/coq/Expressions.v index 3f31d772c7d80a54c925ab982d1cb127c84d1897..9cede73db38e715b7eef87aa703c7f51706d1873 100644 --- a/coq/Expressions.v +++ b/coq/Expressions.v @@ -1,9 +1,9 @@ - (** 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 Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet. +Require Import Daisy.Infra.RealRationalProps Daisy.Infra.RationalSimps. +Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet Daisy.IntervalArithQ Daisy.IntervalArith Daisy.Infra.MachineType. (** Expressions will use binary operators. @@ -11,6 +11,7 @@ Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet. **) Inductive binop : Type := Plus | Sub | Mult | Div. +(** TODO: simplify pattern matching **) Definition binopEqBool (b1:binop) (b2:binop) := match b1 with Plus => match b2 with Plus => true |_ => false end @@ -31,6 +32,12 @@ Definition evalBinop (o:binop) (v1:R) (v2:R) := | Div => Rdiv v1 v2 end. +Lemma binopEqBool_refl b: + binopEqBool b b = true. +Proof. + case b; auto. +Qed. + (** Expressions will use unary operators. Define them first @@ -53,15 +60,18 @@ Definition evalUnop (o:unop) (v:R):= |Inv => (/ v)%R end . + + (** Define expressions parametric over some value type V. Will ease reasoning about different instantiations later. **) Inductive exp (V:Type): Type := - Var: nat -> exp V -| Const: V -> exp V + Var: mType -> nat -> exp V +| Const: mType -> V -> exp V | Unop: unop -> exp V -> exp V -| Binop: binop -> exp V -> exp V -> exp V. +| Binop: binop -> exp V -> exp V -> exp V +| Downcast: mType -> exp V -> exp V. (** Boolean equality function on expressions. @@ -69,14 +79,14 @@ Inductive exp (V:Type): Type := **) Fixpoint expEqBool (e1:exp Q) (e2:exp Q) := match e1 with - |Var _ v1 => + |Var _ m1 v1 => match e2 with - |Var _ v2 => v1 =? v2 + |Var _ m2 v2 => andb (mTypeEqBool m1 m2) (v1 =? v2) | _=> false end - |Const n1 => + |Const m1 n1 => match e2 with - |Const n2 => Qeq_bool n1 n2 + |Const m2 n2 => andb (mTypeEqBool m1 m2) (Qeq_bool n1 n2) | _=> false end |Unop o1 e11 => @@ -89,8 +99,158 @@ Fixpoint expEqBool (e1:exp Q) (e2:exp Q) := |Binop o2 e21 e22 => andb (binopEqBool o1 o2) (andb (expEqBool e11 e21) (expEqBool e12 e22)) |_ => false end + |Downcast m1 f1 => + match e2 with + |Downcast m2 f2 => andb (mTypeEqBool m1 m2) (expEqBool f1 f2) + |_ => false + end + end. + + +(* Lemma expEqBool_eq e1 e2: *) +(* e1 = e2 -> *) +(* expEqBool e1 e2 = true. *) +(* Proof. *) +(* revert e1 e2. *) +(* induction e1; intros; split; intros. *) +(* - simpl in H. destruct e2; try inversion H; apply andb_true_iff in H; destruct H. *) +(* f_equal. *) +(* + apply EquivEqBoolEq; auto. *) +(* + apply beq_nat_true; auto. *) +(* - simpl. destruct e2; try inversion H. *) +(* rewrite mTypeEqBool_refl. *) +(* simpl. *) +(* symmetry; apply beq_nat_refl. *) +(* - simpl in H; destruct e2; try inversion H. apply andb_true_iff in H; destruct H. *) +(* f_equal. *) +(* + apply EquivEqBoolEq; auto. *) +(* + admit. *) +(* - *) + + + +Lemma expEqBool_refl e: + expEqBool e e = true. +Proof. + induction e; apply andb_true_iff; split; simpl in *; auto; try (apply EquivEqBoolEq; auto). + - symmetry; apply beq_nat_refl. + - apply Qeq_bool_iff; lra. + - case u; auto. + - case b; auto. + - apply andb_true_iff; split. + apply IHe1. apply IHe2. +Qed. + +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. + +Lemma expEqBool_sym e e': + expEqBool e e' = expEqBool e' e. +Proof. + revert e'. + induction e; intros e'; destruct e'; simpl; try auto. + - f_equal. + + apply mTypeEqBool_sym; auto. + + apply beq_nat_sym. + - f_equal. + + apply mTypeEqBool_sym; auto. + + apply Qeq_bool_sym. + - f_equal. + + destruct u; auto. + + apply IHe. + - f_equal. + + destruct b; auto. + + f_equal. + * apply IHe1. + * apply IHe2. + - f_equal. + + apply mTypeEqBool_sym; auto. + + apply IHe. +Qed. + +Lemma expEqBool_trans e f g: + expEqBool e f = true -> + expEqBool f g = true -> + expEqBool e g = true. +Proof. + revert e f g; induction e; destruct f; intros; simpl in H; inversion H; rewrite H; clear H; destruct g; simpl in H0; inversion H0; rewrite H0; clear H0; apply andb_true_iff in H1; destruct H1; apply andb_true_iff in H2; destruct H2; simpl. + - apply EquivEqBoolEq in H1. + apply EquivEqBoolEq in H. + apply beq_nat_true in H2. + apply beq_nat_true in H0. + subst. + rewrite <- beq_nat_refl,mTypeEqBool_refl. + auto. + - apply EquivEqBoolEq in H1. + apply EquivEqBoolEq in H. + subst. + rewrite mTypeEqBool_refl; simpl. + apply Qeq_bool_iff in H2. + apply Qeq_bool_iff in H0. + apply Qeq_bool_iff. + lra. + - assert (u = u0) by (destruct u; destruct u0; inversion H1; auto). + assert (u0 = u1) by (destruct u0; destruct u1; inversion H; auto). + subst. + assert (unopEqBool u1 u1 = true) by (destruct u1; auto). + apply andb_true_iff; split; try auto. + eapply IHe; eauto. + - apply andb_true_iff; split. + + destruct b; destruct b0; destruct b1; auto. + + apply andb_true_iff in H2; destruct H2. + apply andb_true_iff in H0; destruct H0. + apply andb_true_iff; split. + eapply IHe1; eauto. + eapply IHe2; eauto. + - apply EquivEqBoolEq in H1. + apply EquivEqBoolEq in H. + subst. + rewrite mTypeEqBool_refl; simpl. + eapply IHe; eauto. +Qed. + + + + +Fixpoint toRExp (e:exp Q) := + match e with + |Var _ m v => Var R m v + |Const m n => Const m (Q2R n) + |Unop o e1 => Unop o (toRExp e1) + |Binop o e1 e2 => Binop o (toRExp e1) (toRExp e2) + |Downcast m e1 => Downcast m (toRExp e1) end. +Fixpoint toREval (e:exp R) := + match e with + | Var _ _ v => Var R M0 v + | 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) + end. + +Definition toREvalEnv (E:env) : env := + fun (n:nat) => + let s := (E n) in + match s with + | None => None + | Some (r, _) => Some (r, M0) + end. + + (** Define a perturbation function to ease writing of basic definitions **) @@ -103,26 +263,36 @@ 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 (eps:R) (E:env) :(exp R) -> R -> Prop := -| Var_load x v: - E x = Some v -> - eval_exp eps E (Var R x) v -| Const_dist n delta: - Rle (Rabs delta) eps -> - eval_exp eps E (Const n) (perturb n delta) -| Unop_neg f1 v1: - eval_exp eps E f1 v1 -> - eval_exp eps E (Unop Neg f1) (evalUnop Neg v1) -| Unop_inv f1 v1 delta: - Rle (Rabs delta) eps -> - eval_exp eps E f1 v1 -> - eval_exp eps E (Unop Inv f1) (perturb (evalUnop Inv v1) delta) -| Binop_dist op f1 f2 v1 v2 delta: - Rle (Rabs delta) eps -> - eval_exp eps E f1 v1 -> - eval_exp eps E f2 v2 -> +Inductive eval_exp (E:env) :(exp R) -> R -> mType -> Prop := +| Var_load m x v: + (** isMorePrecise m m1 = true ->**) + (**mTypeEqBool m m1 = true ->*) + E x = Some (v, m) -> + eval_exp E (Var R m x) v m +| Const_dist m n delta: + Rle (Rabs delta) (Q2R (meps m)) -> + eval_exp E (Const m n) (perturb n delta) m +| Unop_neg m f1 v1: + eval_exp E f1 v1 m -> + eval_exp E (Unop Neg f1) (evalUnop Neg v1) m +| Unop_inv m f1 v1 delta: + Rle (Rabs delta) (Q2R (meps m)) -> + eval_exp E f1 v1 m -> + eval_exp E (Unop Inv f1) (perturb (evalUnop Inv v1) delta) m +| Binop_dist m1 m2 op f1 f2 v1 v2 delta: + (*isJoinOf m m1 m2 = true ->*) + Rle (Rabs delta) (Q2R (meps (computeJoin m1 m2))) -> + eval_exp E f1 v1 m1 -> + eval_exp E f2 v2 m2 -> ((op = Div) -> (~ v2 = 0)%R) -> - eval_exp eps E (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta). + eval_exp E (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta) (computeJoin m1 m2) +| 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 f1 v1 m1 -> + eval_exp E (Downcast m f1) (perturb v1 delta) m. + (** Define the set of "used" variables of an expression to be the set of variables @@ -130,9 +300,10 @@ Inductive eval_exp (eps:R) (E:env) :(exp R) -> R -> Prop := **) Fixpoint usedVars (V:Type) (e:exp V) :NatSet.t := match e with - | Var _ x => NatSet.singleton x + | Var _ _ x => NatSet.singleton x | Unop u e1 => usedVars e1 | Binop b e1 e2 => NatSet.union (usedVars e1) (usedVars e2) + | Downcast _ e1 => usedVars e1 | _ => NatSet.empty end. @@ -148,75 +319,121 @@ Proof. lra. Qed. + +Lemma general_meps_0_deterministic (f:exp R) (E:env): + forall v1 v2 m1, + m1 = M0 -> + eval_exp E (toREval f) v1 m1 -> + eval_exp E (toREval f) v2 M0 -> + v1 = v2. +Proof. + induction f; intros v1 v2 m1 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 H7 in H3; inversion H3; 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): forall v1 v2, - eval_exp 0 E f v1 -> - eval_exp 0 E f v2 -> + eval_exp E (toREval f) v1 M0 -> + eval_exp E (toREval f) v2 M0 -> v1 = v2. Proof. - induction f; intros v1 v2 eval_v1 eval_v2; - inversion eval_v1; inversion eval_v2; - repeat try rewrite delta_0_deterministic; subst; auto. - - rewrite H3 in H0; inversion H0; - subst; auto. - - rewrite (IHf v0 v3); auto. - - inversion H3. - - inversion H4. - - rewrite (IHf v0 v3); auto. - - rewrite (IHf1 v0 v4); auto. - rewrite (IHf2 v3 v5); auto. + intros v1 v2 ev1 ev2. + assert (M0 = M0) by auto. + apply (general_meps_0_deterministic f H ev1 ev2). Qed. + (** Helping lemma. Needed in soundness proof. 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 eps E vF: - eval_exp eps E (Binop b f1 f2) vF -> - exists vF1 vF2, - eval_exp eps E f1 vF1 /\ - eval_exp eps E f2 vF2 /\ - eval_exp eps (updEnv 2 vF2 (updEnv 1 vF1 emptyEnv)) - (Binop b (Var R 1) (Var R 2)) vF. +Lemma binary_unfolding b f1 f2 m E vF: + eval_exp E (Binop b f1 f2) vF m -> + exists vF1 vF2 m1 m2, + m = computeJoin m1 m2 /\ + eval_exp E f1 vF1 m1 /\ + eval_exp E f2 vF2 m2 /\ + eval_exp (updEnv 2 m2 vF2 (updEnv 1 m1 vF1 emptyEnv)) + (Binop b (Var R m1 1) (Var R m2 2)) vF m. Proof. intros eval_float. inversion eval_float; subst. - exists v1 ; exists v2; repeat split; try auto. - constructor; try auto. - - constructor. - unfold updEnv; cbv; auto. - - constructor. - unfold updEnv; cbv; auto. + 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). + (* unfold mTypeEqBool; apply Qeq_bool_iff; apply Qeq_refl. *) + eapply Var_load; eauto. + (* unfold mTypeEqBool; apply Qeq_bool_iff; apply Qeq_refl. *) Qed. -(** -Analogous lemma for unary expressions. -**) -Lemma unary_unfolding (e:exp R) (eps:R) (E:env) (v:R): - (eval_exp eps E (Unop Inv e) v <-> - exists v1, - eval_exp eps E e v1 /\ - eval_exp eps (updEnv 1 v1 E) (Unop Inv (Var R 1)) v). +(* (** *) +(* Analogous lemma for unary expressions. *) +(* **) *) +Lemma unary_unfolding (e:exp R) (m:mType) (E:env) (v:R): + (eval_exp E (Unop Inv e) v m -> + exists v1 m1, + eval_exp E e v1 m1 /\ + eval_exp (updEnv 1 m1 v1 E) (Unop Inv (Var R m1 1)) v m). Proof. - split. - - intros eval_un. + intros eval_un. inversion eval_un; subst. - exists v1. + exists v1; exists m. repeat split; try auto. - constructor; try auto. - constructor; auto. - - intros exists_val. - destruct exists_val as [v1 [eval_f1 eval_e_E]]. - inversion eval_e_E; subst. - inversion H1; subst. - unfold updEnv in *; simpl in *. - constructor; auto. - inversion H2; subst; auto. + econstructor; try auto. + pose proof (isMorePrecise_refl m). + econstructor; eauto. + (* - intros exists_val. *) + (* destruct exists_val as [v1 [m1 [eval_f1 eval_e_E]]]. *) + (* inversion eval_e_E; subst. *) + (* inversion H1; subst. *) + (* econstructor; eauto. *) + (* unfold updEnv in H6. *) + (* simpl in H6. *) + (* inversion H6. *) + (* rewrite <- H2. *) + + (* rewrite <- H1. *) + (* auto. *) Qed. (** @@ -229,17 +446,17 @@ Inductive bexp (V:Type) : Type := (** Define evaluation of boolean expressions **) -Inductive bval (eps:R) (E:env): (bexp R) -> Prop -> Prop := - leq_eval (f1:exp R) (f2:exp R) (v1:R) (v2:R): - eval_exp eps E f1 v1 -> - eval_exp eps E f2 v2 -> - bval eps E (leq f1 f2) (Rle v1 v2) -|less_eval (f1:exp R) (f2:exp R) (v1:R) (v2:R): - eval_exp eps E f1 v1 -> - eval_exp eps E f2 v2 -> - bval eps E (less f1 f2) (Rlt v1 v2). -(** - Simplify arithmetic later by making > >= only abbreviations -**) -Definition gr := fun (V:Type) (f1: exp V) (f2: exp V) => less f2 f1. -Definition greq := fun (V:Type) (f1:exp V) (f2: exp V) => leq f2 f1. \ No newline at end of file +(* Inductive bval (E:env): (bexp R) -> Prop -> Prop := *) +(* leq_eval (f1:exp R) (f2:exp R) (v1:R) (v2:R): *) +(* eval_exp E f1 v1 -> *) +(* eval_exp E f2 v2 -> *) +(* bval E (leq f1 f2) (Rle v1 v2) *) +(* |less_eval (f1:exp R) (f2:exp R) (v1:R) (v2:R): *) +(* eval_exp E f1 v1 -> *) +(* eval_exp E f2 v2 -> *) +(* bval E (less f1 f2) (Rlt v1 v2). *) +(* (** *) +(* Simplify arithmetic later by making > >= only abbreviations *) +(* **) *) +(* Definition gr := fun (V:Type) (f1: exp V) (f2: exp V) => less f2 f1. *) +(* Definition greq := fun (V:Type) (f1:exp V) (f2: exp V) => leq f2 f1. *) \ No newline at end of file diff --git a/coq/Infra/Abbrevs.v b/coq/Infra/Abbrevs.v index 4a64d9b5596e809bc9a5ce8f3dbadc76f569378e..08c1f05436d16830c567a5ee47e97f5e6898add3 100644 --- a/coq/Infra/Abbrevs.v +++ b/coq/Infra/Abbrevs.v @@ -2,6 +2,7 @@ This file contains some type abbreviations, to ease writing. **) Require Import Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qreals. +Require Import Daisy.Infra.MachineType. Global Set Implicit Arguments. (** @@ -36,15 +37,15 @@ Arguments ivlo _ /. Arguments ivhi _ /. (** -Later we will argue about program preconditions. -Define a precondition to be a function mapping numbers (resp. variables) to intervals. + Later we will argue about program preconditions. + Define a precondition to be a function mapping numbers (resp. variables) to intervals. **) Definition precond :Type := nat -> intv. (** Abbreviation for the type of a variable environment, which should be a partial function **) -Definition env := nat -> option R. +Definition env := nat -> option (R * mType). (** The empty environment must return NONE for every variable @@ -54,8 +55,98 @@ Definition emptyEnv:env := fun _ => None. (** Define environment update function as abbreviation, for variable environments **) - -Definition updEnv (x:nat) (v: R) (E:env) (y:nat) := - if y =? x - then Some v +Definition updEnv (x:nat) (mx:mType) (v: R) (E:env) (y:nat) := + if (y =? x) + then Some (v, mx) else E y. + + +(* Definition EnvEq: relation env := *) +(* fun E1 E2 => forall n : nat, *) +(* match (E1 n), (E2 n) with *) +(* | None, None => Is_true true *) +(* | Some (v1, m1), Some (v2, m2) => (v1 = v2) /\ ((meps m1) == (meps m2)) *) +(* | _, _ => Is_true false *) +(* end. *) + +(* Global Instance EnvEquivalence: Equivalence EnvEq. *) +(* Proof. *) +(* split; intros. *) +(* - intros E1 n. *) +(* case_eq (E1 n). *) +(* + intros [v m] hyp; auto. *) +(* split; auto. *) +(* apply Qeq_refl. *) +(* + intros. *) +(* unfold Is_true; trivial. *) +(* - intros E1 E2 hyp n. *) +(* case_eq (E1 n). *) +(* + intros [v1 m1] H1; auto. *) +(* case_eq (E2 n). *) +(* * intros [v2 m2] H2; auto. *) +(* pose proof (hyp n). *) +(* rewrite H1 in H. *) +(* rewrite H2 in H. *) +(* destruct H as [Hv Hm]. *) +(* split; symmetry; auto. *) +(* * intros. *) +(* pose proof (hyp n). *) +(* rewrite H1 in H0. *) +(* rewrite H in H0. *) +(* auto. *) +(* + intros. pose proof (hyp n). *) +(* rewrite H in H0. *) +(* case_eq (E2 n). intros [v2 m2] H2. *) +(* rewrite H2 in H0; auto. *) +(* intro H2. rewrite H2 in H0; auto. *) +(* - intros E1 E2 E3 H12 H23 n. *) +(* case_eq (E1 n). *) +(* + intros [v1 m1] H1; auto. *) +(* pose proof (H12 n) as H12. *) +(* pose proof (H23 n) as H23. *) +(* case_eq (E3 n). *) +(* * intros [v3 m3] H3; auto. *) +(* rewrite H1 in H12. *) +(* rewrite H3 in H23. *) +(* case_eq (E2 n). *) +(* intros [v2 m2] H2; auto. *) +(* rewrite H2 in H12. *) +(* rewrite H2 in H23. *) +(* destruct H12 as [H12v H12m]. *) +(* destruct H23 as [H23v H23m]. *) +(* split. *) +(* rewrite H12v; auto. *) +(* rewrite H12m; auto. *) +(* intros. *) +(* rewrite H in H12. *) +(* unfold Is_true in H12. *) +(* inversion H12. *) +(* * intros H3. *) +(* rewrite H1 in H12. *) +(* rewrite H3 in H23. *) +(* case_eq (E2 n). *) +(* intros [v2 m2] H2; auto. *) +(* rewrite H2 in H12; rewrite H2 in H23. *) +(* apply H23. *) +(* intro H2; auto. *) +(* rewrite H2 in H12; rewrite H2 in H23. *) +(* apply H12. *) +(* + intro H1; auto. *) +(* pose proof (H12 n) as H12. *) +(* pose proof (H23 n) as H23. *) +(* case_eq (E3 n). *) +(* * intros [v3 m3] H3; auto. *) +(* rewrite H1 in H12; rewrite H3 in H23. *) +(* case_eq (E2 n). *) +(* intros [v2 m2] H2; auto. *) +(* rewrite H2 in H12; rewrite H2 in H23; auto. *) +(* intros H2; rewrite H2 in H12; rewrite H2 in H23; auto. *) +(* * rewrite H1 in H12. *) +(* intros H3. *) +(* rewrite H3 in H23. *) +(* case_eq (E2 n). *) +(* intros [v2 m2] H2. *) +(* rewrite H2 in H12; rewrite H2 in H23; auto. *) +(* unfold Is_true in H12; inversion H12. *) +(* intro H2; rewrite H2 in H12; rewrite H2 in H23; auto. *) +(* Defined. *) \ No newline at end of file diff --git a/coq/Infra/Ltacs.v b/coq/Infra/Ltacs.v index 99dd3a84174ffa6bd39a4f2a476e74ca19ab7744..fdd0c30feea92b523aae6dc704b2e2403a4d8be5 100644 --- a/coq/Infra/Ltacs.v +++ b/coq/Infra/Ltacs.v @@ -2,7 +2,6 @@ Require Import Coq.Bool.Bool Coq.Reals.Reals. Require Import Daisy.Infra.RealSimps Daisy.Infra.NatSet. - Ltac iv_assert iv name:= assert (exists ivlo ivhi, iv = (ivlo, ivhi)) as name by (destruct iv; repeat eexists; auto). diff --git a/coq/Infra/MachineType.v b/coq/Infra/MachineType.v new file mode 100644 index 0000000000000000000000000000000000000000..dc9e2f020b685556e98bf5c379c2686470c732e2 --- /dev/null +++ b/coq/Infra/MachineType.v @@ -0,0 +1,330 @@ +Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals. +Require Import Coq.Reals.Reals Coq.micromega.Psatz. + +(** + Define machine types, and some tool functions. Needed for the + mixed-precision part, to be able to define a rounding operator. + **) +Inductive mType: Type := M0 | M32 | M64 | M128 | M256. + +Definition inj_eps_Q (e:mType) : Q := + match e with + | M0 => 0 + | M32 => (Qpower (2#1) (Zneg 24)) + | M64 => (Qpower (2#1) (Zneg 54)) + | M128 => (Qpower (2#1) (Zneg 113)) + | M256 => (Qpower (2#1) (Zneg 237)) + end. + +Definition meps := inj_eps_Q. + +Lemma inj_eps_pos : + forall e, 0 <= inj_eps_Q e. +Proof. + intro e. + case_eq e; intro; simpl inj_eps_Q; apply Qle_bool_iff; auto. +Qed. + +Lemma inj_eps_posR : + forall e, (0 <= Q2R (meps e))%R. +Proof. + intro. + assert (Q2R 0 = 0%R) by (unfold Q2R; simpl; lra). + rewrite <- H. + apply Qle_Rle. + apply inj_eps_pos. +Qed. + +(* Definition mTypeEqBool (m1:mType) (m2:mType) := *) +(* Qeq_bool (meps m1) (meps m2). *) + +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) := + match m1, m2 with + | M0, M0 => true + | M32, M32 => true + | M64, M64 => true + | M128, M128 => true + | M256, M256 => true + | _, _ => false + end. + +Lemma mTypeEqBool_sym (m1:mType) (m2:mType): + forall b, mTypeEqBool m1 m2 = b -> mTypeEqBool m2 m1 = b. +Proof. + intros. + destruct b, m1, m2; simpl; cbv; auto. +Qed. + +Lemma mTypeEqBool_refl (m:mType): + mTypeEqBool m m = true. +Proof. + intros. destruct m; cbv; 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. +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. +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. +Proof. + unfold isMorePrecise; simpl. + case_eq (mTypeEqBool m1 M0); intro hyp; [ auto | apply Qle_bool_iff; apply Qle_refl ]. +Qed. + +(* Definition isMorePrecise_rel (m1:mType) (m2:mType) := *) +(* Qle (meps m1) (meps m2). *) + + +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. + + +Definition computeJoin (m1:mType) (m2:mType) := + if (isMorePrecise m1 m2) then m1 else m2. + + + +(* Lemma eq_compat_join (m:mType) (m2:mType) (m1:mType) (m0:mType) : *) +(* mTypeEq m m2 -> *) +(* isJoinOf m m1 m0 = true -> *) +(* isJoinOf m2 m1 m0 = true. *) +(* Proof. *) +(* intros. *) +(* unfold isJoinOf in *. *) +(* case_eq (isMorePrecise m1 m0); intros; rewrite H1 in H0; auto; *) +(* apply mTypeEquivs in H0; apply mTypeEquivs; *) +(* [ apply (Equivalence_Transitive m2 m m1) | apply (Equivalence_Transitive m2 m m0) ]; *) +(* auto; apply (Equivalence_Symmetric m m2); auto. *) +(* Qed. *) + +(* Lemma M0_is_bot (m:mType): *) +(* isMorePrecise m M0 = true. *) +(* Proof. *) +(* unfold isMorePrecise. *) +(* destruct m. *) +(* simpl; auto. *) +(* Qed. *) + +(* (* Lemma ifM0isJoin_l (m:mType) (m1:mType) (m2:mType) : *) *) +(* (* (meps m) == 0 -> isJoinOf m m1 m2 = true -> mTypeEqBool M0 m1 = true. *) *) +(* (* Proof. *) *) +(* (* intros H0 H. *) *) +(* (* unfold isJoinOf in H. *) *) +(* (* case_eq (isMorePrecise m1 m2); intro Hyp; rewrite Hyp in H; simpl in H. *) *) +(* (* - auto. *) *) +(* (* unfold mTypeEqBool. *) *) +(* (* simpl (meps M0). *) *) +(* (* unfold mTypeEqBool in H. *) *) +(* (* rewrite H0 in H. *) *) +(* (* auto. *) *) +(* (* - unfold isMorePrecise in Hyp. *) *) +(* (* unfold mTypeEqBool in *. *) *) +(* (* apply Qeq_bool_iff in H. *) *) +(* (* symmetry in H. *) *) +(* (* apply Qeq_eq_bool in H. *) *) +(* (* rewrite H0 in H. *) *) +(* (* simpl (meps M0) in Hyp. *) *) +(* (* rewrite H in Hyp. *) *) +(* (* apply diff_true_false in Hyp. *) *) +(* (* inversion Hyp. *) *) +(* (* Qed. *) *) + + +(* (* Lemma ifM0isJoin_r (m:mType) (m1:mType) (m2:mType) : *) *) +(* (* (meps m) == 0 -> isJoinOf m m1 m2 = true -> mTypeEqBool M0 m2 = true. *) *) +(* (* Proof. *) *) +(* (* intros H0 H. *) *) +(* (* unfold isJoinOf in H. *) *) +(* (* case_eq (isMorePrecise m1 m2); intro Hyp; rewrite Hyp in H; simpl in H. *) *) +(* (* - unfold isMorePrecise in Hyp. *) *) +(* (* case_eq (mTypeEqBool m2 M0); intro H2; rewrite H2 in Hyp. *) *) +(* (* + unfold mTypeEqBool in *. *) *) +(* (* rewrite Qeq_bool_iff in *. *) *) +(* (* symmetry; auto. *) *) +(* (* + unfold mTypeEqBool in H; apply Qeq_bool_iff in H; symmetry in H; apply Qeq_eq_bool in H. *) *) +(* (* unfold mTypeEqBool in Hyp. *) *) +(* (* assert (Qeq_bool (meps m1) (meps M0) = true). *) *) +(* (* apply Qeq_bool_iff. *) *) +(* (* apply Qeq_bool_iff in H. *) *) +(* (* rewrite H0 in H. *) *) +(* (* rewrite H. *) *) +(* (* simpl meps. *) *) +(* (* lra. *) *) +(* (* rewrite H1 in Hyp; apply diff_false_true in Hyp; inversion Hyp. *) *) +(* (* - unfold mTypeEqBool in *. simpl in *. rewrite H0 in H. auto. *) *) +(* (* Qed. *) *) + + +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. + +Lemma ifM0isJoin_l (m:mType) (m1:mType) (m2:mType) : + m = M0 -> isJoinOf m m1 m2 = true -> m1 = 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. + - 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. +Qed. + + +Lemma ifM0isJoin_r (m:mType) (m1:mType) (m2:mType) : + m = M0 -> isJoinOf m m1 m2 = true -> m2 = 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. +Qed. + +Lemma ifM0isJoin (m1:mType) (m2:mType): + isJoinOf M0 m1 m2 = true -> m1 = M0 /\ m2 = M0. +Proof. + assert (M0 = M0) by auto. + intros; split. + - apply (ifM0isJoin_l M0 m1 m2); auto. + - apply (ifM0isJoin_r M0 m1 m2); 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. + +Lemma isJoinComputeJoin (M:mType) (m1:mType) (m2:mType) : + isJoinOf M m1 m2 = true -> + M = computeJoin m1 m2. +Proof. + intros. + unfold computeJoin. + unfold isJoinOf in H. + case_eq (isMorePrecise m1 m2); intros; auto; rewrite H0 in H; apply EquivEqBoolEq; auto. +Qed. + (* Lemma joinIsMP (m1:mType) (m2:mType) : *) +(* isMorePrecise (computeJoin m1 m2) m1 = true. *) +(* Proof. *) +(* unfold computeJoin. *) +(* case_eq (isMorePrecise m1 m2); intros. *) +(* apply isMorePrecise_refl. *) + +(* unfold isMorePrecise in *. *) +(* case_eq (mTypeEqBool m2 M0); intros; rewrite H0 in H; auto. *) +(* inversion H. *) +(* case_eq (mTypeEqBool m1 M0); intros; rewrite H1 in H; auto. *) +(* rewrite Qle_bool_iff. *) +(* apply Qnot_lt_le. *) + +(* intro. *) + +(* apply not_true_iff_false in H. *) + + +(* Lemma Qnot_lt_le : forall x y, ~ x y<=x. *) + +(* Lemma Qnot_le_lt : forall x y, ~ x<=y -> y ~ y<=x. *) + +(* Lemma Qle_not_lt : forall x y, x<=y -> ~ y Var R v - |Const n => Const (Q2R n) - |Unop o e1 => Unop o (toRExp e1) - |Binop o e1 e2 => Binop o (toRExp e1) (toRExp e2) - end. - -Fixpoint toRCmd (f:cmd Q) := - match f with - |Let x e g => Let x (toRExp e) (toRCmd g) - |Ret e => Ret (toRExp e) - end. +Require Import Daisy.IntervalArith Daisy.Infra.RealSimps. Lemma Q2R0_is_0: Q2R 0 = 0%R. @@ -153,15 +139,15 @@ Proof. unfold Q2RP; destruct iv; apply minAbs_impl_RminAbs. Qed. -Lemma mEps_geq_zero: - (0 <= Q2R RationalSimps.machineEpsilon)%R. -Proof. - rewrite <- Q2R0_is_0. - apply Qle_Rle. - unfold machineEpsilon. - apply Qle_bool_iff. - unfold Qle_bool; auto. -Qed. +(* Lemma mEps_geq_zero: *) +(* (0 <= Q2R RationalSimps.machineEpsilon)%R. *) +(* Proof. *) +(* rewrite <- Q2R0_is_0. *) +(* apply Qle_Rle. *) +(* unfold machineEpsilon. *) +(* apply Qle_bool_iff. *) +(* unfold Qle_bool; auto. *) +(* Qed. *) Lemma Q_case_div_to_R_case_div a b: (b < 0 \/ 0 < a)%Q -> diff --git a/coq/IntervalArithQ.v b/coq/IntervalArithQ.v index 09537c1393d19f3876b5826c2762a44e9f1cb531..24be82c46503d4e492af464df2b9a9aeaceca98e 100644 --- a/coq/IntervalArithQ.v +++ b/coq/IntervalArithQ.v @@ -46,6 +46,29 @@ Proof. rewrite H0. unfold Is_true; auto. Qed. +Definition isEqIntv (iv1:intv) (iv2:intv) := + (ivlo iv1 == ivlo iv2) /\ (ivhi iv1 == ivhi iv2). + +Lemma supIntvAntisym (iv1:intv) (iv2:intv) : + isSupersetIntv iv1 iv2 = true -> + isSupersetIntv iv2 iv1 = true -> + isEqIntv iv1 iv2. +Proof. + intros incl12 incl21. + unfold isSupersetIntv in *. + apply andb_true_iff in incl12. + apply andb_true_iff in incl21. + destruct incl12 as [incl12_low incl12_hi]. + destruct incl21 as [incl21_low incl21_hi]. + apply Qle_bool_iff in incl12_low. + apply Qle_bool_iff in incl12_hi. + apply Qle_bool_iff in incl21_low. + apply Qle_bool_iff in incl21_hi. + split. + - apply (Qle_antisym (ivlo iv1) (ivlo iv2)); auto. + - apply (Qle_antisym (ivhi iv1) (ivhi iv2)); auto. +Qed. + (** Definition of validity conditions for intv operations, Addition, Subtraction, Multiplication and Division **) diff --git a/coq/IntervalValidation.v b/coq/IntervalValidation.v index 2637dc8c4cbd0c57226c5af5257f518a024723c3..b91a005ae30d5577cd637b95adf4d6cb97eab899 100644 --- a/coq/IntervalValidation.v +++ b/coq/IntervalValidation.v @@ -7,17 +7,17 @@ **) Require Import Coq.QArith.QArith Coq.QArith.Qreals QArith.Qminmax Coq.Lists.List Coq.micromega.Psatz. Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps. -Require Import Daisy.Infra.Ltacs Daisy.Infra.RealSimps. +Require Import Daisy.Infra.Ltacs Daisy.Infra.RealSimps Daisy.Typing. Require Export Daisy.IntervalArithQ Daisy.IntervalArith Daisy.ssaPrgs. Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond) (validVars:NatSet.t) := let (intv, _) := absenv e in match e with - | Var _ v => + | Var _ _ v => if NatSet.mem v validVars then true else isSupersetIntv (P v) intv && (Qleb (ivlo (P v)) (ivhi (P v))) - | Const n => isSupersetIntv (n,n) intv + | Const _ n => isSupersetIntv (n,n) intv | Unop o f => if validIntervalbounds f absenv P validVars then @@ -60,31 +60,41 @@ Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond) (vali else false 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... *) end. Fixpoint validIntervalboundsCmd (f:cmd Q) (absenv:analysisResult) (P:precond) (validVars:NatSet.t) :bool:= match f with - | Let x e g => + | Let m x e g => if (validIntervalbounds e absenv P validVars && - Qeq_bool (fst (fst (absenv e))) (fst (fst (absenv (Var Q x)))) && - Qeq_bool (snd (fst (absenv e))) (snd (fst (absenv (Var Q x))))) + Qeq_bool (fst (fst (absenv e))) (fst (fst (absenv (Var Q m x)))) && + Qeq_bool (snd (fst (absenv e))) (snd (fst (absenv (Var Q m x))))) then validIntervalboundsCmd g absenv P (NatSet.add x validVars) else false |Ret e => validIntervalbounds e absenv P validVars end. -Theorem ivbounds_approximatesPrecond_sound f absenv P V: +Theorem ivbounds_approximatesPrecond_sound f absenv P V Gamma: validIntervalbounds f absenv P V = true -> - forall v, NatSet.In v (NatSet.diff (usedVars f) V) -> - Is_true(isSupersetIntv (P v) (fst (absenv (Var Q v)))). + (exists mF, validType Gamma f mF) -> + forall v, NatSet.In v (NatSet.diff (Expressions.usedVars f) V) -> + exists m, Gamma (Var Q m v) = Some m /\ + Is_true(isSupersetIntv (P v) (fst (absenv (Var Q m v)))). Proof. induction f; unfold validIntervalbounds. - - intros approx_true v v_in_fV; simpl in *. + - simpl. intros approx_true valid_tf v v_in_fV; simpl in *. + inversion valid_tf; subst. rewrite NatSet.diff_spec in v_in_fV. rewrite NatSet.singleton_spec in v_in_fV; destruct v_in_fV; subst. - destruct (absenv (Var Q n)); simpl in *. + destruct valid_tf as [mF valid_tf]. + inversion valid_tf; subst. + exists mF; split; auto. + destruct (absenv (Var Q mF n)); simpl in *. case_eq (NatSet.mem n V); intros case_mem; rewrite case_mem in approx_true; simpl in *. + rewrite NatSet.mem_spec in case_mem. @@ -92,34 +102,50 @@ Proof. + apply Is_true_eq_left in approx_true. apply andb_prop_elim in approx_true. destruct approx_true; auto. - - intros approx_true v0 v_in_fV; simpl in *. - inversion v_in_fV. - - intros approx_unary_true v v_in_fV. - unfold freeVars in v_in_fV. + - intros approx_true valid_tf v0 v_in_fV; simpl in *. + inversion v_in_fV. + - intros approx_unary_true valid_tf v v_in_fV; simpl in *. apply Is_true_eq_left in approx_unary_true. + simpl in *. destruct (absenv (Unop u f)); destruct (absenv f); simpl in *. apply andb_prop_elim in approx_unary_true. destruct approx_unary_true. apply IHf; try auto. - apply Is_true_eq_true; auto. - - intros approx_bin_true v v_in_fV. + + apply Is_true_eq_true; auto. + + destruct valid_tf as [mF valid_tf]. + inversion valid_tf; subst; auto. + exists mF; auto. + - intros approx_bin_true valid_tf v v_in_fV. simpl in v_in_fV. rewrite NatSet.diff_spec in v_in_fV. destruct v_in_fV as [ v_in_fV v_not_in_V]. rewrite NatSet.union_spec in v_in_fV. apply Is_true_eq_left in approx_bin_true. - destruct (absenv (Binop b f1 f2)); destruct (absenv f1); destruct (absenv f2); simpl in *. + destruct valid_tf as [mf valid_tf]. + inversion valid_tf; subst. + destruct (absenv (Binop b f1 f2)); destruct (absenv f1); + destruct (absenv f2); simpl in *. apply andb_prop_elim in approx_bin_true. destruct approx_bin_true. apply andb_prop_elim in H. destruct H. destruct v_in_fV. - + apply IHf1; auto. - apply Is_true_eq_true; auto. - rewrite NatSet.diff_spec; split; auto. - + apply IHf2; auto. - apply Is_true_eq_true; auto. - rewrite NatSet.diff_spec; split; auto. + + apply IHf1; try auto. + * apply Is_true_eq_true; auto. + * eauto. + * rewrite NatSet.diff_spec; split; auto. + + apply IHf2; try auto. + * apply Is_true_eq_true; auto. + * eauto. + * rewrite NatSet.diff_spec; split; auto. + - intros approx_rnd_true [mf valid_tf] v v_in_fV. + simpl in *; destruct (absenv (Downcast m f)); destruct (absenv f). + apply Is_true_eq_left in approx_rnd_true. + apply andb_prop_elim in approx_rnd_true. + destruct approx_rnd_true. + apply IHf; auto. + apply Is_true_eq_true in H; try auto. + inversion valid_tf; subst; eauto. Qed. Corollary Q2R_max4 a b c d: @@ -137,31 +163,121 @@ Qed. Ltac env_assert absenv e name := assert (exists iv err, absenv e = (iv,err)) as name by (destruct (absenv e); repeat eexists; auto). -Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) fVars dVars E: - forall vR, + +Lemma validBoundsDiv_uneq_zero e1 e2 absenv P V ivlo_e2 ivhi_e2 err: + absenv e2 = ((ivlo_e2,ivhi_e2), err) -> + validIntervalbounds (Binop Div e1 e2) absenv P V = true -> + (ivhi_e2 < 0) \/ (0 < ivlo_e2). +Proof. + intros absenv_eq validBounds. + unfold validIntervalbounds in validBounds. + env_assert absenv (Binop Div e1 e2) abs_div; destruct abs_div as [iv_div [err_div abs_div]]. + env_assert absenv e1 abs_e1; destruct abs_e1 as [iv_e1 [err_e1 abs_e1]]. + rewrite abs_div, abs_e1, absenv_eq in validBounds. + repeat (rewrite <- andb_lazy_alt in validBounds). + apply Is_true_eq_left in validBounds. + apply andb_prop_elim in validBounds. + destruct validBounds as [_ validBounds]; apply andb_prop_elim in validBounds. + destruct validBounds as [nodiv0 _]. + apply Is_true_eq_true in nodiv0. + unfold isSupersetIntv in *; simpl in *. + apply le_neq_bool_to_lt_prop; auto. +Qed. + +(* Lemma validVarsUnfolding_l (E:env) (absenv:analysisResult) (f1 f2: exp Q) dVars (b:binop) m0: *) +(* (typeMap (Binop b f1 f2)) (Binop b f1 f2) = Some m0 -> *) +(* (forall (v : NatSet.elt) (m : mType), *) +(* NatSet.mem v dVars = true -> *) +(* typeMap (Binop b f1 f2) (Var Q m v) = Some m -> *) +(* exists vR : R, *) +(* E v = Some (vR, M0) /\ *) +(* (Q2R (fst (fst (absenv (Var Q m v)))) <= vR <= Q2R (snd (fst (absenv (Var Q m v)))))%R) *) +(* -> *) +(* (forall (v : NatSet.elt) (m : mType), *) +(* NatSet.mem v dVars = true -> *) +(* typeMap f1 (Var Q m v) = Some m -> *) +(* exists vR : R, *) +(* E v = Some (vR, M0) /\ *) +(* (Q2R (fst (fst (absenv (Var Q m v)))) <= vR <= Q2R (snd (fst (absenv (Var Q m v)))))%R). *) +(* Proof. *) +(* intros. *) +(* specialize (H0 v m H1). *) +(* case_eq (typeMap f2 (Var Q m v)); intros; auto. *) +(* - case_eq (mTypeEqBool m m1); intros. *) +(* + (*apply EquivEqBoolEq in H4. ; rewrite <- H4 in H3.*) *) +(* assert (typeMap (Binop b f1 f2) (Var Q m v) = Some m). *) +(* simpl typeMap. rewrite H2. *) +(* auto. *) +(* specialize (H0 H5); auto. *) +(* + pose proof (typeMapVarDet _ _ _ H3). *) +(* rewrite H5 in H4. *) +(* rewrite mTypeEqBool_refl in H4. *) +(* inversion H4. *) +(* - assert (typeMap (Binop b f1 f2) (Var Q m v) = Some m) by (simpl; rewrite H2; auto). *) +(* specialize (H0 H4). *) +(* auto. *) +(* Qed. *) + +(* Lemma validVarsUnfolding_r (E:env) (absenv:analysisResult) (f1 f2: exp Q) dVars (b:binop) m0: *) +(* (typeMap (Binop b f1 f2)) (Binop b f1 f2) = Some m0 -> *) +(* (forall (v : NatSet.elt) (m : mType), *) +(* NatSet.mem v dVars = true -> *) +(* typeMap (Binop b f1 f2) (Var Q m v) = Some m -> *) +(* exists vR : R, *) +(* E v = Some (vR, M0) /\ *) +(* (Q2R (fst (fst (absenv (Var Q m v)))) <= vR <= Q2R (snd (fst (absenv (Var Q m v)))))%R) *) +(* -> *) +(* (forall (v : NatSet.elt) (m : mType), *) +(* NatSet.mem v dVars = true -> *) +(* typeMap f2 (Var Q m v) = Some m -> *) +(* exists vR : R, *) +(* E v = Some (vR, M0) /\ *) +(* (Q2R (fst (fst (absenv (Var Q m v)))) <= vR <= Q2R (snd (fst (absenv (Var Q m v)))))%R). *) +(* Proof. *) +(* intros. *) +(* specialize (H0 v m H1). *) +(* case_eq (typeMap f1 (Var Q m v)); intros; auto. *) +(* - case_eq (mTypeEqBool m1 m); intros. *) +(* + (*apply EquivEqBoolEq in H4. ; rewrite <- H4 in H3.*) *) +(* assert (typeMap (Binop b f1 f2) (Var Q m v) = Some m). *) +(* simpl typeMap; rewrite H3. *) +(* apply EquivEqBoolEq in H4; rewrite H4; auto. *) +(* specialize (H0 H5); auto. *) +(* + pose proof (typeMapVarDet _ _ _ H3). *) +(* rewrite H5 in H4. *) +(* rewrite mTypeEqBool_refl in H4. *) +(* inversion H4. *) +(* - assert (typeMap (Binop b f1 f2) (Var Q m v) = Some m) by (simpl; rewrite H2,H3; auto). *) +(* specialize (H0 H4). *) +(* auto. *) +(* Qed. *) + +Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) fVars dVars (E:env) Gamma: + forall vR m, + validType Gamma f m -> validIntervalbounds f absenv P dVars = true -> - (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) -> - NatSet.Subset (NatSet.diff (usedVars f) dVars) fVars -> + (forall v mV, NatSet.mem v dVars = true -> + exists vR mv, E v = Some (vR, M0) /\ Gamma (Var Q mv v) = Some mV /\ + (Q2R (fst (fst (absenv (Var Q mV v)))) <= vR <= Q2R (snd (fst (absenv (Var Q mV v)))))%R) -> + NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars -> (forall v, NatSet.mem v fVars = true -> - exists vR, E v = Some vR /\ + exists vR, E v = Some (vR, M0) /\ (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> - eval_exp 0%R E (toRExp f) vR -> - (Q2R (fst (fst(absenv f))) <= vR <= Q2R (snd (fst (absenv f))))%R. + eval_exp E (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 freeVars_subset valid_freeVars eval_f. + induction f; intros vR mf typing_ok valid_bounds valid_definedVars usedVars_subset valid_usedVars eval_f. - unfold validIntervalbounds in valid_bounds. - env_assert absenv (Var Q n) absenv_var. + env_assert absenv (Var Q m n) absenv_var. destruct absenv_var as [ iv [err absenv_var]]. - specialize (valid_freeVars n). - rewrite absenv_var in *; simpl in *. + 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 precond_sound]]. - rewrite E_n_eq in *. - inversion H0; subst. + + specialize (valid_definedVars n m case_mem). + inversion typing_ok; subst. + destruct valid_definedVars as [vR' [mv [E_n_eq [gamma_n iv_n]]]]. + rewrite H2 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. @@ -175,19 +291,19 @@ Proof. * assert (NatSet.In n (NatSet.singleton n)) as in_singleton by (rewrite NatSet.singleton_spec; auto). rewrite NatSet.mem_spec. - hnf in freeVars_subset. - apply freeVars_subset. + 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_freeVars in_fVars); - destruct valid_freeVars as [vR' [vR_def P_valid]]. - rewrite vR_def in H0; inversion H0; subst. + * specialize (valid_usedVars in_fVars); + destruct valid_usedVars as [vR' [vR_def P_valid]]. + rewrite vR_def in H2; inversion H2; subst. lra. - unfold validIntervalbounds in valid_bounds. - destruct (absenv (Const v)) as [intv err]; simpl. + 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]. @@ -203,10 +319,11 @@ Proof. 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. - rewrite absenv_unop 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. @@ -214,7 +331,9 @@ Proof. 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 freeVars_subset valid_freeVars H2). + + (*assert (typeMap f f = Some mf) as typing_f_ok by (simpl in typing_ok; rewrite expEqBool_refl in typing_ok; apply typeGivesTypeMap; auto).*) + inversion typing_ok; subst. + specialize (IHf v1 mf H1 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. @@ -232,7 +351,9 @@ Proof. * eapply Rle_trans. Focus 2. apply valid_hi. rewrite Q2R_opp; lra. - + specialize (IHf v1 valid_rec valid_definedVars freeVars_subset valid_freeVars H3). + + (*assert (typeMap f f = Some mf) as typing_f_ok by (simpl in typing_ok; rewrite expEqBool_refl in typing_ok; apply typeGivesTypeMap; auto).*) + inversion typing_ok; subst. + specialize (IHf v1 mf H2 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]. @@ -273,7 +394,7 @@ Proof. 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. + apply Rlt_Qlt in nodiv0_pos; apply Rle_Qle in H3; lra. } { eapply Rle_trans. Focus 2. apply valid_hi. @@ -298,8 +419,9 @@ Proof. 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. + apply Rlt_Qlt in nodiv0_pos; apply Rle_Qle in H3; lra. } + { rewrite Q2R0_is_0 in H1; auto. } - inversion eval_f; subst. rewrite delta_0_deterministic in eval_f; auto. rewrite delta_0_deterministic; auto. @@ -307,6 +429,7 @@ Proof. 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. @@ -314,22 +437,33 @@ Proof. apply andb_prop_elim in valid_rec. destruct valid_rec as [valid_e1 valid_e2]. apply Is_true_eq_true in valid_e1; apply Is_true_eq_true in valid_e2. - specialize (IHf1 v1 valid_e1 valid_definedVars); - specialize (IHf2 v2 valid_e2 valid_definedVars). + destruct m1; destruct m2; cbv in H2; inversion H2. + inversion typing_ok; subst. + + (* pose proof (typeMap_gives_type _ typing_ok). *) + (* simpl in H. case_eq (typeExpression f1); intros; rewrite H0 in H; [ | inversion H ]. *) + (* case_eq (typeExpression f2); intros; rewrite H1 in H; inversion H. *) + (* pose proof (validVarsUnfolding_l _ _ _ _ _ _ typing_ok valid_definedVars) as valid_definedVars_f1. *) + (* pose proof (validVarsUnfolding_r _ _ _ _ _ _ typing_ok valid_definedVars) as valid_definedVars_f2. *) + (* pose proof (binop_type_unfolding _ _ _ typing_ok) as subtypes. *) + (* destruct subtypes as [mf1 [mf2 [typing_f1 [typing_f2 join_f1_f2]]]]. *) + (* apply typeGivesTypeMap in H0. apply typeGivesTypeMap in H1. *) + specialize (IHf1 v1 m1 H4 valid_e1 valid_definedVars). + specialize (IHf2 v2 m2 H8 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 freeVars_subset. + 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_freeVars not_dVar]. + 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 freeVars_subset. + 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. @@ -345,7 +479,7 @@ Proof. 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. + - eapply Rle_trans. (*rewrite absenv_bin;*) apply valid_lo. unfold ivlo. unfold addIntv. simpl in valid_add_lo. repeat rewrite <- Q2R_plus in valid_add_lo. @@ -353,7 +487,7 @@ Proof. unfold absIvUpd; auto. - eapply Rle_trans. Focus 2. - apply valid_hi. + (*rewrite absenv_bin;*) apply valid_hi. unfold ivlo, addIntv. simpl in valid_add_hi. repeat rewrite <- Q2R_plus in valid_add_hi. @@ -369,7 +503,7 @@ Proof. 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. + - eapply Rle_trans. (*rewrite absenv_bin;*) apply valid_lo. unfold ivlo. unfold subtractIntv. simpl in valid_sub_lo. repeat rewrite <- Rsub_eq_Ropp_Rplus in valid_sub_lo. @@ -378,7 +512,7 @@ Proof. unfold absIvUpd; auto. - eapply Rle_trans. Focus 2. - apply valid_hi. + (*rewrite absenv_bin;*) apply valid_hi. unfold ivlo, addIntv. simpl in valid_sub_hi. repeat rewrite <- Rsub_eq_Ropp_Rplus in valid_sub_hi. @@ -395,7 +529,7 @@ Proof. 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. + - eapply Rle_trans. (*rewrite absenv_bin;*) apply valid_lo. unfold ivlo. unfold multIntv. simpl in valid_mul_lo. repeat rewrite <- Q2R_mult in valid_mul_lo. @@ -403,7 +537,7 @@ Proof. unfold absIvUpd; auto. - eapply Rle_trans. Focus 2. - apply valid_hi. + (*rewrite absenv_bin;*) apply valid_hi. unfold ivlo, addIntv. simpl in valid_mul_hi. repeat rewrite <- Q2R_mult in valid_mul_hi. @@ -447,7 +581,7 @@ Proof. rewrite ivlo2_0 in H0. lra. } { split. - - eapply Rle_trans. apply valid_lo. + - eapply Rle_trans. (*rewrite absenv_bin;*) apply valid_lo. unfold ivlo. unfold multIntv. simpl in valid_div_lo. rewrite <- Q2R_inv in valid_div_lo; [ | auto]. @@ -456,112 +590,131 @@ Proof. rewrite <- Q2R_min4 in valid_div_lo; auto. - eapply Rle_trans. Focus 2. - apply valid_hi. + (*rewrite absenv_bin;*) 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 erasure 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. + inversion typing_ok; subst. + eapply IHf; try eauto. + apply Is_true_eq_true in vI1; auto. Qed. -Fixpoint getRetExp (V:Type) (f:cmd V) := - match f with - |Let x e g => getRetExp g - | Ret e => e - end. +(* Unused, proof not up-to-date *) +(* Theorem validIntervalboundsCmd_sound (f:cmd Q) (absenv:analysisResult): *) +(* forall E vR fVars dVars outVars elo ehi err P, *) +(* ssaPrg f (NatSet.union fVars dVars) outVars -> *) +(* bstep (toREvalCmd (toRCmd f)) E vR M0 -> *) +(* (forall v m, NatSet.mem v dVars = true -> *) +(* exists vR, *) +(* E v = Some (vR, m) /\ *) +(* (Q2R (fst (fst (absenv (Var Q m v)))) <= vR <= Q2R (snd (fst (absenv (Var Q m v)))))%R) -> *) +(* (forall v m, NatSet.mem v fVars = true -> *) +(* exists vR, *) +(* E v = Some (vR, m) /\ *) +(* (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> *) +(* 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. *) +(* Proof. *) +(* induction f; *) +(* intros * ssa_f eval_f dVars_sound fVars_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 m 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. *) +(* + admit. *) +(* + *) +(* intros v0 m0 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. *) +(* 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. *) +(* 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. *) +(* - unfold validIntervalboundsCmd in valid_bounds_f. *) +(* inversion eval_f; subst. *) +(* unfold updEnv. *) +(* assert (Q2R (fst (fst (absenv (erasure e)))) <= vR <= Q2R (snd (fst (absenv (erasure e)))))%R. *) +(* + simpl in valid_bounds_f; eapply validIntervalbounds_sound; eauto. *) +(* + simpl in *. rewrite absenv_f in *; auto. *) +(* Qed. *) -Theorem validIntervalboundsCmd_sound (f:cmd Q) (absenv:analysisResult): - forall E vR fVars dVars outVars elo ehi err P, - ssa f (NatSet.union fVars dVars) outVars -> - bstep (toRCmd f) E 0%R vR -> - (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) -> - NatSet.Subset (NatSet.diff (freeVars f) dVars) fVars -> - validIntervalboundsCmd f absenv P dVars = true -> - absenv (getRetExp f) = ((elo, ehi), err) -> - (Q2R elo <= vR <= Q2R ehi)%R. -Proof. - induction f; - intros E vR fVars dVars outVars elo ehi err P ssa_f eval_f dVars_sound - fVars_valid freeVars_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 freeVars_subset. - hnf. intros a in_freeVars. - apply freeVars_subset. - rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec. - rewrite NatSet.diff_spec in in_freeVars. - destruct in_freeVars as [ in_freeVars not_dVar]. - repeat split; try auto. - { hnf; intros; subst. - specialize (H2 n in_freeVars). - rewrite <- NatSet.mem_spec in H2. - rewrite H2 in H5; 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 freeVars_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. - - unfold validIntervalboundsCmd in valid_bounds_f. - inversion eval_f; subst. - unfold updEnv. - assert (Q2R (fst (fst (absenv e))) <= vR <= Q2R (snd (fst (absenv e))))%R. - + eapply validIntervalbounds_sound; eauto. - + simpl in *. rewrite absenv_f in *; auto. -Qed. diff --git a/coq/Typing.v b/coq/Typing.v new file mode 100644 index 0000000000000000000000000000000000000000..9a31ffec351f863a5f880ae6b6e47096accfe329 --- /dev/null +++ b/coq/Typing.v @@ -0,0 +1,1286 @@ +Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.Qreals Coq.MSets.MSets. +Require Import Daisy.Infra.RealRationalProps Daisy.Expressions Daisy.Infra.Ltacs Daisy.Commands Daisy.ssaPrgs. +Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet Daisy.IntervalArithQ Daisy.IntervalArith Daisy.Infra.MachineType. + +Fixpoint typeExpression (V:Type) (e:exp V) : option mType := + match e with + | Var _ m v => Some m + | Const m n => Some m + | Unop u e1 => typeExpression e1 + | Binop b e1 e2 => + let tm1 := typeExpression e1 in + let tm2 := typeExpression e2 in + match tm1, tm2 with + | Some m1, Some m2 => Some (computeJoin m1 m2) + | _, _=> None + end + | Downcast m e1 => + let tm1 := typeExpression e1 in + match tm1 with + |Some m1 => if (isMorePrecise m1 m) then Some m else None + |_ => None + end + end. + +Fixpoint typeMap (e:exp Q) (e': exp Q) : option mType := + match e with + | Var _ m v => if expEqBool e e' then Some m else None + | Const m n => if expEqBool e e' then Some m else None + | Unop u e1 => if expEqBool e e' then typeExpression e else typeMap e1 e' + | Binop b e1 e2 => if expEqBool e e' then typeExpression e + else + match (typeMap e1 e') with + | None => typeMap e2 e' + | x => x + end + | Downcast m e1 => if expEqBool e e' then typeExpression (Downcast m e1) else typeMap e1 e' + end. + +Lemma typeMapVarDet e m m' v: + typeMap e (Var Q m v) = Some m' -> + m = m'. +Proof. + revert e; induction e; intros. + - simpl in H. + case_eq (mTypeEqBool m0 m && (n =? v)); intros; rewrite H0 in H. + apply andb_true_iff in H0; destruct H0. + inversion H; subst. + apply EquivEqBoolEq in H0; subst; auto. + inversion H. + - simpl in H. inversion H. + - simpl in H. apply IHe; auto. + - simpl in H. + case_eq (typeMap e1 (Var Q m v)); intros; rewrite H0 in H. + + inversion H; subst. + apply IHe1; auto. + + apply IHe2; auto. + - simpl in H. apply IHe; auto. +Qed. + +Lemma typeGivesTypeMap e m : + typeExpression e = Some m -> + typeMap e e = Some m. +Proof. + intros; induction e; simpl in *; auto. + - rewrite mTypeEqBool_refl, <- beq_nat_refl; simpl; auto. + - rewrite mTypeEqBool_refl. + assert (Qeq_bool v v = true) by (apply Qeq_bool_iff; lra). + rewrite H0; simpl; auto. + - assert (unopEqBool u u = true) by (destruct u; auto). + rewrite H0, expEqBool_refl; simpl; auto. + - pose proof (expEqBool_refl (Binop b e1 e2)). + simpl in H0; rewrite H0. + auto. + - rewrite mTypeEqBool_refl,expEqBool_refl. + simpl; auto. +Qed. + +Lemma typeMap_gives_type: + forall e m, + typeMap e e = Some m -> + typeExpression e = Some m. +Proof. + intros e; induction e; intros; simpl in *; try auto. + - rewrite mTypeEqBool_refl in H. + rewrite <- beq_nat_refl in H. simpl in *. auto. + - assert (Qeq_bool v v = true) as Qeq_bool_refl by (apply Qeq_bool_iff; lra). + rewrite Qeq_bool_refl,mTypeEqBool_refl in H. + simpl in H; auto. + - assert (unopEqBool u u = true) as unopEqBool_refl by (destruct u; auto). + rewrite unopEqBool_refl,expEqBool_refl in H; simpl in H; auto. + - assert (binopEqBool b b = true) as binopEqBool_refl by (destruct b; auto). + rewrite binopEqBool_refl,expEqBool_refl,expEqBool_refl in H; simpl in H; auto. + - rewrite mTypeEqBool_refl,expEqBool_refl in H; simpl in H; auto. +Qed. + +Lemma unop_neq u e: + expEqBool (Unop u e) e = true -> False . +Proof. + induction e; intros; simpl in *; try congruence. + case_eq ( unopEqBool u u0); intros; rewrite H0 in *; simpl in *; try congruence. + apply IHe. + assert (u = u0) by (destruct u; destruct u0; cbv in H0; inversion H0; auto). + subst. auto. +Qed. + +Lemma t e u m: + typeMap e e = Some m -> + typeMap (Unop u e) e = Some m. +Proof. + intros. + simpl. destruct e; try auto. + case_eq (expEqBool (Unop u0 e) e); intros case_exp. + - exfalso. eapply unop_neq; eauto. + - rewrite andb_false_r. + assumption. +Qed. + +Inductive validType (Gamma:exp Q -> option mType) : exp Q -> mType -> Prop := +|tVar m v: + Gamma (Var Q m v) = Some m -> validType Gamma (Var Q m v) m +|tConst m n: + Gamma (Const m n) = Some m -> validType Gamma (Const m n) m +|tUnop u e1 m: + validType Gamma e1 m -> + Gamma (Unop u e1) = Some m -> + validType Gamma (Unop u e1) m +|tBinop b e1 e2 m m1 m2: + validType Gamma e1 m1 -> + validType Gamma e2 m2 -> + m = computeJoin m1 m2 -> + Gamma (Binop b e1 e2) = Some m -> + validType Gamma (Binop b e1 e2) m +|tDowncast m e1 m1: + validType Gamma e1 m1 -> + isMorePrecise m1 m = true -> + Gamma (Downcast m e1) = Some m -> + validType Gamma (Downcast m e1) m. + +Lemma valid_typing e m: + typeExpression e = Some m -> + validType (fun e => typeExpression e) e m. +Proof. + revert m; induction e; intros; simpl in *. + - inversion H; constructor; auto. + - inversion H; constructor; auto. + - constructor; simpl; auto. + - case_eq (typeExpression e1); intros; rewrite H0 in H; [ | inversion H ]. + case_eq (typeExpression e2); intros; rewrite H1 in H; inversion H; subst. + specialize (IHe1 _ H0). specialize (IHe2 _ H1). + econstructor; try eauto. + simpl; rewrite H0, H1; auto. + - case_eq (typeExpression e); intros; rewrite H0 in H; [| inversion H]. + case_eq (isMorePrecise m1 m); intros; rewrite H1 in H; [| inversion H]. + inversion H; subst. + econstructor; try eauto. + simpl; rewrite H0,H1; auto. +Qed. + + +Inductive validTypeCmd (Gamma:exp Q -> option mType) : cmd Q -> mType -> Prop := +|tRet m e: + validType Gamma e m -> validTypeCmd Gamma (Ret e) m +|tLet m x e c mc: + validType Gamma e m -> + validType Gamma (Var Q m x) m -> + validTypeCmd Gamma c mc -> + validTypeCmd Gamma (Let m x e c) mc. + +Fixpoint typeCmd (f:cmd Q) (vartype:nat -> option mType) : option mType := + match f with + |Let m n e c => match typeExpression e with + |Some m' => if mTypeEqBool m m' then typeCmd c (fun f => if (n =? f) then Some m else vartype f) + else None + |None => None + end + |Ret e => typeExpression e (* TODO vartype *) + end. + +Fixpoint typeMapCmd (f:cmd Q) (f':exp Q) : option mType := + match f with + |Let m n e c => if expEqBool f' (Var Q m n) then + match typeMap e f' with + |None => None + |Some m1 => if mTypeEqBool m1 m then Some m else None + end + else + let te := typeMap e in + let tc := typeMapCmd c in + match (te f'), (tc f') with + |Some m1, Some m2 => if mTypeEqBool m1 m2 then Some m1 else None + |Some m1, None => Some m1 + |None, Some m2 => Some m2 + |None, None => None + end + |Ret e => (typeMap e) f' + end. + + + +Lemma Gamma_strengthening e m Gamma1 Gamma2: + (forall e m, Gamma1 e = Some m -> Gamma2 e = Some m ) -> + validType Gamma1 e m -> + validType Gamma2 e m. +Proof. + revert Gamma1 Gamma2 m; induction e; + intros; + inversion H0; subst; + econstructor; eauto. +Qed. + +Definition GammaStronger (Gamma1 Gamma2:exp Q -> option mType):= + forall e m, Gamma1 e = Some m -> Gamma2 e = Some m. + + + +Lemma binop_neq_l b e1 e2: + expEqBool (Binop b e1 e2) e1 = false. +Admitted. + +Lemma binop_neq_r b e1 e2: + expEqBool (Binop b e1 e2) e2 = false. +Admitted. + +Lemma downcast_neq m e: + expEqBool (Downcast m e) e = false. +Admitted. + +Lemma typeExpressionIsSound E e v m: + eval_exp E (toRExp e) v m -> + typeExpression e = Some m. +Proof. + revert v m; induction e; intros * eval_e. + - simpl. inversion eval_e; subst; auto. + - simpl. inversion eval_e; subst; auto. + - simpl. + inversion eval_e; subst. + + eapply IHe; eauto. + + eapply IHe; eauto. + - simpl. + inversion eval_e; subst. + specialize (IHe1 _ _ H3). + specialize (IHe2 _ _ H6). + rewrite IHe1, IHe2. + auto. + - inversion eval_e; subst; simpl. + specialize (IHe _ _ H5); rewrite IHe. + rewrite H1; auto. +Qed. + + + +Lemma validTypeMap e m vF E2: + eval_exp E2 (toRExp e) vF m -> validType (typeMap e) e m. +Proof. + revert m vF; induction e; intros * eval_e. + - inversion eval_e; subst. + econstructor; eauto. + unfold typeMap; rewrite expEqBool_refl; auto. + - inversion eval_e; subst. + econstructor; eauto. + unfold typeMap; rewrite expEqBool_refl; auto. + - inversion eval_e; subst. + + specialize (IHe _ _ H3). + econstructor; eauto. + * eapply Gamma_strengthening; auto. + Focus 2. eauto. + intros. unfold typeMap. + assert (expEqBool (Unop Neg e) e0 = false) by admit. + rewrite H0; auto. + * simpl; rewrite expEqBool_refl. + eapply typeExpressionIsSound; eauto. + + specialize (IHe _ _ H4). + econstructor; eauto. + * eapply Gamma_strengthening; auto. + Focus 2. eauto. + intros. unfold typeMap. + assert (expEqBool (Unop Inv e) e0= false) by admit. + rewrite H0; auto. + * simpl; rewrite expEqBool_refl. + eapply typeExpressionIsSound; eauto. + - inversion eval_e; subst. + econstructor; eauto. + + specialize (IHe1 _ _ H3). + eapply Gamma_strengthening. + Focus 2. eapply IHe1. + intros. unfold typeMap. + assert (expEqBool (Binop b e1 e2) e = false) by admit. + rewrite H0. + unfold typeMap in H; rewrite H. + auto. + + specialize (IHe2 _ _ H6). + eapply Gamma_strengthening. + Focus 2. eapply IHe2. + intros. unfold typeMap. + assert (expEqBool (Binop b e1 e2) e = false) by admit. + rewrite H0. + unfold typeMap in H; rewrite H. + case_eq (typeMap e1 e); intros; unfold typeMap in H1; rewrite H1. + * (* todo: need to change typeMap *) admit. + * auto. + + unfold typeMap; rewrite expEqBool_refl. + eapply typeExpressionIsSound; eauto. + - inversion eval_e; subst. + econstructor; eauto. + + eapply Gamma_strengthening. + Focus 2. eapply IHe; eauto. + intros. unfold typeMap. + assert (expEqBool (Downcast m0 e) e0 = false) by admit. + rewrite H0. + unfold typeMap in H. auto. + + unfold typeMap; rewrite expEqBool_refl. + eapply typeExpressionIsSound; eauto. +Admitted. + +Lemma typeCmdIsSound f E v m cont: + bstep (toRCmd f) E v m -> typeCmd f cont = Some m. +Proof. + revert cont E v m; induction f; intros. + - inversion H; subst. + specialize (IHf (fun n' => if n =? n' then Some m else cont n') _ _ _ H8). + simpl. + pose proof (typeExpressionIsSound _ H7) as t_e; rewrite t_e. + rewrite mTypeEqBool_refl. + rewrite IHf. + auto. + - simpl. + inversion H; subst. + eapply typeExpressionIsSound; eauto. +Qed. + +Lemma typeMapCmdValid f E v m: + bstep (toRCmd f) E v m -> validTypeCmd (typeMapCmd f) f m. +Proof. + revert E v m; induction f; intros * bstep_f. + - inversion bstep_f; subst. + econstructor; eauto. + + pose proof (validTypeMap _ H6). + eapply Gamma_strengthening. + Focus 2. eapply H. + intros. simpl. rewrite H0. + case_eq (expEqBool e0 (Var Q m n)); intros eq_e_varn. + * admit. + * admit. + + econstructor; eauto. +Admitted. + +(* Fixpoint isSubExpression (e':exp Q) (e:exp Q) := *) +(* orb (expEqBool e e') *) +(* (match e with *) +(* |Var _ _ _ => false *) +(* |Const _ _ => false *) +(* |Unop o1 e1 => isSubExpression e' e1 *) +(* |Binop b e1 e2 => orb (isSubExpression e' e1) (isSubExpression e' e2) *) +(* |Downcast m e1 => isSubExpression e' e1 *) +(* end). *) + +(* Lemma eqImpliesSub e e': *) +(* expEqBool e' e = true -> isSubExpression e e' = true. *) +(* Proof. *) +(* revert e e'; destruct e'; intros; simpl in *; rewrite H; auto. *) +(* Qed. *) + +(* Lemma typeMapSubExpr e e' m: *) +(* typeMap e e' = Some m -> isSubExpression e' e = true. *) +(* Proof. *) +(* revert e e' m; induction e; intros. *) +(* - unfold typeMap in H. *) +(* case_eq (expEqBool (Var Q m n) e'); intros; rewrite H0 in H; inversion H; subst. *) +(* apply eqImpliesSub; auto. *) +(* - unfold typeMap in H. *) +(* case_eq (expEqBool (Const m v) e'); intros hyp_if; rewrite hyp_if in H; inversion H; subst. *) +(* apply eqImpliesSub; auto. *) +(* - unfold typeMap in H. *) +(* case_eq (expEqBool (Unop u e) e'); intros hyp_if; rewrite hyp_if in H. *) +(* + apply eqImpliesSub; auto. *) +(* + specialize (IHe _ _ H). *) +(* simpl. *) +(* rewrite IHe; auto; apply orb_true_r. *) +(* - unfold typeMap in H. *) +(* case_eq (expEqBool (Binop b e1 e2) e'); intros hyp_if; rewrite hyp_if in H. *) +(* + apply eqImpliesSub; auto. *) +(* + case_eq (typeMap e1 e'); intros; unfold typeMap in H0; rewrite H0 in H. *) +(* * inversion H; subst. *) +(* specialize (IHe1 _ _ H0). *) +(* simpl; rewrite IHe1; simpl; apply orb_true_r. *) +(* * case_eq (typeMap e2 e'); intros; unfold typeMap in H1; rewrite H1 in H. *) +(* { inversion H; subst. *) +(* specialize (IHe2 _ _ H1). *) +(* simpl; rewrite IHe2; repeat rewrite orb_true_r; auto. } *) +(* { inversion H. } *) +(* - unfold typeMap in H. *) +(* case_eq (expEqBool (Downcast m e) e'); intros hyp_if; rewrite hyp_if in H. *) +(* + apply eqImpliesSub; auto. *) +(* + specialize (IHe _ _ H). *) +(* simpl. *) +(* rewrite IHe; auto; apply orb_true_r. *) +(* Qed. *) + + +(* Lemma rewriteEqInSub e e' f: *) +(* expEqBool e e' = true -> *) +(* isSubExpression e f = true -> *) +(* isSubExpression e' f = true. *) +(* Proof. *) +(* induction f; intros. *) +(* - unfold isSubExpression in *. *) +(* rewrite orb_false_r in *. *) +(* eapply expEqBool_trans; eauto. *) +(* - unfold isSubExpression in *. *) +(* rewrite orb_false_r in *. *) +(* eapply expEqBool_trans; eauto. *) +(* - unfold isSubExpression in *. *) +(* case_eq (expEqBool (Unop u f) e); intros; rewrite H1 in H0. *) +(* + pose proof (expEqBool_trans _ _ _ H1 H); rewrite H2. *) +(* simpl; auto. *) +(* + simpl in H0. *) +(* apply orb_true_iff; right. *) +(* eapply IHf; eauto. *) +(* - unfold isSubExpression in *. *) +(* case_eq (expEqBool (Binop b f1 f2) e); intros; rewrite H1 in H0. *) +(* + apply orb_true_iff; left. *) +(* eapply expEqBool_trans; eauto. *) +(* + apply orb_true_iff; right. *) +(* simpl in H0. *) +(* case_eq (isSubExpression e f1); intros; unfold isSubExpression in H2; rewrite H2 in H0. *) +(* * apply orb_true_iff; left. *) +(* clear H0. *) +(* clear IHf2. *) +(* eapply IHf1; eauto. *) +(* * simpl in H0. *) +(* apply orb_true_iff; right. *) +(* eapply IHf2; eauto. *) +(* - unfold isSubExpression in *. *) +(* case_eq (expEqBool (Downcast m f) e); intros; rewrite H1 in H0. *) +(* + apply orb_true_iff; left. *) +(* eapply expEqBool_trans; eauto. *) +(* + apply orb_true_iff; right. *) +(* eapply IHf; eauto. *) +(* Qed. *) + + +(* Lemma subExpr_antisym e f: *) +(* isSubExpression e f = true -> *) +(* isSubExpression f e = true -> *) +(* expEqBool e f = true. *) +(* Proof. *) +(* Admitted. *) + + +(* Lemma subExprNotUnop u e: *) +(* isSubExpression (Unop u e) e = false. *) +(* Proof. *) +(* revert u e; induction e. *) +(* - simpl; auto. *) +(* - simpl; auto. *) +(* - simpl. *) +(* intros. *) +(* rewrite expEqBool_sym,unop_neq. *) +(* rewrite andb_false_r; simpl. *) + +(* Admitted. *) + +(* Lemma equal_typing e e1 e2 m: *) +(* expEqBool e1 e2 = true -> *) +(* typeMap e e1 = Some m -> *) +(* typeMap e e2 = Some m. *) +(* revert e1 e2 m; induction e; intros *; intros eqExp type_e1. *) +(* - simpl in *. destruct e1; try congruence. *) +(* case_eq (mTypeEqBool m m1 && (n =? n0)); intros case_types; *) +(* rewrite case_types in *; try congruence. *) +(* destruct e2; simpl in *; try congruence. *) +(* admit. *) +(* - admit. *) +(* - simpl in *. *) +(* destruct e1; destruct e2; simpl in *; try congruence; simpl in *. *) +(* + eapply IHe; eauto. *) +(* simpl; auto. *) +(* + eapply IHe; eauto. *) +(* simpl; auto. *) +(* + admit. *) +(* + eapply IHe; eauto. *) +(* simpl; auto. *) +(* + eapply IHe; eauto. *) +(* simpl; auto. *) +(* - simpl in *. *) +(* destruct e0; destruct e3; simpl in *; try congruence; simpl in *. *) +(* + admit. *) +(* + admit. *) +(* + admit. *) +(* + admit. *) +(* + admit. *) +(* - admit. *) +(* Admitted. *) + +(* Lemma unopTypeMapStrenghtening u e e0 m: *) +(* typeMap e e0 = Some m -> typeMap (Unop u e) e0 = Some m. *) +(* Proof. *) +(* intros. *) +(* induction e0; destruct e0; simpl in *; try auto; try congruence. *) +(* case_eq (unopEqBool u u0 && expEqBool e e0); intros. *) +(* - assert (typeMap e (Unop u e) = Some m). *) +(* + eapply equal_typing; eauto. simpl; auto. admit. *) +(* + *) +(* unfold typeMap. *) +(* (* pose proof (typeMapSubExpr _ _ H). *) *) +(* (* assert (isSubExpression e (Unop u e) = true) by admit.*) *) +(* case_eq (expEqBool (Unop u e) e0); intros. *) +(* - assert (typeMap e (Unop u e) = Some m) by admit. *) +(* simpl in *. *) +(* (* pose proof (typeMapSubExpr _ _ H). *) +(* assert (isSubExpression (Unop u e) e = true) by (eapply rewriteEqInSub; eauto; rewrite expEqBool_sym; auto). *) +(* (* contradiction in H2 *) *) +(* admit. *) *) +(* - apply H. *) +(* Admitted. *) + +(* Lemma binopTypeMapStrenghtening_l b e1 e2 e m: *) +(* typeMap e1 e = Some m -> typeMap (Binop b e1 e2) e = Some m. *) +(* Proof. *) +(* intros. unfold typeMap. *) +(* case_eq (expEqBool (Binop b e1 e2) e); intros. *) +(* - pose proof (typeMapSubExpr _ _ H). *) +(* admit. *) +(* - unfold typeMap in H; rewrite H. auto. *) +(* Admitted. *) + +(* Lemma binopTypeMapStrenghtening_r b e1 e2 e m: *) +(* typeMap e2 e = Some m -> typeMap (Binop b e1 e2) e = Some m. *) +(* Proof. *) +(* intros. unfold typeMap. *) +(* case_eq (expEqBool (Binop b e1 e2) e); intros. *) +(* - pose proof (typeMapSubExpr _ _ H). *) +(* admit. *) +(* - unfold typeMap in H; rewrite H. auto. *) +(* Admitted. *) + +(* Lemma roundinTypeMapStrengthening e e0 m m0: *) +(* typeMap e e0 = Some m -> typeMap (Downcast m0 e) e0 = Some m. *) +(* Proof. *) +(* intros; unfold typeMap. *) +(* case_eq (expEqBool (Downcast m0 e) e0); intros. *) +(* - pose proof (typeMapSubExpr _ _ H). *) +(* admit. *) +(* - unfold typeMap in H; rewrite H. auto. *) +(* Admitted. *) + + +(* Lemma typeExpressionSoundness e m: *) +(* typeExpression e = Some m -> *) +(* validType (typeMap e) e m. *) +(* Proof. *) +(* revert m; induction e; intros; auto. *) +(* - simpl in *. *) +(* inversion H; subst; econstructor; eauto. *) +(* rewrite <- beq_nat_refl,mTypeEqBool_refl. *) +(* simpl; auto. *) +(* - simpl in *. *) +(* inversion H; subst; econstructor; eauto. *) +(* assert (Qeq_bool v v = true) by (apply Qeq_bool_iff; lra). *) +(* rewrite H0,mTypeEqBool_refl; simpl; auto. *) +(* - constructor. *) +(* + simpl in H. specialize (IHe m H). *) + +(* eapply Gamma_strengthening. *) +(* Focus 2. apply IHe. apply unopTypeMapStrenghtening. *) +(* + unfold typeMap. rewrite expEqBool_refl. auto. *) +(* - simpl in H. *) +(* case_eq (typeExpression e1); intros; rewrite H0 in H; [ | inversion H ]. *) +(* case_eq (typeExpression e2); intros; rewrite H1 in H; inversion H. *) +(* econstructor; eauto. *) +(* + specialize (IHe1 _ H0). *) +(* eapply Gamma_strengthening. *) +(* Focus 2. apply IHe1. *) +(* apply binopTypeMapStrenghtening_l. *) +(* + specialize (IHe2 _ H1). *) +(* eapply Gamma_strengthening. *) +(* Focus 2. apply IHe2. *) +(* apply binopTypeMapStrenghtening_r. *) +(* + unfold typeMap. *) +(* rewrite expEqBool_refl. *) +(* simpl. *) +(* rewrite H0, H1; auto. *) +(* - simpl in H. *) +(* case_eq (typeExpression e); intros; rewrite H0 in H; [ | inversion H ]. *) +(* case_eq (isMorePrecise m1 m); intros; rewrite H1 in H; inversion H; subst. *) +(* econstructor; eauto. *) +(* + specialize (IHe _ H0). *) +(* eapply Gamma_strengthening. *) +(* Focus 2. apply IHe. *) +(* intros e0 m; apply roundinTypeMapStrengthening. *) +(* + unfold typeMap. *) +(* rewrite expEqBool_refl; auto. *) +(* Qed. *) + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +(* (*******************) *) +(* (*******************) *) +(* (*******************) *) +(* (***** UNUSED ******) *) +(* (*******************) *) +(* (*******************) *) +(* (*******************) *) +(* (** *) +(* Now we want a TypeEnv function, taking an expression and returning a exp -> option mType *) +(* Soundness property is: TypeEnv e = T -> eval_exp e E v m -> T e = m. *) +(* **) *) + +(* Definition updTEnv (e:exp Q) (t:mType) (cont:exp Q-> option mType) := *) +(* (fun e' => *) +(* if expEqBool e e' *) +(* then Some t *) +(* else cont e'). *) + +(* Definition emptyTEnv :exp Q -> option mType := fun e => None. *) + + +(* Definition typeExpression e := typeExpression_trec e emptyTEnv. *) + +(* Definition updNatEnv (x:nat) (m:mType) (env: nat -> option mType) := *) +(* (fun n => if (n =? x) then Some m else (env n)). *) + +(* Definition emptyNatEnv :nat -> option mType := fun n => None. *) + + + +(* Fixpoint typeCmd_trec1 (f:cmd Q) (cont: exp Q -> option mType) (env: nat -> option mType) := *) +(* match f with *) +(* | Let m x e g => (* check that env x = None ? or this is already done by ssa ? *) *) +(* let gamma := typeExpression_trec e cont in *) +(* match (gamma e) with *) +(* | Some m' => if mTypeEqBool m m' then *) +(* (* hum. Should we just return tEnv_g ? *) *) +(* typeCmd_trec1 g gamma (updNatEnv x m' env) *) +(* else *) +(* emptyTEnv *) +(* | None => emptyTEnv *) +(* end *) +(* | Ret e => *) +(* typeExpression_trec e cont *) +(* end. *) + +(* (* Definition typeCmd f := typeCmd_trec1 f emptyTEnv emptyNatEnv. *) *) + +(* (* Eval compute in typeCmd (Let M32 1 (Const M32 (1#1)) (Ret (Binop Plus (Var Q M32 1) (Const M64 (2#1))))). *) *) +(* (* Eval compute in typeCmd (Let M64 1 (Const M32 (1#1)) (Ret (Binop Plus (Var Q M64 1) (Const M64 (2#1))))). *) *) +(* (* Eval compute in typeCmd (Let M64 1 (Const M32 (1#1)) (Ret (Binop Plus (Var Q M32 1) (Const M32 (2#1))))). *) *) + + + +(* (* do we need this env:nat -> option mType ? The updTEnv does the same kind of thing I guess... *) *) +(* (* issue here is that we may have (Var Q m x) and (Var Q m' x). But this should not happen... *) *) +(* Fixpoint typeCmd_trec2 (f:cmd Q) (cont: exp Q -> option mType) := *) +(* match f with *) +(* | Let m x e g => *) +(* let gamma := typeExpression_trec e cont in *) +(* match (gamma e) with *) +(* | Some m' => if mTypeEqBool m m' then *) +(* let newCont := updTEnv (Var Q m x) m gamma in *) +(* typeCmd_trec2 g newCont *) +(* else *) +(* emptyTEnv *) +(* | None => emptyTEnv *) +(* end *) +(* | Ret e => *) +(* typeExpression_trec e cont *) +(* end. *) + +(* Definition typeCmd f := typeCmd_trec2 f emptyTEnv. *) + +(* Eval compute in typeCmd (Let M32 1 (Const M32 (1#1)) (Ret (Binop Plus (Var Q M32 1) (Const M64 (2#1))))). *) +(* Eval compute in typeCmd (Let M64 1 (Const M32 (1#1)) (Ret (Binop Plus (Var Q M64 1) (Const M64 (2#1))))). *) +(* Eval compute in typeCmd (Let M64 1 (Const M32 (1#1)) (Ret (Binop Plus (Var Q M32 1) (Const M32 (2#1))))). *) + +(* Eval compute in typeCmd (Let M32 1 (Const M32 (1#1)) *) +(* (Let M64 1 (Const M64 (1#1)) *) +(* (Ret (Binop Plus (Var Q M32 1) (Var Q M64 1))))). *) + + +(* Theorem typeCmd_sound (f:cmd Q) inVars E v m: *) +(* validSSA f inVars = true -> *) +(* bstep (toRCmd f) E v m -> *) +(* typeCmd f (getRetExp f) = Some m. *) +(* Proof. *) +(* Admitted. *) + + + + + +(* (* NB: one might be tempted to prove the following lemma: *) *) +(* (* Lemma typeExpressionPropagatesNone e e0: *) *) +(* (* isSubExpression e0 e = true -> *) *) +(* (* typeExpression e e0 = None -> *) *) +(* (* typeExpression e e = None. *) *) +(* (* However, due to the definition of typeExpression, this is not true: *) *) +(* (* typeExpression (Binop b e1 e2) (Binop b e1 e2) = computeJoin (typeExpression e1 e1) (typeExpression e2 e2). *) *) +(* (* But we can have typeExpression e1 e0 = typeExpression e2 e0 = None. *) *) +(* (* Ie, when computing the types of Binop b e1 e2, we do not check if typing is coherent for all subexpressions *) *) + +(* Lemma detTypingBinop (f1 f2: exp Q) (b:binop) (m m0 m1 m2: mType) x: *) +(* typeExpression (Binop b f1 f2) (Var Q m0 x) = Some m -> *) +(* typeExpression f1 (Var Q m0 x) = Some m1 -> *) +(* typeExpression f2 (Var Q m0 x) = Some m2 -> *) +(* m = m1 /\ m = m2. *) +(* Proof. *) +(* intros. *) +(* split; simpl in *; rewrite H0, H1 in H. *) +(* - case_eq (mTypeEqBool m1 m2); intros; auto; rewrite H2 in H. *) +(* + apply EquivEqBoolEq in H2; subst. *) +(* assert (mTypeEqBool m2 m2 = true) by (apply EquivEqBoolEq; auto). *) +(* inversion H; auto. *) +(* + inversion H. *) +(* - case_eq (mTypeEqBool m1 m2); intros; auto; rewrite H2 in H. *) +(* + apply EquivEqBoolEq in H2; subst. *) +(* assert (mTypeEqBool m2 m2 = true) by (apply EquivEqBoolEq; auto). *) +(* inversion H; auto. *) +(* + inversion H. *) +(* Qed. *) + +(* Lemma typeExpressionIsSound e E v m: *) +(* eval_exp E (toRExp e) v m -> *) +(* (typeExpression e) e = Some m. *) +(* Proof. *) +(* revert e E v m; induction e; intros; inversion H; simpl in *; subst. *) +(* - assert (mTypeEqBool m0 m0 && (n =? n) = true) by (apply andb_true_iff; split; [ apply EquivEqBoolEq | rewrite <- beq_nat_refl ]; auto). *) +(* rewrite H0. *) +(* trivial. *) +(* - assert (mTypeEqBool m0 m0 && Qeq_bool v v = true). *) +(* apply andb_true_iff; split; [apply EquivEqBoolEq; auto | apply Qeq_bool_iff; lra]. *) +(* rewrite H0. *) +(* auto. *) +(* - rewrite expEqBool_refl. *) +(* eapply IHe; eauto. *) +(* - rewrite expEqBool_refl. *) +(* eapply IHe; eauto. *) +(* - rewrite expEqBool_refl; simpl. *) +(* rewrite expEqBool_refl; simpl. *) +(* rewrite andb_true_r. *) +(* rewrite binopEqBool_refl; simpl. *) +(* pose proof (IHe1 E v1 m1 H6). *) +(* pose proof (IHe2 E v2 m2 H7). *) +(* rewrite H0, H1. *) +(* auto. *) +(* - rewrite expEqBool_refl. *) +(* assert (mTypeEqBool m0 m0 = true) by (apply EquivEqBoolEq; auto). *) +(* rewrite H0; simpl. *) +(* pose proof (IHe E v1 m2 H6). *) +(* rewrite H1,H2; auto. *) +(* Qed. *) + + +(* Lemma typingVarDet (e:exp Q) m m0 v: *) +(* typeExpression e (Var Q m v) = Some m0 -> *) +(* m = m0. *) +(* Proof. *) +(* revert e; induction e; intros. *) +(* - simpl in H. *) +(* case_eq (mTypeEqBool m1 m && (n =? v)); intros; rewrite H0 in H; inversion H; auto. *) +(* rewrite <- H2. *) +(* apply andb_true_iff in H0; destruct H0 as [H0m H0n]. *) +(* apply EquivEqBoolEq in H0m; auto. *) +(* - simpl in H; inversion H. *) +(* - simpl in H; apply IHe; auto. *) +(* - simpl in H. *) +(* case_eq (typeExpression e1 (Var Q m v)); intros; rewrite H0 in H; auto; *) +(* case_eq (typeExpression e2 (Var Q m v)); intros; rewrite H1 in H; auto. *) +(* + case_eq (mTypeEqBool m1 m2); intros; rewrite H2 in H; inversion H; auto. *) +(* apply IHe1; auto. *) +(* rewrite <- H4; auto. *) +(* + inversion H; subst; apply IHe1; auto. *) +(* + inversion H; subst; apply IHe2; auto. *) +(* + inversion H. *) +(* - apply IHe. *) +(* simpl in H. *) +(* auto. *) +(* Qed. *) + +(* Lemma typingConstDet (e:exp Q) m m0 v: *) +(* typeExpression e (Const m v) = Some m0 -> *) +(* m = m0. *) +(* Proof. *) +(* revert e; induction e; intros. *) +(* - simpl in H; inversion H. *) +(* - simpl in H. *) +(* case_eq (mTypeEqBool m1 m && Qeq_bool v0 v); intros; rewrite H0 in H; inversion H; auto. *) +(* rewrite <- H2. *) +(* apply andb_true_iff in H0; destruct H0 as [H0m H0n]. *) +(* apply EquivEqBoolEq in H0m; auto. *) +(* - simpl in H; apply IHe; auto. *) +(* - simpl in H. *) +(* case_eq (typeExpression e1 (Const m v)); intros; rewrite H0 in H; auto; *) +(* case_eq (typeExpression e2 (Const m v)); intros; rewrite H1 in H; auto. *) +(* + case_eq (mTypeEqBool m1 m2); intros; rewrite H2 in H; inversion H; auto. *) +(* apply IHe1; auto. *) +(* rewrite <- H4; auto. *) +(* + inversion H; subst; apply IHe1; auto. *) +(* + inversion H; subst; apply IHe2; auto. *) +(* + inversion H. *) +(* - apply IHe. *) +(* simpl in H. *) +(* auto. *) +(* Qed. *) + +(* Fixpoint isSubExpression (e':exp Q) (e:exp Q) := *) +(* orb (expEqBool e e') ( *) +(* match e with *) +(* |Var _ _ _ => false *) +(* |Const _ _ => false *) +(* |Unop o1 e1 => isSubExpression e' e1 *) +(* |Binop b e1 e2 => orb (isSubExpression e' e1) (isSubExpression e' e2) *) +(* |Downcast m e1 => isSubExpression e' e1 *) +(* end). *) + +(* Lemma typeNotSubExpr e e1: *) +(* isSubExpression e1 e = false -> typeExpression e e1 = None. *) +(* Proof. *) +(* revert e e1; induction e; intros. *) +(* - simpl in H. rewrite orb_false_r in H. *) +(* simpl; rewrite H; auto. *) +(* - simpl in H; rewrite orb_false_r in H. *) +(* simpl; rewrite H; auto. *) +(* - simpl in H. *) +(* case_eq (isSubExpression e1 e); intros; rewrite H0 in H; auto. *) +(* + rewrite orb_true_r in H. *) +(* inversion H. *) +(* + rewrite orb_false_r in H. *) +(* simpl; rewrite H; auto. *) +(* - simpl in H. *) +(* case_eq (isSubExpression e0 e1); intros; *) +(* case_eq (isSubExpression e0 e2); intros; rewrite H0,H1 in H; auto. *) +(* + rewrite orb_true_r in H; inversion H. *) +(* + rewrite orb_true_r in H; inversion H. *) +(* + rewrite orb_true_r in H; inversion H. *) +(* + rewrite orb_false_r in H. *) +(* simpl; rewrite H. *) +(* specialize (IHe1 e0 H0). *) +(* specialize (IHe2 e0 H1). *) +(* rewrite IHe1, IHe2. *) +(* auto. *) +(* - simpl in H. *) +(* case_eq (isSubExpression e1 e); intros; rewrite H0 in H. *) +(* + rewrite orb_true_r in H; inversion H. *) +(* + rewrite orb_false_r in H. simpl; rewrite H; auto. *) +(* Qed. *) + +(* Lemma typedVarIsSubExpr e m v: *) +(* typeExpression e (Var Q m v) = Some m -> *) +(* isSubExpression (Var Q m v) e = true. *) +(* Proof. *) +(* revert e; induction e; intros; simpl in H. *) +(* - case_eq (mTypeEqBool m0 m && (n =? v)); intros; rewrite H0 in H; inversion H; subst. *) +(* simpl; rewrite H0; auto. *) +(* - inversion H. *) +(* - apply IHe; auto. *) +(* - case_eq (typeExpression e1 (Var Q m v)); intros; case_eq (typeExpression e2 (Var Q m v)); intros; rewrite H0,H1 in H; inversion H; subst. *) +(* + clear H3. *) +(* case_eq (mTypeEqBool m0 m1); intros; rewrite H2 in H; inversion H; subst. *) +(* specialize (IHe1 H0). *) +(* simpl; rewrite IHe1; auto. *) +(* + specialize (IHe1 H0); simpl; rewrite IHe1; auto. *) +(* + specialize (IHe2 H1); simpl; rewrite IHe2. apply orb_true_r. *) +(* - simpl; apply IHe; auto. *) +(* Qed. *) + +(* Lemma typedIsSubExpr e f m: *) +(* typeExpression e f = Some m -> *) +(* isSubExpression f e = true. *) +(* Proof. *) +(* revert e m; induction e; intros. *) +(* - simpl in H; destruct f; inversion H. *) +(* simpl. *) +(* case_eq (mTypeEqBool m m1 && (n =? n0)); intros; rewrite H0 in H; inversion H. *) +(* auto. *) +(* - simpl in H; destruct f; inversion H. *) +(* simpl. *) +(* case_eq (mTypeEqBool m m1 && Qeq_bool v q); intros; rewrite H0 in H; inversion H. *) +(* auto. *) +(* - case_eq (expEqBool (Unop u e) f); intros; simpl in H,H0; rewrite H0 in H. *) +(* + destruct f; [ inversion H0 | inversion H0 | | inversion H0 | inversion H0 ]. *) +(* simpl. *) +(* rewrite H0; auto. *) +(* + specialize (IHe _ H). *) +(* simpl. *) +(* rewrite IHe. *) +(* apply orb_true_r. *) +(* - case_eq (expEqBool (Binop b e1 e2) f); intros; simpl in H,H0; rewrite H0 in H. *) +(* + destruct f; inversion H0. *) +(* rewrite H0. *) +(* simpl. *) +(* rewrite H0. *) +(* auto. *) +(* + simpl; rewrite H0; rewrite orb_false_l. *) +(* case_eq (typeExpression e1 f); intros; rewrite H1 in H. *) +(* * specialize (IHe1 _ H1). *) +(* rewrite IHe1; auto. *) +(* * case_eq (typeExpression e2 f); intros; rewrite H2 in H; inversion H; subst. *) +(* specialize (IHe2 _ H2); rewrite IHe2; auto. *) +(* apply orb_true_r. *) +(* - case_eq (expEqBool (Downcast m e) f); intros; simpl in H,H0; rewrite H0 in H. *) +(* + destruct f; inversion H0. *) +(* rewrite H0; simpl; rewrite H0; auto. *) +(* + specialize (IHe _ H). *) +(* simpl. *) +(* rewrite IHe. *) +(* apply orb_true_r. *) +(* Qed. *) + +(* Lemma typedVarIsUsed e m m0 v: *) +(* typeExpression e (Var Q m0 v) = Some m -> *) +(* NatSet.In v (usedVars e). *) +(* Proof. *) +(* intros; induction e. *) +(* - simpl in *. *) +(* case_eq (mTypeEqBool m1 m0 && (n =? v)); intros; auto; rewrite H0 in H. *) +(* + andb_to_prop H0. *) +(* apply InA_cons. *) +(* left; symmetry. *) +(* apply beq_nat_true; auto. *) +(* + inversion H. *) +(* - simpl in *; inversion H. *) +(* - simpl in *; apply IHe; auto. *) +(* - pose proof (detTypingBinop e1 e2 b). *) +(* case_eq (typeExpression e1 (Var Q m0 v)); case_eq (typeExpression e2 (Var Q m0 v)); intros; auto. *) +(* + specialize (H0 _ _ _ _ _ H H2 H1) as [H01 H02]; subst. *) +(* simpl; apply NatSet.union_spec; left; apply IHe1; auto. *) +(* + simpl. *) +(* simpl in H; rewrite H1,H2 in H; inversion H; subst. *) +(* apply NatSet.union_spec; left; apply IHe1; auto. *) +(* + simpl; simpl in H. *) +(* rewrite H1,H2 in H; inversion H; subst. *) +(* apply NatSet.union_spec; right; apply IHe2; auto. *) +(* + simpl in H; rewrite H1, H2 in H. *) +(* inversion H. *) +(* - apply IHe; auto. *) +(* Qed. *) + + +(* Lemma binop_type_unfolding b f1 f2 mf: *) +(* typeExpression (Binop b f1 f2) (Binop b f1 f2) = Some mf -> *) +(* (exists m0 m1, typeExpression f1 f1 = Some m0 /\ typeExpression f2 f2 = Some m1 /\ mf = computeJoin m0 m1). *) +(* Proof. *) +(* intros. *) +(* simpl in H. *) +(* pose proof (expEqBool_refl (Binop b f1 f2)); simpl in H0; rewrite H0 in H. *) +(* case_eq (typeExpression f1 f1); intros; case_eq (typeExpression f2 f2); intros; try rewrite H1 in H; try rewrite H2 in H; inversion H. *) +(* exists m, m0. *) +(* auto. *) +(* Qed. *) + + +(* Lemma binary_type_unfolding b e1 e2 f m: *) +(* expEqBool (Binop b e1 e2) f = false -> *) +(* typeExpression (Binop b e1 e2) f = Some m -> *) +(* (typeExpression e1 f = Some m \/ typeExpression e2 f = Some m). *) +(* Proof. *) +(* intros notEq typeBinop. *) +(* assert (isSubExpression f (Binop b e1 e2) = true) as isSubExpr by (eapply typedIsSubExpr; eauto). *) +(* simpl in *. rewrite notEq in *. *) +(* case_eq (typeExpression e1 f); intros; rewrite H in typeBinop. *) +(* - case_eq (typeExpression e2 f); intros; rewrite H0 in typeBinop. *) +(* case_eq (mTypeEqBool m0 m1); intros; rewrite H1 in typeBinop; inversion typeBinop; subst; auto. *) +(* left; auto. *) +(* - case_eq (typeExpression e2 f); intros; rewrite H0 in typeBinop. *) +(* + right; auto. *) +(* + inversion typeBinop. *) +(* Qed. *) + +(* Lemma stupidcase e e' m m': *) +(* expEqBool e e' = true -> *) +(* typeExpression e e = Some m -> *) +(* typeExpression e' e' = Some m' -> *) +(* m = m'. *) +(* Proof. *) +(* revert e e' m m'; induction e; destruct e'; intros; inversion H; simpl in *. *) +(* - case_eq (mTypeEqBool m m && (n =? n)); intros; case_eq (mTypeEqBool m0 m0 && (n0 =? n0)); intros; rewrite H2 in H0; rewrite H4 in H1; inversion H0; inversion H1; subst; auto. *) +(* apply andb_true_iff in H; destruct H; apply EquivEqBoolEq in H; auto. *) +(* - case_eq (mTypeEqBool m m && Qeq_bool v v); intros; case_eq (mTypeEqBool m0 m0 && Qeq_bool q q); intros; rewrite H2 in H0; rewrite H4 in H1; inversion H0; inversion H1; subst; auto. *) +(* apply andb_true_iff in H; destruct H; apply EquivEqBoolEq in H; auto. *) +(* - clear H3. *) +(* pose proof (expEqBool_refl (Unop u e)); simpl in H2; rewrite H2 in H0. *) +(* pose proof (expEqBool_refl (Unop u0 e')); simpl in H3; rewrite H3 in H1. *) +(* apply andb_true_iff in H; destruct H. *) +(* eapply IHe; eauto. *) +(* - clear H3. *) +(* pose proof (expEqBool_refl (Binop b e1 e2)); simpl in H2; rewrite H2 in H0. *) +(* pose proof (expEqBool_refl (Binop b0 e'1 e'2)); simpl in H3; rewrite H3 in H1. *) +(* case_eq (typeExpression e1 e1); intros; case_eq (typeExpression e2 e2); intros; try rewrite H4 in H0; try rewrite H5 in H0; inversion H0. *) +(* case_eq (typeExpression e'1 e'1); intros; case_eq (typeExpression e'2 e'2); intros; try rewrite H6 in H1; try rewrite H8 in H1; inversion H1. *) +(* apply andb_true_iff in H; destruct H. *) +(* apply andb_true_iff in H9; destruct H9. *) +(* specialize (IHe1 e'1 _ _ H9 H4 H6). *) +(* specialize (IHe2 e'2 _ _ H11 H5 H8). *) +(* subst. *) +(* auto. *) +(* - clear H3. *) +(* apply andb_true_iff in H; destruct H. *) +(* apply EquivEqBoolEq in H; subst. *) +(* pose proof (expEqBool_refl (Downcast m0 e)); simpl in H; rewrite H in H0. *) +(* pose proof (expEqBool_refl (Downcast m0 e')); simpl in H3; rewrite H3 in H1. *) +(* clear H H3. *) +(* case_eq (typeExpression e e); intros; rewrite H in H0; inversion H0; clear H4. *) +(* case_eq (isMorePrecise m m0); intros; rewrite H3 in H0; inversion H0; subst; clear H0. *) +(* case_eq (typeExpression e' e'); intros; rewrite H0 in H1; inversion H1; clear H5. *) +(* case_eq (isMorePrecise m0 m1); intros; rewrite H4 in H1; inversion H1; subst; clear H1; *) +(* auto. *) +(* Qed. *) + +(* (* Lemma subExprRewriting e f1 f2: *) *) +(* (* expEqBool f1 f2 = true -> *) *) +(* (* isSubExpression f1 e = true -> *) *) +(* (* isSubExpression f2 e = true. *) *) +(* (* Proof. *) *) +(* (* revert e; induction e; intros. *) *) +(* (* - destruct f1; inversion H0. *) *) +(* (* rewrite H2. *) *) +(* (* destruct f2; inversion H. *) *) +(* (* rewrite H3. *) *) +(* (* simpl. *) *) +(* (* rewrite orb_false_r. *) *) +(* (* rewrite orb_false_r in H2. *) *) +(* (* apply andb_true_iff in H2; apply andb_true_iff in H3; destruct H2,H3. *) *) +(* (* apply andb_true_iff; split. *) *) +(* (* + apply EquivEqBoolEq in H1; apply EquivEqBoolEq in H3; subst. *) *) +(* (* apply mTypeEqBool_refl. *) *) +(* (* + apply beq_nat_true in H2. *) *) +(* (* apply beq_nat_true in H4; subst. *) *) +(* (* rewrite <- beq_nat_refl; auto. *) *) +(* (* - destruct f1; inversion H0; rewrite H2. *) *) +(* (* destruct f2; inversion H; rewrite H3. *) *) +(* (* simpl. *) *) +(* (* rewrite orb_false_r in *. *) *) +(* (* apply andb_true_iff in H2. apply andb_true_iff in H3. *) *) +(* (* destruct H2, H3. *) *) +(* (* apply andb_true_iff; split. *) *) +(* (* + apply EquivEqBoolEq in H1; apply EquivEqBoolEq in H3; subst. *) *) +(* (* apply mTypeEqBool_refl. *) *) +(* (* + apply Qeq_bool_iff in H2. *) *) +(* (* apply Qeq_bool_iff in H4. *) *) +(* (* apply Qeq_bool_iff; rewrite H2,H4; auto. *) *) +(* (* lra. *) *) +(* (* - case_eq (expEqBool (Unop u e) f1); intros. *) *) +(* (* + assert (expEqBool (Unop u e) f2 = true) by admit. *) *) +(* (* simpl; simpl in H2; rewrite H2. *) *) +(* (* auto. *) *) +(* (* + simpl in H0; simpl in H1; rewrite H1 in H0. *) *) +(* (* simpl in H0. *) *) +(* (* assert (expEqBool (Unop u e) f2 = false) by admit. *) *) +(* (* simpl in H2; simpl; rewrite H2; auto. *) *) +(* (* - case_eq (expEqBool (Binop b e1 e2) f1); intros. *) *) +(* (* + assert (expEqBool (Binop b e1 e2) f2 = true) by admit. *) *) +(* (* simpl; simpl in H2; rewrite H2; auto. *) *) +(* (* + assert (expEqBool (Binop b e1 e2) f2 = false) by admit. *) *) +(* (* simpl; simpl in H2; rewrite H2; auto; simpl. *) *) +(* (* simpl in H1; simpl in H0; rewrite H1 in H0; simpl in H0. *) *) +(* (* case_eq (isSubExpression f1 e1); intros. *) *) +(* (* * rewrite (IHe1 H H3); auto. *) *) +(* (* * rewrite H3 in H0; simpl in H0. *) *) +(* (* rewrite (IHe2 H H0); auto. *) *) +(* (* apply orb_true_r. *) *) +(* (* - case_eq (expEqBool (Downcast m e) f1); intros. *) *) +(* (* + assert (expEqBool (Downcast m e) f2 = true) by admit. *) *) +(* (* simpl; simpl in H2; rewrite H2; auto. *) *) +(* (* + assert (expEqBool (Downcast m e) f2 = false) by admit. *) *) +(* (* simpl; simpl in H2; rewrite H2; auto; simpl. *) *) +(* (* simpl in H1; simpl in H0; rewrite H1 in H0; simpl in H0. *) *) +(* (* apply IHe; auto. *) *) +(* (* Admitted. *) *) + +(* Lemma stupidNotEq u0 f: *) +(* expEqBool f (Unop u0 f) = false. *) +(* Proof. *) +(* induction f; simpl; auto. *) +(* destruct u; destruct u0; simpl; auto. *) +(* Qed. *) + +(* (* Lemma stupidNotSubExpr u f: *) *) +(* (* isSubExpression (Unop u f) f = false. *) *) +(* (* Proof. *) *) +(* (* revert f; induction f. *) *) +(* (* - simpl; auto. *) *) +(* (* - simpl; auto. *) *) +(* (* - case_eq (unopEqBool u0 u && expEqBool f (Unop u0 f)); intros. *) *) +(* (* + apply andb_true_iff in H; destruct H. *) *) +(* (* pose proof (stupidNotEq u0 f). *) *) +(* (* rewrite H1 in H0; inversion H0. *) *) +(* (* + simpl. *) *) +(* (* rewrite H; simpl. *) *) +(* (* admit. *) *) +(* (* - admit. *) *) +(* (* - simpl; auto. *) *) +(* (* Admitted. *) *) + +(* (* Lemma unary_type_unfolding u e f m: *) *) +(* (* isSubExpression f e = true -> *) *) +(* (* typeExpression (Unop u e) f = Some m -> *) *) +(* (* typeExpression e f = Some m. *) *) +(* (* Proof. *) *) +(* (* Admitted. *) *) + + +(* (* Lemma weakRewritingInTypeExpr e e' f m m': *) *) +(* (* expEqBool e e' = true -> *) *) +(* (* typeExpression e f = Some m -> *) *) +(* (* typeExpression e' f = Some m' -> *) *) +(* (* m = m'. *) *) +(* (* Proof. *) *) +(* (* revert m m' e e' f; induction e; intros; destruct e'; inversion H. *) *) +(* (* - admit. *) *) +(* (* - simpl in H; apply andb_true_iff in H; destruct H. *) *) +(* (* simpl in H0; destruct f; inversion H0. *) *) +(* (* simpl in H1. *) *) +(* (* case_eq (mTypeEqBool m0 m2 && Qeq_bool v q0); intros; rewrite H4 in H0; [ | inversion H0 ]. *) *) +(* (* case_eq (mTypeEqBool m1 m2 && Qeq_bool q q0); intros; rewrite H6 in H1; [ | inversion H1 ]. *) *) +(* (* inversion H0; inversion H1; subst. *) *) +(* (* apply EquivEqBoolEq in H; auto. *) *) +(* (* - apply andb_true_iff in H3; destruct H3. *) *) +(* (* assert (isSubExpression f (Unop u e) = true) by (eapply typedIsSubExpr; eauto). (*lemma from somewhere*) *) *) +(* (* unfold isSubExpression in H4. *) *) +(* (* case_eq (expEqBool (Unop u e) f); intros. *) *) +(* (* + clear H4. *) *) +(* (* unfold typeExpression in H0. *) *) +(* (* rewrite H5 in H0. *) *) +(* (* assert (expEqBool (Unop u0 e') f = true) by admit. (* transitivity of eq by H5 and H1 *) *) *) +(* (* unfold typeExpression in H1; rewrite H4 in H1. *) *) +(* (* apply (stupidcase e e'); auto. *) *) +(* (* + rewrite H5 in H4; simpl in H4. *) *) +(* (* pose proof (unary_type_unfolding u e f H4 H0). *) *) +(* (* assert (isSubExpression f e' = true) by admit. *) *) +(* (* pose proof (unary_type_unfolding u0 e' f H7 H1). *) *) +(* (* eapply IHe; eauto. *) *) +(* (* - clear H. *) *) +(* (* apply andb_true_iff in H3; destruct H3. *) *) +(* (* apply andb_true_iff in H2; destruct H2. *) *) +(* (* assert (b = b0) by (destruct b; destruct b0; inversion H; auto). *) *) +(* (* symmetry in H4; subst. *) *) +(* (* assert (isSubExpression f (Binop b e1 e2) = true) by (eapply typedIsSubExpr; eauto). *) *) +(* (* simpl in H4. (*unfold isSubExpression in H4.*) *) *) +(* (* case_eq (expEqBool (Binop b e1 e2) f); intros. *) *) +(* (* + clear H4. *) *) +(* (* simpl in H0; simpl in H5; rewrite H5 in H0. *) *) +(* (* assert (expEqBool (Binop b e'1 e'2) f = true) by admit. (* transitivity of eq by H2+H3+H5 *) *) *) +(* (* simpl in H1; simpl in H4; rewrite H4 in H1. *) *) +(* (* case_eq (typeExpression e1 e1); intros; rewrite H6 in H0; *) *) +(* (* case_eq (typeExpression e2 e2); intros; try rewrite H7 in H0; inversion H0. *) *) +(* (* case_eq (typeExpression e'1 e'1); intros; rewrite H8 in H1; *) *) +(* (* case_eq (typeExpression e'2 e'2); intros; try rewrite H10 in H1; inversion H1. *) *) +(* (* pose proof (stupidcase _ _ H2 H6 H8). *) *) +(* (* pose proof (stupidcase _ _ H3 H7 H10). *) *) +(* (* subst; auto. *) *) +(* (* + assert (expEqBool (Binop b e'1 e'2) f = false) by admit. (* still transitivity *) *) *) +(* (* pose proof (binary_type_unfolding _ _ _ _ H5 H0). *) *) +(* (* pose proof (binary_type_unfolding _ _ _ _ H6 H1). *) *) +(* (* simpl in H5; rewrite H5 in H4. *) *) +(* (* simpl in H4. *) *) +(* (* simpl in H0; rewrite H5 in H0. *) *) +(* (* simpl in H6; simpl in H1; rewrite H6 in H1. *) *) +(* (* case_eq (typeExpression e1 f); intros; try rewrite H9 in H0; *) *) +(* (* case_eq (typeExpression e'1 f); intros; try rewrite H10 in H1. *) *) +(* (* Admitted. *) *) + +(* Lemma typingBinopDet b e1 e2 f m m0: *) +(* typeExpression (Binop b e1 e2) (Binop b e1 e2) = Some m -> *) +(* typeExpression f (Binop b e1 e2) = Some m0 -> *) +(* m = m0. *) +(* Proof. *) +(* revert m m0 f; induction f; intros. *) +(* - simpl in *; inversion H0. *) +(* - simpl in *; inversion H0. *) +(* - apply IHf; auto. *) +(* - case_eq (expEqBool (Binop b0 f1 f2) (Binop b e1 e2)); intros. *) +(* + simpl in H1,H0,H. rewrite H1 in H0. *) +(* pose proof (expEqBool_refl (Binop b e1 e2)); simpl in H2; rewrite H2 in H. *) +(* case_eq (typeExpression e1 e1); intros; case_eq (typeExpression f1 f1); intros; try rewrite H3 in H; try rewrite H4 in H0; inversion H; inversion H0; clear H6 H7. *) +(* case_eq (typeExpression e2 e2); intros; case_eq (typeExpression f2 f2); intros; try rewrite H5 in H; try rewrite H6 in H0; inversion H; inversion H0. *) +(* apply andb_true_iff in H1; destruct H1. *) +(* apply andb_true_iff in H7; destruct H7. *) +(* pose proof (stupidcase _ _ H7 H4 H3); *) +(* pose proof (stupidcase _ _ H10 H6 H5); subst; auto. *) +(* + simpl in H1,H0; rewrite H1 in H0. *) +(* specialize (IHf1 H); specialize (IHf2 H). *) +(* case_eq (typeExpression f1 (Binop b e1 e2)); intros; rewrite H2 in H0. *) +(* * case_eq (typeExpression f2 (Binop b e1 e2)); intros; rewrite H3 in H0. *) +(* { case_eq (mTypeEqBool m1 m2); intros; rewrite H4 in H0; inversion H0. *) +(* apply EquivEqBoolEq in H4; subst. *) +(* apply IHf1; auto. } *) +(* { inversion H0; subst. *) +(* apply IHf1; auto. } *) +(* * case_eq (typeExpression f2 (Binop b e1 e2)); intros; rewrite H3 in H0; inversion H0; subst. *) +(* apply IHf2; auto. *) +(* - apply IHf; auto. *) +(* Qed. *) + + + +(* (* Lemma helpinglemma (e:exp Q) m v : *) *) +(* (* typeExpression e (Var Q m v) = Some m -> *) *) +(* (* isSubExpression (Var Q m v) e = true. *) *) +(* (* Proof. *) *) +(* (* revert e; induction e; intros. *) *) +(* (* - unfold typeExpression in H. *) *) +(* (* case_eq (expEqBool (Var Q m0 n) (Var Q m v)); intros; rewrite H0 in H; inversion H; auto. *) *) +(* (* subst; simpl. *) *) +(* (* unfold expEqBool in H0. *) *) +(* (* rewrite orb_false_r. *) *) +(* (* auto. *) *) +(* (* - simpl in H; inversion H. *) *) +(* (* - simpl in *; apply IHe; auto. *) *) +(* (* - simpl in *. *) *) +(* (* apply orb_true_iff. *) *) +(* (* case_eq (typeExpression e1 (Var Q m v)); intros; rewrite H0 in H; auto. *) *) +(* (* + left. *) *) +(* (* apply IHe1. *) *) +(* (* rewrite H0. *) *) +(* (* apply typingVarDet in H0; rewrite H0; auto. *) *) +(* (* + case_eq (typeExpression e2 (Var Q m v)); intros; rewrite H1 in H; auto. *) *) +(* (* * right. apply IHe2. rewrite H1; apply typingVarDet in H1; rewrite H1; auto. *) *) +(* (* * inversion H. *) *) +(* (* - simpl in *; apply IHe; auto. *) *) +(* (* Qed. *) *) + +(* Lemma stupid e1 e: *) +(* expEqBool e1 e = true -> *) +(* isSubExpression e1 e = true. *) +(* Proof. *) +(* intros. *) +(* unfold isSubExpression. *) +(* destruct e; destruct e1; try (rewrite expEqBool_sym in H; rewrite H); simpl in *; auto; simpl in H; inversion H. *) +(* Qed. *) + + +(* Lemma downcast_typing_unfolding m e f: *) +(* isSubExpression (Downcast m e) f = true -> *) +(* isSubExpression e f = true. *) +(* Proof. *) +(* revert e f; induction f; intros; simpl in H; inversion H; clear H1. *) +(* - rewrite H. *) +(* simpl. rewrite IHf; auto. *) +(* apply orb_true_r. *) +(* - rewrite H. *) +(* simpl. *) +(* case_eq (isSubExpression (Downcast m e) f1); intros. *) +(* + rewrite (IHf1 H0). simpl. apply orb_true_r. *) +(* + rewrite H0 in H; simpl in H. *) +(* rewrite (IHf2 H). repeat rewrite orb_true_r; auto. *) +(* - rewrite H; simpl. *) +(* case_eq (isSubExpression (Downcast m e) f); intros. *) +(* + rewrite (IHf H0); simpl. apply orb_true_r. *) +(* + rewrite H0 in H; simpl in H; rewrite orb_false_r in H. *) +(* apply andb_true_iff in H; destruct H. *) +(* rewrite expEqBool_sym in H1. *) +(* rewrite (stupid _ _ H1). *) +(* apply orb_true_r. *) +(* Qed. *) diff --git a/coq/ssaPrgs.v b/coq/ssaPrgs.v index 1174528e8718267f04739b4be15b97ec893c7e0e..f0f6c63d49f71572cb6f071d08340a8a8504106e 100644 --- a/coq/ssaPrgs.v +++ b/coq/ssaPrgs.v @@ -41,27 +41,27 @@ Qed. Lemma validVars_non_stuck (e:exp Q) inVars E: NatSet.Subset (usedVars e) inVars -> (forall v, NatSet.In v (usedVars e) -> - exists r, E v = Some r)%R -> - exists vR, eval_exp 0 E (toRExp e) vR. + exists r, (toREvalEnv E) v = Some (r, M0))%R -> + exists vR, eval_exp (toREvalEnv E) (toREval (toRExp e)) vR M0. Proof. - revert inVars E; induction e; + revert inVars E; induction e; intros inVars E vars_valid fVars_live. - simpl in *. assert (NatSet.In n (NatSet.singleton n)) as in_n by (rewrite NatSet.singleton_spec; auto). specialize (fVars_live n in_n). destruct fVars_live as [vR E_def]. - exists vR; constructor; auto. + exists vR; econstructor; eauto. - exists (perturb (Q2R v) 0); constructor. - rewrite Rabs_R0; lra. - - assert (exists vR, eval_exp 0 E (toRExp e) vR) + simpl (meps M0); rewrite Rabs_R0; rewrite Q2R0_is_0; lra. + - assert (exists vR, eval_exp (toREvalEnv E) (toREval (toRExp e)) vR M0) as eval_e_def by (eapply IHe; eauto). destruct eval_e_def as [ve eval_e_def]. case_eq u; intros; subst. + exists (evalUnop Neg ve); constructor; auto. + exists (perturb (evalUnop Inv ve) 0); constructor; auto. - rewrite Rabs_R0; lra. + simpl (meps M0); rewrite Q2R0_is_0; rewrite Rabs_R0; lra. - repeat rewrite NatSet.subset_spec in *; simpl in *. - assert (exists vR1, eval_exp 0 E (toRExp e1) vR1) as eval_e1_def. + assert (exists vR1, eval_exp (toREvalEnv E) (toREval (toRExp e1)) vR1 M0) as eval_e1_def. + eapply IHe1; eauto. * hnf; intros. apply vars_valid. @@ -69,7 +69,7 @@ Proof. * intros. destruct (fVars_live v) as [vR E_def]; try eauto. apply NatSet.union_spec; auto. - + assert (exists vR2, eval_exp 0 E (toRExp e2) vR2) as eval_e2_def. + + assert (exists vR2, eval_exp (toREvalEnv E) (toREval (toRExp e2)) vR2 M0) as eval_e2_def. * eapply IHe2; eauto. { hnf; intros. apply vars_valid. @@ -79,21 +79,30 @@ Proof. apply NatSet.union_spec; auto. } * destruct eval_e1_def as [vR1 eval_e1_def]; destruct eval_e2_def as [vR2 eval_e2_def]. - exists (perturb (evalBinop b vR1 vR2) 0); constructor; auto. - rewrite Rabs_R0; lra. + exists (perturb (evalBinop b vR1 vR2) 0). + replace M0 with (computeJoin M0 M0) by auto. + constructor; auto. + simpl meps; rewrite Q2R0_is_0. rewrite Rabs_R0; lra. + - assert (exists vR, eval_exp (toREvalEnv E) (toREval (toRExp e)) vR M0) as eval_r_def by (eapply IHe; eauto). + destruct eval_r_def as [vr eval_r_def]. + exists vr. + simpl toREval. + auto. Qed. *) + Inductive ssa (V:Type): (cmd V) -> (NatSet.t) -> (NatSet.t) -> Prop := - ssaLet x e s inVars Vterm: + ssaLet m x e s inVars Vterm: NatSet.Subset (usedVars e) inVars-> NatSet.mem x inVars = false -> ssa s (NatSet.add x inVars) Vterm -> - ssa (Let x e s) inVars Vterm + ssa (Let m x e s) inVars Vterm |ssaRet e inVars Vterm: NatSet.Subset (usedVars e) inVars -> NatSet.Equal inVars Vterm -> ssa (Ret e) inVars Vterm. + Lemma ssa_subset_freeVars V (f:cmd V) inVars outVars: ssa f inVars outVars -> NatSet.Subset (freeVars f) inVars. @@ -112,6 +121,7 @@ Proof. apply H; auto. Qed. + Lemma ssa_equal_set V (f:cmd V) inVars inVars' outVars: NatSet.Equal inVars' inVars -> ssa f inVars outVars -> @@ -134,9 +144,10 @@ Proof. + rewrite set_eq; auto. Qed. + Fixpoint validSSA (f:cmd Q) (inVars:NatSet.t) := match f with - |Let x e g => + |Let m x e g => andb (andb (negb (NatSet.mem x inVars)) (NatSet.subset (usedVars e) inVars)) (validSSA g (NatSet.add x inVars)) |Ret e => NatSet.subset (usedVars e) inVars end. @@ -163,11 +174,11 @@ Proof. + hnf; intros; split; auto. Qed. -Lemma ssa_shadowing_free x y v v' e f inVars outVars E: - ssa (Let x e f) inVars outVars -> +Lemma ssa_shadowing_free m x y v v' e f inVars outVars E: + ssa (Let m x (toREval (toRExp e)) (toREvalCmd (toRCmd f))) inVars outVars -> NatSet.In y inVars -> - eval_exp 0 E (toRExp e) v -> - forall E n, updEnv x v (updEnv y v' E) n = updEnv y v' (updEnv x v E) n. + eval_exp E (toREval (toRExp e)) v M0 -> + forall E n, updEnv x m v (updEnv y m v' E) n = updEnv y m v' (updEnv x m v E) n. Proof. intros ssa_let y_free eval_e. inversion ssa_let; subst. @@ -181,54 +192,61 @@ Proof. rewrite n_eq_x in n_eq_y. rewrite <- n_eq_y in y_free. rewrite <- NatSet.mem_spec in y_free. - rewrite y_free in H5. inversion H5. + rewrite y_free in H6. inversion H6. - intros n_neq_x. case_eq (n =? y); auto. Qed. + Lemma shadowing_free_rewriting_exp e v E1 E2: - (forall n, E1 n = E2 n) -> - eval_exp 0 E1 e v <-> - eval_exp 0 E2 e v. +(* (forall n, exists v m, + E1 n = Some (v,m) -> + exists m', (E2 n = Some (v,m') /\ (meps m) == (meps m'))) ->*) + (forall n, E1 n = E2 n)-> + eval_exp E1 (toREval e) v M0 <-> + eval_exp E2 (toREval e) v M0. Proof. revert v E1 E2. induction e; intros v' E1 E2 agree_on_vars. - split; intros eval_Var. + inversion eval_Var; subst. - rewrite agree_on_vars in H0. - apply (Var_load _ _ _ H0). + (*assert (m1 = M0) by (apply ifisMorePreciseM0; auto); subst.*) + rewrite agree_on_vars in H2. + eapply Var_load; eauto. + inversion eval_Var; subst. - rewrite <- agree_on_vars in H0. - apply (Var_load _ _ _ H0). + rewrite <- agree_on_vars in H2. + eapply Var_load; eauto. - split; intros eval_Const; inversion eval_Const; subst; econstructor; auto. - split; intros eval_Unop; inversion eval_Unop; subst; econstructor; try auto. + erewrite IHe; eauto. + erewrite IHe; eauto. + erewrite <- IHe; eauto. + erewrite <- IHe; eauto. - - split; intros eval_Binop; inversion eval_Binop; subst; econstructor; try auto; + - split; intros eval_Binop; inversion eval_Binop; subst; econstructor; eauto; + destruct m1; destruct m2; inversion H2; try (erewrite IHe1; eauto); - try (erewrite IHe2; eauto). + try (erewrite IHe2; eauto); auto. + - split; intros eval_Downcast; simpl; simpl in eval_Downcast; erewrite IHe; eauto. Qed. Lemma shadowing_free_rewriting_cmd f E1 E2 vR: (forall n, E1 n = E2 n) -> - bstep f E1 0 vR <-> - bstep f E2 0 vR. + bstep (toREvalCmd f) E1 vR M0 <-> + bstep (toREvalCmd f) E2 vR M0. Proof. - revert E1 E2 vR. +revert E1 E2 vR. induction f; intros E1 E2 vR agree_on_vars. - split; intros bstep_Let; inversion bstep_Let; subst. - + erewrite shadowing_free_rewriting_exp in H5; auto. + + erewrite shadowing_free_rewriting_exp in H6; auto. econstructor; eauto. rewrite <- IHf. - apply H6. + apply H7. intros n'; unfold updEnv. case_eq (n' =? n); auto. - + erewrite <- shadowing_free_rewriting_exp in H5; auto. + + erewrite <- shadowing_free_rewriting_exp in H6; auto. econstructor; eauto. rewrite IHf. - apply H6. + apply H7. intros n'; unfold updEnv. case_eq (n' =? n); auto. - split; intros bstep_Ret; inversion bstep_Ret; subst. @@ -241,13 +259,13 @@ Qed. Lemma dummy_bind_ok e v x v' inVars E: NatSet.Subset (usedVars e) inVars -> NatSet.mem x inVars = false -> - eval_exp 0 E (toRExp e) v -> - eval_exp 0 (updEnv x v' E) (toRExp e) v. + eval_exp E (toREval (toRExp e)) v M0 -> + eval_exp (updEnv x M0 v' E) (toREval (toRExp e)) v M0. Proof. revert v x v' inVars E. induction e; intros v1 x v2 inVars E valid_vars x_not_free eval_e. - inversion eval_e; subst. - assert ((updEnv x v2 E) n = E n). + assert ((updEnv x M0 v2 E) n = E n). + unfold updEnv. case_eq (n =? x); try auto. intros n_eq_x. @@ -261,13 +279,14 @@ Proof. rewrite <- NatSet.mem_spec in valid_vars. rewrite valid_vars in *; congruence. + econstructor. - rewrite H; auto. + eauto. + rewrite H; auto. - inversion eval_e; subst; constructor; auto. - - inversion eval_e; subst; constructor; auto. - + eapply IHe; eauto. - + eapply IHe; eauto. + - inversion eval_e; subst; econstructor; eauto. - simpl in valid_vars. - inversion eval_e; subst; constructor; auto. + inversion eval_e; subst; econstructor; eauto; + destruct m1; destruct m2; inversion H2; + subst. + eapply IHe1; eauto. hnf; intros a in_e1. apply valid_vars; @@ -276,20 +295,22 @@ Proof. hnf; intros a in_e2. apply valid_vars; rewrite NatSet.union_spec; auto. + - apply (IHe v1 x v2 inVars E); auto. Qed. Fixpoint exp_subst (e:exp Q) x e_new := match e with - |Var _ v => if v =? x then e_new else Var Q v + |Var _ m v => if v =? x then e_new else Var Q m v |Unop op e1 => Unop op (exp_subst e1 x e_new) |Binop op e1 e2 => Binop op (exp_subst e1 x e_new) (exp_subst e2 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: - eval_exp (0%R) E (toRExp e_sub) v -> - eval_exp (0%R) (updEnv x v E) (toRExp e) v_res <-> - eval_exp (0%R) E (toRExp (exp_subst e x e_sub)) v_res. + eval_exp E (toREval (toRExp e_sub)) v M0 -> + eval_exp (updEnv x M0 v E) (toREval (toRExp e)) v_res M0 <-> + eval_exp E (toREval (toRExp (exp_subst e x e_sub))) v_res M0. Proof. intros eval_e. revert v_res. @@ -298,87 +319,146 @@ Proof. + unfold updEnv in eval_upd. simpl in *. inversion eval_upd; subst. case_eq (n =? x); intros; try auto. - * rewrite H in H0. - inversion H0; subst; auto. - * rewrite H in H0. - apply (Var_load _ _ _ H0). + * rewrite H in H2. + inversion H2; subst; auto. + * rewrite H in H2. + eapply Var_load; eauto. + simpl in eval_subst. case_eq (n =? x); intros n_eq_case; rewrite n_eq_case in eval_subst. * simpl. - assert (updEnv x v E n = Some v_res). + assert (updEnv x M0 v E n = Some (v_res, M0)). { unfold updEnv; rewrite n_eq_case. - f_equal. eapply meps_0_deterministic; eauto. } - { econstructor; eauto. } + f_equal. assert (v = v_res) by (eapply meps_0_deterministic; eauto). rewrite H. auto. } + { econstructor; eauto. } * simpl. inversion eval_subst; subst. - assert (E n = updEnv x v E n). + assert (E n = updEnv x M0 v E n). { unfold updEnv; rewrite n_eq_case; reflexivity. } - { rewrite H in H0. apply (Var_load _ _ _ H0). } + { rewrite H in H2. eapply Var_load; eauto. } (*unfold updEnv in *. rewrite n_eq_case in *. unfold toREvalEnv. apply H4. }*) - intros v_res; split; [intros eval_upd | intros eval_subst]. + inversion eval_upd; constructor; auto. + inversion eval_subst; constructor; auto. - split; [intros eval_upd | intros eval_subst]. - + inversion eval_upd; constructor; try auto. - * rewrite <- IHe; auto. - * rewrite <- IHe; auto. - + inversion eval_subst; constructor; try auto. - * rewrite IHe; auto. - * rewrite IHe; auto. + + inversion eval_upd; econstructor; auto; + rewrite <- IHe; auto. + + inversion eval_subst; constructor; try auto; + rewrite IHe; auto. - intros v_res; split; [intros eval_upd | intros eval_subst]. - + inversion eval_upd; constructor; try auto. + + inversion eval_upd; econstructor; auto; + destruct m1; destruct m2; inversion H2. * rewrite <- IHe1; auto. * rewrite <- IHe2; auto. - + inversion eval_subst; constructor; try auto. + + inversion eval_subst; econstructor; auto; + destruct m1; destruct m2; inversion H2. * rewrite IHe1; auto. * rewrite IHe2; auto. + - split; [intros eval_upd | intros eval_subst]. + + rewrite <- IHe; auto. + + rewrite IHe; auto. Qed. Fixpoint map_subst (f:cmd Q) x e := match f with - |Let y e_y g => Let y (exp_subst e_y x e) (map_subst g x e) + |Let m y e_y g => Let m y (exp_subst e_y x e) (map_subst g x e) |Ret e_r => Ret (exp_subst e_r x e) end. + +(* Lemma updEnv_comp_toREval (n:nat) (v:R): *) +(* forall E var, updEnv n M0 v (toREvalEnv E) var = toREvalEnv (updEnv n M0 v E) var. *) +(* Proof. *) +(* intros. *) +(* unfold updEnv; unfold toREvalEnv. *) +(* case_eq (var =? n); intros; auto. *) +(* Qed. *) + +(* Lemma bli (e:exp Q) (n:nat) (v vR:R) (E:env): *) +(* eval_exp (toREvalEnv (updEnv n M0 v E)) (toREval (toRExp e)) vR M0 <-> *) +(* eval_exp (updEnv n M0 v (toREvalEnv E)) (toREval (toRExp e)) vR M0. *) +(* Proof. *) +(* revert e n v vR E. *) +(* induction e; split; intros. *) +(* - inversion H; subst; econstructor; eauto. *) +(* rewrite updEnv_comp_toREval; auto. *) +(* - inversion H; subst; econstructor; eauto. *) +(* rewrite <- updEnv_comp_toREval; auto. *) +(* - inversion H; subst; econstructor; eauto. *) +(* - inversion H; subst; econstructor; eauto. *) +(* - inversion H; subst; econstructor; eauto; apply IHe; auto. *) +(* - inversion H; subst; econstructor; eauto; apply IHe; auto. *) +(* - inversion H; subst; econstructor; eauto; *) +(* assert (m1 = M0) by (apply (ifM0isJoin_l M0 m1 m2); auto); *) +(* assert (m2 = M0) by (apply (ifM0isJoin_r M0 m1 m2); auto); subst. *) +(* apply IHe1; auto. *) +(* apply IHe2; auto. *) +(* - inversion H; subst; econstructor; eauto; *) +(* assert (m1 = M0) by (apply (ifM0isJoin_l M0 m1 m2); auto); *) +(* assert (m2 = M0) by (apply (ifM0isJoin_r M0 m1 m2); auto); subst. *) +(* apply IHe1; auto. *) +(* apply IHe2; auto. *) +(* - apply IHe; auto. *) +(* - apply IHe; auto. *) +(* Qed. *) + +(* Lemma bla (c: cmd Q) (n:nat) (v vR:R) (E:env): *) +(* bstep (toREvalCmd (toRCmd c)) (updEnv n M0 v (toREvalEnv E)) vR M0 <-> *) +(* bstep (toREvalCmd (toRCmd c)) (toREvalEnv (updEnv n M0 v E)) vR M0. *) +(* Proof. *) +(* revert c n v vR E. *) +(* induction c; split; intros. *) +(* - inversion H; subst. *) +(* econstructor; eauto. *) +(* apply bli; eauto. *) +(* apply IHc; auto. *) +(* Admitted. *) +(* remember (updEnv n0 M0 v (toREvalEnv E)) as E'. *) + +(* replace E' with (toREvalEnv E') in H9. *) +(* + apply IHc in H9. *) +(* rewrite HeqE' in H9. *) +(* replace E with (toREvalEnv E) by admit. *) +(* apply H9. *) +(* Admitted. *) + + Lemma stepwise_substitution x e v f E vR inVars outVars: - ssa f inVars outVars -> + ssa (toREvalCmd (toRCmd f)) inVars outVars -> NatSet.In x inVars -> NatSet.Subset (usedVars e) inVars -> - eval_exp 0%R E (toRExp e) v -> - bstep (toRCmd f) (updEnv x v E) 0%R vR <-> - bstep (toRCmd (map_subst f x e)) E 0%R vR. + eval_exp E (toREval (toRExp e)) v M0 -> + bstep (toREvalCmd (toRCmd f)) (updEnv x M0 v E) vR M0 <-> + bstep (toREvalCmd (toRCmd (map_subst f x e))) E vR M0. Proof. revert E e x vR inVars outVars. induction f; intros E e0 x vR inVars outVars ssa_f x_free valid_vars_e eval_e. - split; [ intros bstep_let | intros bstep_subst]. + inversion bstep_let; subst. - simpl in *. inversion ssa_f; subst. - assert (forall E var, updEnv n v0 (updEnv x v E) var = updEnv x v (updEnv n v0 E) var). + assert (forall E var, updEnv n M0 v0 (updEnv x M0 v E) var = updEnv x M0 v (updEnv n M0 v0 E) var). * eapply ssa_shadowing_free. apply ssa_f. apply x_free. - apply H5. - * rewrite (shadowing_free_rewriting_cmd _ _ _ _ (H E)) in H6. - econstructor; auto. - rewrite <- exp_subst_correct; eauto. - rewrite <- IHf; eauto. - rewrite NatSet.add_spec. - right; auto. - apply validVars_add; auto. - eapply dummy_bind_ok; eauto. + apply H6. + * erewrite (shadowing_free_rewriting_cmd _ _ _ _) in H7; try eauto. + simpl in *. + econstructor; eauto. + { rewrite <- exp_subst_correct; eauto. } + { rewrite <- IHf; eauto. + rewrite NatSet.add_spec; right; auto. + apply validVars_add; auto. + eapply dummy_bind_ok; eauto. } + inversion bstep_subst; subst. simpl in *. inversion ssa_f; subst. - econstructor. + econstructor; try auto. rewrite exp_subst_correct; eauto. - rewrite <- IHf in H6; eauto. - rewrite <- shadowing_free_rewriting_cmd in H6; eauto. - eapply ssa_shadowing_free; eauto. - rewrite <- exp_subst_correct in H5; eauto. - rewrite NatSet.add_spec. - right; auto. - apply validVars_add; auto. - eapply dummy_bind_ok; eauto. + rewrite <- IHf in H7; eauto. + * rewrite <- shadowing_free_rewriting_cmd in H7; eauto. + eapply ssa_shadowing_free; eauto. + rewrite <- exp_subst_correct in H6; eauto. + * rewrite NatSet.add_spec; auto. + * apply validVars_add; auto. + * eapply dummy_bind_ok; eauto. - split; [intros bstep_let | intros bstep_subst]. + inversion bstep_let; subst. simpl in *. @@ -387,20 +467,20 @@ Proof. + inversion bstep_subst; subst. simpl in *. rewrite <- exp_subst_correct in H0; eauto. - constructor; assumption. + econstructor; eauto. Qed. Fixpoint let_subst (f:cmd Q) := match f with - | Let x e1 g => + | Let m x e1 g => exp_subst (let_subst g) x e1 | Ret e1 => e1 end. Lemma eval_subst_subexp E e' n e vR: NatSet.In n (usedVars e) -> - eval_exp 0 E (toRExp (exp_subst e n e')) vR -> - exists v, eval_exp 0 E (toRExp e') v. + eval_exp E (toREval (toRExp (exp_subst e n e'))) vR M0 -> + exists v, eval_exp E (toREval (toRExp e')) v M0. Proof. revert E e' n vR. induction e; @@ -415,14 +495,15 @@ Proof. eapply IHe; eauto. - inversion eval_subst; subst. rewrite NatSet.union_spec in n_fVar. + destruct m1; destruct m2; inversion H2. destruct n_fVar as [n_fVar_e1 | n_fVare2]; [eapply IHe1; eauto | eapply IHe2; eauto]. Qed. Lemma bstep_subst_subexp_any E e x f vR: NatSet.In x (liveVars f) -> - bstep (toRCmd (map_subst f x e)) E 0 vR -> - exists E' v, eval_exp 0 E' (toRExp e) v. + bstep (toREvalCmd (toRCmd (map_subst f x e))) E vR M0 -> + exists E' v, eval_exp E' (toREval (toRExp e)) v M0. Proof. revert E e x vR; induction f; @@ -440,13 +521,14 @@ Qed. Lemma bstep_subst_subexp_ret E e x e' vR: NatSet.In x (liveVars (Ret e')) -> - bstep (toRCmd (map_subst (Ret e') x e)) E 0 vR -> - exists v, eval_exp 0 E (toRExp e) v. + bstep (toREvalCmd (toRCmd (map_subst (Ret e') x e))) E vR M0 -> + exists v, eval_exp E (toREval (toRExp e)) v M0. Proof. simpl; intros x_live bstep_ret. inversion bstep_ret; subst. eapply eval_subst_subexp; eauto. Qed. + Lemma no_forward_refs V (f:cmd V) inVars outVars: ssa f inVars outVars -> forall v, NatSet.In v (definedVars f) -> @@ -464,19 +546,19 @@ Proof. - intros v v_in_empty; inversion v_in_empty. Qed. -Lemma bstep_subst_subexp_let E e x y e' g vR: - NatSet.In x (liveVars (Let y e' g)) -> +Lemma bstep_subst_subexp_let E e x y e' g vR m: + NatSet.In x (liveVars (Let m y e' g)) -> (forall x, NatSet.In x (usedVars e) -> exists v, E x = v) -> - bstep (toRCmd (map_subst (Let y e' g) x e)) E 0 vR -> - exists v, eval_exp 0 E (toRExp e) v. + bstep (toREvalCmd (toRCmd (map_subst (Let m y e' g) x e))) E vR M0 -> + exists v, eval_exp E (toREval (toRExp e)) v M0. Proof. revert E e x y e' vR; induction g; intros E e0 x y e' vR x_live uedVars_def bstep_f. - simpl in *. inversion bstep_f; subst. - specialize (IHg (updEnv y v E) e0 x n e). + specialize (IHg (updEnv y m v E) e0 x n e). rewrite NatSet.union_spec in x_live. destruct x_live as [x_used | x_live]. + eapply eval_subst_subexp; eauto. @@ -488,8 +570,8 @@ Theorem let_free_agree f E vR inVars outVars e: (forall v, NatSet.In v (definedVars f) -> NatSet.In v (liveVars f)) -> let_subst f = e -> - bstep (toRCmd (Ret e)) E 0 vR -> - bstep (toRCmd f) E 0 vR. + bstep (toREvalCmd (toRCmd (Ret e))) E vR M0 -> + bstep (toREvalCmd (toRCmd f)) E vR M0. Proof. intros ssa_f. revert E vR e; @@ -498,7 +580,7 @@ Proof. simpl in *. (* Let Case, prove that the value of the let binding must be used somewhere *) - case_eq (let_subst s). - + intros e0 subst_s; rewrite subst_s in *. + + intros m0 e0 subst_s; rewrite subst_s in *. Admitted. (*inversion subst_step; subst. clear subst_s subst_step. @@ -520,11 +602,11 @@ Admitted. Theorem let_free_form f E vR inVars outVars e: ssa f inVars outVars -> - bstep (toRCmd f) E 0 vR -> + bstep (toREvalCmd (toRCmd f)) E vR M0 -> let_subst f = e -> - bstep (toRCmd (Ret e)) E 0 vR. + bstep (toREvalCmd (toRCmd (Ret e))) E vR M0. Proof. - revert E vR inVars outVars e; + revert E vR inVars outVars e; induction f; intros E vR inVars outVars e_subst ssa_f bstep_f subst_step. - simpl. @@ -533,7 +615,7 @@ Proof. Admitted. (* case_eq (let_subst f). + intros f_subst subst_f_eq. - specialize (IHf (updEnv n v E) vR (NatSet.add n inVars) outVars f_subst H8 H6 subst_f_eq). + specialize (IHf (updEnv n M0 v E) vR (NatSet.add n inVars) outVars f_subst H9 H7 subst_f_eq). rewrite subst_f_eq in subst_step. inversion IHf; subst. constructor. @@ -564,4 +646,5 @@ Proof. induction ssa_f; intros VarEnv ParamEnv P eps fVars_live. - - *) \ No newline at end of file + *) +