Tactics discussion

Stream: iris-lean

[Markus de Medeiros]

@Mario Carneiro yesterday you mentioned that you had some ideas for how we should implement the iApply and iMod tactics. Could you expand on what you had in mind?

[Markus de Medeiros]

cc @Oliver Soeser who has started working on tactics

[suhr]

I would like to know more about how all these tactics work, since I'd like to make a term style syntax (maybe in style of αλ-calculus?).

[Oliver Soeser]

I think iApply and iMod are really gonna be key to making iris-lean useful in practice, so we need to have a solid foundation for implementing them

[Shreyas Srinivas]

Do we have a list of tactics we need? There are lots of ltac scripts in Rocq developments that:

1. Are essentially just macros
2. Not how I have seen lean developments work.

[Shreyas Srinivas]

Also @Oliver Soeser : I am trying to understand these tactics better, so are you already working on both of these tactics and if not, can I pitch in for one of them?

[Oliver Soeser]

I've not started on either of these yet, I'm still working on iRevert

[Markus de Medeiros]

(re. Shreyas) The tactics in Iris are a little more involved. I would strongly recommend reading the MoSeL paper to get acquainted with the design (it is a very good paper!) and Lars König's thesis to get acquainted with the differences to Rocq.

[Oliver Soeser]

Shreyas Srinivas said:

Do we have a list of tactics we need? There are lots of ltac scripts in Rocq developments that:

1. Are essentially just macros
2. Not how I have seen lean developments work.

@Michael Sammler and I were talking about this and our list of needed tactics is: iRevert, iAssert, iAccu, iFrame, iApply, iInduction, iMod

[Oliver Soeser]

(Roughly in order of estimated implementation complexity)

[Shreyas Srinivas]

Markus de Medeiros said:

(re. Shreyvas)

It's "Shreyas" :slight_smile:

The tactics in Iris are a little more involved. I would strongly recommend reading the MoSeL paper to get acquainted with the design (it is a very good paper!) and Lars König's thesis to get acquainted with the differences to Rocq.

I have read the former an aeon ago. I will revisit that. I still need to read Lars' thesis

[Markus de Medeiros]

Oops, sorry!

[suhr]

I guess I should read MoSeL paper too. Thanks for suggestion.

[Markus de Medeiros]

At a high level, the tactics use three components:

• Theorems about the proof state
• Typeclasses that encapsulate these theorems
• (Relatively small) Ltac tactics to apply theorems from those typeclasses

So for example, the LTac script to do iApply H where H : X in the Iris context would loosely do something like:

• Look for an IntoWand X A B typeclass instance to turn X into a wand A -* B
• Check to see if the goal has Iris type B
• Apply a theorem which lets you update a proof state whose goal is B and a wand A -* B into a proof state whose goal is A.

[Markus de Medeiros]

In Rocq, typeclass synthesis is done in a backtracking loop. So if it synthesizes the wrong IntoWand X A B in the first step, the tactic will fail, backtrack, and try to find another instance.

This is not something that can be easily done in Lean from my understanding, but it's also not something that necessarily has to. If there is, for example, some way to do "all of the typeclass synthesis at once", then we could implement a version of this which is extensible and hopefully pretty fast given Lean's optimized typeclass system.

[suhr]

Can we CoeFun a proof of A -* B into a proof of X? Or there's something special about IntoWand which does not allow that?

[Markus de Medeiros]

Markus de Medeiros said:

This is not something that can be easily done in Lean from my understanding, but it's also not something that necessarily has to. If there is, for example, some way to do "all of the typeclass synthesis at once", then we could implement a version of this which is extensible and hopefully pretty fast given Lean's optimized typeclass system.

I've linked it before, but this is what I did in my iApply prototype. I added another typeclass InferIntoWand which is like intoWand but has different outParams. Idk if it works in all situations but it works for the simple ones. Someone needs to think harder about if this strategy will work for all of the tactics Oliver listed.

[suhr]

Or wait, that was a silly question, since it should be CoeWand.

[Markus de Medeiros]

suhr said:

Can we CoeFun a proof of A -* B into a proof of X? Or there's something special about IntoWand which does not allow that?

It's a little different but not much more complex

class IntoWand [BI PROP] (p q : Bool) (R P : PROP) (Q : outParam PROP) where
  into_wand : □?p R ⊢ □?q P -∗ Q
export IntoWand (into_wand)

[suhr]

Markus de Medeiros said:

So if it synthesizes the wrong IntoWand X A B in the first step, the tactic will fail, backtrack, and try to find another instance.

So there's many ways to convert something into a wand.

[Markus de Medeiros]

Yeah

[suhr]

I'd like to have some examples to build a bit of intuition.

[Markus de Medeiros]

You can peruse the instances in the Rocq Iris repo: link

[Markus de Medeiros]

The real party line here is that supporting multiple instances also makes the tactics easily extensible. It's common in Iris developments to add more instances to extend the behavior of the proofmode. Example: here defines a new modality, and then gives an IntoWand instance to tweak how it works with the proofmode.

[Shreyas Srinivas]

Couldn't we just write our own backtracking instance search?

[Markus de Medeiros]

That's one option, but I imagine it isn't the best.

[Shreyas Srinivas]

It's not the fastest, but at some point we might want to control how we do instance search

[Shreyas Srinivas]

Also, a lesson from mathlib recently was that lean's existing instance search works better with mixins than typeclass hierarchies

[Markus de Medeiros]

Oh? Do you have a link to that thread somewhere

[Shreyas Srinivas]

I think they discovered this in the algebra hierarchy and it shaved some build time off mathlib

[Shreyas Srinivas]

Let me check. I am going on my memory here

[Shreyas Srinivas]

Found a PR : https://github.com/leanprover-community/mathlib4/pull/20676

[Shreyas Srinivas]

linked thread : #mathlib4 > Ways to speed up Mathlib @ 💬

[Shreyas Srinivas]

I understand I am dropping you in the middle of a long thread, but I gather that the gist of it is that it is better to split typeclasses and mix them in than build long hierarchies of typeclasses.

[Markus de Medeiros]

Fascinating!

[Markus de Medeiros]

Our proofmode typeclasses don't really have a hierarchy, but yeah that's an interesting read

[Markus de Medeiros]

From what I understood when I talked to my advisor about Iris speedups, he said that data representation (duplicating proof contexts) was a big time spend. I'm optimistic that Iris-Lean can be quicker, especially since we're using a more succinct representation of the proof context, but only time will tell :)