Zulip Chat Archive

Stream: lean4

Topic: Simp does not unify with subexpresion


Tomas Skrivan (Nov 07 2021 at 01:22):

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 (Nov 07 2021 at 01:37):

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 (Nov 07 2021 at 01:50):

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 (Nov 07 2021 at 01:50):

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

Tomas Skrivan (Nov 07 2021 at 08:24):

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 (Nov 07 2021 at 09:36):

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 (Nov 07 2021 at 11:05):

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

Sebastian Ullrich (Nov 07 2021 at 11:07):

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

Sebastian Ullrich (Nov 07 2021 at 11:21):

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

Tomas Skrivan (Nov 07 2021 at 17:03):

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

Tomas Skrivan (Nov 07 2021 at 17:06):

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 (Nov 07 2021 at 17:40):

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 (Nov 08 2021 at 09:10):

@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.


Last updated: Dec 20 2023 at 11:08 UTC