Closed Alizter closed 6 months ago
@JasonGross Do you know how to get coq to unify something like this?
Have you tried making a notation with literally that body? If that doesn't work, you can do something like
Notation "a '@lr' b" := (match _, _ return _ with X1, Y1 => cu_concat_lr a b (sji0:=X1) (sji1:=X1) (sj0i:=Y1) (sj1i:=Y1) (pj11:=1) end) (only parsing).
(Or a slightly different version of the notation)
If you're asking about hinting implicits with existing notations, the only way you can do that is with type annotations of explicit variables. If that's not powerful enough, you need to make a new notation.
@JasonGross That's an interesting solution but I am worried I am being too restrictive with the notation. It's not really a problem with the notation but with the definition of cu_concat_lr
. I am wondering if I can hint to coq which implicit parameters to choose when it is refining this.
I don't understand. If you could make your own syntax for what you want and give it your own semantics, what would it look like and what would it do?
@JasonGross if you pop over to TorusEquivCircles.v and stick in refine ((sq_ap2_compose c2t' t2c loop loop) @lr _).
right after 1,2,3,4: exact (eisretr _ _)^.
in c2t2c
it doesn't work. Even if we redefine @lr
to be as you said above.
This is why I have to explicitly tell coq which parameters are the same etc. I am wondering if coq can do this automatically?
The notation @lr
is not really important it is just an alias for cu_concat_lr
.
This is a shortcoming of Coq's unification and belongs as a feature request upstream. From my time helping develop Coq, I can say that making something like this work is not easy to do as tweaking unification has a lot of breakages etc. Therefore I wouldn't think it would be a priority.
So in
Spaces/Torus/TorusEquivCircles.v
, I ran into the following problem with coq's unification, which you can find in the code below.Am I able to somehow hint to coq that when I write
refine (a @lr _).
, I want it to act asrefine (cu_concat_lr a _ (sji0:=?[X1]) (sji1:=?X1) (sj0i:=?[Y1]) (sj1i:=?Y1) (pj11:=1)).
?Explicitly hinting with existential variables works but it makes it a lot scarier and harder to read than it actually is.