Stream: Hierarchy Builder devs & users

Topic: inheritance finite Type -> ordered Type


view this post on Zulip Aleksandar Nanevski (Sep 05 2023 at 17:21):

Hi.

I've been playing with HB, and have run into a problem. I'm trying to define my own version of ordered types, and have a canonical way to coerce every finite type into an ordered type. I tried the following code.

From HB Require Import structures.
From Coq Require Import ssreflect ssrbool ssrfun.
From mathcomp Require Import ssrnat eqtype seq path fintype.
Export Set Implicit Arguments.
Export Unset Strict Implicit.
Export Unset Printing Implicit Defensive.

Definition connected (T : eqType) (ord : rel T) :=
  forall x y, x != y -> ord x y || ord y x.

HB.mixin Record isOrdered T of Equality T := {
  ord : rel T;
  irr : irreflexive ord;
  trans : transitive ord;
  connex : connected ord}.

#[short(type="ordType")]
HB.structure Definition Ordered :=
  {T of Equality T & isOrdered T}.

Section FinTypeOrd.
Variable T : finType.

Definition ordf : rel T :=
  fun x y => index x (enum T) < index y (enum T).

Lemma fintp_irr : irreflexive ordf.
Proof. by move=>x; rewrite /ordf ltnn. Qed.

Lemma fintp_trans : transitive ordf.
Proof. by move=>x y z; rewrite /ordf; apply: ltn_trans. Qed.

Lemma fintp_connex : connected ordf.
Proof.
move=>x y; rewrite /ordf; case: ltngtP=>//= H.
have [H1 H2]: x \in enum T /\ y \in enum T by rewrite !mem_enum.
by rewrite -(nth_index x H1) -(nth_index x H2) H eq_refl.
Qed.

HB.instance Definition _ :=
  isOrdered.Build T fintp_irr fintp_trans fintp_connex.

End FinTypeOrd.

The last Definition gives me the following warning:

Warning:
non forgetful inheritance detected.
 You have two solutions:
1. (Best practice) Reorganize your hierarchy to make ordtype_isOrdered depend on
fintype_Finite. See the paper "Competing inheritance paths in
dependent type theory" (https://hal.inria.fr/hal-02463336) for more explanations
2. Use the attribute #[non_forgetful_inheritance] to disable this check.
We strongly advise you encapsulate this instance inside a module,
in order to isolate it from the rest of the code, and to be able
to import it on demand. See the above paper and the file
https://github.com/math-comp/hierarchy-builder/blob/master/tests/non_forgetful_inheritance.v
to witness devastating effects.
[HB.non-forgetful-inheritance,HB]

What's the right way to generate this instance, without the warning?

Thanks.

view this post on Zulip Pierre Roux (Sep 07 2023 at 15:46):

You can see that wiki page (in addition to the paper mentionned in the warning message) to learn more about non forgetful inheritance: https://github.com/math-comp/hierarchy-builder/wiki/NFI with examples and fixes.

view this post on Zulip Aleksandar Nanevski (Sep 08 2023 at 02:42):

I have looked into the wiki page and the paper, and I appreciate the point that I should try to combine finite and ordered structure somehow. However, I haven't been able to convince HB to accept any combination that I have thought of so far, as just trying to use Finite when building a mixin or a structure invariably comes back with an error message that I don't know how to work around. For example, if in the context of the above code I declare something like below (with the goal to combine finite types and orders):

HB.mixin Record isFinOrdered T of Finite T := {
  ord : rel T;
  irr : irreflexive ord;
  trans : transitive ord;
  connex : connected ord}.

I get that:

Error:
The conclusion of a builder is a mixin whose parameters depend on other mixins: extract-conclusion-params c1
 (prod `record` (app [global (indt «Finite.axioms_»), c1]) c2 \
   app [global (indt «choice.hasChoice.axioms_»), c1]) X0^2

Not sure what hasChoice has to do with this, nor how to proceed from here.

-Aleks

view this post on Zulip Pierre Roux (Sep 08 2023 at 06:30):

Why not doing something like (haven't tested):

HB.mixin Record isOrdered T := {
  ord : rel T;
  irr : irreflexive ord;
  trans : transitive ord;
  connex : connected ord}.
HB.structure Definition FinOrdered := {T of isFinite T & isOrdered T}.

Last updated: Apr 21 2024 at 02:41 UTC