Borel hierarchy

Stream: maths

[Pedro Sánchez Terraf]

I'd like to present my first attempt at a contribution to mathlib. It is the definition of the Borel hierarchy plus some API around it. You can find it (with a bunch of nonsensical garbage in the repo history) here.

The linked theory may serve as a refactor of Gouëzel's formalization of the cardinality bound for $\sigma$-algebras src#measurable_space.cardinal_generate_measurable_le . I reproved the main theorems in this file using my definitions---from lines 450 onward statements and proofs follow that same file closely.

One of the main differences is that I have used unions, suprema, etc., indexed by ordinals (as it is customary in the literature) instead of using representatives. Accordingly, the notation $\omega_1$ is introduced for the ordinal (aleph 1).ord and not for (aleph 1).ord.out.α.

A brief implementation note: I defined the pair $\langle\Sigma^0_\alpha, \Pi^0_\alpha\rangle$ by recursion on $\alpha$, as suggested by Kevin here. I couldn't figure out how to use the more elegant inductive definitions suggested by Junyan Xu in the same thread.

I'd like to hear any comments to enhance the code, in order to prepare a PR. Thanks to all for your help in the past weeks, in particular @Felix Weilacher for some discussions about which were the possible directions the formalization of Descriptive Set Theory could go.

[Junyan Xu]

@Pedro Sánchez Terraf Here's how you might define the Sigma and Pi hierarchies inductively and simultaneously (where ff : bool corresponds to your S and tt corresponds to P):

import set_theory.cardinal.continuum

universe u

inductive sigma0_pi0_rec {α : Type u} (s : set (set α)) :
  ordinal.{u} → set α → bool → Prop
| basic (u ∈ s) : sigma0_pi0_rec 0 u tt
| empty : sigma0_pi0_rec 0 ∅ tt
| univ : sigma0_pi0_rec 0 set.univ tt
| compl {i u} : sigma0_pi0_rec i u ff → sigma0_pi0_rec i uᶜ tt
| union {i} (f : ℕ → set α) (g : ℕ → ordinal.{u}) :
    (∀ n, g n < i) → (∀ n, sigma0_pi0_rec (g n) (f n) tt) → sigma0_pi0_rec i (⋃ n, f n) ff

BTW, nonempty_compl_equiv can be proved using docs#equiv.set.image and docs#compl_injective.

[Eric Wieser]

docs#equiv.image combined with docs#equiv.compl is a better spelling that's computable (edit: that doesn't seem to work)

[Pedro Sánchez Terraf]

Junyan Xu said:

Pedro Sánchez Terraf Here's how you might define the Sigma and Pi hierarchies inductively and simultaneously (where ff : bool corresponds to your S and tt corresponds to P):

Thank you very much, I'll give it a try.

[Pedro Sánchez Terraf]

Junyan Xu said:

Pedro Sánchez Terraf Here's how you might define the Sigma and Pi hierarchies inductively and simultaneously
[...]
BTW, nonempty_compl_equiv can be proved using docs#equiv.set.image and docs#compl_injective.

I did the second thing and recovered all the main theorems using this alternative definition. The results are here. Nevertheless, working with this alternative definition was more difficult for me, and the new proofs are much longer, having to use extensionality where there was no need before. Most surely I'm missing some tricks, or guidelines to set up an API to make my life easier.

For instance, I could not recover my lemma sigma0_one (commented out in the file linked above). One particular problem I have is that working on this goal:

α : Type u,
s : set (set α),
z : set α,
h : z ∈ sigma0_pi0_rec 1 ff
⊢ ∃ (y : ℕ → ↥(s ∪ {∅, univ})), (⋃ (n : ℕ), ↑(y n)) = z

I can't usecases h. The culprit seems to be that the ordinal 1 does not appear in the inductive definition. The error reads:

