Strange module system sorries

Stream: new members

[Snir Broshi]

module

import Mathlib.Combinatorics.SimpleGraph.Basic

@[expose] public section

variable {V : Type*} {G : SimpleGraph V}

theorem foo (h₁ : G.foo) (h₂ : G.bar) : G.baz := by
  exact h₁

The goal state at the start of the theorem is:

h₁ : sorry
h₂ : sorry
⊢ sorry

Adding public before the import fixes it, but surely there should be errors everywhere, and the file shouldn't just build?

[Snir Broshi]

Here's a compiling proof of the Riemann hypothesis with no sorry in the source (although it does mark it as declaration uses 'sorry'):

module

import Mathlib.Combinatorics.SimpleGraph.Basic
public import Mathlib.NumberTheory.LSeries.RiemannZeta

@[expose] public section

variable {V : Type*} {G : SimpleGraph V}

theorem foo (h₁ : G.foo) (h₂ : G.bar) : RiemannHypothesis := by
  exact h₁

[Snir Broshi]

I wonder if it's possible to even avoid the warning

[Aaron Liu]

that's weird, I would've expected "unknown identifier"

[Aaron Liu]

the hover information for G.foo and G.bar is also missing

[Aaron Liu]

maybe it's because G has been extracted to a variable?

[Snir Broshi]

I expect this error on the variable command:

Unknown identifier `SimpleGraph`

Note: A public declaration `SimpleGraph` exists but is imported privately;
consider adding `public import Mathlib.Combinatorics.SimpleGraph.Basic`.

[Aaron Liu]

but that's only because you're using the variable in a public theorem

[Snir Broshi]

AFAICT this is a bug with the variable command. I can use private declarations in it, then they get turned to sorry so the theorem can access any fake property of G

[Aaron Liu]

if theorem foo were instead private theorem foo then you should expect no error on the variable I think

[Snir Broshi]

Hmm, even with a private foo the variable command creates G : sorry

[Aaron Liu]

hmm, replacing it with private theorem foo doesn't make a difference

[Snir Broshi]

the public section seems to negate the private modifier, though it shouldn't

[Aaron Liu]

the sorrys in the goal state still have source information on them

[Snir Broshi]

Technically a proof of RH with no warnings:

module
import Mathlib.Combinatorics.SimpleGraph.Basic
public import Mathlib.NumberTheory.LSeries.RiemannZeta
public section
variable {V : Type*} {G : SimpleGraph V}
theorem foo (_ : G.RH = RiemannHypothesis) : G.RH := by
  exact ‹_›

[Aaron Liu]

oh it eats all the errors

module
import Mathlib.Combinatorics.SimpleGraph.Basic
public import Mathlib.NumberTheory.LSeries.RiemannZeta
public section
variable {V : Type*} {G : SimpleGraph V}
theorem foo (_ : G.RH = RiemannHypothesis) : G.RH := by
  exact ‹_›

/--
info: [Error pretty printing signature: incorrect number of universe levels foo]
foo
-/
#guard_msgs in
#check foo

[Snir Broshi]

I wonder what Comparator or lean4checker would make of this

[Snir Broshi]

Perhaps they'd complain that the conclusion of foo is of type sorry

[Aaron Liu]

I sneaked a SimpleGraph into the public scope even though it's only imported privated

module

import Mathlib.Combinatorics.SimpleGraph.Basic

-- public section

variable {V : Type*} {G : SimpleGraph V}

public def foo (h₁ : Nat) (h₂ : Nat) : Nat :=
  have := G
  h₁

/-- info: foo.{u_1} {V : Type u_1} {G : SimpleGraph V} (h₁ h₂ : ℕ) : ℕ -/
#guard_msgs in
#check foo

[Sebastian Ullrich]

Mmh, indeed it's a problem that variables are checked only once for errors (in the private scope) and then assumed to be well-formed in any subsequent declaration. I think the principled solution would be to add support for public variable, and deny use of private variables in public declarations.

[Snir Broshi]

This is lean4#10760

[Jovan Gerbscheid]

I discovered some examples where this actually goes wrong in mathlib, thanks to batteries#1688.

The variable command can contain a by-block that produces a proof that becomes a private auxiliary theorem. For example docs#CategoryTheory.Limits.FormalCoproduct.pullbackCone contains a private proof inside one of its parameters. When importing this into another module and inspecting the type, we get an unknown constant error.