Josh Tilles, and a metaprogramming question

Stream: new members

[Josh Tilles]

:wave: Hello all! I’m a software developer with a hobbyist interest in math-y topics, particularly interested in using Lean to work through the exercises and puzzles of various books I’m reading.

I think I’d like some help getting started with Lean.PrettyPrinter.Parenthesizer… The following code block provides the details and context for why I’m asking.

-- I’m tinkering with Lean to write up my solutions to the exercises in Raymond Smullyan’s *To Mock a Mockingbird*.

-- I’m trying to bring the code nearer to the book's conventions. I'd especially appreciate help on the printing side of things (like, in the proof state).

-- “A certain enchanted forest is inhabited by talking birds. Given any birds A and B, if you call out the name of B to A, then A will respond by calling out the name of some bird to you”

inductive Bird : Type where
  | call : Bird → Bird → Bird

/-
“By a *mockingbird* is meant a bird M such that for any bird x, the following condition holds:

    Mx = xx

M is called a mockingbird for the simple reason that its response to any bird x is the same as x’s response to itself—in other words, M *mimics* x as far as its response to x goes. This means that if you call out x to M or if you call out x to itself, you will get the same response in either case.”
-/

def Bird.is_a_mockingbird__v0 (M : Bird) : Prop :=
  ∀ x : Bird, M.call x = x.call x

-- Allow writing the bird equations more directly by treating the birds like functions:

instance : CoeFun Bird (fun _ => Bird → Bird) where
  coe := Bird.call

def Bird.is_a_mockingbird (M : Bird) : Prop :=
  ∀ x : Bird, M x = x x

def Bird.is_a_bluebird (B : Bird) : Prop :=
  ∀ x y z : Bird, B x y z = x (y z)

def Bird.is_an_eagle (E : Bird) : Prop :=
  ∀ x y z w v : Bird, E x y z w v = x y (z w v)

-- A sample problem: prove than an eagle can be derived from a bluebird.
example : (∃ B : Bird, B.is_a_bluebird) → ∃ E : Bird, E.is_an_eagle :=
  sorry  -- solution omitted since it's not the emphasis of my current question

variable (B E a b c d e : Bird)
  (hB : B.is_a_bluebird)
  (hE : E.is_an_eagle)

-- The below example shows how the equations become unwieldy pretty quickly:

/--
info: hB a b : ∀ (z : Bird), ((B.call a).call b).call z = a.call (b.call z)
-/
#guard_msgs in
#check hB a b

-- I tried asking Claude and it directed me to the `app_unexpander` attribute.

@[app_unexpander Bird.call]
def unexpandBirdCall : Lean.PrettyPrinter.Unexpander
  | `($_ $x $y) => ``($x $y)
  | _ => throw ()

-- That results in a significant improvement!

/--
info: hB a b : ∀ (z : Bird), ((B a) b) z = a (b z)
-/
#guard_msgs in
#check hB a b

-- However, there are still more parentheses in the output than seem necessary.
-- I'll construct a slightly more complex example to illustrate the improvement I'd like to see.

/--
info: hE a b c d e : ((((E a) b) c) d) e = (a b) ((c d) e)
-/
#guard_msgs in
#check hE a b c d e

-- I’d like the printed output to reflect the convention of left-associativity.
-- hE a b c d e : E a b c d e = a b (c d e)

-- I’m guessing `Lean.PrettyPrinter.Parenthesizer` is relevant here but it's unclear to me how to get started applying it to the code thus far.

[Kyle Miller]

What's going on is that applications are Syntax objects, and they're supposed to include a list of all arguments that are part of that application. Having the function itself be an application necessitates parentheses since Lean will elaborate (f a b) c d slightly differently from f a b c d.

You can write an unexpander that looks for applications and merges them:

@[app_unexpander Bird.call]
def unexpandBirdCall : Lean.PrettyPrinter.Unexpander
  | `($_ $x $ys*) =>
    match x with
    | `($x $xs*) => `($x $xs* $ys*)
    | _ => `($x $ys*)
  | _ => throw ()

/-- info: hB a b : ∀ (z : Bird), B a b z = a (b z) -/
#guard_msgs in
#check hB a b

/-- info: hE a b c d e : E a b c d e = a b (c d e) -/
#guard_msgs in
#check hE a b c d e