A tactic or option to see all var, fun and const

Stream: Is there code for X?

[V S]

Hello! Is there a specific set_option or tactic like show_term that shows all the variables, functions and constants used in the specific string of proof with their types? For example, for theorem q {x : Real} {f : Real -> Real} (h0: ∀ x, f x = x + 1): (2 : Real) ^ (f x) = (2 : Real) ^ (x + 1) := by sorry, it would be nice to be able to automatically get x : Real, f : Real -> Real, 2 : Real (and possibly 1 : Real) and, if there was a lemma used to prove q which didn't define but used f in its statement, f would still appear in a 'wanted tactic\option' result. The closest thing I know about is trace.Meta.isDefEq, but it has too much unwanted info about metavariables (that I have no idea how to use to get the needed info). If it's impossible to get var+fun+const, but possible for var+fun, it would still be very helpful.

[Kenny Lau]

what about #print q

[V S]

Kenny Lau said:

what about #print q

I've tried it for the following,

import Mathlib

theorem q {x : Real} {f : Real -> Real} (h0: ∀ x, f x = x + 1): (2 : Real) ^ (f x) = (2 : Real) ^ (x + 1) := by
  have h {x : Real}: f 2 = 3 := by
    simp_all
    norm_num
  sorry
  #print h
#print q

and it doesn't mention that the f in h is the same as f in q or mention it in the 'breakthrough' of h:

theorem q : ∀ {x : ℝ} {f : ℝ → ℝ}, (∀ (x : ℝ), f x = x + 1) → 2 ^ f x = 2 ^ (x + 1) :=
fun {x} {f} h0 =>
  have h := fun {x} =>
    Eq.mpr (id (congrArg (fun x => x = 3) ((fun x => h0 x) 2)))
      (Mathlib.Meta.NormNum.isNat_eq_true
        (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))
          (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl 3))
        (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3)));
  sorry

Although it is easy for a human to understand what variables etc are used in what parts of the proof by just taking a look at both the theorem and the output of print, I want to kind of automate this process, so that the script (if there is no such tactic/option) would take some code and be able to easily identify all variables etc, and I'm not sure how to do it for h in this instance, especially since #print h won't work

[Kenny Lau]

@V S write set_option pp.all true before that

[Robin Arnez]

Do you want something like

import Lean

open Lean
def usedStuff (n : Name) : CoreM MessageData := do
  let info ← getConstInfo n
  let consts := info.getUsedConstantsAsSet
  let mut msgs := #[]
  for c in consts do
    let val ← getConstVal c
    let type := val.type
    let levels := val.levelParams
    msgs := msgs.push m!"{Expr.const c (levels.map Level.param)} : {type}"
  return MessageData.joinSep msgs.toList "\n"

elab "#show_used_constants " n:ident : command => do
  let msg ← Elab.Command.liftCoreM (usedStuff n.getId)
  Lean.logInfo msg

#show_used_constants usedStuff

which prints

@pure : {f : Type u → Type v} → [self : Pure f] → {α : Type u} → α → f α
@getConstInfo : {m : Type → Type} → [Monad m] → [MonadEnv m] → [MonadError m] → Name → m ConstantInfo
MessageData : Type
@MonadError.mk : {m : Type → Type} →
  [toMonadExceptOf : MonadExceptOf Exception m] →
    [toMonadRef : MonadRef m] → [toAddErrorMessageContext : AddErrorMessageContext m] → MonadError m
instMonadExceptOfExceptionCoreM : MonadExceptOf Exception CoreM
Std.instToFormatString : ToFormat String
MessageData.joinSep : List MessageData → MessageData → MessageData
Core.instMonadRefCoreM : MonadRef CoreM
@Array.push : {α : Type u} → Array α → α → Array α
ConstantVal : Type
ConstantVal.levelParams : ConstantVal → List Name
ConstantInfo.getUsedConstantsAsSet : ConstantInfo → NameSet
ReaderT : Type u → (Type u → Type v) → Type u → Type (max u v)
NameSet : Type
String : Type
@List.map : {α : Type u} → {β : Type v} → (α → β) → List α → List β
Core.instMonadEnvCoreM : MonadEnv CoreM
Expr.const : Name → List Level → Expr
instAddErrorMessageContextOfAddMessageContextOfMonad : (m : Type → Type) →
  [AddMessageContext m] → [Monad m] → AddErrorMessageContext m
MessageData.instAppend : Append MessageData
@Function.comp : {α : Sort u} → {β : Sort v} → {δ : Sort w} → (β → δ) → (α → β) → α → δ
ConstantVal.type : ConstantVal → Expr
instToMessageDataExpr : ToMessageData Expr
Expr : Type
IO.RealWorld : Type
Level.param : Name → Level
EIO : Type → Type → Type
@forIn : {m : Type u₁ → Type u₂} →
  {ρ : Type u} →
    {α : outParam (Type v)} → [self : ForIn m ρ α] → {β : Type u₁} → [Monad m] → ρ → β → (α → β → m (ForInStep β)) → m β
