Stream: math-comp users

Topic: Linking order.v and 'I_n


view this post on Zulip Pierre Jouvelot (Nov 29 2023 at 22:15):

I'm trying to use a simple ordinal as an orderType (using 8.17 and 1.17). The following attempt fails:

From mathcomp Require Import all_ssreflect all_fingroup.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import Order.Theory.

Open Scope order_scope.

Definition f : forall (T : orderType tt), T -> seq T -> seq T := fun T t0 b => t0 :: b.

Definition x := (@f 'I_2 (@ord0 1) [::]).

What should I be doing instead?

view this post on Zulip Quentin VERMANDE (Nov 30 2023 at 07:43):

The canonical structure is in Order.OrdinalOrder.Exports, so you need to import this module. You will need to generalize the display parameter of orderType (as in f : forall (d : unit) (T : orderType d) ...) since ordinals have their own custom display parameter. Lastly, you may have to leave the implicit arguments of f uninstanciated (it is at least the case with coq 8.15.2 and mathcomp 1.15).

view this post on Zulip Pierre Roux (Nov 30 2023 at 07:48):

Quentin VERMANDE said:

The canonical structure is in Order.OrdinalOrder.Exports, so you need to import this module.

Given the name, I would have expected the module to be already exported in order.v.

view this post on Zulip Quentin VERMANDE (Nov 30 2023 at 07:50):

On the mathcomp-1 branch, it is (in order.v l.8745), so I am also surprised.

view this post on Zulip Quentin VERMANDE (Nov 30 2023 at 07:59):

Ah, no it works, I did the debugging in the wrong order. Generalizing the display parameter in the definition of f and removing the implicit argument when using it suffices, there is no need to import Order.OrdinalOrder.Exports. Thanks [at]Pierre Roux.

view this post on Zulip Pierre Jouvelot (Nov 30 2023 at 08:59):

Thanks a lot @Quentin VERMANDE @Pierre Roux . For the record, this indeed works:

Definition f : forall (d : unit) (T : orderType d), T -> seq T -> seq T := fun d T t0 b => t0 :: b.

Definition x := (@f _ _ (@ord0 1) [::]). (* or (f (@ord0 1) [::]). *)

Last updated: Jul 25 2024 at 16:02 UTC