Tactic writing approach

Stream: general

[Chris Hughes]

I decided to give tactic writing a serious go recently, so as an exercise I wrote a tactic to prove equality of group expressions. I did it without using the simplifier so it would not be a trivial exercise. Code here. The approach I tried was to define the type group_term, and the define an inductive relation rel on group_term that said they were equal as group elements.

@[derive decidable_eq, derive has_reflect] inductive group_term : Type
| of : ℕ → group_term
| one : group_term
| mul : group_term → group_term → group_term
| inv : group_term → group_term

The relation rel was defined to be in Type rather than Prop. I defined a function that would return the term of type option (rel a b), returning some whenever a and b were equal as group elements. This function in principal need not be a meta function, it is in my example, but only because I didn't prove termination. I wrote a tactic suffices_rel that given an equality in a group, proved that it suffices to prove two explicit group_terms were rel. I wrote a reflect : rel a v -> expr, and once my goal was to prove rel a b, I could compute the term of type rel and reflect it. This approach worked and I have a group tactic.

My questions are

1. When writing a tactic that solves non trivial maths problems, is it a sensible approach to write a non-meta program that does the hard work of solving the maths problem and producing a certificate, and then a small amount of meta code interfacing this with the tactic state? I find it very ugly to have stuff about meta objects mixed in with code that solves a maths problem that has nothing to do with any meta objects. Maybe equality of group expressions is too trivial for this approach, but is it sensible for harder problems?

2. Why is my group_tac so slow? It seems like most of the time is spent on rel.reflect reflecting the certificate, not actually computing the certificate. The derive handler doesn't work for dependent types, so I my own reflect function.

[Patrick Massot]

You don't have enough type of group terms. What about g^n?

[Chris Hughes]

This is an exercise, so I didn't bother with that

[Rob Lewis]

Chris Hughes said:

1. When writing a tactic that solves non trivial maths problems, is it a sensible approach to write a non-meta program that does the hard work of solving the maths problem and producing a certificate, and then a small amount of meta code interfacing this with the tactic state? I find it very ugly to have stuff about meta objects mixed in with code that solves a maths problem that has nothing to do with any meta objects. Maybe equality of group expressions is too trivial for this approach, but is it sensible for harder problems?

Yes, this can be sensible. It's the approach taken by omega, and used quite a bit in Coq. I think the general sense we have is that producing and checking proof terms is faster in Lean than relying on kernel reduction. (The Coq people warn about impossibly large expressions doing this.) ring2 uses proof by reflection like you describe, but Mario concluded a while ago that he couldn't make it as fast as ring which produces proof terms.

[Rob Lewis]

Lean will be particularly slow evaluating anything defined non-meta with well-founded recursion, even if you're evaluating in the VM. @Gabriel Ebner pointed this out to me very recently.

[Rob Lewis]

I'll see if I can find the slow part of your code when I have a chance, probably not tonight though.

[Chris Hughes]

Rob Lewis said:

I think the general sense we have is that producing and checking proof terms is faster in Lean than relying on kernel reduction.

I didn't mean to rely on kernel reduction. The group_tac I wrote reflects a term of type rel _ _, but it shouldn't be any work to type check this term. It seems easier to me to define an inductive language capable of proving only the problems I'm interested in, which is a far simpler type than a Lean expr, and prove soundness. I can reflect a term of this type at the end to give the Lean proofs. This seems easier because you're guaranteed that whatever it comes up with will type check, and you won't be using meta constants which I don't understand the precise behaviour of and give me app_builder errors.

[Jannis Limperg]

Your approach is fairly close to the well-known recipe for "proof by reflection" (with some divergence where you move into meta land; typical proof by reflection would implement the decision procedure as a non-meta function and prove it sound). Rob already points out some of the Lean-specific performance issues, which I assume could be solved with more engineering hours; I'll add some more conceptual considerations:

