Congruence closure

Stream: general

[Yury G. Kudryashov]

Hi, what cc tactic can do?

[Yury G. Kudryashov]

Docs say "Tries to prove the main goal using congruence closure."

[Yury G. Kudryashov]

But no examples

[Reid Barton]

Basically it can reason about equality

[Patrick Massot]

https://github.com/leanprover-community/mathlib/blob/master/docs/tactics.md#cc-congruence-closure

[Rob Lewis]

(or https://leanprover-community.github.io/mathlib_docs/tactics.html#cc%20(congruence%20closure) )

[Moses Schönfinkel]

I've also grep'd for cc in whatever file I currently have open to give you a practical example. These are the kinds of things I use it for normally.

this : l₂h = y
⊢ (x, y) = (x, l₂h)

eq₁ : {x := a, y := r} = hd,
h₁ : {x := px, y := py} = hd
⊢ py = r

I am not sure whether it's an overkill for these but there you go - I use it to show equality "through" structures.

[Jesse Michael Han]

cc can also discharge some otherwise gnarly heterogeneous equality goals

[Mario Carneiro]

both of those are cases, refl for me