lean2/src/kernel/replace_visitor.h
Leonardo de Moura 6d7ec9d7b6 refactor(kernel): add heterogeneous equality back to expr
The main motivation is that we will be able to move equalities between universes.

For example, suppose we have
    A : (Type i)
    B : (Type i)
    H : @eq (Type j) A B
where j > i

We didn't find any trick for deducing (@eq (Type i) A B) from H.
Before this commit, heterogeneous equality as a constant with type

   heq : {A B : (Type U)} : A -> B -> Bool

So, from H, we would only be able to deduce

   (@heq (Type j) (Type j) A B)

Not being able to move the equality back to a smaller universe is
problematic in several cases. I list some instances in the end of the commit message.

With this commit, Heterogeneous equality is a special kind of expression.
It is not a constant anymore. From H, we can deduce

   H1 : A == B

That is, we are essentially "erasing" the universes when we move to heterogeneous equality.
Now, since A and B have (Type i), we can deduce (@eq (Type i) A B) from H1. The proof term is

  (to_eq (Type i) A B (to_heq (Type j) A B H))  :  (@eq (Type i) A B)

So, it remains to explain why we need this feature.

For example, suppose we want to state the Pi extensionality axiom.

axiom hpiext {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} :
      A = A' → (∀ x x', x == x' → B x == B' x') → (∀ x, B x) == (∀ x, B' x)

This axiom produces an "inflated" equality at (Type U) when we treat heterogeneous
equality as a constant. The conclusion

     (∀ x, B x) == (∀ x, B' x)

is syntax sugar for

   (@heq (Type U) (Type U) (∀ x : A, B x) (∀ x : A', B' x))

Even if A, A', B, B' live in a much smaller universe.

As I described above, it doesn't seem to be a way to move this equality back to a smaller universe.

So, if we wanted to keep the heterogeneous equality as a constant, it seems we would
have to support axiom schemas. That is, hpiext would be parametrized by the universes where
A, A', B and B'. Another possibility would be to have universe polymorphism like Agda.
None of the solutions seem attractive.

So, we decided to have heterogeneous equality as a special kind of expression.
And use the trick above to move equalities back to the right universe.

BTW, the parser is not creating the new heterogeneous equalities yet.
Moreover, kernel.lean still contains a constant name heq2 that is the heterogeneous
equality as a constant.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-07 10:28:10 -08:00

63 lines
2 KiB
C++

/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "kernel/expr_maps.h"
#include "kernel/replace_fn.h"
#include "kernel/context.h"
namespace lean {
/**
\brief Base class for implementing operations that apply modifications
an expressions.
The default behavior is a NOOP, users must create subclasses and
redefine the visit_* methods.
This is a more expensive (and flexible) version of replace_fn in
the file kernel/replace.h
*/
class replace_visitor {
protected:
typedef expr_map<expr> cache;
cache m_cache;
context m_ctx;
expr save_result(expr const & e, expr && r, bool shared);
virtual expr visit_type(expr const &, context const &);
virtual expr visit_value(expr const &, context const &);
virtual expr visit_constant(expr const &, context const &);
virtual expr visit_var(expr const &, context const &);
virtual expr visit_metavar(expr const &, context const &);
virtual expr visit_heq(expr const &, context const &);
virtual expr visit_pair(expr const &, context const &);
virtual expr visit_proj(expr const &, context const &);
virtual expr visit_app(expr const &, context const &);
virtual expr visit_abst(expr const &, context const &);
virtual expr visit_lambda(expr const &, context const &);
virtual expr visit_pi(expr const &, context const &);
virtual expr visit_sigma(expr const &, context const &);
virtual expr visit_let(expr const &, context const &);
virtual expr visit(expr const &, context const &);
optional<expr> visit(optional<expr> const &, context const &);
void set_ctx(context const & ctx) {
if (!is_eqp(m_ctx, ctx)) {
m_ctx = ctx;
m_cache.clear();
}
}
public:
expr operator()(expr const & e, context const & ctx = context()) {
set_ctx(ctx);
return visit(e, ctx);
}
void clear() {
m_ctx = context();
m_cache.clear();
}
};
}