Generalize lhs, lhs_V, rhs and rhs_V to all transitive relations about coq-hott

[Alizter]

I experimented with this a bit:

Tactic Notation "lhs" tactic3(tac) :=
  let R := match goal with |- ?R _ _ => constr:(R) end in 
  let pre_transitivity_proof_term_head := constr:(_ : Transitive R) in
  let transitivity_proof_term_head := (eval hnf in pre_transitivity_proof_term_head) in
  nrefine (pre_transitivity_proof_term_head _ _ _ ltac:(tac) _).

It didn't work out too well for the following reasons:

1. Doing a typeclass search every time is a lot of wasted work.
2. In some situations we implicitly assume that the goal will resolve to paths.
3. The universe levels cause unification issues.
4. The proof terms are a bit more complex.

My next suggestion would be to hard code the transitivity proofs for each kind of relation we want this to work on in order to solve (1) but then we get stuck on (2).

(3) is really tricky to understand when things go wrong.

(4) isn't great as Coq spends more and more time unfolding terms that it shouldn't need to.

We could instead introduce variants of lhs like lhsE for Equiv, lhsC` for wildcat etc. That way we wouldn't have issues 1-4, however then we would have even more tactics.

[jdchristensen]

Can you explain more?

1. I would assume that the typeclass search should be very fast, since in every case where we would use this, the instance should be obvious.
2. I don't understand what you mean here.
3. Can you give an example? Why are there universe issues with this?
4. Can you give an example? It looks to me like it should give a very similar proof term.