Library mathcomp_eulerian.descent

From mathcomp Require Import all_ssreflect fingroup perm.
From mathcomp_eulerian Require Import ordinal_reindex perm_compress.

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


Section Descent.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+1}) (i : 'I_n).

is_descent s i holds when s descends at position i, i.e. when s i > s (i+1). Stanley's predicate "i is a descent of w" (Stanley EC1, S1.4).
Definition is_descent s i : bool :=
  s (widen_ord (leqnSn n) i) > s (lift ord0 i).

descent_set s is the descent set of s, Stanley's D(w) (Stanley EC1, S1.4).
Definition descent_set s : {set 'I_n} := [set i | is_descent s i].

des s is the descent number of s, Stanley's d(w) = #D(w) (Stanley EC1, S1.4).
Definition des s : nat := #|descent_set s|.

asc s = n - des s is the ascent number of s.
Definition asc s : nat := n - des s.

Equivalence with the underlying boolean for rewriting. Membership in descent_set s is just is_descent s i; rewrites inE form.
Lemma mem_descent_set s i : (i \in descent_set s) = is_descent s i.
Proof. by rewrite inE. Qed.

Descent number is bounded by n, the number of consecutive positions.
Lemma des_le s : des s ≤ n.
Proof. by rewrite /des (leq_trans (max_card _)) // card_ord. Qed.

Descents and ascents partition the n consecutive positions.
Lemma des_add_asc s : des s + asc s = n.
Proof. by rewrite /asc subnKC // des_le. Qed.

The identity permutation has no descents.
Lemma des_id : des (1 : {perm 'I_n.+1}) = 0.
Proof.
apply/eqP; rewrite cards_eq0; apply/eqP/setP ⇒ i; rewrite !inE.
by rewrite /is_descent !perm1 ltnNge /= leqW.
Qed.

End Descent.


Section DescentDrop.
Variable n : nat.

Descents at interior positions are preserved by drop_perm: for s : {perm 'I_n.+2} and i : 'I_n, the descent of drop_perm s at i corresponds to the descent of s at widen_ord i.
End DescentDrop.


Section DescentReverse.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+1}).

rev_perm_ord is the reversal permutation i |-> n - i of 'I_n.+1.
Definition rev_perm_ord : {perm 'I_n.+1} := perm (@rev_ord_inj n.+1).

Equivalence with the underlying rev_ord for rewriting.
Lemma rev_perm_ordE (j : 'I_n.+1) : rev_perm_ord j = rev_ord j.
Proof. by rewrite permE. Qed.

rev_perm s is the reversal of s (compose with rev_perm_ord on the left). It corresponds to reading the one-line notation of s backwards.
Definition rev_perm s : {perm 'I_n.+1} := rev_perm_ord × s.

Defining equation: rev_perm s j = s (rev_ord j).
Lemma rev_permE s (j : 'I_n.+1) : rev_perm s j = s (rev_ord j).
Proof. by rewrite permM rev_perm_ordE. Qed.

Reversal swaps descents and ascents pointwise: i is a descent of rev_perm s iff rev_ord i is not a descent of s.
Lemma is_descent_rev s (i : 'I_n) :
  is_descent (rev_perm s) i = ~~ is_descent s (rev_ord i).
Proof.
rewrite /is_descent !rev_permE.
have E1 : rev_ord (widen_ord (leqnSn n) i) = lift ord0 (rev_ord i).
  by apply/val_inj; rewrite /= /bump /= add1n subSn // ltn_ord.
have E2 : rev_ord (lift ord0 i) = widen_ord (leqnSn n) (rev_ord i).
  by apply/val_inj; rewrite /= /bump /= add1n.
rewrite E1 E2.
set a := widen_ord _ _; set b := lift ord0 _.
have ab_ne : a != b by rewrite -val_eqE /= /bump /= add1n neq_ltn ltnSn.
have sab : s a != s b by apply: contra ab_ne ⇒ /eqP /perm_inj →.
by rewrite ltn_neqAle leqNgt sab /=.
Qed.

Descent count under reversal: des (rev_perm s) = n - des s. This is the involution underlying the symmetry eulerian n k = eulerian n (n-k).
Lemma des_rev_perm s : des (rev_perm s) = n - des s.
Proof.
rewrite /des /descent_set.
have revK : involutive (@rev_ord n) by move⇒ x; exact: rev_ordK.
rewrite -(card_imset _ (can_inj revK)).
have → : [set rev_ord x | x in [set i | is_descent (rev_perm s) i]]
= ~: [set i | is_descent s i].
  apply/setP ⇒ j; rewrite !inE; apply/imsetP/idP.
  + by case⇒ x; rewrite inE is_descent_rev ⇒ Hx →.
  + move⇒ Hj; ∃ (rev_ord j); first by rewrite inE is_descent_rev rev_ordK.
    by rewrite rev_ordK.
by rewrite cardsCs setCK card_ord.
Qed.

The reversal permutation n,n-1,...,0 has the maximal n descents.
End DescentReverse.