bound quantifier experiments

Stream: lean4

[Jeremy Avigad]

Has anyone tried implementing bounded quantifiers in Lean 4?

For context, I am working with mathlib4, which has these:

import Lean

class Mem (α : outParam $ Type u) (γ : Type v) where
  mem : α → γ → Prop

infix:50 " ∈ " => Mem.mem

notation:50 x " ∉ " s => ¬ x ∈ s

def mem (a : α) : List α → Prop
| [] => False
| (b :: l) => a = b ∨ mem a l

instance : Mem α (List α) := ⟨mem⟩

This seems to work reasonably well for parsing:

def forallb (l : List α) (p : α → Prop) := ∀ x, x ∈ l → p x
def existsb (l : List α) (p : α → Prop) := ∃ x, x ∈ l ∧ p x

macro "∀ " x:ident " ∈ " t:term ", " p:term : term => `(forallb $t fun $x => $p)
macro "∃ " x:ident " ∈ " t:term ", " p:term : term => `(existsb $t fun $x => $p)

#check ∀ x ∈ [1, 2, 3], x = x
#check ∃ x ∈ [1, 2, 3], x = x

I tried to see if I could get the expressions to pretty-print. This seems to have no effect:

@[appUnexpander forallb] def unexpandForallb : Lean.PrettyPrinter.Unexpander
 | `(forallb $l:term fun $x:ident => $p:term) => `(∀ $x ∈ $l, $p)
 | _ => throw ()

@[appUnexpander existsb] def unexpandExistsb : Lean.PrettyPrinter.Unexpander
  | `(existsb $l:term fun $x:ident => $p:term) => `(∃ $x ∈ $l, $p)
  | _ => throw ()

#check ∀ x ∈ [1, 2, 3], x = x
#check ∃ x ∈ [1, 2, 3], x = x

These definitions work reasonably well, but they leave the body of the expression eta-expanded:

section
open Lean PrettyPrinter.Delaborator

@[delab app.forallb] def delabForallb : Delab := do
  let e ← getExpr
  guard $ e.getAppNumArgs == 3
  let t ← withAppFn $ withAppArg delab
  let n := e.appArg!.bindingName!
  let p ← withAppArg delab
  let x := mkIdent n
  `(∀ $x ∈ $t, $p $x)

@[delab app.existsb] def delabExistsb : Delab := do
  let e ← getExpr
  guard $ e.getAppNumArgs == 3
  let t ← withAppFn $ withAppArg delab
  let n := e.appArg!.bindingName!
  let p ← withAppArg delab
  let x := mkIdent n
  `(∃ $x ∈ $t, $p $x)

end

#check ∀ x ∈ [1, 2, 3], x = x
#check ∃ x ∈ [1, 2, 3], x = x

I thought using withBindingBody would extract the body of the lambda expression, but then I get the error message indicated below:

section
open Lean PrettyPrinter.Delaborator

@[delab app.forallb] def delabForallb : Delab := do
  let e ← getExpr
  guard $ e.getAppNumArgs == 3
  let t ← withAppFn $ withAppArg delab
  let n := e.appArg!.bindingName!
  let p ← withBindingBody n $ withAppArg delab
  let x := mkIdent n
  `(∀ $x ∈ $t, $p)

@[delab app.existsb] def delabExistsb : Delab := do
  let e ← getExpr
  guard $ e.getAppNumArgs == 3
  let t ← withAppFn $ withAppArg delab
  let n := e.appArg!.bindingName!
  let p ← withBindingBody n $ withAppArg delab
  let x := mkIdent n
  `(∃ $x ∈ $t, $p)

end

#check ∀ x ∈ [1, 2, 3], x = x
#check ∃ x ∈ [1, 2, 3], x = x

-- failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) : Prop

I'd be grateful for any help or suggestions.

[Daniel Selsam]

@Jeremy Avigad Your unexpander just needs to include the type of the binder:

@[appUnexpander forallb] def unexpandForallb : Lean.PrettyPrinter.Unexpander
 | `(forallb $l:term fun $x:ident => $p:term) => `(∀ $x ∈ $l, $p)
 | `(forallb $l:term fun ($x:ident:$ty:term) => $p:term) => `(∀ $x ∈ $l, $p)
 | _ => throw ()

#check ∀ x ∈ [1, 2, 3], x = x -- ∀ x ∈ [1, 2, 3], x = x : Prop

[Jeremy Avigad]

Beautiful! Many thanks.

[Patrick Massot]

Did you manage to get bounded existential to expand to what we want?

[Jeremy Avigad]

The outcome of the #check is ∃ x ∈ [1, 2, 3], x = x : Prop, but we have

example : (∃ x ∈ [1, 2, 3], x = x) = (∃ x, x ∈ [1, 2, 3] ∧ x = x) := rfl

Is that what you were hoping for?

[Patrick Massot]

Yes!

[Jeremy Avigad]

@Daniel Selsam I am still curious as to why the longer code with withBindingBody did not work. (It is similar to the delaboration for dite expressions in PrettyPrinter/Delaborator/Builtins.lean. ) But if it is not easy to give me a quick answer, don't worry about it. I am just curious.

[Jeremy Avigad]

@Patrick Massot We should be able to generalize the notation to other types and other kinds of bounding (like <). I'll consult my oracle (Mario) as to how best to do it.

[Sebastian Ullrich]

You used the wrong order :)

  let p ← withAppArg $ withBindingBody n delab

[Daniel Selsam]

Yes, this works:

@[delab app.forallb] def delabForallb : Delab := do
  let e ← getExpr
  guard $ e.getAppNumArgs == 3
  let n := e.appArg!.bindingName!
  let x := mkIdent n
  let t ← withAppFn (withAppArg delab)
  let p ← withAppArg (withBindingBody n delab)
  `(∀ $x ∈ $t, $p)

#check ∀ x ∈ [1, 2, 3], x = x -- ∀ x ∈ [1, 2, 3], x = x : Prop

[Jeremy Avigad]

Whoa, all this monad trickery is above my pay grade. Initially, the expression being delaborated is of the form forallb t p. The let t ← ... picks out the t part. The next step is to get the body of p. Don't we have to get p first, and then get the binding body?

[Daniel Selsam]

The with* functions only change the ReaderT context, so when e.g. let t ← withAppFn (withAppArg delab) returns, the context is reset so that delab would refer back to the original expression.

[Daniel Selsam]

I may not have understood your question -- are you confused about the "resetting" or the order of the with* calls?

[Jeremy Avigad]

That's what I thought -- so that after the let t ← ... returns, we should be back to the original expression forallb t p. Then I would use expect withAppArg delab to return p, and then withBindingBody n (withAppArg delab) to return the body of p. So I guess it is the order of the with* calls that is confusing me.

[Daniel Selsam]

Yes, it is confusing :) Here is the relevant code for application:

def descend {α} (child : Expr) (childIdx : Nat) (d : DelabM α) : DelabM α :=
  withReader (fun cfg => { cfg with expr := child, pos := cfg.pos * 3 + childIdx }) d

def withAppFn {α} (d : DelabM α) : DelabM α := do
  let Expr.app fn _ _ ← getExpr | unreachable!
  descend fn 0 d

def withAppArg {α} (d : DelabM α) : DelabM α := do
  let Expr.app _ arg _ ← getExpr | unreachable!
  descend arg 1 d

So the line withAppFn (withAppArg delab) will evaluate withAppArg delab in the context of the app-function, which will evaluate delab in the context of the app-function's app-argument. So the "actions" go left-to-right.

[Jeremy Avigad]

Ah, yes, that makes sense. Many thanks for the patient explanation.