add notation to define the PROP we use for a particular turnstile

Fixes #156 (closed)

changed milestone to %Generalized Proofmode Merger

Although I proposed the notation myself, I'm having second thoughts. We currently mainly use { n } to denote the step-indexed version of a notation. How likely is it that we need the step-indexed version of ⊢ in the future? (In principle, we already have the step-indexed version of ⊣⊢, namely ≡{n}≡).

With SProp, that seems not unlikely... though we probably want a general notation for "give me this SProp at that step-index", not one notation per SProp.

Should we change it to ⊢[ _ ]?

With SProp, that seems not unlikely... though we probably want a general notation for "give me this SProp at that step-index", not one notation per SProp.

You mean once we define the entailment as an SProp?

Should we change it to ⊢[ _ ]?

[ and ] always scare me... But supposedly since it's part of the token ⊢[ it's probably fine. Unless we ever want to overload the list notation in bi_scope (which arguably does not make much sense).

You mean once we define the entailment as an SProp?

Yes.

added 1 commit

• f72c6534 - change typed entailment to use brackets instead of braces

Compare with previous version

I changed the notation to use brackets.

@robbertkrebbers ping

This MR is probably fine.

I am still a bit skeptic in terms how this approach scales to other notations.

For example, for equality = it would not work, e.g. l =[x] is potentially ambiguous. For equality, I noticed Coq already has x = y :> A, but that is not going to work for P ⊢ Q :> PROP, I think, because ⊢ is at level 200.

Any idea what other libraries (e.g. Ssreflect) are doing to make type arguments explicit in notations?

For equality, I noticed Coq already has x = y :> A, but that is not going to work for P ⊢ Q :> PROP, I think, because ⊢ is at level 200.

I just tried this; it indeed does not work: :> is already declared at level 100 (*), so when having Q at level 200 in P ⊢ Q :> PROP, this will be parsed as P ⊢ (Q :> PROP).

(*) What is the notation :> (without =) for anyway?

(*) What is the notation :> (without =) for anyway?

Print Scope shows nothing, but (plus :> 0) becomes just plus 0, so this may be Coq's version of Haskell's $?

How bad would it be to change the level of |-?

Alternatively I could make it ⊢_[PROP]; the added underscore makes it less likely for conflicts to arise: y =_[x] being parsed differently from y = [x] should not be too surprising. It's not pretty, but this syntax shouldn't be very common and it's not SO bad, either.

Print Scope shows nothing, but (plus :> 0) becomes just plus 0, so this may be Coq's version of Haskell's $?

If it's the latter, the associativity is wrong: plus :> 1 + 1 is being parsed as plus 1 + 1.

How bad would it be to change the level of |-?

It will break many things, for example, P ⊢ Q -∗ R will then be parsed as (P ⊢ Q) -∗ R.

Alternatively I could make it ⊢_[PROP]; the added underscore makes it less likely for conflicts to arise: y =_[x] being parsed differently from y = [x] should not be too surprising. It's not pretty, but this syntax shouldn't be very common and it's not SO bad, either.

That notation also causes conflicts, for example, it's not too strange the write something like refine (y = _ [x]) where the _ represents a hole.

@jjourdan Do you have any suggestions?

That notation also causes conflicts, for example, it's not too strange the write something like refine (y = _ [x]) where the _ represents a hole.

=_[ would be one token, so your expression as written should be fine.

=_[ would be one token, so your expression as written should be fine.

I don't like it too much to rely on spaces.

By the same way of reasoning, we could also use x =[A] y, which most surely breaks compatibility with many existing Coq developments where people forgot to put a space between = and a list notation at some places.

This is a matter of trade-offs, we don't have a perfect solution. My goal is to find the "least bad" syntax we can come up with. Otherwise we will never be able to add any new syntax for anything.

We already rely on spaces elsewhere, like for the {{ in WP and Hoare triples or the ≡{ for updates and n-equality (ambiguous with equivalence on sigma types: .. ≡ { x | some_pred x }).

I think people are pretty unlikely to write y=_[x] and intend _ to be a hole, which is why I feel this is a reasonable trade-off.

Yet another proposal: @{A}. We then end up with:

Without	With
x = y	x =@{A} y
x ≡ y	x ≡@{A} y
x ≡{n}≡ y	x ≡{n}@{A}≡ y
x ≼ y	x ≼@{A} y
x ≼{n} y	x ≼{n}@{A} y
x ⊢ y	P ⊢@{PROP} Q
x ⊣⊢ y	P ⊣⊢@{PROP} Q

@ is fine for me as well. However I'd change the step-indexed version to x ≡{n}≡@{A} y.

Fine to me.

By the way, I think the @ is free of conflicts as long as it's followed by something that cannot be parsed as an identifier.