From 812c1a296030ae623800d1d6d721f55dc7b0b77a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 20 Dec 2013 02:16:41 -0800 Subject: [PATCH] feat(library/elaborator): only expand definitions that are not marked as hidden MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The elaborator produces better proof terms. This is particularly important when we have to prove the remaining holes using tactics. For example, in one of the tests, the elaborator was producing the sub-expression (λ x : N, if ((λ x::1 : N, if (P a x x::1) ⊥ ⊤) == (λ x : N, ⊤)) ⊥ ⊤) After, this commit it produces (λ x : N, ¬ ∀ x::1 : N, ¬ P a x x::1) The expressions above are definitionally equal, but the second is easier to work with. Question: do we really need hidden definitions? Perhaps, we can use only the opaque flag. Signed-off-by: Leonardo de Moura --- src/library/elaborator/elaborator.cpp | 3 +- src/library/hidden_defs.cpp | 2 +- tests/lean/elab1.lean.expected.out | 173 +++++++++--------- tests/lean/elab6.lean | 2 - tests/lean/exists4.lean.expected.out | 2 +- tests/lean/interactive/elab6.lean | 9 + .../{ => interactive}/elab6.lean.expected.out | 2 +- tests/lean/tst6.lean.expected.out | 8 +- 8 files changed, 101 insertions(+), 100 deletions(-) delete mode 100644 tests/lean/elab6.lean create mode 100644 tests/lean/interactive/elab6.lean rename tests/lean/{ => interactive}/elab6.lean.expected.out (67%) diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 6d6b9be37..4efea6f37 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -19,6 +19,7 @@ Author: Leonardo de Moura #include "kernel/replace_fn.h" #include "kernel/builtin.h" #include "kernel/update_expr.h" +#include "library/hidden_defs.h" #include "library/type_inferer.h" #include "library/elaborator/elaborator.h" #include "library/elaborator/elaborator_justification.h" @@ -626,7 +627,7 @@ class elaborator::imp { int get_const_weight(expr const & a) { lean_assert(is_constant(a)); optional obj = m_env->find_object(const_name(a)); - if (obj && obj->is_definition() && !obj->is_opaque()) + if (obj && obj->is_definition() && !obj->is_opaque() && !is_hidden(m_env, const_name(a))) return obj->get_weight(); else return -1; diff --git a/src/library/hidden_defs.cpp b/src/library/hidden_defs.cpp index 1ddeb1913..28180f9fe 100644 --- a/src/library/hidden_defs.cpp +++ b/src/library/hidden_defs.cpp @@ -63,7 +63,7 @@ void set_hidden_flag(environment const & env, name const & d, bool flag) { void hide_builtin(environment const & env) { for (auto c : { mk_implies_fn(), mk_iff_fn(), mk_not_fn(), mk_or_fn(), mk_and_fn(), - mk_forall_fn(), mk_exists_fn(), mk_homo_eq_fn() }) + mk_forall_fn() }) set_hidden_flag(env, const_name(c)); } diff --git a/tests/lean/elab1.lean.expected.out b/tests/lean/elab1.lean.expected.out index e25f66c26..8226bf04c 100644 --- a/tests/lean/elab1.lean.expected.out +++ b/tests/lean/elab1.lean.expected.out @@ -130,47 +130,43 @@ A : Type, B : Type, a : ?M::0, b : ?M::1, C : Type ⊢ ?M::0[lift:0:3] ≺ C Assumed: b Assumed: H Failed to solve - ⊢ if ?M::0 (if (if ?M::3 (if a ⊥ ⊤) ⊤) ⊥ ⊤) ⊤ ≺ b - Normalize - ⊢ if ?M::0 (?M::3 ∧ a) ⊤ ≺ b - Substitution - ⊢ if ?M::0 ?M::1 ⊤ ≺ b - Normalize - ⊢ ?M::0 ⇒ ?M::1 ≺ b - (line: 20: pos: 18) Type of definition 't1' must be convertible to expected type. - Assignment - H1 : ?M::2 ⊢ ?M::3 ∧ a ≺ ?M::1 - Substitution - H1 : ?M::2 ⊢ ?M::3 ∧ ?M::4 ≺ ?M::1 - Destruct/Decompose - ⊢ Π H1 : ?M::2, ?M::3 ∧ ?M::4 ≺ Π a : ?M::0, ?M::1 - (line: 20: pos: 18) Type of argument 3 must be convertible to the expected type in the application of - Discharge::explicit + ⊢ ?M::0 ⇒ ?M::3 ∧ a ≺ b + Substitution + ⊢ ?M::0 ⇒ ?M::1 ≺ b + (line: 20: pos: 18) Type of definition 't1' must be convertible to expected type. + Assignment + H1 : ?M::2 ⊢ ?M::3 ∧ a ≺ ?M::1 + Substitution + H1 : ?M::2 ⊢ ?M::3 ∧ ?M::4 ≺ ?M::1 + Destruct/Decompose + ⊢ Π H1 : ?M::2, ?M::3 ∧ ?M::4 ≺ Π a : ?M::0, ?M::1 + (line: 20: pos: 18) Type of argument 3 must be convertible to the expected type in the application of + Discharge::explicit + with arguments: + ?M::0 + ?M::1 + λ H1 : ?M::2, Conj H1 (Conjunct1 H) + Assignment + H1 : ?M::2 ⊢ a ≺ ?M::4 + Substitution + H1 : ?M::2 ⊢ ?M::5 ≺ ?M::4 + (line: 20: pos: 37) Type of argument 4 must be convertible to the expected type in the application of + Conj::explicit with arguments: - ?M::0 - ?M::1 - λ H1 : ?M::2, Conj H1 (Conjunct1 H) - Assignment - H1 : ?M::2 ⊢ a ≺ ?M::4 - Substitution - H1 : ?M::2 ⊢ ?M::5 ≺ ?M::4 - (line: 20: pos: 37) Type of argument 4 must be convertible to the expected type in the application of - Conj::explicit - with arguments: - ?M::3 - ?M::4 - H1 - Conjunct1 H - Assignment - H1 : ?M::2 ⊢ a ≈ ?M::5 - Destruct/Decompose - H1 : ?M::2 ⊢ a ∧ b ≺ ?M::5 ∧ ?M::6 - (line: 20: pos: 45) Type of argument 3 must be convertible to the expected type in the application of - Conjunct1::explicit - with arguments: - ?M::5 - ?M::6 - H + ?M::3 + ?M::4 + H1 + Conjunct1 H + Assignment + H1 : ?M::2 ⊢ a ≈ ?M::5 + Destruct/Decompose + H1 : ?M::2 ⊢ a ∧ b ≺ ?M::5 ∧ ?M::6 + (line: 20: pos: 45) Type of argument 3 must be convertible to the expected type in the application of + Conjunct1::explicit + with arguments: + ?M::5 + ?M::6 + H Failed to solve ⊢ b ≈ a Substitution @@ -342,50 +338,26 @@ Failed to solve ⊢ ?M::1 ≈ Bool Assumption 6 Failed to solve -a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ if (if a b ⊤) a ⊤ ≺ a - Normalize - a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ (a ⇒ b) ⇒ a ≺ a +a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ (a ⇒ b) ⇒ a ≺ a + Substitution + a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ (a ⇒ b) ⇒ a ≺ ?M::5[lift:0:1] Substitution - a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ (a ⇒ b) ⇒ a ≺ ?M::5[lift:0:1] - Substitution - a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ ?M::2[lift:0:2] ≺ ?M::5[lift:0:1] - Destruct/Decompose - a : Bool, b : Bool, H : ?M::2 ⊢ Π H_a : ?M::6, ?M::2[lift:0:2] ≺ Π a : ?M::3, ?M::5[lift:0:1] - (line: 27: pos: 21) Type of argument 5 must be convertible to the expected type in the application of - DisjCases::explicit - with arguments: - ?M::3 - ?M::4 - ?M::5 - EM a - λ H_a : ?M::6, H - λ H_na : ?M::7, NotImp1 (MT H H_na) - Normalize assignment - ?M::0 - Assignment - a : Bool, b : Bool ⊢ ?M::2 ≈ ?M::0 - Destruct/Decompose - a : Bool, b : Bool ⊢ Π H : ?M::2, ?M::5 ≺ Π a : ?M::0, ?M::1[lift:0:1] - (line: 27: pos: 4) Type of argument 3 must be convertible to the expected type in the application of - Discharge::explicit - with arguments: - ?M::0 - ?M::1 - λ H : ?M::2, - DisjCases (EM a) (λ H_a : ?M::6, H) (λ H_na : ?M::7, NotImp1 (MT H H_na)) - Assignment - a : Bool, b : Bool ⊢ ?M::0 ≈ (a ⇒ b) ⇒ a - Destruct/Decompose - a : Bool, b : Bool ⊢ ?M::0 ⇒ ?M::1 ≺ ((a ⇒ b) ⇒ a) ⇒ a - Destruct/Decompose - a : Bool ⊢ Π b : Bool, ?M::0 ⇒ ?M::1 ≺ Π b : Bool, ((a ⇒ b) ⇒ a) ⇒ a - Destruct/Decompose - ⊢ Π a b : Bool, ?M::0 ⇒ ?M::1 ≺ Π a b : Bool, ((a ⇒ b) ⇒ a) ⇒ a - (line: 26: pos: 16) Type of definition 'pierce' must be convertible to expected type. - Assignment - a : Bool, b : Bool, H : ?M::2 ⊢ ?M::5 ≺ a - Substitution - a : Bool, b : Bool, H : ?M::2 ⊢ ?M::5 ≺ ?M::1[lift:0:1] + a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ ?M::2[lift:0:2] ≺ ?M::5[lift:0:1] + Destruct/Decompose + a : Bool, b : Bool, H : ?M::2 ⊢ Π H_a : ?M::6, ?M::2[lift:0:2] ≺ Π a : ?M::3, ?M::5[lift:0:1] + (line: 27: pos: 21) Type of argument 5 must be convertible to the expected type in the application of + DisjCases::explicit + with arguments: + ?M::3 + ?M::4 + ?M::5 + EM a + λ H_a : ?M::6, H + λ H_na : ?M::7, NotImp1 (MT H H_na) + Normalize assignment + ?M::0 + Assignment + a : Bool, b : Bool ⊢ ?M::2 ≈ ?M::0 Destruct/Decompose a : Bool, b : Bool ⊢ Π H : ?M::2, ?M::5 ≺ Π a : ?M::0, ?M::1[lift:0:1] (line: 27: pos: 4) Type of argument 3 must be convertible to the expected type in the application of @@ -394,12 +366,33 @@ a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ if (if a b ⊤) a ⊤ ≺ a ?M::0 ?M::1 λ H : ?M::2, DisjCases (EM a) (λ H_a : ?M::6, H) (λ H_na : ?M::7, NotImp1 (MT H H_na)) - Assignment - a : Bool, b : Bool ⊢ ?M::1 ≈ a + Assignment + a : Bool, b : Bool ⊢ ?M::0 ≈ (a ⇒ b) ⇒ a + Destruct/Decompose + a : Bool, b : Bool ⊢ ?M::0 ⇒ ?M::1 ≺ ((a ⇒ b) ⇒ a) ⇒ a Destruct/Decompose - a : Bool, b : Bool ⊢ ?M::0 ⇒ ?M::1 ≺ ((a ⇒ b) ⇒ a) ⇒ a + a : Bool ⊢ Π b : Bool, ?M::0 ⇒ ?M::1 ≺ Π b : Bool, ((a ⇒ b) ⇒ a) ⇒ a Destruct/Decompose - a : Bool ⊢ Π b : Bool, ?M::0 ⇒ ?M::1 ≺ Π b : Bool, ((a ⇒ b) ⇒ a) ⇒ a - Destruct/Decompose - ⊢ Π a b : Bool, ?M::0 ⇒ ?M::1 ≺ Π a b : Bool, ((a ⇒ b) ⇒ a) ⇒ a - (line: 26: pos: 16) Type of definition 'pierce' must be convertible to expected type. + ⊢ Π a b : Bool, ?M::0 ⇒ ?M::1 ≺ Π a b : Bool, ((a ⇒ b) ⇒ a) ⇒ a + (line: 26: pos: 16) Type of definition 'pierce' must be convertible to expected type. + Assignment + a : Bool, b : Bool, H : ?M::2 ⊢ ?M::5 ≺ a + Substitution + a : Bool, b : Bool, H : ?M::2 ⊢ ?M::5 ≺ ?M::1[lift:0:1] + Destruct/Decompose + a : Bool, b : Bool ⊢ Π H : ?M::2, ?M::5 ≺ Π a : ?M::0, ?M::1[lift:0:1] + (line: 27: pos: 4) Type of argument 3 must be convertible to the expected type in the application of + Discharge::explicit + with arguments: + ?M::0 + ?M::1 + λ H : ?M::2, DisjCases (EM a) (λ H_a : ?M::6, H) (λ H_na : ?M::7, NotImp1 (MT H H_na)) + Assignment + a : Bool, b : Bool ⊢ ?M::1 ≈ a + Destruct/Decompose + a : Bool, b : Bool ⊢ ?M::0 ⇒ ?M::1 ≺ ((a ⇒ b) ⇒ a) ⇒ a + Destruct/Decompose + a : Bool ⊢ Π b : Bool, ?M::0 ⇒ ?M::1 ≺ Π b : Bool, ((a ⇒ b) ⇒ a) ⇒ a + Destruct/Decompose + ⊢ Π a b : Bool, ?M::0 ⇒ ?M::1 ≺ Π a b : Bool, ((a ⇒ b) ⇒ a) ⇒ a + (line: 26: pos: 16) Type of definition 'pierce' must be convertible to expected type. diff --git a/tests/lean/elab6.lean b/tests/lean/elab6.lean deleted file mode 100644 index be1ea8590..000000000 --- a/tests/lean/elab6.lean +++ /dev/null @@ -1,2 +0,0 @@ -Theorem ForallIntro2 (A : (Type U)) (P : A -> Bool) (H : Pi x, P x) : forall x, P x := - Abst (fun x, EqTIntro (H x)) diff --git a/tests/lean/exists4.lean.expected.out b/tests/lean/exists4.lean.expected.out index 34137fd9b..d1b65d6aa 100644 --- a/tests/lean/exists4.lean.expected.out +++ b/tests/lean/exists4.lean.expected.out @@ -17,7 +17,7 @@ Theorem T1 : ∃ x y z : N, P x y z := a (ExistsIntro::explicit N - (λ x : N, if ((λ x::1 : N, if (P a x x::1) ⊥ ⊤) == (λ x : N, ⊤)) ⊥ ⊤) + (λ x : N, ¬ ∀ x::1 : N, ¬ P a x x::1) b (ExistsIntro::explicit N (λ z : N, P a b z) c H3)) Theorem T2 : ∃ x y z : N, P x y z := ExistsIntro a (ExistsIntro b (ExistsIntro c H3)) diff --git a/tests/lean/interactive/elab6.lean b/tests/lean/interactive/elab6.lean new file mode 100644 index 000000000..9cf23fdbd --- /dev/null +++ b/tests/lean/interactive/elab6.lean @@ -0,0 +1,9 @@ +(** +-- The elaborator does not expand definitions marked as 'hidden'. +-- To be able to prove the following theorem, we have to unmark the +-- 'forall' +local env = get_environment() +set_hidden_flag(env, "forall", false) +**) +Theorem ForallIntro2 (A : (Type U)) (P : A -> Bool) (H : Pi x, P x) : forall x, P x := + Abst (fun x, EqTIntro (H x)) diff --git a/tests/lean/elab6.lean.expected.out b/tests/lean/interactive/elab6.lean.expected.out similarity index 67% rename from tests/lean/elab6.lean.expected.out rename to tests/lean/interactive/elab6.lean.expected.out index 0049320f0..0ff7de0f8 100644 --- a/tests/lean/elab6.lean.expected.out +++ b/tests/lean/interactive/elab6.lean.expected.out @@ -1,3 +1,3 @@ - Set: pp::colors +# Set: pp::colors Set: pp::unicode Proved: ForallIntro2 diff --git a/tests/lean/tst6.lean.expected.out b/tests/lean/tst6.lean.expected.out index a740b7192..618943f90 100644 --- a/tests/lean/tst6.lean.expected.out +++ b/tests/lean/tst6.lean.expected.out @@ -84,8 +84,8 @@ Theorem Example2 (a b c d : N) a b c - (Conjunct1::explicit (a == b) (b == c) H1) - (Conjunct2::explicit (a == b) (b == c) H1)) + (Conjunct1::explicit (a == b) (eq::explicit N b c) H1) + (Conjunct2::explicit (eq::explicit N a b) (b == c) H1)) (Refl::explicit N b)) (λ H1 : eq::explicit N a d ∧ eq::explicit N d c, CongrH::explicit @@ -98,8 +98,8 @@ Theorem Example2 (a b c d : N) a d c - (Conjunct1::explicit (a == d) (d == c) H1) - (Conjunct2::explicit (a == d) (d == c) H1)) + (Conjunct1::explicit (a == d) (eq::explicit N d c) H1) + (Conjunct2::explicit (eq::explicit N a d) (d == c) H1)) (Refl::explicit N b)) Proved: Example3 Set: lean::pp::implicit