New, much easier algorithm for characterizing path types#1112
Merged
Conversation
Collaborator
|
Can you run Jason's timing scripts to see if there is an improvement? |
Collaborator
|
I am a bit worried about changing some record types to sigmas but other than that it looks really good. I am especially pleased with definitional behaviour of path_pmap. :-) As I understood it, the reason we use record types is when coq unfolds these terms in its unification algorithm, record types are better behaved whereas sigma types have a lot of useless junk too. This leads to a noticeable performance hit. I imagine it won't make much difference for a 2 component sigma type but for something big like Factorization it might. But I don't really know, I am speculating. LGTM. |
Alizter
reviewed
Oct 26, 2019
| Definition path_pmap `{Funext} {A B : pType} {f g : A ->* B} | ||
| : (f ==* g) -> (f = g) := equiv_path_pmap f g. | ||
|
|
||
| (* We note that the inverse of [path_pmap] computes definitionally on reflexivity, and hence [path_pmap] itself computes typally so. *) |
Collaborator
There was a problem hiding this comment.
what does "typally" mean?
Contributor
Author
|
I'll run the timing checks. Sorry, it's been a while since i've done that, I have to remember how... Two things are "typally" equal if their identity type is inhabited (the contrast to "definitionally" or "judgmentally"). The old word for this was "propositionally", but in HoTT that's misleading because the identity type may not be a proposition. |
Contributor
Author
|
We could of course put the |
Collaborator
|
@mikeshulman I was under the impression that this issig proofs were judgemental. I might experiment with them later to see if the library becomes more performant when using records. I have near no idea what I am talking about however, so it might be better to ask @JasonGross. Regarding "typally". I have heard "typically" typically being used before, but this is obviously very silly. In the context of HoTT, I would simply settle for "equal". Also if it is too much bother, I can do the time checks since I recently messed around with them. |
Contributor
Author
|
I just meant that applying the issigs inside the path equivalence proofs is annoying. But maybe I can write a lemma or tactic that does it for us. The problem with just "equal" is that definitional equality is also a kind of "equal". Normally it's enough to just say "equal", but if you need to emphasize that what you mean is typal equality rather than definitional equality, it's helpful to have a word. |
Member
|
Looks good. Aside, we could potentially use meta-coq to program tactics about records and Sigma types. At that level we have full control. I believe this was once suggested by @mattam82 |
Collaborator
|
The dream solution would be to have sigma types being as good as record types. And when defining a record what we should really doing is syntactic sugar for nested sigmas and their projections. |
Member
|
Records are just macros. However, we don't have access to this in Gallina,
but we do have access to this at the meta-coq level.
https://coq.inria.fr/refman/language/gallina-extensions.html
…On Sat, Oct 26, 2019 at 2:10 PM Ali Caglayan ***@***.***> wrote:
The dream solution would be to have sigma types being as good as record
types. And when defining a record what we should really doing is syntactic
sugar for nested sigmas and their projections.
—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
<#1112>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AABTNTSYMNJFFPXDRFLPVSLQQQXSDANCNFSM4JFMBL5A>
.
|
Contributor
Author
|
I reverted things to records, with another tactic in |
Member
|
LGTM |
Collaborator
|
@mikeshulman The new issig in #1106 can automatically derive the correct issig statement and prove it. What we would then want is something like |
Alizter
approved these changes
Oct 27, 2019
Collaborator
Alizter
left a comment
Alizter
left a comment
There was a problem hiding this comment.
LGTM I will see about timing this later today.
Member
|
Wouldn't Equations be helpful in that style?
…On Sun, Oct 27, 2019 at 2:28 PM Ali Caglayan ***@***.***> wrote:
@mikeshulman <https://github.com/mikeshulman> The new issig in #1106
<#1106> can automatically derive the
correct issig statement and prove it. What we would then want is something
like refine ((ap _^-1 _)^-1 _) which would then have a hole for an
equivalence which we will provide with issig. This would let us turn A = B
into sigA = sigB where A and B are records and sigA and sigB are the
expected sigma types. The refine might not work exactly right now since it
cannot infer that _^-1 needs to be filled with an equivalence, but rather
it will infer that it needs a function that happens to be IsEquiv.
—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
<#1112>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AABTNTQKWU533J57YAKUU5LQQWCNHANCNFSM4JFMBL5A>
.
|
Collaborator
|
@spitters I am not sure what you mean. I thought Equations really helped when we had complicated match statements. Here I was just describing how to turn a path of records into a path of sigmas, i.e. how one might write such a tactic. Unless you were talking about something else? |
Member
|
It's also a general way of writing agda style proofs.
However, you are right, it might be overkill here.
…On Sun, Oct 27, 2019 at 2:43 PM Ali Caglayan ***@***.***> wrote:
@spitters <https://github.com/spitters> I am not sure what you mean. I
thought Equations really helped when we had complicated match statements.
Here I was just describing how to turn a path of records into a path of
sigmas, i.e. how one might write such a tactic. Unless you were talking
about something else?
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#1112>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AABTNTQ3DLNLF6H7CQL5K6DQQWEHFANCNFSM4JFMBL5A>
.
|
Collaborator
|
Here is the timing data before Mike changed the sigmas back to records: Timing data with sigma types
As you can see it is significantly slower, especially in Idempotents. Here is the timing data after Mike changed the sigmas back to records: Timing data with records
As you can see, this means there is very little change in the library when using the new path_pmap. I would say that this is mostly a success. I think there are still some optimizations to be made with the new tactics in PathAny. Notably Pointed.pMap is taking a bit longer. After experimenting a bit, I suggest we change the tactic Ltac eqp_issig_contr e :=
match goal with
| [ |- ?X <~> ?x = ?y ] => revert x y
| _ => idtac
end;
let x := fresh in
let y := fresh in
equiv_intro e x;
equiv_intro e y;
refine ((equiv_ap' e^-1 _ _)^-1 oE _);
revert x y;
match goal with
[ |- forall x y, @?P x y <~> ?eq ] =>
notypeclasses refine (equiv_path_from_contr P)
end.All I did was put notypeclasses infront of the final refine. This stops coq from searching for Reflexivity. Currently, the only use of this tactic has reflexivity manually supplied. Coq is therefore wasting time here. Other than this it all looks good. I imagine some more documentation on these new tactics would be beneficial too. |
Contributor
Author
|
I went ahead and just changed the |
Collaborator
|
@mikeshulman I couldn't manage to speed that up. I suspect that unification of sigmas is causing the problem but I can't be sure. I wonder if explicitly giving the contr hyothesis will allows typeclass search to pick it up faster. I would test this but currently I am trying to update my version of coq which is taking longer than expected. |
Collaborator
Contributor
Author
|
I heard two LGTMs so I'm going to merge this. Then I'll see about combining the tactics on top of #1106. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Wow! I just learned this from Egbert. Those gigantic transport calculations using obscure lemmas in
FactorizationandIdempotent? Gone! Also solves #1111 .