Merge wit Raphaels mixed precision implementation

.gitignore

@@ -33,15 +33,15 @@ hol4/*/*Theory*
 hol4/*/*.ui
 hol4/*/*.uo
 hol4/*/.*
-hol4/heap
 hol4/*/heap
+hol4/heap
 hol4/output/*.sml
 hol4/binary/cake_checker
 hol4/binary/checker.S
+hol4/output/certificate_*
 
 daisy
 rawdata/*
 .ensime*
-/daisy
 last.log
 output/*

coq/CertificateChecker.v

@@ -6,15 +6,17 @@
 **)
 Require Import Coq.Reals.Reals Coq.QArith.Qreals.
 Require Import Daisy.Infra.RealSimps Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps Daisy.Infra.Ltacs.
-Require Import Daisy.IntervalValidation Daisy.ErrorValidation Daisy.Environments.
+Require Import Daisy.IntervalValidation Daisy.ErrorValidation Daisy.Environments Daisy.Typing.
 
 Require Export Coq.QArith.QArith.
 Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Commands.
 
 (** Certificate checking function **)
-Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
-  if (validIntervalbounds e absenv P NatSet.empty)
-  then (validErrorbound e absenv NatSet.empty)
+Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) (defVars:nat -> option mType) :=
+  if (typeCheck e defVars (typeMap defVars e)) then
+    if (validIntervalbounds e absenv P NatSet.empty)
+    then (validErrorbound e (typeMap defVars e) absenv NatSet.empty)
+    else false
   else false.
 
 (**
@@ -22,24 +24,23 @@ Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
    Apart from assuming two executions, one in R and one on floats, we assume that
    the real valued execution respects the precondition.
 **)
-Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P:
-  forall (E1 E2:env) (vR:R) (vF:R) fVars,
-    approxEnv E1 absenv fVars NatSet.empty E2 ->
+Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P defVars:
+  forall (E1 E2:env) (vR:R) (vF:R) fVars m,
+    approxEnv E1 defVars absenv fVars NatSet.empty E2 ->
     (forall v, NatSet.mem v fVars = true ->
           exists vR, E1 v = Some vR /\
                 (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
-    NatSet.Subset (usedVars e) fVars ->
-    eval_exp 0%R E1 (toRExp e) vR ->
-    eval_exp (Q2R machineEpsilon) E2 (toRExp e) vF ->
-    CertificateChecker e absenv P = true ->
+    NatSet.Subset (Expressions.usedVars e) fVars ->
+    eval_exp E1 (toREvalVars defVars) (toREval (toRExp e)) vR M0 ->
+    eval_exp E2 defVars (toRExp e) vF m ->
+    CertificateChecker e absenv P defVars = true ->
     (Rabs (vR - vF) <= Q2R (snd (absenv e)))%R.
 (**
    The proofs is a simple composition of the soundness proofs for the range
    validator and the error bound validator.
 **)
 Proof.
-  intros E1 E2 vR vF fVars approxE1E2 P_valid fVars_subset eval_real eval_float
-         certificate_valid.
+  intros * approxE1E2 P_valid fVars_subset eval_real eval_float certificate_valid.
   unfold CertificateChecker in certificate_valid.
   rewrite <- andb_lazy_alt in certificate_valid.
   andb_to_prop certificate_valid.
@@ -57,58 +58,51 @@ Proof.
     inversion v_in_empty.
 Qed.
 
-Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) :=
-  if (validSSA f (freeVars f))
-  then
-    if (validIntervalboundsCmd f absenv P NatSet.empty)
-    then (validErrorboundCmd f absenv NatSet.empty)
-    else false
+Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) defVars:=
+  if (typeCheckCmd f defVars (typeMapCmd defVars f) && validSSA f (freeVars f))
+       then if (validIntervalboundsCmd f absenv P NatSet.empty)
+            then (validErrorboundCmd f (typeMapCmd defVars f) absenv NatSet.empty)
+            else false
   else false.
 
-Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P:
-  forall (E1 E2:env) vR vF ,
-    (* The execution environments are only off by the machine epsilon *)
-    approxEnv E1 absenv (freeVars f) NatSet.empty E2 ->
-    (* All free variables are respecting the precondition *)
+Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P defVars:
+  forall (E1 E2:env) vR vF m,
+    approxEnv E1 defVars absenv (freeVars f) NatSet.empty E2 ->
     (forall v, NatSet.mem v (freeVars f)= true ->
           exists vR, E1 v = Some vR /\
                 (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
-    (* Evaluations on the reals and on 1+delta floats *)
-    bstep (toRCmd f) E1 0 vR ->
-    bstep (toRCmd f) E2 (Q2R machineEpsilon) vF ->
-    (* Certificate checking succeeds *)
-    CertificateCheckerCmd f absenv P = true ->
-    (* Thereby we obtain a valid roundoff error *)
+    bstep (toREvalCmd (toRCmd f)) E1 (toREvalVars defVars) vR M0 ->
+    bstep (toRCmd f) E2 defVars vF m ->
+    CertificateCheckerCmd f absenv P defVars = true ->
     (Rabs (vR - vF) <= Q2R (snd (absenv (getRetExp f))))%R.
 (**
    The proofs is a simple composition of the soundness proofs for the range
    validator and the error bound validator.
 **)
 Proof.
-  intros E1 E2 vR vF approxE1E2 P_valid eval_real eval_float certificate_valid.
+  intros * approxE1E2 P_valid eval_real eval_float certificate_valid.
   unfold CertificateCheckerCmd in certificate_valid.
   repeat rewrite <- andb_lazy_alt in certificate_valid.
   andb_to_prop certificate_valid.
-  assert (exists outVars, ssa f (freeVars f) outVars) as ssa_f.
-  - apply validSSA_sound; auto.
-  - destruct ssa_f as [outVars ssa_f].
-    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.
-    + instantiate (1 := outVars).
-      eapply ssa_equal_set; try eauto.
-      hnf.
-      intros a; split; intros in_union.
-      * rewrite NatSet.union_spec in in_union.
-        destruct in_union as [in_fVars | in_empty]; try auto.
-        inversion in_empty.
-      * rewrite NatSet.union_spec; auto.
-    + hnf; intros a in_diff.
-      rewrite NatSet.diff_spec in in_diff.
-      destruct in_diff; auto.
-    + intros v v_in_empty.
-      rewrite NatSet.mem_spec in v_in_empty.
-      inversion v_in_empty.
-Qed.
+  apply validSSA_sound in R0.
+  destruct R0 as [outVars ssa_f].
+  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.
+  - instantiate (1 := outVars).
+    eapply ssa_equal_set; try eauto.
+    hnf.
+    intros a; split; intros in_union.
+    + rewrite NatSet.union_spec in in_union.
+      destruct in_union as [in_fVars | in_empty]; try auto.
+      inversion in_empty.
+    + rewrite NatSet.union_spec; auto.
+  - hnf; intros a in_diff.
+    rewrite NatSet.diff_spec in in_diff.
+    destruct in_diff; auto.
+  - intros v v_in_empty.
+    rewrite NatSet.mem_spec in v_in_empty.
+    inversion v_in_empty.
+Qed.y

coq/Commands.v

@@ -2,6 +2,7 @@
  Formalization of the Abstract Syntax Tree of a subset used in the Daisy framework
  **)
 Require Import Coq.Reals.Reals Coq.QArith.QArith.
+Require Import Daisy.Expressions.
 Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Infra.NatSet.
 
 (**
@@ -10,21 +11,55 @@ Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Infra.NatSet.
   Only assignments and return statement
 **)
 Inductive cmd (V:Type) :Type :=
-Let: nat -> exp V -> cmd V -> cmd V
+Let: mType -> nat -> exp V -> cmd V -> cmd V
 | Ret: exp V -> cmd V.
 
+Fixpoint getRetExp (V:Type) (f:cmd V) :=
+  match f with
+  |Let m x e g => getRetExp g
+  | Ret e => e
+  end.
+
+
+Fixpoint toRCmd (f:cmd Q) :=
+  match f with
+  |Let m x e g => Let m x (toRExp e) (toRCmd g)
+  |Ret e => Ret (toRExp e)
+  end.
+
+Fixpoint toREvalCmd (f:cmd R) :=
+  match f with
+  |Let m x e g => Let M0 x (toREval e) (toREvalCmd g)
+  |Ret e => Ret (toREval e)
+  end.
+
+(*
+UNUSED!
+   Small Step semantics for Daisy language
+Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
+  let_s x e s E v eps:
+    eval_exp eps E e v ->
+    sstep (Let x e s) E eps s (updEnv x v E)
+ |ret_s e E v eps:
+    eval_exp eps E e v ->
+    sstep (Ret e) E eps (Nop R) (updEnv 0 v E).
+ *)
+
 (**
   Define big step semantics for the Daisy language, terminating on a "returned"
   result value
  **)
-Inductive bstep : cmd R -> env -> R -> R -> Prop :=
-  let_b x e s E v eps res:
-    eval_exp eps E e v ->
-    bstep s (updEnv x v E) eps res ->
-    bstep (Let x e s) E eps res
- |ret_b e E v eps:
-    eval_exp eps E e v ->
-    bstep (Ret e) E eps v.
+Inductive bstep : cmd R -> env -> (nat -> option mType) -> R -> mType -> Prop :=
+  let_b m m' x e s E v res defVars:
+    eval_exp E defVars  e v m ->
+    defVars x = Some m ->
+    bstep s (updEnv x v E) defVars res m' ->
+    bstep (Let m x e s) E defVars res m'
+ |ret_b m e E v defVars:
+    eval_exp E defVars e v m ->
+    bstep (Ret e) E defVars v m.
+
+
 
 (**
   The free variables of a command are all used variables of expressions
@@ -32,8 +67,8 @@ Inductive bstep : cmd R -> env -> R -> R -> Prop :=
 **)
 Fixpoint freeVars V (f:cmd V) :NatSet.t :=
   match f with
-  | Let x e g => NatSet.remove x (NatSet.union (usedVars e) (freeVars g))
-  | Ret e => usedVars e
+  | Let _ x e1 g => NatSet.remove x (NatSet.union (Expressions.usedVars e1) (freeVars g))
+  | Ret e => Expressions.usedVars e
   end.
 
 (**
@@ -41,7 +76,7 @@ Fixpoint freeVars V (f:cmd V) :NatSet.t :=
 **)
 Fixpoint definedVars V (f:cmd V) :NatSet.t :=
   match f with
-  | Let x _ g => NatSet.add x (definedVars g)
+  | Let _ x _ g => NatSet.add x (definedVars g)
   | Ret _ => NatSet.empty
   end.
 
@@ -51,13 +86,6 @@ Fixpoint definedVars V (f:cmd V) :NatSet.t :=
  **)
 Fixpoint liveVars V (f:cmd V) :NatSet.t :=
   match f with
-  | Let _ e g => NatSet.union (usedVars e) (liveVars g)
+  | Let _ _ e g => NatSet.union (usedVars e) (liveVars g)
   | Ret e => usedVars e
   end.
-
-Fixpoint cmdEq f1 f2 :=
-  match f1, f2 with
-  |Let x e g, Let y e' g' => expEqBool e e' && (x =? y) && cmdEq g g'
-  |Ret e, Ret e' => expEqBool e e'
-  |_, _ => false
-  end.
\ No newline at end of file

coq/Environments.v

@@ -12,24 +12,25 @@ It is necessary to have this relation, since two evaluations of the very same
 expression may yield different values for different machine epsilons
 (or environments that already only approximate each other)
  **)
-Inductive approxEnv : env -> analysisResult -> NatSet.t -> NatSet.t -> env -> Prop :=
-|approxRefl A:
-   approxEnv emptyEnv A NatSet.empty NatSet.empty emptyEnv
-|approxUpdFree E1 E2 A v1 v2 x fVars dVars:
-   approxEnv E1 A fVars dVars E2 ->
-   (Rabs (v1 - v2) <= Rabs v1 * Q2R machineEpsilon)%R ->
+Inductive approxEnv : env -> (nat -> option mType) -> analysisResult -> NatSet.t -> NatSet.t -> env -> Prop :=
+|approxRefl defVars A:
+   approxEnv emptyEnv defVars A NatSet.empty NatSet.empty emptyEnv
+|approxUpdFree E1 E2 defVars A v1 v2 x fVars dVars m:
+   approxEnv E1 defVars A fVars dVars E2 ->
+   defVars x = Some m ->
+   (Rabs (v1 - v2) <= (Rabs v1) * Q2R (meps m))%R ->
    NatSet.mem x (NatSet.union fVars dVars) = false ->
-   approxEnv (updEnv x v1 E1) A (NatSet.add x fVars) dVars (updEnv x v2 E2)
-|approxUpdBound E1 E2 A v1 v2 x fVars dVars:
-   approxEnv E1 A fVars dVars E2 ->
+   approxEnv (updEnv x v1 E1) defVars A (NatSet.add x fVars) dVars (updEnv x v2 E2)
+|approxUpdBound E1 E2 defVars A v1 v2 x fVars dVars:
+   approxEnv E1 defVars A fVars dVars E2 ->
    (Rabs (v1 - v2) <= Q2R (snd (A (Var Q x))))%R ->
    NatSet.mem x (NatSet.union fVars dVars) = false ->
-   approxEnv (updEnv x v1 E1) A fVars (NatSet.add x dVars) (updEnv x v2 E2).
+   approxEnv (updEnv x v1 E1) defVars A fVars (NatSet.add x dVars) (updEnv x v2 E2).
 
-Inductive approxParams :env -> R -> env -> Prop :=
-|approxParamRefl eps:
-   approxParams emptyEnv eps emptyEnv
-|approxParamUpd E1 E2 eps x v1 v2 :
-   approxParams E1 eps E2 ->
-   (Rabs (v1 - v2) <= eps)%R ->
-   approxParams (updEnv x v1 E1) eps (updEnv x v2 E2).
+(* Inductive approxParams :env -> env -> Prop := *)
+(* |approxParamRefl: *)
+(*    approxParams emptyEnv emptyEnv *)
+(* |approxParamUpd E1 E2 m x v1 v2 : *)
+(*    approxParams E1 E2 -> *)
+(*    (Rabs (v1 - v2) <= Q2R (meps m))%R -> *)
+(*    approxParams (updEnv x M0 v1 E1) (updEnv x m v2 E2). *)

coq/Infra/Abbrevs.v

@@ -2,6 +2,7 @@
   This file contains some type abbreviations, to ease writing.
  **)
 Require Import Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qreals.
+Require Import Daisy.Infra.MachineType.
 
 Global Set Implicit Arguments.
 (**
@@ -36,8 +37,8 @@ Arguments ivlo _ /.
 Arguments ivhi _ /.
 
 (**
-Later we will argue about program preconditions.
-Define a precondition to be a function mapping numbers (resp. variables) to intervals.
+  Later we will argue about program preconditions.
+  Define a precondition to be a function mapping numbers (resp. variables) to intervals.
 **)
 Definition precond :Type := nat -> intv.
 
@@ -54,8 +55,10 @@ Definition emptyEnv:env := fun _ => None.
 (**
   Define environment update function as abbreviation, for variable environments
 **)
-
 Definition updEnv (x:nat) (v: R) (E:env) (y:nat) :=
-  if y =? x
+  if (y =? x)
   then Some v
   else E y.
+
+Definition updDefVars (x:nat) (m:mType) (defVars:nat -> option mType) (y:nat) :=
+  if (y =? x) then Some m else defVars y.

coq/Infra/Ltacs.v

@@ -2,7 +2,6 @@
 Require Import Coq.Bool.Bool Coq.Reals.Reals.
 Require Import Daisy.Infra.RealSimps Daisy.Infra.NatSet.
 
-
 Ltac iv_assert iv name:=
   assert (exists ivlo ivhi, iv = (ivlo, ivhi)) as name by (destruct iv; repeat eexists; auto).
 

coq/Infra/MachineType.v

+Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals.
+Require Import Coq.Reals.Reals Coq.micromega.Psatz.
+
+(**
+   Define machine types, and some tool functions. Needed for the
+   mixed-precision part, to be able to define a rounding operator.
+ **)
+Inductive mType: Type := M0 | M32 | M64 | M128 | M256.
+
+Definition meps (e:mType) : Q :=
+  match e with
+  | M0 => 0
+  | M32 => (Qpower (2#1) (Zneg 24))
+  | M64 => (Qpower (2#1) (Zneg 53))
+  (* the epsilons below match what is used internally in daisy,
+  although these value do not match the IEEE standard *)
+  | M128 => (Qpower (2#1) (Zneg 105))
+  | M256 => (Qpower (2#1) (Zneg 211))
+  end.
+
+Lemma meps_pos :
+  forall e, 0 <= meps e.
+Proof.
+  intro e.
+  case_eq e; intro; simpl meps; apply Qle_bool_iff; auto.
+Qed.
+
+Lemma meps_posR :
+  forall e, (0 <= Q2R (meps e))%R.
+Proof.
+  intro.
+  assert (Q2R 0 = 0%R) by (unfold Q2R; simpl; lra).
+  rewrite <- H.
+  apply Qle_Rle.
+  apply meps_pos.
+Qed.
+
+(* Definition mTypeEqBool (m1:mType) (m2:mType) := *)
+(*   Qeq_bool (meps m1) (meps m2). *)
+
+(* TODO: unused? *)
+(* Theorem eq_mType_dec: forall (m1 m2:mType), {m1 = m2} + {m1 <> m2}. *)
+(* Proof. *)
+(*   intros. *)
+(*   case_eq m1; intros; case_eq m2; intros; auto; right; intro; inversion H1. *)
+(* Qed. *)
+
+Definition mTypeEqBool (m1:mType) (m2:mType) :=
+  match m1, m2 with
+  | M0, M0 => true
+  | M32, M32 => true
+  | M64, M64 => true
+  | M128, M128 => true
+  | M256, M256 => true
+  | _, _ => false
+  end.
+
+Lemma mTypeEqBool_sym (m1:mType) (m2:mType):
+  forall b, mTypeEqBool m1 m2 = b -> mTypeEqBool m2 m1 = b.
+Proof.
+  intros.
+  destruct b, m1, m2; simpl; cbv; auto.
+Qed.
+
+Lemma mTypeEqBool_refl (m:mType):
+  mTypeEqBool m m = true.
+Proof.
+  intros. destruct m; cbv; auto.
+Qed.
+
+
+(* Definition mTypeEqComp (m1:mType) (m2:mType) := *)
+(*   Qeq_bool (meps m1) (meps m2). *)
+
+(* Lemma EquivBoolComp (m1:mType) (m2:mType): *)
+(*   mTypeEqBool m1 m2 = true <-> mTypeEqComp m1 m2 = true. *)
+(* Proof. *)
+(*   split; intros. *)
+(*   - case_eq m1; intros; case_eq m2; intros; auto; try rewrite H0 in H; rewrite H1 in H; cbv; auto. *)
+(*   - case_eq m1; intros; case_eq m2; intros; auto; try rewrite H0 in H; rewrite H1 in H; unfold mTypeEqComp in H; cbv in H; inversion H. *)
+(* Qed.     *)
+
+Lemma EquivEqBoolEq (m1:mType) (m2:mType):
+  mTypeEqBool m1 m2 = true <-> m1 = m2.
+Proof.
+  split; intros; case_eq m1; intros; case_eq m2; intros; auto; rewrite H0 in H; rewrite H1 in H; cbv in H; inversion H; auto.
+Qed.
+
+
+(*   Definition mTypeEq: relation mType := *)
+(*   fun m1 m2 => Qeq (meps m1) (meps m2). *)
+
+
+(* Instance mTypeEquivalence: Equivalence mTypeEq. *)
+(* Proof. *)
+(*   split; intros. *)
+(*   - intro. apply Qeq_refl. *)
+(*   - intros a b eq. apply Qeq_sym. auto. *)
+(*   - intros a b c eq1 eq2. eapply Qeq_trans; eauto. *)
+(* Qed. *)
+
+
+(* Lemma mTypeEquivs (m1:mType) (m2:mType): *)
+(*   mTypeEqBool m1 m2 = true <-> mTypeEq m1 m2. *)
+(* Proof. *)
+(*   split; unfold mTypeEqBool; unfold mTypeEq; apply Qeq_bool_iff. *)
+(* Qed. *)
+
+Definition isMorePrecise (m1:mType) (m2:mType) :=
+  (* check if m1 is more precise than m2, i.e. if the epsilon of m1 is *)
+  (*   smaller than the epsilon of m2 *)
+  if (mTypeEqBool m2 M0) then
+    true
+  else if (mTypeEqBool m1 M0) then
+    mTypeEqBool m2 M0
+  else
+    Qle_bool (meps m1) (meps m2).
+
+(**
+  Check if m1 is a more precise floating point type, meaning that the corresponding machine epsilon is less.
+  Special Case m0, which must be the bottom element.
+**)
+Definition isMorePrecise' (m1:mType) (m2:mType) :=
+  match m2, m1 with
+  |M0, _ => true
+  |M32, M0 => false
+  |M32, _ => true
+  |M64, M0 | M64, M32 => false
+  |M64, _ => true
+  |M128, M128 => true
+  |M128, M256 => true
+  |M256, M256 => true
+  |_, _ => false
+  end.
+
+(* Lemma ismoreprec_rw m1 m2: *)
+(*   forall b, isMorePrecise m1 m2  = b <-> isMorePrecise' m1 m2 = b. *)
+(* Admitted. *)
+
+Lemma isMorePrecise_refl (m1:mType) :
+  isMorePrecise m1 m1 = true.
+Proof.
+  unfold isMorePrecise; simpl.
+  case_eq (mTypeEqBool m1 M0); intro hyp; [ auto |  apply Qle_bool_iff; apply Qle_refl ].
+Qed.
+
+(* Definition isMorePrecise_rel (m1:mType) (m2:mType) := *)
+(*   Qle (meps m1) (meps m2). *)
+
+
+Definition computeJoin (m1:mType) (m2:mType) :=
+  if (isMorePrecise m1 m2) then m1 else m2.
+
+
+(* Everything below is unused? *)
+Definition isJoinOf (m:mType) (m1:mType) (m2:mType) :=
+  (* is m the join of m1 and m2 ?*)
+  if (isMorePrecise m1 m2) then
+    mTypeEqBool m m1
+  else
+    mTypeEqBool m m2.
+
+Lemma ifisMorePreciseM0 (m:mType) :
+  isMorePrecise M0 m = true -> m = M0.
+Proof.
+  intro.
+  unfold isMorePrecise in H.
+  case_eq (mTypeEqBool m M0); intros; rewrite H0 in H; auto.
+  - apply EquivEqBoolEq in H0; auto.
+  - assert (mTypeEqBool M0 M0 = true) by (apply EquivEqBoolEq; auto).
+    rewrite H1 in H.
+    inversion H.
+Qed.
+
+Lemma ifM0isJoin_l (m:mType) (m1:mType) (m2:mType) :
+  m = M0 -> isJoinOf m m1 m2 = true -> m1 = M0.
+Proof.
+  intros H0 H.
+  unfold isJoinOf in H.
+  case_eq (isMorePrecise m1 m2); intro Hyp; rewrite Hyp in H; simpl in H; rewrite H0 in H; subst.
+  - case_eq m1; intros; auto; unfold isMorePrecise in Hyp; rewrite H0 in H; compute in H; inversion H.
+  - unfold isMorePrecise in Hyp.
+    apply EquivEqBoolEq in H; symmetry in H; apply EquivEqBoolEq in H.
+    rewrite H in Hyp; inversion Hyp.
+Qed.
+
+
+Lemma ifM0isJoin_r (m:mType) (m1:mType) (m2:mType) :
+  m = M0 -> isJoinOf m m1 m2 = true -> m2 = M0.
+Proof.
+  intros H0 H.
+  unfold isJoinOf in H.
+  case_eq (isMorePrecise m1 m2); intro Hyp; rewrite Hyp in H; simpl in H; rewrite H0 in H; subst.
+  - apply EquivEqBoolEq in H. rewrite <- H in Hyp; subst.
+    unfold isMorePrecise in Hyp.
+    case_eq (mTypeEqBool m2 M0); intros; auto; rewrite H in Hyp.
+    apply EquivEqBoolEq in H; auto.
+    case_eq (mTypeEqBool M0 M0); intros; auto; rewrite H0 in Hyp.
+    inversion Hyp.
+    unfold mTypeEqBool in H0; inversion H0.
+  - apply EquivEqBoolEq in H; auto.
+Qed.
+
+Lemma ifM0isJoin (m1:mType) (m2:mType):
+  isJoinOf M0 m1 m2 = true -> m1 = M0 /\ m2 = M0.
+Proof.
+  assert (M0 = M0) by auto.
+  intros; split.
+  - apply (ifM0isJoin_l M0 m1 m2); auto.
+  - apply (ifM0isJoin_r M0 m1 m2); auto.
+Qed.
+
+Lemma computeJoinIsJoin (m1:mType) (m2:mType) :
+  isJoinOf (computeJoin m1 m2) m1 m2 = true.
+Proof.
+  remember (computeJoin m1 m2) as m.
+  unfold isJoinOf.
+  unfold computeJoin in Heqm.
+  case_eq (isMorePrecise m1 m2); intros; auto;
+  rewrite H in Heqm;
+  rewrite Heqm;
+  apply EquivEqBoolEq; auto.
+Qed.
+
+Lemma isJoinComputeJoin (M:mType) (m1:mType) (m2:mType) :
+  isJoinOf M m1 m2 = true ->
+  M = computeJoin m1 m2.
+Proof.
+  intros.
+  unfold computeJoin.