From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 22 May 2019 13:43:08 +0200 Subject: htmldoc regenerated --- docs/htmldoc/mathcomp.fingroup.perm.html | 250 ++++++++++++++++--------------- 1 file changed, 131 insertions(+), 119 deletions(-) (limited to 'docs/htmldoc/mathcomp.fingroup.perm.html') diff --git a/docs/htmldoc/mathcomp.fingroup.perm.html b/docs/htmldoc/mathcomp.fingroup.perm.html index e957ec7..7a984bf 100644 --- a/docs/htmldoc/mathcomp.fingroup.perm.html +++ b/docs/htmldoc/mathcomp.fingroup.perm.html @@ -21,7 +21,6 @@
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.

@@ -65,45 +64,45 @@ Variable T : finType.

-Inductive perm_type : predArgType :=
-  Perm (pval : {ffun T → T}) & injectiveb pval.
+Inductive perm_type : predArgType :=
+  Perm (pval : {ffun T → T}) & injectiveb pval.
Definition pval p := let: Perm f _ := p in f.
-Definition perm_of of phant T := perm_type.
+Definition perm_of of phant T := perm_type.
Identity Coercion type_of_perm : perm_of >-> perm_type.

-Notation pT := (perm_of (Phant T)).
+Notation pT := (perm_of (Phant T)).

-Canonical perm_subType := Eval hnf in [subType for pval].
-Definition perm_eqMixin := Eval hnf in [eqMixin of perm_type by <:].
+Canonical perm_subType := Eval hnf in [subType for pval].
+Definition perm_eqMixin := Eval hnf in [eqMixin of perm_type by <:].
Canonical perm_eqType := Eval hnf in EqType perm_type perm_eqMixin.
-Definition perm_choiceMixin := [choiceMixin of perm_type by <:].
+Definition perm_choiceMixin := [choiceMixin of perm_type by <:].
Canonical perm_choiceType := Eval hnf in ChoiceType perm_type perm_choiceMixin.
-Definition perm_countMixin := [countMixin of perm_type by <:].
+Definition perm_countMixin := [countMixin of perm_type by <:].
Canonical perm_countType := Eval hnf in CountType perm_type perm_countMixin.
-Canonical perm_subCountType := Eval hnf in [subCountType of perm_type].
-Definition perm_finMixin := [finMixin of perm_type by <:].
+Canonical perm_subCountType := Eval hnf in [subCountType of perm_type].
+Definition perm_finMixin := [finMixin of perm_type by <:].
Canonical perm_finType := Eval hnf in FinType perm_type perm_finMixin.
-Canonical perm_subFinType := Eval hnf in [subFinType of perm_type].
+Canonical perm_subFinType := Eval hnf in [subFinType of perm_type].

-Canonical perm_for_subType := Eval hnf in [subType of pT].
-Canonical perm_for_eqType := Eval hnf in [eqType of pT].
-Canonical perm_for_choiceType := Eval hnf in [choiceType of pT].
-Canonical perm_for_countType := Eval hnf in [countType of pT].
-Canonical perm_for_subCountType := Eval hnf in [subCountType of pT].
-Canonical perm_for_finType := Eval hnf in [finType of pT].
-Canonical perm_for_subFinType := Eval hnf in [subFinType of pT].
+Canonical perm_for_subType := Eval hnf in [subType of pT].
+Canonical perm_for_eqType := Eval hnf in [eqType of pT].
+Canonical perm_for_choiceType := Eval hnf in [choiceType of pT].
+Canonical perm_for_countType := Eval hnf in [countType of pT].
+Canonical perm_for_subCountType := Eval hnf in [subCountType of pT].
+Canonical perm_for_finType := Eval hnf in [finType of pT].
+Canonical perm_for_subFinType := Eval hnf in [subFinType of pT].

-Lemma perm_proof (f : T → T) : injective f → injectiveb (finfun f).
+Lemma perm_proof (f : T → T) : injective f → injectiveb (finfun f).

End PermDefSection.

-Notation "{ 'perm' T }" := (perm_of (Phant T))
+Notation "{ 'perm' T }" := (perm_of (Phant T))
  (at level 0, format "{ 'perm' T }") : type_scope.

