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!