Unified interface for subobjects

Stream: general

[Anne Baanen]

Indeed, I think you point to the right issue: there's no functionality in Lean that allows you to be parametric in declarations in the correct way that ML-ish functors would allow you to be. Typeclasses come close, but you can't write down which implicits are allowed to differ: you can't do to_additive with them because there's no way to say "let X be either an add_comm_monoid or a comm_monoid and Y the same (but not X additive and Y multiplicative)". Or we'd have to completely unbundle the data from the proofs, but then you lose the head symbols as a result.

[Anne Baanen]

So I think the best way with the current architecture of Lean is duplicating the mem_carrier, ext, copy parts of set_like, either manually or programmatically. But that's just a constant amount of work per subobject, and what I'm interested in is that we have a multiplicative amount of duplication of lemmas of the form subfoo.bar_mem: (number of subobject types extending subfoo) × (number of operations closed under subfoo): currently we (incompletely and ad-hoc) copy over each of these per subobject type extending subfoo. And for that issue typeclasses can be useful.

[Anne Baanen]

More specifically, for each

structure subfoo (α : Type*) [foo α] :=
(carrier : set α)
(op_mem' : ∀ {x}, x ∈ carrier → foo.op x ∈ carrier)

we create a

class subfoo_class (S : Type*) (α : out_param Type*) [foo α]
  extends set_like S α :=
(op_mem : ∀ {s : S} {x}, x ∈ s → foo.op x ∈ s

and then every subobject coercible to a subfoo can get an instance of subfoo_class.

[Anne Baanen]

Since the class is parametrized only by types and other instances, we don't have any issues with equalities requiring transport of instances. We keep the head symbols ∈ and (coe : subfoo α → set α) from the bundled subobjects so no issues with rw/simp. And no more duplication of _mem lemmas: for each operation op₂ that subfoos are closed under, we can define op₂_mem as follows:

lemma op₂_mem {S α : Type*} [foo α] [subfoo_class S α] {s : S}
  {x y : α} (hx : x ∈ s) (hy : y ∈ s) : op₂ x y ∈ s :=
sorry

And for each structure subbar α extends subfoo α with a corresponding subfoo_class (subbar α) α instance gets immediate access to op₂_mem, no need for hacks like subbar.to_subfoo.op₂_mem.

[Anne Baanen]

(Shall we move this discussion to a separate thread in #general?)

[Eric Wieser]

In my PR I was trying to generalize over op2 as well, but perhaps that was greedy

[Notification Bot]

This topic was moved here from #new members > Show specific set forms a subspace iff some condition holds by Anne Baanen

[Anne Baanen]

Eric Wieser said:

In my PR I was trying to generalize over op2 as well, but perhaps that was greedy

I was going to check out your PR last night but grocery shopping intervened. Thanks for the reminder!

[Anne Baanen]

Also I want to point out everything said in this thread goes, mutatis mutandis, for homomorphisms: we have a coe_fn : foo_hom A B → (A → B) taking the place of coe : subfoo A → set A, map_op taking the place of op_mem, etc.

[Anne Baanen]

Eric Wieser said:

In my PR I was trying to generalize over op2 as well, but perhaps that was greedy

Indeed, looking at the defeq trace, the issue is really that the inference for the has_zero β instance will only be attempted after the defeq check for the instance to be applied, measurable.subtype.closed_under_zero. So it can't figure out semiring.zero =?= @has_zero.zero β ?. Maybe that's changed in Lean 4 now that the elaborator can postpone goals, but here the only way I can find to force the has_zero β instance to be there already is through including it in one of the types.

[Anne Baanen]

(Or you can make it an out_param I guess, but that brings with it a whole other host of issues!)

[Anne Baanen]

After exactly 100 commits, the subobject refactor builds! :tada: I created PR #11545 while I waited for the linter results to come in.

[Reid Barton]

Remember when GitHub would create a squashed commit with 100 lines of * fix things?

[Anne Baanen]

I'm having trouble with a timeout in the fails_quickly linter for docs#measure_theory.Lp_meas.complete_space. The weird thing is that I get the same timeout on master, even though the linter seems happy enough there:

import measure_theory.function.conditional_expectation

namespace measure_theory

def foo₂ (α F 𝕜 : Type*) (p : ennreal)
  [_inst_1 : is_R_or_C 𝕜]
  [_inst_13 : normed_group F]
  [_inst_14 : normed_space 𝕜 F]
  [_inst_15 : measurable_space F]
  [_inst_16 : borel_space F]
  [_inst_17 : topological_space.second_countable_topology F]
  [_inst_37 : opens_measurable_space 𝕜]
  (m m0 : measurable_space α)
  (μ : measure_theory.measure α)
  [hm : fact (m ≤ m0)]
  [hp : fact (1 ≤ p)] :
  complete_space ↥(measure_theory.Lp_meas F 𝕜 m p μ) :=
by apply_instance

end measure_theory

[Anne Baanen]

@Rémy Degenne , it looks like you defined this instance, would you have any tips for how to resolve the issue?

[Anne Baanen]

Actually hang on, if I replace Type* with universe variables, the linter passes on both master and my branch?

import all

open tactic

run_cmd get_decl `measure_theory.Lp_meas.complete_space >>= fails_quickly 15000 >>= tactic.trace -- none

universes u v w

namespace measure_theory

def foo₂ (α : Type u) (F : Type v) (𝕜 : Type w) (p : ennreal)
  [_inst_1 : is_R_or_C 𝕜]
  [_inst_13 : normed_group F]
  [_inst_14 : normed_space 𝕜 F]
  [_inst_15 : measurable_space F]
  [_inst_16 : borel_space F]
  [_inst_17 : topological_space.second_countable_topology F]
  [_inst_37 : opens_measurable_space 𝕜]
  (m m0 : measurable_space α)
  (μ : measure_theory.measure α)
  [hm : fact (m ≤ m0)]
  [hp : fact (1 ≤ p)] :
  complete_space ↥(measure_theory.Lp_meas F 𝕜 m p μ) :=
by apply_instance -- works

end measure_theory

[Rémy Degenne]

I saw that a linter complained at some point, but did not manage to fix it, and it did not prevent me from making PRs in that file or anything else, so I did not try much. Glad you found a solution!
Now I am curious to know why that fix changes anything :) .

[Anne Baanen]

Sorry, let me be clearer: in both my branch and on master, manually invoking the fails_quickly linter does not fail (even when I do import all), while the manual examples time out iff the universes are implicit (in the form of Type*). The full lint script fails only on my branch.

[Anne Baanen]

Ok, from a bit of binary search looks like the max_steps goes from about 10 000 on master to 13 000 on my branch. If the linters don't completely empty their caches or something like that, then I can believe this barely pushes the search over the limit of 15 000 in the actual linting run. I'll try bumping the limit to 20 000, since the actual time it takes to fail is not so different: ~2.6s for master vs ~2.9s on my branch.

[Anne Baanen]

Split off the first part of the refactor into #11750 which only introduces the new definitions (and does a bit of fixing)

[Anne Baanen]

Second part of the refactor, moving the generic _mem lemmas to the root namespace, is now PR #11758.

[Anne Baanen]

Third part, deleting all the duplicate subgroup.to_group (etc.) instances in favour of subgroup_class.to_group: #11759