Skip to content

Commit 2d1c4e3

Browse files
hiverthivert
committed
Better handling of Ordtype display
1 parent dc8ad37 commit 2d1c4e3

13 files changed

Lines changed: 70 additions & 64 deletions

File tree

‎theories/Basic/ordtype.v‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -83,7 +83,7 @@ Definition covers {disp} {T : finPOrderType disp} :=
8383

8484
Section CoversFinPOrder.
8585

86-
Variable (disp : _) (T : finPOrderType disp).
86+
Context disp (T : finPOrderType disp).
8787
Implicit Type (x y : T).
8888

8989
Lemma coversP x y : reflect (x < y /\ (forall z, ~(x < z < y))) (covers x y).
@@ -263,7 +263,7 @@ End Dual.
263263
(** *** Maximum of a sequence *)
264264
Section MaxSeq.
265265

266-
Variables (disp : _) (T : orderType disp).
266+
Context disp (T : orderType disp).
267267
Implicit Type a b c : T.
268268
Implicit Type u v : seq T.
269269

@@ -299,7 +299,7 @@ End MaxSeq.
299299
(** *** Comparison of the elements of a sequence to an element *)
300300
Section AllLeqLtn.
301301

302-
Variables (disp : _) (T : orderType disp).
302+
Context disp (T : orderType disp).
303303
Implicit Type a b c : T.
304304
Implicit Type u v : seq T.
305305

@@ -452,7 +452,7 @@ End AllLeqLtn.
452452
(** *** Removing the largest letter of a sequence *)
453453
Section RemoveBig.
454454

455-
Variables (disp : _) (T : orderType disp).
455+
Context disp (T : orderType disp).
456456
Variable Z : T.
457457
Implicit Type a b c : T.
458458
Implicit Type u v w r : seq T.

‎theories/Basic/unitriginv.v‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@ Import GRing.Theory.
4848
Section UniTriangular.
4949

5050
Variable R : comUnitRingType.
51-
Variables (disp : _) (T : finPOrderType disp).
51+
Context disp (T : finPOrderType disp).
5252
Implicit Type M : T -> T -> R.
5353
Implicit Types t u v : T.
5454

@@ -150,8 +150,7 @@ End UniTriangular.
150150

151151
Section TriangularInv.
152152

153-
Variable R : comUnitRingType.
154-
Variable (disp : _) (T : finPOrderType disp).
153+
Context (R : comUnitRingType) disp (T : finPOrderType disp).
155154
Variable M : T -> T -> R.
156155
Implicit Types t u v : T.
157156

‎theories/Combi/skewtab.v‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -134,7 +134,7 @@ Qed.
134134
(** ** Skew tableaux *)
135135
Section Dominate.
136136

137-
Variables (disp : _) (T : inhOrderType disp).
137+
Context disp (T : inhOrderType disp).
138138
Implicit Type u v : seq T.
139139

140140
Definition skew_dominate sh u v := dominate (drop sh u) v.
@@ -375,7 +375,7 @@ End Dominate.
375375
(** ** Skewing and joining tableaux *)
376376
Section FilterLeqGeq.
377377

378-
Variables (disp : _) (T : inhOrderType disp).
378+
Context disp (T : inhOrderType disp).
379379
Implicit Type l : T.
380380
Implicit Type r w : seq T.
381381
Implicit Type t : seq (seq T).

‎theories/Combi/std.v‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -238,7 +238,7 @@ End StdCombClass.
238238
(** * Standardisation of a word over a totally ordered alphabet *)
239239
Section Standardisation.
240240

241-
Context {disp : _} {Alph : orderType disp}.
241+
Context {disp} {Alph : orderType disp}.
242242
Implicit Type s u v w : seq Alph.
243243

244244
Fixpoint std_rec n s :=
@@ -359,7 +359,7 @@ Definition eq_inv d1 d2 (T1 : inhOrderType d1) (T2 : inhOrderType d2)
359359
(w1 : seq T1) (w2 : seq T2) :=
360360
(versions w1) =2 (versions w2).
361361

362-
Variables (disp1 disp2 disp3 : _)
362+
Context disp1 disp2 disp3
363363
(S : inhOrderType disp1)
364364
(T : inhOrderType disp2)
365365
(U : inhOrderType disp3).
@@ -401,7 +401,7 @@ Qed.
401401

402402
Section EqInvAltDef.
403403

404-
Variables (disp1 disp2 disp3 : _)
404+
Context disp1 disp2 disp3
405405
(S : inhOrderType disp1)
406406
(T : inhOrderType disp2)
407407
(U : inhOrderType disp3).
@@ -479,7 +479,7 @@ Qed.
479479

