Merge branch 'new_semantics' of gitlab.mpi-sws.org:hbecker/daisy into certificates

coq/CertificateChecker.v

@@ -13,7 +13,9 @@ Require Export Daisy.Infra.ExpressionAbbrevs.
 
 (** Certificate checking function **)
 Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
-  andb (validIntervalbounds e absenv P NatSet.empty) (validErrorbound e absenv NatSet.empty).
+  if (validIntervalbounds e absenv P NatSet.empty)
+  then (validErrorbound e absenv NatSet.empty)
+  else false.
 
 (**
    Soundness proof for the certificate checker.
@@ -22,10 +24,11 @@ Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
 **)
 Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P:
   forall (E1 E2:env) (vR:R) (vF:R) fVars,
-    (forall v, NatSet.mem v (Expressions.freeVars e)= true ->
+    approxEnv E1 absenv fVars NatSet.empty E2 ->
+    (forall v, NatSet.mem v fVars = true ->
           exists vR, E1 v = Some vR /\
                 (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
-    approxEnv E1 absenv fVars NatSet.empty E2 ->
+    NatSet.Subset (Expressions.freeVars e) fVars ->
     eval_exp 0%R E1 (toRExp e) vR ->
     eval_exp (Q2R machineEpsilon) E2 (toRExp e) vF ->
     CertificateChecker e absenv P = true ->
@@ -35,32 +38,37 @@ Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P:
    validator and the error bound validator.
 **)
 Proof.
-  intros VarEnv1 VarEnv2 ParamEnv vR vF P_valid approxC1C2 eval_real eval_float certificate_valid.
+  intros E1 E2 vR vF fVars 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.
-  assert (exists iv err, absenv e = (iv,err)) by (destruct (absenv e); repeat eexists).
-  destruct H as [iv [err absenv_eq]].
-  assert (exists ivlo ivhi, iv = (ivlo, ivhi)) by (destruct iv; repeat eexists).
-  destruct H as [ivlo [ ivhi iv_eq]].
-  subst; rewrite absenv_eq in *; simpl in *.
-  eapply (validErrorbound_sound); eauto.
-  intros v v_in_empty.
-  rewrite NatSet.mem_spec in v_in_empty.
-  hnf in v_in_empty.
-  inversion v_in_empty.
-  admit.
-Admitted.
+  env_assert absenv e env_e.
+  destruct env_e as [iv [err absenv_eq]].
+  destruct iv as [ivlo ivhi].
+  rewrite absenv_eq; simpl.
+  eapply validErrorbound_sound; eauto.
+  - hnf. intros a in_diff.
+    rewrite NatSet.diff_spec in in_diff.
+    apply fVars_subset.
+    destruct in_diff; auto.
+  - intros v v_in_empty.
+    rewrite NatSet.mem_spec in v_in_empty.
+    inversion v_in_empty.
+Qed.
 
 Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) :=
-  andb (validIntervalboundsCmd f absenv P NatSet.empty)
-       (validErrorboundCmd f absenv NatSet.empty).
+  if (validIntervalboundsCmd f absenv P NatSet.empty)
+  then (validErrorboundCmd f 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,
+    approxEnv E1 absenv fVars NatSet.empty E2 ->
     (forall v, NatSet.mem v fVars= true ->
           exists vR, E1 v = Some vR /\
                 (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
-    approxEnv E1 absenv fVars NatSet.empty E2 ->
+    NatSet.Subset (Commands.freeVars f) fVars ->
     ssaPrg f fVars outVars ->
     bstep (toRCmd f) E1 0 vR ->
     bstep (toRCmd f) E2 (Q2R machineEpsilon) vF ->
@@ -71,22 +79,28 @@ 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 P_valid approxC1C2 ssa_f eval_real eval_float
+  intros E1 E2 outVars vR vF fVars 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.
   andb_to_prop certificate_valid.
-  assert (exists iv err, absenv (getRetExp f) = (iv,err)) by (destruct (absenv (getRetExp f)); repeat eexists).
-  destruct H as [iv [err absenv_eq]].
-  assert (exists ivlo ivhi, iv = (ivlo, ivhi)) by (destruct iv; repeat eexists).
-  destruct H as [ivlo [ ivhi iv_eq]].
-  subst; rewrite absenv_eq in *; simpl in *.
+  env_assert absenv (getRetExp f) env_f.
+  destruct env_f as [iv [err absenv_eq]].
+  destruct iv as [ivlo ivhi].
+  rewrite absenv_eq; simpl.
   eapply (validErrorboundCmd_sound); eauto.
-  - hnf.
-    intros a; split; intros in_set.
-    + rewrite NatSet.union_spec in in_set.
-      destruct in_set; try auto.
-      inversion H.
+  - instantiate (1 := outVars).
+    eapply ssa_equal_set; try eauto.
+    hnf.
+    intros a; split; intros in_union.
+    + rewrite NatSet.union_spec in in_union.
+      destruct in_union as [in_fVars | in_empty]; try auto.
+      inversion in_empty.
     + rewrite NatSet.union_spec; auto.
+  - hnf; intros a in_diff.
+    rewrite NatSet.diff_spec in in_diff.
+    destruct in_diff.
+    apply fVars_subset; auto.
   - intros v v_in_empty.
     rewrite NatSet.mem_spec in v_in_empty.
     inversion v_in_empty.

coq/Commands.v

@@ -23,7 +23,7 @@ Fixpoint toRCmd (f:cmd Q) :=
 
 Fixpoint toREvalCmd (f:cmd R) :=
   match f with
-  |Let m x e g => Let m x (toREval e) (toREvalCmd g)
+  |Let m x e g => Let M0 x (toREval e) (toREvalCmd g)
   |Ret e => Ret (toREval e)
   end.
 
@@ -45,23 +45,23 @@ Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
 (**
   Analogously define Big Step semantics for the Daisy language
  **)
-Inductive bstep : cmd R -> env -> R * mType -> Prop :=
+Inductive bstep : cmd R -> env -> R -> mType -> Prop :=
   let_b m m1 x e s E v res:
     isMorePrecise m1 m = true ->
-    eval_exp E e (v,m) ->
-    bstep s (updEnv x m v E) (res,m) ->
-    bstep (Let m1 x e s) E (res,m)
- |ret_b e E v:
-    eval_exp E e v ->
-    bstep (Ret e) E v.
+    eval_exp E e v m ->
+    bstep s (updEnv x m v E) res m ->
+    bstep (Let m1 x e s) E res m
+ |ret_b m e E v:
+    eval_exp E e v m ->
+    bstep (Ret e) E v m.
 
-Fixpoint freeVars (f:cmd Q) :NatSet.t :=
+Fixpoint freeVars V (f:cmd V) :NatSet.t :=
   match f with
   | Let _ x e1 g => NatSet.remove x (NatSet.union (Expressions.freeVars e1) (freeVars g))
   | Ret e => Expressions.freeVars e
   end.
 
-Fixpoint definedVars (f:cmd Q) :NatSet.t :=
+Fixpoint definedVars V (f:cmd V) :NatSet.t :=
   match f with
   | Let _ x _ g => NatSet.add x (definedVars g)
   | Ret _ => NatSet.empty

coq/Environments.v

@@ -17,14 +17,14 @@ Inductive approxEnv : env -> analysisResult -> NatSet.t -> NatSet.t -> env -> Pr
    approxEnv emptyEnv A NatSet.empty NatSet.empty emptyEnv
 |approxUpdFree E1 E2 A v1 v2 x fVars dVars m:
    approxEnv E1 A fVars dVars E2 ->
-   (Rabs (v1 - v2) <= v1 * Q2R (meps m))%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)
+   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 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 -> env -> Prop :=
 |approxParamRefl:
@@ -32,4 +32,4 @@ Inductive approxParams :env -> env -> Prop :=
 |approxParamUpd E1 E2 m x v1 v2 :
    approxParams E1 E2 ->
    (Rabs (v1 - v2) <= Q2R (meps m))%R ->
-   approxParams (updEnv x v1 E1) (updEnv x v2 E2).
+   approxParams (updEnv x M0 v1 E1) (updEnv x m v2 E2).

coq/Expressions.v

@@ -116,7 +116,7 @@ Fixpoint toREval (e:exp R) :=
   | Const n => Const n
   | Unop o e1 => Unop o (toREval e1)
   | Binop o e1 e2 => Binop o (toREval e1) (toREval e2)
-  | Downcast _ e1 => (toREval e1)
+  | Downcast _ e1 =>  (toREval e1)
   end.
 
 Definition toREvalEnv (E:env) : env :=
@@ -193,107 +193,39 @@ Proof.
   lra.
 Qed.
 
-
-(* Lemma compat_eexp (E:env) (f f':exp R) (v:R): *)
-(*   forall m1, *)
-(*     mTypeEq m1 M0 -> *)
-(*     f' = toREval f -> *)
-(*     eval_exp E f' v m1 <-> *)
-(*     eval_exp E f' v M0. *)
-(* Proof. *)
-(*   intros m1 meq. *)
-(*   induction f'; intros; split; intros; inversion H0; subst; auto. *)
-(*   - constructor; auto. *)
-(*     unfold isMorePrecise in *. *)
-(*     unfold mTypeEqBool in *. *)
-(*     case_eq (Qeq_bool (meps m) (meps M0)); intros; auto. *)
-(*     rewrite H1 in H3. *)
-(*     apply mTypeEquivs in meq; unfold mTypeEqBool in meq; rewrite meq in H3. *)
-(*     inversion H3. *)
-(*   - admit. *)
-(*   - constructor; auto. *)
-(*     unfold mTypeEq in meq. *)
-(*     apply Qeq_eqR in meq. *)
-(*     rewrite <- meq; auto. *)
-(*   - admit. *)
-(*   - constructor; auto. *)
-
-(*   -  constructor. *)
-(*     unfold mTypeEq in meq. *)
-(*     apply Qeq_eqR in meq. *)
-(*     rewrite meq in H. *)
-(*     auto. *)
-(*   - constructor. *)
-(*     apply (IHeval_exp meq); auto. *)
-(*   - constructor. *)
-(*     unfold mTypeEq in meq; apply Qeq_eqR in meq; rewrite <- meq; auto. *)
-(*     apply IHeval_exp; auto. *)
-(*   - assert (isJoinOf M0 m1 m2 = true) as join012. *)
-(*     apply (eq_compat_join m M0 m1 m2); auto. *)
-(*     apply (Binop_dist M0 op delta join012); auto. *)
-(*     unfold mTypeEq in meq; apply Qeq_eqR in meq; rewrite <- meq; auto. *)
-(*   - apply (Downcast_dist m delta). *)
     
-(* Qed. *)
-
-
-(*     Lemma bla (m:mType) E f v: *)
-(*   (meps m) == 0 -> *)
-(*   eval_exp E (toREval f) v m <-> eval_exp E (toREval f) v M0. *)
-(* Proof. *)
-(*   intros. *)
-(*   assert (mTypeEq m M0). *)
-(*   unfold mTypeEq. *)
-(*   rewrite H. *)
-(*   simpl (meps M0). *)
-(*   lra. *)
-(*   rewrite H0. *)
-(*   split; trivial. *)
-(* Qed. *)
-
 Lemma general_meps_0_deterministic (f:exp R) (E:env):
-  forall v1 v2 m1 m2,
-    (meps m1) == 0 ->
-    (meps m2) == 0 ->
+  forall v1 v2 m1,
+    m1 = M0 ->
     eval_exp E (toREval f) v1 m1 ->
-    eval_exp E (toREval f) v2 m2 ->
+    eval_exp E (toREval f) v2 M0 ->
     v1 = v2.
 Proof.
-  induction f; intros v1 v2 m1 m2 meps1 meps2 eval_v1 eval_v2.
+  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 H4 in H10; inversion H10; 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.
-    rewrite (Qeq_eqR (meps m1) 0 meps1) in H0.
-    rewrite (Qeq_eqR (meps m2) 0 meps2) in H4.
-    rewrite Q2R0_is_0 in *.
-    rewrite delta_0_deterministic; auto. symmetry. rewrite delta_0_deterministic; 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.
-    + apply Ropp_eq_compat. apply (IHf v0 v3 m1 m2); auto.     
+    + apply Ropp_eq_compat. apply (IHf v0 v3 M0); auto.     
     + inversion H4.
     + inversion H5.
-    + rewrite (Qeq_eqR (meps m1) 0 meps1) in H1.
-      rewrite (Qeq_eqR (meps m2) 0 meps2) in H7.
-      rewrite Q2R0_is_0 in *.
-      rewrite delta_0_deterministic; auto. symmetry. rewrite delta_0_deterministic; auto.
-      rewrite (IHf v0 v3 m1 m2); auto.
+    + 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.
-    rewrite (Qeq_eqR (meps m1) 0 meps1) in H3.
-    rewrite (Qeq_eqR (meps m2) 0 meps2) in H12.
-    rewrite Q2R0_is_0 in *.
-    rewrite delta_0_deterministic; auto. symmetry. rewrite delta_0_deterministic; auto.
-    rewrite (IHf1 v0 v4 m0 m5); auto.
-    rewrite (IHf2 v5 v3 m6 m3); auto.
-    apply (ifM0isJoin_r m2 m5 m6); auto.
-    apply (ifM0isJoin_r m1 m0 m3); auto.
-    apply (ifM0isJoin_l m1 m0 m3); auto.
-    apply (ifM0isJoin_l m2 m5 m6); auto.
+    assert (M0 = M0) as M00 by auto.
+    pose proof (ifM0isJoin_l M0 m0 m2 M00 H2); auto.
+    pose proof (ifM0isJoin_r M0 m0 m2 M00 H2); auto.
+    pose proof (ifM0isJoin_l M0 m4 m5 M00 H11); auto.
+    pose proof (ifM0isJoin_r M0 m4 m5 M00 H11); auto.
+    subst.
+    rewrite (IHf1 v0 v4 M0); auto.
+    rewrite (IHf2 v5 v3 M0); auto.
   - simpl toREval in eval_v1.
     simpl toREval in eval_v2.
-    apply (IHf v1 v2 m1 m2); auto.
+    apply (IHf v1 v2 m1); auto.
 Qed.
 
 
@@ -308,8 +240,8 @@ Lemma meps_0_deterministic (f:exp R) (E:env):
   v1 = v2.
 Proof.
   intros v1 v2 ev1 ev2.
-  assert ((meps M0) == 0) by (simpl; lra).
-  apply (general_meps_0_deterministic f H H ev1 ev2). 
+  assert (M0 = M0) by auto.
+  apply (general_meps_0_deterministic f H ev1 ev2). 
 Qed.
 
 

coq/Infra/Abbrevs.v

@@ -59,3 +59,94 @@ 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

coq/Infra/MachineType.v

@@ -5,49 +5,80 @@ 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.
  **)
-Record mType : Type := mkmType {meps : Q; meps_geq_zero: 0 <= meps}.
-Arguments meps _ /.
+Inductive mType: Type := M0 | M32 | M64 | M128 | M256.
 
-Lemma M0_is_geq_zero: 0 <= 0.
-Proof. apply Qle_refl. Qed.
+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.
 
-Lemma M32_is_geq_zero: 0 <= (Qpower (2#1) (Zneg 24)).
-Proof. apply Qle_bool_iff; auto. Qed.
+Definition meps := inj_eps_Q.
 
-Lemma M64_is_geq_zero: 0 <= (Qpower (2#1) (Zneg 53)).
-Proof. apply Qle_bool_iff; auto. Qed.
-
-Lemma M128_is_geq_zero: 0 <= (Qpower (2#1) (Zneg 113)).
-Proof. apply Qle_bool_iff; auto. Qed.
-
-Lemma M256_is_geq_zero: 0 <= (Qpower (2#1) (Zneg 237)).
-Proof. apply Qle_bool_iff; auto. Qed.
+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.
+  
+(* Definition mTypeEqBool (m1:mType) (m2:mType) := *)
+(*   Qeq_bool (meps m1) (meps m2). *)
 
-Definition M0 := mkmType 0 (M0_is_geq_zero).
-Definition M32 := mkmType (Qpower (2#1) (Zneg 24)) (M32_is_geq_zero). 
-Definition M64 := mkmType (Qpower (2#1) (Zneg 53)) (M64_is_geq_zero).
-Definition M128 := mkmType (Qpower (2#1) (Zneg 113)) (M128_is_geq_zero).
-Definition M256 := mkmType (Qpower (2#1) (Zneg 237)) (M256_is_geq_zero).
+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) :=
-  Qeq_bool (meps m1) (meps m2).
-
-Definition mTypeEq: relation mType :=
-  fun m1 m2 => Qeq (meps m1) (meps m2).
+  match m1, m2 with
+  | M0, M0 => true
+  | M32, M32 => true
+  | M64, M64 => true
+  | M128, M128 => true
+  | M256, M256 => true
+  | _, _ => false
+  end.
+
+(* 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.     *)
 
-Instance mTypeEquivalence: Equivalence mTypeEq.
+Lemma EquivEqBoolEq (m1:mType) (m2:mType):
+  mTypeEqBool m1 m2 = true <-> m1 = m2.
 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.
+  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). *)
 
-Lemma mTypeEquivs (m1:mType) (m2:mType):
-  mTypeEqBool m1 m2 = true <-> mTypeEq m1 m2.
-Proof.
-  split; unfold mTypeEqBool; unfold mTypeEq; apply Qeq_bool_iff.
-Qed.
+
+(* 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 *)
@@ -57,7 +88,7 @@ Definition isMorePrecise (m1:mType) (m2:mType) :=
   else if (mTypeEqBool m1 M0) then
     mTypeEqBool m2 M0
   else
-    Qle_bool (meps m1) (meps m2). 
+    Qle_bool (meps m1) (meps m2).
 
 Lemma isMorePrecise_refl (m1:mType) :
   isMorePrecise m1 m1 = true.
@@ -66,8 +97,8 @@ Proof.
   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 isMorePrecise_rel (m1:mType) (m2:mType) := *)
+(*   Qle (meps m1) (meps m2). *)
 
 
 Definition isJoinOf (m:mType) (m1:mType) (m2:mType) :=
@@ -79,129 +110,106 @@ Definition isJoinOf (m:mType) (m1:mType) (m2:mType) :=
 
 
 Definition computeJoin (m1:mType) (m2:mType) :=
-  if (isMorePrecise m1 m2) then m1 else m2. 
+  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;