Stream: Hierarchy Builder devs & users

Topic: Subsequences as a fintype


view this post on Zulip Florent Hivert (Dec 10 2023 at 21:41):

I'm trying to define the finType of subsequences of a seq. Everything goes well upto countType but HB is complaining about non-forgetful inheritance. I don't understand why. Here is the code

Variables (T : choiceType) (w : seq T).

Structure subseqs : predArgType :=
  Subseqs {subseqsval :> seq T; _ : subseq subseqsval w}.
HB.instance Definition _ := [isSub of subseqs for subseqsval].
HB.instance Definition _ := [Choice of subseqs by <:].

Implicit Type (s : subseqs).

Lemma to_mask_spec s : {m : (size w).-tuple bool | mask m w == s}.
Proof.
move: s => [s subs]; apply/sigW => /=.
by move: subs => /subseqP [m /eqP szm ->{s}]; exists (Tuple szm).
Qed.
Definition to_mask s := let: exist m _ := to_mask_spec s in m.

Lemma to_maskK : cancel to_mask (fun m => Subseqs (mask_subseq (val m) w)).
Proof.
by rewrite /to_mask => s; case: to_mask_spec => m /eqP eqm; apply val_inj.
Qed.

HB.instance Definition _ := CanIsCountable to_maskK.

Works well. However

HB.instance Definition _ := CanIsFinite to_maskK.

suggest to "Reorganize your hierarchy to make fintype_isFinite depend on eqtype_Equality." which doesn't makes sense to me. Any suggestion ?

view this post on Zulip Florent Hivert (Dec 11 2023 at 03:50):

I thinks I've found the solution: I just defined the subtype structure with

HB.instance Definition _ := [isSub of subseqs for subseqsval].

But not the choice type at let HB define it as consequence of the finType definition:

HB.instance Definition _ := Finite.copy subseqs (can_type to_maskK).

My understanding is that there is two way to get the eqType structure: either from the subtype or from the can_type. Mixing both create problems. Do you confirm that this is indeed the problem and that my solution is the right one ?

view this post on Zulip Cyril Cohen (Dec 11 2023 at 07:37):

Florent Hivert said:

I'm trying to define the finType of subsequences of a seq. Everything goes well upto countType but when I try to declare a canonical finType instance HB is complaining about non-forgetful inheritance. I don't understand why. Here is the code

Variables (T : choiceType) (w : seq T).

Structure subseqs : predArgType :=
  Subseqs {subseqsval :> seq T; _ : subseq subseqsval w}.
HB.instance Definition _ := [isSub of subseqs for subseqsval].
HB.instance Definition _ := [Choice of subseqs by <:].

Implicit Type (s : subseqs).

Lemma to_mask_spec s : {m : (size w).-tuple bool | mask m w == s}.
Proof.
move: s => [s subs]; apply/sigW => /=.
by move: subs => /subseqP [m /eqP szm ->{s}]; exists (Tuple szm).
Qed.
Definition to_mask s := let: exist m _ := to_mask_spec s in m.

Lemma to_maskK : cancel to_mask (fun m => Subseqs (mask_subseq (val m) w)).
Proof.
by rewrite /to_mask => s; case: to_mask_spec => m /eqP eqm; apply val_inj.
Qed.

HB.instance Definition _ := CanIsCountable to_maskK.

Works well. However

HB.instance Definition _ := CanIsFinite to_maskK.

suggest to "Reorganize your hierarchy to make fintype_isFinite depend on eqtype_Equality." which doesn't makes sense to me. Any suggestion ?

The inferred type was probably wrong, to avoid such issues one should always ensure the subject/key one wants to put an instance on is explicit. Here in order to make it explicit you must put the type annotation:
HB.instance Definition _ : IsFinite subseqs := CanIsFinite to_maskK.

view this post on Zulip Pierre Roux (Dec 11 2023 at 07:39):

Don't we have a syntax like HB.instance Definition _ := Finite.copy subseqs (can_type to_maskK)?

view this post on Zulip Cyril Cohen (Dec 11 2023 at 08:06):

This does something slightly different, I will provide more details later


Last updated: Apr 21 2024 at 01:02 UTC