From 51719145f9a123a7b39dfa2f63f723b5622ad704 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 12 Nov 2014 17:28:33 -0800 Subject: [PATCH] feat(library/unifier): solved universe constraints of the form succ^k1 a = max k2 ?m (when k1 >= k2) --- src/kernel/level.h | 3 ++ src/library/unifier.cpp | 42 ++++++++++++++- tests/lean/run/univ_problem.lean | 88 ++++++++++++++++++++++++++++++++ 3 files changed, 132 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/univ_problem.lean diff --git a/src/kernel/level.h b/src/kernel/level.h index b4dfe4295..737bba0fc 100644 --- a/src/kernel/level.h +++ b/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 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; } diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 4a6fc26c4..328d5644a 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include #include +#include #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 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. diff --git a/tests/lean/run/univ_problem.lean b/tests/lean/run/univ_problem.lean new file mode 100644 index 000000000..d846183a2 --- /dev/null +++ b/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