Ssreflect Users Discussion List

[Florent Hivert <>]

      Hi there,

Suppose that I have a type T and a structure S for which T has two different
S-structure S1 S2. My practical use case is the following: I'm writing various
structures for ordered sets (partially or totally, countable, finite ...), and
there may be several natural order on a given set.  As an example, there is a
canonical order on nat's, but there are two natural one on OT1 + OT2 for OT1
and OT2 ordered types:

- the disjoint union where x1 in OT1 and x2 in OT2 are never comparable. This
  is only a partial order;
- the ordered sum where x1 <= x2 if x1 in OT1 and x2 in OT2. This is total
  provided OT1 and OT2 are totally ordered.

Depending on the context, I need to consider S1 or S2 as canonical in Coq
sense though they aren't in the mathematical sense. I'm currently using the
following construct:

Module S1Can.
Canonical T_S := ...
End S1Can.

Module S2Can.
Canonical T_S := ...
End S2Can.

And then assuming there is a lemma Foo on S structure, inside a proof I'm
allowed to write:

apply (Foo (T := S1Can.T_S)).

I'm also allowed to Import S1can or S2can when needed.

My questions are the following: as someone ever experimented with this
construct ? Is this robust ? Are there any better alternatives ?

Cheers,

Florent