Stream: math-comp users

Topic: Hierarchy builder: two groups on the same type

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

Hi all,
I need to define an action but I need to use the function composition for permutations instead of the perm_mul as the group operation.
I know how to define a group with Hierarchy Builder but it seems that Coq keeps using the previously defined operation in perm (which is also useful to me because it already has results proven in it).
How can I keep both group operations on the same type?

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

The problem I find is that whenever I try to use results from fingroup, Coq assumes I'm talking about perm_mul.
The only think I need to know is how to specify to Coq which baseFinGroupType I'm talking about.

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

The usual solution is to use an alias.

(* build a group on type group1 with law1 : group1 -> group1 -> group1 *)
Definition group2 : Type := group1
(* build a group on type group2 with law2 *)
(* now in '(x : group1) * y' the '*' will be law1 whereas in '(x : group2) * y' the '*' will be law2 *)

Last updated: Jul 25 2024 at 15:02 UTC