• This approach is fairly closed: you have to define the entire language of your problem up front. Contrast this with tactics, where you can often provide 'hooks' that allow people to fill in their own domain-specific simplification strategies or whatever. There's research into compositional proof by reflection, but that's a big hammer.
• You usually want to have a notion of 'uninterpreted term' in your group_term language. An uninterpreted term is an arbitrary inhabitant of the group you're interested in (e.g. Patrick's g^n) which you treat as a constant. You never inspect these terms; you just carry them around. This allows you to work with terms that don't strictly fit into your little language. Adding this is not too hard, but may lead to some technical issues.
• The complexity of this approach really blows up when you move into expression languages with more than one type. Your group_terms are unityped: every group_term denotes an element of some given group. But if you try to scale this to, say, a simplification procedure for category theoretic expressions, you now need expressions that denote elements of a category, other elements that denote arrows between specific elements, other elements that denote functors between specific categories, etc. In the extreme, you're implementing a type checker for a little dependently typed language, which is well known to be unpleasant. (I tried this in Agda once and walked away with little to show for it.)
• In particular, when you want to deal with things at different universe levels (e.g. categories), you're probably just screwed. In Agda, I still have some hope since it has first-class universe expressions, but Lean is much more restrictive in this regard.

I'm being maybe a little too critical here -- when the approach works, it's very nice and elegant (and fast if your computation is fast). But these limitations make me sceptical about scaling from toy problems to bigger domains.

[Mario Carneiro]

ring2 uses proof by reflection like you describe, but Mario concluded a while ago that he couldn't make it as fast as ring which produces proof terms.

Actually there is a further distinction to be made here. One option is to have an inductive type that represents some kind of certificate and write non-meta functions over them and evaluate them in the VM as part of tactic execution. This is what omega does, and I would recommend it especially if you need to perform some nontrivial computation / search before actually producing the result. I don't use this method in ring mainly because it is almost entirely doing straight "consume input expr -> produce proof" and so there is little to be gained by an intermediate type that would still need to be translated to and from expr.

ring2 is doing something different, what is called computational (large-scale) reflection in the Coq community. This is characterized by a "heavy rfl" proof after some small reification step; this means the evaluation of the non-meta function is being done in the kernel instead of the VM, and the emitted proof is small (essentially constant size no matter the complexity of the algorithm). In order to make this efficient in lean you need to use careful data structures (many of the usual data structures in the library are inefficient because they carry proofs as invariants or use a pathologically bad encoding e.g. nat), and even then it's slower than VM evaluation by a small margin.

[Mario Carneiro]

Rob Lewis said:

Lean will be particularly slow evaluating anything defined non-meta with well-founded recursion, even if you're evaluating in the VM. Gabriel Ebner pointed this out to me very recently.

This is news to me. My understanding was that the VM uses the same method for compiling non-meta wf (or other eqn compiler) recursions as for meta recursions, namely unguarded recursion. What is the cause for the performance gap?

[Gabriel Ebner]

It was always planned, but then Lean 4 came along IIRC. The reason is that the VM compilation happens long after the equation compiler is finished with them and has added the WF-encoding to the environment. Meta declarations are added without translation to the environment (using the rec_fn_macro).

[Gabriel Ebner]

I'm not sure if there is a difference with unary well-founded functions, but for binary functions the encoding causes a big slowdown in the VM.

[Chris Hughes]

I'm trying to do deciding single relation on a group tactic, i.e. given t₁ = t₂ in a group, prove t₃ = t₄. This doesn't seem to have the problems that Jannis pointed out, everything will just be one type, although there is more than one group involved, so multiple Types. It also seems to be mostly just a computation, so I guess the heavy rfl approach might be best.

[Mario Carneiro]

From what I can tell, I think an approach like ring would be the most efficient. One thing that is "searchy" about the algorithm is identity testing: you have to determine whether to apply a cancellation rule or not, when the proof should just do it without a test

[Chris Hughes]

What is the approach of ring?

[Mario Carneiro]

Pattern match on the expression, apply small step proof rules recursively

[Mario Carneiro]

this is very straightforward for group

[Chris Hughes]

The single relation tactic is not straightforward.

