I have defined a clone of polymorphic pairs which looks like:

```
Variables (H T : Type).
Inductive hash := Hash of T * H.
Definition pair_of_hash h := let: Hash th := h in th.
Canonical hash_subType := [newType for pair_of_hash].
```

and I would like to see it as an ordered type when applicable. In fact, I am only interested in the case when the two polymorphic parameters are countable types. How should I proceed?

Assia Mahboubi said:

I have defined a clone of polymorphic pairs which looks like:

`Variables (H T : Type). Inductive hash := Hash of T * H. Definition pair_of_hash h := let: Hash th := h in th. Canonical hash_subType := [newType for pair_of_hash].`

and I would like to see it as an ordered type when applicable. In fact, I am only interested in the case when the two polymorphic parameters are countable types. How should I proceed?

Like this:

```
From mathcomp Require Import all_ssreflect.
Import Order.Theory.
Section raw.
Variables (H T : Type).
Inductive hash := Hash of T * H.
Definition pair_of_hash h := let: Hash th := h in th.
Canonical hash_subType := [newType for pair_of_hash].
End raw.
Section eqType.
Variables (H T : eqType).
Definition hash_eqMixin := [eqMixin of hash H T by <:].
Canonical hash_eqType := EqType (hash H T) hash_eqMixin.
End eqType.
Section choiceType.
Variables (H T : choiceType).
Definition hash_choiceMixin := [choiceMixin of hash H T by <:].
Canonical hash_choiceType := ChoiceType (hash H T) hash_choiceMixin.
End choiceType.
Section porderedType.
Variables (H T : porderType tt).
Local Import DefaultProdOrder.
Definition hash_porderMixin := [porderMixin of hash H T by <:].
Canonical hash_porderType := POrderType tt (hash H T) hash_porderMixin.
End porderedType.
```

Note the subtly in the last section where I use a local import just before calling `[porderMixin of hash H T by <:].`

It's because cartesian products do not have a default canonical order, one must choose either generally, or locally, or using an alias, from "product order" or "lexicographic order". BTW using an alias another solution could be:

```
From mathcomp Require Import all_ssreflect.
Import Order.Theory.
Section raw.
Variables (H T : Type).
Inductive hash := Hash of T *p H.
(* the alias is here, `_ *p _` stands for cartesian product with "product order" *)
Definition pair_of_hash h := let: Hash th := h in th.
Canonical hash_subType := [newType for pair_of_hash].
End raw.
Section eqType.
Variables (H T : eqType).
Definition hash_eqMixin := [eqMixin of hash H T by <:].
Canonical hash_eqType := EqType (hash H T) hash_eqMixin.
End eqType.
Section choiceType.
Variables (H T : choiceType).
Definition hash_choiceMixin := [choiceMixin of hash H T by <:].
Canonical hash_choiceType := ChoiceType (hash H T) hash_choiceMixin.
End choiceType.
Section porderedType.
Variables (H T : porderType tt).
(* no need to import the default ordering on products anymore *)
Definition hash_porderMixin := [porderMixin of hash H T by <:].
Canonical hash_porderType := POrderType tt (hash H T) hash_porderMixin.
End porderedType.
```

Last updated: Jul 25 2024 at 16:02 UTC