!4#3664 Topology.Algebra.UniformConvergence

Stream: mathlib4

[Jeremy Tan]

!4#3664 I need help with the five remaining errors in this file; it's on the same critical path as Analysis.Seminorm

[Scott Morrison]

I've fixed a few errors here, but have observed something weird I don't understand. There's a point where an OfNat.ofNat leaks into the goal, where I would have expected to just see 0.

I extracted the problem out into a lemma:

-- FIXME this declaration is just isolating a problem that occurs below, for diagnosis.
lemma foo (φ : hom) (V : Set E) (m : 0 ∈ V):
    @FunLike.coe hom H (fun _ ↦ α →ᵤ[𝔖] E) SMulHomClass.toFunLike φ 0 x ∈ V := by
  rw [map_zero]
  -- `OfNat.ofNat` has leaked into the goal: `⊢ OfNat.ofNat 0 x ∈ V`
  exact m

which you can find in this branch !4#3664.

If anyone has a suggestion for a general diagnosis for leaking OfNat.ofNat's, please let us know!

[Scott Morrison]

(This is not blocking the PR, but still I would like to fix / understand.)

[Scott Morrison]

Actually, the remaining two errors in this PR are caused by the same issue. We could work around them but I'd prefer to just avoid the OfNat.ofNats here.

[Scott Morrison]

@Mario Carneiro, do you recognise this one?

[Jeremy Tan]

Note that in the line convert UniformFun.hasBasis_nhds_of_basis α _ (1 : α →ᵤ G) this the type-ascripted 1 was originally just that, without ascription (in the mathport output)

[Jeremy Tan]

And similarly for the other such convert

[Mario Carneiro]

@Scott Morrison Usually when you see a OfNat.ofNat 0 that means it's a double ofNat expression (i.e. the 0 is not a raw numeral, which you can tell by hovering on it in the infoview - raw numerals just show 0 again in the infoview but normal numerals reveal an ofNat)

[Mario Carneiro]

needless to say, that's not supposed to happen

[Scott Morrison]

That's not the case here. The pop-up-infoview just shows 0 (or 1 in the other examples).

[Mario Carneiro]

in that case it might be a non-canonical term? Ah! the x there is an over-application

[Mario Carneiro]

core lean doesn't handle over-applications well, Std has a delaborator combinator to handle that

[Mario Carneiro]

