Examples of CoqEAL style refinement

[palmskog]

From what I can tell from the paper and examples directory in the repo, nearly all examples are about proof transfer for isomorphisms/equality. Or are there any Trocq-based examples lying around somewhere for CoqEAL style refinement based on partial quotient refinement relations, where the target type has "more elements" than the source type?

[CohenCyril]

Hi @palmskog indeed there are no examples of CoqEAL style refinement stricto sensu, however both https://github.com/coq-community/trocq/blob/master/examples/nat_ind.v and https://github.com/coq-community/trocq/blob/master/examples/flt3_step.v feature examples which are not iso, and although we could have performed transfer of ground terms to achieve enhanced computation à la CoqEAL, we chose to show we support transfer of more intricate statements.
At some point "we" should work towards porting CoqEAL to trocq indeed.

[palmskog]

For the record, I think a Trocq port of the rational number refinement example from the CoqEAL paper would be nice, and also demonstrate to observers that Trocq has these refinement capabilities. If a spare moment to do this shows up and nobody beats me to it, I will make a PR.