grind congruence closure fails

Stream: lean4

[Christian Merten]

Is the following grind failure known? (It fails both on latest mathlib and on Lean nightly)

-- works
example (m : Nat) (a b : Nat → Nat) (h : b = a) :
    b m = a m := by
  grind

-- fails
example (m : Nat) (a : Nat → Nat) (f : (Nat → Nat) → (Nat → Nat)) (h : f a = a) :
    f a m = a m := by
  grind

(cc succeeds here)

[Aaron Liu]

#lean4 > `grind` with partial application

[Christian Merten]

The underlying cause might be the same, but this example does not involve any e-matching.

[Kim Morrison]

Yes, this is by design.

[Christian Merten]

Could you elaborate on why this is expected or is this documented somewhere? I could not find anything related to this in the language reference.
Is there a way to make grind succeed here (by providing some arguments for example)?

[Jakub Nowak]

Multiple people already had that problem. :C
I hope this will be addressed. I'm not familiar with grind's code so looking at this myself would be a huge work.

[Jakub Nowak]

You can add set_option trade.grind.debug true to see representation of an e-graph:

    #0 := False, [val]
    #1 := True, [val]
    #2 := true, [ctor]
    #3 := false, [ctor]
    #4 := 0, [val]
    #5 := Ordering.eq, [ctor]
    #6 := #7 #8 ↦ #8
    #7 := f
    #8 := a
    #9 := @Eq #10 #11 #13 ↦ #0
    #10 := Nat
    #11 := #7 #8 #12
    #12 := m
    #13 := #8 #12
    {#8, #6}
    {#0, #9}

f a m belongs to #11 and f a (I think, not sure) belongs to #6. I don't know why 2-ary application isn't represent as two 1-ary applications. This way, instead of #11 := #7 #8 #12 we would get #11 := #6 #12, and grind would succeed.

[Jakub Nowak]

I think it might be implemented this way, because current code isn't able to match patterns across multiple e-nodes. So to be able to match n-ary patterns the whole n-ary expression must be stored in one e-node.
This is probably not a problem, the whole expressions are stored in e-nodes and 1-ary application can always be treated as n-ary.

[Jakub Nowak]

https://arxiv.org/pdf/1701.04391

I think this is the paper grind algorithm is based upon? In the paper the proposed congruent procedure is:

procedure congruent(D, E)
  (f, a) ← app(D); (g, b) ← app(E)
  return a ≈ b and
    [(f ≈ g and type(f) ≡ type(g)) or
      (f and g are local definitions and congruent(def(f), def(g)))]

And I think that what is currently implemented in lean4 is

procedure congruent(D, E)
  (f, a) ← app(D); (g, b) ← app(E)
  return a ≈ b and
    [if f and g are both applications
      then congruent(def(f), def(g))
      else f ≈ g and type(f) ≡ type(g)]

I.e. if f and g are applications they're being eagerly unfolded.

Similarly the proposed congrhash procedure:

procedure congrhash(D)
  given: `h`, a hash function on terms
  (f, a) ← app(D)
  return hashcombine(h(repr[f]), h(repr[a]))

is implemented in lean4 as

procedure congrhash(D)
  given: `h`, a hash function on terms
  (f, a) ← app(D)
  if f is application then
    return hashcombine(congrhash(f), h(repr[a]))
  else
    return hashcombine(h(repr[f]), h(repr[a]))

The "local definition" part was replaced with checking if expression is application, which I think is fine. We don't want grind to automatically unfold definitions.
But we shouldn't eagerly unfold applications until reaching head expression. I think that implementing the congruence algorithm as described in the paper would fix the issue.

[Jakub Nowak]

Looks like this was fixed in nightly. :tada:

[Jakub Nowak]

Or not? It seems like this particular case works, by doesn't in this other example #lean4 > `grind` should unfold projections @ 💬

[Jakub Nowak]

Maybe grind learned how to rewrite equalities in head expressions, but still can't match grind patterns when head expression is an e-class?

[Théophile]

Relevant PR: https://github.com/leanprover/lean4/pull/11323