new and improved issig#1106
Conversation
JasonGross
left a comment
JasonGross
left a comment
There was a problem hiding this comment.
Thanks for putting this together!
|
Btw, if you're not going to add the extensive documentation, it might be worth putting a link to #1093 (comment) in the commit message itself (or even in the comments in the file), so it's easier to find that explanation by looking through git history. |
|
And the collapsible timing is very cool, I'm going to have to start using that when I report timing diffs |
|
What about adding Record.v as a file in Basics.v. Since it is used all over the library, I don't see any need to have to import it when needed. |
|
It would be preferable to copy the explanation from the #1093 comment into the comments in the file, so that it stands on its own without forcing people to follow a link to a github discussion.
Isn't it already exported by |
|
@mikeshulman This is true. The issue here is that we want to move issig into Tactics.v. To do this we will need to move the lemmas issig_contr somewhere else. It would make more sense to me if we defined issig in Basics and use it everywhere else. At the moment it doesn't really make sense that we have to import types in order to have issig_contr. It should be noted that Types.Record only relies on Basics.Overture. I am not really sure it needs to be in Types anymore. |
|
Ah, I see. Yes, I could see putting |
|
Here is a test case for a big record: Record Diagram3x3 : Type := {
A00 : Type; A02 : Type; A04 : Type;
A20 : Type; A22 : Type; A24 : Type;
A40 : Type; A42 : Type; A44 : Type;
f01 : A02 -> A00; f03 : A02 -> A04;
f10 : A20 -> A00; f12 : A22 -> A02; f14 : A24 -> A04;
f21 : A22 -> A20; f23 : A22 -> A24;
f30 : A20 -> A40; f32 : A22 -> A42; f34 : A24 -> A44;
f41 : A42 -> A40; f43 : A42 -> A44;
H11 : f01 o f12 == f10 o f21; H13 : f03 o f12 == f14 o f23;
H31 : f41 o f32 == f30 o f21; H33 : f43 o f32 == f34 o f23;
}.Currently if we issig this with Definition issig_Diagram3x3 : _ <~> Diagram3x3 := ltac:(issig).We get an error since ntc_rapply doesn't nearly go high enough. Here is a version which you can replace in basics that does: (* An alternative version of [rapply] using [notypeclasses refine]. *)
Local Ltac ntc_rapply p :=
ntc_refine p ||
ntc_refine (p _) ||
ntc_refine (p _ _) ||
ntc_refine (p _ _ _) ||
ntc_refine (p _ _ _ _) ||
ntc_refine (p _ _ _ _ _) ||
ntc_refine (p _ _ _ _ _ _) ||
ntc_refine (p _ _ _ _ _ _ _) ||
ntc_refine (p _ _ _ _ _ _ _ _) ||
ntc_refine (p _ _ _ _ _ _ _ _ _) ||
ntc_refine (p _ _ _ _ _ _ _ _ _ _) ||
ntc_refine (p _ _ _ _ _ _ _ _ _ _ _) ||
ntc_refine (p _ _ _ _ _ _ _ _ _ _ _ _) ||
ntc_refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
ntc_refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
ntc_refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
ntc_refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
ntc_refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
ntc_refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
ntc_refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
ntc_refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
ntc_refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
ntc_refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
ntc_refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
ntc_refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
ntc_refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
ntc_refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _).This goes up to 25 arguments which is needed. Even now, issig takes a few minutes to complete. @JasonGross Is this slowdown because of the sigma type problem or something to do with the tactic? Also is there a better way to have a variable number of underscores? In the coq library, rapply is defined the same way. If we could somehow test the arity of a function and then start with that many underscores and slowly reduce them, we might have a better tactic? Maybe we could write a recursive tactic where |
|
I have a PR waiting to be merged which generalizes rapply: rocq-prover/rocq#10760 Feel free to replace all of our tactics with variants of that (you may need to copy over As for performance, you can try |
|
@JasonGross Thanks for letting me know about your PR. I will experiment with adding it to the HoTT library later. When I use Which is fine because it shows up every time there is a branch. Since it is waiting so long after each message, I can deduce that it is indeed the nested sigma types causing the trouble. I suppose coq is spending a lot of time unwrapping these massive sigma terms for unification. I wonder if there are any optimizations that can be made here. I don't quite understand what you mean by explicitly sharing let binders however. |
|
What's the status of this? |
|
@mikeshulman I will rebase tomorrow. I need to fix a conflict in idempotents but I don't have time tonight. Also @JasonGross are you happy with this currently or did you still want more documentation? |
|
@mikeshulman I rebased and updated STYLE.md. I will await confirmation from @JasonGross or anybody else before we merge. |
|
Rebased |
|
OK waiting for someone else to review then we can merge. |
|
@JasonGross @andreaslyn @spitters anyone else able to review? |
4 participants
Here is the new issig tactic from #1093.
Here are the biggest timing changes. As you can see it is near negligible. I may have even moved the mouse around a bit which may account for some of the changes.
Timing (Click me to open)
Check this out if you want to see how I managed the above text with markdown inside.
The changes can be summarized as follows: Any lemma using the old issig tactic now uses the new issig tactic. Only
ua_isomorphic.vbecame broken after doing this, and I went ahead and changed the broken proof to use a cleaner lemma instead of failing to destruct something.The new tactic looks a bit complicated but this is because it has many helper lemmas. The way it guesses the constructor of a record used to be with
econstructor, however this resolves typeclasses which means it didn't work forua_isomorphic.vin particular. Jason went ahead and wrote a version ofserapplythat usesnotypeclasses refineinstead. That way he managed to write a version ofeconstructorthat doesn't use typeclasses.I've tried to document how the tactic works, but I can probably do better. Jason described it in great detail in #1093.
This closes #1097.