simp is not picking up a theorem

Stream: lean4

[Tomas Skrivan]

In this particular case, the simp tactic does not simplify the target with theorem foo even though rw [foo] solves it.

variable {U V}

def f : (U → V) → (U → U) := sorry
def add  {U} : U → U → U := sorry

@[simp] theorem foo  (u : U) : f (add u) = id := sorry

def bar (u v : U) : f (add u) v =  id v :=
by
  simp    --- Why is foo not used here?
  rw [foo]
  simp

What is going on here?

[Mac]

@Tomas Skrivan Could it be that simp does not work on partial application equalities?

[Tomas Skrivan]

What does that mean?

[Mac]

I mean does simp try to look for theorems of partial subsets of an application? It may just look for theorems about the individual component terms (i.e., f, add u, v) and the full term (e.g., f (add u) v), but not for the partial term (e.g., f (add u)).

[Tomas Skrivan]

Yes it does look for subexpressions. If you add this extra theorem

@[simp] theorem foo2  (u : U) : (add u) = (add (id u)) := sorry

Then the first simp rewrites the goal to f (add (id u)) v = v

[Mac]

Tomas Skrivan That is a very different kind of subexpression. That falls under the category of 'individual component terms' I mentioned. Polyadic applications in Lean 4 are a single Syntax-- thus f (add u) is not a sub--Syntax of f (add u) v, it is merely a slice of the full application Syntax. Thus, simp may not be considering such slices.

[Mac]

However, this is just a hypothesis of mine as to what the problem may be. simp very well may look for theorems of said partial applications and this could just be a bug. I am sadly not an expert on how simp works, but such a thing could be the reason one why your example does not work.

[Tomas Skrivan]

Makes sense now. I will investigate if that is really the problem or not.

[Leonardo de Moura]

I fixed this issue. The example above should now work with master.

[Tomas Skrivan]

Huge huge thanks! Works perfectly. I'm trying to build an automatic differentiation tool and this started looking as a bigger and bigger problem.

[Sebastian Ullrich]

Mac said:

Polyadic applications in Lean 4 are a single Syntax

Note that tactics work on the elaborated Expr level, which uses binary applications

[Mac]

@Sebastian Ullrich Yeah, that may me a bit unsure of my statement, but looking at the fix Leo made, it seems there are many places even at the Expr level where said binary applications are convert back into an Array.

[Sebastian Ullrich]

sure