Library mathcomp.fingroup.presentation
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
++ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+ Support for generator-and-relation presentations of groups. We provide the
+ syntax:
+ G \homg Grp (x_1 : ... x_n : (s_1 = t_1, ..., s_m = t_m))
+ <=> G is generated by elements x_1, ..., x_m satisfying the relations
+ s_1 = t_1, ..., s_m = t_m, i.e., G is a homomorphic image of the
+ group generated by the x_i, subject to the relations s_j = t_j.
+ G \isog Grp (x_1 : ... x_n : (s_1 = t_1, ..., s_m = t_m))
+ <=> G is isomorphic to the group generated by the x_i, subject to the
+ relations s_j = t_j. This is an intensional predicate (in Prop), as
+ even the non-triviality of a generated group is undecidable.
+ Syntax details:
+
+-
+
- Grp is a litteral constant. + + +
- There must be at least one generator and one relation. + + +
- A relation s_j = 1 can be abbreviated as simply s_j (a.k.a. a relator). + + +
- Two consecutive relations s_j = t, s_j+1 = t can be abbreviated + s_j = s_j+1 = t. + + +
- The s_j and t_j are terms built from the x_i and the standard group + operators *, 1, ^-1, ^+, ^-, ^, [~ u_1, ..., u_k]; no other operator or + abbreviation may be used, as the notation is implemented using static + overloading. + + +
- This is the closest we could get to the notation used in Aschbacher, + Grp (x_1, ... x_n : t_1,1 = ... = t_1,k1, ..., t_m,1 = ... = t_m,km) + under the current limitations of the Coq Notation facility. + + +
-
+
- G \isog Grp (...) : Prop expands to the statement + forall rT (H : {group rT}), (H \homg G) = (H \homg Grp (...)) + (with rT : finGroupType). + + +
- G \homg Grp (x_1 : ... x_n : (s_1 = t_1, ..., s_m = t_m)) : bool, with + G : {set gT}, is convertible to the boolean expression + [exists t : gT * ... gT, let: (x_1, ..., x_n) := t in + (< [x_1]> <*> ... <*> < [x_n]>, (s_1, ... (s_m-1, s_m) ...)) + == (G, (t_1, ... (t_m-1, t_m) ...)) ] + where the tuple comparison above is convertible to the conjunction + [&& < [x_1]> <*> ... <*> < [x_n]> == G, s_1 == t_1, ... & s_m == t_m] + Thus G \homg Grp (...) can be easily exploited by destructing the tuple + created case/existsP, then destructing the tuple equality with case/eqP. + Conversely it can be proved by using apply/existsP, providing the tuple + with a single exists (u_1, ..., u_n), then using rewrite !xpair_eqE /= + to expose the conjunction, and optionally using an apply/and{m+1}P view + to split it into subgoals (in that case, the rewrite is in principle + redundant, but necessary in practice because of the poor performance of + conversion in the Coq unifier). + +
+
+
+Set Implicit Arguments.
+ +
+Import GroupScope.
+ +
+Module Presentation.
+ +
+Section Presentation.
+ +
+Implicit Types gT rT : finGroupType.
+Implicit Type vT : finType. (* tuple value type *)
+ +
+Inductive term :=
+ | Cst of nat
+ | Idx
+ | Inv of term
+ | Exp of term & nat
+ | Mul of term & term
+ | Conj of term & term
+ | Comm of term & term.
+ +
+Fixpoint eval {gT} e t : gT :=
+ match t with
+ | Cst i ⇒ nth 1 e i
+ | Idx ⇒ 1
+ | Inv t1 ⇒ (eval e t1)^-1
+ | Exp t1 n ⇒ eval e t1 ^+ n
+ | Mul t1 t2 ⇒ eval e t1 × eval e t2
+ | Conj t1 t2 ⇒ eval e t1 ^ eval e t2
+ | Comm t1 t2 ⇒ [~ eval e t1, eval e t2]
+ end.
+ +
+Inductive formula := Eq2 of term & term | And of formula & formula.
+Definition Eq1 s := Eq2 s Idx.
+Definition Eq3 s1 s2 t := And (Eq2 s1 t) (Eq2 s2 t).
+ +
+Inductive rel_type := NoRel | Rel vT of vT & vT.
+ +
+Definition bool_of_rel r := if r is Rel vT v1 v2 then v1 == v2 else true.
+ +
+Definition and_rel vT (v1 v2 : vT) r :=
+ if r is Rel wT w1 w2 then Rel (v1, w1) (v2, w2) else Rel v1 v2.
+ +
+Fixpoint rel {gT} (e : seq gT) f r :=
+ match f with
+ | Eq2 s t ⇒ and_rel (eval e s) (eval e t) r
+ | And f1 f2 ⇒ rel e f1 (rel e f2 r)
+ end.
+ +
+Inductive type := Generator of term → type | Formula of formula.
+Definition Cast p : type := p. (* syntactic scope cast *)
+ +
+Inductive env gT := Env of {set gT} & seq gT.
+Definition env1 {gT} (x : gT : finType) := Env <[x]> [:: x].
+ +
+Fixpoint sat gT vT B n (s : vT → env gT) p :=
+ match p with
+ | Formula f ⇒
+ [∃ v, let: Env A e := s v in and_rel A B (rel (rev e) f NoRel)]
+ | Generator p' ⇒
+ let s' v := let: Env A e := s v.1 in Env (A <*> <[v.2]>) (v.2 :: e) in
+ sat B n.+1 s' (p' (Cst n))
+ end.
+ +
+Definition hom gT (B : {set gT}) p := sat B 1 env1 (p (Cst 0)).
+Definition iso gT (B : {set gT}) p :=
+ ∀ rT (H : {group rT}), (H \homg B) = hom H p.
+ +
+End Presentation.
+ +
+End Presentation.
+ +
+Import Presentation.
+ +
+Coercion bool_of_rel : rel_type >-> bool.
+Coercion Eq1 : term >-> formula.
+Coercion Formula : formula >-> type.
+ +
+
+
++Set Implicit Arguments.
+ +
+Import GroupScope.
+ +
+Module Presentation.
+ +
+Section Presentation.
+ +
+Implicit Types gT rT : finGroupType.
+Implicit Type vT : finType. (* tuple value type *)
+ +
+Inductive term :=
+ | Cst of nat
+ | Idx
+ | Inv of term
+ | Exp of term & nat
+ | Mul of term & term
+ | Conj of term & term
+ | Comm of term & term.
+ +
+Fixpoint eval {gT} e t : gT :=
+ match t with
+ | Cst i ⇒ nth 1 e i
+ | Idx ⇒ 1
+ | Inv t1 ⇒ (eval e t1)^-1
+ | Exp t1 n ⇒ eval e t1 ^+ n
+ | Mul t1 t2 ⇒ eval e t1 × eval e t2
+ | Conj t1 t2 ⇒ eval e t1 ^ eval e t2
+ | Comm t1 t2 ⇒ [~ eval e t1, eval e t2]
+ end.
+ +
+Inductive formula := Eq2 of term & term | And of formula & formula.
+Definition Eq1 s := Eq2 s Idx.
+Definition Eq3 s1 s2 t := And (Eq2 s1 t) (Eq2 s2 t).
+ +
+Inductive rel_type := NoRel | Rel vT of vT & vT.
+ +
+Definition bool_of_rel r := if r is Rel vT v1 v2 then v1 == v2 else true.
+ +
+Definition and_rel vT (v1 v2 : vT) r :=
+ if r is Rel wT w1 w2 then Rel (v1, w1) (v2, w2) else Rel v1 v2.
+ +
+Fixpoint rel {gT} (e : seq gT) f r :=
+ match f with
+ | Eq2 s t ⇒ and_rel (eval e s) (eval e t) r
+ | And f1 f2 ⇒ rel e f1 (rel e f2 r)
+ end.
+ +
+Inductive type := Generator of term → type | Formula of formula.
+Definition Cast p : type := p. (* syntactic scope cast *)
+ +
+Inductive env gT := Env of {set gT} & seq gT.
+Definition env1 {gT} (x : gT : finType) := Env <[x]> [:: x].
+ +
+Fixpoint sat gT vT B n (s : vT → env gT) p :=
+ match p with
+ | Formula f ⇒
+ [∃ v, let: Env A e := s v in and_rel A B (rel (rev e) f NoRel)]
+ | Generator p' ⇒
+ let s' v := let: Env A e := s v.1 in Env (A <*> <[v.2]>) (v.2 :: e) in
+ sat B n.+1 s' (p' (Cst n))
+ end.
+ +
+Definition hom gT (B : {set gT}) p := sat B 1 env1 (p (Cst 0)).
+Definition iso gT (B : {set gT}) p :=
+ ∀ rT (H : {group rT}), (H \homg B) = hom H p.
+ +
+End Presentation.
+ +
+End Presentation.
+ +
+Import Presentation.
+ +
+Coercion bool_of_rel : rel_type >-> bool.
+Coercion Eq1 : term >-> formula.
+Coercion Formula : formula >-> type.
+ +
+
+ Declare (implicitly) the argument scope tags.
+
+
+Notation "1" := Idx : group_presentation.
+ +
+Infix "×" := Mul : group_presentation.
+Infix "^+" := Exp : group_presentation.
+Infix "^" := Conj : group_presentation.
+Notation "x ^-1" := (Inv x) : group_presentation.
+Notation "x ^- n" := (Inv (x ^+ n)) : group_presentation.
+Notation "[ ~ x1 , x2 , .. , xn ]" :=
+ (Comm .. (Comm x1 x2) .. xn) : group_presentation.
+Notation "x = y" := (Eq2 x y) : group_presentation.
+Notation "x = y = z" := (Eq3 x y z) : group_presentation.
+Notation "( r1 , r2 , .. , rn )" :=
+ (And .. (And r1 r2) .. rn) : group_presentation.
+ +
+
+
++ +
+Infix "×" := Mul : group_presentation.
+Infix "^+" := Exp : group_presentation.
+Infix "^" := Conj : group_presentation.
+Notation "x ^-1" := (Inv x) : group_presentation.
+Notation "x ^- n" := (Inv (x ^+ n)) : group_presentation.
+Notation "[ ~ x1 , x2 , .. , xn ]" :=
+ (Comm .. (Comm x1 x2) .. xn) : group_presentation.
+Notation "x = y" := (Eq2 x y) : group_presentation.
+Notation "x = y = z" := (Eq3 x y z) : group_presentation.
+Notation "( r1 , r2 , .. , rn )" :=
+ (And .. (And r1 r2) .. rn) : group_presentation.
+ +
+
+ Declare (implicitly) the argument scope tags.
+
+
+Notation "x : p" := (fun x ⇒ Cast p) : nt_group_presentation.
+ +
+Notation "x : p" := (Generator (x : p)) : group_presentation.
+ +
+Notation "H \homg 'Grp' p" := (hom H p)
+ (at level 70, p at level 0, format "H \homg 'Grp' p") : group_scope.
+ +
+Notation "H \isog 'Grp' p" := (iso H p)
+ (at level 70, p at level 0, format "H \isog 'Grp' p") : group_scope.
+ +
+Notation "H \homg 'Grp' ( x : p )" := (hom H (x : p))
+ (at level 70, x at level 0,
+ format "'[hv' H '/ ' \homg 'Grp' ( x : p ) ']'") : group_scope.
+ +
+Notation "H \isog 'Grp' ( x : p )" := (iso H (x : p))
+ (at level 70, x at level 0,
+ format "'[hv' H '/ ' \isog 'Grp' ( x : p ) ']'") : group_scope.
+ +
+Section PresentationTheory.
+ +
+Implicit Types gT rT : finGroupType.
+ +
+Import Presentation.
+ +
+Lemma isoGrp_hom gT (G : {group gT}) p : G \isog Grp p → G \homg Grp p.
+ +
+Lemma isoGrpP gT (G : {group gT}) p rT (H : {group rT}) :
+ G \isog Grp p → reflect (#|H| = #|G| ∧ H \homg Grp p) (H \isog G).
+ +
+Lemma homGrp_trans rT gT (H : {set rT}) (G : {group gT}) p :
+ H \homg G → G \homg Grp p → H \homg Grp p.
+ +
+Lemma eq_homGrp gT rT (G : {group gT}) (H : {group rT}) p :
+ G \isog H → (G \homg Grp p) = (H \homg Grp p).
+ +
+Lemma isoGrp_trans gT rT (G : {group gT}) (H : {group rT}) p :
+ G \isog H → H \isog Grp p → G \isog Grp p.
+ +
+Lemma intro_isoGrp gT (G : {group gT}) p :
+ G \homg Grp p → (∀ rT (H : {group rT}), H \homg Grp p → H \homg G) →
+ G \isog Grp p.
+ +
+End PresentationTheory.
+ +
+
++ +
+Notation "x : p" := (Generator (x : p)) : group_presentation.
+ +
+Notation "H \homg 'Grp' p" := (hom H p)
+ (at level 70, p at level 0, format "H \homg 'Grp' p") : group_scope.
+ +
+Notation "H \isog 'Grp' p" := (iso H p)
+ (at level 70, p at level 0, format "H \isog 'Grp' p") : group_scope.
+ +
+Notation "H \homg 'Grp' ( x : p )" := (hom H (x : p))
+ (at level 70, x at level 0,
+ format "'[hv' H '/ ' \homg 'Grp' ( x : p ) ']'") : group_scope.
+ +
+Notation "H \isog 'Grp' ( x : p )" := (iso H (x : p))
+ (at level 70, x at level 0,
+ format "'[hv' H '/ ' \isog 'Grp' ( x : p ) ']'") : group_scope.
+ +
+Section PresentationTheory.
+ +
+Implicit Types gT rT : finGroupType.
+ +
+Import Presentation.
+ +
+Lemma isoGrp_hom gT (G : {group gT}) p : G \isog Grp p → G \homg Grp p.
+ +
+Lemma isoGrpP gT (G : {group gT}) p rT (H : {group rT}) :
+ G \isog Grp p → reflect (#|H| = #|G| ∧ H \homg Grp p) (H \isog G).
+ +
+Lemma homGrp_trans rT gT (H : {set rT}) (G : {group gT}) p :
+ H \homg G → G \homg Grp p → H \homg Grp p.
+ +
+Lemma eq_homGrp gT rT (G : {group gT}) (H : {group rT}) p :
+ G \isog H → (G \homg Grp p) = (H \homg Grp p).
+ +
+Lemma isoGrp_trans gT rT (G : {group gT}) (H : {group rT}) p :
+ G \isog H → H \isog Grp p → G \isog Grp p.
+ +
+Lemma intro_isoGrp gT (G : {group gT}) p :
+ G \homg Grp p → (∀ rT (H : {group rT}), H \homg Grp p → H \homg G) →
+ G \isog Grp p.
+ +
+End PresentationTheory.
+ +
+