From mathcomp Require Import all_ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Section Hanoi. Variable n : nat. (*****************************************************************************) (* The pegs are the three elements of 'I_3 *) (*****************************************************************************) Definition peg := 'I_3. Implicit Type p : peg. Definition peg1 : peg := ord0. Definition peg2 : peg := inord 1. Definition peg3 : peg := inord 2. Lemma pegE p : [\/ p = peg1, p = peg2 | p = peg3]. Proof. by case: p => [] [|[|[|]]] // H; [apply Or31|apply Or32|apply Or33]; apply/val_eqP; rewrite //= /peg2 inordK. Qed. (* Finding the free peg that differs from p1 and p2 *) Definition opeg p1 p2 : peg := inord (3 - (p1 + p2)). Lemma opeg_sym p1 p2 : opeg p1 p2 = opeg p2 p1. Proof. by rewrite /opeg addnC. Qed. Lemma opegDl p1 p2 : p1 != p2 -> opeg p1 p2 != p1. Proof. move=> /eqP/val_eqP /= p1Dp2. apply/eqP/val_eqP; rewrite /= /opeg inordK //; last first. case: (p1: nat) p1Dp2 => [|n1] //=. by case: (p2: nat) => //= n2 _; rewrite (leq_ltn_trans (leq_subr _ 2)). by rewrite (leq_ltn_trans (leq_subr _ 2)). by case: (p1 : nat) (p2 : nat) p1Dp2 (ltn_ord p1) (ltn_ord p2) => [|[|[|]]] // [|[|[|[|]]]]. Qed. Lemma opegDr p1 p2 : p1 != p2 -> opeg p1 p2 != p2. Proof. by rewrite eq_sym opeg_sym; exact: opegDl. Qed. Lemma opegE p p1 p2 : p1 != p2 -> (opeg p1 p2 == p) = ((p1 != p) && (p2 != p)). Proof. move=> /eqP/val_eqP /= p1Dp2. have F : 3 - (p1 + p2) < 3. case: (p1: nat) p1Dp2 => [|n1] //=. by case: (p2: nat) => //= n2 _; rewrite (leq_ltn_trans (leq_subr _ 2)). by rewrite (leq_ltn_trans (leq_subr _ 2)). apply/eqP/andP=> [/val_eqP /= H1|[/eqP/val_eqP/= H1 /eqP/val_eqP/= H2]]. by split; apply/eqP/val_eqP=> /=; move: H1; rewrite /opeg inordK //; case: (p: nat) (p1 : nat) (p2 : nat) p1Dp2 (ltn_ord p1) (ltn_ord p2) (ltn_ord p) => [|[|[|]]] // [|[|[|[|]]]] // [|[|[|[|]]]] //. apply/val_eqP=> /=. by move: H1 H2; rewrite /opeg inordK //; case: (p: nat) (p1 : nat) (p2 : nat) p1Dp2 (ltn_ord p1) (ltn_ord p2) (ltn_ord p) => [|[|[|]]] // [|[|[|[|]]]] // [|[|[|[|]]]] //. Qed. (*****************************************************************************) (* The disks are represented with the element of 'I_n with *) (* the idea that disk d1 is larger than disk d2 is d2 <= d1. *) (*****************************************************************************) Definition disk := 'I_n. Implicit Type d : disk. Definition mk_disk m (H : m < n) : disk := Ordinal H. (*****************************************************************************) (* Given a configuration c, the disks on the peg p can be reconstructed by *) (* the list in decreasing order of the disk d such that c d = p *) (*****************************************************************************) Definition configuration := {ffun disk -> peg}. Implicit Type c : configuration. (* A perfect configuration is one where all the pegs are on peg p *) Definition perfect p : configuration := [ffun d => p]. (* Build from the configuration c the weak perfect configuration where with respect to c, all the disks smaller than m are now on peg p. *) Definition mk_perfect m p c : configuration := [ffun d : disk => if d < m then p else c d]. Lemma mkd_perfect0 p c : mk_perfect n p c = perfect p. Proof. by apply/ffunP => i; rewrite !ffunE ltn_ord. Qed. Lemma mk_perfect_max m1 m2 p c : mk_perfect m1 p (mk_perfect m2 p c) = mk_perfect (maxn m1 m2) p c. Proof. by apply/ffunP=> d; rewrite !ffunE leq_max; case: leqP. Qed. Definition setd d p c : configuration := [ffun d1 : disk => if d1 == d then p else c d1]. (*****************************************************************************) (* A move is a relation between two configurations c1 c2: *) (* there must exists a disk d1, that is the only one that has changed of *) (* peg (c1 d1 != c2 d1) and that was the minimum of the peg (c1 d1) and *) (* is the minimum of the peg (c2 d1). *) (* The parameter m is here to restrict the range on which one can select the *) (* disk that has moved. *) (* This is done to accomodate inductive which is the key of the proof *) (*****************************************************************************) Definition move m : rel configuration := [rel c1 c2 | [exists d1 : 'I_n, [&& d1 < m, (c1 : configuration) d1 != c2 d1, [forall d2, (d1 != d2) ==> (c1 d2 == c2 d2)], [forall d2, (c1 d1 == c1 d2) ==> (d1 <= d2)] & [forall d2, (c2 d1 == c2 d2) ==> (d1 <= d2)]]]]. Lemma moveP m c1 c2 : reflect (exists d1, [/\ d1 < m, c1 d1 != c2 d1, forall d2, d1 != d2 -> c1 d2 = c2 d2, forall d2, c1 d1 = c1 d2 -> d1 <= d2 & forall d2, c2 d1 = c2 d2 -> d1 <= d2]) (move m c1 c2). Proof. apply: (iffP existsP) => [[d /and5P[H1 H2 /forallP H3 /forallP H4 /forallP H5]]|[d [H1 H2 H3 H4 H5]]]; exists d. split => // d1 H; first by apply/eqP/(implyP (H3 _)). by apply/(implyP (H4 _))/eqP. by apply/(implyP (H5 _))/eqP. by rewrite H1 H2 /=; apply/and3P; split; apply/forallP => d1; apply/implyP => H; rewrite ?H3 // ?(H4 _ (eqP H)) // (H5 _ (eqP H)). Qed. Lemma movenP c1 c2 : reflect (exists d1, [/\ c1 d1 != c2 d1, forall d2, d1 != d2 -> c1 d2 = c2 d2, forall d2, c1 d1 = c1 d2 -> d1 <= d2 & forall d2, c2 d1 = c2 d2 -> d1 <= d2]) (move n c1 c2). Proof. by apply: (iffP (moveP n _ _))=> [[d []]|[d []]]; exists d. Qed. Lemma move0E c1 c2 : move 0 c1 c2 = false. Proof. by apply/idP=> /moveP[d []]; rewrite ltn0. Qed. Lemma move_mk_perfect m c1 c2 : move m c1 c2 -> exists d, [/\ d < m, c1 d != c2 d, forall d1, d != d1 -> c1 d1 = c2 d1, c1 = mk_perfect d (opeg (c1 d) (c2 d)) c1 & c2 = mk_perfect d (opeg (c1 d) (c2 d)) c2]. Proof. move=> /moveP[d [Hd1 Hd2 Hd3 Hd4 Hd5]]; exists d; split => //. apply/ffunP=> i; rewrite ffunE. case: leqP => // iLm; rewrite ltnNge in iLm. apply/sym_equal/eqP; rewrite opegE // -negb_or. apply: contra (iLm) => /orP[/eqP/Hd4//|]. rewrite Hd3=> [/eqP/Hd5//|]. by apply: contra (iLm) => /eqP->. apply/ffunP=> i; rewrite ffunE. case: leqP => // iLm; rewrite ltnNge in iLm. apply/sym_equal/eqP; rewrite opegE // -negb_or. apply: contra (iLm) => /orP[|/eqP/Hd5//]. rewrite -Hd3=> [/eqP/Hd4//|]. by apply: contra (iLm) => /eqP->. Qed. Lemma moveW m1 m2 : m1 <= m2 -> subrel (move m1) (move m2). Proof. move=> d1Ld2 c1 c2 /existsP[d /and5P[H1 H2 H3 H4 H5]]. by apply/existsP; exists d; rewrite (leq_trans H1) // H2 H3 H4. Qed. Lemma move_sym m c1 c2 : move m c1 c2 = move m c2 c1. Proof. by apply/moveP/moveP=> [] [d [H1 H2 H3 H4 H5]]; exists d; split; rewrite 1?eq_sym // => e dDe; apply/sym_equal/H3. Qed. Lemma move_large m d c1 c2 : m <= d -> move m c1 c2 -> c1 d = c2 d. Proof. move=> mLd /moveP[d1 [H1 H2 H3 H4 H5]]. by apply: H3; rewrite neq_ltn (leq_trans H1). Qed. (* In a move only one disk moves *) Lemma move_disk1 d1 d2 m c1 c2 : move m c1 c2 -> d1 != d2 -> c1 d1 != c2 d1 -> c1 d2 = c2 d2. Proof. case/moveP=> d3 [H1 H2 H3 H4 H5] d1Dd2 c1d1Dc2d1. have [/eqP d3Ed1|d3Dd1] := boolP (d3 == d1). by apply: H3; rewrite d3Ed1. by case/eqP: c1d1Dc2d1; apply: H3. Qed. (* In a move only one, all the smaller disks are pilled up *) Lemma move_perfectr m d c1 c2 : move m c1 c2 -> c1 d != c2 d -> c2 = mk_perfect d (opeg (c1 d) (c2 d)) c2. Proof. case/moveP=> d1 [H1 H2 H3 H4 H5] c1d1Dc2d1. apply/ffunP=> d2; rewrite !ffunE. have dEd1 : d = d1. apply/eqP; rewrite eq_sym -[_ == _]negbK. apply: contra c1d1Dc2d1 => H. by apply/eqP/H3. case: leqP => // d2Ld. apply/eqP; rewrite eq_sym opegE // dEd1. (apply/andP; split; apply/eqP)=> [|/H5]; last first. by rewrite leqNgt -dEd1 d2Ld. have /H3<- : d1 != d2. by rewrite -dEd1; apply/eqP=> dEd2; move: d2Ld; rewrite dEd2 ltnn. by move/H4; rewrite leqNgt -dEd1 d2Ld. Qed. Lemma move_perfectl m d c1 c2 : move m c1 c2 -> c1 d != c2 d -> c1 = mk_perfect d (opeg (c1 d) (c2 d)) c1. Proof. rewrite move_sym eq_sym opeg_sym. exact: move_perfectr. Qed. Lemma moveS m c1 c2 : c1 m = c2 m -> move m.+1 c1 c2 -> move m c1 c2. Proof. move=> c1Ec2 /moveP[d [H1 H2 H3 H4 H5]]. apply/moveP; exists d; split => //. move: H1; rewrite leq_eqVlt => /orP[] //= H. have H6 : m = d by apply/val_eqP; rewrite -eqSS eq_sym. by case/eqP: H2; rewrite -H6. Qed. Lemma moveP_gtn m : n <= m -> move m =2 move n. Proof. move=> nLm c1 c2. apply/moveP/moveP=> [] [d [H1 H2 H3 H4 H5]]; exists d; split=> //. by rewrite (leq_trans _ nLm). Qed. Lemma move_opeg_l c1 c2 d m : c1 m != c2 m -> move m.+1 c1 c2 -> d < m -> c1 d = opeg (c1 m) (c2 m). Proof. move=> c1Dc2 /moveP[d1 [H1 H2 H3 H4 H5]] dLm. have d1Em : d1 = m. by apply/eqP; case: eqP => // /eqP /H3 /eqP H6; case/negP: c1Dc2. apply/eqP; rewrite eq_sym opegE // -d1Em. (apply/andP; split; apply/eqP)=> [/H4 |]. by rewrite leqNgt d1Em dLm. rewrite H3=> [/H5|]; last by rewrite neq_ltn d1Em dLm orbT. by rewrite d1Em leqNgt dLm. Qed. Lemma move_opeg_r c1 c2 d m : c1 m != c2 m -> move m.+1 c1 c2 -> d < m -> c2 d = opeg (c1 m) (c2 m). Proof. rewrite eq_sym move_sym => c2Dc1 Hm dLm. by rewrite opeg_sym 1?eq_sym // (move_opeg_l _ Hm). Qed. (* Some lifting of theorems about move to path *) Implicit Type cs : seq configuration. Lemma path_move_rev m c cs : path (move m) (last c cs) (rev (belast c cs)) = path (move m) c cs. Proof. by rewrite rev_path; apply: eq_path => c1 c2; exact: move_sym. Qed. Lemma path_large m d c1 c2 cs : m <= d -> path (move m) c1 cs -> c2 \in c1 :: cs -> c1 d = c2 d. Proof. move=> mLd Hp; rewrite inE=> /orP[/eqP->//|]. elim: cs c1 Hp => //= c3 cs IH c1 /andP[H Hmem]. rewrite inE => /orP[/eqP->|H1]; first by apply: move_large H. by rewrite (move_large _ H) // IH. Qed. Lemma pathS m c cs : (forall c1, c1 \in cs -> c1 m = c m) -> path (move m.+1) c cs -> path (move m) c cs. Proof. move=> Hc /pathP Hw. apply/(pathP c) => i Hi. apply: moveS (Hw _ _ Hi); apply: sym_equal. rewrite Hc ?mem_nth //. case: i Hi => [|i1 Hi1] //=. by rewrite Hc ?mem_nth // (leq_trans _ Hi1). Qed. Inductive pathS_spec (d : 'I_n) c : forall cs (b : bool), Type := pathS_specW : forall cs, path (move d) c cs -> pathS_spec d c cs true | pathS_spec_move : forall c1 cs1 cs2, path (move d) c cs1 -> c d != c1 d-> move d.+1 (last c cs1) c1 -> path (move d.+1) c1 cs2 -> pathS_spec d c (cs1 ++ c1 :: cs2) true | pathS_spec_false : forall cs, pathS_spec d c cs false. (* Inversion theorem on a path for move d.+1 *) Lemma pathSP d c cs : pathS_spec d c cs (path (move d.+1) c cs). Proof. have [Hp|_] := boolP (path _ _ _); last by apply: pathS_spec_false. pose f c1 := c1 d != c d. have [Hh|/hasPn Hn] := boolP (has f cs); last first. apply/pathS_specW/(pathS _ Hp) => c1 Hc1. by have := Hn _ Hc1; rewrite negbK=> /eqP. pose n1 := find f cs; pose c1 := nth c cs n1. pose cs1 := take n1 cs; pose cs2 := drop n1.+1 cs. have csE : cs = cs1 ++ c1 :: cs2. by rewrite -[cs](cat_take_drop n1.+1) -cat_rcons -take_nth // -has_find. rewrite csE; apply: pathS_spec_move; last 3 first. - by rewrite eq_sym; have := nth_find c Hh. - by move: Hp; rewrite csE cat_path => /and3P[]. - by move: Hp; rewrite csE cat_path => /and3P[]. apply: pathS => [c2 Hc2|]. have /(before_find c) : index c2 cs < find f cs. by rewrite {1}csE index_cat Hc2 (leq_trans (_ : _ < size cs1)) // ?index_mem // size_take -has_find Hh. rewrite csE index_cat Hc2 nth_cat index_mem Hc2 nth_index //. by move=> /idP/negP; rewrite negbK => /eqP. by move: Hp; rewrite csE cat_path => /andP[]. Qed. Lemma move_set d p c1 c2 : move d c1 c2 -> move d (setd d p c1) (setd d p c2). Proof. case/moveP=> d1 [H1 H2 H3 H4 H5]. apply/moveP; exists d1; split=> [||d2|d2|d2]; rewrite ?ffunE //. - by case: (d1 =P _) H1 => //->; rewrite ltnn. - by case: (d2 =P _) => // _; apply: H3. - case: (d1 =P _) H1 => [->|]; first by rewrite ltnn. by case: (d2 =P _) => [-> _ /ltnW//| _ _ _ /H4]. case: (d1 =P _) H1 => [->|]; first by rewrite ltnn. by case: (d2 =P _) => [-> _ /ltnW//| _ _ _ /H5]. Qed. Lemma setd_id d c : setd d (c d) c = c. Proof. by apply/ffunP=> d1; rewrite !ffunE; case: eqP => [->|]. Qed. (* we can restrict a path from d.+1 to d *) Lemma pathS_restrict d c cs : path (move d.+1) c cs -> {cs'| [/\ path (move d) (setd d (last c cs d) c) cs', last (setd d (last c cs d) c) cs' = last c cs & size cs' <= size cs ?= iff ((cs' == cs) && (last c cs d == c d))]}. Proof. elim: cs c => /= [c _|c1 cs IH c /andP[cMc1 /IH[cs1 [c1Pcs1 lccs1Mlc1cs S]]]]. by exists [::]; split; rewrite ?setd_id //; apply: leqif_refl; rewrite !eqxx. have [/eqP c1dEcd|c1dDcd] := boolP (c d == c1 d). exists (setd d (last c1 cs d) c1 :: cs1); split=> //=. - by rewrite move_set 1?moveS. rewrite eqseq_cons c1dEcd. case: (cs1 == _) S; rewrite ?andbF /=; last first. by move=> /leqifP H; apply/leqifP. case: (_ =P c1 d); rewrite ?andbF /=; last first. by move=> _ /leqifP H; apply/leqifP. rewrite !andbT => HH. move=> /leqifP H; apply/leqifP. case: eqP => // [] []. apply/ffunP=> d1; rewrite ffunE. by case: eqP => [->|]. have -> : setd d (last c1 cs d) c = setd d (last c1 cs d) c1. apply/ffunP=> d1; rewrite !ffunE. case: eqP=> // /eqP d1Dd. by apply: move_disk1 cMc1 _ c1dDcd; rewrite 1?eq_sym. exists cs1; split=> //=. apply/leqifP; case: eqP=> [H|/= _]; last by rewrite ltnS S. by have := leq_of_leqif S; rewrite H /= ltnn. Qed. (* we can restrict a path from d.+1 to d *) Lemma pathS_restrictE d c cs : path (move d.+1) c cs -> last c cs d = c d -> {cs'| [/\ path (move d) c cs', last c cs' = last c cs & size cs' <= size cs ?= iff (cs' == cs)]}. Proof. move=> cPcs lccsdEcd. have [cs1 [H1 H2 H3]] := pathS_restrict cPcs. have F : setd d (last c cs d) c = c. by apply/ffunP=> d1; rewrite !ffunE; case: eqP=> // ->. exists cs1; split; first by rewrite -F. by rewrite -{1}F. by move: H3; rewrite lccsdEcd eqxx andbT. Qed. (* we can restrict a path from d.+1 to d *) Lemma pathS_restrictES d c c1 cs : path (move d.+1) c cs -> last c cs d = c d -> c1 \in cs -> c1 d != c d -> {cs'| [/\ path (move d) c cs', last c cs' = last c cs & size cs' < size cs]}. Proof. move=> cPcs lccsdEcd c1Ics c1dDcd. have [cs1 [H1 H2 H3]] := pathS_restrictE cPcs lccsdEcd. exists cs1; split => //. move/leqifP : H3; case: eqP => // cs1Ecs. case/eqP: c1dDcd. apply: sym_equal; apply: path_large H1 _ => //. by rewrite inE cs1Ecs c1Ics orbT. Qed. (* connect is symmetric *) (* there should be a shorter proof since move n is symmetric *) Lemma connect_sym : connect_sym (move n). Proof. move=> c1 c2. apply/connectP/connectP=> [] [p H1 H2]. exists (rev (belast c1 p)); first by rewrite H2 path_move_rev. by case: (p) H2 => [->//|c3 p1 _]; rewrite rev_cons last_rcons. exists (rev (belast c2 p)); first by rewrite H2 path_move_rev. by case: (p) H2 => [->//|c3 p1 _]; rewrite rev_cons last_rcons. Qed. Lemma connect_large m d c1 c2 : m <= d -> connect (move m) c1 c2 -> c1 d = c2 d. Proof. move=> mLd /connectP[[|c3 cs] Pc1cs ->//=]. apply: path_large Pc1cs _ => //. by rewrite in_cons (mem_last _ _) orbT. Qed. (*****************************************************************************) (* *) (* Key Intermediate Lemma : *) (* if the bottom disk had moved twice either we have come back to the *) (* initial position or we have connected two perfect configurations *) (* *) (*****************************************************************************) Lemma move_twice d c1 c2 c3 c4 : c1 != c4 -> c1 d != c2 d -> c3 d != c4 d -> move d.+1 c1 c2 -> connect (move d) c2 c3 -> move d.+1 c3 c4 -> c2 = mk_perfect d (opeg (c1 d) (c2 d)) c2 /\ c3 = mk_perfect d (c1 d) c2. Proof. move=> c1Dc4 c1Dc2 c3Dc4 c1Mc2 c2Cc3 c3Mc4. have [/eqP c1dEc4d| c1dDc4d] := boolP (c1 d == c4 d). case/eqP: c1Dc4; apply/ffunP=> p. have [|dLp] := leqP p d; last first. rewrite (move_large _ c1Mc2) // (connect_large _ c2Cc3) 1?ltnW //. rewrite (move_disk1 c3Mc4 (_ : d != _)) //. apply/eqP=> mEp. by move: dLp; rewrite mEp ltnn. rewrite leq_eqVlt=> /orP[/val_eqP->//|pLm]. rewrite (move_perfectl c1Mc2 c1Dc2) !ffunE pLm. rewrite (move_perfectr c3Mc4 c3Dc4) -c1dEc4d. rewrite !ffunE pLm (_ : c3 d = c2 d) 1?opeg_sym //. by apply/sym_equal/(connect_large _ c2Cc3). split; first by rewrite {1}(move_perfectr c1Mc2 c1Dc2). apply/ffunP=> d1; rewrite !ffunE. case: leqP=> d1Ld; first by rewrite (connect_large _ c2Cc3). rewrite {1}(move_perfectl c3Mc4 c3Dc4) !ffunE d1Ld. apply/eqP; rewrite opegE //. rewrite -(connect_large _ c2Cc3) // eq_sym c1Dc2. by rewrite [c4 _ == _]eq_sym c1dDc4d andbT. Qed. (*****************************************************************************) (* Function that builds a path from a configuration to a peg *) (*****************************************************************************) Fixpoint rpeg_path_rec (m : nat) : m <= n -> _ -> _ -> seq configuration := match m with | 0 => fun _ _ _ => [::] | m1.+1 => fun H c p => let H1 := ltnW H in let dm := mk_disk H in if c dm == p then rpeg_path_rec H1 c p else let p1 := opeg (c dm) p in let c1 := setd dm p (mk_perfect m1 p1 c) in rpeg_path_rec H1 c p1 ++ c1 :: rpeg_path_rec H1 c1 p end. Lemma rpeg_path_rec_eq m1 m2 c p (H1 : m1 <= n) (H2 : m2 <= n) : m1 = m2 -> rpeg_path_rec H1 c p = rpeg_path_rec H2 c p. Proof. elim: m1 m2 c p H1 H2=> [[|m2] //|m1 IH [//|m2] c p H1 H2 m1SEm2S /=]. have m1Em2 : m1 = m2 by rewrite [m1]pred_Sn m1SEm2S. have <- : mk_disk H1 = mk_disk H2 by apply/val_eqP/eqP. set c1 := setd _ _ _; set c2 := setd _ _ _. have ->: c1 = c2. apply/ffunP=> d; rewrite !ffunE. congr (if _ then _ else _). by congr (if _ then _ else _); rewrite m1Em2. by congr (if _ then _ else _ ++ _ :: _); apply: IH. Qed. Definition rpeg_path c p := rpeg_path_rec (leqnn n) c p. Lemma rpeg_path_rec_id m (H : m <= n) c p : (forall d, d < m -> c d = p) -> rpeg_path_rec H c p = [::]. Proof. elim: m H c p => //= m IH H c p Heq. rewrite Heq ?leqnn // eqxx. by apply: IH => d dLm; apply/Heq/(leq_trans _ dLm). Qed. Lemma rpeg_path_id p : rpeg_path (perfect p) p = [::]. Proof. by apply: rpeg_path_rec_id=> d; rewrite ffunE. Qed. Lemma rpeg_path_rec_nil_inv m (H : m <= n) d c p : rpeg_path_rec H c p = [::] -> d < m -> c d = p. Proof. elim: m H d => //= m IH H d. case: eqP => [H1 /IH H2|_ ]; last by case: rpeg_path_rec. rewrite ltnS leq_eqVlt=> /orP[/eqP H3|]; last by apply: H2. by rewrite (_ : d = mk_disk H) //; apply/val_eqP/eqP. Qed. Lemma rpeg_path_rec_correct m (H : m <= n) c p (cs := rpeg_path_rec H c p) : path (move m) c cs /\ last c cs = mk_perfect m p c. Proof. rewrite /cs; elim: m H c p {cs} => /= [_ c p| m IH H c p]. by split=> //; apply/ffunP=> d; rewrite ffunE. set H1 := ltnW _; set dm := mk_disk _. set c1 := mk_perfect _ _ _. case: eqP => [Ho|/eqP Do]. have [Hp Hl] := IH H1 c p. split; first by apply/(sub_path _ Hp)/moveW. rewrite Hl; apply/ffunP=> d1; rewrite !ffunE. rewrite ltnS [d1 <= _]leq_eqVlt orbC. case: leqP => //= _; case: eqP => // dEm. by rewrite -Ho; congr (_ _); apply/val_eqP/eqP. set c2 := setd _ _ _. split; last first. rewrite last_cat /=. have [_ ->] := IH H1 c2 p. by apply/ffunP=> d; rewrite !ffunE ltnS [d <= m]leq_eqVlt orbC; case: leqP. have [IH1 IH2] := IH H1 c (opeg (c dm) p). have [IH3 IH4] := IH H1 c2 p. rewrite cat_path /= !(sub_path (moveW (leqnSn _))) ?andbT //= IH2. apply/moveP; exists dm; split => // [|d|d|d]; rewrite !ffunE. - by rewrite ltnn eqxx. - by rewrite eq_sym=> /negPf->. - rewrite ltnn; case: ltnP => //= _ /eqP. by rewrite eq_sym (negPf (opegDl _)). rewrite eqxx; case: eqP => [-> //|] /=. case: leqP=> // _ _ /eqP. by rewrite eq_sym (negPf (opegDr _)). Qed. Lemma rpeg_path_correct c p (cs := rpeg_path c p) : path (move n) c cs /\ last c cs = perfect p. Proof. have [H1 ->] := rpeg_path_rec_correct (leqnn n) c p. by split => //; apply/ffunP=> d; rewrite !ffunE ltn_ord. Qed. (* We can go from any configuration to a perfect configuration *) Lemma move_connect_rpeg c p : connect (move n) c (perfect p). Proof. have [H1 H2] := rpeg_path_correct c p. by apply/connectP; exists (rpeg_path c p). Qed. (* So we can also from a perfect configuration c to any configuration *) Lemma move_connect_lpeg c p : connect (move n) (perfect p) c. Proof. by rewrite connect_sym move_connect_rpeg. Qed. (* Two configurations are always connected *) Lemma move_connect c1 c2 : connect (move n) c1 c2. Proof. by apply: connect_trans (move_connect_rpeg c1 peg1) (move_connect_lpeg c2 peg1). Qed. (*****************************************************************************) (* Computes the size of rpeg_path *) (*****************************************************************************) Fixpoint size_rpeg_path_rec (m : nat) : m <= n -> configuration -> peg -> nat := match m with | 0 => fun _ _ _ => 0 | m1.+1 => fun H c p => let H1 := ltnW H in let d := mk_disk H in if c d == p then size_rpeg_path_rec H1 c p else let p1 := opeg (c d) p in size_rpeg_path_rec H1 c p1 + 2 ^ (m.-1) end. Lemma size_rpeg_path_rec_eq m1 m2 c p (H1 : m1 <= n) (H2 : m2 <= n) : m1 = m2 -> size_rpeg_path_rec H1 c p = size_rpeg_path_rec H2 c p. Proof. elim: m1 m2 c p H1 H2=> [[|m2] //|m1 IH [//|m2] c p H1 H2 m1SEm2S /=]. have m1Em2 : m1 = m2 by rewrite [m1]pred_Sn m1SEm2S. have <- : mk_disk H1 = mk_disk H2 by apply/val_eqP/eqP. by congr (if _ then _ else _ + _); rewrite ?m1Em2 //; apply: IH. Qed. (* size on a perfect configuration is a power of 2 *) Lemma size_rpeg_path_rec_2p m (H: m <= n) p1 p2 c (c1 := mk_perfect m p1 c) : size_rpeg_path_rec H c1 p2 = (2^ m).-1 * (p1 != p2). Proof. case: eqP=> [<-|/eqP p1Dp2]; rewrite (muln1, muln0). rewrite {}/c1; elim: m H c => //= m1 IH H c. rewrite ffunE leqnn eqxx. have := mk_perfect_max m1 m1.+1 p1 c. by have /maxn_idPr-> : m1 <= m1.+1 => [|<-]. rewrite {}/c1; elim: m H c p2 p1Dp2 => //= m1 IH H c p2 p1Dp2. rewrite ffunE leqnn (negPf p1Dp2). have := mk_perfect_max m1 m1.+1 p1 c. have /maxn_idPr-> : m1 <= m1.+1 => [//|<-]. rewrite IH; last by rewrite eq_sym opegDl. rewrite expnS mul2n -addnn. have: 0 < 2 ^ m1 by rewrite expn_gt0. by case: (_ ^ _). Qed. (* size computes the size *) Lemma size_rpeg_path_rec_pr m (H: m <= n) c p : size (rpeg_path_rec H c p) = size_rpeg_path_rec H c p. Proof. elim: m H c p => //= m1 IH H c p. set c2 := mk_perfect _ _ _. set d1 := mk_disk _. case: eqP => [//|/eqP Hd]. rewrite size_cat IH /=. congr (_ + _). rewrite IH. set c1 := setd _ _ _. have->: c1 = mk_perfect m1 (opeg (c d1) p) c1. apply/ffunP=> d; rewrite !ffunE. case: eqP=> [->|]; first by rewrite ltnn. by case: leqP. rewrite size_rpeg_path_rec_2p opegDr // muln1. have: 0 < 2 ^ m1 by rewrite expn_gt0. by case: (_ ^ _). Qed. (* Upper bound on the size *) Lemma size_rpeg_path_rec_up m (H: m <= n) c p : size_rpeg_path_rec H c p <= (2^ m).-1. Proof. elim: m H c p => //= m IH H c p. set H1 := ltnW _; set d := mk_disk _. case: eqP => _. apply: (leq_trans (IH H1 _ _)). case: (_ ^ _) (expn_eq0 2 m) (expn_eq0 2 m.+1) (leq_pexp2l (isT: 0 < 2) (ltnW (leqnn m.+1))) => //= n1 _. by case: (_ ^ _). apply: leq_trans (_ : (2^m).-1 + (2^m) <= _). by rewrite leq_add2r. rewrite expnS mul2n -addnn. by case: (2 ^ m) (expn_eq0 2 m) => [|n1]; rewrite ?addn0. Qed. Lemma eqseq_cat_size (T : eqType) (s1 s2 s3 s4 : seq T) : size s2 <= size s1 -> size s4 <= size s3 -> (s1 ++ s3 == s2 ++ s4) = (s1 == s2) && (s3 == s4). Proof. move=> H1 H2; apply/eqP/andP=> [/eqP|[/eqP-> /eqP->//]]. elim: s1 s2 H1 H2 => [[|] //= _ _ -> // | a s1 IH [/= H1 H2 /eqP H3|b s2]]. suff : size s4 < size (a :: s1 ++ s3) by rewrite -H3 ltnn. by rewrite /= size_cat ltnS (leq_trans H2) // leq_addl. rewrite /= !eqseq_cons ltnS => H1 H2 /andP[-> /IH/=]. by apply. Qed. (* rpeg_path_rec gives the smallest path to a perfect configuration. *) (* This path is unique *) Lemma rpeg_path_rec_min m (H: m <= n) c1 p cs (c2 := mk_perfect m p c1) : path (move m) c1 cs -> last c1 cs = c2 -> size_rpeg_path_rec H c1 p <= size cs ?= iff (cs == rpeg_path_rec H c1 p). Proof. rewrite {}/c2. elim: m p c1 cs H => [p c1 [|]//|m IH p c1 cs mLn]. elim: {cs}_.+1 {-2}cs (leqnn (size cs).+1) c1 => //= n1 IH1 cs Lcs c1 c1PScs. set mLen := ltnW _; set dm := mk_disk _. case: eqP=> [c1mEp lcsP |/eqP c1mDp]. have lcsmEc1m : last c1 cs dm = c1 dm. by rewrite lcsP ffunE c1mEp leqnn. have [cs1 [c1Pcs1 lcsElcs1 /leqifP]] := pathS_restrictE (c1PScs : path (move dm.+1) c1 cs) lcsmEc1m. have lcs1P : last c1 cs1 = mk_perfect m p c1. apply/ffunP=> d; rewrite lcsElcs1 lcsP !ffunE ltnS leq_eqVlt. case: eqP=> // /eqP H. have->: d = dm by apply/val_eqP. by rewrite ltnn. case: eqP=> [cs1Ecs _|/eqP cs1Dcs Lcs1]. by apply: IH; rewrite // -cs1Ecs. apply/leqifP; case: eqP => [->//|_]. by rewrite size_rpeg_path_rec_pr. apply: leq_ltn_trans Lcs1. by apply: (leq_of_leqif (IH _ _ _ _ _ _)). case: pathSP {c1PScs}(c1PScs : path (move dm.+1) _ _) Lcs => {cs}//= [cs c1Pcs _ Lcs| c3 cs1 cs2 c1Pcs1 c1mDc3m lcs1Mc3 c3PScs2 _]. (* the last disk is already well-placed *) set c2 := mk_perfect _ _ _ => lcsEc2 /=. case/eqP: c1mDp. have-> : p = c2 dm by rewrite ffunE leqnn. by apply: path_large c1Pcs _; rewrite // -lcsEc2 mem_last. set fc := setd _ _ _ => Lcs. rewrite last_cat /=. set c2 := mk_perfect _ _ _ => lcs2Ec2 /=. have c2mEp : c2 dm = p by rewrite ffunE leqnn. (* c3 is the first configuration when the last disk has moved *) have lcs1mEc1m : last c1 cs1 dm = c1 dm. by rewrite (path_large _ c1Pcs1 (mem_last _ _)). (* Now we check if the last disk has moved after c3 *) case: pathSP (c3PScs2 : path (move dm.+1) _ _) Lcs lcs2Ec2 => {cs2 c3PScs2}//= [cs2 c3Pcs2 _ Lcs lcs2Ec2 | c4 cs2 cs3 c3Pcs2 c3mDc4m lcs2Mc4 c4Pcs3]. (* there is no more move, so the last disk is well-placed at c3 *) have c3mEp : c3 dm = p. rewrite (path_large _ c3Pcs2 (mem_last _ _)) //. by rewrite [last _ _]lcs2Ec2 !ffunE leqnn. have lcs1mEc3m : last c1 cs1 dm != c3 dm by rewrite lcs1mEc1m. rewrite (_ : fc = c3); last first. apply/ffunP=> d; rewrite !ffunE. case: eqP=> [->//|/val_eqP/= dDm]. case: leqP; last first. rewrite (move_perfectr lcs1Mc3 lcs1mEc3m) ffunE => ->. by rewrite lcs1mEc1m c3mEp. rewrite leq_eqVlt eq_sym (negPf dDm) /= => mLd. rewrite (path_large _ c1Pcs1 (mem_last _ _)) 1?ltnW //. by apply: move_large lcs1Mc3. have lcs1P : last c1 cs1 = mk_perfect dm (opeg (c1 dm) p) c1. rewrite (move_perfectl lcs1Mc3 lcs1mEc3m). apply/ffunP=> d; rewrite !ffunE /=. case: leqP=> [mLd|dLm]. by apply/sym_equal/(path_large mLd c1Pcs1 (mem_last _ _)). by rewrite lcs1mEc1m c3mEp. have V1 := IH _ _ _ mLen c1Pcs1 lcs1P. have lcs2P : last c3 cs2 = mk_perfect dm p c3. apply/ffunP=> d; rewrite !ffunE. case: leqP => HH. by apply: sym_equal; apply: path_large c3Pcs2 (mem_last _ _). by rewrite lcs2Ec2 ffunE ltnW. have V2 := IH _ _ _ mLen c3Pcs2 lcs2P. have c3P : c3 = mk_perfect dm (opeg (c1 dm) p) c3. have : last c1 cs1 dm != c3 dm by rewrite lcs1mEc1m. move/(move_perfectr lcs1Mc3) -> . apply/ffunP=> d; rewrite !ffunE; case: leqP=> //. by rewrite lcs1mEc1m c3mEp. move: V2; rewrite c3P size_rpeg_path_rec_2p opegDr // muln1 => V2. rewrite eqseq_cat_size; last 2 first. - by rewrite size_rpeg_path_rec_pr (leq_of_leqif V1). - rewrite /= ltnS size_rpeg_path_rec_pr. by rewrite size_rpeg_path_rec_2p opegDr // muln1 (leq_of_leqif V2). rewrite eqseq_cons size_cat /=. apply: leqif_add => //. by rewrite eqxx -[2 ^ _]prednK ?expn_gt0. (* we move twice the last disk so the path is not optimal *) rewrite last_cat /=. move => _ Lcs lcs3Ec2. have lcs1mDc3m : last c1 cs1 dm != c3 dm by rewrite lcs1mEc1m. have c3Clcs2 : connect (move dm) c3 (last c3 cs2) by apply/connectP; exists cs2. have lcs2mDc4m : last c3 cs2 dm != c4 dm. by rewrite -(path_large _ c3Pcs2) // mem_last. apply/leqifP. case: eqP => [->|_]. rewrite size_cat size_rpeg_path_rec_pr eqn_add2l /=. have-> : fc = mk_perfect m (opeg (c1 dm) p) fc. apply/ffunP=> d; rewrite !ffunE. case: eqP => [->|]; first by rewrite ltnn. by case: leqP. rewrite size_rpeg_path_rec_pr size_rpeg_path_rec_2p. by rewrite opegDr // muln1 prednK // expn_gt0. have [/eqP lcs1Ec3| lcs1Dc4] := boolP (last c1 cs1 == c4). have c1PScs1cs3 : path (move m.+1) c1 (cs1 ++ cs3). by rewrite cat_path (sub_path (moveW (leqnSn _))) // lcs1Ec3. have Lcs1 : size (cs1 ++ cs3) < n1. move: Lcs; rewrite size_cat /= size_cat /= !addnS ltnS => Lcs. apply: leq_ltn_trans Lcs. by rewrite size_cat -!addnS leq_add2l -addSnnS leq_addl. have lcs1cs3P : last c1 (cs1 ++ cs3) = mk_perfect m.+1 p c1. by rewrite last_cat lcs1Ec3 lcs3Ec2. have /= := IH1 _ Lcs1 _ c1PScs1cs3 lcs1cs3P. rewrite -/dm (negPf c1mDp) => /leq_of_leqif /leq_ltn_trans->//. by rewrite !size_cat /= addnS ltnS leq_add2l size_cat /= -addSnnS leq_addl. have [Pc3 Plcs2] := move_twice lcs1Dc4 lcs1mDc3m lcs2mDc4m lcs1Mc3 c3Clcs2 lcs2Mc4. have Lcs2 : (2 ^ m).-1 <= size cs2. have /leq_of_leqif := IH _ _ _ mLen c3Pcs2 Plcs2. by rewrite Pc3 size_rpeg_path_rec_2p opegDl // muln1. (* now we just need to quantify size cs3 *) move: Lcs lcs3Ec2. rewrite !size_cat /= !size_cat /= !addnS /= ltnS. case: pathSP (c4Pcs3 : path (move dm.+1) c4 cs3) => {cs3 c4Pcs3}//= [cs3 c4Pcs3 _ Lcs lcs3Ec2| c5 cs3 cs4 c4Pcs3 c4dmDc5dm lcs3M5 c5Pcs4 _ Lcs]. have c4mEp: c4 dm = p. by rewrite (path_large _ c4Pcs3 (mem_last _ _)) // -c2mEp lcs3Ec2. have lcs3P : last c4 cs3 = mk_perfect m p c4. apply/ffunP=> d; rewrite lcs3Ec2 !ffunE. rewrite ltnS leq_eqVlt orbC; case: leqP => //=. rewrite leq_eqVlt eq_sym; case: eqP => *. by rewrite (_ : d = dm) //; apply/val_eqP/eqP. rewrite (path_large _ c1Pcs1 (mem_last _ _)) 1?ltnW //. rewrite (move_large _ lcs1Mc3) //. rewrite (path_large _ c3Pcs2 (mem_last _ _)) 1?ltnW //. by rewrite (move_large _ lcs2Mc4). have c4P : c4 = mk_perfect dm (opeg (c3 dm) p) c4. have := move_perfectr lcs2Mc4 lcs2mDc4m. by rewrite Plcs2 ffunE ltnn c4mEp. have Lcs3: (2 ^ m).-1 <= size cs3. have /leq_of_leqif := IH _ _ _ mLen c4Pcs3 lcs3P. by rewrite c4P size_rpeg_path_rec_2p opegDr -?c4mEp // ?muln1. rewrite ltnS -!addnS. apply: leq_trans (leq_addl _ _). apply: leq_add. by apply: leq_trans (size_rpeg_path_rec_up _ _ _) _. by rewrite -[2 ^ _]prednK // expn_gt0. rewrite last_cat /= => lcs4Ec2. have lcs3mEc4m : last c4 cs3 dm = c4 dm. by apply/sym_equal/(path_large (leqnn dm) c4Pcs3 (mem_last _ _)). have lcs3mDc5m : last c4 cs3 dm != c5 dm by rewrite lcs3mEc4m. have c4Clcs3 : connect (move dm) c4 (last c4 cs3) by apply/connectP; exists cs3. have [/eqP lcs2Ec5|lcs2Dc5] := boolP (last c3 cs2 == c5). have c1PScs1c3cs2cs4 : path (move m.+1) c1 (cs1 ++ (c3 :: cs2) ++ cs4). rewrite cat_path (sub_path (moveW (leqnSn _))) //=. by rewrite lcs1Mc3 cat_path (sub_path (moveW (leqnSn _))) //= lcs2Ec5. have Lcs1c3cs2cs4 : size (cs1 ++ (c3 :: cs2) ++ cs4) < n1. move: Lcs; rewrite size_cat /= size_cat /= !addnS => Lcs. apply: leq_ltn_trans Lcs. by rewrite size_cat -!addnS !leq_add2l -addSnnS leq_addl. have lcs4P : last c1 (cs1 ++ (c3 :: cs2) ++ cs4) = mk_perfect m.+1 p c1. by rewrite last_cat /= last_cat /= lcs2Ec5 lcs4Ec2. have /= := IH1 _ Lcs1c3cs2cs4 _ c1PScs1c3cs2cs4 lcs4P. rewrite -/dm (negPf c1mDp) => /leq_of_leqif /leq_ltn_trans->//. rewrite !size_cat /= size_cat /= !addnS !ltnS -!addnS. by rewrite !leq_add2l -addSnnS leq_addl. have [c4P lcs3P] := move_twice lcs2Dc5 lcs2mDc4m lcs3mDc5m lcs2Mc4 c4Clcs3 lcs3M5. have Lcs3 : (2 ^ m).-1 <= size cs3. have /leq_of_leqif := IH _ _ _ mLen c4Pcs3 lcs3P. by rewrite c4P size_rpeg_path_rec_2p opegDl // muln1. rewrite size_cat /= -!addSn addnA. apply: leq_add=> //; last first. rewrite -addSnnS (leq_trans _ (leq_addr _ _)) //. by rewrite -[2 ^ _]prednK // expn_gt0. rewrite addSnnS. apply: leq_trans (leq_addl _ _). apply: leq_ltn_trans (size_rpeg_path_rec_up _ _ _) _. by rewrite ltnS. Qed. (*****************************************************************************) (* Function that builds a path from a peg to a configuration *) (*****************************************************************************) Definition lpeg_path_rec m (H : m <= n) p c := rev (belast c (rpeg_path_rec H c p)). Definition lpeg_path p c := lpeg_path_rec (leqnn n) p c. Lemma lpeg_path_rec_id m (H : m <= n) p c : (forall d, d < m -> c d = p) -> lpeg_path_rec H p c = [::]. Proof. by move=> Hc; rewrite /lpeg_path_rec rpeg_path_rec_id. Qed. Lemma lpeg_path_id p : lpeg_path p (perfect p) = [::]. Proof. by apply: lpeg_path_rec_id=> d; rewrite ffunE. Qed. Lemma lpeg_path_rec_nil_inv m (H : m <= n) d p c : lpeg_path_rec H p c = [::] -> d < m -> c d = p. Proof. move=> H1 H2. have := @rpeg_path_rec_nil_inv _ H _ c p _ H2. move: H1; rewrite /lpeg_path_rec. case: rpeg_path_rec => [_ ->//|c1 cs /=]. by rewrite rev_cons; case: rev. Qed. Lemma lpeg_path_rec_correct m (H: m <= n) p c (cs := lpeg_path_rec H p c) : path (move m) (mk_perfect m p c) cs /\ last c cs = c. Proof. rewrite {}/cs. rewrite /lpeg_path_rec. have [H1 H2] := rpeg_path_rec_correct H c p. rewrite /lpeg_path_rec -H2 path_move_rev; split=> //. case: rpeg_path_rec => //= c1 cs. by rewrite rev_cons last_rcons. Qed. Lemma lpeg_path_correct p c (cs := lpeg_path p c) : path (move n) (perfect p) cs /\ last c cs = c. Proof. have [H1 ->] := lpeg_path_rec_correct (leqnn n) p c. by rewrite mkd_perfect0 in H1. Qed. Lemma size_lpeg_path_rec_pr m (H: m <= n) c p : size (lpeg_path_rec H p c) = size_rpeg_path_rec H c p. Proof. by rewrite size_rev size_belast size_rpeg_path_rec_pr. Qed. Lemma lpeg_path_rec_min m (H: m <= n) p c1 cs (c2 := mk_perfect m p c1) : path (move m) c2 cs -> last c2 cs = c1 -> size_rpeg_path_rec H c1 p <= size cs ?= iff (cs == lpeg_path_rec H p c1). Proof. (* why this is so complicated???? *) move=> H1 H2. have F1 : path (move m) c1 (rev (belast c2 cs)). by rewrite -H2 path_move_rev. have F2 : last c1 (rev (belast c2 cs)) = c2. rewrite -H2; case: (cs)=> //= c3 cs1. by rewrite rev_cons last_rcons. have := rpeg_path_rec_min H F1 F2. rewrite /lpeg_path_rec size_rev size_belast. set u := rev _ ; set v := rpeg_path_rec _ _ _. have -> : (u == v) = (rev (c1 :: u) == rev (c1 :: v)). rewrite !rev_cons eqseq_rcons eqxx andbT. apply/eqP/eqP=> [->//|]. by rewrite -{2}[u]revK => ->; rewrite revK. rewrite [c1:: v]lastI -/v rev_rcons. rewrite rev_cons revK -{2}H2 -lastI eqseq_cons andbC. case: eqP=> //; case: eqP => // H3 Hcs; case: H3. by have [] := rpeg_path_rec_correct H c1 p. Qed. (*****************************************************************************) (* Function that builds a path between two arbitrary configurations *) (* we use size_rpeg_path_rec to make the decision on where to move the disks *) (*****************************************************************************) Fixpoint hanoi_path_rec (m : nat) : m <= n -> _ -> _ -> seq configuration := if m is m1.+1 then fun H c1 c2 => let H1 := ltnW H in let dm := mk_disk H in if c1 dm == c2 dm then hanoi_path_rec H1 c1 c2 else (* one jump *) let p := opeg (c1 dm) (c2 dm) in let n1 := size_rpeg_path_rec H1 c1 p + size_rpeg_path_rec H1 c2 p in (* two jumps *) let n2 := size_rpeg_path_rec H1 c1 (c2 dm) + 2 ^ m1 + size_rpeg_path_rec H1 c2 (c1 dm) in if n1 <= n2 then let c3 := setd dm (c2 dm) (mk_perfect m1 p c1) in rpeg_path_rec H1 c1 p ++ c3 :: lpeg_path_rec H1 p c2 else let c3 := setd dm p (mk_perfect m1 (c2 dm) c1) in let c4 := setd dm (c2 dm) (mk_perfect m1 (c1 dm) c1) in rpeg_path_rec H1 c1 (c2 dm) ++ c3 :: rpeg_path_rec H1 c3 (c1 dm) ++ c4 :: lpeg_path_rec H1 (c1 dm) c2 else fun _ _ _ => [::]. Definition hanoi_path c1 c2 := hanoi_path_rec (leqnn n) c1 c2. Lemma hanoi_path_rec_correct m (H: m <= n) c1 c2 (cs := hanoi_path_rec H c1 c2) : (forall d, m <= d -> c1 d = c2 d) -> path (move m) c1 cs /\ last c1 cs = c2. Proof. rewrite {}/cs. elim: m H c1 c2 => /= [_ c1 c2 H|m IH H c1 c2 Hs]. by split=> //; apply/ffunP=> d; apply: H. set H1 := ltnW _; set dm := mk_disk _. set c3 := setd _ _ _; set c4 := setd _ _ _; set c5 := setd _ _ _. set p := opeg _ _. case: eqP => [c1mEc2m|/eqP c1mDc2m]. have /(IH H1)[H2 H3] : forall d, m <= d -> c1 d = c2 d. move=> d; rewrite leq_eqVlt => /orP[/eqP mEd|]; last by apply: Hs. by rewrite -(_ : dm = d) //; apply/val_eqP/eqP. by split=> //; apply: sub_path H2; apply/moveW. case: leqP=> _; rewrite !cat_path !last_cat {IH}/= ?cat_path ?last_cat /=. split; first (apply/and3P; split). - have [Hs1 Hs2] := rpeg_path_rec_correct H1 c1 p. by apply: sub_path Hs1; apply/moveW. - apply/moveP; exists dm. have [_ ->] := rpeg_path_rec_correct H1 c1 p. split=> // [|d dmDd|d|d]. - by rewrite !ffunE ltnn eqxx. - by rewrite !ffunE eq_sym (negPf dmDd). - rewrite !ffunE ltnn. case: leqP=> // _ /eqP. by rewrite eq_sym (negPf (opegDl _)). rewrite !ffunE eqxx; case: leqP => //. case: eqP=> [->|_ _ /eqP]; first by rewrite ltnn. by rewrite eq_sym (negPf (opegDr _)). - have [Hs1 Hs2] := lpeg_path_rec_correct H1 p c2. rewrite (_ : c3 = mk_perfect m p c2). by apply: sub_path Hs1; apply/moveW. apply/ffunP=> d. rewrite !ffunE; case: eqP => //= [->|]; first by rewrite ltnn. case: leqP => // Hu1 /eqP Hu2. apply: Hs. by rewrite ltn_neqAle eq_sym Hu2. have [Hs1 Hs2] := lpeg_path_rec_correct H1 p c2. have := @lpeg_path_rec_nil_inv _ H1 _ p c2. case: lpeg_path_rec Hs2 => //= _ HH. apply/ffunP=> d; rewrite !ffunE. case: eqP=> [->|] //. case: leqP => // HH1 /eqP HH2. by apply: Hs; rewrite ltn_neqAle eq_sym HH2. by apply/sym_equal/HH. split; first (apply/and5P; split). - have [Hs1 Hs2] := rpeg_path_rec_correct H1 c1 (c2 dm). by apply: sub_path Hs1; apply/moveW. - have [_ ->]:= rpeg_path_rec_correct H1 c1 (c2 dm). apply/moveP; exists dm; split => // [|d2|d2|d2]; rewrite ?ffunE. - by rewrite eqxx ltnn eq_sym opegDl. - by rewrite eq_sym => /negPf->. - by rewrite ltnn; case: leqP => // _ HH; case/eqP: c1mDc2m. rewrite eqxx; case: eqP => [->//|]. by case: leqP=> // _ _ /eqP; rewrite (negPf (opegDr c1mDc2m)). - have [Hs1 Hs2] := rpeg_path_rec_correct H1 c4 (c1 dm). by apply: sub_path Hs1; apply/moveW. - have [_ ->]:= rpeg_path_rec_correct H1 c4 (c1 dm). apply/moveP; exists dm; split => // [|d2|d2|d2]; rewrite ?ffunE. - by rewrite ltnn eqxx opegDr. - rewrite eq_sym => /negPf->. case: leqP => //. - rewrite ltnn eqxx; case: leqP => // _ /eqP. by rewrite (negPf (opegDl _)). - rewrite eqxx; case: leqP => //; case: eqP => // [-> //|_ ]. by rewrite ltnn. by move=> _ /eqP; rewrite eq_sym (negPf c1mDc2m). - have [Hs1 Hs2] := lpeg_path_rec_correct H1 (c1 dm) c2. rewrite (_ : c5 = mk_perfect m (c1 dm) c2). by apply: sub_path Hs1; apply/moveW. apply/ffunP=> d. rewrite !ffunE; case: eqP => //= [->|]; first by rewrite ltnn. case: leqP => // Hu1 /eqP Hu2. apply: Hs. by rewrite ltn_neqAle eq_sym Hu2. - have [_ ] := lpeg_path_rec_correct H1 (c1 dm) c2. have := @rpeg_path_rec_nil_inv _ H1 _ c2 (c1 dm). rewrite /lpeg_path_rec. case: rpeg_path_rec => /= [Hd _|c6 cs1 _]. apply/ffunP=> d. rewrite !ffunE; case: eqP=> [->//|]. case: leqP=> Hd1 /eqP Hd2; last by apply/sym_equal/Hd. apply: Hs. by rewrite ltn_neqAle eq_sym Hd2. by rewrite rev_cons !last_rcons. Qed. Lemma hanoi_path_correct c1 c2 (cs := hanoi_path c1 c2) : path (move n) c1 cs /\ last c1 cs = c2. Proof. apply: hanoi_path_rec_correct => d. by rewrite leqNgt ltn_ord. Qed. Lemma hanoi_rec_min m (H: m <= n) c1 c2 cs : path (move m) c1 cs -> last c1 cs = c2 -> size (hanoi_path_rec H c1 c2) <= size cs. Proof. elim: m c1 c2 cs H => [p c1 [|]//|m IH c1 c2 cs mLn /=]. set mLen := ltnW _; set dm := mk_disk _; set p := opeg _ _. case: eqP=> [c1mEc2m c1PScs lcsEc2|/eqP c1mDc2m c1PScs lcsEc2]. have lcsmEc1m : last c1 cs dm = c1 dm by rewrite lcsEc2. have [cs1 [c1Pcs1 lcsElcs1 /leq_of_leqif/(leq_trans _)->//]] := pathS_restrictE (c1PScs : path (move dm.+1) c1 cs) lcsmEc1m. by apply: IH; rewrite ?lcsElcs1. set u := _ + _; set v := _ + _. suff : minn u v < size cs. rewrite minnC /minn; case: (leqP u) => H1; rewrite !size_cat /= ?size_cat /= !addnS ?ltnS !size_rpeg_path_rec_pr !size_lpeg_path_rec_pr => H2. by apply: leq_trans H2. set c4 := setd _ _ _. apply: leq_ltn_trans _ H2. rewrite -addnS -addSn !addnA !leq_add //. rewrite -[2 ^ _]prednK ?expn_gt0 // ltnS. by apply: size_rpeg_path_rec_up. elim: {cs}_.+1 {-2}cs (leqnn (size cs).+1) c1PScs lcsEc2 => //= n1 IH1 cs Lcs c1PScs lcsEc2. case: pathSP {c1PScs}(c1PScs : path (move dm.+1) _ _) lcsEc2 Lcs => {cs}// [cs c1Pcs _ lcsEc2| c3 cs1 cs2 c1Pcs1 c1mDc3m lcs1Mc3 c3PScs2 _]. case/eqP: c1mDc2m. by apply: path_large c1Pcs _; rewrite // -lcsEc2 mem_last. rewrite last_cat /= => lcs2Ec2. rewrite size_cat /= addnS ltnS => Lcs. have lcs1mEc1m : last c1 cs1 dm = c1 dm. by rewrite (path_large _ c1Pcs1 (mem_last _ _)). have lcs1mDc3m : last c1 cs1 dm != c3 dm by rewrite lcs1mEc1m. have [/eqP c2mEc3m | c2mDc3m] := boolP (c2 dm == c3 dm). have lcs2mEc2m : last c3 cs2 dm = c3 dm by rewrite lcs2Ec2. have [cs3 [c3Pcs3 lcs3Elcs2 /leq_of_leqif Lcs3]] := pathS_restrictE (c3PScs2 : path (move dm.+1) c3 cs2) lcs2mEc2m. apply: leq_trans (leq_add (leqnn _) Lcs3). apply: leq_trans (geq_minl _ _) _. apply: leq_add. apply: leq_of_leqif (rpeg_path_rec_min _ _ _ ) => //. rewrite (move_perfectl lcs1Mc3 lcs1mDc3m). apply/ffunP=> d; rewrite !ffunE; case: leqP=> H. by rewrite (path_large _ c1Pcs1 (mem_last _ _)). by rewrite lcs1mEc1m -c2mEc3m. have c3P : c3 = mk_perfect m p c2. rewrite (move_perfectr lcs1Mc3 lcs1mDc3m). rewrite lcs1mEc1m -c2mEc3m -/p. apply/ffunP=> d; rewrite !ffunE; case: leqP=> H //. rewrite (path_large _ c3Pcs3 (mem_last _ _)) //. by rewrite lcs3Elcs2 lcs2Ec2. apply: leq_of_leqif (lpeg_path_rec_min _ _ _ ) => //. by rewrite -c3P. by rewrite -c3P lcs3Elcs2. case: pathSP (c3PScs2 : path (move dm.+1) _ _) lcs2Ec2 Lcs => {cs2 c3PScs2}//= [cs2 c3Pcs2 _ lcs2Ec2 Lcs | c4 cs2 cs3 c3Pcs2 c3mDc4m lcs2Mc4 c4PScs3 _]. case/eqP: c2mDc3m. by rewrite -lcs2Ec2 (path_large _ c3Pcs2 (mem_last _ _)). rewrite size_cat /= last_cat /= => lcs3Ec2 Lcs. rewrite -addSnnS ltnS. have lcs2mEc3m : last c3 cs2 dm = c3 dm. by rewrite -(path_large _ c3Pcs2 (mem_last _ _)). have lcs2mDc4m : last c3 cs2 dm != c4 dm by rewrite lcs2mEc3m. have [/eqP c4mEc1m|c4mDc1m] := boolP (c4 dm == c1 dm). have c4Elcs1 : c4 = last c1 cs1. rewrite (move_perfectl lcs1Mc3 lcs1mDc3m). rewrite (move_perfectr lcs2Mc4 lcs2mDc4m). rewrite lcs2mEc3m lcs1mEc1m c4mEc1m opeg_sym. apply/ffunP=> d; rewrite !ffunE; case: leqP => //. rewrite leq_eqVlt => /orP[/eqP dmEd|dmLd]. rewrite -(_ : dm = d); last by apply/val_eqP/eqP. by rewrite -(path_large _ c1Pcs1 (mem_last _ _)). rewrite -(move_large _ lcs2Mc4) //. rewrite -(path_large _ c3Pcs2 (mem_last _ _)) 1?ltnW //. by rewrite -(move_large _ lcs1Mc3). apply: leq_trans (_ : size (cs1 ++ cs3) <= _). apply/ltnW/IH1. - apply: leq_ltn_trans Lcs. by rewrite size_cat leq_add2l -addSnnS leq_addl. - by rewrite cat_path (sub_path (moveW (leqnSn _))) // -c4Elcs1. by rewrite last_cat -c4Elcs1. by rewrite size_cat leq_add2l leq_addl. have c4mEc2m : c4 dm = c2 dm. rewrite (_ : c2 dm = opeg (c1 dm) (c3 dm)); apply/eqP; rewrite eq_sym opegE //. by rewrite eq_sym c4mDc1m. by rewrite c1mDc2m // eq_sym. apply: leq_trans (geq_minr _ _) _. rewrite -[v]addnA leq_add //. apply: leq_of_leqif (rpeg_path_rec_min _ _ _ ) => //. rewrite (move_perfectl lcs1Mc3 lcs1mDc3m). apply/ffunP=> d; rewrite !ffunE; case: leqP=> H. by rewrite (path_large _ c1Pcs1 (mem_last _ _)). apply/eqP. by rewrite opegE lcs1mEc1m // c1mDc2m eq_sym. apply: leq_add. rewrite -[2 ^ _]prednK ?expn_gt0 // ltnS. have <-: size_rpeg_path_rec mLen c3 (opeg (c3 dm) (c2 dm)) = (2 ^ m).-1. rewrite (move_perfectr lcs1Mc3 lcs1mDc3m) lcs1mEc1m. rewrite size_rpeg_path_rec_2p. rewrite ffunE ltnn opegE // negb_and !negbK. by rewrite eq_sym opegE 1?eq_sym // c1mDc3m eq_sym c1mDc2m muln1. apply: leq_of_leqif (rpeg_path_rec_min _ _ _) => //. rewrite (move_perfectl lcs2Mc4 lcs2mDc4m) lcs2mEc3m c4mEc2m. apply/ffunP=> d; rewrite !ffunE; case: leqP => // H. by rewrite (path_large _ c3Pcs2 (mem_last _ _)). have lcs3mEc4m : last c4 cs3 dm = c4 dm by rewrite lcs3Ec2 c4mEc2m. have [cs4 [c4Pcs4 lcs4Elcs3 /leq_of_leqif Lcs3]] := pathS_restrictE (c4PScs3 : path (move dm.+1) c4 cs3) lcs3mEc4m. apply: leq_trans Lcs3. have c4P : c4 = mk_perfect m (c1 dm) c2. rewrite (move_perfectr lcs2Mc4 lcs2mDc4m). apply/ffunP=> d; rewrite !ffunE; case: leqP=> [|_]. rewrite leq_eqVlt => /orP[/eqP dmEd| dmLd]. by rewrite -(_ : dm = d) //; apply/val_eqP/eqP. by rewrite -lcs3Ec2 (path_large _ c4PScs3 (mem_last _ _)). apply/eqP. by rewrite lcs2mEc3m c4mEc2m opegE 1?eq_sym // c1mDc3m eq_sym. apply: leq_of_leqif (lpeg_path_rec_min _ _ _); rewrite -?c4P //. by rewrite lcs4Elcs3. Qed. Lemma hanoi_min c1 c2 cs : path (move n) c1 cs -> last c1 cs = c2 -> size (hanoi_path c1 c2) <= size cs. Proof. by apply: hanoi_rec_min. Qed. End Hanoi.