Assia Mahboubi (Jul 25 2022 at 15:45): 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.
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: Apr 19 2024 at 09:01 UTC