grind check for equivalence

Stream: lean4

[Marcus Rossel]

Grind has a function docs#Lean.Meta.Grind.isEqv which checks whether two internalized expressions are in the same equivalence class. Notably, AFAICT, this is not the same as checking whether two expressions are equivalent according to grind's e-graph. For example, in the following (false goal):

example (f : Nat → Nat) (a b : Nat) (h : a = b) : f a = 0 := by
  grind

... the e-graph produced by grind does not have f a and f b in the same equivalence class (in fact, f b is not even internalized), so isEqv fails. However, the e-graph has a and b in the same equivalence class, so we should be able to deduce that f a = f b. Is there a good way of doing this? I tried internalizing f b, but that doesn't place it in the same e-class as f a.

---

Sorry for asking all these grind implementation questions on Zulip - I can't make it to the relevant office hours as I'm located in Europe.

[Chris Henson]

I am not knowledgeable about these internals so I usually just spectate, but I personally find it useful for these discussions to be on Zulip as opposed to just office hours!

[Marcus Rossel]

Ah, docs#Lean.Meta.Grind.Goal.isCongruent might be the answer.