From cfe576f55149edea0761cf3f76ac83a9604aa046 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 8 Jan 2014 12:10:46 -0800 Subject: [PATCH] fix(library/elaborator): bug in the elaborator The elaborator was not handling correctly constraints of the form ctx |- ?m << (Pi x : A, B) and ctx |- (Pi x : A, B) << ?m Signed-off-by: Leonardo de Moura --- src/builtin/kernel.lean | 8 +-- src/builtin/obj/kernel.olean | Bin 15306 -> 15086 bytes src/library/elaborator/elaborator.cpp | 82 +++++++++++++++++++++----- 3 files changed, 68 insertions(+), 22 deletions(-) diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 6a4ca392e..68240a21a 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -321,12 +321,8 @@ theorem eq::exists::intro {A : (Type U)} {P Q : A → Bool} (H : ∀ x : A, P x := congr2 (Exists A) (abst H) theorem not::forall (A : (Type U)) (P : A → Bool) : (¬ (∀ x : A, P x)) == (∃ x : A, ¬ P x) -:= let - l1 : ∀ x : A, P x == ¬ ¬ P x := λ x : A, symm (not::not::eq (P x)), - l2 : (∀ x : A, P x) == (∀ x : A, ¬ ¬ P x) := abstpi l1, - s1 : (¬ ∀ x : A, P x) == (¬ ∀ x : A, ¬ ¬ P x) := not::congr l2, - s2 : (¬ ∀ x : A, ¬ ¬ P x) == (∃ x : A, ¬ P x) := refl (∃ x : A, ¬ P x) - in trans s1 s2 +:= calc (¬ ∀ x : A, P x) = (¬ ∀ x : A, ¬ ¬ P x) : not::congr (abstpi (λ x : A, symm (not::not::eq (P x)))) + ... = (∃ x : A, ¬ P x) : refl (∃ x : A, ¬ P x) theorem not::forall::elim {A : (Type U)} {P : A → Bool} (H : ¬ (∀ x : A, P x)) : ∃ x : A, ¬ P x := (not::forall A P) ◂ H diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index 0474c65b838b579dd8c07d187fccba8e69442447..1cd0eb5b84b0324694c10362e699a51ac66a3aca 100644 GIT binary patch delta 795 zcmY*WO=}ZT6n!5vlBCtC*qCaXMs25KqYyF8n{;Azp+X7~1VPY^R1icERFLZ0wVU2Q z;K#z9bYHqq(1o}u-8XdEMQ7uxy3l*>YY7g#^Ugc>-Z$sn`(q`4x%Q$(p^F}@Pb>b8 z9x<=5tH>Wg&+)PwvEfbsf}rm5vR`MRsQUmFg~01V0cZa|+b^`*nj4!z=nbI2%WjZv z-&`90Xcck~pwc%}XJ+$6I(!SVa!@`2e$)GOQ7amxRegs3q|H$kn%<-5 z$O;s>&TCzywN5+{K`6*j^gTrN9Vo|WuaoL3`djnW7Q{%? zj{!d!>^^NToN_0asy-g#N8Oi6^l_G{NjFMt?=mF2p8)?-l3mP#28M5>nW>*z%MZ)c63%@L2KoAXQ$-qHs3Z$a-=glqIShQk8WgKl%_ akg3w`ZmkgeL&Ar0ap~zZWSACFH~j~&6{);>HVp87P zaKxOv@8FkqVHZoVhhdh?_j+|qq)kU~Za1R#Eh(n%EK5{eg>m``*s}~_cK-L(2Lw|| zd6y1%;~sk!&QVe(L1`f{W-YQ_!2#kI;?5pD>I)FMKwVfGPBOCYj2$t#OjaHP93>(u zIqEAC&O;c?slKg}6_3~-*e(c6ER2>gJjlpm+<6#v9#V-cqDLAgWxU3@E&=r(>yQ}) z6ATvs^9+v?Qm>a0cyiF**+uk+dE6+7Bj#-*=tO65=S8qfTx+O^6b?|+SyA!0T>Oa$T9@&LWY#=iKQ3k7{B3rnc1^Ff zy;Y%vbCMNu7u$9P(KJUPQ@bntiZ3ASwCGV!$>;_1rqvTU^QUz}RE_7aAIc@<;QDQ_ zbk1DzABd9q>{qf?1eW+BiYv&9i-@e6`L-|0q$g{xwQu?xNLewPfL2T$(28jg(tY0C z4T6HF%b4G7uXY-&5hUB|jccVQaIps`MZ&nJ&R{t0nPKNtpeFIUP@uO%?mqr;6$gy; z0L#%h!zwSEmz}n#v2q!#jkSwBe_gUiFq~ow&`!ZB(r6>zk% diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 43dd68765..3d65fb900 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -1307,6 +1307,45 @@ class elaborator::imp { } } + /** + \brief Resolve constraints of the form + + ctx |- ?m << Pi(x : A, B) (param is_lhs is true) + and + ctx |- Pi(x : A, B) << ?m (param is_lhs is false) + + where ?m is not assigned and does not have a local context. + + We replace + ctx | ?m << Pi(x : A, B) + with + ctx |- ?m == Pi(x : A, ?m1) + ctx, x : A |- ?m1 << B + */ + void process_metavar_conv_pi(unification_constraint const & c, expr const & m, expr const & pi, bool is_lhs) { + lean_assert(!is_eq(c)); + lean_assert(is_metavar(m) && !has_local_context(m)); + lean_assert(!is_assigned(m)); + lean_assert(is_pi(pi)); + lean_assert(is_lhs || is_eqp(convertible_to(c), m)); + lean_assert(!is_lhs || is_eqp(convertible_from(c), m)); + context ctx = get_context(c); + context new_ctx = extend(ctx, abst_name(pi), abst_domain(pi)); + expr m1 = m_state.m_menv->mk_metavar(new_ctx); + justification new_jst(new destruct_justification(c)); + + // Add ctx, x : A |- ?m1 << B when is_lhs == true, + // and ctx, x : A |- B << ?m1 when is_lhs == false + expr lhs = m1; + expr rhs = abst_body(pi); + if (!is_lhs) + swap(lhs, rhs); + push_new_constraint(false, new_ctx, lhs, rhs, new_jst); + + // Add ctx |- ?m == Pi(x : A, ?m1) + push_new_eq_constraint(ctx, m, update_abstraction(pi, abst_domain(pi), m1), new_jst); + } + bool process_eq_convertible(context const & ctx, expr const & a, expr const & b, unification_constraint const & c) { bool eq = is_eq(c); if (a == b) @@ -1376,23 +1415,30 @@ class elaborator::imp { if (!is_meta_app(a) && !is_meta_app(b) && normalize_head(a, b, c)) { return true; } if (!eq) { - // TODO(Leo): use is_actual_lower and is_actual_upper - // Try to assign convertability constraints. - if (!is_type(b) && !is_meta(b) && is_metavar(a) && !is_assigned(a) && !has_local_context(a)) { - // We can assign a <- b at this point IF b is not (Type lvl) or Metavariable - lean_assert(!has_metavar(b, a)); - return assign(a, b, c, true); + if (is_metavar(a) && !is_assigned(a) && !has_local_context(a)) { + if (is_pi(b)) { + process_metavar_conv_pi(c, a, b, true); + return true; + } else if (!is_type(b) && !is_meta(b)) { + // We can assign a <- b at this point IF b is not (Type lvl) or Metavariable + lean_assert(!has_metavar(b, a)); + return assign(a, b, c, true); + } } - if (!is_type(a) && !is_meta(a) && a != Bool && is_metavar(b) && !is_assigned(b) && !has_local_context(b)) { - // We can assign b <- a at this point IF a is not (Type lvl) or Metavariable or Bool. - lean_assert(!has_metavar(a, b)); - return assign(b, a, c, false); + + if (is_metavar(b) && !is_assigned(b) && !has_local_context(b)) { + if (is_pi(a)) { + process_metavar_conv_pi(c, b, a, false); + return true; + } else if (!is_type(a) && !is_meta(a) && a != Bool) { + // We can assign b <- a at this point IF a is not (Type lvl) or Metavariable or Bool. + lean_assert(!has_metavar(a, b)); + return assign(b, a, c, false); + } } } - // TODO(Leo): normalize pi domain... to make sure we are not missing solutions in process_simple_ho_match - if (process_simple_ho_match(ctx, a, b, true, c) || process_simple_ho_match(ctx, b, a, false, c)) return true; @@ -1511,8 +1557,6 @@ class elaborator::imp { } if (is_bool(lhs1)) lhs1 = Type(); - if (is_bool(lhs2)) - lhs2 = Type(); if (is_type(lhs1) && is_type(lhs2)) { justification new_jst(new normalize_justification(c)); expr new_lhs = mk_type(max(ty_level(lhs1), ty_level(lhs2))); @@ -1526,10 +1570,16 @@ class elaborator::imp { justification new_jst(new normalize_justification(c)); push_active(mk_convertible_constraint(get_context(c), lhs2, rhs, new_jst)); return true; - } else if (lhs2 == rhs) { - // ctx |- max(lhs1, lhs2) == rhs + } else if (lhs2 == rhs && is_type(lhs2)) { + // ctx |- max(lhs1, lhs2) == rhs IF lhs2 is a Type // ==> IF lhs1 = rhs // ctx |- lhs2 << rhs + + // Remark: this rule is not applicable when lhs2 == Bool. + // Recall that max is actually a constraint generated for a Pi(x : A, B) + // where lhs1 and lhs2 represent the types of A and B. + // If lhs2 == Bool, the type of Pi(x : A, B) is Bool, and the type + // of A (lhs1) can be as big as we want justification new_jst(new normalize_justification(c)); push_active(mk_convertible_constraint(get_context(c), lhs1, rhs, new_jst)); return true;