LinearAlgebra.Quotient !4#2286

Stream: mathlib4

[Jireh Loreaux]

This file is also unimaginably slow (cf. https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/linear_algebra.2Efinsupp.20!4.232277). It's having trouble (slow, but successful) with rfl proofs. I haven't investigated much yet.

[Jireh Loreaux]

I managed to finish this (i.e., it builds and lints), but there are a few issues I think still need to be addressed:

1. Adding type ascriptions to mk or mk x and friends greatly speeds up elaboration issues. (this is just for your information and fixes the rfl issues mentioned above)
2. What is the proper casing convention for mkq or liftq (and variants). Is is mkq, or mkQ?
3. How should submodule.comap_mkq.rel_iso be called according to our naming conventions?
4. Why can't Lean fill in optParams automatically in simp or rw? (This is super inconvenient)
5. Why did I need to add an optParam in Submodule.Quotient.equiv_apply that wasn't needed in Lean 3, and why didn't simps generate this lemma?
6. There are some instances I feel like we may want to be default_instances, but I'm not sure.

[Johan Commelin]

Re2: I would prefer mkq and liftq.
Re3: The current name Submodule.ComapMkq.relIso looks good to me.

[Jireh Loreaux]

Sorry, Johan, just to confirm about 3: you realize that there is no def called comapMkq, right? It's just comap_mkq, which is a proof of some prop.

[Johan Commelin]

hmm... ok, now I'm in doubt again what the naming convention wants...

[Jireh Loreaux]

Yeah, this seems like an edge case. I think my feeling is that the name is just entirely wrong (even in Lean 3). I think it should be something like Submodule.comapMkqRelIso or RelIso.submoduleComapMkq. I don't htink there is any reason for a secondary namespace.

[Thomas Murrills]

Re: 2, I think it “should” be mkQ and liftQ, since q is an abbreviation for a different word (make + quotient) so there’s a casing boundary. We write things like getI and mapM, and this is of the same form. But, if they’re very widely used names prior to this file and are sufficiently lexicalized into their own thing, like foldr and [other prominent example I’m not thinking of], I think mkq, liftq is fine—but I can’t speak to whether that’s really the case.

My tentative guess is they’re not though…if that’s true, then the liftQ case is pretty unambiguous imo, and I think there’s a strong case for mkQ.

[Johan Commelin]

@Mario Carneiro do you know what's going on with item 4+5 above?

[Mario Carneiro]

simp and rw have never inferred optional parameters

[Johan Commelin]

So in Lean 3 this was also fake?

[Mario Carneiro]

?

[Mario Carneiro]

I guess I don't know the context here

[Mario Carneiro]

I agree with thomas re: mkQ and liftQ, those look more consistent with the rest of the naming convention to me

[Johan Commelin]

https://github.com/leanprover-community/mathlib4/pull/2286/files/78a7161fdd8dd5b3edeb145628f7cdec5c92a088..ca4ff42c2c4e133e8bf69c6710619ffe3261cf65#diff-231484eaa15206e44d62480604548dfef568324265aba7d3b34a6c1affdb42bbR454-R459 suggests that Lean 3 was smarter than Lean 4. But maybe for different reasons.

[Mario Carneiro]

the proof looks rather different. In the first version you wouldn't even need the optParam in mapq_comp (which is not even being passed to simp?) since everything is determined by unification

[Jireh Loreaux]

Sorry, I missed a place where I should have put a porting note. You're right that that proof looks quite different. A better example of the way Lean 4 is failing in comparison to Lean 3 is here: https://github.com/leanprover-community/mathlib4/pull/2286/files/78a7161fdd8dd5b3edeb145628f7cdec5c92a088..ca4ff42c2c4e133e8bf69c6710619ffe3261cf65#diff-231484eaa15206e44d62480604548dfef568324265aba7d3b34a6c1affdb42bbR576-R586

[Jireh Loreaux]

Regarding naming, I have renamed mkq, liftq and mapq to mkQ, liftQ and mapQ. In addition, I have made Submodule.ComapMkq.relIso into Submodule.comapMkQRelIso and Submodule.ComapMkq.orderEmbedding into Submodule.ComapMkQOrderEmbedding Since there isn't really any reason for the extra namespace.

[Johan Commelin]

@Jireh Loreaux I think most of your points have been addressed. Could you please update the top comment on the PR page? Which questions remain?

[Jireh Loreaux]

I've updated the PR comment. Basically, I still don't know why simp and rw need so much information in Lean 4 as compared to Lean 3 in the diff I linked above. I've encountered this kind of thing before in porting, and every time it's a royal pain. I think anything with quotients will only make it worse.

But if you want to merge the PR so we can proceed, that's fine.

[Johan Commelin]

Thanks!