cc tactic comes to Lean4

Stream: lean4

[Pol'tta / Miyahara Kō]

I'm glad to tell you this news.
I've ported cc tactic in Mathlib and awaiting review. (#5938)
I post this thread in not mathlib but lean4 stream because this is the core function of Lean3.
I hope this tactic helps your formal proof.

[Scott Morrison]

Wow, impressive. :-) I wasn't expecting that.

Can I ask about the test suite: does this have everything that was in the Lean 3 tests (if any such even existed??)

[Pol'tta / Miyahara Kō]

@Scott Morrison Yes, I ported all tests of cc, it's the large tests.

[Pol'tta / Miyahara Kō]

By the way, who can review this PR?

[Johan Commelin]

@Scott Morrison @Mario Carneiro @Kyle Miller @Floris van Doorn @Anne Baanen @Rob Lewis are some of the maintainers that can review meta PRs.

[Pol'tta / Miyahara Kō]

@Scott Morrison
I requested you review. This is a large and complicated tactic so you can take all the time you want.
Thank you for review.

[Scott Morrison]

Okay! I will hopefully be able to let you know next week if/when I can actually review it! :-)

[Rob Lewis]

This is an impressive amount of work! To make reviewing easier, could I ask for some "big picture" documentation? A sketch of the algorithm, what features it supports/doesn't support, what the key functions are?

[Pol'tta / Miyahara Kō]

This algorithm is too complex to describe in the header. I've added the reference to the paper about the algorithm in header.

[Pol'tta / Miyahara Kō]

Oh, I found the good summary of this tactic from tactic documents in Lean3! I've replaced the header with this.

[Pol'tta / Miyahara Kō]

@Scott Morrison Any news?

[Pol'tta / Miyahara Kō]

@Scott Morrison Any news?

[Scott Morrison]

I'm sorry, I don't think I'm going to be reviewing cc for mathlib soon.

[Patrick Massot]

@Pol'tta / Miyahara Kō, Scott is very busy with important infrastructure work. In particular he tries to ensure that Lean core, the Std lib and Mathlib can grow together harmoniously.

[Pol'tta / Miyahara Kō]

@Scott Morrison @Patrick Massot OK! I'm sorry to rush you!

[Patrick Massot]

You don't have to be sorry, I'm only explaining why Scott is not available. I know the review process can be very frustrating, especially when you have very technical metaprogramming PRs.

[Patrick Massot]

Scott is also facing this from the other side with his rewrite search PR.

[Mario Carneiro]

I might take a stab at it, but I'm starting to realize that I am rather oversubscribed, so no promises

[James Gallicchio]

this is maybe a chaos-gremlin suggestion, but thoughts on just merging it and battle-testing it in mathlib? :stuck_out_tongue_closed_eyes: I think everyone prefers a useful but maybe buggy tactic to no tactic at all

[James Gallicchio]

if we just want a code style review, I'd be happy to do that

[Scott Morrison]

@James Gallicchio, if you could take a start that would be great.

[Johan Commelin]

James Gallicchio said:

I think everyone prefers a useful but maybe buggy tactic to no tactic at all

Yes an no. The nightmare scenario is: user A submits a proof using buggy_tactic and everything is fine, because we're in a happy spot where the bug isn't triggered. Then user B refactors a file somewhere in the hierarchy, and now the proof using buggy_tactic is broken, because a bug got triggered, despite the fact that it still should work.
Now user B suddenly has to fix this proof even when the maths in that file is not their expertise, and fixing the tactic isn't their expertise either.

[Johan Commelin]

So I only want buggy tactics that are buggy in a reliable way.

[Kevin Buzzard]

Does this situation indicate a problem with the system? With maths PRs there are usually one or two people who can review something, but here we have a potentially useful tactic but the obvious candidate reviewers are clearly tied up with other things right now.

By the way @Pol'tta / Miyahara Kō thank you very much for porting this tactic! It's one of those tactics which I only use rarely but when I do use it I'm always very grateful that it's there :-)

[Mario Carneiro]

This is a very complex tactic, one of the most complex tactics to be written in mathlib4 to date. It definitely needs a review, if only so that someone other than the author can be in a position to fix problems in it later

[Mario Carneiro]

Otherwise it will suffer the fate of many other tactics in mathlib like omega, finish, and eblast that are effectively dead because no one can maintain them

[Jakob von Raumer]

I think e.g. omega might become obsolete with a good aesop configuration

[Ioannis Konstantoulas]

Mario Carneiro said:

Otherwise it will suffer the fate of many other tactics in mathlib like omega, finish, and eblast that are effectively dead because no one can maintain them

I... I can't help but giggle at the relationship between the names of those tactics and their status :sweat_smile:

[Scott Morrison]

Jakob von Raumer said:

I think e.g. omega might become obsolete with a good aesop configuration

You might be thinking of a different omega? omega is not going to be replaced by aesop. A Lean 4 implementation is in the works. (Noting that the mathlib3 implementation was actually far from complete!)