Zulip Chat Archive

Stream: lean4

Topic: Simp bug - produces`application type mismatch`


Tomas Skrivan (Oct 15 2021 at 15:01):

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 : YZ) (g : XY) (x : X) := f (g x)
def swap (f : XYZ) (y : Y) (x : X) := f x y
def diag (f : XXY) (x : X) := (f x x)

@[simp] def comp_reduce (f : YZ) (g : XY) (x : X) : (comp f g x) = f (g x) := by simp[comp] done
@[simp] def swap_reduce (f : XYZ) (y : Y) (x : X) : (swap f y x) = f x y := by simp[swap] done
@[simp] def diag_reduce (f : XXY) (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 : (XYZ)  (XY)  (XZ) := (swap (comp (comp diag) (comp comp (swap comp))))

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

@[simp] def subs_reduce' (f : XYZ) (g : XY) (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 (Oct 15 2021 at 15:15):

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 : XYZ) (g : XY) (x : X) : comp diag (comp (swap comp g)) f x = f x (g x) :=
by
  simp
  done  -- works!

Tomas Skrivan (Oct 15 2021 at 16:13):

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 (Oct 15 2021 at 16:19):

Manually repeating these rewrites works fine

def subs_reduce'' (f : XYZ) (g : XY) (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 (Oct 15 2021 at 16:36):

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 : YZ) (g : XY) (x : X) := f (g x)
def swap (f : XYZ) (y : Y) (x : X) := f x y
def diag (f : XXY) (x : X) := (f x x)

@[simp] def comp_reduce (f : YZ) (g : XY) (x : X) : (comp f g x) = f (g x) := by simp[comp] done
def swap_reduce (f : XYZ) (y : Y) (x : X) : (swap f y x) = f x y := by simp[swap] done
@[simp] def diag_reduce (f : XXY) (x : X) : (diag f x) = f x x := by simp[diag] done

def subs : (XYZ)  (XY)  (XZ) := (swap (comp (comp diag) (comp comp (swap comp))))

set_option trace.Meta.Tactic.simp true

def foo {W} := ((comp comp (swap comp)) : (XY)  _  W  X  Z)
def subs_reduce' (f : XYZ) (g : XY) (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 (Oct 15 2021 at 16:54):

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

Leonardo de Moura (Oct 18 2021 at 21:01):

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


Last updated: Dec 20 2023 at 11:08 UTC