From ea739100b3a69a3340eb825277e27fd6111bd67f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 28 Oct 2014 16:08:39 -0700 Subject: [PATCH] fix(library/unifier): broken optimization in the unifier See new comments and tests for details. --- library/data/quotient/classical.lean | 9 +++-- library/hott/equiv.lean | 3 ++ library/hott/path.lean | 9 +++-- src/library/unifier.cpp | 51 +++++++++++++++++------- tests/lean/slow/path_groupoids.lean | 1 + tests/lean/unifier_bug.lean | 7 ++++ tests/lean/unifier_bug.lean.expected.out | 8 ++++ 7 files changed, 68 insertions(+), 20 deletions(-) create mode 100644 tests/lean/unifier_bug.lean create mode 100644 tests/lean/unifier_bug.lean.expected.out diff --git a/library/data/quotient/classical.lean b/library/data/quotient/classical.lean index cc17afef6..894ef444e 100644 --- a/library/data/quotient/classical.lean +++ b/library/data/quotient/classical.lean @@ -34,9 +34,12 @@ have H3 : ∀c, R a c ↔ R b c, from iff.intro (assume H4 : R a c, transR (symmR H2) H4) (assume H4 : R b c, transR H2 H4), -have H4 : (fun c, R a c) = (fun c, R b c), from funext (take c, iff_to_eq (H3 c)), -show @epsilon _ (nonempty.intro a) (λc, R a c) = @epsilon _ (nonempty.intro b) (λc, R b c), - from congr_arg _ H4 +have H4 : (fun c, R a c) = (fun c, R b c), from + funext (take c, iff_to_eq (H3 c)), +have H5 [visible] : nonempty A, from + nonempty.intro a, +show epsilon (λc, R a c) = epsilon (λc, R b c), from + congr_arg _ H4 definition quotient {A : Type} (R : A → A → Prop) : Type := image (prelim_map R) diff --git a/library/hott/equiv.lean b/library/hott/equiv.lean index c3bd6af5c..6a21aa0f1 100644 --- a/library/hott/equiv.lean +++ b/library/hott/equiv.lean @@ -130,6 +130,8 @@ namespace IsEquiv variables {A B : Type} (f : A → B) (g : B → A) (retr : Sect g f) (sect : Sect f g) + context + set_option unifier.max_steps 30000 --To construct an equivalence it suffices to state the proof that the inverse is a quasi-inverse. definition adjointify : IsEquiv f := let sect' := (λx, ap g (ap f ((sect x)⁻¹)) ⬝ ap g (retr (f x)) ⬝ sect x) in @@ -163,6 +165,7 @@ namespace IsEquiv from moveR_M1 _ _ eq3, eq4) in IsEquiv_mk g retr sect' adj' + end end IsEquiv namespace IsEquiv diff --git a/library/hott/path.lean b/library/hott/path.lean index bb6ae51e1..4e992eab6 100644 --- a/library/hott/path.lean +++ b/library/hott/path.lean @@ -8,7 +8,7 @@ -- o Try doing these proofs with tactics. -- o Try using the simplifier on some of these proofs. -import general_notation algebra.function +import general_notation algebra.function tools.tactic open function @@ -344,8 +344,11 @@ rec_on q idp definition concat_p_A1p {A : Type} {g : A → A} (p : Πx, x ≈ g x) {x y : A} (q : x ≈ y) {z : A} (s : g y ≈ z) : p x ⬝ (ap g q ⬝ s) ≈ q ⬝ (p y ⬝ s) := -rec_on s (rec_on q (concat_1p _ ▹ idp)) - +begin + apply (rec_on s), + apply (rec_on q), + apply (concat_1p _ ▹ idp) +end -- Action of [apD10] and [ap10] on paths -- ------------------------------------- diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 710af564a..4a6fc26c4 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -1635,21 +1635,44 @@ struct unifier_fn { expr mk_imitiation_arg(expr const & arg, expr const & type, buffer const & locals, constraint_seq & cs) { - if (!has_meta_args() && is_local(arg) && contains_local(arg, locals)) { - return arg; + // The following optimization is broken. It does not really work when we have dependent + // types. The problem is that the type of arg may depend on other arguments, + // and constraints are not generated to enforce it. + // + // Here is a minimal counterexample + // ?M A B a b H B b =?= heq.type_eq A B a b H + // with this optimization the imitation is + // + // ?M := fun (A B a b H B' b'), heq.type_eq A (?M1 A B a b H B' b') a (?M2 A B a b H B' b') H + // + // This imitation is only correct if + // typeof(H) is (heq A a (?M1 A B a b H B' b') (?M2 A B a b H B' b')) + // + // Adding an extra constraint is problematic since typeof(H) may contain local constants, + // and these local constants may have been "renamed" by mk_local_context above + // + // For now, we simply comment the optimization. + // + + // Broken optimization + // if (!has_meta_args() && is_local(arg) && contains_local(arg, locals)) { + // return arg; + // } + + // The following code is not affected by the problem above because we + // attach the type \c type to the new metavariables being created. + + // std::cout << "type: " << type << "\n"; + if (context_check(type, locals)) { + expr maux = mk_metavar(u.m_ngen.next(), Pi(locals, type)); + // std::cout << " >> " << maux << " : " << mlocal_type(maux) << "\n"; + cs = mk_eq_cnstr(mk_app(maux, margs), arg, j, relax) + cs; + return mk_app(maux, locals); } else { - // std::cout << "type: " << type << "\n"; - if (context_check(type, locals)) { - expr maux = mk_metavar(u.m_ngen.next(), Pi(locals, type)); - // std::cout << " >> " << maux << " : " << mlocal_type(maux) << "\n"; - cs = mk_eq_cnstr(mk_app(maux, margs), arg, j, relax) + cs; - return mk_app(maux, locals); - } else { - expr maux_type = mk_metavar(u.m_ngen.next(), Pi(locals, mk_sort(mk_meta_univ(u.m_ngen.next())))); - expr maux = mk_metavar(u.m_ngen.next(), Pi(locals, mk_app(maux_type, locals))); - cs = mk_eq_cnstr(mk_app(maux, margs), arg, j, relax) + cs; - return mk_app(maux, locals); - } + expr maux_type = mk_metavar(u.m_ngen.next(), Pi(locals, mk_sort(mk_meta_univ(u.m_ngen.next())))); + expr maux = mk_metavar(u.m_ngen.next(), Pi(locals, mk_app(maux_type, locals))); + cs = mk_eq_cnstr(mk_app(maux, margs), arg, j, relax) + cs; + return mk_app(maux, locals); } } diff --git a/tests/lean/slow/path_groupoids.lean b/tests/lean/slow/path_groupoids.lean index fe251f9a2..14e7f4769 100644 --- a/tests/lean/slow/path_groupoids.lean +++ b/tests/lean/slow/path_groupoids.lean @@ -12,6 +12,7 @@ infixl `∘`:60 := compose -- Path -- ---- +set_option unifier.max_steps 100000 inductive path {A : Type} (a : A) : A → Type := idpath : path a a diff --git a/tests/lean/unifier_bug.lean b/tests/lean/unifier_bug.lean new file mode 100644 index 000000000..af6f1136d --- /dev/null +++ b/tests/lean/unifier_bug.lean @@ -0,0 +1,7 @@ +import logic + +theorem test {A B : Type} {a : A} {b : B} (H : a == b) : + eq.rec_on (heq.type_eq H) a = b +:= +-- Remark the error message should not occur in the token theorem +heq.rec_on H rfl diff --git a/tests/lean/unifier_bug.lean.expected.out b/tests/lean/unifier_bug.lean.expected.out new file mode 100644 index 000000000..58fd36010 --- /dev/null +++ b/tests/lean/unifier_bug.lean.expected.out @@ -0,0 +1,8 @@ +unifier_bug.lean:7:0: error: type mismatch at application + heq.rec_on H rfl +term + rfl +has type + eq.rec_on (heq.type_eq H) a = eq.rec_on (heq.type_eq H) a +but is expected to have type + eq.rec_on (heq.type_eq H) a = b