tactic writing for dummies

Stream: general

[Patrick Massot]

Here is what I think is a nice little Lean story. In the perfectoid project, we need to start with a multiplicative totally ordered group and add a zero element, which is absorbent for multiplication and lower than all original elements. For instance, starting from the group of positive real numbers, the new thing is isomorphic to the monoid of non-negative real numbers. Then there are many lemmas about the properties of this kind of monoid. In the real world, these lemmas are not even stated. If cornered, a mathematician will tell you that they follow from easy case discussions, depending on which element is zero or a an element of the original group. In general the case where something is zero is trivial, and the other case follows from properties of the original group. Of course when there are two or three elements, these discussions are nested. In the perfectoid project, we suffered quite a bit with those lemmas which are not even stated in the real world. First we modeled them using with_zero, which is a wrapper around option. But we were not careful to keep this abstraction, and stated various lemmas in terms of none instead of zero and, even more often, in terms of some x instead of (x : with_zero G). Then we fixed that. And then comes the interesting bit. We need automation to get rid of proofs that mathematicians wouldn't write. We can't expect all mathematicians to become skilled tactic writers. But we can politely ask computer scientists to write heavy-lifting tactics. At some point @Rob Lewis got tired of listening to Kevin's whining and asked @Paul-Nicolas Madelaine to write norm_cast. This was a huge boost to help getting rid of those proofs. But it was too general. In the mean time @Simon Hudon taught me rudiments of tactic writing, and I was able to write a small very specialized tactic on top of induction and norm_cast. That last step was done in https://github.com/leanprover-community/lean-perfectoid-spaces/commit/01fd6abb7127b0593dd82b02bab5799947e83327. That's 7 lines of tactic code which gets rid of 38 lines of proof. It doesn't sound impressive, but it brings the proofs much closer to what they look like in my head (when I'm forced to think about these trivial lemmas of course).

[Patrick Massot]

Now I have a question for real tactic writers. My tactic is a bit slow, and it would probably be faster to call norm_cast only on elements of the context created by the induction calls. I know induction returns a list of tuples containing relevant information. But I don't know how to use this list in conjunction with the seq that is used to call induction on multiple elements. Any idea? Should I call norm_cast before the inductive call to my tactic? Or can I do it in the end but pass around some list?

[Patrick Massot]

I think I deserved to open that bottle I bought at the Edinburgh airport when leaving the Big Proof workshop.

[Reid Barton]

Those proof simplifications are very nice!

[Simon Hudon]

norm_cast sometimes uses simp without arguments. That means that it tries every simp lemma in mathlib. It would be faster if you could be more targeted or optionally disable the use of simp all together.

[Paul-Nicolas Madelaine]

@Simon Hudon you mean simpa?
norm_cast should never call simp without arguments.
But it uses simpa to discharge proofs, which may not be necessary.

[Patrick Massot]

Having a fast norm_cast could become important because I think it will be used a lot. But it needs to stay as powerful. We can wait a bit if this is the prize to pay for getting rid of all coercion bureaucracy.

[Simon Hudon]

Because you're using simpa inside of norm_cast, you're only going to be as fast as simpa. But simpa offers the only, [_,_] and with options that could be available through the norm_cast interface.

[Simon Hudon]

You can even offers the options (e.g. through a ? notation) of calling squeeze_simpa to help make an invocation faster