480480
Section EqInvPosRemBig.
481481

482-
Variables (disp1 disp2 : _) (S : inhOrderType disp1) (T : inhOrderType disp2).
482+
Context disp1 disp2 (S : inhOrderType disp1) (T : inhOrderType disp2).
483483

484484
Lemma eq_inv_posbig (u : seq S) (v : seq T) :
485485
eq_inv u v -> posbig u = posbig v.
@@ -601,7 +601,7 @@ End EqInvPosRemBig.
601601

602602
Section Spec.
603603

604-
Variables (disp1 disp2 : _) (S : inhOrderType disp1) (T : inhOrderType disp2).
604+
Context disp1 disp2 (S : inhOrderType disp1) (T : inhOrderType disp2).
605605

606606
Variant std_spec (s : seq T) (p : seq nat) : Prop :=
607607
| StdSpec : is_std p -> eq_inv s p -> std_spec s p.
@@ -672,7 +672,7 @@ End Spec.
672672

673673
Section StdTakeDrop.
674674

675-
Variables (disp1 disp2 : _) (S : inhOrderType disp1) (T : inhOrderType disp2).
675+
Context disp1 disp2 (S : inhOrderType disp1) (T : inhOrderType disp2).
676676
Implicit Type u v : seq T.
677677

678678
Lemma std_take_std u v : std (take (size u) (std (u ++ v))) = std u.
@@ -700,7 +700,7 @@ End StdTakeDrop.
700700

701701
Section PermEq.
702702

703-
Variable (disp : _) (Alph : orderType disp).
703+
Context disp (Alph : orderType disp).
704704
Implicit Type u v : seq Alph.
705705

706706
Theorem perm_stdE u v : perm_eq u v -> std u = std v -> u = v.
@@ -729,7 +729,7 @@ End PermEq.
729729
(** ** Standardization and elementary transpositions of a word *)
730730
Section Transp.
731731

732-
Variable (disp : _) (Alph : inhOrderType disp).
732+
Context disp (Alph : inhOrderType disp).
733733
Implicit Type u v : seq Alph.
734734

735735
Lemma nth_transp u v a b i :

‎theories/Combi/stdtab.v‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -96,7 +96,7 @@ Import Order.Theory.
9696
(** ** Appending on the n-th row *)
9797
Section AppendNth.
9898

99-
Variables (disp : _) (T : inhOrderType disp).
99+
Context disp (T : inhOrderType disp).
100100
Implicit Type b : T.
101101
Implicit Type t : seq (seq T).
102102

@@ -599,7 +599,7 @@ Qed.
599599
End Bijection.
600600

601601

602-
Lemma eq_inv_is_row (d1 d2 : _) (T1 : inhOrderType d1) (T2 : inhOrderType d2)
602+
Lemma eq_inv_is_row d1 d2 (T1 : inhOrderType d1) (T2 : inhOrderType d2)
603603
(u1 : seq T1) (u2 : seq T2) :
604604
eq_inv u1 u2 -> is_row u1 -> is_row u2.
605605
Proof.
@@ -609,7 +609,7 @@ rewrite -(Hinv i j Hij).
609609
exact: Hrow.
610610
Qed.
611611

612-
Lemma is_row_stdE (d : _) (T : inhOrderType d) (w : seq T) :
612+
Lemma is_row_stdE d (T : inhOrderType d) (w : seq T) :
613613
is_row (std w) = is_row w.
614614
Proof.
615615
by apply/idP/idP; apply eq_inv_is_row; first apply eq_inv_sym; apply: eq_inv_std.

‎theories/Combi/tableau.v‎

Lines changed: 6 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -58,7 +58,7 @@ Import Order.Theory.
5858
(** ** Specialization of sorted Lemmas *)
5959
Section Rows.
6060

61-
Variables (disp : _) (T : inhOrderType disp).
61+
Context disp (T : inhOrderType disp).
6262

6363
Implicit Type l : T.
6464
Implicit Type r : seq T.
@@ -92,7 +92,7 @@ Notation is_row := (sorted <=%O).
9292
(** ** Dominance order for rows *)
9393
Section Dominate.
9494

95-
Context {disp : _} {T : inhOrderType disp}.
95+
Context {disp} {T : inhOrderType disp}.
9696

9797
Implicit Type l : T.
9898
Implicit Type r u v : seq T.
@@ -205,7 +205,7 @@ Arguments dominate_rev_trans {disp T}.
205205
(** * Tableaux : definition and basic properties *)
206206
Section Tableau.
207207

