How to print shadowed declarations?

Stream: lean4

[Eric Rodriguez]

Take this code:

structure Box where
  a : Nat
  b : Nat
deriving BEq

#print instBEqBox -- { beq := beqBox✝ }

Turning on pp.sanitizeNames does let you access the underlying name of this, but this changes on the ngen and such like so we can't actually access it. It'd be really nice to print it so that I could modify the instance generated by deriving without having to rewrite the scaffolding.

[Eric Rodriguez]

I was told about open private here but I just can't get it to work. I am told that there is private declarations, but can't seem to figure out the syntax to actually do the opening.

[Mario Carneiro]

this is not a private declaration (well it is but that's not the problem because you are still in the same module as the declaration), it is a declaration with an inaccessible name. You can call #print if you construct the name manually:

import Lean
open Lean

structure Box where
  a : Nat
  b : Nat
deriving BEq

set_option pp.sanitizeNames false in
#print instBEqBox
-- def instBEqBox : BEq Box :=
-- { beq := beqBox.22 }

run_cmd Elab.Command.elabCommand <|←
  `(#print $(mkIdent (addMacroScope (← getMainModule) `beqBox 22)))
-- private def beqBox._@.Mathlib.Test._hyg.22 : Box → Box → Bool :=
-- fun x x_1 ↦
--   match x, x_1 with
--   | { a := a, b := a_1 }, { a := b, b := b_1 } => true && a == b && a_1 == b_1
--   | x, x_2 => false

[Mario Carneiro]

(The fact that several deriving instances produce global declarations with inaccessible names is a recurring source of issues, and I've been planning to write a PR to make them accessible for some time. For example this causes an issue if you want to prove that an autogenerated Ord or BEq instance is lawful.)

[Eric Rodriguez]

Thanks! This really does seem quite annoying. One thing I've been meaning to figure out is macro scopes - what are they and how should I use them?

[Robert Maxton]

They're the scope of a macro :p. That is, the 'jurisdiction' of a macro over names and definitions. When a new macro is begun (controlled I think primarily withNewMacroScope?), it gets to include its macro scope (which is apparently implemented as just a unique number, probably encoding nesting of macros?) into the name of all (parsing) variables it introduces; this enforces hygiene requirements.

[Robert Maxton]

ah, yeah, here: docs#Lean.MacroScope

[Robert Maxton]

So, in theory, you should introduce a new macro scope whenever there might be danger of name collision of parse variables. In practice I think it's not much used/handled for you when writing notation or simple macro_rules and elab_rules, but more involved elaborators pretty much all start with withNewMacroScope do, and also if you might collide with yourself (through a recursive call, for example) that should get a withNewMacroScope do as well.

[Eric Rodriguez]

Ahh, so that number 22 is a macro-scope in this case. It does seem odd to me because I feel like no macros have been involved here, but I guess (a) most things are macros in some way or another and (b) it's probably the macro scope of the deriving stuff. [Not sure whether multiple derivings would have same or different macro scopes, I guess it depends on the implementation...].

[Kyle Miller]

It's possible to make a command that prints the value after unfolding all inaccessible constants (i.e., the ones with macro scopes):

structure Box where
  a : Nat
  b : Nat
deriving BEq

open Lean Elab Command in
elab "#print_val " id:ident : command => do
  addCompletionInfo <| CompletionInfo.id id id.getId (danglingDot := false) {} none
  let c ← resolveGlobalConstNoOverloadWithInfo id
  let some d := (← getEnv).find? c | throwError "unknown identifier '{mkConst c}'"
  let some val := d.value? | throwError "no value for decl"
  let val ← liftTermElabM <| Meta.transform val
    (pre := fun e => do
      if let .const n .. := e.getAppFn' then
        if n.hasMacroScopes then
          if let some e' ← Meta.unfoldDefinition? e then
            return .visit e'
      return .continue)
  logInfo m!"{val}"

#print_val instBEqBox
/-
{
  beq := fun x x_1 ↦
    (fun motive x x_2 h_1 h_2 ↦ Box.casesOn x fun a b ↦ Box.casesOn x_2 fun a_1 b_1 ↦ h_1 a b a_1 b_1) (fun x x ↦ Bool)
      x x_1 (fun a a_1 b b_1 ↦ true && a == b && a_1 == b_1) fun x x ↦ false }
-/

[Malvin Gattinger]

Together with @Andrés Goens we are trying to print the internals of a derived DecdiableEq instance using the code by @Kyle Miller above. Somehow this works for a simple type, but not for something properly inductive.

import Lean

open Lean Elab Command in
elab "#print_val " id:ident : command => do
  addCompletionInfo <| CompletionInfo.id id id.getId (danglingDot := false) {} none
  let c : Name ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo id
  let some d := (← getEnv).find? c | throwError "unknown identifier '{mkConst c}'"
  let some val := d.value? | throwError "no value for decl"
  let val ← liftTermElabM <| Meta.transform val
    (pre := fun e => do
      if let .const n .. := e.getAppFn' then
        if n.hasMacroScopes then
          if let some e' ← Meta.unfoldDefinition? e then
            return .visit e'
      return .continue)
  logInfo m!"{val}"


inductive ABox : List Nat → Type
  | b : ABox []
  | a : ABox l -- no recursion
deriving DecidableEq

#print instDecidableEqABox -- ... fun {a} => decEqABox✝
#print_val instDecidableEqABox -- ... nice detailed output :-)


inductive Box : List Nat → Type
  | b : Box []
  | a : Box [] → Box l -- recursion
deriving DecidableEq

theorem bla : Box.b ≠ Box.a Box.b := by decide -- DecidableEq works.

#print_val instDecidableEqBox -- ... fun {a} => decEqBox✝ -- Why is this not unfolded?

What is happening here / preventing this? Thanks for any suggestions :)

