From fb323d770db6a2c1489d61f72bf7ca656549f739 Mon Sep 17 00:00:00 2001 From: Florent Hivert Date: Thu, 1 Feb 2024 09:03:42 +0100 Subject: [PATCH] Typo in the doc + minor proof improvements --- theories/Erdos_Szekeres/Erdos_Szekeres.v | 2 +- theories/LRrule/Greene_inv.v | 26 ++++++++++++------------ theories/LRrule/freeSchur.v | 4 ++-- theories/LRrule/plactic.v | 2 ++ 4 files changed, 18 insertions(+), 16 deletions(-) diff --git a/theories/Erdos_Szekeres/Erdos_Szekeres.v b/theories/Erdos_Szekeres/Erdos_Szekeres.v index 7ee7ad6..ceda0d4 100644 --- a/theories/Erdos_Szekeres/Erdos_Szekeres.v +++ b/theories/Erdos_Szekeres/Erdos_Szekeres.v @@ -22,7 +22,7 @@ type contains - either a nondecreasing subsequence of length [n+1]; - or a strictly decreasing subsequence of length [m+1]. We prove it as a corollary of Greene's theorem on the Robinson-Schensted -correspondance. Note that there are other proof which require less theory. +correspondance. Note that there are other proofs which require less theory. *****) Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq fintype. diff --git a/theories/LRrule/Greene_inv.v b/theories/LRrule/Greene_inv.v index 65e0438..b77b7e1 100644 --- a/theories/LRrule/Greene_inv.v +++ b/theories/LRrule/Greene_inv.v @@ -1314,10 +1314,9 @@ case (boolP [exists S, [&& S \in S1, posa \in S & posc \in S] ]). by rewrite HSb orbT. have /extract2 -> : posa < posc by []. rewrite !(tnth_nth b) /= andbT. - elim u => [| u0 u'] /=. - + move: Hord => /andP[/le_lt_trans /[apply]]. - by rewrite leNgt => ->. - + by apply. + elim u => [| u0 u'] //=. + move: Hord => /andP[/le_lt_trans /[apply]]. + by rewrite leNgt => ->. - rewrite negb_exists => /forallP Hall. exists (NoSetContainingBoth.Q S1); rewrite NoSetContainingBoth.size_cover_Q /=. @@ -1352,19 +1351,19 @@ case (boolP [exists S, [&& S \in P, posa \in S & posc \in S] ]). move HcastS : (cast_set (congr1 size Hbac) S) => S'. have HS'in : S' \in P' by rewrite -HcastP -HcastS; apply: imset_f. set pos1 := Swap.pos1 u (c :: w) b a. - have Hpos1 : pos1 \in S'. + have {posa HSa} Hpos1 : pos1 \in S'. rewrite -(cast_ordKV (congr1 size Hbac) pos1) -HcastS /cast_set /=. apply: imset_f. suff -> /= : cast_ord (esym (congr1 size Hbac)) pos1 = posa by []. by apply: val_inj; rewrite /= size_cat /= addn1. set pos2 := SetContainingBothLeft.posc u w a b c. - have Hpos2 : pos2 \in S'. + have {posc HSc} Hpos2 : pos2 \in S'. rewrite -(cast_ordKV (congr1 size Hbac) pos2) -HcastS /cast_set /=. apply: imset_f. suff -> /= : cast_ord (esym (congr1 size Hbac)) pos2 = posc by []. by apply: val_inj; rewrite /= size_cat /= addn1. - have:= SetContainingBothLeft.exists_Qy Hyp Hsupp' HS'in Hpos1 Hpos2. - move=> [Q [Hcover HsuppQ]]. + have {pos1 pos2 Hyp Hsupp' S' HcastS HS'in Hpos1 Hpos2} [Q [Hcover HsuppQ]] + := SetContainingBothLeft.exists_Qy Hyp Hsupp' HS'in Hpos1 Hpos2. exists Q; apply/andP; split; last exact HsuppQ. by rewrite Hcover -HcastP -size_cover_inj //=; exact: cast_ord_inj. - rewrite negb_exists => /forallP Hall. @@ -1439,19 +1438,19 @@ case (boolP [exists S, [&& S \in P, posa \in S & posc \in S] ]). move HcastS : (cast_set (congr1 size Hbca) S) => S'. have HS'in : S' \in P' by rewrite -HcastP -HcastS; apply: imset_f. set pos1 := Swap.pos1 u (a :: w) b c. - have Hpos1 : pos1 \in S'. + have {posa HSa} Hpos1 : pos1 \in S'. rewrite -(cast_ordKV (congr1 size Hbca) pos1) -HcastS /cast_set /=. apply: imset_f. suff -> /= : cast_ord (esym (congr1 size Hbca)) pos1 = posa by []. by apply: val_inj; rewrite /= size_cat /= addn1. set pos2 := Ordinal (SetContainingBothLeft.u2lt u w c b a). - have Hpos2 : pos2 \in S'. + have {posc HSc} Hpos2 : pos2 \in S'. rewrite -(cast_ordKV (congr1 size Hbca) pos2) -HcastS /cast_set /=. apply: imset_f. suff -> /= : cast_ord (esym (congr1 size Hbca)) pos2 = posc by []. by apply: val_inj; rewrite /= size_cat /= addn1. - have:= SetContainingBothLeft.exists_Qy Hyp Hsupp' HS'in Hpos1 Hpos2. - move=> [Q [Hcover HsuppQ]]. + have {pos1 pos2 Hyp Hsupp' S' HcastS HS'in Hpos1 Hpos2} [Q [Hcover HsuppQ]] + := SetContainingBothLeft.exists_Qy Hyp Hsupp' HS'in Hpos1 Hpos2. exists Q; apply/andP; split; last exact HsuppQ. by rewrite Hcover -HcastP -size_cover_inj //=; exact: cast_ord_inj. - rewrite negb_exists => /forallP Hall. @@ -1616,7 +1615,8 @@ rewrite -Greene_row_tab; last exact: is_tableau_RS. by apply: Greene_row_invar_plactic; exact: congr_RS. Qed. -Corollary plactic_shapeRS_row_proof u v : u =Pl v -> shape (RS u) = shape (RS v). +Corollary plactic_shapeRS_row_proof u v : + u =Pl v -> shape (RS u) = shape (RS v). Proof using. move=> Hpl. suff HeqRS k : Greene_row (to_word (RS u)) k = Greene_row (to_word (RS v)) k diff --git a/theories/LRrule/freeSchur.v b/theories/LRrule/freeSchur.v index b10b317..6ebe242 100644 --- a/theories/LRrule/freeSchur.v +++ b/theories/LRrule/freeSchur.v @@ -182,7 +182,7 @@ Qed. End TableauReading. -(** * Free Schur function : lifting Schur function is the free algebra *) +(** * Free Schur functions : lifting Schur functions in the free algebra *) Section FreeSchur. Variable R : comRingType. @@ -453,7 +453,7 @@ by rewrite size_rcons IHw. Qed. -(** ** Invariance with respect to choice of the Q-Tableau *) +(** ** Invariance with respect to the choice of the Q-Tableau *) Section Bij_LRsupport. Section ChangeUT. diff --git a/theories/LRrule/plactic.v b/theories/LRrule/plactic.v index ad17476..b7d6968 100644 --- a/theories/LRrule/plactic.v +++ b/theories/LRrule/plactic.v @@ -15,6 +15,8 @@ (******************************************************************************) (** * The plactic monoid +Knuth rewriting rules: + - [plact1] == rewriting rule acb -> cab if a <= b < c - [plact1i] == rewriting rule cab -> acb if a <= b < c - [plact2] == rewriting rule bac -> bca if a < b <= c