Commit 615bcb77 authored by ='s avatar =

Removing unused/commented proofs.

I also simplified the double pattern matchings used in Expressions.v
parent 57805bbd
......@@ -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 ->
......
......@@ -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.
......
......@@ -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;
......
......@@ -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.
(**
......
......@@ -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
......@@ -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. *) *)