proposition: Lemma gdist_geq (n : nat) (p1 p2 : peg 4) : p1 != p2 -> ϕ(n) <= `d[`c[p1, n], `c[p2, n]]_rmove.
proof: Proof. case: n => // n p1Dp2. have /gpath_connect [g gHp1p2] := connect_move `c[p1, n.+1] `c[p2, n.+1]. have p2Ig : `c[p2] \in g. have := mem_last `c[p1] g. by rewrite inE (gpath_last gHp1p2) eq_sym perfect_eqE (negPf p1Dp2). pose N : disk n.+1 := ldisk. have cH : codom `c[p2, n.+1] \subset [:: p2]. by apply/subsetP=> i /codomP[j]; rewrite inE ffunE => ->. case (@split_first _ g (fun c : configuration _ _ => c(N) != p1)) => /=. apply/negP=> /allP /(_ _ p2Ig); rewrite /= -topredE negbK. have /subsetP/(_ (`c[p2] N))/(_ (codom_f _ _)) := cH. by rewrite !inE !ffunE eq_sym (negPf p1Dp2). move=> [[z0s z0sb] z0sa] /= [/allP z0sbP0 z0sND0 gE']. pose z0 := last `c[p1] z0sb. have z0N1 : z0 N = p1. have := mem_last `c[p1] z0sb; rewrite !inE /z0 => /orP[/eqP->|/z0sbP0]. by rewrite ffunE. by rewrite !inE negbK => /eqP. have z0NDz0sN : z0 N != z0s N by rewrite z0N1 eq_sym. have z0Mz0s : z0 `-->_r z0s. by move: (gpath_path gHp1p2); rewrite gE' cat_path /= => /and3P[]. move: (gHp1p2); rewrite gE' => /gpath_catl; rewrite -/z0 => gHp1z0. move: (gHp1p2); rewrite gE' => /gpath_catr; rewrite -/z0 => gHz0p2. move: (gHp1p2); rewrite gE' => /gdist_cat; rewrite -/z0 => dp1p2E. case (@split_last _ (z0 :: z0s :: z0sa) (fun c : configuration _ _ => c N != p2)). have z0Iz0sz0sa : z0 \in z0 :: z0s :: z0sa by rewrite inE eqxx. apply/negP=> /allP /(_ _ z0Iz0sz0sa); rewrite /= -topredE negbK. by rewrite z0N1 (negPf p1Dp2). move=> [[z2p z2b] [|z2 z2a]] /= [z2pN2 z2aEp2 z0sz0saE]. have : last z0 (z0s :: z0sa) = z2p. by rewrite -[last _ _]/(last z0 (z0 :: z0s :: z0sa)) z0sz0saE last_cat. move: (gpath_last gHp1p2); rewrite gE' last_cat /= => -> p2Ez2p. by case/eqP: z2pN2; rewrite -p2Ez2p ffunE. have {}z2aEp2 c : c \in z2 :: z2a -> c N = p2. case/andP: z2aEp2; rewrite -topredE negbK => /eqP z2NEp2 /allP H. by rewrite inE => /orP[/eqP-> //|/H/=]; rewrite -topredE negbK => /eqP. have z0Ez2p : z2b = [::] -> z0 = z2p by case: z2b z0sz0saE => [[]|]. have {}z0sz0saE : z0s :: z0sa = (rcons (behead (rcons z2b z2p)) z2) ++ z2a. case: (z2b) z0sz0saE => [[_ -> ->]|zz ll [_ ->]] //=. by rewrite !cat_rcons. move: (gHz0p2); rewrite z0sz0saE => /gpath_catl; rewrite last_rcons => gHz0z2. move: (gHz0p2); rewrite z0sz0saE => /gpath_catr; rewrite last_rcons => gHz2p2. move: (gHz0p2); rewrite z0sz0saE => /gdist_cat; rewrite last_rcons => dz0p2E. have z2Ig : z2 \in g. by rewrite gE' z0sz0saE !(inE, mem_cat, mem_rcons, eqxx, orbT). have z2N2 : z2 N = p2 by apply: z2aEp2; rewrite inE eqxx. have z2pNDz2N : z2p N != z2 N by rewrite z2N2. have z2pMz2 : z2p `-->_r z2. move: gHz0z2; case: (z2b) z0Ez2p => [->// /gpath_path/andP[] |a l _] //=. by rewrite -cats1 => /gpath_catr; rewrite last_rcons => /gpath_path/andP[]. have dp1z0_leq : psi `[N] <= `d[`c[p1], z0]_rmove. have -> : `[N] = s2f [set i | ↓[`c[p1, n.+1]] i == p1]. apply/fsetP => i; rewrite mem_sint. apply/idP/imfsetP; last by move=> /= [j]; rewrite inE !ffunE // => _ ->. by move=> /= iLN; exists (Ordinal iLN);rewrite //= inE !ffunE. apply: leq_trans (gdist_cunlift _); last by apply: connect_move. have /peg4comp2[pp1 [pp2 [[pp2Dpp1 pp2Dpz0sN pp2Dz0N] [pp1Dz0sN pp1Dz0N] Hz]]] := z0NDz0sN. have cH1 : codom ↓[z0] \subset [:: pp1; pp2]. apply/subsetP => i /codomP[j ->]; rewrite !inE ffunE. case: (Hz (z0 (trshift 1 j))); try by move->; rewrite ?(eqxx, orbT). move=> /eqP; rewrite -[_ == z0 N]negbK; case/negP. by apply: (move_on_toplDl z0Mz0s) => /=. move=> /eqP; rewrite -[_ == z0s N]negbK; case/negP. by apply: (move_on_toplDr z0Mz0s); rewrite //= ltnW. by apply: gdist_le_psi cH1; split => //; rewrite -z0N1. have dp2z2_leq : psi `[N] <= `d[`c[p2], z2]_rmove. have -> : `[N] = s2f [set i | ↓[`c[p2, n.+1]] i == p2]. apply/fsetP => i; rewrite mem_sint. apply/idP/imfsetP; last by move=> /= [j]; rewrite inE !ffunE // => _ ->. by move=> /= iLN; exists (Ordinal iLN);rewrite //= inE !ffunE. apply: leq_trans (gdist_cunlift _); last by apply: connect_move. have /peg4comp2[pp1 [pp2 [[pp2Dpp1 pp2Dpz2sN pp2Dz2N] [pp1Dz2sN pp1Dz2N] Hz]]] := z2pNDz2N. have cH1 : codom ↓[z2] \subset [:: pp1; pp2]. apply/subsetP => i /codomP[j ->]; rewrite !inE ffunE. case: (Hz (z2 (trshift 1 j))); try by move->; rewrite ?(eqxx, orbT). move=> /eqP; rewrite -[_ == z2p N]negbK; case/negP. by apply: (move_on_toprDl z2pMz2) => //=; rewrite ltnW. move=> /eqP; rewrite -[_ == z2 N]negbK; case/negP. by apply: (move_on_toprDr z2pMz2); rewrite /=. by apply: gdist_le_psi cH1; split => //; rewrite -z2N2. rewrite dp1p2E; apply: leq_trans (leq_add dp1z0_leq (leqnn _)). rewrite dz0p2E [gdist _ z2 _]gdistC ?addnA; last by apply/move_sym/rsym. apply: leq_trans (leq_add (leqnn _) dp2z2_leq). rewrite addnAC addnn psi_sint_phi addnC. move: (gdist_gt0 rmove z0 z2). have -> : z0 != z2. by apply/eqP => /ffunP/(_ ldisk) /eqP; rewrite z0N1 z2N2 (negPf p1Dp2). move/idP; case: gdist => // k _. by rewrite addSnnS prednK // leq_addl. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist ghanoi ghanoi4 triangular phi rhanoi3 psi)