Finish fixing merge of Expressions

coq/Expressions.v

@@ -385,6 +385,12 @@ Module ExpOrderedType (V_ordered:OrderType) <: OrderType.
         * destruct m, m0; unfold morePrecise in *; cbv; congruence.
   Qed.
 
+  Lemma expCompare_eq_sym e1 e2:
+      expCompare e1 e2 = Eq <-> expCompare e2 e1 = Eq.
+  Proof.
+    now split; intros H; rewrite expCompare_antisym; rewrite H.
+  Qed.
+
   Lemma expCompare_lt_eq_is_lt e1:
     forall e2 e3,
       expCompare e1 e2 = Lt -> expCompare e2 e3 = Eq -> expCompare e1 e3 = Lt.
@@ -632,7 +638,32 @@ Module ExpOrderedType (V_ordered:OrderType) <: OrderType.
       try (split; try congruence; intros);
       try (specialize (IHe1_1 _ Heqc _ _ Heqc0); simpl in *; rewrite IHe1_1 in *; congruence);
       try (specialize (IHe1_1 _ Heqc _ _ Heqc0); simpl in *; rewrite <- IHe1_1 in *; congruence).
-    - admit.
+    - try (split; auto; fail);
+        destruct (expCompare e1_1 e2_1) eqn:?;
+                 destruct (expCompare e3_1 e4_1) eqn:?;
+                 try congruence;
+        destruct (expCompare e1_1 e3_1) eqn:?;
+                 destruct (expCompare e2_1 e4_1) eqn:?;
+                 try (split; congruence);
+        try (specialize (IHe1_2 _ e1_eq_e2 _ _ e3_eq_e4); simpl in *; rewrite IHe1_2 in *; split; auto; fail);
+        try (split; try congruence; intros);
+        try (specialize (IHe1_1 _ Heqc _ _ Heqc0); simpl in *; rewrite IHe1_1 in *; congruence);
+        try (specialize (IHe1_1 _ Heqc _ _ Heqc0); simpl in *; rewrite <- IHe1_1 in *; congruence);
+        try (split; auto; fail);
+        destruct (expCompare e1_2 e2_2) eqn:?;
+                 destruct (expCompare e3_2 e4_2) eqn:?;
+                 try congruence;
+        destruct (expCompare e1_2 e3_2) eqn:?;
+                 destruct (expCompare e2_2 e4_2) eqn:?;
+                 try (split; congruence);
+        try (split; try congruence; intros);
+        try (specialize (IHe1_2 _ Heqc3 _ _ Heqc4); simpl in *; rewrite IHe1_2 in *; congruence);
+        try (specialize (IHe1_2 _ Heqc3 _ _ Heqc4); simpl in *; rewrite <- IHe1_2 in *; congruence);
+        try congruence;
+        erewrite expCompare_eq_trans; eauto;
+        erewrite expCompare_eq_trans; eauto;
+        rewrite expCompare_antisym;
+        now (try rewrite e3_eq_e4; try rewrite e1_eq_e2).
     -  destruct (mTypeEq m m0) eqn:?; destruct (mTypeEq m1 m2) eqn:?;
                [type_conv | | |].
        + specialize (IHe1 _ e1_eq_e2 _ _ e3_eq_e4); simpl in *.
@@ -641,7 +672,7 @@ Module ExpOrderedType (V_ordered:OrderType) <: OrderType.
        + destruct (morePrecise m1 m2); congruence.
        + destruct (morePrecise m m0); congruence.
        + destruct (morePrecise m m0); congruence.
-  Admitted.
+  Qed.
 
   Instance lt_compat: Proper (eq ==> eq ==> iff) lt.
   Proof.
@@ -681,7 +712,38 @@ Module ExpOrderedType (V_ordered:OrderType) <: OrderType.
         try (specialize (IHe1_1 _ Heqc _ _ Heqc0); simpl in *; rewrite <- IHe1_1 in *; congruence);
         try (rewrite (eq_comp _ _ Heqc _ _ Heqc0) in *; congruence);
         try (rewrite <- (eq_comp _ _ Heqc _ _ Heqc0) in *; congruence).
-    - admit.
+    - pose proof eq_compat as eq_comp. unfold Proper, eq in eq_comp.
+      destruct (expCompare e1_1 e2_1) eqn:?;
+               destruct (expCompare e3_1 e4_1) eqn:?;
+               try congruence;
+        destruct (expCompare e1_1 e3_1) eqn:?;
+                 destruct (expCompare e2_1 e4_1) eqn:?;
+                 try (split; congruence);
+        try (specialize (IHe1_2 _ e1_eq_e2 _ _ e3_eq_e4); simpl in *; rewrite IHe1_2 in *; split; auto; fail);
+        try (split; try congruence; intros);
+        try (specialize (IHe1_1 _ Heqc _ _ Heqc0); simpl in *; rewrite IHe1_1 in *; congruence);
+        try (specialize (IHe1_1 _ Heqc _ _ Heqc0); simpl in *; rewrite <- IHe1_1 in *; congruence);
+        try (rewrite (eq_comp _ _ Heqc _ _ Heqc0) in *; congruence);
+        try (rewrite <- (eq_comp _ _ Heqc _ _ Heqc0) in *; congruence);
+        destruct (expCompare e1_2 e2_2) eqn:?;
+               destruct (expCompare e3_2 e4_2) eqn:?;
+               try congruence;
+        destruct (expCompare e1_2 e3_2) eqn:?;
+                 destruct (expCompare e2_2 e4_2) eqn:?;
+                 try (split; congruence);
+        try (specialize (IHe1_3 _ e1_eq_e2 _ _ e3_eq_e4); simpl in *; rewrite IHe1_3 in *; split; auto; fail);
+        try (split; try congruence; intros);
+        try (specialize (IHe1_2 _ Heqc3 _ _ Heqc4); simpl in *; rewrite IHe1_2 in *; congruence);
+        try (specialize (IHe1_2 _ Heqc3 _ _ Heqc4); simpl in *; rewrite <- IHe1_2 in *; congruence);
+        try (rewrite (eq_comp _ _ Heqc3 _ _ Heqc4) in *; congruence);
+        try (rewrite <- (eq_comp _ _ Heqc3 _ _ Heqc4) in *; congruence);
+        try congruence.
+      + apply (expCompare_lt_eq_is_lt _ _ _ H) in e3_eq_e4;
+        rewrite expCompare_eq_sym in e1_eq_e2;
+        now apply (expCompare_eq_lt_is_lt _ _ _ e1_eq_e2).
+      + rewrite expCompare_eq_sym in e3_eq_e4;
+        apply (expCompare_lt_eq_is_lt _ _ _ H) in e3_eq_e4;
+        now apply (expCompare_eq_lt_is_lt _ _ _ e1_eq_e2).
     -  destruct (mTypeEq m m0) eqn:?; destruct (mTypeEq m1 m2) eqn:?;
                [type_conv | | |].
        + specialize (IHe1 _ e1_eq_e2 _ _ e3_eq_e4); simpl in *.
@@ -690,7 +752,7 @@ Module ExpOrderedType (V_ordered:OrderType) <: OrderType.
        + destruct (morePrecise m1 m2); congruence.
        + destruct (morePrecise m m0); congruence.
        + destruct (morePrecise m m0); congruence.
-  Admitted.
+  Qed.
 
   Lemma compare_spec : forall x y, CompSpec eq lt x y (expCompare x y).
   Proof.