feat(library/elaborator): compensate the lack of eta-reduction (and eta-expanded normal forms) in the kernel normalizer
Before this commit, the elaborator was solving constraints of the form
ctx |- (?m x) == (f x)
as
?m <- (fun x : A, f x) where A is the domain of f.
In our kernel, the terms f and (fun x, f x) are not definitionally equal.
So, the solution above is not the only one. Another possible solution is
?m <- f
Depending of the circumstances we want ?m <- (fun x : A, f x) OR ?m <- f.
For example, when Lean is elaborating the eta-theorem in kernel.lean, the first solution should be used:
?m <- (fun x : A, f x)
When we are elaborating the axiom_of_choice theorem, we need to use the second one:
?m <- f
Of course, we can always provide the parameters explicitly and bypass the elaborator.
However, this goes against the idea that the elaborator can do mechanical steps for us.
This commit addresses this issue by creating a case-split
?m <- (fun x : A, f x)
OR
?m <- f
Another solution is to implement eta-expanded normal forms in the Kernel.
With this change, we were able to cleanup the following "hacks" in kernel.lean:
@eps_ax A (nonempty_ex_intro H) P w Hw
@axiom_of_choice A B P H
where we had to explicitly provided the implicit arguments
This commit also improves the imitation step for Pi-terms that are actually arrows.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
6cb4d165c9
commit
8214c7add4
8 changed files with 142 additions and 48 deletions
|
|
@ -216,7 +216,7 @@ theorem nonempty_ex_intro {A : TypeU} {P : A → Bool} (H : ∃ x, P x) : nonemp
|
|||
|
||||
theorem exists_to_eps {A : TypeU} {P : A → Bool} (H : ∃ x, P x) : P (ε (nonempty_ex_intro H) P)
|
||||
:= obtain (w : A) (Hw : P w), from H,
|
||||
@eps_ax A (nonempty_ex_intro H) P w Hw
|
||||
eps_ax (nonempty_ex_intro H) w Hw
|
||||
|
||||
theorem axiom_of_choice {A : TypeU} {B : A → TypeU} {R : ∀ x : A, B x → Bool} (H : ∀ x, ∃ y, R x y) : ∃ f, ∀ x, R x (f x)
|
||||
:= exists_intro
|
||||
|
|
@ -238,8 +238,7 @@ theorem iff_intro {a b : Bool} (Hab : a → b) (Hba : b → a) : a ↔ b
|
|||
theorem skolem_th {A : TypeU} {B : A → TypeU} {P : ∀ x : A, B x → Bool} :
|
||||
(∀ x, ∃ y, P x y) ↔ ∃ f, (∀ x, P x (f x))
|
||||
:= iff_intro
|
||||
(λ H : (∀ x, ∃ y, P x y),
|
||||
@axiom_of_choice A B P H)
|
||||
(λ H : (∀ x, ∃ y, P x y), axiom_of_choice H)
|
||||
(λ H : (∃ f, (∀ x, P x (f x))),
|
||||
take x, obtain (fw : ∀ x, B x) (Hw : ∀ x, P x (fw x)), from H,
|
||||
exists_intro (fw x) (Hw x))
|
||||
|
|
|
|||
Binary file not shown.
Binary file not shown.
Binary file not shown.
|
|
@ -305,13 +305,13 @@ class elaborator::imp {
|
|||
}
|
||||
|
||||
/**
|
||||
\brief Return (f x_{num_vars - 1} ... x_0)
|
||||
\brief Return (f x_{num_vars + first - 1} ... x_first)
|
||||
*/
|
||||
expr mk_app_vars(expr const & f, unsigned num_vars) {
|
||||
expr mk_app_vars(expr const & f, unsigned num_vars, unsigned first = 0) {
|
||||
buffer<expr> args;
|
||||
args.push_back(f);
|
||||
unsigned i = num_vars;
|
||||
while (i > 0) {
|
||||
unsigned i = num_vars + first;
|
||||
while (i > first) {
|
||||
--i;
|
||||
args.push_back(mk_var(i));
|
||||
}
|
||||
|
|
@ -703,21 +703,6 @@ class elaborator::imp {
|
|||
return e && e->get_body();
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Return true iff all arguments of the application \c a are variables that do
|
||||
not have a definition in \c ctx.
|
||||
*/
|
||||
static bool are_args_vars(context const & ctx, expr const & a) {
|
||||
lean_assert(is_app(a));
|
||||
for (unsigned i = 1; i < num_args(a); i++) {
|
||||
if (!is_var(arg(a, i)))
|
||||
return false;
|
||||
if (has_body(ctx, var_idx(arg(a, i))))
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Return true iff \c a may be an actual lower bound for a convertibility constraint.
|
||||
That is, if the result is false, it means the convertability constraint is essentially
|
||||
|
|
@ -736,14 +721,6 @@ class elaborator::imp {
|
|||
return is_type(a) || is_metavar(a) || (is_pi(a) && is_actual_upper(abst_body(a)));
|
||||
}
|
||||
|
||||
/**
|
||||
\brief See \c process_simple_ho_match
|
||||
*/
|
||||
bool is_simple_ho_match(context const & ctx, expr const & a, expr const & b, bool is_lhs, unification_constraint const & c) {
|
||||
return is_meta_app(a) && !has_local_context(arg(a, 0)) && are_args_vars(ctx, a) && closed(b) &&
|
||||
(is_eq(c) || (is_lhs && !is_actual_upper(b)) || (!is_lhs && !is_actual_lower(b)));
|
||||
}
|
||||
|
||||
optional<expr> try_get_type(context const & ctx, expr const & e) {
|
||||
try {
|
||||
return some_expr(m_type_inferer(e, ctx));
|
||||
|
|
@ -752,17 +729,105 @@ class elaborator::imp {
|
|||
}
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Return true iff all arguments of the application \c a are variables that do
|
||||
not have a definition in \c ctx.
|
||||
*/
|
||||
static bool are_args_vars(context const & ctx, expr const & a) {
|
||||
lean_assert(is_app(a));
|
||||
for (unsigned i = 1; i < num_args(a); i++) {
|
||||
if (!is_var(arg(a, i)))
|
||||
return false;
|
||||
if (has_body(ctx, var_idx(arg(a, i))))
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief are_args_vars(a) && all variables are distinct
|
||||
*/
|
||||
static bool are_args_distinct_vars(context const & ctx, expr const & a) {
|
||||
if (!are_args_vars(ctx, a))
|
||||
return false;
|
||||
buffer<bool> found;
|
||||
for (unsigned i = 1; i < num_args(a); i++) {
|
||||
unsigned vidx = var_idx(arg(a, i));
|
||||
if (vidx >= found.size())
|
||||
found.resize(vidx+1, false);
|
||||
if (found[vidx])
|
||||
return false;
|
||||
found[vidx] = true;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief See \c process_simple_ho_match (case 1)
|
||||
*/
|
||||
bool is_simple_ho_match_closed(context const & ctx, expr const & a, expr const & b, bool is_lhs, unification_constraint const & c) {
|
||||
return is_meta_app(a) && are_args_vars(ctx, a) && closed(b) &&
|
||||
(is_eq(c) || (is_lhs && !is_actual_upper(b)) || (!is_lhs && !is_actual_lower(b)));
|
||||
}
|
||||
|
||||
/**
|
||||
\brief See \c process_simple_ho_match (case 2)
|
||||
*/
|
||||
bool is_simple_ho_match_app(context const & ctx, expr const & a, expr const & b, bool is_lhs, unification_constraint const & c) {
|
||||
if (is_meta_app(a) && are_args_distinct_vars(ctx, a) && is_app(b) && !is_meta_app(b) &&
|
||||
num_args(a) == num_args(b) &&
|
||||
(is_eq(c) || (is_lhs && !is_actual_upper(b)) || (!is_lhs && !is_actual_lower(b)))) {
|
||||
// check if a and b have the same arguments
|
||||
for (unsigned i = 1; i < num_args(a); i++) {
|
||||
if (arg(a, i) != arg(b, i))
|
||||
return false;
|
||||
}
|
||||
// a is of the form (?m x1 ... xn) AND b is of the form (f x1 ... xn)
|
||||
// f should not contain any xi
|
||||
bool failed = false;
|
||||
for_each(arg(b, 0), [&](expr const & e, unsigned offset) {
|
||||
if (failed)
|
||||
return false; // abort search
|
||||
if (is_var(e)) {
|
||||
unsigned vidx = var_idx(e);
|
||||
if (vidx >= offset) {
|
||||
vidx -= offset;
|
||||
for (unsigned i = 1; i < num_args(a); i++) {
|
||||
if (var_idx(arg(a, i)) == vidx) {
|
||||
failed = true;
|
||||
return false;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
return true; // continue search
|
||||
});
|
||||
return !failed;
|
||||
} else {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Return true iff ctx |- a == b is a "simple" higher-order matching constraint. By simple, we mean
|
||||
a constraint of the form
|
||||
ctx |- (?m x) == c
|
||||
The constraint is solved by assigning ?m to (fun (x : T), c).
|
||||
|
||||
1) a constraint of the form
|
||||
ctx |- (?m x1 ... xn) == c where c is closed
|
||||
The constraint is solved by assigning ?m to (fun x1 ... xn, c).
|
||||
The arguments may contain duplicate occurrences of variables.
|
||||
|
||||
|
||||
2) a constraint of the form
|
||||
ctx |- (?m x1 ... xn) == (f x1 ... xn) where f does not contain x1 ... xn, and x1 ... xn are distinct
|
||||
The constraint is solved by assigning ?m to f OR ?m to (fun x1 ... xn, f x1 ... xn)
|
||||
*/
|
||||
bool process_simple_ho_match(context const & ctx, expr const & a, expr const & b, bool is_lhs, unification_constraint const & c) {
|
||||
// Solve constraint of the form
|
||||
// ctx |- (?m x) == c
|
||||
// using imitation
|
||||
if (is_simple_ho_match(ctx, a, b, is_lhs, c)) {
|
||||
bool eq_closed = is_simple_ho_match_closed(ctx, a, b, is_lhs, c);
|
||||
bool eq_app = is_simple_ho_match_app(ctx, a, b, is_lhs, c);
|
||||
if (eq_closed || eq_app) {
|
||||
expr m = arg(a, 0);
|
||||
buffer<expr> types;
|
||||
for (unsigned i = 1; i < num_args(a); i++) {
|
||||
|
|
@ -772,12 +837,37 @@ class elaborator::imp {
|
|||
else
|
||||
return false;
|
||||
}
|
||||
justification new_jst(new destruct_justification(c));
|
||||
expr s = mk_lambda(types, b);
|
||||
if (!is_lhs)
|
||||
swap(m, s);
|
||||
push_new_eq_constraint(ctx, m, s, new_jst);
|
||||
return true;
|
||||
if (eq_closed) {
|
||||
justification new_jst(new destruct_justification(c));
|
||||
expr s = mk_lambda(types, b);
|
||||
push_new_eq_constraint(ctx, m, s, new_jst);
|
||||
return true;
|
||||
} else {
|
||||
lean_assert(eq_app);
|
||||
expr f = arg(b, 0);
|
||||
std::unique_ptr<generic_case_split> new_cs(new generic_case_split(c, m_state));
|
||||
{
|
||||
// eta-expanded version: m = fun x1 ... xn, f x1 ... xn
|
||||
unsigned n = types.size();
|
||||
expr s = mk_lambda(types, mk_app_vars(lift_free_vars(f, 0, n), n));
|
||||
state new_state(m_state);
|
||||
justification new_assumption = mk_assumption();
|
||||
push_new_eq_constraint(new_state.m_active_cnstrs, ctx, m, s, new_assumption);
|
||||
new_cs->push_back(new_state, new_assumption);
|
||||
}
|
||||
{
|
||||
// m = f
|
||||
state new_state(m_state);
|
||||
justification new_assumption = mk_assumption();
|
||||
push_new_eq_constraint(new_state.m_active_cnstrs, ctx, m, f, new_assumption);
|
||||
new_cs->push_back(new_state, new_assumption);
|
||||
}
|
||||
// add case split
|
||||
bool r = new_cs->next(*this);
|
||||
lean_assert(r);
|
||||
m_case_splits.push_back(std::move(new_cs));
|
||||
return r;
|
||||
}
|
||||
} else {
|
||||
return false;
|
||||
}
|
||||
|
|
@ -843,9 +933,15 @@ class elaborator::imp {
|
|||
context new_ctx = extend(ctx, abst_name(b), abst_domain(b));
|
||||
expr h_2 = new_state.m_menv->mk_metavar(extend(ctx, abst_name(b), abst_domain(b)));
|
||||
push_new_eq_constraint(new_state.m_active_cnstrs, ctx, update_app(a, 0, h_1), abst_domain(b), new_assumption);
|
||||
push_new_eq_constraint(new_state.m_active_cnstrs, new_ctx,
|
||||
mk_app(update_app(lift_free_vars(a, 1), 0, h_2), mk_var(0)), abst_body(b), new_assumption);
|
||||
imitation = mk_lambda(arg_types, update_abstraction(b, mk_app_vars(add_lift(h_1, 0, num_a - 1), num_a - 1), mk_app_vars(add_lift(h_2, 1, num_a - 1), num_a)));
|
||||
if (is_arrow(b)) {
|
||||
push_new_eq_constraint(new_state.m_active_cnstrs, new_ctx,
|
||||
update_app(lift_free_vars(a, 1), 0, h_2), abst_body(b), new_assumption);
|
||||
imitation = mk_lambda(arg_types, update_abstraction(b, mk_app_vars(add_lift(h_1, 0, num_a - 1), num_a - 1), mk_app_vars(add_lift(h_2, 1, num_a - 1), num_a - 1, 1)));
|
||||
} else {
|
||||
push_new_eq_constraint(new_state.m_active_cnstrs, new_ctx,
|
||||
mk_app(update_app(lift_free_vars(a, 1), 0, h_2), mk_var(0)), abst_body(b), new_assumption);
|
||||
imitation = mk_lambda(arg_types, update_abstraction(b, mk_app_vars(add_lift(h_1, 0, num_a - 1), num_a - 1), mk_app_vars(add_lift(h_2, 1, num_a - 1), num_a)));
|
||||
}
|
||||
} else {
|
||||
// "Dumb imitation" aka the constant function
|
||||
// Assign f_a <- fun (x_1 : T_1) ... (x_{num_a} : T_{num_a}), b
|
||||
|
|
|
|||
|
|
@ -15,6 +15,6 @@ variable R {A A' : Type}
|
|||
{B' : A' → Type}
|
||||
(H : @eq Type (∀ x : A, B x) (∀ x : A', B' x))
|
||||
(a : A) :
|
||||
@eq Type (B a) (B' (@C A A' (@D A A' (λ x : A, B x) (λ x : A', B' x) H) a))
|
||||
@eq Type (B a) (B' (@C A A' (@D A A' B B' H) a))
|
||||
theorem R2 (A1 A2 B1 B2 : Type) (H : @eq Type (A1 → B1) (A2 → B2)) (a : A1) : @eq Type B1 B2 :=
|
||||
@R A1 A2 (λ x : A1, B1) (λ x : A2, B2) H a
|
||||
|
|
|
|||
|
|
@ -15,6 +15,6 @@ variable R {A A' : Type}
|
|||
{B' : A' → Type}
|
||||
(H : @eq Type (∀ x : A, B x) (∀ x : A', B' x))
|
||||
(a : A) :
|
||||
@eq Type (B a) (B' (@C A A' (@D A A' (λ x : A, B x) (λ x : A', B' x) H) a))
|
||||
@eq Type (B a) (B' (@C A A' (@D A A' B B' H) a))
|
||||
theorem R2 (A1 A2 B1 B2 : Type) (H : @eq Type (A1 → B1) (A2 → B2)) (a : A1) : @eq Type B1 B2 :=
|
||||
@R A1 A2 (λ x : A1, B1) (λ x : A2, B2) H a
|
||||
|
|
|
|||
|
|
@ -9,9 +9,8 @@
|
|||
Assumed: H
|
||||
Assumed: a
|
||||
eta (F2 a) : (λ x : B, F2 a x) = F2 a
|
||||
funext (λ a : A, trans (symm (eta (F1 a))) (trans (funext (λ b : B, H a b)) (eta (F2 a)))) :
|
||||
(λ x : A, F1 x) = (λ x : A, F2 x)
|
||||
funext (λ a : A, funext (λ b : B, H a b)) : (λ (x : A) (x::1 : B), F1 x x::1) = (λ (x : A) (x::1 : B), F2 x x::1)
|
||||
funext (λ a : A, trans (symm (eta (F1 a))) (trans (funext (λ b : B, H a b)) (eta (F2 a)))) : F1 = F2
|
||||
funext (λ a : A, funext (λ b : B, H a b)) : F1 = F2
|
||||
Proved: T1
|
||||
Proved: T2
|
||||
Proved: T3
|
||||
|
|
|
|||
Loading…
Reference in a new issue