Library corde

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq finfun path.
Require Import fintype finset tuple div zmodp bigop ssralg perm fingroup rat.

Import GRing.Theory.

Section Corde.

(******************************************************************************)
(*                                                                            *)
(*                                                                            *)
(*                          MODÉLISATION                                      *)
(*                                                                            *)
(*                                                                            *)
(******************************************************************************)

(* Un ensemble de noeuds est une permutation dont tous les cycles sont de     *)
(* longueur 2                                                                 *)

Definition is_node n :=
  [set p | [forall i : 'I_n, ((p : 'S_n) (p i) == i) && (p i != i)]].

Notation " 'N[ n ] " := (@is_node n).

Lemma is_nodeK n (p : 'S_n) i : p \in 'N[n] -> p (p i) = i.

Lemma is_node_diff n (p : 'S_n) i : p \in 'N[n] -> p i != i.

Lemma is_node_flip n p i j : p \in 'N[n] -> p i = j -> p j = i.

(* Une configuration valide est une paire de permutation de 2-cycles          *)

Definition config n := ('S_n * 'S_n)%type.

Definition cvalid n : {set config n} := setX 'N[n] 'N[n].

Notation " 'N2[ n ] " := (cvalid n).

(* On suit la corde i pour m.*2 suivant la config c                          *)

Fixpoint follow m n (c : config n) x :=
  if m is m1.+1 then x :: c.1 x :: follow m1 c (c.2 (c.1 x)) else [::].

(* On obtient bien une liste de longuer 2m                                   *)
Lemma size_follow m n (c : config n) x : size (follow m c x) = m.*2.

(* Les cordes sont toutes liées entre elles, si en suivant la corde 0 on     *)
(* obtient toutes les cordes                                                 *)

Definition c2l n (c : config n.+1.*2) : seq 'I_n.+1.*2 := follow n.+1 c 0%R.

Definition one_cycle n := [set c | uniq (@c2l n c)].
Notation " 'O[ n ] " := (@one_cycle n).

(******************************************************************************)
(*                                                                            *)
(*                     NOMBRE DE CONFIGURATIONS                               *)
(*                                                                            *)
(******************************************************************************)

(* Les ordinaux plus petits qu'une certaine valeur                            *)

Definition lordinal n k := [set i | (i : 'I_n) < k].

Lemma card_lordinal n k : k <= n -> #|lordinal n k| = k.

(* Enlever les deux cycles (i, p i) et (j, p j)                               *)

Definition swap_node n (p : 'S_n) i j :=
    (p * tperm i (p i) * tperm j (p j) * tperm (p i) (p j))%g.

Lemma swap_nodeL n (p : 'S_n) i j :
  p i != i -> p (p j) = j -> i != j -> swap_node p i j i = i.

Lemma swap_nodeLp n (p : 'S_n) i j :
  p i != j -> p (p i) = i -> i != j -> swap_node p i j (p i) = p j.

Lemma swap_nodeR n (p : 'S_n) i j :
  p j != j -> p (p j) = j -> i != j -> swap_node p i j j = j.

Lemma swap_nodeRp n (p : 'S_n) i j :
  p i != j -> p (p j) = j -> i != j -> swap_node p i j (p j) = p i.

Lemma swap_nodeD n (p : 'S_n) i j k :
 p (p i) = i -> p (p j) = j ->
 k \notin [:: i; j; p i; p j] -> swap_node p i j k = p k.

(* Rajouter deux cycles (i, k) et (j, p k)                                    *)

Definition unswap_node n (p : 'S_n) i j k :=
    (p * tperm i (p k) * tperm j k * tperm k (p k))%g.

Lemma unswap_nodeL n (p : 'S_n) i j k :
  p i = i -> p j = j -> p k != k -> unswap_node p i j k i = k.

Lemma unswap_nodeR n (p : 'S_n) i j k :
  i != j -> p j = j -> p k != k -> unswap_node p i j k j = p k.

Lemma unswap_nodeM n (p : 'S_n) i j k :
  i != j -> p i = i -> p j = j -> p k != k -> unswap_node p i j k k = i.

Lemma unswap_nodeMp n (p : 'S_n) i j k :
  i != j -> p i = i -> p j = j -> p k != k -> p (p k) = k ->
  unswap_node p i j k (p k) = j.

Lemma unswap_nodeD n (p : 'S_n) i j k l :
  p i = i -> p j = j -> p (p k) = k ->
  l \notin [:: i; j; k; p k] -> unswap_node p i j k l = p l.

Lemma swap_nodeK n (p : 'S_n) i j :
  i != j -> p i != i -> p (p i) = i -> p j != j -> p (p j) = j ->
  unswap_node (swap_node p i j) i j (p i) = p.

Lemma unswap_nodeK n (p : 'S_n) i j k:
  i != j -> p i = i -> p j = j -> p k != k -> p (p k) = k ->
  swap_node (unswap_node p i j k) i j = p.

(* Ajouter les deux cycles (i, t.2) et (i + 1, p t.2))                        *)

Definition pI2S m (i : 'I_m.+2) (t : 'S_m.+2 * 'I_m.+2) : 'S_m.+2 :=
  unswap_node t.1 (i + 1)%R i t.2.

(* Enlever les deux cycles (i, p i) et (i + 1, p (i + 1))                     *)

Definition S2pI m (i : 'I_m.+2) (p : 'S_m.+2) : 'S_m.+2 * 'I_m.+2 :=
  (swap_node p (i + 1)%R i, p (i + 1)%R).

(* Version de is_node paramétré pour permettre une preuve par induction       *)

Definition is_nodeL m k :=
  [set p |
     [forall i : 'I_m, if i < k.*2 then ((p : 'S_m) (p i) == i) && (p i != i)
                       else p i == i]].
Notation " 'N[ n , k ] " := (@is_nodeL n k).

Lemma is_nodeLE n : 'N[n.*2,n] = 'N[n.*2].

Lemma PPN n k p i : p \in 'N[n, k] -> p (p i) = i.

Lemma PDN n k p (i : 'I_n) : p \in 'N[n, k] -> i < k.*2 -> p i != i.

Lemma PEN n k p (i : 'I_n) : p \in 'N[n, k] -> k.*2 <= i -> p i = i.

Lemma PLN n k p (i : 'I_n) : p \in'N[n, k] -> i < k.*2 -> p i < k.*2.

Lemma ISE n (i: 'I_n.+2) : i <= n -> (i + 1)%R = i.+1 :> nat.

Lemma ISDE n (i: 'I_n.+2) : i <= n -> (i + 1)%R != i.

(* Sp2I est bijectif                                                          *)

Lemma S2pIK n k (i : 'I_n.+2) :
  i < k.*2.+1 <= n.+1 -> {in 'N[n.+2, k.+1], (pI2S i) \o (S2pI i) =1 id}.

(* pI2S est bijectif                                                          *)

Lemma pI2SK n k (i : 'I_n.+2) :
   k.*2 = i -> i <= n ->
  {in setX 'N[n.+2, k] (lordinal n.+2 k.*2.+1), (S2pI i) \o (pI2S i) =1 id}.

(* L'image de S2pI (k décroit)                                                *)

Lemma subset_S2pI n k (i : 'I_n.+2) :
  k.*2 = i -> i <= n ->
 [set S2pI i p | p in 'N[n.+2, k.+1]]
\subset setX 'N[n.+2, k] (lordinal n.+2 k.*2.+1).

(* L'image de p2SI (k croit)                                                  *)

Lemma subset_pI2S n k (i : 'I_n.+2) :
  k.*2 = i -> i <= n ->
 [set pI2S i t | t in setX 'N[n.+2, k] (lordinal n.+2 k.*2.+1)]
         \subset'N[n.+2, k.+1].

(* Cardinalité des permutations dont tous les cycles sont de longueur 2       *)
(* On fait la preuve par induction en enlevant deux cycles à la fois          *)

Lemma card_is_node n : #|'N[n.+1.*2]| = \prod_(i < n.+1) i.*2.+1.

(* Cardinal des configurations                                                *)

Lemma card_cvalid n : #|'N2[n.+1.*2]| = (\prod_(i < n.+1) i.*2.+1) ^ 2.

Fact card_cvalid6 : #|'N2[6]| = 15 ^ 2.

(******************************************************************************)
(*                                                                            *)
(*                     NOMBRE DE CONFIGURATIONS A 1 CYCLE                     *)
(*                                                                            *)
(******************************************************************************)

(* Promouvoir une fonction en une permutation                                 *)

Definition perm_of n (f : {ffun 'I_n.+1 -> 'I_n.+1}) : 'S_n.+1 :=
  odflt 1%g [pick p | f == (pval p)].

Lemma perm_ofE n (f: {ffun 'I_n.+1 -> _}) : injective f -> perm_of f =1 f.

Lemma oddI_pre n (i : 'I_n.+2) : ~~ odd n -> odd (i - 1)%R = ~~ odd i.

Lemma oddIS n (i : 'I_n.+2) : ~~ odd n -> odd (i + 1)%R = ~~ odd i.

(* Traduire une configuration en une permutation en utilisant la liste S2l    *)

Definition c2p n (c : config n.+1.*2) :=
  perm_of ([ffun n : 'I_ _ => nth 0%R (c2l c) n]).

(* Récupération de la première permutation de la configuration                *)

Definition fun_permL n (p : 'S_n.+2) :=
 [ffun i : 'I_n.+2 =>
    let k := p^-1%g i in
    if odd k then p (k - 1)%R else p (k + 1)%R].

Lemma fun_permLK n (p : 'S_n.+2) i :
  ~~ odd n -> fun_permL p (fun_permL p i) = i.

Lemma injective_permL n (p : 'S_n.+2) : ~~ odd n -> injective (fun_permL p).

Lemma fun_permLF n (p : 'S_n.+2) i : ~~ odd n -> fun_permL p i != i.

(* Récupération de la deuxième permutation de la configuration                *)

Definition fun_permR n (p : 'S_n.+2) :=
  [ffun i : 'I_n.+2 =>
    let k := p^-1%g i in
    if odd k then p (k + 1)%R else p (k - 1)%R].

Lemma fun_permRK n (p : 'S_n.+2) i :
  ~~ odd n -> fun_permR p (fun_permR p i) = i.

Lemma injective_permR n (p : 'S_n.+2) : ~~ odd n -> injective (fun_permR p).

Lemma fun_permRF n (p : 'S_n.+2) i : ~~ odd n -> fun_permR p i != i.

(* Traduire une permutation telle que p 0 = 0 en une configuration            *)

Definition p2c n (p: 'S_n.+2) : config n.+2 :=
  (perm_of (fun_permL p), perm_of (fun_permR p)).

(* Permutation qui valent 0 en 0                                              *)

Definition perm_fix0 n : pred 'S_n.+1 := perm_on [set~ ord0].
Notation " 'F[ n ] " := (@perm_fix0 n).

Lemma perm_fix0P n p : p \in @perm_fix0 n = (p 0%R == 0%R).

Lemma c2l_codom n (p: 'S_n.+1.*2) : p 0%R = 0%R -> c2l (p2c p) = codom p.

Lemma card_perm_fix0 n : #|'F[n]| = n`!.

Lemma imp2c n: [set p2c p | p in 'F[n.*2.+1]] \subset 'N2[(n.+1).*2] :&: 'O[n].

Lemma imc2p n: [set c2p c | c in 'N2[(n.+1).*2] :&: 'O[n]] \subset 'F[n.*2.+1].

Lemma p2SK n : {in 'F[n.*2.+1], (@c2p _) \o (@p2c n.*2) =1 id}.

Lemma I_preE n (i: 'I_n.+2) : 0 < i -> (i - 1)%R = i.-1 :> nat.

Lemma c2lLE n (c: config n.+1.*2) (i : 'I_ n.+1.*2) (p := c.1) :
  ((forall i, p (p i) = i) ->
     p (c2l c)`_i = (c2l c)`_(if odd i then (i - 1) else (i + 1)))%R.

Lemma c2lRE n (c: config n.+1.*2) (i : 'I_ n.+1.*2) (p := c.2) :
  ((forall i, p (p i) = i) -> (forall i, p i != i) -> uniq (c2l c) ->
     p (c2l c)`_i = (c2l c)`_(if odd i then (i + 1) else (i - 1)))%R.

Lemma S2pK n : {in 'N2[n.+1.*2] :&: 'O[n], (@p2c n.*2) \o (@c2p _) =1 id}.

Lemma card_N2O n : #|'N2[n.+1.*2] :&: 'O[n]| = n.*2.+1 `!.

(******************************************************************************)
(*                                                                            *)
(*                           PROBABILITÉ                                      *)
(*                                                                            *)
(******************************************************************************)

Open Scope ring_scope.

(* Le rapport entre tous les configurations de noeuds avec un cycle et toutes *)
(* les configurations                                                         *)

Definition Proba n : rat := #|'N2[n.+1.*2] :&: 'O[n]|%:R / #|'N2[n.+1.*2]|%:R.

Lemma ProbaE n : Proba n = n.*2.+1 `!%:R / ((\prod_(i < n.+1) i.*2.+1) ^2)%:R.

Lemma result : Proba 2 = 8%:R / 15%:R.

End Corde.

This page has been generated by coqdoc