cases tactic failed, unsupported equality between type and constructor indices
(only equalities between constructors and/or variables are supported, try cases on the indices):
quot.mk setoid.r {α := punit, r := empty_relation punit, wo := _} =
  quot.mk setoid.r {α := pempty, r := empty_relation pempty, wo := _}

I'm unable to understand the hint of “trying cases on the indices”. I also tried to use the internal lemmas that arise from the inductive definition, like pointclasses.sigma0_pi0_rec.cases_on, which I can correctly check for type but I can not invoke it using apply inside the proof.

[Reid Barton]

Ah because the 1 is an ordinal.
Probably you could use generalizing somehow to replace it by a variable, together with a hypothesis that it's equal to 1, and then use a lemma to eliminate some impossible cases.

[Pedro Sánchez Terraf]

Looks like another proof growing longer... I'll check it

[Pedro Sánchez Terraf]

But, @Reid Barton , generalizing is part of an induction tactic, isn't it? But here I have the inductive thing in my hyps, not in my target.

[Reid Barton]

Oh sorry, I meant generalize

[Pedro Sánchez Terraf]

Reid Barton said:

Oh sorry, I meant generalize

Again, it seems that this tactic only operates on the target. It was generalize_hyp :wink:

EDIT: ... that didn't work either since it forgets that the new variable has value 1. I think there was a tactic that did exactly what you are suggesting, but I'm not sure. I'll do it by hand.

EDIT 2:... It was rather circuitous in the end:

set o := (1 : ordinal) with ho,
replace h : sigma0_pi0_rec o ff z,
{ tauto },
clear_value o, -- needed!

Only then I could use cases . Surely there is a better way :cry:

[Junyan Xu]

induction h apparently works. Seems cases is trying to too many things at once.

[Pedro Sánchez Terraf]

Junyan Xu said:

induction h apparently works. Seems cases is trying to too many things at once.

I'm done, but I'll try that too. This is unexpected for me, since I thought that tactic was used only when have the inductive object on the target.

[Junyan Xu]

It's an inductive predicate (inductive family of propositions), so if you do induction on it it will enumerate all possible ways to construct a term of type, i.e. a proof of the proposition, with appropriate inductive hypothesis added to the context (which cases doesn't do).

[Reid Barton]

Does it add a hypothesis like 0 = 1 for the first three cases?

[Pedro Sánchez Terraf]

No.
Actually, the application of induction succeeds here, but finally I'm stuck again because without the info that the argument was 1 is lost. Therefore, one of the proof obligations requires me to prove certain closure under complements that is not true (it would if I was proving something general, but not in this case).

[Pedro Sánchez Terraf]

To make things clear: What I've been trying is induction h with ..., but now I see there is a different induction h : t which I didn't check before.

[Junyan Xu]

Yeah I was too optimistic when I said induction works. I can't seem to make it work nicely. ordinal isn't an inductive type so it's not good to do pattern matching on 0 : ordinal, but even if I replace the constructors by | empty (i = 0) : sigma0_pi0_rec i tt ∅, induction still doesn't keep the original 1 but generalizes 1 to an arbitrary ordinal, which is bad. So the inductive definition apparently doesn't work as nicely as expected, and makes me wonder whether we should just fall back to your original definition by well-founded recursion.

[Pedro Sánchez Terraf]

Yeah, I've seen some other awful behavior, like an awkward expansion of the definition of 0. Some of that can be seen in the last error message I pasted above, but even in the Infoview at line 131 of the file, hypothesis glt :puke:

[Reid Barton]

Maybe worth trying induction' as well?

[Pedro Sánchez Terraf]

Junyan Xu said:

So the inductive definition apparently doesn't work as nicely as expected, and makes me wonder whether we should just fall back to your original definition by well-founded recursion.

Haha none of the options work smoothly for me, but the original was apparently more amenable to the standard tactits (at least the ones I remember of the top of my head). Anyway, I did this at another branch, so the original is still alive and kicking.

