proposition: Lemma main p1 p2 p3 n l (u : {ffun 'I_l.+1 -> configuration 4 n}) : p1 != p2 -> p1 != p3 -> p2 != p3 -> p1 != p0 -> p2 != p0 -> p3 != p0 -> (forall k : 'I_l.+1, 0 < k < l -> codom (u k) \subset [:: p2; a[p1, p3] k]) -> (S_[l] n).*2 <= \sum_(i < l) `d[u (inord i), u (inord i.+1)]_smove + \sum_(k < n) (u ord0 k != p1) * β_[n, l] k + \sum_(k < n) (u ord_max k != a[p1, p3] l) * β_[n, l] k.
proof: Proof. elim: n l p1 p2 p3 u => [|[|n] IH] l p1 p2 p3 u p1Dp2 p1Dp3 p2Dp3 p1Dp0 p2Dp0 p3Dp0 cH. - by rewrite /dsum_alphaL /conv /= dsum_alpha_0 muln0. - rewrite /dsum_alphaL /conv /= dsum_alpha_1 dsum_alpha_0 muln0 addn0 add0n muln1. rewrite [X in _ <= _ + X + _]big_ord_recl big_ord0 /= addn0. rewrite [X in _ <= _ + X]big_ord_recl big_ord0 /= addn0. have d0fE (c1 c2 : configuration 4 1) : c1 != `c[p0] -> c2 != `c[p0] -> `d[c1, c2]_smove = (c1 != c2).*2. move=> c1Dp0 c2Dp0. case: (gpath_connect (shanoi_connect c1 c2)) => [] [/gpath_dist H |a [|b p]]. - by rewrite H; move/eqP: H; rewrite gdist_eq0 => ->. - case/gpathP; rewrite /= andbT => /moveP[z]. rewrite [z]disk1_all => [] [zH _ _ _] aE. case/andP: zH => _; rewrite aE. move: c1Dp0 c2Dp0; rewrite !configuration1_eq !Ival_eq /= !ffunE /=. by do 2 case: val. move=> /gpath_dist; case: eqP => [<-|/eqP c1Dc2]; first by rewrite gdist0. move=> H; apply/eqP; rewrite eqn_leq {2}H /= andbT. have pH : path smove c1 [::`c[p0]; c2]. rewrite /=; apply/and3P; split => //. apply/moveP; exists ord0; split => //=. - rewrite !ffunE; apply/andP; split; last by rewrite muln0. by move: c1Dp0; rewrite configuration1_eq ffunE. - by move=> i; rewrite [i]disk1_all. - by apply/on_topP => j; rewrite [j]disk1_all. by apply/on_topP => j; rewrite [j]disk1_all. apply/moveP; exists ord0; split => //=. - rewrite !ffunE; apply/andP; split=> //. by move: c2Dp0; rewrite configuration1_eq ffunE eq_sym. - by move=> i; rewrite [i]disk1_all. - by apply/on_topP => j; rewrite [j]disk1_all. by apply/on_topP => j; rewrite [j]disk1_all. rewrite -[1.*2]/(size [:: `c[p0]; c2]). by apply: gdist_path_le pH _. case: l u cH => [|l] u cH; first by rewrite (minn_idPr _). case: l u cH => [|l] u cH. rewrite (minn_idPr _) //. rewrite big_ord_recl big_ord0 addn0. rewrite inord_eq0 // (_ : inord 1 = ord_max); last first. by apply/val_eqP; rewrite /= inordK. rewrite /beta !(apegS, apeg0) /= alphaL1E -[_ 0]/1; do 2 case: eqP; rewrite /= ?addn0; try by move=> *; rewrite leq_addl. move=> u1E u0E. rewrite d0fE //. - by rewrite configuration1_eq u1E u0E p1Dp3. - by rewrite configuration1_eq ffunE u0E. by rewrite configuration1_eq ffunE u1E. rewrite (minn_idPl _) // -[_.*2]/4. rewrite big_ord_recl big_ord_recr /=. rewrite -!addnA addnC -!addnA (leq_trans _ (leq_addl _ _)) //. rewrite !apegS /beta /= alphaL_0 (minn_idPl _) /bump /= ?add1n //. rewrite addnCA addnC !addnA -addnA -[4]/(2 + 2). apply: leq_add. case: eqP => /= [umE|umD]; last by rewrite leq_addl. rewrite addn0 d0fE. - case: eqP => // H. have /cH : 0 < (inord l.+1 : 'I_l.+3) < l.+2 by rewrite inordK /=. move=> /subsetP/(_ _ (codom_f _ sdisk)). rewrite H (_ : inord l.+2 = ord_max). rewrite umE inordK // apegS //= !inE. rewrite (apeg_eqC _ _ _) // (negPf (apeg_neq _ _ _)) //=. by rewrite (negPf p1Dp3). by rewrite eq_sym. by apply/val_eqP; rewrite /= inordK. - rewrite configuration1_eq ffunE. case: (_ =P _) => // H. have /cH : 0 < (inord l.+1 : 'I_l.+3) < l.+2 by rewrite inordK /=. move=> /subsetP/(_ _ (codom_f _ sdisk)). by rewrite H !inE eq_sym (negPf p2Dp0) /= eq_sym (negPf (apeg_neq _ _ _)). rewrite configuration1_eq ffunE. rewrite (_ : inord l.+2 = ord_max). by rewrite umE apeg_neq. by apply/val_eqP; rewrite /= inordK. case: eqP => /= [u0E|u0D]; last by rewrite leq_addl. rewrite addn0 d0fE. - case: eqP => // H. have /cH : 0 < (inord 1 : 'I_l.+3) < l.+2 by rewrite inordK /=. move=> /subsetP/(_ _ (codom_f _ sdisk)). rewrite -H inord_eq0 // u0E inordK //= !(apegS, apeg0). by rewrite !inE (negPf p1Dp2) (negPf p1Dp3). - by rewrite configuration1_eq ffunE inord_eq0 // u0E. rewrite configuration1_eq ffunE. case: eqP => // H. have /cH : 0 < (inord 1 : 'I_l.+3) < l.+2 by rewrite inordK /=. move=> /subsetP/(_ _ (codom_f _ sdisk)). by rewrite H !inE eq_sym (negPf p2Dp0) /= eq_sym (negPf (apeg_neq _ _ _)). case: l u cH => [|l] u cH; first by rewrite S0E. rewrite apegS. pose u' : {ffun 'I_l.+2 -> configuration 4 n.+1} := [ffun i : 'I_l.+2 => ↓[u i]]. have H (k : 'I_l.+2) : 0 < k < l.+1 -> codom (u' k) \subset [:: p2; a[p1, p3] k]. by move=> k1; rewrite ffunE; apply/codom_liftr/cH. pose K := (u ord0 ord_max != p1) + (u ord_max ord_max != a[p3, p1] l). have [HK|] := boolP ((K == 2) || ((K == 1) && (l == 0))). rewrite dsum_alphaL_S doubleD. have IH' := IH _ p1 p2 p3 u' p1Dp2 p1Dp3 p2Dp3 p1Dp0 p2Dp0 p3Dp0 H. rewrite apegS in IH'. rewrite ![\sum_(_ < _.+2) _]big_ord_recr /=. set u1 := \sum_ (_ < _) _; set u2 := \sum_ (_ < _) _; set u3 := \sum_ (_ < _) _. rewrite -!addnA [_ + (u3 + _)]addnCA 2!addnA. apply: leq_add. apply: leq_trans IH' _. apply: leq_add; last first. apply: leq_sum => i _. apply: leq_mul. rewrite leq_eqVlt; apply/orP; left; apply/eqP. by rewrite !ffunE; congr (u _ _ != _); apply/val_eqP. rewrite {2}/beta eqn_leq [_ <= i]leqNgt ltn_ord !andbF /=. apply: geq_beta. apply: leq_add; last first. apply: leq_sum => i _. apply: leq_mul. rewrite leq_eqVlt; apply/orP; left; apply/eqP. by rewrite !ffunE; congr (u _ _ != _); apply/val_eqP. rewrite {2}/beta eqn_leq [_ <= i]leqNgt ltn_ord !andbF /=. apply: geq_beta. apply: leq_sum => i _. rewrite !ffunE. by apply/gdist_cunlift/shanoi_connect. rewrite -mulnDl -/K. case/orP: HK => [/eqP->|/andP[/eqP-> /eqP->]]. by rewrite mul2n leq_double leq_beta. by rewrite mul1n /beta /= /alphaL /delta !S1E. rewrite negb_or negb_and. have: K <= 2 by rewrite /K; do 2 case: (_ != _). case: ltngtP; rewrite // ltnS. case: ltngtP => //= KE _ _ l_gt0; last first. move: KE; rewrite /K. (case: eqP => [KH1|/eqP KH1] /=; case: eqP) => // [/eqP KH2|KH2] _. by apply: (@case1 _ IH) cH KH1 KH2 l_gt0. pose u1 : {ffun 'I_l.+2 -> configuration 4 n.+2} := [ffun i : 'I_l.+2 => u (inord (l.+1 - i))]. have -> : \sum_(i < l.+1) `d[u (inord i), u (inord i.+1)]_smove = \sum_(i < l.+1) `d[u1 (inord i), u1 (inord i.+1)]_smove. have F : injective (fun i : 'I_l.+1 => (inord (l - i) : 'I_l.+1)). move=> i j /val_eqP. have lBiLl (i1 : 'I_l.+1) : l - i1 < l.+1. by rewrite ltn_subLR ?leq_addl // -ltnS. rewrite /= !inordK // => /eqP liE; apply/val_eqP => /=. rewrite -(subKn (_ : i <= l)); last by rewrite -ltnS. by rewrite liE subKn // -ltnS. rewrite (reindex_inj F) /=. apply: eq_bigr => i _; rewrite !ffunE. have iLl2 : i < l.+2 by apply: leq_trans (ltn_ord _) _. have lBiLl : l - i < l.+1 by rewrite ltn_subLR ?leq_addl // -ltnS. have iLl : i <= l by rewrite -ltnS. rewrite gdistC; last by apply/move_sym/ssym. congr (`d[u _,u _]_smove). by apply/val_eqP; rewrite /= !inordK ?subSn. by apply/val_eqP; rewrite /= !inordK // ?subSS ltnS // ltnW. pose p1' := a[p3, p1] l. pose p3' := a[p1, p3] l. have -> : \sum_(k < n.+2) (u ord0 k != p1) * β_[n.+2, l.+1] k = \sum_(k < n.+2) (u1 ord_max k != a[p1', p3'] l.+1) * β_[n.+2, l.+1] k. apply: eq_bigr => i _; congr (_ * _). rewrite ffunE subnn. by rewrite inord_eq0 // -apegD addSn addnn apegS apeg_double. have -> : \sum_(k < n.+2) (u ord_max k != a[p3, p1] l) * β_[n.+2, l.+1] k = \sum_(k < n.+2) (u1 ord0 k != p1') * β_[n.+2, l.+1] k. apply: eq_bigr => i _; congr (_ * _). rewrite ffunE subn0. suff -> : inord l.+1 = ord_max :> 'I_l.+2 by []. by apply/val_eqP; rewrite /= inordK. have cH1 (k : 'I_l.+2) : 0 < k < l.+1 -> codom (u1 k) \subset [:: p2; a[p1', p3'] k]. move=> /andP[kH1 kH2]; rewrite ffunE. have F1 : k <= l.+1 by apply: ltnW. have F2 : l.+1 - k < l.+2. by rewrite ltn_subLR // addnS ltnS leq_addl. have -> : a[p1', p3'] k = a[p1, p3] (inord (l.+1 - k) : 'I_l.+2). rewrite -apegD inordK // [RHS]apegO oddB //. by rewrite -oddD -apegO addSn apegS addnC. apply: cH; rewrite inordK // subn_gt0 // ltn_subLR // kH2 //=. by rewrite addnS ltnS -{1}[l.+1]add1n leq_add2r. rewrite -addnA [X in _ <= _ + X]addnC addnA apegS. apply: (@case1 _ IH) cH1 _ _ _ => //. - by rewrite apeg_neq // eq_sym. - by rewrite apeg_eqC // eq_sym. - by rewrite eq_sym apeg_neq // eq_sym. - by rewrite apeg_neq // eq_sym. - by rewrite apeg_neq // eq_sym. - rewrite ffunE subn0. suff -> : inord l.+1 = ord_max :> 'I_l.+2 by []. by apply/val_eqP; rewrite /= inordK. by rewrite ffunE subnn inord_eq0 // -apegD addnn apeg_double. move: KE; rewrite /K; do 2 case: eqP => //=. move => uME u0E _. by apply: (case3 IH _ _ _ _ _ _ cH). Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra star gdist lhanoi3 ghanoi ghanoi4 shanoi)