ext

Stream: mathlib4

[Xavier Roblot]

In mathlib4#1353, we need to prove at some point that two FreeMagma.hom are equal (line 119). With lean3, it was done using ext, rfl. It fails in lean4. The reason appears to be that, with lean4, ext is not using the ext lemma defined just a few lines above (line 78)

@[ext, to_additive]
theorem hom_ext {β : Type v} [Mul β] {f g : FreeMagma α →ₙ* β} (h : f ∘ of = g ∘ of) : f = g :=

Indeed, replacing ext in the proof by an explicit call to FreeMagma.hom_ext enables rfl to close the goal.

Something similar is happening on line 479 where it is necessary to replace ext by FreeSemigroup.ext to finish the proof.

Is this normal? Is the use of generic ext deprecated and one needs to call instead the specific ext lemma?

[Xavier Roblot]

There are more failing rfl in this PR and all are following an ext or an ext1: see lines 746, 773 and 776

[Chris Hughes]

I remember ext in Lean3 depended chose the ext lemma based on the order they were declared in so they had to be declared in the right order. This is a bad design and probably the cause of the breakages in Lean4

[Eric Wieser]

I don't agree that it was bad design; in practice the right order was the one that always occurred naturally

[Eric Wieser]

Does it work here if you disable the default ext lemma that it is finding?

[Xavier Roblot]

How do I that?

[Eric Wieser]

Something like attribute [-ext] MulHom.ext

[Xavier Roblot]

lean doesn't like that: attribute cannot be erased

[Eric Wieser]

Then you might need to make a mwe by copying out the two ext lemmas and basic theory into a new file

[Eric Wieser]

Or we should teach lean how to erase it

[Xavier Roblot]

Here is a mwe (well, maybe more a we)

import Mathlib.Algebra.Hom.Equiv.Basic

universe u v l

inductive FreeMagma (α : Type u) : Type u
  | of : α → FreeMagma α
  | mul : FreeMagma α → FreeMagma α → FreeMagma α
  deriving DecidableEq

namespace FreeMagma

variable {α : Type u}  {β : Type v} [Mul β] (f : α → β)

instance : Mul (FreeMagma α) := ⟨FreeMagma.mul⟩

theorem mul_eq (x y : FreeMagma α) : mul x y = x * y := rfl

@[elab_as_elim]
noncomputable def recOnMul {C : FreeMagma α → Sort l} (x) (ih1 : ∀ x, C (of x))
    (ih2 : ∀ x y, C x → C y → C (x * y)) : C x :=
  FreeMagma.recOn x ih1 ih2

@[ext]
theorem hom_ext {β : Type v} [Mul β] {f g : FreeMagma α →ₙ* β} (h : f ∘ of = g ∘ of) : f = g :=
  (FunLike.ext _ _) fun x ↦
    recOnMul x (congr_fun h) <| by
      intros
      simp only [map_mul, *]

def liftAux {α : Type u} {β : Type v} [Mul β] (f : α → β) : FreeMagma α → β
  | FreeMagma.of x => f x
  | x * y => liftAux f x * liftAux f y

