From 5e2185cfbea6d09f9b5d3d80200c2340ab2bd846 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 1 Aug 2014 21:50:25 -0700
Subject: [PATCH] =?UTF-8?q?feat(library/unifier):=20postpone=20as=20much?=
 =?UTF-8?q?=20as=20possible=20universe=20constraints=20of=20the=20form=20?=
 =?UTF-8?q?=3Fm1=20=3D=3F=3D=20max(l1,=20l2)=20and=20=3Fm1=20=3D=3F=3D=20i?=
 =?UTF-8?q?max(l1,=20l2)=20where=20=3Fm1=20occurs=20in=20the=20right=20han?=
 =?UTF-8?q?d=20side.=20When=20there=20is=20nothing=20else=20to=20be=20done?=
 =?UTF-8?q?,=20try=20to=20solve=20them=20by=20reducing=20to=20=3Fm1=20=3D?=
 =?UTF-8?q?=20l1=20and=20=3Fm1=20=3D=20l2.?=

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/unifier.cpp       | 53 +++++++++++++++++++++++++++++++----
 tests/lean/run/univ_bug1.lean | 26 +++++++++++++++++
 2 files changed, 74 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/run/univ_bug1.lean

diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index f7c688bdd..3b4f53c11 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -1581,12 +1581,51 @@ struct unifier_fn {
         return try_level_eq_zero(rhs, lhs, j);
     }
 
+    /** \brief Try to solve constraints of the form
+              (?m1 =?= max ?m2 ?m3)
+              (?m1 =?= max ?m2 ?m3)
+        by assigning ?m1 =?= ?m2 and ?m1 =?= ?m3
+
+        \remark we may miss solutions.
+    */
+    status try_merge_max_core(level const & lhs, level const & rhs, justification const & j) {
+        level m1 = lhs;
+        level m2, m3;
+        if (is_max(rhs)) {
+            m2 = max_lhs(rhs);
+            m3 = max_rhs(rhs);
+        } else if (is_imax(rhs)) {
+            m2 = imax_lhs(rhs);
+            m3 = imax_rhs(rhs);
+        } else {
+            return Continue;
+        }
+        if (process_constraint(mk_level_eq_cnstr(m1, m2, j)) &&
+            process_constraint(mk_level_eq_cnstr(m1, m3, j)))
+            return Solved;
+        else
+            return Failed;
+    }
+
+    /** \see try_merge_max_core */
+    status try_merge_max(constraint const & c) {
+        lean_assert(is_level_eq_cnstr(c));
+        level const & lhs = cnstr_lhs_level(c);
+        level const & rhs = cnstr_rhs_level(c);
+        justification const & j = c.get_justification();
+        status st = try_merge_max_core(lhs, rhs, j);
+        if (st != Continue) return st;
+        return try_merge_max_core(rhs, lhs, j);
+    }
+
     /** \brief Process the next constraint in the constraint queue m_cnstrs */
     bool process_next() {
         lean_assert(!m_cnstrs.empty());
         lean_assert(!m_tc[0]->next_cnstr());
         lean_assert(!m_tc[1]->next_cnstr());
-        constraint c = m_cnstrs.min()->first;
+        auto const * p = m_cnstrs.min();
+        unsigned cidx  = p->second;
+        constraint c   = p->first;
         m_cnstrs.erase_min();
         if (is_choice_cnstr(c)) {
             return process_choice_constraint(c);
@@ -1600,10 +1639,14 @@ struct unifier_fn {
                 if (modified)
                     return process_constraint(c);
                 status st = try_level_eq_zero(c);
-                if (st != Continue)
-                    return st == Solved;
-                else
-                    return process_plugin_constraint(c);
+                if (st != Continue) return st == Solved;
+                if (cidx < get_group_first_index(cnstr_group::FlexFlex)) {
+                    add_cnstr(c, cnstr_group::FlexFlex);
+                    return true;
+                }
+                st = try_merge_max(c);
+                if (st != Continue) return st == Solved;
+                return process_plugin_constraint(c);
             } else {
                 lean_assert(is_eq_cnstr(c));
                 if (is_delta_cnstr(c)) {
diff --git a/tests/lean/run/univ_bug1.lean b/tests/lean/run/univ_bug1.lean
new file mode 100644
index 000000000..c4fd877cd
--- /dev/null
+++ b/tests/lean/run/univ_bug1.lean
@@ -0,0 +1,26 @@
+----------------------------------------------------------------------------------------------------
+--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+--- Released under Apache 2.0 license as described in the file LICENSE.
+--- Author: Jeremy Avigad
+----------------------------------------------------------------------------------------------------
+
+import logic data.nat
+using nat
+
+namespace simp
+-- set_option pp.universes true
+-- set_option pp.implicit true
+
+-- first define a class of homogeneous equality
+inductive simplifies_to {T : Type} (t1 t2 : T) : Prop :=
+| mk : t1 = t2 → simplifies_to t1 t2
+
+theorem get_eq {T : Type} {t1 t2 : T} (C : simplifies_to t1 t2) : t1 = t2 :=
+simplifies_to_rec (λx, x) C
+
+theorem infer_eq {T : Type} (t1 t2 : T) {C : simplifies_to t1 t2} : t1 = t2 :=
+simplifies_to_rec (λx, x) C
+
+theorem simp_app [instance] (S T : Type) (f1 f2 : S → T) (s1 s2 : S)
+   (C1 : simplifies_to f1 f2) (C2 : simplifies_to s1 s2) : simplifies_to (f1 s1) (f2 s2) :=
+mk (congr (get_eq C1) (get_eq C2))