Further cleanup of Init.Logic

Stream: PR reviews

[Jeremy Tan]

#16691 moves ExistsUnique and Xor' out of Init.Logic.

#16692 deprecates if_congr, dif_ctx_congr and if_ctx_congr, lemmas that were still used in mathlib at the time of the first deprecation.

[Kim Morrison]

I don't understand the motivation of #16692. Why do you want to do that?

[Kim Morrison]

Johan 'd #16691

[Jeremy Tan]

Kim Morrison said:

I don't understand the motivation of #16692. Why do you want to do that?

Those three lemmas are only used a few times and can all be replaced out by core tactics

[Johan Commelin]

I conjecture there are > 1000 lemmas with that property

[Johan Commelin]

If the diff is negative, then that seems like a fine argument. But proofs are getting longer in your diff.

[Violeta Hernández]

if_congr seems highly reasonable to me, I can imagine using it in place of having to call split_ifs

[Violeta Hernández]

I could agree with getting rid of if_ctx_congr on account of how specific it is, iff there's a clear improvement in removing it from existing proofs

[Jeremy Tan]

Johan Commelin said:

If the diff is negative, then that seems like a fine argument. But proofs are getting longer in your diff.

I pushed a better idea. Deprecate only dif_ctx_congr and move the other two lemmas to Logic.Basic too

[Kim Morrison]

Thanks, 'd.

[Jeremy Tan]

@Kim Morrison it was rejected by the awaiting-CI label, can you merge again?

[Jeremy Tan]

#16698 deprecates everything in Init.Algebra.Classes except one class – IsSymmOp, which generalises IsSymm and Std.Commutative

In Init.Logic though there are "very unbundled" versions of order typeclasses that seem like duplicates – Symmetric for IsSymm, Reflexive for IsRefl, etc. What do I do with them?

[Jeremy Tan]

And where could I move IsSymmOp to? (It still has some uses as a typeclass in mathlib.)

[Kim Morrison]

Let's just move IsSymmOp to Mathlib.Logic.IsSymmOp (a new file).

[Johan Commelin]

@Jeremy Tan If Symmetric is really a duplicate of IsSymm, then let's deprecate it.

[Jeremy Tan]

#16721 deprecates 14 Init.Logic lemmas that are essentially duplicates

[Jeremy Tan]

My next planned PR will put IsSymmOp, IsLeftCommutative and IsRightCommutative in one new file, thereby completely deprecating Init.Algebra.Classes

[Johan Commelin]

Jeremy Tan said:

#16721 deprecates 14 Init.Logic lemmas that are essentially duplicates

Nice!
I assume you generated most of the diff using search-replace? Or maybe sed?
Can you please indicate the 14 replacements in the PR commit message?

[Jeremy Tan]

Johan Commelin said:

Jeremy Tan said:

#16721 deprecates 14 Init.Logic lemmas that are essentially duplicates

Nice!
I assume you generated most of the diff using search-replace? Or maybe sed?
Can you please indicate the 14 replacements in the PR commit message?

Search-replace, yes. I have indicated the 14 in the PR desc

[Johan Commelin]

Hmm, do the old lemmas still exist? It's hard to find them in the diff.

[Johan Commelin]

Aaah, I found them!

[Johan Commelin]

In the future, please add the @[deprecated] in a separate commit. That makes reviewing a bit easier.

[Johan Commelin]

[Jeremy Tan]

#16749 deprecates un-namespaced Commutative, Associative in Init.Logic in favour of the Std-namespaced counterparts

[Jeremy Tan]

#16751 upgrades (Left|Right)Commutative into typeclasses, in preparation for the move of them and IsSymmOp (collectively called the heteroclasses) in #16748

[Jeremy Tan]

What would be a better name than Logic.Heteroclasses for the new file containing IsSymmOp, LeftCommutative and RightCommutative?

[Jeremy Tan]

(in branch#tidy-logic I am going to do a bunch of smaller deprecations of unused or almost-unused declarations, move out the definition EmptyRelation, and conform IsSymmOp to the new typeclasses of #16751, i.e. make its α andβ implicit rather than the current explicit)

[Yaël Dillies]

What about Logic.OpClass/Logic.RelClass?

[Jeremy Tan]

Jeremy Tan said:

(in branch#tidy-logic I am going to do a bunch of smaller deprecations of unused or almost-unused declarations, move out the definition EmptyRelation, and conform IsSymmOp to the new typeclasses of #16751, i.e. make its α andβ implicit rather than the current explicit)

This is now #16757

[Jeremy Tan]

Yaël Dillies said:

What about Logic.OpClass/Logic.RelClass?

I will go with Logic.OpClass

[Jeremy Tan]

lean4#5329 upstreams the @[refl] attribute on Iff.refl

[Jeremy Tan]

…and the core PR is merged. Still got the two mathlib ones

[Violeta Hernández]

Jeremy Tan said:

lean4#5329 upstreams the @[refl] attribute on Iff.refl

Whoa, that's something I never knew I was missing

[Kim Morrison]

(There was an alternate mechanism, which this attribute replaces.)

[Jeremy Tan]

I can see the end right now. #16748 does the move to Logic.OpClass as described above, and in one final Mathlib.Init cleanup PR I will move the six undeprecated relation definitions and the trans attributes to Order.Defs and Logic.Basic respectively

[Jeremy Tan]

And then there will be none – Mathlib.Init will be entirely deprecated

[Jeremy Tan]

Jeremy Tan said:

and in one final Mathlib.Init cleanup PR I will move the six undeprecated relation definitions and the trans attributes to Order.Defs and Logic.Basic respectively

This PR is #16796

[Jeremy Tan]

also #16748 is ready for review

[Jeremy Tan]

#16796 – the last one – now passes CI.

I have taken this opportunity to also remove the [refl] attribute on Iff.refl, since that has been upstreamed. Only one line elsewhere needs to be changed in current mathlib for this attribute removal