diff --git a/coq/Commands.v b/coq/Commands.v index 3a1950b361fc5aa57e82b1e311a228a95bf9dd02..5adacde24bbd2febb0c5b7048642052da35392a5 100644 --- a/coq/Commands.v +++ b/coq/Commands.v @@ -33,9 +33,6 @@ Fixpoint toREvalCmd (f:cmd R) := |Ret e => Ret (toREval e) end. - -(*| Nop: cmd V. *) - (* UNUSED! Small Step semantics for Daisy language @@ -52,16 +49,6 @@ Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop := Define big step semantics for the Daisy language, terminating on a "returned" result value **) - -(* 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 -> diff --git a/coq/ErrorBounds.v b/coq/ErrorBounds.v index 204dffff21344dd3559657c62bc5be5f864c95fe..5bdd694c21aad62e73cc1f0a0b2a03a274be1811 100644 --- a/coq/ErrorBounds.v +++ b/coq/ErrorBounds.v @@ -36,7 +36,6 @@ Proof. inversion eval_float; subst. unfold perturb; simpl. exists v; split; try auto. - rewrite H3 in H8; inversion H8. rewrite Rabs_err_simpl. repeat rewrite Rabs_mult. diff --git a/coq/ErrorValidation.v b/coq/ErrorValidation.v index f0aac13657462f1e24cfd6fb1ea325592669024e..e5e02a81597730ee9d7d3da5c693503e5f213b9c 100644 --- a/coq/ErrorValidation.v +++ b/coq/ErrorValidation.v @@ -129,21 +129,9 @@ Proof. 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; 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. @@ -193,8 +181,8 @@ Proof. + apply IHapproxCEnv; try auto. * constructor; auto. * constructor; auto. - * intros v0 m2 (*overVar*) mem_dVars (*isSubExpr*). - specialize (dVars_sound v0 m2 (*overVar*) mem_dVars (*isSubExpr*)). + * intros v0 m2 mem_dVars. + specialize (dVars_sound v0 m2 mem_dVars). destruct dVars_sound as [vR0 [mR0 iv_sound_val]]. case_eq (v0 =? x); intros case_mem; rewrite case_mem in iv_sound_val; simpl in iv_sound_val. @@ -250,8 +238,8 @@ 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 m2 (*overVar*) mem_dVars (*isSubExpr*). - specialize (dVars_sound v0 m2 (*overVar*)). + * intros v0 m2 mem_dVars. + specialize (dVars_sound v0 m2). 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. @@ -345,12 +333,6 @@ Proof. try eauto. 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. @@ -1946,8 +1928,6 @@ Proof. 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. @@ -2056,7 +2036,6 @@ Proof. 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. @@ -2087,13 +2066,6 @@ Proof. 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. rewrite NatSet.diff_spec in in_diff. @@ -2101,13 +2073,6 @@ Proof. 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_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. @@ -2124,67 +2089,17 @@ Proof. apply fVars_subset. rewrite NatSet.diff_spec, NatSet.union_spec. split; try auto. } - * (*destruct m1; destruct m2; inversion H3.*) - destruct H0, H1, H. destruct b. + * destruct H0, H1, H. destruct b. { eapply (validErrorboundCorrectAddition (e1:=e1) absenv); eauto. 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. 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. 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. - 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 ]. @@ -2208,18 +2123,6 @@ Proof. 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. @@ -2278,46 +2181,6 @@ Proof. 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 m Gamma, validTypeCmd Gamma f m -> @@ -2338,7 +2201,7 @@ Theorem validErrorboundCmd_sound (f:cmd Q) (absenv:analysisResult): (Rabs (vR - vF) <= (Q2R err))%R. Proof. induction f; - intros * type_f approxc1c2 ssa_f freeVars_subset eval_real eval_float (*issubcmd_ok*) valid_bounds valid_intv fVars_sound P_valid absenv_res. + intros * type_f approxc1c2 ssa_f freeVars_subset eval_real eval_float valid_bounds valid_intv fVars_sound P_valid absenv_res. - simpl in eval_real, eval_float. inversion eval_float; inversion eval_real; subst. inversion ssa_f; subst. @@ -2383,21 +2246,6 @@ Proof. assumption. - instantiate (1 := q0). instantiate (1 := q). rewrite absenv_e; auto. } - (* * inversion ssa_f; subst. - case_eq (NatSet.mem n fVars); intros case_mem. - { rewrite NatSet.mem_spec in case_mem. - assert (NatSet.In n fVars \/ NatSet.In n dVars) as in_disj by (left; auto). - rewrite <- NatSet.union_spec, <- NatSet.mem_spec in in_disj. - hnf in inVars_union. - rewrite NatSet.mem_spec in in_disj. - rewrite inVars_union in in_disj. - rewrite <- NatSet.mem_spec in in_disj. - rewrite in_disj in H7. inversion H7. } - { case_eq (NatSet.mem n (NatSet.union fVars dVars)); intros case_union; try auto. - rewrite NatSet.mem_spec in case_union. - rewrite inVars_union in case_union. - rewrite <- NatSet.mem_spec in case_union. - rewrite case_union in H7; inversion H7. } *) + simpl in valid_bounds. andb_to_prop valid_bounds. rename L0 into validbound_e; diff --git a/coq/Expressions.v b/coq/Expressions.v index 9cede73db38e715b7eef87aa703c7f51706d1873..0d787188d3d5f8bdb40f2cd87840ee2378716827 100644 --- a/coq/Expressions.v +++ b/coq/Expressions.v @@ -13,11 +13,12 @@ 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 - | Sub => match b2 with Sub => true |_ => false end - | Mult => match b2 with Mult => true |_ => false end - | Div => match b2 with Div => true |_ => false end + match b1, b2 with + | Plus, Plus => true + | Sub, Sub => true + | Mult, Mult => true + | Div, Div => true + | _,_ => false end. (** @@ -45,9 +46,10 @@ Qed. Inductive unop: Type := Neg | Inv. Definition unopEqBool (o1:unop) (o2:unop) := - match o1 with - |Neg => match o2 with |Neg => true |_=> false end - |Inv => match o2 with |Inv => true |_ => false end + match o1, o2 with + | Neg, Neg => true + | Inv, Inv => true + | _ , _ => false end. (** @@ -78,57 +80,16 @@ Inductive exp (V:Type): Type := Used in certificates to define the analysis result as function **) Fixpoint expEqBool (e1:exp Q) (e2:exp Q) := - match e1 with - |Var _ m1 v1 => - match e2 with - |Var _ m2 v2 => andb (mTypeEqBool m1 m2) (v1 =? v2) - | _=> false - end - |Const m1 n1 => - match e2 with - |Const m2 n2 => andb (mTypeEqBool m1 m2) (Qeq_bool n1 n2) - | _=> false - end - |Unop o1 e11 => - match e2 with - |Unop o2 e22 => andb (unopEqBool o1 o2) (expEqBool e11 e22) - |_ => false - end - |Binop o1 e11 e12 => - match e2 with - |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 + match e1, e2 with + | Var _ m1 v1, Var _ m2 v2 => andb (mTypeEqBool m1 m2) (v1 =? v2) + | Const m1 n1, Const m2 n2 => andb (mTypeEqBool m1 m2) (Qeq_bool n1 n2) + | Unop o1 e11, Unop o2 e22 => andb (unopEqBool o1 o2) (expEqBool e11 e22) + | Binop o1 e11 e12, Binop o2 e21 e22 => andb (binopEqBool o1 o2) (andb (expEqBool e11 e21) (expEqBool e12 e22)) + | Downcast m1 f1, Downcast m2 f2 => andb (mTypeEqBool m1 m2) (expEqBool f1 f2) + | _, _ => false 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. @@ -221,8 +182,7 @@ Proof. eapply IHe; eauto. Qed. - - + Fixpoint toRExp (e:exp Q) := match e with @@ -265,8 +225,6 @@ using a perturbation of the real valued computation by (1 + delta), where **) 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: @@ -280,7 +238,6 @@ Inductive eval_exp (E:env) :(exp R) -> R -> mType -> Prop := 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 -> @@ -401,14 +358,10 @@ Proof. 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) (m:mType) (E:env) (v:R): (eval_exp E (Unop Inv e) v m -> exists v1 m1, @@ -422,18 +375,6 @@ Proof. 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. (** diff --git a/coq/Infra/Abbrevs.v b/coq/Infra/Abbrevs.v index 08c1f05436d16830c567a5ee47e97f5e6898add3..5330daa35c327ca5657624ce0203132e4359d9b0 100644 --- a/coq/Infra/Abbrevs.v +++ b/coq/Infra/Abbrevs.v @@ -58,95 +58,4 @@ Definition emptyEnv:env := fun _ => None. 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 + else E y. \ No newline at end of file diff --git a/coq/Infra/MachineType.v b/coq/Infra/MachineType.v index dc9e2f020b685556e98bf5c379c2686470c732e2..a63e4da0b0085dfc298c3dde2563bbfecd776114 100644 --- a/coq/Infra/MachineType.v +++ b/coq/Infra/MachineType.v @@ -158,79 +158,6 @@ Definition isJoinOf (m:mType) (m1:mType) (m2:mType) := 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. @@ -301,30 +228,4 @@ Proof. 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 (Q2R b < 0 \/ 0 < Q2R a)%R. diff --git a/coq/IntervalValidation.v b/coq/IntervalValidation.v index b91a005ae30d5577cd637b95adf4d6cb97eab899..7b3ccb7f19ebaa5095d5cf2301e3cdc34e341aa2 100644 --- a/coq/IntervalValidation.v +++ b/coq/IntervalValidation.v @@ -183,74 +183,6 @@ Proof. 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, @@ -331,8 +263,7 @@ Proof. destruct valid_bounds as [valid_rec valid_unop]. apply Is_true_eq_true in valid_rec. inversion eval_f; subst. - + (*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. + + 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 *) @@ -351,8 +282,7 @@ Proof. * eapply Rle_trans. Focus 2. apply valid_hi. rewrite Q2R_opp; lra. - + (*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. + + 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. @@ -439,15 +369,6 @@ Proof. apply Is_true_eq_true in valid_e1; apply Is_true_eq_true in valid_e2. destruct m1; destruct m2; cbv in H2; inversion H2. 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. @@ -479,7 +400,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. (*rewrite absenv_bin;*) apply valid_lo. + - eapply Rle_trans. apply valid_lo. unfold ivlo. unfold addIntv. simpl in valid_add_lo. repeat rewrite <- Q2R_plus in valid_add_lo. @@ -487,7 +408,7 @@ Proof. unfold absIvUpd; auto. - eapply Rle_trans. Focus 2. - (*rewrite absenv_bin;*) apply valid_hi. + apply valid_hi. unfold ivlo, addIntv. simpl in valid_add_hi. repeat rewrite <- Q2R_plus in valid_add_hi. @@ -503,7 +424,8 @@ 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. (*rewrite absenv_bin;*) apply valid_lo. + - eapply Rle_trans. + apply valid_lo. unfold ivlo. unfold subtractIntv. simpl in valid_sub_lo. repeat rewrite <- Rsub_eq_Ropp_Rplus in valid_sub_lo. @@ -512,7 +434,7 @@ Proof. unfold absIvUpd; auto. - eapply Rle_trans. Focus 2. - (*rewrite absenv_bin;*) apply valid_hi. + apply valid_hi. unfold ivlo, addIntv. simpl in valid_sub_hi. repeat rewrite <- Rsub_eq_Ropp_Rplus in valid_sub_hi. @@ -529,7 +451,8 @@ 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. (*rewrite absenv_bin;*) apply valid_lo. + - eapply Rle_trans. + apply valid_lo. unfold ivlo. unfold multIntv. simpl in valid_mul_lo. repeat rewrite <- Q2R_mult in valid_mul_lo. @@ -537,7 +460,7 @@ Proof. unfold absIvUpd; auto. - eapply Rle_trans. Focus 2. - (*rewrite absenv_bin;*) apply valid_hi. + apply valid_hi. unfold ivlo, addIntv. simpl in valid_mul_hi. repeat rewrite <- Q2R_mult in valid_mul_hi. @@ -581,7 +504,7 @@ Proof. rewrite ivlo2_0 in H0. lra. } { split. - - eapply Rle_trans. (*rewrite absenv_bin;*) apply valid_lo. + - eapply Rle_trans. apply valid_lo. unfold ivlo. unfold multIntv. simpl in valid_div_lo. rewrite <- Q2R_inv in valid_div_lo; [ | auto]. @@ -590,7 +513,7 @@ Proof. rewrite <- Q2R_min4 in valid_div_lo; auto. - eapply Rle_trans. Focus 2. - (*rewrite absenv_bin;*) apply valid_hi. + apply valid_hi. simpl in valid_div_hi. rewrite <- Q2R_inv in valid_div_hi; [ | auto]. rewrite <- Q2R_inv in valid_div_hi; [ | auto]. @@ -601,7 +524,6 @@ Proof. + 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. @@ -717,4 +639,3 @@ Qed. (* + simpl in valid_bounds_f; eapply validIntervalbounds_sound; eauto. *) (* + simpl in *. rewrite absenv_f in *; auto. *) (* Qed. *) - diff --git a/coq/Typing.v b/coq/Typing.v index 9a31ffec351f863a5f880ae6b6e47096accfe329..c5b4d1a654fd29d0d2a2bbe549a940a4e624a0a7 100644 --- a/coq/Typing.v +++ b/coq/Typing.v @@ -591,696 +591,3 @@ Admitted. (* + 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 f0f6c63d49f71572cb6f071d08340a8a8504106e..4d76d691db70d4cf0ecf5f880aee2296bfdafd2e 100644 --- a/coq/ssaPrgs.v +++ b/coq/ssaPrgs.v @@ -199,9 +199,6 @@ Qed. Lemma shadowing_free_rewriting_exp e v E1 E2: -(* (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. @@ -210,7 +207,6 @@ Proof. induction e; intros v' E1 E2 agree_on_vars. - split; intros eval_Var. + inversion eval_Var; subst. - (*assert (m1 = M0) by (apply ifisMorePreciseM0; auto); subst.*) rewrite agree_on_vars in H2. eapply Var_load; eauto. + inversion eval_Var; subst. @@ -334,7 +330,7 @@ Proof. * simpl. inversion eval_subst; subst. assert (E n = updEnv x M0 v E n). { unfold updEnv; rewrite n_eq_case; reflexivity. } - { rewrite H in H2. eapply Var_load; eauto. } (*unfold updEnv in *. rewrite n_eq_case in *. unfold toREvalEnv. apply H4. }*) + { rewrite H in H2. eapply Var_load; eauto. } - intros v_res; split; [intros eval_upd | intros eval_subst]. + inversion eval_upd; constructor; auto. + inversion eval_subst; constructor; auto. @@ -363,64 +359,6 @@ Fixpoint map_subst (f:cmd Q) 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 (toREvalCmd (toRCmd f)) inVars outVars -> NatSet.In x inVars ->