ext issues

Stream: mathlib4

[Kevin Buzzard]

There are some (easily worked-around) issues with ext in !4#3208 (port CategoryTheory.Limits.Presheaf) and I thought I'd try and understand them rather than just pushing the PR through (which now compiles). Here's the first one:

-- lean 3
import category_theory.types

def foo (A B : Type) (f g : A ⟶ B) : f = g := begin
  ext x, -- works
  sorry -- `⊢ f x = g x`
end

#print foo -- it's `funext`

In Lean 4 this currently fails:

-- lean 4
import Mathlib.CategoryTheory.Types

example (A B : Type) (f g : A ⟶ B) : f = g := by
  --ext x -- fails
  funext x -- works

I don't really understand why it works in Lean 3 but not Lean 4. There seem to be no ext lemmas in category_theory.types. Does Lean 3 see through more stuff than Lean 4 somehow? My instinct was to make an ext lemma for concrete_category but actually this is not imported in the example. Should I just make an ext lemma for Type u and dump it in the imported file?

[Kyle Miller]

Do you know if you can import Mathlib.CategoryTheory.ConcreteCategory.Basic into that file? It looks like there's a relevant ext lemma.

[Kyle Miller]

Though perhaps it should have a specialized one for Type still, because this isn't great:

[Kyle Miller]

-- lean 4
import Mathlib.CategoryTheory.Types
import Mathlib.CategoryTheory.ConcreteCategory.Basic

example (A B : Type) (f g : A ⟶ B) : f = g := by
  ext x -- works
  -- ⊢ (CategoryTheory.forget Type).map f x = (CategoryTheory.forget Type).map g x

[Adam Topaz]

There was a thread a while ago explaining the issue

[Adam Topaz]

I’ll try to dig it up when I get home

[Kyle Miller]

Something like this:

-- lean 4
import Mathlib.CategoryTheory.Types
import Mathlib.CategoryTheory.ConcreteCategory.Basic

@[ext 950]
theorem CategoryTheory.ConcreteCategory.type_hom_ext {X Y : Type v} (f g : X ⟶ Y)
  (h : ∀ (x : X), f x = g x) : f = g := funext h

example (A B : Type) (f g : A ⟶ B) : f = g := by
  ext x -- works
  -- ⊢ f x = g x

[Kyle Miller]

Adam Topaz said:

There was a thread a while ago explaining the issue

I think it might be this one: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/ext.20debugging/near/348821912

[Adam Topaz]

No there was one even before that (I think I initiated it)

[Kevin Buzzard]

The second issue is that Lean 3 ext seems to unfold definitions if necessary, but Lean 4 doesn't. Here's an example:

-- lean 3
import tactic

constant X : Type

@[ext] lemma X.ext (a b : X) : a = b := sorry

example (a b : X) : a = b :=
begin
  ext, --works fine
end

noncomputable def Y : Type := X

example (a b : Y) : a = b :=
begin
  ext, -- also works fine!
end

The analogous code in Lean 4 doesn't work:

-- lean 4
import Mathlib.Tactic

opaque X : Type

@[ext] lemma X.ext (a b : X) : a = b := sorry

example (a b : X) : a = b := by
  ext --works fine

noncomputable def Y : Type := X

example (a b : Y) : a = b := by
  ext -- no applicable extensionality lemma found for `Y`

[Kyle Miller]

In that thread I linked to, Gabriel mentioned that the Lean 3 ext tactic would try applying all ext lemmas as a last resort, which might be why the Lean 3 examples work here.

[Kevin Buzzard]

This is kind of a big call. We have

theorem extendAlongYoneda_obj (P : Cᵒᵖ ⥤ Type u₁) :
    (extendAlongYoneda A).obj P = colimit ((CategoryOfElements.π P).leftOp ⋙ A) :=
  rfl

and we have an ext lemma for colimits, so I could obviously make the corresponding ext lemma for (extendAlongYoneda A).obj P but it might be better to have Lean 4 ext doing the same thing as Lean 3.

[Kevin Buzzard]

Kyle Miller said:

In that thread I linked to, Gabriel mentioned that the Lean 3 ext tactic would try applying all ext lemmas as a last resort, which might be why the Lean 3 examples work here.

Is there a reason that we don't want to do this in Lean 4? I mean, if we change the behaviour of the tactic then things are going to break, and are breaking.

[Kevin Buzzard]

In fact this explains a lot!

[Kyle Miller]

The old behavior seems really unpredictable to me. It depends on whatever random order the ext lemmas are defined in and what happens to unfold to what. There are probably things that are broken that are things that shouldn't have ever worked (though still some that arguably should).

There should be some way to tell ext that it should unfold definitions while searching for ext lemmas... In any case, this breakage/change in behavior is making us fix "bad exts".

[Kevin Buzzard]

Oh dear, the linked thread seems to indicate that making ext try all the ext lemmas as a last resort is not an option any more. So should I just add the "missing" ext lemmas?

[Kyle Miller]

That to me seems like the right thing to do

[Kyle Miller]

Maybe we could create an attribute to inherit ext lemmas from another definition, like maybe

@[exts] noncomputable def Y : Type := X

[Kyle Miller]

Anyway, I'm not sure what to call it, but this should definitely accompany hom_ext:

@[ext 950]
theorem CategoryTheory.ConcreteCategory.type_hom_ext {X Y : Type v} (f g : X ⟶ Y)
  (h : ∀ (x : X), f x = g x) : f = g := funext h

I don't know what ext priority it should be either. I just chose that number to be above the priority for hom_ext.

[Adam Topaz]

Another option is to add funext to aesop_cat’s rule set (maybe scoped to concrete categories)

[Adam Topaz]

Actually I think the right solution is to make Homs in the category of types (and also in all the categories arising from bundled, like GroupCat etc.) into a structure with a single field, similar to docs#category_theory.Sheaf.hom

[Kevin Buzzard]

!4#3593 adds the ext lemma for Type u. This is part of what we need to unblock !4#3208 .