Stream: math-comp users

Topic: ✔ Hierarchy builder: two groups on the same type


view this post on Zulip Raül (May 14 2023 at 14:33):

I'm trying to do it with Hierarchy Builder and it says "cannot inhabit mixin fingroup_BaseFinGroup_isGroup on perm_type2".
Why is it?

view this post on Zulip Pierre Roux (May 14 2023 at 14:48):

Looks like a missing instance but please give a minimal working example otherwise its hard to tell more.

view this post on Zulip Raül (May 14 2023 at 15:06):

I have this code:

From mathcomp Require Import  all_fingroup perm.

Section Comp_Mul.

Set Implicit Arguments.
Variable T : finType.

Definition perm_type2 : predArgType := perm_type T.
Definition perm_of2 of phant T := perm_type2.
Identity Coercion type2_of_perm2 : perm_of2 >-> perm_type2.

Notation "{ 'perm2' T }" := (perm_of2 (Phant T)).

Implicit Types (x y : T) (s t : {perm2 T}) (S : {set T}).

Definition comp_mul s t : {perm2 T} := perm (inj_comp (@perm_inj T s) (@perm_inj T t)).
Definition comp_one : {perm2 T} := perm (@inj_id T).
Definition comp_inv s : {perm2 T} := perm (can_inj (perm_invK s)).

Lemma comp_oneP : left_id comp_one comp_mul.
Proof.
  by move=> s; apply/permP => x; rewrite permE /= permE.
Qed.

Lemma comp_invP : left_inverse  comp_one comp_inv comp_mul.
Proof.
  by move=> s; apply/permP=> x; rewrite !permE /= permE iinv_f;
  last exact: perm_inj.
Qed.

Lemma comp_mulP : associative comp_mul.
Proof.
  by move=> s t u; apply/permP=> x; do !rewrite permE /=.
Qed.


HB.instance Definition _ := isMulGroup.Build (perm_type2)
  comp_mulP comp_oneP comp_invP.

The error is on the HB instance.

view this post on Zulip Pierre Roux (May 14 2023 at 15:38):

According to HB.about isMulGroup.Build you need perm_type2 to be finite so HB.instance Definition _ := Finite.on perm_type2. just before your HB.instance makes it work.

view this post on Zulip Notification Bot (May 14 2023 at 15:39):

Raül has marked this topic as resolved.


Last updated: Jul 23 2024 at 20:01 UTC