Module system weirdness

Stream: mathlib4

[David Loeffler]

I just ran into a fascinating bug: if you take any of the dozens of lemmas in Mathlib that involve the complex norm function, and use the extract_goal tactic somewhere in the proof, then instead of printing the current goal, it gives a mystery error message:

Unknown constant `_private.Mathlib.Analysis.Complex.Norm.0.Complex.norm_nonneg`

The diagnosis seems to be the following:

• As a step in building the NormedAddCommGroup instance on ℂ, there is a private lemma Complex.norm_nonneg, which is flagged as private because it is no longer needed once the instance is complete (the root-level norm_nonneg lemma takes over).
• However, Complex.norm_nonneg is used for one of the fields of the instance Complex.isAbsoluteValueNorm, resulting in a public declaration that relies on a private one (against the rules of the module system).
• For some reason Lean doesn't complain about this at the point where Complex.isAbsoluteValueNorm is declared, but it causes extract_goal to complain if it is used in any later proof where complex numbers occur!

These mystery errors go away if we make Complex.norm_nonneg public; or if we conceal the use of a private lemma inside a tactic block, changing

instance isAbsoluteValueNorm : IsAbsoluteValue (‖·‖ : ℂ → ℝ) where
  abv_nonneg' := norm_nonneg
  ...

to

instance isAbsoluteValueNorm : IsAbsoluteValue (‖·‖ : ℂ → ℝ) where
  abv_nonneg' := by exact norm_nonneg
  ...

I'm very puzzled about how this is supposed to work.

• Why is it forbidden to use private lemmas as proof fields in defs? I would have expected that since we have proof-irrelevance, in particular it should be irrelevant whether proofs are private or not.
• If it's forbidden to do this in def's, why is it permitted in instances? (Edit: maybe Lean allows it if the instance is not data-carrying, i.e. lives in Prop rather than Type*?)
• Why does := by exact foo work if := foo does not?
• Why does the error only manifest itself when using extract_goal?

[Johan Commelin]

by exact foo makes the proof private instead of exposing it. That's (half of?) an answer to your 3rd q.
I hope others can step in with answering the rest.

[David Loeffler]

Johan Commelin said:

by exact foo makes the proof private instead of exposing it. That's (half of?) an answer to your 3rd q.

Since proofs are definitionally singletons in Lean's logic, what does it mean to "expose" a proof? Surely "revealing that a proof exists without revealing its implementation" is a meaningless distinction in the presence of proof irrelevance?

[Johan Commelin]

From the kernel's point of view, yes. But not from the point of view of other parts of the system. Eg, a tactic could inspect what an exposed proof looks like, if I understand correctly.

(In other words, in theory we could implement a using_the_same_strategy_as myFancyProof tactic.)

[David Loeffler]

Johan Commelin said:

(In other words, in theory we could implement a using_the_same_strategy_as myFancyProof tactic.)

But such a tactic would be pretty useless if it couldn't see inside a tactic block, wouldn't it? I mean, if myFancyProof is really all that fancy, it is bound to have a by in it somewhere.

[Johan Commelin]

Fair enough. It also wasn't a serious idea. Just trying to explain that different parts of the system have different povs on proof irrelevance. There might be better examples out there. But I'm not enough of an expert.

[David Loeffler]

I think distinguishing between "exposed" and "non-exposed" even for proofs is a bit silly; but even if that's the design intention here, then something is still wrong, because the IsAbsoluteValue instance is somehow exposing information that should be private (without raising an error in the process).