ac_refl

Stream: mathlib4

[Scott Morrison]

In Order.BooleanAlgebra, we encounter a whole pile of proofs by ac_refl. ac_refl uses the machinery that cc develops. I think we've been punting on cc for a while. Do we have ideas for porting / replacing this?

[Mario Carneiro]

Note that there is a lean 4 tactic by the name ac_rfl

[Mario Carneiro]

it's a from-scratch implementation though so no promises that it closes the same goals

[Scott Morrison]

ac_rfl does in fact work, once you realise the mathlib4's IsAssociative is not the same as Lean.IsAssociative...

[Scott Morrison]

I am not going to attempt to unify them, just add instances from mathlib's versions to core's versions.

[Scott Morrison]

It works perfectly in Order.BooleanAlgebra.

[Patrick Massot]

What is the current status of porting ac_refl? I don't see it tracked on https://github.com/leanprover-community/mathlib4/issues/430. One of the MSRI projects would have been a lot nicer with this tactic.

[Yury G. Kudryashov]

git grep ac_rfl shows many matches

[Patrick Massot]

Oh, it's ac_rfl, not ac_refl! Thanks!