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

fix(library/simplifier): remove support in the simplifier for (forall x : A, B x) when it is not a proposition, the problem is that hpiext axiom produces an equality in a too big universe

Browse source 
For example, in the hpiext axiom, the resultant equality if for (Type M+1)

axiom hpiext {A A' : TypeM} {B : A -> TypeM} {B' : A' -> TypeM} :
      A = A' -> (∀ x x', x == x' -> B x = B' x') -> (∀ x, B x) = (∀ x, B' x)

even if the actual arguments A, A’, B, B’ "live" in a much smaller universe (e.g., Type).

So, it would be great if we could move the resultant equality back to the right universe.
I don't see how to do it right now.

The other solution would require a major rewrite of the code base.
We would have to support universe level arguments like Agda, and write the axiom hpiext as:

axiom hpiext {l : level} {A A' : (Type l)} {B : A -> (Type l)} {B' : A' -> (Type l)} :
      A = A' -> (∀ x x', x == x' -> B x = B' x') -> (∀ x, B x) = (∀ x, B' x)

This is the first instance I found where it is really handy to have this feature.
I think this would be a super clean solution, but it would require a big rewrite in the code base.
Another problem is that the actual semantics that Agda has for this kind of construction is not clear to me.
For instance, sometimes Agda reports that the type of an expression is (Set omega).

An easier to implement hack is to support "axiom templates".
We create instances of hipext "on-demand" for different universe levels.
This is essentially what Coq does, since the universe levels are implicit in Coq.
This is not as clean as the Agda approach, but it is much easier to implement.

A super dirty trick is to include some instances of hpiext for commonly used universes
(e.g., Type and (Type 1)).

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-26 12:10:27 -08:00
parent 52ee9b35dd
commit 29e448f034
1 changed files with 30 additions and 37 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

67
src/library/simplifier/simplifier.cpp
View file

