From 46ed0ad6778f37b87ffbe664604656bfe59931cd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 8 Feb 2018 13:20:45 -0800 Subject: [PATCH] refactor(library/congr_lemma): remove `mk_rel_iff_congr_lemma` and `mk_rel_eq_congr_lemma` --- library/init/meta/congr_lemma.lean | 10 -- library/init/meta/congr_tactic.lean | 21 ---- library/init/meta/interactive.lean | 1 - src/library/congr_lemma.cpp | 106 +-------------------- src/library/congr_lemma.h | 15 +-- src/library/tactic/congr_lemma_tactics.cpp | 16 ---- tests/lean/run/congr_tactic.lean | 32 +------ 7 files changed, 5 insertions(+), 196 deletions(-) diff --git a/library/init/meta/congr_lemma.lean b/library/init/meta/congr_lemma.lean index 0ed9e623a6..d01038c5ae 100644 --- a/library/init/meta/congr_lemma.lean +++ b/library/init/meta/congr_lemma.lean @@ -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 diff --git a/library/init/meta/congr_tactic.lean b/library/init/meta/congr_tactic.lean index 49dfe671bf..fb5a267cf8 100644 --- a/library/init/meta/congr_tactic.lean +++ b/library/init/meta/congr_tactic.lean @@ -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 diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 8e6f9a987e..b2b206c743 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -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 diff --git a/src/library/congr_lemma.cpp b/src/library/congr_lemma.cpp index 31d6088d1b..7e68fcb6cf 100644 --- a/src/library/congr_lemma.cpp +++ b/src/library/congr_lemma.cpp @@ -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 mk_rel_congr(expr const & R, bool is_iff) { - try { - if (!is_constant(R)) - return optional(); - name const & R_name = const_name(R); - auto info = m_cache.m_relation_info_getter(R_name); - if (!info) - return optional(); - 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(r->second); - type_context::tmp_locals locals(m_ctx); - buffer hyps; - buffer 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(); - 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(res); - } catch (app_builder_exception &) { - trace_app_builder_failure(R); - return optional(); - } - } - - optional mk_rel_iff_congr(expr const & R) { - return mk_rel_congr(R, true); - } - - optional mk_rel_eq_congr(expr const & R) { - return mk_rel_congr(R, false); - } }; optional mk_congr_simp(type_context & ctx, expr const & fn) { @@ -746,14 +650,6 @@ optional mk_hcongr(type_context & ctx, expr const & fn, unsigned na return congr_lemma_manager(ctx).mk_hcongr(fn, nargs); } -optional mk_rel_iff_congr(type_context & ctx, expr const & R) { - return congr_lemma_manager(ctx).mk_rel_iff_congr(R); -} - -optional 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(); }); diff --git a/src/library/congr_lemma.h b/src/library/congr_lemma.h index 336b89dac6..125b5e96aa 100644 --- a/src/library/congr_lemma.h +++ b/src/library/congr_lemma.h @@ -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 mk_specialized_congr(type_context & ctx, expr const & a); optional mk_hcongr(type_context & ctx, expr const & fn); optional 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 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 mk_rel_eq_congr(type_context & ctx, expr const & R); - void initialize_congr_lemma(); void finalize_congr_lemma(); } diff --git a/src/library/tactic/congr_lemma_tactics.cpp b/src/library/tactic/congr_lemma_tactics.cpp index d5e83b2f55..a597680df5 100644 --- a/src/library/tactic/congr_lemma_tactics.cpp +++ b/src/library/tactic/congr_lemma_tactics.cpp @@ -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() { diff --git a/tests/lean/run/congr_tactic.lean b/tests/lean/run/congr_tactic.lean index a5ba2a7377..8ab1282d65 100644 --- a/tests/lean/run/congr_tactic.lean +++ b/tests/lean/run/congr_tactic.lean @@ -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