kernel error from `proofsInPublic`

Stream: lean4

[Jovan Gerbscheid]

If in one module, I write

@[no_expose] def five : Nat := 5

class A where
  a : five = 5
  b : Nat

set_option backward.proofsInPublic false in
instance : A where
  a := by rfl
  b := 0

Then in another module that imports it,

example : instA = { instA with b := 0 } := rfl

gives a kernel error:

(kernel) declaration type mismatch, '_private.MathlibTest.Real.0._example' has type
  instA = instA
but it is expected to have type
  instA =
    let __src := instA;
    { a := A.a }

I discovered this bug when trying to adapt Real to the module system.

Note that the set_option backward.proofsInPublic false in is only necessary in Mathlib. The default value of backward.proofsInPublic is already false.

[Sebastian Ullrich]

Thanks, fixed in #11673

[Sebastian Ullrich]

I discovered this bug when trying to adapt Real to the module system.

I believe @Kim Morrison and @Johan Commelin may have some thoughts on where to best start with such experiments, which may also inform how quickly this fix should land in a release.

[Michael Rothgang]

lean4#11673 (for anybody who wants to check, e.g. me)

[Johan Commelin]

@Jovan Gerbscheid Happy to discuss this further! Did you meet any other obstacles while modulizing Real?

One thought I had was to try this with some p-adic types, since they probably have fewer files depending on them. Eg WittVector will have very little depending on it (inside Mathlib, there's much more outside Mathlib, which we should be conscious of). And padicInt has some more material depending on it inside Mathlib, but much less than Real.

[Jovan Gerbscheid]

The PR is #32872. I've managed to work around the kernel error by not using rfl for the problematic proofs. All of mathlib builds, but there are some remaining errors in Counterexamples and Archive. There are some questions about which things should and should not be @[no_expose]. For example, we have a - b defined as a + -b, and a / b as a * b⁻¹. This defEq is actually used somewhere. We also have a ≤ b defined as a < b ∨ a = b, but I found that exposing this only lead to some proof working in an unexpected way.

I also made #32861 which does similar changes in a couple of other files.

[Johan Commelin]

I think none of those definitional details should be exposed.

[Kevin Buzzard]

No more sub_eq_add_neg defeq abuse?? What exactly do we gain from this?

Johan and I are old enough to remember the days when that was a simp lemma :-) Maybe we should go back to that :-) (no! no! no!)

[Jovan Gerbscheid]

I've now fixed the failures in #32872 by simply making those files into modules. Is there a plan to turn everything into modules in mathlib? (so, Counterexamples, and Archive, etc.)

[Jovan Gerbscheid]

Though there are some failures from the simpNF linter timing out. Does anyone know if simpNF is run in a module or not?

[Jovan Gerbscheid]

Also, the following error shows up from marking the projection Real.cauchy as private :sweat_smile:

/- The `structureInType` linter reports:
FOUND STRUCTURES THAT SHOULD BE IN PROP. -/
-- Mathlib.Data.Real.Basic
error: ℝ LINTER FAILED:
Unknown constant `Real.cauchy`