proposition: Lemma bisimul_instab t l b lb : is_tableau t -> (l < b)%O -> (forall row, row \in t -> is_row (rcons row b)) -> (forall j : nat, j < lb -> (last b (nth [::] t j) < b)%O) -> let tres := (append_nth t b lb) in instab tres l = append_nth (instab t l) b (last_big (instab tres l) b).
proof: Proof. Proof using. elim: t l lb => [/= l lb _| t0 t IHt l lb Htab] Hl Hallrow. - case: lb => [_ /=| lb Hj]; first by rewrite Hl /= (lt_eqF Hl) eq_refl. by exfalso; move/(_ 0 (ltn0Sn _)): Hj; rewrite /= ltxx. - move: Htab => /= /and4P[Hnnil Hrow0 _ Htab]. case: lb => [/= _ {IHt Htab} | lb Hj /=]. + have Hrow: is_row (rcons t0 b) by apply: Hallrow; rewrite inE eq_refl. case: (boolP (bump t0 l)) => [Hbump | Hnbump]. * have:= bump_bumprow_rconsE Hrow Hl Hbump. rewrite (bump_bumprowE Hrow0 Hbump) => ->. by rewrite /= last_rcons eq_refl. * have:= nbump_bumprow_rconsE Hrow Hl Hnbump. rewrite (nbump_bumprowE Hrow0 Hnbump) (nbump_ins_rconsE Hrow0 Hnbump) => ->. rewrite /= last_rcons (lt_eqF Hl) /= {Hrow0 Hrow Hnbump}. case: t Hallrow => [/= _ | t1 t Hallrow /=]; first by rewrite eq_refl. have : t1 \in [:: t0, t1 & t] by rewrite !inE eq_refl orbT. move/Hallrow/bumprow_rcons => -> /=. by rewrite last_rcons eq_refl. + have Hlast0:= Hj 0 (ltn0Sn _); rewrite /= in Hlast0. have {}Hj j : j < lb -> (last b (nth [::] t j) < b)%O by apply/(Hj j.+1). case: (boolP (bump t0 l)) => [Hbump | Hnbump]. * rewrite (bump_bumprowE Hrow0 Hbump) /=. have Hbumped := bumped_lt Hrow0 Hl Hlast0. rewrite (lt_eqF (last_ins_lt Hl Hlast0)). have {}Hallrow row : row \in t -> is_row (rcons row b). by move=> Hrow; apply: Hallrow; rewrite inE Hrow orbT. by rewrite /= {1}(IHt _ _ Htab Hbumped Hallrow Hj). * rewrite (nbump_bumprowE Hrow0 Hnbump) /=. by rewrite (lt_eqF (last_ins_lt Hl Hlast0)) /= (last_big_append_nth Hj). Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr