feat(library/unifier): consider whnf case-split on flex-rigid constraints whenever the rhs contains a local constant that is not in the lhs

src/library/unifier.cpp

@@ -264,13 +264,6 @@ static cnstr_group to_cnstr_group(unsigned d) {
     return static_cast<cnstr_group>(d);
 }
 
-/** \brief Return true if all arguments of lhs are local constants */
-static bool all_local(expr const & lhs) {
-    buffer<expr> margs;
-    get_app_args(lhs, margs);
-    return std::all_of(margs.begin(), margs.end(), [&](expr const & e) { return is_local(e); });
-}
-
 /** \brief Convert choice constraint delay factor to cnstr_group */
 cnstr_group get_choice_cnstr_group(constraint const & c) {
     lean_assert(is_choice_cnstr(c));
@@ -1677,6 +1670,31 @@ struct unifier_fn {
         return none_expr();
     }
 
+    /** \brief When solving flex-rigid constraints lhs =?= rhs (lhs is of the form ?M a_1 ... a_n),
+        we consider an additional case-split where rhs is put in weak-head-normal-form when
+
+        1- Option unifier.computation is true
+        2- At least one a_i is not a local constant
+        3- rhs contains a local constant that is not equal to any a_i.
+    */
+    bool use_flex_rigid_whnf_split(expr const & lhs, expr const & rhs) {
+        lean_assert(is_meta(lhs));
+        if (m_config.m_computation)
+            return true; // if unifier.computation is true, we always consider the additional whnf split
+        buffer<expr> locals;
+        expr const * it = &lhs;
+        while (is_app(*it)) {
+            expr const & arg = app_arg(*it);
+            if (!is_local(arg))
+                return true; // lhs contains non-local constant
+            locals.push_back(arg);
+            it = &(app_fn(*it));
+        }
+        if (!context_check(rhs, locals))
+            return true; // rhs contains local constant that is not in locals
+        return false;
+    }
+
     /** \brief Process a flex rigid constraint */
     bool process_flex_rigid(expr lhs, expr const & rhs, justification const & j, bool relax) {
         lean_assert(is_meta(lhs));
@@ -1705,7 +1723,7 @@ struct unifier_fn {
         buffer<constraints> alts;
         process_flex_rigid_core(lhs, rhs, j, relax, alts);
         append_auxiliary_constraints(alts, to_list(aux.begin(), aux.end()));
-        if (m_config.m_computation || !all_local(lhs)) {
+        if (use_flex_rigid_whnf_split(lhs, rhs)) {
             expr rhs_whnf = whnf(rhs, j, relax, aux);
             if (rhs_whnf != rhs) {
                 if (is_meta(rhs_whnf)) {

tests/lean/run/cat.lean

@@ -0,0 +1,42 @@
+-- Copyright (c) 2014 Floris van Doorn. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Floris van Doorn
+
+-- category
+import logic.core.eq logic.core.connectives
+import data.unit data.sigma data.prod
+import struc.function
+
+inductive category [class] (ob : Type) (mor : ob → ob → Type) : Type :=
+mk : Π (comp : Π⦃A B C : ob⦄, mor B C → mor A B → mor A C)
+           (id : Π {A : ob}, mor A A),
+            (Π {A B C D : ob} {f : mor A B} {g : mor B C} {h : mor C D},
+            comp h (comp g f) = comp (comp h g) f) →
+           (Π {A B : ob} {f : mor A B}, comp f id = f) →
+           (Π {A B : ob} {f : mor A B}, comp id f = f) →
+            category ob mor
+
+namespace category
+  precedence `∘` : 60
+
+  section
+  parameters {ob : Type} {mor : ob → ob → Type} {Cat : category ob mor}
+  abbreviation compose := rec (λ comp id assoc idr idl, comp) Cat
+  abbreviation id := rec (λ comp id assoc idr idl, id) Cat
+  abbreviation ID (A : ob) := @id A
+
+  infixr `∘` := compose
+
+  theorem assoc : Π {A B C D : ob} {f : mor A B} {g : mor B C} {h : mor C D},
+                h ∘ (g ∘ f) = (h ∘ g) ∘ f :=
+  rec (λ comp id assoc idr idl, assoc) Cat
+
+  theorem id_right : Π {A B : ob} {f : mor A B}, f ∘ id = f :=
+  rec (λ comp id assoc idr idl, idr) Cat
+  theorem id_left  : Π {A B : ob} {f : mor A B}, id ∘ f = f :=
+  rec (λ comp id assoc idr idl, idl) Cat
+
+  theorem id_left2 {A B : ob} {f : mor A B} : id ∘ f = f :=
+  rec (λ comp id assoc idr idl, idl A B f) Cat
+  end
+end category

tests/lean/run/impbug1.lean

@@ -0,0 +1,19 @@
+-- category
+
+abbreviation Prop := Type.{0}
+variable eq {A : Type} : A → A → Prop
+infix `=`:50 := eq
+
+inductive category (ob : Type) (mor : ob → ob → Type) : Type :=
+mk : Π (id : Π (A : ob), mor A A),
+     (Π (A B : ob) (f : mor A A), id A = f) → category ob mor
+
+abbreviation id (ob : Type) (mor : ob → ob → Type) (Cat : category ob mor) := category.rec (λ id idl, id) Cat
+
+theorem id_left (ob : Type) (mor : ob → ob → Type) (Cat : category ob mor) (A : ob) (f : mor A A) :
+     @eq (mor A A) (id ob mor Cat A) f :=
+@category.rec ob mor (λ (C : category ob mor), @eq (mor A A) (id ob mor C A) f)
+  (λ (id  : Π (A : ob), mor A A)
+     (idl : Π (A : ob), _),
+     idl A A f)
+  Cat

tests/lean/run/impbug2.lean

@@ -0,0 +1,21 @@
+-- category
+
+abbreviation Prop := Type.{0}
+variable eq {A : Type} : A → A → Prop
+infix `=`:50 := eq
+
+inductive category (ob : Type) (mor : ob → ob → Type) : Type :=
+mk : Π (id : Π (A : ob), mor A A),
+     (Π (A B : ob) (f : mor A A), id A = f) → category ob mor
+
+abbreviation id (ob : Type) (mor : ob → ob → Type) (Cat : category ob mor) := category.rec (λ id idl, id) Cat
+variable ob  : Type.{1}
+variable mor : ob → ob → Type.{1}
+variable Cat : category ob mor
+
+theorem id_left (A : ob) (f : mor A A) : @eq (mor A A) (id ob mor Cat A) f :=
+@category.rec ob mor (λ (C : category ob mor), @eq (mor A A) (id ob mor C A) f)
+  (λ (id  : Π (T : ob), mor T T)
+     (idl : Π (T : ob), _),
+     idl A A f)
+  Cat

tests/lean/run/impbug3.lean

@@ -0,0 +1,22 @@
+-- category
+
+abbreviation Prop := Type.{0}
+variable eq {A : Type} : A → A → Prop
+infix `=`:50 := eq
+
+variable ob  : Type.{1}
+variable mor : ob → ob → Type.{1}
+
+inductive category : Type :=
+mk : Π (id : Π (A : ob), mor A A),
+     (Π (A B : ob) (f : mor A A), id A = f) → category
+
+abbreviation id (Cat : category) := category.rec (λ id idl, id) Cat
+variable Cat : category
+
+theorem id_left (A : ob) (f : mor A A) : @eq (mor A A) (id Cat A) f :=
+@category.rec (λ (C : category), @eq (mor A A) (id C A) f)
+  (λ (id  : Π (T : ob), mor T T)
+     (idl : Π (T : ob), _),
+     idl A A f)
+  Cat

tests/lean/run/impbug4.lean

@@ -0,0 +1,23 @@
+-- category
+
+abbreviation Prop := Type.{0}
+variable eq {A : Type} : A → A → Prop
+infix `=`:50 := eq
+
+variable ob  : Type.{1}
+variable mor : ob → ob → Type.{1}
+
+inductive category : Type :=
+mk : Π (id : Π (A : ob), mor A A),
+     (Π (A B : ob) (f : mor A A), id A = f) → category
+
+abbreviation id (Cat : category) := category.rec (λ id idl, id) Cat
+variable Cat : category
+
+set_option unifier.computation true
+print "-----------------"
+theorem id_left (A : ob) (f : mor A A) : @eq (mor A A) (id Cat A) f :=
+@category.rec
+  (λ (C : category), Π (A B : ob) (f : mor A A), @eq (mor A A) (id C A) f)
+  (λ id idl, idl)
+  Cat A A f