chore(library): remove relation_manager
This commit is contained in:
Leonardo de Moura
parent
373e979a2a
commit
c48eaed9a4
8 changed files with 14 additions and 537 deletions
|
|
@ -215,20 +215,18 @@ intro :: (mp : a → b) (mpr : b → a)
|
|||
|
||||
infix = := eq
|
||||
|
||||
attribute [refl] eq.refl
|
||||
|
||||
@[pattern] def rfl {α : Sort u} {a : α} : a = a := eq.refl a
|
||||
|
||||
@[elab_as_eliminator, subst]
|
||||
@[elab_as_eliminator]
|
||||
theorem eq.subst {α : Sort u} {P : α → Prop} {a b : α} (h₁ : a = b) (h₂ : P a) : P b :=
|
||||
eq.ndrec h₂ h₁
|
||||
|
||||
notation h1 ▸ h2 := eq.subst h1 h2
|
||||
|
||||
@[trans] theorem eq.trans {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c :=
|
||||
theorem eq.trans {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c :=
|
||||
h₂ ▸ h₁
|
||||
|
||||
@[symm] theorem eq.symm {α : Sort u} {a b : α} (h : a = b) : b = a :=
|
||||
theorem eq.symm {α : Sort u} {a b : α} (h : a = b) : b = a :=
|
||||
h ▸ rfl
|
||||
|
||||
infix == := heq
|
||||
|
|
@ -627,7 +625,7 @@ notation x && y := band x y
|
|||
|
||||
def implies (a b : Prop) := a → b
|
||||
|
||||
@[trans] theorem implies.trans {p q r : Prop} (h₁ : implies p q) (h₂ : implies q r) : implies p r :=
|
||||
theorem implies.trans {p q r : Prop} (h₁ : implies p q) (h₂ : implies q r) : implies p r :=
|
||||
assume hp, h₂ (h₁ hp)
|
||||
|
||||
def trivial : true := ⟨⟩
|
||||
|
|
@ -725,8 +723,6 @@ theorem eq_tt_of_ne_ff : ∀ {b : bool}, b ≠ ff → b = tt
|
|||
| tt h := rfl
|
||||
| ff h := false.elim (h rfl)
|
||||
|
||||
attribute [refl] heq.refl
|
||||
|
||||
section
|
||||
variables {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ}
|
||||
|
||||
|
|
@ -744,19 +740,19 @@ eq.rec_on (eq_of_heq h₁) h₂
|
|||
theorem heq.subst {p : ∀ T : Sort u, T → Prop} (h₁ : a == b) (h₂ : p α a) : p β b :=
|
||||
heq.ndrec_on h₁ h₂
|
||||
|
||||
@[symm] theorem heq.symm (h : a == b) : b == a :=
|
||||
theorem heq.symm (h : a == b) : b == a :=
|
||||
heq.ndrec_on h (heq.refl a)
|
||||
|
||||
theorem heq_of_eq (h : a = a') : a == a' :=
|
||||
eq.subst h (heq.refl a)
|
||||
|
||||
@[trans] theorem heq.trans (h₁ : a == b) (h₂ : b == c) : a == c :=
|
||||
theorem heq.trans (h₁ : a == b) (h₂ : b == c) : a == c :=
|
||||
heq.subst h₂ h₁
|
||||
|
||||
@[trans] theorem heq_of_heq_of_eq (h₁ : a == b) (h₂ : b = b') : a == b' :=
|
||||
theorem heq_of_heq_of_eq (h₁ : a == b) (h₂ : b = b') : a == b' :=
|
||||
heq.trans h₁ (heq_of_eq h₂)
|
||||
|
||||
@[trans] theorem heq_of_eq_of_heq (h₁ : a = a') (h₂ : a' == b) : a == b :=
|
||||
theorem heq_of_eq_of_heq (h₁ : a = a') (h₂ : a' == b) : a == b :=
|
||||
heq.trans (heq_of_eq h₁) h₂
|
||||
|
||||
def type_eq_of_heq (h : a == b) : α = β :=
|
||||
|
|
@ -820,20 +816,17 @@ theorem iff.elim_right : (a ↔ b) → b → a := iff.mpr
|
|||
theorem iff_iff_implies_and_implies (a b : Prop) : (a ↔ b) ↔ (a → b) ∧ (b → a) :=
|
||||
iff.intro (λ h, and.intro h.mp h.mpr) (λ h, iff.intro h.left h.right)
|
||||
|
||||
@[refl]
|
||||
theorem iff.refl (a : Prop) : a ↔ a :=
|
||||
iff.intro (assume h, h) (assume h, h)
|
||||
|
||||
theorem iff.rfl {a : Prop} : a ↔ a :=
|
||||
iff.refl a
|
||||
|
||||
@[trans]
|
||||
theorem iff.trans (h₁ : a ↔ b) (h₂ : b ↔ c) : a ↔ c :=
|
||||
iff.intro
|
||||
(assume ha, iff.mp h₂ (iff.mp h₁ ha))
|
||||
(assume hc, iff.mpr h₁ (iff.mpr h₂ hc))
|
||||
|
||||
@[symm]
|
||||
theorem iff.symm (h : a ↔ b) : b ↔ a :=
|
||||
iff.intro (iff.elim_right h) (iff.elim_left h)
|
||||
|
||||
|
|
@ -1734,15 +1727,15 @@ instance setoid_has_equiv {α : Sort u} [setoid α] : has_equiv α :=
|
|||
namespace setoid
|
||||
variables {α : Sort u} [setoid α]
|
||||
|
||||
@[refl] theorem refl (a : α) : a ≈ a :=
|
||||
theorem refl (a : α) : a ≈ a :=
|
||||
match setoid.iseqv α with
|
||||
| ⟨h_refl, h_symm, h_trans⟩ := h_refl a
|
||||
|
||||
@[symm] theorem symm {a b : α} (hab : a ≈ b) : b ≈ a :=
|
||||
theorem symm {a b : α} (hab : a ≈ b) : b ≈ a :=
|
||||
match setoid.iseqv α with
|
||||
| ⟨h_refl, h_symm, h_trans⟩ := h_symm hab
|
||||
|
||||
@[trans] theorem trans {a b c : α} (hab : a ≈ b) (hbc : b ≈ c) : a ≈ c :=
|
||||
theorem trans {a b c : α} (hab : a ≈ b) (hbc : b ≈ c) : a ≈ c :=
|
||||
(match setoid.iseqv α with
|
||||
| ⟨h_refl, h_symm, h_trans⟩ := h_trans hab hbc)
|
||||
end setoid
|
||||
|
|
@ -1787,7 +1780,7 @@ eq.subst (@iff_eq_eq a true) this
|
|||
/- Quotients -/
|
||||
|
||||
-- iff can now be used to do substitutions in a calculation
|
||||
@[subst] theorem iff_subst {a b : Prop} {p : Prop → Prop} (h₁ : a ↔ b) (h₂ : p a) : p b :=
|
||||
theorem iff_subst {a b : Prop} {p : Prop → Prop} (h₁ : a ↔ b) (h₂ : p a) : p b :=
|
||||
eq.subst (propext h₁) h₂
|
||||
|
||||
namespace quot
|
||||
|
|
|
|||
|
|
@ -198,7 +198,7 @@ h₁ ◾ h₂ ◾ h₃ ◾ h₄ ◾ h₅ ◾ h₆
|
|||
|
||||
/- Inequalities -/
|
||||
|
||||
@[refl] protected def le_refl : ∀ n : nat, n ≤ n
|
||||
protected def le_refl : ∀ n : nat, n ≤ n
|
||||
| zero := rfl
|
||||
| (succ n) := le_refl n
|
||||
|
||||
|
|
|
|||
|
|
@ -6,8 +6,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
|
|||
class.cpp util.cpp print.cpp annotation.cpp quote.cpp
|
||||
protected.cpp reducible.cpp init_module.cpp
|
||||
exception.cpp fingerprint.cpp pp_options.cpp
|
||||
app_builder.cpp projection.cpp relation_manager.cpp
|
||||
user_recursors.cpp idx_metavar.cpp noncomputable.cpp
|
||||
app_builder.cpp projection.cpp user_recursors.cpp idx_metavar.cpp noncomputable.cpp
|
||||
aux_recursors.cpp trace.cpp
|
||||
attribute_manager.cpp local_context.cpp metavar_context.cpp type_context.cpp export_decl.cpp
|
||||
fun_info.cpp replace_visitor_with_tc.cpp aux_definition.cpp pattern_attribute.cpp
|
||||
|
|
|
|||
|
|
@ -13,7 +13,6 @@ Author: Leonardo de Moura
|
|||
#include "library/constants.h"
|
||||
#include "library/cache_helper.h"
|
||||
#include "library/app_builder.h"
|
||||
#include "library/relation_manager.h"
|
||||
|
||||
namespace lean {
|
||||
static void trace_fun(name const & n) {
|
||||
|
|
@ -414,26 +413,6 @@ public:
|
|||
return mk_app(c, total_nargs, {a1, a2, a3});
|
||||
}
|
||||
|
||||
/** \brief Similar to mk_app(n, lhs, rhs), but handles eq and iff more efficiently. */
|
||||
expr mk_rel(name const & n, expr const & lhs, expr const & rhs) {
|
||||
if (n == get_eq_name()) {
|
||||
return mk_eq(lhs, rhs);
|
||||
} else if (n == get_iff_name()) {
|
||||
return mk_iff(lhs, rhs);
|
||||
} else if (auto info = get_relation_info(env(), n)) {
|
||||
buffer<bool> mask;
|
||||
for (unsigned i = 0; i < info->get_arity(); i++) {
|
||||
mask.push_back(i == info->get_lhs_pos() || i == info->get_rhs_pos());
|
||||
}
|
||||
expr args[2] = {lhs, rhs};
|
||||
return mk_app(n, info->get_arity(), mask.data(), args);
|
||||
} else {
|
||||
// for unregistered relations assume lhs and rhs are the last two arguments.
|
||||
expr args[2] = {lhs, rhs};
|
||||
return mk_app(n, 2, args);
|
||||
}
|
||||
}
|
||||
|
||||
expr mk_eq(expr const & a, expr const & b) {
|
||||
expr A = m_ctx.infer(a);
|
||||
level lvl = get_level(A);
|
||||
|
|
@ -459,8 +438,6 @@ public:
|
|||
return mk_iff_refl(a);
|
||||
} else if (relname == get_heq_name()) {
|
||||
return mk_heq_refl(a);
|
||||
} else if (auto info = get_refl_extra_info(env(), relname)) {
|
||||
return mk_app(info->m_name, 1, &a);
|
||||
} else {
|
||||
lean_app_builder_trace(
|
||||
tout() << "failed to build reflexivity proof, '" << relname
|
||||
|
|
@ -490,8 +467,6 @@ public:
|
|||
return mk_iff_symm(H);
|
||||
} else if (relname == get_heq_name()) {
|
||||
return mk_heq_symm(H);
|
||||
} else if (auto info = get_symm_extra_info(env(), relname)) {
|
||||
return mk_app(info->m_name, 1, &H);
|
||||
} else {
|
||||
lean_app_builder_trace(
|
||||
tout() << "failed to build symmetry proof, '" << relname
|
||||
|
|
@ -544,9 +519,6 @@ public:
|
|||
return mk_iff_trans(H1, H2);
|
||||
} else if (relname == get_heq_name()) {
|
||||
return mk_heq_trans(H1, H2);
|
||||
} else if (auto info = get_trans_extra_info(env(), relname, relname)) {
|
||||
expr args[2] = {H1, H2};
|
||||
return mk_app(info->m_name, 2, args);
|
||||
} else {
|
||||
lean_app_builder_trace(
|
||||
tout() << "failed to build symmetry proof, '" << relname
|
||||
|
|
@ -670,27 +642,6 @@ public:
|
|||
return ::lean::mk_app({mk_constant(get_heq_of_eq_name(), {lvl}), A, a, b, H});
|
||||
}
|
||||
|
||||
/** \brief Given a reflexive relation R, and a proof H : a = b,
|
||||
build a proof for (R a b) */
|
||||
expr lift_from_eq(name const & R, expr const & H) {
|
||||
if (R == get_eq_name())
|
||||
return H;
|
||||
expr H_type = m_ctx.relaxed_whnf(m_ctx.infer(H));
|
||||
// H_type : @eq A a b
|
||||
expr A, a, b;
|
||||
if (!is_eq(H_type, A, a, b)) {
|
||||
lean_app_builder_trace(tout() << "failed to build lift_of_eq equality proof expected:\n" << H << "\n";);
|
||||
throw app_builder_exception();
|
||||
}
|
||||
type_context_old::tmp_locals locals(m_ctx);
|
||||
expr x = locals.push_local(name("A"), A);
|
||||
// motive := fun x : A, a ~ x
|
||||
expr motive = locals.mk_lambda(mk_rel(R, a, x));
|
||||
// minor : a ~ a
|
||||
expr minor = mk_refl(R, a);
|
||||
return mk_eq_rec(motive, minor, H);
|
||||
}
|
||||
|
||||
expr mk_ss_elim(expr const & A, expr const & ss_inst, expr const & old_e, expr const & new_e) {
|
||||
level lvl = get_level(A);
|
||||
return ::lean::mk_app(mk_constant(get_subsingleton_elim_name(), {lvl}), A, ss_inst, old_e, new_e);
|
||||
|
|
@ -784,10 +735,6 @@ expr mk_app(type_context_old & ctx, name const & c, unsigned total_nargs, unsign
|
|||
return app_builder(ctx).mk_app(c, total_nargs, expl_nargs, expl_args);
|
||||
}
|
||||
|
||||
expr mk_rel(type_context_old & ctx, name const & n, expr const & lhs, expr const & rhs) {
|
||||
return app_builder(ctx).mk_rel(n, lhs, rhs);
|
||||
}
|
||||
|
||||
expr mk_eq(type_context_old & ctx, expr const & lhs, expr const & rhs) {
|
||||
return app_builder(ctx).mk_eq(lhs, rhs);
|
||||
}
|
||||
|
|
@ -950,10 +897,6 @@ expr mk_funext(type_context_old & ctx, expr const & lam_pf) {
|
|||
return mk_app(ctx, get_funext_name(), lam_pf);
|
||||
}
|
||||
|
||||
expr lift_from_eq(type_context_old & ctx, name const & R, expr const & H) {
|
||||
return app_builder(ctx).lift_from_eq(R, H);
|
||||
}
|
||||
|
||||
expr mk_iff_false_intro(type_context_old & ctx, expr const & H) {
|
||||
// TODO(Leo): implement custom version if bottleneck.
|
||||
return mk_app(ctx, get_iff_false_intro_name(), {H});
|
||||
|
|
|
|||
|
|
@ -8,7 +8,6 @@ Author: Leonardo de Moura
|
|||
#include <memory>
|
||||
#include <unordered_map>
|
||||
#include "kernel/environment.h"
|
||||
#include "library/relation_manager.h"
|
||||
#include "library/reducible.h"
|
||||
#include "library/type_context.h"
|
||||
|
||||
|
|
@ -81,7 +80,6 @@ inline expr mk_app(type_context_old & ctx, name const & c, unsigned total_nargs,
|
|||
}
|
||||
|
||||
/** \brief Similar to mk_app(n, lhs, rhs), but handles eq and iff more efficiently. */
|
||||
expr mk_rel(type_context_old & ctx, name const & n, expr const & lhs, expr const & rhs);
|
||||
expr mk_eq(type_context_old & ctx, expr const & lhs, expr const & rhs);
|
||||
expr mk_iff(type_context_old & ctx, expr const & lhs, expr const & rhs);
|
||||
expr mk_heq(type_context_old & ctx, expr const & lhs, expr const & rhs);
|
||||
|
|
@ -133,10 +131,6 @@ expr mk_congr(type_context_old & ctx, expr const & H1, expr const & H2, bool ski
|
|||
|
||||
expr mk_funext(type_context_old & ctx, expr const & lam_pf);
|
||||
|
||||
/** \brief Given a reflexive relation R, and a proof H : a = b,
|
||||
build a proof for (R a b) */
|
||||
expr lift_from_eq(type_context_old & ctx, name const & R, expr const & H);
|
||||
|
||||
/** \brief not p -> (p <-> false) */
|
||||
expr mk_iff_false_intro(type_context_old & ctx, expr const & H);
|
||||
/** \brief p -> (p <-> true) */
|
||||
|
|
|
|||
|
|
@ -27,7 +27,6 @@ Author: Leonardo de Moura
|
|||
#include "library/util.h"
|
||||
#include "library/pp_options.h"
|
||||
#include "library/projection.h"
|
||||
#include "library/relation_manager.h"
|
||||
#include "library/user_recursors.h"
|
||||
#include "library/noncomputable.h"
|
||||
#include "library/aux_recursors.h"
|
||||
|
|
@ -98,7 +97,6 @@ void initialize_library_module() {
|
|||
initialize_quote();
|
||||
initialize_pp_options();
|
||||
initialize_projection();
|
||||
initialize_relation_manager();
|
||||
initialize_user_recursors();
|
||||
initialize_noncomputable();
|
||||
initialize_aux_recursors();
|
||||
|
|
@ -126,7 +124,6 @@ void finalize_library_module() {
|
|||
finalize_aux_recursors();
|
||||
finalize_noncomputable();
|
||||
finalize_user_recursors();
|
||||
finalize_relation_manager();
|
||||
finalize_projection();
|
||||
finalize_pp_options();
|
||||
finalize_quote();
|
||||
|
|
|
|||
|
|
@ -1,351 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include <string>
|
||||
#include "runtime/sstream.h"
|
||||
#include "runtime/optional.h"
|
||||
#include "util/name.h"
|
||||
#include "util/rb_map.h"
|
||||
#include "library/constants.h"
|
||||
#include "library/scoped_ext.h"
|
||||
#include "library/relation_manager.h"
|
||||
#include "library/attribute_manager.h"
|
||||
|
||||
namespace lean {
|
||||
// Check whether e is of the form (f ...) where f is a constant. If it is return f.
|
||||
static name const & get_fn_const(expr const & e, char const * msg) {
|
||||
expr const & fn = get_app_fn(e);
|
||||
if (!is_constant(unwrap_pos(fn)))
|
||||
throw exception(msg);
|
||||
return const_name(fn);
|
||||
}
|
||||
|
||||
static pair<expr, unsigned> extract_arg_types_core(environment const & env, name const & f, buffer<expr> & arg_types) {
|
||||
constant_info info = env.get(f);
|
||||
expr f_type = info.get_type();
|
||||
while (is_pi(f_type)) {
|
||||
arg_types.push_back(binding_domain(f_type));
|
||||
f_type = binding_body(f_type);
|
||||
}
|
||||
return mk_pair(f_type, info.get_num_lparams());
|
||||
}
|
||||
|
||||
enum class op_kind { Relation, Subst, Trans, Refl, Symm };
|
||||
|
||||
struct rel_entry {
|
||||
op_kind m_kind;
|
||||
name m_name;
|
||||
rel_entry() {}
|
||||
rel_entry(op_kind k, name const & n):m_kind(k), m_name(n) {}
|
||||
};
|
||||
|
||||
struct rel_state {
|
||||
typedef name_map<refl_info> refl_table;
|
||||
typedef name_map<subst_info> subst_table;
|
||||
typedef name_map<symm_info> symm_table;
|
||||
typedef rb_map<name_pair, trans_info, name_pair_quick_cmp> trans_table;
|
||||
typedef name_map<relation_info> rop_table;
|
||||
trans_table m_trans_table;
|
||||
refl_table m_refl_table;
|
||||
subst_table m_subst_table;
|
||||
symm_table m_symm_table;
|
||||
rop_table m_rop_table;
|
||||
rel_state() {}
|
||||
|
||||
bool is_equivalence(name const & rop) const {
|
||||
return m_trans_table.contains(mk_pair(rop, rop)) && m_refl_table.contains(rop) && m_symm_table.contains(rop);
|
||||
}
|
||||
|
||||
static void throw_invalid_relation(name const & rop) {
|
||||
throw exception(sstream() << "invalid binary relation declaration, relation '" << rop
|
||||
<< "' must have two explicit parameters");
|
||||
}
|
||||
|
||||
void register_rop(environment const & env, name const & rop) {
|
||||
if (m_rop_table.contains(rop))
|
||||
return;
|
||||
constant_info info = env.get(rop);
|
||||
optional<unsigned> lhs_pos;
|
||||
optional<unsigned> rhs_pos;
|
||||
unsigned i = 0;
|
||||
expr type = info.get_type();
|
||||
while (is_pi(type)) {
|
||||
if (is_explicit(binding_info(type))) {
|
||||
if (!lhs_pos) {
|
||||
lhs_pos = i;
|
||||
} else if (!rhs_pos) {
|
||||
rhs_pos = i;
|
||||
} else {
|
||||
lhs_pos = rhs_pos;
|
||||
rhs_pos = i;
|
||||
}
|
||||
}
|
||||
type = binding_body(type);
|
||||
i++;
|
||||
}
|
||||
if (lhs_pos && rhs_pos) {
|
||||
m_rop_table.insert(rop, relation_info(i, *lhs_pos, *rhs_pos));
|
||||
} else {
|
||||
throw_invalid_relation(rop);
|
||||
}
|
||||
}
|
||||
|
||||
void add_subst(environment const & env, name const & subst) {
|
||||
buffer<expr> arg_types;
|
||||
auto p = extract_arg_types_core(env, subst, arg_types);
|
||||
expr r_type = p.first;
|
||||
unsigned nunivs = p.second;
|
||||
unsigned nargs = arg_types.size();
|
||||
if (nargs < 2)
|
||||
throw exception("invalid substitution theorem, it must have at least 2 arguments");
|
||||
name const & rop = get_fn_const(arg_types[nargs-2], "invalid substitution theorem, penultimate argument must be an operator application");
|
||||
m_subst_table.insert(rop, subst_info(subst, nunivs, nargs));
|
||||
}
|
||||
|
||||
void add_refl(environment const & env, name const & refl) {
|
||||
buffer<expr> arg_types;
|
||||
auto p = extract_arg_types_core(env, refl, arg_types);
|
||||
expr r_type = p.first;
|
||||
unsigned nunivs = p.second;
|
||||
unsigned nargs = arg_types.size();
|
||||
if (nargs < 1)
|
||||
throw exception("invalid reflexivity rule, it must have at least 1 argument");
|
||||
name const & rop = get_fn_const(r_type, "invalid reflexivity rule, result type must be an operator application");
|
||||
register_rop(env, rop);
|
||||
m_refl_table.insert(rop, refl_info(refl, nunivs, nargs));
|
||||
}
|
||||
|
||||
void add_trans(environment const & env, name const & trans) {
|
||||
buffer<expr> arg_types;
|
||||
auto p = extract_arg_types_core(env, trans, arg_types);
|
||||
expr r_type = p.first;
|
||||
unsigned nunivs = p.second;
|
||||
unsigned nargs = arg_types.size();
|
||||
if (nargs < 5)
|
||||
throw exception("invalid transitivity rule, it must have at least 5 arguments");
|
||||
name const & rop = get_fn_const(r_type, "invalid transitivity rule, result type must be an operator application");
|
||||
name const & op1 = get_fn_const(arg_types[nargs-2], "invalid transitivity rule, penultimate argument must be an operator application");
|
||||
name const & op2 = get_fn_const(arg_types[nargs-1], "invalid transitivity rule, last argument must be an operator application");
|
||||
register_rop(env, rop);
|
||||
m_trans_table.insert(name_pair(op1, op2), trans_info(trans, nunivs, nargs, rop));
|
||||
}
|
||||
|
||||
void add_symm(environment const & env, name const & symm) {
|
||||
buffer<expr> arg_types;
|
||||
auto p = extract_arg_types_core(env, symm, arg_types);
|
||||
expr r_type = p.first;
|
||||
unsigned nunivs = p.second;
|
||||
unsigned nargs = arg_types.size();
|
||||
if (nargs < 1)
|
||||
throw exception("invalid symmetry rule, it must have at least 1 argument");
|
||||
name const & rop = get_fn_const(r_type, "invalid symmetry rule, result type must be an operator application");
|
||||
register_rop(env, rop);
|
||||
m_symm_table.insert(rop, symm_info(symm, nunivs, nargs));
|
||||
}
|
||||
};
|
||||
|
||||
struct rel_config {
|
||||
typedef rel_state state;
|
||||
typedef rel_entry entry;
|
||||
static void add_entry(environment const & env, io_state const &, state & s, entry const & e) {
|
||||
switch (e.m_kind) {
|
||||
case op_kind::Relation: s.register_rop(env, e.m_name); break;
|
||||
case op_kind::Refl: s.add_refl(env, e.m_name); break;
|
||||
case op_kind::Subst: s.add_subst(env, e.m_name); break;
|
||||
case op_kind::Trans: s.add_trans(env, e.m_name); break;
|
||||
case op_kind::Symm: s.add_symm(env, e.m_name); break;
|
||||
}
|
||||
}
|
||||
static const char * get_serialization_key() { return "REL"; }
|
||||
static void write_entry(serializer & s, entry const & e) {
|
||||
s << static_cast<char>(e.m_kind) << e.m_name;
|
||||
}
|
||||
static entry read_entry(deserializer & d) {
|
||||
entry e;
|
||||
char cmd;
|
||||
d >> cmd >> e.m_name;
|
||||
e.m_kind = static_cast<op_kind>(cmd);
|
||||
return e;
|
||||
}
|
||||
static optional<unsigned> get_fingerprint(entry const &) {
|
||||
return optional<unsigned>();
|
||||
}
|
||||
};
|
||||
|
||||
template class scoped_ext<rel_config>;
|
||||
typedef scoped_ext<rel_config> rel_ext;
|
||||
|
||||
environment add_relation(environment const & env, name const & n, bool persistent) {
|
||||
return rel_ext::add_entry(env, get_dummy_ios(), rel_entry(op_kind::Relation, n), persistent);
|
||||
}
|
||||
|
||||
environment add_subst(environment const & env, name const & n, bool persistent) {
|
||||
return rel_ext::add_entry(env, get_dummy_ios(), rel_entry(op_kind::Subst, n), persistent);
|
||||
}
|
||||
|
||||
environment add_refl(environment const & env, name const & n, bool persistent) {
|
||||
return rel_ext::add_entry(env, get_dummy_ios(), rel_entry(op_kind::Refl, n), persistent);
|
||||
}
|
||||
|
||||
environment add_symm(environment const & env, name const & n, bool persistent) {
|
||||
return rel_ext::add_entry(env, get_dummy_ios(), rel_entry(op_kind::Symm, n), persistent);
|
||||
}
|
||||
|
||||
environment add_trans(environment const & env, name const & n, bool persistent) {
|
||||
return rel_ext::add_entry(env, get_dummy_ios(), rel_entry(op_kind::Trans, n), persistent);
|
||||
}
|
||||
|
||||
static optional<relation_lemma_info> get_info(name_map<relation_lemma_info> const & table, name const & op) {
|
||||
if (auto it = table.find(op)) {
|
||||
return optional<relation_lemma_info>(*it);
|
||||
} else {
|
||||
return optional<relation_lemma_info>();
|
||||
}
|
||||
}
|
||||
|
||||
optional<refl_info> get_refl_extra_info(environment const & env, name const & op) {
|
||||
return get_info(rel_ext::get_state(env).m_refl_table, op);
|
||||
}
|
||||
optional<subst_info> get_subst_extra_info(environment const & env, name const & op) {
|
||||
return get_info(rel_ext::get_state(env).m_subst_table, op);
|
||||
}
|
||||
optional<symm_info> get_symm_extra_info(environment const & env, name const & op) {
|
||||
return get_info(rel_ext::get_state(env).m_symm_table, op);
|
||||
}
|
||||
|
||||
optional<trans_info> get_trans_extra_info(environment const & env, name const & op1, name const & op2) {
|
||||
if (auto it = rel_ext::get_state(env).m_trans_table.find(mk_pair(op1, op2))) {
|
||||
return optional<trans_info>(*it);
|
||||
} else {
|
||||
return optional<trans_info>();
|
||||
}
|
||||
}
|
||||
|
||||
bool is_subst_relation(environment const & env, name const & op) {
|
||||
return rel_ext::get_state(env).m_subst_table.contains(op);
|
||||
}
|
||||
|
||||
optional<name> get_refl_info(environment const & env, name const & op) {
|
||||
if (auto it = get_refl_extra_info(env, op))
|
||||
return optional<name>(it->m_name);
|
||||
else
|
||||
return optional<name>();
|
||||
}
|
||||
|
||||
optional<name> get_symm_info(environment const & env, name const & op) {
|
||||
if (auto it = get_symm_extra_info(env, op))
|
||||
return optional<name>(it->m_name);
|
||||
else
|
||||
return optional<name>();
|
||||
}
|
||||
|
||||
optional<name> get_trans_info(environment const & env, name const & op) {
|
||||
if (auto it = get_trans_extra_info(env, op, op))
|
||||
return optional<name>(it->m_name);
|
||||
else
|
||||
return optional<name>();
|
||||
}
|
||||
|
||||
refl_info_getter mk_refl_info_getter(environment const & env) {
|
||||
auto t = rel_ext::get_state(env).m_refl_table;
|
||||
return [=](name const & n) { return get_info(t, n); }; // NOLINT
|
||||
}
|
||||
|
||||
trans_info_getter mk_trans_info_getter(environment const & env) {
|
||||
auto t = rel_ext::get_state(env).m_trans_table;
|
||||
return [=](name const & op1, name const & op2) { // NOLINT
|
||||
if (auto it = t.find(mk_pair(op1, op2))) {
|
||||
return optional<trans_info>(*it);
|
||||
} else {
|
||||
return optional<trans_info>();
|
||||
}
|
||||
};
|
||||
}
|
||||
|
||||
symm_info_getter mk_symm_info_getter(environment const & env) {
|
||||
auto t = rel_ext::get_state(env).m_symm_table;
|
||||
return [=](name const & n) { return get_info(t, n); }; // NOLINT
|
||||
}
|
||||
|
||||
bool is_equivalence(environment const & env, name const & rop) {
|
||||
return rel_ext::get_state(env).is_equivalence(rop);
|
||||
}
|
||||
|
||||
relation_info const * get_relation_info(environment const & env, name const & rop) {
|
||||
return rel_ext::get_state(env).m_rop_table.find(rop);
|
||||
}
|
||||
|
||||
relation_info_getter mk_relation_info_getter(environment const & env) {
|
||||
auto table = rel_ext::get_state(env).m_rop_table;
|
||||
return [=](name const & rop) { // NOLINT
|
||||
if (auto r = table.find(rop))
|
||||
return optional<relation_info>(*r);
|
||||
else
|
||||
return optional<relation_info>();
|
||||
};
|
||||
}
|
||||
|
||||
bool is_relation(name_map<relation_info> const & table, expr const & e, name & rop, expr & lhs, expr & rhs) {
|
||||
if (!is_app(e))
|
||||
return false;
|
||||
expr const & f = get_app_fn(e);
|
||||
if (!is_constant(f))
|
||||
return false;
|
||||
auto r = table.find(const_name(f));
|
||||
if (!r)
|
||||
return false;
|
||||
buffer<expr> args;
|
||||
get_app_args(e, args);
|
||||
if (r->get_arity() != args.size())
|
||||
return false;
|
||||
rop = const_name(f);
|
||||
lhs = args[r->get_lhs_pos()];
|
||||
rhs = args[r->get_rhs_pos()];
|
||||
return true;
|
||||
}
|
||||
|
||||
bool is_relation(environment const & env, expr const & e, name & rop, expr & lhs, expr & rhs) {
|
||||
return is_relation(rel_ext::get_state(env).m_rop_table, e, rop, lhs, rhs);
|
||||
}
|
||||
|
||||
is_relation_pred mk_is_relation_pred(environment const & env) {
|
||||
name_map<relation_info> table = rel_ext::get_state(env).m_rop_table;
|
||||
return [=](expr const & e, name & rop, expr & lhs, expr & rhs) { // NOLINT
|
||||
return is_relation(table, e, rop, lhs, rhs);
|
||||
};
|
||||
}
|
||||
|
||||
void initialize_relation_manager() {
|
||||
rel_ext::initialize();
|
||||
register_system_attribute(basic_attribute("refl", "reflexive relation",
|
||||
[](environment const & env, io_state const &, name const & d, unsigned,
|
||||
bool persistent) {
|
||||
return add_refl(env, d, persistent);
|
||||
}));
|
||||
|
||||
register_system_attribute(basic_attribute("symm", "symmetric relation",
|
||||
[](environment const & env, io_state const &, name const & d, unsigned,
|
||||
bool persistent) {
|
||||
return add_symm(env, d, persistent);
|
||||
}));
|
||||
|
||||
register_system_attribute(basic_attribute("trans", "transitive relation",
|
||||
[](environment const & env, io_state const &, name const & d, unsigned,
|
||||
bool persistent) {
|
||||
return add_trans(env, d, persistent);
|
||||
}));
|
||||
|
||||
register_system_attribute(basic_attribute("subst", "substitution",
|
||||
[](environment const & env, io_state const &, name const & d, unsigned,
|
||||
bool persistent) {
|
||||
return add_subst(env, d, persistent);
|
||||
}));
|
||||
}
|
||||
|
||||
void finalize_relation_manager() {
|
||||
rel_ext::finalize();
|
||||
}
|
||||
}
|
||||
|
|
@ -1,98 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2015 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/environment.h"
|
||||
|
||||
namespace lean {
|
||||
struct relation_info {
|
||||
unsigned m_arity;
|
||||
unsigned m_lhs_pos;
|
||||
unsigned m_rhs_pos;
|
||||
public:
|
||||
relation_info() {}
|
||||
relation_info(unsigned arity, unsigned lhs, unsigned rhs):
|
||||
m_arity(arity), m_lhs_pos(lhs), m_rhs_pos(rhs) {
|
||||
lean_assert(m_lhs_pos < m_arity);
|
||||
lean_assert(m_rhs_pos < m_arity);
|
||||
}
|
||||
unsigned get_arity() const { return m_arity; }
|
||||
unsigned get_lhs_pos() const { return m_lhs_pos; }
|
||||
unsigned get_rhs_pos() const { return m_rhs_pos; }
|
||||
};
|
||||
|
||||
/** \brief Return true if \c rop is a registered equivalence relation in the given manager */
|
||||
bool is_equivalence(environment const & env, name const & rop);
|
||||
|
||||
/** \brief If \c rop is a registered relation, then return a non-null pointer to the associated information
|
||||
Lean assumes that the arguments of the binary relation are the last two explicit arguments.
|
||||
Everything else is assumed to be a parameter.
|
||||
*/
|
||||
relation_info const * get_relation_info(environment const & env, name const & rop);
|
||||
inline bool is_relation(environment const & env, name const & rop) { return get_relation_info(env, rop) != nullptr; }
|
||||
|
||||
typedef std::function<optional<relation_info>(name const &)> relation_info_getter;
|
||||
relation_info_getter mk_relation_info_getter(environment const & env);
|
||||
|
||||
/** \brief Return true iff \c e is of the form (lhs rop rhs) where rop is a registered relation. */
|
||||
bool is_relation(environment const & env, expr const & e, name & rop, expr & lhs, expr & rhs);
|
||||
typedef std::function<bool(expr const &, name &, expr &, expr &)> is_relation_pred; // NOLINT
|
||||
/** \brief Construct an \c is_relation predicate for the given environment. */
|
||||
is_relation_pred mk_is_relation_pred(environment const & env);
|
||||
|
||||
/** \brief Declare a new binary relation named \c n */
|
||||
environment add_relation(environment const & env, name const & n, bool persistent);
|
||||
|
||||
/** \brief Declare subst/refl/symm/trans lemmas for a binary relation,
|
||||
* it also declares the relation if it has not been declared yet */
|
||||
environment add_subst(environment const & env, name const & n, bool persistent);
|
||||
environment add_refl(environment const & env, name const & n, bool persistent);
|
||||
environment add_symm(environment const & env, name const & n, bool persistent);
|
||||
environment add_trans(environment const & env, name const & n, bool persistent);
|
||||
|
||||
struct relation_lemma_info {
|
||||
name m_name;
|
||||
unsigned m_num_univs;
|
||||
unsigned m_num_args;
|
||||
relation_lemma_info() {}
|
||||
relation_lemma_info(name const & n, unsigned nunivs, unsigned nargs):m_name(n), m_num_univs(nunivs), m_num_args(nargs) {}
|
||||
};
|
||||
|
||||
typedef relation_lemma_info refl_info;
|
||||
typedef relation_lemma_info symm_info;
|
||||
typedef relation_lemma_info subst_info;
|
||||
|
||||
struct trans_info : public relation_lemma_info {
|
||||
name m_res_relation;
|
||||
trans_info() {}
|
||||
trans_info(name const & n, unsigned nunivs, unsigned nargs, name const & rel):
|
||||
relation_lemma_info(n, nunivs, nargs), m_res_relation(rel) {}
|
||||
};
|
||||
|
||||
optional<subst_info> get_subst_extra_info(environment const & env, name const & op);
|
||||
optional<refl_info> get_refl_extra_info(environment const & env, name const & op);
|
||||
optional<symm_info> get_symm_extra_info(environment const & env, name const & op);
|
||||
optional<trans_info> get_trans_extra_info(environment const & env, name const & op1, name const & op2);
|
||||
optional<name> get_refl_info(environment const & env, name const & op);
|
||||
optional<name> get_symm_info(environment const & env, name const & op);
|
||||
optional<name> get_trans_info(environment const & env, name const & op);
|
||||
|
||||
typedef std::function<optional<refl_info>(name const &)> refl_info_getter;
|
||||
typedef std::function<optional<trans_info>(name const &, name const &)> trans_info_getter;
|
||||
typedef std::function<optional<symm_info>(name const &)> symm_info_getter;
|
||||
|
||||
refl_info_getter mk_refl_info_getter(environment const & env);
|
||||
trans_info_getter mk_trans_info_getter(environment const & env);
|
||||
symm_info_getter mk_symm_info_getter(environment const & env);
|
||||
|
||||
bool is_subst_relation(environment const & env, name const & op);
|
||||
inline bool is_trans_relation(environment const & env, name const & op) { return static_cast<bool>(get_trans_info(env, op)); }
|
||||
inline bool is_symm_relation(environment const & env, name const & op) { return static_cast<bool>(get_symm_info(env, op)); }
|
||||
inline bool is_refl_relation(environment const & env, name const & op) { return static_cast<bool>(get_refl_info(env, op)); }
|
||||
|
||||
void initialize_relation_manager();
|
||||
void finalize_relation_manager();
|
||||
}
|
||||
Loading…
Add table
Reference in a new issue