@ -1282,6 +1282,7 @@ class simplifier_fn {
\brief Simplify the body of (forall x : A, P x), when P x is a proposition. \brief Simplify the body of (forall x : A, P x), when P x is a proposition.
*/ */
result simplify_forall_body(expr const & e) { result simplify_forall_body(expr const & e) {
lean_assert(is_pi(e) && is_proposition(e));
expr fresh_const = mk_fresh_const(abst_domain(e)); expr fresh_const = mk_fresh_const(abst_domain(e));
expr const & d = abst_domain(e); expr const & d = abst_domain(e);
expr b = abst_body(e); expr b = abst_body(e);
@ -1302,17 +1303,24 @@ class simplifier_fn {
} }
/** /**
\brief Simplify (forall x : A, P x) when the heq module is available. \brief Simplify (forall x : A, P x) proposition when the heq module is available.
In this case, we can simplify the domain and body of the Pi/forall expression. In this case, we can simplify the domain and body of the forall expression.
*/ */
result simplify_pi_with_heq(expr const & e) { result simplify_forall_with_heq(expr const & e) {
lean_assert(is_pi(e) && is_proposition(e));
// We don't support Pi's that are not proposition yet.
// The problem is that
// axiom hpiext {A A' : TypeM} {B : A → TypeM} {B' : A' → TypeM} :
// A = A' → (∀ x x', x == x' → B x = B' x') → (∀ x, B x) = (∀ x, B' x)
// produces an equality in TypeM even if A, A', B and B' live in smaller universes.
//
// This limitation does not seem to be a big problem in practice.
expr const & d = abst_domain(e); expr const & d = abst_domain(e);
result res_d = simplify(d); result res_d = simplify(d);
expr new_d = res_d.m_expr; expr new_d = res_d.m_expr;
bool is_prop = is_proposition(e); if (is_eqp(d, new_d))
if (is_eqp(d, new_d) && is_prop)
return simplify_forall_body(e); return simplify_forall_body(e);
if (is_definitionally_equal(d, new_d) && is_prop) if (is_definitionally_equal(d, new_d))
return simplify_forall_body(update_pi(e, new_d, abst_body(e))); return simplify_forall_body(update_pi(e, new_d, abst_body(e)));
// d and new_d are only provably equal, so we need to use hpiext or hallext // d and new_d are only provably equal, so we need to use hpiext or hallext
expr x_old = mk_fresh_const(d); expr x_old = mk_fresh_const(d);
@ -1333,38 +1341,22 @@ class simplifier_fn {
ensure_homogeneous(bi, res_bi); ensure_homogeneous(bi, res_bi);
// Remark: the argument with type A = A' in hallext and hpiext is actually @eq TypeM A A', // Remark: the argument with type A = A' in hallext and hpiext is actually @eq TypeM A A',
// so we need to translate the proof d_eq_new_d_proof : d = new_d to a TypeM equality proof // so we need to translate the proof d_eq_new_d_proof : d = new_d to a TypeM equality proof
expr d_eq_new_d_proof = translate_eq_typem_proof(d, res_d); expr d_eq_new_d_proof = translate_eq_typem_proof(d, res_d);
expr bi_eq_new_bi_proof; expr bi_eq_new_bi_proof = get_proof(res_bi);
if (is_prop)
bi_eq_new_bi_proof = get_proof(res_bi);
else
bi_eq_new_bi_proof = translate_eq_typem_proof(bi, res_bi);
// Heqb : (∀ x x', x == x' → B x = B' x') // Heqb : (∀ x x', x == x' → B x = B' x')
expr Heqb = mk_lambda(abst_name(e), d, expr Heqb = mk_lambda(abst_name(e), d,
mk_lambda(name(abst_name(e), 1), lift_free_vars(new_d, 0, 1), mk_lambda(name(abst_name(e), 1), lift_free_vars(new_d, 0, 1),
mk_lambda(name(g_H, m_next_idx++), abstract(x_old_eq_x_new, {x_old, x_new}), mk_lambda(name(g_H, m_next_idx++), abstract(x_old_eq_x_new, {x_old, x_new}),
abstract(bi_eq_new_bi_proof, {x_old, x_new, H_x_old_eq_x_new})))); abstract(bi_eq_new_bi_proof, {x_old, x_new, H_x_old_eq_x_new}))));
if (is_prop) { // Using
// Using // theorem hallext {A A' : TypeM} {B : A → Bool} {B' : A' → Bool} :
// theorem hallext {A A' : TypeM} {B : A → Bool} {B' : A' → Bool} : // A = A' → (∀ x x', x == x' → B x = B' x') → (∀ x, B x) = (∀ x, B' x)
// A = A' → (∀ x x', x == x' → B x = B' x') → (∀ x, B x) = (∀ x, B' x) expr new_proof = mk_hallext_th(d, new_d,
expr new_proof = mk_hallext_th(d, new_d, Fun(x_old, d, bi), // B
Fun(x_old, d, bi), // B Fun(x_new, new_d, new_bi), // B'
Fun(x_new, new_d, new_bi), // B' d_eq_new_d_proof, // A = A'
d_eq_new_d_proof, // A = A' Heqb);
Heqb); return rewrite(e, result(new_e, new_proof));
return rewrite(e, result(new_e, new_proof));
} else {
// Using
// axiom hpiext {A A' : TypeM} {B : A → TypeM} {B' : A' → TypeM} :
// A = A' → (∀ x x', x == x' → B x = B' x') → (∀ x, B x) = (∀ x, B' x)
expr new_proof = mk_hpiext_th(d, new_d,
Fun(x_old, d, bi), // B
Fun(x_new, new_d, new_bi), // B'
d_eq_new_d_proof, // A = A'
Heqb);
return rewrite(e, result(new_e, new_proof, false, true));
}
} }
result simplify_pi(expr const & e) { result simplify_pi(expr const & e) {
@ -1374,12 +1366,13 @@ class simplifier_fn {
return simplify_implication(e); return simplify_implication(e);
else else
return simplify_arrow(e); return simplify_arrow(e);
} else if (m_has_heq) {
return simplify_pi_with_heq(e);
} else if (is_proposition(e)) { } else if (is_proposition(e)) {
return simplify_forall_body(e); if (m_has_heq)
return simplify_forall_with_heq(e);
else
return simplify_forall_body(e);
} else { } else {
// if the environment does not contain heq axioms, then we don't simplify Pi's that are not forall's // We currently do simplify (forall x : A, B x) when it is not a proposition.
return result(e); return result(e);
} }
} }