Simp does not unify with subexpresion

Stream: lean4

[Tomas Skrivan]

I'm having a problem with simp tactic, it is not applying a theorem about f a to an expression f a b.

Here is MWE:

class Zero (α) where
  (zero : α)
export Zero (zero)

instance : Zero Nat := ⟨0⟩
instance {α β} [Zero β] : Zero (α → β) := ⟨λ _ => zero⟩

@[simp] theorem foo [Zero α] [Zero β] (f : α → β) : f zero = zero := sorry

set_option trace.Meta.Tactic.simp true
theorem foo' [Zero α] (f : Nat → β → α) (b : β) : f zero b = zero := by simp done    -- Error: unsolved goals
set_option trace.Meta.Tactic.simp false

theorem foo'' [Zero α] (f : Nat → β → α) (b : β) : f zero b = zero :=
by
  rw [foo f]
  simp[zero]
  done

The trace reveals that simp does not even attempt to unify ?f zero with f zero . Why is that?

[Tomas Skrivan]

This problem is very similar to the one I had earlier, however this time f is a parameter of the simplification theorem foo.

[Scott Morrison]

Because the head symbol of the LHS of the simp lemma is a variable (f), Lean can not match on it. This is a fundamental limitation of the simplifier.

[Scott Morrison]

See, for example, in mathlib3, how we use bundled morphisms (e.g. ring_hom and all its friends) to get around this.

[Tomas Skrivan]

Right, when you use morphism then the head of the expression would be coercion and simplifier has no longer problem with it.
Interestingly enough, I have encountered this problem exactly when working with unbundled morphisms, i.e. when the property of a function is automatically fetched by the type class system.

[Tomas Skrivan]

I went through some lengths to be able to work with unbundled morphisms, so I do not want to revert back to bundled ones just yet where I had tons of other problems.

Couldn't the simplifier exploit the fact that the argument, zero, is fixed in the simplification theorem? Or is it fundamentally important that the matching is based on the head of the expression?

[Sebastian Ullrich]

Removal of the b argument shows that the mvar head is not the problem

[Sebastian Ullrich]

Or that it is at least connected with the partial application issue, I haven't looked at the implementation yet

[Sebastian Ullrich]

Basically, with a constant head, simp knows how many arguments to match, but not with a variable head

[Tomas Skrivan]

Ok this makes sense that simp should not do all of these unifications if variable head would be allowed.

[Tomas Skrivan]

However, I'm still unsure how am I supposed to deal with the simplification of the fact that "linear map of zero is zero" and keep on working with unbundled morphisms. I probably need to write a tactic that looks at a zero and test all functions applied to it for linearity.

[Kyle Miller]

There's something I've wanted to experiment with, which is having "semibundled" morphisms. You can attach an instance to an unbundled morphism using a custom identity function -- using the example below, map_zero f still is f, but now it's carrying around a has_map_zero instance that theorems can make use of without needing to do typeclass inference again. It also lets you apply simp lemmas when the function is the head symbol, since there's a map_zero there. I imagine you'd want some tactic to automatically wrap everything in map_zero for this to not be annoying to work with.

class Zero (α) where
  (zero : α)
export Zero (zero)

instance : Zero Nat := ⟨0⟩
instance {α β} [Zero β] : Zero (α → β) := ⟨λ _ => zero⟩

class has_map_zero [Zero α] [Zero β] (f : α → β) : Prop where
  map_zero : f zero = zero

/-- Attach a proof that `f` implements `has_map_zero` to the expression. -/
@[reducible]
def map_zero [Zero α] [Zero β] (f : α → β) {h : has_map_zero f} := f

/-- Use `rw [attach_map_zero f]` to insert the `has_map_zero` instance
into the expression.
(Caveat: this unfortunately can be recursively applied...) -/
theorem attach_map_zero [Zero α] [Zero β] (f : α → β) [h : has_map_zero f] :
  f = map_zero f (h := h) := rfl

-- `h` is an implicit argument so you don't need to do typeclass inference for it to use the theorem.
@[simp]
theorem map_zero_apply_zero [Zero α] [Zero β] (f : α → β) {h : has_map_zero f} :
  map_zero f (h := h) zero = zero := h.map_zero

instance [Zero α] [Zero β] : has_map_zero (zero : α → β) where
  map_zero := rfl

abbrev const_zero : Nat → Nat := zero

theorem const_zero_apply : const_zero zero = zero :=
by
  rw [attach_map_zero const_zero]
  simp

[Tomas Skrivan]

@Kyle Miller Interesting idea, I would need to experiment with it a bit to understand what exactly is going on there, but I might get inspired by your approach.