Library mathcomp_eulerian.altsub
From mathcomp Require Import all_ssreflect fingroup perm.
From mathcomp_eulerian Require Import ordinal_reindex perm_compress
descent eulerian beta beta_omega beta_swap.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Section TurnDefs.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).
Definition is_turn s (i : 'I_n) : bool :=
is_descent s (widen_ord (leqnSn _) i) (+) is_descent s (lift ord0 i).
Definition turn_count s : nat :=
#|[set i : 'I_n | is_turn s i]|.
Lemma is_turnE s i :
is_turn s i =
is_descent s (widen_ord (leqnSn _) i) (+) is_descent s (lift ord0 i).
Proof. by []. Qed.
End TurnDefs.
Fixpoint alt_aux (b : bool) (x : nat) (xs : seq nat) : bool :=
match xs with
| [::] ⇒ true
| y :: xs' ⇒
(if b then x < y else y < x) && alt_aux (~~ b) y xs'
end.
Definition is_alt (xs : seq nat) : bool :=
match xs with
| [::] ⇒ true
| [:: _] ⇒ true
| x :: y :: xs' ⇒
((x < y) && alt_aux false y xs') || ((y < x) && alt_aux true y xs')
end.
Definition perm_seq n (s : {perm 'I_n.+2}) : seq nat :=
[seq val (s i) | i <- enum 'I_n.+2].
Lemma size_perm_seq n (s : {perm 'I_n.+2}) :
size (perm_seq s) = n.+2.
Proof. by rewrite size_map size_enum_ord. Qed.
Definition pick_seq n (s : {perm 'I_n.+2}) (I : {set 'I_n.+2}) : seq nat :=
[seq val (s j) | j <- sort (fun a b : 'I_n.+2 ⇒ val a ≤ val b) (enum I)].
Definition as_perm_max n (s : {perm 'I_n.+2}) : nat :=
\max_(I : {set 'I_n.+2} | is_alt (pick_seq s I)) #|I|.
Definition as_perm n (s : {perm 'I_n.+2}) : nat := (turn_count s).+2.
Example alt_312 : is_alt [:: 3; 1; 2] = true.
Proof. by []. Qed.
Example alt_321 : is_alt [:: 3; 2; 1] = false.
Proof. by []. Qed.
Example alt_3142 : is_alt [:: 3; 1; 4; 2] = true.
Proof. by []. Qed.
Example alt_31425 : is_alt [:: 3; 1; 4; 2; 5] = true.
Proof. by []. Qed.
Example alt_321_sub : is_alt [:: 3; 1] = true.
Proof. by []. Qed.
Lemma is_alt_nil : is_alt [::] = true.
Proof. by []. Qed.
Lemma is_alt_singleton x : is_alt [:: x] = true.
Proof. by []. Qed.
Lemma alt_aux_cons b x y xs :
alt_aux b x (y :: xs) = (if b then x < y else y < x) && alt_aux (~~ b) y xs.
Proof. by []. Qed.
Lemma is_alt_cons2 x y xs :
is_alt (x :: y :: xs) =
((x < y) && alt_aux false y xs) || ((y < x) && alt_aux true y xs).
Proof. by []. Qed.
Lemma alt_aux_size_ge1 b x xs :
alt_aux b x xs → 0 < size xs → ∃ y xs', xs = y :: xs'.
Proof.
case: xs ⇒ [|y xs'] // _ _; by ∃ y, xs'.
Qed.
Lemma is_alt_tail x y xs :
is_alt (x :: y :: xs) → is_alt (y :: xs).
Proof.
rewrite is_alt_cons2.
case/orP ⇒ /andP [Hxy].
-
case: xs ⇒ [|z xs'] //=.
case/andP ⇒ Hzy Hrest.
by rewrite Hzy Hrest /= orbT.
- case: xs ⇒ [|z xs'] //=.
case/andP ⇒ Hyz Hrest.
by rewrite Hyz Hrest /=.
Qed.
Section TurnLemmas.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).
Lemma turn_count_le s : turn_count s ≤ n.
Proof.
rewrite /turn_count (leq_trans (max_card _)) // card_ord //.
Qed.
Lemma as_permE s : as_perm s = (turn_count s).+2.
Proof. by []. Qed.
Lemma as_perm_ge2 s : 2 ≤ as_perm s.
Proof. by rewrite as_permE. Qed.
Lemma as_perm_le_size s : as_perm s ≤ n.+2.
Proof. by rewrite as_permE ltnS ltnS turn_count_le. Qed.
Lemma turn_count_id : turn_count (1 : {perm 'I_n.+2}) = 0.
Proof.
apply/eqP; rewrite cards_eq0; apply/eqP/setP ⇒ i; rewrite !inE.
rewrite /is_turn /is_descent !perm1.
have H1 : (val (lift ord0 (widen_ord (leqnSn n) i)) : nat) =
(val (widen_ord (leqnSn n.+1) (widen_ord (leqnSn n) i))).+1.
by rewrite /=.
have H2 : (val (lift ord0 (lift ord0 i)) : nat) =
(val (widen_ord (leqnSn n.+1) (lift ord0 i))).+1.
by rewrite /= /bump /= add1n.
rewrite ltnNge leqW //=.
rewrite ltnNge leqW //=.
Qed.
Lemma as_perm_id : as_perm (1 : {perm 'I_n.+2}) = 2.
Proof. by rewrite as_permE turn_count_id. Qed.
End TurnLemmas.
Section AltDesc.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).
Lemma turn_count_alt_desc s :
descent_set s = alt_desc_set n.+1 → turn_count s = n.
Proof.
move⇒ Hds.
rewrite /turn_count -[RHS]card_ord.
apply: eq_card ⇒ i.
rewrite !inE /=.
rewrite /is_turn -!mem_descent_set Hds !mem_alt_desc_set /=.
rewrite negbK add0n.
by case: (odd i).
Qed.
Lemma as_perm_alt_desc s :
descent_set s = alt_desc_set n.+1 → as_perm s = n.+2.
Proof. by move⇒ Hds; rewrite as_permE (turn_count_alt_desc Hds). Qed.
Lemma turn_count_max_iff s :
(turn_count s == n) =
[∀ i : 'I_n, is_turn s i].
Proof.
apply/eqP/forallP ⇒ [Hcard i|Hall].
- have Hsub : [set i : 'I_n | is_turn s i] = setT.
apply/eqP; rewrite eqEcard subsetT /=.
by rewrite cardsT card_ord -/(turn_count s) Hcard.
by have := in_setT i; rewrite -Hsub inE.
- rewrite /turn_count.
rewrite -[RHS]card_ord.
apply: eq_card ⇒ i; rewrite inE.
by rewrite (Hall i).
Qed.
End AltDesc.
Section AsPermMaxBounds.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).
Lemma is_alt_pick_seq_le2 s (I : {set 'I_n.+2}) :
#|I| ≤ 1 → is_alt (pick_seq s I).
Proof.
move⇒ HI.
rewrite /pick_seq.
have Hsz : size (sort (fun a b : 'I_n.+2 ⇒ val a ≤ val b) (enum I)) ≤ 1.
by rewrite size_sort -cardE.
case: (sort _ _) Hsz ⇒ [|x [|y rest]] //=.
Qed.
Lemma as_perm_max_ge0 s : 0 ≤ as_perm_max s.
Proof. by []. Qed.
End AsPermMaxBounds.
Section MaxAlternation.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).
Lemma as_perm_full s :
descent_set s = alt_desc_set n.+1 →
as_perm s = size (perm_seq s).
Proof.
move⇒ Hds.
by rewrite size_perm_seq (as_perm_alt_desc Hds).
Qed.
End MaxAlternation.
Definition sign_seq (xs : seq nat) : seq bool :=
if xs is x :: xs' then pairmap (fun a b ⇒ a < b) x xs'
else [::].
Lemma sign_seq_cons2 x y xs :
sign_seq (x :: y :: xs) = (x < y) :: sign_seq (y :: xs).
Proof. by []. Qed.
Lemma size_sign_seq xs : size (sign_seq xs) = (size xs).-1.
Proof.
case: xs ⇒ [|x xs] //=.
by rewrite size_pairmap.
Qed.
Definition flip_count (ss : seq bool) : nat :=
if ss is a :: ss' then \sum_(p <- pairmap (fun u v ⇒ u (+) v) a ss') p
else 0.
Lemma flip_count_cons2 a b ss :
flip_count (a :: b :: ss) = (a (+) b) + flip_count (b :: ss).
Proof.
rewrite /flip_count /=.
by rewrite big_cons.
Qed.
Definition turn_count_seq (xs : seq nat) : nat := flip_count (sign_seq xs).
Lemma turn_count_seq_nil : turn_count_seq [::] = 0.
Proof. by []. Qed.
Lemma turn_count_seq_singleton x : turn_count_seq [:: x] = 0.
Proof. by []. Qed.
Lemma turn_count_seq_pair x y : turn_count_seq [:: x; y] = 0.
Proof. by rewrite /turn_count_seq /sign_seq /= /flip_count /= big_nil. Qed.
Example tcs_312 : turn_count_seq [:: 3; 1; 2] = 1.
Proof.
by rewrite /turn_count_seq /sign_seq /= /flip_count /= big_cons big_nil.
Qed.
Example tcs_3142 : turn_count_seq [:: 3; 1; 4; 2] = 2.
Proof.
by rewrite /turn_count_seq /sign_seq /= /flip_count /= !big_cons big_nil.
Qed.
Example tcs_321 : turn_count_seq [:: 3; 2; 1] = 0.
Proof.
by rewrite /turn_count_seq /sign_seq /= /flip_count /= big_cons big_nil.
Qed.
Example tcs_12345 : turn_count_seq [:: 1; 2; 3; 4; 5] = 0.
Proof.
by rewrite /turn_count_seq /sign_seq /= /flip_count /= !big_cons big_nil.
Qed.
Section SignPerm.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).
Lemma size_sign_seq_perm s :
size (sign_seq (perm_seq s)) = n.+1.
Proof. by rewrite size_sign_seq size_perm_seq /=. Qed.
Lemma enum_ord_split :
enum 'I_n.+2 = ord0 :: [seq lift ord0 i | i <- enum 'I_n.+1].
Proof.
apply: (@eq_from_nth _ ord0).
by rewrite /= size_map !size_enum_ord.
rewrite size_enum_ord ⇒ i Hi.
case: i Hi ⇒ [|i] Hi /=.
apply: val_inj ⇒ /=.
by have := @nth_enum_ord n.+2 ord0 0 Hi.
rewrite (nth_map ord0); last by rewrite size_enum_ord -ltnS.
have Hi' : i < n.+1 by rewrite -ltnS.
apply: val_inj ⇒ /=.
have H1 := @nth_enum_ord n.+2 ord0 i.+1 Hi.
have H2 := @nth_enum_ord n.+1 ord0 i Hi'.
by rewrite H1 /bump /= add1n H2.
Qed.
Lemma not_is_descentE s (i : 'I_n.+1) :
~~ is_descent s i = (val (s (widen_ord (leqnSn _) i)) < val (s (lift ord0 i))).
Proof.
rewrite /is_descent -leqNgt.
have Hne : widen_ord (leqnSn n.+1) i != lift ord0 i.
by rewrite -val_eqE /= /bump /= add1n neq_ltn ltnSn.
have Hsne : s (widen_ord (leqnSn n.+1) i) != s (lift ord0 i).
by apply: contra Hne ⇒ /eqP /perm_inj →.
have Hvne : val (s (widen_ord (leqnSn n.+1) i)) != val (s (lift ord0 i)).
by rewrite val_eqE.
rewrite leq_eqVlt (negbTE Hvne) /=.
by [].
Qed.
Lemma sign_seq_perm_seq s :
sign_seq (perm_seq s) = [seq ~~ is_descent s i | i <- enum 'I_n.+1].
Proof.
apply: (@eq_from_nth _ true).
by rewrite size_sign_seq_perm size_map size_enum_ord.
move⇒ i; rewrite size_sign_seq_perm ⇒ Hi.
rewrite (nth_map ord0); last by rewrite size_enum_ord.
rewrite /sign_seq /perm_seq.
rewrite enum_ord_split map_cons -map_comp.
rewrite (@nth_pairmap _ 0 _ true (fun a b : nat ⇒ a < b)); last first.
by rewrite size_map size_enum_ord.
rewrite not_is_descentE.
have Hidx : nth ord0 (enum 'I_n.+1) i = Ordinal Hi.
by apply: val_inj ⇒ /=; rewrite nth_enum_ord.
case: i Hi Hidx ⇒ [|j] Hi Hidx /=.
- rewrite (nth_map ord0); last by rewrite size_enum_ord.
rewrite Hidx /=. by congr (s _ < s _); apply: val_inj.
- have Hj : j < n.+1 by apply: ltnW.
rewrite (nth_map ord0); last by rewrite size_enum_ord.
rewrite (nth_map ord0); last by rewrite size_enum_ord.
rewrite Hidx.
have → : nth ord0 (enum 'I_n.+1) j = Ordinal Hj.
by apply: val_inj ⇒ /=; rewrite nth_enum_ord.
by rewrite /=; congr (s _ < s _); apply: val_inj ⇒ /=; rewrite /bump /= add1n.
Qed.
End SignPerm.
Section AsPermMaxBoundsM.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).
Lemma as_perm_max_le_size s : as_perm_max s ≤ n.+2.
Proof.
rewrite /as_perm_max.
apply/bigmax_leqP ⇒ I _.
by rewrite (leq_trans (subset_leq_card (subsetT I))) // cardsT card_ord.
Qed.
End AsPermMaxBoundsM.
Section PickSeqFull.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).
Lemma sorted_val_enum_ord m :
sorted (fun a b : 'I_m ⇒ val a ≤ val b) (enum 'I_m).
Proof.
have := iota_sorted 0 m.
rewrite -val_enum_ord.
elim: (enum 'I_m) ⇒ [|x [|y xs] IH] //=.
move⇒ /andP [Hxy Hr].
by rewrite Hxy; apply: IH; rewrite /= Hr.
Qed.
Lemma pick_seq_setT s : pick_seq s [set: 'I_n.+2] = perm_seq s.
Proof.
rewrite /pick_seq /perm_seq.
congr [seq val (s _) | _ <- _].
rewrite enum_setT -enumT.
apply: sorted_sort.
- by move⇒ a b c; apply: leq_trans.
- exact: sorted_val_enum_ord.
Qed.
Lemma as_perm_max_full s :
is_alt (perm_seq s) → as_perm_max s = n.+2.
Proof.
move⇒ Halt.
apply/eqP; rewrite eqn_leq.
apply/andP; split; first exact: as_perm_max_le_size.
have <- : #|[set: 'I_n.+2]| = n.+2 by rewrite cardsT card_ord.
rewrite /as_perm_max.
apply: (leq_bigmax_cond [set: 'I_n.+2]).
by rewrite pick_seq_setT.
Qed.
End PickSeqFull.
Lemma is_alt_size_le1 (xs : seq nat) : size xs ≤ 1 → is_alt xs.
Proof. by case: xs ⇒ [|x [|y xs]]. Qed.
Lemma is_alt_three x y z xs :
is_alt (x :: y :: z :: xs) →
(x < y < z) = false ∧ (z < y < x) = false.
Proof.
rewrite is_alt_cons2 /=.
case/orP ⇒ /andP [Hxy].
- case/andP ⇒ Hzy _.
split.
+ by rewrite Hxy /= ltnNge ltnW.
+ by rewrite Hzy /= ltnNge (ltnW Hxy).
- case/andP ⇒ Hyz _.
split.
+ by rewrite ltnNge (ltnW Hxy).
+ apply/andP⇒ -[Hzy _].
by have := ltn_trans Hyz Hzy; rewrite ltnn.
Qed.
Lemma is_alt_subseq_strictmono_le2 (xs sub : seq nat) :
subseq sub xs → sorted ltn xs → is_alt sub → size sub ≤ 2.
Proof.
move⇒ Hsub Hxs Halt.
case Hsz: (size sub ≤ 2) ⇒ //.
move/negbT: Hsz; rewrite -ltnNge.
move⇒ Hsz.
case: sub Hsub Halt Hsz ⇒ [|a [|b [|c sub']]] // Hsub Halt _.
have /(_ a b c sub' Halt) [Habs _] := is_alt_three.
have Hsubmono : sorted ltn (a :: b :: c :: sub').
apply: subseq_sorted Hsub Hxs.
by move⇒ x y z; apply: ltn_trans.
move/and3P: Hsubmono ⇒ [Hab Hbc _].
have Hab' : a < b := Hab.
have Hbc' : b < c := Hbc.
by rewrite Hab' Hbc' in Habs.
Qed.
Section SlotInterval.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).
Definition slot_iv (i j : 'I_n.+2) : {set 'I_n.+1} :=
[set k : 'I_n.+1 | (val i ≤ val k) && (val k < val j)].
Lemma mem_slot_iv (i j : 'I_n.+2) (k : 'I_n.+1) :
(k \in slot_iv i j) = (val i ≤ val k) && (val k < val j).
Proof. by rewrite inE. Qed.
Lemma card_slot_iv (i j : 'I_n.+2) :
val j ≤ n.+1 →
#|slot_iv i j| = val j - val i.
Proof.
move⇒ Hj.
rewrite cardE size_filter -[Finite.enum _]enumT.
have ME : ∀ k : 'I_n.+1, mem (slot_iv i j) k
= (val i ≤ val k) && (val k < val j).
by move⇒ k; rewrite -mem_slot_iv.
under eq_count ⇒ k do rewrite ME.
rewrite -(count_map val (fun m ⇒ (val i ≤ m) && (m < val j))).
rewrite val_enum_ord.
have Hi := ltn_ord i.
have HiSm : val i ≤ n.+1 by rewrite -ltnS (leq_trans Hi).
case: (leqP (val i) (val j)) ⇒ Hij; last first.
have → : val j - val i = 0 by apply/eqP; rewrite subn_eq0 ltnW.
apply/eqP; rewrite -leqn0 leqNgt -has_count; apply/hasPn ⇒ m _ /=.
by case: (leqP (val i) m) ⇒ //= Him; rewrite ltnNge (leq_trans (ltnW Hij) Him).
have HX : n.+1 = val i + (n.+1 - val i) by rewrite subnKC.
rewrite [in iota 0 n.+1]HX iotaD count_cat.
have → : count (fun m : nat ⇒ val i ≤ m < val j) (iota 0 (val i)) = 0.
apply/eqP; rewrite -leqn0 leqNgt -has_count; apply/hasPn ⇒ m.
rewrite mem_iota add0n ⇒ /andP [_ Hm] /=.
apply/negP ⇒ /andP [Hi' _].
by have := leq_ltn_trans Hi' Hm; rewrite ltnn.
rewrite add0n add0n.
have HY : n.+1 - val i = (val j - val i) + (n.+1 - val j).
have HK : val j - val i + (n.+1 - val j) = n.+1 - val i.
apply/eqP; rewrite -(eqn_add2r (val i)) addnAC -addnA subnK //.
by rewrite addnA (subnK Hij) addnC (subnK Hj).
by rewrite -HK.
rewrite HY iotaD count_cat.
have → : count (fun m : nat ⇒ val i ≤ m < val j)
(iota (val i + (val j - val i)) (n.+1 - val j)) = 0.
apply/eqP; rewrite -leqn0 leqNgt -has_count; apply/hasPn ⇒ m.
rewrite mem_iota subnKC // ⇒ /andP [Hm _] /=.
by apply/negP ⇒ /andP [_ Hm']; have := leq_ltn_trans Hm Hm'; rewrite ltnn.
rewrite addn0.
rewrite -[RHS](size_iota (val i) (val j - val i)) -[in RHS]count_predT.
apply: eq_in_count ⇒ m.
rewrite mem_iota ⇒ /andP [Hm Hm2] /=.
rewrite subnKC // in Hm2.
by rewrite Hm Hm2.
Qed.
End SlotInterval.
Section InterTurn.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).
Lemma slot_descent_const s (i j : 'I_n.+2) :
(∀ t : 'I_n, val i ≤ (val t).+1 < val j → ~~ is_turn s t) →
∀ (k1 k2 : 'I_n.+1),
val i ≤ val k1 → val k1 ≤ val k2 → val k2 < val j →
is_descent s k1 = is_descent s k2.
Proof.
move⇒ Hnoturn k1 k2 Hi1 H12 H2j.
move: H12 Hi1.
elim: (val k2 - val k1) {-2}k1 (refl_equal (val k2 - val k1)) ⇒
[|d IH] k1' Hd H12 Hi1.
- move/eqP: Hd; rewrite subn_eq0 ⇒ Hk21.
have : val k1' = val k2 by apply/eqP; rewrite eqn_leq H12 Hk21.
by move⇒ /val_inj →.
- have Hk1lt : val k1' < val k2 by rewrite -subn_gt0 Hd.
have Hk1ord : val k1' < n.
by have := ltn_ord k2; rewrite ltnS ⇒ Hk2; rewrite (leq_trans Hk1lt).
pose t : 'I_n := Ordinal Hk1ord.
have Ht : val i ≤ (val t).+1 < val j.
apply/andP; split; first by rewrite (leq_trans Hi1).
by rewrite (leq_trans _ H2j).
have := Hnoturn t Ht.
rewrite /is_turn negb_add ⇒ /eqP Hd1.
have Hk1eq : (widen_ord (leqnSn n) t : 'I_n.+1) = k1' by apply: val_inj.
rewrite Hk1eq in Hd1; rewrite Hd1.
have HSk1 : val (lift ord0 t : 'I_n.+1) = (val k1').+1
by rewrite /= /bump /= add1n.
apply: (IH (lift ord0 t)).
- rewrite HSk1; apply: succn_inj.
by rewrite subnSK // Hd.
- by rewrite HSk1.
- by rewrite HSk1 (leq_trans Hi1).
Qed.
Lemma constant_descent_monotone s (p q : 'I_n.+2) (b : bool) :
val p < val q →
(∀ k : 'I_n.+1, val p ≤ val k < val q → is_descent s k = b) →
if b then val (s q) < val (s p) else val (s p) < val (s q).
Proof.
move⇒ Hpq Hconst.
move: q Hpq Hconst.
elim: (n.+2 - val p) {-2}p (refl_equal (n.+2 - val p)) ⇒
[|d IH] p' Hd q Hpq Hconst.
have Hq2 : val q < n.+2 by exact: ltn_ord.
move/eqP: Hd; rewrite subn_eq0 ⇒ Hp'.
by have := leq_ltn_trans (leq_trans Hp' (ltnW Hpq)) Hq2; rewrite ltnn.
have Hp'lt : val p' < n.+1.
by rewrite -ltnS; apply: leq_trans (ltn_ord q).
pose k0 : 'I_n.+1 := Ordinal Hp'lt.
have Hwidp : (widen_ord (leqnSn n.+1) k0 : 'I_n.+2) = p' by apply: val_inj.
case: (eqVneq (val q) (val p').+1) ⇒ [Hpq1|Hne].
- have Hkrange : val p' ≤ val k0 < val q by rewrite /= leqnn /= Hpq1.
have Hkdesc := Hconst k0 Hkrange.
rewrite /is_descent in Hkdesc.
have Hliftq : (lift ord0 k0 : 'I_n.+2) = q.
by apply: val_inj ⇒ /=; rewrite /bump /= add1n.
rewrite Hwidp Hliftq in Hkdesc.
have Hpqne : p' != q by rewrite -val_eqE neq_ltn Hpq.
have Hspqne : s p' != s q by apply: contra_neq Hpqne ⇒ /perm_inj.
have Hvspqne : val (s p') != val (s q) by rewrite val_eqE.
have Hsd : (val (s q) < val (s p'))%N = b by [].
case Eb : b Hsd ⇒ Hsd /=; first by [].
rewrite -[s p' < s q]/(val (s p') < val (s q))%N.
rewrite ltn_neqAle leqNgt Hsd /=.
by rewrite Hvspqne.
- have HqGtSp : (val p').+1 < val q by rewrite ltn_neqAle eq_sym Hne /= Hpq.
pose pmid : 'I_n.+2 := lift ord0 k0.
have Hpmid : val pmid = (val p').+1 by rewrite /= /bump /= add1n.
have Hd' : n.+2 - val pmid = d.
rewrite Hpmid; apply: succn_inj.
have Hp'2 : val p' < n.+2 by exact: ltn_ord.
by rewrite subnSK // Hd.
have Hpmidq : val pmid < val q by rewrite Hpmid.
have Hslot1 : val p' ≤ val k0 < val q.
by rewrite /= leqnn (ltn_trans _ HqGtSp).
have Hd1 := Hconst k0 Hslot1.
rewrite /is_descent Hwidp in Hd1.
have Hliftpmid : (lift ord0 k0 : 'I_n.+2) = pmid by [].
rewrite Hliftpmid in Hd1.
have Hsubconst : ∀ k : 'I_n.+1,
val pmid ≤ val k < val q → is_descent s k = b.
move⇒ k /andP [Hk1 Hk2].
apply: Hconst.
rewrite Hk2 andbT.
by rewrite (leq_trans _ Hk1) // Hpmid leqnSn.
have IHmid := IH pmid Hd' q Hpmidq Hsubconst.
have Hpmidne : pmid != p'.
by rewrite -val_eqE Hpmid eqn_leq leqNgt ltnSn /=.
have Hspmidne : s pmid != s p' by apply: contra_neq Hpmidne ⇒ /perm_inj.
have Hvne1 : val (s pmid) != val (s p') by rewrite val_eqE.
case Eb : b Hd1 IHmid ⇒ Hd1 IHmid /=.
+ have Hd1' : (val (s pmid) < val (s p'))%N by [].
have IHmid' : (val (s q) < val (s pmid))%N by [].
by apply: ltn_trans IHmid' Hd1'.
+ have HX1 : ~~ (val (s pmid) < val (s p'))%N by rewrite Hd1.
have Hd1' : (val (s p') < val (s pmid))%N.
by rewrite ltn_neqAle leqNgt HX1 /=; rewrite eq_sym Hvne1.
have IHmid' : (val (s pmid) < val (s q))%N by [].
rewrite -[s p' < s q]/(val (s p') < val (s q))%N.
by apply: ltn_trans Hd1' IHmid'.
Qed.
Lemma inter_turn_monotone s (i j : 'I_n.+2) :
val i < val j →
(∀ t : 'I_n, val i ≤ (val t).+1 < val j → ~~ is_turn s t) →
∀ (p q : 'I_n.+2),
val i ≤ val p → val p < val q → val q ≤ val j →
(val (s p) < val (s q))%N = (val (s i) < val (s j))%N.
Proof.
move⇒ Hij Hnoturn p q Hip Hpq Hqj.
have Hjle : val i < n.+1.
by have := ltn_ord j; rewrite ltnS ⇒ Hj2; rewrite (leq_trans Hij).
pose k0 : 'I_n.+1 := Ordinal Hjle.
have Hk0range : val i ≤ val k0 < val j by rewrite /= leqnn /= Hij.
pose b := is_descent s k0.
have Hconst_ij : ∀ k : 'I_n.+1,
val i ≤ val k < val j → is_descent s k = b.
move⇒ k /andP [Hki Hkj].
case: (leqP (val k0) (val k)) ⇒ Hkk0.
- rewrite /b /=.
by apply: esym; apply: (slot_descent_const Hnoturn) ⇒ //=.
- apply: (slot_descent_const Hnoturn) ⇒ //=.
exact: ltnW.
have Hconst_pq : ∀ k : 'I_n.+1,
val p ≤ val k < val q → is_descent s k = b.
move⇒ k /andP [Hkp Hkq].
apply: Hconst_ij.
by rewrite (leq_trans Hip Hkp) /= (leq_trans Hkq).
have Hmono_ij := constant_descent_monotone Hij Hconst_ij.
have Hmono_pq := constant_descent_monotone Hpq Hconst_pq.
case Eb : b Hmono_ij Hmono_pq ⇒ Hmono_ij Hmono_pq /=.
- rewrite ltnNge (ltnW Hmono_pq) /=.
by rewrite ltnNge (ltnW Hmono_ij) /=.
- by rewrite Hmono_pq Hmono_ij.
Qed.
Lemma pick_flip_has_turn s (i j k : 'I_n.+2) :
val i < val j < val k →
(val (s i) < val (s j))%N ≠ (val (s j) < val (s k))%N →
∃ t : 'I_n, (val i ≤ (val t).+1 < val k) ∧ is_turn s t.
Proof.
move⇒ /andP [Hij Hjk] Hflip.
have Hik : val i < val k by apply: ltn_trans Hij Hjk.
case Habs :
[∃ t : 'I_n, (val i ≤ (val t).+1 < val k) && is_turn s t].
case/existsP: Habs ⇒ t /andP [Ht Htn].
by ∃ t; split.
exfalso; apply: Hflip.
have Habs' : ∀ t : 'I_n,
¬ ((val i ≤ (val t).+1 < val k) ∧ is_turn s t).
move⇒ t [Ht Htn].
have Hcontra :
¬ [∃ t0 : 'I_n,
(val i ≤ (val t0).+1 < val k) && is_turn s t0]
by rewrite Habs.
by apply: Hcontra; apply/existsP; ∃ t; rewrite Ht Htn.
have Hno' : ∀ t : 'I_n,
val i ≤ (val t).+1 < val k → ~~ is_turn s t.
move⇒ t Ht; apply/negP ⇒ Htn; by apply: (Habs' t).
rewrite (inter_turn_monotone Hik Hno' (p := i) (q := j)) //; last exact: ltnW.
by rewrite (inter_turn_monotone Hik Hno' (p := j) (q := k)) // ltnW.
Qed.
End InterTurn.
Section UpperBound.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).
Definition turn_iv s (a b : nat) : {set 'I_n} :=
[set t : 'I_n | is_turn s t && (a ≤ (val t).+1 < b)].
Lemma mem_turn_iv s a b (t : 'I_n) :
(t \in turn_iv s a b) = (is_turn s t && (a ≤ (val t).+1 < b)).
Proof. by rewrite inE. Qed.
Lemma turn_iv_subset s a b :
turn_iv s a b \subset [set t : 'I_n | is_turn s t].
Proof. by apply/subsetP ⇒ t; rewrite !inE; case/andP ⇒ →. Qed.
Lemma card_turn_iv_le s a b :
#|turn_iv s a b| ≤ turn_count s.
Proof. exact: subset_leq_card (turn_iv_subset s a b). Qed.
Lemma turn_iv_split s (a b c : nat) :
a ≤ b → b ≤ c →
#|turn_iv s a c| = #|turn_iv s a b| + #|turn_iv s b c|.
Proof.
move⇒ Hab Hbc.
have Heq : turn_iv s a c = turn_iv s a b :|: turn_iv s b c.
apply/setP ⇒ t; rewrite !inE.
apply/and3P/orP.
case⇒ Hturn Hat Htc.
case: (ltnP (val t).+1 b) ⇒ Htb.
by left; apply/and3P; split.
by right; apply/and3P; split.
case⇒ /and3P [Hturn H1 H2]; split⇒ //.
exact: leq_trans H2 Hbc.
exact: leq_trans Hab H1.
rewrite Heq cardsU.
have → : turn_iv s a b :&: turn_iv s b c = set0.
apply/setP ⇒ t; rewrite !inE.
apply/negP ⇒ /andP [/and3P [_ _ Htb] /and3P [_ Hbt _]].
by have := leq_ltn_trans Hbt Htb; rewrite ltnn.
by rewrite cards0 subn0.
Qed.
End UpperBound.
Lemma bool_triangle (a b c : bool) : (a (+) c) ≤ (a (+) b) + (b (+) c).
Proof. by case: a; case: b; case: c. Qed.
Lemma triangle_xor_nat_g (a x y z : nat) :
(a < x) (+) (x < z) ≤ (a < x) (+) (x < y) + ((x < y) (+) (y < z)).
Proof.
case Hxy : (x < y)%N; case Hyz : (y < z)%N.
- have Hxz : (x < z)%N by exact: ltn_trans Hxy Hyz.
rewrite Hxz /=.
by case: (a < x)%N.
- by case: (a < x)%N; case: (x < z)%N.
- by case: (a < x)%N; case: (x < z)%N.
- move/negbT: Hxy; rewrite -leqNgt ⇒ Hyx.
move/negbT: Hyz; rewrite -leqNgt ⇒ Hzy.
have Hxz : ~~ (x < z)%N by rewrite -leqNgt (leq_trans Hzy Hyx).
rewrite (negbTE Hxz) /=.
by case: (a < x)%N.
Qed.
Lemma triangle_xor_nat (w y z r : nat) :
(w < z) (+) (z < r) ≤ (w < y) (+) (y < z) + ((y < z) (+) (z < r)).
Proof.
case Hwz : (w < z)%N; case Hzr : (z < r)%N; rewrite /= ?addn0 ?addn1.
- exact: leq0n.
- case Hwy : (w < y)%N; case Hyz : (y < z)%N; rewrite //=.
move/negbT: Hwy; rewrite -leqNgt ⇒ Hyw.
move/negbT: Hyz; rewrite -leqNgt ⇒ Hzy.
have Hwz' : ~~ (w < z)%N by rewrite -leqNgt (leq_trans Hzy Hyw).
by rewrite Hwz in Hwz'.
- case Hwy : (w < y)%N; case Hyz : (y < z)%N; rewrite //=.
have Hwz' : (w < z)%N by exact: ltn_trans Hwy Hyz.
by rewrite Hwz in Hwz'.
- exact: leq0n.
Qed.
Lemma flip_count_pairmap_insert (a y : nat) (xs : seq nat) :
flip_count (pairmap (fun u : nat ⇒ [eta leq u.+1]) a xs) ≤
flip_count (pairmap (fun u : nat ⇒ [eta leq u.+1]) a (y :: xs)).
Proof.
case: xs ⇒ [|x xs] /=.
- by rewrite /flip_count /= big_nil.
- case Exs : xs ⇒ [|x' xs'] /=.
+ rewrite /flip_count /= !big_cons big_nil !addn0.
by case: ((a < y)%N (+) (y < x)%N).
+ rewrite /flip_count /= !big_cons.
rewrite addnA leq_add2r.
exact: (triangle_xor_nat a y x x').
Qed.
Lemma flip_step_helper (a x y z : nat) (s1 s2 : nat) :
s1 ≤ ((x < y) (+) (y < z)) + s2 →
((x < z) = (y < z) → s1 = s2) →
(a < x) (+) (x < z) + s1 ≤ (a < x) (+) (x < y) + ((x < y) (+) (y < z) + s2).
Proof.
move⇒ IHv Hsame.
case Hxz : (x<z)%N; case Hyz : (y<z)%N.
- have Hs : s1 = s2 by apply: Hsame; rewrite Hxz Hyz.
rewrite Hs addnA leq_add2r.
exact: bool_triangle.
- have Hxy : (x < y)%N.
move/negbT: Hyz; rewrite -leqNgt ⇒ Hzy.
have Hxz' : (x<z)%N by rewrite Hxz.
exact: leq_trans Hxz' Hzy.
rewrite Hxy /=.
rewrite leq_add2l.
by rewrite Hxy Hyz /= in IHv.
- have Hyx : (x < y)%N = false.
move/negbT: Hxz; rewrite -leqNgt ⇒ Hzx.
have Hyz' : (y<z)%N by rewrite Hyz.
have Hyx' : (y < x)%N by exact: leq_trans Hyz' Hzx.
apply/negbTE; rewrite -leqNgt; exact: ltnW.
rewrite Hyx /=.
rewrite Hyx Hyz /= in IHv.
rewrite leq_add2l.
exact: IHv.
- have Hs : s1 = s2 by apply: Hsame; rewrite Hxz Hyz.
rewrite Hs addnA leq_add2r.
exact: bool_triangle.
Qed.
Lemma flip_count_pairmap_insert_anywhere (xs ys : seq nat) (y : nat) (a : nat) :
flip_count (pairmap (fun u : nat ⇒ [eta leq u.+1]) a (xs ++ ys)) ≤
flip_count (pairmap (fun u : nat ⇒ [eta leq u.+1]) a (xs ++ y :: ys)).
Proof.
move: a; elim: xs ⇒ [|x xs IH] a /=.
- exact: flip_count_pairmap_insert.
- have IHv := IH x.
case Exs : xs IHv ⇒ [|x' xs'] IHv.
+ rewrite /= in IHv |- ×.
case Eys : ys IHv ⇒ [|z ys'] IHv.
× rewrite /flip_count /= !big_cons big_nil !addn0.
by case: ((a < x)%N (+) (x < y)%N).
× rewrite /flip_count /= !big_cons in IHv |- ×.
apply: flip_step_helper.
-- exact: IHv.
-- by move⇒ →.
+ rewrite /=.
rewrite /flip_count /= !big_cons.
rewrite leq_add2l.
rewrite /= in IHv.
exact: IHv.
Qed.
Lemma flip_count_sign_seq_insert_front (y : nat) (xs : seq nat) :
flip_count (sign_seq xs) ≤ flip_count (sign_seq (y :: xs)).
Proof.
case: xs ⇒ [|x xs] /=.
by [].
case: xs ⇒ [|x' xs'] /=.
by rewrite /flip_count /= big_nil.
rewrite /flip_count /= !big_cons.
by case: ((y < x)%N (+) (x < x')%N).
Qed.
Lemma subseq_drop_extra (xs ys : seq nat) :
subseq xs ys → size xs < size ys →
∃ i, i < size ys ∧
subseq xs (take i ys ++ drop i.+1 ys).
Proof.
elim: ys xs ⇒ [|y ys IH] xs //=.
case: xs ⇒ [|x xs] /=.
- move⇒ _ _.
∃ 0; split ⇒ //=.
by rewrite drop0 sub0seq.
- case Eeq : (x == y) ⇒ Hsub Hsz.
+ have Hsz' : size xs < size ys by [].
have [i [Hi Hsubi]] := IH xs Hsub Hsz'.
∃ i.+1; split ⇒ //=.
by rewrite Eeq.
+ ∃ 0; split ⇒ //=.
by rewrite drop0.
Qed.
Lemma size_take_drop_skip (i : nat) (ys : seq nat) :
i < size ys → size (take i ys ++ drop i.+1 ys) = (size ys).-1.
Proof.
move⇒ Hi.
rewrite size_cat size_take size_drop Hi.
case Hsz : (size ys) Hi ⇒ [|m] Hi //=.
rewrite subSS.
have Him : i ≤ m by rewrite -ltnS.
by rewrite subnKC.
Qed.
Lemma flip_count_pairmap_le_subseq (xs ys : seq nat) :
subseq xs ys →
∀ a : nat,
flip_count (pairmap (fun u : nat ⇒ [eta leq u.+1]) a xs) ≤
flip_count (pairmap (fun u : nat ⇒ [eta leq u.+1]) a ys).
Proof.
move⇒ Hsub.
have [k Hk] : ∃ k, size ys = size xs + k.
by ∃ (size ys - size xs); rewrite addnC subnK //; exact: size_subseq.
move: xs ys Hsub Hk.
elim: k ⇒ [|k IH] xs ys Hsub Hk a.
- rewrite addn0 in Hk.
have HL := size_subseq_leqif Hsub.
have Heq : xs = ys.
by case: HL ⇒ _ Hiff; apply/eqP; rewrite -Hiff Hk.
by rewrite Heq.
- have Hszlt : size xs < size ys by rewrite Hk addnS ltnS leq_addr.
have [i [Hi Hsubi]] := subseq_drop_extra Hsub Hszlt.
pose ys' := take i ys ++ drop i.+1 ys.
have Hsz' : size ys' = size xs + k.
have := size_take_drop_skip Hi.
rewrite -/ys' Hk addnS /=.
by case Hsz0: (size ys) ⇒ [|m] //= [->].
have IHv := IH xs ys' Hsubi Hsz' a.
apply: leq_trans IHv _.
have Hys_split : ys = take i ys ++ (nth 0 ys i :: drop i.+1 ys).
rewrite -[in LHS](cat_take_drop i ys).
congr (_ ++ _).
by rewrite (drop_nth 0 Hi).
rewrite [X in _ ≤ flip_count (pairmap _ _ X)]Hys_split.
exact: flip_count_pairmap_insert_anywhere.
Qed.
Lemma flip_count_sign_seq_le_subseq (xs ys : seq nat) :
subseq xs ys →
flip_count (sign_seq xs) ≤ flip_count (sign_seq ys).
Proof.
move⇒ Hsub.
case: xs Hsub ⇒ [|x xs] Hsub /=.
- by [].
- case: ys Hsub ⇒ [|y ys] Hsub.
+ by move: Hsub; rewrite /= ⇒ /eqP.
+ rewrite /sign_seq /=.
case Eeq : (x == y) Hsub ⇒ Hsub.
× move/eqP: Eeq ⇒ Eeq; rewrite Eeq in Hsub ×.
have Hsub' : subseq xs ys.
by move: Hsub; rewrite /= eq_refl.
exact: flip_count_pairmap_le_subseq Hsub' y.
× have Hsubys : subseq (x :: xs) ys.
by move: Hsub; rewrite /= Eeq.
have Hstep1 := flip_count_sign_seq_insert_front y (x :: xs).
rewrite /sign_seq /= in Hstep1.
have Hstep2 : flip_count (pairmap (fun u : nat ⇒ [eta leq u.+1]) y (x :: xs)) ≤
flip_count (pairmap (fun u : nat ⇒ [eta leq u.+1]) y ys).
exact: flip_count_pairmap_le_subseq Hsubys y.
exact: leq_trans Hstep1 Hstep2.
Qed.
Fixpoint is_alt_bool_aux (a : bool) (xs : seq bool) : bool :=
match xs with
| [::] ⇒ true
| b :: rest ⇒ (a (+) b) && is_alt_bool_aux b rest
end.
Definition is_alt_bool (xs : seq bool) : bool :=
match xs with
| [::] ⇒ true
| a :: rest ⇒ is_alt_bool_aux a rest
end.
Lemma flip_count_is_alt_bool xs :
is_alt_bool xs → flip_count xs = (size xs).-1.
Proof.
case: xs ⇒ [|a xs] //=.
elim: xs a ⇒ [|b xs IH] a //=.
by rewrite /flip_count /= big_nil.
case/andP ⇒ Hab Halt.
rewrite /flip_count /= big_cons Hab /=.
have IHv := IH b Halt.
rewrite /flip_count /= in IHv.
by rewrite IHv add1n.
Qed.
Lemma sign_seq_is_alt xs :
is_alt xs → 2 ≤ size xs → is_alt_bool (sign_seq xs).
Proof.
case: xs ⇒ [|x [|y rest]] //=.
move⇒ Halt _.
move: x y Halt; elim: rest ⇒ [|z rest IH] x y //= Halt.
case/orP: Halt ⇒ /andP [Hcmp Halt].
- case/andP: Halt ⇒ Hzy Halt2.
rewrite Hcmp /=.
have Hyzn : ~~ (y < z) by rewrite -leqNgt ltnW.
rewrite (negbTE Hyzn) /=.
have Halt' : (y < z) && alt_aux false z rest || (z < y) && alt_aux true z rest.
by rewrite Hzy Halt2 /= orbT.
have IHv := IH y z Halt'.
by move: IHv; rewrite (negbTE Hyzn).
- case/andP: Halt ⇒ Hyz Halt2.
have Hxyn : ~~ (x < y) by rewrite -leqNgt ltnW.
rewrite (negbTE Hxyn) Hyz /=.
have Halt' : (y < z) && alt_aux false z rest || (z < y) && alt_aux true z rest.
by rewrite Hyz Halt2 /=.
have IHv := IH y z Halt'.
by move: IHv; rewrite Hyz.
Qed.
Lemma is_alt_flip_count xs :
is_alt xs → 2 ≤ size xs → flip_count (sign_seq xs) = (size xs).-2.
Proof.
move⇒ Halt Hsz.
have := flip_count_is_alt_bool (sign_seq_is_alt Halt Hsz).
rewrite size_sign_seq.
by case: xs Halt Hsz ⇒ [|x [|y [|z rest]]] //= _ _ →.
Qed.
Section UpperBoundAssembly.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).
Lemma sort_enum_strict_sorted (I : {set 'I_n.+2}) :
sorted (fun a b : 'I_n.+2 ⇒ val a < val b)
(sort (fun a b : 'I_n.+2 ⇒ val a ≤ val b) (enum I)).
Proof.
have Hsort := sort_sorted (T := 'I_n.+2)
(fun a b ⇒ leq_total (val a) (val b)) (enum I).
have Huniq : uniq (sort (fun a b : 'I_n.+2 ⇒ val a ≤ val b) (enum I)).
by rewrite sort_uniq enum_uniq.
move: Hsort Huniq.
elim: (sort _ _) ⇒ [|a [|b xs] IH] //= /andP [Hab Hsorted] /andP [Han Hu].
have Hab' : val a < val b.
rewrite ltn_neqAle Hab andbT.
apply/eqP ⇒ Hva.
have Hab2 : a = b by apply: val_inj.
by move: Han; rewrite Hab2 inE eq_refl.
rewrite Hab' /=.
exact: IH.
Qed.
End UpperBoundAssembly.
Section LowerBound.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).
Definition turn_inj (t : 'I_n) : 'I_n.+2 :=
lift ord0 (widen_ord (leqnSn n) t).
Lemma val_turn_inj (t : 'I_n) : val (turn_inj t) = (val t).+1.
Proof. by rewrite /turn_inj /= /bump /= add1n. Qed.
Lemma turn_inj_inj : injective turn_inj.
Proof.
move⇒ a b /(congr1 val); rewrite !val_turn_inj ⇒ /succn_inj.
exact: val_inj.
Qed.
Definition turn_witness s : {set 'I_n.+2} :=
ord0 |: (ord_max |: [set turn_inj t | t in [set i : 'I_n | is_turn s i]]).
Lemma card_turn_image s :
#|[set turn_inj t | t in [set i : 'I_n | is_turn s i]]| = turn_count s.
Proof. by rewrite card_imset //; apply: turn_inj_inj. Qed.
Lemma turn_image_lt_max s (x : 'I_n.+2) :
x \in [set turn_inj t | t in [set i : 'I_n | is_turn s i]] →
0 < val x ≤ n.
Proof.
case/imsetP ⇒ t _ →.
rewrite val_turn_inj /=.
by have := ltn_ord t.
Qed.
Lemma ord0_notin_turn_image s :
(ord0 : 'I_n.+2) \notin [set turn_inj t | t in [set i : 'I_n | is_turn s i]].
Proof.
apply/negP ⇒ /turn_image_lt_max /andP [].
by rewrite (_ : val (ord0 : 'I_n.+2) = 0).
Qed.
Lemma ord_max_notin_turn_image s :
(ord_max : 'I_n.+2) \notin
[set turn_inj t | t in [set i : 'I_n | is_turn s i]].
Proof.
apply/negP ⇒ /turn_image_lt_max /andP [_].
rewrite (_ : val (ord_max : 'I_n.+2) = n.+1) //.
by rewrite ltnn.
Qed.
Lemma ord0_neq_ord_max : (ord0 : 'I_n.+2) != ord_max.
Proof. by rewrite -val_eqE /=. Qed.
Lemma card_turn_witness s :
#|turn_witness s| = (turn_count s).+2.
Proof.
rewrite /turn_witness.
rewrite cardsU1 in_setU1 (negbTE ord0_neq_ord_max) /=.
rewrite (negbTE (ord0_notin_turn_image s)) /=.
rewrite cardsU1 (negbTE (ord_max_notin_turn_image s)) /=.
by rewrite card_turn_image add1n add1n.
Qed.
Lemma slot_descent_const_strict s (i j : 'I_n.+2) :
(∀ t : 'I_n, val i < (val t).+1 < val j → ~~ is_turn s t) →
∀ (k1 k2 : 'I_n.+1),
val i ≤ val k1 → val k1 ≤ val k2 → val k2 < val j →
is_descent s k1 = is_descent s k2.
Proof.
move⇒ Hnoturn k1 k2 Hi1 H12 H2j.
move: H12 Hi1.
elim: (val k2 - val k1) {-2}k1 (refl_equal (val k2 - val k1)) ⇒
[|d IH] k1' Hd H12 Hi1.
- move/eqP: Hd; rewrite subn_eq0 ⇒ Hk21.
have : val k1' = val k2 by apply/eqP; rewrite eqn_leq H12 Hk21.
by move⇒ /val_inj →.
- have Hk1lt : val k1' < val k2 by rewrite -subn_gt0 Hd.
have Hk1ord : val k1' < n.
by have := ltn_ord k2; rewrite ltnS ⇒ Hk2; rewrite (leq_trans Hk1lt).
pose t : 'I_n := Ordinal Hk1ord.
have Ht : val i < (val t).+1 < val j.
apply/andP; split; first by apply: leq_ltn_trans Hi1 _.
by rewrite (leq_trans _ H2j).
have := Hnoturn t Ht.
rewrite /is_turn negb_add ⇒ /eqP Hd1.
have Hk1eq : (widen_ord (leqnSn n) t : 'I_n.+1) = k1' by apply: val_inj.
rewrite Hk1eq in Hd1; rewrite Hd1.
have HSk1 : val (lift ord0 t : 'I_n.+1) = (val k1').+1
by rewrite /= /bump /= add1n.
apply: (IH (lift ord0 t)).
- rewrite HSk1; apply: succn_inj.
by rewrite subnSK // Hd.
- by rewrite HSk1.
- by rewrite HSk1 (leq_trans Hi1).
Qed.
Lemma inter_turn_monotone_strict s (i j : 'I_n.+2) :
val i < val j →
(∀ t : 'I_n, val i < (val t).+1 < val j → ~~ is_turn s t) →
∀ (p q : 'I_n.+2),
val i ≤ val p → val p < val q → val q ≤ val j →
(val (s p) < val (s q))%N = (val (s i) < val (s j))%N.
Proof.
move⇒ Hij Hnoturn p q Hip Hpq Hqj.
have Hjle : val i < n.+1.
by have := ltn_ord j; rewrite ltnS ⇒ Hj2; rewrite (leq_trans Hij).
pose k0 : 'I_n.+1 := Ordinal Hjle.
have Hk0range : val i ≤ val k0 < val j by rewrite /= leqnn /= Hij.
pose b := is_descent s k0.
have Hconst_ij : ∀ k : 'I_n.+1,
val i ≤ val k < val j → is_descent s k = b.
move⇒ k /andP [Hki Hkj].
case: (leqP (val k0) (val k)) ⇒ Hkk0.
- rewrite /b /=.
by apply: esym; apply: (slot_descent_const_strict Hnoturn) ⇒ //=.
- apply: (slot_descent_const_strict Hnoturn) ⇒ //=.
exact: ltnW.
have Hconst_pq : ∀ k : 'I_n.+1,
val p ≤ val k < val q → is_descent s k = b.
move⇒ k /andP [Hkp Hkq].
apply: Hconst_ij.
by rewrite (leq_trans Hip Hkp) /= (leq_trans Hkq).
have Hmono_ij := constant_descent_monotone Hij Hconst_ij.
have Hmono_pq := constant_descent_monotone Hpq Hconst_pq.
case Eb : b Hmono_ij Hmono_pq ⇒ Hmono_ij Hmono_pq /=.
- rewrite ltnNge (ltnW Hmono_pq) /=.
by rewrite ltnNge (ltnW Hmono_ij) /=.
- by rewrite Hmono_pq Hmono_ij.
Qed.
Lemma dir_left_of_turn s (a b : 'I_n.+2) (t : 'I_n) :
b = turn_inj t → val a ≤ val t →
(∀ t' : 'I_n, val a < (val t').+1 < val b → ~~ is_turn s t') →
(val (s a) < val (s b))%N = ~~ is_descent s (widen_ord (leqnSn n) t).
Proof.
move⇒ Hbeq Hat Hno.
have Hbval : val b = (val t).+1 by rewrite Hbeq val_turn_inj.
have Htlt2 : val t < n.+2 by rewrite (leq_trans (ltn_ord t)) //; apply: ltnW.
pose p' : 'I_n.+2 := Ordinal Htlt2.
have Hp'val : val p' = val t by [].
have Hap' : val a ≤ val p' by rewrite Hp'val.
have Hp'b : val p' < val b by rewrite Hp'val Hbval.
have Hbb : val b ≤ val b by [].
have Hab : val a < val b by rewrite (leq_ltn_trans Hap' Hp'b).
rewrite -(inter_turn_monotone_strict Hab Hno Hap' Hp'b Hbb).
have Hwt : (widen_ord (leqnSn n.+1) (widen_ord (leqnSn n) t) : 'I_n.+2) = p'
by apply: val_inj.
have Hlt : (lift ord0 (widen_ord (leqnSn n) t) : 'I_n.+2) = b
by apply: val_inj ⇒ /=; rewrite Hbval /bump /= add1n.
have := not_is_descentE s (widen_ord (leqnSn n) t).
by rewrite Hwt Hlt ⇒ →.
Qed.
Lemma dir_right_of_turn s (b c : 'I_n.+2) (t : 'I_n) :
b = turn_inj t → val b < val c →
(∀ t' : 'I_n, val b < (val t').+1 < val c → ~~ is_turn s t') →
(val (s b) < val (s c))%N = ~~ is_descent s (lift ord0 t).
Proof.
move⇒ Hbeq Hbc Hno.
have Hbval : val b = (val t).+1 by rewrite Hbeq val_turn_inj.
have Htn : val t < n by apply: ltn_ord.
have HtSlt2 : (val t).+2 < n.+2 by rewrite !ltnS.
pose c' : 'I_n.+2 := Ordinal HtSlt2.
have Hc'val : val c' = (val t).+2 by [].
have Hbc' : val b < val c' by rewrite Hbval Hc'val.
have Hbb : val b ≤ val b by [].
have Hc'c : val c' ≤ val c.
by rewrite Hc'val -Hbval.
rewrite -(inter_turn_monotone_strict Hbc Hno Hbb Hbc' Hc'c).
have Hwt : (widen_ord (leqnSn n.+1) (lift ord0 t) : 'I_n.+2) = b.
by apply: val_inj ⇒ /=; rewrite Hbval /bump /= add1n.
have Hlt : (lift ord0 (lift ord0 t) : 'I_n.+2) = c'.
by apply: val_inj ⇒ /=; rewrite /bump /= !add1n.
have := not_is_descentE s (lift ord0 t).
by rewrite Hwt Hlt ⇒ →.
Qed.
Lemma sign_flip_at_turn s (a b c : 'I_n.+2) (t : 'I_n) :
is_turn s t → b = turn_inj t →
val a ≤ val t → val b < val c →
(∀ t' : 'I_n, val a < (val t').+1 < val b → ~~ is_turn s t') →
(∀ t' : 'I_n, val b < (val t').+1 < val c → ~~ is_turn s t') →
(val (s a) < val (s b))%N != (val (s b) < val (s c))%N.
Proof.
move⇒ Htn Hbeq Hat Hbc Hno_left Hno_right.
rewrite (dir_left_of_turn Hbeq Hat Hno_left).
rewrite (dir_right_of_turn Hbeq Hbc Hno_right).
move: Htn; rewrite /is_turn.
by case: (is_descent _ _); case: (is_descent _ _).
Qed.
End LowerBound.
Definition uniq_adj (xs : seq nat) : bool :=
match xs with
| [::] ⇒ true
| x :: xs' ⇒ all (fun p ⇒ p.1 != p.2) (zip (x :: xs') xs')
end.
Lemma uniq_adj_cons2 x y rest :
uniq_adj (x :: y :: rest) = (x != y) && uniq_adj (y :: rest).
Proof. by rewrite /= eqE. Qed.
Lemma uniq_adj_tail x y rest :
uniq_adj (x :: y :: rest) → uniq_adj (y :: rest).
Proof. by case: rest ⇒ [|z r] /= /andP []. Qed.
Lemma uniq_adj_head_neq x y rest :
uniq_adj (x :: y :: rest) → x != y.
Proof. by case: rest ⇒ [|z r] /= /andP []. Qed.
Lemma sign_pair_neq (x y : nat) : x != y → (x < y)%N = ~~ (y < x)%N.
Proof.
move⇒ Hne; case Hxy : (x < y)%N.
by rewrite ltnNge ltnW.
move/negbT: Hxy; rewrite -leqNgt leq_eqVlt ⇒ /orP [/eqP Hxy|->] //.
by rewrite Hxy eq_refl in Hne.
Qed.
Lemma alt_aux_from_sign x y xs :
uniq_adj (x :: y :: xs) →
is_alt_bool (sign_seq (x :: y :: xs)) →
alt_aux (~~ (x < y)%N) y xs.
Proof.
elim: xs y x ⇒ [|z rest IH] y x /=.
by [].
move⇒ Hu Hab.
have Hyz_ne : y != z by case/and3P: Hu.
have Huyz : uniq_adj (y :: z :: rest).
by case: rest Hu {IH Hab} ⇒ [|w r] /=; case/and3P⇒ _ Hyz Hr; rewrite Hyz //=.
move: Hab ⇒ /=.
case/andP⇒ Hflip Hbabool.
have Hrec : alt_aux (~~ (y < z)%N) z rest by exact: IH.
move: Hrec.
have Hxy_yz : (x < y)%N (+) (y < z)%N by exact: Hflip.
case Exy : (x < y)%N Hxy_yz ⇒ Hxy_yz /=.
- have Hyz_false : (y < z)%N = false by case: (y < z)%N Hxy_yz.
rewrite Hyz_false /= ⇒ →.
by rewrite andbT ltn_neqAle leqNgt Hyz_false /= eq_sym Hyz_ne.
- have Hyz_true : (y < z)%N = true by case: (y < z)%N Hxy_yz.
by rewrite Hyz_true /= ⇒ →.
Qed.
Lemma sign_seq_alt_of_triple_flip n (s : {perm 'I_n.+2}) (js : seq 'I_n.+2) :
(∀ i, i.+2 < size js →
(val (s (nth ord0 js i)) < val (s (nth ord0 js i.+1)))%N
!= (val (s (nth ord0 js i.+1)) < val (s (nth ord0 js i.+2)))%N) →
is_alt_bool (sign_seq [seq val (s j) | j <- js]).
Proof.
elim: js ⇒ [|x [|y [|z rest]]] // IH Htriples /=.
have Hrec_hyp : ∀ i, i.+2 < size [:: y, z & rest] →
(val (s (nth ord0 [:: y, z & rest] i))
< val (s (nth ord0 [:: y, z & rest] i.+1)))%N
!= (val (s (nth ord0 [:: y, z & rest] i.+1))
< val (s (nth ord0 [:: y, z & rest] i.+2)))%N.
by move⇒ i Hi; apply: (Htriples i.+1).
have Hrec := IH Hrec_hyp.
move: Hrec; rewrite /sign_seq /=.
move⇒ Hrec.
apply/andP; split; last exact: Hrec.
have H0 : 2 < size [:: x, y, z & rest] by [].
have := Htriples 0%N H0; rewrite /=.
by case: (val (s x) < _)%N; case: (val (s y) < _)%N.
Qed.
Lemma uniq_adj_of_uniq (xs : seq nat) : uniq xs → uniq_adj xs.
Proof.
case: xs ⇒ [|x xs] //=.
elim: xs x ⇒ [|y rest IH] x //= /andP [Hx /andP [Hy Hu]].
have Hxy : x != y by apply: contraNneq Hx ⇒ ->; rewrite mem_head.
rewrite Hxy /=.
by apply: IH; rewrite Hy Hu.
Qed.
Lemma is_alt_from_sign xs :
uniq_adj xs → is_alt_bool (sign_seq xs) → is_alt xs.
Proof.
case: xs ⇒ [|x [|y rest]] // Hu Hab.
have Hxy_ne : x != y by exact: uniq_adj_head_neq Hu.
rewrite is_alt_cons2.
have Hrec := alt_aux_from_sign Hu Hab.
case Exy : (x < y)%N Hrec ⇒ /= Hrec.
by rewrite Hrec.
by rewrite Hrec andbT ltn_neqAle leqNgt Exy /= eq_sym Hxy_ne.
Qed.
Section ExistenceLB.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).
Definition pos_seq s : seq 'I_n.+2 :=
sort (fun a b : 'I_n.+2 ⇒ val a ≤ val b) (enum (turn_witness s)).
Lemma size_pos_seq s : size (pos_seq s) = (turn_count s).+2.
Proof. by rewrite /pos_seq size_sort -cardE card_turn_witness. Qed.
Lemma pos_seq_uniq s : uniq (pos_seq s).
Proof. by rewrite /pos_seq sort_uniq enum_uniq. Qed.
Lemma pick_seq_pos_seq s :
pick_seq s (turn_witness s) = [seq val (s j) | j <- pos_seq s].
Proof. by []. Qed.
Lemma pos_seq_strict_sorted s :
sorted (fun a b : 'I_n.+2 ⇒ val a < val b) (pos_seq s).
Proof. exact: sort_enum_strict_sorted. Qed.
Lemma mem_pos_seq s (x : 'I_n.+2) :
x \in pos_seq s = (x \in turn_witness s).
Proof. by rewrite /pos_seq mem_sort mem_enum. Qed.
Lemma pos_seq_val_lt s (i j : nat) :
i < size (pos_seq s) → j < size (pos_seq s) → i < j →
val (nth ord0 (pos_seq s) i) < val (nth ord0 (pos_seq s) j).
Proof.
move⇒ Hi Hj Hij.
have Htrans : transitive (fun a b : 'I_n.+2 ⇒ val a < val b).
by move⇒ a b c; apply: ltn_trans.
exact: (sorted_ltn_nth Htrans ord0 (pos_seq_strict_sorted s)).
Qed.
Lemma pos_seq_val_lt_inv s (i j : nat) :
i < size (pos_seq s) → j < size (pos_seq s) →
val (nth ord0 (pos_seq s) i) < val (nth ord0 (pos_seq s) j) →
i < j.
Proof.
move⇒ Hi Hj Hlt.
case: (ltngtP i j) Hlt ⇒ // Hij Hlt.
by have := pos_seq_val_lt Hj Hi Hij; rewrite ltnNge ltnW.
by rewrite Hij ltnn in Hlt.
Qed.
Lemma no_inner_in_pos_seq s i (x : 'I_n.+2) :
i.+1 < size (pos_seq s) →
x \in pos_seq s →
val (nth ord0 (pos_seq s) i) < val x →
val x < val (nth ord0 (pos_seq s) i.+1) →
False.
Proof.
move⇒ Hi Hin Hxa Hxb.
have Hi0 : i < size (pos_seq s) by exact: ltnW.
have /(nthP ord0) [j Hj Hxnth] := Hin.
rewrite -Hxnth in Hxa Hxb.
have H1 := pos_seq_val_lt_inv Hi0 Hj Hxa.
have H2 := pos_seq_val_lt_inv Hj Hi Hxb.
by have := leq_trans H2 H1; rewrite ltnn.
Qed.
Lemma pos_seq_nth0 s : nth ord0 (pos_seq s) 0 = ord0.
Proof.
have Hsz : 0 < size (pos_seq s) by rewrite size_pos_seq.
have Hord0_in : (ord0 : 'I_n.+2) \in pos_seq s.
by rewrite mem_pos_seq /turn_witness !inE eq_refl.
have /(nthP ord0) [k Hk Hk_eq] := Hord0_in.
case Ek : k Hk Hk_eq ⇒ [|k'] Hk Hk_eq.
by [].
have Hk0lt : (0 < k'.+1)%N by [].
have := pos_seq_val_lt Hsz Hk Hk0lt.
rewrite Hk_eq /=.
by [].
Qed.
Lemma pos_seq_last_val s :
val (nth ord0 (pos_seq s) (turn_count s).+1) = n.+1.
Proof.
have Hszm1 : (turn_count s).+1 < size (pos_seq s) by rewrite size_pos_seq.
have Hord_max_in : (ord_max : 'I_n.+2) \in pos_seq s.
by rewrite mem_pos_seq /turn_witness !inE eq_refl orbT.
have /(nthP ord0) [k Hk Hk_eq] := Hord_max_in.
have Hk_le : k ≤ (turn_count s).+1.
rewrite leqNgt; apply/negP ⇒ Hk_gt.
have Hsz_eq : size (pos_seq s) = (turn_count s).+2 by rewrite size_pos_seq.
by have := Hk; rewrite Hsz_eq ltnS leqNgt Hk_gt.
case: (eqVneq k (turn_count s).+1) ⇒ [Heq|Hne].
by rewrite -Heq Hk_eq.
have Hk_lt : k < (turn_count s).+1 by rewrite ltn_neqAle Hne.
have := pos_seq_val_lt Hk Hszm1 Hk_lt.
rewrite Hk_eq /= ⇒ Hcontr.
have Hbound : val (nth ord0 (pos_seq s) (turn_count s).+1) < n.+2 by exact: ltn_ord.
by apply/eqP; rewrite eqn_leq; apply/andP; split;
[have := Hbound; rewrite ltnS | apply: ltnW].
Qed.
Lemma interior_is_turn_inj s (i : nat) :
0 < i → i.+1 < size (pos_seq s) →
∃ t : 'I_n, is_turn s t ∧ nth ord0 (pos_seq s) i = turn_inj t.
Proof.
move⇒ H0 Hi.
have Hi0 : i < size (pos_seq s) by exact: ltnW.
pose b := nth ord0 (pos_seq s) i.
have Hbin : b \in pos_seq s by apply: mem_nth.
rewrite mem_pos_seq /turn_witness !inE in Hbin.
case/orP: Hbin ⇒ [/eqP Hb_ord0|].
exfalso.
have Hsz_pos : 0 < size (pos_seq s) by rewrite size_pos_seq.
have := pos_seq_val_lt Hsz_pos Hi0 H0.
by rewrite pos_seq_nth0 -/b Hb_ord0.
case/orP ⇒ [/eqP Hb_ord_max|].
exfalso.
have Hsz_eq : size (pos_seq s) = (turn_count s).+2 by rewrite size_pos_seq.
have Hi_lt : i < (turn_count s).+1 by have := Hi; rewrite Hsz_eq.
have Hszm1 : (turn_count s).+1 < size (pos_seq s) by rewrite Hsz_eq.
have := pos_seq_val_lt Hi0 Hszm1 Hi_lt.
rewrite -/b Hb_ord_max pos_seq_last_val.
by rewrite ltnn.
case/imsetP ⇒ t Hin Heq.
∃ t; split.
by move: Hin; rewrite inE.
by [].
Qed.
Lemma interior_val_bounds s i :
0 < i → i.+1 < size (pos_seq s) →
0 < val (nth ord0 (pos_seq s) i) ∧
val (nth ord0 (pos_seq s) i) < n.+1.
Proof.
move⇒ H0 Hi.
have Hi0 : i < size (pos_seq s) by exact: ltnW.
have [t [Ht Heq]] := interior_is_turn_inj H0 Hi.
rewrite Heq val_turn_inj.
split; first by [].
by have := ltn_ord t.
Qed.
Lemma triple_flip_pos_seq s i :
i.+2 < size (pos_seq s) →
(val (s (nth ord0 (pos_seq s) i)) < val (s (nth ord0 (pos_seq s) i.+1)))%N
!= (val (s (nth ord0 (pos_seq s) i.+1)) < val (s (nth ord0 (pos_seq s) i.+2)))%N.
Proof.
move⇒ Hi.
have Hi1 : i.+1 < size (pos_seq s) by exact: ltnW.
have Hi0 : i < size (pos_seq s) by do 2 apply: ltnW.
pose a := nth ord0 (pos_seq s) i.
pose b := nth ord0 (pos_seq s) i.+1.
pose c := nth ord0 (pos_seq s) i.+2.
have Hab : val a < val b by exact: pos_seq_val_lt.
have Hbc : val b < val c by exact: pos_seq_val_lt.
have [t [Htn Heqb]] := interior_is_turn_inj (i := i.+1) (ltn0Sn _) Hi.
have Hbeq : b = turn_inj t by [].
have Hbval : val b = (val t).+1 by rewrite Hbeq val_turn_inj.
have Hat : val a ≤ val t.
by rewrite -ltnS -Hbval.
have Hno_left : ∀ t' : 'I_n, val a < (val t').+1 < val b → ~~ is_turn s t'.
move⇒ t' /andP [Ht1 Ht2].
apply/negP ⇒ Ht'turn.
pose x := turn_inj t'.
have Hxin : x \in pos_seq s.
rewrite mem_pos_seq /turn_witness !inE.
apply/orP; right; apply/orP; right.
apply/imsetP; ∃ t' ⇒ //.
by rewrite inE.
have Hxa : val a < val x by rewrite val_turn_inj.
have Hxb : val x < val b by rewrite val_turn_inj.
exact: (no_inner_in_pos_seq Hi1 Hxin Hxa Hxb).
have Hno_right : ∀ t' : 'I_n, val b < (val t').+1 < val c → ~~ is_turn s t'.
move⇒ t' /andP [Ht1 Ht2].
apply/negP ⇒ Ht'turn.
pose x := turn_inj t'.
have Hxin : x \in pos_seq s.
rewrite mem_pos_seq /turn_witness !inE.
apply/orP; right; apply/orP; right.
apply/imsetP; ∃ t' ⇒ //.
by rewrite inE.
have Hxb : val b < val x by rewrite val_turn_inj.
have Hxc : val x < val c by rewrite val_turn_inj.
exact: (no_inner_in_pos_seq Hi Hxin Hxb Hxc).
exact: (sign_flip_at_turn Htn Heqb Hat Hbc Hno_left Hno_right).
Qed.
Theorem is_alt_pick_turn_witness s :
is_alt (pick_seq s (turn_witness s)).
Proof.
rewrite pick_seq_pos_seq.
apply: is_alt_from_sign.
apply: uniq_adj_of_uniq.
rewrite map_inj_in_uniq.
exact: pos_seq_uniq.
by move⇒ x y _ _ /val_inj /perm_inj.
apply: sign_seq_alt_of_triple_flip.
exact: triple_flip_pos_seq.
Qed.
Theorem as_perm_max_lower s : (turn_count s).+2 ≤ as_perm_max s.
Proof.
rewrite -card_turn_witness.
rewrite /as_perm_max.
exact: (leq_bigmax_cond (turn_witness s) (is_alt_pick_turn_witness s)).
Qed.
End ExistenceLB.
Section UpperBoundChain.
Variable n : nat.
Implicit Types (s : {perm 'I_n.+2}).
Lemma sort_enum_subseq_enum (I : {set 'I_n.+2}) :
subseq (sort (fun a b : 'I_n.+2 ⇒ val a ≤ val b) (enum I)) (enum 'I_n.+2).
Proof.
have Hle_total : total (fun a b : 'I_n.+2 ⇒ val a ≤ val b).
by move⇒ a b; apply: leq_total.
have Hle_trans : transitive (fun a b : 'I_n.+2 ⇒ val a ≤ val b).
by move⇒ a b c; apply: leq_trans.
have Hsub_enumI : subseq (enum I) (enum 'I_n.+2).
rewrite enumT /enum_mem.
exact: filter_subseq.
have Hsorted : sorted (fun a b : 'I_n.+2 ⇒ val a ≤ val b) (enum 'I_n.+2).
exact: sorted_val_enum_ord.
have Hsort_enum : sort (fun a b : 'I_n.+2 ⇒ val a ≤ val b) (enum 'I_n.+2) =
enum 'I_n.+2.
exact: (sorted_sort Hle_trans Hsorted).
rewrite -Hsort_enum.
apply: (subseq_sort Hle_total Hle_trans).
exact: Hsub_enumI.
Qed.
Lemma pick_seq_subseq_perm_seq s (I : {set 'I_n.+2}) :
subseq (pick_seq s I) (perm_seq s).
Proof.
rewrite /pick_seq /perm_seq.
exact: map_subseq (sort_enum_subseq_enum I).
Qed.
Lemma flip_count_pick_le_perm s (I : {set 'I_n.+2}) :
flip_count (sign_seq (pick_seq s I)) ≤ flip_count (sign_seq (perm_seq s)).
Proof.
exact: flip_count_sign_seq_le_subseq (pick_seq_subseq_perm_seq s I).
Qed.
Lemma flip_count_as_sum (xs : seq bool) :
flip_count xs = \sum_(0 ≤ i < (size xs).-1) (nth false xs i (+) nth false xs i.+1).
Proof.
case: xs ⇒ [|x xs] /=.
by rewrite /flip_count /= big_nil.
rewrite /flip_count /=.
rewrite (big_nth false) size_pairmap.
apply: eq_big_nat ⇒ i Hi.
have Hi' : i < size xs by case/andP: Hi.
rewrite (nth_pairmap x) //.
case: i Hi' {Hi} ⇒ [|i] Hi' //=.
- by rewrite (@set_nth_default _ _ false x).
- rewrite (@set_nth_default _ _ false x i (ltnW Hi')).
by rewrite (@set_nth_default _ _ false x i.+1 Hi').
Qed.
Lemma neg_add_neg (a b : bool) : ~~ a (+) ~~ b = a (+) b.
Proof. by case: a; case: b. Qed.
Lemma flip_count_perm_seq_eq_turn_count s :
flip_count (sign_seq (perm_seq s)) = turn_count s.
Proof.
rewrite sign_seq_perm_seq flip_count_as_sum.
rewrite size_map size_enum_ord /=.
under eq_big_nat ⇒ i Hi.
have Hi1 : i < n.+1 by case/andP: Hi ⇒ _; apply: ltnW.
have Hi2 : i.+1 < n.+1 by case/andP: Hi.
rewrite (nth_map ord0); last by rewrite size_enum_ord.
rewrite (nth_map ord0); last by rewrite size_enum_ord.
rewrite neg_add_neg.
over.
rewrite big_mkord.
have Hsum_eq : ∀ i : 'I_n,
is_descent s (nth ord0 (enum 'I_n.+1) i)
(+) is_descent s (nth ord0 (enum 'I_n.+1) i.+1) = is_turn s i.
move⇒ i.
have Heq1 : (nth ord0 (enum 'I_n.+1) i : 'I_n.+1) = widen_ord (leqnSn n) i.
by apply: val_inj ⇒ /=; rewrite nth_enum_ord //; apply: ltnW; apply: ltn_ord.
have Heq2 : (nth ord0 (enum 'I_n.+1) i.+1 : 'I_n.+1) = lift ord0 i.
apply: val_inj ⇒ /=.
rewrite nth_enum_ord /=. by rewrite /bump /= add1n.
by apply: ltn_ord.
by rewrite Heq1 Heq2.
under eq_bigr ⇒ i _ do rewrite Hsum_eq.
rewrite /turn_count -sum1_card.
rewrite [in RHS]big_mkcond.
apply: eq_bigr ⇒ i _.
rewrite inE.
by case: (is_turn s i).
Qed.
Lemma as_perm_max_upper s : as_perm_max s ≤ (turn_count s).+2.
Proof.
rewrite /as_perm_max.
apply/bigmax_leqP ⇒ I HI.
case Hsize : (#|I| ≤ 1).
by rewrite (leq_trans Hsize).
move/negbT: Hsize; rewrite -ltnNge ⇒ Hsize2.
have Hps_size : size (pick_seq s I) = #|I|.
by rewrite /pick_seq size_map size_sort -cardE.
have Hsz_ge2 : 2 ≤ size (pick_seq s I) by rewrite Hps_size.
have Halt_fc := is_alt_flip_count HI Hsz_ge2.
rewrite Hps_size in Halt_fc.
have Hbound : (#|I|).-2 ≤ turn_count s.
rewrite -Halt_fc -flip_count_perm_seq_eq_turn_count.
exact: flip_count_pick_le_perm.
by case Hcard : #|I| Hsize2 Hbound ⇒ [|[|m]] // _ _.
Qed.
Theorem as_perm_max_eq s : as_perm_max s = (turn_count s).+2.
Proof.
apply: anti_leq.
apply/andP; split.
- exact: as_perm_max_upper.
- exact: as_perm_max_lower.
Qed.
End UpperBoundChain.