- -

Library mathcomp.fingroup.presentation

- -

-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-

- -

- 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. - -

- Semantics details: -

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.
- -
-

- -

- 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.
- -
-

- -

- 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.
- -
-