fixing final proof for expressions

coq/Expressions.v

@@ -1074,9 +1074,67 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
           - apply nat_compare_lt in c1. apply nat_compare_lt in c2.
             assert (c3: (n ?= n1)%nat = Lt) by (apply nat_compare_lt; omega).
             now rewrite c3. }
-        { admit. }
-        { admit. }
-        { admit. }
+        { destruct (n ?= n0)%nat eqn:c1; destruct (n0 ?= n1)%nat eqn:c2; try congruence.
+          - apply Nat.compare_eq in c1. apply Nat.compare_eq in c2. subst.
+            rewrite Nat.compare_refl.
+            apply mTypeEq_compat_eq in Heqb. subst.
+            rewrite Heqb0. auto.
+          - apply Nat.compare_eq in c1. subst.
+            rewrite c2. now destruct (mTypeEq m m1).
+          - apply Nat.compare_eq in c2. subst.
+            rewrite c1. now destruct (mTypeEq m m1).
+          - apply nat_compare_lt in c1. apply nat_compare_lt in c2.
+            assert (c3: (n ?= n1)%nat = Lt) by (apply nat_compare_lt; omega).
+            rewrite c3. now destruct (mTypeEq m m1). }
+        { destruct (n ?= n0)%nat eqn:c1; destruct (n0 ?= n1)%nat eqn:c2; try congruence.
+          - apply Nat.compare_eq in c1. apply Nat.compare_eq in c2. subst.
+            rewrite Nat.compare_refl.
+            apply mTypeEq_compat_eq in Heqb0. subst.
+            rewrite Heqb. auto.
+          - apply Nat.compare_eq in c1. subst.
+            rewrite c2. now destruct (mTypeEq m m1).
+          - apply Nat.compare_eq in c2. subst.
+            rewrite c1. now destruct (mTypeEq m m1).
+          - apply nat_compare_lt in c1. apply nat_compare_lt in c2.
+            assert (c3: (n ?= n1)%nat = Lt) by (apply nat_compare_lt; omega).
+            rewrite c3. now destruct (mTypeEq m m1). }
+        { destruct (n ?= n0)%nat eqn:c1; destruct (n0 ?= n1)%nat eqn:c2; try congruence.
+          - apply Nat.compare_eq in c1. apply Nat.compare_eq in c2. subst.
+            rewrite Nat.compare_refl.
+            destruct (mTypeEq m m1) eqn:?.
+            + type_conv.
+              destruct (morePrecise m1 m0) eqn:prec1;
+                destruct (morePrecise m0 m1) eqn:prec2;
+                destruct m0, m1; simpl in *; try congruence; try auto;
+                  destruct (w ?= w0) eqn:case_w0; rewrite Pos.compare_antisym in lt_e1_e2;
+                    rewrite case_w0 in *; cbn in *; try congruence;
+                      rewrite N.compare_antisym, lt_e2_e3 in lt_e1_e2; cbn in *; congruence.
+            + type_conv; subst.
+              destruct (morePrecise m1 m0) eqn:prec1;
+                destruct (morePrecise m0 m1) eqn:prec2;
+                destruct m, m0, m1; simpl in *; try congruence; try auto;
+                  destruct (w ?= w0) eqn:case_w0; destruct (w0 ?= w1) eqn:case_w1;
+                    try (apply Ndec.Pcompare_Peqb in case_w0);
+                    try (apply Ndec.Pcompare_Peqb in case_w1);
+                    try rewrite Pos.eqb_eq in *;
+                    try rewrite N.eqb_eq in *;
+                    subst;
+                    try congruence;
+                    try rewrite case_w0;
+                    try rewrite case_w1; try auto;
+                      try rewrite Pos.compare_refl;
+                      try (rewrite N.compare_lt_iff in *; eapply N.lt_trans; eauto);
+                      assert (w ?= w1 = Lt) as G
+                          by (rewrite Pos.compare_lt_iff in *;
+                              eapply Pos.lt_trans; eauto);
+                      rewrite G; auto.
+          - apply Nat.compare_eq in c1. subst.
+            rewrite c2. now destruct (mTypeEq m m1).
+          - apply Nat.compare_eq in c2. subst.
+            rewrite c1. now destruct (mTypeEq m m1).
+          - apply nat_compare_lt in c1. apply nat_compare_lt in c2.
+            assert (c3: (n ?= n1)%nat = Lt) by (apply nat_compare_lt; omega).
+            rewrite c3. now destruct (mTypeEq m m1). }
 
         (*
          destruct (morePrecise m m0); destruct m, m0; try congruence;
@@ -1134,7 +1192,7 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
           try (erewrite exprCompare_eq_lt_is_lt; eauto; fail);
           try (erewrite exprCompare_lt_eq_is_lt; eauto; fail);
           try (erewrite IHe1_2; eauto).
-  Admitted.
+  Qed.
 
   Instance eq_compat: Proper (eq ==> eq ==> iff) eq.
   Proof.