Specify `apply` and other tactics inside a tactic

Stream: general

[Jason Rute]

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]

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

[Reid Barton]

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

[Jason Rute]

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]

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

[Mario Carneiro]

You should use tactic.apply

[Mario Carneiro]

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

[Mario Carneiro]

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

[Jesse Michael Han]

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]

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

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

[Mario Carneiro]

Other functions are more complicated because of universe parameters and such

[Jason Rute]

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

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

[Mario Carneiro]

i.e. tactic.applyc ``true.intro

[Jason Rute]

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

[Mario Carneiro]

sure

[Jason Rute]

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

[Mario Carneiro]

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

[Jason Rute]

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

[Mario Carneiro]

there are non-interactive versions of all the tactics

[Mario Carneiro]

those are more suitable for use from programs and drivers

[Jason Rute]

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]

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

[Mario Carneiro]

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