From 4de71cadfa8cd6356899300629bbb0d6710d45e4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 20 Jan 2017 20:27:07 -0800 Subject: [PATCH] feat(library/init/meta): expose additional app_builder tactics --- library/init/meta/congr_lemma.lean | 60 +++++++++++----------- library/init/meta/interactive.lean | 4 +- library/init/meta/simp_tactic.lean | 4 +- library/init/meta/tactic.lean | 16 ++++++ library/tools/super/simp.lean | 6 +-- src/library/tactic/app_builder_tactics.cpp | 51 ++++++++++++++++++ src/library/tactic/congr_lemma_tactics.cpp | 40 +++++++-------- 7 files changed, 124 insertions(+), 57 deletions(-) diff --git a/library/init/meta/congr_lemma.lean b/library/init/meta/congr_lemma.lean index 7d90a613fa..d2445a316d 100644 --- a/library/init/meta/congr_lemma.lean +++ b/library/init/meta/congr_lemma.lean @@ -26,57 +26,57 @@ meta structure congr_lemma := (type : expr) (proof : expr) (arg_kinds : list congr_arg_kind) namespace tactic -meta constant mk_congr_simp_core : transparency → expr → tactic congr_lemma -meta constant mk_congr_simp_n_core : transparency → expr → nat → tactic congr_lemma +meta constant mk_congr_lemma_simp_core : transparency → expr → tactic congr_lemma +meta constant mk_congr_lemma_simp_n_core : transparency → expr → nat → tactic congr_lemma /- Create a specialized theorem using (a prefix of) the arguments of the given application. -/ -meta constant mk_specialized_congr_simp_core : transparency → expr → tactic congr_lemma +meta constant mk_specialized_congr_lemma_simp_core : transparency → expr → tactic congr_lemma -meta constant mk_congr_core : transparency → expr → tactic congr_lemma -meta constant mk_congr_n_core : transparency → expr → nat → tactic congr_lemma +meta constant mk_congr_lemma_core : transparency → expr → tactic congr_lemma +meta constant mk_congr_lemma_n_core : transparency → expr → nat → tactic congr_lemma /- Create a specialized theorem using (a prefix of) the arguments of the given application. -/ -meta constant mk_specialized_congr_core : transparency → expr → tactic congr_lemma +meta constant mk_specialized_congr_lemma_core : transparency → expr → tactic congr_lemma -meta constant mk_hcongr_core : transparency → expr → tactic congr_lemma -meta constant mk_hcongr_n_core : transparency → expr → nat → tactic congr_lemma +meta constant mk_hcongr_lemma_core : transparency → expr → tactic congr_lemma +meta constant mk_hcongr_lemma_n_core : transparency → expr → nat → 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_core : transparency → expr → tactic congr_lemma +meta constant mk_rel_iff_congr_lemma_core : transparency → expr → 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_core : transparency → expr → tactic congr_lemma +meta constant mk_rel_eq_congr_lemma_core : transparency → expr → tactic congr_lemma -meta def mk_congr_simp : expr → tactic congr_lemma := -mk_congr_simp_core semireducible +meta def mk_congr_lemma_simp : expr → tactic congr_lemma := +mk_congr_lemma_simp_core semireducible -meta def mk_congr_simp_n : expr → nat → tactic congr_lemma := -mk_congr_simp_n_core semireducible +meta def mk_congr_lemma_simp_n : expr → nat → tactic congr_lemma := +mk_congr_lemma_simp_n_core semireducible -meta def mk_specialized_congr_simp : expr → tactic congr_lemma := -mk_specialized_congr_simp_core semireducible +meta def mk_specialized_congr_lemma_simp : expr → tactic congr_lemma := +mk_specialized_congr_lemma_simp_core semireducible -meta def mk_congr : expr → tactic congr_lemma := -mk_congr_core semireducible +meta def mk_congr_lemma : expr → tactic congr_lemma := +mk_congr_lemma_core semireducible -meta def mk_congr_n : expr → nat → tactic congr_lemma := -mk_congr_n_core semireducible +meta def mk_congr_lemma_n : expr → nat → tactic congr_lemma := +mk_congr_lemma_n_core semireducible -meta def mk_specialized_congr : expr → tactic congr_lemma := -mk_specialized_congr_core semireducible +meta def mk_specialized_congr_lemma : expr → tactic congr_lemma := +mk_specialized_congr_lemma_core semireducible -meta def mk_hcongr : expr → tactic congr_lemma := -mk_hcongr_core semireducible +meta def mk_hcongr_lemma : expr → tactic congr_lemma := +mk_hcongr_lemma_core semireducible -meta def mk_hcongr_n : expr → nat → tactic congr_lemma := -mk_hcongr_n_core semireducible +meta def mk_hcongr_lemma_n : expr → nat → tactic congr_lemma := +mk_hcongr_lemma_n_core semireducible -meta def mk_rel_iff_congr : expr → tactic congr_lemma := -mk_rel_iff_congr_core semireducible +meta def mk_rel_iff_congr_lemma : expr → tactic congr_lemma := +mk_rel_iff_congr_lemma_core semireducible -meta def mk_rel_eq_congr : expr → tactic congr_lemma := -mk_rel_eq_congr_core semireducible +meta def mk_rel_eq_congr_lemma : expr → tactic congr_lemma := +mk_rel_eq_congr_lemma_core semireducible end tactic diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 1dc15384de..8c1e78a5eb 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -358,14 +358,14 @@ private meta def simp_goal (cfg : simplify_config) : simp_lemmas → tactic unit (new_target, Heq) ← target >>= simplify_core cfg s `eq, tactic.assert `Htarget new_target, swap, Ht ← get_local `Htarget, - mk_app `eq.mpr [Heq, Ht] >>= tactic.exact + mk_eq_mpr Heq Ht >>= tactic.exact private meta def simp_hyp (cfg : simplify_config) (s : simp_lemmas) (h_name : name) : tactic unit := do h ← get_local h_name, htype ← infer_type h, (new_htype, eqpr) ← simplify_core cfg s `eq htype, tactic.assert (expr.local_pp_name h) new_htype, - mk_app `eq.mp [eqpr, h] >>= tactic.exact, + mk_eq_mp eqpr h >>= tactic.exact, try $ tactic.clear h private meta def simp_hyps (cfg : simplify_config) : simp_lemmas → location → tactic unit diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean index 22b36a6f00..b8af80979c 100644 --- a/library/init/meta/simp_tactic.lean +++ b/library/init/meta/simp_tactic.lean @@ -211,7 +211,7 @@ meta def simplify_goal_core (cfg : simplify_config) (S : simp_lemmas) : tactic u do (new_target, heq) ← target >>= simplify cfg S, assert `htarget new_target, swap, ht ← get_local `htarget, - mk_app `eq.mpr [heq, ht] >>= exact + mk_eq_mpr heq ht >>= exact meta def simplify_goal (S : simp_lemmas) : tactic unit := simplify_goal_core default_simplify_config S @@ -274,7 +274,7 @@ do when (expr.is_local_constant h = ff) (fail "tactic simp_at failed, the given S ← S^.append extra_lemmas, (new_htype, heq) ← simplify default_simplify_config S htype, assert (expr.local_pp_name h) new_htype, - mk_app `eq.mp [heq, h] >>= exact, + mk_eq_mp heq h >>= exact, try $ clear h meta def simp_at : expr → tactic unit := diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index fdf2ba9b0a..611382245e 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -299,6 +299,22 @@ meta constant mk_app_core : transparency → name → list expr → tactic exp returns the application @ite.{1} (a > b) (nat.decidable_gt a b) nat a b -/ meta constant mk_mapp_core : transparency → name → list (option expr) → tactic expr +/-- (mk_congr_arg h₁ h₂) is a more efficient version of (mk_app `congr_arg [h₁, h₂]) -/ +meta constant mk_congr_arg : expr → expr → tactic expr +/-- (mk_congr_fun h₁ h₂) is a more efficient version of (mk_app `congr_fun [h₁, h₂]) -/ +meta constant mk_congr_fun : expr → expr → tactic expr +/-- (mk_congr h₁ h₂) is a more efficient version of (mk_app `congr [h₁, h₂]) -/ +meta constant mk_congr : expr → expr → tactic expr +/-- (mk_eq_refl h) is a more efficient version of (mk_app `eq.refl [h]) -/ +meta constant mk_eq_refl : expr → tactic expr +/-- (mk_eq_symm h) is a more efficient version of (mk_app `eq.symm [h]) -/ +meta constant mk_eq_symm : expr → tactic expr +/-- (mk_eq_trans h₁ h₂) is a more efficient version of (mk_app `eq.trans [h₁, h₂]) -/ +meta constant mk_eq_trans : expr → expr → tactic expr +/-- (mk_eq_mp h₁ h₂) is a more efficient version of (mk_app `eq.mp [h₁, h₂]) -/ +meta constant mk_eq_mp : expr → expr → tactic expr +/-- (mk_eq_mpr h₁ h₂) is a more efficient version of (mk_app `eq.mpr [h₁, h₂]) -/ +meta constant mk_eq_mpr : expr → expr → tactic expr /- Given a local constant t, if t has type (lhs = rhs) apply susbstitution. Otherwise, try to find a local constant that has type of the form (t = t') or (t' = t). The tactic fails if the given expression is not a local constant. -/ diff --git a/library/tools/super/simp.lean b/library/tools/super/simp.lean index 3d6d3ca793..b9e808872a 100644 --- a/library/tools/super/simp.lean +++ b/library/tools/super/simp.lean @@ -25,15 +25,15 @@ meta def try_simplify_left (c : clause) (i : ℕ) : tactic (list clause) := on_left_at c i $ λtype, do (type', heq, add_hyps) ← simplify_capturing_assumptions type, hyp ← mk_local_def `h type', - prf ← mk_app ``eq.mpr [heq, hyp], + prf ← mk_eq_mpr heq hyp, return [(hyp::add_hyps, prf)] meta def try_simplify_right (c : clause) (i : ℕ) : tactic (list clause) := on_right_at' c i $ λhyp, do (type', heq, add_hyps) ← simplify_capturing_assumptions hyp^.local_type, heqtype ← infer_type heq, - heqsymm ← mk_app ``eq.symm [heq], - prf ← mk_app ``eq.mpr [heqsymm, hyp], + heqsymm ← mk_eq_symm heq, + prf ← mk_eq_mpr heqsymm hyp, return [(add_hyps, prf)] meta def simp_inf : inf_decl := inf_decl.mk 40 $ take given, sequence' $ do diff --git a/src/library/tactic/app_builder_tactics.cpp b/src/library/tactic/app_builder_tactics.cpp index 175d001c4d..d847ee3ec5 100644 --- a/src/library/tactic/app_builder_tactics.cpp +++ b/src/library/tactic/app_builder_tactics.cpp @@ -26,6 +26,49 @@ vm_obj tactic_mk_app_core(vm_obj const & tmode, vm_obj const & c, vm_obj const & } } +#define MK_APP(CODE) { \ + tactic_state const & s = to_tactic_state(_s); \ + try { \ + type_context ctx = mk_type_context_for(s); \ + expr r = CODE; \ + return mk_tactic_success(to_obj(r), s); \ + } catch (exception & ex) { \ + return mk_tactic_exception(ex, s); \ + } \ +} + +vm_obj tactic_mk_congr_arg(vm_obj const & f, vm_obj const & H, vm_obj const & _s) { + MK_APP(mk_congr_arg(ctx, to_expr(f), to_expr(H))); +} + +vm_obj tactic_mk_congr_fun(vm_obj const & H, vm_obj const & a, vm_obj const & _s) { + MK_APP(mk_congr_fun(ctx, to_expr(H), to_expr(a))); +} + +vm_obj tactic_mk_congr(vm_obj const & H1, vm_obj const & H2, vm_obj const & _s) { + MK_APP(mk_congr(ctx, to_expr(H1), to_expr(H2))); +} + +vm_obj tactic_mk_eq_refl(vm_obj const & a, vm_obj const & _s) { + MK_APP(mk_eq_refl(ctx, to_expr(a))); +} + +vm_obj tactic_mk_eq_symm(vm_obj const & h, vm_obj const & _s) { + MK_APP(mk_eq_symm(ctx, to_expr(h))); +} + +vm_obj tactic_mk_eq_trans(vm_obj const & h1, vm_obj const & h2, vm_obj const & _s) { + MK_APP(mk_eq_trans(ctx, to_expr(h1), to_expr(h2))); +} + +vm_obj tactic_mk_eq_mpr(vm_obj const & h1, vm_obj const & h2, vm_obj const & _s) { + MK_APP(mk_eq_mpr(ctx, to_expr(h1), to_expr(h2))); +} + +vm_obj tactic_mk_eq_mp(vm_obj const & h1, vm_obj const & h2, vm_obj const & _s) { + MK_APP(mk_eq_mp(ctx, to_expr(h1), to_expr(h2))); +} + vm_obj tactic_mk_mapp_core(vm_obj const & tmode, vm_obj const & c, vm_obj const & as, vm_obj const & _s) { tactic_state const & s = to_tactic_state(_s); try { @@ -53,6 +96,14 @@ vm_obj tactic_mk_mapp_core(vm_obj const & tmode, vm_obj const & c, vm_obj const void initialize_app_builder_tactics() { DECLARE_VM_BUILTIN(name({"tactic", "mk_app_core"}), tactic_mk_app_core); DECLARE_VM_BUILTIN(name({"tactic", "mk_mapp_core"}), tactic_mk_mapp_core); + DECLARE_VM_BUILTIN(name({"tactic", "mk_congr_arg"}), tactic_mk_congr_arg); + DECLARE_VM_BUILTIN(name({"tactic", "mk_congr_fun"}), tactic_mk_congr_fun); + DECLARE_VM_BUILTIN(name({"tactic", "mk_congr"}), tactic_mk_congr); + DECLARE_VM_BUILTIN(name({"tactic", "mk_eq_refl"}), tactic_mk_eq_refl); + DECLARE_VM_BUILTIN(name({"tactic", "mk_eq_symm"}), tactic_mk_eq_symm); + DECLARE_VM_BUILTIN(name({"tactic", "mk_eq_trans"}), tactic_mk_eq_trans); + DECLARE_VM_BUILTIN(name({"tactic", "mk_eq_mp"}), tactic_mk_eq_mp); + DECLARE_VM_BUILTIN(name({"tactic", "mk_eq_mpr"}), tactic_mk_eq_mpr); } void finalize_app_builder_tactics() { diff --git a/src/library/tactic/congr_lemma_tactics.cpp b/src/library/tactic/congr_lemma_tactics.cpp index fd1edfe095..7e9c4c66b5 100644 --- a/src/library/tactic/congr_lemma_tactics.cpp +++ b/src/library/tactic/congr_lemma_tactics.cpp @@ -39,70 +39,70 @@ static vm_obj mk_result(optional const & l, vm_obj const & s) { #define TRY LEAN_TACTIC_TRY #define CATCH LEAN_TACTIC_CATCH(to_tactic_state(s)) -vm_obj tactic_mk_congr_simp(vm_obj const & m, vm_obj const & fn, vm_obj const & s) { +vm_obj tactic_mk_congr_lemma_simp(vm_obj const & m, vm_obj const & fn, vm_obj const & s) { TRY; type_context ctx = mk_type_context_for(s, m); return mk_result(mk_congr_simp(ctx, to_expr(fn)), s); CATCH; } -vm_obj tactic_mk_congr_simp_n(vm_obj const & m, vm_obj const & fn, vm_obj const & n, vm_obj const & s) { +vm_obj tactic_mk_congr_lemma_simp_n(vm_obj const & m, vm_obj const & fn, vm_obj const & n, vm_obj const & s) { TRY; type_context ctx = mk_type_context_for(s, m); return mk_result(mk_congr_simp(ctx, to_expr(fn), force_to_unsigned(n, 0)), s); CATCH; } -vm_obj tactic_mk_specialized_congr_simp(vm_obj const & m, vm_obj const & a, vm_obj const & s) { +vm_obj tactic_mk_specialized_congr_lemma_simp(vm_obj const & m, vm_obj const & a, vm_obj const & s) { TRY; type_context ctx = mk_type_context_for(s, m); return mk_result(mk_specialized_congr_simp(ctx, to_expr(a)), s); CATCH; } -vm_obj tactic_mk_congr(vm_obj const & m, vm_obj const & fn, vm_obj const & s) { +vm_obj tactic_mk_congr_lemma(vm_obj const & m, vm_obj const & fn, vm_obj const & s) { TRY; type_context ctx = mk_type_context_for(s, m); return mk_result(mk_congr(ctx, to_expr(fn)), s); CATCH; } -vm_obj tactic_mk_congr_n(vm_obj const & m, vm_obj const & fn, vm_obj const & n, vm_obj const & s) { +vm_obj tactic_mk_congr_lemma_n(vm_obj const & m, vm_obj const & fn, vm_obj const & n, vm_obj const & s) { TRY; type_context ctx = mk_type_context_for(s, m); return mk_result(mk_congr(ctx, to_expr(fn), force_to_unsigned(n, 0)), s); CATCH; } -vm_obj tactic_mk_specialized_congr(vm_obj const & m, vm_obj const & a, vm_obj const & s) { +vm_obj tactic_mk_specialized_congr_lemma(vm_obj const & m, vm_obj const & a, vm_obj const & s) { TRY; type_context ctx = mk_type_context_for(s, m); return mk_result(mk_specialized_congr(ctx, to_expr(a)), s); CATCH; } -vm_obj tactic_mk_hcongr(vm_obj const & m, vm_obj const & fn, vm_obj const & s) { +vm_obj tactic_mk_hcongr_lemma(vm_obj const & m, vm_obj const & fn, vm_obj const & s) { TRY; type_context ctx = mk_type_context_for(s, m); return mk_result(mk_hcongr(ctx, to_expr(fn)), s); CATCH; } -vm_obj tactic_mk_hcongr_n(vm_obj const & m, vm_obj const & fn, vm_obj const & n, vm_obj const & s) { +vm_obj tactic_mk_hcongr_lemma_n(vm_obj const & m, vm_obj const & fn, vm_obj const & n, vm_obj const & s) { TRY; type_context ctx = mk_type_context_for(s, m); return mk_result(mk_hcongr(ctx, to_expr(fn), force_to_unsigned(n, 0)), s); CATCH; } -vm_obj tactic_mk_rel_iff_congr(vm_obj const & m, vm_obj const & r, vm_obj const & s) { +vm_obj tactic_mk_rel_iff_congr_lemma(vm_obj const & m, vm_obj const & r, 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(vm_obj const & m, vm_obj const & r, vm_obj const & s) { +vm_obj tactic_mk_rel_eq_congr_lemma(vm_obj const & m, vm_obj const & r, 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); @@ -110,16 +110,16 @@ vm_obj tactic_mk_rel_eq_congr(vm_obj const & m, vm_obj const & r, vm_obj const & } void initialize_congr_lemma_tactics() { - DECLARE_VM_BUILTIN(name({"tactic", "mk_congr_simp_core"}), tactic_mk_congr_simp); - DECLARE_VM_BUILTIN(name({"tactic", "mk_congr_simp_n_core"}), tactic_mk_congr_simp_n); - DECLARE_VM_BUILTIN(name({"tactic", "mk_specialized_congr_simp_core"}), tactic_mk_specialized_congr_simp); - DECLARE_VM_BUILTIN(name({"tactic", "mk_congr_core"}), tactic_mk_congr); - DECLARE_VM_BUILTIN(name({"tactic", "mk_congr_n_core"}), tactic_mk_congr_n); - DECLARE_VM_BUILTIN(name({"tactic", "mk_specialized_congr_core"}), tactic_mk_specialized_congr); - DECLARE_VM_BUILTIN(name({"tactic", "mk_hcongr_core"}), tactic_mk_hcongr); - DECLARE_VM_BUILTIN(name({"tactic", "mk_hcongr_n_core"}), tactic_mk_hcongr_n); - DECLARE_VM_BUILTIN(name({"tactic", "mk_rel_iff_congr_core"}), tactic_mk_rel_iff_congr); - DECLARE_VM_BUILTIN(name({"tactic", "mk_rel_eq_congr_core"}), tactic_mk_rel_eq_congr); + DECLARE_VM_BUILTIN(name({"tactic", "mk_congr_lemma_simp_core"}), tactic_mk_congr_lemma_simp); + DECLARE_VM_BUILTIN(name({"tactic", "mk_congr_lemma_simp_n_core"}), tactic_mk_congr_lemma_simp_n); + DECLARE_VM_BUILTIN(name({"tactic", "mk_specialized_congr_lemma_simp_core"}), tactic_mk_specialized_congr_lemma_simp); + DECLARE_VM_BUILTIN(name({"tactic", "mk_congr_lemma_core"}), tactic_mk_congr_lemma); + DECLARE_VM_BUILTIN(name({"tactic", "mk_congr_lemma_n_core"}), tactic_mk_congr_lemma_n); + DECLARE_VM_BUILTIN(name({"tactic", "mk_specialized_congr_lemma_core"}), tactic_mk_specialized_congr_lemma); + DECLARE_VM_BUILTIN(name({"tactic", "mk_hcongr_lemma_core"}), tactic_mk_hcongr_lemma); + DECLARE_VM_BUILTIN(name({"tactic", "mk_hcongr_lemma_n_core"}), tactic_mk_hcongr_lemma_n); + DECLARE_VM_BUILTIN(name({"tactic", "mk_rel_iff_congr_lemma_core"}), tactic_mk_rel_iff_congr_lemma); + DECLARE_VM_BUILTIN(name({"tactic", "mk_rel_eq_congr_lemma_core"}), tactic_mk_rel_eq_congr_lemma); } void finalize_congr_lemma_tactics() {