proposition: Lemma pathSP n (c : configuration n.+1) cs : pathS_spec c cs (path move c cs).
proof: Proof. have [Hp|_] := boolP (path _ _ _); last by apply: pathS_spec_false. pose f (c1 : configuration n.+1) := c1 ldisk != c ldisk. have [Hh|/hasPn Hn] := boolP (has f cs); last first. have csE : cs = [seq ↑[i]_(c ldisk) | i <- [seq ↓[i] | i <- cs]]. rewrite -map_comp -[LHS]map_id. apply/eq_in_map => x /Hn; rewrite negbK => /eqP <-/=. by rewrite cunliftrK. apply: pathS_specW csE _. by rewrite path_unlift_eq // => c1 /Hn; rewrite negbK => /eqP. pose n1 := find f cs; pose lc1 := nth c cs n1. pose p1 := c ldisk; pose p2 := lc1 ldisk. have p1Dp2 : p1 != p2. by have := nth_find c Hh; rewrite eq_sym. pose c1 := ↓[c]. pose lcs1 := take n1 cs; pose cs2 := drop n1.+1 cs. have slcs1 : size lcs1 = n1 by rewrite size_take -has_find Hh. have Plcs1 c2 : c2 \in lcs1 -> c2 ldisk = p1. move=> c2Ilcs1p; move: (c2Ilcs1p). rewrite -index_mem slcs1 => /(before_find c) /idP /negP. rewrite negbK => /eqP. by rewrite -[cs](cat_take_drop n1) nth_cat index_mem c2Ilcs1p nth_index. pose cs1 := map cunliftr lcs1. have lcs1E : lcs1 = [seq ↑[i]_p1 | i <- cs1]. rewrite -map_comp -[LHS]map_id. apply/eq_in_map => x /Plcs1 H. by rewrite /= -H cunliftrK. have csE : cs = [seq ↑[i]_p1 | i <- cs1] ++ lc1 :: cs2. by rewrite -[cs](cat_take_drop n1.+1) -cat_rcons -lcs1E (take_nth c) // -has_find. have Hm : move (last c lcs1) lc1. by move: Hp; rewrite csE lcs1E cat_path /= => /and3P[]. have lc1E : lc1 = cliftr p2 (last c1 cs1). rewrite /p2. have Hd : (last c lcs1) ldisk != lc1 ldisk. case: (lcs1) Plcs1 => //= a l -> //. by apply: mem_last. rewrite last_map -[LHS]cunliftrK. congr cliftr. apply/ffunP=> i; rewrite !ffunE /=. apply/sym_equal/(move_disk1 Hm Hd). apply/eqP/val_eqP => /=. by rewrite eqn_leq negb_and -ltnNge ltn_ord. have Hm1 : move ↑[last c1 cs1]_p1 ↑[last c1 cs1]_p2. have ->: ↑[last ↓[c] cs1]_p1 = last c lcs1. by rewrite -[in LHS]last_map -lcs1E cunliftrK. by rewrite -lc1E. apply: pathS_spec_move (p1Dp2) _ _ _ (Hm1) _ => //. - have := @move_diskr _ ldisk _ _ Hm1. by rewrite !cliftr_ldisk; apply. - by rewrite csE lc1E -lcs1E. - rewrite path_unlift_eq => //. by move: Hp; rewrite -[cs](cat_take_drop n1) cat_path => /andP[]. rewrite -lc1E. by move: Hp; rewrite csE cat_path /= => /and3P[]. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)