def lift : (α → β) ≃ (FreeMagma α →ₙ* β) where
  toFun f :=
    { toFun := liftAux f
      map_mul' := fun x y ↦ rfl }
  invFun F := F ∘ of
  left_inv f := by rfl
  right_inv F := by
    ext -- fails
    -- refine hom_ext ?_ -- works
    rfl

end FreeMagma

[Eric Wieser]

Does it give any useful message?

[Xavier Roblot]

I am not sure it is useful but here is the error message

type mismatch
  HEq.rfl
has type
  HEq ?m.4713 ?m.4713 : Prop
but is expected to have type
  ↑((fun f => { toFun := liftAux f, map_mul' := (_ : ∀ (x y : FreeMagma α), liftAux f (x * y) = liftAux f (x * y)) })
          ((fun F => ↑F ∘ of) F))
      x✝ =
    ↑F x✝ : Prop

[Xavier Roblot]

So I guess it is using FunLike.ext instead of hom_ext

[Eric Wieser]

Is the error on the ext or the rfl?

[Eric Wieser]

Here is a mwe (well, maybe more a we)

You need to put your own version of MulHom in that MWE too, that doesn't implement FunLike

[Eric Wieser]

(What I'm trying to work out here is whether hom_ext is even a valid ext lemma in Lean4)

[Xavier Roblot]

Eric Wieser said:

Is the error on the ext or the rfl?

The rfl fails to close the goal (see the error message above). The ext does not cause any error.

[Eric Wieser]

Oh, I assumed ext did cause an error because you wrote ext -- fails!

[Xavier Roblot]

Sorry, I was not clear. The proof does not complete with ext but completes when you replace it with refine hom_ext ?_

[Eric Wieser]

Here's a better mwe:

import Mathlib.Algebra.Group.Basic
import Mathlib.Logic.Equiv.Basic

universe u v l

structure MulHom (M N : Type _) [Mul M] [Mul N] where
  toFun : M → N
  map_mul : ∀ a b, toFun (a * b) = toFun a * toFun b

-- fails if you uncomment this line
-- @[ext]
lemma MulHom.ext {M N : Type _} [Mul M] [Mul N] {f g : MulHom M N} (h : ∀ x, f.toFun x = g.toFun x) : f = g :=
  sorry

inductive FreeMagma (α : Type u) : Type u
  | of : α → FreeMagma α
  | mul : FreeMagma α → FreeMagma α → FreeMagma α
  deriving DecidableEq

namespace FreeMagma

variable {α : Type u}  {β : Type v} [Mul β] (f : α → β)

instance : Mul (FreeMagma α) := ⟨FreeMagma.mul⟩

theorem mul_eq (x y : FreeMagma α) : mul x y = x * y := rfl

@[elab_as_elim]
noncomputable def recOnMul {C : FreeMagma α → Sort l} (x) (ih1 : ∀ x, C (of x))
    (ih2 : ∀ x y, C x → C y → C (x * y)) : C x :=
  FreeMagma.recOn x ih1 ih2

@[ext]
theorem hom_ext {β : Type v} [Mul β] {f g : MulHom (FreeMagma α) β} (h : f.toFun ∘ of = g.toFun ∘ of) : f = g :=
  sorry

def liftAux {α : Type u} {β : Type v} [Mul β] (f : α → β) : FreeMagma α → β
  | FreeMagma.of x => f x
  | x * y => liftAux f x * liftAux f y

def lift : (α → β) ≃ (MulHom (FreeMagma α) β) where
  toFun f :=
    { toFun := liftAux f
      map_mul := fun x y ↦ rfl }
  invFun F := F.toFun ∘ of
  left_inv f := by rfl
  right_inv F := by
    ext -- works?
    rfl

end FreeMagma

[Eric Wieser]

(deleted)

[Eric Wieser]

So this does seem to be a priority problem of some kind

[Gabriel Ebner]

Same story as with simp lemmas I think. The order of the lemmas in the files no longer reliably influences the order they're tried in. I think we should add a priority argument to the ext attribute.

[Eric Wieser]

It looks to me like ext doesn't understand priority at all?

[Junyan Xu]

Can you do show_term { ext } or ext? in Lean 4?
I'd expect some goals previously closed by by { ext, refl } might be closed by rfl alone due to eta defeq.

[Mario Carneiro]

yes (it's show_term ext)

[Xavier Roblot]

Junyan Xu said:

I'd expect some goals previously closed by by { ext, refl } might be closed by rfl alone due to eta defeq.

This is not the case in mathlib#1353 (unfortunately).

[Xavier Roblot]

Same story as with simp lemmas I think. The order of the lemmas in the files no longer reliably influences the order they're tried in. I think we should add a priority argument to the ext attribute.

In the meantime, what should I do about mathlib#1353? Should I just replace every ext by the explicit ext lemma that should be used?

Or just wait for ext to be fixed...

[Yaël Dillies]

Replacing ext by the ext lemmas and leaving porting notes where that happened is fine, I would say.

[Eric Wieser]

I think it's worth opening an issue about and referencing that in the porting note

[Eric Wieser]

That way it's easy to clean everything up if we fix it

[Eric Wieser]

This problem will likely bite us for every lemma tagged with the "partially applied ext lemma" note.

[Gabriel Ebner]

std4#84