Support Trakt-like declarations for goal pre-processing

[palmskog]

In a typical use of Trakt, the user can relatively easily declare "partial isomorphisms" for goal transfers, such as that nat to Z for all x >= 0. This allows preprocessing goals on nat to become goals on Z that include the >= 0 constraint.

With Trocq, the same transfer can be done by declaring nat as parametrically related to Z at some appropriate level of the Trocq hierarchy by, e.g., defining a Coq record with the following fields:

R : nat -> {z : Z & z >= 0} -> Type
map : nat -> {z : Z & z >= 0}
map_in_R : forall (n : nat) (z : {z : Z & z >= 0}), map n = z -> R n z
comap : {z : Z & z >= 0} -> nat
R_in_comap : forall (z : {z : Z & z >= 0}) (n : nat), R n z -> comap z = n

Even with this witness accepted by Trocq, the user still needs to do custom ad-hoc post-processing to get the Zs out from the sigma types and get goals equivalent to Trakt.

It would be nice if Trocq could provide a Trakt-like command Isomorphism A B record that turns a declaration into the right Trocq witness in the hierarchy and enables goal transfer post-processing.

Credit to @ecranceMERCE for the technical details here which I think should be preserved as useful in future work.

[CohenCyril]

@palmskog Trocq is currently missing a user interface overall (not just Isomorphism). I will try to list the API I had in mind from our meetings with @amahboubi and @ecranceMERCE, ASAP, so that we can discuss it altogether. Thank you for contributing this piece of the API.

[palmskog]

Sounds good. For full transparency, one of my motivating examples is this issue:

One way to improve the success rate on mathcomp problems could be to preprocess mathcomp goals into a form which CoqHammer can handle better. This wouldn't actually require much modification of CoqHammer itself.