text:
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
(* Distributed under the terms of CeCILL-B.                                  *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
From mathcomp Require Import div choice fintype tuple finfun bigop prime.
From mathcomp Require Import ssralg poly finset fingroup morphism perm.
From mathcomp Require Import automorphism quotient gproduct action finalg.
From mathcomp Require Import zmodp commutator cyclic center pgroup gseries.
From mathcomp Require Import nilpotent sylow maximal abelian matrix.
From mathcomp Require Import mxalgebra mxrepresentation.

(******************************************************************************)
(*   This file completes the theory developed in mxrepresentation.v with the  *)
(* construction and properties of linear representations over finite fields,  *)
(* and in particular the correspondance between internal action on a (normal) *)
(* elementary abelian p-subgroup and a linear representation on an Fp-module. *)
(*   We provide the following next constructions for a finite field F:        *)
(*        'Zm%act == the action of {unit F} on 'M[F]_(m, n).                  *)
(*         rowg A == the additive group of 'rV[F]_n spanned by the row space  *)
(*                   of the matrix A.                                         *)
(*      rowg_mx L == the partial inverse to rowg; for any 'Zm-stable group L  *)
(*                   of 'rV[F]_n we have rowg (rowg_mx L) = L.                *)
(*     GLrepr F n == the natural, faithful representation of 'GL_n[F].        *)
(*     reprGLm rG == the morphism G >-> 'GL_n[F] equivalent to the            *)
(*                   representation r of G (with rG : mx_repr r G).           *)
(*   ('MR rG)%act == the action of G on 'rV[F]_n equivalent to the            *)
(*                   representation r of G (with rG : mx_repr r G).           *)
(* The second set of constructions defines the interpretation of a normal     *)
(* non-trivial elementary abelian p-subgroup as an 'F_p module. We assume     *)
(* abelE : p.-abelem E and ntE : E != 1, throughout, as these are needed to   *)
(* build the isomorphism between E and a nontrivial 'rV['F_p]_n.              *)
(*         'rV(E) == the type of row vectors of the 'F_p module equivalent    *)
(*                   to E when E is a non-trivial p.-abelem group.            *)
(*          'M(E) == the type of matrices corresponding to E.                 *)
(*         'dim E == the width of vectors/matrices in 'rV(E) / 'M(E).         *)
(* abelem_rV abelE ntE == the one-to-one injection of E onto 'rV(E).          *)
(*  rVabelem abelE ntE == the one-to-one projection of 'rV(E) onto E.         *)
(* abelem_repr abelE ntE nEG == the representation of G on 'rV(E) that is     *)
(*                   equivalent to conjugation by G in E; here abelE, ntE are *)
(*                   as above, and G \subset 'N(E).                           *)
(* This file end with basic results on p-modular representations of p-groups, *)
(* and theorems giving the structure of the representation of extraspecial    *)
(* groups; these results use somewhat more advanced group theory than the     *)
(* rest of mxrepresentation, in particular, results of sylow.v and maximal.v. *)
(******************************************************************************)

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import GroupScope GRing.Theory FinRing.Theory.
Local Open Scope ring_scope.

(* Special results for representations on a finite field. In this case, the   *)
(* representation is equivalent to a morphism into the general linear group   *)
(* 'GL_n[F]. It is furthermore equivalent to a group action on the finite     *)
(* additive group of the corresponding row space 'rV_n. In addition, row      *)
(* spaces of matrices in 'M[F]_n correspond to subgroups of that vector group *)
(* (this is only surjective when F is a prime field 'F_p), with moduleules    *)
(* corresponding to subgroups stabilized by the external action.              *)

Section FinRingRepr.

Variable (R : finComUnitRingType) (gT : finGroupType).
Variables (G : {group gT}) (n : nat) (rG : mx_representation R G n).

Definition mx_repr_act (u : 'rV_n) x := u *m rG (val (subg G x)).

Lemma mx_repr_actE u x : x \in G -> mx_repr_act u x = u *m rG x.
Proof. by move=> Gx; rewrite /mx_repr_act /= subgK. Qed.

Fact mx_repr_is_action : is_action G mx_repr_act.
Proof.
split=> [x | u x y Gx Gy]; first exact: can_inj (repr_mxK _ (subgP _)).
by rewrite !mx_repr_actE ?groupM // -mulmxA repr_mxM.
Qed.
Canonical Structure mx_repr_action := Action mx_repr_is_action.

Fact mx_repr_is_groupAction : is_groupAction [set: 'rV[R]_n] mx_repr_action.
Proof.
move=> x Gx /=; rewrite !inE.
apply/andP; split; first by apply/subsetP=> u; rewrite !inE.
by apply/morphicP=> /= u v _ _; rewrite !actpermE /= /mx_repr_act mulmxDl.
Qed.
Canonical Structure mx_repr_groupAction := GroupAction mx_repr_is_groupAction.

End FinRingRepr.

Notation "''MR' rG" := (mx_repr_action rG)
  (at level 10, rG at level 8) : action_scope.
Notation "''MR' rG" := (mx_repr_groupAction rG) : groupAction_scope.

Section FinFieldRepr.

Variable F : finFieldType.

(* The external group action (by scaling) of the multiplicative unit group   *)
(* of the finite field, and the correspondence between additive subgroups    *)
(* of row vectors that are stable by this action, and the matrix row spaces. *)
Section ScaleAction.

Variables m n : nat.

Definition scale_act (A : 'M[F]_(m, n)) (a : {unit F}) := val a *: A.
Lemma scale_actE A a : scale_act A a = val a *: A. Proof. by []. Qed.
Fact scale_is_action : is_action setT scale_act.
Proof.
apply: is_total_action=> [A | A a b]; rewrite /scale_act ?scale1r //.
by rewrite ?scalerA mulrC.
Qed.
Canonical scale_action := Action scale_is_action.
Fact scale_is_groupAction : is_groupAction setT scale_action.
Proof.
move=> a _ /=; rewrite inE; apply/andP.
split; first by apply/subsetP=> A; rewrite !inE.
by apply/morphicP=> u A _ _ /=; rewrite !actpermE /= /scale_act scalerDr.
Qed.
Canonical scale_groupAction := GroupAction scale_is_groupAction.

Lemma astab1_scale_act A : A != 0 -> 'C[A | scale_action] = 1%g.
Proof.
rewrite -mxrank_eq0=> nzA; apply/trivgP/subsetP=> a; apply: contraLR.
rewrite !inE -val_eqE -subr_eq0 sub1set !inE => nz_a1.
by rewrite -subr_eq0 -scaleN1r -scalerDl -mxrank_eq0 eqmx_scale.
Qed.

End ScaleAction.

Local Notation "'Zm" := (scale_action _ _) (at level 8) : action_scope.

Section RowGroup.

Variable n : nat.
Local Notation rVn := 'rV[F]_n.

Definition rowg m (A : 'M[F]_(m, n)) : {set rVn} := [set u | u <= A]%MS.

Lemma mem_rowg m A v : (v \in @rowg m A) = (v <= A)%MS.
Proof. by rewrite inE. Qed.

Fact rowg_group_set m A : group_set (@rowg m A).
Proof.
by apply/group_setP; split=> [|u v]; rewrite !inE ?sub0mx //; apply: addmx_sub.
Qed.
Canonical rowg_group m A := Group (@rowg_group_set m A).

Lemma rowg_stable m (A : 'M_(m, n)) : [acts setT, on rowg A | 'Zm].
Proof. by apply/actsP=> a _ v; rewrite !inE eqmx_scale // -unitfE (valP a). Qed.

Lemma rowgS m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
  (rowg A \subset rowg B) = (A <= B)%MS.
Proof.
apply/subsetP/idP=> sAB => [| u].
  by apply/row_subP=> i; have:= sAB (row i A); rewrite !inE row_sub => ->.
by rewrite !inE => suA; apply: submx_trans sAB.
Qed.

Lemma eq_rowg m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
  (A :=: B)%MS -> rowg A = rowg B.
Proof. by move=> eqAB; apply/eqP; rewrite eqEsubset !rowgS !eqAB andbb. Qed.

Lemma rowg0 m : rowg (0 : 'M_(m, n)) = 1%g.
Proof. by apply/trivgP/subsetP=> v; rewrite !inE eqmx0 submx0. Qed.

Lemma rowg1 : rowg 1%:M = setT.
Proof. by apply/setP=> x; rewrite !inE submx1. Qed.

Lemma trivg_rowg m (A : 'M_(m, n)) : (rowg A == 1%g) = (A == 0).
Proof. by rewrite -submx0 -rowgS rowg0 (sameP trivgP eqP). Qed.

Definition rowg_mx (L : {set rVn}) := <<\matrix_(i < #|L|) enum_val i>>%MS.

Lemma rowgK m (A : 'M_(m, n)) : (rowg_mx (rowg A) :=: A)%MS.
Proof.
apply/eqmxP; rewrite !genmxE; apply/andP; split.
  by apply/row_subP=> i; rewrite rowK; have:= enum_valP i; rewrite /= inE.
apply/row_subP=> i; set v := row i A.
have Av: v \in rowg A by rewrite inE row_sub.
by rewrite (eq_row_sub (enum_rank_in Av v)) // rowK enum_rankK_in.
Qed.

Lemma rowg_mxS (L M : {set 'rV[F]_n}) :
  L \subset M -> (rowg_mx L <= rowg_mx M)%MS.
Proof.
move/subsetP=> sLM; rewrite !genmxE; apply/row_subP=> i.
rewrite rowK; move: (enum_val i) (sLM _ (enum_valP i)) => v Mv.
by rewrite (eq_row_sub (enum_rank_in Mv v)) // rowK enum_rankK_in.
Qed.

Lemma sub_rowg_mx (L : {set rVn}) : L \subset rowg (rowg_mx L).
Proof.
apply/subsetP=> v Lv; rewrite inE genmxE.
by rewrite (eq_row_sub (enum_rank_in Lv v)) // rowK enum_rankK_in.
Qed.

Lemma stable_rowg_mxK (L : {group rVn}) :
  [acts setT, on L | 'Zm] -> rowg (rowg_mx L) = L.
Proof.
move=> linL; apply/eqP; rewrite eqEsubset sub_rowg_mx andbT.
apply/subsetP=> v; rewrite inE genmxE => /submxP[u ->{v}].
rewrite mulmx_sum_row group_prod // => i _.
rewrite rowK; move: (enum_val i) (enum_valP i) => v Lv.
case: (eqVneq (u 0 i) 0) => [->|]; first by rewrite scale0r group1.
by rewrite -unitfE => aP; rewrite ((actsP linL) (FinRing.Unit _ aP)) ?inE.
Qed.

Lemma rowg_mx1 : rowg_mx 1%g = 0.
Proof. by apply/eqP; rewrite -submx0 -(rowg0 0) rowgK sub0mx. Qed.

Lemma rowg_mx_eq0 (L : {group rVn}) : (rowg_mx L == 0) = (L :==: 1%g).
Proof.
rewrite -trivg_rowg; apply/idP/eqP=> [|->]; last by rewrite rowg_mx1 rowg0.
exact/contraTeq/subG1_contra/sub_rowg_mx.
Qed.

Lemma rowgI m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
  rowg (A :&: B)%MS = rowg A :&: rowg B.
Proof. by apply/setP=> u; rewrite !inE sub_capmx. Qed.

Lemma card_rowg m (A : 'M_(m, n)) : #|rowg A| = (#|F| ^ \rank A)%N.
Proof.
rewrite -[\rank A]mul1n -card_matrix.
have injA: injective (mulmxr (row_base A)).
  have /row_freeP[A' A'K] := row_base_free A.
  by move=> ?; apply: can_inj (mulmxr A') _ => u; rewrite /= -mulmxA A'K mulmx1.
rewrite -(card_image (injA _)); apply: eq_card => v.
by rewrite inE -(eq_row_base A) (sameP submxP codomP).
Qed.

Lemma rowgD m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
  rowg (A + B)%MS = (rowg A * rowg B)%g.
Proof.
apply/eqP; rewrite eq_sym eqEcard mulG_subG /= !rowgS.
rewrite addsmxSl addsmxSr -(@leq_pmul2r #|rowg A :&: rowg B|) ?cardG_gt0 //=.
by rewrite -mul_cardG -rowgI !card_rowg -!expnD mxrank_sum_cap.
Qed.

Lemma cprod_rowg m1 m2 (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
  rowg A \* rowg B = rowg (A + B)%MS.
Proof. by rewrite rowgD cprodE // (sub_abelian_cent2 (zmod_abelian setT)). Qed.

Lemma dprod_rowg  m1 m2 (A : 'M[F]_(m1, n)) (B : 'M[F]_(m2, n)) :
  mxdirect (A + B) -> rowg A \x rowg B = rowg (A + B)%MS.
Proof.
rewrite (sameP mxdirect_addsP eqP) -trivg_rowg rowgI => /eqP tiAB.
by rewrite -cprod_rowg dprodEcp.
Qed.

Lemma bigcprod_rowg m I r (P : pred I) (A : I -> 'M[F]_n) (B : 'M[F]_(m, n)) :
    (\sum_(i <- r | P i) A i :=: B)%MS ->
  \big[cprod/1%g]_(i <- r | P i) rowg (A i) = rowg B.
Proof.
by move/eq_rowg <-; apply/esym/big_morph=> [? ?|]; rewrite (rowg0, cprod_rowg).
Qed.

Lemma bigdprod_rowg m (I : finType) (P : pred I) A (B : 'M[F]_(m, n)) :
    let S := (\sum_(i | P i) A i)%MS in (S :=: B)%MS -> mxdirect S ->
  \big[dprod/1%g]_(i | P i) rowg (A i) = rowg B.
Proof.
move=> S defS; rewrite mxdirectE defS /= => /eqP rankB.
apply: bigcprod_card_dprod (bigcprod_rowg defS) (eq_leq _).
by rewrite card_rowg rankB expn_sum; apply: eq_bigr => i _; rewrite card_rowg.
Qed.

End RowGroup.

Variables (gT : finGroupType) (G : {group gT}) (n' : nat).
Local Notation n := n'.+1.
Variable (rG : mx_representation F G n).

Fact GL_mx_repr : mx_repr 'GL_n[F] GLval. Proof. by []. Qed.
Canonical GLrepr := MxRepresentation GL_mx_repr.

Lemma GLmx_faithful : mx_faithful GLrepr.
Proof. by apply/subsetP=> A; rewrite !inE mul1mx. Qed.

Definition reprGLm x : {'GL_n[F]} := insubd (1%g : {'GL_n[F]}) (rG x).

Lemma val_reprGLm x : x \in G -> val (reprGLm x) = rG x.
Proof. by move=> Gx; rewrite val_insubd (repr_mx_unitr rG). Qed.

Lemma comp_reprGLm : {in G, GLval \o reprGLm =1 rG}.
Proof. exact: val_reprGLm. Qed.

Lemma reprGLmM : {in G &, {morph reprGLm : x y / x * y}}%g.
Proof.
by move=> x y Gx Gy; apply: val_inj; rewrite /= !val_reprGLm ?groupM ?repr_mxM.
Qed.
Canonical reprGL_morphism := Morphism reprGLmM.

Lemma ker_reprGLm : 'ker reprGLm = rker rG.
Proof.
apply/setP=> x; rewrite !inE mul1mx; apply: andb_id2l => Gx.
by rewrite -val_eqE val_reprGLm.
Qed.

Lemma astab_rowg_repr m (A : 'M_(m, n)) : 'C(rowg A | 'MR rG) = rstab rG A.
Proof.
apply/setP=> x; rewrite !inE /=; apply: andb_id2l => Gx.
apply/subsetP/eqP=> cAx => [|u]; last first.
  by rewrite !inE mx_repr_actE // => /submxP[u' ->]; rewrite -mulmxA cAx.
apply/row_matrixP=> i; apply/eqP; move/implyP: (cAx (row i A)).
by rewrite !inE row_sub mx_repr_actE //= row_mul.
Qed.

Lemma astabs_rowg_repr m (A : 'M_(m, n)) : 'N(rowg A | 'MR rG) = rstabs rG A.
Proof.
apply/setP=> x; rewrite !inE /=; apply: andb_id2l => Gx.
apply/subsetP/idP=> nAx => [|u]; last first.
  by rewrite !inE mx_repr_actE // => Au; apply: (submx_trans (submxMr _ Au)).
apply/row_subP=> i; move/implyP: (nAx (row i A)).
by rewrite !inE row_sub mx_repr_actE //= row_mul.
Qed.

Lemma acts_rowg (A : 'M_n) : [acts G, on rowg A | 'MR rG] = mxmodule rG A.
Proof. by rewrite astabs_rowg_repr. Qed.

Lemma astab_setT_repr : 'C(setT | 'MR rG) = rker rG.
Proof. by rewrite -rowg1 astab_rowg_repr. Qed.

Lemma mx_repr_action_faithful :
  [faithful G, on setT | 'MR rG] = mx_faithful rG.
Proof.
by rewrite /faithful astab_setT_repr (setIidPr _) // [rker _]setIdE subsetIl.
Qed.

Lemma afix_repr (H : {set gT}) :
  H \subset G -> 'Fix_('MR rG)(H) = rowg (rfix_mx rG H).
Proof.
move/subsetP=> sHG; apply/setP=> /= u; rewrite !inE.
apply/subsetP/rfix_mxP=> cHu x Hx; have:= cHu x Hx;
  by rewrite !inE /= => /eqP; rewrite mx_repr_actE ?sHG.
Qed.

Lemma gacent_repr (H : {set gT}) :
  H \subset G -> 'C_(| 'MR rG)(H) = rowg (rfix_mx rG H).
Proof. by move=> sHG; rewrite gacentE // setTI afix_repr. Qed.

End FinFieldRepr.

Arguments rowg_mx {F n%N} L%g.
Notation "''Zm'" := (scale_action _ _ _) (at level 8) : action_scope.
Notation "''Zm'" := (scale_groupAction _ _ _) : groupAction_scope.

Section MatrixGroups.

Implicit Types m n p q : nat.

Lemma exponent_mx_group m n q :
  m > 0 -> n > 0 -> q > 1 -> exponent [set: 'M['Z_q]_(m, n)] = q.
Proof.
move=> m_gt0 n_gt0 q_gt1; apply/eqP; rewrite eqn_dvd; apply/andP; split.
  apply/exponentP=> x _; apply/matrixP=> i j; rewrite mulmxnE !mxE.
  by rewrite -mulr_natr -Zp_nat_mod // modnn mulr0.
pose cmx1 := const_mx 1%R : 'M['Z_q]_(m, n).
apply: dvdn_trans (dvdn_exponent (in_setT cmx1)).
have/matrixP/(_ (Ordinal m_gt0))/(_ (Ordinal n_gt0))/eqP := expg_order cmx1.
by rewrite mulmxnE !mxE -order_dvdn order_Zp1 Zp_cast.
Qed.

Lemma rank_mx_group m n q : 'r([set: 'M['Z_q]_(m, n)]) = (m * n)%N.
Proof.
wlog q_gt1: q / q > 1 by case: q => [|[|q -> //]] /(_ 2)->.
set G := setT; have cGG: abelian G := zmod_abelian _.
have [mn0 | ] := posnP (m * n).
  by rewrite [G](card1_trivg _) ?rank1 // cardsT card_matrix mn0.
rewrite muln_gt0 => /andP[m_gt0 n_gt0].
have expG: exponent G = q := exponent_mx_group m_gt0 n_gt0 q_gt1.
apply/eqP; rewrite eqn_leq andbC -(leq_exp2l _ _ q_gt1) -{2}expG.
have ->: (q ^ (m * n))%N = #|G| by rewrite cardsT card_matrix card_ord Zp_cast.
rewrite max_card_abelian //= -grank_abelian //= -/G.
pose B : {set 'M['Z_q]_(m, n)} := [set delta_mx ij.1 ij.2 | ij : 'I_m * 'I_n].
suffices ->: G = <<B>>.
  have ->: (m * n)%N = #|{: 'I_m * 'I_n}| by rewrite card_prod !card_ord.
  exact: leq_trans (grank_min _) (leq_imset_card _ _).
apply/setP=> v; rewrite inE (matrix_sum_delta v).
rewrite group_prod // => i _; rewrite group_prod // => j _.
rewrite -[v i j]natr_Zp scaler_nat groupX // mem_gen //.
by apply/imsetP; exists (i, j).
Qed.

Lemma mx_group_homocyclic m n q : homocyclic [set: 'M['Z_q]_(m, n)].
Proof.
wlog q_gt1: q / q > 1 by case: q => [|[|q -> //]] /(_ 2)->.
set G := setT; have cGG: abelian G := zmod_abelian _.
rewrite -max_card_abelian //= rank_mx_group cardsT card_matrix card_ord -/G.
rewrite {1}Zp_cast //; have [-> // | ] := posnP (m * n).
by rewrite muln_gt0 => /andP[m_gt0 n_gt0]; rewrite exponent_mx_group.
Qed.

Lemma abelian_type_mx_group m n q :
  q > 1 -> abelian_type [set: 'M['Z_q]_(m, n)] = nseq (m * n) q.
Proof.
rewrite (abelian_type_homocyclic (mx_group_homocyclic m n q)) rank_mx_group.
have [-> // | ] := posnP (m * n); rewrite muln_gt0 => /andP[m_gt0 n_gt0] q_gt1.
by rewrite exponent_mx_group.
Qed.

End MatrixGroups.

Delimit Scope abelem_scope with Mg.
Open Scope abelem_scope.

Definition abelem_dim' (gT : finGroupType) (E : {set gT}) :=
  (logn (pdiv #|E|) #|E|).-1.
Arguments abelem_dim' {gT} E%g.
Notation "''dim' E" := (abelem_dim' E).+1
  (at level 10, E at level 8, format "''dim'  E") : abelem_scope.

Notation "''rV' ( E )" := 'rV_('dim E)
  (at level 8, format "''rV' ( E )") : abelem_scope.
Notation "''M' ( E )" := 'M_('dim E)
  (at level 8, format "''M' ( E )") : abelem_scope.
Notation "''rV[' F ] ( E )" := 'rV[F]_('dim E)
  (at level 8, only parsing) : abelem_scope.
Notation "''M[' F ] ( E )" := 'M[F]_('dim E)
  (at level 8, only parsing) : abelem_scope.

Section AbelemRepr.

Section FpMatrix.

Variables p m n : nat.
Local Notation Mmn := 'M['F_p]_(m, n).

Lemma mx_Fp_abelem : prime p -> p.-abelem [set: Mmn].
Proof. exact: fin_Fp_lmod_abelem. Qed.

Lemma mx_Fp_stable (L : {group Mmn}) : [acts setT, on L | 'Zm].
Proof.
apply/subsetP=> a _; rewrite !inE; apply/subsetP=> A L_A.
by rewrite inE /= /scale_act -[val _]natr_Zp scaler_nat groupX.
Qed.

End FpMatrix.

Section FpRow.

Variables p n : nat.
Local Notation rVn := 'rV['F_p]_n.

Lemma rowg_mxK (L : {group rVn}) : rowg (rowg_mx L) = L.
Proof. by apply: stable_rowg_mxK; apply: mx_Fp_stable. Qed.

Lemma rowg_mxSK (L : {set rVn}) (M : {group rVn}) :
  (rowg_mx L <= rowg_mx M)%MS = (L \subset M).
Proof.
apply/idP/idP; last exact: rowg_mxS.
by rewrite -rowgS rowg_mxK; apply/subset_trans/sub_rowg_mx.
Qed.

Lemma mxrank_rowg (L : {group rVn}) :
  prime p -> \rank (rowg_mx L) = logn p #|L|.
Proof.
by move=> p_pr; rewrite -{2}(rowg_mxK L) card_rowg card_Fp ?pfactorK.
Qed.

End FpRow.

Variables (p : nat) (gT : finGroupType) (E : {group gT}).
Hypotheses (abelE : p.-abelem E) (ntE : E :!=: 1%g).

Let pE : p.-group E := abelem_pgroup abelE.
Let p_pr : prime p. Proof. by have [] := pgroup_pdiv pE ntE. Qed.

Local Notation n' := (abelem_dim' (gval E)).
Local Notation n := n'.+1.
Local Notation rVn := 'rV['F_p](gval E).

Lemma dim_abelemE : n = logn p #|E|.
Proof.
rewrite /n'; have [_ _ [k ->]] :=  pgroup_pdiv pE ntE.
by rewrite /pdiv primes_exp ?primes_prime // pfactorK.
Qed.

Lemma card_abelem_rV : #|rVn| = #|E|.
Proof.
by rewrite dim_abelemE card_matrix mul1n card_Fp // -p_part part_pnat_id.
Qed.

Lemma isog_abelem_rV : E \isog [set: rVn].
Proof.
by rewrite (isog_abelem_card _ abelE) cardsT card_abelem_rV mx_Fp_abelem /=.
Qed.

Local Notation ab_rV_P := (existsP isog_abelem_rV).
Definition abelem_rV : gT -> rVn := xchoose ab_rV_P.

Local Notation ErV := abelem_rV.

Lemma abelem_rV_M : {in E &, {morph ErV : x y / (x * y)%g >-> x + y}}.
Proof. by case/misomP: (xchooseP ab_rV_P) => fM _; move/morphicP: fM. Qed.

Canonical abelem_rV_morphism := Morphism abelem_rV_M.

Lemma abelem_rV_isom : isom E setT ErV.
Proof. by case/misomP: (xchooseP ab_rV_P). Qed.

Lemma abelem_rV_injm : 'injm ErV. Proof. by case/isomP: abelem_rV_isom. Qed.

Lemma abelem_rV_inj : {in E &, injective ErV}.
Proof. by apply/injmP; apply: abelem_rV_injm. Qed.

Lemma im_abelem_rV : ErV @* E = setT. Proof. by case/isomP: abelem_rV_isom. Qed.

Lemma mem_im_abelem_rV u : u \in ErV @* E.
Proof. by rewrite im_abelem_rV inE. Qed.

Lemma sub_im_abelem_rV mA : subset mA (mem (ErV @* E)).
Proof. by rewrite unlock; apply/pred0P=> v /=; rewrite mem_im_abelem_rV. Qed.
Hint Resolve mem_im_abelem_rV sub_im_abelem_rV : core.

Lemma abelem_rV_1 : ErV 1 = 0%R. Proof. by rewrite morph1. Qed.

Lemma abelem_rV_X x i : x \in E -> ErV (x ^+ i) = i%:R *: ErV x.
Proof. by move=> Ex; rewrite morphX // scaler_nat. Qed.

Lemma abelem_rV_V x : x \in E -> ErV x^-1 = - ErV x.
Proof. by move=> Ex; rewrite morphV. Qed.

Definition rVabelem : rVn -> gT := invm abelem_rV_injm.
Canonical rVabelem_morphism := [morphism of rVabelem].
Local Notation rV_E := rVabelem.

Lemma rVabelem0 : rV_E 0 = 1%g. Proof. exact: morph1. Qed.

Lemma rVabelemD : {morph rV_E : u v / u + v >-> (u * v)%g}.
Proof. by move=> u v /=; rewrite -morphM. Qed.

Lemma rVabelemN : {morph rV_E: u / - u >-> (u^-1)%g}.
Proof. by move=> u /=; rewrite -morphV. Qed.

Lemma rVabelemZ (m : 'F_p) : {morph rV_E : u / m *: u >-> (u ^+ m)%g}.
Proof. by move=> u; rewrite /= -morphX -?[(u ^+ m)%g]scaler_nat ?natr_Zp. Qed.

Lemma abelem_rV_K : {in E, cancel ErV rV_E}. Proof. exact: invmE. Qed.

Lemma rVabelemK : cancel rV_E ErV. Proof. by move=> u; rewrite invmK. Qed.

Lemma rVabelem_inj : injective rV_E. Proof. exact: can_inj rVabelemK. Qed.

Lemma rVabelem_injm : 'injm rV_E. Proof. exact: injm_invm abelem_rV_injm. Qed.

Lemma im_rVabelem : rV_E @* setT = E.
Proof. by rewrite -im_abelem_rV im_invm. Qed.

Lemma mem_rVabelem u : rV_E u \in E.
Proof. by rewrite -im_rVabelem mem_morphim. Qed.

Lemma sub_rVabelem L : rV_E @* L \subset E.
Proof. by rewrite -[_ @* L]morphimIim im_invm subsetIl. Qed.
Hint Resolve mem_rVabelem sub_rVabelem : core.

Lemma card_rVabelem L : #|rV_E @* L| = #|L|.
Proof. by rewrite card_injm ?rVabelem_injm. Qed.

Lemma abelem_rV_mK (H : {set gT}) : H \subset E -> rV_E @* (ErV @* H) = H.
Proof. exact: morphim_invm abelem_rV_injm H. Qed.

Lemma rVabelem_mK L : ErV @* (rV_E @* L) = L.
Proof. by rewrite morphim_invmE morphpreK. Qed.

Lemma rVabelem_minj : injective (morphim (MorPhantom rV_E)).
Proof. exact: can_inj rVabelem_mK. Qed.

Lemma rVabelemS L M : (rV_E @* L \subset rV_E @* M) = (L \subset M).
Proof. by rewrite injmSK ?rVabelem_injm. Qed.

Lemma abelem_rV_S (H K : {set gT}) :
  H \subset E -> (ErV @* H \subset ErV @* K) = (H \subset K).
Proof. by move=> sHE; rewrite injmSK ?abelem_rV_injm. Qed.

Lemma sub_rVabelem_im L (H : {set gT}) :
  (rV_E @* L \subset H) = (L \subset ErV @* H).
Proof. by rewrite sub_morphim_pre ?morphpre_invm. Qed.

Lemma sub_abelem_rV_im (H : {set gT}) (L : {set 'rV['F_p]_n}) :
  H \subset E -> (ErV @* H \subset L) = (H \subset rV_E @* L).
Proof. by move=> sHE; rewrite sub_morphim_pre ?morphim_invmE. Qed.

Section OneGroup.

Variable G : {group gT}.
Definition abelem_mx_fun (g : subg_of G) v := ErV ((rV_E v) ^ val g).
Definition abelem_mx of G \subset 'N(E) :=
  fun x => lin1_mx (abelem_mx_fun (subg G x)).

Hypothesis nEG : G \subset 'N(E).
Local Notation r := (abelem_mx nEG).

Fact abelem_mx_linear_proof g : linear (abelem_mx_fun g).
Proof.
rewrite /abelem_mx_fun; case: g => x /= /(subsetP nEG) Nx /= m u v.
rewrite rVabelemD rVabelemZ conjMg conjXg.
by rewrite abelem_rV_M ?abelem_rV_X ?groupX ?memJ_norm // natr_Zp.
Qed.
Canonical abelem_mx_linear g := Linear (abelem_mx_linear_proof g).

Let rVabelemJmx v x : x \in G -> rV_E (v *m r x) = (rV_E v) ^ x.
Proof.
move=> Gx; rewrite /= mul_rV_lin1 /= /abelem_mx_fun subgK //.
by rewrite abelem_rV_K // memJ_norm // (subsetP nEG).
Qed.

Fact abelem_mx_repr : mx_repr G r.
Proof.
split=> [|x y Gx Gy]; apply/row_matrixP=> i; apply: rVabelem_inj.
  by rewrite rowE -row1 rVabelemJmx // conjg1.
by rewrite !rowE mulmxA !rVabelemJmx ?groupM // conjgM.
Qed.
Canonical abelem_repr := MxRepresentation abelem_mx_repr.
Let rG := abelem_repr.

Lemma rVabelemJ v x : x \in G -> rV_E (v *m rG x) = (rV_E v) ^ x.
Proof. exact: rVabelemJmx. Qed.

Lemma abelem_rV_J : {in E & G, forall x y, ErV (x ^ y) = ErV x *m rG y}.
Proof.
by move=> x y Ex Gy; rewrite -{1}(abelem_rV_K Ex) -rVabelemJ ?rVabelemK.
Qed.

Lemma abelem_rowgJ m (A : 'M_(m, n)) x :
  x \in G -> rV_E @* rowg (A *m rG x) = (rV_E @* rowg A) :^ x.
Proof.
move=> Gx; apply: (canRL (conjsgKV _)); apply/setP=> y.
rewrite mem_conjgV !morphim_invmE !inE memJ_norm ?(subsetP nEG) //=.
apply: andb_id2l => Ey; rewrite abelem_rV_J //.
by rewrite submxMfree // row_free_unit (repr_mx_unit rG).
Qed.

Lemma rV_abelem_sJ (L : {group gT}) x :
  x \in G -> L \subset E -> ErV @* (L :^ x) = rowg (rowg_mx (ErV @* L) *m rG x).
Proof.
move=> Gx sLE; apply: rVabelem_minj; rewrite abelem_rowgJ //.
by rewrite rowg_mxK !morphim_invm // -(normsP nEG x Gx) conjSg.
Qed.

Lemma rstab_abelem m (A : 'M_(m, n)) : rstab rG A = 'C_G(rV_E @* rowg A).
Proof.
apply/setP=> x; rewrite !inE /=; apply: andb_id2l => Gx.
apply/eqP/centP=> cAx => [_ /morphimP[u _ Au ->]|].
  move: Au; rewrite inE => /submxP[u' ->] {u}.
  by apply/esym/commgP/conjg_fixP; rewrite -rVabelemJ -?mulmxA ?cAx.
apply/row_matrixP=> i; apply: rVabelem_inj.
by rewrite row_mul rVabelemJ // /conjg -cAx ?mulKg ?mem_morphim // inE row_sub.
Qed.

Lemma rstabs_abelem m (A : 'M_(m, n)) : rstabs rG A = 'N_G(rV_E @* rowg A).
Proof.
apply/setP=> x; rewrite !inE /=; apply: andb_id2l => Gx.
by rewrite -rowgS -rVabelemS abelem_rowgJ.
Qed.

Lemma rstabs_abelemG (L : {group gT}) :
  L \subset E -> rstabs rG (rowg_mx (ErV @* L)) = 'N_G(L).
Proof. by move=> sLE; rewrite rstabs_abelem rowg_mxK morphim_invm. Qed.

Lemma mxmodule_abelem m (U : 'M['F_p]_(m, n)) :
  mxmodule rG U = (G \subset 'N(rV_E @* rowg U)).
Proof. by rewrite -subsetIidl -rstabs_abelem. Qed.

Lemma mxmodule_abelemG (L : {group gT}) :
  L \subset E -> mxmodule rG (rowg_mx (ErV @* L)) = (G \subset 'N(L)).
Proof. by move=> sLE; rewrite -subsetIidl -rstabs_abelemG. Qed.

Lemma mxsimple_abelemP (U : 'M['F_p]_n) :
  reflect (mxsimple rG U) (minnormal (rV_E @* rowg U) G).
Proof.
apply: (iffP mingroupP) => [[/andP[ntU modU] minU] | [modU ntU minU]].
  split=> [||V modV sVU ntV]; first by rewrite mxmodule_abelem.
    by apply: contraNneq ntU => ->; rewrite /= rowg0 morphim1.
  rewrite -rowgS -rVabelemS [_ @* rowg V]minU //.
    rewrite -subG1 sub_rVabelem_im morphim1 subG1 trivg_rowg ntV /=.
    by rewrite -mxmodule_abelem.
  by rewrite rVabelemS rowgS.
split=> [|D /andP[ntD nDG sDU]].
  rewrite -subG1 sub_rVabelem_im morphim1 subG1 trivg_rowg ntU /=.
  by rewrite -mxmodule_abelem.
apply/eqP; rewrite eqEsubset sDU sub_rVabelem_im /= -rowg_mxSK rowgK.
have sDE: D \subset E := subset_trans sDU (sub_rVabelem _).
rewrite minU ?mxmodule_abelemG //.
  by rewrite -rowgS rowg_mxK sub_abelem_rV_im.
by rewrite rowg_mx_eq0 (morphim_injm_eq1 abelem_rV_injm).
Qed.

Lemma mxsimple_abelemGP (L : {group gT}) :
  L \subset E -> reflect (mxsimple rG (rowg_mx (ErV @* L))) (minnormal L G).
Proof.
move/abelem_rV_mK=> {2}<-; rewrite -{2}[_ @* L]rowg_mxK.
exact: mxsimple_abelemP.
Qed.

Lemma abelem_mx_irrP : reflect (mx_irreducible rG) (minnormal E G).
Proof.
by rewrite -[E in minnormal E G]im_rVabelem -rowg1; apply: mxsimple_abelemP.
Qed.

Lemma rfix_abelem (H : {set gT}) :
  H \subset G -> (rfix_mx rG H :=: rowg_mx (ErV @* 'C_E(H)%g))%MS.
Proof.
move/subsetP=> sHG; apply/eqmxP/andP; split.
  rewrite -rowgS rowg_mxK -sub_rVabelem_im // subsetI sub_rVabelem /=.
  apply/centsP=> y /morphimP[v _]; rewrite inE => cGv ->{y} x Gx.
  by apply/commgP/conjg_fixP; rewrite /= -rVabelemJ ?sHG ?(rfix_mxP H _).
rewrite genmxE; apply/rfix_mxP=> x Hx; apply/row_matrixP=> i.
rewrite row_mul rowK; case/morphimP: (enum_valP i) => z Ez /setIP[_ cHz] ->.
by rewrite -abelem_rV_J ?sHG // conjgE (centP cHz) ?mulKg.
Qed.

Lemma rker_abelem : rker rG = 'C_G(E).
Proof. by rewrite /rker rstab_abelem rowg1 im_rVabelem. Qed.

Lemma abelem_mx_faithful : 'C_G(E) = 1%g -> mx_faithful rG.
Proof. by rewrite /mx_faithful rker_abelem => ->. Qed.

End OneGroup.

Section SubGroup.

Variables G H : {group gT}.
Hypotheses (nEG : G \subset 'N(E)) (sHG : H \subset G).
Let nEH := subset_trans sHG nEG.
Local Notation rG := (abelem_repr nEG).
Local Notation rHG := (subg_repr rG sHG).
Local Notation rH := (abelem_repr nEH).

Lemma eq_abelem_subg_repr : {in H, rHG =1 rH}.
Proof.
move=> x Hx; apply/row_matrixP=> i; rewrite !rowE !mul_rV_lin1 /=.
by rewrite /abelem_mx_fun !subgK ?(subsetP sHG).
Qed.

Lemma rsim_abelem_subg : mx_rsim rHG rH.
Proof.
exists 1%:M => // [|x Hx]; first by rewrite row_free_unit unitmx1.
by rewrite mul1mx mulmx1 eq_abelem_subg_repr.
Qed.

Lemma mxmodule_abelem_subg m (U : 'M_(m, n)) : mxmodule rHG U = mxmodule rH U.
Proof.
apply: eq_subset_r => x; rewrite !inE; apply: andb_id2l => Hx.
by rewrite eq_abelem_subg_repr.
Qed.

Lemma mxsimple_abelem_subg U : mxsimple rHG U <-> mxsimple rH U.
Proof.
have eq_modH := mxmodule_abelem_subg; rewrite /mxsimple eq_modH.
by split=> [] [-> -> minU]; split=> // V; have:= minU V; rewrite eq_modH.
Qed.

End SubGroup.

End AbelemRepr.

Arguments rVabelem_inj {p%N gT E%G} abelE ntE [v1%R v2%R] : rename.

Section ModularRepresentation.

Variables (F : fieldType) (p : nat) (gT : finGroupType).
Hypothesis charFp : p \in [char F].
Implicit Types G H : {group gT}.

(* This is Gorenstein, Lemma 2.6.3. *)
Lemma rfix_pgroup_char G H n (rG : mx_representation F G n) :
  n > 0 -> p.-group H -> H \subset G -> rfix_mx rG H != 0.
Proof.
move=> n_gt0 pH sHG; rewrite -(rfix_subg rG sHG).
move: {2}_.+1 (ltnSn (n + #|H|)) {rG G sHG}(subg_repr _ _) => m.
elim: m gT H pH => // m IHm gT' G pG in n n_gt0 *; rewrite ltnS => le_nG_m rG.
apply/eqP=> Gregular; have irrG: mx_irreducible rG.
  apply/mx_irrP; split=> // U modU; rewrite -mxrank_eq0 -lt0n => Unz.
  rewrite /row_full eqn_leq rank_leq_col leqNgt; apply/negP=> ltUn.
  have: rfix_mx (submod_repr modU) G != 0.
    by apply: IHm => //; apply: leq_trans le_nG_m; rewrite ltn_add2r.
  by rewrite -mxrank_eq0 (rfix_submod modU) // Gregular capmx0 linear0 mxrank0.
have{m le_nG_m IHm} faithfulG: mx_faithful rG.
  apply/trivgP/eqP/idPn; set C := _ rG => ntC.
  suffices: rfix_mx (kquo_repr rG) (G / _)%g != 0.
    by rewrite -mxrank_eq0 rfix_quo // Gregular mxrank0.
  apply: (IHm _ _ (morphim_pgroup _ _)) => //.
  by apply: leq_trans le_nG_m; rewrite ltn_add2l ltn_quotient // rstab_sub.
have{Gregular} ntG: G :!=: 1%g.
  apply: contraL n_gt0; move/eqP=> G1; rewrite -leqNgt -(mxrank1 F n).
  rewrite -(mxrank0 F n n) -Gregular mxrankS //; apply/rfix_mxP=> x.
  by rewrite {1}G1 mul1mx => /set1P->; rewrite repr_mx1.
have p_pr: prime p by case/andP: charFp.
have{ntG pG} [z]: {z | z \in 'Z(G) & #[z] = p}; last case/setIP=> Gz cGz ozp.
  apply: Cauchy => //; apply: contraR ntG; rewrite -p'natE // => p'Z.
  have pZ: p.-group 'Z(G) by rewrite (pgroupS (center_sub G)).
  by rewrite (trivg_center_pgroup pG (card1_trivg (pnat_1 pZ p'Z))).
have{cGz} cGz1: centgmx rG (rG z - 1%:M).
  apply/centgmxP=> x Gx; rewrite mulmxBl mulmxBr mulmx1 mul1mx.
  by rewrite -!repr_mxM // (centP cGz).
have{irrG faithfulG cGz1} Urz1: rG z - 1%:M \in unitmx.
  apply: (mx_Schur irrG) cGz1 _; rewrite subr_eq0.
  move/implyP: (subsetP faithfulG z).
  by rewrite !inE Gz mul1mx -order_eq1 ozp -implybNN neq_ltn orbC prime_gt1.
do [case: n n_gt0 => // n' _; set n := n'.+1] in rG Urz1 *.
have charMp: p \in [char 'M[F]_n].
  exact: (rmorph_char (scalar_mx_rmorphism _ _)).
have{Urz1}: Frobenius_aut charMp (rG z - 1) \in GRing.unit by rewrite unitrX.
rewrite (Frobenius_autB_comm _ (commr1 _)) Frobenius_aut1.
by rewrite -[_ (rG z)](repr_mxX rG) // -ozp expg_order repr_mx1 subrr unitr0.
Qed.

Variables (G : {group gT}) (n : nat) (rG : mx_representation F G n).

Lemma pcore_sub_rstab_mxsimple M : mxsimple rG M -> 'O_p(G) \subset rstab rG M.
Proof.
case=> modM nzM simM; have sGpG := pcore_sub p G.
rewrite rfix_mx_rstabC //; set U := rfix_mx _ _.
have:= simM (M :&: U)%MS; rewrite sub_capmx submx_refl.
apply; rewrite ?capmxSl //.
  by rewrite capmx_module // normal_rfix_mx_module ?pcore_normal.
rewrite -(in_submodK (capmxSl _ _)) val_submod_eq0 -submx0.
rewrite -(rfix_submod modM) // submx0 rfix_pgroup_char ?pcore_pgroup //.
by rewrite lt0n mxrank_eq0.
Qed.

Lemma pcore_sub_rker_mx_irr : mx_irreducible rG -> 'O_p(G) \subset rker rG.
Proof. exact: pcore_sub_rstab_mxsimple. Qed.

(* This is Gorenstein, Lemma 3.1.3. *)
Lemma pcore_faithful_mx_irr :
  mx_irreducible rG -> mx_faithful rG -> 'O_p(G) = 1%g.
Proof.
move=> irrG ffulG; apply/trivgP; apply: subset_trans ffulG.
exact: pcore_sub_rstab_mxsimple.
Qed.

End ModularRepresentation.

Section Extraspecial.

Variables (F : fieldType) (gT : finGroupType) (S : {group gT}) (p n : nat).
Hypotheses (pS : p.-group S) (esS : extraspecial S).
Hypothesis oSpn : #|S| = (p ^ n.*2.+1)%N.
Hypotheses (splitF : group_splitting_field F S) (F'S : [char F]^'.-group S).

Let p_pr := extraspecial_prime pS esS.
Let p_gt0 := prime_gt0 p_pr.
Let p_gt1 := prime_gt1 p_pr.
Let oZp := card_center_extraspecial pS esS.

Let modIp' (i : 'I_p.-1) : (i.+1 %% p = i.+1)%N.
Proof. by case: i => i; rewrite /= -ltnS prednK //; apply: modn_small. Qed.

(* This is Aschbacher (34.9), parts (1)-(4). *)
Theorem extraspecial_repr_structure (sS : irrType F S) :
  [/\ #|linear_irr sS| = (p ^ n.*2)%N,
      exists iphi : 'I_p.-1 -> sS, let phi i := irr_repr (iphi i) in
        [/\ injective iphi,
            codom iphi =i ~: linear_irr sS,
            forall i, mx_faithful (phi i),
            forall z, z \in 'Z(S)^# ->
              exists2 w, primitive_root_of_unity p w
                       & forall i, phi i z = (w ^+ i.+1)%:M
          & forall i, irr_degree (iphi i) = (p ^ n)%N]
    & #|sS| = (p ^ n.*2 + p.-1)%N].
Proof.
have [[defPhiS defS'] prZ] := esS; set linS := linear_irr sS.
have nb_lin: #|linS| = (p ^ n.*2)%N.
  rewrite card_linear_irr // -divgS ?der_sub //=.
  by rewrite oSpn defS' oZp expnS mulKn.
have nb_irr: #|sS| = (p ^ n.*2 + p.-1)%N.
  pose Zcl := classes S ::&: 'Z(S).
  have cardZcl: #|Zcl| = p.
    transitivity #|[set [set z] | z in 'Z(S)]|; last first.
      by rewrite card_imset //; apply: set1_inj.
    apply: eq_card => zS; apply/setIdP/imsetP=> [[] | [z]].
      case/imsetP=> z Sz ->{zS} szSZ.
      have Zz: z \in 'Z(S) by rewrite (subsetP szSZ) ?class_refl.
      exists z => //; rewrite inE Sz in Zz.
      apply/eqP; rewrite eq_sym eqEcard sub1set class_refl cards1.
      by rewrite -index_cent1 (setIidPl _) ?indexgg // sub_cent1.
    case/setIP=> Sz cSz ->{zS}; rewrite sub1set inE Sz; split=> //.
    apply/imsetP; exists z; rewrite //.
    apply/eqP; rewrite eqEcard sub1set class_refl cards1.
    by rewrite -index_cent1 (setIidPl _) ?indexgg // sub_cent1.
  move/eqP: (class_formula S); rewrite (bigID (mem Zcl)) /=.
  rewrite (eq_bigr (fun _ => 1%N)) => [|zS]; last first.
    case/andP=> _ /setIdP[/imsetP[z Sz ->{zS}] /subsetIP[_ cSzS]].
    rewrite (setIidPl _) ?indexgg // sub_cent1 (subsetP cSzS) //.
    exact: mem_repr (class_refl S z).
  rewrite sum1dep_card setIdE (setIidPr _) 1?cardsE ?cardZcl; last first.
    by apply/subsetP=> zS; rewrite 2!inE => /andP[].
  have pn_gt0: p ^ n.*2 > 0 by rewrite expn_gt0 p_gt0.
  rewrite card_irr // oSpn expnS -(prednK pn_gt0) mulnS eqn_add2l.
  rewrite (eq_bigr (fun _ => p)) => [|xS]; last first.
    case/andP=> SxS; rewrite inE SxS; case/imsetP: SxS => x Sx ->{xS} notZxS.
    have [y Sy ->] := repr_class S x; apply: p_maximal_index => //.
    apply: cent1_extraspecial_maximal => //; first exact: groupJ.
    apply: contra notZxS => Zxy; rewrite -{1}(lcoset_id Sy) class_lcoset.
    rewrite ((_ ^: _ =P [set x ^ y])%g _) ?sub1set // eq_sym eqEcard.
    rewrite sub1set class_refl cards1 -index_cent1 (setIidPl _) ?indexgg //.
    by rewrite sub_cent1; apply: subsetP Zxy; apply: subsetIr.
  rewrite sum_nat_cond_const mulnC eqn_pmul2l //; move/eqP <-.
  rewrite addSnnS prednK // -cardZcl -[card _](cardsID Zcl) /= addnC.
  by congr (_ + _)%N; apply: eq_card => t; rewrite !inE andbC // andbAC andbb.
have fful_nlin i: i \in ~: linS -> mx_faithful (irr_repr i).
  rewrite !inE => nlin_phi.
  apply/trivgP; apply: (TI_center_nil (pgroup_nil pS) (rker_normal _)).
  rewrite setIC; apply: (prime_TIg prZ); rewrite /= -defS' der1_sub_rker //.
  exact: socle_irr.
have [i0 nlin_i0]: exists i0, i0 \in ~: linS.
  by apply/card_gt0P; rewrite cardsCs setCK nb_irr nb_lin addKn -subn1 subn_gt0.
have [z defZ]: exists z, 'Z(S) = <[z]> by apply/cyclicP; rewrite prime_cyclic.
have Zz: z \in 'Z(S) by [rewrite defZ cycle_id]; have [Sz cSz] := setIP Zz.
have ozp: #[z] = p by rewrite -oZp defZ.
have ntz: z != 1%g by rewrite -order_gt1 ozp.
pose phi := irr_repr i0; have irr_phi: mx_irreducible phi := socle_irr i0.
pose w := irr_mode i0 z.
have phi_z: phi z = w%:M by rewrite /phi irr_center_scalar.
have phi_ze e: phi (z ^+ e)%g = (w ^+ e)%:M.
  by rewrite /phi irr_center_scalar ?groupX ?irr_modeX.
have wp1: w ^+ p = 1 by rewrite -irr_modeX // -ozp expg_order irr_mode1.
have injw: {in 'Z(S) &, injective (irr_mode i0)}.
  move=> x y Zx Zy /= eq_xy; have [[Sx _] [Sy _]] := (setIP Zx, setIP Zy).
  apply: mx_faithful_inj (fful_nlin _ nlin_i0) _ _ Sx Sy _.
  by rewrite !{1}irr_center_scalar ?eq_xy; first by split.
have prim_w e: 0 < e < p -> p.-primitive_root (w ^+ e).
  case/andP=> e_gt0 lt_e_p; apply/andP; split=> //.
  apply/eqfunP=> -[d ltdp] /=; rewrite unity_rootE -exprM.
  rewrite -(irr_mode1 i0) -irr_modeX // (inj_in_eq injw) ?groupX ?group1 //.
  rewrite -order_dvdn ozp Euclid_dvdM // gtnNdvd //=.
  move: ltdp; rewrite leq_eqVlt.
  by case: eqP => [-> _ | _ ltd1p]; rewrite (dvdnn, gtnNdvd).
have /cyclicP[a defAutZ]: cyclic (Aut 'Z(S)) by rewrite Aut_prime_cyclic ?ozp.
have phi_unitP (i : 'I_p.-1): (i.+1%:R : 'Z_#[z]) \in GRing.unit.
  by rewrite unitZpE ?order_gt1 // ozp prime_coprime // -lt0n !modIp'.
pose ephi i := invm (injm_Zpm a) (Zp_unitm (FinRing.Unit _ (phi_unitP i))).
pose j : 'Z_#[z] := val (invm (injm_Zp_unitm z) a).
have co_j_p: coprime j p.
  rewrite coprime_sym /j; case: (invm _ a) => /=.
  by rewrite ozp /GRing.unit /= Zp_cast.
have [alpha Aut_alpha alphaZ] := center_aut_extraspecial pS esS co_j_p.
have alpha_i_z i: ((alpha ^+ ephi i) z = z ^+ i.+1)%g.
  transitivity ((a ^+ ephi i) z)%g.
    elim: (ephi i : nat) => // e IHe; rewrite !expgS !permM alphaZ //.
    have Aut_a: a \in Aut 'Z(S) by rewrite defAutZ cycle_id.
    rewrite -{2}[a](invmK (injm_Zp_unitm z)); last by rewrite im_Zp_unitm -defZ.
    rewrite /= autE ?cycle_id // -/j /= /cyclem.
    rewrite -(autmE (groupX _ Aut_a)) -(autmE (groupX _ Aut_alpha)).
    by rewrite !morphX //= !autmE IHe.
  rewrite [(a ^+ _)%g](invmK (injm_Zpm a)) /=; last first.
    by rewrite im_Zpm -defAutZ defZ Aut_aut.
  by rewrite autE ?cycle_id //= val_Zp_nat ozp ?modIp'.
have rphiP i: S :==: autm (groupX (ephi i) Aut_alpha) @* S by rewrite im_autm.
pose rphi i := morphim_repr (eqg_repr phi (rphiP i)) (subxx S).
have rphi_irr i: mx_irreducible (rphi i) by apply/morphim_mx_irr/eqg_mx_irr.
have rphi_fful i: mx_faithful (rphi i).
  rewrite /mx_faithful rker_morphim rker_eqg.
  by rewrite (trivgP (fful_nlin _ nlin_i0)) morphpreIdom; apply: injm_autm.
have rphi_z i: rphi i z = (w ^+ i.+1)%:M.
  by rewrite /rphi [phi]lock /= /morphim_mx autmE alpha_i_z -lock phi_ze.
pose iphi i := irr_comp sS (rphi i); pose phi_ i := irr_repr (iphi i).
have{phi_ze} phi_ze i e: phi_ i (z ^+ e)%g = (w ^+ (e * i.+1)%N)%:M.
  rewrite /phi_ !{1}irr_center_scalar ?groupX ?irr_modeX //.
  suffices ->: irr_mode (iphi i) z = w ^+ i.+1 by rewrite mulnC exprM.
  have:= mx_rsim_sym (rsim_irr_comp sS F'S (rphi_irr i)).
  case/mx_rsim_def=> B [B' _ homB]; rewrite /irr_mode homB // rphi_z.
  rewrite -{1}scalemx1 -scalemxAr -scalemxAl -{1}(repr_mx1 (rphi i)).
  by rewrite -homB // repr_mx1 scalemx1 mxE.
have inj_iphi: injective iphi.
  move=> i1 i2 eqi12; apply/eqP.
  move/eqP: (congr1 (fun i => irr_mode i (z ^+ 1)) eqi12).
  rewrite /irr_mode !{1}[irr_repr _ _]phi_ze !{1}mxE !mul1n.
  by rewrite (eq_prim_root_expr (prim_w 1%N p_gt1)) !modIp'.
have deg_phi i: irr_degree (iphi i) = irr_degree i0.
  by case: (rsim_irr_comp sS F'S (rphi_irr i)).
have im_iphi: codom iphi =i ~: linS.
  apply/subset_cardP; last apply/subsetP=> _ /codomP[i ->].
    by rewrite card_image // card_ord cardsCs setCK nb_irr nb_lin addKn.
  by rewrite !inE /= (deg_phi i) in nlin_i0 *.
split=> //; exists iphi; rewrite -/phi_.
split=> // [i | ze | i].
- have sim_i := rsim_irr_comp sS F'S (rphi_irr i).
  by rewrite -(mx_rsim_faithful sim_i) rphi_fful.
- rewrite {1}defZ 2!inE andbC; case/andP.
  case/cyclePmin=> e; rewrite ozp => lt_e_p ->{ze}.
  case: (posnP e) => [-> | e_gt0 _]; first by rewrite eqxx.
  exists (w ^+ e) => [|i]; first by rewrite prim_w ?e_gt0.
  by rewrite phi_ze exprM.
rewrite deg_phi {i}; set d := irr_degree i0.
apply/eqP; move/eqP: (sum_irr_degree sS F'S splitF).
rewrite (bigID (mem linS)) /= -/irr_degree.
rewrite (eq_bigr (fun _ => 1%N)) => [|i]; last by rewrite !inE; move/eqP->.
rewrite sum1_card nb_lin.
rewrite (eq_bigl (mem (codom iphi))) // => [|i]; last first.
  by rewrite -in_setC -im_iphi.
rewrite (eq_bigr (fun _ => d ^ 2))%N => [|_ /codomP[i ->]]; last first.
  by rewrite deg_phi.
rewrite sum_nat_const card_image // card_ord oSpn (expnS p) -{3}[p]prednK //.
rewrite mulSn eqn_add2l eqn_pmul2l; last by rewrite -ltnS prednK.
by rewrite -muln2 expnM eqn_sqr.
Qed.

(* This is the corolloray of the above that is actually used in the proof of  *)
(* B & G, Theorem 2.5. It encapsulates the dependency on a socle of the       *)
(* regular representation.                                                    *)

Variables (m : nat) (rS : mx_representation F S m) (U : 'M[F]_m).
Hypotheses (simU :  mxsimple rS U) (ffulU : rstab rS U == 1%g).
Let sZS := center_sub S.
Let rZ := subg_repr rS sZS.

Lemma faithful_repr_extraspecial :
 \rank U = (p ^ n)%N /\
   (forall V, mxsimple rS V -> mx_iso rZ U V -> mx_iso rS U V).
Proof.
suffices IH V: mxsimple rS V -> mx_iso rZ U V ->
  [&& \rank U == (p ^ n)%N & mxsimple_iso rS U V].
- split=> [|/= V simV isoUV].
    by case/andP: (IH U simU (mx_iso_refl _ _)) => /eqP.
  by case/andP: (IH V simV isoUV) => _ /(mxsimple_isoP simU).
move=> simV isoUV; wlog sS: / irrType F S by apply: socle_exists.
have [[_ defS'] prZ] := esS.
have{prZ} ntZ: 'Z(S) :!=: 1%g by case: eqP prZ => // ->; rewrite cards1.
have [_ [iphi]] := extraspecial_repr_structure sS.
set phi := fun i => _ => [] [inj_phi im_phi _ phiZ dim_phi] _.
have [modU nzU _]:= simU; pose rU := submod_repr modU.
have nlinU: \rank U != 1%N.
  apply/eqP=> /(rker_linear rU); apply/negP; rewrite /rker rstab_submod.
  by rewrite (eqmx_rstab _ (val_submod1 _)) (eqP ffulU) defS' subG1.
have irrU: mx_irreducible rU by apply/submod_mx_irr.
have rsimU := rsim_irr_comp sS F'S irrU.
set iU := irr_comp sS rU in rsimU; have [_ degU _ _]:= rsimU.
have phiUP: iU \in codom iphi by rewrite im_phi !inE -degU.
rewrite degU -(f_iinv phiUP) dim_phi eqxx /=; apply/(mxsimple_isoP simU).
have [modV _ _]:= simV; pose rV := submod_repr modV.
have irrV: mx_irreducible rV by apply/submod_mx_irr.
have rsimV := rsim_irr_comp sS F'S irrV.
set iV := irr_comp sS rV in rsimV; have [_ degV _ _]:= rsimV.
have phiVP: iV \in codom iphi by rewrite im_phi !inE -degV -(mxrank_iso isoUV).
pose jU := iinv phiUP; pose jV := iinv phiVP.
have [z Zz ntz]:= trivgPn _ ntZ.
have [|w prim_w phi_z] := phiZ z; first by rewrite 2!inE ntz.
suffices eqjUV: jU == jV.
  apply/(mx_rsim_iso modU modV); apply: mx_rsim_trans rsimU _.
  by rewrite -(f_iinv phiUP) -/jU (eqP eqjUV) f_iinv; apply: mx_rsim_sym.
have rsimUV: mx_rsim (subg_repr (phi jU) sZS) (subg_repr (phi jV) sZS).
  have [bU _ bUfree bUhom] := mx_rsim_sym rsimU.
  have [bV _ bVfree bVhom] := rsimV.
  have modUZ := mxmodule_subg sZS modU; have modVZ := mxmodule_subg sZS modV.
  case/(mx_rsim_iso modUZ modVZ): isoUV => [bZ degZ bZfree bZhom].
  rewrite /phi !f_iinv; exists (bU *m bZ *m bV)=> [||x Zx].
  - by rewrite -degU degZ degV.
  - by rewrite /row_free !mxrankMfree.
  have Sx := subsetP sZS x Zx.
  by rewrite 2!mulmxA bUhom // -(mulmxA _ _ bZ) bZhom // -4!mulmxA bVhom.
have{rsimUV} [B [B' _ homB]] := mx_rsim_def rsimUV.
have:= eqxx (irr_mode (iphi jU) z); rewrite /irr_mode; set i0 := Ordinal _.
rewrite {2}[_ z]homB // ![_ z]phi_z mxE mulr1n -scalemx1 -scalemxAr -scalemxAl.
rewrite -(repr_mx1 (subg_repr (phi jV) sZS)) -{B B'}homB // repr_mx1 scalemx1.
by rewrite mxE (eq_prim_root_expr prim_w) !modIp'.
Qed.

End Extraspecial.

author: gares

repo: mathcomp

save_path: github-repos/coq/gares-mathcomp


text:
Require Export Logic.

Fixpoint evenb (n:nat) : bool :=
  match n with
  | O        => true
  | S O      => false
  | S (S n') => evenb n'
  end.

Definition even (n:nat) : Prop :=
  evenb n = true.

Inductive ev : nat -> Prop :=
  | ev_0 : ev O
  | ev_SS : forall n:nat, ev n -> ev (S (S n)).

Definition double n := n * 2.

Theorem double_even : forall n,
  ev (double n).
Proof.
induction n.
apply ev_0.
simpl.
apply ev_SS.
apply IHn.
Qed.

Inductive beautiful : nat -> Prop :=
  b_0   : beautiful 0
| b_3   : beautiful 3
| b_5   : beautiful 5
| b_sum : forall n m, beautiful n -> beautiful m -> beautiful (n+m).

Theorem three_is_beautiful: beautiful 3.
Proof.
   apply b_3.
Qed.

Theorem eight_is_beautiful: beautiful 8.
Proof.
   apply b_sum with (n:=3) (m:=5).
   apply b_3.
   apply b_5.
Qed.

Theorem beautiful_plus_eight: forall n, beautiful n -> beautiful (8+n).
Proof.
  intros n B.
  apply b_sum with (n:=8) (m:=n).
  apply eight_is_beautiful.
  apply B.
Qed.

Theorem b_times2: forall n, beautiful n -> beautiful (2*n).
Proof.
intros.
simpl.
apply b_sum.
apply H.
apply b_sum.
apply H.
apply b_0.
Qed.

Theorem b_timesm: forall n m, beautiful n -> beautiful (m*n).
Proof.
intros.
induction m.
simpl.
apply b_0.
apply b_sum.
apply H.
apply IHm.
Qed.

Inductive gorgeous : nat -> Prop :=
  g_0 : gorgeous 0
| g_plus3 : forall n, gorgeous n -> gorgeous (3+n)
| g_plus5 : forall n, gorgeous n -> gorgeous (5+n).

Theorem gorgeous_plus13: forall n,
  gorgeous n -> gorgeous (13+n).
Proof.
intros.
apply g_plus5 with (n:= (8 + n)).
apply g_plus3 with (n:= (5 + n)).
apply g_plus5.
apply H.
Qed.

Theorem gorgeous__beautiful : forall n,
  gorgeous n -> beautiful n.
Proof.
intros.
induction H.
apply b_0.
apply b_sum.
apply b_3.
apply IHgorgeous.
apply b_sum.
apply b_5.
apply IHgorgeous.
Qed.

Theorem gorgeous_sum : forall n m,
  gorgeous n -> gorgeous m -> gorgeous (n + m).
Proof.
intros.
induction H.
simpl.
apply H0.
apply g_plus3.
apply IHgorgeous.
apply g_plus5.
apply IHgorgeous.
Qed.

Theorem beautiful__gorgeous : forall n, beautiful n -> gorgeous n.
Proof.
intros.
induction H.
apply g_0.
apply g_plus3 with (n := 0).
apply g_0.
apply g_plus5 with (n := 0).
apply g_0.
apply gorgeous_sum.
apply IHbeautiful1.
apply IHbeautiful2.
Qed.

Lemma plus_0 : forall n : nat, n + 0 = n.
Proof.
induction n.
reflexivity.
simpl.
rewrite IHn.
reflexivity.
Qed.

Theorem g_times2: forall n, gorgeous n -> gorgeous (2*n).
Proof.
intros n H.
simpl.
induction H.
simpl.
apply g_0.
apply g_plus3.
apply gorgeous_sum.
simpl.
apply H.
apply g_plus3 with (n := (n + 0)).
rewrite -> plus_0.
apply H.
apply gorgeous_sum.
apply g_plus5.
apply H.
apply gorgeous_sum.
apply g_plus5.
apply H.
apply g_0.
Qed.

Theorem ev__even : forall n,
  ev n -> even n.
Proof.
intros n E.
induction E as [| n' E'].
unfold even.
reflexivity.
unfold even.
apply IHE'.
Qed.

Theorem ev_sum : forall n m,
   ev n -> ev m -> ev (n+m).
Proof.
intros.
induction H.
simpl.
apply H0.
simpl.
apply ev_SS.
apply IHev.
Qed.

Theorem ev_minus2: forall n,  ev n -> ev (pred (pred n)).
Proof.
  intros n E.
  inversion E as [| n' E'].
simpl. apply ev_0.
simpl. apply E'.  Qed.

Theorem SSev__even : forall n,
  ev (S (S n)) -> ev n.
Proof.
  intros n E.
  inversion E as [| n' E'].
  apply E'. Qed.

Theorem SSSSev__even : forall n,
  ev (S (S (S (S n)))) -> ev n.
Proof.
intros.
inversion H.
inversion H1.
apply H3.
Qed.

Theorem even5_nonsense :
  ev 5 -> 2 + 2 = 9.
Proof.
intros.
inversion H.
inversion H1.
inversion H3.
Qed.

Theorem ev_ev__ev : forall n m,
  ev (n+m) -> ev n -> ev m.
Proof.
  intros n m E En. generalize dependent E.
  induction En.
simpl.
intros.
apply E.
simpl.
intros.
inversion E.
apply IHEn in H0.
apply H0.
Qed.

Module LeModule.

Inductive le : nat -> nat -> Prop :=
  | le_n : forall n, le n n
  | le_S : forall n m, (le n m) -> (le n (S m)).

Notation "m <= n" := (le m n).

Theorem test_le1 :
  3 <= 3.
Proof.
  apply le_n.  Qed.

Theorem test_le2 :
  3 <= 6.
Proof.
  apply le_S. apply le_S. apply le_S. apply le_n.  Qed.

Theorem test_le3 :
  (2 <= 1) -> 2 + 2 = 5.
Proof.
  intros H. inversion H. inversion H2.  Qed.

End LeModule.

Definition lt (n m:nat) := le (S n) m.

Notation "m < n" := (lt m n).

Inductive square_of : nat -> nat -> Prop :=
  sq : forall n:nat, square_of n (n * n).

Inductive next_nat : nat -> nat -> Prop :=
  | nn : forall n:nat, next_nat n (S n).

Inductive next_even : nat -> nat -> Prop :=
  | ne_1 : forall n, ev (S n) -> next_even n (S n)
  | ne_2 : forall n, ev (S (S n)) -> next_even n (S (S n)).

Lemma le_trans : forall m n o, m <= n -> n <= o -> m <= o.
Proof.
intros m n o H1 H2.
generalize dependent H1.
generalize dependent m.
induction H2.
intros.
apply H1.
intros.
apply le_S.
apply IHle.
apply H1.
Qed.

Theorem O_le_n : forall n,
  0 <= n.
Proof.
intros.
induction n.
apply le_n.
apply le_S.
apply IHn.
Qed.

Theorem n_le_m__Sn_le_Sm : forall n m,
  n <= m -> S n <= S m.
Proof.
intros.
induction H.
apply le_n.
apply le_S.
apply IHle.
Qed.

Theorem Sn_le_Sm__n_le_m : forall n m,
  S n <= S m -> n <= m.
Proof.
intros.
inversion H.
apply le_n.
apply le_trans with (n:= S n).
Theorem n_le_Sn : forall n, n <= S n.
intros.
apply le_S.
apply le_n.
Qed.
apply n_le_Sn.
apply H1.
Qed.

Theorem le_plus_l : forall a b,
  a <= a + b.
Proof.
intros.
induction a.
simpl.
apply O_le_n.
simpl.
apply n_le_m__Sn_le_Sm.
apply IHa.
Qed.

Theorem plus_lt : forall n1 n2 m,
  n1 + n2 < m ->
  n1 < m /\ n2 < m.
Proof.
Admitted.

Theorem lt_S : forall n m,
  n < m ->
  n < S m.
Proof.
intros.
induction H.
simpl.
apply le_S.
apply le_n.
inversion H.
apply le_S.
apply le_S.
apply le_n.
apply le_S.
apply le_S.
apply le_S.
apply H0.
Qed.

Fixpoint ble_nat (n m : nat) {struct n} : bool :=
  match n with
  | O => true
  | S n' =>
      match m with
      | O => false
      | S m' => ble_nat n' m'
      end
  end.

Theorem ble_nat_true : forall n m,
  ble_nat n m = true -> n <= m.
Proof.
intros.
generalize dependent n.
induction m.
destruct n.
simpl.
intros.
apply le_n.
simpl.
intros.
inversion H.
intros.
destruct n.
apply O_le_n.
apply n_le_m__Sn_le_Sm.
apply IHm.
simpl in H.
apply H.
Qed.

Theorem le_ble_nat : forall n m,
  n <= m ->
  ble_nat n m = true.
Proof.
intros.
generalize dependent n.
induction m.
destruct n.
simpl.
intros.
reflexivity.
intros.
inversion H.
intros.
destruct n.
simpl.
reflexivity.
simpl.
apply IHm.
apply Sn_le_Sm__n_le_m.
apply H.
Qed.

Theorem ble_nat_true_trans : forall n m o,
  ble_nat n m = true -> ble_nat m o = true -> ble_nat n o = true.
Proof.
intros.
apply le_ble_nat.
apply le_trans with ( n:= m ).
apply ble_nat_true.
apply H.
apply ble_nat_true.
apply H0.
Qed.

Module R.

Inductive R : nat -> nat -> nat -> Prop :=
   | c1 : R 0 0 0
   | c2 : forall m n o, R m n o -> R (S m) n (S o)
   | c3 : forall m n o, R m n o -> R m (S n) (S o)
   | c4 : forall m n o, R (S m) (S n) (S (S o)) -> R m n o
   | c5 : forall m n o, R m n o -> R n m o.

End R.

Theorem plus_2_2_is_4 :
  2 + 2 = 4.
Proof. simpl. reflexivity.  Qed.

Definition between (n m o: nat) : Prop :=
  andb (ble_nat n o) (ble_nat o m) = true.

Definition teen : nat->Prop := between 13 19.

Definition true_for_zero (P:nat->Prop) : Prop :=
  P 0.

Definition true_for_all_numbers (P:nat->Prop) : Prop :=
  forall n, P n.

Definition preserved_by_S (P:nat->Prop) : Prop :=
  forall n', P n' -> P (S n').

Definition natural_number_induction_valid : Prop :=
  forall (P:nat->Prop),
    true_for_zero P ->
    preserved_by_S P ->
    true_for_all_numbers P.

Inductive ex (X:Type) (P : X -> Prop) : Prop := ex_intro : forall (witness:X), P witness -> ex X P.

Notation "'exists' x , p" := (ex _ (fun x => p))
  (at level 200, x ident, right associativity) : type_scope.
Notation "'exists' x : X , p" := (ex _ (fun x:X => p))
  (at level 200, x ident, right associativity) : type_scope.

Example exists_example_1 : exists n, n + (n * n) = 6.
Proof.
  apply ex_intro with (witness:=2).
  reflexivity. Qed.

Example exists_example_1' : exists n, n + (n * n) = 6.
Proof.
  exists 2.
  reflexivity. Qed.

Theorem exists_example_2 : forall n,(exists m, n = 4 + m) -> (exists o, n = 2 + o).
Proof.
intros.
inversion H as [m Hm].
exists (2 + m).
apply Hm.
Qed.

Lemma exists_example_3 : exists (n:nat), even n /\ beautiful n.
Proof.
exists 8.
split.
unfold even.
simpl.
reflexivity.
apply b_sum with (n := 3) (m := 5).
apply b_3.
apply b_5.
Qed.

Theorem dist_not_exists : forall(X:Type) (P : X -> Prop),
  (forall x, P x) -> ~ (exists x, ~ P x).
Proof.
intros.
unfold not.
intros.
inversion H0.
apply H1.
apply H with (x := witness).
Qed.

Definition excluded_middle := forall P:Prop,
  P \/ ~P.

Theorem not_exists_dist :
  excluded_middle ->
  forall (X:Type) (P : X -> Prop),
    ~ (exists x, ~ P x) -> (forall x, P x).
Proof.
unfold not.
intros.
unfold excluded_middle in H.
assert ((P x) \/ (P x -> False)) as HP.
apply H with (P := P x).
inversion HP.
apply H1.
Theorem ex_falso_quodlibet: forall P : Prop, False -> P.
intros.
inversion H.
Qed.
apply ex_falso_quodlibet.
apply H0.
exists x.
apply H1.
Qed.

Theorem dist_exists_or : forall(X:Type) (P Q : X -> Prop),
  (exists x, P x \/ Q x) <-> (exists x, P x) \/ (exists x, Q x).
Proof.
split.
intros.
inversion H.
inversion H0.
left.
exists witness.
apply H1.
right.
exists witness.
apply H1.
intros.
inversion H.
inversion H0.
exists witness.
left.
apply H1.
inversion H0.
exists witness.
right.
apply H1.
Qed.

Inductive sumbool (A B : Prop) : Set :=
 | left : A -> sumbool A B
 | right : B -> sumbool A B.

Notation "{ A } + { B }" := (sumbool A B) : type_scope.

Theorem eq_nat_dec : forall n m : nat, {n = m} + {~(n = m)}.
Proof.
  intros n.
  induction n as [|n'].
    intros m.
    destruct m as [|m'].
      left. reflexivity.
      right. intros contra. inversion contra.
    intros m.
    destruct m as [|m'].
      right. intros contra. inversion contra.
      destruct IHn' with (m := m') as [eq | neq].
      left. apply f_equal. apply eq.
      right. intros Heq. inversion Heq as [Heq']. apply neq. apply Heq'.
Defined.

author: DanielRrr

repo: Coq-Studies

save_path: github-repos/coq/DanielRrr-Coq-Studies


text:
(**************************************************************************)
(*   Mechanised Framework for Local Interactions & Distributed Algorithms *)
(*   P. Courtieu, L. Rieg, X. Urbain                                      *)
(*   PACTOLE project                                                      *)
(*                                                                        *)
(*   This file is distributed under the terms of the CeCILL-C licence     *)
(*                                                                        *)
(**************************************************************************)

(**************************************************************************)
(**  Mechanised Framework for Local Interactions & Distributed Algorithms

     T. Balabonski, P. Courtieu, L. Rieg, X. Urbain

     PACTOLE project

     This file is distributed under the terms of the CeCILL-C licence.    *)
(**************************************************************************)

Set Implicit Arguments.
Require Import Utf8.
Require Import SetoidDec.
Require Import Pactole.Util.Coqlib.
Require Import Pactole.Util.Bijection.
Require Import Pactole.Util.Ratio.
Require Pactole.Util.Stream.
Require Import Pactole.Core.Identifiers.
Require Import Pactole.Core.State.
Require Import Pactole.Core.Configuration.
Require Import Pactole.Observations.Definition.

Typeclasses eauto := 5.
Remove Hints eq_setoid : typeclass_instances.

Section Formalism.
(* We use explicit names instead of simply `{Observation}
   in order to get meaningful names for implicit arguments. *)
Context {info : Type}.
Context {Loc : Location}.
Context {St : State info}.
Context {N : Names}.
Context {Obs : Observation}.
Variables Trobot Tframe Tactive Tinactive : Type.

(** **  Robograms and Executions  **)

(** Executions are simply streams of configurations. *)
Definition execution := Stream.t configuration.

(** Good robots have a common program, which we call a [robogram].
    It returns some piece of information (e.g. target location) which must form a setoid. *)
Class robot_choice := { robot_choice_Setoid :> Setoid Trobot }.

Record robogram `{robot_choice} := {
  pgm :> observation -> Trobot;
  pgm_compat :> Proper (equiv ==> equiv) pgm}.

Global Instance robogram_Setoid `{robot_choice} : Setoid robogram.
simple refine {| equiv := fun r1 r2 => forall s, pgm r1 s == pgm r2 s |};
try apply robot_choice_Setoid; [].
Proof. split.
+ intros ? ?. reflexivity.
+ intros ? ? ? ?. now symmetry.
+ intros ? ? ? ? ? ?. etransitivity; eauto.
Defined.

Global Instance pgm_full_compat `{robot_choice} : Proper (equiv ==> equiv ==> equiv) pgm.
Proof using .
  intros r1 r2 Hr s1 s2 Hs. rewrite (Hr s1). now apply pgm_compat.
Qed.

(** ** Demonic schedulers *)

(** A [demonic_action] performs four things:
    - it selects which robots are activated,
    - it moves all activated byzantine robots as it wishes,
    - in the look phase, it sets the referential of all activated good robots,
    - in the move phase, it makes some choices about how the robots' states should be updated.

    Therefore, it can make choices at two places: while computing the local frame of reference
    for a robot and while updating robot states.
    These choice points will be represented explicitely as demon choices. *)

(** A [frame_choice] represents the choices made by the demon to compute the observation.
    It must at least contain a bijection to compute the change of frame of reference.  *)
Class frame_choice := {
  frame_choice_bijection : Tframe -> bijection location;
  frame_choice_Setoid :> Setoid Tframe;
  frame_choice_bijection_compat :> Proper (equiv ==> equiv) frame_choice_bijection }.

(** An [update_choice] represents the choices the demon makes after a robot computation. *)
Class update_choice := {
  update_choice_Setoid :> Setoid Tactive;
  update_choice_EqDec :> EqDec update_choice_Setoid }.

(** An [inactive_choice] represents the choices the demon makes when a robot is not activated. *)
Class inactive_choice := {
  inactive_choice_Setoid :> Setoid Tinactive;
  inactive_choice_EqDec :> EqDec inactive_choice_Setoid }.

(** These choices are then used by update functions that depend on the model. *)
(* RMK: we cannot combine them toghether otherwise we get dependencies on the other parameter. *)
Class update_function `{robot_choice} `{frame_choice} `{update_choice} := {
  update : configuration -> G -> Tframe -> Trobot -> Tactive -> info;
  update_compat :> Proper (equiv ==> Logic.eq ==> equiv ==> equiv ==> equiv ==> equiv) update }.

Class inactive_function  `{inactive_choice} := {
  inactive : configuration -> ident -> Tinactive -> info;
  inactive_compat :> Proper (equiv ==> Logic.eq ==> equiv ==> equiv) inactive }.

Context {RC : robot_choice}.
Context {FC : frame_choice}.
Context {UC : update_choice}.
Context {IC : inactive_choice}.
Context {UpdFun : @update_function _ _ _}.
Context {InaFun : @inactive_function _}.

(* NB: The byzantine robots are not always activated
       because fairness depends on all robots, not only good ones. *)
(* RMK: /!\ activate does not take the configuration as argument because we cannot define fairness
            in that case: fairness properties are about a single execution, not a tree of them. *)
Record demonic_action := {
  (** Select which robots are activated *)
  activate : ident -> bool;
  (** Update the state of (activated) byzantine robots *)
  relocate_byz : configuration -> B -> info;
  (** Local referential for (activated) good robots in the compute phase *)
  change_frame : configuration -> G -> Tframe;
  (** Update the state of (activated) good robots in the move phase  *)
  choose_update : configuration -> G -> Trobot -> Tactive;
  (** Update the state of inactive robots *)
  choose_inactive : configuration -> ident -> Tinactive;
  (** The change of frame and its inverse must satisfy the condition to be lifted to states *)
  precondition_satisfied : forall config g,
    precondition (frame_choice_bijection (change_frame config g));
  precondition_satisfied_inv : forall config g,
    precondition ((frame_choice_bijection (change_frame config g)) ⁻¹);
  (** Compatibility properties *)
  activate_compat : Proper (Logic.eq ==> equiv) activate;
  relocate_byz_compat : Proper (equiv ==> Logic.eq ==> equiv) relocate_byz;
  change_frame_compat : Proper (equiv ==> Logic.eq ==> equiv) change_frame;
  choose_update_compat : Proper (equiv ==> Logic.eq ==> equiv ==> equiv) choose_update;
  choose_inactive_compat : Proper (equiv ==> equiv ==> equiv) choose_inactive }.

(** Equivalence relation over [demonic_action]. *)
Global Instance da_Setoid : Setoid demonic_action.
simple refine {| equiv := fun (da1 da2 : demonic_action) =>
     (forall id, da1.(activate) id == da2.(activate) id)
  /\ (forall config b, da1.(relocate_byz) config b == da2.(relocate_byz) config b)
  /\ (forall config g, da1.(change_frame) config g == da2.(change_frame) config g)
  /\ (forall config g pt, da1.(choose_update) config g pt == da2.(choose_update) config g pt)
  /\ (forall config id, da1.(choose_inactive) config id == da2.(choose_inactive) config id) |};
try apply bool_Setoid || apply state_Setoid || apply frame_choice_Setoid
                       || apply update_choice_Setoid || apply inactive_choice_Setoid; [].
Proof. split.
+ repeat split; intuition.
+ intros da1 da2 [? [? [? [? ?]]]]. repeat split; intros; symmetry; auto.
+ intros da1 da2 da3 [? [? [? [? ?]]]] [? [? [? [? ?]]]].
  repeat split; intros; etransitivity; eauto.
Defined.

Global Instance activate_da_compat : Proper (equiv ==> Logic.eq ==> equiv) activate.
Proof using . intros ? ? Hda. repeat intro. now etransitivity; apply Hda || apply activate_compat. Qed.

Global Instance relocate_byz_da_compat : Proper (equiv ==> equiv ==> eq ==> equiv) relocate_byz.
Proof using . intros ?? Hda. repeat intro. now etransitivity; apply Hda || apply relocate_byz_compat. Qed.

Global Instance change_frame_da_compat : Proper (equiv ==> equiv ==> eq ==> equiv) change_frame.
Proof using . intros ?? Hda. repeat intro. now etransitivity; apply Hda || apply change_frame_compat. Qed.

Global Instance choose_update_da_compat :
  Proper (equiv ==> equiv ==> Logic.eq ==> equiv ==> equiv) choose_update.
Proof using . intros ?? Hda. repeat intro. now etransitivity; apply Hda || apply choose_update_compat. Qed.

Global Instance choose_inactive_da_compat :
  Proper (equiv ==> equiv ==> Logic.eq ==> equiv) choose_inactive.
Proof using .
intros ? ? Hda. repeat intro.
now etransitivity; apply Hda || apply choose_inactive_compat.
Qed.

(** Definitions of two subsets of robots: active and idle ones. *)
Definition active da := List.filter (activate da) names.

(* TODO: rename into inactive? *)
Definition idle da := List.filter (fun id => negb (activate da id)) names.

Global Instance active_compat : Proper (equiv ==> Logic.eq) active.
Proof using .
intros da1 da2 Hda.
unfold active. induction names as [| id l]; simpl.
+ reflexivity.
+ destruct (activate da1 id) eqn:Hactivate1, (activate da2 id) eqn:Hactivate2.
  - f_equal. apply IHl.
  - rewrite Hda, Hactivate2 in Hactivate1. discriminate.
  - rewrite Hda, Hactivate2 in Hactivate1. discriminate.
  - apply IHl.
Qed.

Global Instance idle_compat : Proper (equiv ==> Logic.eq) idle.
Proof using .
intros da1 da2 Hda.
unfold idle. induction names as [| id l]; simpl.
+ reflexivity.
+ destruct (activate da1 id) eqn:Hactivate1, (activate da2 id) eqn:Hactivate2.
  - apply IHl.
  - rewrite Hda, Hactivate2 in Hactivate1. discriminate.
  - rewrite Hda, Hactivate2 in Hactivate1. discriminate.
  - simpl. f_equal. apply IHl.
Qed.

Lemma idle_spec : forall da id, List.In id (idle da) <-> activate da id = false.
Proof using .
intros da id. unfold idle. rewrite List.filter_In.
destruct (activate da id); intuition; try discriminate; [].
apply In_names.
Qed.

Lemma active_spec : forall da id, List.In id (active da) <-> activate da id = true.
Proof using .
intros da id. unfold active. rewrite List.filter_In.
destruct (activate da id); intuition; try discriminate; [].
apply In_names.
Qed.

(** A [demon] is just a stream of [demonic_action]s. *)
Definition demon := Stream.t demonic_action.

(** **  One step executions  **)

(** [round r da config] returns the new configuration of robots (that is, a function
    giving the position of each robot) from the previous one [config] by applying
    the robogram [r] on each observation seen by each robot. [da.(relocate_byz)]
    is used for byzantine robots.

    This setting is general enough to accomodate all models we have considered so far. *)
Definition round (r : robogram) (da : demonic_action) (config : configuration) : configuration :=
  (* for a given robot, we compute the new configuration *)
  fun id =>
    let state := config id in
    if da.(activate) id                       (* first see whether the robot is activated *)
    then
      match id with
        | Byz b => da.(relocate_byz) config b (* byzantine robots are relocated by the demon *)
        | Good g =>
          (* change the frame of reference *)
          let frame_choice := da.(change_frame) config g in
          let new_frame := frame_choice_bijection frame_choice in
          let local_config := map_config (lift (existT precondition new_frame
                                                       (precondition_satisfied da config g)))
                                         config in
          let local_state := local_config (Good g) in
          (* compute the observation *)
          let obs := obs_from_config local_config local_state in
          (* apply r on the observation *)
          let local_robot_decision := r obs in
          (* the demon chooses how to perform the state update *)
          let choice := da.(choose_update) local_config g local_robot_decision in
          (* the actual update of the robot state is performed by the update function *)
          let new_local_state := update local_config g frame_choice local_robot_decision choice in
          (* return to the global frame of reference *)
          lift (existT precondition (new_frame ⁻¹) (precondition_satisfied_inv da config g))
               new_local_state
        end
    else inactive config id (da.(choose_inactive) config id).

Global Instance round_compat : Proper (equiv ==> equiv ==> equiv ==> equiv) round.
Proof using .
intros r1 r2 Hr da1 da2 Hda config1 config2 Hconfig id.
unfold round. rewrite Hda. destruct_match.
* (* active robot *)
  destruct id as [g | b].
  + (* good robot *)
    assert (Heq : map_config (lift (existT precondition
                                      (frame_choice_bijection (change_frame da1 config1 g))
                                      (precondition_satisfied da1 config1 g))) config1
               == map_config (lift (existT precondition
                                      (frame_choice_bijection (change_frame da2 config2 g))
                                      (precondition_satisfied da2 config2 g))) config2).
    { f_equiv; trivial; []. apply lift_compat. intros x y Hxy. simpl. f_equiv; trivial; [].
      apply frame_choice_bijection_compat. now f_equiv. }
    apply lift_compat, update_compat.
    - intros ? ? ?. simpl. f_equiv; trivial; []. apply frame_choice_bijection_compat. now f_equiv.
    - apply Heq.
    - reflexivity.
    - now f_equiv.
    - repeat (f_equiv; trivial).
    - repeat (f_equiv; trivial).
  + (* byzantine robot *)
    now f_equiv.
* (* inactive robot *)
  now apply inactive_compat, choose_inactive_da_compat.
Qed.

(** A third subset of robots: moving ones. *)
Definition moving r da config :=
  List.filter
    (fun id => if round r da config id =?= config id then false else true)
    names.

Global Instance moving_compat : Proper (equiv ==> equiv ==> equiv ==> equiv) moving.
Proof using .
intros r1 r2 Hr da1 da2 Hda c1 c2 Hc. unfold moving.
induction names as [| id l]; simpl.
* reflexivity.
* destruct (round r1 da1 c1 id =?= c1 id) as [Heq1 | Heq1],
           (round r2 da2 c2 id =?= c2 id) as [Heq2 | Heq2].
  + apply IHl.
  + elim Heq2. transitivity (round r1 da1 c1 id).
    - symmetry. now apply round_compat.
    - rewrite Heq1. apply Hc.
  + elim Heq1. transitivity (round r2 da2 c2 id).
    - now apply round_compat.
    - rewrite Heq2. symmetry. apply Hc.
  + f_equal. apply IHl.
Qed.

Lemma moving_spec : forall r da config id,
  List.In id (moving r da config) <-> round r da config id =/= config id.
Proof using .
intros r da config id. unfold moving. rewrite List.filter_In.
split; intro Hin.
+ destruct Hin as [_ Hin].
  destruct (round r da config id =?= config id) as [_ | Hneq]; intuition.
+ split.
  - apply In_names.
  - destruct (round r da config id =?= config id) as [Heq | _]; intuition.
Qed.

Lemma no_moving_same_config : forall r da config,
  moving r da config = List.nil -> round r da config == config.
Proof using .
intros r da config Hmove id.
destruct (round r da config id =?= config id) as [Heq | Heq]; trivial; [].
apply <- moving_spec in Heq. rewrite Hmove in Heq. inversion Heq.
Qed.

(** [execute r d config] returns an (infinite) execution from an initial global
    configuration [config], a demon [d] and a robogram [r] running on each good robot. *)
Definition execute (r : robogram) : demon -> configuration -> execution :=
  cofix execute d config :=
  Stream.cons config (execute (Stream.tl d) (round r (Stream.hd d) config)).

(** Decomposition lemmas for [execute]. *)
Lemma execute_hd : forall (r : robogram) (d : demon) (config : configuration),
  Stream.hd (execute r d config) = config.
Proof using . reflexivity. Qed.

Lemma execute_tail : forall (r : robogram) (d : demon) (config : configuration),
  Stream.tl (execute r d config) = execute r (Stream.tl d) (round r (Stream.hd d) config).
Proof using . reflexivity. Qed.

Global Instance execute_compat : Proper (equiv ==> equiv ==> equiv ==> equiv) execute.
Proof using .
intros r1 r2 Hr. coinduction proof.
- simpl. assumption.
- now f_equiv.
- apply round_compat; trivial. now f_equiv.
Qed.

(** **  Execution models  **)

(** ***  Semi-synchronous (SSYNC) model  **)

(* FIXME?: this must hold for all configurations whereas only the current one may be useful *)
(* NB: The precondition is necessary to have the implication FSYNC -> SSYNC.
       We could impose [Tinactive = unit] but this can create problems when comparing settings. *)
Definition SSYNC_da da := forall id, da.(activate) id = false ->
  forall config, inactive config id (da.(choose_inactive) config id) == config id.

Definition SSYNC d := Stream.forever (Stream.instant SSYNC_da) d.

Global Instance SSYNC_da_compat : Proper (equiv ==> iff) SSYNC_da.
Proof using . intros da1 da2 Hda. unfold SSYNC_da. now setoid_rewrite Hda. Qed.

Global Instance SSYNC_compat : Proper (equiv ==> iff) SSYNC.
Proof using . apply Stream.forever_compat, Stream.instant_compat, SSYNC_da_compat. Qed.

(** All moving robots are active.
    This is only true for the SSYNC (and FSYNC) model: in the ASYNC one,
    robots can keep moving while others are activated. *)
Lemma moving_active : forall da, SSYNC_da da ->
  forall r config, List.incl (moving r da config) (active da).
Proof using .
intros da HSSYNC r config id. rewrite moving_spec, active_spec.
unfold round. destruct_match_eq Hcase; intuition.
Qed.

(** If no robot is active, then the configuration does not change. *)
Lemma no_active_same_config : forall da, SSYNC_da da ->
  forall r config, active da = List.nil -> round r da config == config.
Proof using .
intros da HSSYNC r config Hactive.
assert (Hfalse : forall id, activate da id = false).
{ intro id. destruct (activate da id) eqn:Heq; trivial; []. exfalso.
  rewrite <- active_spec, Hactive in Heq. intuition. }
intro id. unfold round. rewrite (Hfalse id). intuition.
Qed.

Lemma SSYNC_round_simplify : forall r da config, SSYNC_da da ->
  round r da config
  == fun id =>
    let state := config id in
    if da.(activate) id
    then
      match id with
        | Byz b => da.(relocate_byz) config b
        | Good g =>
          let frame_choice := da.(change_frame) config g in
          let new_frame := frame_choice_bijection frame_choice in
          let local_config := map_config (lift (existT precondition new_frame
                                                       (precondition_satisfied da config g)))
                                         config in
          let local_state := local_config (Good g) in
          let obs := obs_from_config local_config local_state in
          let local_robot_decision := r obs in
          let choice := da.(choose_update) local_config g local_robot_decision in
          let new_local_state := update local_config g frame_choice local_robot_decision choice in
          lift (existT precondition (new_frame ⁻¹) (precondition_satisfied_inv da config g))
               new_local_state
        end
    else state.
Proof using . unfold round. repeat intro. destruct_match_eq Hcase; auto. Qed.

(** ***  Fully-synchronous (FSYNC) model  **)

(** A fully synchronous demon is a particular case of fair demon: all good robots are activated
    at each round. In our setting this means that the [activate] function is always true. *)

Definition FSYNC_da da := forall id, da.(activate) id = true.

Definition FSYNC d := Stream.forever (Stream.instant FSYNC_da) d.

Global Instance FSYNC_da_compat : Proper (equiv ==> iff) FSYNC_da.
Proof using . intros da1 da2 Hda. unfold FSYNC_da. now setoid_rewrite Hda. Qed.

Global Instance FSYNC_compat : Proper (equiv ==> iff) FSYNC.
Proof using . apply Stream.forever_compat, Stream.instant_compat, FSYNC_da_compat. Qed.

Lemma FSYNC_SSYNC_da : forall da, FSYNC_da da -> SSYNC_da da.
Proof using . unfold FSYNC_da, SSYNC_da. intuition. congruence. Qed.

Theorem FSYNC_SSYNC : forall d, FSYNC d -> SSYNC d.
Proof using . apply Stream.forever_impl_compat, Stream.instant_impl_compat, FSYNC_SSYNC_da. Qed.

Lemma FSYNC_round_simplify : forall r da config, FSYNC_da da ->
  round r da config
  == fun id =>
    let state := config id in
    match id with
      | Byz b => da.(relocate_byz) config b
      | Good g =>
        let frame_choice := da.(change_frame) config g in
        let new_frame := frame_choice_bijection frame_choice in
        let local_config := map_config (lift (existT precondition new_frame
                                                     (precondition_satisfied da config g)))
                                       config in
        let local_state := local_config (Good g) in
        let obs := obs_from_config local_config local_state in
        let local_robot_decision := r obs in
        let choice := da.(choose_update) local_config g local_robot_decision in
        let new_local_state := update local_config g frame_choice local_robot_decision choice in
        lift (existT precondition (new_frame ⁻¹) (precondition_satisfied_inv da config g))
             new_local_state
      end.
Proof using .
intros * HFSYNC. rewrite SSYNC_round_simplify; auto using FSYNC_SSYNC_da; [].
repeat intro. now rewrite HFSYNC.
Qed.

(** **  Fairness  **)

(** A [demon] is [Fair] if at any time it will later activate any robot. *)
(* RMK: This is a stronger version of eventually because P is negated in the Later clause *)
Inductive LocallyFairForOne id (d : demon) : Prop :=
  | NowFair : activate (Stream.hd d) id == true -> LocallyFairForOne id d
  | LaterFair : activate (Stream.hd d) id = false ->
                LocallyFairForOne id (Stream.tl d) -> LocallyFairForOne id d.

Definition Fair : demon -> Prop := Stream.forever (fun d => ∀ id, LocallyFairForOne id d).

(** [Between id id' d] means that [id] will be activated before at most [k]
    steps of [id'] in demon [d]. *)
Inductive Between id id' (d : demon) : nat -> Prop :=
| kReset : forall k, activate (Stream.hd d) id = true -> Between id id' d k
| kReduce : forall k, activate (Stream.hd d) id = false ->
                      activate (Stream.hd d) id' = true ->
                      Between id id' (Stream.tl d) k -> Between id id' d (S k)
| kStall : forall k, activate (Stream.hd d) id = false ->
                     activate (Stream.hd d) id' = false ->
                     Between id id' (Stream.tl d) k -> Between id id' d k.

(** k-fairnes: Every robot is activated within at most k activation of any other robot. *)
Definition kFair k : demon -> Prop := Stream.forever (fun d => forall id id', Between id id' d k).

(** Compatibility properties *)
Local Lemma LocallyFairForOne_compat_aux : forall id d1 d2,
  d1 == d2 -> LocallyFairForOne id d1 -> LocallyFairForOne id d2.
Proof using .
intros id da1 da2 Hda Hfair. revert da2 Hda. induction Hfair; intros da2 Hda;
constructor; solve [now rewrite <- Hda | apply IHHfair; now f_equiv].
Qed.

Global Instance LocallyFairForOne_compat : Proper (Logic.eq ==> equiv ==> iff) LocallyFairForOne.
Proof using .
intros ? ? ? ? ? Heq. subst. split; intro.
- eapply LocallyFairForOne_compat_aux; eauto.
- symmetry in Heq. eapply LocallyFairForOne_compat_aux; eauto.
Qed.

Global Instance Fair_compat : Proper (equiv ==> iff) Fair.
Proof using . apply Stream.forever_compat. intros ? ? Heq. now setoid_rewrite Heq. Qed.

Local Lemma Between_compat_aux : forall id id' k d1 d2,
  d1 == d2 -> Between id id' d1 k -> Between id id' d2 k.
Proof using .
intros id id' k d1 d2 Heq bet. revert d2 Heq. induction bet; intros d2 Heq;
constructor; solve [now rewrite <- Heq | apply IHbet; now f_equiv].
Qed.

Global Instance Between_compat : Proper (eq ==> eq ==> equiv ==> eq ==> iff) Between.
Proof using .
intros ? ? ? ? ? ? ? ? Heq ? ? ?. subst. split; intro.
- now eapply Between_compat_aux; eauto.
- symmetry in Heq. now eapply Between_compat_aux; eauto.
Qed.

Global Instance kFair_compat : Proper (Logic.eq ==> equiv ==> iff) kFair.
Proof using . intros k ??. subst. apply Stream.forever_compat. intros ?? Heq. now setoid_rewrite Heq. Qed.

(** A robot is never activated before itself with a fair demon!
    The fairness hypothesis is necessary, otherwise the robot may never be activated. *)
Lemma Between_same :
  forall id (d : demon) k, LocallyFairForOne id d -> Between id id d k.
Proof using . intros id d k Hd. induction Hd; now econstructor; eauto. Qed.

(** A k-fair demon is fair. *)
Lemma Between_LocallyFair : forall id (d : demon) id' k,
  Between id id' d k -> LocallyFairForOne id d.
Proof using . intros * Hg. induction Hg; now constructor; trivial; firstorder. Qed.

Theorem kFair_Fair : forall k (d : demon), kFair k d -> Fair d.
Proof using .
intro. apply Stream.forever_impl_compat.
intros ? ? id. eauto using (@Between_LocallyFair id _ id).
Qed.

(** [Between g h d k] is monotonic on [k]. *)
Lemma Between_mono : forall id id' (d : demon) k,
  Between id id' d k -> forall k', (k <= k')%nat -> Between id id' d k'.
Proof using .
intros id id' d k Hd. induction Hd; intros k' Hk; auto using Between; [].
destruct k'.
- now inversion Hk.
- constructor; assumption || now (apply IHHd; auto with arith).
Qed.

(** [kFair k d] is monotonic on [k]. *)
Theorem kFair_mono : forall k (d: demon),
  kFair k d -> forall k', (k <= k')%nat -> kFair k' d.
Proof using .
coinduction fair; match goal with H : kFair _ _ |- _ => destruct H end.
- intros. now apply Between_mono with k.
- now apply (fair k).
Qed.

(** A synchronous demon is fair *)
Lemma FSYNC_implies_0Fair: ∀ d, FSYNC d → kFair 0 d.
Proof using . apply Stream.forever_impl_compat. intros s Hs id id'. constructor. apply Hs. Qed.

Corollary FSYNC_implies_fair: ∀ d, FSYNC d → Fair d.
Proof using . intros. now eapply kFair_Fair, FSYNC_implies_0Fair. Qed.

(** If a demon is 0-fair, then the activation states of all robots are the same:
    either all are activated, or none is. *)
Theorem Fair0 : forall d, kFair 0 d ->
  forall id id', (Stream.hd d).(activate) id = (Stream.hd d).(activate) id'.
Proof using .
intros d Hd id id'. destruct Hd as [Hd _].
assert (Hg := Hd id id'). assert (Hh := Hd id' id).
inv Hg; inv Hh;
repeat match goal with
  | H : forall c : configuration, _ |- _ => specialize (H config)
  | H : _ /\ _ |- _ => destruct H
  | |- _ => congruence
end.
Qed.

(** [FirstMove r d config] gives the number of rounds before one robot moves. *)
Inductive FirstMove r (d : demon) (config : configuration) : Prop :=
  | MoveNow : moving r (Stream.hd d) config <> nil -> FirstMove r d config
  | MoveLater : moving r (Stream.hd d) config = nil ->
                FirstMove r (Stream.tl d) (round r (Stream.hd d) config) -> FirstMove r d config.

Global Instance FirstMove_compat : Proper (equiv ==> equiv ==> equiv ==> iff) FirstMove.
Proof using .
intros r1 r2 Hr d1 d2 Hd c1 c2 Hc. split; intro Hfirst.
* revert r2 d2 c2 Hr Hd Hc. induction Hfirst; intros r2 d2 c2 Hr Hd Hc.
  + apply MoveNow. now rewrite <- Hr, <- Hd, <- Hc.
  + apply MoveLater.
    - now rewrite <- Hr, <- Hd, <- Hc.
    - destruct Hd. now apply IHHfirst, round_compat.
* revert r1 d1 c1 Hr Hd Hc. induction Hfirst; intros r1 d1 c1 Hr Hd Hc.
  + apply MoveNow. now rewrite Hr, Hd, Hc.
  + apply MoveLater.
    - now rewrite Hr, Hd, Hc.
    - destruct Hd. apply IHHfirst; trivial. now apply round_compat; f_equiv.
Qed.

End Formalism.

Arguments robogram {info} {_} {_} {_} {_} {Trobot} {_}.
Arguments Build_robogram {info} {_} {_} {_} {_} {Trobot} {_} pgm {_}.
Arguments update_choice_Setoid {_} {_}.
Arguments update_choice_EqDec {_} {_}.
Arguments update_function {info} {_} {_} {_} Trobot Tframe Tactive {_} {_} {_}.
Arguments inactive_function {info} {_} {_} {_} Tinactive {_}.
Arguments update {info} {_} {_} {_} {Trobot} {Tframe} {Tactive} {_} {_} {_} {_}.
Arguments update_compat {info} {_} {_} {_} {Trobot} {Tframe} {Tactive} {_} {_} {_} {_}.
Arguments inactive {info} {_} {_} {_} {Tinactive} {_} {_}.
Arguments inactive_compat {info} {_} {_} {_} {Tinactive} {_} {_}.
Arguments demonic_action {info} {_} {_} {_} {Trobot} {Tframe} {Tactive} {Tinactive} {_} {_} {_} {_}.
Arguments demon {info} {_} {_} {_} {Trobot} {Tframe} {Tactive} {Tinactive} {_} {_} {_} {_}.

Require Import Pactole.Spaces.RealMetricSpace.
Require Import Pactole.Spaces.Similarity.

Section ChoiceExample.
(** **  Most Common Examples of Demon Choices  **)

Context `{State}.
Context {VS : RealVectorSpace location}.

(** An exemple of frame choice: just a bijection. *)
Definition FrameChoiceBijection : frame_choice (bijection location) := {|
  frame_choice_bijection := Datatypes.id;
  frame_choice_Setoid := @bij_Setoid location _;
  frame_choice_bijection_compat := fun _ _ Heq => Heq |}.

(** Similarities as a frame choice, only make sense inside real metric spaces. *)
Definition FirstChoiceSimilarity {RMS : RealMetricSpace location}
  : frame_choice (similarity location) := {|
  frame_choice_bijection := @sim_f location _ _ _ _;
  frame_choice_Setoid := similarity_Setoid;
  frame_choice_bijection_compat := f_compat |}.

(** An exemple of update choice: no choice at all. *)
Definition NoChoice : update_choice unit := {|
  update_choice_Setoid := _;
  update_choice_EqDec := _ |}.

(** Combining two update choices into a choice over a pair. *)
Definition MergeUpdateChoices A B `{update_choice A} `{update_choice B} : update_choice (A * B) :=
  {| update_choice_Setoid := _;
     update_choice_EqDec := _ |}.

(** Idem for inactive choice. *)
Instance NoChoiceIna : inactive_choice unit := {|
  inactive_choice_Setoid := _;
  inactive_choice_EqDec := _ |}.

Definition MergeInactiveChoices A B `{inactive_choice A} `{inactive_choice B}
  : inactive_choice (A * B) := {| inactive_choice_Setoid := _;
                                  inactive_choice_EqDec := _ |}.

Instance NoChoiceInaFun `{Names} : inactive_function unit := {|
  inactive := fun config g _ => config g;
  inactive_compat := ltac:(intros ? ? Heq ? ? ? ? ? ?; subst; apply Heq) |}.

End ChoiceExample.

author: MathisBD


text:
(*
This module shows off different possible definitions of concat_lang and how they are all equivalent
to the defintion we use in Language.v, namely `concat_lang`.
This also includes the tactic `destruct_concat_lang`, which is a useful replacement for the constructor tactic when concat_lang is in the goal.
*)

Require Import CoqStock.DubStep.
Require Import CoqStock.Invs.
Require Import CoqStock.List.
Require Import CoqStock.Listerine.
Require Import CoqStock.Untie.
Require Import CoqStock.WreckIt.

Require Import Brzozowski.Alphabet.
Require Import Brzozowski.Language.
Require Import Brzozowski.Regex.

(*
concat_lang_ex uses exists to define concat,
instead of forall as is done by `concat_lang`.
This is arguably closer to the mathematical definition of concat.

  $(P.Q) = \{ s | s = p.q; p \in P, q \in Q \}$.

*)
Inductive concat_lang_ex (P Q: lang): lang :=
  | mk_concat_ex: forall (s: str),
    (exists
      (p: str)
      (q: str)
      (pqs: p ++ q = s),
      p \in P /\
      q \in Q
    ) ->
    concat_lang_ex P Q s
  .

(*
concat_ex_equivalent shows how `concat_lang_ex` is equivalent to
the main definition of `concat_lang`.
*)
Theorem concat_ex_equivalent (P Q: lang):
  concat_lang_ex P Q {<->} concat_lang P Q.
Proof.
split.
- intros.
  destruct H.
  destruct H as [p [q [H [Hp Hq]]]].
  apply (mk_concat P Q p q s); assumption.
- intros.
  destruct H.
  constructor.
  exists p.
  exists q.
  exists H.
  split; assumption.
Qed.

(*
When concat is in the goal, it can be harder to apply the tactic,
since now some variables need to be provided to mk_concat.
The destruct_concat_lang tactic solves this by replacing the
concat_lang definition with the concat_lang_ex definition,
which can be easily deconstructed.
*)
Ltac destruct_concat_lang :=
  apply concat_ex_equivalent;
  fold denote_regex;
  apply mk_concat_ex.

(* example_destruct_concat_lang shows how the destruct_concat_lang can be used. *)
Example example_destruct_concat_lang:
  forall (p q: regex),
  [] \in {{p}} /\ [] \in {{q}} ->
  [] \in {{concat p q}}.
Proof.
intros.
destruct_concat_lang.
exists [].
exists [].
listerine.
exists eq_refl.
assumption.
Qed.

author: awalterschulze

repo: regex-reexamined-coq