Zulip Chat Archive

Stream: general

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


view this post on Zulip 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.)

view this post on Zulip Reid Barton (Feb 02 2020 at 20:20):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 02 2020 at 21:38):

You should use tactic.apply

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Feb 02 2020 at 22:14):

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

view this post on Zulip Mario Carneiro (Feb 02 2020 at 22:14):

Other functions are more complicated because of universe parameters and such

view this post on Zulip 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.)

view this post on Zulip Mario Carneiro (Feb 02 2020 at 22:15):

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

view this post on Zulip Mario Carneiro (Feb 02 2020 at 22:15):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Feb 02 2020 at 22:16):

sure

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip Jason Rute (Feb 02 2020 at 22:18):

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

view this post on Zulip Mario Carneiro (Feb 02 2020 at 22:18):

there are non-interactive versions of all the tactics

view this post on Zulip Mario Carneiro (Feb 02 2020 at 22:19):

those are more suitable for use from programs and drivers

view this post on Zulip 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!

view this post on Zulip Mario Carneiro (Feb 02 2020 at 22:20):

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

view this post on Zulip 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