!4#4075 Topology.ContinuousFunction.Bounded

Stream: PR reviews

[Damiano Testa]

I saw that PR !4#4075 was marked as help-wanted and simply went in and pushed fixes: I hope that this is the standard practice!

There were three instances that were not picked up, so I simply went ahead and explicitly told Lean what their names were. I do not know why this was not picked up automatically. Here is one of them, in case you are curious:

instance ring : Ring (α →ᵇ R) :=
  FunLike.coe_injective.ring _ coe_zero coe_one coe_add coe_mul coe_neg coe_sub
    (fun _ _ => coe_nsmul _ _) (fun _ _ => coe_zsmul _ _) (fun _ _ => coe_pow _ _) coe_natCast
    coe_intCast

instance : SeminormedRing (α →ᵇ R) :=
  { (show Ring (α →ᵇ R) from ring),  -- porting note: this was not present in the original
    BoundedContinuousFunction.nonUnitalSeminormedRing with }

Without show ... from ..., Lean says fields missing: 'one_mul', 'mul_one'. The other two are similar and similarly annotated in the file.

[Kevin Buzzard]

The kind of question I ask in these situations is "why did it work in Lean 3 and not now"? I don't really like to proceed until I've got to the bottom of things, because I figure that if I don't follow up now then the next time the problem occurs it might be harder to debug than the first time.

[Damiano Testa]

Ok, I am happy to try, but I do not know where to start...

[Kevin Buzzard]

Well I'd start by trying to figure out how the fieldsone_mul and mul_one were being filled in mathlib3.

[Kevin Buzzard]

Presumably from ring? Is there no mention of ring or apply_instance or something, which summoned it, in the Lean 3 code?

[Kevin Buzzard]

Just randomly fixing things runs the risk of causing more problems down the line. I think that different people have different attitudes to this sort of thing. I feel like I want to have a good understanding of every deviation from the auto-generated output, rather than just fixing it, because I feel like it gives me a better understanding of Lean 4.

[Damiano Testa]

I'll look into it. For the moment, this is what the Lean 3 code was:

instance : ring (α →ᵇ R) :=
fun_like.coe_injective.ring _ coe_zero coe_one coe_add coe_mul coe_neg coe_sub
  (λ _ _, coe_nsmul _ _)
  (λ _ _, coe_zsmul _ _)
  (λ _ _, coe_pow _ _)
  coe_nat_cast
  coe_int_cast

instance : semi_normed_ring (α →ᵇ R) :=
{ ..bounded_continuous_function.non_unital_semi_normed_ring }

[Kevin Buzzard]

Yeah that's a pretty wild Lean 3 proof, because it's hard to imagine that an instance called bounded_continuous_function.non_unital_semi_normed_ring was carrying around any information about one, and clearly we need information about one to make the proof compile. Do you understand how the mathlib3 proof worked? (I don't)

[Damiano Testa]

Earlier in the file there is a has_one instance, explicitly.

[Damiano Testa]

@[to_additive]
instance : One (α →ᵇ β) :=
  ⟨const α 1⟩

and a similar one in Lean 3. Anyway, thanks for the suggestions! I'll see if I find something.

[Kevin Buzzard]

Right, but how would that last proof know about one_mul and mul_one?

[Damiano Testa]

I assumed that Lean 3 picked up that the type was a ring, so it had a 1 and the mul_one, one_mul stuff... no?

[Damiano Testa]

I am probably being very naïve...

[Kevin Buzzard]

What is going to pick that up? You have only told it to look at bounded_continuous_function.non_unital_semi_normed_ring which I am assuming doesn't mention one. Does typeclass inference just randomly run? I mean, it can't do -- if it did, you wouldn't need to put ..bounded_continuous_function.non_unital_semi_normed_ring. I'm just confused about something basic here.

[Damiano Testa]

Ok, I do not know. The non_unital stuff, does not have one, I checked!

[Damiano Testa]

There is something else which is funny: if instead of Ring i give it a Monoid structure:

show Monoid (α →ᵇ R) from MonoidWithZero.toMonoid

give the error:

type mismatch
  HEq.rfl
has type
  HEq ?m.1468859 ?m.1468859 : Prop
but is expected to have type
  NatCast.natCast 0 = 0 : Prop

[Damiano Testa]

(The monoid instance I found using #synth.)

[Kevin Buzzard]

Yeah, handling of numerals has changed completely in Lean 4 and this is something else I don't understand at all.

[Damiano Testa]

Ok, so I'll simply undo my "fixes" and let someone else look at this! Thanks!

[Ruben Van de Velde]

I don't think you should undo your work, porting notes should be sufficient (unless the reviewers disagree)

[Damiano Testa]

Alongside the porting notes in the file, mentioning that I added the extra instances, I also left a comment on the PR and a link to this Zulip discussion.

Anyway, it was certainly not my intention to cause more work for everyone involved, so I am happy to follow any decision on the issue!

[Kevin Buzzard]

Some ports are smooth: all the errors are just because you have to change functor.map to Functor.map or whatever. Others are a bit less smooth but still very much "under control" -- some simp proof fails and you convince yourself that this is because our simp lemmas are not confluent so it matters what order they're applied in, and lean 4 is applying them in a different order to Lean 3. Some errors are "mathlib3 needed apply_instance here but the goal is already solved in mathlib4". This is somehow the next easiest level of file -- it's clear what's going on so you just fix it. But if typeclasses are messing you around or simp lemmas aren't firing or universes aren't being unified then this is the hard part of porting, because you have to both fix the problem and understand why it is there so that other people either won't find themselves in the same situation later, or they will but we know what to do about it.