Stream: math-comp users

Topic: Examples for HB.instance using order.v


view this post on Zulip Pierre Jouvelot (Dec 02 2023 at 10:11):

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?

view this post on Zulip Quentin VERMANDE (Dec 02 2023 at 11:07):

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.

view this post on Zulip Pierre Jouvelot (Dec 02 2023 at 11:19):

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?

view this post on Zulip Pierre Jouvelot (Dec 02 2023 at 11:37):

Oh, I hadn't noticed the whole enclosing Module Order. in order.v. So you can discard the previous question. Thanks @Quentin VERMANDE

view this post on Zulip Pierre Jouvelot (Dec 02 2023 at 18:40):

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.

?

view this post on Zulip Pierre Roux (Dec 02 2023 at 20:09):

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)

view this post on Zulip Pierre Jouvelot (Dec 02 2023 at 20:21):

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

view this post on Zulip Pierre Roux (Dec 02 2023 at 21:11):

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.

view this post on Zulip Pierre Jouvelot (Dec 02 2023 at 21:40):

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 :)

view this post on Zulip Paolo Giarrusso (Dec 03 2023 at 02:25):

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

view this post on Zulip Pierre Jouvelot (Dec 03 2023 at 12:49):

Thanks @Paolo Giarrusso


Last updated: Jul 15 2024 at 20:02 UTC