Level : Type
@instMonadEIO : {ε : Type} → Monad (EIO ε)
MessageData.ofFormat : Format → MessageData
@Applicative.toPure : {f : Type u → Type v} → [self : Applicative f] → Pure f
ForInStep : Type u → Type u
instToMessageDataString : ToMessageData String
@Array.toList : {α : Type u} → Array α → List α
@List.toArray : {α : Type u_1} → List α → Array α
@format : {α : Type u} → [self : ToFormat α] → α → Format
Array : Type u → Type u
@instHAppendOfAppend : {α : Type u_1} → [Append α] → HAppend α α α
List : Type u → Type u
Core.State : Type
CoreM : Type → Type
StateRefT' : Type → Type → (Type → Type) → Type → Type
@StateRefT'.instMonad : {ω σ : Type} → {m : Type → Type} → [Monad m] → Monad (StateRefT' ω σ m)
PUnit : Sort u
@toMessageData : {α : Type} → [self : ToMessageData α] → α → MessageData
Format : Type
@NameSet.instForInName : {m : Type u_1 → Type u_2} → ForIn m NameSet Name
Name : Type
@Monad.toBind : {m : Type u → Type v} → [self : Monad m] → Bind m
@bind : {m : Type u → Type v} → [self : Bind m] → {α β : Type u} → m α → (α → m β) → m β
PUnit.unit : PUnit
Core.instMonadCoreM : Monad CoreM
ConstantInfo : Type
@ReaderT.instApplicativeOfMonad : {ρ : Type u} → {m : Type u → Type v} → [Monad m] → Applicative (ReaderT ρ m)
@getConstVal : {m : Type → Type} → [Monad m] → [MonadEnv m] → [MonadError m] → Name → m ConstantVal
Core.instAddMessageContextCoreM : AddMessageContext CoreM
@HAppend.hAppend : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HAppend α β γ] → α → β → γ
Exception : Type
@ForInStep.yield : {α : Type u} → α → ForInStep α
Core.Context : Type
@List.nil : {α : Type u} → List α

[V S]

Kenny Lau said:

set_option pp.all true

Thank you! The pp.all goes into 'too much info to get the parameters properly' territory, but I feel like there might be a combination of 'pp.something's that will give me enough info to easily identify everything I need and not drown in oversimplifications (for this purpose)

[Kenny Lau]

@V S you said the first option was catering for humans, and now you say that the second option is not human-readable, so which one do you want?

[Kenny Lau]

anyway Robin's code above seems to be better?

[V S]

@Robin Arnez I have not used structures like these yet, but will try to figure out how it all works, thank you! Right now I can't seem to figure out how to use both the code you provided and my code (so that it will work for arbitrary proof)

[Robin Arnez]

Does it not work for an arbitrary proof? It at least should just show all constants it depends on

[Robin Arnez]

Even though the result might not be too useful

[Robin Arnez]

Since it contains proofs + types as well

[V S]

Kenny Lau said:

V S you said the first option was catering for humans, and now you say that the second option is not human-readable, so which one do you want?

Sorry for the confusion :smiling_face_with_tear: I mistakenly thought that 2 and 3 from the example were somehow broken down as well which was stupid of me to think since they are Real, but the main thing I wanted to convey is 'I had no idea about pp and it seems like I can 'customise' the output to my advantage, so I will try and understand how it all works, so thank you for giving me a research direction'

[Kenny Lau]

yeah you can play around with the pretty printer to see what you want

[Kenny Lau]

you probably want set_option pp.explicit true first

[V S]

Robin Arnez said:

Does it not work for an arbitrary proof? It at least should just show all constants it depends on

I'm probably too much of a noob in Lean to understand how to combine your code and proofs. Do they go in one lean file (tried it, didn't work) or is your code used somewhere else? So I will probably first try to get an understanding of everything in your code which will hopefully lead me to the answer (since I don't want to waste anyone's time when I know what I could try to do to get it myself)

[Robin Arnez]

You could copy every except for the import Lean

[Robin Arnez]

Shouldn't matter which file

[V S]

Kenny Lau said:

set_option pp.explicit true

Thank you, that is way easier for me to work with!

[V S]

Robin Arnez said:

You could copy every except for the import Lean

I've tried

for this code

import Lean

import Mathlib

set_option pp.explicit true

open Lean

def usedStuff (n : Name) : CoreM MessageData := do

  let info ← getConstInfo n

  let consts := info.getUsedConstantsAsSet

  let mut msgs := #[]

  for c in consts do

    let val ← getConstVal c

    let type := val.type

    let levels := val.levelParams

    msgs := msgs.push m!"{Expr.const c (levels.map Level.param)} : {type}"

  return MessageData.joinSep msgs.toList "\n"

elab "#show_used_constants " n:ident : command => do

  let msg ← Elab.Command.liftCoreM (usedStuff n.getId)

  Lean.logInfo msg

theorem q {x : Real} {f : Real -> Real} (h0: ∀ x, f x = x + 1): (2 : Real) ^ (f x) = (2 : Real) ^ (x + 1) := by

  have h: f 2 = 3 := by

    simp_all

    norm_num

  sorry

#print q

#show_used_constants usedStuff

[Robin Arnez]

Try #show_used_constants q

[Kyle Miller]

You might like #explode from mathlib, which gives the types of many intermediate parts of an expression, but it's focused on proofs, so you won't see that 1 is Real, just each intermediate proof term.

[Kyle Miller]

You also might be interested in the pp.numericTypes option, which helps with understanding numeric constants in expressions.

[V S]

Robin Arnez said:

Try #show_used_constants q

Right, thank you! This does work and I will also try to process the input

[V S]

@Kyle Miller thank you, that's also very helpful!