simp guard

Stream: lean4

[Tomas Skrivan]

I have a simplifier theorem that applies to itself, which is bad, but it happens only if one of the arguments is inferred to be identity function.

I would like to write a simp guard that prevents application of a theorem if one of the arguments is particular expression. I think I know how to do this, I'm more asking if this is a good idea or not?

---

Particular example - differentiation of function composition:

variable {α β γ δ : Type}

def D (f : α → β) : α → α → β := sorry

theorem D_comp
  (f : β → γ) (g : α → β)
  : D (λ x => f (g x)) = λ x dx => D f (g x) (D g x dx) := sorry

The D function is differential function, taking a function and returning its differential. The problem with D_comp is that if f has an additional argument then simplifier fails to use this theorem.

Therefore I have an additional theorem:

theorem D_comp_parm
  (f : β → δ → γ) (g : α → β) (d : δ)
  : D (λ x => f (g x) d) = λ x dx => D (λ y => f y d) (g x) (D g x dx) :=
by
  simp [D_comp] -- fails to unify
  apply D_comp (λ y => f y d) g -- we have to specify `f` explicitly

However, this theorem has a problem as it applies to itself.

This demonstrates the behavior:

example
  (f : β → δ → γ) (g : α → β) (d : δ)
  : D (λ x => f (g x) d) = λ x dx => D (λ y => f y d) (g x) (D g x dx) :=
by
  -- simp [D_comp_parm] -- timeout as D_comp_parm applies to itself

  -- Fails to solve the goal as it applies the theorem to rhs too with `g = id`
  -- This behavior is undesirable
  simp (config := {singlePass := true}) only [D_comp_parm]

  -- force the application of the theorem only to the lhs
  conv =>
    lhs
    simp (config := {singlePass := true}) only [D_comp_parm]

  done

My idea is to create a new attribute simp_guard that would be used as:

@[simp, simp_guard g id]
theorem D_comp_parm
   ...

which would prevent applying this theorem if g unifies to id.

---

How to implement this?

I believe this can be done in synthesizeArgs function. Using the thmId : Origin I can get the theorem's declaration name thus I should be able to check if the theorem has the simp_guard attribute and do the appropriate checks.

So the question is: Is this a good idea? Would anyone else use this? Is there a better way to achieve similar behavior?

[James Gallicchio]

Is there a simp-normal form for D applications? Maybe this is somewhere that a dedicated tactic for reducing D applications would be better?

[Tomas Skrivan]

James Gallicchio said:

Is there a simp-normal form for D applications?

What does "simp-normal form" exactly mean? I have only a vague idea and thus not sure how to answer this.

James Gallicchio said:

Maybe this is somewhere that a dedicated tactic for reducing D applications would be better?

Yes I will slowly build a custom tactic for it but at its core it is has to behave a lot like the simplifier. Instead of reimplementing simplifier myself I want to slowly modify the existing one into tactic I want.

[Kevin Buzzard]

Sometimes there is more than one way to coerce a term into another term. For example if a term f of some complicated type (like a ring homomorphism) can be coerced to a function, then you might find that f.1, f.to_fun, and ⇑f are all ways of making that coercion. If we had lemmas in mathlib about all three of those ways it would be horrible, so we typically choose one of them to be the "simp normal form" (for example let's choose ⇑f) and then we might write simp lemmas of the form f.1 = ⇑f and f.to_fun = ⇑f, so that the simplifier is always pushing towards the form we chose, and then (for example if f is a ring homomorphism) lemmas like ⇑f (a + b) = ⇑f a + ⇑f b will be found by simp even if for whatever reason your goal ended up having f.1 (a + b) in. That's my understanding of simp normal form anyway. Is it in the glossary? I never remember how this works. glossary#simp_normal_form ?

[Kevin Buzzard]

glossary#simp-normal-form apparently (although it's mostly a broken link :-/ )

[Tomas Skrivan]

Makes sense, remember seeing stuff like this in mathlib.

However, I still unsure what would that mean for D as it involves functions and you can create whatever shenanigans with lambdas.

[James Gallicchio]

Is it possible to avoid this entirely by just flipping function argument order as needed?

[James Gallicchio]

(Maybe you could even quite literally have a simp lemma do that flipping, and consider the expression simp-normalized only if it's eta reduced or something)

[Tomas Skrivan]

I do not know how to write such lemma.

[Tomas Skrivan]

Maybe something like this?

def swap (f : α → β → γ) := λ x y => f y x
@[simp]
theorem D_norm_parm
  (f : β → δ → γ) (d : δ) : D (λ y => f y d) = D (λ y => swap f d y) := by rfl

But then (D fun x => f (g x) d) simplifies to (D fun y => swap (fun y => f (g y)) d y) and how do you deal with that?

[James Gallicchio]

Do you have some examples of f?

[Tomas Skrivan]

I don't know, it can be whatever for example arctan2

[Tomas Skrivan]

It can also be Function.comp

[James Gallicchio]

and the idea with like arctan2 is you want to be differentiating by the first arg instead of the second and then you have the D fun x => arctan (g x) y?

[Tomas Skrivan]

exactly

[Tomas Skrivan]

If anyone is interested, I have managed to get the simplified guard working.

So you can now write a theorem like this:

@[simp_guard g (λ (x : α) => x)]
theorem D_comp_parm {α β γ : Type}
  (f : β → δ → γ) (g : α → β) (d : δ)
  : D (λ x => f (g x) d) = λ x dx => D (λ y => f y d) (g x) (D g x dx) :=
by
  apply D_comp (λ y => f y d) g

where the @[simp_guard g (λ (x : α) => x)] says:

If the theorem is used as simp theorem and g unifies to λ (x : α) => x then do not apply the theorem

Code pointers:
definition of simp_guard

[Tomas Skrivan]

The only unfortunate thing is that lsp is having trouble with α in @[simp_guard g (λ (x : α) => x)]. Asking for "Go to definition" on α gives an error LSP :: Not found for: α

[Tomas Skrivan]

And I'm a bit unsure how to handle metavaribles, one appears if you write the simp guard as @[simp_guard g (λ x => x)]