proposition: Lemma ppeg_min n p1 p2 (cs : seq (configuration 3 n)) : p1 != p2 -> path rmove `c[p1] cs -> last `c[p1] cs = `c[p2] -> (2^ n).-1 <= size cs ?= iff (cs == ppeg p1 p2).
proof: Proof. have irrH := @rirr 3; have symH := @rsym 3. have [m sLm] := ubnP (size cs); elim: m => // m IHm in n p1 p2 cs sLm *. elim: n p1 p2 cs sLm => /= [p1 p2 [|] //|]n IH p1 p2 cs sLm p1Dp2. have /= := size_ppeg n.+1 p1 p2. case: path3SP => //. case: cs sLm => /= [_ _ _ _ _ /ffunP /(_ ldisk)/eqP|a cs sLm]. by rewrite !ffunE (negPf p1Dp2). rewrite !ffunE => acsE _ _ _ lacsE. have := mem_last a cs. rewrite acsE lacsE inE => /orP[/eqP/ffunP/(_ ldisk)/eqP|]. by rewrite cliftr_ldisk !ffunE eq_sym (negPf p1Dp2). case/mapP => c _ /ffunP /(_ ldisk)/eqP. by rewrite cliftr_ldisk ffunE eq_sym (negPf p1Dp2). rewrite !ffunE perfect_unliftr /= => cs1 cs2 p3 p1Dp3 _. move=> p1cs1Lp1p3 csE p1Pcs1. have Scs1 : size cs1 < m.+1. by apply: leq_trans sLm; rewrite csE size_cat size_map ltnS leq_addr. have p1Dp1p3 : p1 != `p[p1, p3] by rewrite eq_sym opegDl. have HL1 := IH _ _ _ Scs1 p1Dp1p3 p1Pcs1 p1cs1Lp1p3. have n2E : (2 ^ n.+1).-1 = (2 ^ n).-1 + (2 ^ n).-1.+1. by rewrite expnS mul2n -addnn -[2 ^ n]prednK ?expn_gt0. case: path3SP => //=. rewrite cliftr_ldisk cliftrK /=. move=> cs2E p1p3Pcs2 _ sH _ p1csLp2. have p3E : p3 = p2. move: p1csLp2; rewrite csE cs2E last_cat /= last_map. by move=> /ffunP /(_ ldisk); rewrite cliftr_ldisk ffunE. rewrite p3E in p1cs1Lp1p3 csE HL1 cs2E p1p3Pcs2. have Scs2 : size [seq ↓[i] | i <- cs2] < m.+1. apply: leq_trans sLm. by rewrite csE size_cat !size_map /= ltnS -addSnnS leq_addl. have p1p2Lcs2 : last `c[`p[p1, p2]] [seq ↓[i] | i <- cs2] = `c[p2]. rewrite -[`c[_]](cliftrK p2) last_map. by have := p1csLp2; rewrite csE last_cat /= => ->; rewrite perfect_unliftr. have HL2 := IH _ _ _ Scs2 (opegDr _ _) p1p3Pcs2 p1p2Lcs2. move/leqifP : HL1; case: eqP => [<- /eqP HL1|_ HL1]. move/leqifP : HL2; case: eqP => [<- /eqP HL2|_ HL2]. rewrite size_map in HL2. rewrite csE size_cat /= size_map -HL1 -HL2 -cs2E eqxx //= n2E. by apply/leqifP. apply/leqifP; case: eqP => [/(congr1 size)->|_]. by rewrite -sH !size_cat /= !size_map -HL1 size_ppeg. rewrite csE size_cat /= !size_map in HL2 *. by rewrite -HL1 n2E ltn_add2l. apply/leqifP; case: eqP => [/(congr1 size)->|_]; first by rewrite -sH. rewrite csE size_cat /= !size_map in HL2 *. by rewrite n2E -addSn leq_add // ltnS HL2. move=> cs3 cs4 p4; rewrite -!/rmove !cliftr_ldisk cliftrK. move => p3Dp4 _ p1p3cs3Lp3p4 cs2E p1p3Pcs3 p3p4Pcs4 _ sH _ p1csLp2. apply/leqifP; case: eqP => [/(congr1 size)|_]. by rewrite size_cat /= !size_map !size_ppeg n2E => ->. case: (p4 =P p1) => [p4Ep1 | /eqP p4Dp1]. rewrite p4Ep1 in p3Dp4 p1p3cs3Lp3p4 cs2E p3p4Pcs4. pose cs' := [seq ↑[i]_p1 | i <- cs1] ++ cs4. have Scs' : size cs' < size cs. rewrite csE /cs' cs2E !size_cat /= size_cat !size_map /=. by rewrite ltn_add2l -!addSnnS ltnS leq_addl. apply: leq_trans (Scs'); rewrite ltnS. rewrite (IHm _ p1 p2) //; first by rewrite (leq_trans Scs'). rewrite cat_path /= -[`c[_]](cunliftrK) ffunE perfect_unliftr. by rewrite path_liftr // p1Pcs1 /= last_map p1cs1Lp1p3 opeg_sym. rewrite last_cat /= -[`c[_]](cunliftrK) ffunE perfect_unliftr. rewrite last_map p1cs1Lp1p3. have := p1csLp2. by rewrite csE cs2E !last_cat /= last_cat /= opeg_sym. rewrite csE cs2E size_cat /= size_cat /= !size_map n2E !addnS !ltnS addnA. apply: leq_trans (leq_add _ _) (leq_addr _ _); first by rewrite HL1. have Scs3 : size cs3 < m.+1. apply: leq_trans sLm. rewrite csE cs2E size_cat /= size_cat /= !size_map addnC ltnS addnS !addSnnS. by rewrite -addnA leq_addr. rewrite (IH _ _ _ Scs3 _ p1p3Pcs3 p1p3cs3Lp3p4) //. by rewrite opeg3E // eq_sym opeg3E // eq_sym p1Dp3 p4Dp1 eq_sym opegDl. Qed.
imports: mathcomp(all_ssreflect) hanoi(extra gdist ghanoi ghanoi3)