Unification not working on simple expected case.

ericrbg commented 1 year ago

Prerequisites

[X] Put an X between the brackets on this line if you have done all of the following:
- Checked that your issue isn't already filed.
- Reduced the issue to a self-contained, reproducible test case.

Description

example (a b c : Nat) : a = b → a * c = b * c := congrArg _ --fails, works with (· * c) requires you to explicitly spell out the function. In lean3, this is not required, and often used in mathlib.

Expected behavior: Success.

Actual behavior:

type mismatch
  congrArg ?m.56535
has type
  ?m.56533 = ?m.56534 → ?m.56535 ?m.56533 = ?m.56535 ?m.56534 : Prop
but is expected to have type
  a = b → a * c = b * c : Prop

Reproduces how often: 100%

Versions

Lean (version 4.0.0-nightly-2023-01-16, commit 5349a089e5bb, Release) OSX Ventura 13.1, M1 Mac

ericrbg commented 1 year ago

Just want to confirm that this is still an issue on new Lean4 releases.

kim-em commented 1 year ago

@leodemoura, do we know what exactly changed in Lean4 that resulted in this change in behaviour? I don't know here whether to say this is an unavoidable regression due to some deeper change, or something that could potentially be addressed.

Kha commented 1 year ago

@semorrison I believe this is https://github.com/leanprover/lean4/blob/29b09b0900966e7ed2f5c57abba17ef178a47db9/src/Lean/Elab/Config.lean#L14 Indeed, carefully arranging the proof of a similar example such that Lean is sure that a may be used in the hole but b/c may not (making it a regular pattern unification problem) makes it work.

example : ∀ (a b c : Nat), b = c → b * a = c * a :=
  fun a =>
    let f := _
    fun b c => congrArg f  -- replace `f` with `_` to break it

leanprover / lean4