when to use section over namespace ?

Stream: lean4

[TongKe Xue]

I am working through https://leanprover.github.io/theorem_proving_in_lean4/Dependent-Type-Theory/#dependent-type-theory

I find namespaces intuitive and helpful.

I am confused on the point of section, as in:

section useful
  variable (α β γ : Type)
  variable (g : β → γ) (f : α → β) (h : α → α)
  variable (x : α)

  def compose := g (f x)
  def doTwice := h (h x)
  def doThrice := h (h (h x))
end useful

Quoting the reference manual:

When the section is closed, the variables go out of scope, and cannot be referenced any more.

I am confused:

1. Why are sections useful if when they are closed, vars go out of scope, and cannot be referenced any more. (If we can't reference them, why declare them in first place?)

2. I like being able to reference things I declare. Why would I ever want to use section instead of namespace ?

I'm clearly misunderstanding something fundamental. Thanks!

[Mario Xerxes Castelán Castro 🇲🇽]

I have been learning Lean for a few days only. AFAIK: Sections are for when you want to limit the scope of variable declarations and similar. namespace is for when you want to create a namespace, i.e.: if you want compose to be accessible as userful.namespace.

[Aaron Liu]

in mathlib it's quite common to do something like

/--
The Foo of a monoid is the universal Bar that Baz.
-/
def Foo {α : Type*} [Monoid α] := ...

namespace Foo
variable {α : Type*}

section Monoid
variable [Monoid α]
-- lemmas and constructions that apply to monoids
end Monoid

section CommMonoid
variable [CommMonoid α]
-- lemmas and constructions that apply to commutative monoids
end CommMonoid

section CancelCommMonoid
variable [CommMonoid α] [IsCancelMul α]
-- lemmas and constructions that apply to commutative monoids with cancellative multiplication
end CancelCommMonoid

-- etc.
end Foo

[TongKe Xue]

Ah, thanks I think I understand my mistake now. When it says 'variable' it literally means 'variable.' lines, but not 'def.' lines, so

section useful
  variable (α β γ : Type) -- writes to 'section' lexical scope
   variable (g : β → γ) (f : α → β) (h : α → α) -- writes to 'section' lexical scope
  variable (x : α) -- writes to 'section' lexical scope

  def compose := g (f x) -- writes to module scope
  def doTwice := h (h x) -- writes to module scope
  def doThrice := h (h (h x)) -- writes to module scope
end useful

Is the correct mental model:

1. "section" provides "lexical scope for variable", but
2. "def" still writes to (module) global scope ?

(for some reason, I held the mistake view that section provided a single "lexical scope" that held "everything lexically defined in it")

[Kevin Buzzard]

yeah defs and theorems survive section ends.