Library mathcomp_eulerian.beta_bridge

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

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


Definition set_to_seq (n : nat) (D : {set 'I_n}) : seq nat :=
  sort leq [seq val i | i <- enum D].

Lemma mem_set_to_seq n (D : {set 'I_n}) (k : nat) :
  (k \in set_to_seq D) = (k \in [seq val i | i <- enum D]).
Proof. by rewrite mem_sort. Qed.

Lemma mem_set_to_seq_iff n (D : {set 'I_n}) (k : nat) :
  (k \in set_to_seq D) =
  has (fun i ⇒ val i == k) (enum D).
Proof.
rewrite mem_set_to_seq.
elim: (enum D) ⇒ [| x xs IH] //=.
rewrite in_cons IH.
by congr orb.
Qed.

Lemma mem_set_to_seq_ord n (D : {set 'I_n}) (i : 'I_n) :
  (val i \in set_to_seq D) = (i \in D).
Proof.
rewrite mem_set_to_seq_iff.
apply/hasP/idP.
- case⇒ j Hj /eqP Hv.
  have → : i = j by apply/val_inj.
  by rewrite mem_enum in Hj.
- move⇒ Hi; ∃ i ⇒ //.
  by rewrite mem_enum.
Qed.

Lemma uniq_set_to_seq n (D : {set 'I_n}) :
  uniq (set_to_seq D).
Proof.
rewrite sort_uniq map_inj_uniq ?enum_uniq //.
by move⇒ x y /= /val_inj.
Qed.

Lemma set_to_seq_bound n (D : {set 'I_n}) (k : nat) :
  k \in set_to_seq D → k < n.
Proof.
rewrite mem_set_to_seq ⇒ /mapP [i _ ->].
exact: ltn_ord.
Qed.


Definition omega_seq_local (s : seq nat) : seq nat :=
  [seq k <- iota 0 (foldr maxn 0 s).+1
   | (k \in s) != ((k.+1) \in s)].


Lemma foldr_maxn_set_to_seq_lb n (D : {set 'I_n}) (k : nat) :
  k \in set_to_seq D → k ≤ foldr maxn 0 (set_to_seq D).
Proof.
elim: (set_to_seq D) ⇒ [| x xs IH] //=.
rewrite in_cons ⇒ /orP [/eqP → | /IH Hle].
- by rewrite leq_maxl.
- exact: leq_trans Hle (leq_maxr _ _).
Qed.

Lemma omega_set_seq_local_bridge (m : nat)
    (D : {set 'I_m.+1}) (k : 'I_m) :
  (k \in omega_set D) =
  (val k \in omega_seq_local (set_to_seq D)).
Proof.
rewrite mem_omega_set /omega_seq_local mem_filter mem_iota
        /= add0n.
pose w := widen_ord (leqnSn m) k.
pose l := lift ord0 k.
have Hwv : val w = val k by [].
have Hlv : val l = (val k).+1
  by rewrite /l /= /bump /= add1n.
rewrite -(mem_set_to_seq_ord D w) Hwv.
rewrite -(mem_set_to_seq_ord D l) Hlv.
set b := (_ != _).
case Hb: b ⇒ /=; last by [].
move: Hb; rewrite /b {b}.
case Hk: (val k \in set_to_seq D);
  case Hk1: ((val k).+1 \in set_to_seq D) ⇒ //= _.
-
  have := foldr_maxn_set_to_seq_lb Hk.
  by move⇒ ?; rewrite ltnS.
-
  have Hle := foldr_maxn_set_to_seq_lb Hk1.
  symmetry; apply/idP. rewrite ltnS.
  exact: leq_trans (leqnSn _) Hle.
Qed.