[Aaron Liu]

it's smart unfolding

[Aaron Liu]

set_option smartUnfolding false
/--
info: fun {a} x x_1 =>
  Box.brecOn (motive := fun {a} x => (x_2 : Box a) → Decidable (x = x_2)) x
    (fun {a} x f x_2 =>
      (fun x_3 =>
          Box.casesOn (motive := fun a_1 x_4 =>
            a = a_1 →
              x ≍ x_4 →
                (fun a x x_5 =>
                    Box.below (motive := fun {a} x => (x_6 : Box a) → Decidable (x = x_6)) x → Decidable (x = x_5))
                  a x x_2)
            x_3
            (fun h =>
              Eq.ndrec (motive := fun a =>
                (x x_4 : Box a) →
                  x ≍ Box.b →
                    (fun a x x_5 =>
                        Box.below (motive := fun {a} x => (x_6 : Box a) → Decidable (x = x_6)) x → Decidable (x = x_5))
                      a x x_4)
                (fun x x_4 h =>
                  ⋯ ▸
                    Box.casesOn (motive := fun a x =>
                      [] = a →
                        x_4 ≍ x →
                          (fun a x x_5 =>
                              Box.below (motive := fun {a} x => (x_6 : Box a) → Decidable (x = x_6)) x →
                                Decidable (x = x_5))
                            [] Box.b x_4)
                      x_4 (fun h h => ⋯ ▸ (fun a x => isTrue ⋯) ())
                      (fun {l} a h =>
                        Eq.ndrec (motive := fun {l} =>
                          x_4 ≍ a.a →
                            (fun a x x_5 =>
                                Box.below (motive := fun {a} x => (x_6 : Box a) → Decidable (x = x_6)) x →
                                  Decidable (x = x_5))
                              [] Box.b x_4)
                          (fun h => ⋯ ▸ (fun a x => isFalse ⋯) a) h)
                      ⋯ ⋯)
                ⋯ x x_2)
            fun {l} a_1 h =>
            Eq.ndrec (motive := fun {l} =>
              x ≍ a_1.a →
                (fun a x x_4 =>
                    Box.below (motive := fun {a} x => (x_5 : Box a) → Decidable (x = x_5)) x → Decidable (x = x_4))
                  a x x_2)
              (fun h =>
                ⋯ ▸
                  Box.casesOn (motive := fun a_2 x =>
                    a = a_2 →
                      x_2 ≍ x →
                        (fun a x x_4 =>
                            Box.below (motive := fun {a} x => (x_5 : Box a) → Decidable (x = x_5)) x →
                              Decidable (x = x_4))
                          a a_1.a x_2)
                    x_2
                    (fun h =>
                      Eq.ndrec (motive := fun a =>
                        (x : Box a) →
                          x ≍ Box.b →
                            (fun a x x_4 =>
                                Box.below (motive := fun {a} x => (x_5 : Box a) → Decidable (x = x_5)) x →
                                  Decidable (x = x_4))
                              a a_1.a x)
                        (fun x h => ⋯ ▸ (fun a x => isFalse ⋯) a_1) ⋯ x_2)
                    (fun {l} a_2 h =>
                      Eq.ndrec (motive := fun {l} =>
                        x_2 ≍ a_2.a →
                          (fun a x x_4 =>
                              Box.below (motive := fun {a} x => (x_5 : Box a) → Decidable (x = x_5)) x →
                                Decidable (x = x_4))
                            a a_1.a x_2)
                        (fun h =>
                          ⋯ ▸
                            (fun x a b x_4 =>
                                let inst := x_4.1 b;
                                if h : a = b then
                                  h ▸
                                    let inst := x_4.1 a;
                                    isTrue ⋯
                                else isFalse ⋯)
                              a a_1 a_2)
                        h)
                    ⋯ ⋯)
              h)
        x ⋯ ⋯ f)
    x_1
-/
#guard_msgs in
#print_val instDecidableEqBox

[Malvin Gattinger]

Cool, thank you!

[Aaron Liu]

with smart unfolding you get to unfold with the equational lemmas
@decEqBox✝ [] .b .b = isTrue decEqBox._proof_1✝
@decEqBox✝ [] .b (.a b) = isFalse ⋯
@decEqBox✝ [] (.a a) .b = isFalse ⋯
@decEqBox✝ l (.a a) (.a b) = if h : a = b then h ▸ have inst := decEqBox✝ a a; isTrue ⋯ else isFalse ⋯

[Malvin Gattinger]

We are trying to get a self-contained proof term, so is there a way to also avoid/unfold the ... ._proof_ parts?

import Lean

open Lean Elab Command in
elab "#print_val " id:ident : command => do
  addCompletionInfo <| CompletionInfo.id id id.getId (danglingDot := false) {} none
  let c : Name ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo id
  let some d := (← getEnv).find? c | throwError "unknown identifier '{mkConst c}'"
  let some val := d.value? | throwError "no value for decl"
  let val ← liftTermElabM <| Meta.transform val
    (pre := fun e => do
      if let .const n .. := e.getAppFn' then
        if n.hasMacroScopes then
          if let some e' ← Meta.unfoldDefinition? e then
            return .visit e'
      return .continue)
  logInfo m!"{val}"

inductive Box : List Nat → Type
  | b : Box []
  | a : Box [] → Box l -- recursion
deriving DecidableEq

theorem bla : Box.b ≠ Box.a Box.b := by decide -- DecidableEq works.

set_option pp.proofs true
set_option pp.deepTerms true
set_option pp.maxSteps 1000000000000
set_option smartUnfolding false
#print_val instDecidableEqBox -- still contains `(decEqBox._proof_4✝ x a)` etc.

[Kyle Miller]

Mathlib has docs#Lean.Meta.unfoldAuxLemmas for unfolding these aux lemmas

[Kyle Miller]

You don't need mathlib if you don't want for it; it's a tiny definition you can copy out of the library.

I think you could even just copy the Lean.Name.isAuxLemma definition and then change the #print_val command to use the condition n.hasMacroScopes || n.isAuxLemma.