## Stream: general

### Topic: Specify apply and other tactics inside a tactic

#### Jason Rute (Feb 02 2020 at 19:24):

I have a question about calling tactics in meta programming. I'm making an AI* which will control certain common tactics (like apply, simp, rw, ...). How within my own custom tactic (say within a do ... return () block), do I say to run the apply tactic? The issue is the parameter. Here are three use cases. How do I do them?

1. apply h where h is from the local context. I know how to access and look at the (the expressions of the) local context. So let's assume I know which hypothesis h I want to use in apply. How do I specify that inside a tactic?
2. apply true.intro where true.intro is just an example of a theorem in the environment. Let's say I already know the name of that theorem, e.g. true.intro. How do I apply it?
3. apply (f h) where f h is an example of a compound term. Again, let's say I know how to find f and h and they are either in the local context or the environment.

If (3) is much harder, I am happy with solutions to (1) or (2). Do the same basic ideas apply for tactics which takes lists of terms like rw or simp?

*When I say "I am making an AI", what I really mean is that I am making a prototype of a tool which lets one control tactics from outside of Lean. I'm trying to do it through Lean's IO and not the Lean server, hence the questions. (See more here about this project.)

#### Reid Barton (Feb 02 2020 at 20:20):

For 2, if I understand correctly, you could use  [apply true.intro] 

#### Reid Barton (Feb 02 2020 at 20:22):

For 1, or more generally, you can just apply tactic.apply or even tactic.interactive.apply directly

#### Jason Rute (Feb 02 2020 at 21:35):

Let me be more clear. This will be done entirely programmatically and dynamically. I assume I can't enter  [apply n] , where n is a name/expr/other?

#### Jason Rute (Feb 02 2020 at 21:35):

Anyway, I'm looking at this set of notes: https://github.com/leanprover-community/mathlib/blob/master/docs/extras/tactic_writing.md

#### Mario Carneiro (Feb 02 2020 at 21:38):

You should use tactic.apply

#### Mario Carneiro (Feb 02 2020 at 21:38):

it takes an argument of type expr, which you can construct from any of the mentioned sources

#### Mario Carneiro (Feb 02 2020 at 21:40):

the interactive apply tactic is just a shim over tactic.apply that parses the input pre-expression first

#### Jesse Michael Han (Feb 02 2020 at 21:41):

assuming "I know which hypothesis h" means a predicate pred : expr -> tactic bool, you can try something like this:

namespace tactic
namespace interactive

meta def try_apply_pred (pred : expr → tactic bool) : tactic unit :=
let try_trace_apply : expr → tactic unit :=
λ e, tactic.apply e *> tactic.trace format!"applied {e.to_string}" <|>
tactic.trace format!"failed to apply {e.to_string}" in
local_context >>= list.mfilter pred >>= list.mfoldl (λ _ e, try_trace_apply e) ()

end interactive
end tactic

example (H₁ : false → true) (H₂ : true → true) : true :=
begin
-- H : false → true
-- ⊢ true
try_apply_pred (λ _, return true),
-- H : false → true
-- ⊢ false
end


#### Jason Rute (Feb 02 2020 at 22:13):

@Mario Carneiro Where I am struggling is that expr is a very broad category of objects. What form does the expression need to be in? For example, what expression would I use for true.intro? How do I get that from its declaration?

#### Mario Carneiro (Feb 02 2020 at 22:14):

true.intro has no arguments, so  (true.intro) suffices

#### Mario Carneiro (Feb 02 2020 at 22:14):

Other functions are more complicated because of universe parameters and such

#### Jason Rute (Feb 02 2020 at 22:15):

@Jesse Michael Han, thanks! I think that gives me the answer for (1). I use tactic.apply e where e is the object from the local context. (I think it is of the form local_const.)

#### Mario Carneiro (Feb 02 2020 at 22:15):

there is also tactic.applyc which takes a name that refers to a constant

#### Mario Carneiro (Feb 02 2020 at 22:15):

i.e. tactic.applyc true.intro

#### Jason Rute (Feb 02 2020 at 22:16):

@Mario Carneiro So let's say, I'm willing to loop over all thm declarations and try apply with all of them, would tactic.applyc nm where nm is the name from the declaration be the right approach?

sure

#### Jason Rute (Feb 02 2020 at 22:17):

(Obviously, I'm not going to do that loop, but that is the idea I'm looking for.)

#### Mario Carneiro (Feb 02 2020 at 22:17):

note that if it is successful, you need to be sure to revert the state afterward if you want to backtrack

#### Jason Rute (Feb 02 2020 at 22:18):

This covers apply. Is there a general principle for other tactics like rw?

#### Mario Carneiro (Feb 02 2020 at 22:18):

there are non-interactive versions of all the tactics

#### Mario Carneiro (Feb 02 2020 at 22:19):

those are more suitable for use from programs and drivers

#### Jason Rute (Feb 02 2020 at 22:19):

Ok. I think I'm going to just need to experiment and look a the code (when it is not in C++). Thanks!

#### Mario Carneiro (Feb 02 2020 at 22:20):

Check out init.meta.tactic for the list of core tactics

#### Mario Carneiro (Feb 02 2020 at 22:21):

it's not comprehensive though; there are other files that define more core tactics, and some non-builtin tactics are also probably worth treating atomically like simp`

Last updated: May 15 2021 at 02:11 UTC