michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/elaborator): only expand definitions that are not marked as hidden

Browse source 
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 <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-20 02:16:41 -08:00
parent cb48fbf3c4
commit 812c1a2960
8 changed files with 101 additions and 100 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/library/elaborator/elaborator.cpp
View file

@ -19,6 +19,7 @@ Author: Leonardo de Moura
#include "kernel/replace_fn.h" #include "kernel/replace_fn.h"
#include "kernel/builtin.h" #include "kernel/builtin.h"
#include "kernel/update_expr.h" #include "kernel/update_expr.h"
#include "library/hidden_defs.h"
#include "library/type_inferer.h" #include "library/type_inferer.h"
#include "library/elaborator/elaborator.h" #include "library/elaborator/elaborator.h"
#include "library/elaborator/elaborator_justification.h" #include "library/elaborator/elaborator_justification.h"
@ -626,7 +627,7 @@ class elaborator::imp {
int get_const_weight(expr const & a) { int get_const_weight(expr const & a) {
lean_assert(is_constant(a)); lean_assert(is_constant(a));
optional<object> obj = m_env->find_object(const_name(a)); optional<object> 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(); return obj->get_weight();
else else
return -1; return -1;

2
src/library/hidden_defs.cpp
View file

@ -63,7 +63,7 @@ void set_hidden_flag(environment const & env, name const & d, bool flag) {
void hide_builtin(environment const & env) { void hide_builtin(environment const & env) {
for (auto c : { mk_implies_fn(), mk_iff_fn(), mk_not_fn(), mk_or_fn(), mk_and_fn(), 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)); set_hidden_flag(env, const_name(c));
} }

173
tests/lean/elab1.lean.expected.out
View file

@ -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: b
Assumed: H Assumed: H
Failed to solve Failed to solve
⊢ if ?M::0 (if (if ?M::3 (if a ⊥ ⊤) ⊤) ⊥ ⊤) ⊤ ≺ b ⊢ ?M::0 ⇒ ?M::3 ∧ a ≺ b
Normalize Substitution
⊢ if ?M::0 (?M::3 ∧ a) ⊤ ≺ b ⊢ ?M::0 ⇒ ?M::1 ≺ b
Substitution (line: 20: pos: 18) Type of definition 't1' must be convertible to expected type.
⊢ if ?M::0 ?M::1 ⊤ ≺ b Assignment
Normalize H1 : ?M::2 ⊢ ?M::3 ∧ a ≺ ?M::1
⊢ ?M::0 ⇒ ?M::1 ≺ b Substitution
(line: 20: pos: 18) Type of definition 't1' must be convertible to expected type. H1 : ?M::2 ⊢ ?M::3 ∧ ?M::4 ≺ ?M::1
Assignment Destruct/Decompose
H1 : ?M::2 ⊢ ?M::3 ∧ a ≺ ?M::1 ⊢ Π H1 : ?M::2, ?M::3 ∧ ?M::4 ≺ Π a : ?M::0, ?M::1
Substitution (line: 20: pos: 18) Type of argument 3 must be convertible to the expected type in the application of
H1 : ?M::2 ⊢ ?M::3 ∧ ?M::4 ≺ ?M::1 Discharge::explicit
Destruct/Decompose with arguments:
⊢ Π H1 : ?M::2, ?M::3 ∧ ?M::4 ≺ Π a : ?M::0, ?M::1 ?M::0
(line: 20: pos: 18) Type of argument 3 must be convertible to the expected type in the application of ?M::1
Discharge::explicit λ 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: with arguments:
?M::0 ?M::3
?M::1 ?M::4
λ H1 : ?M::2, Conj H1 (Conjunct1 H) H1
Assignment Conjunct1 H
H1 : ?M::2 ⊢ a ≺ ?M::4 Assignment
Substitution H1 : ?M::2 ⊢ a ≈ ?M::5
H1 : ?M::2 ⊢ ?M::5 ≺ ?M::4 Destruct/Decompose
(line: 20: pos: 37) Type of argument 4 must be convertible to the expected type in the application of H1 : ?M::2 ⊢ a ∧ b ≺ ?M::5 ∧ ?M::6
Conj::explicit (line: 20: pos: 45) Type of argument 3 must be convertible to the expected type in the application of
with arguments: Conjunct1::explicit
?M::3 with arguments:
?M::4 ?M::5
H1 ?M::6
Conjunct1 H 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 Failed to solve
⊢ b ≈ a ⊢ b ≈ a
Substitution Substitution
@ -342,50 +338,26 @@ Failed to solve
⊢ ?M::1 ≈ Bool ⊢ ?M::1 ≈ Bool
Assumption 6 Assumption 6
Failed to solve Failed to solve
a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ if (if a b ⊤) a ⊤ ≺ a a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ (a ⇒ b) ⇒ a ≺ a
Normalize Substitution
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 ≺ ?M::5[lift:0:1]
Substitution Substitution
a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ (a ⇒ b) ⇒ a ≺ ?M::5[lift:0:1] a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ ?M::2[lift:0:2] ≺ ?M::5[lift:0:1]
Substitution Destruct/Decompose
a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ ?M::2[lift:0:2] ≺ ?M::5[lift:0:1] a : Bool, b : Bool, H : ?M::2 ⊢ Π H_a : ?M::6, ?M::2[lift:0:2] ≺ Π a : ?M::3, ?M::5[lift:0:1]
Destruct/Decompose (line: 27: pos: 21) Type of argument 5 must be convertible to the expected type in the application of
a : Bool, b : Bool, H : ?M::2 ⊢ Π H_a : ?M::6, ?M::2[lift:0:2] ≺ Π a : ?M::3, ?M::5[lift:0:1] DisjCases::explicit
(line: 27: pos: 21) Type of argument 5 must be convertible to the expected type in the application of with arguments:
DisjCases::explicit ?M::3
with arguments: ?M::4
?M::3 ?M::5
?M::4 EM a
?M::5 λ H_a : ?M::6, H
EM a λ H_na : ?M::7, NotImp1 (MT H H_na)
λ H_a : ?M::6, H Normalize assignment
λ H_na : ?M::7, NotImp1 (MT H H_na) ?M::0
Normalize assignment Assignment
?M::0 a : Bool, b : Bool ⊢ ?M::2 ≈ ?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]
Destruct/Decompose Destruct/Decompose
a : Bool, b : Bool ⊢ Π H : ?M::2, ?M::5 ≺ Π a : ?M::0, ?M::1[lift:0:1] 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 (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::0
?M::1 ?M::1
λ H : ?M::2, DisjCases (EM a) (λ H_a : ?M::6, H) (λ H_na : ?M::7, NotImp1 (MT H H_na)) λ H : ?M::2, DisjCases (EM a) (λ H_a : ?M::6, H) (λ H_na : ?M::7, NotImp1 (MT H H_na))
Assignment Assignment
a : Bool, b : Bool ⊢ ?M::1 ≈ a 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 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 Destruct/Decompose
a : Bool ⊢ Π b : Bool, ?M::0 ⇒ ?M::1 ≺ Π b : Bool, ((a ⇒ b) ⇒ a) ⇒ a ⊢ Π a b : Bool, ?M::0 ⇒ ?M::1 ≺ Π a b : Bool, ((a ⇒ b) ⇒ a) ⇒ a
Destruct/Decompose (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 Assignment
(line: 26: pos: 16) Type of definition 'pierce' must be convertible to expected type. 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.

2
tests/lean/elab6.lean
View file

@ -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))

2
tests/lean/exists4.lean.expected.out
View file

@ -17,7 +17,7 @@ Theorem T1 : ∃ x y z : N, P x y z :=
a a
(ExistsIntro::explicit (ExistsIntro::explicit
N 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 b
(ExistsIntro::explicit N (λ z : N, P a b z) c H3)) (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)) Theorem T2 : ∃ x y z : N, P x y z := ExistsIntro a (ExistsIntro b (ExistsIntro c H3))

9
tests/lean/interactive/elab6.lean Normal file
View file

@ -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))

2
tests/lean/elab6.lean.expected.out → tests/lean/interactive/elab6.lean.expected.out
View file

@ -1,3 +1,3 @@
Set: pp::colors # Set: pp::colors
Set: pp::unicode Set: pp::unicode
Proved: ForallIntro2 Proved: ForallIntro2

8
tests/lean/tst6.lean.expected.out
View file

@ -84,8 +84,8 @@ Theorem Example2 (a b c d : N)
a a
b b
c c
(Conjunct1::explicit (a == b) (b == c) H1) (Conjunct1::explicit (a == b) (eq::explicit N b c) H1)
(Conjunct2::explicit (a == b) (b == c) H1)) (Conjunct2::explicit (eq::explicit N a b) (b == c) H1))
(Refl::explicit N b)) (Refl::explicit N b))
(λ H1 : eq::explicit N a d ∧ eq::explicit N d c, (λ H1 : eq::explicit N a d ∧ eq::explicit N d c,
CongrH::explicit CongrH::explicit
@ -98,8 +98,8 @@ Theorem Example2 (a b c d : N)
a a
d d
c c
(Conjunct1::explicit (a == d) (d == c) H1) (Conjunct1::explicit (a == d) (eq::explicit N d c) H1)
(Conjunct2::explicit (a == d) (d == c) H1)) (Conjunct2::explicit (eq::explicit N a d) (d == c) H1))
(Refl::explicit N b)) (Refl::explicit N b))
Proved: Example3 Proved: Example3
Set: lean::pp::implicit Set: lean::pp::implicit