feat(library/unifier): solved universe constraints of the form succ^k1 a = max k2 ?m (when k1 >= k2)

src/kernel/level.h

@@ -85,6 +85,9 @@ level mk_param_univ(name const & n);
 level mk_global_univ(name const & n);
 level mk_meta_univ(name const & n);
 
+/** \brief Convert (succ^k l) into (l, k). If l is not a succ, then return (l, 0) */
+pair<level, unsigned> to_offset(level l);
+
 inline unsigned hash(level const & l) { return l.hash(); }
 inline level_kind kind(level const & l) { return l.kind(); }
 inline bool is_zero(level const & l)   { return kind(l) == level_kind::Zero; }

src/library/unifier.cpp

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <memory>
 #include <vector>
 #include <limits>
+#include <algorithm>
 #include "util/interrupt.h"
 #include "util/luaref.h"
 #include "util/lazy_list_fn.h"
@@ -2043,7 +2044,7 @@ struct unifier_fn {
         }
     }
 
-    /** \brief Return true iff \c is a constraint of the form
+    /** \brief Return solved iff \c c is a constraint of the form
                    lhs =?= max(rest, lhs)
                and is successfully solved.
     */
@@ -2060,6 +2061,43 @@ struct unifier_fn {
             return Continue;
     }
 
+    /** Auxiliary method for process_succ_eq_max */
+    status process_succ_eq_max_core(level const & lhs, level const & rhs, justification const & jst) {
+        if (!is_succ(lhs) || !is_max(rhs))
+            return Continue;
+        level rhs_l = max_lhs(rhs);
+        level rhs_r = max_rhs(rhs);
+        if (is_meta(rhs_l))
+            std::swap(rhs_l, rhs_r);
+        if (!is_meta(rhs_r) || !is_explicit(rhs_l))
+            return Continue;
+        unsigned k_2 = to_explicit(rhs_l);
+        pair<level, unsigned> lhs_k = to_offset(lhs);
+        if (lhs_k.second < k_2)
+            return Continue;
+        if (assign(rhs_r, lhs, jst)) {
+            return Solved;
+        } else {
+            set_conflict(jst);
+            return Failed;
+        }
+    }
+
+    /** \brief Return Solved iff \c c is a constraint of the form
+                  succ^k_1 a =?= max(k_2, ?m)
+               where k_1 >= k_2
+              and is successfully solved
+    */
+    status process_succ_eq_max(constraint const & c) {
+        lean_assert(is_level_eq_cnstr(c));
+        level lhs = cnstr_lhs_level(c);
+        level rhs = cnstr_rhs_level(c);
+        justification jst = c.get_justification();
+        status st = process_succ_eq_max_core(lhs, rhs, jst);
+        if (st != Continue) return st;
+        return process_succ_eq_max_core(rhs, lhs, jst);
+    }
+
     /**
        \brief Process the following constraints
           1. (max l1 l2) =?= 0    OR
@@ -2152,6 +2190,8 @@ struct unifier_fn {
                 }
                 status st = process_l_eq_max(c);
                 if (st != Continue) return st == Solved;
+                st = process_succ_eq_max(c);
+                if (st != Continue) return st == Solved;
                 if (m_config.m_discard) {
                     // we only try try_level_eq_zero and try_merge_max when we are discarding
                     // constraints that canno be solved.

tests/lean/run/univ_problem.lean

@@ -0,0 +1,88 @@
+import logic data.nat.basic data.prod data.unit
+open nat prod
+
+inductive vector (A : Type) : nat → Type :=
+vnil {} : vector A zero,
+vcons   : Π {n : nat}, A → vector A n → vector A (succ n)
+
+namespace vector
+  print definition no_confusion
+  infixr `::` := vcons
+
+  section
+    universe variables l₁ l₂
+    variable {A : Type.{l₁}}
+    variable {C : Π (n : nat), vector A n → Type.{l₂+1}}
+    definition brec_on {n : nat} (v : vector A n) (H : Π (n : nat) (v : vector A n), @below A C n v → C n v) : C n v :=
+    have general : C n v × @below A C n v, from
+      rec_on v
+       (pair (H zero vnil unit.star) unit.star)
+       (λ (n₁ : nat) (a₁ : A) (v₁ : vector A n₁) (r₁ : C n₁ v₁ × @below A C n₁ v₁),
+          have b : @below A C _ (vcons a₁ v₁), from
+            r₁,
+          have c : C (succ n₁) (vcons a₁ v₁), from
+            H (succ n₁) (vcons a₁ v₁) b,
+          pair c b),
+    pr₁ general
+  end
+
+  print "====================="
+  definition append {A : Type} {n m : nat} (w : vector A m) (v : vector A n) : vector A (n + m) :=
+  brec_on w (λ (n : nat) (w : vector A n),
+    cases_on w
+      (λ (B : below vnil), v)
+      (λ (n₁ : nat) (a₁ : A) (v₁ : vector A n₁) (B : below (vcons a₁ v₁)),
+         vcons a₁ (pr₁ B)))
+
+  exit
+  check brec_on
+  definition bw := @below
+
+  definition sum {n : nat} (v : vector nat n) : nat :=
+  brec_on v (λ (n : nat) (v : vector nat n),
+    cases_on v
+      (λ (B : bw vnil), zero)
+      (λ (n₁ : nat) (a : nat) (v₁ : vector nat n₁) (B : bw (vcons a v₁)),
+         a + pr₁ B))
+
+  example :  sum (10 :: 20 :: vnil) = 30 :=
+  rfl
+
+  definition addk {n : nat} (v : vector nat n) (k : nat) : vector nat n :=
+  brec_on v (λ (n : nat) (v : vector nat n),
+    cases_on v
+      (λ (B : bw vnil), vnil)
+      (λ (n₁ : nat) (a₁ : nat) (v₁ : vector nat n₁) (B : bw (vcons a₁ v₁)),
+         vcons (a₁+k) (pr₁ B)))
+
+  example : addk (1 :: 2 :: vnil) 3 = 4 :: 5 :: vnil :=
+  rfl
+
+  example : append (1 :: 2 :: vnil) (3 :: vnil) = 1 :: 2 :: 3 :: vnil :=
+  rfl
+
+  definition head {A : Type} {n : nat} (v : vector A (succ n)) : A :=
+  cases_on v
+    (λ H : succ n = 0, nat.no_confusion H)
+    (λn' h t (H : succ n = succ n'), h)
+    rfl
+
+  definition tail {A : Type} {n : nat} (v : vector A (succ n)) : vector A n :=
+  @cases_on A (λn' v, succ n = n' → vector A (pred n')) (succ n) v
+    (λ H : succ n = 0, nat.no_confusion H)
+    (λ (n' : nat) (h : A) (t : vector A n') (H : succ n = succ n'),
+       t)
+    rfl
+
+  definition add {n : nat} (w v : vector nat n) : vector nat n :=
+  @brec_on nat (λ (n : nat) (v : vector nat n), vector nat n → vector nat n) n w
+  (λ (n : nat) (w : vector nat n),
+    cases_on w
+      (λ (B : bw vnil) (w : vector nat zero), vnil)
+      (λ (n₁ : nat) (a₁ : nat) (v₁ : vector nat n₁) (B : bw (vcons a₁ v₁)) (v : vector nat (succ n₁)),
+         vcons (a₁ + head v) (pr₁ B (tail v)))) v
+
+  example : add (1 :: 2 :: vnil) (3 :: 5 :: vnil) = 4 :: 7 :: vnil :=
+  rfl
+
+end vector