[Mario Carneiro]

Single relation?

[Kevin Buzzard]

you know one relation and you're trying to prove an identity

[Mario Carneiro]

oh I missed the context

[Chris Hughes]

Given t₁ = t₂ prove t₃ = t₄

[Kevin Buzzard]

e.g. if you know ab=ba you want to be able to deduce a^2b^3=b^3a^2

[Kevin Buzzard]

or if you know abcd=1 you want to be able to deduce cdab=1

[Mario Carneiro]

That's true, but you still only need data structures other than expr when you are trying to remember your place in the algorithm

[Mario Carneiro]

The general pattern is to use expr for the input and the output (because you have to) and use custom data structures for everything else

[Chris Hughes]

I don't fully understand the algorithm yet, but the very approximate gist is to keep changing the basis of the free group, until your relation is a generator.

[Mario Carneiro]

and don't produce any proof terms that are not a syntactic match (i.e. no heavy rfl)

[Mario Carneiro]

the kernel never sees your data structures, it sees you applying theorems about groups

[Chris Hughes]

So defining my mini inductive language would be sensible?

[Chris Hughes]

The certificate may well just be a list of conjugates of my relation and it's inverse that my goal is the product of.

[Mario Carneiro]

It may be, but I suspect that you can straightforwardly compose snormalize and rel.reflect and skip the middle man

[Chris Hughes]

For the single relation tactic I mean. I'm sure that group_tac is not optimised, and it's more to test the approach.

[Mario Carneiro]

I would only suggest using rel if you are constructing proofs that you sometimes discard

[Mario Carneiro]

in a lot of cases if you structure the control flow of the tactic right everything you construct will appear in the final proof so there is no need

[Mario Carneiro]

I don't actually know the one relation algorithm, so I can't comment on the difficulty (besides noting that the paper I recall seeing seemed pretty long)

[Kevin Buzzard]

Supervising an MSc project has never been so easy!

[Mario Carneiro]

Reading the code, I see that you are relying on kernel reduction for evaluating eval, which is not horrible but probably not a great idea

[Mario Carneiro]

You also forgot to use id_rhs to protect the target type. If you return an expression of the wrong type it might unfold in an unfavorable way

[Chris Hughes]

Mario Carneiro said:

You also forgot to use id_rhs to protect the target type. If you return an expression of the wrong type it might unfold in an unfavorable way

Where should I have used id_rhs?

[Mario Carneiro]

Just before the exact on L224

[Mario Carneiro]

I think there is a function that wraps this pattern up

[Mario Carneiro]

there is mk_id_proof although that just uses id. I think it should work

[Mario Carneiro]

you give it your proof and the type you want it to have (which is different from the inferred type, resulting in kernel computation of the eval function)

[Mario Carneiro]

and nth, etc

[Mario Carneiro]

You also have an eq.rec_on in your snormalize. I'm not really sure what happens there once it gets reflected. It's a bit weird that rel is dependent type here

[Chris Hughes]

Mario Carneiro said:

You also have an eq.rec_on in your snormalize. I'm not really sure what happens there once it gets reflected. It's a bit weird that rel is dependent type here

I agree it's a bit weird, that's why I asked about it, particularly given that there's no handler for derive reflect for dependent types. I thought the eq.rec_on was okay, because I'm doing basically nothing with to make a group_term other than applying constructors, and using no functions on nat, so it's going to typecheck easily.

[Chris Hughes]

I realised there would be a problem if the eq.rec_on used funext, and the type depended on a function, or similar with Prop and propext, but it should be fine with an inductive type like group_term.

[Mario Carneiro]

I think any eq.rec_on could be problematic if it's not definitional in the result

[Mario Carneiro]

because the has_reflect instance doesn't know to add them back and will likely produce a not well typed term

[Chris Hughes]

When will it not be definitional in the result? Provided it's an inductive type without pi types or Sorts as constructors it should be fine right?

[Mario Carneiro]

If it's any random equality, from the context or something

[Chris Hughes]

If two group_terms are equal they're defeq right?