Library mathcomp_eulerian.beta_omega

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

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


Definition sym_diff (n : nat) (D E : {set 'I_n}) : {set 'I_n} :=
  (D :\: E) :|: (E :\: D).

Definition toggle_at (n : nat) (D : {set 'I_n}) (i : 'I_n) : {set 'I_n} :=
  sym_diff D [set i].

Lemma toggle_at_in n (D : {set 'I_n}) (i j : 'I_n) :
  (j \in toggle_at D i) = (i == j) (+) (j \in D).
Proof.
rewrite /toggle_at /sym_diff !inE eq_sym.
by case: eqP ⇒ _ /=; case: (j \in D).
Qed.

Lemma toggle_atK n (D : {set 'I_n}) (i : 'I_n) :
  toggle_at (toggle_at D i) i = D.
Proof.
apply/setP ⇒ j; rewrite !toggle_at_in.
by case: eqP ⇒ _ /=; case: (j \in D).
Qed.

Lemma toggle_at_self n (D : {set 'I_n}) (i : 'I_n) :
  (i \in toggle_at D i) = ~~ (i \in D).
Proof. by rewrite toggle_at_in eqxx. Qed.

Lemma toggle_at_other n (D : {set 'I_n}) (i j : 'I_n) :
  i != j → (j \in toggle_at D i) = (j \in D).
Proof. by move⇒ H; rewrite toggle_at_in (negbTE H). Qed.


Definition omega_set (n : nat) (D : {set 'I_n.+1}) : {set 'I_n} :=
  [set k : 'I_n | (widen_ord (leqnSn n) k \in D) != (lift ord0 k \in D)].

Lemma mem_omega_set n (D : {set 'I_n.+1}) (k : 'I_n) :
  (k \in omega_set D) =
  ((widen_ord (leqnSn n) k \in D) != (lift ord0 k \in D)).
Proof. by rewrite inE. Qed.

Lemma toggle_at_omega_bit_i_new n (D : {set 'I_n.+1}) (i j : 'I_n.+1) :
  val j = (val i).+1 → i \in D → j \in D →
  ∃ k : 'I_n,
    [/\ widen_ord (leqnSn n) k = i,
        lift ord0 k = j,
        k \notin omega_set D &
        k \in omega_set (toggle_at D i)].
Proof.
move⇒ Hj Hi Hj'.
have Hik : val i < n.
  by have := ltn_ord j; rewrite Hj -ltnS.
pose k := Ordinal Hik.
have Ewid : widen_ord (leqnSn n) k = i by apply/val_inj.
have Elif : lift ord0 k = j by apply/val_inj; rewrite /= /bump /= add1n -Hj.
have Hij : i != j by rewrite -val_eqE Hj /=; elim: (val i).
∃ k; split ⇒ //.
  by rewrite mem_omega_set Ewid Elif Hi Hj'.
by rewrite mem_omega_set Ewid Elif toggle_at_self Hi /= toggle_at_other // Hj'.
Qed.

Lemma toggle_at_omega_strict_superset n
  (D : {set 'I_n.+1}) (i j : 'I_n.+1) :
  val j = (val i).+1 → i \in D → j \in D →
  (∀ p : 'I_n.+1, val p = (val i).-1 → val i != 0 → p \in D) →
  omega_set D \proper omega_set (toggle_at D i).
Proof.
move⇒ Hj Hi Hj' Hpred.
have [k [Ewid Elif Hknot Hkin]] := toggle_at_omega_bit_i_new Hj Hi Hj'.
apply/properP; split; last by ∃ k.
apply/subsetP ⇒ x Hx.
have Hij : i != j by rewrite -val_eqE Hj /=; elim: (val i).
rewrite mem_omega_set in Hx ×.
have Hxk : x != k.
  by apply/eqP ⇒ E; move: Hknot; rewrite -E mem_omega_set Hx.
case E0 : (val i == 0).
  have Hxwid : widen_ord (leqnSn n) x != i.
    apply/eqP ⇒ Exi; move/eqP: Hxk; apply; apply/val_inj.
    by move: (congr1 val Exi) (congr1 val Ewid); rewrite /= ⇒ <- <-.
  have Hxlif : lift ord0 x != i.
    by rewrite -val_eqE /= /bump /= add1n (eqP E0).
  by rewrite mem_omega_set !toggle_at_other //; rewrite eq_sym.
move/negbT: E0 ⇒ Hi0.
have Hxwid : widen_ord (leqnSn n) x != i.
  apply/eqP ⇒ Exi; move/eqP: Hxk; apply; apply/val_inj.
  by move: (congr1 val Exi) (congr1 val Ewid); rewrite /= ⇒ <- <-.
case Elxi : (lift ord0 x == i); last first.
  move/negbT: Elxi ⇒ Hxlif.
  by rewrite mem_omega_set !toggle_at_other //; rewrite eq_sym.
move/eqP: Elxi ⇒ Elxi.
have Hvx : val x = (val i).-1.
  have H := congr1 val Elxi.
  move: H; rewrite /= /bump /= add1n ⇒ H.
  by rewrite -H /=.
pose p := widen_ord (leqnSn n) x.
have Hvp : val p = (val i).-1 by rewrite /=.
have Hpd : p \in D by apply: Hpred.
rewrite mem_omega_set toggle_at_other; last by rewrite eq_sym.
rewrite Elxi toggle_at_self Hi /=.
by rewrite -/p Hpd.
Qed.

Lemma toggle_at_j_omega_bit_i_new n (D : {set 'I_n.+1}) (i j : 'I_n.+1) :
  val j = (val i).+1 → i \in D → j \in D →
  ∃ k : 'I_n,
    [/\ widen_ord (leqnSn n) k = i,
        lift ord0 k = j,
        k \notin omega_set D &
        k \in omega_set (toggle_at D j)].
Proof.
move⇒ Hj Hi Hj'.
have Hik : val i < n.
  by have := ltn_ord j; rewrite Hj -ltnS.
pose k := Ordinal Hik.
have Ewid : widen_ord (leqnSn n) k = i by apply/val_inj.
have Elif : lift ord0 k = j by apply/val_inj; rewrite /= /bump /= add1n -Hj.
have Hij : i != j by rewrite -val_eqE Hj /=; elim: (val i).
∃ k; split ⇒ //.
  by rewrite mem_omega_set Ewid Elif Hi Hj'.
rewrite mem_omega_set Ewid Elif.
have Hji : j != i by rewrite eq_sym.
by rewrite (toggle_at_other _ Hji) Hi toggle_at_self Hj'.
Qed.

Lemma toggle_at_j_omega_strict_superset n
  (D : {set 'I_n.+1}) (i j : 'I_n.+1) :
  val j = (val i).+1 → i \in D → j \in D →
  (∀ q : 'I_n.+1, val q = (val j).+1 → q \in D) →
  omega_set D \proper omega_set (toggle_at D j).
Proof.
move⇒ Hj Hi Hj' Hsucc.
have [k [Ewid Elif Hknot Hkin]] := toggle_at_j_omega_bit_i_new Hj Hi Hj'.
apply/properP; split; last by ∃ k.
apply/subsetP ⇒ x Hx.
have Hxk : x != k.
  by apply/eqP ⇒ E; subst x; move: Hknot; rewrite Hx.
have Hij : i != j by rewrite -val_eqE Hj /=; elim: (val i).
rewrite mem_omega_set in Hx ×.
case Elxj : (lift ord0 x == j).
- exfalso; move/eqP: Hxk; apply; apply/val_inj.
  have Hxval : val x = val i.
    have := congr1 val (eqP Elxj); rewrite /= /bump /= add1n Hj ⇒ [[]] //.
  rewrite Hxval; have := congr1 val Ewid; rewrite /= ⇒ <- //.
- case Ewxj : (widen_ord (leqnSn n) x == j).
  + rewrite mem_omega_set (eqP Ewxj) toggle_at_self Hj' /=.
    have Hlxnj : j != lift ord0 x by rewrite eq_sym; exact: negbT Elxj.
    rewrite toggle_at_other //.
    have Hvlx : val (lift ord0 x) = (val j).+1.
      have := congr1 val (eqP Ewxj); rewrite /= ⇒ Hvx.
      by rewrite /= /bump /= add1n Hvx.
    by rewrite (Hsucc _ Hvlx).
  + rewrite mem_omega_set.
    have Hwxnj : j != widen_ord (leqnSn n) x.
      by rewrite eq_sym; exact: negbT Ewxj.
    have Hlxnj : j != lift ord0 x by rewrite eq_sym; exact: negbT Elxj.
    by rewrite !toggle_at_other.
Qed.


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

Definition left_ok s i (l : 'I_n) : bool :=
  (val l ≤ val i)
  && [∀ k : 'I_n, (val l ≤ val k ≤ val i) ==> is_descent s k].

Definition right_ok s i (r : 'I_n) : bool :=
  (val i ≤ val r)
  && [∀ k : 'I_n, (val i ≤ val k ≤ val r) ==> is_descent s k].

Lemma left_ok_self s i : is_descent s i → left_ok s i i.
Proof.
move⇒ Hi; rewrite /left_ok leqnn /=.
apply/forallP ⇒ k; apply/implyP; case/andP ⇒ H1 H2.
by have → : k = i by apply/val_inj; apply/eqP; rewrite eqn_leq H2 H1.
Qed.

Lemma right_ok_self s i : is_descent s i → right_ok s i i.
Proof.
move⇒ Hi; rewrite /right_ok leqnn /=.
apply/forallP ⇒ k; apply/implyP; case/andP ⇒ H1 H2.
by have → : k = i by apply/val_inj; apply/eqP; rewrite eqn_leq H2 H1.
Qed.

Definition block_left s i : 'I_n :=
  if is_descent s i then [arg min_(l < i | left_ok s i l) val l]
  else i.

Definition block_right s i : 'I_n :=
  if is_descent s i then [arg max_(r > i | right_ok s i r) val r]
  else i.

Lemma block_left_left_ok s i : is_descent s i → left_ok s i (block_left s i).
Proof.
move⇒ Hi; rewrite /block_left Hi.
by case: arg_minnP; first exact: left_ok_self.
Qed.

Lemma block_right_right_ok s i :
  is_descent s i → right_ok s i (block_right s i).
Proof.
move⇒ Hi; rewrite /block_right Hi.
by case: arg_maxnP; first exact: right_ok_self.
Qed.

Lemma block_left_min s i (l : 'I_n) :
  is_descent s i → left_ok s i l → val (block_left s i) ≤ val l.
Proof.
move⇒ Hi Hl; rewrite /block_left Hi.
by case: arg_minnP; [exact: left_ok_self | move⇒ ? _; apply].
Qed.

Lemma block_right_max s i (r : 'I_n) :
  is_descent s i → right_ok s i r → val r ≤ val (block_right s i).
Proof.
move⇒ Hi Hr; rewrite /block_right Hi.
by case: arg_maxnP; [exact: right_ok_self | move⇒ ? _; apply].
Qed.

Lemma block_left_le s i :
  is_descent s i → val (block_left s i) ≤ val i.
Proof. by move⇒ /block_left_left_ok /andP[]. Qed.

Lemma block_right_ge s i :
  is_descent s i → val i ≤ val (block_right s i).
Proof. by move⇒ /block_right_right_ok /andP[]. Qed.

Lemma block_left_descent s i (k : 'I_n) :
  is_descent s i →
  val (block_left s i) ≤ val k ≤ val i → is_descent s k.
Proof.
move⇒ Hi Hk.
have /andP [_ /forallP /(_ k) /implyP /(_ Hk) //] := block_left_left_ok Hi.
Qed.

Lemma block_right_descent s i (k : 'I_n) :
  is_descent s i →
  val i ≤ val k ≤ val (block_right s i) → is_descent s k.
Proof.
move⇒ Hi Hk.
have /andP [_ /forallP /(_ k) /implyP /(_ Hk) //] := block_right_right_ok Hi.
Qed.

Lemma block_descent_chain s i (k : 'I_n) :
  is_descent s i →
  val (block_left s i) ≤ val k ≤ val (block_right s i) →
  is_descent s k.
Proof.
move⇒ Hi Hk; case/andP: Hk ⇒ H1 H2.
case: (leqP (val k) (val i)) ⇒ Hki.
  have Hr : val (block_left s i) ≤ val k ≤ val i by rewrite H1 Hki.
  exact: block_left_descent Hi Hr.
have Hr : val i ≤ val k ≤ val (block_right s i) by rewrite (ltnW Hki) H2.
exact: block_right_descent Hi Hr.
Qed.

Lemma block_left_le_right s i :
  is_descent s i → val (block_left s i) ≤ val (block_right s i).
Proof.
move⇒ Hi; apply: (leq_trans (block_left_le Hi) (block_right_ge Hi)).
Qed.

Lemma block_left_minimal s i :
  is_descent s i →
  ∀ l' : 'I_n, val l' = (val (block_left s i)).-1 →
  val (block_left s i) > 0 → ~~ is_descent s l'.
Proof.
move⇒ Hi l' Hl' Hpos; apply/negP ⇒ Hdes.
have Hok : left_ok s i l'.
  rewrite /left_ok; apply/andP; split.
    rewrite Hl'; apply: (leq_trans (leq_pred _) (block_left_le Hi)).
  apply/forallP ⇒ k; apply/implyP; case/andP ⇒ Hk1 Hk2.
  case: (leqP (val (block_left s i)) (val k)) ⇒ Hkb.
    have Hr : val (block_left s i) ≤ val k ≤ val i by rewrite Hkb Hk2.
    exact: block_left_descent Hi Hr.
  have Ek : k = l'.
    apply/val_inj; apply/eqP; rewrite eqn_leq.
    have Hkle : val k ≤ (val (block_left s i)).-1.
      by rewrite -ltnS prednK.
    by rewrite -Hl' in Hkle; rewrite Hkle Hk1.
  by rewrite Ek.
have := block_left_min Hi Hok; rewrite Hl' leqNgt ⇒ /negP; apply.
by rewrite prednK.
Qed.

Lemma block_right_maximal s i :
  is_descent s i →
  ∀ r' : 'I_n, val r' = (val (block_right s i)).+1 →
  ~~ is_descent s r'.
Proof.
move⇒ Hi r' Hr'; apply/negP ⇒ Hdes.
have Hok : right_ok s i r'.
  rewrite /right_ok; apply/andP; split.
    by rewrite Hr'; apply: (leq_trans (block_right_ge Hi)).
  apply/forallP ⇒ k; apply/implyP; case/andP ⇒ Hk1 Hk2.
  case: (leqP (val k) (val (block_right s i))) ⇒ Hkb.
    have Hr : val i ≤ val k ≤ val (block_right s i) by rewrite Hk1 Hkb.
    exact: block_right_descent Hi Hr.
  have Ek : k = r'.
    apply/val_inj; apply/eqP; rewrite eqn_leq.
    by rewrite Hr' Hkb /= -Hr' Hk2.
  by rewrite Ek.
have := block_right_max Hi Hok; rewrite Hr' leqNgt ⇒ /negP; apply.
by rewrite ltnS.
Qed.

Lemma block_chain_step s i (k : 'I_n) :
  is_descent s i →
  val (block_left s i) ≤ val k ≤ val (block_right s i) →
  s (widen_ord (leqnSn n) k) > s (lift ord0 k).
Proof. by move⇒ Hi Hk; have := block_descent_chain Hi Hk. Qed.

Lemma block_chain_values s i (p q : 'I_n.+1) :
  is_descent s i →
  val (block_left s i) ≤ val p → val q ≤ (val (block_right s i)).+1 →
  val p < val q → s p > s q.
Proof.
move⇒ Hi Hp Hq Hpq.
suff H : ∀ d (p' q' : 'I_n.+1),
    val q' = (val p' + d.+1)%N →
    val (block_left s i) ≤ val p' →
    val q' ≤ (val (block_right s i)).+1 →
    s p' > s q'.
  pose d := (val q - val p).-1.
  have Hd : val q = (val p + d.+1)%N.
    have Hsub : val q - val p > 0 by rewrite subn_gt0.
    rewrite /d prednK // addnBA; last exact: ltnW.
    by rewrite addnC addnK.
  exact: (H d p q Hd Hp Hq).
move⇒ {p q Hp Hq Hpq}.
move⇒ d; elim: d ⇒ [|d IH] p q Hq Hp Hqr.
  rewrite addn1 in Hq.
  have Hp_lt : val p < n.
    have Hle : (val p).+1 ≤ (val (block_right s i)).+1 by rewrite -Hq.
    rewrite ltnS in Hle.
    exact: (leq_ltn_trans Hle (ltn_ord _)).
  pose k := Ordinal Hp_lt.
  have Hk_range : val (block_left s i) ≤ val k ≤ val (block_right s i).
    rewrite /= Hp /=.
    have Hle : (val p).+1 ≤ (val (block_right s i)).+1 by rewrite -Hq.
    by rewrite ltnS in Hle.
  have Hstep := block_chain_step Hi Hk_range.
  have Ep : p = widen_ord (leqnSn n) k by apply/val_inj.
  have Eq : q = lift ord0 k.
    by apply/val_inj; rewrite /= /bump /= add1n Hq.
  by rewrite Ep Eq.
have Hp_le_br : val p ≤ val (block_right s i).
  have Hle : val p + d.+2 ≤ (val (block_right s i)).+1 by rewrite -Hq.
  by rewrite -ltnS; apply: (leq_trans _ Hle); rewrite addnS ltnS; apply: leq_addr.
have Hp_lt_n : val p < n by apply: (leq_ltn_trans Hp_le_br); apply: ltn_ord.
have Hp1_lt : (val p).+1 < n.+1 by rewrite ltnS.
pose p' := Ordinal Hp1_lt.
have Hp'_val : val p' = (val p).+1 by [].
pose k := Ordinal Hp_lt_n.
have Hk_range : val (block_left s i) ≤ val k ≤ val (block_right s i)
  by rewrite /= Hp /= Hp_le_br.
have Hstep := block_chain_step Hi Hk_range.
have Ep : p = widen_ord (leqnSn n) k by apply/val_inj.
have Ep' : p' = lift ord0 k by apply/val_inj; rewrite /= /bump /= add1n.
have step1 : s p > s p' by rewrite Ep Ep'.
have step2 : s p' > s q.
  apply: (IH p' q) ⇒ //.
    by rewrite Hp'_val Hq addnS.
  by apply: (leq_trans Hp); rewrite Hp'_val.
exact: (ltn_trans step2 step1).
Qed.

End FoataBlocks.