how to tell if defs rely on partial defs?

Stream: lean4

[James Gallicchio]

def infLoop := λ () => Id.run do
  let mut x := 0
  while true do
    x := x + 1
  return x

theorem bad : False := by
  suffices infLoop () = infLoop () + 1 by
    generalize infLoop () = x at this
    cases this
  simp [infLoop, Id.run, forIn, Lean.Loop.forIn]
  unfold Lean.Loop.forIn.loop

#print axioms infLoop

I originally thought partial infected all downstream declarations, but evidently it does not. Is there any way to tell if a definition relies on another partial definition? (and if so, which partial definition?)

Obviously I am stopped from proving false because I can't unfold through the partial definition, but I'm not sure how I would easily find that it relies on this partial function without just trying to prove something about its behavior.

I'm also curious if there's an easy way to see what opaque definitions a definition relies on, since it seems like a similar problem to me

[Mario Carneiro]

No, partial definitions are intentionally not viral

[Mario Carneiro]

opaque definitions are not axioms, they cannot be used to prove anything more than you already could

[James Gallicchio]

And partial definitions are implicitly opaque?

[Mario Carneiro]

they are explicitly opaque, try #print on them

[Mario Carneiro]

Your code is making the assumption that a partial definition satisfies its definitional equation, and this is generally false

[James Gallicchio]

Ah :big_smile: didn't know print shows that!

And I see that this is sound, that part makes sense to me -- but is there any way to see what opaque definitions a given symbol depends on? I'm not really concerned about soundness but rather as a human checking whether a given function is partial (even transitively so)

[Mario Carneiro]

Looking at the dependency graph won't tell you if a function is partial

[Mario Carneiro]

because the partial function might actually be total

[Mario Carneiro]

it might even be proved total

[Mario Carneiro]

But if you want to you can do #print axioms yourself, just copy and modify the code

[Mario Carneiro]

src4#Lean.Elab.Command.elabPrintAxioms

[James Gallicchio]

Will put it on the list of things to check out at some point :)