Simp bug - produces`application type mismatch`

Stream: lean4

[Tomas Skrivan]

I'm playing around with combinatory logic and I have encountered a problem with simp tactic. It seems to produce an invalid expression on nightly build.

This example defines S combinator with B(comp) and C(swap) and diagonal(no clue what is the official name)

Define comp, swap, diag and their reductions

variable {X : Type u} {Y : Type v} {Z : Type w}

def comp (f : Y→Z) (g : X→Y) (x : X) := f (g x)
def swap (f : X→Y→Z) (y : Y) (x : X) := f x y
def diag (f : X→X→Y) (x : X) := (f x x)

@[simp] def comp_reduce (f : Y→Z) (g : X→Y) (x : X) : (comp f g x) = f (g x) := by simp[comp] done
@[simp] def swap_reduce (f : X→Y→Z) (y : Y) (x : X) : (swap f y x) = f x y := by simp[swap] done
@[simp] def diag_reduce (f : X→X→Y) (x : X) : (diag f x) = f x x := by simp[diag] done

Define subs(S combinator) in terms of the previous three and prove it is indeed S combinator

def subs : (X→Y→Z) → (X→Y) → (X→Z) := (swap (comp (comp diag) (comp comp (swap comp))))

@[simp] def subs_reduce (f : X→Y→Z) (g : X→Y) (x : X) : (subs f g x) = (f x) (g x) :=
by
  conv => lhs; whnf;
  done

@[simp] def subs_reduce' (f : X→Y→Z) (g : X→Y) (x : X) : (subs f g x) = (f x) (g x) :=
by
  simp[subs]
  done

On nighly build leanprover/lean4:nightly-2021-10-13 proving subs_reduce' fails with an error:

application type mismatch
  comp diag (comp (swap comp g)) x
argument has type
  X
but function has type
  (X → Y → Z) → X → Z

[Tomas Skrivan]

For some reason after couple of simplifications it produces an invalid goal:

comp diag (comp (swap comp g)) x f = f x (g x)

but the correct goal should be

comp diag (comp (swap comp g)) f x = f x (g x)

Continuing from that point on works fine:

def finish_proof (f : X→Y→Z) (g : X→Y) (x : X) : comp diag (comp (swap comp g)) f x = f x (g x) :=
by
  simp
  done  -- works!

[Tomas Skrivan]

The simp.rewrite trace is:

23:2:
[Meta.Tactic.simp.rewrite] swap_reduce:1000, swap (comp (comp diag) (comp comp (swap comp))) f
  g ==> comp (comp diag) (comp comp (swap comp)) g f
23:2:
[Meta.Tactic.simp.rewrite] comp_reduce:1000, comp (comp diag) (comp comp (swap comp))
  g ==> comp diag (comp comp (swap comp) g)
23:2:
[Meta.Tactic.simp.rewrite] comp_reduce:1000, comp comp (swap comp) g ==> comp (swap comp g)

[Tomas Skrivan]

Manually repeating these rewrites works fine

def subs_reduce'' (f : X→Y→Z) (g : X→Y) (x : X) : ((swap (comp (comp diag) (comp comp (swap comp)))) f g x) = (f x) (g x) :=
by
  rw [swap_reduce]
  rw [comp_reduce]
  conv =>
    enter [1,2]
    rw [comp_reduce]
  done

[Tomas Skrivan]

Here is a self contained version that produces invalid goal just after one step of simp.rewrite

variable {X : Type u} {Y : Type v} {Z : Type w}

def comp (f : Y→Z) (g : X→Y) (x : X) := f (g x)
def swap (f : X→Y→Z) (y : Y) (x : X) := f x y
def diag (f : X→X→Y) (x : X) := (f x x)

@[simp] def comp_reduce (f : Y→Z) (g : X→Y) (x : X) : (comp f g x) = f (g x) := by simp[comp] done
def swap_reduce (f : X→Y→Z) (y : Y) (x : X) : (swap f y x) = f x y := by simp[swap] done
@[simp] def diag_reduce (f : X→X→Y) (x : X) : (diag f x) = f x x := by simp[diag] done

def subs : (X→Y→Z) → (X→Y) → (X→Z) := (swap (comp (comp diag) (comp comp (swap comp))))

set_option trace.Meta.Tactic.simp true

def foo {W} := ((comp comp (swap comp)) : (X→Y) → _ → W → X → Z)
def subs_reduce' (f : X→Y→Z) (g : X→Y) (x : X) : comp (comp diag) foo g f x = (f x) (g x) :=
by
  simp
  done   --  application type mismatch: comp diag (foo g) x

[Tomas Skrivan]

Maybe related to this commit. It even has a comment about reversed order of arguments.

[Leonardo de Moura]

Pushed a fix for this bug.
https://github.com/leanprover/lean4/commit/6b2303b24305deab05a7609985f03af3e9fdece5