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

Why is it?

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

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.

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.

Raül has marked this topic as resolved.

Last updated: Jul 23 2024 at 20:01 UTC