Add "if <term> is <pattern> then _ else _" syntax

[proux01]

New syntactic sugar if g is c then t else e for match g with c => t | _ => e end. This adds the new reserved keyword is.

In a future PR ( #22123 ) we will deprecate the specific if ... then ... else for inductives with two constructors (that is error prone, since it depends from the order of the constructors) with a quickfix toward the new if g is first_constructor then ... else variant and restrict if ... then ... else to booleans (or anything coercible to bool).

• Added / updated test-suite.

• Added changelog.
• Added / updated documentation.
  • Documented any new / changed user messages.
  • Updated documented syntax by running make doc_gram_rsts.

Overlays (to be merged before the current PR)

• Adapt to https://github.com/rocq-prover/rocq/pull/21609 mit-plv/bedrock2#509
• Adapt to https://github.com/rocq-prover/rocq/pull/21478 fblanqui/color#60
• Adapt to https://github.com/rocq-prover/rocq/pull/21478 AbsInt/CompCert#570
• Adapt to https://github.com/rocq-prover/rocq/pull/21478 mit-plv/fiat-crypto#2246
• Adapt to https://github.com/rocq-prover/rocq/pull/21478 mit-plv/fiat-crypto#2247
• Adapt to https://github.com/rocq-prover/rocq/pull/21609 DeepSpec/InteractionTrees#283
• https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/685
• Adapt to https://github.com/rocq-prover/rocq/pull/21609 UniMath/UniMath#2066
• Adapt to https://github.com/rocq-prover/rocq/pull/21478 uwplse/verdi#149

Alternative

In the discussion, some alternative syntax proposition came out, see https://github.com/rocq-prover/rocq/wiki/if-syntax for details.

[SkySkimmer]

This adds the new reserved keywords is and isn't

Not sure we want this.
We could have something like if let pattern := v then e1 else e2 instead of if v is pattern then e1 else e2?
It would mean if let x := e in e then e else e stops parsing, but can still be parenthesized if (let x := e in e) then e else e (would need to change printing to use those parens).
Or use a new keyword if-let which probably isn't as disruptive?
Or ' like in let patterns and binders, ie if 'pattern := v then e1 else e2?

Not sure about isn't but do we actually need it?

[proux01]

We could have something like if let pattern := v then e1 else e2 instead of if v is pattern then e1 else e2

I don't like that, it reverses the term and the pattern, making it look different than the match-with usual syntax.

Not sure about isn't but do we actually need it?

Yes, for instance for the common idiom if l isn't cons x l' then <trivial thing> else <longer actual code using x and l'>. Sure you could write if l is cons x l' then <longer actual code using x and l'> else <trivial thing> but you definitely don't want to.

[yannl35133]

isn't could be "is"; IDENT "not", could it not?
EDIT: unless someone names a constructor "not"...

[SkySkimmer]

if e then 'pat => e else 'pat => e? not very pretty I guess (if e0 then e1 else 'pat => e2 would reorder branches to desugar to match e0 with pat => e2 | _ => e1 end)

[TheoWinterhalter]

I would say that the isn't version is very misleading, I wouldn't expect it to perform matching in the else branch.

[proux01]

isn't could be "is"; IDENT "not", could it not?

Would avoid making ins't a keyword but not sure it's worth it.

if e then 'pat => e else 'pat => e? not very pretty I guess

Well, at this point we can just write the match.

I would say that the isn't version is very misleading, I wouldn't expect it to perform matching in the else branch.

If you write things like if _ isn't _ then <very long term> else _ probably, but that's nothing specific to isn't. The common use case if rather if _ isn't <pattern with vars> then <short term obviously without vars> else <term with vars>

Don't forget that we have more than a decade of experience with the syntax in the entire mathcomp ecosystem and that it seems to work pretty well (at least in that context).

[TheoWinterhalter]

My understanding is that the syntax of mathcomp is the main barrier for adoption.

Which is not to mean that it's an argument to reject the notation, but just "trust me" seems a bit weak as argument for it. But I'm not part of the Rocq team so I will not fight against it of course.

Just to clarify I'm not trying to be mean, I just wanted to express my concerns and it's very likely misplaced.

[andres-erbsen]

I find the Rust if let syntax easier to read and write despite learning about the mathcomp syntax earlier having read more code that uses it.

[proux01]

"trust me" seems a bit weak as argument for it

The argument is not "trust me", rather: it has been used extensively, by many people for a long time, and proved effective (at least in that context, maybe more math oriented than PL community). You can browse all the codebase by yourself if you want to check.

Just to clarify I'm not trying to be mean, I just wanted to express my concerns and it's very likely misplaced.

No worries, any opinion is welcome, as long as it remain based on concrete arguments and facts.

I find the Rust if let syntax easier to read and write

I can indeed see that syntax fitting better in the C-like syntax of Rust (where "if" may be the primary control structure, no "then" keyword, no "in" keyword for "let",...) but it doesn't fit well in the ML like syntax of Rocq (with "match" being the main control structure, with "with" and "then" keywords, "let" always followed by "in",...). As already pointed above, such syntaxes with "let" reverse the order of the term and the pattern compared to the usual "match term with (| pattern => term)* end" syntax.

[SkySkimmer]

As already pointed above, such syntaxes with "let" reverse the order of the term and the pattern compared to the usual "match term

I don't think that's really a problem, we already have let 'pattern := e in e

[proux01]

That's my point, the pattern in let is only doing some destructuring, no control flow, since a let is a match with a single branch. In contrary, an if is essentially a match with multiple branches.

The case where the else branch is the main one (not uncommon, think about nat or list for instance) also remains unclear in that kind of proposals.

Anyway, I tried to sum up the discussion in the top message, feel free to point any argument I would have forgotten.

[TheoWinterhalter]

Another alternative could be to change if rather than the is. For instance

unless t is p then _ else _

The main advantage I see is that the pattern matching clause is still framed positively, so it restores, in my mind, the idea that some new variables are bound.

In any case, doesn't this syntax encourage bad matching like the following?

if n is 3 then _ else _

To me it now feels more natural to write, but you should actually not do it. You can make things worse by using a string rather than 3 in the above example.

[andres-erbsen]

I agree with @proux01 that the large-else-branch scenario is important and could benefit from nice shorthand syntax. (Thank you for stressing it, I had been thinking about the if .. is construct as the main feature until then.)

Here are some more options that come to mind that I would hope to be broadly recognizable:

let 'pattern := ex else default in eC (rust)

match ex with pattern else default in eC

and

let 'pattern := ex then eC else default

match ex with pattern => eC else default

To be confirmed whether they're compatible with the grammar, though.

[samuelgruetter]

Indeed, a construct that allowed me to write short error handling branches before a main branch that does not get formatted at a higher level of indentation, like eg the following, seems useful:

let 'x::xs := myList else None in
some lengthy code referring to x and xs;
formatted without an additional level of indentation;
finally returning
Some result

Or, if I understood correctly, the same using isn't would be

if myList isn't x::xs then None else
some lengthy code referring to x and xs;
formatted without an additional level of indentation;
finally returning
Some result

[proux01]

@samuelgruetter added to the if-let offer in the top message

[proux01]

To be discussed in a future Call: https://github.com/rocq-prover/rocq/wiki/Rocq-Call-2026-03-17

[SkySkimmer]

BTW we already have

rocq/theories/Corelib/Init/Notations.v

Line 113 in c4fa328

Notation "'if' c 'is' p 'then' u 'else' v" :=

[gares]

Shouldnt we remove the grammar rule from ssrewrite?

[proux01]

All overlays merged, CI green, this is ready

[gares]

@coqbot merge now