Proofs done until validErrorbound_sound included

43ce2820 · Raphaël Monat · bd0ba831 · 43ce2820 · 43ce2820 · 43ce2820
Commit 43ce2820 authored Mar 10, 2017 by Raphaël Monat
7 changed files
--- a/coq/ErrorBounds.v
+++ b/coq/ErrorBounds.v
@@ -58,29 +58,28 @@ Lemma add_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
 Proof.
  intros e1_real e1_float e2_real e2_float plus_real plus_float bound_e1 bound_e2.
  (* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
-  inversion plus_real; subst;
-    assert (m3 = M0) by (apply (ifM0isJoin_l M0 m3 m4); auto);
-    assert (m4 = M0) by (apply (ifM0isJoin_r M0 m3 m4); auto); subst;
-      simpl (meps M0) in H3; rewrite Q2R0_is_0 in H3; auto.
+  inversion plus_real; subst.
+  destruct m0; destruct m3; inversion H2;
+      simpl in H4; rewrite Q2R0_is_0 in H4; auto.
  rewrite delta_0_deterministic in plus_real; auto.
  rewrite (delta_0_deterministic (evalBinop Plus v1 v2) delta); auto.
  unfold evalBinop in *; simpl in *.
-  clear delta H3.
-  rewrite (meps_0_deterministic (toRExp e1) H6 e1_real);
-    rewrite (meps_0_deterministic (toRExp e2) H7 e2_real).
-  rewrite (meps_0_deterministic (toRExp e1) H6 e1_real) in plus_real.
-  rewrite (meps_0_deterministic (toRExp e2) H7 e2_real) in plus_real.
-  clear H6 H7 v1 v2.
+  clear delta H4.
+  rewrite (meps_0_deterministic (toRExp e1) H5 e1_real);
+    rewrite (meps_0_deterministic (toRExp e2) H6 e2_real).
+  rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in plus_real.
+  rewrite (meps_0_deterministic (toRExp e2) H6 e2_real) in plus_real.
+  clear H5 H6 v1 v2.
  (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
  inversion plus_float; subst.
  unfold perturb; simpl.
-  inversion H7; subst; inversion H8; subst.
+  inversion H6; subst; inversion H7; subst.
  unfold updEnv; simpl.
-  unfold updEnv in H6,H9; simpl in *.
-  symmetry in H6,H9.
-  inversion H6; inversion H9; subst.
+  unfold updEnv in H5,H8; simpl in *.
+  symmetry in H5,H8.
+  inversion H5; inversion H8; subst.
  (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
-  clear plus_float H7 H8 plus_real e1_real e1_float e2_real e2_float H9 H6.
+  clear plus_float H7 H8 plus_real e1_real e1_float e2_real e2_float H5 H8.
  repeat rewrite Rmult_plus_distr_l.
  rewrite Rmult_1_r.
  rewrite Rsub_eq_Ropp_Rplus.
@@ -103,7 +102,7 @@ Proof.
    eapply Rle_trans.
    eapply Rmult_le_compat_l.
    apply Rabs_pos.
-    apply H4.
+    apply H3.
    apply Req_le; auto.
 Qed.

@@ -125,28 +124,27 @@ Proof.
  intros e1_real e1_float e2_real e2_float sub_real sub_float bound_e1 bound_e2.
  (* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
  inversion sub_real; subst;
-    assert (m3 = M0) by (apply (ifM0isJoin_l M0 m3 m4); auto);
-    assert (m4 = M0) by (apply (ifM0isJoin_r M0 m3 m4); auto); subst;
-      simpl (meps M0) in H3; rewrite Q2R0_is_0 in H3; auto.
+  destruct m0; destruct m3; inversion H2;
+      simpl in H4; rewrite Q2R0_is_0 in H4; auto.
  rewrite delta_0_deterministic in sub_real; auto.
  rewrite delta_0_deterministic; auto.
  unfold evalBinop in *; simpl in *.
-  clear delta H3.
-  rewrite (meps_0_deterministic (toRExp e1) H6 e1_real);
-    rewrite (meps_0_deterministic (toRExp e2) H7 e2_real).
-  rewrite (meps_0_deterministic (toRExp e1) H6 e1_real) in sub_real.
-  rewrite (meps_0_deterministic (toRExp e2) H7 e2_real) in sub_real.
-  clear H6 H7 v1 v2.
+  clear delta H4.
+  rewrite (meps_0_deterministic (toRExp e1) H5 e1_real);
+    rewrite (meps_0_deterministic (toRExp e2) H6 e2_real).
+  rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in sub_real.
+  rewrite (meps_0_deterministic (toRExp e2) H6 e2_real) in sub_real.
+  clear H5 H6 v1 v2.
  (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
  inversion sub_float; subst.
  unfold perturb; simpl.
-  inversion H7; subst; inversion H8; subst.
+  inversion H6; subst; inversion H7; subst.
  unfold updEnv; simpl.
-  symmetry in H6, H9.
-  unfold updEnv in H6, H9; simpl in H6, H9.
-  inversion H6; inversion H9; subst.
+  symmetry in H5, H8.
+  unfold updEnv in H5, H8; simpl in H5, H8.
+  inversion H5; inversion H8; subst.
  (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
-  clear sub_float H7 H8 sub_real e1_real e1_float e2_real e2_float H6 H9.
+  clear sub_float H7 H8 sub_real e1_real e1_float e2_real e2_float H5 H8.
  repeat rewrite Rmult_plus_distr_l.
  rewrite Rmult_1_r.
  repeat rewrite Rsub_eq_Ropp_Rplus.
@@ -182,27 +180,26 @@ Proof.
  intros e1_real e1_float e2_real e2_float mult_real mult_float.
  (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
  inversion mult_real; subst;
-    assert (m3 = M0) by (apply (ifM0isJoin_l M0 m3 m4); auto);
-    assert (m4 = M0) by (apply (ifM0isJoin_r M0 m3 m4); auto); subst;
-      simpl (meps M0) in H3; rewrite Q2R0_is_0 in H3; auto.
+    destruct m0; destruct m3; inversion H2;
+      simpl in H4; rewrite Q2R0_is_0 in H4; auto.
  rewrite delta_0_deterministic in mult_real; auto.
  rewrite delta_0_deterministic; auto.
  unfold evalBinop in *; simpl in *.
-  clear delta H3.
-  rewrite (meps_0_deterministic (toRExp e1) H6 e1_real);
-    rewrite (meps_0_deterministic (toRExp e2) H7 e2_real).
-  rewrite (meps_0_deterministic (toRExp e1) H6 e1_real) in mult_real.
-  rewrite (meps_0_deterministic (toRExp e2) H7 e2_real) in mult_real.
-  clear H6 H7 v1 v2.
+  clear delta H4.
+  rewrite (meps_0_deterministic (toRExp e1) H5 e1_real);
+    rewrite (meps_0_deterministic (toRExp e2) H6 e2_real).
+  rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in mult_real.
+  rewrite (meps_0_deterministic (toRExp e2) H6 e2_real) in mult_real.
+  clear H5 H6 v1 v2.
  (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
  inversion mult_float; subst.
  unfold perturb; simpl.
-  inversion H7; subst; inversion H8; subst.
-  symmetry in H6, H9;
+  inversion H6; subst; inversion H7; subst.
+  symmetry in H5, H8;
    unfold updEnv in *; simpl in *.
-  inversion H6; inversion H9; subst.
+  inversion H5; inversion H8; subst.
  (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
-  clear mult_float H7 H8 mult_real e1_real e1_float e2_real e2_float H6 H9.
+  clear mult_float H7 H8 mult_real e1_real e1_float e2_real e2_float H5 H8.
  repeat rewrite Rmult_plus_distr_l.
  rewrite Rmult_1_r.
  rewrite Rsub_eq_Ropp_Rplus.
@@ -232,27 +229,26 @@ Proof.
  intros e1_real e1_float e2_real e2_float div_real div_float.
  (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
  inversion div_real; subst;
-    assert (m3 = M0) by (apply (ifM0isJoin_l M0 m3 m4); auto);
-    assert (m4 = M0) by (apply (ifM0isJoin_r M0 m3 m4); auto); subst;
-      simpl (meps M0) in H3; rewrite Q2R0_is_0 in H3; auto.
+  destruct m0; destruct m3; inversion H2;
+    simpl in H4; rewrite Q2R0_is_0 in H4; auto.
  rewrite delta_0_deterministic in div_real; auto.
  rewrite delta_0_deterministic; auto.
  unfold evalBinop in *; simpl in *.
-  clear delta H3.
-  rewrite (meps_0_deterministic (toRExp e1) H6 e1_real);
-    rewrite (meps_0_deterministic (toRExp e2) H7 e2_real).
-  rewrite (meps_0_deterministic (toRExp e1) H6 e1_real) in div_real.
-  rewrite (meps_0_deterministic (toRExp e2) H7 e2_real) in div_real.
-  clear H6 H7 v1 v2.
+  clear delta H4.
+  rewrite (meps_0_deterministic (toRExp e1) H5 e1_real);
+    rewrite (meps_0_deterministic (toRExp e2) H6 e2_real).
+  rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in div_real.
+  rewrite (meps_0_deterministic (toRExp e2) H6 e2_real) in div_real.
+  clear H5 H6 v1 v2.
  (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
  inversion div_float; subst.
  unfold perturb; simpl.
-  inversion H7; subst; inversion H8; subst.
-  symmetry in H6, H9;
+  inversion H6; subst; inversion H7; subst.
+  symmetry in H5, H8;
    unfold updEnv in *; simpl in *.
-  inversion H6; inversion H9; subst.
+  inversion H5; inversion H8; subst.
  (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
-  clear div_float H7 H8 div_real e1_real e1_float e2_real e2_float H6 H9.
+  clear div_float H7 H8 div_real e1_real e1_float e2_real e2_float H5 H8.
  repeat rewrite Rmult_plus_distr_l.
  rewrite Rmult_1_r.
  rewrite Rsub_eq_Ropp_Rplus.
@@ -447,10 +443,10 @@ Proof.
  rewrite Q2R0_is_0; auto.
 Qed.

-Lemma round_abs_err_bounded (e:exp R) (nR nF1 nF:R) (E: env) (err:R) (machineEpsilon m:mType):
-  eval_exp E (toREval e) nR M0 ->
-  eval_exp E e nF1 m ->
-  eval_exp (updEnv 1 m nF1 E) (toRExp (Downcast machineEpsilon (Var Q m 1))) nF machineEpsilon->
+Lemma round_abs_err_bounded (e:exp R) (nR nF1 nF:R) (E1 E2: env) (err:R) (machineEpsilon m:mType):
+  eval_exp E1 (toREval e) nR M0 ->
+  eval_exp E2 e nF1 m ->
+  eval_exp (updEnv 1 m nF1 emptyEnv) (toRExp (Downcast machineEpsilon (Var Q m 1))) nF machineEpsilon->
  (Rabs (nR - nF1) <= err)%R ->
  (Rabs (nR - nF) <= err + (Rabs nF1) * Q2R (meps machineEpsilon))%R.
 Proof.

--- a/coq/ErrorValidation.v
+++ b/coq/ErrorValidation.v
--- a/coq/Expressions.v
+++ b/coq/Expressions.v
@@ -235,12 +235,12 @@ Inductive eval_exp (E:env) :(exp R) -> R -> mType -> Prop :=
    Rle (Rabs delta) (Q2R (meps m)) ->
    eval_exp E f1 v1 m ->
    eval_exp E (Unop Inv f1) (perturb (evalUnop Inv v1) delta) m
-| Binop_dist m m1 m2 op f1 f2 v1 v2 delta:
-    isJoinOf m m1 m2 = true ->
-    Rle (Rabs delta) (Q2R (meps 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 ->
-    eval_exp E (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta) m
+    eval_exp E (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta)  (computeJoin m1 m2)
 | Downcast_dist m m1 f1 v1 delta:
    (* Downcast expression f1 (evaluating to machine type m1), to a machine type m, less precise than m1.*)
    isMorePrecise m1 m = true ->
@@ -296,18 +296,27 @@ Proof.
  - 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.
    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.
+    destruct m0; destruct m2; inversion H4.
+    destruct m3; destruct m4; inversion H10.
+    simpl in *.
    rewrite (IHf1 v0 v4 M0); auto.
    rewrite (IHf2 v5 v3 M0); auto.
+    rewrite Q2R0_is_0 in H2,H12.
+    rewrite delta_0_deterministic; auto.
+    rewrite delta_0_deterministic; auto.
  - simpl toREval in eval_v1.
    simpl toREval in eval_v2.
    apply (IHf v1 v2 m1); auto.
 Qed.

+(* Lemma rnd_0_deterministic f E m v: *)
+(*   eval_exp E (toREval (Downcast m f)) v M0 <-> *)
+(*   eval_exp E (toREval f) v M0. *)
+(* Proof. *)
+(*   split; intros. *)
+(*   - simpl in H. auto. *)
+(*   - simpl; auto. *)
+(* Qed. *)

  
 (**
@@ -334,10 +343,11 @@ variables in the Environment.
 Lemma binary_unfolding b f1 f2 m E vF:
  eval_exp E (Binop b f1 f2) vF m ->
  exists vF1 vF2 m1 m2,
-  eval_exp E f1 vF1 m1 /\
-  eval_exp E f2 vF2 m2 /\
-  eval_exp  (updEnv 2 m2 vF2 (updEnv 1 m1 vF1 emptyEnv))
-           (Binop b (Var R m1 1) (Var R m2 2)) vF m.
+    m = computeJoin m1 m2 /\
+    eval_exp E f1 vF1 m1 /\
+    eval_exp E f2 vF2 m2 /\
+    eval_exp  (updEnv 2 m2 vF2 (updEnv 1 m1 vF1 emptyEnv))
+              (Binop b (Var R m1 1) (Var R m2 2)) vF m.
 Proof.
  intros eval_float.
  inversion eval_float; subst.

--- a/coq/Infra/MachineType.v
+++ b/coq/Infra/MachineType.v
@@ -272,6 +272,15 @@ Proof.
  - 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.

--- a/coq/IntervalValidation.v
+++ b/coq/IntervalValidation.v
@@ -476,7 +476,7 @@ Proof.
      rewrite NatSet.diff_spec in in_diff_e1.
      destruct in_diff_e1 as [ in_usedVars not_dVar].
      split; try auto.
-      assert (m1 = M0) by (apply (ifM0isJoin_l M0 m1 m2); auto); subst; auto.
+      destruct m1; destruct m2; inversion H2; subst; auto.
    + assert (Q2R (fst (fst (iv2, err2))) <= v2 <= Q2R (snd (fst (iv2, err2))))%R as valid_bounds_e2.
      * apply IHf2; try auto.
        intros v in_diff_e2.
@@ -484,7 +484,7 @@ Proof.
        simpl. rewrite NatSet.diff_spec, NatSet.union_spec.
        rewrite NatSet.diff_spec in in_diff_e2.
        destruct in_diff_e2; split; auto.
-        assert (m2 = M0) by (apply (ifM0isJoin_r M0 m1 m2); auto); subst; auto.
+        destruct m1; destruct m2; inversion H2; auto.
      * destruct b; simpl in *.
        { pose proof (interval_addition_valid (iv1 :=(Q2R (fst iv1),Q2R (snd iv1))) (iv2 :=(Q2R (fst iv2), Q2R (snd iv2)))) as valid_add.
          unfold validIntervalAdd in valid_add.
@@ -614,8 +614,10 @@ Proof.
                    rewrite <- Q2R_inv in valid_div_hi; [ | auto].
                    repeat rewrite <- Q2R_mult in valid_div_hi.
                    rewrite <- Q2R_max4 in valid_div_hi; auto. } }
-    + simpl in H3; rewrite Q2R0_is_0 in H3; auto.
-    + simpl in H3; rewrite Q2R0_is_0 in H3; auto.
+    + destruct m1; destruct m2; inversion H2.
+      simpl in H4; rewrite Q2R0_is_0 in H4; auto.
+    + destruct m1; destruct m2; inversion H2.
+      simpl in H4; rewrite Q2R0_is_0 in H4; auto.
  - unfold validIntervalbounds in valid_bounds.
    (*simpl erasure in valid_bounds.*)
    simpl in *; destruct (absenv (Downcast m f)); destruct (absenv f); simpl in *.

--- a/coq/Typing.v
+++ b/coq/Typing.v
@@ -95,10 +95,9 @@ Proof.
    rewrite expEqBool_refl; simpl.
    rewrite andb_true_r.
    rewrite binopEqBool_refl; simpl.
-    pose proof (IHe1 E v1 m1 H7).
-    pose proof (IHe2 E v2 m2 H8).
+    pose proof (IHe1 E v1 m1 H6).
+    pose proof (IHe2 E v2 m2 H7).
    rewrite H0, H1.
-    assert (m = computeJoin m1 m2) by (apply isJoinComputeJoin; auto); subst.
    auto.
  - rewrite expEqBool_refl.
    assert (mTypeEqBool m0 m0 = true) by (apply EquivEqBoolEq; auto).
@@ -107,6 +106,59 @@ Proof.
    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
@@ -116,7 +168,7 @@ Fixpoint isSubExpression (e':exp Q) (e:exp Q) :=
  |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.
@@ -149,6 +201,67 @@ Proof.
    + 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 ->
@@ -193,31 +306,247 @@ Proof.
 Qed.


-Lemma typingVarDet (e:exp Q) m m0 v:
-  typeExpression e (Var Q m v) = Some m0 ->
-  m = m0.
+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.
-  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.
+  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.
-Qed.    
+  - 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.