cc tactic

Stream: lean4

[Chris Lovett]

The Natural Number Game and the Hithikers guide to Logic Verification, make quite a bit of use of the congruence closure tactic "cc", which doesn't seem to exist in Mathlib4. Is anyone working on it? Does anyone know how to port it to a different combination of existing Lean 4 tactics?

[James Gallicchio]

I was looking into it, but it's a big project and I am kinda busy this semester... I've made a tiny bit of progress implementing the data structures needed for it

[Mario Carneiro]

It's on the todo list along with a bunch of other tactics. We're aware of it but these kinds of things don't get implemented overnight (most of the time)