max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/meta): expose additional app_builder tactics

Browse source
This commit is contained in:
Leonardo de Moura 2017-01-20 20:27:07 -08:00
parent f079d05fc2
commit 4de71cadfa
7 changed files with 124 additions and 57 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

60
library/init/meta/congr_lemma.lean
View file

@ -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

4
library/init/meta/interactive.lean
View file

@ -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

4
library/init/meta/simp_tactic.lean
View file

@ -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 :=

16
library/init/meta/tactic.lean
View file

@ -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. -/

6
library/tools/super/simp.lean
View file

@ -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

51
src/library/tactic/app_builder_tactics.cpp
View file

@ -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() {

40
src/library/tactic/congr_lemma_tactics.cpp
View file

@ -39,70 +39,70 @@ static vm_obj mk_result(optional<congr_lemma> 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() {