an unsafe version of tactic

Stream: general

[Edward Ayers]

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]

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]

was thinking tactic.unsafe

[Edward Ayers]

But it's a different monad to tactic.

[Edward Ayers]

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

[Simon Hudon]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Edward Ayers]

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]

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

[Edward Ayers]

Ah no you mean the Pi x, ?m thing

[Mario Carneiro]

You can use refine with a placeholder

[Mario Carneiro]

as in construct \Pi x, _ as a pexpr

[Edward Ayers]

yep

[Mario Carneiro]

I think your way is better though

[Edward Ayers]

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]

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.