Stream: math-comp users

Topic: ✔ Implement lexical order


view this post on Zulip Léon Ducruet (Jun 22 2022 at 08:15):

Given two partially ordered types T and tr, I would like to implement a lexical order on T * tr. This seems not to be the right way.

From mathcomp Require Import all_ssreflect.

Import DefaultProdLexiOrder.

Section sandbox.

Variable (tr : choiceType).

Variable (T : finType).

Variable tr_o : leOrderMixin tr.

Variable T_o : leOrderMixin T.

Canonical tr_orderType := POrderType Order.lexi_display tr tr_o.

Canonical T_orderType := POrderType Order.lexi_display T T_o.

Variable tr1 : tr.

Variables t1 t2 : T.

Check (((tr1, t1): tr *l T) < ((tr1, t2): tr *l T))%O.

What can I do ? What is missing ?

view this post on Zulip Cyril Cohen (Jun 22 2022 at 09:26):

Oh I see... well... The answer is structures do not compose that way (that's why in Hierarchy Builder (HB) we introduced the command HB.context). You cannot have a structure and "add stuff". Either you start with "full structures" as in:

Variables (tr : porderType tt) (T : finPOrderType tt).
Variables (tr1 : tr) (t1 t2 : T).
Check ((tr1, t1) < (tr1, t2))%O.

Or with "naked types" and build your way up like this:

Variables (tr T : Type).

Variable tr_choice : Choice.class_of tr.
Canonical tr_eqType := EqType tr tr_choice.
Canonical tr_choiceType := ChoiceType tr (Choice.mixin tr_choice).
Variable tr_o : leOrderMixin [choiceType of tr].
Canonical tr_orderType := POrderType tt tr tr_o.

Variable T_fin : Finite.class_of T.
Canonical T_eqType := EqType T T_fin.
Canonical T_choiceType := ChoiceType T (Choice.mixin T_fin).
Canonical T_countType := CountType T T_fin.
Canonical T_finType := FinType T T_fin.
Variable T_o : leOrderMixin [choiceType of T].
Canonical T_orderType := POrderType tt T T_o.

Variables (tr1 : tr) (t1 t2 : T).

Check ((tr1, t1) < (tr1, t2))%O.

The later is obviously very tedious and fortunately automated by HB in the future

view this post on Zulip Notification Bot (Jun 22 2022 at 09:40):

Léon Ducruet has marked this topic as resolved.


Last updated: Jul 25 2024 at 16:02 UTC