(over-application means that the constructor is applied to more arguments than it is declared to have, which is generally a type error but can be valid if it's a generic function instantiated at a function type)

[Mario Carneiro]

lean's delaborators usually bail out upon seeing this, but they should instead match the arguments they are expecting and add some parentheses for the rest

[Mario Carneiro]

in which case it would be printed as 0 x ∈ V

[Scott Morrison]

Hmm... but here it's not just a pretty-printing issue: a simp lemma is failing to fire.

[Mario Carneiro]

what lemma?

[Mario Carneiro]

the MWE only shows the pretty printing issue

[Scott Morrison]

Yeah, you're right. Maybe it is a missing simp lemma, that 0 x = 0.

[Scott Morrison]

(But I'm a bit confused what has changed, if such a lemma wasn't already needed in mathlib3.)

[Scott Morrison]

So back in mathlib3 simp is successfully deploying pi.zero_apply. Trying to generate a clear example showing the difference.

[Scott Morrison]

Okay, so indeed:

--- mathlib3:
example (x : α) : (0 : α →ᵤ[𝔖] E) x = 0 := by simp?   -- succeeds, using `simp only [pi.zero_apply, eq_self_iff_true]`

--- mathlib4:
example (x : α) : (0 : α →ᵤ[𝔖] E) x = 0 := by simp    -- does nothing,
-- displays goal as `OfNat.ofNat 0 x = 0`

[Scott Morrison]

So perhaps the OfNat.ofNat is just a red herring, and Lean 4 will just need a more specific simp lemma here.

[Scott Morrison]

Adding

@[to_additive (attr := simp)]
lemma UniformFun.one_apply [Monoid β] : (1 : α →ᵤ β) x = 1 := Pi.one_apply x

@[to_additive (attr := simp)]
lemma UniformOnFun.one_apply [Monoid β] : (1 : α →ᵤ[𝔖] β) x = 1 := Pi.one_apply x

has resolved the issues, but I worry that later we will need more of them.

I guess this is just overusing type synonyms biting us.

[Scott Morrison]

Okay, I've marked this PR as awaiting review now.

[Yaël Dillies]

@Scott Morrison, if I'm understanding this correctly, those are not the right lemmas to have as simp. Instead you should have

@[to_additive (attr := [simp, norm_cast])]
lemma UniformFun.coe_one [Monoid β] : (1 : α →ᵤ β) = 1 := rfl

@[to_additive (attr := [simp, norm_cast])]
lemma UniformOnFun.coe_one [Monoid β] : (1 : α →ᵤ[𝔖] β) = 1 := rfl

[Yaël Dillies]

You can (and should) still have the apply lemmas, but you don't need to tag them as simp (and might get shouted at by the simp-nf linter if you do so).

[Scott Morrison]

Would you be able to try those in the PR?

[Yaël Dillies]

Let's try

[Yaël Dillies]

Ohohoh, that's bad. We're missing the fun_like instance.

[Yaël Dillies]

I would declare this file as not ready to port and fix all that back in mathlib.

[Yaël Dillies]

If you're happy with that, I'll go and fix the design.

[Jeremy Tan]

Yaël Dillies said:

If you're happy with that, I'll go and fix the design.

Have a mathlib3 PR ready when you can

[Scott Morrison]

@Jeremy Tan, I don't think it is helpful for you to answer for me here!

[Scott Morrison]

@Yaël Dillies, presumably you want to put FunLike in Topology.Algebra.UniformConvergenceTopology, right? That file has already been ported, so we'll have to do some back and forth to synchronize everything here.

[Yaël Dillies]

Yeah, unfortunately

[Scott Morrison]

Perhaps you could verify that you can install the fun_like in the right place in mathlib3, and then directly port the change as part of the current PR !4#3644?

[Scott Morrison]

That would save an extra round of waiting for PRs, at the cost of having to get the port right manually. :-)

[Yaël Dillies]

We can still let my mathlib PR run through mathport, right? Then nothing needs to be manual and we can still do everything in one mathlib4 PR.

[Scott Morrison]

Alternatively we could merge the current PR in the state it's in now, and then once you've installed fun_like successfully the forward port could remove my lemmas?

[Scott Morrison]

We could --- I'm just interested in speeding things up if possible as other significant files are downstream of this one, I think.

[Anatole Dedecker]

Sorry for the mess around these type aliases. If I'm honest it was already painful in mathlib3 so it's not surprising that these are annoying to port. If you have ideas on how to make these cleaner it would be great !

[Eric Wieser]

My experience with some affine PRs is that a lot of downstream hacks quickly pile up if a funlike instance is missing

[Eric Wieser]

So it really probably is best to make the mathlib PR first rather than proceed with the fun_like-less version

[Yaël Dillies]

I just found Anatole's note:

-- Note: we don't declare a `has_coe_to_fun` instance because Lean wouldn't insert it when writing
-- `f x` (because of definitional equality with `α → β`).

[Yaël Dillies]

and indeed

instance uniform_fun.fun_like {α β} : fun_like (α →ᵤ β) α (λ _, β) :=
{ coe := id,
  coe_injective' := function.injective_id }

example {α β} (f : α →ᵤ β) (a : α) : f a = f a :=
begin
  -- ⊢ f a = f a
end

[Yaël Dillies]

So either we make uniform_fun irreducible, or we make it a structure.

[Yaël Dillies]

... or we give up on fun_like

[Yaël Dillies]

Given the information I know have, I think it is acceptable to go forward with Scott's simp lemmas and no fun_like for now. The situation is analogous to set, which is semireducible too. And indeed there were set lemmas misfiring on predicates in Lean 3.