specialization pattern syntax

Stream: iris-lean

[Michael Sammler]

As already came up in multiple places, we should discuss what syntax we want to use for specialization patterns. Based on https://leanprover.zulipchat.com/#narrow/channel/490604-iris-lean/topic/proof.20mode.20terms.20for.20icases/with/564255452 I thought a bit more about what syntax to use for the specialization patterns and collected the following ideas based on the suggestions in the thread. What do you think about these options? Any other ideas?

As the example, consider h : ∀ x, ⊢ ∀ y, ⌜A x⌝ -∗ P x -∗ Q y -∗ R.

[Michael Sammler]

Option 1: h a $! b with [%] H1 [H2, H3]
pro:

• same notation as in Rocq
• clearly separated what is a Lean hypothesis vs Iris universal quantifier vs Iris hypothesis

con:

• "with" conflicts with "with" of icases
• does not support universal quantifiers after wands

[Michael Sammler]

Option 2: h a b [%] H1 [H2, H3]
pro:

• no symbols like $!
• does not conflict with another notation
• supports universal quantifiers after wands

con:

• hard to see what are Lean hypothesis / quantifiers vs Iris
• might have weird edge cases in parsing since one cannot use the normal term parser (or can one?)
  • I am worried about e.g. passing implicit or named arguments to h, i.e. the case when it is not just a list of space separated terms
• ambigous if [H2, H3] refers to a list or the specialization pattern
  • maybe one can find another notation?

[Michael Sammler]

Option 3: h a $! b [%] H1 [H2, H3]
pro:

• only one symbol $!
• does not conflict with another notation
• clearly delimits lean arguments from Iris arguments
• supports universal quantifiers after wands

con:

• one has to remember $!

[Michael Sammler]

Option 4: h %a b % H1 [H2, H3]
pro:

• no $!
• does not conflict with another notation
• distingushes lean arguments from Iris arguments
• supports universal quantifiers after wands

con:

• might be hard to parse?
• usage of % might conflict with % for creating pure goals

[Michael Sammler]

Option 5: h %a %b % H1 [H2, H3]
pro:

• no $!
• does not conflict with another notation
• % uniformly means pure (either type / ∀ or prop / ⌜_⌝)
• supports universal quantifiers after wands

con:

• might be hard to parse?

[Shreyas Srinivas]

Why not use lean syntax?

[Shreyas Srinivas]

For patterns I mean

[Shreyas Srinivas]

With angular braces.

[Michael Sammler]

To make sure that we are one the same page: The lean syntax for instantiating a hypothesis of type h : ∀ x y, A x → P x → Q y → R would be h a b _ H1 _. (There is no equivalent of [H2, H3] in Lean since there it is not necessary to split the context.) Option 2 is probably closest to this (but maybe also confusing because of this).

[Shreyas Srinivas]

Option 2 looks good.

[Shreyas Srinivas]

But I am also sure we can find some unicode separator like \| or \|-

[Shreyas Srinivas]

Do we not need to separate iris universal quantifiers from lean universal quantifiers?

[Markus de Medeiros]

Thanks for writing this all out! I'll give my 2¢, but I'll go with whatever the most people like.

• Universal quantifiers after wands would be a nice feature, I like this.
• I also like the ability to cleanly distinguish Lean and Iris terms since it could afford us more flexibility in terms of mixing in Lean terms.
  • For example, maybe the [%] in Option 3 could be extended to a syntax like [%(...)] which refines the proof goal with the terms, or holes in ...
  • Then it would be completely idiomatic to write h a $! b [%(⟨?_, ?_⟩)] H1 [H2, H3] or evenh a $! b [%(by grind)] H1 [H2, H3]. Anyways, just some food for thought.
• I mentioned above my main gripe with $! is that I find it hard to remember... seeing the upsides and downsides I think my main issue is the the symbol itself. From your list it seems that having a delimiter between the Iris and Lean terms makes our lives simpler. I'd be happy with this if we just used an English word instead (as? from? using? whence? Alright that last one is a joke.)
• The uniformity of pure patterns in Option 5 is satisfying, but I think you're correct that parsing could be tricky.

Overall, your Option 3 (with an English version of $!) seems to have the most upsides. Interested in hearing other's opinions!

[Michael Sammler]

I also like Option 3 the most. I am open to bikeshedding which word / symbol to use for the delimiter. Shreyas suggested ∣ (i.e. \|), but I think this looks too close to | and will confuse people. But maybe just | could work? Alternatively, maybe we can use $? (a bit like how it is used in Haskell for application)
I think the problem of $! in Iris Rocq is that it is used very seldomly, so if one needs it it is hard to remember. But the symbol we pick will be used very often (almost all calls to iapply), so I think people will be able to remember it (or find an iapply call close by that uses the symbol).
If we use a word, it should be clear that it means function application. Maybe using would work? (with would also be good, but we cannot use it because of the conflict with cases)

[Markus de Medeiros]

Great, I agree completely!

[Shreyas Srinivas]

My two cents on \| vs | : At least in vscode, hovering the mouse pointer over a symbol tells you how to enter it. I have this confusion with unicode symbols with other theorem provers which don't provide these helpful tooltips yet, so I can see why you might be concerned. With good docstrings finding the notation and the shortcuts shouldn't be too hard. \| is used as the divisibility operator in mathlib for example. I recommend against plain | because that might interact badly with the | used in arms of matches for example. Since Iris syntax is still in the term syntax category, this might cause headaches later

[Michael Sammler]

I implemented the unified proof mode patterns (Option 3) in https://github.com/leanprover-community/iris-lean/pull/109
This PR uses $$ as the delimiter, but this is open to bikeshedding.
It worked surprisingly well. You can do things like ispecialize H $$ %(by grind) and get a working proof mode inside the by

[Zongyuan Liu]

I'm in favour of Option 5. Can you remind me why we want to delimit lean arguments from Iris arguments?

[Michael Sammler]

One problem with Option 5 is that parsing becomes harder. With Option 3 we can just elaborate everything on the left of $$ / $! as a normal Lean term, so all lean term notation works without problem (e.g. specifying implicit arguments via (A:=A). For Option 5, it is a bit less clear how parsing work. Do we only allow identifiers for h or more?
Another difference of Option 3 vs Option 5 is that Option 3 allows one to skip all Lean arguments. If we have h : ∀ x y z, |- ∀ a, P, with Option 3 we can write h $$ %a to specify just a, while for Option 5 we need to write h %_ %_ %_ %a. This might make a difference for lemmas with many parameters that one wants to fill with underscores (this is how it works in Rocq).

[Zongyuan Liu]

Thanks. I now agree that option 3 seems to be the best. I however prefer a one-character separator, since one would have to type it a lot. For instance the proposed $?

[Michael Sammler]

$ is already used as an alias for |> in terms, so we sadly cannot use it. But I would also like a single character if we can find a good one.

[Shreyas Srinivas]

I still think \| is a good candidate. Also wow that was blazing fast :scream:

[Ayhon]

If $ doesn't work, why not €, £ or ¥ (or ¢?) /j

[Ayhon]

On a more serious note, this made me go through the list of symbols abbreviations supported by Lean, so I collected a list of symbols that I think could work, beyond the already proposed ones. I tried to choose those that wouldn't bee too much of a pain to write down while typing.

• ‖: \Vert
• ‡: \ddagger, \ddag
• ⅌: \per
• ¡: \!
• ∷: \::
• ✂: \8<

[Ayhon]

Ok, it seems like Zulip is not a big fan of \per, :frown: