## Stream: math-comp users

### Topic: Transfer of structure for ordered types

#### Assia Mahboubi (Jul 25 2022 at 15:45):

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?

#### Cyril Cohen (Jul 26 2022 at 09:36):

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.
``````

#### Cyril Cohen (Jul 26 2022 at 09:38):

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: Jan 29 2023 at 19:02 UTC