proposition: Lemma leq_shanoi4 p1 p2 n : p1 != p0 -> p2 != p0 -> p1 != p2 -> `d[`c[p1, n],`c[p2, n]]_smove <= (S_[1] n).*2.
proof: Proof. elim/ltn_ind : n p1 p2 => [] [|n] IH p1 p2 p1Dp0 p2Dp0 p1Dp2. rewrite alphaS_small double0. rewrite (_ : `c[p1] = `c[p2]) ?gdist0 //. by apply/ffunP=> [] []. rewrite S1E S1_bigmin -muln2 -bigminMr. apply/bigmin_leqP => i iLn. have iLn1 : i <= n.+1 by apply: leq_trans iLn _. rewrite -{-5}(subnK iLn1). rewrite eq_sym in p2Dp0. have [p3 [[p3Dp2 p3Dp0 p3Dp1] _]] := peg4comp3 p1Dp0 p1Dp2 p2Dp0. rewrite eq_sym in p2Dp0. pose p1n := `c[p1, n.+1 - i]. pose p2n := `c[p2, n.+1 - i]. pose p3n := `c[p3, n.+1 - i]. pose p1i := `c[p1, i]. pose p2i := `c[p2, i]. pose p3i := `c[p3, i]. pose c1 := cmerge p1n p1i. pose c2 := cmerge p1n p3i. pose c3 := cmerge p2n p3i. pose c4 := cmerge p2n p2i. have <- : c1 = `c[p1]. apply/ffunP => j; rewrite /c1 !ffunE. by case: tsplitP => k; rewrite !ffunE. have <- : c4 = `c[p2]. apply/ffunP => j; rewrite /c1 !ffunE. by case: tsplitP => k; rewrite !ffunE. apply: leq_trans (_ : _ <= `d[c1, c2]_smove + `d[c2, c3]_smove + `d[c3, c4]_smove) _. apply: leq_trans (leq_add (gdist_triangular _ _ _ _) (leqnn _)). apply: gdist_triangular. rewrite -addnn !mulnDl [X in _ <= X]addnAC !muln2. repeat apply: leq_add; first 2 last. - apply: leq_trans (gdist_merger _ _ _) _; first by apply: sirr. by apply: shanoi_connect. by rewrite -S1E; apply: IH. - apply: leq_trans (gdist_merger _ _ _) _; first by apply: sirr. by apply: shanoi_connect. by rewrite -S1E; apply: IH => //; rewrite eq_sym. rewrite div2K; last first. rewrite -subn1 oddB ?expn_gt0 // addbT. by rewrite oddX orbT. have -> : c2 = clmerge p1 p2 p3 _ `c[ord0]. apply/ffunP=> x; rewrite !ffunE. by case: tsplitP => // j; rewrite !ffunE /=. have -> : c3 = clmerge p1 p2 p3 _ `c[inord 2]. apply/ffunP=> x; rewrite !ffunE. by case: tsplitP => // j; rewrite !ffunE /= inordK. apply: leq_trans (gdist_clmerge _ _ _ _ _ _ _ _ _) _ => //; try by rewrite eq_sym. rewrite gdist_lhanoi3p /lrel /= inordK //=. case: eqP=> [/val_eqP/=|]; first by rewrite inordK. by rewrite muln1. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra star gdist lhanoi3 ghanoi ghanoi4 shanoi)