proposition: Lemma lhanoi3_min n (c1 c2 : configuration 3 n) cs : path lmove c1 cs -> last c1 cs = c2 -> size (lhanoi3 c1 c2) <= size cs ?= iff (cs == lhanoi3 c1 c2).
proof: Proof. have [m sLm] := ubnP (size cs); elim: m => // m IHm in n c1 c2 cs sLm *. elim : n c1 c2 cs sLm => [c1 p [|] //=|n IH c1 c cs Scs c1Pcs lc1csEp /=]. set (p := c ldisk). rewrite !fun_if !size_cat /= !size_cat /= !size_map. case: (c1 _ =P p) => [lc1Ep |/eqP lc1Dp]. have [cs1 [c1'Pcs1 lc1'csElc1cs' /leqifP]] := pathS_restrict (@lirr 3) c1Pcs. have lc1'cs1E : last ↓[c1] cs1 = ↓[c]. by rewrite lc1'csElc1cs'; congr cunliftr. case: eqP=> [csEcs1 /eqP<- |/eqP csDcs1 scs1L]. rewrite csEcs1 lc1Ep eq_map_liftr. apply: IH => //. by move: Scs; rewrite csEcs1 size_map. apply/leqifP; case: eqP => [->//|_]. by rewrite size_map. apply: leq_ltn_trans (scs1L). apply: IH => //. by apply: ltn_trans Scs. pose f (c : configuration 3 n.+1) := c ldisk. have HHr := @lirr 3. have HHs := @lsym 3. case: path3SP c1Pcs => // [c1' cs' p1 csE c1'Ecs1'| cs1 cs2 p1 p2 p3 c1' c2 p1Dp2 p1Rp2 lc1'cs1Epp3 csE c1'Pcs1 c2Pcs2 _]. case/eqP: lc1Dp. move: lc1csEp => /(congr1 f). by rewrite /f csE -{1}[c1]cunliftrK last_map cliftr_ldisk. rewrite csE size_cat -/p1. have Scs1 : size cs1 < m.+1. apply: ltn_trans Scs. by rewrite csE size_cat /= size_map addnS ltnS leq_addr. have Scs2 : size cs2 < m.+1. apply: ltn_trans Scs. by rewrite csE size_cat /= size_map addnS ltnS leq_addl. have [p1Rp| p1NRp] := boolP (lrel p1 p). case: (p2 =P p) => [p2Ep|/eqP p2Dp]. rewrite -p2Ep -/p3 size_map /=. have/(pathS_restrict (@lirr 3))[cs2' [c2'Pcs2' lc2'cs2'E cs2'L]] := c2Pcs2. have Scs2' : size cs2' < m.+1. by apply: leq_ltn_trans Scs2; rewrite cs2'L. have /IH := lc1'cs1Epp3 => // /(_ Scs1 c1'Pcs1) IHc1. have /IH : last ↓[c2] cs2' = ↓[c] => [| /(_ Scs2' c2'Pcs2') IHc2]. rewrite lc2'cs2'E; congr cunliftr. by move: lc1csEp; rewrite csE last_cat /= => ->. rewrite cliftrK in IHc2. move /leqifP : cs2'L. case: eqP => [cs2E _ | /eqP cs2D Lcs2]. rewrite cs2E size_map cliftr_ldisk /=. have /leqifP := IHc1; case: eqP => [->_ |_ Lc1]. have /leqifP := IHc2; case: eqP => [->_ |_ Lc2]. apply/leqifP; case: eqP => [/(congr1 size)|[]]. by rewrite !size_cat /= !size_map => ->. by congr (_ ++ _ :: _); rewrite !cliftK. apply/leqifP; case: eqP => [/(congr1 size)|_]. by rewrite size_cat /= size_cat /= !size_map => ->. by rewrite ltn_add2l ltnS. apply/leqifP; case: eqP => [/(congr1 size)|_]. by rewrite !size_cat /= !size_map => ->. by rewrite -addSn leq_add // ltnS IHc2. apply/leqifP; case: eqP => [/(congr1 size)|_]. by rewrite !size_cat /= !size_map => ->. rewrite -addnS leq_add //= ?ltnS. by rewrite IHc1. by apply: leq_ltn_trans Lcs2; rewrite IHc2. have p3Ep : p3 = p by apply/eqP; rewrite opeg3E // lc1Dp. have p1Dp : p1 != p by rewrite eq_sym -p3Ep opeg3E // eqxx. apply/leqifP; case: eqP => [/(congr1 size)|_]. by rewrite !size_cat /= !size_map => ->. case: path3SP c2Pcs2 => // [c2' cs2' p2' cs2E c2'Pcs2' _| cs3 cs4 p4 p5 p6 c2' c3 p4Dp5 p4Rp5 lc2'cs3Epp6 cs2E c2'Pcs3 c3Pcs4 _]. case/eqP: p2Dp. have := lc1csEp. rewrite csE last_cat /= cs2E -[c2]cunliftrK last_map => /(congr1 f). by rewrite /f !cliftr_ldisk. have p4Ep2 : p4 = p2 by rewrite /p4 !cliftr_ldisk. have p5Ep1: p5 = p1. apply: (@lrel3ON4 p1 p p2 p5) => //; first by rewrite eq_sym. by rewrite -p4Ep2. have p6Ep3 : p6 = p3. by apply/eqP; rewrite /p6 opeg3E // p4Ep2 p5Ep1 p3Ep p2Dp. pose cs5 := [seq ↑[i]_p1 | i <- cs1] ++ cs4. have scs5Lscs : size cs5 < size cs. rewrite /cs5 csE cs2E !size_cat /= !size_cat /= !size_map. by rewrite ltn_add2l // !addnS! ltnS -addSn leq_addl. have c1Mcs5 : path lmove c1 cs5. rewrite cat_path -{1}[c1]cunliftrK /= !path_liftr //=. rewrite c1'Pcs1. rewrite -{1}[c1]cunliftrK last_map lc1'cs1Epp3 //. by rewrite -p6Ep3 -/p1 -p5Ep1. have lc1cs5E : last c1 cs5 = c. rewrite last_cat. rewrite -[c1]cunliftrK last_map lc1'cs1Epp3 //. rewrite -p6Ep3 -/p1 -p5Ep1 //. have := lc1csEp. by rewrite csE cs2E last_cat /= last_cat. apply: leq_trans (_ : size cs5 < _); last first. by rewrite cs2E /= !size_cat /= !size_map ltn_add2l //= ltnS -addSnnS leq_addl. rewrite ltnS. have /IHm : size cs5 < m. rewrite -ltnS. by apply: leq_ltn_trans Scs. move=> /(_ c1 c c1Mcs5 lc1cs5E) /=. by rewrite /= (negPf lc1Dp) p1Rp -/p1 size_cat /= !size_map => ->. have p2Dp : p2 != p by apply: contra p1NRp => /eqP<-. have p3Ep : p3 = p. by apply/eqP; rewrite opeg3E // lc1Dp. case: path3SP c2Pcs2 => // [c2' cs2' p2' cs2E c2'Pcs2' _| cs3 cs4 p4 p5 p6 c2' c3 p4Dp5 p4Rp5 lc2'cs3Epp6 cs2E c2'Pcs3 c3Pcs4 _]. case/eqP: p2Dp. move: lc1csEp. rewrite csE cs2E last_cat /= -[c2]cunliftrK last_map !cliftr_ldisk. by move => /(congr1 f); rewrite /f !cliftr_ldisk. rewrite cs2E /= size_cat !size_map /=. have Scs3 : size cs3 < m.+1. by apply: leq_trans Scs2; rewrite ltnS cs2E size_cat /= size_map leq_addr. have Scs4 : size cs4 < m.+1. by apply: leq_trans Scs2; rewrite ltnS cs2E size_cat /= -addSnnS leq_addl. have p4Ep2 : p4 = p2 by rewrite [LHS]cliftr_ldisk. case: (p5 =P p1) => [p5Ep1|/eqP p5Dp1]. apply/leqifP; case: eqP => [/(congr1 size)|_]. rewrite !size_cat /= size_cat !size_map size_cat /= !size_map => ->. by rewrite !(addSn, addnS) addnA. have p6Ep3 : p6 = p3. by rewrite /p6 /p3 opeg_sym; congr opeg. have lc1'cs1Ec3 : cliftr p1 (last c1' cs1) = c3. by rewrite lc1'cs1Epp3 -p6Ep3 -p5Ep1. pose cs5 := [seq ↑[i]_p1 | i <- cs1] ++ cs4. have scs5Lscs : size cs5 < size cs. rewrite /cs5 csE cs2E !size_cat /= !size_cat /= !size_map. by rewrite ltn_add2l // addnS !ltnS -addSn leq_addl. have c1Mcs5 : path lmove c1 cs5. rewrite cat_path -{1}[c1]cunliftrK /= !path_liftr //=. rewrite c1'Pcs1. rewrite -{1}[c1]cunliftrK last_map lc1'cs1Epp3 //. by rewrite -p6Ep3 -/p1 -p5Ep1. have lc1cs5E : last c1 cs5 = c. rewrite last_cat. rewrite -[c1]cunliftrK last_map lc1'cs1Epp3 //. rewrite -p6Ep3 -/p1 -p5Ep1 //. have := lc1csEp. by rewrite csE cs2E last_cat /= last_cat. apply: leq_trans (_ : size cs5 < _); last first. by rewrite !size_cat /= !size_map ltn_add2l //= ltnS -addSnnS leq_addl. have /IHm : size cs5 < m. rewrite -ltnS. by apply: leq_ltn_trans Scs. move=> /(_ c1 c c1Mcs5 lc1cs5E) /=. rewrite /= (negPf lc1Dp) (negPf p1NRp) -/p1 ltnS. by rewrite !size_cat /= size_cat /= !size_map => ->. have p5Ep : p5 = p. by apply/eqP; rewrite eq_sym -p3Ep opeg3E // eq_sym p5Dp1 -p4Ep2. have p2Ep1p : p2 = opeg p1 p. by apply/eqP; rewrite eq_sym opeg3E // p1Dp2 eq_sym p2Dp. have p6Ep1 : p6 = p1. by apply/eqP; rewrite opeg3E // p4Ep2 eq_sym p1Dp2. case: path3SP c3Pcs4 => // [c3' cs4' p8 cs4E c3'Pcs4' _| cs5 cs6 p8 p9 p10 c3' c4 p8Dp9 p8Rp9 lc3'cs5Epp10 cs4E c3'Pcs5 c4Pcs6 _]. have Scs4' : size cs4' < m.+1 by rewrite cs4E size_map in Scs4. rewrite cs4E size_map. rewrite csE cs2E last_cat /= last_cat /= -[c3]cunliftrK cs4E last_map in lc1csEp. have /(congr1 cunliftr) := lc1csEp. rewrite cliftrK => lc3'cs4'Ec'. have /IH := c1'Pcs1 => /(_ _ Scs1 lc1'cs1Epp3) IH1. rewrite p3Ep in IH1. have /IH := c2'Pcs3 => /(_ _ Scs3 lc2'cs3Epp6) IH2. rewrite [c2']cliftrK p3Ep p6Ep1 in IH2. have /IH := c3'Pcs4' => /(_ _ Scs4' lc3'cs4'Ec') IH3. rewrite [c3']cliftrK p6Ep1 in IH3. move /leqifP : IH1. case: eqP => [E1 _ | /eqP cs1D Lcs1]. have /leqifP := IH2; case: eqP => [E2 _ |_ Lc1]. have /leqifP := IH3; case: eqP => [E3 _ |_ Lc2]. apply/leqifP; case: eqP => [/(congr1 size)|[]]. rewrite !size_cat /= size_cat /= size_cat /= !size_map => ->. by rewrite !(addSn, addnS) addnA. congr (_ ++ _ :: _ ++ _ :: _). - by rewrite E1. - by rewrite /c2 p3Ep p2Ep1p. - by rewrite p4Ep2 -p2Ep1p E2. - by rewrite /c3 p6Ep1 p5Ep. - congr (map (cliftr _) _). by rewrite /p8 !cliftr_ldisk. by []. apply/leqifP; case: eqP => [/(congr1 size)|_]. rewrite !size_cat /= !size_cat /= !size_map => ->. by rewrite !(addSn, addnS) addnA. by rewrite E1 E2 !(addSn, addnS) !ltnS !ltn_add2l. apply/leqifP; case: eqP => [/(congr1 size)|_]. rewrite !size_cat /= !size_cat /= !size_map => ->. by rewrite !(addSn, addnS) addnA. rewrite E1 !(addSn, addnS) !ltnS !ltn_add2l. apply: leq_ltn_trans (_ : _ <= size (lhanoi3 `c[p, n] `c[p1]) + size cs4') _. by rewrite leq_add2l IH3. by rewrite ltn_add2r. apply/leqifP; case: eqP => [/(congr1 size)|_]. rewrite !size_cat /= !size_cat /= !size_map => ->. by rewrite !(addSn, addnS). by rewrite !(addSn, addnS) !ltnS -addSn !leq_add ?IH2 ?IH3. have p8Ep : p8 = p by rewrite [LHS]cliftr_ldisk. have p9Ep2 : p9 = p2. apply: lrel3ON4 p8Rp9. - by rewrite eq_sym; exact: p1Dp2. - by rewrite p8Ep. - by rewrite p8Ep. - by rewrite lsym. by rewrite p8Ep -p4Ep2 -p5Ep. have p10Ep1 : p10 = p1. by apply/eqP; rewrite opeg3E // p8Ep eq_sym lc1Dp p9Ep2 eq_sym. have cc : cliftr p2 (last c2' cs3) = c4. by rewrite /c4 lc2'cs3Epp6 p6Ep1 p10Ep1 p9Ep2. apply/leqifP; case: eqP => [/(congr1 size)|_]. rewrite !size_cat /= size_cat !size_map size_cat /= !size_map => ->. by rewrite !(addSn, addnS). pose cs7 := [seq ↑[i]_p1 | i <- cs1] ++ c2 :: [seq ↑[i]_p4 | i <- cs3] ++ cs6. have scs7Lscs7: size cs7 < size cs. rewrite /cs7 csE cs2E cs4E. rewrite size_cat /= size_cat /= size_cat /= size_cat /= size_cat /= !size_map. by rewrite !addnS ltnS -!addnS !leq_add2l addnS ltnS -addSnnS leq_addl. have c1Mcs7 : path lmove c1 cs7. rewrite cat_path -{1}[c1]cunliftrK /= !path_liftr //=. rewrite c1'Pcs1. rewrite -{1}[c1]cunliftrK last_map lc1'cs1Epp3 //. rewrite p4Ep2 cat_path /c2 -/p1 /=. apply/and3P; split => //. - apply: move_liftr_perfect => //. by rewrite eq_sym opegDl. by rewrite eq_sym opegDr. by rewrite path_liftr //; rewrite [c2']cliftrK in c2'Pcs3. by rewrite last_map; rewrite [c2']cliftrK in cc; rewrite cc. have lc1cs7E : last c1 cs7 = c. rewrite last_cat /= last_cat p4Ep2. rewrite -[c2]cunliftrK !cliftr_ldisk. rewrite last_map lc2'cs3Epp6. have := lc1csEp. rewrite csE cs2E cs4E last_cat /= last_cat /= last_cat /=. by rewrite /c4 p10Ep1 p6Ep1 p9Ep2. apply: leq_trans (_ : size cs7 < _); last first. rewrite !size_cat /= size_cat /= !size_map ltn_add2l //=. rewrite cs4E size_cat /= size_map !addnS !ltnS -addnS -addSn. by rewrite leq_add2l leq_addl. have /IHm : size cs7 < m. rewrite -ltnS. by apply: leq_ltn_trans Scs. move=> /(_ c1 c c1Mcs7 lc1cs7E) /=. rewrite /= (negPf lc1Dp) (negPf p1NRp) -/p1 ltnS. by rewrite size_cat /= size_cat /= !size_map => ->. Qed.
imports: mathcomp(all_ssreflect) hanoi(gdist ghanoi ghanoi3)