proposition: Lemma rpeg_min n (c : configuration 3 n) p cs : path rmove c cs -> last c cs = `c[p] -> size_rpeg c p <= size cs ?= iff (cs == rpeg c p).
proof: Proof. have [m sLm] := ubnP (size cs); elim: m => // m IHm in n c p cs sLm *. elim : n c p cs sLm => [c1 p [|] //=|n IH c1 p cs Scs c1Pcs lc1csEp /=]. case: (_ =P p) => [c1nEp |/eqP c1nDp]. have lcsnEc1n : last c1 cs ldisk = c1 ldisk. by rewrite lc1csEp !ffunE. have [cs1 [c1Pcs1 lcsElcs1 /leqifP]] := pathS_restrict (@rirr 3) c1Pcs. have lcs1P : last (↓[c1]) cs1 = `c[p]. by rewrite lcsElcs1 lc1csEp perfect_unliftr. case: eqP=> [csEcs1 /eqP<- |/eqP csDcs1 scs1L]. rewrite csEcs1 c1nEp eq_map_liftr. apply: IH => //. by move: Scs; rewrite csEcs1 size_map. apply/leqifP; case: eqP => [->|_]. by rewrite size_map size_rpegE. apply: leq_ltn_trans (scs1L). apply: IH => //. by apply: ltn_trans Scs. pose f (c : configuration 3 n.+1) := c ldisk. have HHr := @rirr 3. have HHs := @rsym 3. case: path3SP c1Pcs => // [c1' cs' p1 csE c1'Pcs' _| cs1 cs2 p1 p2 p3 c1' c2 p1Dp2 p1Rp2 lc1'cs1Epp3 csE c1'Pcs1 c2Pcs2 _]. case/eqP: c1nDp. move : lc1csEp; rewrite csE -[c1](cunliftrK) last_map => /(congr1 f). by rewrite /f !cliftr_ldisk !ffunE. rewrite csE size_cat -/p1. have p1Dp : p1 != p by []. 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. case: (p2 =P p) => [p2Ep|/eqP p2Dp]. pose c2' := ↓[c2]. have c2'Epp3 : c2' = `c[`p[p1, p2]] by rewrite [LHS]cliftrK. have/(pathS_restrict HHr)[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[p] => [| /(_ Scs2' c2'Pcs2') IHc2]. rewrite lc2'cs2'E -perfect_unliftr. by move: lc1csEp; rewrite csE last_cat /= => ->. rewrite -p2Ep in IHc2. move /leqifP : cs2'L. case: eqP => [cs2E _ | /eqP cs2D Lcs2]. rewrite cs2E size_map -p2Ep -/p3. have /leqifP := IHc1; case: eqP => [->_ |_ Lc1]. have /leqifP := IHc2; case: eqP => [->_ |_ Lc2]. apply/leqifP; case: eqP => [/(congr1 size)|[]]. rewrite !size_cat /= !size_map !addnS !size_rpegE c2'Epp3. by rewrite !rpeg_ppeg ?opegDr // size_ppeg -addnS prednK ?expn_gt0. congr (_ ++ _ :: _). by rewrite /c2' /c2 cliftrK cliftr_ldisk rpeg_ppeg // opegDr. apply/leqifP; case: eqP => [/(congr1 size)|_]. rewrite !size_cat /= !size_map !size_rpegE. by rewrite size_ppeg prednK ?expn_gt0 // => ->. rewrite /= size_rpegE ltn_add2l ltnS size_map. rewrite c2'Epp3 size_rpegE rpeg_ppeg ?opegDr // size_ppeg in Lc2. by rewrite prednK // expn_gt0 in Lc2. apply/leqifP; case: eqP => [/(congr1 size)|_]. rewrite !size_cat /= !size_map !size_rpegE => ->. by rewrite size_ppeg prednK // expn_gt0. rewrite /= -addSn leq_add // size_map -[_ ^ _]prednK ?expn_gt0 // ltnS. have := IHc2; rewrite c2'Epp3 size_rpegE rpeg_ppeg ?opegDr // size_ppeg. by move=>->. apply/leqifP; case: eqP => [/(congr1 size)|_]. rewrite !size_cat /= !size_map !size_rpegE. by rewrite size_ppeg prednK ?expn_gt0 // => ->. rewrite -addnS leq_add //= ?ltnS -?p2Ep. by rewrite size_map IHc1. rewrite -[_ ^ _]prednK ?expn_gt0 //. apply: leq_ltn_trans Lcs2. have := IHc2. by rewrite c2'Epp3 size_rpegE rpeg_ppeg ?opegDr // size_ppeg => ->. have p3Ep : p3 = p. by apply/eqP; rewrite opeg3E // p1Dp. apply/leqifP; case: eqP => [/(congr1 size)|_]. rewrite !size_cat /= !size_map !size_rpegE. by rewrite size_ppeg prednK ?expn_gt0 // => ->. case: path3SP c2Pcs2 => // [c2' cs2'|cs3 cs4]. rewrite !cliftr_ldisk /= => cs2E c2'Pcs2'. case/eqP: p2Dp. have := lc1csEp. rewrite csE last_cat /= => /(congr1 f). by rewrite /f cs2E last_map !cliftr_ldisk !ffunE. rewrite !cliftr_ldisk => p2'. rewrite {}/p2' => p4. set p5 := `p[p2, p4]; set c2' := ↓[c2]. move=> p2Dp4 p2Rp4 c2'cs5Epp5 cs2E c2'Pcs3 pp5p4Pcs4 _. case: (p5 =P p3) => [p5Ep3 /= | /eqP p5Dp3]. have p4Ep1: p4 = p1. move/eqP : p5Ep3; rewrite eq_sym // opeg3E // eq_sym //. by rewrite opeg3E // negb_and !negbK eq_sym (negPf p1Dp2) => /andP[/eqP] . pose cs5 := [seq ↑[i]_p1 | i <- cs1] ++ cs4. have scs5Lscs : size cs5 < size cs. rewrite /cs5 csE cs2E !size_cat /= !size_cat /= !size_map. rewrite ltn_add2l // !addnS! ltnS -addSn leq_addl //. have c1Mcs5 : path rmove c1 cs5. rewrite cat_path -[c1](cunliftrK) !path_liftr //=. rewrite c1'Pcs1. by rewrite last_map lc1'cs1Epp3 -/p1 -p5Ep3 -p4Ep1. have lc1cs5E : last c1 cs5 = `c[p]. rewrite last_cat -[c1](cunliftrK) last_map lc1'cs1Epp3. rewrite -lc1csEp csE cs2E last_cat /= last_cat /= -/p1. by rewrite p5Ep3 p4Ep1. 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 p c1Mcs5 lc1cs5E) /=. by rewrite -/p1 (negPf p1Dp) => ->. have [cs4' [pp5p4Pcs4' lpp5p4cs4'Elpp5p4cs4 scs4'L]] := pathS_restrict HHr pp5p4Pcs4. rewrite cliftrK in lpp5p4cs4'Elpp5p4cs4 pp5p4Pcs4'. have Scs3 : size cs3 < m.+1. apply: ltn_trans Scs2. by rewrite cs2E size_cat /= size_map addnS ltnS leq_addr. have Scs4 : size cs4 < m.+1. apply: ltn_trans Scs2. by rewrite cs2E size_cat /= size_map addnS ltnS leq_addl. have Scs4' : size cs4' < m.+1. by apply: leq_ltn_trans Scs4; rewrite scs4'L. rewrite cs2E /= size_cat /= !size_map. have /IH := c2'cs5Epp5 => /(_ Scs3 c2'Pcs3) IHc1. have c2'E : c2' = `c[p3] by rewrite [LHS]cliftrK. rewrite c2'E size_rpegE rpeg_ppeg // in IHc1; last by rewrite eq_sym. rewrite size_ppeg in IHc1. have p6Dp : p5 != p. by apply: contra p5Dp3 => /eqP->; apply/eqP. move: lc1csEp; rewrite csE cs2E. rewrite last_cat /= last_cat /= => lpp5p4cs4Epp. have lpp5cs4'Epp : last `c[p5] cs4' = `c[p]. by rewrite lpp5p4cs4'Elpp5p4cs4 lpp5p4cs4Epp perfect_unliftr. have /IH : last `c[p5] cs4' = `c[p] => [//| /(_ Scs4' pp5p4Pcs4') IHc2]. rewrite size_rpegE rpeg_ppeg // size_ppeg in IHc2. rewrite -[2 ^ n]prednK ?expn_gt0 //. rewrite !addnS !ltnS. apply: leq_trans (leq_addl _ _). apply: leq_add. by apply: leq_trans (size_rpeg_up _ _) _; rewrite IHc1. apply: leq_trans scs4'L. by rewrite IHc2. Qed.
imports: mathcomp(all_ssreflect) hanoi(extra gdist ghanoi ghanoi3)