Zulip Chat Archive

Stream: lean4

Topic: bound quantifier experiments


Jeremy Avigad (Jun 24 2021 at 21:09):

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 (Jun 24 2021 at 21:17):

@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 (Jun 24 2021 at 21:22):

Beautiful! Many thanks.

Patrick Massot (Jun 24 2021 at 21:24):

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

Jeremy Avigad (Jun 24 2021 at 21:28):

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 (Jun 24 2021 at 21:30):

Yes!

Jeremy Avigad (Jun 24 2021 at 21:31):

@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 (Jun 24 2021 at 21:33):

@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 (Jun 24 2021 at 21:39):

You used the wrong order :)

  let p  withAppArg $ withBindingBody n delab

Daniel Selsam (Jun 24 2021 at 21:42):

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 (Jun 24 2021 at 21:49):

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 (Jun 24 2021 at 21:52):

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 (Jun 24 2021 at 21:54):

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

Jeremy Avigad (Jun 24 2021 at 21:56):

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 (Jun 24 2021 at 22:01):

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 (Jun 24 2021 at 22:04):

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


Last updated: Dec 20 2023 at 11:08 UTC