I want to equip the ordinals with a different order relation, which means, I guess, define a new HB instance for OrderType. Where can I find simple examples for such a task using HB (I'm running coq 8.17 and mathcomp 2.0)?

BTW, when I try to run a copy-pasted version of the OrdinalOrder module from order.v, I get the following error message:

```
From HB Require Import structures.
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.
Module OrdinalOrder.
Section OrdinalOrder.
Fact ord_display : unit. Proof. exact: tt. Qed.
Section PossiblyTrivial.
Variable (n : nat).
#[export]
HB.instance Definition _ :=
[SubChoice_isSubOrder of 'I_n by <: with ord_display].
Lemma leEord : (le : rel 'I_n) = leq. Proof. by []. Qed.
The term "le" has type "nat -> nat -> Prop" while it is expected to have type
"rel 'I_n" (cannot unify "Prop" and "bool").
```

when I reach the point of compiling `leEord`

. Any idea where this could come from?

I guess the `README.md`

in https://github.com/math-comp/hierarchy-builder counts as a simple example.

Regarding the second question, it looks like `le`

is the inequality on `nat`

defined in `Coq.Init.Peano`

. What you are looking for is `Order.le`

, which you can access with the notation`<=%O`

.

Thanks @Quentin VERMANDE: I'll look at the README file. Also, do you know how this distinction between between `Order.le`

and `le`

is actually automatically performed in the order.v file?

Oh, I hadn't noticed the whole enclosing `Module Order.`

in order.v. So you can discard the previous question. Thanks @Quentin VERMANDE

I'm still confused about how HB works. I managed to get the following to typecheck and run, yielding the expected success messages:

```
#[export]
HB.instance Definition _ :=
@Order.isOrder.Build tt 'I_n.+1 lev ltv meet join ltv_def meet_def join_def lev_anti lev_trans total_lev.
```

inside a Section within a module called ValueOrder that includes all the proper lemmas used by `isOrder.Build`

(mimicking how OrdinalOrder is defined in order.v) . Now how do I pass this non-standard ordered ordinal type (there is no name for this `Definition`

) and a value of that type to a function such as:

```
Definition foo (T : orderType tt) (x : T) := x.
```

?

The usual trick is to use an alias

```
Definition T_new_order := T.
HB.instance Definition _ := Order.Build disp (T_new_order) ...
```

Now `T_new_order`

is convertible with `T`

but equipped with your alternative order. (There are quite a few examples at the end of the order.v file of mathcomp, for instance with different orders for lists IIRC)

Thanks @Pierre Roux . Unfortunately, when I do:

```
Definition P := 'I_n.+1.
#[export]
HB.instance Definition _ :=
@Order.isOrder.Build tt (P) lev ltv meet join ltv_def meet_def join_def lev_anti lev_trans total_lev.
```

where `n`

is a `Variable`

in my module, I get the error message (it works fine if I replace `P`

by its value, as before`):

```
Error: HB: cannot inhabit mixin Order_DistrLattice_isTotal on P
```

That's because isOrder requires a choiceType, you can copy it from 'I_n.+1 to P by preceding your HB.instance with

```
HB.instance Definition _ := Choice.on P.
```

Thanks @Pierre Roux . This is working fine, at least as long as I import my module. Otherwise it fails.

```
Section WithImport.
Import ValueOrder.
Definition foo (T : orderType tt) (x : T) := x.
Check (foo (P0 2)).
End WithImport.
Definition foo' (T : orderType tt) (x : T) := x.
Check (foo (ValueOrder.P0 2)).
(* fails with message: "The term "ValueOrder.P0 2" has type "ValueOrder.P 2" while it is expected to have type
"Order.Total.sort ?T". *)
```

`P0 : P`

is defined as `ord0`

in my module. Anyway, this works fine if I import my module, so this is good enough, I guess :)

Canonical structures are AFAIK never available if not imported, and that's intentional. Filtered imports should let you import canonicals, coercions and notations https://coq.inria.fr/refman/language/core/modules.html#coq:cmd.Import

Thanks @Paolo Giarrusso

Last updated: Jul 15 2024 at 20:02 UTC