From bb5616a033b6c689c4a2cc85cac14d64ad395f6b Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Sun, 24 Dec 2023 15:52:50 +0100 Subject: [PATCH] Minor reformat --- theories/LRrule/Schensted.v | 50 ++++++++++++++++++++++--------------- 1 file changed, 30 insertions(+), 20 deletions(-) diff --git a/theories/LRrule/Schensted.v b/theories/LRrule/Schensted.v index f631efa..7cbe71a 100644 --- a/theories/LRrule/Schensted.v +++ b/theories/LRrule/Schensted.v @@ -17,12 +17,12 @@ This file is a formalization of Schensted's algorithm and the Robinson-Schensted correspondence. In the latter, it is easier to first store record the insertion -as a Yamanouchi word, that is the reverted sequence of the index of the rows where -the elements were inserted. In a second step, we translate the Yamanouchi word -in a standard tableau. +as a Yamanouchi word, that is the reverted sequence of the index of the rows +where the elements were inserted. In a second step, we translate the Yamanouchi +word in a standard tableau. -Note: There is some duplication is this file, essentially for pedagogical purpose. -And also because it was my first serious Coq/Mathcomp development ;-) +Note: There is some duplication is this file, essentially for pedagogical +purpose. And also because it was my first serious Coq/Mathcomp development ;-) Here are the contents: @@ -76,14 +76,17 @@ Inverting the Robinson-Schensted map: [instabnrow t l = (s, n)]. This is Theorem [invinstabnrowK]. See also Theorem [instabnrowinvK]. -- [RSmap w] == the Robinson-Schensted map where the recording tableau is returned - as a Yamanouchi word. +- [RSmap w] == the Robinson-Schensted map where the recording tableau is + returned as a Yamanouchi word. - [is_RSpair (P, Q)] == [P] is a tableau, [Q] is a Yammanouchi word and the shape of [P] is equal to the evaluation of [Q]. + The main result is of course [Theorem RSmap_spec w : is_RSpair (RSmap w).] -- [RSmapinv tab yam] == the Robinson-Schensted inverse map of the pair [(tab, yam)] +- [RSmapinv tab yam] == the Robinson-Schensted inverse map of the pair + [(tab, yam)] - [RSmapinv2 p] == the uncurrying of [RSmapinv]. + The bijectivity of [RSmap] and [RSmapinv2] are stated in - Theorem [RSmapK] stated as [RSmapinv2 (RSmap w) = w.] - and Theorem [RSmapinv2K] as [RSmap (RSmapinv2 pair) = pair.] @@ -96,6 +99,7 @@ A sigma type for Robinson-Schensted pairs: - [rspair T] == a sigma type for RS pair with tableau in type [T]. - [RSbij w] == the [rspair T] associated to [w : seq T] - [RSbijinv p] == the [seq T] associated to [p : rspair T] + On has [Lemma bijRS : bijective RSbij.] @@ -104,7 +108,6 @@ Robinson-Schensted classes: - [RSclass t] == the list of word [w] having [t] as RS tableau. This is stated in Lemma [RSclassE] which says [w \in RSclass tab = (RS w == tab)]. - Robinson-Schensted with standard recording tableau: - [is_RStabpair (P, Q)] == [P] and [Q] are two tableau of the same shape, @@ -116,6 +119,7 @@ Robinson-Schensted with standard recording tableau: - [RStab w] == the RS map applied to [w] as a [rstabpair T]. - [RStabinv pair] == the word [w] associated to a [rstabpair] + Again, one has [Lemma bijRStab : bijective RStab.] **************) From HB Require Import structures. @@ -924,8 +928,9 @@ Lemma shape_instabnrow t l : let: (tr, nrow) := instabnrow t l in shape tr = incr_nth (shape t) nrow. Proof using. case H : (instabnrow t l) => [tr nrow] Htab. -elim: t Htab l tr nrow H => [/= _| t0 t IHt /= /and4P [] _ Hrow _ Htab] l tr nrow /=; - first by move=> [] <- <-. +elim: t Htab l tr nrow H => + [/= _| t0 t IHt /= /and4P[_ Hrow _ Htab]] l tr nrow /=; + first by move=> [<- <-]. case (boolP (bump t0 l)) => [Hbump | Hnbump]. - rewrite (bump_bumprowE Hrow Hbump). case: nrow => [|nrow]; first by case (instabnrow t (bumped t0 l)). @@ -1060,7 +1065,7 @@ Definition RSmap w := RSmap_rev (rev w). Lemma RSmapE w : (RSmap w).1 = RS w. Proof using. -elim/last_ind: w => [//= | w wn /=]; rewrite /RSmap /RS rev_rcons /= -instabnrowE. +elim/last_ind: w => [| w wn] //=; rewrite /RSmap /RS rev_rcons /= -instabnrowE. case: (RSmap_rev (rev w)) => [t rows] /= ->. by case: (instabnrow (RS_rev (rev w)) wn). Qed. @@ -1097,7 +1102,8 @@ by case Hins: (instabnrow t l0) => [tr row] /= -> ->. Qed. Definition is_RSpair pair := - let: (P, Q) := pair in [&& is_tableau (T:=T) P, is_yam Q & (shape P == evalseq Q)]. + let: (P, Q) := pair in + [&& is_tableau (T:=T) P, is_yam Q & (shape P == evalseq Q)]. Theorem RSmap_spec w : is_RSpair (RSmap w). Proof using. @@ -1138,7 +1144,8 @@ case H : (invbumprow b s) => [r a] /=. by case: (leP b (head b s)) => _ //= ->. Qed. -Lemma yam_tail_non_nil (l : nat) (s : seq nat) : is_yam (l.+1 :: s) -> s != [::]. +Lemma yam_tail_non_nil (l : nat) (s : seq nat) : + is_yam (l.+1 :: s) -> s != [::]. Proof using. case: s => [|//=] Hyam. by have:= is_part_eval_yam Hyam; rewrite part_head0F. @@ -1180,7 +1187,8 @@ Lemma head_tableau_non_nil h t : is_tableau (h :: t) -> h != [::]. Proof using. by move/and4P => [] ->. Qed. Lemma is_tableau_instabnrowinv1 (s : seq (seq T)) nrow : - is_tableau s -> is_rem_corner (shape s) nrow -> is_tableau (invinstabnrow s nrow).1. + is_tableau s -> is_rem_corner (shape s) nrow -> + is_tableau (invinstabnrow s nrow).1. Proof using. rewrite /is_rem_corner. elim: s nrow => [/= |s0 s IHs] nrow; first by case nrow. @@ -1276,7 +1284,8 @@ Qed. Theorem count_RS w p : count p w = count p (to_word (RS w)). Proof using. -elim/last_ind: w => [//= | w0 w]; rewrite /RS !rev_rcons /= -[(RS_rev (rev w0))]/(RS w0). +elim/last_ind: w => [//= | w0 w]; + rewrite /RS !rev_rcons /= -[(RS_rev (rev w0))]/(RS w0). rewrite (count_instab _ _ (is_tableau_RS _)) => <-. by rewrite -[rcons _ _](revK) rev_rcons count_rev /= count_rev. Qed. @@ -1314,10 +1323,11 @@ End Bijection. (** ** Robinson-Schensted classes *) Section Classes. -Definition RSclass := [fun tab => -[seq RSmapinv2 (tab, y) | y <- enum_yameval (shape tab)] ]. +Definition RSclass := + [fun tab => [seq RSmapinv2 (tab, y) | y <- enum_yameval (shape tab)] ]. -Lemma RSclassP tab : is_tableau tab -> all (fun w => RS w == tab) (RSclass tab). +Lemma RSclassP tab : + is_tableau tab -> all (fun w => RS w == tab) (RSclass tab). Proof using. move=> Htab /=; apply/allP => w /mapP [] Q. move /(allP (enum_yamevalP (is_part_sht Htab))). @@ -1345,7 +1355,7 @@ Lemma mem_RSclass w : w \in (RSclass (RS w)). Proof using. apply negbNE; apply/count_memPn. by rewrite RSclass_countE. Qed. Lemma RSclassE tab w : -is_tableau tab -> w \in RSclass tab = (RS w == tab). + is_tableau tab -> w \in RSclass tab = (RS w == tab). Proof using. move=> Htab /=; apply/idP/idP. - by move: Htab=> /RSclassP/allP H{}/H.