Built with
Alectryon , running Coq+SerAPI v8.13.0+0.13.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
From mathcomp Require Import all_ssreflect.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
From hanoi Require Import extra gdist ghanoi ghanoi3.
Set Implicit Arguments .
Unset Strict Implicit .
Unset Printing Implicit Defensive .
Section Hanoi3 .
(*****************************************************************************)
(* The pegs are the three elements of 'I_3 *)
(*****************************************************************************)
Implicit Type p : peg 3 .
Local Notation "c1 `-->_r c2" := (rmove c1 c2)
(format "c1 `-->_r c2" , at level 60 ).
Local Notation "c1 `-->*_r c2" := (connect rmove c1 c2)
(format "c1 `-->*_r c2" , at level 60 ).
(******************************************************************************)
(* Function that builds a path from peg to peg *)
(******************************************************************************)
Fixpoint ppeg {n : nat} p1 p2 :=
if n isn't n1.+1 return seq (configuration 3 n) then [::] else
let p3 := `p[p1, p2] in
[seq ↑[i]_p1 | i <- ppeg p1 p3] ++
[seq ↑[i]_p2 | i <- `c[p3] :: ppeg p3 p2].
Lemma size_ppeg n p1 p2 :
size (ppeg p1 p2 : seq (configuration 3 n)) = (2 ^ n).-1 .size (ppeg p1 p2 : seq (configuration 3 n)) =
(2 ^ n).-1
Proof .2
elim : n p1 p2 => //= n IH p1 p2.5 IH : forall p1 p2 , size (ppeg p1 p2) = (2 ^ n).-1
6 size
([seq ↑[i]_p1 | i <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i]_p2 | i <- ppeg `p[p1, p2] p2]) =
(2 ^ n.+1 ).-1
rewrite size_cat /= !size_map !IH expnS mul2n -addnn.c (2 ^ n).-1 + (2 ^ n).-1 .+1 = (2 ^ n + 2 ^ n).-1
by rewrite -(prednK (_ : 0 < 2 ^ n)) // expn_gt0.
Qed .
Lemma last_ppeg n p1 p2 c (cs := ppeg p1 p2 : seq (configuration 3 n)) :
last c cs = `c[p2].5 6 c : configuration 3 n
cs := ppeg p1 p2 : seq (configuration 3 n) : seq (configuration 3 n)
last c cs = `c[p2]
Proof .14
have HH := @rirr 3 .5 6 17 18 HH : irreflexive (rrel (n:=3 ))
19
rewrite /cs; elim : n p1 p2 c {cs} => //= [_ p2 c | n IH p1 p2 c].1f p2 : peg 3
c : configuration 3 0
c = `c[p2]
by apply /ffunP=> [] [].
by rewrite last_cat /= last_map IH perfect_liftr.
Qed .
Lemma path_ppeg n p1 p2 (cs := ppeg p1 p2 : seq (configuration 3 n)) :
p1 != p2 -> path rmove `c[p1] cs.5 6 18
p1 != p2 -> path rmove `c[p1] cs
Proof .31
have HH := @rirr 3 .
rewrite /cs; elim : n p1 p2 {cs} => //= n IH p1 p2 p1Dp2.1f 5 IH : forall p1 p2 ,
p1 != p2 -> path rmove `c[p1] (ppeg p1 p2)
6 p1Dp2 : p1 != p2
path rmove `c[p1]
([seq ↑[i]_p1 | i <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i]_p2 | i <- ppeg `p[p1, p2] p2])
set p3 := `p[_,_].1f 5 3e 6 3f p3 := `p[p1, p2] : peg 3
path rmove `c[p1]
([seq ↑[i]_p1 | i <- ppeg p1 p3] ++
↑[`c[p3]]_p2 :: [seq ↑[i]_p2 | i <- ppeg p3 p2])
have p1Dp3 : p1 != p3 by rewrite eq_sym opegDl.
have p3Dp2 : p3 != p2 by rewrite opegDr.1f 5 3e 6 3f 45 4b p3Dp2 : p3 != p2
46
rewrite cat_path /= -{1 }[`c[p1]]cunliftrK ffunE !path_liftr // perfect_unliftr.4f [&& path (move (rrel (n:=3 ))) `c[p1] (ppeg p1 p3),
last `c[p1] [seq ↑[i]_p1 | i <- ppeg p1 p3] `-->_r ↑[`c[p3]]_p2
& path (move (rrel (n:=3 ))) `c[p3] (ppeg p3 p2)]
rewrite !IH // ?andbT /=.4f last `c[p1] [seq ↑[i]_p1 | i <- ppeg p1 p3] `-->_r ↑[`c[p3]]_p2
rewrite -{1 }[`c[_]]cunliftrK ffunE last_map perfect_unliftr last_ppeg.4f ↑[`c[p3]]_p1 `-->_r ↑[`c[p3]]_p2
by apply : move_liftr_perfect; rewrite // eq_sym opegDr.
Qed .
(* We can go from any perfect configuration to a perfect configuration *)
Lemma move_connect_ppeg n p1 p2 : `c[p1, n] `-->*_r `c[p2].4 `c[p1 , n] `-->*_r `c[p2]
Proof .5e
case : (p1 =P p2) => [->|/eqP p1Dp2] //.5 6 3f
`c[p1] `-->*_r `c[p2]
apply /connectP; exists (ppeg p1 p2 ); first by apply : path_ppeg.65 `c[p2] = last `c[p1] (ppeg p1 p2)
by rewrite last_ppeg.
Qed .
(* The proof is done by inspecting the moves that the last disk is doing in cs*)
(* We use a double induction : *)
(* The first induction is used when the path has duplicates *)
(* The second induction is on n and to bound recursive call *)
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).5 6 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 .6c
have irrH := @rirr 3 ; have symH := @rsym 3 .5 6 6f irrH : irreflexive (rrel (n:=3 ))
symH : symmetric (rrel (n:=3 ))
70
(* The first induction is used when the path has duplicates (1 case) *)
have [m sLm] := ubnP (size cs); elim : m => // m IHm in n p1 p2 cs sLm *.76 77 m : nat
IHm : forall (n : nat) p1 p2
(cs : seq (configuration 3 n)),
size cs < m ->
p1 != p2 ->
path rmove `c[p1] cs ->
last `c[p1] cs = `c[p2] ->
(2 ^ n).-1 <= size cs ?= iff (cs == ppeg p1 p2)
5 6 6f sLm : size cs < m.+1
70
elim : n p1 p2 cs sLm => /= [p1 p2 [|] //|]n IH p1 p2 cs sLm p1Dp2.76 77 7c 7d 5 IH : forall p1 p2 (cs : seq (configuration 3 n)),
size cs < m.+1 ->
p1 != p2 ->
path rmove `c[p1] cs ->
last `c[p1] cs = `c[p2] ->
(2 ^ n).-1 <= size cs ?= iff (cs == ppeg p1 p2)
6 cs : seq (configuration 3 n.+1 )
7e 3f path rmove `c[p1] cs ->
last `c[p1] cs = `c[p2] ->
(2 ^ n.+1 ).-1 <= size cs
?= iff (cs ==
[seq ↑[i]_p1
| i <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i]_p2
| i <- ppeg `p[p1, p2] p2])
have /= := size_ppeg n.+1 p1 p2.82 size
([seq ↑[i]_p1 | i <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i]_p2 | i <- ppeg `p[p1, p2] p2]) =
(2 ^ n.+1 ).-1 ->
path rmove `c[p1] cs ->
last `c[p1] cs = `c[p2] ->
(2 ^ n.+1 ).-1 <= size cs
?= iff (cs ==
[seq ↑[i]_p1
| i <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i]_p2
| i <- ppeg `p[p1, p2] p2])
(* Is there a move of the last first disk *)
case : path3SP => //.82 let c' := ↓[`c[p1]] in
let cs' := [seq ↓[i] | i <- cs] in
let p := `c[p1] ldisk in
cs = [seq ↑[i]_p | i <- cs'] ->
path (move (rrel (n:=3 ))) c' cs' ->
size
([seq ↑[i0]_p1 | i0 <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i0]_p2 | i0 <- ppeg `p[p1, p2] p2]) =
(2 ^ n.+1 ).-1 ->
true ->
last `c[p1] cs = `c[p2] ->
(2 ^ n.+1 ).-1 <= size cs
?= iff (cs ==
[seq ↑[i0]_p1
| i0 <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i0]_p2
| i0 <- ppeg `p[p1, p2] p2])
(* No move : impossible since p1 != p2 *)
case : cs sLm => /= [_ _ _ _ _ /ffunP /(_ ldisk)/eqP|a cs sLm].76 77 7c 7d 5 83 6 3f
`c[p1] ldisk == `c[p2] ldisk ->
(2 ^ n.+1 ).-1 <= 0
?= iff ([::] ==
[seq ↑[i]_p1
| i <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i]_p2
| i <- ppeg `p[p1, p2] p2])
by rewrite !ffunE (negPf p1Dp2).98 a :: cs =
↑[↓[a]]_(`c[p1] ldisk)
:: [seq ↑[i]_(`c[p1] ldisk)
| i <- [seq ↓[i] | i <- cs]] ->
move (rrel (n:=3 )) ↓[`c[p1]] ↓[a] &&
path (move (rrel (n:=3 ))) ↓[a] [seq ↓[i] | i <- cs] ->
size
([seq ↑[i0]_p1 | i0 <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i0]_p2 | i0 <- ppeg `p[p1, p2] p2]) =
(2 ^ n.+1 ).-1 ->
true ->
last a cs = `c[p2] ->
(2 ^ n.+1 ).-1 <= (size cs).+1
?= iff (a :: cs ==
[seq ↑[i0]_p1
| i0 <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i0]_p2
| i0 <- ppeg `p[p1, p2] p2])
8e
rewrite !ffunE => acsE _ _ _ lacsE.76 77 7c 7d 5 83 6 3f 99 84 9a acsE : a :: cs =
↑[↓[a]]_p1
:: [seq ↑[i]_p1 | i <- [seq ↓[i] | i <- cs]]
lacsE : last a cs = `c[p2]
(2 ^ n.+1 ).-1 <= (size cs).+1
?= iff (a :: cs ==
[seq ↑[i]_p1
| i <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i]_p2
| i <- ppeg `p[p1, p2] p2])
8e
have := mem_last a cs.a3 last a cs \in a :: cs ->
(2 ^ n.+1 ).-1 <= (size cs).+1
?= iff (a :: cs ==
[seq ↑[i]_p1
| i <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i]_p2
| i <- ppeg `p[p1, p2] p2])
8e
rewrite acsE lacsE inE => /orP[/eqP/ffunP/(_ ldisk)/eqP|].a3 `c[p2] ldisk == ↑[↓[a]]_p1 ldisk ->
(2 ^ n.+1 ).-1 <= (size cs).+1
?= iff (↑[↓[a]]_p1
:: [seq ↑[i]_p1
| i <- [seq ↓[i]
| i <- cs]] ==
[seq ↑[i]_p1
| i <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i]_p2
| i <- ppeg `p[p1, p2] p2])
by rewrite cliftr_ldisk !ffunE eq_sym (negPf p1Dp2).a3 `c[p2] \in [seq ↑[i]_p1 | i <- [seq ↓[i] | i <- cs]] ->
(2 ^ n.+1 ).-1 <= (size cs).+1
?= iff (↑[↓[a]]_p1
:: [seq ↑[i]_p1
| i <- [seq ↓[i]
| i <- cs]] ==
[seq ↑[i]_p1
| i <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i]_p2
| i <- ppeg `p[p1, p2] p2])
8e
case /mapP => c _ /ffunP /(_ ldisk)/eqP.76 77 7c 7d 5 83 6 3f 99 84 9a a4 a5 c : finfun_eqType (ordinal_finType n)
(ordinal_eqType 3 )
`c[p2] ldisk == ↑[c]_p1 ldisk ->
(2 ^ n.+1 ).-1 <= (size cs).+1
?= iff (↑[↓[a]]_p1
:: [seq ↑[i]_p1
| i <- [seq ↓[i]
| i <- cs]] ==
[seq ↑[i]_p1
| i <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i]_p2
| i <- ppeg `p[p1, p2] p2])
8e
by rewrite cliftr_ldisk ffunE eq_sym (negPf p1Dp2).82 forall (cs1 : seq (configuration 3 n))
(cs2 : seq (configuration 3 n.+1 )),
let p3 := `c[p1] ldisk in
forall p4 ,
let p5 := `p[p3, p4] in
let c1 := ↓[`c[p1]] in
let c2 := ↑[`c[p5]]_p4 in
p3 != p4 ->
rrel p3 p4 ->
last c1 cs1 = `c[p5] ->
cs = [seq ↑[i1]_p3 | i1 <- cs1] ++ c2 :: cs2 ->
path (move (rrel (n:=3 ))) c1 cs1 ->
path (move (rrel (n:=3 ))) c2 cs2 ->
size
([seq ↑[i3]_p1 | i3 <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i3]_p2 | i3 <- ppeg `p[p1, p2] p2]) =
(2 ^ n.+1 ).-1 ->
true ->
last `c[p1] cs = `c[p2] ->
(2 ^ n.+1 ).-1 <= size cs
?= iff (cs ==
[seq ↑[i3]_p1
| i3 <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i3]_p2
| i3 <- ppeg `p[p1, p2] p2])
(* There is a move from p1 to p3 *)
rewrite !ffunE perfect_unliftr /= => cs1 cs2 p3 p1Dp3 _.76 77 7c 7d 5 83 6 84 7e 3f cs1 : seq (configuration 3 n)
cs2 : seq (configuration 3 n.+1 )
p3 : peg 3
4b last `c[p1] cs1 = `c[`p[p1, p3]] ->
cs =
[seq ↑[i]_p1 | i <- cs1] ++
↑[`c[`p[p1, p3]]]_p3 :: cs2 ->
path (move (rrel (n:=3 ))) `c[p1] cs1 ->
path (move (rrel (n:=3 ))) ↑[`c[`p[p1, p3]]]_p3 cs2 ->
size
([seq ↑[i1]_p1 | i1 <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i1]_p2 | i1 <- ppeg `p[p1, p2] p2]) =
(2 ^ n.+1 ).-1 ->
true ->
last `c[p1] cs = `c[p2] ->
(2 ^ n.+1 ).-1 <= size cs
?= iff (cs ==
[seq ↑[i1]_p1
| i1 <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i1]_p2
| i1 <- ppeg `p[p1, p2] p2])
move => p1cs1Lp1p3 csE p1Pcs1.76 77 7c 7d 5 83 6 84 7e 3f c4 c5 c6 4b p1cs1Lp1p3 : last `c[p1] cs1 = `c[`p[p1, p3]]
csE : cs =
[seq ↑[i]_p1 | i <- cs1] ++
↑[`c[`p[p1, p3]]]_p3 :: cs2
p1Pcs1 : path (move (rrel (n:=3 ))) `c[p1] cs1
path (move (rrel (n:=3 ))) ↑[`c[`p[p1, p3]]]_p3 cs2 ->
size
([seq ↑[i0]_p1 | i0 <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i0]_p2 | i0 <- ppeg `p[p1, p2] p2]) =
(2 ^ n.+1 ).-1 ->
true ->
last `c[p1] cs = `c[p2] ->
(2 ^ n.+1 ).-1 <= size cs
?= iff (cs ==
[seq ↑[i0]_p1
| i0 <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i0]_p2
| i0 <- ppeg `p[p1, p2] p2])
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.76 77 7c 7d 5 83 6 84 7e 3f c4 c5 c6 4b cc cd ce d7 p1Dp1p3 : p1 != `p[p1, p3]
cf
(* After the first move, last disk is on p3, the other disk is `p[p1, p3] *)
have HL1 := IH _ _ _ Scs1 p1Dp1p3 p1Pcs1 p1cs1Lp1p3.76 77 7c 7d 5 83 6 84 7e 3f c4 c5 c6 4b cc cd ce d7 e0 HL1 : (2 ^ n).-1 <= size cs1
?= iff (cs1 == ppeg p1 `p[p1, p3])
cf
have n2E : (2 ^ n.+1 ).-1 = (2 ^ n).-1 + (2 ^ n).-1 .+1 .e4 (2 ^ n.+1 ).-1 = (2 ^ n).-1 + (2 ^ n).-1 .+1
by rewrite expnS mul2n -addnn -[2 ^ n]prednK ?expn_gt0 .
(* Is there another move *)
case : path3SP => //=.ec cs2 =
[seq ↑[i]_(↑[`c[`p[p1, p3]]]_p3 ldisk)
| i <- [seq ↓[i] | i <- cs2]] ->
path (move (rrel (n:=3 ))) ↓[↑[`c[`p[p1, p3]]]_p3]
[seq ↓[i] | i <- cs2] ->
true ->
size
([seq ↑[i1]_p1 | i1 <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i1]_p2 | i1 <- ppeg `p[p1, p2] p2]) =
(2 ^ n.+1 ).-1 ->
true ->
last `c[p1] cs = `c[p2] ->
(2 ^ n.+1 ).-1 <= size cs
?= iff (cs ==
[seq ↑[i1]_p1
| i1 <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i1]_p2
| i1 <- ppeg `p[p1, p2] p2])
(* there is no move so p3 = p2 and simple induction should make it *)
rewrite cliftr_ldisk cliftrK /=.ec cs2 = [seq ↑[i]_p3 | i <- [seq ↓[i] | i <- cs2]] ->
path (move (rrel (n:=3 ))) `c[`p[p1, p3]]
[seq ↓[i] | i <- cs2] ->
true ->
size
([seq ↑[i1]_p1 | i1 <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i1]_p2 | i1 <- ppeg `p[p1, p2] p2]) =
(2 ^ n.+1 ).-1 ->
true ->
last `c[p1] cs = `c[p2] ->
(2 ^ n.+1 ).-1 <= size cs
?= iff (cs ==
[seq ↑[i1]_p1
| i1 <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i1]_p2
| i1 <- ppeg `p[p1, p2] p2])
f5
move => cs2E p1p3Pcs2 _ sH _ p1csLp2.76 77 7c 7d 5 83 6 84 7e 3f c4 c5 c6 4b cc cd ce d7 e0 e5 ed cs2E : cs2 =
[seq ↑[i]_p3 | i <- [seq ↓[i] | i <- cs2]]
p1p3Pcs2 : path (move (rrel (n:=3 ))) `c[`p[p1, p3]]
[seq ↓[i] | i <- cs2]
sH : size
([seq ↑[i]_p1 | i <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i]_p2 | i <- ppeg `p[p1, p2] p2]) =
(2 ^ n.+1 ).-1
p1csLp2 : last `c[p1] cs = `c[p2]
(2 ^ n.+1 ).-1 <= size cs
?= iff (cs ==
[seq ↑[i]_p1
| i <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i]_p2
| i <- ppeg `p[p1, p2] p2])
f5
have p3E : p3 = p2.
move : p1csLp2; rewrite csE cs2E last_cat /= last_map.76 77 7c 7d 5 83 6 84 7e 3f c4 c5 c6 4b cc cd ce d7 e0 e5 ed 100 101 102
↑[last `c[`p[p1, p3]] [seq ↓[i] | i <- cs2]]_p3 =
`c[p2] -> p3 = p2
109
by move => /ffunP /(_ ldisk); rewrite cliftr_ldisk ffunE.
rewrite p3E in p1cs1Lp1p3 csE HL1 cs2E p1p3Pcs2.76 77 7c 7d 5 83 6 84 7e 3f c4 c5 c6 4b ce d7 e0 ed 102 103 10c p1cs1Lp1p3 : last `c[p1] cs1 = `c[`p[p1, p2]]
csE : cs =
[seq ↑[i]_p1 | i <- cs1] ++
↑[`c[`p[p1, p2]]]_p2 :: cs2
HL1 : (2 ^ n).-1 <= size cs1
?= iff (cs1 == ppeg p1 `p[p1, p2])
cs2E : cs2 =
[seq ↑[i]_p2 | i <- [seq ↓[i] | i <- cs2]]
p1p3Pcs2 : path (move (rrel (n:=3 ))) `c[`p[p1, p2]]
[seq ↓[i] | i <- cs2]
104 f5
have Scs2 : size [seq ↓[i] | i <- cs2] < m.+1 .119 size [seq ↓[i] | i <- cs2] < m.+1
apply : leq_trans sLm.76 77 7c 7d 5 83 6 84 3f c4 c5 c6 4b ce d7 e0 ed 102 103 10c 11a 11b 11c 11d 11e
size [seq ↓[i] | i <- cs2] < (size cs).+1
123
by rewrite csE size_cat !size_map /= ltnS -addSnnS leq_addl.
have p1p2Lcs2 : last `c[`p[p1, p2]] [seq ↓[i] | i <- cs2] = `c[p2].125 last `c[`p[p1, p2]] [seq ↓[i] | i <- cs2] = `c[p2]
rewrite -[`c[_]](cliftrK p2) last_map.125 ↓[last ↑[`c[`p[p1, p2]]]_p2 cs2] = `c[p2]
133
by have := p1csLp2; rewrite csE last_cat /= => ->; rewrite perfect_unliftr.
have HL2 := IH _ _ _ Scs2 (opegDr _ _) p1p3Pcs2 p1p2Lcs2.76 77 7c 7d 5 83 6 84 7e 3f c4 c5 c6 4b ce d7 e0 ed 102 103 10c 11a 11b 11c 11d 11e 126 136 HL2 : (2 ^ n).-1 <= size [seq ↓[i] | i <- cs2]
?= iff ([seq ↓[i] | i <- cs2] ==
ppeg `p[p1, p2] p2)
104 f5
move /leqifP : HL1; case : eqP => [<- /eqP HL1|_ HL1].76 77 7c 7d 5 83 6 84 7e 3f c4 c5 c6 4b ce d7 e0 ed 102 103 10c 11a 11b 11d 11e 126 136 142 HL1 : (2 ^ n).-1 = size cs1
(2 ^ n.+1 ).-1 <= size cs
?= iff (cs ==
[seq ↑[i]_p1 | i <- cs1] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i]_p2
| i <- ppeg `p[p1, p2] p2])
move /leqifP : HL2; case : eqP => [<- /eqP HL2|_ HL2].76 77 7c 7d 5 83 6 84 7e 3f c4 c5 c6 4b ce d7 e0 ed 102 103 10c 11a 11b 11d 11e 126 136 147 HL2 : (2 ^ n).-1 = size [seq ↓[i] | i <- cs2]
(2 ^ n.+1 ).-1 <= size cs
?= iff (cs ==
[seq ↑[i]_p1 | i <- cs1] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i]_p2
| i <- [seq ↓[i]
| i <- cs2]])
rewrite size_map in HL2.76 77 7c 7d 5 83 6 84 7e 3f c4 c5 c6 4b ce d7 e0 ed 102 103 10c 11a 11b 11d 11e 126 136 147 HL2 : (2 ^ n).-1 = size cs2
152 153
rewrite csE size_cat /= size_map -HL1 -HL2 -cs2E eqxx //= n2E.15b (2 ^ n).-1 + (2 ^ n).-1 .+1 <= (2 ^ n).-1 +
(2 ^ n).-1 .+1
?= iff true
153
by apply /leqifP.
apply /leqifP; case : eqP => [/(congr1 size)->|_].155 (2 ^ n.+1 ).-1 ==
size
([seq ↑[i]_p1 | i <- cs1] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i]_p2 | i <- ppeg `p[p1, p2] p2])
by rewrite -sH !size_cat /= !size_map -HL1 size_ppeg.
rewrite csE size_cat /= !size_map in HL2 *.76 77 7c 7d 5 83 6 84 7e 3f c4 c5 c6 4b ce d7 e0 ed 102 103 10c 11a 11b 11d 11e 126 136 147 HL2 : (2 ^ n).-1 < size cs2
(2 ^ n.+1 ).-1 < size cs1 + (size cs2).+1
149
by rewrite -HL1 n2E ltn_add2l.
apply /leqifP; case : eqP => [/(congr1 size)->|_]; first by rewrite -sH.
rewrite csE size_cat /= !size_map in HL2 *.76 77 7c 7d 5 83 6 84 7e 3f c4 c5 c6 4b ce d7 e0 ed 102 103 10c 11a 11b 11d 11e 126 136 14c HL2 : (2 ^ n).-1 <= size cs2
?= iff ([seq ↓[i] | i <- cs2] ==
ppeg `p[p1, p2] p2)
173 f5
by rewrite n2E -addSn leq_add // ltnS HL2.ec forall (cs1 : seq (configuration 3 n))
(cs3 : seq (configuration 3 n.+1 )) p4 ,
↑[`c[`p[p1, p3]]]_p3 ldisk != p4 ->
rrel (↑[`c[`p[p1, p3]]]_p3 ldisk) p4 ->
last ↓[↑[`c[`p[p1, p3]]]_p3] cs1 =
`c[`p[↑[`c[`p[p1, p3]]]_p3 ldisk, p4]] ->
cs2 =
[seq ↑[i1]_(↑[`c[`p[p1, p3]]]_p3 ldisk) | i1 <- cs1] ++
↑[`c[`p[↑[`c[`p[p1, p3]]]_p3 ldisk, p4]]]_p4 :: cs3 ->
path (move (rrel (n:=3 ))) ↓[↑[`c[`p[p1, p3]]]_p3] cs1 ->
path (move (rrel (n:=3 )))
↑[`c[`p[↑[`c[`p[p1, p3]]]_p3 ldisk, p4]]]_p4 cs3 ->
true ->
size
([seq ↑[i4]_p1 | i4 <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i4]_p2 | i4 <- ppeg `p[p1, p2] p2]) =
(2 ^ n.+1 ).-1 ->
true ->
last `c[p1] cs = `c[p2] ->
(2 ^ n.+1 ).-1 <= size cs
?= iff (cs ==
[seq ↑[i4]_p1
| i4 <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i4]_p2
| i4 <- ppeg `p[p1, p2] p2])
move => cs3 cs4 p4; rewrite -!/rmove !cliftr_ldisk cliftrK.76 77 7c 7d 5 83 6 84 7e 3f c4 c5 c6 4b cc cd ce d7 e0 e5 ed cs3 : seq (configuration 3 n)
cs4 : seq (configuration 3 n.+1 )
p4 : peg 3
p3 != p4 ->
rrel p3 p4 ->
last `c[`p[p1, p3]] cs3 = `c[`p[p3, p4]] ->
cs2 =
[seq ↑[i1]_p3 | i1 <- cs3] ++
↑[`c[`p[p3, p4]]]_p4 :: cs4 ->
path rmove `c[`p[p1, p3]] cs3 ->
path rmove ↑[`c[`p[p3, p4]]]_p4 cs4 ->
true ->
size
([seq ↑[i4]_p1 | i4 <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i4]_p2 | i4 <- ppeg `p[p1, p2] p2]) =
(2 ^ n.+1 ).-1 ->
true ->
last `c[p1] cs = `c[p2] ->
(2 ^ n.+1 ).-1 <= size cs
?= iff (cs ==
[seq ↑[i4]_p1
| i4 <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i4]_p2
| i4 <- ppeg `p[p1, p2] p2])
move => p3Dp4 _ p1p3cs3Lp3p4 cs2E p1p3Pcs3 p3p4Pcs4 _ sH _ p1csLp2.76 77 7c 7d 5 83 6 84 7e 3f c4 c5 c6 4b cc cd ce d7 e0 e5 ed 187 188 189 p3Dp4 : p3 != p4
p1p3cs3Lp3p4 : last `c[`p[p1, p3]] cs3 =
`c[`p[p3, p4]]
cs2E : cs2 =
[seq ↑[i]_p3 | i <- cs3] ++
↑[`c[`p[p3, p4]]]_p4 :: cs4
p1p3Pcs3 : path rmove `c[`p[p1, p3]] cs3
p3p4Pcs4 : path rmove ↑[`c[`p[p3, p4]]]_p4 cs4
102 103 104
(* we did two moves of the largest disk so we cannot be = *)
apply /leqifP; case : eqP => [/(congr1 size)|_].18e size cs =
size
([seq ↑[i]_p1 | i <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i]_p2 | i <- ppeg `p[p1, p2] p2]) ->
(2 ^ n.+1 ).-1 == size cs
by rewrite size_cat /= !size_map !size_ppeg n2E => ->.
(* Did we come back to p1 *)
case : (p4 =P p1) => [p4Ep1 | /eqP p4Dp1].76 77 7c 7d 5 83 6 84 7e 3f c4 c5 c6 4b cc cd ce d7 e0 e5 ed 187 188 189 18f 190 191 192 193 102 103 p4Ep1 : p4 = p1
16a
rewrite p4Ep1 in p3Dp4 p1p3cs3Lp3p4 cs2E p3p4Pcs4.76 77 7c 7d 5 83 6 84 7e 3f c4 c5 c6 4b cc cd ce d7 e0 e5 ed 187 188 189 192 102 103 1a1 p3Dp4 : p3 != p1
p1p3cs3Lp3p4 : last `c[`p[p1, p3]] cs3 =
`c[`p[p3, p1]]
cs2E : cs2 =
[seq ↑[i]_p3 | i <- cs3] ++
↑[`c[`p[p3, p1]]]_p1 :: cs4
p3p4Pcs4 : path rmove ↑[`c[`p[p3, p1]]]_p1 cs4
16a 1a2
(* if so cs has a repetition so we can use IHm *)
pose cs' := [seq ↑[i]_p1 | i <- cs1] ++ cs4.76 77 7c 7d 5 83 6 84 7e 3f c4 c5 c6 4b cc cd ce d7 e0 e5 ed 187 188 189 192 102 103 1a1 1aa 1ab 1ac 1ad cs' := [seq ↑[i]_p1 | i <- cs1] ++ cs4 : seq (configuration 3 n.+1 )
16a 1a2
have Scs' : size cs' < size cs.
rewrite csE /cs' cs2E !size_cat /= size_cat !size_map /=.1b1 size cs1 + size cs4 <
size cs1 + (size cs3 + (size cs4).+1 ).+1
1b7
by rewrite ltn_add2l -!addSnnS ltnS leq_addl.
apply : leq_trans (Scs'); rewrite ltnS.1b9 (2 ^ n.+1 ).-1 <= size cs'
1a2
rewrite (IHm _ p1 p2) //; first by rewrite (leq_trans Scs').
rewrite cat_path /= -[`c[_]](cunliftrK) ffunE perfect_unliftr.1b9 path rmove ↑[`c[p1]]_p1 [seq ↑[i]_p1 | i <- cs1] &&
path rmove
(last ↑[`c[p1]]_p1 [seq ↑[i]_p1 | i <- cs1]) cs4
1ca
by rewrite path_liftr // p1Pcs1 /= last_map p1cs1Lp1p3 opeg_sym.
rewrite last_cat /= -[`c[_]](cunliftrK) ffunE perfect_unliftr.1b9 last (last ↑[`c[p1]]_p1 [seq ↑[i]_p1 | i <- cs1]) cs4 =
`c[p2]
1a2
rewrite last_map p1cs1Lp1p3.1b9 last ↑[`c[`p[p1, p3]]]_p1 cs4 = `c[p2]
1a2
have := p1csLp2.1b9 last `c[p1] cs = `c[p2] ->
last ↑[`c[`p[p1, p3]]]_p1 cs4 = `c[p2]
1a2
by rewrite csE cs2E !last_cat /= last_cat /= opeg_sym.
rewrite csE cs2E size_cat /= size_cat /= !size_map n2E !addnS !ltnS addnA.1a4 (2 ^ n).-1 + (2 ^ n).-1 <=
size cs1 + size cs3 + size cs4
apply : leq_trans (leq_add _ _) (leq_addr _ _); first by rewrite HL1.1a4 (2 ^ n).-1 <= size cs3
have Scs3 : size cs3 < m.+1 .
apply : leq_trans sLm.76 77 7c 7d 5 83 6 84 3f c4 c5 c6 4b cc cd ce d7 e0 e5 ed 187 188 189 18f 190 191 192 193 102 103 1a5
size cs3 < (size cs).+1
1ef
rewrite csE cs2E size_cat /= size_cat /= !size_map addnC ltnS addnS !addSnnS.1f6 size cs3 <= size cs3 + size cs4 + (size cs1).+2
1ef
by rewrite -addnA leq_addr.
rewrite (IH _ _ _ Scs3 _ p1p3Pcs3 p1p3cs3Lp3p4) //.1f1 `p[p1, p3] != `p[p3, p4]
by rewrite opeg3E // eq_sym opeg3E // eq_sym p1Dp3 p4Dp1 eq_sym opegDl.
Qed .
Lemma gdist_rhanoi3p n p1 p2 :
`d[`c[p1, n], `c[p2]]_rmove = (2 ^ n).-1 * (p1 != p2).4 `d[`c[p1 , n], `c[p2]]_rmove = (2 ^ n).-1 * (p1 != p2)
Proof .204
case : eqP => [<-|/eqP p1Dp2]; first by rewrite muln0 gdist0.65 `d[`c[p1], `c[p2]]_rmove = (2 ^ n).-1 * ~~ false
rewrite muln1.65 `d[`c[p1], `c[p2]]_rmove = (2 ^ n).-1
apply /eqP; rewrite eqn_leq -(size_ppeg n p1 p2).65 `d[`c[p1], `c[p2]]_rmove <= size (ppeg p1 p2) <=
`d[`c[p1], `c[p2]]_rmove
rewrite gdist_path_le //=; last 2 first .65 path rmove `c[p1] (ppeg p1 p2)
- 215
by apply : path_ppeg.
- 21f
by rewrite last_ppeg.
have /gpath_connect [cs csH] : connect rmove `c[p1, n] `c[p2].
by apply : move_connect_ppeg.
rewrite size_ppeg (gpath_dist csH) /=.
apply : ppeg_min p1Dp2 (gpath_path csH) _ => //.5 6 22b 22c
last `c[p1] cs = `c[p2]
by apply : gpath_last csH.
Qed .
(*****************************************************************************)
(* Function that builds a path from a configuration to a peg *)
(*****************************************************************************)
Fixpoint rpeg {n : nat} :=
if n is n1.+1 return configuration 3 n -> peg 3 -> seq (configuration 3 n)
then
fun c p =>
let p1 := c ldisk in
if p1 == p then [seq ↑[i]_p | i <- rpeg ↓[c] p] else
let p2 := `p[p1, p] in
[seq ↑[i]_p1 | i <- rpeg ↓[c] p2] ++
[seq ↑[i]_p | i <- `c[p2] :: ppeg p2 p]
else fun _ _ => [::].
Lemma rpeg_perfect n p : rpeg (`c[p]) p = [::] :> seq (configuration 3 n).
Proof .23a
elim : n => //= n IH.23d 5 IH : rpeg `c[p] p = [::]
(if `c[p] ldisk == p
then [seq ↑[i]_p | i <- rpeg ↓[`c[p]] p]
else
[seq ↑[i]_(`c[p] ldisk)
| i <- rpeg ↓[`c[p]] `p[`c[p] ldisk, p]] ++
↑[`c[`p[`c[p] ldisk, p]]]_p
:: [seq ↑[i]_p | i <- ppeg `p[`c[p] ldisk, p] p]) =
[::]
by rewrite ffunE eqxx perfect_unliftr IH.
Qed .
Lemma rpeg_nil_inv n c p : rpeg c p = [::] -> c = `c[p] :> configuration _ n.5 17 23d
rpeg c p = [::] -> c = `c[p]
Proof .247
elim : n c => [c _|n IH c] /=; first by apply /ffunP=> [] [].23d 5 IH : forall c : configuration 3 n,
rpeg c p = [::] -> c = `c[p]
2b (if c ldisk == p
then [seq ↑[i]_p | i <- rpeg ↓[c] p]
else
[seq ↑[i]_(c ldisk) | i <- rpeg ↓[c] `p[c ldisk, p]] ++
↑[`c[`p[c ldisk, p]]]_p
:: [seq ↑[i]_p | i <- ppeg `p[c ldisk, p] p]) = [::] ->
c = `c[p]
case : eqP => [H | H] //=; last by case : map.[seq ↑[i]_p | i <- rpeg ↓[c] p] = [::] -> c = `c[p]
rewrite -{2 }[c]cunliftrK.255 [seq ↑[i]_p | i <- rpeg ↓[c] p] = [::] ->
↑[↓[c]]_(c ldisk) = `c[p]
case : rpeg (IH (↓[c])) => // -> // _.255 ↑[`c[p]]_(c ldisk) = `c[p]
by rewrite H perfect_liftr.
Qed .
Lemma rpeg_ppeg n p1 p2 : p1 != p2 -> rpeg `c[p1, n] p2 = ppeg p1 p2.4 p1 != p2 -> rpeg `c[p1 , n] p2 = ppeg p1 p2
Proof .261
elim : n p1 p2 => //= n IH p1 p2 p1Dp2.5 IH : forall p1 p2 ,
p1 != p2 -> rpeg `c[p1] p2 = ppeg p1 p2
6 3f (if `c[p1] ldisk == p2
then [seq ↑[i]_p2 | i <- rpeg ↓[`c[p1]] p2]
else
[seq ↑[i]_(`c[p1] ldisk)
| i <- rpeg ↓[`c[p1]] `p[`c[p1] ldisk, p2]] ++
↑[`c[`p[`c[p1] ldisk, p2]]]_p2
:: [seq ↑[i]_p2 | i <- ppeg `p[`c[p1] ldisk, p2] p2]) =
[seq ↑[i]_p1 | i <- ppeg p1 `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i]_p2 | i <- ppeg `p[p1, p2] p2]
by rewrite ffunE perfect_unliftr (negPf p1Dp2) !IH // eq_sym opegDl.
Qed .
Lemma last_rpeg n (c : configuration 3 n) p (cs := rpeg c p) :
last c cs = `c[p].5 17 23d cs := rpeg c p : seq (configuration 3 n)
last c cs = `c[p]
Proof .26c
rewrite /cs; elim : n c p {cs} => /= [c p| n IH c p].
by apply /ffunP=> [] [].
case : eqP => [Ho|/eqP Do].last c [seq ↑[i]_p | i <- rpeg ↓[c] p] = `c[p]
by rewrite -{1 }[c](cunliftrK) Ho last_map IH perfect_liftr.
by rewrite last_cat /= last_map last_ppeg perfect_liftr.
Qed .
Lemma path_rpeg n (c : configuration 3 n) p (cs := rpeg c p) :
path rmove c cs.
Proof .28e
have HH := @rirr 3 .
rewrite /cs; elim : n c p {cs} => //= n IH c p.1f 5 IH : forall (c : configuration 3 n) p ,
path rmove c (rpeg c p)
2b 23d path rmove c
(if c ldisk == p
then [seq ↑[i]_p | i <- rpeg ↓[c] p]
else
[seq ↑[i]_(c ldisk)
| i <- rpeg ↓[c] `p[c ldisk, p]] ++
↑[`c[`p[c ldisk, p]]]_p
:: [seq ↑[i]_p | i <- ppeg `p[c ldisk, p] p])
case : eqP => [Ho|/eqP Do].1f 5 29a 2b 23d 283
path rmove c [seq ↑[i]_p | i <- rpeg ↓[c] p]
by rewrite -{1 }[c](cunliftrK) Ho path_liftr.
set c2 := `c[_].1f 5 29a 2b 23d 288 c2 := `c[`p[c ldisk, p]] : configuration 3 n
path rmove c
([seq ↑[i]_(c ldisk)
| i <- rpeg ↓[c] `p[c ldisk, p]] ++
↑[c2]_p
:: [seq ↑[i]_p | i <- ppeg `p[c ldisk, p] p])
rewrite cat_path /= -{1 }[c]cunliftrK !path_liftr // IH path_ppeg ?opegDr //.2ab [&& true,
last c
[seq ↑[i]_(c ldisk)
| i <- rpeg ↓[c] `p[c ldisk, p]] `-->_r ↑[c2]_p
& true]
rewrite andbT /=.2ab last c
[seq ↑[i]_(c ldisk) | i <- rpeg ↓[c] `p[c ldisk, p]] `-->_r ↑[c2]_p
rewrite -{1 }[c]cunliftrK last_map last_rpeg -/c2.2ab ↑[c2]_(c ldisk) `-->_r ↑[c2]_p
apply : move_liftr_perfect => //; first by rewrite eq_sym (opegDl _).
by rewrite eq_sym (opegDr _).
Qed .
(* We can go from any configuration to a perfect configuration *)
Lemma move_connect_rpeg n (c : configuration _ n) p : c `-->*_r `c[p].
Proof .2bf
apply /connectP; exists (rpeg c p ); first by apply : path_rpeg.249 `c[p] = last c (rpeg c p)
by rewrite last_rpeg.
Qed .
(* So we can also from a perfect configuration c to any configuration *)
Lemma move_connect_lpeg n (c : configuration _ n) p : `c[p] `-->*_r c.
Proof .2c8
rewrite [connect _ _ _]connect_sym //.249 connect (move (rrel (n:=3 ))) c `c[p]
by apply : move_connect_rpeg.
by exact : rsym.
Qed .
(* Two configurations are always connected *)
Lemma move_connect n (c1 c2 : configuration 3 n) : c1 `-->*_r c2.5 c1, c2 : configuration 3 n
c1 `-->*_r c2
Proof .2d7
by apply : connect_trans (move_connect_rpeg c1 (inord 1 ))
(move_connect_lpeg c2 (inord 1 )).
Qed .
(******************************************************************************)
(* Function that builds a path from a configuration to a peg *)
(******************************************************************************)
(*****************************************************************************)
(* Computes the size of rpeg *)
(*****************************************************************************)
Fixpoint size_rpeg {n : nat} : (configuration _ n) -> _ -> nat :=
match n with
| 0 => fun _ _ => 0
| n1.+1 =>
fun c p =>
let p1 := c ldisk in
if p1 == p then size_rpeg ↓[c] p else
let p2 := `p[p1, p] in size_rpeg ↓[c] p2 + 2 ^ n1
end .
Lemma size_rpegE n p (c : _ _ n) : size_rpeg c p = size (rpeg c p).5 23d 17
size_rpeg c p = size (rpeg c p)
Proof .2de
elim : n p c => //= n IH p c.5 IH : forall p (c : configuration 3 n),
size_rpeg c p = size (rpeg c p)
23d 2b (if c ldisk == p
then size_rpeg ↓[c] p
else size_rpeg ↓[c] `p[c ldisk, p] + 2 ^ n) =
size
(if c ldisk == p
then [seq ↑[i]_p | i <- rpeg ↓[c] p]
else
[seq ↑[i]_(c ldisk)
| i <- rpeg ↓[c] `p[c ldisk, p]] ++
↑[`c[`p[c ldisk, p]]]_p
:: [seq ↑[i]_p | i <- ppeg `p[c ldisk, p] p])
case : eqP => [clEp|/eqP clDp]; first by rewrite size_map IH.5 2e7 23d 2b clDp : c ldisk != p
size_rpeg ↓[c] `p[c ldisk, p] + 2 ^ n =
size
([seq ↑[i]_(c ldisk)
| i <- rpeg ↓[c] `p[c ldisk, p]] ++
↑[`c[`p[c ldisk, p]]]_p
:: [seq ↑[i]_p | i <- ppeg `p[c ldisk, p] p])
by rewrite size_cat /= !size_map size_ppeg prednK ?expn_gt0 // IH.
Qed .
(* Upper bound on the size *)
Lemma size_rpeg_up n (c : _ _ n) p : size_rpeg c p <= (2 ^ n).-1 .249 size_rpeg c p <= (2 ^ n).-1
Proof .2f0
elim : n c p => //= n IH c p.5 IH : forall (c : configuration 3 n) p ,
size_rpeg c p <= (2 ^ n).-1
2b 23d (if c ldisk == p
then size_rpeg ↓[c] p
else size_rpeg ↓[c] `p[c ldisk, p] + 2 ^ n) <=
(2 ^ n.+1 ).-1
case : eqP => _.2f7 size_rpeg ↓[c] p <= (2 ^ n.+1 ).-1
apply : (leq_trans (IH _ _)).2f7 (2 ^ n).-1 <= (2 ^ n.+1 ).-1
2fe
case : (_ ^ _) (expn_eq0 2 n) (expn_eq0 2 n.+1 )
(leq_pexp2l (isT: 0 < 2 ) (ltnW (leqnn n.+1 ))) => //= n1 _.(2 ^ n.+1 == 0 ) = false ->
n1 < 2 ^ n.+1 -> n1 <= (2 ^ n.+1 ).-1
2fe
by case : (_ ^ _).
apply : leq_trans (_ : (2 ^n).-1 + (2 ^n) <= _).2f7 size_rpeg ↓[c] `p[c ldisk, p] + 2 ^ n <=
(2 ^ n).-1 + 2 ^ n
by rewrite leq_add2r IH.
rewrite expnS mul2n -addnn.2f7 (2 ^ n).-1 + 2 ^ n <= (2 ^ n + 2 ^ n).-1
by case : (2 ^ n) (expn_eq0 2 n) => [|n1]; rewrite ?addn0 .
Qed .
(* rpeg gives the smallest path to a perfect configuration. *)
(* This path is unique *)
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).5 17 23d 6f
path rmove c cs ->
last c cs = `c[p] ->
size_rpeg c p <= size cs ?= iff (cs == rpeg c p)
Proof .31d
(* As we want this statememnt to hold for any configuration c1 *)
(* and not just for initial perfect configuration the proof is more *)
(* intricate. We need a double induction : *)
(* The first induction is used when the path has duplicates (1 case) *)
have [m sLm] := ubnP (size cs); elim : m => // m IHm in n c p cs sLm *.7c IHm : forall (n : nat) (c : configuration 3 n) p (cs : seq (configuration 3 n)),
size cs < m ->
path rmove c cs ->
last c cs = `c[p] -> size_rpeg c p <= size cs ?= iff (cs == rpeg c p)
5 17 23d 6f 7e 320
(* The usual induction on the number of disks *)
elim : n c p cs sLm => [c1 p [|] //=|n IH c1 p cs Scs c1Pcs lc1csEp /=].7c 326 5 IH : forall (c : configuration 3 n) p
(cs : seq (configuration 3 n)),
size cs < m.+1 ->
path rmove c cs ->
last c cs = `c[p] ->
size_rpeg c p <= size cs ?= iff (cs == rpeg c p)
c1 : configuration 3 n.+1
23d 84 Scs : size cs < m.+1
c1Pcs : path rmove c1 cs
lc1csEp : last c1 cs = `c[p]
(if c1 ldisk == p
then size_rpeg ↓[c1] p
else size_rpeg ↓[c1] `p[c1 ldisk, p] + 2 ^ n) <=
size cs
?= iff
(cs ==
(if
c1
ldisk ==
p
then
[
seq ↑[i]_p
| i <-
rpeg
↓[c1]
p]
else
[
seq ↑[i]_
(c1
ldisk)
| i <-
rpeg
↓[c1]
`p[
c1
ldisk, p]] ++
↑[`c[`p[
c1
ldisk, p]]]_p
:: [
seq ↑[i]_p
| i <-
ppeg
`p[
c1
ldisk, p]
p]))
case : (_ =P p) => [c1nEp |/eqP c1nDp].7c 326 5 32b 32c 23d 84 32d 32e 32f c1nEp : c1 ldisk = p
size_rpeg ↓[c1] p <= size cs
?= iff (cs ==
[seq ↑[i]_p
| i <- rpeg ↓[c1] p])
(* the largest disk is already well-placed *)
have lcsnEc1n : last c1 cs ldisk = c1 ldisk.334 last c1 cs ldisk = c1 ldisk
by rewrite lc1csEp !ffunE.7c 326 5 32b 32c 23d 84 32d 32e 32f 335 345
336 337
have [cs1 [c1Pcs1 lcsElcs1 /leqifP]] :=
pathS_restrict (@rirr 3 ) c1Pcs.7c 326 5 32b 32c 23d 84 32d 32e 32f 335 345 c4 c1Pcs1 : path (move (rrel (n:=3 ))) ↓[c1] cs1
lcsElcs1 : last ↓[c1] cs1 = ↓[last c1 cs]
(if cs == [seq ↑[i]_(c1 ldisk) | i <- cs1]
then size cs1 == size cs
else size cs1 < size cs) ->
size_rpeg ↓[c1] p <= size cs
?= iff (cs ==
[seq ↑[i]_p
| i <- rpeg ↓[c1] p])
337
have lcs1P : last (↓[c1]) cs1 = `c[p].34e last ↓[c1] cs1 = `c[p]
by rewrite lcsElcs1 lc1csEp perfect_unliftr.7c 326 5 32b 32c 23d 84 32d 32e 32f 335 345 c4 34f 350 359
351 337
case : eqP=> [csEcs1 /eqP<- |/eqP csDcs1 scs1L].7c 326 5 32b 32c 23d 84 32d 32e 32f 335 345 c4 34f 350 359 csEcs1 : cs = [seq ↑[i]_(c1 ldisk) | i <- cs1]
size_rpeg ↓[c1] p <= size cs1
?= iff (cs ==
[seq ↑[i]_p
| i <- rpeg ↓[c1] p])
rewrite csEcs1 c1nEp eq_map_liftr.362 size_rpeg ↓[c1] p <= size cs1
?= iff (cs1 == rpeg ↓[c1] p)
365
apply : IH => //.7c 326 5 32c 23d 84 32d 32e 32f 335 345 c4 34f 350 359 363
d3 365
by move : Scs; rewrite csEcs1 size_map.7c 326 5 32b 32c 23d 84 32d 32e 32f 335 345 c4 34f 350 359 368 369
336 337
apply /leqifP; case : eqP => [->|_].375 size_rpeg ↓[c1] p ==
size [seq ↑[i]_p | i <- rpeg ↓[c1] p]
by rewrite size_map size_rpegE.
apply : leq_ltn_trans (scs1L).375 size_rpeg ↓[c1] p <= size cs1
337
apply : IH => //.7c 326 5 32c 23d 84 32d 32e 32f 335 345 c4 34f 350 359 368 369
d3 337
by apply : ltn_trans Scs.7c 326 5 32b 32c 23d 84 32d 32e 32f 33c
size_rpeg ↓[c1] `p[c1 ldisk, p] + 2 ^ n <= size cs
?= iff (cs ==
[seq ↑[i]_
(c1
ldisk)
| i <-
rpeg
↓[c1]
`p[
c1
ldisk, p]] ++
↑[`c[`p[
c1
ldisk, p]]]_p
:: [
seq ↑[i]_p
| i <-
ppeg
`p[
c1
ldisk, p]
p])
pose f (c : configuration 3 n.+1 ) := c ldisk.7c 326 5 32b 32c 23d 84 32d 32e 32f 33c f := fun_of_fin^~ ldisk : configuration 3 n.+1 -> (fun => peg 3 ) ldisk
38c
have HHr := @rirr 3 .7c 326 5 32b 32c 23d 84 32d 32e 32f 33c 391 HHr : irreflexive (rrel (n:=3 ))
38c
have HHs := @rsym 3 .7c 326 5 32b 32c 23d 84 32d 32e 32f 33c 391 396 HHs : symmetric (rrel (n:=3 ))
38c
(* We need to move the largest disk *)
case : path3SP c1Pcs => // [c1' cs' p1 csE c1'Pcs' _|
cs1 cs2 p1 p2 p3 c1' c2
p1Dp2 p1Rp2 lc1'cs1Epp3 csE c1'Pcs1 c2Pcs2 _].7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c1' := ↓[c1] : configuration 3 n
cs' := [seq ↓[i] | i <- cs] : seq (configuration 3 n)
p1 := c1 ldisk : peg 3
csE : cs = [seq ↑[i]_p1 | i <- cs']
c1'Pcs' : path (move (rrel (n:=3 ))) c1' cs'
38c
(* this case is impossible the largest disk has to move *)
case /eqP: c1nDp.7c 326 5 32b 32c 23d 84 32d 32f 391 396 39b 3a0 3a1 3a2 3a3 3a4
c1 ldisk = p
3a5
move : lc1csEp; rewrite csE -[c1](cunliftrK) last_map => /(congr1 f).7c 326 5 32b 32c 23d 84 32d 391 396 39b 3a0 3a1 3a2 3a3 3a4
f ↑[last ↓[c1] cs']_(c1 ldisk) = f `c[p] ->
↑[↓[c1]]_(c1 ldisk) ldisk = p
3a5
by rewrite /f !cliftr_ldisk !ffunE.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3ad
38c
(* c2 is the first configuration when the largest disk has moved *)
rewrite csE size_cat -/p1.3bb size_rpeg ↓[c1] `p[p1, p] + 2 ^ n <= size
[seq ↑[i]_p1
| i <- cs1] +
size (c2 :: cs2)
?= iff ([seq ↑[i]_p1
| i <- cs1] ++
c2 :: cs2 ==
[seq ↑[i]_p1
| i <-
rpeg ↓[c1]
`p[p1, p]] ++
↑[`c[`p[p1, p]]]_p
:: [seq ↑[i]_p
| i <-
ppeg
`p[p1, p]
p])
have p1Dp : p1 != p by [].7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3ad p1Dp : p1 != p
3bf
have Scs1 : size cs1 < m.+1 .
apply : ltn_trans Scs.7c 326 5 32b 32c 23d 84 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3ad 3c4
size cs1 < size cs
3c8
by rewrite csE size_cat /= size_map addnS ltnS leq_addr.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3ad 3c4 d7
3bf
have Scs2 : size cs2 < m.+1 .
apply : ltn_trans Scs.7c 326 5 32b 32c 23d 84 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3ad 3c4 d7
size cs2 < size cs
3d9
by rewrite csE size_cat /= size_map addnS ltnS leq_addl.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3ad 3c4 d7 3dc
3bf
case : (p2 =P p) => [p2Ep|/eqP p2Dp].7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3ad 3c4 d7 3dc p2Ep : p2 = p
3bf
pose c2' := ↓[c2].7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3ad 3c4 d7 3dc 3ea c2' := ↓[c2] : configuration 3 n
3bf 3eb
have c2'Epp3 : c2' = `c[`p[p1, p2]] by rewrite [LHS]cliftrK.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3ad 3c4 d7 3dc 3ea 3f3 c2'Epp3 : c2' = `c[`p[p1, p2]]
3bf 3eb
(* the first moves of largest disk of cs is the right one *)
have /(pathS_restrict HHr)[cs2' [c2'Pcs2' lc2'cs2'E cs2'L]] := c2Pcs2.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3ad 3c4 d7 3dc 3ea 3f3 3f8 cs2' : seq (configuration 3 n)
c2'Pcs2' : path (move (rrel (n:=3 ))) ↓[c2] cs2'
lc2'cs2'E : last ↓[c2] cs2' = ↓[last c2 cs2]
cs2'L : size cs2' <= size cs2
?= iff (cs2 ==
[seq ↑[i]_
(c2 ldisk)
| i <- cs2'])
3bf 3eb
have Scs2' : size cs2' < m.+1 .
by apply : leq_ltn_trans Scs2; rewrite cs2'L.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3ad 3c4 d7 3dc 3ea 3f3 3f8 3fd 3fe 3ff 400 408
3bf 3eb
have /IH := lc1'cs1Epp3 => // /(_ Scs1 c1'Pcs1) IHc1.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3ad 3c4 d7 3dc 3ea 3f3 3f8 3fd 3fe 3ff 400 408 IHc1 : size_rpeg c1' p3 <= size cs1
?= iff
(cs1 == rpeg c1' p3)
3bf 3eb
have /IH : last c2' cs2' = `c[p] => [| /(_ Scs2' c2'Pcs2') IHc2].
rewrite lc2'cs2'E -perfect_unliftr.410 ↓[last c2 cs2] = ↓[`c[p]]
416
by move : lc1csEp; rewrite csE last_cat /= => ->.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3ad 3c4 d7 3dc 3ea 3f3 3f8 3fd 3fe 3ff 400 408 411 419
3bf 3eb
rewrite -p2Ep in IHc2.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3ad 3c4 d7 3dc 3ea 3f3 3f8 3fd 3fe 3ff 400 408 411 IHc2 : size_rpeg c2' p2 <= size cs2'
?= iff
(cs2' == rpeg c2' p2)
3bf 3eb
move /leqifP : cs2'L.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3ad 3c4 d7 3dc 3ea 3f3 3f8 3fd 3fe 3ff 408 411 426
(if cs2 == [seq ↑[i]_(c2 ldisk) | i <- cs2']
then size cs2' == size cs2
else size cs2' < size cs2) ->
size_rpeg ↓[c1] `p[p1, p] + 2 ^ n <= size
[seq ↑[i]_p1
| i <- cs1] +
size (c2 :: cs2)
?= iff ([seq ↑[i]_p1
| i <- cs1] ++
c2 :: cs2 ==
[seq ↑[i]_p1
| i <-
rpeg ↓[c1]
`p[p1, p]] ++
↑[`c[`p[p1, p]]]_p
:: [seq ↑[i]_p
| i <-
ppeg
`p[p1, p]
p])
3eb
case : eqP => [cs2E _ | /eqP cs2D Lcs2].7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3ad 3c4 d7 3dc 3ea 3f3 3f8 3fd 3fe 3ff 408 411 426 cs2E : cs2 = [seq ↑[i]_(c2 ldisk) | i <- cs2']
3bf
(* there is only one move of the largest disk in cs *)
rewrite cs2E size_map -p2Ep -/p3.42f size_rpeg ↓[c1] p3 + 2 ^ n <= size cs1 +
size
(c2
:: [seq ↑[i]_(c2
ldisk)
| i <- cs2'])
?= iff ([seq ↑[i]_p1
| i <- cs1] ++
c2
:: [seq ↑[i]_(c2
ldisk)
| i <- cs2'] ==
[seq ↑[i]_p1
| i <- rpeg
↓[c1]
p3] ++
↑[`c[p3]]_p2
:: [seq ↑[i]_p2
| i <- ppeg
p3 p2])
431
have /leqifP := IHc1; case : eqP => [->_ |_ Lc1].42f size_rpeg ↓[c1] p3 + 2 ^ n <= size (rpeg c1' p3) +
size
(c2
:: [seq ↑[i]_(c2
ldisk)
| i <- cs2'])
?= iff ([seq ↑[i]_p1
| i <- rpeg c1'
p3] ++
c2
:: [seq ↑[i]_(c2
ldisk)
| i <- cs2'] ==
[seq ↑[i]_p1
| i <- rpeg
↓[c1]
p3] ++
↑[`c[p3]]_p2
:: [seq ↑[i]_p2
| i <- ppeg
p3 p2])
(* the first part of cs is perfect *)
have /leqifP := IHc2; case : eqP => [->_ |_ Lc2].42f size_rpeg ↓[c1] p3 + 2 ^ n <= size (rpeg c1' p3) +
size
(c2
:: [seq ↑[i]_(c2
ldisk)
| i <- rpeg c2'
p2])
?= iff ([seq ↑[i]_p1
| i <- rpeg c1'
p3] ++
c2
:: [seq ↑[i]_(c2
ldisk)
| i <- rpeg
c2'
p2] ==
[seq ↑[i]_p1
| i <- rpeg
↓[c1]
p3] ++
↑[`c[p3]]_p2
:: [seq ↑[i]_p2
| i <- ppeg
p3 p2])
(* the second part of cs is perfect, only case of equality *)
apply /leqifP; case : eqP => [/(congr1 size)|[]].42f size
([seq ↑[i]_p1 | i <- rpeg c1' p3] ++
c2 :: [seq ↑[i]_(c2 ldisk) | i <- rpeg c2' p2]) =
size
([seq ↑[i]_p1 | i <- rpeg ↓[c1] p3] ++
↑[`c[p3]]_p2 :: [seq ↑[i]_p2 | i <- ppeg p3 p2]) ->
size_rpeg ↓[c1] p3 + 2 ^ n ==
size (rpeg c1' p3) +
size (c2 :: [seq ↑[i]_(c2 ldisk) | i <- rpeg c2' p2])
rewrite !size_cat /= !size_map !addnS !size_rpegE c2'Epp3.42f (size (rpeg c1' p3) + size (rpeg `c[`p[p1, p2]] p2)).+1 =
(size (rpeg c1' p3) + size (ppeg p3 p2)).+1 ->
size (rpeg ↓[c1] p3) + 2 ^ n ==
(size (rpeg c1' p3) + size (rpeg `c[`p[p1, p2]] p2)).+1
450
by rewrite !rpeg_ppeg ?opegDr // size_ppeg -addnS prednK ?expn_gt0 .
congr (_ ++ _ :: _).42f [seq ↑[i]_(c2 ldisk) | i <- rpeg c2' p2] =
[seq ↑[i]_p2 | i <- ppeg p3 p2]
447
by rewrite /c2' /c2 cliftrK cliftr_ldisk rpeg_ppeg // opegDr.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3ad 3c4 d7 3dc 3ea 3f3 3f8 3fd 3fe 3ff 408 411 426 430 44a
43d 43e
apply /leqifP; case : eqP => [/(congr1 size)|_].462 size
([seq ↑[i]_p1 | i <- rpeg c1' p3] ++
c2 :: [seq ↑[i]_(c2 ldisk) | i <- cs2']) =
size
([seq ↑[i]_p1 | i <- rpeg ↓[c1] p3] ++
↑[`c[p3]]_p2 :: [seq ↑[i]_p2 | i <- ppeg p3 p2]) ->
size_rpeg ↓[c1] p3 + 2 ^ n ==
size (rpeg c1' p3) +
size (c2 :: [seq ↑[i]_(c2 ldisk) | i <- cs2'])
rewrite !size_cat /= !size_map !size_rpegE.462 size (rpeg c1' p3) + (size cs2').+1 =
size (rpeg c1' p3) + (size (ppeg p3 p2)).+1 ->
size (rpeg ↓[c1] p3) + 2 ^ n ==
size (rpeg c1' p3) + (size cs2').+1
467
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.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3ad 3c4 d7 3dc 3ea 3f3 3f8 3fd 3fe 3ff 408 411 426 430 Lc2 : (2 ^ n).-1 < size cs2'
474 43e
by rewrite prednK // expn_gt0 in Lc2.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3ad 3c4 d7 3dc 3ea 3f3 3f8 3fd 3fe 3ff 408 411 426 430 441
439 431
apply /leqifP; case : eqP => [/(congr1 size)|_].47d size
([seq ↑[i]_p1 | i <- cs1] ++
c2 :: [seq ↑[i]_(c2 ldisk) | i <- cs2']) =
size
([seq ↑[i]_p1 | i <- rpeg ↓[c1] p3] ++
↑[`c[p3]]_p2 :: [seq ↑[i]_p2 | i <- ppeg p3 p2]) ->
size_rpeg ↓[c1] p3 + 2 ^ n ==
size cs1 +
size (c2 :: [seq ↑[i]_(c2 ldisk) | i <- cs2'])
rewrite !size_cat /= !size_map !size_rpegE => ->.47d size (rpeg ↓[c1] p3) + 2 ^ n ==
size (rpeg ↓[c1] p3) + (size (ppeg p3 p2)).+1
482
by rewrite size_ppeg prednK // expn_gt0.
rewrite /= -addSn leq_add // size_map -[_ ^ _]prednK ?expn_gt0 // ltnS.47d (2 ^ n).-1 <= size cs2'
431
have := IHc2; rewrite c2'Epp3 size_rpegE rpeg_ppeg ?opegDr // size_ppeg.47d (2 ^ n).-1 <= size cs2'
?= iff (cs2' == ppeg `p[p1, p2] p2) ->
(2 ^ n).-1 <= size cs2'
431
by move =>->.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3ad 3c4 d7 3dc 3ea 3f3 3f8 3fd 3fe 3ff 408 411 426 434 435
3bf 3eb
apply /leqifP; case : eqP => [/(congr1 size)|_].497 size ([seq ↑[i]_p1 | i <- cs1] ++ c2 :: cs2) =
size
([seq ↑[i]_p1 | i <- rpeg ↓[c1] `p[p1, p]] ++
↑[`c[`p[p1, p]]]_p
:: [seq ↑[i]_p | i <- ppeg `p[p1, p] p]) ->
size_rpeg ↓[c1] `p[p1, p] + 2 ^ n ==
size [seq ↑[i]_p1 | i <- cs1] + size (c2 :: cs2)
rewrite !size_cat /= !size_map !size_rpegE.497 size cs1 + (size cs2).+1 =
size (rpeg ↓[c1] `p[p1, p]) +
(size (ppeg `p[p1, p] p)).+1 ->
size (rpeg ↓[c1] `p[p1, p]) + 2 ^ n ==
size cs1 + (size cs2).+1
49c
by rewrite size_ppeg prednK ?expn_gt0 // => ->.
rewrite -addnS leq_add //= ?ltnS -?p2Ep .497 size_rpeg ↓[c1] `p[p1, p2] <=
size [seq ↑[i]_p1 | i <- cs1]
by rewrite size_map IHc1.
rewrite -[_ ^ _]prednK ?expn_gt0 //.497 (2 ^ n).-1 < size cs2
3eb
apply : leq_ltn_trans Lcs2.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3ad 3c4 d7 3dc 3ea 3f3 3f8 3fd 3fe 3ff 408 411 426 434
48f 3eb
have := IHc2.4b7 size_rpeg c2' p2 <= size cs2'
?= iff (cs2' == rpeg c2' p2) ->
(2 ^ n).-1 <= size cs2'
3eb
by rewrite c2'Epp3 size_rpegE rpeg_ppeg ?opegDr // size_ppeg => ->.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3ad 3c4 d7 3dc 3ee
3bf
(* The largest disk jumped to an intermediate peg *)
have p3Ep : p3 = p.
by apply /eqP; rewrite opeg3E // p1Dp.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3ad 3c4 d7 3dc 3ee 4c7
3bf
(* cs cannot be optimal *)
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].7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 3f3 cs2' := [seq ↓[i] | i <- cs2] : seq (configuration 3 n)
let p0 := c2 ldisk in
cs2 = [seq ↑[i]_p0 | i <- cs2'] ->
path (move (rrel (n:=3 ))) c2' cs2' ->
true ->
size_rpeg ↓[c1] `p[p1, p] + 2 ^ n <
size [seq ↑[i0]_p1 | i0 <- cs1] + size (c2 :: cs2)
(* this is impossible we need another move of the largest disk *)
rewrite !cliftr_ldisk /= => cs2E c2'Pcs2'.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 3f3 4db cs2E : cs2 = [seq ↑[i]_p2 | i <- cs2']
c2'Pcs2' : path (move (rrel (n:=3 ))) c2' cs2'
true ->
size_rpeg ↓[c1] `p[p1, p] + 2 ^ n <
size [seq ↑[i]_p1 | i <- cs1] + (size cs2).+1
4dd
case /eqP: p2Dp.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 4c7 3f3 4db 4e5 4e6
p2 = p
4dd
have := lc1csEp.4eb last c1 cs = `c[p] -> p2 = p
4dd
rewrite csE last_cat /= => /(congr1 f).4eb f (last c2 cs2) = f `c[p] -> p2 = p
4dd
by rewrite /f cs2E last_map !cliftr_ldisk !ffunE.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 187 188
4e0
rewrite !cliftr_ldisk => p2'.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 187 188 p2' := p2 : peg 3
forall p2 ,
let p3 := `p[p2', p2] in
let c3 := ↓[c2] in
let c4 := ↑[`c[p3]]_p2 in
p2' != p2 ->
rrel p2' p2 ->
last c3 cs3 = `c[p3] ->
cs2 = [seq ↑[i1]_p2' | i1 <- cs3] ++ c4 :: cs4 ->
path (move (rrel (n:=3 ))) c3 cs3 ->
path (move (rrel (n:=3 ))) c4 cs4 ->
true ->
size_rpeg ↓[c1] `p[p1, p] + 2 ^ n <
size [seq ↑[i3]_p1 | i3 <- cs1] + size (c2 :: cs2)
rewrite {}/p2' => p4.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 187 188 189
p2 != p4 ->
rrel p2 p4 ->
last ↓[c2] cs3 = `c[`p[p2, p4]] ->
cs2 =
[seq ↑[i1]_p2 | i1 <- cs3] ++
↑[`c[`p[p2, p4]]]_p4 :: cs4 ->
path (move (rrel (n:=3 ))) ↓[c2] cs3 ->
path (move (rrel (n:=3 ))) ↑[`c[`p[p2, p4]]]_p4 cs4 ->
true ->
size_rpeg ↓[c1] `p[p1, p] + 2 ^ n <
size [seq ↑[i3]_p1 | i3 <- cs1] + size (c2 :: cs2)
set p5 := `p[p2, p4]; set c2' := ↓[c2].7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 187 188 189 p5 := `p[p2, p4] : peg 3
3f3 p2 != p4 ->
rrel p2 p4 ->
last c2' cs3 = `c[p5] ->
cs2 =
[seq ↑[i1]_p2 | i1 <- cs3] ++ ↑[`c[p5]]_p4 :: cs4 ->
path (move (rrel (n:=3 ))) c2' cs3 ->
path (move (rrel (n:=3 ))) ↑[`c[p5]]_p4 cs4 ->
true ->
size_rpeg ↓[c1] `p[p1, p] + 2 ^ n <
size [seq ↑[i3]_p1 | i3 <- cs1] + size (c2 :: cs2)
move => p2Dp4 p2Rp4 c2'cs5Epp5 cs2E c2'Pcs3 pp5p4Pcs4 _.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 187 188 189 508 3f3 p2Dp4 : p2 != p4
p2Rp4 : rrel p2 p4
c2'cs5Epp5 : last c2' cs3 = `c[p5]
cs2E : cs2 =
[seq ↑[i]_p2 | i <- cs3] ++ ↑[`c[p5]]_p4 :: cs4
c2'Pcs3 : path (move (rrel (n:=3 ))) c2' cs3
pp5p4Pcs4 : path (move (rrel (n:=3 ))) ↑[`c[p5]]_p4 cs4
49e
case : (p5 =P p3) => [p5Ep3 /= | /eqP p5Dp3].7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 187 188 189 508 3f3 50e 50f 510 511 512 513 p5Ep3 : p5 = p3
size_rpeg ↓[c1] `p[p1, p] + 2 ^ n <
size [seq ↑[i]_p1 | i <- cs1] + (size cs2).+1
(* the path has a duplicate use the induction hypothesis *)
have p4Ep1: p4 = p1.
move /eqP : p5Ep3; rewrite eq_sym // opeg3E // eq_sym //.50d (p5 != p1) && (p2 != p5) -> p4 = p1
522
by rewrite opeg3E // negb_and !negbK eq_sym (negPf p1Dp2)
=> /andP[/eqP] .7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 187 188 189 508 3f3 50e 50f 510 511 512 513 518 1a1
519 51a
pose cs5 := [seq ↑[i]_p1 | i <- cs1] ++ cs4.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 187 188 189 508 3f3 50e 50f 510 511 512 513 518 1a1 cs5 := [seq ↑[i]_p1 | i <- cs1] ++ cs4 : seq (configuration 3 n.+1 )
519 51a
have scs5Lscs : size cs5 < size cs.
rewrite /cs5 csE cs2E !size_cat /= !size_cat /= !size_map.
rewrite ltn_add2l // !addnS! ltnS -addSn leq_addl //.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 187 188 189 508 3f3 50e 50f 510 511 512 513 518 1a1 531 539
519 51a
have c1Mcs5 : path rmove c1 cs5.
rewrite cat_path -[c1](cunliftrK) !path_liftr //=.540 path (move (rrel (n:=3 ))) ↓[c1] cs1 &&
path rmove
(last ↑[↓[c1]]_(c1 ldisk) [seq ↑[i]_p1 | i <- cs1])
cs4
545
rewrite c1'Pcs1.540 true &&
path rmove
(last ↑[↓[c1]]_(c1 ldisk) [seq ↑[i]_p1 | i <- cs1])
cs4
545
by rewrite last_map lc1'cs1Epp3 -/p1 -p5Ep3 -p4Ep1.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 187 188 189 508 3f3 50e 50f 510 511 512 513 518 1a1 531 539 548
519 51a
have lc1cs5E : last c1 cs5 = `c[p].
rewrite last_cat -[c1](cunliftrK) last_map lc1'cs1Epp3.554 last ↑[`c[p3]]_(c1 ldisk) cs4 = `c[p]
559
rewrite -lc1csEp csE cs2E last_cat /= last_cat /= -/p1.554 last ↑[`c[p3]]_p1 cs4 = last ↑[`c[p5]]_p4 cs4
559
by rewrite p5Ep3 p4Ep1.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 187 188 189 508 3f3 50e 50f 510 511 512 513 518 1a1 531 539 548 55c
519 51a
apply : leq_trans (_ : size cs5 < _); last first .568 size cs5 <
size [seq ↑[i]_p1 | i <- cs1] + (size cs2).+1
by rewrite cs2E /= !size_cat !size_map /=
ltn_add2l // ltnS -addSnnS leq_addl.
rewrite ltnS.568 size_rpeg ↓[c1] `p[p1, p] + 2 ^ n <= size cs5
51a
have /IHm : size cs5 < m.
rewrite -ltnS.568 (size cs5).+1 < m.+1
57b
by apply : leq_ltn_trans Scs.
move => /(_ c1 p c1Mcs5 lc1cs5E) /=.568 (if c1 ldisk == p
then size_rpeg ↓[c1] p
else size_rpeg ↓[c1] `p[c1 ldisk, p] + 2 ^ n) <=
size cs5
?= iff
(cs5 ==
(if
c1
ldisk ==
p
then
[
seq ↑[i]_p
| i <-
rpeg
↓[c1]
p]
else
[
seq ↑[i]_
(c1
ldisk)
| i <-
rpeg
↓[c1]
`p[
c1
ldisk, p]] ++
↑[`c[`p[
c1
ldisk, p]]]_p
:: [
seq ↑[i]_p
| i <-
ppeg
`p[
c1
ldisk, p]
p])) ->
size_rpeg ↓[c1] `p[p1, p] + 2 ^ n <= size cs5
51a
by rewrite -/p1 (negPf p1Dp) => ->.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 187 188 189 508 3f3 50e 50f 510 511 512 513 51d
49e
(* now we just need to use the induction principle on the two subpath *)
have [cs4' [pp5p4Pcs4' lpp5p4cs4'Elpp5p4cs4 scs4'L]] :=
pathS_restrict HHr pp5p4Pcs4.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 187 188 189 508 3f3 50e 50f 510 511 512 513 51d cs4' : seq (configuration 3 n)
pp5p4Pcs4' : path (move (rrel (n:=3 ))) ↓[↑[`c[p5]]_p4]
cs4'
lpp5p4cs4'Elpp5p4cs4 : last ↓[↑[`c[p5]]_p4] cs4' =
↓[last ↑[`c[p5]]_p4 cs4]
scs4'L : size cs4' <= size cs4
?= iff (cs4 ==
[seq ↑[i]_
(↑[`c[p5]]_p4 ldisk)
| i <- cs4'])
49e
rewrite cliftrK in lpp5p4cs4'Elpp5p4cs4 pp5p4Pcs4'.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 187 188 189 508 3f3 50e 50f 510 511 512 513 51d 591 594 lpp5p4cs4'Elpp5p4cs4 : last `c[p5] cs4' =
↓[last ↑[`c[p5]]_p4 cs4]
pp5p4Pcs4' : path (move (rrel (n:=3 ))) `c[p5] cs4'
49e
have Scs3 : size cs3 < m.+1 .
apply : ltn_trans Scs2.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3ee 4c7 187 188 189 508 3f3 50e 50f 510 511 512 513 51d 591 594 599 59a
size cs3 < size cs2
59e
by rewrite cs2E size_cat /= size_map addnS ltnS leq_addr.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 187 188 189 508 3f3 50e 50f 510 511 512 513 51d 591 594 599 59a 1f2
49e
have Scs4 : size cs4 < m.+1 .
apply : ltn_trans Scs2.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3ee 4c7 187 188 189 508 3f3 50e 50f 510 511 512 513 51d 591 594 599 59a 1f2
size cs4 < size cs2
5ae
by rewrite cs2E size_cat /= size_map addnS ltnS leq_addl.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 187 188 189 508 3f3 50e 50f 510 511 512 513 51d 591 594 599 59a 1f2 5b1
49e
have Scs4' : size cs4' < m.+1 .
by apply : leq_ltn_trans Scs4; rewrite scs4'L.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 187 188 189 508 3f3 50e 50f 510 511 512 513 51d 591 594 599 59a 1f2 5b1 5c2
49e
rewrite cs2E /= size_cat /= !size_map.5c6 size_rpeg ↓[c1] `p[p1, p] + 2 ^ n <
size cs1 + (size cs3 + (size cs4).+1 ).+1
have /IH := c2'cs5Epp5 => /(_ Scs3 c2'Pcs3) IHc1.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 187 188 189 508 3f3 50e 50f 510 511 512 513 51d 591 594 599 59a 1f2 5b1 5c2 IHc1 : size_rpeg c2' p5 <= size cs3
?= iff
(cs3 == rpeg c2' p5)
5ca
have c2'E : c2' = `c[p3] by rewrite [LHS]cliftrK.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 187 188 189 508 3f3 50e 50f 510 511 512 513 51d 591 594 599 59a 1f2 5b1 5c2 5cf c2'E : c2' = `c[p3]
5ca
rewrite c2'E size_rpegE rpeg_ppeg // in IHc1; last by rewrite eq_sym.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 187 188 189 508 3f3 50e 50f 510 511 512 513 51d 591 594 599 59a 1f2 5b1 5c2 5d4 IHc1 : size (ppeg p3 p5) <= size cs3
?= iff
(cs3 == ppeg p3 p5)
5ca
rewrite size_ppeg in IHc1.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 187 188 189 508 3f3 50e 50f 510 511 512 513 51d 591 594 599 59a 1f2 5b1 5c2 5d4 IHc1 : (2 ^ n).-1 <= size cs3
?= iff (cs3 == ppeg p3 p5)
5ca
have p6Dp : p5 != p.
by apply : contra p5Dp3 => /eqP->; apply /eqP.7c 326 5 32b 32c 23d 84 32d 32f 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 187 188 189 508 3f3 50e 50f 510 511 512 513 51d 591 594 599 59a 1f2 5b1 5c2 5d4 5de 5e6
5ca
move : lc1csEp; rewrite csE cs2E.7c 326 5 32b 32c 23d 84 32d 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 187 188 189 508 3f3 50e 50f 510 511 512 513 51d 591 594 599 59a 1f2 5b1 5c2 5d4 5de 5e6
last c1
([seq ↑[i]_p1 | i <- cs1] ++
c2
:: [seq ↑[i]_p2 | i <- cs3] ++ ↑[`c[p5]]_p4 :: cs4) =
`c[p] ->
size_rpeg ↓[c1] `p[p1, p] + 2 ^ n <
size cs1 + (size cs3 + (size cs4).+1 ).+1
rewrite last_cat /= last_cat /= => lpp5p4cs4Epp.7c 326 5 32b 32c 23d 84 32d 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 187 188 189 508 3f3 50e 50f 510 511 512 513 51d 591 594 599 59a 1f2 5b1 5c2 5d4 5de 5e6 lpp5p4cs4Epp : last ↑[`c[p5]]_p4 cs4 = `c[p]
5ca
have lpp5cs4'Epp : last `c[p5] cs4' = `c[p].5f3 last `c[p5] cs4' = `c[p]
by rewrite lpp5p4cs4'Elpp5p4cs4 lpp5p4cs4Epp perfect_unliftr.7c 326 5 32b 32c 23d 84 32d 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 187 188 189 508 3f3 50e 50f 510 511 512 513 51d 591 594 599 59a 1f2 5b1 5c2 5d4 5de 5e6 5f4 5fc
5ca
have /IH : last `c[p5] cs4' = `c[p] => [//| /(_ Scs4' pp5p4Pcs4') IHc2].7c 326 5 32b 32c 23d 84 32d 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 187 188 189 508 3f3 50e 50f 510 511 512 513 51d 591 594 599 59a 1f2 5b1 5c2 5d4 5de 5e6 5f4 5fc IHc2 : size_rpeg `c[p5] p <= size cs4'
?= iff
(cs4' == rpeg `c[p5] p)
5ca
rewrite size_rpegE rpeg_ppeg // size_ppeg in IHc2.7c 326 5 32b 32c 23d 84 32d 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 187 188 189 508 3f3 50e 50f 510 511 512 513 51d 591 594 599 59a 1f2 5b1 5c2 5d4 5de 5e6 5f4 5fc IHc2 : (2 ^ n).-1 <= size cs4'
?= iff (cs4' == ppeg p5 p)
5ca
rewrite -[2 ^ n]prednK ?expn_gt0 //.609 size_rpeg ↓[c1] `p[p1, p] + (2 ^ n).-1 .+1 <
size cs1 + (size cs3 + (size cs4).+1 ).+1
rewrite !addnS !ltnS.609 size_rpeg ↓[c1] `p[p1, p] + (2 ^ n).-1 <=
size cs1 + (size cs3 + size cs4)
apply : leq_trans (leq_addl _ _).609 size_rpeg ↓[c1] `p[p1, p] + (2 ^ n).-1 <=
size cs3 + size cs4
apply : leq_add.609 size_rpeg ↓[c1] `p[p1, p] <= size cs3
by apply : leq_trans (size_rpeg_up _ _) _; rewrite IHc1.
apply : leq_trans scs4'L.7c 326 5 32b 32c 23d 84 32d 33c 391 396 39b c4 c5 3a2 24 45 3a0 3a8 3f 3a9 3aa 3ab 3ac 3c4 d7 3dc 3ee 4c7 187 188 189 508 3f3 50e 50f 510 511 512 513 51d 591 599 59a 1f2 5b1 5c2 5d4 5de 5e6 5f4 5fc 60a
(2 ^ n).-1 <= size cs4'
by rewrite IHc2.
Qed .
Lemma gdist_size_rpeg n (c1 : _ _ n) p : `d[c1, `c[p]]_rmove = size_rpeg c1 p.`d[c1, `c[p]]_rmove = size_rpeg c1 p
Proof .628
apply /eqP; rewrite eqn_leq [size_rpeg _ _]size_rpegE.62a `d[c1, `c[p]]_rmove <= size (rpeg c1 p) <=
`d[c1, `c[p]]_rmove
rewrite gdist_path_le; last 2 first .62a path rmove c1 (rpeg c1 p)
- 633
by apply : path_rpeg.
- 63d
by rewrite last_rpeg.
have /gpath_connect [p1 p1H] : connect rmove c1 `c[p].
by apply : move_connect_rpeg.
rewrite -size_rpegE (gpath_dist p1H) /=.64a size_rpeg c1 p <= size p1
apply : (rpeg_min (gpath_path p1H)) => //.
by apply : gpath_last p1H.
Qed .
Lemma gdist_perfect_le n (c : configuration 3 n) p :
`d[c, `c[p]]_rmove <= (2 ^ n).-1 .249 `d[c, `c[p]]_rmove <= (2 ^ n).-1
Proof .659
by rewrite gdist_size_rpeg; apply : size_rpeg_up. Qed .
(******************************************************************************)
(* Function that builds a path from a peg to a configuration *)
(******************************************************************************)
Definition lpeg n p (c : _ _ n) := rev (belast c (rpeg c p)).
Lemma lpeg_perfect n p : lpeg p `c[p, n] = [::].23c lpeg p `c[p , n] = [::]
Proof .65e
by rewrite /lpeg rpeg_perfect. Qed .
Lemma lpeg_nil_inv n c p :
lpeg p c = [::] -> c = `c[p] :> configuration _ n.249 lpeg p c = [::] -> c = `c[p]
Proof .663
have := @rpeg_nil_inv _ c p.249 (rpeg c p = [::] -> c = `c[p]) ->
lpeg p c = [::] -> c = `c[p]
rewrite /lpeg; case : rpeg => //= a l.5 17 23d a : configuration 3 n
l : seq (configuration 3 n)
(a :: l = [::] -> c = `c[p]) ->
rev (c :: belast a l) = [::] -> c = `c[p]
by rewrite rev_cons; case : rev.
Qed .
Lemma path_lpeg n (c : configuration 3 n) p (cs := lpeg p c) :
path rmove `c[p] cs.5 17 23d cs := lpeg p c : seq (configuration 3 n)
path rmove `c[p] cs
Proof .673
have HHs := @rsym 3 .
rewrite {}/cs /lpeg -(last_rpeg c) path_move_rev //.5 17 23d 39b
path (move (rrel (n:=3 ))) c (rpeg c p)
by apply : path_rpeg.
Qed .
Lemma last_lpeg n (c : configuration 3 n) p (cs := lpeg p c) :
last `c[p] cs = c.
Proof .683
have HHs := @rsym 3 ; have := last_rpeg c p.67c (let cs := rpeg c p in last c cs = `c[p]) ->
last `c[p] cs = c
rewrite {}/cs /lpeg; case : rpeg => //= c1 cs.5 17 23d 39b 62b 6f
last c1 cs = `c[p] ->
last `c[p] (rev (c :: belast c1 cs)) = c
by rewrite rev_cons last_rcons.
Qed .
Lemma size_lpegE n (c : _ _ n) p :
size_rpeg c p = size (lpeg p c).249 size_rpeg c p = size (lpeg p c)
Proof .691
by rewrite size_rev size_belast size_rpegE. Qed .
Lemma lpeg_min n (c : configuration 3 n) p cs :
path rmove `c[p] cs -> last `c[p] cs = c ->
size_rpeg c p <= size cs ?= iff (cs == lpeg p c).31f path rmove `c[p] cs ->
last `c[p] cs = c ->
size_rpeg c p <= size cs ?= iff (cs == lpeg p c)
Proof .696
(* why this is so complicated???? *)
move => pPcs lccsEc.5 17 23d 6f pPcs : path rmove `c[p] cs
lccsEc : last `c[p] cs = c
size_rpeg c p <= size cs ?= iff (cs == lpeg p c)
have HHs := @rsym 3 .
have cPr : path rmove c (rev (belast `c[p] cs)).6a4 path rmove c (rev (belast `c[p] cs))
by rewrite -{1 }lccsEc path_move_rev.
have lcrEp : last c (rev (belast `c[p] cs)) = `c[p].6ab last c (rev (belast `c[p] cs)) = `c[p]
rewrite -lccsEc; case : (cs)=> //= c3 cs1.5 17 23d 6f 69e 69f 39b 6ac c3 : configuration 3 n
c4 last (last c3 cs1) (rev (`c[p] :: belast c3 cs1)) =
`c[p]
6b4
by rewrite rev_cons last_rcons.
have := rpeg_min cPr lcrEp.6b6 size_rpeg c p <= size (rev (belast `c[p] cs))
?= iff (rev (belast `c[p] cs) ==
rpeg c p) ->
size_rpeg c p <= size cs ?= iff (cs == lpeg p c)
rewrite /lpeg size_rev size_belast.6b6 size_rpeg c p <= size cs
?= iff (rev (belast `c[p] cs) ==
rpeg c p) ->
size_rpeg c p <= size cs
?= iff (cs == rev (belast c (rpeg c p)))
set u := rev _ ; set v := rpeg _ _.5 17 23d 6f 69e 69f 39b 6ac 6b7 u := rev (belast `c[p] cs) : seq (configuration 3 n)
v := rpeg c p : seq (configuration 3 n)
size_rpeg c p <= size cs ?= iff (u == v) ->
size_rpeg c p <= size cs
?= iff (cs == rev (belast c v))
have -> : (u == v) = (rev (c :: u) == rev (c :: v)).6cc (u == v) = (rev (c :: u) == rev (c :: v))
rewrite !rev_cons eqseq_rcons eqxx andbT.6cc (u == v) = (rev u == rev v)
6d4
apply /eqP/eqP=> [->//|].6cc rev u = rev v -> u = v
6d4
by rewrite -{2 }[u]revK => ->; rewrite revK.
rewrite [c :: v]lastI -/v rev_rcons.6cc size_rpeg c p <= size cs
?= iff (rev (c :: u) ==
last c v :: rev (belast c v)) ->
size_rpeg c p <= size cs
?= iff (cs == rev (belast c v))
rewrite rev_cons revK -{2 }lccsEc -lastI eqseq_cons andbC.6cc size_rpeg c p <= size cs
?= iff (cs == rev (belast c v)) &&
(`c[p] == last c v) ->
size_rpeg c p <= size cs
?= iff (cs == rev (belast c v))
case : eqP=> //; case : eqP => // pDl Hcs; case : pDl.5 17 23d 6f 69e 69f 39b 6ac 6b7 6cd 6ce Hcs : cs = rev (belast c v)
`c[p] = last c v
by rewrite last_rpeg.
Qed .
Fixpoint rhanoi3 {n : nat} :=
if n is n1.+1 return configuration 3 n -> configuration 3 n -> _
_ then
fun c1 c2 =>
let p1 := c1 ldisk in
let p2 := c2 ldisk in
let c1' := ↓[c1] in
let c2' := ↓[c2] in
if p1 == p2 then [seq ↑[i]_p1 | i <- rhanoi3 c1' c2'] else
let p := `p[p1, p2] in
(* one jump *)
let m1 := size_rpeg c1' p + size_rpeg c2' p in
(* two jumps *)
let m2 := size_rpeg c1' p2 + 2 ^ n1 + size_rpeg c2' p1
in if m1 <= m2 then
[seq ↑[i]_p1 | i <- rpeg c1' p] ++
[seq ↑[i]_p2 | i <- `c[p] :: lpeg p c2']
else
[seq ↑[i]_p1 | i <- rpeg c1' p2] ++
[seq ↑[i]_p | i <- `c[p2] :: ppeg p2 p1] ++
[seq ↑[i]_p2 | i <- `c[p1] :: lpeg p1 c2']
else fun _ _ => [::].
Lemma last_rhanoi3 n (c1 c2 : _ _ n) (cs := rhanoi3 c1 c2) :
last c1 cs = c2.5 2da cs := rhanoi3 c1 c2 : seq (configuration 3 n)
last c1 cs = c2
Proof .6f1
have HHr := @rirr 3 .
rewrite {}/cs.5 2da 396
last c1 (rhanoi3 c1 c2) = c2
elim : n c1 c2 => /= [c1 c2 |n IH c1 c2]; first by apply /ffunP=> [] [].396 5 IH : forall c1 c2 : configuration 3 n,
last c1 (rhanoi3 c1 c2) = c2
c1, c2 : configuration 3 n.+1
last c1
(if c1 ldisk == c2 ldisk
then
[seq ↑[i]_(c1 ldisk) | i <- rhanoi3 ↓[c1] ↓[c2]]
else
if
size_rpeg ↓[c1] `p[c1 ldisk, c2 ldisk] +
size_rpeg ↓[c2] `p[c1 ldisk, c2 ldisk] <=
size_rpeg ↓[c1] (c2 ldisk) + 2 ^ n +
size_rpeg ↓[c2] (c1 ldisk)
then
[seq ↑[i]_(c1 ldisk)
| i <- rpeg ↓[c1] `p[c1 ldisk, c2 ldisk]] ++
↑[`c[`p[c1 ldisk, c2 ldisk]]]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk)
| i <- lpeg `p[c1 ldisk, c2 ldisk] ↓[c2]]
else
[seq ↑[i]_(c1 ldisk)
| i <- rpeg ↓[c1] (c2 ldisk)] ++
↑[`c[c2 ldisk]]_(`p[c1 ldisk, c2 ldisk])
:: [seq ↑[i]_(`p[c1 ldisk, c2 ldisk])
| i <- ppeg (c2 ldisk) (c1 ldisk)] ++
↑[`c[c1 ldisk]]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk)
| i <- lpeg (c1 ldisk) ↓[c2]]) = c2
set p1 := _ ldisk; set p2 := _ ldisk.396 5 704 705 p1 := c1 ldisk : (fun => peg 3 ) ldisk
p2 := c2 ldisk : (fun => peg 3 ) ldisk
last c1
(if p1 == p2
then [seq ↑[i]_p1 | i <- rhanoi3 ↓[c1] ↓[c2]]
else
if
size_rpeg ↓[c1] `p[p1, p2] +
size_rpeg ↓[c2] `p[p1, p2] <=
size_rpeg ↓[c1] p2 + 2 ^ n + size_rpeg ↓[c2] p1
then
[seq ↑[i]_p1 | i <- rpeg ↓[c1] `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i]_p2 | i <- lpeg `p[p1, p2] ↓[c2]]
else
[seq ↑[i]_p1 | i <- rpeg ↓[c1] p2] ++
↑[`c[p2]]_(`p[p1, p2])
:: [seq ↑[i]_(`p[p1, p2]) | i <- ppeg p2 p1] ++
↑[`c[p1]]_p2
:: [seq ↑[i]_p2 | i <- lpeg p1 ↓[c2]]) = c2
set c3 := cliftr _ _; set c4 := cliftr _ _; set c5 := cliftr _ _.396 5 704 705 70b 70c c3 := ↑[`c[`p[p1, p2]]]_p2 : configuration 3 n.+1
c4 := ↑[`c[p2]]_(`p[p1, p2]) : configuration 3 n.+1
c5 := ↑[`c[p1]]_p2 : configuration 3 n.+1
last c1
(if p1 == p2
then [seq ↑[i]_p1 | i <- rhanoi3 ↓[c1] ↓[c2]]
else
if
size_rpeg ↓[c1] `p[p1, p2] +
size_rpeg ↓[c2] `p[p1, p2] <=
size_rpeg ↓[c1] p2 + 2 ^ n + size_rpeg ↓[c2] p1
then
[seq ↑[i]_p1 | i <- rpeg ↓[c1] `p[p1, p2]] ++
c3 :: [seq ↑[i]_p2 | i <- lpeg `p[p1, p2] ↓[c2]]
else
[seq ↑[i]_p1 | i <- rpeg ↓[c1] p2] ++
c4
:: [seq ↑[i]_(`p[p1, p2]) | i <- ppeg p2 p1] ++
c5 :: [seq ↑[i]_p2 | i <- lpeg p1 ↓[c2]]) = c2
set p := `p[_, _].396 5 704 705 70b 70c 712 713 714 p := `p[p1, p2] : peg 3
last c1
(if p1 == p2
then [seq ↑[i]_p1 | i <- rhanoi3 ↓[c1] ↓[c2]]
else
if
size_rpeg ↓[c1] p + size_rpeg ↓[c2] p <=
size_rpeg ↓[c1] p2 + 2 ^ n + size_rpeg ↓[c2] p1
then
[seq ↑[i]_p1 | i <- rpeg ↓[c1] p] ++
c3 :: [seq ↑[i]_p2 | i <- lpeg p ↓[c2]]
else
[seq ↑[i]_p1 | i <- rpeg ↓[c1] p2] ++
c4
:: [seq ↑[i]_p | i <- ppeg p2 p1] ++
c5 :: [seq ↑[i]_p2 | i <- lpeg p1 ↓[c2]]) = c2
case : eqP => [p1Ep2|/eqP p1Dp2].396 5 704 705 70b 70c 712 713 714 71a p1Ep2 : p1 = p2
last c1 [seq ↑[i]_p1 | i <- rhanoi3 ↓[c1] ↓[c2]] = c2
by rewrite -{1 }[c1]cunliftrK last_map IH [c1 _]p1Ep2 cunliftrK.
case : leqP => _; first by rewrite last_cat /= last_map last_lpeg cunliftrK.724 last c1
([seq ↑[i]_p1 | i <- rpeg ↓[c1] p2] ++
c4
:: [seq ↑[i]_p | i <- ppeg p2 p1] ++
c5 :: [seq ↑[i]_p2 | i <- lpeg p1 ↓[c2]]) = c2
by rewrite last_cat /= last_cat /= last_map last_lpeg cunliftrK.
Qed .
Lemma path_rhanoi3 n (c1 c2 : _ _ n) (cs := rhanoi3 c1 c2) :
path rmove c1 cs.
Proof .72e
have HHr := @rirr 3 .
rewrite {}/cs.6fe path rmove c1 (rhanoi3 c1 c2)
elim : n c1 c2 => //= n IH c1 c2.396 5 IH : forall c1 c2 : configuration 3 n,
path rmove c1 (rhanoi3 c1 c2)
705 path rmove c1
(if c1 ldisk == c2 ldisk
then
[seq ↑[i]_(c1 ldisk) | i <- rhanoi3 ↓[c1] ↓[c2]]
else
if
size_rpeg ↓[c1] `p[c1 ldisk, c2 ldisk] +
size_rpeg ↓[c2] `p[c1 ldisk, c2 ldisk] <=
size_rpeg ↓[c1] (c2 ldisk) + 2 ^ n +
size_rpeg ↓[c2] (c1 ldisk)
then
[seq ↑[i]_(c1 ldisk)
| i <- rpeg ↓[c1] `p[c1 ldisk, c2 ldisk]] ++
↑[`c[`p[c1 ldisk, c2 ldisk]]]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk)
| i <- lpeg `p[c1 ldisk, c2 ldisk] ↓[c2]]
else
[seq ↑[i]_(c1 ldisk)
| i <- rpeg ↓[c1] (c2 ldisk)] ++
↑[`c[c2 ldisk]]_(`p[c1 ldisk, c2 ldisk])
:: [seq ↑[i]_(`p[c1 ldisk, c2 ldisk])
| i <- ppeg (c2 ldisk) (c1 ldisk)] ++
↑[`c[c1 ldisk]]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk)
| i <- lpeg (c1 ldisk) ↓[c2]])
set p1 := _ ldisk; set p2 := _ ldisk.396 5 73d 705 70b 70c
path rmove c1
(if p1 == p2
then [seq ↑[i]_p1 | i <- rhanoi3 ↓[c1] ↓[c2]]
else
if
size_rpeg ↓[c1] `p[p1, p2] +
size_rpeg ↓[c2] `p[p1, p2] <=
size_rpeg ↓[c1] p2 + 2 ^ n + size_rpeg ↓[c2] p1
then
[seq ↑[i]_p1 | i <- rpeg ↓[c1] `p[p1, p2]] ++
↑[`c[`p[p1, p2]]]_p2
:: [seq ↑[i]_p2 | i <- lpeg `p[p1, p2] ↓[c2]]
else
[seq ↑[i]_p1 | i <- rpeg ↓[c1] p2] ++
↑[`c[p2]]_(`p[p1, p2])
:: [seq ↑[i]_(`p[p1, p2]) | i <- ppeg p2 p1] ++
↑[`c[p1]]_p2
:: [seq ↑[i]_p2 | i <- lpeg p1 ↓[c2]])
set c3 := cliftr _ _; set c4 := cliftr _ _; set c5 := cliftr _ _.396 5 73d 705 70b 70c 712 713 714
path rmove c1
(if p1 == p2
then [seq ↑[i]_p1 | i <- rhanoi3 ↓[c1] ↓[c2]]
else
if
size_rpeg ↓[c1] `p[p1, p2] +
size_rpeg ↓[c2] `p[p1, p2] <=
size_rpeg ↓[c1] p2 + 2 ^ n + size_rpeg ↓[c2] p1
then
[seq ↑[i]_p1 | i <- rpeg ↓[c1] `p[p1, p2]] ++
c3 :: [seq ↑[i]_p2 | i <- lpeg `p[p1, p2] ↓[c2]]
else
[seq ↑[i]_p1 | i <- rpeg ↓[c1] p2] ++
c4
:: [seq ↑[i]_(`p[p1, p2]) | i <- ppeg p2 p1] ++
c5 :: [seq ↑[i]_p2 | i <- lpeg p1 ↓[c2]])
set p := `p[_, _].396 5 73d 705 70b 70c 712 713 714 71a
path rmove c1
(if p1 == p2
then [seq ↑[i]_p1 | i <- rhanoi3 ↓[c1] ↓[c2]]
else
if
size_rpeg ↓[c1] p + size_rpeg ↓[c2] p <=
size_rpeg ↓[c1] p2 + 2 ^ n + size_rpeg ↓[c2] p1
then
[seq ↑[i]_p1 | i <- rpeg ↓[c1] p] ++
c3 :: [seq ↑[i]_p2 | i <- lpeg p ↓[c2]]
else
[seq ↑[i]_p1 | i <- rpeg ↓[c1] p2] ++
c4
:: [seq ↑[i]_p | i <- ppeg p2 p1] ++
c5 :: [seq ↑[i]_p2 | i <- lpeg p1 ↓[c2]])
case : eqP => [p1Ep2|/eqP p1Dp2].396 5 73d 705 70b 70c 712 713 714 71a 720
path rmove c1 [seq ↑[i]_p1 | i <- rhanoi3 ↓[c1] ↓[c2]]
by rewrite -{1 }[c1]cunliftrK path_liftr.
case : leqP => _; rewrite !cat_path /=; apply /and3P; split .755 path rmove c1 [seq ↑[i]_p1 | i <- rpeg ↓[c1] p]
- 75b
by rewrite -{1 }[c1]cunliftrK path_liftr // path_rpeg.
- 76b
rewrite -{1 }[c1]cunliftrK last_map last_rpeg.755 ↑[`c[p]]_(c1 ldisk) `-->_r c3
76d
apply /moveP; exists ldisk .755 [/\ rrel (↑[`c[p]]_(c1 ldisk) ldisk) (c3 ldisk),
forall d2 : ordinal_finType n.+1 ,
ldisk != d2 -> ↑[`c[p]]_(c1 ldisk) d2 = c3 d2,
on_top ldisk ↑[`c[p]]_(c1 ldisk)
& on_top ldisk c3]
76d
split => // [|d dmDd||].755 rrel (↑[`c[p]]_(c1 ldisk) ldisk) (c3 ldisk)
- 778
by rewrite !cliftr_ldisk.
- 787
rewrite !ffunE; case : tsplitP => [j|j jE]; first by rewrite !ffunE.396 5 73d 705 70b 70c 712 713 714 71a 3f 77e 77f j : 'I_1
jE : d = j + n
`c[c1 ldisk] j = `c[p2] j
789
by case /eqP: dmDd; apply /val_eqP; rewrite /= jE; case : (j) => [] [].
- 793
apply /on_topP=> d; rewrite !cliftr_ldisk !ffunE.396 5 73d 705 70b 70c 712 713 714 71a 3f 77e
c1 ldisk =
match tsplit d with
| inl j => `c[c1 ldisk] j
| inr j => `c[p] j
end -> ldisk <= d
795
case : tsplitP => [j _ /eqP|j jE].396 5 73d 705 70b 70c 712 713 714 71a 3f 77e j : 'I_n
c1 ldisk == `c[p] j -> ldisk <= d
by rewrite !ffunE -/p1 eq_sym (negPf (opegDl _ _)).
by rewrite /= !ffunE jE /= leq_addl.
apply /on_topP=> d; rewrite /= !cliftr_ldisk !ffunE.79a p2 =
match tsplit d with
| inl j => `c[p2] j
| inr j => `c[`p[p1, p2]] j
end -> n <= d
76d
case : tsplitP => [j _ /eqP|j ->]; last by case : j => [] [].79f p2 == `c[`p[p1, p2]] j -> n <= d
76d
by rewrite !ffunE eq_sym (negPf (opegDr _ _)).
- 7b5
by rewrite -[c3]cunliftrK !cliftr_ldisk /= path_liftr // cliftrK path_lpeg.
- 7ba
by rewrite -{1 }[c1]cunliftrK path_liftr // path_rpeg.
- 7bf
rewrite -{1 }[c1]cunliftrK last_map last_rpeg.755 ↑[`c[p2]]_(c1 ldisk) `-->_r c4
7c1
apply /moveP; exists ldisk ; split => // [|d2||];
rewrite ?cliftr_ldisk ?ffunE //=.755 rrel (c1 ldisk) `p[p1, p2]
- 7c8
by rewrite /rrel /= eq_sym opegDl.
- 7d6
case : tsplitP => //= j d2E /eqP[].396 5 73d 705 70b 70c 712 713 714 71a 3f 7ce 78f d2E : d2 = j + n
ldisk = d2
7d8
by apply /val_eqP; rewrite /= d2E; case : (j) => [] [].
- 7e1
apply /on_topP=> d2.7cd ↑[`c[p2]]_(c1 ldisk) ldisk = ↑[`c[p2]]_(c1 ldisk) d2 ->
ldisk <= d2
7e3
rewrite cliftr_ldisk /= !ffunE.7cd c1 ldisk =
match tsplit d2 with
| inl j => `c[c1 ldisk] j
| inr j => `c[p2] j
end -> n <= d2
7e3
case : tsplitP => [k _ /eqP | [[]] // j -> //].396 5 73d 705 70b 70c 712 713 714 71a 3f 7ce k : 'I_n
c1 ldisk == `c[p2] k -> n <= d2
7e3
by rewrite ?ffunE (negPf p1Dp2).
apply /on_topP=> d2.7cd c4 ldisk = c4 d2 -> ldisk <= d2
7c1
rewrite cliftr_ldisk /= !ffunE.7cd `p[p1, p2] =
match tsplit d2 with
| inl j => `c[`p[p1, p2]] j
| inr j => `c[p2] j
end -> n <= d2
7c1
case : tsplitP => [k _ /eqP | [[]] // j -> //].7f0 `p[p1, p2] == `c[p2] k -> n <= d2
7c1
by rewrite !ffunE (negPf (opegDr _ _)).
rewrite cat_path /=; apply /and3P; split => //.755 path rmove c4 [seq ↑[i]_p | i <- ppeg p2 p1]
- 806
rewrite -[c4]cunliftrK cliftr_ldisk -/p path_liftr // cliftrK // path_ppeg //.
by rewrite eq_sym.
- 814
rewrite -[c4]cunliftrK cliftr_ldisk -/p last_map cliftrK // last_ppeg //.755 ↑[`c[p1]]_p `-->_r c5
816
apply /moveP; exists ldisk ; split => // [|d2||];
rewrite ?cliftr_ldisk ?ffunE /=.
- 81d
by rewrite /rrel /= opegDr.
- 829
case : tsplitP => [j | j d2E /eqP[]] //=.
by apply /val_eqP => /=; rewrite d2E; case : (j) => [] [].
- 830
apply /on_topP=> d2.7cd ↑[`c[p1]]_p ldisk = ↑[`c[p1]]_p d2 -> ldisk <= d2
832
rewrite cliftr_ldisk /= !ffunE.7cd p =
match tsplit d2 with
| inl j => `c[p] j
| inr j => `c[p1] j
end -> n <= d2
832
case : tsplitP => [k _ /eqP | [[]] // j -> //].7f0 p == `c[p1] k -> n <= d2
832
by rewrite !ffunE (negPf (opegDl _ _)).
apply /on_topP=> d2.7cd c5 ldisk = c5 d2 -> ldisk <= d2
816
rewrite cliftr_ldisk /= !ffunE.7cd p2 =
match tsplit d2 with
| inl j => `c[p2] j
| inr j => `c[p1] j
end -> n <= d2
816
case : tsplitP => [k _ /eqP | [[]] // j -> //].7f0 p2 == `c[p1] k -> n <= d2
816
by rewrite !ffunE eq_sym (negPf p1Dp2).
by rewrite path_liftr // path_lpeg.
Qed .
Lemma rhanoi3_min n (c1 c2 : configuration 3 n) cs :
path rmove c1 cs -> last c1 cs = c2 ->
size (rhanoi3 c1 c2) <= size cs.5 2da 6f
path rmove c1 cs ->
last c1 cs = c2 -> size (rhanoi3 c1 c2) <= size cs
Proof .853
have HHr := @rirr 3 .
have HHs := @rsym 3 .
elim : n c1 c2 cs => [p c1 [|]//|n IH c1 c2 cs /=].396 39b 5 IH : forall (c1 c2 : configuration 3 n)
(cs : seq (configuration 3 n)),
path rmove c1 cs ->
last c1 cs = c2 ->
size (rhanoi3 c1 c2) <= size cs
705 84 path rmove c1 cs ->
last c1 cs = c2 ->
size
(if c1 ldisk == c2 ldisk
then
[seq ↑[i]_(c1 ldisk) | i <- rhanoi3 ↓[c1] ↓[c2]]
else
if
size_rpeg ↓[c1] `p[c1 ldisk, c2 ldisk] +
size_rpeg ↓[c2] `p[c1 ldisk, c2 ldisk] <=
size_rpeg ↓[c1] (c2 ldisk) + 2 ^ n +
size_rpeg ↓[c2] (c1 ldisk)
then
[seq ↑[i]_(c1 ldisk)
| i <- rpeg ↓[c1] `p[c1 ldisk, c2 ldisk]] ++
↑[`c[`p[c1 ldisk, c2 ldisk]]]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk)
| i <- lpeg `p[c1 ldisk, c2 ldisk] ↓[c2]]
else
[seq ↑[i]_(c1 ldisk)
| i <- rpeg ↓[c1] (c2 ldisk)] ++
↑[`c[c2 ldisk]]_(`p[c1 ldisk, c2 ldisk])
:: [seq ↑[i]_(`p[c1 ldisk, c2 ldisk])
| i <- ppeg (c2 ldisk) (c1 ldisk)] ++
↑[`c[c1 ldisk]]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk)
| i <- lpeg (c1 ldisk) ↓[c2]]) <=
size cs
set p := `p[_, _]; set p1 := _ ldisk; set p2 := _ ldisk.396 39b 5 864 705 84 p := `p[c1 ldisk, c2 ldisk] : peg 3
70b 70c path rmove c1 cs ->
last c1 cs = c2 ->
size
(if p1 == p2
then [seq ↑[i]_p1 | i <- rhanoi3 ↓[c1] ↓[c2]]
else
if
size_rpeg ↓[c1] p + size_rpeg ↓[c2] p <=
size_rpeg ↓[c1] p2 + 2 ^ n + size_rpeg ↓[c2] p1
then
[seq ↑[i]_p1 | i <- rpeg ↓[c1] p] ++
↑[`c[p]]_p2 :: [seq ↑[i]_p2 | i <- lpeg p ↓[c2]]
else
[seq ↑[i]_p1 | i <- rpeg ↓[c1] p2] ++
↑[`c[p2]]_p
:: [seq ↑[i]_p | i <- ppeg p2 p1] ++
↑[`c[p1]]_p2
:: [seq ↑[i]_p2 | i <- lpeg p1 ↓[c2]]) <=
size cs
case : eqP => [p1Ep2 c1Pcs lc1csEc2|/eqP p1Dp2 c1Pcs lc1csEc2].396 39b 5 864 705 84 86a 70b 70c 720 32e lc1csEc2 : last c1 cs = c2
size [seq ↑[i]_p1 | i <- rhanoi3 ↓[c1] ↓[c2]] <=
size cs
have lcsmEc1m : last c1 cs ldisk = p1 by rewrite lc1csEc2.396 39b 5 864 705 84 86a 70b 70c 720 32e 870 lcsmEc1m : last c1 cs ldisk = p1
871 872
have [cs1 [c1Pcs1 lc1csElcs1 /leq_of_leqif/(leq_trans _)->//]] :=
pathS_restrict (@rirr 3 ) c1Pcs.396 39b 5 864 705 84 86a 70b 70c 720 32e 870 87a c4 34f lc1csElcs1 : last ↓[c1] cs1 = ↓[last c1 cs]
size [seq ↑[i]_p1 | i <- rhanoi3 ↓[c1] ↓[c2]] <=
size cs1
872
by rewrite size_map IH // lc1csElcs1 lc1csEc2.
set u := _ + _; set v := _ + _.396 39b 5 864 705 84 86a 70b 70c 3f 32e 870 u := size_rpeg ↓[c1] p + size_rpeg ↓[c2] p : nat
v := size_rpeg ↓[c1] p2 + 2 ^ n + size_rpeg ↓[c2] p1 : nat
size
(if u <= v
then
[seq ↑[i]_p1 | i <- rpeg ↓[c1] p] ++
↑[`c[p]]_p2 :: [seq ↑[i]_p2 | i <- lpeg p ↓[c2]]
else
[seq ↑[i]_p1 | i <- rpeg ↓[c1] p2] ++
↑[`c[p2]]_p
:: [seq ↑[i]_p | i <- ppeg p2 p1] ++
↑[`c[p1]]_p2
:: [seq ↑[i]_p2 | i <- lpeg p1 ↓[c2]]) <=
size cs
suff : minn u v < size cs.887 minn u v < size cs ->
size
(if u <= v
then
[seq ↑[i]_p1 | i <- rpeg ↓[c1] p] ++
↑[`c[p]]_p2 :: [seq ↑[i]_p2 | i <- lpeg p ↓[c2]]
else
[seq ↑[i]_p1 | i <- rpeg ↓[c1] p2] ++
↑[`c[p2]]_p
:: [seq ↑[i]_p | i <- ppeg p2 p1] ++
↑[`c[p1]]_p2
:: [seq ↑[i]_p2 | i <- lpeg p1 ↓[c2]]) <=
size cs
rewrite minnC /minn; case : (leqP u) => H1;
rewrite !size_cat /= ?size_cat /= !addnS ?ltnS
!size_map -size_rpegE -size_lpegE -/u => Lscs.396 39b 5 864 705 84 86a 70b 70c 3f 32e 870 888 889 H1 : u <= v
Lscs : u < size cs
u < size cs
by apply : leq_trans Lscs.
apply : leq_ltn_trans _ Lscs.396 39b 5 864 705 84 86a 70b 70c 3f 32e 870 888 889 89c
size_rpeg ↓[c1] p2 +
(size (ppeg p2 p1) + size_rpeg ↓[c2] p1) < v
88f
rewrite -addnS -addSn !addnA !leq_add //.8a5 size (ppeg p2 p1) < 2 ^ n
88f
by rewrite -[2 ^ _]prednK ?expn_gt0 // ltnS size_ppeg.
pose f (c : configuration 3 n.+1 ) := c ldisk.396 39b 5 864 705 84 86a 70b 70c 3f 32e 870 888 889 391
891
have [m Lcs] := ubnP (size cs); elim : m => // m IH1 in cs Lcs c1Pcs lc1csEc2 *.396 39b 5 864 705 86a 70b 70c 3f 888 889 391 7c IH1 : forall cs : seq (configuration 3 n.+1 ),
size cs < m ->
path rmove c1 cs ->
last c1 cs = c2 -> minn u v < size cs
84 Lcs : size cs < m.+1
32e 870 891
case : path3SP c1Pcs => // [c1' cs' /= csE c1'Pcs' _|
cs1 cs2 p1' p3 p4 c1' c3 p1Dp3 p1Rp3 lc1'cs1Epp4 csE
c1'Pcs1 c3Pcs2 _].396 39b 5 864 705 86a 70b 70c 3f 888 889 391 7c 8b6 84 8b7 870 3a0 3a1 csE : cs = [seq ↑[i]_(c1 ldisk) | i <- cs']
3a4 891
case /eqP: p1Dp2.396 39b 5 864 705 86a 70b 70c 888 889 391 7c IH1 : forall cs : seq (configuration 3 n.+1 ),
size cs < m -> path rmove c1 cs -> last c1 cs = c2 -> minn u v < size cs
84 8b7 870 3a0 3a1 8bc 3a4 p1 = p2
8bd
have := congr1 f lc1csEc2.8cb f (last c1 cs) = f c2 -> p1 = p2
8bd
rewrite /f csE -{1 }[c1](cunliftrK) last_map.8cb ↑[last ↓[c1] cs']_(c1 ldisk) ldisk = c2 ldisk ->
p1 = p2
8bd
by rewrite !cliftr_ldisk.
have p1'Ep1 : p1' = p1 by [].396 39b 5 864 705 86a 70b 70c 3f 888 889 391 7c 8b6 84 8b7 870 c4 c5 8c0 c6 8c1 3a0 8c2 8c3 8c4 8c5 8c6 3ac 8c7 p1'Ep1 : p1' = p1
891
move : Lcs; rewrite csE size_cat size_map /= addnS ltnS => Lcs.396 39b 5 864 705 86a 70b 70c 3f 888 889 391 7c 8b6 84 870 c4 c5 8c0 c6 8c1 3a0 8c2 8c3 8c4 8c5 8c6 3ac 8c7 8dd Lcs : size cs1 + size cs2 < m
minn u v < (size cs1 + size cs2).+1
move : lc1csEc2; rewrite csE last_cat /= => lc3cs2Ec2.396 39b 5 864 705 86a 70b 70c 3f 888 889 391 7c 8b6 84 c4 c5 8c0 c6 8c1 3a0 8c2 8c3 8c4 8c5 8c6 3ac 8c7 8dd 8e2 lc3cs2Ec2 : last c3 cs2 = c2
8e3
have [/eqP p3Ep2 | p3Dp2] := boolP (p3 == p2).396 39b 5 864 705 86a 70b 70c 3f 888 889 391 7c 8b6 84 c4 c5 8c0 c6 8c1 3a0 8c2 8c3 8c4 8c5 8c6 3ac 8c7 8dd 8e2 8e8 p3Ep2 : p3 = p2
8e3
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.396 39b 5 864 705 86a 70b 70c 3f 888 889 391 7c 8b6 84 c4 c5 8c0 c6 8c1 3a0 8c2 8c3 8c4 8c5 8c6 3ac 8c7 8dd 8e2 8e8 8ed 8f8 3fd pp4Pcs2' : path (move (rrel (n:=3 ))) ↓[c3] cs2'
pp4cs2'E : last ↓[c3] cs2' = ↓[last c3 cs2]
scs2'Lscs2 : size cs2' <= size cs2
?= iff (cs2 ==
[seq ↑[i]_
(c3 ldisk)
| i <- cs2'])
8e3 8ee
rewrite cliftrK in pp4Pcs2' pp4cs2'E.396 39b 5 864 705 86a 70b 70c 3f 888 889 391 7c 8b6 84 c4 c5 8c0 c6 8c1 3a0 8c2 8c3 8c4 8c5 8c6 3ac 8c7 8dd 8e2 8e8 8ed 8f8 3fd 906 pp4Pcs2' : path (move (rrel (n:=3 ))) `c[p4] cs2'
pp4cs2'E : last `c[p4] cs2' = ↓[last c3 cs2]
8e3 8ee
apply : leq_trans (leq_add (leqnn _) scs2'Lscs2).90a minn u v <= size cs1 + size cs2'
8ee
apply : leq_trans (geq_minl _ _) _.90a u <= size cs1 + size cs2'
8ee
apply : leq_add.
apply : leq_of_leqif (rpeg_min _ _ ) => //.
by rewrite lc1'cs1Epp4; congr `c[`p[_, _]].
apply : leq_of_leqif (lpeg_min _ _ ); rewrite -p4Ep //.90a last `c[p4] cs2' = ↓[c2]
8ee
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 //.92d (p1 != p2) && ~~ ((p1 != p2) && (p2 != p2))
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 _].396 39b 5 864 705 86a 70b 70c 3f 888 889 391 7c 8b6 84 c4 c5 8c0 c6 8c1 3a0 8c2 8c3 8c4 8c5 8c6 3ac 8dd 8e2 8e8 50 4c7 938 c3' := ↓[c3] : configuration 3 n
4db p5 := c3 ldisk : peg 3
cs2E : cs2 = [seq ↑[i]_p5 | i <- cs2']
c3'Pcs2' : path (move (rrel (n:=3 ))) c3' cs2'
8e3
have := congr1 f lc3cs2Ec2.94d f (last c3 cs2) = f c2 ->
minn u v < (size cs1 + size cs2).+1
952
rewrite cs2E /f -[c3]cunliftrK last_map !cliftr_ldisk -/p2 /=
=> p3Ep2.396 39b 5 864 705 86a 70b 70c 3f 888 889 391 7c 8b6 84 c4 c5 8c0 c6 8c1 3a0 8c2 8c3 8c4 8c5 8c6 3ac 8dd 8e2 8e8 50 4c7 938 94e 4db 94f 950 951 8ed
minn u v <
(size cs1 + size [seq ↑[i]_p5 | i <- cs2']).+1
952
by case /eqP: p3Dp2.
have p5Ep: p5 = p by rewrite /p5 /c3 !cliftr_ldisk.396 39b 5 864 705 86a 70b 70c 3f 888 889 391 7c 8b6 84 c4 c5 8c0 c6 8c1 3a0 8c2 8c3 8c4 8c5 8c6 3ac 8dd 8e2 8e8 50 4c7 938 187 188 94f 955 956 94e 957 958 959 95a 95b 95c 95d p5Ep : p5 = p
8e3
move : lc3cs2Ec2 Lcs; rewrite cs2E last_cat /= size_cat /= size_map =>
lc6cs4Ec2 Lcs.396 39b 5 864 705 86a 70b 70c 3f 888 889 391 7c 8b6 84 c4 c5 8c0 c6 8c1 3a0 8c2 8c3 8c4 8c5 8c6 3ac 8dd 50 4c7 938 187 188 94f 955 956 94e 957 958 959 95a 95b 95c 95d 96e lc6cs4Ec2 : last c4 cs4 = c2
Lcs : size cs1 + (size cs3 + (size cs4).+1 ) < m
minn u v < (size cs1 + (size cs3 + (size cs4).+1 )).+1
rewrite -addSnnS ltnS.972 minn u v <= size cs1 + ((size cs3).+1 + size cs4)
have [/eqP p6Ep1|p6Dp1] := boolP (p6 == p1).396 39b 5 864 705 86a 70b 70c 3f 888 889 391 7c 8b6 84 c4 c5 8c0 c6 8c1 3a0 8c2 8c3 8c4 8c5 8c6 3ac 8dd 50 4c7 938 187 188 94f 955 956 94e 957 958 959 95a 95b 95c 95d 96e 973 974 p6Ep1 : p6 = p1
979
have p7Ep2 : p7 = p2.
apply /eqP.
by rewrite opeg3E // p5Ep p6Ep1 opeg3E // p1Dp2 eqxx.
apply : leq_trans (_ : size (map (cliftr p1) cs1 ++ cs4) <= _).989 minn u v <= size ([seq ↑[i]_p1 | i <- cs1] ++ cs4)
apply /ltnW/IH1.989 size ([seq ↑[i]_p1 | i <- cs1] ++ cs4) < m
- 99a
by rewrite size_cat !size_map (leq_trans _ Lcs) // ltnS;
rewrite leq_add2l -addSnnS leq_addl.
- 9a4
rewrite cat_path -{1 }[c1]cunliftrK path_liftr //=.989 path (move (rrel (n:=3 ))) ↓[c1] cs1 &&
path rmove (last c1 [seq ↑[i]_p1 | i <- cs1]) cs4
9a6
rewrite c1'Pcs1.989 true &&
path rmove (last c1 [seq ↑[i]_p1 | i <- cs1]) cs4
9a6
by rewrite -{1 }[c1]cunliftrK last_map lc1'cs1Epp4
-/p1 -p6Ep1 p4Ep2 -p7Ep2.
rewrite last_cat -{1 }[c1]cunliftrK last_map.989 last ↑[last ↓[c1] cs1]_(c1 ldisk) cs4 = c2
996
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.396 39b 5 864 705 86a 70b 70c 3f 888 889 391 7c 8b6 84 c4 c5 8c0 c6 8c1 3a0 8c2 8c3 8c4 8c5 8c6 3ac 8dd 50 4c7 938 187 188 94f 955 956 94e 957 958 959 95a 95b 95c 95d 96e 973 974 982 p6Dp2 : p6 != p2
9c0 9c1
case /negP: p5Dp6.396 39b 5 864 705 86a 70b 70c 3f 888 889 391 7c 8b6 84 c4 c5 8c0 c6 8c1 3a0 8c2 8c3 8c4 8c5 8c6 3ac 8dd 50 4c7 938 187 188 94f 955 956 94e 957 959 95a 95b 95c 95d 96e 973 974 982 9c9
p5 == p6
9c1
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 _ _) _.9d8 v <= size cs1 + ((size cs3).+1 + size cs4)
rewrite -[v]addnA leq_add //.9d8 size_rpeg ↓[c1] p2 <= size cs1
apply : leq_of_leqif (rpeg_min _ _ ) => //.9d8 last ↓[c1] cs1 = `c[p2]
9e9
by rewrite lc1'cs1Epp4 p4Ep2.
apply : leq_add.9d8 2 ^ n <= (size cs3).+1
rewrite -[2 ^ _]prednK ?expn_gt0 // ltnS.
have <-: size_rpeg (↓[c3]) p1 = (2 ^ n).-1 .9d8 size_rpeg ↓[c3] p1 = (2 ^ n).-1
by rewrite cliftrK size_rpegE rpeg_ppeg ?opegDl // size_ppeg.
apply : leq_of_leqif (rpeg_min _ _) => //.9d8 last ↓[c3] cs3 = `c[p1]
9f7
by rewrite c3'cs3Epp7 p7Ep1.
have [cs4' [c4'Pcs4' lc4'cs4'Elc4cs4 /leq_of_leqif Lcs4']] :=
pathS_restrict HHr c4Pcs4.396 39b 5 864 705 86a 70b 70c 3f 888 889 391 7c 8b6 84 c4 c5 8c0 c6 8c1 3a0 8c2 8c3 8c4 8c5 8c6 3ac 8dd 50 4c7 938 187 188 94f 955 956 94e 957 958 959 95a 95b 95c 95d 96e 973 974 982 9c4 9d9 591 c4'Pcs4' : path (move (rrel (n:=3 ))) ↓[c4] cs4'
lc4'cs4'Elc4cs4 : last ↓[c4] cs4' = ↓[last c4 cs4]
Lcs4' : size cs4' <= size cs4
9f9
rewrite cliftrK p7Ep1 in c4'Pcs4'.396 39b 5 864 705 86a 70b 70c 3f 888 889 391 7c 8b6 84 c4 c5 8c0 c6 8c1 3a0 8c2 8c3 8c4 8c5 8c6 3ac 8dd 50 4c7 938 187 188 94f 955 956 94e 957 958 959 95a 95b 95c 95d 96e 973 974 982 9c4 9d9 591 a13 a14 c4'Pcs4' : path (move (rrel (n:=3 ))) `c[p1] cs4'
9f9
rewrite cliftrK p7Ep1 in lc4'cs4'Elc4cs4.396 39b 5 864 705 86a 70b 70c 3f 888 889 391 7c 8b6 84 c4 c5 8c0 c6 8c1 3a0 8c2 8c3 8c4 8c5 8c6 3ac 8dd 50 4c7 938 187 188 94f 955 956 94e 957 958 959 95a 95b 95c 95d 96e 973 974 982 9c4 9d9 591 a14 a19 lc4'cs4'Elc4cs4 : last `c[p1] cs4' = ↓[last c4 cs4]
9f9
apply : leq_trans Lcs4'.396 39b 5 864 705 86a 70b 70c 3f 888 889 391 7c 8b6 84 c4 c5 8c0 c6 8c1 3a0 8c2 8c3 8c4 8c5 8c6 3ac 8dd 50 4c7 938 187 188 94f 955 956 94e 957 958 959 95a 95b 95c 95d 96e 973 974 982 9c4 9d9 591 a19 a1e
size_rpeg ↓[c2] p1 <= size cs4'
apply : leq_of_leqif (lpeg_min _ _) => //.a22 last `c[p1] cs4' = ↓[c2]
by rewrite lc4'cs4'Elc4cs4 lc6cs4Ec2.
Qed .
Fixpoint size_rhanoi3 {n : nat} : _ _ n -> _ _ n -> nat :=
if n is n1.+1 then
fun c1 c2 : configuration 3 n1.+1 =>
let p1 := c1 ldisk in
let p2 := c2 ldisk in
let c1' := ↓[c1] in
let c2' := ↓[c2] in
if p1 == p2 then size_rhanoi3 c1' c2' else
(* one jump *)
let p := `p[p1, p2] in
let m1 := size_rpeg c1' p + size_rpeg c2' p in
(* two jumps *)
let m2 := size_rpeg c1' p2 + 2 ^ n1 + size_rpeg c2' p1
in (minn m1 m2).+1
else fun _ _ => 0 .
(* size computes the size *)
Lemma size_rhanoi3E n (c1 c2 : _ _ n) : size_rhanoi3 c1 c2 = size (rhanoi3 c1 c2).2d9 size_rhanoi3 c1 c2 = size (rhanoi3 c1 c2)
Proof .a29
elim : n c1 c2 => //= n IH c1 c2.5 IH : forall c1 c2 : configuration 3 n,
size_rhanoi3 c1 c2 = size (rhanoi3 c1 c2)
705 (if c1 ldisk == c2 ldisk
then size_rhanoi3 ↓[c1] ↓[c2]
else
(minn
(size_rpeg ↓[c1] `p[c1 ldisk, c2 ldisk] +
size_rpeg ↓[c2] `p[c1 ldisk, c2 ldisk])
(size_rpeg ↓[c1] (c2 ldisk) + 2 ^ n +
size_rpeg ↓[c2] (c1 ldisk))).+1 ) =
size
(if c1 ldisk == c2 ldisk
then
[seq ↑[i]_(c1 ldisk) | i <- rhanoi3 ↓[c1] ↓[c2]]
else
if
size_rpeg ↓[c1] `p[c1 ldisk, c2 ldisk] +
size_rpeg ↓[c2] `p[c1 ldisk, c2 ldisk] <=
size_rpeg ↓[c1] (c2 ldisk) + 2 ^ n +
size_rpeg ↓[c2] (c1 ldisk)
then
[seq ↑[i]_(c1 ldisk)
| i <- rpeg ↓[c1] `p[c1 ldisk, c2 ldisk]] ++
↑[`c[`p[c1 ldisk, c2 ldisk]]]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk)
| i <- lpeg `p[c1 ldisk, c2 ldisk] ↓[c2]]
else
[seq ↑[i]_(c1 ldisk)
| i <- rpeg ↓[c1] (c2 ldisk)] ++
↑[`c[c2 ldisk]]_(`p[c1 ldisk, c2 ldisk])
:: [seq ↑[i]_(`p[c1 ldisk, c2 ldisk])
| i <- ppeg (c2 ldisk) (c1 ldisk)] ++
↑[`c[c1 ldisk]]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk)
| i <- lpeg (c1 ldisk) ↓[c2]])
case : eqP => [E|/eqP NE].5 a31 705 E : c1 ldisk = c2 ldisk
size_rhanoi3 ↓[c1] ↓[c2] =
size [seq ↑[i]_(c1 ldisk) | i <- rhanoi3 ↓[c1] ↓[c2]]
by rewrite size_map; apply : IH.
set p := `p[_, _].5 a31 705 a3c 86a
(minn (size_rpeg ↓[c1] p + size_rpeg ↓[c2] p)
(size_rpeg ↓[c1] (c2 ldisk) + 2 ^ n +
size_rpeg ↓[c2] (c1 ldisk))).+1 =
size
(if
size_rpeg ↓[c1] p + size_rpeg ↓[c2] p <=
size_rpeg ↓[c1] (c2 ldisk) + 2 ^ n +
size_rpeg ↓[c2] (c1 ldisk)
then
[seq ↑[i]_(c1 ldisk) | i <- rpeg ↓[c1] p] ++
↑[`c[p]]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk) | i <- lpeg p ↓[c2]]
else
[seq ↑[i]_(c1 ldisk) | i <- rpeg ↓[c1] (c2 ldisk)] ++
↑[`c[c2 ldisk]]_p
:: [seq ↑[i]_p | i <- ppeg (c2 ldisk) (c1 ldisk)] ++
↑[`c[c1 ldisk]]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk)
| i <- lpeg (c1 ldisk) ↓[c2]])
set x := size_rpeg _ _; set y := size_rpeg _ _.5 a31 705 a3c 86a x := size_rpeg ↓[c1] p : nat
y := size_rpeg ↓[c2] p : nat
(minn (x + y)
(size_rpeg ↓[c1] (c2 ldisk) + 2 ^ n +
size_rpeg ↓[c2] (c1 ldisk))).+1 =
size
(if
x + y <=
size_rpeg ↓[c1] (c2 ldisk) + 2 ^ n +
size_rpeg ↓[c2] (c1 ldisk)
then
[seq ↑[i]_(c1 ldisk) | i <- rpeg ↓[c1] p] ++
↑[`c[p]]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk) | i <- lpeg p ↓[c2]]
else
[seq ↑[i]_(c1 ldisk) | i <- rpeg ↓[c1] (c2 ldisk)] ++
↑[`c[c2 ldisk]]_p
:: [seq ↑[i]_p | i <- ppeg (c2 ldisk) (c1 ldisk)] ++
↑[`c[c1 ldisk]]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk)
| i <- lpeg (c1 ldisk) ↓[c2]])
set z := size_rpeg _ _; set t := size_rpeg _ _.5 a31 705 a3c 86a a4a a4b z := size_rpeg ↓[c1] (c2 ldisk) : nat
t := size_rpeg ↓[c2] (c1 ldisk) : nat
(minn (x + y) (z + 2 ^ n + t)).+1 =
size
(if x + y <= z + 2 ^ n + t
then
[seq ↑[i]_(c1 ldisk) | i <- rpeg ↓[c1] p] ++
↑[`c[p]]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk) | i <- lpeg p ↓[c2]]
else
[seq ↑[i]_(c1 ldisk) | i <- rpeg ↓[c1] (c2 ldisk)] ++
↑[`c[c2 ldisk]]_p
:: [seq ↑[i]_p | i <- ppeg (c2 ldisk) (c1 ldisk)] ++
↑[`c[c1 ldisk]]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk)
| i <- lpeg (c1 ldisk) ↓[c2]])
rewrite fun_if.a50 (minn (x + y) (z + 2 ^ n + t)).+1 =
(if x + y <= z + 2 ^ n + t
then
size
([seq ↑[i]_(c1 ldisk) | i <- rpeg ↓[c1] p] ++
↑[`c[p]]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk) | i <- lpeg p ↓[c2]])
else
size
([seq ↑[i]_(c1 ldisk)
| i <- rpeg ↓[c1] (c2 ldisk)] ++
↑[`c[c2 ldisk]]_p
:: [seq ↑[i]_p | i <- ppeg (c2 ldisk) (c1 ldisk)] ++
↑[`c[c1 ldisk]]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk)
| i <- lpeg (c1 ldisk) ↓[c2]]))
rewrite size_cat /= size_cat /= size_cat /= !size_map.a50 (minn (x + y) (z + 2 ^ n + t)).+1 =
(if x + y <= z + 2 ^ n + t
then size (rpeg ↓[c1] p) + (size (lpeg p ↓[c2])).+1
else
size (rpeg ↓[c1] (c2 ldisk)) +
(size (ppeg (c2 ldisk) (c1 ldisk)) +
(size (lpeg (c1 ldisk) ↓[c2])).+1 ).+1 )
rewrite -!(size_rpegE, size_lpegE) /=.a50 (minn (x + y) (z + 2 ^ n + t)).+1 =
(if x + y <= z + 2 ^ n + t
then size_rpeg ↓[c1] p + (size_rpeg ↓[c2] p).+1
else
size_rpeg ↓[c1] (c2 ldisk) +
(size (ppeg (c2 ldisk) (c1 ldisk)) +
(size_rpeg ↓[c2] (c1 ldisk)).+1 ).+1 )
rewrite -/x -/y -/z -/t.a50 (minn (x + y) (z + 2 ^ n + t)).+1 =
(if x + y <= z + 2 ^ n + t
then x + y.+1
else
z + (size (ppeg (c2 ldisk) (c1 ldisk)) + t.+1 ).+1 )
rewrite size_ppeg -[_ + t.+1 ]addSnnS prednK ?expn_gt0 //.a50 (minn (x + y) (z + 2 ^ n + t)).+1 =
(if x + y <= z + 2 ^ n + t
then x + y.+1
else z + (2 ^ n + t).+1 )
rewrite !addnS.a50 (minn (x + y) (z + 2 ^ n + t)).+1 =
(if x + y <= z + 2 ^ n + t
then (x + y).+1
else (z + (2 ^ n + t)).+1 )
rewrite /minn !addnA.a50 (if x + y < z + 2 ^ n + t
then x + y
else z + 2 ^ n + t).+1 =
(if x + y <= z + 2 ^ n + t
then (x + y).+1
else (z + 2 ^ n + t).+1 )
case : leqP => LL1; case : leqP => LL2 //.5 a31 705 a3c 86a a4a a4b a51 a52 LL1 : z + 2 ^ n + t <= x + y
LL2 : x + y <= z + 2 ^ n + t
(z + 2 ^ n + t).+1 = (x + y).+1
by congr (_.+1 ); apply /eqP; rewrite eqn_leq LL1.
by congr (_.+1 ); apply /eqP; rewrite eqn_leq ltnW // ltnW.
Qed .
Lemma gdist_rhanoi3 n (c1 c2 : _ _ n) : `d[c1, c2]_rmove = size_rhanoi3 c1 c2.2d9 `d[c1, c2]_rmove = size_rhanoi3 c1 c2
Proof .a81
apply /eqP; rewrite eqn_leq.2d9 `d[c1, c2]_rmove <= size_rhanoi3 c1 c2 <=
`d[c1, c2]_rmove
rewrite [size_rhanoi3 _ _]size_rhanoi3E gdist_path_le //=; last 2 first .
- a8a
by apply : path_rhanoi3.
- a92
by apply : last_rhanoi3.
have /gpath_connect [p1 p1H] : connect rmove c1 c2 by apply : move_connect.5 2da 64b p1H : gpath rmove c1 c2 p1
a8f
rewrite (gpath_dist p1H) rhanoi3_min //; first apply : gpath_path p1H.
by apply : gpath_last p1H.
Qed .
End Hanoi3 .