[Pedro Sánchez Terraf]

Reid Barton said:

Maybe worth trying induction' as well?

Is that Lean4?

[Pedro Sánchez Terraf]

Or something from the last 3 months? Didn't update mathlib3 since then.

[Junyan Xu]

Maybe I can rescue the inductive approach by proving the desired induction principle separately and use that instead of the induction tactic ...

[Yaël Dillies]

tactic#induction'

[Pedro Sánchez Terraf]

Junyan Xu said:

Maybe I can rescue the inductive approach by proving the desired induction principle separately and use that instead of the induction tactic ...

I thought a bit about the shape of such an inductive principle, which is obvious in the case of docs#measurable_space.generate_measurable, but having the ordinal argument confused me.

[Reid Barton]

https://github.com/leanprover-community/mathlib/blob/master/src/tactic/induction.lean

[Reid Barton]

https://github.com/leanprover-community/mathlib/blob/master/src/tactic/induction.lean#L1331

- If the major premise (the hypothesis we are performing induction on) has
  complex indices, `induction'` 'remembers' them. A complex expression is any
  expression that is not merely a local hypothesis. A major premise
  `h : I p₁ ... pₙ j₁ ... jₘ`, where `I` is an inductive type with `n`
  parameters and `m` indices, has a complex index if any of the `jᵢ` are
  complex. In this situation, standard `induction` effectively forgets the exact
  values of the complex indices, which often leads to unprovable goals.
  `induction'` 'remembers' them by adding propositional equalities. As a
  result, you may find equalities named `induction_eq` in your goal, and the
  induction hypotheses may also quantify over additional equalities.

[Pedro Sánchez Terraf]

Reid Barton said:

https://github.com/leanprover-community/mathlib/blob/master/src/tactic/induction.lean

Yeah, I was not importing it. That's why didn't find it.

[Junyan Xu]

Oh I vaguely remembered that induction' exists and tried it but was missing the import. Now I added the import but it still fails:

Failed to apply the (dependent) recursor for pointclasses.sigma0_pi0_rec on h.
state:
α : Type u,
s : set (set α),
index : ordinal,
index_1 : bool,
index_2 : set α,
h : sigma0_pi0_rec index index_1 index_2
⊢ ∀ (z : set α),
    index = 1 →
    index_1 = ff → index_2 = z → (∃ (y : ℕ → ↥(s ∪ {∅, univ})), (⋃ (n : ℕ), ↑(y n)) = index_2)

[Pedro Sánchez Terraf]

Yaël Dillies said:

tactic#induction'

Btw, this points nowhere in my end. Missing docs? (though I see them in the sources)

[Junyan Xu]

Why isn't it mentioned in the tactic page ... that's why I wasn't sure it exists

[Pedro Sánchez Terraf]

Junyan Xu said:

Oh I vaguely remembered that induction' exists and tried it but was missing the import. Now I added the import but it still fails:

