namespaces inside sections

Stream: general

[Patrick Massot]

@Sebastian Ullrich I see that namespaces are not allowed inside sections in Lean 4. This is a very frustrating restriction and Gabriel got rid of it in Lean 3. Is there any reason to keep it in Lean 4?

[Johan Commelin]

@Patrick Massot I think you wanted to link to https://github.com/leanprover/lean4/blob/master/doc/namespaces.md
In the docs on sections, I didn't see any mention of this restriction.

[Gabriel Ebner]

The commit message was very pessimistic. AFAICR we didn't find a single horribly broken corner case.

[Kevin Buzzard]

Funnily enough I might have found one at Xena yesterday, regarding include. Let me see if I can reproduce.

[Kevin Buzzard]

This file https://github.com/ImperialCollegeLondon/M40002/blob/master/src/problem_sheet_two.lean breaks when you put the entire contents within a namespace. I'll minimise.

[Gabriel Ebner]

My first instinct was "ctrl+f parameter", and indeed it found something. I woudln't be surprised if that was the issue.

[Kevin Buzzard]

Yes it's parameters. Are they problematic within a namespace? I can't put these theorems in a namespace:

import data.real.basic

--namespace foo

section Q4

noncomputable theory

section two

parameters {a : ℝ} (ha : 0 < a) {n : ℕ} (hn : 0 < n)

include ha hn

def S := {s : ℝ | 0 ≤ s ∧ s ^ n < a}

def x := Sup S

theorem is_lub_x : is_lub S x :=
begin
  sorry,
end

lemma x_nonneg : 0 ≤ x :=
begin
  rcases is_lub_x with ⟨h, -⟩,
  sorry
end

end two

end Q4

--end foo

[Kevin Buzzard]

Mathlib-free. Is this a known issue? I was surprised. Uncomment the namespace and end lines and I get an error.

--namespace foo

section two

parameters {a : ℕ} (ha : 0 < a)

include ha

def x := 37

theorem is_lub_x : x = 37 :=
begin
  refl
end

lemma x_nonneg : 0 ≤ x :=
begin
  have h : x = 37 := is_lub_x,
  sorry
end

end two

--end foo

[Sebastian Ullrich]

Johan Commelin said:

Patrick Massot I think you wanted to link to https://github.com/leanprover/lean4/blob/master/doc/namespaces.md
In the docs on sections, I didn't see any mention of this restriction.

The sentence is gone; the restriction didn't actually exist :)