Zulip Chat Archive

Stream: general

Topic: an unsafe version of tactic


Edward Ayers (May 20 2019 at 11:41):

Hello all, I've been playing with Lean 3's source a lot recently and I am toying with exposing some of the datastructures that Lean uses to implement the tactic monad. For example metavar_context, local_context, type_context_old.

Afaik, the reason why these are not available in the Lean VM is:
1. there are some caching optimisations in tactic that will be hard to get right if you are allowed to see its guts.
2. the abstraction offered by tactic is that it is very hard for the result expression to be badly typed according to the kernel. That is, if I only use tactic builtins and it succeeds, then it is highly likely that I won't have a strange type error in the declaration.
3. The user model gets more complicated, you have not only metavariables but temporary metavariables which live in special scopes and so on.
However, some of my automation projects could be made much faster and easier to write by working with these deeper constructs instead of through tactic. For example I want to hold lots of different metavariable contexts and be able to unify terms within specific contexts, which is what temporary mvars were invented for. At the moment I do this by having lots of tactic_states flying around, but this is bad for caching since the cache resets every time you use <|> so unification is really slow. I would also love to be able to add locals directly to the context and use delayed abstraction without having to use intro.

I don't think it is sensible to simply add new builtins on to tactic.lean though, because now we have lost some safety as described in reason 2. I am wondering if there is a demand to do this and if there is, what would be a good way to do it that keeps with the functional paradigm while not breaking tactic and also ideally with some of the same caching that tactic enjoys.

I've got an experiment going on https://github.com/leanprover-community/lean/tree/ctxt_manip
See this file where I've reimplemented intro as my_intro using some new builtins.

I recall @Simon Hudon saying that people have already talked about this, but I don't know where I would find this discussion.

Simon Hudon (May 20 2019 at 15:59):

Do you think this low-level kind of manipulation could be encapsulated in a different monad than tactic, something unoriginally called lowlevel_tactic for instance?

Edward Ayers (May 20 2019 at 16:12):

was thinking tactic.unsafe

Edward Ayers (May 20 2019 at 16:14):

But it's a different monad to tactic.

Edward Ayers (May 20 2019 at 16:21):

Yeah it would be a monad without alternative so that there are no headscratchers with getting the cache to behave nicely.

Simon Hudon (May 20 2019 at 17:03):

That sounds like an interesting idea. How hard will it be to build and what are the benefit beside distinguishing temporary meta-variables?

Edward Ayers (May 21 2019 at 13:55):

Benefits:

  • can implement many builtins within Lean. eg intro. An example tactic that I find myself wanting is one that solves the goal Type u with the expression Pi x : X, ?m[x]. Maybe one could even reimplement more complicated ones like simp within lean. Would be interesting to see perf differences.
  • can use temporary metavariables.
  • can avoid cache resets when speculatively trying to unify things
  • can add local constants to the context without going through intro.
  • just being able to manipulate the tactic's context directly is so much easier than builtins for some tasks.
    When I am writing automation I catch myself thinking: "I really just want to change the type context to look like this, how can I do that only using the library builtins which were not designed for this use case?". I feel like I am working against the tactic abstraction and I would much rather be able to just explicitly say what I want the metavariable context to look like.
  • This wouldn't be solved directly by just making this new module, but I feel like it is important for tactic to not just be this black box where you can't understand how it works without looking at the C++ source code. Eg at the moment it's basically impossible to understand the seemingly contradictory message tactic failed, result contains meta-variables \n state: no goals without someone explaining what tactic is doing under the hood. You can't discover how tactic works for yourself but it is easy to newcomers to end up with the wrong mental model of it.

Difficulties: exposing a type_context monad wouldn't be that difficult. All of the machinery is already in the C++ it's just about making it available leanside. Testing and managing caches might be a little more challenging.

Mario Carneiro (May 21 2019 at 13:58):

I'm definitely sold, but it sounds like a lot of work

Mario Carneiro (May 21 2019 at 13:59):

Your first example can be achieved by refine btw. That doesn't address the rest of it or efficiency though

Mario Carneiro (May 21 2019 at 14:00):

simp in lean is a non-starter, I think. It's not a question of capabilities, it's an efficiency problem

Mario Carneiro (May 21 2019 at 14:00):

You would have to do this via code generation, JIT, or lean 4

Edward Ayers (May 21 2019 at 14:05):

Your first example can be achieved by refine btw. That doesn't address the rest of it or efficiency though

I guess you mean something like refine \lambda x, _? I mean you can't create a local constant on the context without already having your target be a Pi, and you can't create a local constant without also making all of the metavariables and delayed abstractions that go along with using refine or intro.

Mario Carneiro (May 21 2019 at 14:06):

I mean refine \Pi x, _, since that's your goal

Edward Ayers (May 21 2019 at 14:06):

Ah no you mean the Pi x, ?m thing

Mario Carneiro (May 21 2019 at 14:07):

You can use refine with a placeholder

Mario Carneiro (May 21 2019 at 14:07):

as in construct \Pi x, _ as a pexpr

Edward Ayers (May 21 2019 at 14:07):

yep

Mario Carneiro (May 21 2019 at 14:08):

I think your way is better though

Edward Ayers (May 21 2019 at 14:11):

simp in lean is a non-starter, I think. It's not a question of capabilities, it's an efficiency problem

Yeah you are probably right here. My point was just that you could implement simp within Lean and get the temp-mvars efficiency boost, but that's probably not enough.

Edward Ayers (May 27 2019 at 01:18):

I got a minimal prototype working at https://github.com/leanprover-community/lean/tree/ctxt_manip
Look at the tests/lean/tco.lean for some examples.


Last updated: Dec 20 2023 at 11:08 UTC