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
perm_seq_basics.
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.
char_mono_perm_to_seq -- the seq-side char_mono of
perm_to_seq s equals the perm-side boolean vector of
descent_set s. Bridges psi_cdindex descent patterns to perm
descent sets.
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.
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.
psi_apply_psis_comm -- the single psi i commutes with the
iterated apply_psis ss (on uniq seqs), via psi_comm.
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.
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.
apply_psis_rev -- since each psi i is involutive and they
commute, apply_psis is independent of the order of the
operations: rev ss gives the same result as ss.
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.
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.
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.
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.
powerset_internal_apply_psis -- the internal-vertex powerset
used to enumerate the M-class is invariant under apply_psis;
consequence of internal_vertices_apply_psis.
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.
uniq w →
powerset_internal (apply_psis ops w) =
powerset_internal w.
Proof.
move⇒ Hu.
by rewrite /powerset_internal
internal_vertices_apply_psis.
Qed.
class_char_monos_uniq -- the descent patterns of the M-class
members of w are pairwise distinct (combines fact3 with
uniq_expand_cde).
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.
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.
char_mono_class_inj -- M-class injectivity: within the M-class
of w, two class members with the same descent pattern are
actually the same sequence. Follows from fact3 and
uniq_expand_cde.
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.
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.
all_bnd_apply_psis -- the boundedness predicate
all (< n) is preserved by apply_psis (uses
perm_eq_apply_psis).
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.
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.
size w = n → size (apply_psis ss w) = n.
Proof. move⇒ <-; exact: size_apply_psis. Qed.
uniq_expand_cde -- expand_cde produces a list of pairwise
distinct boolean vectors (key for M-class injectivity).
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.
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.
nil_in_powerset_internal -- the empty list is always a member
of powerset_internal w (the M-class always contains w
itself).
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.
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.
char_mono_in_expand_cde -- the descent pattern of w itself
appears in expand_cde (phi_w w) (corresponding to ss = nil
in the fact3 enumeration).
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.
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.
find_ss w bv -- search for an ss in powerset_internal w
such that apply_psis ss w has descent pattern bv; returns the
first match (or :: if none).
Definition find_ss (w : seq nat) (bv : seq bool) : seq nat :=
head [::] [seq ss <- powerset_internal w | char_mono (apply_psis ss w) == bv].
head [::] [seq ss <- powerset_internal w | char_mono (apply_psis ss w) == bv].
find_ss_spec -- whenever bv is a descent pattern realized in
the M-class of w, find_ss w bv returns a valid witness:
in powerset_internal w and yielding the requested pattern.
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.
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.
class_map bv sigma -- map a permutation sigma to the M-class
member with descent pattern bv, packaged back as a perm. The
core injection used in the proof of omega_proper_beta_lt.
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)).
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)).
perm_to_seq_class_map -- perm_to_seq of class_map bv sigma
is exactly apply_psis (find_ss ... bv) (perm_to_seq 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.
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.
omega_seq_mem_eq -- the psi_cdindex omega_seq and the local
omega_seq_local (in beta_bridge) agree on memberships
(definitionally identical).
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.
(k \in omega_seq s) = (k \in omega_seq_local s).
Proof. by rewrite /omega_seq /omega_seq_local. Qed.
omega_set_seq_bridge_bounded -- bridge in the bounded form: for
k < m, k \in omega_seq (set_to_seq D) iff Ordinal Hkm \in
omega_set D.
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.
(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.
omega_seq_subset_bounded -- a subset relation on omega-sets
transports to membership at the seq level for any list of
bounded indices.
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.
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.
index_lt_sorted -- in a uniq sorted list, order on values
coincides with order on positions: x < y iff index x s <
index y s.
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.
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.
S_w_seq_all_lt -- elements of S_w_seq w (the support indices
of the omega map) are bounded by (size w).-2.
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.
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.
omega_proper_beta_lt -- Stanley EC1 (2nd ed.) Proposition 1.6.4
at the finset level: a strict inclusion omega_set D \proper
omega_set E of omega-sets implies the strict inequality
beta D < beta E of descent counts. Headline result of this
file; proof injects {sigma | descent D} into {tau | descent E}
via the M-class class_map and exhibits a strict witness via
strict_witness_exists.
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.
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.