Pattern matching inside forall binder

Stream: general

[Jason Rute]

I doubt this exists, but I want to be sure. Lean has nice pattern matching features in many cases:

#check fun (⟨i, j⟩ : Nat × Nat) => i + j
#check let ⟨i, j⟩ := (1,2) ; i + j
#check { ⟨x,y⟩ : ℕ × ℕ | x < y }

But one missing case seems to be forall binders (and pi binders and exists binders), both pure forall binders and various notational versions. Is there a reason for this? Is this notation just not added yet?

#check ∀ (⟨i, j⟩ : Nat × Nat), i = j
#check ∀ ⟨i,j⟩ ∈ { ⟨x,y⟩ : ℕ × ℕ | x < y }, i < j

I understand why we don't want to support, say:

example (⟨i, j⟩ : Nat × Nat) : i = j := sorry

for the same reason we don't support

example (i < 1) : i = 0 := sorry

But it seems to me that extending the ∀ ... ∈ ... notation to support, say,

#check ∀ ⟨i,j⟩ ∈ { ⟨x,y⟩ : ℕ × ℕ | x < y }, i < j

would be very convenient. (This came up in practice as I was writing an answer to this PA.SX question. This notation would have made things a lot easier.)

[Eric Wieser]

I guess ∀ ⟨i, j⟩ ∈ s, i < j would desugar to ∀ p, match p with | ⟨i, j⟩ => ⟨i, j⟩ ∈ s -> i < j?

[Mario Carneiro]

Jason Rute said:

for the same reason we don't support

example (i < 1), i = 0 := sorry

This actually used to be supported in lean 3 (you need a : instead of , in these examples though)

[Mario Carneiro]

I think things would be much more consistent if there was a "binder" grammatical category instead of 3 or 4 different definitions of what a binder is

[Robin Arnez]

I think one problem is whether you want
∀ (a b : Nat), (a, b) ∈ [(1, 2), (3, 4), (5, 6)] → a < b : Prop
or
∀ (x : Nat × Nat), match x with | (a, b) => (a, b) ∈ [(1, 2), (3, 4), (5, 6)] → a < b : Prop
I would guess the first one would be preferable but then we probably need some help from match elaboration to tell us which variables are pattern variables (since it's not always completely obvious)

[Robin Arnez]

e.g. should ∀ .inl a ∈ [Sum.inl 3, Sum.inr true, Sum.inl 9], a < b fail?

[Eric Wieser]

Could we reuse .() notation to mark the intended behvaior, something like ∀ some (long condition (involving .(x))), p x

[Robin Arnez]

The meaning is not quite the same since .(_) usually stands in place of a pattern

[Robin Arnez]

Really what I mean though is that we can't implement this just as macro (if we won't it to be correct)

[Robin Arnez]

We would need to use something like docs#Lean.Elab.Term.getPatternVars

[Jakub Nowak]

Instead of ∀ (x : Nat × Nat), match x with | (a, b) => (a, b) ∈ [(1, 2), (3, 4), (5, 6)] → a < b : Prop, I think this is more clear: ∀ (x : Nat × Nat) ∈ [(1, 2), (3, 4), (5, 6)], match x with | (a, b) => a < b : Prop.

[Jakub Nowak]

The way you wrote it, I don't see a difference between the two.

[Robin Arnez]

Okay, here's a proof of concept:

import Lean

syntax (name := forallTerm) (priority := low) "∀ " term:lead binderPred ", " term : term

open Lean Elab Term

@[term_elab forallTerm]
def elabForallTerm : TermElab := fun stx e? => do
  match stx with
  | `(∀ $d:term $p:binderPred, $b:term) =>
    let vars : Array Ident := TSyntaxArray.mk (← getPatternVars d)
    let newStx ← `(∀ $[$vars:ident]*, satisfies_binder_pred% $d $p → $b)
    withMacroExpansion stx newStx do
      elabForall newStx e?
  | _ => throwUnsupportedSyntax

variable (s : List (Nat × Nat))

/-- info: ∀ (i j : Nat), (i, j) ∈ s → i < j : Prop -/
#guard_msgs in
#check ∀ ⟨i, j⟩ ∈ s, i < j

/-- info: ∀ (a : Nat), Sum.inl a ∈ [Sum.inl 13, Sum.inr true] → a = 13 : Prop -/
#guard_msgs in
#check ∀ .inl a ∈ [Sum.inl 13, Sum.inr true], a = 13