simp lemmas with side conditions

Stream: mathlib4

[Scott Morrison]

I am confused about something. Why is a lemma like src4#LieHom.idealRange_eq_top_of_surjective marked as @[simp]? It has the side condition h : Function.Surjective f. I think simp would never be able to use this lemma.

[Scott Morrison]

Oh!!! My confusion is that this is a simp regression.

[Scott Morrison]

In Lean3:

@[simp] lemma ideal_range_eq_top_of_surjective (h : function.surjective f) : f.ideal_range = ⊤ :=
begin
  rw ← f.range_eq_top at h,
  rw [ideal_range_eq_lie_span_range, h, ← lie_subalgebra.coe_to_submodule,
    ← lie_submodule.coe_to_submodule_eq_iff, lie_submodule.top_coe_submodule,
      lie_subalgebra.top_coe_submodule, lie_submodule.coe_lie_span_submodule_eq_iff],
  use ⊤,
  exact lie_submodule.top_coe_submodule,
end

example (h : function.surjective f) : f.ideal_range = ⊤ :=
by simp only [ideal_range_eq_top_of_surjective, h] -- works fine

while in Lean4

@[simp]
theorem idealRange_eq_top_of_surjective (h : Function.Surjective f) : f.idealRange = ⊤ := by
  rw [← f.range_eq_top] at h
  rw [idealRange_eq_lieSpan_range, h, ← LieSubalgebra.coe_to_submodule, ←
    LieSubmodule.coe_toSubmodule_eq_iff, LieSubmodule.top_coeSubmodule,
    LieSubalgebra.top_coe_submodule, LieSubmodule.coe_lieSpan_submodule_eq_iff]
  use ⊤
  exact LieSubmodule.top_coeSubmodule
#align lie_hom.ideal_range_eq_top_of_surjective LieHom.idealRange_eq_top_of_surjective

example (h : Function.Surjective f) : f.idealRange = ⊤ := by
  simp only [idealRange_eq_top_of_surjective, h] -- doesn't do anything, so `by` fails with unsolved goals.

[Scott Morrison]

which minimises straightforwardly as oops.

[Scott Morrison]

Am I missing something!? How did we miss this?

[Scott Morrison]

The Lean4 failure, under set_option trace.Meta.Tactic.simp true, gives:

[Meta.Tactic.simp.discharge] >> discharge?: Function.Surjective ↑f

[Meta.Tactic.simp.discharge] @LieHom.idealRange_eq_top_of_surjective, failed to discharge hypotheses
      Function.Surjective ↑f

[Meta.Tactic.simp.unify] @eq_self:1000, failed to unify
      ?a = ?a
    with
      LieHom.idealRange f = ⊤

[Scott Morrison]

even though h : Function.Surjective f is right there in the simp set.

[Scott Morrison]

and it's not that discharging side goals is completely broken:

def P : Prop := True
@[simp] theorem foo (h : P) : Nat = Int := by sorry
example (h : P) : Nat = Int := by simp only [foo, h]   -- works fine

[Scott Morrison]

I'm not sure in what direction I should be trying to minimize this.

[Scott Morrison]

Okay, partial minimisation:

-- Lean 3, works fine
import algebra.hom.group

variables {M N : Type*} [monoid M] [monoid N] (f : M →* N)
theorem foo (h : function.surjective f) : f 1 = 1 := by simp

example (h : function.surjective f) : f 1 = 1 := by simp only [foo, h]

-- Lean 4, fails
import Mathlib.Algebra.Hom.Group

variable [Monoid M] [Monoid N] (f : M →* N)
theorem foo (h : Function.Surjective f) : f 1 = 1 := by simp

example (h : Function.Surjective f) : f 1 = 1 := by simp only [foo, h]

[Scott Morrison]

And a mathlib-free minimization:

-- Lean 3, works fine
class one (α : Type _) :=
(one : α)

structure OneHom (M : Type _) (N : Type _) [one M] [one N] :=
(to_fun : M → N)
(map_one : to_fun one.one = one.one)

variables {M N : Type _} [one M] [one N] (f : OneHom M N)

theorem foo (h : function.surjective f.to_fun) : f.to_fun one.one = one.one := f.map_one

example (h : function.surjective f.to_fun) : f.to_fun one.one = one.one := by simp only [foo, h]

-- Lean 4, fails
@[reducible] def Function.Surjective (f : α → β) : Prop := ∀ b, ∃ a, f a = b

class One (α : Type u) where
  one : α

structure OneHom (M : Type _) (N : Type _) [One M] [One N] where
  to_fun : M → N
  map_one : to_fun One.one = One.one

variable {M N : Type _} [One M] [One N] (f : OneHom M N)

theorem foo (h : Function.Surjective f.to_fun) : f.to_fun One.one = One.one := f.map_one

example (h : Function.Surjective f.to_fun) : f.to_fun One.one = One.one := by simp only [foo, h]

[Scott Morrison]

@Gabriel Ebner, @Mario Carneiro, do either of you recognise this, or see what I'm doing wrong here? It seems Lean 4 is having great difficulty discharging side goals of simp lemmas. :-(

[Mario Carneiro]

minimized some more:

-- Lean 4, fails
@[reducible] def Function.Surjective (f : α → β) : Prop := ∀ b, ∃ a, f a = b

example (h : Function.Surjective f) : Function.Surjective f := by simp only [h]

[Mario Carneiro]

TBH it's not that surprising to me that this fails, the hypothesis has a lot of internal structure and simp is getting lost in the weeds, necessitating some additional theorems like (A -> True) = True to simplify it

[Scott Morrison]

Haha, nice :-) That's terrible. Just double checking:

-- Lean 3, works fine
example {α β : Type} {f : α → β} (h : function.surjective f) : function.surjective f := by simp only [h]

[Mario Carneiro]

which is why simp only doesn't work

[Scott Morrison]

It hadn't occurred to me until now that the @[reducible] was implicated here!

[Mario Carneiro]

I think it's not the full story however, the last two cases here have different behavior even though I only unfolded reducibles:

@[reducible] def Function.Surjective (f : α → β) : Prop := ∀ b, ∃ a, f a = b

variable {f : α → β}
example (h : ∀ b, ∃ a, f a = b) : ∀ b, ∃ a, f a = b := by
  simp only [h] -- fails
example (h : ∀ b, ∃ a, f a = b) : ∀ b, ∃ a, f a = b := by
  simp only [h, implies_true] -- ok
example (h : Function.Surjective f) : ∀ b, ∃ a, f a = b := by
  simp only [h, implies_true] -- ok
example (h : Function.Surjective f) : Function.Surjective f := by
  simp only [h, implies_true] -- fails

[Mario Carneiro]

example (h : ∀ b, ∃ a, f a = b) : Function.Surjective f := by
  simp only [h, implies_true] -- fails

[Scott Morrison]

Curiously (at least) the first 1/3 of mathlib4 compiles just fine without @[reducible] on Function.Surjective.

[Scott Morrison]

!4#5063 removes @[reducible] from Function.Surjective.

[Scott Morrison]

and !4#5064 adds some simp lemmas that were missing, but become useful after this fix. (and which I needed for something else).

[Gabriel Ebner]

See also !4#375 which removed @[reducible] on Function.Injective.