(**************************************************************)
(*   Copyright Dominique Larchey-Wendling [*]                 *)
(*                                                            *)
(*                             [*] Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

Require Import List Arith Omega.
Require Import utils_tac utils_list sums php.

Set Implicit Arguments.

Local Notation "∑" := (msum plus 0).

Section nat_swap.

  Variables (i j : nat).

  Definition swap n := if eq_nat_dec n i then j else
                       if eq_nat_dec n j then i else n.

  Fact swap_spec_i : swap i = j.
(* Goal: @eq nat (swap i) j *)
  Proof. unfold swap; destruct (eq_nat_dec i i); auto; omega. Qed.

  Fact swap_spec_j : swap j = i.
  Proof. 
(* Goal: @eq nat (swap j) i *)
    unfold swap. 
(* Goal: @eq nat (if Nat.eq_dec j i then j else if Nat.eq_dec j j then i else j) i *)
    destruct (eq_nat_dec j i); auto.
(* Goal: @eq nat (if Nat.eq_dec j j then i else j) i *)
    destruct (eq_nat_dec j j); auto; omega. 
  Qed.

  Fact swap_spec n : n <> i -> n <> j -> swap n = n.
  Proof. 
(* Goal: forall (_ : not (@eq nat n i)) (_ : not (@eq nat n j)), @eq nat (swap n) n *)
    unfold swap; intros.
(* Goal: @eq nat (if Nat.eq_dec n i then j else if Nat.eq_dec n j then i else n) n *)
    destruct (eq_nat_dec n i); try omega.
(* Goal: @eq nat (if Nat.eq_dec n j then i else n) n *)
    destruct (eq_nat_dec n j); omega. 
  Qed.

  Fact swap_involutive n : swap (swap n) = n.
  Proof.
(* Goal: @eq nat (swap (swap n)) n *)
    destruct (eq_nat_dec n i).
(* Goal: lt (p k) n *)
(* Goal: lt (p k) n *)
    { subst n; rewrite swap_spec_i, swap_spec_j; auto. }
(* Goal: @eq nat (swap (swap n)) n *)
    destruct (eq_nat_dec n j).
(* Goal: lt (p k) n *)
(* Goal: lt (p k) n *)
    { subst n; rewrite swap_spec_j, swap_spec_i; auto. }
(* Goal: lt (p k) n *)
(* Goal: lt (p k) n *)
    { do 2 (rewrite swap_spec; auto). }
  Qed.

  Fact swap_inj n m : swap n = swap m -> n = m.
  Proof.
(* Goal: forall _ : @eq nat (swap n) (swap m), @eq nat n m *)
    intros; rewrite <- (swap_involutive n), H.
(* Goal: @eq nat (swap (swap m)) m *)
    apply swap_involutive.
  Qed.
  
End nat_swap.

Opaque swap.

Section php_fun.

  Variable (n : nat) (f : nat -> nat) (Hf : forall i, i <= n -> f i < n).

  Theorem php_fun : exists i j, i < j <= n /\ f i = f j.
  Proof.
    destruct PHP_rel with (S := fun x y => y = f x) (l := list_an 0 (S n)) (m := list_an 0 n)
      as (a & i & b & j & c & v & H1 & H2 & H3 & H4).
    + intros x; rewrite list_an_spec; simpl; intros [ _ H ].
(* Goal: @ex nat (fun y : nat => and (@In nat y (list_an O n)) (@eq nat y (f x))) *)
      exists (f x); split; auto; rewrite list_an_spec; simpl; split; try omega.
(* Goal: lt (f x) n *)
      apply Hf; omega.
    + do 2 rewrite list_an_length; auto.
    + exists i, j; split; try omega.
(* Goal: and (lt i j) (le j n) *)
      generalize H1; intros G1.
(* Goal: and (lt i j) (le j n) *)
      apply list_an_app_inv in G1.
(* Goal: and (lt i j) (le j n) *)
      destruct G1 as (G0 & G1); simpl in G1.
(* Goal: and (lt i j) (le j n) *)
      injection G1; clear G1; intros G1 G2.
(* Goal: and (lt i j) (le j n) *)
      symmetry in G1; apply list_an_app_inv in G1.
(* Goal: and (lt i j) (le j n) *)
      destruct G1 as (G3 & G1); simpl in G1.
(* Goal: and (lt i j) (le j n) *)
      injection G1; clear G1; intros G4 G1.
(* Goal: and (lt i j) (le j n) *)
      apply f_equal with (f := @length _) in H1.
(* Goal: and (lt i j) (le j n) *)
      revert H1; rew length; intros H1.
(* Goal: and (lt i j) (le j n) *)
      omega.
  Qed.

End php_fun.

Section split_interval.

(* Goal: lt (p k) n *)
(* Goal: lt (p k) n *)
  (* [0,i[ U {i} U ]i,n] ~~ [0,n[ U {n} *)

  Variables (n i : nat) (Hi : i <= n).

  Let g j := if le_lt_dec (S n) j then j else     (* j > n  *)
             if le_lt_dec i j then                  
             if le_lt_dec j i then n              (* j = i *)
             else j-1                             (* i < j <= n *)
             else j.                              (* j < i *)

  Let h j := if le_lt_dec (S n) j then j else     (* j > n  *)
             if le_lt_dec n j then i else         (* j = n  *) 
             if le_lt_dec i j then j+1            (* i <= j < n *)
             else j.                              (* j < i *)

  Let Hg1 : forall j, j <= n -> g j <= n.
  Proof.
(* Goal: forall (j : nat) (_ : le j n), le (g j) n *)
    intros j Hj; unfold g.
(* Goal: and (lt i j) (le j n) *)
    destruct (le_lt_dec (S n) j); try omega.
(* Goal: and (lt i j) (le j n) *)
    destruct (le_lt_dec i j); try omega.
(* Goal: and (lt i j) (le j n) *)
    destruct (le_lt_dec j i); omega.
  Qed.

  Let Hg2 j : n < j -> g j = j.
  Proof.
(* Goal: and (lt i j) (le j n) *)
    unfold g; destruct (le_lt_dec (S n) j); intros; omega.
  Qed.

  Let Hh1 : forall j, j <= n -> h j <= n.
  Proof.
(* Goal: forall (j : nat) (_ : le j n), le (h j) n *)
    intros j Hj; unfold h.
(* Goal: and (lt i j) (le j n) *)
    destruct (le_lt_dec (S n) j); try omega.
(* Goal: and (lt i j) (le j n) *)
    destruct (le_lt_dec n j); try omega.
(* Goal: and (lt i j) (le j n) *)
    destruct (le_lt_dec i j); omega.
  Qed.

  Let Hh2 j : n < j -> h j = j.
  Proof.
(* Goal: and (lt i j) (le j n) *)
    unfold h; destruct (le_lt_dec (S n) j); intros; omega.
  Qed.

  Ltac mydestruct H := 
    match goal with
      |- if ?c then _ else _ = _ => destruct c as [ H | H ]; try omega; auto
    end.

(* Goal: lt (p k) n *)
(* Goal: lt (p k) n *)
  Theorem split_interval : { g : nat -> nat & { h | (forall j, j <= n -> g j <= n)
                                                 /\ (forall j, j <= n -> h j <= n)
                                                 /\ (forall j, g (h j) = j)
                                                 /\ (forall j, h (g j) = j) 
                                                 /\ g i = n } }.
  Proof.
    exists g, h.
    split; [ | split; [ | split; [ | split ] ] ]; auto.
    + intros j; unfold h. 
      destruct (le_lt_dec (S n) j) as [ | H1 ]; auto.
      destruct (le_lt_dec n j) as [ H2 | H2 ].
(* Goal: lt (p k) n *)
(* Goal: lt (p k) n *)
      { unfold g.
(* Goal: and (lt i j) (le j n) *)
        destruct (le_lt_dec (S n) i); try omega.
        destruct (le_lt_dec i i); omega. }
      destruct (le_lt_dec i j) as [ H3 | H3 ].
(* Goal: lt (p k) n *)
(* Goal: lt (p k) n *)
      { unfold g.
        destruct (le_lt_dec (S n) (j+1)); try omega.
        destruct (le_lt_dec i (j+1)); try omega.
        destruct (le_lt_dec (j+1) i); omega. }
(* Goal: lt (p k) n *)
(* Goal: lt (p k) n *)
      { unfold g.
(* Goal: and (lt i j) (le j n) *)
        destruct (le_lt_dec (S n) j); try omega.
        destruct (le_lt_dec i j); try omega. }
    + intros j; unfold g. 
      destruct (le_lt_dec (S n) j) as [ | H1 ]; auto.
      destruct (le_lt_dec i j) as [ H2 | H2 ].
      destruct (le_lt_dec j i) as [ H3 | H3 ].
(* Goal: lt (p k) n *)
(* Goal: lt (p k) n *)
      { unfold h.
(* Goal: and (lt i j) (le j n) *)
        destruct (le_lt_dec (S n) n); try omega.
        destruct (le_lt_dec n n); omega. }
(* Goal: lt (p k) n *)
(* Goal: lt (p k) n *)
      { unfold h.
(* Goal: and (lt i j) (le j n) *)
        destruct (le_lt_dec (S n) (j-1)); try omega.
(* Goal: and (lt i j) (le j n) *)
        destruct (le_lt_dec n (j-1)); try omega.
        destruct (le_lt_dec i (j-1)); omega. }
(* Goal: lt (p k) n *)
(* Goal: lt (p k) n *)
      { unfold h.
(* Goal: and (lt i j) (le j n) *)
        destruct (le_lt_dec (S n) j); try omega.
(* Goal: and (lt i j) (le j n) *)
        destruct (le_lt_dec n j); try omega.
        destruct (le_lt_dec i j); omega. }
    + unfold g.
(* Goal: and (lt i j) (le j n) *)
      destruct (le_lt_dec (S n) i); try omega.
(* Goal: and (lt i j) (le j n) *)
      destruct (le_lt_dec i i); omega.
  Qed.

End split_interval.

(* Goal: lt (p k) n *)
(* Goal: lt (p k) n *)
Definition find_max_fun n f : { i | i <= n /\ forall j, j <= n -> f j <= f i }.
Proof.
(* Goal: @sig nat (fun i : nat => and (le i n) (forall (j : nat) (_ : le j n), le (f j) (f i))) *)
  revert f; induction n as [ | n IHn ]; intros f.
  + exists 0; split; auto.
(* Goal: and (lt i j) (le j n) *)
    intros [ | ]; auto; omega.
  + destruct (IHn f) as (i & H1 & H2).
(* Goal: @sig nat (fun i : nat => and (le i (S n)) (forall (j : nat) (_ : le j (S n)), le (f j) (f i))) *)
    destruct (le_lt_dec (f i) (f (S n))) as [ H | H ].
    * exists (S n); split; auto.
(* Goal: forall (j : nat) (_ : le j (S n)), le (f j) (f i) *)
      intros j Hj.
(* Goal: le (f j) (f (S n)) *)
      destruct (le_lt_dec j n) as [ H0 | H0 ].
      - apply le_trans with (2 := H); auto.
(* Goal: and (lt i j) (le j n) *)
      - cutrewrite (j = S n); auto; omega.
    * exists i; split; auto.
(* Goal: forall (j : nat) (_ : le j (S n)), le (f j) (f i) *)
      intros j Hj.
(* Goal: le (f j) (f i) *)
      destruct (le_lt_dec j n) as [ H0 | H0 ]; auto.
(* Goal: and (lt i j) (le j n) *)
      cutrewrite (j = S n); auto; omega.
Qed.

Section sum_bounded_permutation.

  Let sigma_sum_split i n f : i < n -> ∑ (S n) f = f i + f n + ∑ i f + ∑ (n-S i) (fun j => f (S i+j)).
  Proof.
(* Goal: forall _ : lt i n, @eq nat (@msum nat Init.Nat.add O (S n) f) (Init.Nat.add (Init.Nat.add (Init.Nat.add (f i) (f n)) (@msum nat Init.Nat.add O i f)) (@msum nat Init.Nat.add O (Init.Nat.sub n (S i)) (fun j : nat => f (Init.Nat.add (S i) j)))) *)
    intros Hi.
    replace (S n) with (i+1+(n- S i)+1) by omega.
(* Goal: @eq nat (@msum nat Init.Nat.add O (Init.Nat.add (Init.Nat.add (Init.Nat.add i (S O)) (Init.Nat.sub n (S i))) (S O)) f) (Init.Nat.add (Init.Nat.add (Init.Nat.add (f i) (f n)) (@msum nat Init.Nat.add O i f)) (@msum nat Init.Nat.add O (Init.Nat.sub n (S i)) (fun j : nat => f (Init.Nat.add (S i) j)))) *)
    repeat (rewrite msum_plus; auto).
(* Goal: @eq nat (Init.Nat.add (Init.Nat.add (Init.Nat.add (@msum nat Init.Nat.add O i f) (@msum nat Init.Nat.add O (S O) (fun i0 : nat => f (Init.Nat.add i i0)))) (@msum nat Init.Nat.add O (Init.Nat.sub n (S i)) (fun i0 : nat => f (Init.Nat.add (Init.Nat.add i (S O)) i0)))) (@msum nat Init.Nat.add O (S O) (fun i0 : nat => f (Init.Nat.add (Init.Nat.add (Init.Nat.add i (S O)) (Init.Nat.sub n (S i))) i0)))) (Init.Nat.add (Init.Nat.add (Init.Nat.add (f i) (f n)) (@msum nat Init.Nat.add O i f)) (@msum nat Init.Nat.add O (Init.Nat.sub n (S i)) (fun j : nat => f (Init.Nat.add (S i) j)))) *)
    do 2 rewrite msum_S, msum_0.
    repeat rewrite <- plus_assoc.
(* Goal: @eq nat (Nat.add (@msum nat Init.Nat.add O (Init.Nat.sub n (S i)) (fun i0 : nat => f (Init.Nat.add (Init.Nat.add i (S O)) i0))) (Nat.add (f (Nat.add i (S (Nat.add (Init.Nat.sub n (S i)) O)))) (@msum nat Init.Nat.add O i f))) (Nat.add (f n) (Nat.add (@msum nat Init.Nat.add O i f) (@msum nat Init.Nat.add O (Init.Nat.sub n (S i)) (fun j : nat => f (S (Init.Nat.add i j)))))) *)
    rewrite (plus_comm). 
    repeat rewrite <- plus_assoc.
(* Goal: @eq nat (Nat.add (@msum nat Init.Nat.add O i f) (@msum nat Init.Nat.add O (Init.Nat.sub n (S i)) (fun i0 : nat => f (Init.Nat.add (Init.Nat.add i (S O)) i0)))) (Nat.add (@msum nat Init.Nat.add O i f) (@msum nat Init.Nat.add O (Init.Nat.sub n (S i)) (fun j : nat => f (S (Init.Nat.add i j))))) *)
    f_equal.
(* Goal: lt (p k) n *)
(* Goal: lt (p k) n *)
    { f_equal; omega. }
(* Goal: @eq nat (Nat.add O (Nat.add (@msum nat Init.Nat.add O (Init.Nat.sub n (S i)) (fun i0 : nat => f (Init.Nat.add (Init.Nat.add i (S O)) i0))) (Nat.add (f (Nat.add i (Nat.add (S O) (Nat.add (Init.Nat.sub n (S i)) O)))) (Nat.add O (@msum nat Init.Nat.add O i f))))) (Nat.add (f n) (Nat.add (@msum nat Init.Nat.add O i f) (@msum nat Init.Nat.add O (Init.Nat.sub n (S i)) (fun j : nat => f (Init.Nat.add (S i) j))))) *)
    simpl.
(* Goal: @eq nat (Nat.add (@msum nat Init.Nat.add O (Init.Nat.sub n (S i)) (fun i0 : nat => f (Init.Nat.add (Init.Nat.add i (S O)) i0))) (Nat.add (f (Nat.add i (S (Nat.add (Init.Nat.sub n (S i)) O)))) (@msum nat Init.Nat.add O i f))) (Nat.add (f n) (Nat.add (@msum nat Init.Nat.add O i f) (@msum nat Init.Nat.add O (Init.Nat.sub n (S i)) (fun j : nat => f (S (Init.Nat.add i j)))))) *)
    rewrite (plus_comm).
    repeat rewrite <- plus_assoc.
(* Goal: @eq nat (Nat.add (@msum nat Init.Nat.add O i f) (@msum nat Init.Nat.add O (Init.Nat.sub n (S i)) (fun i0 : nat => f (Init.Nat.add (Init.Nat.add i (S O)) i0)))) (Nat.add (@msum nat Init.Nat.add O i f) (@msum nat Init.Nat.add O (Init.Nat.sub n (S i)) (fun j : nat => f (S (Init.Nat.add i j))))) *)
    f_equal.
(* Goal: lt (p k) n *)
(* Goal: lt (p k) n *)
    { f_equal; omega. }
(* Goal: @eq nat (Nat.add (@msum nat Init.Nat.add O i f) (@msum nat Init.Nat.add O (Init.Nat.sub n (S i)) (fun i0 : nat => f (Init.Nat.add (Init.Nat.add i (S O)) i0)))) (Nat.add (@msum nat Init.Nat.add O i f) (@msum nat Init.Nat.add O (Init.Nat.sub n (S i)) (fun j : nat => f (S (Init.Nat.add i j))))) *)
    f_equal.
(* Goal: @eq nat (@msum nat Init.Nat.add O (Init.Nat.sub n (S i)) (fun i0 : nat => f (Init.Nat.add (Init.Nat.add i (S O)) i0))) (@msum nat Init.Nat.add O (Init.Nat.sub n (S i)) (fun j : nat => f (S (Init.Nat.add i j)))) *)
    apply msum_ext.
(* Goal: and (lt i j) (le j n) *)
    intros; f_equal; omega.
  Qed.

  Let sum_permutation_1 n i j g f : 
            i < j < n 
         -> g i = j 
         -> g j = i
         -> (forall k, k <> i -> k <> j -> k < n -> g k = k)
         -> ∑ n f = ∑ n (fun i => f (g i)).
  Proof.
(* Goal: forall (_ : and (lt i j) (lt j n)) (_ : @eq nat (g i) j) (_ : @eq nat (g j) i) (_ : forall (k : nat) (_ : not (@eq nat k i)) (_ : not (@eq nat k j)) (_ : lt k n), @eq nat (g k) k), @eq nat (@msum nat Init.Nat.add O n f) (@msum nat Init.Nat.add O n (fun i : nat => f (g i))) *)
    revert i j g; induction n as [ | n IHn ]; intros i j g (H1 & H2) H3 H4 H5.
    + do 2 rewrite msum_0; auto.
    + destruct (eq_nat_dec j n) as [ H7 | H7 ].
      * rewrite H7 in *; clear j H7 H2.
(* Goal: @eq nat (@msum nat Init.Nat.add O (S n) f) (@msum nat Init.Nat.add O (S n) (fun i : nat => f (g i))) *)
        do 2 rewrite sigma_sum_split with (1 := H1).
        rewrite H3, H4; f_equal; [ f_equal | ]; try omega;
(* Goal: and (lt i j) (le j n) *)
          apply msum_ext; intros; symmetry; f_equal; apply H5; omega.
      * do 2 (rewrite msum_plus1; auto); f_equal.
(* Goal: and (lt i j) (le j n) *)
        - apply IHn with i j; auto; split; auto; omega.
(* Goal: and (lt i j) (le j n) *)
        - symmetry; f_equal; apply H5; omega.
  Qed.

  Inductive bounded_permut n (i j : nat) g : Prop :=
    | in_nat_perm : 
          i < n -> j < n -> g i = j -> g j = i
       -> (forall k, k <> i -> k <> j -> k < n -> g k = k)
       -> bounded_permut n i j g.

  Hint Resolve swap_spec_i swap_spec_j swap_spec.

  Fact swap_bounded_permut n i j : i < n -> j < n -> bounded_permut n i j (swap i j).
  Proof. constructor; auto. Qed.
 
  Inductive composed_permutation n g : Prop :=
    | in_cp_0 : (forall i, i < n -> g i = i) -> composed_permutation n g
    | in_cp_1 : forall i j f h, 
                                bounded_permut n i j f 
                             -> composed_permutation n h 
                             -> (forall i, i < n -> g i = h (f i))
                             -> composed_permutation n g.

  Fact composed_permutation_ext n f g : 
       (forall i, i < n -> f i = g i) -> composed_permutation n f -> composed_permutation n g.
  Proof.
(* Goal: forall (_ : forall (i : nat) (_ : lt i n), @eq nat (f i) (g i)) (_ : composed_permutation n f), composed_permutation n g *)
    intros H1 H2; revert H2 g H1.
(* Goal: forall (_ : composed_permutation n f) (g : forall _ : nat, nat) (_ : forall (i : nat) (_ : lt i n), @eq nat (f i) (g i)), composed_permutation n g *)
    induction 1 as [ f Hg | f i j p q H1 H2 IH2 H3 ]; intros g H4.
    + constructor 1; intros; rewrite <- H4; auto.
    + constructor 2 with i j p q; auto.
      intros; rewrite <- H4; auto.
  Qed.

  Let flat n f i := if le_lt_dec n i then n else f i.

  Let flat_left n f i : i < n -> flat n f i = f i.
  Proof. unfold flat; intro; destruct (le_lt_dec n i); auto; omega. Qed.

  Let flat_right n f i : n <= i -> flat n f i = n.
  Proof. unfold flat; intro; destruct (le_lt_dec n i); auto; omega. Qed.

  Fact composed_permutation_extends n f g : 
         (forall i, i < n -> f i = g i) -> g n = n -> composed_permutation n f -> composed_permutation (S n) g.
  Proof.
(* Goal: forall (_ : forall (i : nat) (_ : lt i n), @eq nat (f i) (g i)) (_ : @eq nat (g n) n) (_ : composed_permutation n f), composed_permutation (S n) g *)
    intros H1 H2 H3; revert H3 g H1 H2.
(* Goal: forall (_ : composed_permutation n f) (g : forall _ : nat, nat) (_ : forall (i : nat) (_ : lt i n), @eq nat (f i) (g i)) (_ : @eq nat (g n) n), composed_permutation (S n) g *)
    induction 1 as [ f Hg | f i j p q H1 H2 IH2 H3 ]; intros g H4 H5.
    + constructor 1; intros j Hj.
(* Goal: @eq nat (g j) j *)
      destruct (eq_nat_dec j n); subst; auto.
(* Goal: and (lt i j) (le j n) *)
      rewrite <- H4, Hg; auto; omega.
    + constructor 2 with i j (flat n p) (flat n q).
(* Goal: and (lt i j) (le j n) *)
      * destruct H1 as [ G1 G2 G3 G4 G5 ]; constructor; try omega.
(* Goal: and (lt i j) (le j n) *)
        - rewrite flat_left; auto; omega.
(* Goal: and (lt i j) (le j n) *)
        - rewrite flat_left; auto; omega.
        - intros k ? ? ?.
(* Goal: @eq nat (g k) (flat n q (flat n p k)) *)
          destruct (eq_nat_dec k n); subst.
          ++ rewrite flat_right; auto.
          ++ rewrite flat_left, G5; omega.
      * apply IH2.
        - intros l Hl; rewrite flat_left; auto.
(* Goal: and (lt i j) (le j n) *)
        - rewrite flat_right; omega.
      * intros k Hk.
(* Goal: @eq nat (g k) (flat n q (flat n p k)) *)
        destruct (eq_nat_dec k n); subst.
(* Goal: and (lt i j) (le j n) *)
        - rewrite (flat_right p), flat_right; omega.
(* Goal: and (lt i j) (le j n) *)
        - rewrite (flat_left p); try omega.
(* Goal: and (lt i j) (le j n) *)
          rewrite flat_left, <- H4; try omega.
          ++ apply H3; omega.
          ++ destruct H1 as [ G1 G2 G3 G4 G5 ].
(* Goal: lt (p k) n *)
             destruct (eq_nat_dec k i). 
(* Goal: lt (p k) n *)
(* Goal: lt (p k) n *)
             { subst; auto. }
(* Goal: lt (p k) n *)
             destruct (eq_nat_dec k j).
(* Goal: lt (p k) n *)
(* Goal: lt (p k) n *)
             { subst k; omega. }
(* Goal: and (lt i j) (le j n) *)
             rewrite G5; omega.
  Qed.

  Fact composed_permutation_S n g : g n = n -> composed_permutation n g -> composed_permutation (S n) g.
  Proof. intro; apply  composed_permutation_extends; auto. Qed.

  Inductive bounded_injective n f : Prop :=
    | in_bounded_inj : (forall i, i < n -> f i < n)
                    -> (forall i j, i < n -> j < n -> f i = f j -> i = j)
                    -> bounded_injective n f.

  Fact injective_composed_permutation n f : bounded_injective n f
                                         -> composed_permutation n f.
  Proof.
    intros [ H1 H2 ].
    revert f H1 H2; induction n as [ | n IHn ]; intros f H1 H2.
    + constructor 1; intros; omega.
    + destruct (find_max_fun n f) as (i & H3 & H4).
      destruct (le_lt_dec n (f i)) as [ C | C ].
      - assert (f i = n) as Hf1.
(* Goal: lt (p k) n *)
(* Goal: lt (p k) n *)
        { apply le_antisym; auto; apply le_S_n, H1; omega. }
        assert (forall j, j <= n -> j <> i -> f j < n) as Hf2.
(* Goal: lt (p k) n *)
(* Goal: lt (p k) n *)
        { intros j G1 G2.
          destruct (eq_nat_dec (f j) n).
          + contradict G2; apply H2; omega.
          + specialize (H1 j); omega. }
        specialize (IHn (fun x => f (swap i n x))).
        spec in IHn.
(* Goal: lt (p k) n *)
(* Goal: lt (p k) n *)
        { intros j Hj.
          destruct (eq_nat_dec j i).
          + subst j; rewrite swap_spec_i; apply Hf2; omega.
          + rewrite swap_spec; try omega; apply Hf2; omega. }
        spec in IHn.
(* Goal: lt (p k) n *)
(* Goal: lt (p k) n *)
        { intros u v G1 G2 G3.
          apply H2 in G3.
          + revert G3; apply swap_inj.
          + destruct (eq_nat_dec u i).
(* Goal: and (lt i j) (le j n) *)
            - subst; rewrite swap_spec_i; omega.
(* Goal: and (lt i j) (le j n) *)
            - rewrite swap_spec; omega.
          + destruct (eq_nat_dec v i).
(* Goal: and (lt i j) (le j n) *)
            - subst; rewrite swap_spec_i; omega.
            - rewrite swap_spec; omega. }
        apply composed_permutation_S in IHn.
        2: rewrite swap_spec_j, Hf1; auto.
        generalize (@swap_bounded_permut (S n) i n); intros G.
        do 2 (spec in G; try omega).
        constructor 2 with (1 := G) (2 := IHn).
        intros; rewrite swap_involutive; auto.
      - destruct (@php_fun n f) as (u & v & G1 & G2).
(* Goal: lt (p k) n *)
(* Goal: lt (p k) n *)
        { intros; apply le_lt_trans with (2 := C); auto. }
(* Goal: and (lt i j) (le j n) *)
        apply H2 in G2; omega.
  Qed.

  Theorem sum_bounded_permutation n i j g f : bounded_permut n i j g -> ∑ n f = ∑ n (fun i => f (g i)).
  Proof.
(* Goal: forall _ : bounded_permut n i j g, @eq nat (@msum nat Init.Nat.add O n f) (@msum nat Init.Nat.add O n (fun i : nat => f (g i))) *)
    intros [ H1 H2 H3 H4 H5 ].
(* Goal: @eq nat (@msum nat Init.Nat.add O n f) (@msum nat Init.Nat.add O n (fun i : nat => f (g i))) *)
    destruct (lt_eq_lt_dec i j) as [ [ G1 | G1 ] | G1 ].
    + apply sum_permutation_1 with i j; auto; split; auto.
    + apply msum_ext; rewrite <- G1 in *; clear j G1.
(* Goal: @eq nat (Nat.add (@msum nat Init.Nat.add O i f) (@msum nat Init.Nat.add O (Init.Nat.sub n (S i)) (fun i0 : nat => f (Init.Nat.add (Init.Nat.add i (S O)) i0)))) (Nat.add (@msum nat Init.Nat.add O i f) (@msum nat Init.Nat.add O (Init.Nat.sub n (S i)) (fun j : nat => f (S (Init.Nat.add i j))))) *)
      intros j Hj; f_equal.
(* Goal: lt (p k) n *)
      destruct (eq_nat_dec j i); subst; auto.
(* Goal: @eq nat j (g j) *)
      rewrite H5; auto.
    + apply sum_permutation_1 with j i; auto; split; auto.
  Qed.

  Theorem sum_composed_permutation n f g : composed_permutation n g -> ∑ n f = ∑ n (fun i => f (g i)).
  Proof.
(* Goal: forall _ : composed_permutation n g, @eq nat (@msum nat Init.Nat.add O n f) (@msum nat Init.Nat.add O n (fun i : nat => f (g i))) *)
    induction 1 as [ g Hg | g i j p q H1 H2 IH2 H3 ].
    + symmetry; apply msum_ext; intros; f_equal; apply Hg; auto.
    + rewrite IH2, sum_bounded_permutation with (1 := H1).
(* Goal: @eq nat (@msum nat Init.Nat.add O n (fun i : nat => f (q (p i)))) (@msum nat Init.Nat.add O n (fun i : nat => f (g i))) *)
      symmetry; apply msum_ext; intros; f_equal; auto.
  Qed.

  Theorem sum_injective n f g : bounded_injective n g -> ∑ n f = ∑ n (fun i => f (g i)).
  Proof.
(* Goal: forall _ : bounded_injective n g, @eq nat (@msum nat Init.Nat.add O n f) (@msum nat Init.Nat.add O n (fun i : nat => f (g i))) *)
    intros; apply sum_composed_permutation, injective_composed_permutation; trivial.
  Qed.

End sum_bounded_permutation.

Section sum_bijection.

  Inductive bijection n g h : Type :=
    | in_bij : (forall i, i < n -> g i < n)
            -> (forall i, i < n -> h i < n) 
            -> (forall i, i < n -> g (h i) = i)
            -> (forall i, i < n -> h (g i) = i)
           -> bijection n g h.

  Theorem sum_bijection n f g h : bijection n g h -> ∑ n f = ∑ n (fun i => f (g i)).
  Proof.
(* Goal: forall _ : bijection n g h, @eq nat (@msum nat Init.Nat.add O n f) (@msum nat Init.Nat.add O n (fun i : nat => f (g i))) *)
    intros [ H1 H2 H3 H4 ].
(* Goal: @eq nat (@msum nat Init.Nat.add O n f) (@msum nat Init.Nat.add O n (fun i : nat => f (g i))) *)
    apply sum_injective.
(* Goal: bounded_injective n g *)
    constructor; auto.
    intros i j G1 G2 G3; rewrite <- (H4 i), G3; auto.
  Qed.


  Inductive triangle_bijection n k g h : Prop :=
    | in_tb : (forall i j, j < i < n -> h (i,j) < k /\ g (h (i,j)) = (i,j))
           -> (forall q, q < k -> snd (g q) < fst (g q) < n /\ h (g q) = q) 
           -> triangle_bijection n k g h.

  Fact sum_triangle_bijection n f k g h :
         triangle_bijection n k g h 
      -> ∑ n (fun i => ∑ i (fun j => f i j)) = ∑ k (fun i => f (fst (g i)) (snd (g i))).
  Proof.
  Admitted.
 

  (* ∑ n (fun i => ∑ i (fun j => f i j * power (e i j) r) = ∑ k *)

End sum_bijection.