Same here, though I was not so sure because my h was z ∈ sigma0_pi0_rec 1 ff (equivalent to sigma0_pi0_rec 1 ff z isn't it???)

[Junyan Xu]

Yeah you have an abuse of defeq here: since sigma0_pi0_rec 1 ff is a predicate you should write sigma0_pi0_rec 1 ff z; if you want to use ∈ you should define

def sigma0 : set (set α) := {s | sigma0_pi0_rec i ff s}

instead. But that shouldn't affect the execution of the tactic. You can do a change and it still doesn't work.

[Yaël Dillies]

Junyan Xu said:

Why isn't it mentioned in the tactic page ... that's why I wasn't sure it exists

Hmm... that's unfortunate.

[Junyan Xu]

At least induction' doesn't error out if I replace parameters {α : Type u} (s : set (set α)) by variables ... Another reason to avoid parameters? I think it's already banned in mathlib.

[Pedro Sánchez Terraf]

Junyan Xu said:

At least induction' doesn't error out if I replace parameters {α : Type u} (s : set (set α)) by variables ... Another reason to avoid parameters? I think it's already banned in mathlib.

Oh I didn't know what was the etiquette about that... Once things were more or less settled, I was going to read the docs concerning PRs.

But I noticed that they worked a bit erratically... Sometimes you are asked to provide them explicitly in function calls.

[Junyan Xu]

Yeah induction' nails it. It's so intelligent that it knows 0 ≠ 1 in ordinals and generates exactly one goal:

lemma sigma0_one :
  sigma0 s 1 = set.range (λ (f : ℕ → s ∪ {∅,univ}), ⋃ n, (f n).1) :=
begin
  ext z,
  refine ⟨λ h, _, λ h, _⟩,
  { induction' h,
    simp_rw ordinal.lt_one_iff_zero at h_1,
    simp_rw h_1 at h,
    change ∀ n, f n ∈ pi0 s 0 at h,
    simp_rw pi0_zero at h,
    use λ n, ⟨f n, h n⟩ },
  sorry,

[Pedro Sánchez Terraf]

Right at the last line I'm left with this target (⋃ (n : ℕ), ↑⟨f n, _⟩) = ⋃ (n : ℕ), f n, which is discharged using exact rfl. Is that normal?

[Yaël Dillies]

Yes. docs#subtype.coe_mk holds definitionally.

[Pedro Sánchez Terraf]

Yaël Dillies said:

Yes. docs#subtype.coe_mk holds definitionally.

What I mean is that it seems that @Junyan Xu didn't have that goal. (His proof doesn't close the goal here).

[Yaël Dillies]

Ah sorry, misunderstood your question.

[Junyan Xu]

Maybe it's because I didn't use simp? So it's .val here but a coercion ↑ in your infoview.

[Junyan Xu]

If I do refine ⟨λ n, ⟨f n, h n⟩, _⟩ instead of use I get

(λ (f : ℕ → ↥(s ∪ {∅, univ})), ⋃ (n : ℕ), (f n).val) (λ (n : ℕ), ⟨f n, _⟩) = ⋃ (n : ℕ), f n

which use automatically closes. exact rfl can be replaced by refl BTW.

[Junyan Xu]

It's strange (and bad) that I can't seem to change the name h_1 auto-generated by induction' though ...

[Pedro Sánchez Terraf]

Junyan Xu said:

Maybe it's because I didn't use simp? So it's .val here but a coercion ↑ in your infoview.

I copypasted your code and it doesn't work as is, that's what I mean---but I think it works in your computer. That's the strange thing!
I already pushed it, you can check it here.

[Pedro Sánchez Terraf]

Junyan Xu said:

It's strange (and bad) that I can't seem to change the name h_1 auto-generated by induction' though ...

You can, the problem is that there are way too many variables: induction' h with _ _ _ _ _ _ _ IH g glt1,

[Junyan Xu]

Nice find! I stopped at h1 h2 h3 h4 h5 h6

[Pedro Sánchez Terraf]

So, what is the final vote on mathlib-appropriate material? Well-founded recursion or an inductive definition?

(I mean, the definitions of sigma0_pi0_rec---both versions of the file need not-so-fine tuning.)

[Junyan Xu]

Given that induction' works, I currently prefer inductive.
induction' still isn't perfect though, it doesn't automatically closes goals with 0 ≠ 0 assumption here:

lemma sigma0_pi0_compl {x : set α} (hi : i ≠ 0) :
  sigma0_pi0_rec s i ff x ↔ sigma0_pi0_rec s i tt xᶜ :=
⟨sigma0_pi0_rec.compl, λ h, begin
  induction' h with _ _ _ y,
  iterate 3 { exact (hi rfl).elim }, -- `induction'` doesn't know `0 ≠ 0` is false ...
  rwa ← compl_inj_iff.1 induction_eq_2,
end