Library mathcomp_eulerian.reflection

From mathcomp Require Import all_ssreflect fingroup perm.
From mathcomp_eulerian Require Import ordinal_reindex perm_compress
                                       descent eulerian beta beta_omega
                                       beta_swap.

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


Definition euler (n : nat) : nat := beta (alt_desc_set n).

Definition eulerA (n : nat) : nat :=
  if n is k.+1 then euler k else 1.


Lemma eulerA_0 : eulerA 0 = 1.
Proof. by []. Qed.

Lemma alt_desc_set_0 : alt_desc_set 0 = set0.
Proof. by apply/setP; case; case. Qed.

Lemma euler_0 : euler 0 = 1.
Proof. by rewrite /euler alt_desc_set_0 beta0. Qed.

Lemma eulerA_1 : eulerA 1 = 1.
Proof. by rewrite /eulerA euler_0. Qed.

Lemma alt_desc_set_1 : alt_desc_set 1 = [set: 'I_1].
Proof.
apply/setP ⇒ i; rewrite mem_alt_desc_set inE.
by have /eqP → : val i == 0%N by rewrite -leqn0 -ltnS ltn_ord.
Qed.

Lemma euler_1 : euler 1 = 1.
Proof. by rewrite /euler alt_desc_set_1 beta_full. Qed.

Lemma eulerA_2 : eulerA 2 = 1.
Proof. by rewrite /eulerA euler_1. Qed.



Lemma descent_set_insert_max_ord0 n (t : {perm 'I_n.+1}) :
  descent_set (insert_max_perm t (ord0 : 'I_n.+2))
  = (ord0 : 'I_n.+1) |: [set lift ord0 j | j in descent_set t].
Proof.
rewrite /descent_set; apply/setP ⇒ i; rewrite !inE.
case: (unliftP ord0 i) ⇒ [j ->|->].
- rewrite eq_sym (negbTE (neq_lift _ _)) /=.
  have E1 : widen_ord (leqnSn n.+1) (lift ord0 j)
          = lift ord0 (widen_ord (leqnSn n) j) :> 'I_n.+2.
    by apply/val_inj; rewrite /= /bump leq0n /= add1n.
  rewrite /is_descent E1 !insert_max_perm_lift.
  apply/idP/imsetP.
  + by move⇒ H; ∃ j; first by rewrite inE /is_descent.
  + by case⇒ j' /[!inE] Hj' /lift_inj ->; rewrite /is_descent.
- rewrite eqxx orTb /is_descent.
  have → : widen_ord (leqnSn n.+1) (ord0 : 'I_n.+1) = ord0 :> 'I_n.+2.
    by apply/val_inj.
  by rewrite insert_max_perm_at_p insert_max_perm_lift /=; apply: ltn_ord.
Qed.

Lemma descent_set_insert_max_ord_max n (t : {perm 'I_n.+1}) :
  descent_set (insert_max_perm t (ord_max : 'I_n.+2))
  = [set (lift ord_max j : 'I_n.+1) | j in descent_set t].
Proof.
rewrite /descent_set; apply/setP ⇒ i; rewrite !inE.
case: (unliftP ord_max i) ⇒ [j ->|->].
- have E1 : widen_ord (leqnSn n.+1) (lift ord_max j)
          = lift ord_max (widen_ord (leqnSn n) j) :> 'I_n.+2.
    apply/val_inj; rewrite /= /bump /=.
    rewrite leqNgt (ltn_ord j) /=.
    by rewrite leqNgt (leq_trans (ltn_ord j) (leqnSn n)).
  have E2 : lift ord0 (lift ord_max j : 'I_n.+1)
          = lift ord_max (lift ord0 j) :> 'I_n.+2.
    apply/val_inj ⇒ /=.
    rewrite /bump /=.
    have H2 : (n ≤ j) = false by apply/negbTE; rewrite -ltnNge; apply: ltn_ord.
    have H3 : (n.+1 ≤ j.+1) = false by apply/negbTE; rewrite -ltnNge; apply: ltn_ord.
    by rewrite H2 H3.
  rewrite /is_descent E1 E2 !insert_max_perm_lift.
  apply/idP/imsetP.
  + by move⇒ H; ∃ j; first by rewrite inE /is_descent.
  + by case⇒ j' /[!inE] Hj' /lift_inj ->; rewrite /is_descent.
- rewrite /is_descent.
  have E1 : widen_ord (leqnSn n.+1) (ord_max : 'I_n.+1)
          = lift ord_max (ord_max : 'I_n.+1) :> 'I_n.+2.
    by apply/val_inj; rewrite /= /bump /= leqNgt ltnSn.
  have → : lift ord0 (ord_max : 'I_n.+1) = ord_max :> 'I_n.+2.
    by apply/val_inj.
  rewrite E1 insert_max_perm_lift insert_max_perm_at_p.
  apply/idP/imsetP.
  + by move⇒ H; move: (ltn_ord (t (ord_max : 'I_n.+1)));
       rewrite ltnNge /= in H; case/negP: H; apply: ltnW.
  + case⇒ j' _ /eqP; rewrite -val_eqE /= /bump /= leqNgt ltn_ord /= ⇒ /eqP eqn.
    rewrite add0n in eqn.
    by move: (ltn_ord j'); rewrite -eqn ltnn.
Qed.

Lemma descent_set_insert_max_interior n (t : {perm 'I_n.+1}) (j : 'I_n) :
  let h := widen_ord (leqnSn n) j in
  descent_set (insert_max_perm t (lift ord0 h))
  = [set lift h x | x in descent_set t :|: [set j]].
Proof.
move⇒ h; set p := lift ord0 h; set sigma := insert_max_perm t p.
rewrite /descent_set; apply/setP ⇒ i; rewrite !inE.
case: (unliftP h i) ⇒ [x ->|->].
- have sigma_lift0 : ∀ y : 'I_n,
    sigma (lift ord0 (lift h y)) = widen_ord (leqnSn n.+1) (t (lift ord0 y)).
    move⇒ y.
    have E : lift ord0 (lift h y) = lift p (lift ord0 y) :> 'I_n.+2.
      by apply/val_inj ⇒ /=; rewrite /p /=; rewrite /bump /= addnCA.
    by rewrite /sigma E insert_max_perm_lift.
  have → : (lift h x \in [set lift h x0 | x0 in descent_set t :|: [set j]])
          = (is_descent t x) || (x == j).
    apply/imsetP/idP ⇒ [[y]|].
    + by rewrite !inE ⇒ /orP[Hy|/eqP ->] /lift_inj ->;
         [rewrite Hy|rewrite eqxx orbT].
    + case/orP ⇒ [H|/eqP ->].
      - by ∃ x; rewrite // !inE H.
      - by ∃ j; rewrite // !inE eqxx orbT.
  rewrite /is_descent sigma_lift0 /=.
  case: (eqVneq x j) ⇒ [->|xnj].
  + have → : sigma (widen_ord (leqnSn n.+1) (lift h j)) = ord_max.
      have E : widen_ord (leqnSn n.+1) (lift h j) = p :> 'I_n.+2.
        by apply/val_inj; rewrite /= /p /= /bump /= leqnn.
      by rewrite /sigma E insert_max_perm_at_p.
    by rewrite orbT; apply: ltn_ord.
  + rewrite orbF.
    have E : widen_ord (leqnSn n.+1) (lift h x) = lift p (widen_ord (leqnSn n) x) :> 'I_n.+2.
      apply/val_inj; rewrite /= /p /= /bump /=.
      case: (ltngtP x j) ⇒ [Hxj|Hxj|Hxj].
      - by [].
      - by [].
      - by rewrite -val_eqE /= Hxj eqxx in xnj.
    by rewrite /sigma E insert_max_perm_lift.
- have Rfalse : (h \in [set lift h x | x in descent_set t :|: [set j]]) = false.
    by apply/negbTE/imsetP ⇒ -[y _ Hy]; have := neq_lift h y; rewrite -Hy eqxx.
  rewrite Rfalse /is_descent.
  have E1 : widen_ord (leqnSn n.+1) h = lift p h :> 'I_n.+2.
    apply/val_inj; rewrite /= /p /= /bump /=.
    by rewrite add1n ltnn.
  have E2 : lift ord0 h = p :> 'I_n.+2 by [].
  rewrite E1 E2 insert_max_perm_lift insert_max_perm_at_p.
  apply/negbTE; rewrite -leqNgt.
  by apply: ltnW; rewrite /=; exact: ltn_ord.
Qed.



Lemma widen_inj n m (h : n ≤ m) : injective (widen_ord h).
Proof. by move⇒ i j /(congr1 val) /=; exact: val_inj. Qed.

Section ImageLeft.

Variables (n : nat) (t : {perm 'I_n.+1}) (j : 'I_n.+2).

Definition leqj_n1 : (j : nat) ≤ n.+1 := ltnSE (ltn_ord j).

Definition embed_left (i : 'I_j) : 'I_n.+1 := widen_ord leqj_n1 i.

Lemma embed_left_inj : injective embed_left.
Proof. exact: widen_inj. Qed.

Definition image_left : {set 'I_n.+1} :=
  [set t (embed_left i) | i : 'I_j].

Lemma t_embed_inj : injective (fun i : 'I_j ⇒ t (embed_left i)).
Proof. by apply: inj_comp; [exact: perm_inj | exact: embed_left_inj]. Qed.

Lemma card_image_left : #|image_left| = j.
Proof.
by rewrite /image_left -[RHS](card_ord j) -(card_imset _ t_embed_inj).
Qed.

Lemma mem_image_left (i : 'I_j) : t (embed_left i) \in image_left.
Proof. by apply/imsetP; ∃ i. Qed.

End ImageLeft.



Section PermOfLeft.

Variables (n : nat) (t : {perm 'I_n.+1}) (j : 'I_n.+2).

Definition rank_left (x0 : 'I_n.+1)
    (Hx0 : x0 \in image_left t j) (y : 'I_n.+1) : 'I_(#|image_left t j|) :=
  enum_rank_in Hx0 y.

Definition cast_to_j (k : 'I_(#|image_left t j|)) : 'I_j :=
  cast_ord (card_image_left t j) k.

Lemma cast_to_j_inj : injective cast_to_j.
Proof. by move⇒ a b /cast_ord_inj. Qed.

Definition perm_left_fun (x0 : 'I_n.+1)
    (Hx0 : x0 \in image_left t j) (i : 'I_j) : 'I_j :=
  cast_to_j (enum_rank_in Hx0 (t (embed_left i))).

Lemma perm_left_fun_inj (x0 : 'I_n.+1) (Hx0 : x0 \in image_left t j) :
  injective (perm_left_fun Hx0).
Proof.
move⇒ i1 i2; rewrite /perm_left_fun ⇒ /cast_to_j_inj.
move⇒ /(congr1 (@enum_val _ _)).
rewrite !enum_rankK_in; try exact: mem_image_left.
by move/perm_inj/embed_left_inj.
Qed.

Definition perm_left (x0 : 'I_n.+1) (Hx0 : x0 \in image_left t j)
  : {perm 'I_j} := perm (@perm_left_fun_inj x0 Hx0).

Lemma perm_leftE (x0 : 'I_n.+1) (Hx0 : x0 \in image_left t j) (i : 'I_j) :
  perm_left Hx0 i = cast_to_j (enum_rank_in Hx0 (t (embed_left i))).
Proof. by rewrite permE. Qed.

Lemma enum_val_perm_left (x0 : 'I_n.+1) (Hx0 : x0 \in image_left t j) (i : 'I_j) :
  enum_val (cast_ord (esym (card_image_left t j)) (perm_left Hx0 i))
  = t (embed_left i).
Proof.
rewrite perm_leftE /cast_to_j cast_ordK.
by rewrite enum_rankK_in //; exact: mem_image_left.
Qed.

End PermOfLeft.


Lemma perm_left_witness_indep n (t : {perm 'I_n.+1}) (j : 'I_n.+2)
    (x0 y0 : 'I_n.+1)
    (Hx0 : x0 \in image_left t j) (Hy0 : y0 \in image_left t j) :
  perm_left Hx0 = perm_left Hy0.
Proof.
apply/permP ⇒ i; rewrite !perm_leftE /cast_to_j; congr cast_ord.
by apply: eq_enum_rank_in (mem_image_left t i).
Qed.


Lemma image_left_witness_pos n (t : {perm 'I_n.+1}) (j : 'I_n.+2) (Hj : 0 < j) :
  t (embed_left (j := j) (Ordinal Hj)) \in image_left t j.
Proof. exact: mem_image_left. Qed.



Section ImageRight.

Variables (n : nat) (t : {perm 'I_n.+1}) (j : 'I_n.+2).

Definition embed_right (i : 'I_(n.+1 - j)) : 'I_n.+1 :=
  cast_ord (subnKC (leqj_n1 j)) (rshift j i).

Lemma embed_right_inj : injective embed_right.
Proof.
move⇒ i1 i2 /(congr1 (cast_ord (esym (subnKC (leqj_n1 j))))).
rewrite !cast_ordK; exact: rshift_inj.
Qed.

Definition image_right : {set 'I_n.+1} :=
  [set t (embed_right i) | i : 'I_(n.+1 - j)].

Lemma t_embed_right_inj : injective (fun i : 'I_(n.+1 - j) ⇒ t (embed_right i)).
Proof. by apply: inj_comp; [exact: perm_inj | exact: embed_right_inj]. Qed.

Lemma card_image_right : #|image_right| = n.+1 - j.
Proof.
by rewrite /image_right -[RHS](card_ord (n.+1 - j)) -(card_imset _ t_embed_right_inj).
Qed.

Lemma mem_image_right (i : 'I_(n.+1 - j)) : t (embed_right i) \in image_right.
Proof. by apply/imsetP; ∃ i. Qed.

End ImageRight.


Section PermOfRight.

Variables (n : nat) (t : {perm 'I_n.+1}) (j : 'I_n.+2).

Definition cast_to_subj (k : 'I_(#|image_right t j|)) : 'I_(n.+1 - j) :=
  cast_ord (card_image_right t j) k.

Lemma cast_to_subj_inj : injective cast_to_subj.
Proof. by move⇒ a b /cast_ord_inj. Qed.

Definition perm_right_fun (x0 : 'I_n.+1)
    (Hx0 : x0 \in image_right t j) (i : 'I_(n.+1 - j)) : 'I_(n.+1 - j) :=
  cast_to_subj (enum_rank_in Hx0 (t (embed_right i))).

Lemma perm_right_fun_inj (x0 : 'I_n.+1) (Hx0 : x0 \in image_right t j) :
  injective (perm_right_fun Hx0).
Proof.
move⇒ i1 i2; rewrite /perm_right_fun ⇒ /cast_to_subj_inj.
move⇒ /(congr1 (@enum_val _ _)).
rewrite !enum_rankK_in; try exact: mem_image_right.
by move/perm_inj/embed_right_inj.
Qed.

Definition perm_right (x0 : 'I_n.+1) (Hx0 : x0 \in image_right t j)
  : {perm 'I_(n.+1 - j)} := perm (@perm_right_fun_inj x0 Hx0).

Lemma perm_rightE (x0 : 'I_n.+1) (Hx0 : x0 \in image_right t j)
    (i : 'I_(n.+1 - j)) :
  perm_right Hx0 i = cast_to_subj (enum_rank_in Hx0 (t (embed_right i))).
Proof. by rewrite permE. Qed.

Lemma enum_val_perm_right (x0 : 'I_n.+1) (Hx0 : x0 \in image_right t j)
    (i : 'I_(n.+1 - j)) :
  enum_val (cast_ord (esym (card_image_right t j)) (perm_right Hx0 i))
  = t (embed_right i).
Proof.
rewrite perm_rightE /cast_to_subj cast_ordK.
by rewrite enum_rankK_in //; exact: mem_image_right.
Qed.

End PermOfRight.

Lemma perm_right_witness_indep n (t : {perm 'I_n.+1}) (j : 'I_n.+2)
    (x0 y0 : 'I_n.+1)
    (Hx0 : x0 \in image_right t j) (Hy0 : y0 \in image_right t j) :
  perm_right Hx0 = perm_right Hy0.
Proof.
apply/permP ⇒ i; rewrite !perm_rightE /cast_to_subj; congr cast_ord.
by apply: eq_enum_rank_in (mem_image_right t i).
Qed.


Lemma sorted_ltn_val_enum n (A : {pred 'I_n}) :
  sorted ltn [seq \val i | i <- enum A].
Proof.
rewrite ltn_sorted_uniq_leq.
apply/andP; split.
- by rewrite map_inj_uniq ?enum_uniq //; exact: val_inj.
- rewrite sorted_map.
  apply: (sorted_filter (leT := relpre val (@leq))); first by move⇒ a b c; apply: leq_trans.
  have ->: Finite.enum (fintype_ordinal__canonical__fintype_Finite n) = enum 'I_n by rewrite enumT.
  by rewrite -sorted_map val_enum_ord; exact: iota_sorted.
Qed.

Lemma enum_val_ltn n (A : {pred 'I_n}) (i j : 'I_(#|A|)) :
  ((val (enum_val i)) < (val (enum_val j)))%N = ((i : nat) < (j : nat))%N.
Proof.
have Hlt := sorted_ltn_val_enum A.
have Hsz : size [seq \val k | k <- enum A] = #|A| by rewrite size_map -cardE.
have Hi : (i : nat) < size [seq \val k | k <- enum A] by rewrite Hsz; exact: ltn_ord.
have Hj : (j : nat) < size [seq \val k | k <- enum A] by rewrite Hsz; exact: ltn_ord.
have Henum : ∀ (k : 'I_(#|A|)),
    \val (enum_val k) = nth 0%N [seq \val k | k <- enum A] k.
  move⇒ k.
  rewrite /enum_val (nth_map (enum_default k)) //.
  by rewrite -cardE; exact: ltn_ord.
rewrite !Henum.
have Hleq : sorted leq [seq \val k | k <- enum A].
  by move: Hlt; rewrite ltn_sorted_uniq_leq ⇒ /andP[].
apply/idP/idP.
- move⇒ Hlt12.
  rewrite ltnNge; apply/negP ⇒ Hge.
  have Hge_app : nth 0%N [seq \val k | k <- enum A] j
                ≤ nth 0%N [seq \val k | k <- enum A] i.
    apply: (sorted_leq_nth (leT := leq) leq_trans leqnn 0%N Hleq);
      try by [rewrite inE | exact Hge].
  by rewrite leqNgt Hlt12 in Hge_app.
- move⇒ Hij.
  apply: (sorted_ltn_nth (leT := ltn) ltn_trans 0%N Hlt);
    by [rewrite inE | exact Hij].
Qed.

Lemma enum_rank_in_val_ltn n (A : {pred 'I_n}) (x0 : 'I_n) (Ax0 : x0 \in A)
    (a b : 'I_n) (Ha : a \in A) (Hb : b \in A) :
  ((enum_rank_in Ax0 a : nat) < (enum_rank_in Ax0 b : nat))%N
  = ((val a) < (val b))%N.
Proof.
have Ea : enum_val (enum_rank_in Ax0 a) = a by rewrite enum_rankK_in.
have Eb : enum_val (enum_rank_in Ax0 b) = b by rewrite enum_rankK_in.
have := enum_val_ltn (A := [eta A])
   (enum_rank_in Ax0 a) (enum_rank_in Ax0 b).
by rewrite Ea Eb.
Qed.


Lemma perm_left_lt_iff n (t : {perm 'I_n.+1}) (j : 'I_n.+2)
    (x0 : 'I_n.+1) (Hx0 : x0 \in image_left t j) (i i' : 'I_j) :
  ((perm_left Hx0 i : nat) < (perm_left Hx0 i' : nat))%N
  = ((val (t (embed_left i))) < (val (t (embed_left i'))))%N.
Proof.
rewrite !perm_leftE /cast_to_j /=.
exact: (enum_rank_in_val_ltn Hx0 (mem_image_left t i) (mem_image_left t i')).
Qed.


Lemma perm_right_lt_iff n (t : {perm 'I_n.+1}) (j : 'I_n.+2)
    (x0 : 'I_n.+1) (Hx0 : x0 \in image_right t j) (i i' : 'I_(n.+1 - j)) :
  ((perm_right Hx0 i : nat) < (perm_right Hx0 i' : nat))%N
  = ((val (t (embed_right i))) < (val (t (embed_right i'))))%N.
Proof.
rewrite !perm_rightE /cast_to_subj /=.
exact: (enum_rank_in_val_ltn Hx0 (mem_image_right t i) (mem_image_right t i')).
Qed.


Lemma leqj_pred_n n (j : 'I_n.+2) : j.-1 ≤ n.
Proof.
have := ltn_ord j; rewrite ltnS ⇒ Hj.
by case: (j : nat) Hj ⇒ [|j'] /=.
Qed.



Section DescentTranslate.

Variables (n : nat) (t : {perm 'I_n.+1}).

Variables (k : nat) (Hk : k.+1 < n.+2).

Let j : 'I_n.+2 := Ordinal Hk.
Let Hkn : k ≤ n := Hk.

Definition embed_desc_left (i : 'I_k) : 'I_n := widen_ord Hkn i.

Lemma is_descent_perm_left
    (x0 : 'I_n.+1) (Hx0 : x0 \in image_left t j) (i : 'I_k) :
  is_descent (perm_left Hx0) i
  = is_descent t (embed_desc_left i).
Proof.
rewrite /is_descent.
rewrite (perm_left_lt_iff Hx0).
have E1 : embed_left (j := j) (widen_ord (leqnSn k) i)
        = widen_ord (leqnSn n) (embed_desc_left i) :> 'I_n.+1.
  by apply/val_inj.
have E2 : embed_left (j := j) (lift ord0 i)
        = lift ord0 (embed_desc_left i) :> 'I_n.+1.
  by apply/val_inj ⇒ /=; rewrite /bump leq0n.
by rewrite E1 E2.
Qed.

End DescentTranslate.

Section DescentTranslateRight.

Variables (n : nat) (t : {perm 'I_n.+1}).
Variables (j : 'I_n.+2) (Hj : j < n.+1).

Lemma sub_succ : (n - j).+1 = n.+1 - j.
Proof. by rewrite subSn. Qed.


Lemma j_plus_lt_n (i : 'I_(n - j)) : j + i < n.
Proof.
have Hi := ltn_ord i.
by rewrite -ltn_subRL.
Qed.

Definition embed_desc_right (i : 'I_(n - j)) : 'I_n := Ordinal (j_plus_lt_n i).

Lemma is_descent_perm_right
    (x0 : 'I_n.+1) (Hx0 : x0 \in image_right t j) (i : 'I_(n - j)) :
  is_descent (cast_perm (esym sub_succ) (perm_right Hx0)) i
  = is_descent t (embed_desc_right i).
Proof.
rewrite /is_descent !cast_permE.
rewrite (perm_right_lt_iff Hx0).
set ci_w : 'I_(n.+1 - j) := cast_ord _ (widen_ord _ i).
set ci_l : 'I_(n.+1 - j) := cast_ord _ (lift _ _).
have E1 : embed_right (j := j) ci_w
        = widen_ord (leqnSn n) (embed_desc_right i) :> 'I_n.+1.
  by apply/val_inj.
have E2 : embed_right (j := j) ci_l
        = lift ord0 (embed_desc_right i) :> 'I_n.+1.
  by apply/val_inj ⇒ /=; rewrite /bump leq0n /= addnS.
by rewrite E1 E2.
Qed.

End DescentTranslateRight.


Lemma image_left_right_disjoint n (t : {perm 'I_n.+1}) (j : 'I_n.+2) :
  [disjoint image_left t j & image_right t j].
Proof.
rewrite -setI_eq0; apply/eqP/setP ⇒ x; rewrite !inE.
apply/negbTE; apply/negP ⇒ /andP[/imsetP[il _ Hl_eq] /imsetP[ir _ Hr_eq]].
have Hl := ltn_ord il.
have Hr : (j : nat) ≤ j + ir by exact: leq_addr.
have Heq : embed_left il = embed_right ir.
  by apply: (@perm_inj _ t); rewrite -Hl_eq Hr_eq.
have := congr1 \val Heq ⇒ /=.
by move⇒ Hv; move: Hl; rewrite Hv ltnNge Hr.
Qed.

Lemma image_left_right_cover n (t : {perm 'I_n.+1}) (j : 'I_n.+2) :
  image_left t j :|: image_right t j = [set: 'I_n.+1].
Proof.
apply/eqP; rewrite eqEcard; apply/andP; split; first by apply/subsetP ⇒ x _; rewrite inE.
rewrite cardsT card_ord cardsU.
rewrite (eqP (_ : (image_left t j :&: image_right t j == set0))).
- rewrite cards0 subn0 card_image_left card_image_right.
  by rewrite addnC subnK //; exact: leqj_n1.
- by have := image_left_right_disjoint t j; rewrite -setI_eq0.
Qed.

Lemma image_left_card_plus_right n (t : {perm 'I_n.+1}) (j : 'I_n.+2) :
  #|image_left t j| + #|image_right t j| = n.+1.
Proof.
by rewrite card_image_left card_image_right addnC subnK //; exact: leqj_n1.
Qed.






Section DescentSplit.

Variables (n : nat) (t : {perm 'I_n.+1}).
Variables (k : nat) (Hk : k.+1 < n.+2).

Let j : 'I_n.+2 := Ordinal Hk.
Let Hkn : k ≤ n := Hk.

Lemma descent_left_of_t (x0 : 'I_n.+1) (Hx0 : x0 \in image_left t j)
    (i : 'I_k) :
  (widen_ord Hkn i \in descent_set t) = (i \in descent_set (perm_left Hx0)).
Proof.
rewrite !mem_descent_set.
have := is_descent_perm_left Hx0 i.
by rewrite /embed_desc_left ⇒ →.
Qed.

End DescentSplit.

Section DescentSplitRight.

Variables (n : nat) (t : {perm 'I_n.+1}).
Variables (j : 'I_n.+2) (Hjn : j < n.+1).

Lemma descent_right_of_t (x0 : 'I_n.+1) (Hx0 : x0 \in image_right t j)
    (i : 'I_(n - j)) :
  (Ordinal (j_plus_lt_n i) \in descent_set t)
  = (i \in descent_set (cast_perm (esym (sub_succ Hjn)) (perm_right Hx0))).
Proof.
rewrite !mem_descent_set.
have := is_descent_perm_right Hjn Hx0 i.
by rewrite /embed_desc_right ⇒ →.
Qed.

End DescentSplitRight.



Section PhaseA.

Variables (n : nat) (t : {perm 'I_n.+1}) (k : nat) (Hk : k.+1 < n.+2).

Let j : 'I_n.+2 := Ordinal Hk.
Let Hkn : k ≤ n := Hk.

Definition descent_left_part : {set 'I_n} :=
  [set i : 'I_n | (val i < k) && is_descent t i].

Definition descent_boundary_part : {set 'I_n} :=
  [set i : 'I_n | (val i == k) && is_descent t i].

Definition descent_right_part : {set 'I_n} :=
  [set i : 'I_n | (val i > k) && is_descent t i].

Lemma descent_set_decomp_partition :
  descent_set t = descent_left_part :|: descent_boundary_part :|: descent_right_part.
Proof.
apply/setP ⇒ i; rewrite mem_descent_set !inE.
case Hi : (is_descent t i); rewrite ?andbT ?andbF /=.
- by case: (ltngtP (val i) k).
- by [].
Qed.

Lemma descent_left_boundary_disjoint :
  [disjoint descent_left_part & descent_boundary_part].
Proof.
rewrite -setI_eq0; apply/eqP/setP ⇒ i; rewrite !inE.
apply/negbTE/negP ⇒ /andP[/andP[Hl _] /andP[/eqP Hb _]].
by rewrite Hb ltnn in Hl.
Qed.

Lemma descent_left_right_disjoint :
  [disjoint descent_left_part & descent_right_part].
Proof.
rewrite -setI_eq0; apply/eqP/setP ⇒ i; rewrite !inE.
apply/negbTE/negP ⇒ /andP[/andP[Hl _] /andP[Hr _]].
by have := ltn_trans Hl Hr; rewrite ltnn.
Qed.

Lemma descent_boundary_right_disjoint :
  [disjoint descent_boundary_part & descent_right_part].
Proof.
rewrite -setI_eq0; apply/eqP/setP ⇒ i; rewrite !inE.
apply/negbTE/negP ⇒ /andP[/andP[/eqP Hb _] /andP[Hr _]].
by rewrite Hb ltnn in Hr.
Qed.

Lemma descent_left_part_image (x0 : 'I_n.+1) (Hx0 : x0 \in image_left t j) :
  descent_left_part = [set widen_ord Hkn i | i in descent_set (perm_left Hx0)].
Proof.
apply/setP ⇒ i; rewrite inE.
apply/idP/imsetP.
- case/andP ⇒ Hi_lt Hd.
  ∃ (Ordinal Hi_lt); last by apply/val_inj.
  rewrite mem_descent_set.
  have := is_descent_perm_left (k := k) (Hk := Hk) Hx0 (Ordinal Hi_lt).
  rewrite /embed_desc_left ⇒ →.
  by suff → : widen_ord (Hk : k ≤ n) (Ordinal Hi_lt) = i by []; apply/val_inj.
- case⇒ i' Hi' →.
  have Hlt : (val (widen_ord Hkn i') < k)%N = true by rewrite /= ltn_ord.
  rewrite Hlt /=.
  rewrite mem_descent_set in Hi'.
  have Heq : widen_ord Hkn i' = embed_desc_left Hk i' :> 'I_n by apply: val_inj.
  rewrite Heq.
  by have := is_descent_perm_left (k := k) (Hk := Hk) Hx0 i'; move⇒ <-.
Qed.

End PhaseA.


Section PhaseARight.

Variables (n : nat) (t : {perm 'I_n.+1}) (j : 'I_n.+2) (Hjn : j < n.+1).

Definition descent_right_part_R : {set 'I_n} :=
  [set i : 'I_n | (val j ≤ val i) && is_descent t i].

Lemma descent_right_part_R_image (x0 : 'I_n.+1) (Hx0 : x0 \in image_right t j) :
  descent_right_part_R =
  [set Ordinal (@j_plus_lt_n n j i) |
       i in descent_set (cast_perm (esym (sub_succ Hjn)) (perm_right Hx0))].
Proof.
apply/setP ⇒ i; rewrite inE.
apply/idP/imsetP.
- case/andP ⇒ Hji Hd.
  have Hi_lt_n : val i < n by exact: ltn_ord.
  have Hr_lt : val i - val j < n - val j.
    by rewrite ltn_sub2r //; exact: leq_ltn_trans Hji Hi_lt_n.
  pose r : 'I_(n - val j) := Ordinal Hr_lt.
  ∃ r.
  + rewrite mem_descent_set.
    have := @is_descent_perm_right n t j Hjn x0 Hx0 r.
    rewrite /embed_desc_right ⇒ →.
    suff → : Ordinal (@j_plus_lt_n n j r) = i :> 'I_n by [].
    by apply: val_inj ⇒ /=; rewrite addnC subnK.
  + by apply: val_inj ⇒ /=; rewrite addnC subnK.
- case⇒ r Hr →.
  have Hge : val j ≤ val (Ordinal (@j_plus_lt_n n j r)) by rewrite /= leq_addr.
  rewrite Hge /=.
  rewrite mem_descent_set in Hr.
  have := @is_descent_perm_right n t j Hjn x0 Hx0 r.
  move⇒ Heq.
  rewrite /embed_desc_right in Heq.
  by rewrite -Heq.
Qed.

End PhaseARight.



Section PhaseB.

Variables (n : nat) (j : 'I_n.+2) (L : {set 'I_n.+1}) (HL : #|L| = j).

Lemma cardCL_eq : #|~: L| = n.+1 - j.
Proof. by rewrite cardsCs setCK card_ord HL. Qed.

Variables (sL : {perm 'I_j}) (sR : {perm 'I_(n.+1 - j)}).

Definition castL (i : 'I_j) : 'I_(#|L|) := cast_ord (esym HL) i.
Definition castR (i : 'I_(n.+1 - j)) : 'I_(#|~: L|) :=
  cast_ord (esym cardCL_eq) i.
Definition leqj : (j : nat) ≤ n.+1 := ltnSE (ltn_ord j).

Definition split_pos (i : 'I_n.+1) : ('I_j + 'I_(n.+1 - j))%type :=
  match split (cast_ord (esym (subnKC leqj)) i) with
  | inl ileft ⇒ inl ileft
  | inr iright ⇒ inr iright
  end.

Definition assemble_fun (i : 'I_n.+1) : 'I_n.+1 :=
  match split_pos i with
  | inl iL ⇒ enum_val (castL (sL iL))
  | inr iR ⇒ enum_val (castR (sR iR))
  end.

Lemma split_pos_inj : injective split_pos.
Proof.
move⇒ i1 i2; rewrite /split_pos.
case: splitP ⇒ [u1 Hu1|u1 Hu1]; case: splitP ⇒ [u2 Hu2|u2 Hu2] //=.
- case⇒ Heq.
  apply: val_inj ⇒ /=.
  move: Hu1 Hu2 ⇒ /=.
  by move⇒ H1 H2; rewrite H1 H2 Heq.
- case⇒ Heq.
  move: Hu1 Hu2 ⇒ /= H1 H2.
  apply: val_inj ⇒ /=.
  by rewrite H1 H2 Heq.
Qed.

Lemma assemble_fun_inj : injective assemble_fun.
Proof.
move⇒ i1 i2; rewrite /assemble_fun.
case E1: (split_pos i1) ⇒ [u1|u1]; case E2: (split_pos i2) ⇒ [u2|u2].
- move/enum_val_inj/cast_ord_inj/perm_inj ⇒ Hu.
  apply: split_pos_inj.
  by rewrite E1 E2 Hu.
- move⇒ Hcontra.
  have HinL : enum_val (castL (sL u1)) \in L by exact: enum_valP.
  have HinR : enum_val (castR (sR u2)) \in ~: L by exact: enum_valP.
  rewrite Hcontra in HinL.
  by rewrite inE HinL in HinR.
- move⇒ Hcontra.
  have HinR : enum_val (castR (sR u1)) \in ~: L by exact: enum_valP.
  have HinL : enum_val (castL (sL u2)) \in L by exact: enum_valP.
  rewrite Hcontra in HinR.
  by rewrite inE HinL in HinR.
- move/enum_val_inj/cast_ord_inj/perm_inj ⇒ Hu.
  apply: split_pos_inj.
  by rewrite E1 E2 Hu.
Qed.

Definition assemble_perm : {perm 'I_n.+1} := perm assemble_fun_inj.

Lemma assemble_permE i : assemble_perm i = assemble_fun i.
Proof. by rewrite permE. Qed.

End PhaseB.


Section AssembleRoundTrip.

Variables (n : nat) (j : 'I_n.+2) (L : {set 'I_n.+1}) (HL : #|L| = j).
Variables (sL : {perm 'I_j}) (sR : {perm 'I_(n.+1 - j)}).

Let t := assemble_perm HL sL sR.

Lemma assemble_left (i : 'I_j) :
  t (embed_left (j := j) i) = enum_val (castL HL (sL i)).
Proof.
rewrite /t assemble_permE /assemble_fun /split_pos.
case: splitP ⇒ [u Hu|u Hu] /=.
- congr enum_val; congr castL; congr (sL _).
  apply: val_inj ⇒ /=.
  by move: Hu ⇒ /= →.
- exfalso.
  move: Hu ⇒ /=.
  rewrite /embed_left /=.
  move⇒ Heq.
  have Hi : (i : nat) < j by exact: ltn_ord.
  have : j ≤ i by rewrite Heq leq_addr.
  by rewrite leqNgt Hi.
Qed.

Lemma assemble_right (i : 'I_(n.+1 - j)) :
  t (embed_right (j := j) i) = enum_val (castR HL (sR i)).
Proof.
rewrite /t assemble_permE /assemble_fun /split_pos.
case: splitP ⇒ [u Hu|u Hu] /=.
- exfalso.
  move: Hu ⇒ /=.
  rewrite /embed_right /=.
  move⇒ Heq.
  have Hu' : (u : nat) < j by exact: ltn_ord.
  have : j ≤ u by rewrite -Heq leq_addr.
  by rewrite leqNgt Hu'.
- congr enum_val; congr castR; congr (sR _).
  apply: val_inj ⇒ /=.
  move: Hu ⇒ /=.
  rewrite /embed_right /= ⇒ Heq.
  by have := addnI Heq.
Qed.

Lemma assemble_image_left : image_left t j = L.
Proof.
apply/setP ⇒ x.
apply/imsetP/idP.
- case⇒ i _ →.
  rewrite assemble_left.
  exact: enum_valP.
- move⇒ HxL.
  pose i_card : 'I_(#|L|) := enum_rank_in HxL x.
  pose i_jj : 'I_j := cast_ord HL i_card.
  pose i_pre : 'I_j := (sL^-1)%g i_jj.
  ∃ i_pre ⇒ //.
  rewrite assemble_left.
  by rewrite /castL /i_pre permKV /i_jj cast_ordK enum_rankK_in.
Qed.

Lemma assemble_image_right : image_right t j = ~: L.
Proof.
apply/setP ⇒ x.
apply/imsetP/idP.
- case⇒ i _ →.
  rewrite assemble_right.
  exact: enum_valP.
- move⇒ HxNL.
  pose i_card : 'I_(#|~: L|) := enum_rank_in HxNL x.
  pose i_jj : 'I_(n.+1 - j) := cast_ord (cardCL_eq HL) i_card.
  pose i_pre : 'I_(n.+1 - j) := (sR^-1)%g i_jj.
  ∃ i_pre ⇒ //.
  rewrite assemble_right.
  by rewrite /castR /i_pre permKV /i_jj cast_ordK enum_rankK_in.
Qed.

End AssembleRoundTrip.


Section AssemblePermLeftRT.

Variables (n : nat) (j : 'I_n.+2) (L : {set 'I_n.+1}) (HL : #|L| = j).
Variables (sL : {perm 'I_j}) (sR : {perm 'I_(n.+1 - j)}).
Let t := assemble_perm HL sL sR.

Lemma assemble_perm_left (x0 : 'I_n.+1) (Hx0 : x0 \in image_left t j) :
  perm_left Hx0 = sL.
Proof.
apply/permP ⇒ i.
rewrite perm_leftE.
rewrite assemble_left.
have HL' : image_left t j = L := assemble_image_left HL sL sR.
have HmemImg : enum_val (castL HL (sL i)) \in image_left t j
  by rewrite HL'; exact: enum_valP.
apply: val_inj ⇒ /=.
have Henum : enum (image_left t j) = enum L by rewrite HL'.
have HuniqL : uniq (enum L) by exact: enum_uniq.
pose v := enum_val (castL HL (sL i)).
have Hv_in : v \in enum L by rewrite mem_enum; exact: enum_valP.
have Hidx : index v (enum L) = sL i.
  have Hv_nth : v = nth (enum_default (castL HL (sL i))) (enum L) (sL i).
    by rewrite /v (enum_val_nth (enum_default (castL HL (sL i)))).
  rewrite Hv_nth index_uniq //.
  have : (sL i : nat) < #|L| by rewrite HL; exact: ltn_ord.
  by rewrite cardE.
rewrite (unlock unlockable_enum_rank_in) /=.
rewrite Henum Hidx.
have HsL_card : (sL i : nat) < #|image_left t j|
  by rewrite card_image_left; exact: ltn_ord.
rewrite insubdK; first by [].
exact: HsL_card.
Qed.

Lemma assemble_perm_right (x0 : 'I_n.+1) (Hx0 : x0 \in image_right t j) :
  perm_right Hx0 = sR.
Proof.
apply/permP ⇒ i.
rewrite perm_rightE.
rewrite assemble_right.
have HR' : image_right t j = ~: L := assemble_image_right HL sL sR.
have HmemImg : enum_val (castR HL (sR i)) \in image_right t j
  by rewrite HR'; exact: enum_valP.
apply: val_inj ⇒ /=.
have Henum : enum (image_right t j) = enum (~: L) by rewrite HR'.
have HuniqR : uniq (enum (~: L)) by exact: enum_uniq.
pose v := enum_val (castR HL (sR i)).
have Hv_in : v \in enum (~: L) by rewrite mem_enum; exact: enum_valP.
have Hidx : index v (enum (~: L)) = sR i.
  have Hv_nth : v = nth (enum_default (castR HL (sR i))) (enum (~: L)) (sR i).
    by rewrite /v (enum_val_nth (enum_default (castR HL (sR i)))).
  rewrite Hv_nth index_uniq //.
  have : (sR i : nat) < #|~: L| by rewrite (cardCL_eq HL); exact: ltn_ord.
  by rewrite cardE.
rewrite (unlock unlockable_enum_rank_in) /=.
rewrite Henum Hidx.
have HsR_card : (sR i : nat) < #|image_right t j|
  by rewrite card_image_right; exact: ltn_ord.
rewrite insubdK; first by [].
exact: HsR_card.
Qed.

End AssemblePermLeftRT.



Section AssembleForwardLeft.
Variables (n : nat) (t : {perm 'I_n.+1}) (j : 'I_n.+2).

Definition card_image_left_eq : #|image_left t j| = j := card_image_left t j.

Variables (x0L : 'I_n.+1) (Hx0L : x0L \in image_left t j).
Variables (x0R : 'I_n.+1) (Hx0R : x0R \in image_right t j).

Lemma assemble_decomp_inverse_left (i : 'I_j) :
  assemble_perm card_image_left_eq (perm_left Hx0L) (perm_right Hx0R)
                (embed_left i) = t (embed_left i).
Proof.
rewrite assemble_left perm_leftE /cast_to_j /castL.
rewrite cast_ord_comp.
have Hetrans : etrans (card_image_left t j)
                (esym card_image_left_eq) = erefl _.
  exact: eq_irrelevance.
rewrite Hetrans cast_ord_id.
by rewrite enum_rankK_in //; exact: mem_image_left.
Qed.

End AssembleForwardLeft.


Lemma image_right_eq_compl n (t : {perm 'I_n.+1}) (j : 'I_n.+2) :
  image_right t j = ~: image_left t j.
Proof.
have Hcov := image_left_right_cover t j.
have Hdis := image_left_right_disjoint t j.
apply/setP ⇒ x; rewrite inE.
apply/idP/idP.
- move⇒ HinR; apply/negP ⇒ HinL.
  by have := disjointFr Hdis HinL; rewrite HinR.
- move⇒ HninL.
  have : x \in [set: 'I_n.+1] by rewrite inE.
  by rewrite -Hcov inE (negbTE HninL) /=.
Qed.


Section AssembleForwardRight.

Variables (n : nat) (t : {perm 'I_n.+1}) (j : 'I_n.+2).
Variables (x0L : 'I_n.+1) (Hx0L : x0L \in image_left t j).
Variables (x0R : 'I_n.+1) (Hx0R : x0R \in image_right t j).

Lemma assemble_decomp_inverse_right (i : 'I_(n.+1 - j)) :
  assemble_perm (card_image_left_eq t j) (perm_left Hx0L) (perm_right Hx0R)
                (embed_right i) = t (embed_right i).
Proof.
rewrite assemble_right.
have HR : image_right t j = ~: image_left t j := image_right_eq_compl t j.
rewrite -(enum_val_perm_right Hx0R i).
pose d := enum_default
            (cast_ord (esym (card_image_right t j)) (perm_right Hx0R i)).
have HenumEq : enum (image_right t j) = enum (~: image_left t j) by rewrite HR.
rewrite (enum_val_nth d (cast_ord _ (perm_right Hx0R i))) HenumEq.
by rewrite (enum_val_nth d (castR (card_image_left_eq t j) (perm_right Hx0R i))).
Qed.

End AssembleForwardRight.


Section AssembleDecompFull.

Variables (n : nat) (t : {perm 'I_n.+1}) (j : 'I_n.+2).
Variables (x0L : 'I_n.+1) (Hx0L : x0L \in image_left t j).
Variables (x0R : 'I_n.+1) (Hx0R : x0R \in image_right t j).

Lemma split_embed (y : 'I_n.+1) :
  (∃ i : 'I_j, y = embed_left i) ∨
  (∃ k : 'I_(n.+1 - j), y = embed_right k).
Proof.
have Hjn : (j : nat) ≤ n.+1 by exact: leqj_n1.
case: (ltnP y j) ⇒ Hyj.
- by left; ∃ (Ordinal Hyj); apply/val_inj.
- right.
  have Hjn1 : j < n.+1 by exact: leq_ltn_trans Hyj (ltn_ord y).
  have Hk : y - j < n.+1 - j by apply: ltn_sub2r ⇒ //; exact: ltn_ord.
  ∃ (Ordinal Hk); apply/val_inj ⇒ /=.
  by rewrite addnC subnK.
Qed.

Lemma assemble_decomp_inverse :
  assemble_perm (card_image_left_eq t j) (perm_left Hx0L) (perm_right Hx0R)
  = t.
Proof.
apply/permP ⇒ y.
case: (split_embed y) ⇒ [[i ->]|[k ->]].
- exact: assemble_decomp_inverse_left.
- exact: assemble_decomp_inverse_right.
Qed.

End AssembleDecompFull.



Section AssembleUnique.
Variables (n : nat) (j : 'I_n.+2) (L : {set 'I_n.+1}) (HL : #|L| = j).
Variables (sL : {perm 'I_j}) (sR : {perm 'I_(n.+1 - j)}).
Let t := assemble_perm HL sL sR.

Lemma assemble_decomp_unique
    (x0L : 'I_n.+1) (Hx0L : x0L \in image_left t j)
    (x0R : 'I_n.+1) (Hx0R : x0R \in image_right t j) :
  perm_left Hx0L = sL ∧ perm_right Hx0R = sR ∧ image_left t j = L.
Proof.
split; first by apply: assemble_perm_left.
split; first by apply: assemble_perm_right.
exact: assemble_image_left.
Qed.

End AssembleUnique.


Lemma eulerA_S2 n : eulerA n.+2 = beta (alt_desc_set n.+1).
Proof. by []. Qed.

Lemma two_eulerA_split n :
  2 × eulerA n.+2
  = beta (alt_desc_set n.+1) + beta (~: alt_desc_set n.+1).
Proof.
rewrite eulerA_S2 mul2n -addnn.
have <- := beta_compl (alt_desc_set n.+1).
by [].
Qed.



Lemma beta_eq_pair_sum n (D : {set 'I_n.+1}) :
  beta D
  = \sum_(tp : {perm 'I_n.+1} × 'I_n.+2)
      (descent_set (insert_max_perm tp.1 tp.2) == D).
Proof.
rewrite /beta -sum1dep_card.
rewrite (reindex _ (onW_bij _ (insert_max_perm_bij n))) /=.
by rewrite -big_mkcond /=.
Qed.

Lemma beta_eq_double_sum n (D : {set 'I_n.+1}) :
  beta D
  = \sum_(t : {perm 'I_n.+1}) \sum_(p : 'I_n.+2)
      (descent_set (insert_max_perm t p) == D).
Proof.
rewrite beta_eq_pair_sum.
by rewrite -(pair_bigA _ (fun t p ⇒ (descent_set (insert_max_perm t p) == D : nat))) /=.
Qed.

Lemma beta_eq_triple_split n (D : {set 'I_n.+1}) :
  beta D
  = \sum_(t : {perm 'I_n.+1})
      ((descent_set (insert_max_perm t ord0) == D)
       + (descent_set (insert_max_perm t ord_max) == D)
       + \sum_(j : 'I_n)
           (descent_set (insert_max_perm t (lift ord0 (widen_ord (leqnSn n) j))) == D)).
Proof.
rewrite beta_eq_double_sum.
apply: eq_bigr ⇒ t _.
rewrite big_ord_recl /= big_ord_recr /=.
have lom : lift ord0 (ord_max : 'I_n.+1) = (ord_max : 'I_n.+2) by apply/val_inj.
rewrite lom addnA addnAC.
by [].
Qed.


Lemma sum_partition_image_left n (j : 'I_n.+2) (R : Type) (idx : R)
    (op : Monoid.com_law idx) (P : {perm 'I_n.+1} → R) :
  \big[op/idx]_(t : {perm 'I_n.+1}) P t
  = \big[op/idx]_(L : {set 'I_n.+1} | #|L| == j)
       \big[op/idx]_(t : {perm 'I_n.+1} | image_left t j == L) P t.
Proof.
rewrite (partition_big (fun t : {perm 'I_n.+1} ⇒ image_left t j)
                       (fun L ⇒ #|L| == j)) //= ⇒ t _.
by rewrite card_image_left.
Qed.

Lemma assemble_perm_pirr n (j : 'I_n.+2) (L : {set 'I_n.+1})
    (HL HL' : #|L| = j)
    (sL : {perm 'I_j}) (sR : {perm 'I_(n.+1 - j)}) :
  assemble_perm HL sL sR = assemble_perm HL' sL sR.
Proof. by have → : HL = HL' by exact: eq_irrelevance. Qed.

Lemma assemble_decomp_inverse_gen n (t : {perm 'I_n.+1}) (j : 'I_n.+2)
    (L : {set 'I_n.+1}) (HL : #|L| = j) (HeqL : image_left t j = L)
    (xL : 'I_n.+1) (HxL : xL \in image_left t j)
    (xR : 'I_n.+1) (HxR : xR \in image_right t j) :
  assemble_perm HL (perm_left HxL) (perm_right HxR) = t.
Proof.
move: HL; rewrite -HeqL ⇒ HL'.
have → : HL' = card_image_left_eq t j by exact: eq_irrelevance.
exact: assemble_decomp_inverse.
Qed.

Lemma sub_gt0_n_j n (j : 'I_n.+2) (Hjn : j < n.+1) : 0 < n.+1 - j.
Proof. by rewrite subn_gt0. Qed.

Section InnerReindexBij.
Variables (n : nat) (j : 'I_n.+2) (Hj : 0 < j) (Hjn : j < n.+1).
Variables (L : {set 'I_n.+1}) (HL : #|L| = j).

Let xLcan (t : {perm 'I_n.+1}) : 'I_n.+1 := t (embed_left (j := j) (Ordinal Hj)).
Let xRcan (t : {perm 'I_n.+1}) : 'I_n.+1 :=
  t (embed_right (j := j) (Ordinal (sub_gt0_n_j Hjn))).

Let HxLcan t : xLcan t \in image_left t j := mem_image_left t (Ordinal Hj).
Let HxRcan t : xRcan t \in image_right t j :=
  mem_image_right t (Ordinal (sub_gt0_n_j Hjn)).

Definition fwdAss (s : {perm 'I_j} × {perm 'I_(n.+1 - j)}) : {perm 'I_n.+1} :=
  assemble_perm HL s.1 s.2.

Definition bwdAss (t : {perm 'I_n.+1}) : {perm 'I_j} × {perm 'I_(n.+1 - j)} :=
  (perm_left (HxLcan t), perm_right (HxRcan t)).

Lemma bwd_fwd s : bwdAss (fwdAss s) = s.
Proof.
case: s ⇒ sL sR; rewrite /bwdAss /fwdAss /=.
by congr pair; [exact: assemble_perm_left | exact: assemble_perm_right].
Qed.

Lemma fwd_bwd t : image_left t j = L → fwdAss (bwdAss t) = t.
Proof.
move⇒ HeqL; rewrite /fwdAss /bwdAss /=.
exact: assemble_decomp_inverse_gen.
Qed.

End InnerReindexBij.

Lemma sum_reindex_inner n (j : 'I_n.+2) (Hj : 0 < j) (Hjn : j < n.+1)
    (L : {set 'I_n.+1}) (HL : #|L| = j) (R : Type) (idx : R)
    (op : Monoid.com_law idx) (F : {perm 'I_n.+1} → R) :
  \big[op/idx]_(t : {perm 'I_n.+1} | image_left t j == L) F t
  = \big[op/idx]_(s : {perm 'I_j} × {perm 'I_(n.+1 - j)})
       F (assemble_perm HL s.1 s.2).
Proof.
rewrite (reindex (@fwdAss n j L HL)) /=.
- apply: eq_bigl ⇒ s; rewrite /fwdAss /=.
  by rewrite assemble_image_left eqxx.
- ∃ (@bwdAss n j Hj Hjn) ⇒ /=.
  + by move⇒ s _; rewrite (@bwd_fwd n j Hj Hjn).
  + move⇒ t /eqP HeqL.
    by rewrite (@fwd_bwd n j Hj Hjn L HL).
Qed.

Lemma imset_lift_eq n (h : 'I_n.+1) (S : {set 'I_n}) (D : {set 'I_n.+1}) :
  ([set lift h x | x in S] == D)
  = (h \notin D) && (S == [set x | lift h x \in D]).
Proof.
apply/eqP/andP ⇒ [<-|].
- split.
  + apply/imsetP ⇒ -[y _ /esym Hy].
    by have := neq_lift h y; rewrite Hy eqxx.
  + apply/eqP/setP ⇒ x; rewrite inE.
    apply/idP/idP.
    × by move⇒ Hx; apply/imsetP; ∃ x.
    × by case/imsetP ⇒ y Hy /lift_inj →.
- case⇒ /negbTE Hh /eqP HS.
  apply/setP ⇒ y; rewrite HS.
  apply/imsetP/idP.
  + by case⇒ x; rewrite inE ⇒ Hx →.
  + move⇒ HyD.
    case: (eqVneq h y) ⇒ [Hyeq|hny]; first by rewrite -Hyeq Hh in HyD.
    case/unlift_some : hny ⇒ x Hx _.
    by ∃ x; rewrite ?inE -Hx.
Qed.

Lemma interior_descent_set_eq n (t : {perm 'I_n.+1}) (j' : 'I_n)
    (D : {set 'I_n.+1}) :
  let h := widen_ord (leqnSn n) j' in
  (descent_set (insert_max_perm t (lift ord0 h)) == D)
  = (h \notin D)
    && (descent_set t :|: [set j']
         == [set x | lift h x \in D]).
Proof. by move⇒ h; rewrite descent_set_insert_max_interior imset_lift_eq. Qed.






Lemma alt_desc_set_is_alt m : set_is_alt (alt_desc_set m).
Proof.
apply/forallP ⇒ i; apply/forallP ⇒ j; apply/implyP ⇒ /eqP Hj.
by rewrite !mem_alt_desc_set Hj /=; case: (odd i).
Qed.

Lemma set_is_alt_indicator m (D : {set 'I_m.+1}) :
  ((D == alt_desc_set m.+1) + (D == ~: alt_desc_set m.+1) : nat)
  = set_is_alt D.
Proof.
have Hord0_alt : (ord0 : 'I_m.+1) \in alt_desc_set m.+1.
  by rewrite mem_alt_desc_set.
have Hord0_nalt : (ord0 : 'I_m.+1) \notin ~: alt_desc_set m.+1.
  by rewrite inE Hord0_alt.
have Halt_neq_nalt :
  (alt_desc_set m.+1 == ~: alt_desc_set m.+1) = false.
  apply/negP ⇒ /eqP Heq.
  have Hin : ord0 \in (alt_desc_set m.+1 : {set _}) by exact: Hord0_alt.
  by rewrite Heq inE Hord0_alt in Hin.
case Halt : (D == alt_desc_set m.+1) ⇒ /=.
- rewrite (eqP Halt) alt_desc_set_is_alt Halt_neq_nalt.
  by [].
- case Hnalt : (D == ~: alt_desc_set m.+1) ⇒ /=.
  + rewrite (eqP Hnalt).
    have : set_is_alt (~: alt_desc_set m.+1).
      apply/forallP ⇒ i; apply/forallP ⇒ j; apply/implyP ⇒ /eqP Hj.
      rewrite !inE Hj.
      by rewrite /= negbK; case: (odd i).
    by move⇒ →.
  + apply/esym; case Hsia : (set_is_alt D) ⇒ //.
    case: (set_is_alt_classify Hsia) ⇒ HD'.
    × by rewrite HD' eqxx in Halt.
    × by rewrite HD' eqxx in Hnalt.
Qed.

Lemma alt_plus_nalt_as_set_is_alt_sum n :
  beta (alt_desc_set n.+1) + beta (~: alt_desc_set n.+1)
  = \sum_(t : {perm 'I_n.+1}) \sum_(p : 'I_n.+2)
       set_is_alt (descent_set (insert_max_perm t p)).
Proof.
rewrite beta_eq_double_sum [beta (~: _)]beta_eq_double_sum -big_split /=.
apply: eq_bigr ⇒ t _; rewrite -big_split /=.
apply: eq_bigr ⇒ p _.
by rewrite -set_is_alt_indicator.
Qed.


Lemma sum_descent_set_indicator m (D : {set 'I_m}) :
  \sum_(t : {perm 'I_m.+1}) (descent_set t == D) = beta D.
Proof.
rewrite /beta -sum1dep_card big_mkcond /= [RHS]big_mkcond /=.
by apply: eq_bigr ⇒ t _; case: eqP.
Qed.

Lemma setU1_imset_lift_eq m (h : 'I_m.+1) (S : {set 'I_m}) (D : {set 'I_m.+1}) :
  (h |: [set lift h x | x in S] == D)
  = (h \in D) && (S == [set x | lift h x \in D]).
Proof.
apply/eqP/andP ⇒ [<-|].
- split; first by rewrite setU11.
  apply/eqP/setP ⇒ x; rewrite inE !inE.
  rewrite eq_sym (negbTE (neq_lift h x)) /=.
  by rewrite mem_imset //; exact: lift_inj.
- case⇒ Hh /eqP HS.
  apply/setP ⇒ y; rewrite !inE.
  case: (eqVneq y h) ⇒ [-> | yneh] /=; first by rewrite Hh.
  have hney : h != y by rewrite eq_sym.
  case: (unlift_some hney) ⇒ x → _.
  rewrite mem_imset; last exact: lift_inj.
  by rewrite HS inE.
Qed.

Lemma nat_of_andb (a b : bool) : ((a && b) : nat) = a × b.
Proof. by case: a; case: b. Qed.


Lemma sum_set_is_alt_ord0 n :
  \sum_(t : {perm 'I_n.+1})
      set_is_alt (descent_set (insert_max_perm t (ord0 : 'I_n.+2)))
  = eulerA n.+1.
Proof.
transitivity (\sum_(t : {perm 'I_n.+1}) (descent_set t == ~: alt_desc_set n : nat)).
  apply: eq_bigr ⇒ t _.
  rewrite -set_is_alt_indicator descent_set_insert_max_ord0 !setU1_imset_lift_eq.
  have → : ((ord0 : 'I_n.+1) \in alt_desc_set n.+1) = true.
    by rewrite mem_alt_desc_set.
  have → : ((ord0 : 'I_n.+1) \in ~: alt_desc_set n.+1) = false.
    by rewrite inE mem_alt_desc_set.
  rewrite /= addn0.
  have → : [set x : 'I_n | lift ord0 x \in alt_desc_set n.+1]
            = ~: alt_desc_set n.
    by apply/setP ⇒ x; rewrite !inE negbK /=.
  by [].
by rewrite sum_descent_set_indicator -beta_compl.
Qed.

Lemma sum_set_is_alt_ord_max n :
  \sum_(t : {perm 'I_n.+1})
      set_is_alt (descent_set (insert_max_perm t (ord_max : 'I_n.+2)))
  = eulerA n.+1.
Proof.
transitivity (\sum_(t : {perm 'I_n.+1})
    (descent_set t == (if odd n then alt_desc_set n else ~: alt_desc_set n)
     : nat)).
  apply: eq_bigr ⇒ t _.
  rewrite -set_is_alt_indicator descent_set_insert_max_ord_max !imset_lift_eq.
  have → : ((ord_max : 'I_n.+1) \notin alt_desc_set n.+1) = odd n.
    by rewrite mem_alt_desc_set negbK.
  have → : ((ord_max : 'I_n.+1) \notin ~: alt_desc_set n.+1) = ~~ odd n.
    by rewrite inE negbK mem_alt_desc_set.
  have → : [set x : 'I_n | lift ord_max x \in alt_desc_set n.+1]
            = alt_desc_set n.
    by apply/setP ⇒ x; rewrite !inE /= /bump leqNgt ltn_ord /=.
  have → : [set x : 'I_n | lift ord_max x \in ~: alt_desc_set n.+1]
            = ~: alt_desc_set n.
    by apply/setP ⇒ x; rewrite !inE /= /bump leqNgt ltn_ord /=.
  by case: (odd n) ⇒ /=; rewrite ?addn0 ?add0n.
by case: (odd n); rewrite sum_descent_set_indicator // -beta_compl.
Qed.


Definition andre_target n (c : 'I_n) : {set 'I_n} :=
  [set x : 'I_n | odd (lift (widen_ord (leqnSn n) c) x) (+) odd c].

Lemma interior_set_is_alt n (t : {perm 'I_n.+1}) (c : 'I_n) :
  (set_is_alt
     (descent_set (insert_max_perm t (lift ord0 (widen_ord (leqnSn n) c))))
   : nat)
  = (descent_set t :|: [set c] == andre_target c).
Proof.
rewrite -set_is_alt_indicator descent_set_insert_max_interior !imset_lift_eq.
have → : (widen_ord (leqnSn n) c \notin alt_desc_set n.+1) = odd c.
  by rewrite mem_alt_desc_set negbK.
have → : (widen_ord (leqnSn n) c \notin ~: alt_desc_set n.+1) = ~~ odd c.
  by rewrite inE negbK mem_alt_desc_set.
case Hc: (odd c) ⇒ /=; rewrite ?addn0 ?add0n.
- have → : [set x : 'I_n | lift (widen_ord (leqnSn n) c) x \in alt_desc_set n.+1]
            = andre_target c.
    by apply/setP ⇒ x; rewrite !inE Hc addbT.
  by [].
- have → : [set x : 'I_n | lift (widen_ord (leqnSn n) c) x \in ~: alt_desc_set n.+1]
            = andre_target c.
    by apply/setP ⇒ x; rewrite !inE Hc addbF negbK.
  by [].
Qed.

Section AndreInterior.

Variables (n : nat) (c : 'I_n).

Lemma andre_split_lt : c.+1 < n.+2.
Proof. by rewrite !ltnS ltnW // ltn_ord. Qed.

Let s : 'I_n.+2 := Ordinal andre_split_lt.

Lemma andre_s_ltn : s < n.+1.
Proof. by rewrite /= ltnS ltn_ord. Qed.

Lemma andre_target_lt (x : 'I_n) : x < c →
  (x \in andre_target c) = odd x (+) odd c.
Proof. by move⇒ Hx; rewrite inE /= /bump leqNgt Hx. Qed.

Lemma andre_target_at : (c \in andre_target c) = true.
Proof. by rewrite inE /= /bump leqnn /= addNb addbb. Qed.

Lemma andre_target_gt (x : 'I_n) : c < x →
  (x \in andre_target c) = ~~ (odd x (+) odd c).
Proof. by move⇒ Hx; rewrite inE /= /bump (ltnW Hx) /= addNb. Qed.

Lemma andre_union_eq_split (t : {perm 'I_n.+1})
    (xL : 'I_n.+1) (HxL : xL \in image_left t s)
    (xR : 'I_n.+1) (HxR : xR \in image_right t s) :
  (descent_set t :|: [set c] == andre_target c)
  = (descent_set (perm_left HxL) == [set i : 'I_c | odd i (+) odd c])
    && (descent_set (cast_perm (esym (sub_succ andre_s_ltn)) (perm_right HxR))
        == [set i : 'I_(n - c.+1) | odd i]).
Proof.
apply/eqP/andP ⇒ [Hset | [/eqP HL /eqP HR]].
- split; apply/eqP; apply/setP ⇒ i.
  + rewrite -(descent_left_of_t (k:=c) (Hk:=andre_split_lt) HxL).
    set w := widen_ord _ i.
    have Hne : (w == c) = false.
      by rewrite -val_eqE /= ltn_eqF // ltn_ord.
    have → : (w \in descent_set t) = (w \in descent_set t :|: [set c]).
      by rewrite !inE Hne orbF.
    by rewrite Hset andre_target_lt ?inE //= ltn_ord.
  + rewrite -(descent_right_of_t andre_s_ltn HxR).
    set y := Ordinal _.
    have Hcy : c < y by apply: ltn_addr.
    have Hne : (y == c) = false by rewrite -val_eqE /= gtn_eqF.
    have → : (y \in descent_set t) = (y \in descent_set t :|: [set c]).
      by rewrite !inE Hne orbF.
    rewrite Hset andre_target_gt // inE /= oddD /=.
    by case: (odd c); case: (odd i).
- apply/setP ⇒ x; rewrite in_setU in_set1.
  case: (ltngtP (val x) (val c)) ⇒ [Hlt|Hgt|Heq]; last 1 first.
  + have → : x = c by apply: val_inj.
    by rewrite eqxx orbT andre_target_at.
  + have → : x = @widen_ord c n andre_split_lt (Ordinal Hlt).
      by apply: val_inj.
    rewrite (descent_left_of_t (k:=c) (Hk:=andre_split_lt) HxL) HL.
    rewrite andre_target_lt //= !inE /=.
    by rewrite -val_eqE /= ltn_eqF // orbF.
  + have Hcn : c.+1 < n by exact: leq_ltn_trans Hgt (ltn_ord x).
    have Hi : (val x) - c.+1 < n - c.+1.
      by apply: ltn_sub2r ⇒ //; exact: ltn_ord.
    have → : x = Ordinal (j_plus_lt_n (j:=s) (Ordinal Hi)).
      by apply: val_inj; rewrite /= subnKC.
    rewrite (descent_right_of_t andre_s_ltn HxR) HR inE.
    rewrite andre_target_gt /= ?subnKC //.
    rewrite -val_eqE /= subnKC // gtn_eqF // orbF oddD /=.
    by case: (odd c); case: (odd (val x - c.+1)).
Qed.

Lemma beta_andre_left : beta [set i : 'I_c | odd i (+) odd c] = eulerA c.+1.
Proof.
case Hc: (odd c).
- have → : [set i : 'I_c | odd i (+) true] = alt_desc_set c.
    by apply/setP ⇒ i; rewrite !inE addbT.
  by [].
- have → : [set i : 'I_c | odd i (+) false] = ~: alt_desc_set c.
    by apply/setP ⇒ i; rewrite !inE addbF negbK.
  by rewrite -beta_compl.
Qed.

Lemma beta_andre_right :
  beta [set i : 'I_(n - c.+1) | odd i] = eulerA (n - c).
Proof.
have → : [set i : 'I_(n - c.+1) | odd i] = ~: alt_desc_set (n - c.+1).
  by apply/setP ⇒ i; rewrite !inE negbK.
rewrite -beta_compl.
by rewrite -(subnSK (ltn_ord c)).
Qed.

Lemma andre_interior_count :
  \sum_(t : {perm 'I_n.+1})
      ((descent_set t :|: [set c] == andre_target c) : nat)
  = 'C(n.+1, c.+1) × (eulerA c.+1 × eulerA (n - c)).
Proof.
have Hs0 : 0 < s by [].
rewrite (sum_partition_image_left s).
transitivity (\sum_(L : {set 'I_n.+1} | #|L| == s :> nat)
                (eulerA c.+1 × eulerA (n - c))).
  apply: eq_bigr ⇒ L /eqP HL.
  rewrite (sum_reindex_inner Hs0 andre_s_ltn HL).
  transitivity (\sum_(s0 : {perm 'I_s} × {perm 'I_(n.+1 - s)})
      (((descent_set s0.1 == [set i : 'I_c | odd i (+) odd c]) : nat)
       × ((descent_set (cast_perm (esym (sub_succ andre_s_ltn)) s0.2)
           == [set i : 'I_(n - c.+1) | odd i]) : nat))).
    apply: eq_bigr ⇒ -[sL sR] _ /=.
    rewrite (andre_union_eq_split
               (image_left_witness_pos (assemble_perm HL sL sR) Hs0)
               (mem_image_right (assemble_perm HL sL sR)
                  (Ordinal (sub_gt0_n_j andre_s_ltn)))).
    by rewrite assemble_perm_left assemble_perm_right nat_of_andb.
  rewrite -(pair_bigA _ (fun sL sR ⇒
      ((descent_set sL == [set i : 'I_c | odd i (+) odd c]) : nat)
      × ((descent_set (cast_perm (esym (sub_succ andre_s_ltn)) sR)
          == [set i : 'I_(n - c.+1) | odd i]) : nat))) /=.
  transitivity
    ((\sum_(sL : {perm 'I_s})
        ((descent_set sL == [set i : 'I_c | odd i (+) odd c]) : nat))
     × (\sum_(sR : {perm 'I_(n.+1 - s)})
          ((descent_set (cast_perm (esym (sub_succ andre_s_ltn)) sR)
            == [set i : 'I_(n - c.+1) | odd i]) : nat))).
    by rewrite big_distrl /=; apply: eq_bigr ⇒ sL _; rewrite big_distrr.
  congr (_ × _); first by rewrite sum_descent_set_indicator beta_andre_left.
  rewrite (reindex (cast_perm (sub_succ andre_s_ltn))) /=; last first.
    apply: onW_bij.
    by ∃ (cast_perm (esym (sub_succ andre_s_ltn)));
      [exact: cast_permK | exact: cast_permKV].
  transitivity (\sum_(u : {perm 'I_(n - c.+1).+1})
      ((descent_set u == [set i : 'I_(n - c.+1) | odd i]) : nat)).
    by apply: eq_bigr ⇒ u _; rewrite cast_permK.
  by rewrite sum_descent_set_indicator beta_andre_right.
rewrite (eq_bigl (fun L : {set 'I_n.+1} ⇒
    L \in [set A : {set 'I_n.+1} | #|A| == c.+1])); last first.
  by move⇒ A; rewrite inE.
by rewrite sum_nat_const card_draws card_ord.
Qed.

End AndreInterior.

Lemma sum_set_is_alt_eq_andre_sum n :
  \sum_(t : {perm 'I_n.+1}) \sum_(p : 'I_n.+2)
       set_is_alt (descent_set (insert_max_perm t p))
  = \sum_(k < n.+2) 'C(n.+1, k) × eulerA k × eulerA (n.+1 - k).
Proof.
transitivity (\sum_(t : {perm 'I_n.+1})
   (set_is_alt (descent_set (insert_max_perm t ord0))
    + set_is_alt (descent_set (insert_max_perm t (ord_max : 'I_n.+2)))
    + \sum_(j < n) ((descent_set t :|: [set j] == andre_target j) : nat))).
  apply: eq_bigr ⇒ t _.
  rewrite big_ord_recl big_ord_recr /=.
  have lom : lift ord0 (ord_max : 'I_n.+1) = (ord_max : 'I_n.+2).
    by apply/val_inj.
  rewrite lom addnA addnAC.
  congr (_ + _).
  by apply: eq_bigr ⇒ j _; rewrite interior_set_is_alt.
rewrite big_split /= big_split /=.
rewrite sum_set_is_alt_ord0 sum_set_is_alt_ord_max.
rewrite exchange_big /=.
rewrite (eq_bigr (fun j : 'I_n ⇒
    'C(n.+1, (val j).+1) × eulerA (val j).+1 × eulerA (n - val j)));
  last by move⇒ j _; rewrite andre_interior_count mulnA.
rewrite big_ord_recl big_ord_recr /=.
rewrite bin0 /bump !leq0n !add1n !add0n binn subnn muln1 !mul1n.
rewrite (eq_bigr (fun i : 'I_n ⇒
    'C(n.+1, (val i).+1) × euler (val i) × eulerA (n - val i))) //.
have → : eulerA 0 = 1 by [].
rewrite muln1.
by rewrite addnA addnAC.
Qed.

Lemma boundary_cancellation_alt n :
  beta (alt_desc_set n.+1) + beta (~: alt_desc_set n.+1)
  = \sum_(k < n.+2) 'C(n.+1, k) × eulerA k × eulerA (n.+1 - k).
Proof.
by rewrite alt_plus_nalt_as_set_is_alt_sum sum_set_is_alt_eq_andre_sum.
Qed.

Theorem euler_rec n :
  2 × eulerA n.+2
  = \sum_(k < n.+2) 'C(n.+1, k) × eulerA k × eulerA (n.+1 - k).
Proof.
by rewrite two_eulerA_split boundary_cancellation_alt.
Qed.


Example euler_rec_n0 :
  2 × eulerA 2 = \sum_(k < 2) 'C(1, k) × eulerA k × eulerA (1 - k).
Proof. exact: euler_rec. Qed.


Example euler_rec_n0_direct :
  2 × eulerA 2 = \sum_(k < 2) 'C(1, k) × eulerA k × eulerA (1 - k).
Proof.
rewrite eulerA_2 muln1 big_ord_recl big_ord_recr big_ord0 /=.
by rewrite /bump /= !add0n euler_0.
Qed.

Example euler_rec_n1_via :
  2 × eulerA 3 = \sum_(k < 3) 'C(2, k) × eulerA k × eulerA (2 - k).
Proof. exact: euler_rec. Qed.

Example euler_rec_n2_via :
  2 × eulerA 4 = \sum_(k < 4) 'C(3, k) × eulerA k × eulerA (3 - k).
Proof. exact: euler_rec. Qed.