Library mathcomp_eulerian.perm_seq_bridge

From mathcomp Require Import all_ssreflect fingroup perm.
From mathcomp_eulerian Require Import
  ordinal_reindex perm_compress descent eulerian beta beta_omega beta_bridge.
Require Import mmtree psi_core psi_comm psi_descent_v2 psi_descent_thms.
Require Import psi_cdindex_core psi_cdindex_witness psi_cdindex_support.

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


Definition perm_to_seq n (s : {perm 'I_n}) : seq nat :=
  [seq val (s i) | i <- enum 'I_n].

Lemma perm_to_seq_size n (s : {perm 'I_n}) : size (perm_to_seq s) = n.
Proof. by rewrite /perm_to_seq size_map size_enum_ord. Qed.

Lemma perm_to_seq_uniq n (s : {perm 'I_n}) : uniq (perm_to_seq s).
Proof.
rewrite /perm_to_seq map_inj_uniq ?enum_uniq //.
move⇒ x y /= /val_inj; exact: perm_inj.
Qed.

Lemma nth_perm_to_seq n (s : {perm 'I_n}) k (Hk : k < n) :
  nth 0 (perm_to_seq s) k = val (s (Ordinal Hk)).
Proof.
rewrite /perm_to_seq (nth_map (Ordinal Hk)); last by rewrite size_enum_ord.
congr (val (s _)).
by apply: val_inj ⇒ /=; rewrite nth_enum_ord.
Qed.

Lemma perm_to_seq_inj n : injective (@perm_to_seq n).
Proof.
move⇒ s1 s2 Heq.
apply/permP ⇒ i.
have Hi := ltn_ord i.
have H := congr1 (fun w ⇒ nth 0 w (val i)) Heq.
rewrite !(nth_perm_to_seq _ Hi) in H.
have Hord : Ordinal Hi = i by apply: val_inj.
by rewrite Hord in H; apply: val_inj.
Qed.


Lemma is_descent_perm_seq n (s : {perm 'I_n.+1}) (i : 'I_n) :
  is_descent s i = is_descent_seq (perm_to_seq s) (val i).
Proof.
rewrite /is_descent /is_descent_seq.
have Hi : val i < n.+1 := leq_trans (ltn_ord i) (leqnSn n).
have Hi1 : (val i).+1 < n.+1.
  by rewrite ltnS; exact: ltn_ord.
rewrite (nth_perm_to_seq s Hi) (nth_perm_to_seq s Hi1).
by congr (_ > _); congr (val (s _)); apply: val_inj.
Qed.


Definition descent_to_bvec n (D : {set 'I_n}) : seq bool :=
  [seq (i \in D) | i <- enum 'I_n].

Lemma size_descent_to_bvec n (D : {set 'I_n}) :
  size (descent_to_bvec D) = n.
Proof. by rewrite /descent_to_bvec size_map size_enum_ord. Qed.

Lemma nth_descent_to_bvec n (D : {set 'I_n}) k (Hk : k < n) :
  nth false (descent_to_bvec D) k = (Ordinal Hk \in D).
Proof.
rewrite /descent_to_bvec (nth_map (Ordinal Hk)); last by rewrite size_enum_ord.
congr (_ \in D).
by apply: val_inj ⇒ /=; rewrite nth_enum_ord.
Qed.

Lemma char_mono_perm_to_seq n (s : {perm 'I_n.+1}) :
  char_mono (perm_to_seq s) = descent_to_bvec (descent_set s).
Proof.
apply: (@eq_from_nth _ false).
  by rewrite /char_mono size_map size_iota perm_to_seq_size
             /descent_to_bvec size_map size_enum_ord.
rewrite /char_mono size_map size_iota perm_to_seq_size ⇒ k Hk.
rewrite (nth_map 0); last by rewrite size_iota.
rewrite nth_iota // add0n.
rewrite /descent_to_bvec (nth_map (Ordinal Hk)); last by rewrite size_enum_ord.
have → : nth (Ordinal Hk) (enum 'I_n) k = Ordinal Hk.
  by apply: val_inj ⇒ /=; rewrite nth_enum_ord.
rewrite inE.
by symmetry; exact: is_descent_perm_seq.
Qed.

Lemma descent_to_bvec_inj n : injective (@descent_to_bvec n).
Proof.
move⇒ D1 D2 Heq.
apply/setP ⇒ i.
have Hi := ltn_ord i.
have Hord : Ordinal Hi = i by apply: val_inj.
have := congr1 (fun v ⇒ nth false v (val i)) Heq.
rewrite !nth_descent_to_bvec // Hord.
by move⇒ →.
Qed.




Lemma psi_apply_psis_comm i ss w :
  uniq w →
  apply_psis ss (psi i w) = psi i (apply_psis ss w).
Proof.
move⇒ Hu.
elim: ss w Hu ⇒ [|j ss IH] w Hu //=.
rewrite (psi_comm j i Hu).
exact: IH (uniq_psi _ Hu).
Qed.

Lemma apply_psis_rev ss w :
  uniq w →
  apply_psis (rev ss) w = apply_psis ss w.
Proof.
move⇒ Hu.
elim: ss w Hu ⇒ [|i ss IH] w Hu //=.
by rewrite rev_cons -cats1 apply_psis_cat /= IH // psi_apply_psis_comm.
Qed.

Lemma apply_psis_revK ss w :
  uniq w →
  apply_psis (rev ss) (apply_psis ss w) = w.
Proof.
move⇒ Hu.
elim: ss w Hu ⇒ [|i ss IH] w Hu //=.
rewrite -/(apply_psis ss (psi i w)) rev_cons -cats1 apply_psis_cat /=.
rewrite IH; last exact: uniq_psi.
exact: psi_involutive.
Qed.

Lemma apply_psis_cancel ss w :
  uniq w →
  apply_psis ss (apply_psis ss w) = w.
Proof.
move⇒ Hu.
rewrite -{1}(apply_psis_rev ss (uniq_apply_psis ss Hu)).
exact: apply_psis_revK.
Qed.

Lemma powerset_internal_apply_psis ops w :
  uniq w →
  powerset_internal (apply_psis ops w) =
  powerset_internal w.
Proof.
move⇒ Hu.
by rewrite /powerset_internal
   internal_vertices_apply_psis.
Qed.

Lemma class_char_monos_uniq w :
  uniq w →
  uniq [seq char_mono (apply_psis ss w) | ss <- powerset_internal w].
Proof.
move⇒ Hu.
have Hfact := fact3 Hu.
rewrite -(sort_uniq leq_seqb) Hfact sort_uniq.
exact: uniq_expand_cde.
Qed.

Lemma char_mono_class_inj w ss1 ss2 :
  uniq w →
  ss1 \in powerset_internal w →
  ss2 \in powerset_internal w →
  char_mono (apply_psis ss1 w) =
    char_mono (apply_psis ss2 w) →
  apply_psis ss1 w = apply_psis ss2 w.
Proof.
move⇒ Hu Hss1 Hss2 Hcm.
have Huniq_cm := class_char_monos_uniq Hu.
set g := fun ss ⇒
  char_mono (apply_psis ss w).
set psi_w := powerset_internal w.
have Hn1 :
  ss1 = nth [::] psi_w (index ss1 psi_w).
  by rewrite nth_index.
have Hn2 :
  ss2 = nth [::] psi_w (index ss2 psi_w).
  by rewrite nth_index.
have Hgn1 : g ss1 =
  nth (g [::]) [seq g s | s <- psi_w]
    (index ss1 psi_w).
  rewrite (nth_map [::]); last by rewrite index_mem.
  by rewrite -Hn1.
have Hgn2 : g ss2 =
  nth (g [::]) [seq g s | s <- psi_w]
    (index ss2 psi_w).
  rewrite (nth_map [::]); last by rewrite index_mem.
  by rewrite -Hn2.
have Hidxs : index ss1 psi_w <
  size [seq g s | s <- psi_w].
  by rewrite size_map index_mem.
have Hidxs2 : index ss2 psi_w <
  size [seq g s | s <- psi_w].
  by rewrite size_map index_mem.
have Hcm_idx :
  nth (g [::]) [seq g s | s <- psi_w]
    (index ss1 psi_w) =
  nth (g [::]) [seq g s | s <- psi_w]
    (index ss2 psi_w).
  by rewrite -Hgn1 -Hgn2 /g Hcm.
have := nth_uniq (g [::]) Hidxs Hidxs2
  Huniq_cm.
rewrite Hcm_idx eqxx ⇒ /esym/eqP Heq_idx.
have Hss_eq : ss1 = ss2
  by rewrite Hn1 Hn2 Heq_idx.
by rewrite Hss_eq.
Qed.


Lemma desc_positions_bvec n (D : {set 'I_n}) :
  [seq i <- iota 0 n | nth false (descent_to_bvec D) i] =
  set_to_seq D.
Proof.
apply: (sorted_eq leq_trans anti_leq).
- by apply: (sorted_filter leq_trans); exact: iota_sorted.
- by rewrite /set_to_seq; apply: sort_sorted; exact: leq_total.
- apply: uniq_perm.
  + by apply: filter_uniq; apply: iota_uniq.
  + exact: uniq_set_to_seq.
  move⇒ x.
  rewrite mem_filter mem_iota add0n mem_set_to_seq.
  apply/andP/mapP.
  + case⇒ Hnth Hx.
    ∃ (Ordinal Hx); last by [].
    by rewrite mem_enum -(nth_descent_to_bvec D Hx).
  + case⇒ i Hi →.
    rewrite mem_enum in Hi.
    split; last exact: ltn_ord.
    rewrite (nth_descent_to_bvec D (ltn_ord i)).
    by have → : Ordinal (ltn_ord i) = i by apply: val_inj.
Qed.


Section SeqToPerm.

Variable n : nat.
Variable w : seq nat.
Hypothesis Hsz : size w = n.
Hypothesis Huniq : uniq w.
Hypothesis Hbnd : all (fun x ⇒ x < n) w.

Lemma seq_nth_bound (i : 'I_n) : nth 0 w (val i) < n.
Proof.
have Hi : val i < size w by rewrite Hsz; exact: ltn_ord.
exact: (allP Hbnd _ (mem_nth 0 Hi)).
Qed.

Definition seq_to_fun (i : 'I_n) : 'I_n := Ordinal (seq_nth_bound i).

Lemma seq_to_fun_inj : injective seq_to_fun.
Proof.
move⇒ i j Heq.
apply/eqP; rewrite -(inj_eq val_inj) /=.
have Hi : val i < size w by rewrite Hsz; exact: ltn_ord.
have Hj : val j < size w by rewrite Hsz; exact: ltn_ord.
rewrite -(nth_uniq 0 Hi Hj Huniq).
suff → : nth 0 w (val i) = nth 0 w (val j) by [].
by have := congr1 val Heq.
Qed.

Definition seq_to_perm : {perm 'I_n} := perm (@seq_to_fun_inj).

Lemma seq_to_perm_nth (i : 'I_n) :
  val (seq_to_perm i) = nth 0 w (val i).
Proof. by rewrite permE. Qed.

End SeqToPerm.


Lemma perm_to_seq_bnd n (s : {perm 'I_n}) :
  all (fun x ⇒ x < n) (perm_to_seq s).
Proof. apply/allP ⇒ x /mapP [i _ ->]; exact: ltn_ord. Qed.

Lemma perm_to_seq_seq_to_perm n (w : seq nat)
  (Hsz : size w = n) (Hu : uniq w) (Hb : all (fun x ⇒ x < n) w) :
  perm_to_seq (seq_to_perm Hsz Hu Hb) = w.
Proof.
apply: (@eq_from_nth _ 0).
  by rewrite perm_to_seq_size Hsz.
move⇒ k Hk; rewrite perm_to_seq_size in Hk.
rewrite /perm_to_seq (nth_map (Ordinal Hk)); last by rewrite size_enum_ord.
have Hord : nth (Ordinal Hk) (enum 'I_n) k = Ordinal Hk
  by apply: val_inj ⇒ /=; rewrite nth_enum_ord.
by rewrite Hord /= permE /seq_to_fun.
Qed.

Lemma seq_to_perm_perm_to_seq n (s : {perm 'I_n}) :
  seq_to_perm (perm_to_seq_size s) (perm_to_seq_uniq s) (perm_to_seq_bnd s) = s.
Proof.
apply: (perm_to_seq_inj (n:=n)).
by rewrite perm_to_seq_seq_to_perm.
Qed.

Lemma all_bnd_apply_psis n ss w :
  all (fun x ⇒ x < n) w → uniq w →
  all (fun x ⇒ x < n) (apply_psis ss w).
Proof.
move⇒ Hbnd Hu; apply/allP ⇒ x Hx.
by apply: (allP Hbnd); rewrite -(perm_mem (perm_eq_apply_psis ss w)).
Qed.

Lemma apply_psis_size_eq n ss (w : seq nat) :
  size w = n → size (apply_psis ss w) = n.
Proof. move⇒ <-; exact: size_apply_psis. Qed.


Lemma uniq_expand_cde letters : uniq (expand_cde letters).
Proof.
elim: letters ⇒ [|[||] l IH] //=.
- rewrite cat_uniq !map_inj_uniq //; try by move⇒ x y [].
  rewrite IH andbT.
  apply/hasPn ⇒ x /mapP [t Ht ->].
  by apply/negP ⇒ /mapP [t' Ht' []].
- rewrite cat_uniq !map_inj_uniq //; try by move⇒ x y [] //.
  rewrite IH andbT.
  apply/hasPn ⇒ x /mapP [t Ht ->].
  by apply/negP ⇒ /mapP [t' Ht' []].
Qed.


Lemma nil_in_powerset_internal w : [::] \in powerset_internal w.
Proof.
rewrite /powerset_internal.
set ivs := internal_vertices w.
have : [::] \in [:: [::] : seq nat] by rewrite mem_seq1.
elim: ivs [:: [::]] ⇒ [|i ivs IH] acc Hin //=.
apply: IH.
rewrite mem_cat; apply/orP; left; exact: Hin.
Qed.

Lemma char_mono_in_expand_cde w :
  uniq w →
  char_mono w \in expand_cde (phi_w w).
Proof.
move⇒ Hu.
have Hfact := fact3 Hu.
have : char_mono w \in
  [seq char_mono (apply_psis ss w) | ss <- powerset_internal w].
  apply/mapP; ∃ [::]; first exact: nil_in_powerset_internal.
  by rewrite apply_psis_nil.
by rewrite -(mem_sort leq_seqb) Hfact mem_sort.
Qed.


Definition find_ss (w : seq nat) (bv : seq bool) : seq nat :=
  head [::] [seq ss <- powerset_internal w | char_mono (apply_psis ss w) == bv].

Lemma find_ss_spec w bv :
  uniq w →
  bv \in expand_cde (phi_w w) →
  find_ss w bv \in powerset_internal w ∧
  char_mono (apply_psis (find_ss w bv) w) = bv.
Proof.
move⇒ Hu Hbv.
rewrite /find_ss.
have Hmem : bv \in [seq char_mono (apply_psis ss w) | ss <- powerset_internal w].
  by rewrite -(mem_sort leq_seqb) (fact3 Hu) mem_sort.
have [ss Hss Heq] := mapP Hmem.
have Hfilter : ss \in [seq s <- powerset_internal w | char_mono (apply_psis s w) == bv].
  by rewrite mem_filter Hss andbT; apply/eqP.
set flt := [seq s <- _ | _].
have Hfilter' : ss \in flt by rewrite /flt.
have Hhead : head [::] flt \in flt.
  by case: (flt) Hfilter' ⇒ [//|x s] _; exact: mem_head.
rewrite mem_filter in Hhead.
by case/andP: Hhead ⇒ /eqP.
Qed.


Definition class_map n (bv : seq bool) (sigma : {perm 'I_n}) : {perm 'I_n} :=
  let w := perm_to_seq sigma in
  let ss := find_ss w bv in
  seq_to_perm (apply_psis_size_eq ss (perm_to_seq_size sigma))
              (uniq_apply_psis ss (perm_to_seq_uniq sigma))
              (all_bnd_apply_psis ss (perm_to_seq_bnd sigma) (perm_to_seq_uniq sigma)).

Lemma perm_to_seq_class_map n bv (sigma : {perm 'I_n}) :
  perm_to_seq (class_map bv sigma) =
  apply_psis (find_ss (perm_to_seq sigma) bv) (perm_to_seq sigma).
Proof. by rewrite /class_map perm_to_seq_seq_to_perm. Qed.


Lemma omega_seq_mem_eq (s : seq nat) k :
  (k \in omega_seq s) = (k \in omega_seq_local s).
Proof. by rewrite /omega_seq /omega_seq_local. Qed.

Lemma omega_set_seq_bridge_bounded m (D : {set 'I_m.+1}) (k : nat) (Hkm : k < m) :
  (k \in omega_seq (set_to_seq D)) = ((Ordinal Hkm) \in omega_set D).
Proof.
rewrite omega_seq_mem_eq.
by rewrite (omega_set_seq_local_bridge D (Ordinal Hkm)).
Qed.

Lemma omega_seq_subset_bounded m (D E : {set 'I_m.+1}) (ks : seq nat) :
  omega_set D \subset omega_set E →
  all (fun k ⇒ k < m) ks →
  all (fun k ⇒ k \in omega_seq (set_to_seq D)) ks →
  all (fun k ⇒ k \in omega_seq (set_to_seq E)) ks.
Proof.
move/subsetP ⇒ Hsub /allP Hbnd /allP HD.
apply/allP ⇒ k Hk.
have Hkm := Hbnd _ Hk.
rewrite (omega_set_seq_bridge_bounded E Hkm).
apply: Hsub.
by rewrite -(omega_set_seq_bridge_bounded D Hkm); apply: HD.
Qed.


Lemma index_lt_sorted (s : seq nat) (x y : nat) :
  sorted leq s → uniq s → x \in s → y \in s →
  (x < y) = (index x s < index y s).
Proof.
move⇒ Hsorted Hu Hx Hy.
have Hfwd := sorted_ltn_index leq_trans Hsorted.
apply/idP/idP.
- move⇒ Hlt.
  rewrite ltn_neqAle.
  apply/andP; split.
  + apply/negP ⇒ /eqP Heq.
    have Hxy : x = y.
      by have := nth_index 0 Hx; have := nth_index 0 Hy; rewrite Heq ⇒ → →.
    by rewrite Hxy ltnn in Hlt.
  + rewrite leqNgt; apply/negP ⇒ Hgt.
    have := Hfwd _ _ Hy Hx Hgt.
    by move⇒ Hyx; have := leq_ltn_trans Hyx Hlt; rewrite ltnn.
- move⇒ Hlt.
  have := Hfwd _ _ Hx Hy Hlt.
  move⇒ Hle.
  rewrite ltn_neqAle Hle andbT.
  apply/negP ⇒ /eqP Heq; subst y.
  by rewrite ltnn in Hlt.
Qed.

Lemma window_size_bound i w :
  window_size i w ≤ size w - i.
Proof.
rewrite /window_size.
have [_ H] := window_size_fuel_bound i (leqnn (size w)).
exact: H.
Qed.

Lemma S_w_seq_all_lt w :
  2 ≤ size w →
  all (fun k ⇒ k < (size w).-2) (S_w_seq w).
Proof.
move⇒ Hsz2.
apply/allP ⇒ k /mapP [i].
rewrite mem_filter ⇒ /andP [HisD Hiota] →.
rewrite /classify_vertex_cde in HisD.
case Hint : (is_internal i w); rewrite Hint /= in HisD; last by [].
rewrite /is_internal in Hint.
move/andP: Hint ⇒ [Hisz Hws].
rewrite mem_iota in Hiota.
move/andP: Hiota ⇒ [H1 _].
have Hbd := window_size_bound i w.
suff Hi_le : i ≤ (size w).-2.
  by rewrite -ltnS prednK //; rewrite -[X in _ < X]prednK // -subn1 subn_gt0.
rewrite -subn2.
have H2si : 2 ≤ size w - i by exact: leq_trans Hws Hbd.
have Hisz' : i ≤ size w
  by apply: ltnW; rewrite -subn_gt0 (leq_trans _ H2si).
by rewrite leq_subRL // addnC -leq_subRL.
Qed.



Lemma omega_proper_beta_lt : ∀ m (D E : {set 'I_m.+1}),
  omega_set D \proper omega_set E →
  beta D < beta E.
Proof.
move⇒ m D E Hprop.
have [Hsub [k Hkin Hknot]] := properP Hprop.
set bvD := descent_to_bvec D.
set bvE := descent_to_bvec E.
set f := class_map (n:=m.+2) bvE.
have bvE_in_class : ∀ sigma : {perm 'I_m.+2}, descent_set sigma = D →
  bvE \in expand_cde (phi_w (perm_to_seq sigma)).
  move⇒ sigma HdescD.
  have Huniq := perm_to_seq_uniq sigma.
  have Hsize := perm_to_seq_size sigma.
  have Hcm : char_mono (perm_to_seq sigma) = bvD.
    by rewrite char_mono_perm_to_seq HdescD.
  have HbvD_in : bvD \in expand_cde (phi_w (perm_to_seq sigma)).
    by rewrite -Hcm; exact: char_mono_in_expand_cde.
  have Hsz2 : 2 ≤ size (perm_to_seq sigma) by rewrite Hsize.
  have HszBvD : size bvD = (size (perm_to_seq sigma)).-1.
    by rewrite /bvD size_descent_to_bvec Hsize.
  have Hsupport_D := phi_w_support_general Huniq Hsz2 HszBvD.
  rewrite -/bvD in Hsupport_D.
  have Hrew : (size (perm_to_seq sigma)).-1 = m.+1 by rewrite Hsize.
  have HD_all : all (fun j ⇒ j \in omega_seq [seq i <- iota 0 m.+1 | nth false bvD i])
                    (S_w_seq (perm_to_seq sigma)).
    by rewrite -[X in iota 0 X]Hrew -Hsupport_D.
  have Hdesc_D : [seq i <- iota 0 m.+1 | nth false bvD i] = set_to_seq D.
    by rewrite /bvD desc_positions_bvec.
  rewrite Hdesc_D in HD_all.
  have Hlt_m : all (fun j ⇒ j < m) (S_w_seq (perm_to_seq sigma)).
    have := S_w_seq_all_lt Hsz2.
    apply: sub_all ⇒ j.
    by rewrite Hsize.
  have HE_all : all (fun j ⇒ j \in omega_seq (set_to_seq E))
                    (S_w_seq (perm_to_seq sigma)).
    exact: omega_seq_subset_bounded Hsub Hlt_m HD_all.
  have Hdesc_E : [seq i <- iota 0 m.+1 | nth false bvE i] = set_to_seq E.
    by rewrite /bvE desc_positions_bvec.
  rewrite -Hdesc_E in HE_all.
  have HszBvE : size bvE = (size (perm_to_seq sigma)).-1.
    by rewrite /bvE size_descent_to_bvec Hsize.
  by rewrite (phi_w_support_general Huniq Hsz2 HszBvE) [X in iota 0 X]Hrew.
have f_descent_E : ∀ sigma : {perm 'I_m.+2}, descent_set sigma = D →
  descent_set (f sigma) = E.
  move⇒ sigma HdescD.
  have Hspec := find_ss_spec (perm_to_seq_uniq sigma) (bvE_in_class sigma HdescD).
  have Hcm : char_mono (perm_to_seq (f sigma)) = bvE.
    by rewrite perm_to_seq_class_map; case: Hspec.
  have := char_mono_perm_to_seq (f sigma).
  rewrite Hcm ⇒ /descent_to_bvec_inj.
  by [].
have f_inj : {in [set sigma | descent_set sigma == D] &, injective f}.
  move⇒ sigma1 sigma2.
  rewrite !inE ⇒ /eqP Hd1 /eqP Hd2 Hfeq.
  have Hseq : perm_to_seq (f sigma1) = perm_to_seq (f sigma2).
    by rewrite Hfeq.
  rewrite !perm_to_seq_class_map in Hseq.
  set w1 := perm_to_seq sigma1 in Hseq ×.
  set w2 := perm_to_seq sigma2 in Hseq ×.
  set ss1 := find_ss w1 bvE in Hseq ×.
  set ss2 := find_ss w2 bvE in Hseq ×.
  have Hu1 := perm_to_seq_uniq sigma1.
  have Hu2 := perm_to_seq_uniq sigma2.
  have Hcm1 : char_mono w1 = bvD by rewrite /w1 char_mono_perm_to_seq Hd1.
  have Hcm2 : char_mono w2 = bvD by rewrite /w2 char_mono_perm_to_seq Hd2.
  set w' := apply_psis ss1 w1.
  have Hw' : apply_psis ss2 w2 = w'
    by rewrite -Hseq.
  have Hu' : uniq w'
    by apply: uniq_apply_psis.
  have Hw1_class : w1 = apply_psis ss1 w'.
    by rewrite /w' apply_psis_cancel.
  have Hw2_class : w2 = apply_psis ss2 w'.
    by rewrite -Hw' apply_psis_cancel.
  have Hss1_pw : ss1 \in powerset_internal w'.
    rewrite /ss1 powerset_internal_apply_psis //.
    exact: (find_ss_spec Hu1
      (bvE_in_class sigma1 Hd1)).1.
  have Hss2_pw : ss2 \in powerset_internal w'.
    rewrite /ss2 -Hw' powerset_internal_apply_psis //.
    exact: (find_ss_spec Hu2
      (bvE_in_class sigma2 Hd2)).1.
  have Hw12 : w1 = w2.
    rewrite Hw1_class Hw2_class.
    apply: (char_mono_class_inj Hu' Hss1_pw Hss2_pw).
    by rewrite -Hw1_class -Hw2_class Hcm1 Hcm2.
  by apply: perm_to_seq_inj; exact: Hw12.
have Hkm : val k < m := ltn_ord k.
have Hkm2 : val k < (m.+2).-2 by rewrite /=.
have [w0 [Hu0 [Hsz0 HS0]]] := strict_witness_exists Hkm2.
have bvE_in_w0 : bvE \in expand_cde (phi_w w0).
  have Hsz2 : 2 ≤ size w0 by rewrite Hsz0.
  have HszBvE : size bvE = (size w0).-1.
    by rewrite /bvE size_descent_to_bvec Hsz0.
  have Hrew0 : (size w0).-1 = m.+1 by rewrite Hsz0.
  rewrite phi_w_support_general // HS0 /=.
  rewrite andbT.
  have Hdesc_E : [seq i <- iota 0 m.+1 | nth false bvE i] = set_to_seq E.
    by rewrite /bvE desc_positions_bvec.
  rewrite [X in iota 0 X]Hrew0 Hdesc_E.
  rewrite (omega_set_seq_bridge_bounded E Hkm).
  by have → : Ordinal Hkm = k by apply: val_inj.
have bvD_notin_w0 : bvD \notin expand_cde (phi_w w0).
  have Hsz2 : 2 ≤ size w0 by rewrite Hsz0.
  have HszBvD : size bvD = (size w0).-1.
    by rewrite /bvD size_descent_to_bvec Hsz0.
  have Hrew0 : (size w0).-1 = m.+1 by rewrite Hsz0.
  rewrite phi_w_support_general // HS0 /=.
  rewrite andbT.
  have Hdesc_D : [seq i <- iota 0 m.+1 | nth false bvD i] = set_to_seq D.
    by rewrite /bvD desc_positions_bvec.
  rewrite [X in iota 0 X]Hrew0 Hdesc_D.
  rewrite (omega_set_seq_bridge_bounded D Hkm).
  have → : Ordinal Hkm = k by apply: val_inj.
  by rewrite (negbTE Hknot).


have img_has_bvD : ∀ sigma : {perm 'I_m.+2},
  sigma \in [set f tau | tau in [set s | descent_set s == D]] →
  bvD \in expand_cde (phi_w (perm_to_seq sigma)).
  move⇒ sigma /imsetP [tau].
  rewrite inE ⇒ /eqP Hdtau →.
  have Hcm : char_mono (perm_to_seq tau) = bvD
    by rewrite char_mono_perm_to_seq Hdtau.
  rewrite perm_to_seq_class_map.
  rewrite phi_w_apply_psis //.
    by rewrite -Hcm; exact: (char_mono_in_expand_cde (perm_to_seq_uniq tau)).
  exact: perm_to_seq_uniq.


have img_sub : [set f tau | tau in [set s | descent_set s == D]]
\subset [set s | descent_set s == E].
  apply/subsetP ⇒ sigma /imsetP [tau].
  rewrite !inE ⇒ /eqP Hdtau →.
  by apply/eqP; exact: f_descent_E.

have card_img : #|[set f tau | tau in [set s | descent_set s == D]]| = beta D.
  by rewrite /beta (card_in_imset f_inj).


set w0_sorted := sort leq w0.
set w0_norm := [seq index x w0_sorted | x <- w0].
have Hsz_norm : size w0_norm = m.+2.
  by rewrite /w0_norm size_map Hsz0.
have Huniq_norm : uniq w0_norm.
  rewrite /w0_norm map_inj_in_uniq //.
  move⇒ x y Hx Hy Hxy.
  have Hx' : x \in w0_sorted by rewrite mem_sort.
  have Hy' : y \in w0_sorted by rewrite mem_sort.
  by apply: (index_inj 0 (s:=w0_sorted)).
have Hbnd_norm : all (fun x ⇒ x < m.+2) w0_norm.
  apply/allP ⇒ x /mapP [y Hy ->].
  rewrite -Hsz0 -(size_sort leq) index_mem.
  by rewrite mem_sort.
have Horder_iso : ∀ p q : nat, p < size w0 → q < size w0 →
  (nth 0 w0 p < nth 0 w0 q) = (nth 0 w0_norm p < nth 0 w0_norm q).
  move⇒ p q Hp Hq.
  rewrite /w0_norm !(nth_map 0) //;
    try by rewrite -Hsz0; first [exact: Hp | exact: Hq].
  set sp := nth 0 w0 p; set sq := nth 0 w0 q.
  have Hsp : sp \in w0 by apply: mem_nth.
  have Hsq : sq \in w0 by apply: mem_nth.
  have Hsp_s : sp \in w0_sorted by rewrite mem_sort.
  have Hsq_s : sq \in w0_sorted by rewrite mem_sort.
  have Huniq_sorted : uniq w0_sorted by rewrite sort_uniq.
  have Hsorted : sorted leq w0_sorted
    by apply: sort_sorted; exact: leq_total.
  exact: index_lt_sorted Hsorted Huniq_sorted Hsp_s Hsq_s.
set sigma0 := seq_to_perm Hsz_norm Huniq_norm Hbnd_norm.
have Hpts0 : perm_to_seq sigma0 = w0_norm.
  by rewrite perm_to_seq_seq_to_perm.










have phi_w_order_iso : ∀ (s1 s2 : seq nat),
  size s1 = size s2 → uniq s1 → uniq s2 →
  (∀ p q, p < size s1 → q < size s1 →
    (nth 0 s1 p < nth 0 s1 q) = (nth 0 s2 p < nth 0 s2 q)) →
  phi_w s1 = phi_w s2.
  move⇒ s1 s2 Hszeq Hu1 Hu2 Hord.
  rewrite /phi_w /phi'_w Hszeq.
  congr (filter _ _).
  apply: eq_map ⇒ i.
  rewrite /classify_vertex_cde.
  have Hint : is_internal i s1 = is_internal i s2.
    rewrite /is_internal Hszeq.
    case Hisz: (i < size s2) ⇒ //=.
    by rewrite (window_size_order_iso i Hszeq Hu1 Hu2 Hord).
  rewrite Hint.
  case: (is_internal i s2) ⇒ //=.
  by rewrite (has_left_child_order_iso i Hszeq Hu1 Hu2 Hord).

have Hsz_norm' : size w0_norm = size w0.
  by rewrite /w0_norm size_map.
have Hord_rev : ∀ p' q', p' < size w0_norm → q' < size w0_norm →
  (nth 0 w0_norm p' < nth 0 w0_norm q') = (nth 0 w0 p' < nth 0 w0 q').
  move⇒ p' q'; rewrite Hsz_norm' ⇒ Hp' Hq'.
  by rewrite (Horder_iso p' q' Hp' Hq').

have Hphi_w0 : phi_w w0_norm = phi_w w0.
  apply: phi_w_order_iso; [exact: Hsz_norm' | exact: Huniq_norm
    | exact: Hu0 | exact: Hord_rev].

have HS_w0 : S_w_seq w0_norm = S_w_seq w0.
  rewrite /S_w_seq Hsz_norm'.
  congr (map _ _).
  apply: eq_in_filter ⇒ i _.
  rewrite /classify_vertex_cde.
  have Hint : is_internal i w0_norm = is_internal i w0.
    rewrite /is_internal Hsz_norm'.
    case Hisz: (i < size w0) ⇒ //=.
    by rewrite (window_size_order_iso i Hsz_norm' Huniq_norm Hu0 Hord_rev).
  rewrite Hint.
  case: (is_internal i w0) ⇒ //=.
  by rewrite (has_left_child_order_iso i Hsz_norm' Huniq_norm Hu0 Hord_rev).

have HbvE_sigma0 : bvE \in expand_cde (phi_w (perm_to_seq sigma0)).
  by rewrite Hpts0 Hphi_w0.

have HbvD_not_sigma0 : bvD \notin expand_cde (phi_w (perm_to_seq sigma0)).
  by rewrite Hpts0 Hphi_w0.

set ss_new := find_ss (perm_to_seq sigma0) bvE.
have [Hss_new Hcm_new] := find_ss_spec (perm_to_seq_uniq sigma0) HbvE_sigma0.
set w_new := apply_psis ss_new (perm_to_seq sigma0).
have Hsz_new : size w_new = m.+2.
  by rewrite /w_new size_apply_psis perm_to_seq_size.
have Huniq_new : uniq w_new.
  by apply: uniq_apply_psis; exact: perm_to_seq_uniq.
have Hbnd_new : all (fun x ⇒ x < m.+2) w_new.
  by apply: all_bnd_apply_psis; [exact: perm_to_seq_bnd | exact: perm_to_seq_uniq].
set sigma_new := seq_to_perm Hsz_new Huniq_new Hbnd_new.
have Hpts_new : perm_to_seq sigma_new = w_new.
  by rewrite perm_to_seq_seq_to_perm.

have Hdesc_new : descent_set sigma_new = E.
  have Hcm : char_mono (perm_to_seq sigma_new) = bvE.
    by rewrite Hpts_new.
  have := char_mono_perm_to_seq sigma_new.
  rewrite Hcm ⇒ /descent_to_bvec_inj.
  by [].

have Hnotin : sigma_new \notin [set f tau | tau in [set s | descent_set s == D]].
  apply/negP ⇒ /imsetP [tau].
  rewrite inE ⇒ /eqP Hdtau Heq.
  have Hsigma_in : sigma_new \in [set f tau' | tau' in [set s | descent_set s == D]].
    by apply/imsetP; ∃ tau ⇒ //; rewrite inE Hdtau.
  have Habs : bvD \in expand_cde (phi_w (perm_to_seq sigma_new))
    by exact: img_has_bvD Hsigma_in.
  move: Habs.
  rewrite Hpts_new /w_new phi_w_apply_psis;
    last by exact: perm_to_seq_uniq.
  by rewrite Hpts0 Hphi_w0 (negbTE bvD_notin_w0).

have Hin_E : sigma_new \in [set s | descent_set s == E].
  by rewrite inE Hdesc_new.

have Hproper : [set f tau | tau in [set s | descent_set s == D]]
\proper [set s | descent_set s == E].
  rewrite properEcard img_sub /=.
  apply: (@leq_ltn_trans #|[set s | descent_set s == E] :\ sigma_new|).
    apply: subset_leq_card.
    apply/subsetP ⇒ x Hx.
    rewrite in_setD1.
    apply/andP; split.
      apply/negP ⇒ /eqP Heq; subst x.
      by move: Hnotin; rewrite Hx.
    exact: (subsetP img_sub _ Hx).
  by rewrite [X in _ < X](cardsD1 sigma_new) Hin_E ltnS leqnn.

rewrite -card_img.
exact: proper_card Hproper.
Qed.


Lemma beta_swap_lt_caseA : ∀ n (D : {set 'I_n}) (i j : 'I_n),
  val j = (val i).+1 → i \in D → j \in D →
  (∀ q : 'I_n, val q = (val j).+1 → q \in D) →
  beta D < beta (toggle_at D j).
Proof.
move⇒ n D i j Hj Hi Hjin Hsucc.
case: n D i j Hj Hi Hjin Hsucc ⇒ [|m] D i j Hj Hi Hjin Hsucc.
- by have := ltn_ord i; rewrite ltn0.
- apply: (omega_proper_beta_lt (m := m)).
  exact: toggle_at_j_omega_strict_superset Hj Hi Hjin Hsucc.
Qed.