proposition: Lemma val2pos_enum (p : {set 'I_(size s)}) : sorted <=%O [seq tnth (in_tuple s) i | i <- enum (mem p)] -> enum (mem [set val2pos x | x in p]) = [seq val2pos x | x <- enum p].
proof: Proof. Proof using. rewrite /enum_mem (eq_filter (a2 := mem p)) // -!enumT /= => H. apply: (inj_map val_inj). rewrite -map_comp (eq_map val2posE). rewrite (eq_filter (a2 := mem [set val2pos x | x in p])) //. move: H; rewrite (eq_map (g := fun i : 'I_(_) => nth (size t) s i)); first last. by move=> i /=; exact: tnth_nth. set l := (X in sorted _ X); rewrite -[RHS]/l. move=> H; apply: (sorted_eq (leT := leq)). - exact: leq_trans. - by move=> i j H1; apply/eqP; rewrite eqn_leq. - apply: (subseq_sorted leq_trans (s2 := map val (enum 'I_(size t)))). + by apply: map_subseq; exact: filter_subseq. + by rewrite val_enum_ord; exact: iota_sorted. - move: H; rewrite /sorted; case: l => [// | l0 l]. by rewrite (eq_path (e' := leq)); last by move=> i j /=; rewrite leEnat. - apply: uniq_perm. + rewrite map_inj_in_uniq. * by apply: filter_uniq; exact: enum_uniq. * by move=> i j Hi _ /=; exact: val_inj. + rewrite map_inj_in_uniq. * by apply: filter_uniq; exact: enum_uniq. * move=> i j Hij _ /= HH; apply: val_inj. have:= Hinvst => /linvseqP Heq. by rewrite /= -(Heq _ (ltn_ord i)) -(Heq _ (ltn_ord j)) HH. + rewrite {H}/l => i /=; apply/idP/idP => /mapP[j]. * rewrite mem_filter => /andP[/= /imsetP[i' Hi' -> _] ->{i}]. apply/mapP; exists i'; last by []. by rewrite mem_filter /= Hi' /=; rewrite mem_enum. * rewrite mem_filter => /andP[/= Hj _ ->{i}]. apply/mapP; exists (Ordinal (linvseq_ltn_szt Hinvst (ltn_ord j))); last by []. rewrite mem_filter; apply/andP; split => /=; last by rewrite mem_enum. by rewrite /val2pos; rewrite imset_f. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordcast partition Yamanouchi ordtype std tableau stdtab sorted Schensted congr plactic Greene Greene_inv