208-
Variables (disp : _) (T : inhOrderType disp).
208+
Context disp (T : inhOrderType disp).
209209

210210
Implicit Type l : T.
211211
Implicit Type r w : seq T.
@@ -522,7 +522,7 @@ Prenex Implicits is_tableau to_word size_tab.
522522
(** ** Tableaux from their row reading *)
523523
Section TableauReading.
524524

525-
Variables (disp : _) (A : inhOrderType disp).
525+
Context disp (A : inhOrderType disp).
526526

527527
Definition tabsh_reading (sh : seq nat) (w : seq A) :=
528528
(size w == sumn sh) && (is_tableau (rev (reshape (rev sh) w))).
@@ -550,7 +550,7 @@ End TableauReading.
550550
(** ** Sigma type for tableaux *)
551551
Section FinType.
552552

553-
Context {disp : _} {T : inhFinOrderType disp}.
553+
Context {disp} {T : inhFinOrderType disp}.
554554
Variables (d : nat) (sh : 'P_d).
555555

556556
Definition is_tab_of_shape (sh : seq nat) :=
@@ -704,9 +704,7 @@ End OrdTableau.
704704
(** ** Tableaux and increasing maps *)
705705
Section IncrMap.
706706

707-
Context (disp1 disp2 : _)
708-
(T1 : inhOrderType disp1)
709-
(T2 : inhOrderType disp2).
707+
Context disp1 disp2 (T1 : inhOrderType disp1) (T2 : inhOrderType disp2).
710708
Variable F : T1 -> T2.
711709

712710
Lemma shape_map_tab (t : seq (seq T1)) :

‎theories/LRrule/Greene.v‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -896,7 +896,7 @@ End Rev.
896896
(** * Greene number for tableaux *)
897897
Section GreeneRec.
898898

899-
Context {disp : _} {Alph : inhOrderType disp}.
899+
Context {disp} {Alph : inhOrderType disp}.
900900
Implicit Type u v w : seq Alph.
901901
Implicit Type t : seq (seq Alph).
902902

@@ -1529,7 +1529,7 @@ End GreeneRec.
15291529
(** ** Greene numbers of a tableau *)
15301530
Section GreeneTab.
15311531

1532-
Context {disp : _} {Alph : inhOrderType disp}.
1532+
Context {disp} {Alph : inhOrderType disp}.
15331533

15341534
Implicit Type t : seq (seq Alph).
15351535

‎theories/LRrule/Greene_inv.v‎

Lines changed: 27 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -140,7 +140,7 @@ Open Scope bool.
140140

141141
Section Duality.
142142

143-
Context {disp : _} {Alph : inhOrderType disp}.
143+
Context {disp} {Alph : inhOrderType disp}.
144144
Let word := seq Alph.
145145

146146
Lemma extract_cut (N : nat) (wt : N.-tuple Alph) (i : 'I_N) (S : {set 'I_N}) :
@@ -348,7 +348,7 @@ End Duality.
348348
Module Swap.
349349
Section Swap.
350350

351-
Context {disp : _} {Alph : inhOrderType disp}.
351+
Context {disp} {Alph : inhOrderType disp}.
352352
Let word := seq Alph.
353353

354354
Implicit Type a b c : Alph.
@@ -486,7 +486,7 @@ Module NoSetContainingBoth.
486486

487487
Section Case.
488488

489-
Context {disp : _} {Alph : inhOrderType disp}.
489+
Context {disp} {Alph : inhOrderType disp}.
490490
Let word := seq Alph.
491491

492492
Implicit Type a b c : Alph.
@@ -645,7 +645,7 @@ Module SetContainingBothLeft.
645645
(** *** Generic order hypothesis *)
646646
Section RelHypothesis.
647647

648-
Context {disp : _} {Alph : inhOrderType disp}.
648+
Context {disp} {Alph : inhOrderType disp}.
649649
Implicit Type a b c : Alph.
650650

