refactor(library/congr_lemma): remove mk_rel_iff_congr_lemma and mk_rel_eq_congr_lemma
This commit is contained in:
Leonardo de Moura
parent
8f25f903da
commit
46ed0ad677
7 changed files with 5 additions and 196 deletions
|
|
@ -40,14 +40,4 @@ meta constant mk_specialized_congr_lemma (h : expr) (md := semireducible) : tact
|
|||
|
||||
meta constant mk_hcongr_lemma (h : expr) (nargs : option nat := none) (md := semireducible) : tactic congr_lemma
|
||||
|
||||
/- If R is an equivalence relation, construct the congruence lemma
|
||||
R a1 a2 -> R b1 b2 -> (R a1 b1) <-> (R a2 b2) -/
|
||||
meta constant mk_rel_iff_congr_lemma (h : expr) (md := semireducible) : tactic congr_lemma
|
||||
|
||||
/- Similar to mk_rel_iff_congr
|
||||
It fails if propext is not available.
|
||||
|
||||
R a1 a2 -> R b1 b2 -> (R a1 b1) = (R a2 b2) -/
|
||||
meta constant mk_rel_eq_congr_lemma (h : expr) (md := semireducible) : tactic congr_lemma
|
||||
|
||||
end tactic
|
||||
|
|
|
|||
|
|
@ -29,34 +29,13 @@ do try (applyc `eq_of_heq),
|
|||
clemma ← mk_hcongr_lemma lhs.get_app_fn lhs.get_app_num_args,
|
||||
apply_congr_core clemma
|
||||
|
||||
meta def apply_rel_iff_congr_core (tgt : expr) : tactic unit :=
|
||||
do (lhs, rhs) ← match_iff tgt,
|
||||
guard lhs.is_app,
|
||||
clemma ← mk_rel_iff_congr_lemma lhs.get_app_fn,
|
||||
apply_congr_core clemma
|
||||
|
||||
meta def apply_rel_eq_congr_core (tgt : expr) : tactic unit :=
|
||||
do (lhs, rhs) ← match_eq tgt,
|
||||
guard lhs.is_app,
|
||||
clemma ← mk_rel_eq_congr_lemma lhs.get_app_fn,
|
||||
apply_congr_core clemma
|
||||
|
||||
meta def congr_core : tactic unit :=
|
||||
do tgt ← target,
|
||||
apply_eq_congr_core tgt
|
||||
<|> apply_heq_congr_core
|
||||
<|> fail "congr tactic failed"
|
||||
|
||||
meta def rel_congr_core : tactic unit :=
|
||||
do tgt ← target,
|
||||
apply_rel_iff_congr_core tgt
|
||||
<|> apply_rel_eq_congr_core tgt
|
||||
<|> fail "rel_congr tactic failed"
|
||||
|
||||
meta def congr : tactic unit :=
|
||||
do focus1 (try assumption >> congr_core >> all_goals (try reflexivity >> try congr))
|
||||
|
||||
meta def rel_congr : tactic unit :=
|
||||
do focus1 (try assumption >> rel_congr_core >> all_goals (try reflexivity))
|
||||
|
||||
end tactic
|
||||
|
|
|
|||
|
|
@ -1534,7 +1534,6 @@ do e ← i_to_expr p,
|
|||
else tactic.fail "specialize requires a term of the form `h x_1 .. x_n` where `h` appears in the local context"
|
||||
|
||||
meta def congr := tactic.congr
|
||||
meta def rel_congr := tactic.rel_congr
|
||||
|
||||
end interactive
|
||||
end tactic
|
||||
|
|
|
|||
|
|
@ -31,11 +31,8 @@ struct congr_lemma_cache {
|
|||
cache m_cache;
|
||||
cache m_cache_spec;
|
||||
cache m_hcache;
|
||||
cache m_rel_cache[2];
|
||||
relation_info_getter m_relation_info_getter;
|
||||
congr_lemma_cache(environment const & env):
|
||||
m_env(env),
|
||||
m_relation_info_getter(mk_relation_info_getter(env)) {}
|
||||
m_env(env) {}
|
||||
environment const & env() const { return m_env; }
|
||||
};
|
||||
|
||||
|
|
@ -619,99 +616,6 @@ struct congr_lemma_manager {
|
|||
fun_info finfo = get_fun_info(m_ctx, fn);
|
||||
return mk_hcongr(fn, finfo.get_arity());
|
||||
}
|
||||
|
||||
/** \brief Given an equivalence relation \c R, create the congruence lemma
|
||||
|
||||
forall a1 a2 b1 b2, R a1 a2 -> R b1 b2 -> (R a1 b1 <-> R a2 b2)
|
||||
|
||||
If is_iff == false, then, it creates the lemma
|
||||
|
||||
forall a1 a2 b1 b2, R a1 a2 -> R b1 b2 -> (R a1 b1 = R a2 b2)
|
||||
|
||||
Propositional extensionality is used when is_iff == false */
|
||||
optional<result> mk_rel_congr(expr const & R, bool is_iff) {
|
||||
try {
|
||||
if (!is_constant(R))
|
||||
return optional<result>();
|
||||
name const & R_name = const_name(R);
|
||||
auto info = m_cache.m_relation_info_getter(R_name);
|
||||
if (!info)
|
||||
return optional<result>();
|
||||
unsigned arity = info->get_arity();
|
||||
key k(R, arity);
|
||||
auto r = m_cache.m_rel_cache[is_iff].find(k);
|
||||
if (r != m_cache.m_rel_cache[is_iff].end())
|
||||
return optional<result>(r->second);
|
||||
type_context::tmp_locals locals(m_ctx);
|
||||
buffer<expr> hyps;
|
||||
buffer<congr_arg_kind> kinds;
|
||||
expr a1, b1, a2, b2;
|
||||
expr H1, H2;
|
||||
expr R_type = infer(R);
|
||||
for (unsigned i = 0; i < arity; i++) {
|
||||
R_type = relaxed_whnf(R_type);
|
||||
if (!is_pi(R_type))
|
||||
return optional<result>();
|
||||
expr h = locals.push_local_from_binding(R_type);
|
||||
if (i == info->get_lhs_pos()) {
|
||||
a1 = h;
|
||||
a2 = locals.push_local_from_binding(R_type);
|
||||
H1 = locals.push_local("H1", mk_rel(m_ctx, R_name, a1, a2));
|
||||
hyps.push_back(a1);
|
||||
hyps.push_back(a2);
|
||||
hyps.push_back(H1);
|
||||
kinds.push_back(congr_arg_kind::Eq);
|
||||
} else if (i == info->get_rhs_pos()) {
|
||||
b1 = h;
|
||||
b2 = locals.push_local_from_binding(R_type);
|
||||
H2 = locals.push_local("H2", mk_rel(m_ctx, R_name, b1, b2));
|
||||
hyps.push_back(b1);
|
||||
hyps.push_back(b2);
|
||||
hyps.push_back(H2);
|
||||
kinds.push_back(congr_arg_kind::Eq);
|
||||
} else {
|
||||
hyps.push_back(h);
|
||||
kinds.push_back(congr_arg_kind::Fixed);
|
||||
}
|
||||
R_type = instantiate(binding_body(R_type), h);
|
||||
}
|
||||
expr lhs = mk_rel(m_ctx, R_name, a1, b1);
|
||||
expr rhs = mk_rel(m_ctx, R_name, a2, b2);
|
||||
// (H1 : R a1 a2) -> (H2 : R b1 b2) -> (R a1 b1 <-> R a2 b2)
|
||||
expr type = is_iff ? mk_iff(m_ctx, lhs, rhs) : mk_eq(m_ctx, lhs, rhs);
|
||||
type = m_ctx.mk_pi(hyps, type);
|
||||
/* Proof:
|
||||
iff.intro
|
||||
(λ H : R a1 b1, trans (symm H1) (trans H H2))
|
||||
(λ H : R a2 b2, trans H1 (trans H (symm H2)))
|
||||
*/
|
||||
expr H;
|
||||
H = locals.push_local("lhs", lhs);
|
||||
expr p1 = m_ctx.mk_lambda({H}, mk_trans(m_ctx, R_name, mk_symm(m_ctx, R_name, H1),
|
||||
mk_trans(m_ctx, R_name, H, H2)));
|
||||
H = locals.push_local("rhs", rhs);
|
||||
expr p2 = m_ctx.mk_lambda({H}, mk_trans(m_ctx, R_name, H1, mk_trans(m_ctx, R_name, H,
|
||||
mk_symm(m_ctx, R_name, H2))));
|
||||
expr pr = mk_app(m_ctx, get_iff_intro_name(), p1, p2);
|
||||
if (!is_iff)
|
||||
pr = mk_app(m_ctx, get_propext_name(), pr);
|
||||
pr = m_ctx.mk_lambda(hyps, pr);
|
||||
result res(type, pr, to_list(kinds));
|
||||
m_cache.m_rel_cache[is_iff].insert(mk_pair(k, res));
|
||||
return optional<result>(res);
|
||||
} catch (app_builder_exception &) {
|
||||
trace_app_builder_failure(R);
|
||||
return optional<result>();
|
||||
}
|
||||
}
|
||||
|
||||
optional<result> mk_rel_iff_congr(expr const & R) {
|
||||
return mk_rel_congr(R, true);
|
||||
}
|
||||
|
||||
optional<result> mk_rel_eq_congr(expr const & R) {
|
||||
return mk_rel_congr(R, false);
|
||||
}
|
||||
};
|
||||
|
||||
optional<congr_lemma> mk_congr_simp(type_context & ctx, expr const & fn) {
|
||||
|
|
@ -746,14 +650,6 @@ optional<congr_lemma> mk_hcongr(type_context & ctx, expr const & fn, unsigned na
|
|||
return congr_lemma_manager(ctx).mk_hcongr(fn, nargs);
|
||||
}
|
||||
|
||||
optional<congr_lemma> mk_rel_iff_congr(type_context & ctx, expr const & R) {
|
||||
return congr_lemma_manager(ctx).mk_rel_iff_congr(R);
|
||||
}
|
||||
|
||||
optional<congr_lemma> mk_rel_eq_congr(type_context & ctx, expr const & R) {
|
||||
return congr_lemma_manager(ctx).mk_rel_eq_congr(R);
|
||||
}
|
||||
|
||||
void initialize_congr_lemma() {
|
||||
register_trace_class("congr_lemma");
|
||||
register_thread_local_reset_fn([]() { get_clch().clear(); });
|
||||
|
|
|
|||
|
|
@ -5,9 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include "library/type_context.h"
|
||||
#include "kernel/expr.h"
|
||||
|
||||
namespace lean {
|
||||
class type_context;
|
||||
|
||||
enum class congr_arg_kind {
|
||||
/* It is a parameter for the congruence lemma, the parameter occurs in the left and right hand sides. */
|
||||
Fixed,
|
||||
|
|
@ -51,17 +53,6 @@ optional<congr_lemma> mk_specialized_congr(type_context & ctx, expr const & a);
|
|||
optional<congr_lemma> mk_hcongr(type_context & ctx, expr const & fn);
|
||||
optional<congr_lemma> mk_hcongr(type_context & ctx, expr const & fn, unsigned nargs);
|
||||
|
||||
/** \brief If R is an equivalence relation, construct the congruence lemma
|
||||
|
||||
R a1 a2 -> R b1 b2 -> (R a1 b1) <-> (R a2 b2) */
|
||||
optional<congr_lemma> mk_rel_iff_congr(type_context & ctx, expr const & R);
|
||||
|
||||
/** \brief Similar to previous one.
|
||||
It returns none if propext is not available.
|
||||
|
||||
R a1 a2 -> R b1 b2 -> (R a1 b1) = (R a2 b2) */
|
||||
optional<congr_lemma> mk_rel_eq_congr(type_context & ctx, expr const & R);
|
||||
|
||||
void initialize_congr_lemma();
|
||||
void finalize_congr_lemma();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -87,28 +87,12 @@ vm_obj tactic_mk_hcongr_lemma(vm_obj const & fn, vm_obj const & nargs, vm_obj co
|
|||
CATCH;
|
||||
}
|
||||
|
||||
vm_obj tactic_mk_rel_iff_congr_lemma(vm_obj const & r, vm_obj const & m, vm_obj const & s) {
|
||||
TRY;
|
||||
type_context ctx = mk_type_context_for(s, m);
|
||||
return mk_result(mk_rel_iff_congr(ctx, to_expr(r)), s);
|
||||
CATCH;
|
||||
}
|
||||
|
||||
vm_obj tactic_mk_rel_eq_congr_lemma(vm_obj const & r, vm_obj const & m, vm_obj const & s) {
|
||||
TRY;
|
||||
type_context ctx = mk_type_context_for(s, m);
|
||||
return mk_result(mk_rel_eq_congr(ctx, to_expr(r)), s);
|
||||
CATCH;
|
||||
}
|
||||
|
||||
void initialize_congr_lemma_tactics() {
|
||||
DECLARE_VM_BUILTIN(name({"tactic", "mk_congr_lemma_simp"}), tactic_mk_congr_lemma_simp);
|
||||
DECLARE_VM_BUILTIN(name({"tactic", "mk_specialized_congr_lemma_simp"}), tactic_mk_specialized_congr_lemma_simp);
|
||||
DECLARE_VM_BUILTIN(name({"tactic", "mk_congr_lemma"}), tactic_mk_congr_lemma);
|
||||
DECLARE_VM_BUILTIN(name({"tactic", "mk_specialized_congr_lemma"}), tactic_mk_specialized_congr_lemma);
|
||||
DECLARE_VM_BUILTIN(name({"tactic", "mk_hcongr_lemma"}), tactic_mk_hcongr_lemma);
|
||||
DECLARE_VM_BUILTIN(name({"tactic", "mk_rel_iff_congr_lemma"}), tactic_mk_rel_iff_congr_lemma);
|
||||
DECLARE_VM_BUILTIN(name({"tactic", "mk_rel_eq_congr_lemma"}), tactic_mk_rel_eq_congr_lemma);
|
||||
}
|
||||
|
||||
void finalize_congr_lemma_tactics() {
|
||||
|
|
|
|||
|
|
@ -72,36 +72,6 @@ end
|
|||
end test5
|
||||
|
||||
namespace test6
|
||||
-- iff relation
|
||||
|
||||
constants (α : Type*)
|
||||
(R : α → α → Prop)
|
||||
(R_refl : ∀ x, R x x)
|
||||
(R_symm : ∀ x y, R x y → R y x)
|
||||
(R_trans : ∀ x y z, R x y → R y z → R x z)
|
||||
|
||||
attribute [refl] R_refl
|
||||
attribute [symm] R_symm
|
||||
attribute [trans] R_trans
|
||||
|
||||
example (x₁ x₁' x₂ x₂' : α) (H₁ : R x₁ x₁') (H₂ : R x₂ x₂') : R x₁ x₂ ↔ R x₁' x₂' :=
|
||||
begin
|
||||
rel_congr,
|
||||
exact H₁,
|
||||
exact H₂
|
||||
end
|
||||
|
||||
-- eq relation
|
||||
example (x₁ x₁' x₂ x₂' : α) (H₁ : R x₁ x₁') (H₂ : R x₂ x₂') : R x₁ x₂ = R x₁' x₂' :=
|
||||
begin
|
||||
rel_congr,
|
||||
exact H₁,
|
||||
exact H₂
|
||||
end
|
||||
|
||||
end test6
|
||||
|
||||
namespace test7
|
||||
|
||||
variables (A : Type) (B : A → Type) (a a' : A) (b : B a) (b' : B a')
|
||||
|
||||
|
|
@ -112,4 +82,4 @@ begin
|
|||
show b == b', from sorry,
|
||||
end
|
||||
|
||||
end test7
|
||||
end test6
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue