Get coq to unify cube concatenation

[Alizter]

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 as refine (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.

  (* We now prove that t2c is a section of c2t *)
  Definition t2c2t : Sect t2c c2t.
  Proof.
    unfold Sect.
    (* We start with Torus induction *)
    refine (Torus_ind _ 1 _ _ _).
    (* Our DSquare is really just a cube *)
    apply cu_ds^-1.
    (* We pretend that our sides have sq_dpath o sq_dpath^-1
      and get rid of them *)
    refine (cu_GGGGcc (eisretr _ _)^ (eisretr _ _)^
      (eisretr _ _)^ (eisretr _ _)^ _).
    (* Apply a symmetry to get the faces on the right side *)
    apply cu_rot_tb_fb.
    (* Clean up other faces *)
    refine (cu_ccGGGG (eisretr _ _)^ (eisretr _ _)^
      (eisretr _ _)^ (eisretr _ _)^ _).
    (* Now we finish the proof with the following composition of cubes *)
    refine ((sq_ap_compose t2c c2t surf)
      @lr (cu_ap c2t (Torus_rec_beta_surf _ _ _ _ _ ))
      @lr (sq_ap_uncurry _ _ _)
      @lr (pr2 (pr2 c2t'_beta))
      @lr (cu_flip_lr (sq_ap_idmap _))).
  Defined.

  (* NOTE: The last step in the previous proof can be done as a sequence of
     refines however coq really struggles to unify this. Below is the original
     way we proved the last statement before making it short and sweet. As can
     be seen, we need to give refine hints using existential variables which is
     tedious to write out, and perhaps motivates why we wrote it as one big
     concatenation. Ideally the way below should be as smooth as the way above,
     since above is difficult to write directly without having tried below.

    (* Now we decompose the cube with middle sq_ap_compose *)
    (* Note: coq sucks at unifying this so we have to explicitly give paths *)
    refine (cu_concat_lr (sq_ap_compose t2c c2t surf) _
      (sji0:=?[X1]) (sji1:=?X1) (sj0i:=?[Y1]) (sj1i:=?Y1) (pj11:=1)).
    (* Now we reduce (sq_ap t2c surf) *)
    refine (cu_concat_lr (cu_ap c2t (Torus_rec_beta_surf _ _ _ _ _ )) _
      (sji0:=?[X2]) (sji1:=?X2) (sj0i:=?[Y2]) (sj1i:=?Y2) (pj11:=1)).
    (* We now uncurry c2t inside sq_ap *)
    refine (cu_concat_lr (sq_ap_uncurry _ _ _) _
      (sji0:=?[X3]) (sji1:=?X3) (sj0i:=?[Y3]) (sj1i:=?Y3) (pj11:=1)).
    (* Reduce sq_ap2 c2t' loop loop *)
    refine (cu_concat_lr (pr2 (pr2 c2t'_beta)) _
      (sji0:=?[X4]) (sji1:=?X4) (sj0i:=?[Y4]) (sj1i:=?Y4) (pj11:=1)).
    (* Finally flip and sq_ap idmap *)
    refine (cu_flip_lr (sq_ap_idmap _)).

  *)

[Alizter]

@JasonGross Do you know how to get coq to unify something like this?

[JasonGross]

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.

[Alizter]

@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.

[JasonGross]

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?

[Alizter]

@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.

[Alizter]

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.