calc unification

Stream: lean4

[Heather Macbeth]

Here is an apparent discrepancy between Lean 3 calc and Lean 4 calc, regarding the ability to fill in _ with terms provided in other places. In Lean 4:

def List.Sorted (R : α → α → Prop) (w : List α) : Prop := sorry

def List.foo (l : List α) (n : Nat) (hn : n < l.length) : α := sorry

theorem List.rel_foo {R : α → α → Prop} {l : List α} (h : l.Sorted R) {i j : Nat}
    (hi : i < l.length) (hj : j < l.length) (hij : i < j) :
    R (l.foo i hi) (l.foo j hj) :=
  sorry

example (w : List Nat) (hw : w.Sorted (· ≥ ·)) {i j : Nat}
    (hi : i < w.length) (hj : j < w.length) (hij : j < i) :
    w.foo i hi ≤ w.foo j hj := by
  calc
    w.foo i _ ≤ w.foo j _ := by apply List.rel_foo hw _ _ hij ; sorry ; sorry
    -- goals generated for `i < List.length w` and `j < List.length w`

[Heather Macbeth]

And in Lean 3 -- no need to fill the holes for i < List.length w and j < List.length w:

variables {α : Type*}

def list.Sorted (R : α → α → Prop) (w : list α) : Prop := sorry

def list.foo (l : list α) (n : nat) (hn : n < l.length) : α := sorry

theorem list.rel_foo {R : α → α → Prop} {l : list α} (h : l.Sorted R) {i j : nat}
    (hi : i < l.length) (hj : j < l.length) (hij : i < j) :
    R (l.foo i hi) (l.foo j hj) :=
  sorry

example (w : list nat) (hw : w.Sorted (≥)) {i j : nat}
    (hi : i < w.length) (hj : j < w.length) (hij : j < i) :
    w.foo i hi ≤ w.foo j hj := by
  calc
    w.foo i _ ≤ w.foo j _ : by apply list.rel_foo hw _ _ hij

[Heather Macbeth]

I am working on nightly-2023-02-03 which I think has all the recent calc improvements by @Gabriel Ebner. It is a minimization of a change needed to make mathlib compile after the bump (see !4#1999).

[Heather Macbeth]

In my opinion, this is of much lower importance than the other issues Gabriel has fixed recently in calc. So if the answer is "this is how it has to be as a tradeoff in fixing the other issues", that's fine with me. Just wanted to record it.

[Gabriel Ebner]

lean4#2095 As a quick fix, you can remove the by.