equation compiler magic in lean4

Stream: lean4

[Eric Rodriguez]

for example, consider this lean3 code:

inductive s : Type | A | B
example : s.A ≠ s.B.
example : s.A ≠ s.B := by {have : s.A ≠ s.B := λ h, match h with end, assumption}

how would we write these in lean4? I heard something about a nomatch keyword, but I can't seem to find much documentation about it

[Ruben Van de Velde]

I think with fun.

[Ruben Van de Velde]

theorem not_false' : ¬false := fun.

[Sebastian Ullrich]

There's documentation right in the editor as soon as you type in nomatch :) . Though I suppose you first need to know that it is a term syntax. https://leanprover-community.github.io/mathlib4_docs/Lean/Parser/Term.html#Lean.Parser.Term.nomatch

[Kyle Miller]

Ruben Van de Velde said:

theorem not_false' : ¬false := fun.

That . is a syntax error.

Here's one way to do nomatch:

example : s.A ≠ s.B := fun h => nomatch h

[Sebastian Ullrich]

If you want to golf: (nomatch ·)

[Ruben Van de Velde]

Kyle Miller said:

Ruben Van de Velde said:

theorem not_false' : ¬false := fun.

That . is a syntax error.

Here's one way to do nomatch:

example : s.A ≠ s.B := fun h => nomatch h

Really? I copied it from mathlib4

[Jannis Limperg]

The fun. syntax is a std4/mathlib4 addition.

[Kyle Miller]

@Sebastian Ullrich Has anyone considered nofun to go with nomatch?

macro "nofun" : term => `((nomatch ·))

inductive s : Type | A | B
example : s.A ≠ s.B := nofun

[Kevin Buzzard]

That's not appropriate because these proofs are a lot of fun

[Mario Carneiro]

Kyle Miller said:

Sebastian Ullrich Has anyone considered nofun to go with nomatch?

macro "nofun" : term => `((nomatch ·))

inductive s : Type | A | B
example : s.A ≠ s.B := nofun

That's exactly the fun. syntax mentioned above

[Alex Keizer]

Kyle Miller said:

Ruben Van de Velde said:

theorem not_false' : ¬false := fun.

That . is a syntax error.

Here's one way to do nomatch:

example : s.A ≠ s.B := fun h => nomatch h

IIRC, the fun . syntax is defined by mathlib4, not Lean itself

[Ruben Van de Velde]

Alex Keizer said:

Kyle Miller said:

Ruben Van de Velde said:

theorem not_false' : ¬false := fun.

That . is a syntax error.

Here's one way to do nomatch:

example : s.A ≠ s.B := fun h => nomatch h

IIRC, the fun . syntax is defined by mathlib4, not Lean itself

Yeah, Jannis mentioned this as well

[Kyle Miller]

@Mario Carneiro That may be functionally the same, but the serious part of what I was getting at is why not have the syntax parallel nomatch? You can't guess that fun. might be related.

[Kyle Miller]

@Mario Carneiro That may be functionally the same, but the serious part of what I was getting at is why not have the syntax parallel nomatch? You can't guess that fun. might be related.

[Mario Carneiro]

I actually prefer fun. for its syntactic consistency. There is also intro. and match x with. in the same file

[Mario Carneiro]

nomatch is a more special notation IMO

[Mario Carneiro]

it doesn't compose as well with other stuff

[Mario Carneiro]

(In case it isn't clear, the syntax pattern I want to encourage is that anywhere a | a => b list is accepted, a . also works and means an empty match)

[Sebastian Ullrich]

I like the consistency idea, but I can't say I like . specifically. It is essentially a Coq remnant that withered down to one specific use case.

[Mario Carneiro]

We can potentially do "nothing at all" as the marker, but that would have to be integrated with the original syntax

[Mario Carneiro]

this would be following my general plan to replace most uses of 1+ syntax in lean with 0+ syntax

[David Thrane Christiansen]

What about nested matches of constructorless types? Agda has the absurd pattern (), and it can occur in any position that expects a pattern, not just the top level. A pattern that validly contains an absurd pattern is then never associated with an RHS. It's quite convenient for pointing at precisely why a case is impossible.

[Mario Carneiro]

lean automatically does nested pattern matching of impossible cases, you just don't mention the case

[Mario Carneiro]

() is obviously not available as the absurd pattern in lean since it's the pattern for unit

[Sebastian Ullrich]

It's quite convenient for pointing at precisely why a case is impossible.

I think that would be a nice addition! Though perhaps not terribly high-priority.

[Sebastian Ullrich]

Mario Carneiro said:

We can potentially do "nothing at all" as the marker, but that would have to be integrated with the original syntax

I think we've rejected that for Lean 3 before. There should be something indicating an absurd pattern match

[Mario Carneiro]

okay, so... .

[Mario Carneiro]

it's derived from the lean 3 syntax but not the same, since it goes in arbitrary terms instead of only coming at the end of a definition

[Sebastian Ullrich]

Is this such a common occurrence that every character counts? I would much prefer a more readable notation such as match | absurd, which is forward-compatible with David's suggestion.

[Sebastian Ullrich]

Tbh the expected use frequency was the whole reason we introduced only nomatch and not nofun etc.

[Mario Carneiro]

yes, this does come up in places where every character counts

[Mario Carneiro]

Here is an example where I would really not have liked to need to use fun | absurd

[Mario Carneiro]

In Std, there are 47 uses of fun., 44 uses of nomatch and 2 uses of match e with. (these are used in places where match is used as a tactic, since there is no nomatch tactic)

[Mario Carneiro]

nomatch feels very ad hoc and incomplete compared to the others, since it is only defined for the expected common case

[David Thrane Christiansen]

I wasn't suggesting () as concrete syntax in Lean, just that it's nice to have _some_ syntax for absurd patterns. It's convenient to leave them out most of the time, but sometimes code communicates more when the author can be more explicit.

[Kevin Buzzard]

How about a Unicode contradiction symbol as notation for something like nomatch

[James Gallicchio]

When I show other CS students ocaml's | _ -> . absurd case syntax they do find the dot very confusing and arbitrary; I would not mind a symbol like \bot or a full absurd keyword to represent a pattern that matches an empty type with no RHS

[Parth Shastri]

What about having . functioning as an optional end? (Or if . is too terse, then just end) That way the syntax works beyond the special case of an empty match and could (though I wouldn't recommend it) be used to delimit nested matches without needing parentheses or indentation, which might be useful for macros:

match m with | 0 => n | 1 => match n with | 0 => m | n' + 1 => n'. | m' + 2 => m'

[James Gallicchio]

(that . is incredibly hard to spot in that snippet, but would love end)

[Sebastian Ullrich]

Why would this matter for macros? Macros manipulate syntax trees, not strings.

[Parth Shastri]

Interesting, I didn't realize that macros support matches with no branches:

macro "test%" : term =>
  let l := #[]
  let r := #[]
  `(match sorryAx False with $[| $l => $r]*)

#check test% -- nomatch (_ : False) : ?m.2440

So having an explicit terminator is not necessary.

[Mario Carneiro]

this is technically a malformed syntax object, since the parser is declared to accept one or more match branch... but yes, the rejection of empty matches is only "skin deep" - the support is all there in the backend, you just have to bypass the front end or pass an invalid syntax and hope that the syntax quotation code doesn't assert that the array is nonempty in the future

[Mario Carneiro]

That's how match e with. is implemented BTW - it just calls the match backend with an empty list of branches