backport remove cc macros

Stream: mathlib4

[Mario Carneiro]

Just testing the waters in advance of doing the work: What do people think about removing the cc_proof, ac_app and perm_ac macros from lean 3? These macros are constructed by the cc and ac_refl tactics as a kind of "delayed proof", which can be expanded by calling the expand() function; I believe #print and the lean export both do this. Since this mechanism is reserved for lean 3 builtin tactics, it is rarely used, and most other tactics that could in principle benefit from it like norm_num and ring instead just construct the whole proof when the tactic is called, rather than delaying to proof export time.

[Scott Morrison]

Sounds good to me.

[Scott Morrison]

I'm not sure how complicated this is, but if it doesn't require too much hacking in C++ you could delegate it out, too. (e.g. I could try.)

[Mario Carneiro]

My impression, without having looked into it much, is that we should basically do the equivalent of calling expand() on the macro when we are about to emit the macro call

[Mario Carneiro]

so it should just be some shuffling around of function calls

[Gabriel Ebner]

Expanding the macros seems 100% ok to me. The more interesting issue is what we do about by cc proofs in the port.

[Mario Carneiro]

I would like us to double down on more and more advanced tactics in lean 4, so certainly the port is going to optimistically translate cc to cc

[Mario Carneiro]

I'm hoping that we can also get things like super, auto, cbv and tactics from isabelle like approximation and real_asymp

[Gabriel Ebner]

I'm not completely sure, but I believe the cc tactic in Lean 3 already expands the macro.

[Mario Carneiro]

The only things we should be migrating away from are tactics that are going to need to be rewritten in a different way in order to address issues in the original implementation; omega and finish come to mind

[Mario Carneiro]

but I would like us to have something that fits in roughly the same space in lean 4

[Eric Rodriguez]

afair, most omega uses got removed for now, so porting omega can be done later

[Patrick Massot]

I guess finish proofs are more common but we could very well get rid of them quickly.

[Patrick Massot]

Mario Carneiro said:

I'm hoping that we can also get things like super, auto, cbv and tactics from isabelle like approximation and real_asymp

Can you expand on "we can get"? Do you mean you intend to work on them? Or do you claim someone should do it?

[Mario Carneiro]

For me personally, it's a thing I would like to work on at some point but it's not a particularly high / short term priority. I would say it's just a few extra tactics on the list of ~100 tactics we need to write in lean 4

[Scott Morrison]

In fact, we don't use omega at all in mathlib now. I'm even tempted to drop it from mathlib in preparation for the port. (I realise the whole tactic directory isn't being automatically ported, so it's not actually "in the way".)

[Reid Barton]

That seems unnecessarily hostile to projects that depend on mathlib