proposition: Lemma rhanoi3_min n (c1 c2 : configuration 3 n) cs : path rmove c1 cs -> last c1 cs = c2 -> size (rhanoi3 c1 c2) <= size cs.
proof: Proof. have HHr := @rirr 3. have HHs := @rsym 3. elim: n c1 c2 cs => [p c1 [|]//|n IH c1 c2 cs /=]. set p := `p[_, _]; set p1 := _ ldisk; set p2 := _ ldisk. case: eqP => [p1Ep2 c1Pcs lc1csEc2|/eqP p1Dp2 c1Pcs lc1csEc2]. have lcsmEc1m : last c1 cs ldisk = p1 by rewrite lc1csEc2. have [cs1 [c1Pcs1 lc1csElcs1 /leq_of_leqif/(leq_trans _)->//]] := pathS_restrict (@rirr 3) c1Pcs. by rewrite size_map IH // lc1csElcs1 lc1csEc2. 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_map -size_rpegE -size_lpegE -/u => Lscs. by apply: leq_trans Lscs. apply: leq_ltn_trans _ Lscs. rewrite -addnS -addSn !addnA !leq_add //. by rewrite -[2 ^ _]prednK ?expn_gt0 // ltnS size_ppeg. pose f (c : configuration 3 n.+1) := c ldisk. have [m Lcs] := ubnP (size cs); elim: m => // m IH1 in cs Lcs c1Pcs lc1csEc2 *. case: path3SP c1Pcs => // [c1' cs' /= csE c1'Pcs' _| cs1 cs2 p1' p3 p4 c1' c3 p1Dp3 p1Rp3 lc1'cs1Epp4 csE c1'Pcs1 c3Pcs2 _]. case/eqP: p1Dp2. have := congr1 f lc1csEc2. rewrite /f csE -{1}[c1](cunliftrK) last_map. by rewrite !cliftr_ldisk. have p1'Ep1 : p1' = p1 by []. move: Lcs; rewrite csE size_cat size_map /= addnS ltnS => Lcs. move: lc1csEc2; rewrite csE last_cat /= => lc3cs2Ec2. have [/eqP p3Ep2 | p3Dp2] := boolP (p3 == p2). have p4Ep : p4 = p. apply/eqP; rewrite opeg3E // eq_sym opeg3E // negb_and !negbK eqxx /=. by rewrite eq_sym opeg3E // p1Dp3 eq_sym p3Ep2 eqxx. have [cs2' [pp4Pcs2' pp4cs2'E scs2'Lscs2]]:= pathS_restrict HHr c3Pcs2. rewrite cliftrK in pp4Pcs2' pp4cs2'E. apply: leq_trans (leq_add (leqnn _) scs2'Lscs2). apply: leq_trans (geq_minl _ _) _. apply: leq_add. apply: leq_of_leqif (rpeg_min _ _ ) => //. by rewrite lc1'cs1Epp4; congr `c[`p[_, _]]. apply: leq_of_leqif (lpeg_min _ _ ); rewrite -p4Ep //. by rewrite pp4cs2'E lc3cs2Ec2. have p3Ep : p3 = p. by apply/eqP; rewrite eq_sym opeg3E // -/p1 -p1'Ep1 p1Dp3 eq_sym. have p4Ep2 : p4 = p2. apply/eqP. rewrite /p4 p3Ep /p -/p1 -/p2 p1'Ep1 !opeg3E //. by rewrite p1Dp2 negbK eqxx. by rewrite eq_sym opeg3E // eqxx eq_sym. case: path3SP c3Pcs2=> // [c3' cs2' p5 cs2E c3'Pcs2' _| cs3 cs4 p5 p6 p7 c3' c4 p5Dp6 p5p6 c3'cs3Epp7 cs2E c3'Pcs3 c4Pcs4 _]. have := congr1 f lc3cs2Ec2. rewrite cs2E /f -[c3]cunliftrK last_map !cliftr_ldisk -/p2 /= => p3Ep2. by case/eqP: p3Dp2. have p5Ep: p5 = p by rewrite /p5 /c3 !cliftr_ldisk. move: lc3cs2Ec2 Lcs; rewrite cs2E last_cat /= size_cat /= size_map => lc6cs4Ec2 Lcs. rewrite -addSnnS ltnS. have [/eqP p6Ep1|p6Dp1] := boolP (p6 == p1). have p7Ep2 : p7 = p2. apply/eqP. by rewrite opeg3E // p5Ep p6Ep1 opeg3E // p1Dp2 eqxx. apply: leq_trans (_ : size (map (cliftr p1) cs1 ++ cs4) <= _). apply/ltnW/IH1. - by rewrite size_cat !size_map (leq_trans _ Lcs) // ltnS; rewrite leq_add2l -addSnnS leq_addl. - rewrite cat_path -{1}[c1]cunliftrK path_liftr //=. rewrite c1'Pcs1. by rewrite -{1}[c1]cunliftrK last_map lc1'cs1Epp4 -/p1 -p6Ep1 p4Ep2 -p7Ep2. rewrite last_cat -{1}[c1]cunliftrK last_map. by rewrite lc1'cs1Epp4 -/p1 -p6Ep1 p4Ep2 -p7Ep2. by rewrite size_cat size_map leq_add2l leq_addl. have p6Ep2 : p6 = p2. case: (p6 =P p2) => // /eqP p6Dp2. case/negP: p5Dp6. by rewrite p5Ep opeg3E // eq_sym p6Dp1 eq_sym. have p7Ep1 : p7 = p1. apply/eqP. by rewrite opeg3E // p5Ep opeg3E // eqxx. apply: leq_trans (geq_minr _ _) _. rewrite -[v]addnA leq_add //. apply: leq_of_leqif (rpeg_min _ _ ) => //. by rewrite lc1'cs1Epp4 p4Ep2. apply: leq_add. rewrite -[2 ^ _]prednK ?expn_gt0 // ltnS. have <-: size_rpeg (↓[c3]) p1 = (2 ^ n).-1. by rewrite cliftrK size_rpegE rpeg_ppeg ?opegDl // size_ppeg. apply: leq_of_leqif (rpeg_min _ _) => //. by rewrite c3'cs3Epp7 p7Ep1. have [cs4' [c4'Pcs4' lc4'cs4'Elc4cs4 /leq_of_leqif Lcs4']] := pathS_restrict HHr c4Pcs4. rewrite cliftrK p7Ep1 in c4'Pcs4'. rewrite cliftrK p7Ep1 in lc4'cs4'Elc4cs4. apply: leq_trans Lcs4'. apply: leq_of_leqif (lpeg_min _ _) => //. by rewrite lc4'cs4'Elc4cs4 lc6cs4Ec2. Qed.
imports: mathcomp(all_ssreflect) hanoi(extra gdist ghanoi ghanoi3)