@@ -111,33 +110,33 @@

-Notation "''S_' n" := {perm 'I_n}
+Notation "''S_' n" := {perm 'I_n}
  (at level 8, n at level 2, format "''S_' n").


Module Type PermDefSig.
-Parameter fun_of_perm : ∀ T, perm_type T → T → T.
-Parameter perm : ∀ (T : finType) (f : T → T), injective f → {perm T}.
-Axiom fun_of_permE : fun_of_perm = fun_of_perm_def.
-Axiom permE : perm = perm_def.
+Parameter fun_of_perm : ∀ T, perm_type T → T → T.
+Parameter perm : ∀ (T : finType) (f : T → T), injective f → {perm T}.
+Axiom fun_of_permE : fun_of_perm = fun_of_perm_def.
+Axiom permE : perm = perm_def.
End PermDefSig.

Module PermDef : PermDefSig.
Definition fun_of_perm := fun_of_perm_def.
Definition perm := perm_def.
-Lemma fun_of_permE : fun_of_perm = fun_of_perm_def.
-Lemma permE : perm = perm_def.
+Lemma fun_of_permE : fun_of_perm = fun_of_perm_def.
+Lemma permE : perm = perm_def.
End PermDef.

Notation fun_of_perm := PermDef.fun_of_perm.
-Notation "@ 'perm'" := (@PermDef.perm) (at level 10, format "@ 'perm'").
+Notation "@ 'perm'" := (@PermDef.perm) (at level 10, format "@ 'perm'").
Notation perm := (@PermDef.perm _ _).
-Canonical fun_of_perm_unlock := Unlockable PermDef.fun_of_permE.
-Canonical perm_unlock := Unlockable PermDef.permE.
+Canonical fun_of_perm_unlock := Unlockable PermDef.fun_of_permE.
+Canonical perm_unlock := Unlockable PermDef.permE.
Coercion fun_of_perm : perm_type >-> Funclass.

@@ -145,46 +144,44 @@
Variable T : finType.
-Implicit Types (x y : T) (s t : {perm T}) (S : {set T}).
+Implicit Types (x y : T) (s t : {perm T}) (S : {set T}).

-Lemma permP s t : s =1 t ↔ s = t.
+Lemma permP s t : s =1 t ↔ s = t.

-Lemma pvalE s : pval s = s :> (T → T).
+Lemma pvalE s : pval s = s :> (T → T).

-Lemma permE f f_inj : @perm T f f_inj =1 f.
+Lemma permE f f_inj : @perm T f f_inj =1 f.

-Lemma perm_inj s : injective s.
- -
-Hint Resolve perm_inj.
+Lemma perm_inj {s} : injective s.
+ Hint Resolve perm_inj : core.

-Lemma perm_onto s : codom s =i predT.
+Lemma perm_onto s : codom s =i predT.

-Definition perm_one := perm (@inj_id T).
+Definition perm_one := perm (@inj_id T).

-Lemma perm_invK s : cancel (fun x ⇒ iinv (perm_onto s x)) s.
+Lemma perm_invK s : cancel (fun x ⇒ iinv (perm_onto s x)) s.

-Definition perm_inv s := perm (can_inj (perm_invK s)).
+Definition perm_inv s := perm (can_inj (perm_invK s)).

-Definition perm_mul s t := perm (inj_comp (perm_inj t) (perm_inj s)).
+Definition perm_mul s t := perm (inj_comp (@perm_inj t) (@perm_inj s)).

-Lemma perm_oneP : left_id perm_one perm_mul.
+Lemma perm_oneP : left_id perm_one perm_mul.

-Lemma perm_invP : left_inverse perm_one perm_inv perm_mul.
+Lemma perm_invP : left_inverse perm_one perm_inv perm_mul.

-Lemma perm_mulP : associative perm_mul.
+Lemma perm_mulP : associative perm_mul.

Definition perm_of_baseFinGroupMixin : FinGroup.mixin_of (perm_type T) :=
@@ -195,95 +192,95 @@
Canonical perm_of_baseFinGroupType :=
-  Eval hnf in [baseFinGroupType of {perm T}].
-Canonical perm_of_finGroupType := Eval hnf in [finGroupType of {perm T} ].
+  Eval hnf in [baseFinGroupType of {perm T}].
+Canonical perm_of_finGroupType := Eval hnf in [finGroupType of {perm T} ].

-Lemma perm1 x : (1 : {perm T}) x = x.
+Lemma perm1 x : (1 : {perm T}) x = x.

-Lemma permM s t x : (s × t) x = t (s x).
+Lemma permM s t x : (s × t) x = t (s x).

-Lemma permK s : cancel s s^-1.
+Lemma permK s : cancel s s^-1.

-Lemma permKV s : cancel s^-1 s.
+Lemma permKV s : cancel s^-1 s.

-Lemma permJ s t x : (s ^ t) (t x) = t (s x).
+Lemma permJ s t x : (s ^ t) (t x) = t (s x).

-Lemma permX s x n : (s ^+ n) x = iter n s x.
+Lemma permX s x n : (s ^+ n) x = iter n s x.

-Lemma im_permV s S : s^-1 @: S = s @^-1: S.
+Lemma im_permV s S : s^-1 @: S = s @^-1: S.

-Lemma preim_permV s S : s^-1 @^-1: S = s @: S.
+Lemma preim_permV s S : s^-1 @^-1: S = s @: S.

-Definition perm_on S : pred {perm T} := fun s ⇒ [pred x | s x != x] \subset S.
+Definition perm_on S : pred {perm T} := fun s ⇒ [pred x | s x != x] \subset S.

-Lemma perm_closed S s x : perm_on S s → (s x \in S) = (x \in S).
+Lemma perm_closed S s x : perm_on S s → (s x \in S) = (x \in S).

Lemma perm_on1 H : perm_on H 1.

-Lemma perm_onM H s t : perm_on H s → perm_on H t → perm_on H (s × t).
+Lemma perm_onM H s t : perm_on H s → perm_on H t → perm_on H (s × t).

-Lemma out_perm S u x : perm_on S u → x \notin S → u x = x.
+Lemma out_perm S u x : perm_on S u → x \notin S → u x = x.

-Lemma im_perm_on u S : perm_on S u → u @: S = S.
+Lemma im_perm_on u S : perm_on S u → u @: S = S.

-Lemma tperm_proof x y : involutive [fun z ⇒ z with x |-> y, y |-> x].
+Lemma tperm_proof x y : involutive [fun z ⇒ z with x |-> y, y |-> x].

-Definition tperm x y := perm (can_inj (tperm_proof x y)).
+Definition tperm x y := perm (can_inj (tperm_proof x y)).

-CoInductive tperm_spec x y z : T → Type :=
-  | TpermFirst of z = x : tperm_spec x y z y
-  | TpermSecond of z = y : tperm_spec x y z x
-  | TpermNone of z ≠ x & z ≠ y : tperm_spec x y z z.
+Variant tperm_spec x y z : T → Type :=
+  | TpermFirst of z = x : tperm_spec x y z y
+  | TpermSecond of z = y : tperm_spec x y z x
+  | TpermNone of z ≠ x & z ≠ y : tperm_spec x y z z.

Lemma tpermP x y z : tperm_spec x y z (tperm x y z).

-Lemma tpermL x y : tperm x y x = y.
+Lemma tpermL x y : tperm x y x = y.

-Lemma tpermR x y : tperm x y y = x.
+Lemma tpermR x y : tperm x y y = x.

-Lemma tpermD x y z : x != z → y != z → tperm x y z = z.
+Lemma tpermD x y z : x != z → y != z → tperm x y z = z.

-Lemma tpermC x y : tperm x y = tperm y x.
+Lemma tpermC x y : tperm x y = tperm y x.

-Lemma tperm1 x : tperm x x = 1.
+Lemma tperm1 x : tperm x x = 1.

-Lemma tpermK x y : involutive (tperm x y).
+Lemma tpermK x y : involutive (tperm x y).

-Lemma tpermKg x y : involutive (mulg (tperm x y)).
+Lemma tpermKg x y : involutive (mulg (tperm x y)).

-Lemma tpermV x y : (tperm x y)^-1 = tperm x y.
+Lemma tpermV x y : (tperm x y)^-1 = tperm x y.

-Lemma tperm2 x y : tperm x y × tperm x y = 1.
+Lemma tperm2 x y : tperm x y × tperm x y = 1.

-Lemma card_perm A : #|perm_on A| = (#|A|)`!.
+Lemma card_perm A : #|perm_on A| = (#|A|)`!.

End Theory.
@@ -291,16 +288,25 @@

-Lemma inj_tperm (T T' : finType) (f : T → T') x y z :
-  injective f → f (tperm x y z) = tperm (f x) (f y) (f z).
+ + +
+ Shorthand for using a permutation to reindex a bigop. +
+
+Notation reindex_perm s := (reindex_inj (@perm_inj _ s)).
+ +
+Lemma inj_tperm (T T' : finType) (f : T → T') x y z :
+  injective f → f (tperm x y z) = tperm (f x) (f y) (f z).

-Lemma tpermJ (T : finType) x y (s : {perm T}) :
-  (tperm x y) ^ s = tperm (s x) (s y).
+Lemma tpermJ (T : finType) x y (s : {perm T}) :
+  (tperm x y) ^ s = tperm (s x) (s y).

-Lemma tuple_perm_eqP {T : eqType} {n} {s : seq T} {t : n.-tuple T} :
-  reflect (∃ p : 'S_n, s = [tuple tnth t (p i) | i < n]) (perm_eq s t).
+Lemma tuple_permP {T : eqType} {n} {s : seq T} {t : n.-tuple T} :
+  reflect (∃ p : 'S_n, s = [tuple tnth t (p i) | i < n]) (perm_eq s t).

Section PermutationParity.
@@ -309,7 +315,7 @@ Variable T : finType.

-Implicit Types (s t u v : {perm T}) (x y z a b : T).
+Implicit Types (s t u v : {perm T}) (x y z a b : T).

@@ -325,69 +331,69 @@
Definition aperm x s := s x.
-Definition pcycle s x := aperm x @: <[s]>.
-Definition pcycles s := pcycle s @: T.
-Definition odd_perm (s : perm_type T) := odd #|T| (+) odd #|pcycles s|.
+Definition pcycle s x := aperm x @: <[s]>.
+Definition pcycles s := pcycle s @: T.
+Definition odd_perm (s : perm_type T) := odd #|T| (+) odd #|pcycles s|.

-Lemma apermE x s : aperm x s = s x.
+Lemma apermE x s : aperm x s = s x.

-Lemma mem_pcycle s i x : (s ^+ i) x \in pcycle s x.
+Lemma mem_pcycle s i x : (s ^+ i) x \in pcycle s x.

-Lemma pcycle_id s x : x \in pcycle s x.
+Lemma pcycle_id s x : x \in pcycle s x.

-Lemma uniq_traject_pcycle s x : uniq (traject s x #|pcycle s x|).
+Lemma uniq_traject_pcycle s x : uniq (traject s x #|pcycle s x|).

-Lemma pcycle_traject s x : pcycle s x =i traject s x #|pcycle s x|.
+Lemma pcycle_traject s x : pcycle s x =i traject s x #|pcycle s x|.

-Lemma iter_pcycle s x : iter #|pcycle s x| s x = x.
+Lemma iter_pcycle s x : iter #|pcycle s x| s x = x.

-Lemma eq_pcycle_mem s x y : (pcycle s x == pcycle s y) = (x \in pcycle s y).
+Lemma eq_pcycle_mem s x y : (pcycle s x == pcycle s y) = (x \in pcycle s y).

-Lemma pcycle_sym s x y : (x \in pcycle s y) = (y \in pcycle s x).
+Lemma pcycle_sym s x y : (x \in pcycle s y) = (y \in pcycle s x).

-Lemma pcycle_perm s i x : pcycle s ((s ^+ i) x) = pcycle s x.
+Lemma pcycle_perm s i x : pcycle s ((s ^+ i) x) = pcycle s x.

Lemma ncycles_mul_tperm s x y : let t := tperm x y in
-  #|pcycles (t × s)| + (x \notin pcycle s y).*2 = #|pcycles s| + (x != y).
+  #|pcycles (t × s)| + (x \notin pcycle s y).*2 = #|pcycles s| + (x != y).

-Lemma odd_perm1 : odd_perm 1 = false.
+Lemma odd_perm1 : odd_perm 1 = false.

-Lemma odd_mul_tperm x y s : odd_perm (tperm x y × s) = (x != y) (+) odd_perm s.
+Lemma odd_mul_tperm x y s : odd_perm (tperm x y × s) = (x != y) (+) odd_perm s.

-Lemma odd_tperm x y : odd_perm (tperm x y) = (x != y).
+Lemma odd_tperm x y : odd_perm (tperm x y) = (x != y).

-Definition dpair (eT : eqType) := [pred t | t.1 != t.2 :> eT].
+Definition dpair (eT : eqType) := [pred t | t.1 != t.2 :> eT].

Lemma prod_tpermP s :
-  {ts : seq (T × T) | s = \prod_(t <- ts) tperm t.1 t.2 & all dpair ts}.
+  {ts : seq (T × T) | s = \prod_(t <- ts) tperm t.1 t.2 & all dpair ts}.

Lemma odd_perm_prod ts :
-  all dpair ts → odd_perm (\prod_(t <- ts) tperm t.1 t.2) = odd (size ts).
+  all dpair ts → odd_perm (\prod_(t <- ts) tperm t.1 t.2) = odd (size ts).

-Lemma odd_permM : {morph odd_perm : s1 s2 / s1 × s2 >-> s1 (+) s2}.
+Lemma odd_permM : {morph odd_perm : s1 s2 / s1 × s2 >-> s1 (+) s2}.

-Lemma odd_permV s : odd_perm s^-1 = odd_perm s.
+Lemma odd_permV s : odd_perm s^-1 = odd_perm s.

-Lemma odd_permJ s1 s2 : odd_perm (s1 ^ s2) = odd_perm s1.
+Lemma odd_permJ s1 s2 : odd_perm (s1 ^ s2) = odd_perm s1.

End PermutationParity.
@@ -405,44 +411,50 @@

-Variable n : nat.
-Implicit Types i j : 'I_n.+1.
-Implicit Types s t : 'S_n.
+Variable n : nat.
+Implicit Types i j : 'I_n.+1.
+Implicit Types s t : 'S_n.

Definition lift_perm_fun i j s k :=
-  if unlift i k is Some k' then lift j (s k') else j.
+  if unlift i k is Some k' then lift j (s k') else j.

Lemma lift_permK i j s :
-  cancel (lift_perm_fun i j s) (lift_perm_fun j i s^-1).
+  cancel (lift_perm_fun i j s) (lift_perm_fun j i s^-1).

-Definition lift_perm i j s := perm (can_inj (lift_permK i j s)).
+Definition lift_perm i j s := perm (can_inj (lift_permK i j s)).

-Lemma lift_perm_id i j s : lift_perm i j s i = j.
+Lemma lift_perm_id i j s : lift_perm i j s i = j.

Lemma lift_perm_lift i j s k' :
-  lift_perm i j s (lift i k') = lift j (s k') :> 'I_n.+1.
+  lift_perm i j s (lift i k') = lift j (s k') :> 'I_n.+1.

Lemma lift_permM i j k s t :
-  lift_perm i j s × lift_perm j k t = lift_perm i k (s × t).
+  lift_perm i j s × lift_perm j k t = lift_perm i k (s × t).

-Lemma lift_perm1 i : lift_perm i i 1 = 1.
+Lemma lift_perm1 i : lift_perm i i 1 = 1.

-Lemma lift_permV i j s : (lift_perm i j s)^-1 = lift_perm j i s^-1.
+Lemma lift_permV i j s : (lift_perm i j s)^-1 = lift_perm j i s^-1.

-Lemma odd_lift_perm i j s : lift_perm i j s = odd i (+) odd j (+) s :> bool.
+Lemma odd_lift_perm i j s : lift_perm i j s = odd i (+) odd j (+) s :> bool.

End LiftPerm.
+
+ +
+Notation tuple_perm_eqP :=
+  (deprecate tuple_perm_eqP tuple_permP) (only parsing).
+
-- cgit v1.2.3