651651
Record hypRabc R a b c := HypRabc {
@@ -683,7 +683,7 @@ End RelHypothesis.
683683

684684
Section Case.
685685

686-
Context {disp : _} {Alph : inhOrderType disp}.
686+
Context {disp} {Alph : inhOrderType disp}.
687687
Let word := seq Alph.
688688

689689
Implicit Type u v w r : word.
@@ -1287,7 +1287,7 @@ End SetContainingBothLeft.
12871287
(** * Greene numbers are invariant by each plactic rules *)
12881288
Section GreeneInvariantsRule.
12891289

1290-
Context {disp : _} {Alph : inhOrderType disp}.
1290+
Context {disp} {Alph : inhOrderType disp}.
12911291
Let word := seq Alph.
12921292

12931293
Variable u v1 w v2 : word.
@@ -1470,7 +1470,7 @@ End GreeneInvariantsRule.
14701470
(** ** Deducing the other comparisons by duality *)
14711471
Section GreeneInvariantsDual.
14721472

1473-
Context {disp : _} {Alph : inhOrderType disp}.
1473+
Context {disp} {Alph : inhOrderType disp}.
14741474
Let word := seq Alph.
14751475
Implicit Type u v w : word.
14761476

@@ -1590,7 +1590,7 @@ End GreeneInvariantsDual.
15901590
(** * Main theorem *)
15911591
Section GreeneInvariants.
15921592

1593-
Context {disp : _} {Alph : inhOrderType disp}.
1593+
Context {disp} {Alph : inhOrderType disp}.
15941594
Let word := seq Alph.
15951595

15961596
Implicit Type a b c : Alph.
@@ -1691,10 +1691,13 @@ Qed.
16911691

16921692
End GreeneInvariants.
16931693

1694-
Corollary Greene_row_eq_shape_RS
1695-
d1 d2 (S : inhOrderType d1) (T : inhOrderType d2)
1696-
(s : seq S) (t : seq T) :
1697-
(forall k, Greene_row s k = Greene_row t k) -> (shape (RS s) = shape (RS t)).
1694+
1695+
Section GreenEqShape.
1696+
1697+
Context d1 d2 (S : inhOrderType d1) (T : inhOrderType d2).
1698+
1699+
Corollary Greene_row_eq_shape_RS (s : seq S) (t : seq T) :
1700+
(forall k, Greene_row s k = Greene_row t k) -> shape (RS s) = shape (RS t).
16981701
Proof.
16991702
move=> HGreene; apply: Greene_row_tab_eq_shape; try apply: is_tableau_RS.
17001703
move=> k.
@@ -1703,10 +1706,8 @@ rewrite -(Greene_row_invar_plactic (u := t)); last exact: congr_RS.
17031706
exact: HGreene.
17041707
Qed.
17051708

1706-
Corollary Greene_col_eq_shape_RS
1707-
d1 d2 (S : inhOrderType d1) (T : inhOrderType d2)
1708-
(s : seq S) (t : seq T) :
1709-
(forall k, Greene_col s k = Greene_col t k) -> (shape (RS s) = shape (RS t)).
1709+
Corollary Greene_col_eq_shape_RS (s : seq S) (t : seq T) :
1710+
(forall k, Greene_col s k = Greene_col t k) -> shape (RS s) = shape (RS t).
17101711
Proof.
17111712
move=> HGreene; apply: Greene_col_tab_eq_shape; try apply: is_tableau_RS.
17121713
move=> k.
@@ -1715,13 +1716,21 @@ rewrite -(Greene_col_invar_plactic (u := t)); last exact: congr_RS.
17151716
exact: HGreene.
17161717
Qed.
17171718

1719+
End GreenEqShape.
1720+
17181721

1719-
(** ** Reverting uniq words *)
1722+
(** ** Reverting words *)
17201723
Section RevConj.
17211724

1722-
Context {disp : _} {Alph : inhOrderType disp}.
1725+
Context d {Alph : inhOrderType d}.
17231726
Implicit Type s : seq Alph.
17241727

1728+
Corollary shape_RS_revdual s : shape (RS (revdual s)) = shape (RS s).
1729+
Proof.
1730+
apply: Greene_row_eq_shape_RS => k.
1731+
by rewrite -Greene_row_dual.
1732+
Qed.
1733+
17251734
Theorem RS_rev_uniq s : uniq s -> RS (rev s) = conj_tab (RS s).
17261735
Proof using.
17271736
move Hsz : (size s) => n.

‎theories/LRrule/Schensted.v‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -137,7 +137,7 @@ Import Order.Theory.
137137

138138
Section NonEmpty.
139139

140-
Variables (disp : _) (T : inhOrderType disp).
140+
Context disp (T : inhOrderType disp).
141141
(** * Schensted's algorithm *)
142142

143143
(** ** Row insertion *)
@@ -1390,7 +1390,7 @@ by apply/idP/idP => Hstd; apply: (perm_std Hstd);
13901390
Qed.
13911391

13921392
Section QTableau.
1393-
Variables (disp : _) (T : inhOrderType disp).
1393+
Context disp (T : inhOrderType disp).
13941394

13951395
Notation TabPair := (seq (seq T) * seq (seq nat) : Type).
13961396

0 commit comments

Comments
 (0)