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 gdist ghanoi ghanoi3.
(******************************************************************************)
(* *)
(* Linear Hanoi Problem with 3 pegs *)
(* *)
(******************************************************************************)
Set Implicit Arguments .
Unset Strict Implicit .
Unset Printing Implicit Defensive .
Section LHanoi3 .
Lemma lrel3D (p1 p2 : peg 3 ) : p1 != p2 -> lrel p1 p2 || lrel p1 `p[p1, p2].p1 != p2 -> lrel p1 p2 || lrel p1 `p[p1, p2]
Proof .2
move => p1Dp2.lrel p1 p2 || lrel p1 `p[p1, p2]
have D p3 p4 : (p3 == p4) = (val p3 == val p4).5 c _t_ : eqType
_p_ : pred _t_
_s_ : subType _p_
p3, p4 : sub_eqType _s_
(p3 == p4) = (val p3 == val p4)
by apply /eqP/idP => /val_eqP.
move : p1Dp2 (opegDl p1 p2) (opegDr p1 p2).5 D : forall (t : eqType) (p : pred t) (s : subType p)
(p3 p4 : sub_eqType s),
(p3 == p4) = (val p3 == val p4)
p1 != p2 ->
`p[p1, p2] != p1 ->
`p[p1, p2] != p2 -> lrel p1 p2 || lrel p1 `p[p1, p2]
by case : (peg3E `p[p1, p2]) => ->;
case : (peg3E p1) => ->;
case : (peg3E p2) => ->;
rewrite !D /lrel /= ?inordK .
Qed .
Lemma lrel3B (p1 p2 : peg 3 ) : p1 != p2 ->
~~ [&& lrel p1 p2, lrel p1 `p[p1, p2] & lrel p2 `p[p1, p2]].4 p1 != p2 ->
~~
[&& lrel p1 p2, lrel p1 `p[p1, p2]
& lrel p2 `p[p1, p2]]
Proof .25
have D p3 p4 : (p3 == p4) = (val p3 == val p4).
by apply /eqP/idP => /val_eqP.
move : (opegDl p1 p2) (opegDr p1 p2).21 `p[p1, p2] != p1 ->
`p[p1, p2] != p2 ->
p1 != p2 ->
~~
[&& lrel p1 p2, lrel p1 `p[p1, p2]
& lrel p2 `p[p1, p2]]
by case : (peg3E `p[p1, p2]) => ->;
case : (peg3E p1) => ->;
case : (peg3E p2) => ->;
rewrite !D /lrel /= ?inordK .
Qed .
Lemma lrel3O (p1 p2 : peg 3 ) : p1 != p2 ->
~~ lrel p1 p2 -> lrel p1 `p[p1, p2].4 p1 != p2 -> ~~ lrel p1 p2 -> lrel p1 `p[p1, p2]
Proof .37
by move /lrel3D; case : lrel. Qed .
Lemma lrel3ON (p1 p2 : peg 3 ) : p1 != p2 ->
lrel p1 p2 -> ~~ lrel p1 `p[p1, p2] -> lrel p2 `p[p1, p2].4 p1 != p2 ->
lrel p1 p2 ->
~~ lrel p1 `p[p1, p2] -> lrel p2 `p[p1, p2]
Proof .3c
have D p3 p4 : (p3 == p4) = (val p3 == val p4).
by apply /eqP/idP => /val_eqP.
move : (opegDl p1 p2) (opegDr p1 p2).21 `p[p1, p2] != p1 ->
`p[p1, p2] != p2 ->
p1 != p2 ->
lrel p1 p2 ->
~~ lrel p1 `p[p1, p2] -> lrel p2 `p[p1, p2]
by case : (peg3E `p[p1, p2]) => ->;
case : (peg3E p1) => ->;
case : (peg3E p2) => ->;
rewrite !D /lrel /= ?inordK .
Qed .
Lemma lrel3ON4 (p1 p2 p3 p4 : peg 3 ) :
p1 != p2 -> p1 != p3 -> p2 != p3 ->
lrel p1 p2 -> lrel p1 p3 -> lrel p3 p4 -> p4 = p1.p1 != p2 ->
p1 != p3 ->
p2 != p3 ->
lrel p1 p2 -> lrel p1 p3 -> lrel p3 p4 -> p4 = p1
Proof .4c
have D p5 p6 : (p5 == p6) = (val p5 == val p6).4f 12 13 14 p5, p6 : sub_eqType _s_
(p5 == p6) = (val p5 == val p6)
by apply /eqP/idP => /val_eqP.
by case : (peg3E p1) => ->;
case : (peg3E p2) => ->;
case : (peg3E p3) => ->;
case : (peg3E p4) => ->;
rewrite !D /lrel /= ?inordK .
Qed .
Local Notation "c1 `-->_r c2" := (lmove c1 c2)
(format "c1 `-->_r c2" , at level 60 ).
Local Notation "c1 `-->*_r c2" := (connect lmove c1 c2)
(format "c1 `-->*_r c2" , at level 60 ).
(******************************************************************************)
(* Function that builds a path from a configuration to a peg *)
(******************************************************************************)
Fixpoint lhanoi3 {n : nat} : configuration 3 n -> configuration _ n -> _ :=
match n with
| 0 => fun _ _ => [::] : seq (configuration _ 0 )
| _.+1 =>
fun c1 c2 =>
let p1 := c1 ldisk in
let p2 := c2 ldisk in
if p1 == p2 then [seq ↑[i]_p2 | i <- lhanoi3 ↓[c1] ↓[c2]] else
let p3 := `p[p1, p2] in
if lrel p1 p2 then
[seq ↑[i]_p1 | i <- lhanoi3 ↓[c1] `c[p3]] ++
[seq ↑[i]_p2 | i <- `c[p3] :: lhanoi3 `c[p3] ↓[c2]]
else
[seq ↑[i]_p1 | i <- lhanoi3 ↓[c1] `c[p2]] ++
[seq ↑[i]_p3 | i <- `c[p2] :: lhanoi3 `c[p2] `c[p1]] ++
[seq ↑[i]_p2 | i <- `c[p1] :: lhanoi3 `c[p1] ↓[c2]]
end .
Lemma lhanoi3_nil_inv n (c1 c2 : _ _ n) : lhanoi3 c1 c2 = [::] -> c1 = c2.n : nat
c1, c2 : configuration 3 n
lhanoi3 c1 c2 = [::] -> c1 = c2
Proof .60
elim : n c1 c2 => [c1 c2 _|n IH c1 c2] /=; first by apply /ffunP=> [] [].63 IH : forall c1 c2 : configuration 3 n,
lhanoi3 c1 c2 = [::] -> c1 = c2
c1, c2 : configuration 3 n.+1
(if c1 ldisk == c2 ldisk
then [seq ↑[i]_(c2 ldisk) | i <- lhanoi3 ↓[c1] ↓[c2]]
else
if lrel (c1 ldisk) (c2 ldisk)
then
[seq ↑[i]_(c1 ldisk)
| i <- lhanoi3 ↓[c1] `c[`p[c1 ldisk, c2 ldisk]]] ++
↑[`c[`p[c1 ldisk, c2 ldisk]]]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk)
| i <- lhanoi3 `c[`p[c1 ldisk, c2 ldisk]]
↓[c2]]
else
[seq ↑[i]_(c1 ldisk)
| i <- lhanoi3 ↓[c1] `c[c2 ldisk]] ++
↑[`c[c2 ldisk]]_(`p[c1 ldisk, c2 ldisk])
:: [seq ↑[i]_(`p[c1 ldisk, c2 ldisk])
| i <- lhanoi3 `c[c2 ldisk] `c[c1 ldisk]] ++
↑[`c[c1 ldisk]]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk)
| i <- lhanoi3 `c[c1 ldisk] ↓[c2]]) = [::] ->
c1 = c2
case : eqP => [H | H] //=; last by case : lrel; case : map.63 6b 6c H : c1 ldisk = c2 ldisk
[seq ↑[i]_(c2 ldisk) | i <- lhanoi3 ↓[c1] ↓[c2]] =
[::] -> c1 = c2
rewrite -{2 }[c1]cunliftrK -{3 }[c2]cunliftrK.71 [seq ↑[i]_(c2 ldisk) | i <- lhanoi3 ↓[c1] ↓[c2]] =
[::] -> ↑[↓[c1]]_(c1 ldisk) = ↑[↓[c2]]_(c2 ldisk)
case : lhanoi3 (IH ↓[c1] ↓[c2]) => //= -> // _.71 ↑[↓[c2]]_(c1 ldisk) = ↑[↓[c2]]_(c2 ldisk)
by rewrite H.
Qed .
Lemma last_lhanoi3 n (c1 c2 : _ _ n) (cs := lhanoi3 c1 c2) :
last c1 cs = c2.63 64 cs := lhanoi3 c1 c2 : seq (configuration 3 n)
last c1 cs = c2
Proof .7d
have HH := @lirr 3 .63 64 80 HH : irreflexive (lrel (n:=3 ))
81
rewrite /cs; elim : n c1 c2 {cs} => /= [c1 c2| n IH c1 c2].87 c1, c2 : configuration 3 0
c1 = c2
by apply /ffunP=> [] [].
case : eqP => [Ho|/eqP Do].87 63 91 6c Ho : c1 ldisk = c2 ldisk
last c1
[seq ↑[i]_(c2 ldisk) | i <- lhanoi3 ↓[c1] ↓[c2]] =
c2
by rewrite -{1 }[c1](cunliftrK) Ho last_map IH // cunliftrK.
set p1 := _ ldisk; set p2 := opeg _ _.87 63 91 6c 9f p1 := c1 ldisk : (fun => peg 3 ) ldisk
p2 := `p[p1, c2 ldisk] : peg 3
last c1
(if lrel p1 (c2 ldisk)
then
[seq ↑[i]_p1 | i <- lhanoi3 ↓[c1] `c[p2]] ++
↑[`c[p2]]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk)
| i <- lhanoi3 `c[p2] ↓[c2]]
else
[seq ↑[i]_p1 | i <- lhanoi3 ↓[c1] `c[c2 ldisk]] ++
↑[`c[c2 ldisk]]_p2
:: [seq ↑[i]_p2
| i <- lhanoi3 `c[c2 ldisk] `c[p1]] ++
↑[`c[p1]]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk)
| i <- lhanoi3 `c[p1] ↓[c2]]) = c2
set cp2 := `c[_]; set cp := `c[_]; set cp1 := `c[_].87 63 91 6c 9f a8 a9 cp2 := `c[p2] : configuration 3 n
cp := `c[c2 ldisk] : configuration 3 n
cp1 := `c[p1] : configuration 3 n
last c1
(if lrel p1 (c2 ldisk)
then
[seq ↑[i]_p1 | i <- lhanoi3 ↓[c1] cp2] ++
↑[cp2]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk) | i <- lhanoi3 cp2 ↓[c2]]
else
[seq ↑[i]_p1 | i <- lhanoi3 ↓[c1] cp] ++
↑[cp]_p2
:: [seq ↑[i]_p2 | i <- lhanoi3 cp cp1] ++
↑[cp1]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk)
| i <- lhanoi3 cp1 ↓[c2]]) = c2
case : (boolP (lrel _ _)) => [Hrel|Hrel].87 63 91 6c 9f a8 a9 af b0 b1 Hrel : lrel p1 (c2 ldisk)
last c1
([seq ↑[i]_p1 | i <- lhanoi3 ↓[c1] cp2] ++
↑[cp2]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk) | i <- lhanoi3 cp2 ↓[c2]]) =
c2
by rewrite last_cat /= last_map IH cunliftrK.
by rewrite last_cat /= last_cat /= last_map IH cunliftrK.
Qed .
Lemma path_lhanoi3 n (c1 c2 : _ _ n) (cs := lhanoi3 c1 c2) :
path lmove c1 cs.
Proof .c2
have HH := @lirr 3 .
rewrite /cs; elim : n c1 c2 {cs} => //= n IH c1 c2.87 63 IH : forall c1 c2 : configuration 3 n,
path lmove c1 (lhanoi3 c1 c2)
6c path lmove c1
(if c1 ldisk == c2 ldisk
then
[seq ↑[i]_(c2 ldisk) | i <- lhanoi3 ↓[c1] ↓[c2]]
else
if lrel (c1 ldisk) (c2 ldisk)
then
[seq ↑[i]_(c1 ldisk)
| i <- lhanoi3 ↓[c1]
`c[`p[c1 ldisk, c2 ldisk]]] ++
↑[`c[`p[c1 ldisk, c2 ldisk]]]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk)
| i <- lhanoi3 `c[`p[c1 ldisk, c2 ldisk]]
↓[c2]]
else
[seq ↑[i]_(c1 ldisk)
| i <- lhanoi3 ↓[c1] `c[c2 ldisk]] ++
↑[`c[c2 ldisk]]_(`p[c1 ldisk, c2 ldisk])
:: [seq ↑[i]_(`p[c1 ldisk, c2 ldisk])
| i <- lhanoi3 `c[c2 ldisk] `c[c1 ldisk]] ++
↑[`c[c1 ldisk]]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk)
| i <- lhanoi3 `c[c1 ldisk] ↓[c2]])
case : eqP => [Ho|/eqP Do].87 63 cd 6c 9a
path lmove c1
[seq ↑[i]_(c2 ldisk) | i <- lhanoi3 ↓[c1] ↓[c2]]
by rewrite -{1 }[c1](cunliftrK) Ho path_liftr.
set p1 := _ ldisk; set p2 := opeg _ _.87 63 cd 6c 9f a8 a9
path lmove c1
(if lrel p1 (c2 ldisk)
then
[seq ↑[i]_p1 | i <- lhanoi3 ↓[c1] `c[p2]] ++
↑[`c[p2]]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk)
| i <- lhanoi3 `c[p2] ↓[c2]]
else
[seq ↑[i]_p1 | i <- lhanoi3 ↓[c1] `c[c2 ldisk]] ++
↑[`c[c2 ldisk]]_p2
:: [seq ↑[i]_p2
| i <- lhanoi3 `c[c2 ldisk] `c[p1]] ++
↑[`c[p1]]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk)
| i <- lhanoi3 `c[p1] ↓[c2]])
set cp2 := `c[_]; set cp := `c[_]; set cp1 := `c[_].87 63 cd 6c 9f a8 a9 af b0 b1
path lmove c1
(if lrel p1 (c2 ldisk)
then
[seq ↑[i]_p1 | i <- lhanoi3 ↓[c1] cp2] ++
↑[cp2]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk) | i <- lhanoi3 cp2 ↓[c2]]
else
[seq ↑[i]_p1 | i <- lhanoi3 ↓[c1] cp] ++
↑[cp]_p2
:: [seq ↑[i]_p2 | i <- lhanoi3 cp cp1] ++
↑[cp1]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk)
| i <- lhanoi3 cp1 ↓[c2]])
case : (boolP (lrel _ _)) => [Hrel|Hrel].87 63 cd 6c 9f a8 a9 af b0 b1 b7
path lmove c1
([seq ↑[i]_p1 | i <- lhanoi3 ↓[c1] cp2] ++
↑[cp2]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk) | i <- lhanoi3 cp2 ↓[c2]])
rewrite cat_path /=; apply /and3P; repeat split .e8 path lmove c1 [seq ↑[i]_p1 | i <- lhanoi3 ↓[c1] cp2]
- ef
by rewrite -{1 }[c1]cunliftrK path_liftr.
- f9
rewrite -{1 }[c1]cunliftrK last_map last_lhanoi3.e8 ↑[cp2]_(c1 ldisk) `-->_r ↑[cp2]_(c2 ldisk)
fb
by apply : move_liftr_perfect; rewrite // eq_sym (opegDl, opegDr).
by rewrite path_liftr.
rewrite cat_path /= cat_path /=; apply /and5P; split .ec path lmove c1 [seq ↑[i]_p1 | i <- lhanoi3 ↓[c1] cp]
- 108
by rewrite -{1 }[c1]cunliftrK /= path_liftr.
- 116
rewrite -{1 }[c1]cunliftrK /= last_map last_lhanoi3.ec ↑[cp]_(c1 ldisk) `-->_r ↑[cp]_p2
118
- 11b
apply : move_liftr_perfect => //; first by apply : lrel3O.
by rewrite opegDr.
- 124
by rewrite path_liftr.
- 129
rewrite last_map last_lhanoi3.ec ↑[cp1]_p2 `-->_r ↑[cp1]_(c2 ldisk)
12b
apply : move_liftr_perfect => //.
- 132
rewrite /p2 opeg_sym lsym lrel3O ?opegDl //; first by rewrite eq_sym.ec ~~ lrel (c2 ldisk) p1
135
by rewrite lsym.
- 140
by rewrite opegDl.
by rewrite eq_sym.
by rewrite path_liftr.
Qed .
(* Two configurations are always connected *)
Lemma move_lconnect3 n (c1 c2 : configuration 3 n) : c1 `-->*_r c2.
Proof .14b
apply /connectP; exists (lhanoi3 c1 c2 ); first by apply : path_lhanoi3.62 c2 = last c1 (lhanoi3 c1 c2)
by rewrite last_lhanoi3.
Qed .
(* lhanoi gives the smallest path connecting c1 to c2 *)
(* This path is unique *)
Lemma lhanoi3_min n (c1 c2 : configuration 3 n) cs :
path lmove c1 cs -> last c1 cs = c2 ->
size (lhanoi3 c1 c2) <= size cs ?= iff (cs == lhanoi3 c1 c2).63 64 cs : seq (configuration 3 n)
path lmove c1 cs ->
last c1 cs = c2 ->
size (lhanoi3 c1 c2) <= size cs
?= iff (cs == lhanoi3 c1 c2)
Proof .154
(* we adapt the proof for the standard ha
noi problem
surely a shorter proof exists *)
have [m sLm] := ubnP (size cs); elim : m => // m IHm in n c1 c2 cs sLm *.m : nat
IHm : forall (n : nat) (c1 c2 : configuration 3 n) (cs : seq (configuration 3 n)),
size cs < m ->
path lmove c1 cs ->
last c1 cs = c2 ->
size (lhanoi3 c1 c2) <= size cs ?= iff (cs == lhanoi3 c1 c2)
63 64 157 sLm : size cs < m.+1
158
(* The usual induction on the number of disks *)
elim : n c1 c2 cs sLm => [c1 p [|] //=|n IH c1 c cs Scs c1Pcs lc1csEp /=].15e 15f 63 IH : forall (c1 c2 : configuration 3 n)
(cs : seq (configuration 3 n)),
size cs < m.+1 ->
path lmove c1 cs ->
last c1 cs = c2 ->
size (lhanoi3 c1 c2) <= size cs
?= iff (cs == lhanoi3 c1 c2)
c1, c : configuration 3 n.+1
cs : seq (configuration 3 n.+1 )
Scs : size cs < m.+1
c1Pcs : path lmove c1 cs
lc1csEp : last c1 cs = c
size
(if c1 ldisk == c ldisk
then [seq ↑[i]_(c ldisk) | i <- lhanoi3 ↓[c1] ↓[c]]
else
if lrel (c1 ldisk) (c ldisk)
then
[seq ↑[i]_(c1 ldisk)
| i <- lhanoi3 ↓[c1] `c[`p[c1 ldisk, c ldisk]]] ++
↑[`c[`p[c1 ldisk, c ldisk]]]_(c ldisk)
:: [seq ↑[i]_(c ldisk)
| i <- lhanoi3 `c[`p[c1 ldisk, c ldisk]]
↓[c]]
else
[seq ↑[i]_(c1 ldisk)
| i <- lhanoi3 ↓[c1] `c[c ldisk]] ++
↑[`c[c ldisk]]_(`p[c1 ldisk, c ldisk])
:: [seq ↑[i]_(`p[c1 ldisk, c ldisk])
| i <- lhanoi3 `c[c ldisk] `c[c1 ldisk]] ++
↑[`c[c1 ldisk]]_(c ldisk)
:: [seq ↑[i]_(c ldisk)
| i <- lhanoi3 `c[c1 ldisk] ↓[c]]) <=
size
cs
?= iff
(cs ==
(if
c1
ldisk ==
c
ldisk
then
[
seq ↑[i]_
(c
ldisk)
| i <-
lhanoi3
↓[c1]
↓[c]]
else
if
lrel
(c1
ldisk)
(c
ldisk)
then
[
seq ↑[i]_
(c1
ldisk)
| i <-
lhanoi3
↓[c1]
`c[`p[
c1
ldisk,
c
ldisk]]] ++
↑[`c[`p[
c1
ldisk,
c
ldisk]]]_
(c
ldisk)
:: [
seq ↑[i]_
(c
ldisk)
| i <-
lhanoi3
`c[`p[
c1
ldisk,
c
ldisk]]
↓[c]]
else
[
seq ↑[i]_
(c1
ldisk)
| i <-
lhanoi3
↓[c1]
`c[
c
ldisk]] ++
↑[`c[
c
ldisk]]_
(`p[
c1
ldisk,
c
ldisk])
::
[
seq ↑[i]_
(`p[
c1
ldisk,
c
ldisk])
| i <-
lhanoi3
`c[
c
ldisk]
`c[
c1
ldisk]] ++
↑[`c[
c1
ldisk]]_
(c
ldisk)
:: [
seq ↑[i]_
(c
ldisk)
| i <-
lhanoi3
`c[
c1
ldisk]
↓[c]]))
set (p := c ldisk).15e 15f 63 165 166 167 168 169 16a p := c ldisk : (fun => peg 3 ) ldisk
size
(if c1 ldisk == p
then [seq ↑[i]_p | i <- lhanoi3 ↓[c1] ↓[c]]
else
if lrel (c1 ldisk) p
then
[seq ↑[i]_(c1 ldisk)
| i <- lhanoi3 ↓[c1] `c[`p[c1 ldisk, p]]] ++
↑[`c[`p[c1 ldisk, p]]]_p
:: [seq ↑[i]_p
| i <- lhanoi3 `c[`p[c1 ldisk, p]] ↓[c]]
else
[seq ↑[i]_(c1 ldisk) | i <- lhanoi3 ↓[c1] `c[p]] ++
↑[`c[p]]_(`p[c1 ldisk, p])
:: [seq ↑[i]_(`p[c1 ldisk, p])
| i <- lhanoi3 `c[p] `c[c1 ldisk]] ++
↑[`c[c1 ldisk]]_p
:: [seq ↑[i]_p
| i <- lhanoi3 `c[c1 ldisk] ↓[c]]) <=
size
cs
?= iff
(cs ==
(if
c1
ldisk ==
p
then
[
seq ↑[i]_p
| i <-
lhanoi3
↓[c1]
↓[c]]
else
if
lrel
(c1
ldisk)
p
then
[
seq ↑[i]_
(c1
ldisk)
| i <-
lhanoi3
↓[c1]
`c[`p[
c1
ldisk, p]]] ++
↑[`c[`p[
c1
ldisk, p]]]_p
:: [
seq ↑[i]_p
| i <-
lhanoi3
`c[`p[
c1
ldisk, p]]
↓[c]]
else
[
seq ↑[i]_
(c1
ldisk)
| i <-
lhanoi3
↓[c1]
`c[p]] ++
↑[`c[p]]_
(`p[
c1
ldisk, p])
::
[
seq ↑[i]_
(`p[
c1
ldisk, p])
| i <-
lhanoi3
`c[p]
`c[
c1
ldisk]] ++
↑[`c[
c1
ldisk]]_p
:: [
seq ↑[i]_p
| i <-
lhanoi3
`c[
c1
ldisk]
↓[c]]))
rewrite !fun_if !size_cat /= !size_cat /= !size_map.16f if c1 ldisk == p
then
(if c1 ldisk == p
then leqif (size (lhanoi3 ↓[c1] ↓[c]))
else
if lrel (c1 ldisk) p
then
leqif
(size (lhanoi3 ↓[c1] `c[`p[c1 ldisk, p]]) +
(size (lhanoi3 `c[`p[c1 ldisk, p]] ↓[c])).+1 )
else
leqif
(size (lhanoi3 ↓[c1] `c[p]) +
(size (lhanoi3 `c[p] `c[c1 ldisk]) +
(size (lhanoi3 `c[c1 ldisk] ↓[c])).+1 ).+1 ))
(size cs)
(cs == [seq ↑[i]_p | i <- lhanoi3 ↓[c1] ↓[c]])
else
if lrel (c1 ldisk) p
then
(if c1 ldisk == p
then leqif (size (lhanoi3 ↓[c1] ↓[c]))
else
if lrel (c1 ldisk) p
then
leqif
(size (lhanoi3 ↓[c1] `c[`p[c1 ldisk, p]]) +
(size (lhanoi3 `c[`p[c1 ldisk, p]] ↓[c])).+1 )
else
leqif
(size (lhanoi3 ↓[c1] `c[p]) +
(size (lhanoi3 `c[p] `c[c1 ldisk]) +
(size (lhanoi3 `c[c1 ldisk] ↓[c])).+1 ).+1 ))
(size cs)
(cs ==
[seq ↑[i]_(c1 ldisk)
| i <- lhanoi3 ↓[c1] `c[`p[c1 ldisk, p]]] ++
↑[`c[`p[c1 ldisk, p]]]_p
:: [seq ↑[i]_p
| i <- lhanoi3 `c[`p[c1 ldisk, p]] ↓[c]])
else
(if c1 ldisk == p
then leqif (size (lhanoi3 ↓[c1] ↓[c]))
else
if lrel (c1 ldisk) p
then
leqif
(size (lhanoi3 ↓[c1] `c[`p[c1 ldisk, p]]) +
(size (lhanoi3 `c[`p[c1 ldisk, p]] ↓[c])).+1 )
else
leqif
(size (lhanoi3 ↓[c1] `c[p]) +
(size (lhanoi3 `c[p] `c[c1 ldisk]) +
(size (lhanoi3 `c[c1 ldisk] ↓[c])).+1 ).+1 ))
(size cs)
(cs ==
[seq ↑[i]_(c1 ldisk) | i <- lhanoi3 ↓[c1] `c[p]] ++
↑[`c[p]]_(`p[c1 ldisk, p])
:: [seq ↑[i]_(`p[c1 ldisk, p])
| i <- lhanoi3 `c[p] `c[c1 ldisk]] ++
↑[`c[c1 ldisk]]_p
:: [seq ↑[i]_p
| i <- lhanoi3 `c[c1 ldisk] ↓[c]])
case : (c1 _ =P p) => [lc1Ep |/eqP lc1Dp].15e 15f 63 165 166 167 168 169 16a 170 lc1Ep : c1 ldisk = p
size (lhanoi3 ↓[c1] ↓[c]) <= size cs
?= iff (cs ==
[seq ↑[i]_p
| i <- lhanoi3
↓[c1]
↓[c]])
(* the largest disk is already well-placed *)
have [cs1 [c1'Pcs1 lc1'csElc1cs' /leqifP]] :=
pathS_restrict (@lirr 3 ) c1Pcs.15e 15f 63 165 166 167 168 169 16a 170 17a cs1 : seq (configuration 3 n)
c1'Pcs1 : path (move (lrel (n:=3 ))) ↓[c1] cs1
lc1'csElc1cs' : 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 (lhanoi3 ↓[c1] ↓[c]) <= size cs
?= iff (cs ==
[seq ↑[i]_p
| i <- lhanoi3
↓[c1]
↓[c]])
17c
have lc1'cs1E : last ↓[c1] cs1 = ↓[c].
by rewrite lc1'csElc1cs'; congr cunliftr.15e 15f 63 165 166 167 168 169 16a 170 17a 187 188 189 192
18a 17c
case : eqP=> [csEcs1 /eqP<- |/eqP csDcs1 scs1L].15e 15f 63 165 166 167 168 169 16a 170 17a 187 188 189 192 csEcs1 : cs = [seq ↑[i]_(c1 ldisk) | i <- cs1]
size (lhanoi3 ↓[c1] ↓[c]) <= size cs1
?= iff (cs ==
[seq ↑[i]_p
| i <- lhanoi3
↓[c1]
↓[c]])
rewrite csEcs1 lc1Ep eq_map_liftr.19b size (lhanoi3 ↓[c1] ↓[c]) <= size cs1
?= iff (cs1 ==
lhanoi3 ↓[c1] ↓[c])
19e
apply : IH => //.15e 15f 63 166 167 168 169 16a 170 17a 187 188 189 192 19c
size cs1 < m.+1
19e
by move : Scs; rewrite csEcs1 size_map.15e 15f 63 165 166 167 168 169 16a 170 17a 187 188 189 192 1a1 1a2
17b 17c
apply /leqifP; case : eqP => [->//|_].1b0 size (lhanoi3 ↓[c1] ↓[c]) ==
size [seq ↑[i]_p | i <- lhanoi3 ↓[c1] ↓[c]]
by rewrite size_map.
apply : leq_ltn_trans (scs1L).1b0 size (lhanoi3 ↓[c1] ↓[c]) <= size cs1
17c
apply : IH => //.15e 15f 63 166 167 168 169 16a 170 17a 187 188 189 192 1a1 1a2
1ac 17c
by apply : ltn_trans Scs.15e 15f 63 165 166 167 168 169 16a 170 181
182
pose f (c : configuration 3 n.+1 ) := c ldisk.15e 15f 63 165 166 167 168 169 16a 170 181 f := fun_of_fin^~ ldisk : configuration 3 n.+1 -> (fun => peg 3 ) ldisk
182
have HHr := @lirr 3 .15e 15f 63 165 166 167 168 169 16a 170 181 1cb HHr : irreflexive (lrel (n:=3 ))
182
have HHs := @lsym 3 .15e 15f 63 165 166 167 168 169 16a 170 181 1cb 1d0 HHs : symmetric (lrel (n:=3 ))
182
(* We need to move the largest disk *)
case : path3SP c1Pcs => // [c1' cs' p1 csE c1'Ecs1'|
cs1 cs2 p1 p2 p3 c1' c2 p1Dp2 p1Rp2
lc1'cs1Epp3 csE c1'Pcs1 c2Pcs2 _].15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 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'Ecs1' : path (move (lrel (n:=3 ))) c1' cs'
true ->
if lrel (c1 ldisk) p
then
(if lrel (c1 ldisk) p
then
leqif
(size (lhanoi3 ↓[c1] `c[`p[c1 ldisk, p]]) +
(size (lhanoi3 `c[`p[c1 ldisk, p]] ↓[c])).+1 )
else
leqif
(size (lhanoi3 ↓[c1] `c[p]) +
(size (lhanoi3 `c[p] `c[c1 ldisk]) +
(size (lhanoi3 `c[c1 ldisk] ↓[c])).+1 ).+1 ))
(size cs)
(cs ==
[seq ↑[i]_(c1 ldisk)
| i <- lhanoi3 ↓[c1] `c[`p[c1 ldisk, p]]] ++
↑[`c[`p[c1 ldisk, p]]]_p
:: [seq ↑[i]_p
| i <- lhanoi3 `c[`p[c1 ldisk, p]] ↓[c]])
else
(if lrel (c1 ldisk) p
then
leqif
(size (lhanoi3 ↓[c1] `c[`p[c1 ldisk, p]]) +
(size (lhanoi3 `c[`p[c1 ldisk, p]] ↓[c])).+1 )
else
leqif
(size (lhanoi3 ↓[c1] `c[p]) +
(size (lhanoi3 `c[p] `c[c1 ldisk]) +
(size (lhanoi3 `c[c1 ldisk] ↓[c])).+1 ).+1 ))
(size cs)
(cs ==
[seq ↑[i]_(c1 ldisk) | i <- lhanoi3 ↓[c1] `c[p]] ++
↑[`c[p]]_(`p[c1 ldisk, p])
:: [seq ↑[i]_(`p[c1 ldisk, p])
| i <- lhanoi3 `c[p] `c[c1 ldisk]] ++
↑[`c[c1 ldisk]]_p
:: [seq ↑[i]_p
| i <- lhanoi3 `c[c1 ldisk] ↓[c]])
(* this case is impossible the largest disk has to move *)
case /eqP: lc1Dp.15e 15f 63 165 166 167 168 16a 170 1cb 1d0 1d5 1da 1db 1dc 1dd 1de
c1 ldisk = p
1e0
move : lc1csEp => /(congr1 f).15e 15f 63 165 166 167 168 170 1cb 1d0 1d5 1da 1db 1dc 1dd 1de
f (last c1 cs) = f c -> c1 ldisk = p
1e0
by rewrite /f csE -{1 }[c1]cunliftrK last_map cliftr_ldisk.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 1eb
182
(* c4 is the first configuration when the largest disk has moved *)
rewrite csE size_cat -/p1.1f9 if lrel p1 p
then
(if lrel p1 p
then
leqif
(size (lhanoi3 ↓[c1] `c[`p[p1, p]]) +
(size (lhanoi3 `c[`p[p1, p]] ↓[c])).+1 )
else
leqif
(size (lhanoi3 ↓[c1] `c[p]) +
(size (lhanoi3 `c[p] `c[p1]) +
(size (lhanoi3 `c[p1] ↓[c])).+1 ).+1 ))
(size [seq ↑[i]_p1 | i <- cs1] + size (c2 :: cs2))
([seq ↑[i]_p1 | i <- cs1] ++ c2 :: cs2 ==
[seq ↑[i]_p1 | i <- lhanoi3 ↓[c1] `c[`p[p1, p]]] ++
↑[`c[`p[p1, p]]]_p
:: [seq ↑[i]_p | i <- lhanoi3 `c[`p[p1, p]] ↓[c]])
else
(if lrel p1 p
then
leqif
(size (lhanoi3 ↓[c1] `c[`p[p1, p]]) +
(size (lhanoi3 `c[`p[p1, p]] ↓[c])).+1 )
else
leqif
(size (lhanoi3 ↓[c1] `c[p]) +
(size (lhanoi3 `c[p] `c[p1]) +
(size (lhanoi3 `c[p1] ↓[c])).+1 ).+1 ))
(size [seq ↑[i]_p1 | i <- cs1] + size (c2 :: cs2))
([seq ↑[i]_p1 | i <- cs1] ++ c2 :: cs2 ==
[seq ↑[i]_p1 | i <- lhanoi3 ↓[c1] `c[p]] ++
↑[`c[p]]_(`p[p1, p])
:: [seq ↑[i]_(`p[p1, p])
| i <- lhanoi3 `c[p] `c[p1]] ++
↑[`c[p1]]_p
:: [seq ↑[i]_p | i <- lhanoi3 `c[p1] ↓[c]])
have Scs1 : size cs1 < m.+1 .
apply : ltn_trans Scs.15e 15f 63 165 166 167 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 1eb
size cs1 < size cs
201
by rewrite csE size_cat /= size_map addnS ltnS leq_addr.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 1eb 204
1fd
have Scs2 : size cs2 < m.+1 .
apply : ltn_trans Scs.15e 15f 63 165 166 167 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 1eb 204
size cs2 < size cs
212
by rewrite csE size_cat /= size_map addnS ltnS leq_addl.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 1eb 204 215
1fd
have [p1Rp| p1NRp] := boolP (lrel p1 p).15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 1eb 204 215 p1Rp : lrel p1 p
size (lhanoi3 ↓[c1] `c[`p[p1, p]]) +
(size (lhanoi3 `c[`p[p1, p]] ↓[c])).+1 <= size
[seq ↑[i]_p1
| i <- cs1] +
size
(c2 :: cs2)
?= iff ([seq ↑[i]_p1
| i <- cs1] ++
c2
:: cs2 ==
[seq ↑[i]_p1
| i <-
lhanoi3
↓[c1]
`c[`p[p1, p]]] ++
↑[`c[`p[p1, p]]]_p
:: [
seq ↑[i]_p
| i <-
lhanoi3
`c[`p[p1, p]]
↓[c]])
case : (p2 =P p) => [p2Ep|/eqP p2Dp].15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 1eb 204 215 223 p2Ep : p2 = p
224
(* the first moves of largest disk of cs is the right one *)
rewrite -p2Ep -/p3 size_map /=.22d size (lhanoi3 ↓[c1] `c[p3]) +
(size (lhanoi3 `c[p3] ↓[c])).+1 <= size cs1 +
(size cs2).+1
?= iff ([seq ↑[i]_p1
| i <- cs1] ++
c2 :: cs2 ==
[seq ↑[i]_p1
| i <-
lhanoi3 ↓[c1]
`c[p3]] ++
↑[`c[p3]]_p2
:: [seq ↑[i]_p2
| i <-
lhanoi3
`c[p3]
↓[c]])
22f
have /(pathS_restrict (@lirr 3 ))[cs2' [c2'Pcs2' lc2'cs2'E cs2'L]] := c2Pcs2.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 1eb 204 215 223 22e cs2' : seq (configuration 3 n)
c2'Pcs2' : path (move (lrel (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'])
237 22f
have Scs2' : size cs2' < m.+1 .
by apply : leq_ltn_trans Scs2; rewrite cs2'L.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 1eb 204 215 223 22e 23c 23d 23e 23f 247
237 22f
have /IH := lc1'cs1Epp3 => // /(_ Scs1 c1'Pcs1) IHc1.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 1eb 204 215 223 22e 23c 23d 23e 23f 247 IHc1 : size (lhanoi3 c1' `c[p3])
<= size cs1
?= iff (cs1 == lhanoi3 c1' `c[p3])
237 22f
have /IH : last ↓[c2] cs2' = ↓[c]
=> [| /(_ Scs2' c2'Pcs2') IHc2].250 last ↓[c2] cs2' = ↓[c]
rewrite lc2'cs2'E; congr cunliftr.
by move : lc1csEp; rewrite csE last_cat /= => ->.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 1eb 204 215 223 22e 23c 23d 23e 23f 247 251 259
237 22f
rewrite cliftrK in IHc2.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 1eb 204 215 223 22e 23c 23d 23e 23f 247 251 IHc2 : size (lhanoi3 `c[p3] ↓[c])
<= size cs2'
?= iff (cs2' == lhanoi3 `c[p3] ↓[c])
237 22f
move /leqifP : cs2'L.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 1eb 204 215 223 22e 23c 23d 23e 247 251 266
(if cs2 == [seq ↑[i]_(c2 ldisk) | i <- cs2']
then size cs2' == size cs2
else size cs2' < size cs2) ->
size (lhanoi3 ↓[c1] `c[p3]) +
(size (lhanoi3 `c[p3] ↓[c])).+1 <= size cs1 +
(size cs2).+1
?= iff ([seq ↑[i]_p1
| i <- cs1] ++
c2 :: cs2 ==
[seq ↑[i]_p1
| i <-
lhanoi3 ↓[c1]
`c[p3]] ++
↑[`c[p3]]_p2
:: [seq ↑[i]_p2
| i <-
lhanoi3
`c[p3]
↓[c]])
22f
case : eqP => [cs2E _ | /eqP cs2D Lcs2].15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 1eb 204 215 223 22e 23c 23d 23e 247 251 266 cs2E : cs2 = [seq ↑[i]_(c2 ldisk) | i <- cs2']
237
(* there is only one move of the largest disk in cs *)
rewrite cs2E size_map cliftr_ldisk /=.26f size (lhanoi3 ↓[c1] `c[p3]) +
(size (lhanoi3 `c[p3] ↓[c])).+1 <= size cs1 +
(size cs2').+1
?= iff ([seq ↑[i]_p1
| i <- cs1] ++
c2
:: [seq ↑[i]_p2
| i <- cs2'] ==
[seq ↑[i]_p1
| i <-
lhanoi3 ↓[c1]
`c[p3]] ++
↑[`c[p3]]_p2
:: [seq ↑[i]_p2
| i <-
lhanoi3
`c[p3]
↓[c]])
271
have /leqifP := IHc1; case : eqP => [->_ |_ Lc1].26f size (lhanoi3 ↓[c1] `c[p3]) +
(size (lhanoi3 `c[p3] ↓[c])).+1 <= size
(lhanoi3 c1'
`c[p3]) +
(size cs2').+1
?= iff ([seq ↑[i]_p1
| i <-
lhanoi3 c1'
`c[p3]] ++
c2
:: [seq ↑[i]_p2
| i <- cs2'] ==
[seq ↑[i]_p1
| i <-
lhanoi3 ↓[c1]
`c[p3]] ++
↑[`c[p3]]_p2
:: [seq ↑[i]_p2
| i <-
lhanoi3
`c[p3]
↓[c]])
(* the first part of cs is perfect *)
have /leqifP := IHc2; case : eqP => [->_ |_ Lc2].26f size (lhanoi3 ↓[c1] `c[p3]) +
(size (lhanoi3 `c[p3] ↓[c])).+1 <= size
(lhanoi3 c1'
`c[p3]) +
(size
(lhanoi3 `c[p3]
↓[c])).+1
?= iff ([seq ↑[i]_p1
| i <-
lhanoi3 c1'
`c[p3]] ++
c2
:: [seq ↑[i]_p2
| i <-
lhanoi3
`c[p3]
↓[c]] ==
[seq ↑[i]_p1
| i <-
lhanoi3 ↓[c1]
`c[p3]] ++
↑[`c[p3]]_p2
:: [seq ↑[i]_p2
| i <-
lhanoi3
`c[p3]
↓[c]])
(* the second part of cs is perfect, only case of equality *)
apply /leqifP; case : eqP => [/(congr1 size)|[]].26f size
([seq ↑[i]_p1 | i <- lhanoi3 c1' `c[p3]] ++
c2 :: [seq ↑[i]_p2 | i <- lhanoi3 `c[p3] ↓[c]]) =
size
([seq ↑[i]_p1 | i <- lhanoi3 ↓[c1] `c[p3]] ++
↑[`c[p3]]_p2
:: [seq ↑[i]_p2 | i <- lhanoi3 `c[p3] ↓[c]]) ->
size (lhanoi3 ↓[c1] `c[p3]) +
(size (lhanoi3 `c[p3] ↓[c])).+1 ==
size (lhanoi3 c1' `c[p3]) +
(size (lhanoi3 `c[p3] ↓[c])).+1
by rewrite !size_cat /= !size_map => ->.
by congr (_ ++ _ :: _); rewrite !cliftK.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 1eb 204 215 223 22e 23c 23d 23e 247 251 266 270 28a
27d 27e
apply /leqifP; case : eqP => [/(congr1 size)|_].29a size
([seq ↑[i]_p1 | i <- lhanoi3 c1' `c[p3]] ++
c2 :: [seq ↑[i]_p2 | i <- cs2']) =
size
([seq ↑[i]_p1 | i <- lhanoi3 ↓[c1] `c[p3]] ++
↑[`c[p3]]_p2
:: [seq ↑[i]_p2 | i <- lhanoi3 `c[p3] ↓[c]]) ->
size (lhanoi3 ↓[c1] `c[p3]) +
(size (lhanoi3 `c[p3] ↓[c])).+1 ==
size (lhanoi3 c1' `c[p3]) + (size cs2').+1
by rewrite size_cat /= size_cat /= !size_map => ->.
by rewrite ltn_add2l ltnS.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 1eb 204 215 223 22e 23c 23d 23e 247 251 266 270 281
279 271
apply /leqifP; case : eqP => [/(congr1 size)|_].2a8 size
([seq ↑[i]_p1 | i <- cs1] ++
c2 :: [seq ↑[i]_p2 | i <- cs2']) =
size
([seq ↑[i]_p1 | i <- lhanoi3 ↓[c1] `c[p3]] ++
↑[`c[p3]]_p2
:: [seq ↑[i]_p2 | i <- lhanoi3 `c[p3] ↓[c]]) ->
size (lhanoi3 ↓[c1] `c[p3]) +
(size (lhanoi3 `c[p3] ↓[c])).+1 ==
size cs1 + (size cs2').+1
by rewrite !size_cat /= !size_map => ->.
by rewrite -addSn leq_add // ltnS IHc2.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 1eb 204 215 223 22e 23c 23d 23e 247 251 266 274 275
237 22f
apply /leqifP; case : eqP => [/(congr1 size)|_].2b6 size ([seq ↑[i]_p1 | i <- cs1] ++ c2 :: cs2) =
size
([seq ↑[i]_p1 | i <- lhanoi3 ↓[c1] `c[p3]] ++
↑[`c[p3]]_p2
:: [seq ↑[i]_p2 | i <- lhanoi3 `c[p3] ↓[c]]) ->
size (lhanoi3 ↓[c1] `c[p3]) +
(size (lhanoi3 `c[p3] ↓[c])).+1 ==
size cs1 + (size cs2).+1
by rewrite !size_cat /= !size_map => ->.
rewrite -addnS leq_add //= ?ltnS .2b6 size (lhanoi3 ↓[c1] `c[p3]) <= size cs1
by rewrite IHc1.
by apply : leq_ltn_trans Lcs2; rewrite IHc2.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 1eb 204 215 223 232
224 225
(* The largest disk jumped to an intermediate peg *)
have p3Ep : p3 = p by apply /eqP; rewrite opeg3E // lc1Dp.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 1eb 204 215 223 232 p3Ep : p3 = p
224 225
have p1Dp : p1 != p by rewrite eq_sym -p3Ep opeg3E // eqxx.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 1eb 204 215 223 232 2d3 p1Dp : p1 != p
224 225
(* cs cannot be optimal *)
apply /leqifP; case : eqP => [/(congr1 size)|_].2d7 size ([seq ↑[i]_p1 | i <- cs1] ++ c2 :: cs2) =
size
([seq ↑[i]_p1 | i <- lhanoi3 ↓[c1] `c[`p[p1, p]]] ++
↑[`c[`p[p1, p]]]_p
:: [seq ↑[i]_p | i <- lhanoi3 `c[`p[p1, p]] ↓[c]]) ->
size (lhanoi3 ↓[c1] `c[`p[p1, p]]) +
(size (lhanoi3 `c[`p[p1, p]] ↓[c])).+1 ==
size [seq ↑[i]_p1 | i <- cs1] + size (c2 :: cs2)
by rewrite !size_cat /= !size_map => ->.
case : path3SP c2Pcs2 => // [c2' cs2' p2' cs2E c2'Pcs2' _|
cs3 cs4 p4 p5 p6 c2' c3
p4Dp5 p4Rp5 lc2'cs3Epp6 cs2E c2'Pcs3 c3Pcs4 _].15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 223 232 2d3 2d8 c2' := ↓[c2] : configuration 3 n
cs2' := [seq ↓[i] | i <- cs2] : seq (configuration 3 n)
p2' := c2 ldisk : peg 3
cs2E : cs2 = [seq ↑[i]_p2' | i <- cs2']
c2'Pcs2' : path (move (lrel (n:=3 ))) c2' cs2'
2e0
(* this is impossible we need another move of the largest disk *)
case /eqP: p2Dp.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 223 2d3 2d8 2e8 2e9 2ea 2eb 2ec
p2 = p
2ed
have := lc1csEp.2ff last c1 cs = c -> p2 = p
2ed
rewrite csE last_cat /= cs2E -[c2]cunliftrK last_map => /(congr1 f).2ff f ↑[last ↓[c2] cs2']_(c2 ldisk) = f c -> p2 = p
2ed
by rewrite /f !cliftr_ldisk.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 223 232 2d3 2d8 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 2fb
2e0 225
(* cs has a duplicate *)
have p4Ep2 : p4 = p2 by rewrite /p4 !cliftr_ldisk.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 223 232 2d3 2d8 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 2fb p4Ep2 : p4 = p2
2e0 225
have p5Ep1: p5 = p1.
apply : (@lrel3ON4 p1 p p2 p5) => //; first by rewrite eq_sym.
by rewrite -p4Ep2.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 223 232 2d3 2d8 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 2fb 311 319
2e0 225
have p6Ep3 : p6 = p3.
by apply /eqP; rewrite /p6 opeg3E // p4Ep2 p5Ep1 p3Ep p2Dp.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 223 232 2d3 2d8 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 2fb 311 319 329
2e0 225
(* exhibit a shortest path *)
pose cs5 := [seq ↑[i]_p1 | i <- cs1] ++ cs4.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 223 232 2d3 2d8 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 2fb 311 319 329 cs5 := [seq ↑[i]_p1 | i <- cs1] ++ cs4 : seq (configuration 3 n.+1 )
2e0 225
have scs5Lscs : size cs5 < size cs.
rewrite /cs5 csE cs2E !size_cat /= !size_cat /= !size_map.331 size cs1 + size cs4 <
size cs1 + (size cs3 + (size cs4).+1 ).+1
337
by rewrite ltn_add2l // !addnS! ltnS -addSn leq_addl.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 223 232 2d3 2d8 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 2fb 311 319 329 332 33a
2e0 225
have c1Mcs5 : path lmove c1 cs5.
rewrite cat_path -{1 }[c1]cunliftrK /= !path_liftr //=.342 path (move (lrel (n:=3 ))) ↓[c1] cs1 &&
path lmove (last c1 [seq ↑[i]_p1 | i <- cs1]) cs4
347
rewrite c1'Pcs1.342 true &&
path lmove (last c1 [seq ↑[i]_p1 | i <- cs1]) cs4
347
rewrite -{1 }[c1]cunliftrK last_map lc1'cs1Epp3 //.342 true && path lmove ↑[`c[p3]]_(c1 ldisk) cs4
347
by rewrite -p6Ep3 -/p1 -p5Ep1.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 223 232 2d3 2d8 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 2fb 311 319 329 332 33a 34a
2e0 225
have lc1cs5E : last c1 cs5 = c.
rewrite last_cat.35a last (last c1 [seq ↑[i]_p1 | i <- cs1]) cs4 = c
35f
rewrite -[c1]cunliftrK last_map lc1'cs1Epp3 //.35a last ↑[`c[p3]]_(c1 ldisk) cs4 = c
35f
rewrite -p6Ep3 -/p1 -p5Ep1 //.35a last ↑[`c[p6]]_p5 cs4 = c
35f
have := lc1csEp.35a last c1 cs = c -> last ↑[`c[p6]]_p5 cs4 = c
35f
by rewrite csE cs2E last_cat /= last_cat.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 223 232 2d3 2d8 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 2fb 311 319 329 332 33a 34a 362
2e0 225
apply : leq_trans (_ : size cs5 < _); last first .376 size cs5 <
size [seq ↑[i]_p1 | i <- cs1] + size (c2 :: cs2)
by rewrite cs2E /= !size_cat /= !size_map ltn_add2l //=
ltnS -addSnnS leq_addl.376 size (lhanoi3 ↓[c1] `c[`p[p1, p]]) +
(size (lhanoi3 `c[`p[p1, p]] ↓[c])).+1 < (size cs5).+1
225
rewrite ltnS.376 size (lhanoi3 ↓[c1] `c[`p[p1, p]]) +
(size (lhanoi3 `c[`p[p1, p]] ↓[c])).+1 <= size cs5
225
have /IHm : size cs5 < m.
rewrite -ltnS.376 (size cs5).+1 < m.+1
38a
by apply : leq_ltn_trans Scs.376 (forall c c0 : configuration 3 n.+1 ,
path lmove c cs5 ->
last c cs5 = c0 ->
size (lhanoi3 c c0) <= size cs5
?= iff (cs5 == lhanoi3 c c0)) ->
size (lhanoi3 ↓[c1] `c[`p[p1, p]]) +
(size (lhanoi3 `c[`p[p1, p]] ↓[c])).+1 <= size cs5
225
move => /(_ c1 c c1Mcs5 lc1cs5E) /=.376 size
(if c1 ldisk == c ldisk
then [seq ↑[i]_(c ldisk) | i <- lhanoi3 ↓[c1] ↓[c]]
else
if lrel (c1 ldisk) (c ldisk)
then
[seq ↑[i]_(c1 ldisk)
| i <- lhanoi3 ↓[c1] `c[`p[c1 ldisk, c ldisk]]] ++
↑[`c[`p[c1 ldisk, c ldisk]]]_(c ldisk)
:: [seq ↑[i]_(c ldisk)
| i <- lhanoi3 `c[`p[c1 ldisk, c ldisk]]
↓[c]]
else
[seq ↑[i]_(c1 ldisk)
| i <- lhanoi3 ↓[c1] `c[c ldisk]] ++
↑[`c[c ldisk]]_(`p[c1 ldisk, c ldisk])
:: [seq ↑[i]_(`p[c1 ldisk, c ldisk])
| i <- lhanoi3 `c[c ldisk] `c[c1 ldisk]] ++
↑[`c[c1 ldisk]]_(c ldisk)
:: [seq ↑[i]_(c ldisk)
| i <- lhanoi3 `c[c1 ldisk] ↓[c]]) <=
size
cs5
?= iff
(cs5 ==
(if
c1
ldisk ==
c
ldisk
then
[
seq ↑[i]_
(c
ldisk)
| i <-
lhanoi3
↓[c1]
↓[c]]
else
if
lrel
(c1
ldisk)
(c
ldisk)
then
[
seq ↑[i]_
(c1
ldisk)
| i <-
lhanoi3
↓[c1]
`c[`p[
c1
ldisk,
c
ldisk]]] ++
↑[`c[`p[
c1
ldisk,
c
ldisk]]]_
(c
ldisk)
:: [
seq ↑[i]_
(c
ldisk)
| i <-
lhanoi3
`c[`p[
c1
ldisk,
c
ldisk]]
↓[c]]
else
[
seq ↑[i]_
(c1
ldisk)
| i <-
lhanoi3
↓[c1]
`c[
c
ldisk]] ++
↑[`c[
c
ldisk]]_
(`p[
c1
ldisk,
c
ldisk])
::
[
seq ↑[i]_
(`p[
c1
ldisk,
c
ldisk])
| i <-
lhanoi3
`c[
c
ldisk]
`c[
c1
ldisk]] ++
↑[`c[
c1
ldisk]]_
(c
ldisk)
:: [
seq ↑[i]_
(c
ldisk)
| i <-
lhanoi3
`c[
c1
ldisk]
↓[c]])) ->
size (lhanoi3 ↓[c1] `c[`p[p1, p]]) +
(size (lhanoi3 `c[`p[p1, p]] ↓[c])).+1 <= size cs5
225
by rewrite /= (negPf lc1Dp) p1Rp -/p1 size_cat /= !size_map => ->.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 1eb 204 215 228
size (lhanoi3 ↓[c1] `c[p]) +
(size (lhanoi3 `c[p] `c[p1]) +
(size (lhanoi3 `c[p1] ↓[c])).+1 ).+1 <= size
[seq ↑[i]_p1
| i <- cs1] +
size
(c2 :: cs2)
?= iff ([seq ↑[i]_p1
| i <- cs1] ++
c2 :: cs2 ==
[seq ↑[i]_p1
| i <-
lhanoi3
↓[c1]
`c[p]] ++
↑[`c[p]]_
(`p[p1, p])
:: [seq ↑[i]_
(`p[p1, p])
| i <-
lhanoi3
`c[p]
`c[p1]] ++
↑[`c[p1]]_p
:: [
seq ↑[i]_p
| i <-
lhanoi3
`c[p1]
↓[c]])
have p2Dp : p2 != p by apply : contra p1NRp => /eqP<-.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 1eb 204 215 228 232
39d
have p3Ep : p3 = p.
by apply /eqP; rewrite opeg3E // lc1Dp.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 1eb 204 215 228 232 2d3
39d
case : path3SP c2Pcs2 => // [c2' cs2' p2' cs2E c2'Pcs2' _|
cs3 cs4 p4 p5 p6 c2' c3
p4Dp5 p4Rp5 lc2'cs3Epp6 cs2E c2'Pcs3 c3Pcs4 _].15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2e8 2e9 2ea 2eb 2ec
39d
(* this is impossible at least two moves to reach p *)
case /eqP: p2Dp.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 2d3 2e8 2e9 2ea 2eb 2ec
300 3b1
move : lc1csEp.15e 15f 63 165 166 167 168 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 2d3 2e8 2e9 2ea 2eb 2ec
304 3b1
rewrite csE cs2E last_cat /= -[c2]cunliftrK last_map !cliftr_ldisk.3bb ↑[last ↓[c2] cs2']_p2 = c -> p2 = p
3b1
by move => /(congr1 f); rewrite /f !cliftr_ldisk.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 2fb
39d
rewrite cs2E /= size_cat !size_map /=.3c3 size (lhanoi3 ↓[c1] `c[p]) +
(size (lhanoi3 `c[p] `c[p1]) +
(size (lhanoi3 `c[p1] ↓[c])).+1 ).+1 <= size cs1 +
(size cs3 +
(size cs4).+1 ).+1
?= iff ([seq ↑[i]_p1
| i <- cs1] ++
c2
:: [seq ↑[i]_p4
| i <- cs3] ++
c3
:: cs4 ==
[seq ↑[i]_p1
| i <-
lhanoi3
↓[c1]
`c[p]] ++
↑[`c[p]]_
(`p[p1, p])
:: [seq ↑[i]_
(`p[p1, p])
| i <-
lhanoi3
`c[p]
`c[p1]] ++
↑[`c[p1]]_p
:: [
seq ↑[i]_p
| i <-
lhanoi3
`c[p1]
↓[c]])
have Scs3 : size cs3 < m.+1 .
by apply : leq_trans Scs2; rewrite ltnS cs2E size_cat /= size_map leq_addr.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 2fb 3cf
3c7
have Scs4 : size cs4 < m.+1 .
by apply : leq_trans Scs2; rewrite ltnS cs2E size_cat /= -addSnnS leq_addl.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 2fb 3cf 3dc
3c7
have p4Ep2 : p4 = p2 by rewrite [LHS]cliftr_ldisk.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 2fb 3cf 3dc 311
3c7
case : (p5 =P p1) => [p5Ep1|/eqP p5Dp1].15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 2fb 3cf 3dc 311 319
3c7
(* cs has a duplicate *)
apply /leqifP; case : eqP => [/(congr1 size)|_].3e8 size
([seq ↑[i]_p1 | i <- cs1] ++
c2 :: [seq ↑[i]_p4 | i <- cs3] ++ c3 :: cs4) =
size
([seq ↑[i]_p1 | i <- lhanoi3 ↓[c1] `c[p]] ++
↑[`c[p]]_(`p[p1, p])
:: [seq ↑[i]_(`p[p1, p])
| i <- lhanoi3 `c[p] `c[p1]] ++
↑[`c[p1]]_p
:: [seq ↑[i]_p | i <- lhanoi3 `c[p1] ↓[c]]) ->
size (lhanoi3 ↓[c1] `c[p]) +
(size (lhanoi3 `c[p] `c[p1]) +
(size (lhanoi3 `c[p1] ↓[c])).+1 ).+1 ==
size cs1 + (size cs3 + (size cs4).+1 ).+1
rewrite !size_cat /= size_cat !size_map size_cat /= !size_map => ->.3e8 size (lhanoi3 ↓[c1] `c[p]) +
(size (lhanoi3 `c[p] `c[p1]) +
(size (lhanoi3 `c[p1] ↓[c])).+1 ).+1 ==
size (lhanoi3 ↓[c1] `c[p]) +
(size (lhanoi3 `c[p] `c[p1]) +
(size (lhanoi3 `c[p1] ↓[c])).+1 ).+1
3f1
by rewrite !(addSn, addnS) addnA.
have p6Ep3 : p6 = p3.
by rewrite /p6 /p3 opeg_sym; congr opeg.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 2fb 3cf 3dc 311 319 329
3f4 3e9
have lc1'cs1Ec3 : cliftr p1 (last c1' cs1) = c3.405 ↑[last c1' cs1]_p1 = c3
by rewrite lc1'cs1Epp3 -p6Ep3 -p5Ep1.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 2fb 3cf 3dc 311 319 329 40d
3f4 3e9
(* exhibit a shortest path *)
pose cs5 := [seq ↑[i]_p1 | i <- cs1] ++ cs4.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 2fb 3cf 3dc 311 319 329 40d 332
3f4 3e9
have scs5Lscs : size cs5 < size cs.
rewrite /cs5 csE cs2E !size_cat /= !size_cat /= !size_map.
by rewrite ltn_add2l // addnS !ltnS -addSn leq_addl.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 2fb 3cf 3dc 311 319 329 40d 332 33a
3f4 3e9
have c1Mcs5 : path lmove c1 cs5.
rewrite cat_path -{1 }[c1]cunliftrK /= !path_liftr //=.
rewrite c1'Pcs1.
rewrite -{1 }[c1]cunliftrK last_map lc1'cs1Epp3 //.
by rewrite -p6Ep3 -/p1 -p5Ep1.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 2fb 3cf 3dc 311 319 329 40d 332 33a 34a
3f4 3e9
have lc1cs5E : last c1 cs5 = c.
rewrite last_cat.
rewrite -[c1]cunliftrK last_map lc1'cs1Epp3 //.
rewrite -p6Ep3 -/p1 -p5Ep1 //.
have := lc1csEp.
by rewrite csE cs2E last_cat /= last_cat.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 2fb 3cf 3dc 311 319 329 40d 332 33a 34a 362
3f4 3e9
apply : leq_trans (_ : size cs5 < _); last first .44b size cs5 < size cs1 + (size cs3 + (size cs4).+1 ).+1
by rewrite !size_cat /= !size_map ltn_add2l //= ltnS -addSnnS leq_addl.44b size (lhanoi3 ↓[c1] `c[p]) +
(size (lhanoi3 `c[p] `c[p1]) +
(size (lhanoi3 `c[p1] ↓[c])).+1 ).+1 < (size cs5).+1
3e9
have /IHm : size cs5 < m.
rewrite -ltnS.
by apply : leq_ltn_trans Scs.44b (forall c c0 : configuration 3 n.+1 ,
path lmove c cs5 ->
last c cs5 = c0 ->
size (lhanoi3 c c0) <= size cs5
?= iff (cs5 == lhanoi3 c c0)) ->
size (lhanoi3 ↓[c1] `c[p]) +
(size (lhanoi3 `c[p] `c[p1]) +
(size (lhanoi3 `c[p1] ↓[c])).+1 ).+1 < (size cs5).+1
3e9
move => /(_ c1 c c1Mcs5 lc1cs5E) /=.44b size
(if c1 ldisk == c ldisk
then [seq ↑[i]_(c ldisk) | i <- lhanoi3 ↓[c1] ↓[c]]
else
if lrel (c1 ldisk) (c ldisk)
then
[seq ↑[i]_(c1 ldisk)
| i <- lhanoi3 ↓[c1] `c[`p[c1 ldisk, c ldisk]]] ++
↑[`c[`p[c1 ldisk, c ldisk]]]_(c ldisk)
:: [seq ↑[i]_(c ldisk)
| i <- lhanoi3 `c[`p[c1 ldisk, c ldisk]]
↓[c]]
else
[seq ↑[i]_(c1 ldisk)
| i <- lhanoi3 ↓[c1] `c[c ldisk]] ++
↑[`c[c ldisk]]_(`p[c1 ldisk, c ldisk])
:: [seq ↑[i]_(`p[c1 ldisk, c ldisk])
| i <- lhanoi3 `c[c ldisk] `c[c1 ldisk]] ++
↑[`c[c1 ldisk]]_(c ldisk)
:: [seq ↑[i]_(c ldisk)
| i <- lhanoi3 `c[c1 ldisk] ↓[c]]) <=
size
cs5
?= iff
(cs5 ==
(if
c1
ldisk ==
c
ldisk
then
[
seq ↑[i]_
(c
ldisk)
| i <-
lhanoi3
↓[c1]
↓[c]]
else
if
lrel
(c1
ldisk)
(c
ldisk)
then
[
seq ↑[i]_
(c1
ldisk)
| i <-
lhanoi3
↓[c1]
`c[`p[
c1
ldisk,
c
ldisk]]] ++
↑[`c[`p[
c1
ldisk,
c
ldisk]]]_
(c
ldisk)
:: [
seq ↑[i]_
(c
ldisk)
| i <-
lhanoi3
`c[`p[
c1
ldisk,
c
ldisk]]
↓[c]]
else
[
seq ↑[i]_
(c1
ldisk)
| i <-
lhanoi3
↓[c1]
`c[
c
ldisk]] ++
↑[`c[
c
ldisk]]_
(`p[
c1
ldisk,
c
ldisk])
::
[
seq ↑[i]_
(`p[
c1
ldisk,
c
ldisk])
| i <-
lhanoi3
`c[
c
ldisk]
`c[
c1
ldisk]] ++
↑[`c[
c1
ldisk]]_
(c
ldisk)
:: [
seq ↑[i]_
(c
ldisk)
| i <-
lhanoi3
`c[
c1
ldisk]
↓[c]])) ->
size (lhanoi3 ↓[c1] `c[p]) +
(size (lhanoi3 `c[p] `c[p1]) +
(size (lhanoi3 `c[p1] ↓[c])).+1 ).+1 < (size cs5).+1
3e9
rewrite /= (negPf lc1Dp) (negPf p1NRp) -/p1 ltnS.44b size
([seq ↑[i]_p1 | i <- lhanoi3 ↓[c1] `c[c ldisk]] ++
↑[`c[c ldisk]]_(`p[p1, c ldisk])
:: [seq ↑[i]_(`p[p1, c ldisk])
| i <- lhanoi3 `c[c ldisk] `c[p1]] ++
↑[`c[p1]]_(c ldisk)
:: [seq ↑[i]_(c ldisk)
| i <- lhanoi3 `c[p1] ↓[c]]) <= size cs5
?= iff (cs5 ==
[
seq ↑[i]_p1
| i <-
lhanoi3
↓[c1]
`c[
c
ldisk]] ++
↑[`c[
c
ldisk]]_
(`p[p1,
c
ldisk])
::
[
seq ↑[i]_
(`p[p1,
c
ldisk])
| i <-
lhanoi3
`c[
c
ldisk]
`c[p1]] ++
↑[`c[p1]]_
(c
ldisk)
:: [
seq ↑[i]_
(c
ldisk)
| i <-
lhanoi3
`c[p1]
↓[c]]) ->
size (lhanoi3 ↓[c1] `c[p]) +
(size (lhanoi3 `c[p] `c[p1]) +
(size (lhanoi3 `c[p1] ↓[c])).+1 ).+1 <= size cs5
3e9
by rewrite !size_cat /= size_cat /= !size_map => ->.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 2fb 3cf 3dc 311 3ec
3c7
have p5Ep : p5 = p.
by apply /eqP; rewrite eq_sym -p3Ep opeg3E // eq_sym p5Dp1 -p4Ep2.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 2fb 3cf 3dc 311 3ec 477
3c7
have p2Ep1p : p2 = opeg p1 p.
by apply /eqP; rewrite eq_sym opeg3E // p1Dp2 eq_sym p2Dp.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 2fb 3cf 3dc 311 3ec 477 483
3c7
have p6Ep1 : p6 = p1.
by apply /eqP; rewrite opeg3E // p4Ep2 eq_sym p1Dp2.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 2fb 3cf 3dc 311 3ec 477 483 48f
3c7
case : path3SP c3Pcs4 => // [c3' cs4' p8 cs4E c3'Pcs4' _|
cs5 cs6 p8 p9 p10 c3' c4
p8Dp9 p8Rp9 lc3'cs5Epp10 cs4E c3'Pcs5 c4Pcs6 _].15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 3cf 3dc 311 3ec 477 483 48f c3' := ↓[c3] : configuration 3 n
cs4' := [seq ↓[i] | i <- cs4] : seq (configuration 3 n)
p8 := c3 ldisk : peg 3
cs4E : cs4 = [seq ↑[i]_p8 | i <- cs4']
c3'Pcs4' : path (move (lrel (n:=3 ))) c3' cs4'
3c7
have Scs4' : size cs4' < m.+1 by rewrite cs4E size_map in Scs4.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 3cf 3dc 311 3ec 477 483 48f 498 499 49a 49b 49c Scs4' : size cs4' < m.+1
3c7 49d
rewrite cs4E size_map.4ae size (lhanoi3 ↓[c1] `c[p]) +
(size (lhanoi3 `c[p] `c[p1]) +
(size (lhanoi3 `c[p1] ↓[c])).+1 ).+1 <= size cs1 +
(size cs3 +
(size cs4').+1 ).+1
?= iff ([seq ↑[i]_p1
| i <- cs1] ++
c2
:: [seq ↑[i]_p4
| i <- cs3] ++
c3
:: [
seq ↑[i]_p8
| i <- cs4'] ==
[seq ↑[i]_p1
| i <-
lhanoi3
↓[c1]
`c[p]] ++
↑[`c[p]]_
(`p[p1, p])
:: [seq ↑[i]_
(`p[p1, p])
| i <-
lhanoi3
`c[p]
`c[p1]] ++
↑[`c[p1]]_p
:: [
seq ↑[i]_p
| i <-
lhanoi3
`c[p1]
↓[c]])
49d
rewrite csE cs2E last_cat /= last_cat /=
-[c3]cunliftrK cs4E last_map in lc1csEp.15e 15f 63 165 166 167 168 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 3cf 3dc 311 3ec 477 483 48f 498 499 49a 49b 49c 4af lc1csEp : ↑[last ↓[c3] cs4']_(c3 ldisk) = c
4b3 49d
have /(congr1 cunliftr) := lc1csEp.4b7 ↓[↑[last ↓[c3] cs4']_(c3 ldisk)] = ↓[c] ->
size (lhanoi3 ↓[c1] `c[p]) +
(size (lhanoi3 `c[p] `c[p1]) +
(size (lhanoi3 `c[p1] ↓[c])).+1 ).+1 <= size cs1 +
(size cs3 +
(size cs4').+1 ).+1
?= iff ([seq ↑[i]_p1
| i <- cs1] ++
c2
:: [seq ↑[i]_p4
| i <- cs3] ++
c3
:: [
seq ↑[i]_p8
| i <- cs4'] ==
[seq ↑[i]_p1
| i <-
lhanoi3
↓[c1]
`c[p]] ++
↑[`c[p]]_
(`p[p1, p])
:: [seq ↑[i]_
(`p[p1, p])
| i <-
lhanoi3
`c[p]
`c[p1]] ++
↑[`c[p1]]_p
:: [
seq ↑[i]_p
| i <-
lhanoi3
`c[p1]
↓[c]])
49d
rewrite cliftrK => lc3'cs4'Ec'.15e 15f 63 165 166 167 168 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 3cf 3dc 311 3ec 477 483 48f 498 499 49a 49b 49c 4af 4b8 lc3'cs4'Ec' : last ↓[c3] cs4' = ↓[c]
4b3 49d
have /IH := c1'Pcs1 => /(_ _ Scs1 lc1'cs1Epp3) IH1.15e 15f 63 165 166 167 168 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 3cf 3dc 311 3ec 477 483 48f 498 499 49a 49b 49c 4af 4b8 4c1 IH1 : size (lhanoi3 c1' `c[p3])
<= size cs1
?= iff (cs1 == lhanoi3 c1' `c[p3])
4b3 49d
rewrite p3Ep in IH1.15e 15f 63 165 166 167 168 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 3cf 3dc 311 3ec 477 483 48f 498 499 49a 49b 49c 4af 4b8 4c1 IH1 : size (lhanoi3 c1' `c[p])
<= size cs1
?= iff (cs1 == lhanoi3 c1' `c[p])
4b3 49d
have /IH := c2'Pcs3 => /(_ _ Scs3 lc2'cs3Epp6) IH2.15e 15f 63 165 166 167 168 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 3cf 3dc 311 3ec 477 483 48f 498 499 49a 49b 49c 4af 4b8 4c1 4cb IH2 : size (lhanoi3 c2' `c[p6])
<= size cs3
?= iff (cs3 == lhanoi3 c2' `c[p6])
4b3 49d
rewrite [c2']cliftrK p3Ep p6Ep1 in IH2.15e 15f 63 165 166 167 168 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 3cf 3dc 311 3ec 477 483 48f 498 499 49a 49b 49c 4af 4b8 4c1 4cb IH2 : size (lhanoi3 `c[p] `c[p1])
<= size cs3
?= iff (cs3 == lhanoi3 `c[p] `c[p1])
4b3 49d
have /IH := c3'Pcs4' => /(_ _ Scs4' lc3'cs4'Ec') IH3.15e 15f 63 165 166 167 168 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 3cf 3dc 311 3ec 477 483 48f 498 499 49a 49b 49c 4af 4b8 4c1 4cb 4d5 IH3 : size (lhanoi3 c3' ↓[c]) <=
size cs4'
?= iff
(cs4' == lhanoi3 c3' ↓[c])
4b3 49d
rewrite [c3']cliftrK p6Ep1 in IH3.15e 15f 63 165 166 167 168 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 3cf 3dc 311 3ec 477 483 48f 498 499 49a 49b 49c 4af 4b8 4c1 4cb 4d5 IH3 : size (lhanoi3 `c[p1] ↓[c])
<= size cs4'
?= iff (cs4' == lhanoi3 `c[p1] ↓[c])
4b3 49d
move /leqifP : IH1.15e 15f 63 165 166 167 168 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 3cf 3dc 311 3ec 477 483 48f 498 499 49a 49b 49c 4af 4b8 4c1 4d5 4df
(if cs1 == lhanoi3 c1' `c[p]
then size (lhanoi3 c1' `c[p]) == size cs1
else size (lhanoi3 c1' `c[p]) < size cs1) ->
size (lhanoi3 ↓[c1] `c[p]) +
(size (lhanoi3 `c[p] `c[p1]) +
(size (lhanoi3 `c[p1] ↓[c])).+1 ).+1 <= size cs1 +
(size cs3 +
(size cs4').+1 ).+1
?= iff ([seq ↑[i]_p1
| i <- cs1] ++
c2
:: [seq ↑[i]_p4
| i <- cs3] ++
c3
:: [
seq ↑[i]_p8
| i <- cs4'] ==
[seq ↑[i]_p1
| i <-
lhanoi3
↓[c1]
`c[p]] ++
↑[`c[p]]_
(`p[p1, p])
:: [seq ↑[i]_
(`p[p1, p])
| i <-
lhanoi3
`c[p]
`c[p1]] ++
↑[`c[p1]]_p
:: [
seq ↑[i]_p
| i <-
lhanoi3
`c[p1]
↓[c]])
49d
case : eqP => [E1 _ | /eqP cs1D Lcs1].15e 15f 63 165 166 167 168 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 3cf 3dc 311 3ec 477 483 48f 498 499 49a 49b 49c 4af 4b8 4c1 4d5 4df E1 : cs1 = lhanoi3 c1' `c[p]
4b3
(* the first part cs1 is perfect *)
have /leqifP := IH2; case : eqP => [E2 _ |_ Lc1].15e 15f 63 165 166 167 168 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 3cf 3dc 311 3ec 477 483 48f 498 499 49a 49b 49c 4af 4b8 4c1 4d5 4df 4e9 E2 : cs3 = lhanoi3 `c[p] `c[p1]
4b3
(* the second part cs3 is perfect *)
have /leqifP := IH3; case : eqP => [E3 _ |_ Lc2].15e 15f 63 165 166 167 168 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 3cf 3dc 311 3ec 477 483 48f 498 499 49a 49b 49c 4af 4b8 4c1 4d5 4df 4e9 4f4 E3 : cs4' = lhanoi3 `c[p1] ↓[c]
4b3
(* the third part cs4 is perfect, only case of equality *)
apply /leqifP; case : eqP => [/(congr1 size)|[]].4fc size
([seq ↑[i]_p1 | i <- cs1] ++
c2
:: [seq ↑[i]_p4 | i <- cs3] ++
c3 :: [seq ↑[i]_p8 | i <- cs4']) =
size
([seq ↑[i]_p1 | i <- lhanoi3 ↓[c1] `c[p]] ++
↑[`c[p]]_(`p[p1, p])
:: [seq ↑[i]_(`p[p1, p])
| i <- lhanoi3 `c[p] `c[p1]] ++
↑[`c[p1]]_p
:: [seq ↑[i]_p | i <- lhanoi3 `c[p1] ↓[c]]) ->
size (lhanoi3 ↓[c1] `c[p]) +
(size (lhanoi3 `c[p] `c[p1]) +
(size (lhanoi3 `c[p1] ↓[c])).+1 ).+1 ==
size cs1 + (size cs3 + (size cs4').+1 ).+1
rewrite !size_cat /= size_cat /= size_cat /= !size_map => ->.
by rewrite !(addSn, addnS) addnA.
congr (_ ++ _ :: _ ++ _ :: _).4fc [seq ↑[i]_p1 | i <- cs1] =
[seq ↑[i]_p1 | i <- lhanoi3 ↓[c1] `c[p]]
- 511
by rewrite E1.
- 51f
by rewrite /c2 p3Ep p2Ep1p.
- 524
by rewrite p4Ep2 -p2Ep1p E2.
- 529
by rewrite /c3 p6Ep1 p5Ep.
- 52e
congr (map (cliftr _) _).
by rewrite /p8 !cliftr_ldisk.
by [].15e 15f 63 165 166 167 168 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 3cf 3dc 311 3ec 477 483 48f 498 499 49a 49b 49c 4af 4b8 4c1 4d5 4df 4e9 4f4 501
4b3 4f5
apply /leqifP; case : eqP => [/(congr1 size)|_].
rewrite !size_cat /= !size_cat /= !size_map => ->.
by rewrite !(addSn, addnS) addnA.
by rewrite E1 E2 !(addSn, addnS) !ltnS !ltn_add2l.15e 15f 63 165 166 167 168 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 3cf 3dc 311 3ec 477 483 48f 498 499 49a 49b 49c 4af 4b8 4c1 4d5 4df 4e9 4f8
4b3 4ea
apply /leqifP; case : eqP => [/(congr1 size)|_].
rewrite !size_cat /= !size_cat /= !size_map => ->.
by rewrite !(addSn, addnS) addnA.
rewrite E1 !(addSn, addnS) !ltnS !ltn_add2l.54e size (lhanoi3 `c[p] `c[p1]) +
size (lhanoi3 `c[p1] ↓[c]) < size cs3 + size cs4'
4ea
apply : leq_ltn_trans (_ : _ <= size (lhanoi3 `c[p, n] `c[p1])
+ size cs4') _.54e size (lhanoi3 `c[p] `c[p1]) +
size (lhanoi3 `c[p1] ↓[c]) <=
size (lhanoi3 `c[p] `c[p1]) + size cs4'
by rewrite leq_add2l IH3.
by rewrite ltn_add2r.15e 15f 63 165 166 167 168 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 3cf 3dc 311 3ec 477 483 48f 498 499 49a 49b 49c 4af 4b8 4c1 4d5 4df 4ed 4ee
4b3 49d
apply /leqifP; case : eqP => [/(congr1 size)|_].
rewrite !size_cat /= !size_cat /= !size_map => ->.
by rewrite !(addSn, addnS).
by rewrite !(addSn, addnS) !ltnS -addSn !leq_add ?IH2 ?IH3 .15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 3cf 3dc 311 3ec 477 483 48f 4a0 4a1 49a 4a2 4a3 498 4a4 4a5 4a6 4a7 4a8 4a9 4aa
3c7
(* three moves in a row -> duplicate *)
have p8Ep : p8 = p by rewrite [LHS]cliftr_ldisk.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 3cf 3dc 311 3ec 477 483 48f 4a0 4a1 49a 4a2 4a3 498 4a4 4a5 4a6 4a7 4a8 4a9 4aa p8Ep : p8 = p
3c7
have p9Ep2 : p9 = p2.
apply : lrel3ON4 p8Rp9.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 3cf 3dc 311 3ec 477 483 48f 4a0 4a1 49a 4a2 4a3 498 4a4 4a5 4a7 4a8 4a9 4aa 57f
p2 != ?Goal0
- 589
by rewrite eq_sym; exact : p1Dp2.
- 599
by rewrite p8Ep.
- 5a2
by rewrite p8Ep.
- 5a7
by rewrite lsym.
by rewrite p8Ep -p4Ep2 -p5Ep.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 3cf 3dc 311 3ec 477 483 48f 4a0 4a1 49a 4a2 4a3 498 4a4 4a5 4a6 4a7 4a8 4a9 4aa 57f 587
3c7
have p10Ep1 : p10 = p1.
by apply /eqP; rewrite opeg3E // p8Ep eq_sym lc1Dp p9Ep2 eq_sym.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 3cf 3dc 311 3ec 477 483 48f 4a0 4a1 49a 4a2 4a3 498 4a4 4a5 4a6 4a7 4a8 4a9 4aa 57f 587 5b9
3c7
have cc : cliftr p2 (last c2' cs3) = c4.5bd ↑[last c2' cs3]_p2 = c4
by rewrite /c4 lc2'cs3Epp6 p6Ep1 p10Ep1 p9Ep2.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 3cf 3dc 311 3ec 477 483 48f 4a0 4a1 49a 4a2 4a3 498 4a4 4a5 4a6 4a7 4a8 4a9 4aa 57f 587 5b9 5c5
3c7
apply /leqifP; case : eqP => [/(congr1 size)|_].
rewrite !size_cat /= size_cat !size_map size_cat /= !size_map => ->.
by rewrite !(addSn, addnS).
(* exhibit a shortest path *)
pose cs7 := [seq ↑[i]_p1 | i <- cs1] ++ c2 :: [seq ↑[i]_p4 | i <- cs3] ++ cs6.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 3cf 3dc 311 3ec 477 483 48f 4a0 4a1 49a 4a2 4a3 498 4a4 4a5 4a6 4a7 4a8 4a9 4aa 57f 587 5b9 5c5 cs7 := [seq ↑[i]_p1 | i <- cs1] ++
c2 :: [seq ↑[i]_p4 | i <- cs3] ++ cs6 : seq (configuration 3 n.+1 )
3f4
have scs7Lscs7: size cs7 < size cs.
rewrite /cs7 csE cs2E cs4E.5d8 size
([seq ↑[i]_p1 | i <- cs1] ++
c2 :: [seq ↑[i]_p4 | i <- cs3] ++ cs6) <
size
([seq ↑[i]_p1 | i <- cs1] ++
c2
:: [seq ↑[i]_p4 | i <- cs3] ++
c3 :: [seq ↑[i]_p8 | i <- cs5] ++ c4 :: cs6)
5de
rewrite size_cat /= size_cat /= size_cat /= size_cat /= size_cat /= !size_map.5d8 size cs1 + (size cs3 + size cs6).+1 <
size cs1 +
(size cs3 + (size cs5 + (size cs6).+1 ).+1 ).+1
5de
by rewrite !addnS ltnS -!addnS !leq_add2l addnS ltnS -addSnnS leq_addl.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 3cf 3dc 311 3ec 477 483 48f 4a0 4a1 49a 4a2 4a3 498 4a4 4a5 4a6 4a7 4a8 4a9 4aa 57f 587 5b9 5c5 5d9 5e1
3f4
have c1Mcs7 : path lmove c1 cs7.
rewrite cat_path -{1 }[c1]cunliftrK /= !path_liftr //=.5ed [&& path (move (lrel (n:=3 ))) ↓[c1] cs1,
last c1 [seq ↑[i]_p1 | i <- cs1] `-->_r c2
& path lmove c2 ([seq ↑[i]_p4 | i <- cs3] ++ cs6)]
5f2
rewrite c1'Pcs1.5ed [&& true, last c1 [seq ↑[i]_p1 | i <- cs1] `-->_r c2
& path lmove c2 ([seq ↑[i]_p4 | i <- cs3] ++ cs6)]
5f2
rewrite -{1 }[c1]cunliftrK last_map lc1'cs1Epp3 //.5ed [&& true, ↑[`c[p3]]_(c1 ldisk) `-->_r c2
& path lmove c2 ([seq ↑[i]_p4 | i <- cs3] ++ cs6)]
5f2
rewrite p4Ep2 cat_path /c2 -/p1 /=.5ed [&& ↑[`c[p3]]_p1 `-->_r ↑[`c[p3]]_p2,
path lmove ↑[`c[p3]]_p2 [seq ↑[i]_p2 | i <- cs3]
& path lmove
(last ↑[`c[p3]]_p2 [seq ↑[i]_p2 | i <- cs3]) cs6]
5f2
apply /and3P; split => //.5ed ↑[`c[p3]]_p1 `-->_r ↑[`c[p3]]_p2
- 607
apply : move_liftr_perfect => //.
by rewrite eq_sym opegDl.
by rewrite eq_sym opegDr.
by rewrite path_liftr //; rewrite [c2']cliftrK in c2'Pcs3.
by rewrite last_map; rewrite [c2']cliftrK in cc; rewrite cc.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 3cf 3dc 311 3ec 477 483 48f 4a0 4a1 49a 4a2 4a3 498 4a4 4a5 4a6 4a7 4a8 4a9 4aa 57f 587 5b9 5c5 5d9 5e1 5f5
3f4
have lc1cs7E : last c1 cs7 = c.
rewrite last_cat /= last_cat p4Ep2.624 last (last c2 [seq ↑[i]_p2 | i <- cs3]) cs6 = c
629
rewrite -[c2]cunliftrK !cliftr_ldisk.624 last (last ↑[↓[c2]]_p2 [seq ↑[i]_p2 | i <- cs3]) cs6 =
c
629
rewrite last_map lc2'cs3Epp6.624 last ↑[`c[p6]]_p2 cs6 = c
629
have := lc1csEp.624 last c1 cs = c -> last ↑[`c[p6]]_p2 cs6 = c
629
rewrite csE cs2E cs4E last_cat /= last_cat /= last_cat /=.624 last c4 cs6 = c -> last ↑[`c[p6]]_p2 cs6 = c
629
by rewrite /c4 p10Ep1 p6Ep1 p9Ep2.15e 15f 63 165 166 167 168 16a 170 181 1cb 1d0 1d5 187 1e3 1dc 1e4 1e5 1da 1e6 c 1e7 1e8 1e9 1ea 204 215 228 232 2d3 2f0 2f1 2f2 2f3 2f4 2e8 2f5 2f6 2f7 2f8 2f9 2fa 3cf 3dc 311 3ec 477 483 48f 4a0 4a1 49a 4a2 4a3 498 4a4 4a5 4a6 4a7 4a8 4a9 4aa 57f 587 5b9 5c5 5d9 5e1 5f5 62c
3f4
apply : leq_trans (_ : size cs7 < _); last first .644 size cs7 < size cs1 + (size cs3 + (size cs4).+1 ).+1
rewrite !size_cat /= size_cat /= !size_map ltn_add2l //=.644 (size cs3 + size cs6).+1 <
(size cs3 + (size cs4).+1 ).+1
649
rewrite cs4E size_cat /= size_map !addnS !ltnS -addnS -addSn.644 size cs3 + size cs6 <=
size cs3 + ((size cs5).+1 + size cs6)
649
by rewrite leq_add2l leq_addl.644 size (lhanoi3 ↓[c1] `c[p]) +
(size (lhanoi3 `c[p] `c[p1]) +
(size (lhanoi3 `c[p1] ↓[c])).+1 ).+1 < (size cs7).+1
have /IHm : size cs7 < m.
rewrite -ltnS.644 (size cs7).+1 < m.+1
65c
by apply : leq_ltn_trans Scs.644 (forall c c0 : configuration 3 n.+1 ,
path lmove c cs7 ->
last c cs7 = c0 ->
size (lhanoi3 c c0) <= size cs7
?= iff (cs7 == lhanoi3 c c0)) ->
size (lhanoi3 ↓[c1] `c[p]) +
(size (lhanoi3 `c[p] `c[p1]) +
(size (lhanoi3 `c[p1] ↓[c])).+1 ).+1 < (size cs7).+1
move => /(_ c1 c c1Mcs7 lc1cs7E) /=.644 size
(if c1 ldisk == c ldisk
then [seq ↑[i]_(c ldisk) | i <- lhanoi3 ↓[c1] ↓[c]]
else
if lrel (c1 ldisk) (c ldisk)
then
[seq ↑[i]_(c1 ldisk)
| i <- lhanoi3 ↓[c1] `c[`p[c1 ldisk, c ldisk]]] ++
↑[`c[`p[c1 ldisk, c ldisk]]]_(c ldisk)
:: [seq ↑[i]_(c ldisk)
| i <- lhanoi3 `c[`p[c1 ldisk, c ldisk]]
↓[c]]
else
[seq ↑[i]_(c1 ldisk)
| i <- lhanoi3 ↓[c1] `c[c ldisk]] ++
↑[`c[c ldisk]]_(`p[c1 ldisk, c ldisk])
:: [seq ↑[i]_(`p[c1 ldisk, c ldisk])
| i <- lhanoi3 `c[c ldisk] `c[c1 ldisk]] ++
↑[`c[c1 ldisk]]_(c ldisk)
:: [seq ↑[i]_(c ldisk)
| i <- lhanoi3 `c[c1 ldisk] ↓[c]]) <=
size
cs7
?= iff
(cs7 ==
(if
c1
ldisk ==
c
ldisk
then
[
seq ↑[i]_
(c
ldisk)
| i <-
lhanoi3
↓[c1]
↓[c]]
else
if
lrel
(c1
ldisk)
(c
ldisk)
then
[
seq ↑[i]_
(c1
ldisk)
| i <-
lhanoi3
↓[c1]
`c[`p[
c1
ldisk,
c
ldisk]]] ++
↑[`c[`p[
c1
ldisk,
c
ldisk]]]_
(c
ldisk)
:: [
seq ↑[i]_
(c
ldisk)
| i <-
lhanoi3
`c[`p[
c1
ldisk,
c
ldisk]]
↓[c]]
else
[
seq ↑[i]_
(c1
ldisk)
| i <-
lhanoi3
↓[c1]
`c[
c
ldisk]] ++
↑[`c[
c
ldisk]]_
(`p[
c1
ldisk,
c
ldisk])
::
[
seq ↑[i]_
(`p[
c1
ldisk,
c
ldisk])
| i <-
lhanoi3
`c[
c
ldisk]
`c[
c1
ldisk]] ++
↑[`c[
c1
ldisk]]_
(c
ldisk)
:: [
seq ↑[i]_
(c
ldisk)
| i <-
lhanoi3
`c[
c1
ldisk]
↓[c]])) ->
size (lhanoi3 ↓[c1] `c[p]) +
(size (lhanoi3 `c[p] `c[p1]) +
(size (lhanoi3 `c[p1] ↓[c])).+1 ).+1 < (size cs7).+1
rewrite /= (negPf lc1Dp) (negPf p1NRp) -/p1 ltnS.644 size
([seq ↑[i]_p1 | i <- lhanoi3 ↓[c1] `c[c ldisk]] ++
↑[`c[c ldisk]]_(`p[p1, c ldisk])
:: [seq ↑[i]_(`p[p1, c ldisk])
| i <- lhanoi3 `c[c ldisk] `c[p1]] ++
↑[`c[p1]]_(c ldisk)
:: [seq ↑[i]_(c ldisk)
| i <- lhanoi3 `c[p1] ↓[c]]) <= size cs7
?= iff (cs7 ==
[
seq ↑[i]_p1
| i <-
lhanoi3
↓[c1]
`c[
c
ldisk]] ++
↑[`c[
c
ldisk]]_
(`p[p1,
c
ldisk])
::
[
seq ↑[i]_
(`p[p1,
c
ldisk])
| i <-
lhanoi3
`c[
c
ldisk]
`c[p1]] ++
↑[`c[p1]]_
(c
ldisk)
:: [
seq ↑[i]_
(c
ldisk)
| i <-
lhanoi3
`c[p1]
↓[c]]) ->
size (lhanoi3 ↓[c1] `c[p]) +
(size (lhanoi3 `c[p] `c[p1]) +
(size (lhanoi3 `c[p1] ↓[c])).+1 ).+1 <= size cs7
by rewrite size_cat /= size_cat /= !size_map => ->.
Qed .
(* size on a perfect configuration depends which peg we consider *)
Lemma size_app_lhanoi3_p n p1 p2 :
size (lhanoi3 `c[p1, n] `c[p2]) =
if lrel p1 p2 then (3 ^ n).-1 ./2 else (3 ^ n).-1 * (p1 != p2).63 5
size (lhanoi3 `c[p1 , n] `c[p2]) =
(if lrel p1 p2
then ((3 ^ n).-1 )./2
else (3 ^ n).-1 * (p1 != p2))
Proof .670
elim : n p1 p2 => [p1 p2|n IH p1 p2] /=; first by rewrite if_same.63 IH : forall p1 p2 : peg 3 ,
size (lhanoi3 `c[p1] `c[p2]) =
(if lrel p1 p2
then ((3 ^ n).-1 )./2
else (3 ^ n).-1 * (p1 != p2))
5 size
(if `c[p1] ldisk == `c[p2] ldisk
then
[seq ↑[i]_(`c[p2] ldisk)
| i <- lhanoi3 ↓[`c[p1]] ↓[`c[p2]]]
else
if lrel (`c[p1] ldisk) (`c[p2] ldisk)
then
[seq ↑[i]_(`c[p1] ldisk)
| i <- lhanoi3 ↓[`c[p1]]
`c[`p[`c[p1] ldisk, `c[p2] ldisk]]] ++
↑[`c[`p[`c[p1] ldisk, `c[p2] ldisk]]]_(`c[p2]
ldisk)
:: [seq ↑[i]_(`c[p2] ldisk)
| i <- lhanoi3
`c[`p[`c[p1] ldisk, `c[p2] ldisk]]
↓[`c[p2]]]
else
[seq ↑[i]_(`c[p1] ldisk)
| i <- lhanoi3 ↓[`c[p1]] `c[`c[p2] ldisk]] ++
↑[`c[`c[p2] ldisk]]_(`p[`c[p1] ldisk, `c[p2]
ldisk])
:: [seq ↑[i]_(`p[`c[p1] ldisk, `c[p2] ldisk])
| i <- lhanoi3 `c[`c[p2] ldisk]
`c[`c[p1] ldisk]] ++
↑[`c[`c[p1] ldisk]]_(`c[p2] ldisk)
:: [seq ↑[i]_(`c[p2] ldisk)
| i <- lhanoi3 `c[`c[p1] ldisk]
↓[`c[p2]]]) =
(if lrel p1 p2
then ((3 ^ n.+1 ).-1 )./2
else (3 ^ n.+1 ).-1 * (p1 != p2))
rewrite !ffunE; case : eqP => [p1Ep2|/eqP p1Dp2].size [seq ↑[i]_p2 | i <- lhanoi3 ↓[`c[p1]] ↓[`c[p2]]] =
(if lrel p1 p2
then ((3 ^ n.+1 ).-1 )./2
else (3 ^ n.+1 ).-1 * ~~ true)
by rewrite !perfect_unliftr size_map IH p1Ep2 eqxx lirr !muln0.
rewrite !perfect_unliftr !fun_if !size_cat /= !size_cat /= !size_map.683 if lrel p1 p2
then
(if lrel p1 p2
then
eq
(size (lhanoi3 `c[p1] `c[`p[p1, p2]]) +
(size (lhanoi3 `c[`p[p1, p2]] `c[p2])).+1 )
else
eq
(size (lhanoi3 `c[p1] `c[p2]) +
(size (lhanoi3 `c[p2] `c[p1]) +
(size (lhanoi3 `c[p1] `c[p2])).+1 ).+1 ))
((3 ^ n.+1 ).-1 )./2
else
(if lrel p1 p2
then
eq
(size (lhanoi3 `c[p1] `c[`p[p1, p2]]) +
(size (lhanoi3 `c[`p[p1, p2]] `c[p2])).+1 )
else
eq
(size (lhanoi3 `c[p1] `c[p2]) +
(size (lhanoi3 `c[p2] `c[p1]) +
(size (lhanoi3 `c[p1] `c[p2])).+1 ).+1 ))
((3 ^ n.+1 ).-1 * 1 )
rewrite !IH eq_sym opegDl // opegDr //= !muln1.683 if lrel p1 p2
then
(if lrel p1 p2
then
eq
((if lrel p1 `p[p1, p2]
then ((3 ^ n).-1 )./2
else (3 ^ n).-1 ) +
(if lrel `p[p1, p2] p2
then ((3 ^ n).-1 )./2
else (3 ^ n).-1 ).+1 )
else
eq
((if lrel p1 p2
then ((3 ^ n).-1 )./2
else (3 ^ n).-1 * (p1 != p2)) +
((if lrel p2 p1
then ((3 ^ n).-1 )./2
else (3 ^ n).-1 * (p2 != p1)) +
(if lrel p1 p2
then ((3 ^ n).-1 )./2
else (3 ^ n).-1 * (p1 != p2)).+1 ).+1 ))
((3 ^ n.+1 ).-1 )./2
else
(if lrel p1 p2
then
eq
((if lrel p1 `p[p1, p2]
then ((3 ^ n).-1 )./2
else (3 ^ n).-1 ) +
(if lrel `p[p1, p2] p2
then ((3 ^ n).-1 )./2
else (3 ^ n).-1 ).+1 )
else
eq
((if lrel p1 p2
then ((3 ^ n).-1 )./2
else (3 ^ n).-1 * (p1 != p2)) +
((if lrel p2 p1
then ((3 ^ n).-1 )./2
else (3 ^ n).-1 * (p2 != p1)) +
(if lrel p1 p2
then ((3 ^ n).-1 )./2
else (3 ^ n).-1 * (p1 != p2)).+1 ).+1 ))
(3 ^ n.+1 ).-1
have Hd : (3 ^ n.+1 ).-1 = (3 ^ n).-1 + (3 ^ n).*2 .683 (3 ^ n.+1 ).-1 = (3 ^ n).-1 + (3 ^ n).*2
rewrite expnS -[3 ^n]prednK ?expn_gt0 //.683 (3 * (3 ^ n).-1 .+1 ).-1 =
(3 ^ n).-1 .+1 .-1 + ((3 ^ n).-1 .+1 ).*2
694
by rewrite mulnS /= doubleS !addnS mulSn mul2n.
rewrite ![lrel p2 _]lsym.696 if lrel p1 p2
then
(if lrel p1 p2
then
eq
((if lrel p1 `p[p1, p2]
then ((3 ^ n).-1 )./2
else (3 ^ n).-1 ) +
(if lrel `p[p1, p2] p2
then ((3 ^ n).-1 )./2
else (3 ^ n).-1 ).+1 )
else
eq
((if lrel p1 p2
then ((3 ^ n).-1 )./2
else (3 ^ n).-1 * (p1 != p2)) +
((if lrel p1 p2
then ((3 ^ n).-1 )./2
else (3 ^ n).-1 * (p2 != p1)) +
(if lrel p1 p2
then ((3 ^ n).-1 )./2
else (3 ^ n).-1 * (p1 != p2)).+1 ).+1 ))
((3 ^ n.+1 ).-1 )./2
else
(if lrel p1 p2
then
eq
((if lrel p1 `p[p1, p2]
then ((3 ^ n).-1 )./2
else (3 ^ n).-1 ) +
(if lrel `p[p1, p2] p2
then ((3 ^ n).-1 )./2
else (3 ^ n).-1 ).+1 )
else
eq
((if lrel p1 p2
then ((3 ^ n).-1 )./2
else (3 ^ n).-1 * (p1 != p2)) +
((if lrel p1 p2
then ((3 ^ n).-1 )./2
else (3 ^ n).-1 * (p2 != p1)) +
(if lrel p1 p2
then ((3 ^ n).-1 )./2
else (3 ^ n).-1 * (p1 != p2)).+1 ).+1 ))
(3 ^ n.+1 ).-1
case : (boolP (lrel _ _)) => [Hrel1|Hrel1]; last first .63 679 5 c 697 Hrel1 : ~~ lrel p1 p2
(3 ^ n).-1 * (p1 != p2) +
((3 ^ n).-1 * (p2 != p1) +
((3 ^ n).-1 * (p1 != p2)).+1 ).+1 = (3 ^ n.+1 ).-1
rewrite [p2 == _]eq_sym p1Dp2 !muln1.6a6 (3 ^ n).-1 + ((3 ^ n).-1 + (3 ^ n).-1 .+1 ).+1 =
(3 ^ n.+1 ).-1
6a9
rewrite expnS !mulSn addn0.6a6 (3 ^ n).-1 + ((3 ^ n).-1 + (3 ^ n).-1 .+1 ).+1 =
(3 ^ n + (3 ^ n + 3 ^ n)).-1
6a9
by case : expn (expn_gt0 3 n) => // k _; rewrite !addnS addnA.
case : (boolP (lrel _ _)) => [Hrel2|Hrel2].63 679 5 c 697 6ac Hrel2 : lrel p1 `p[p1, p2]
((3 ^ n).-1 )./2 +
(if lrel `p[p1, p2] p2
then ((3 ^ n).-1 )./2
else (3 ^ n).-1 ).+1 = ((3 ^ n.+1 ).-1 )./2
rewrite !ifN.6bc ((3 ^ n).-1 )./2 + (3 ^ n).-1 .+1 = ((3 ^ n.+1 ).-1 )./2
by rewrite Hd halfD /= odd_double andbF add0n doubleK prednK ?expn_gt0 .
by have := lrel3B p1Dp2; rewrite Hrel1 Hrel2 lsym.
rewrite ifT; last by rewrite lsym; apply : lrel3ON.6c1 (3 ^ n).-1 + ((3 ^ n).-1 )./2 .+1 = ((3 ^ n.+1 ).-1 )./2
rewrite Hd halfD /= odd_double andbF add0n doubleK -addSnnS addnC.6c1 ((3 ^ n).-1 )./2 + (3 ^ n).-1 .+1 =
((3 ^ n).-1 )./2 + 3 ^ n
by rewrite prednK // expn_gt0.
Qed .
Fixpoint size_lhanoi3 {n : nat} : configuration 3 n -> configuration 3 n -> _ :=
match n with
| 0 => fun _ _ => 0
| n1.+1 =>
fun c1 c2 =>
let p1 := c1 ldisk in
let p2 := c2 ldisk in
if p1 == p2 then size_lhanoi3 ↓[c1] ↓[c2] else
let p3 := `p[p1, p2] in
if lrel p1 p2 then
(size_lhanoi3 ↓[c1] `c[p3] + size_lhanoi3 `c[p3] ↓[c2]).+1
else
(size_lhanoi3 ↓[c1] `c[p2] +
(3 ^ n1).-1 +
size_lhanoi3 `c[p1] ↓[c2]).+2
end .
Lemma size_lhanoi3E n (c1 c2 : _ _ n) :
size_lhanoi3 c1 c2 = size (lhanoi3 c1 c2).62 size_lhanoi3 c1 c2 = size (lhanoi3 c1 c2)
Proof .6da
elim : n c1 c2 => //= n IH c1 c2.63 IH : forall c1 c2 : configuration 3 n,
size_lhanoi3 c1 c2 = size (lhanoi3 c1 c2)
6c (if c1 ldisk == c2 ldisk
then size_lhanoi3 ↓[c1] ↓[c2]
else
if lrel (c1 ldisk) (c2 ldisk)
then
(size_lhanoi3 ↓[c1] `c[`p[c1 ldisk, c2 ldisk]] +
size_lhanoi3 `c[`p[c1 ldisk, c2 ldisk]] ↓[c2]).+1
else
(size_lhanoi3 ↓[c1] `c[c2 ldisk] + (3 ^ n).-1 +
size_lhanoi3 `c[c1 ldisk] ↓[c2]).+2 ) =
size
(if c1 ldisk == c2 ldisk
then
[seq ↑[i]_(c2 ldisk) | i <- lhanoi3 ↓[c1] ↓[c2]]
else
if lrel (c1 ldisk) (c2 ldisk)
then
[seq ↑[i]_(c1 ldisk)
| i <- lhanoi3 ↓[c1]
`c[`p[c1 ldisk, c2 ldisk]]] ++
↑[`c[`p[c1 ldisk, c2 ldisk]]]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk)
| i <- lhanoi3 `c[`p[c1 ldisk, c2 ldisk]]
↓[c2]]
else
[seq ↑[i]_(c1 ldisk)
| i <- lhanoi3 ↓[c1] `c[c2 ldisk]] ++
↑[`c[c2 ldisk]]_(`p[c1 ldisk, c2 ldisk])
:: [seq ↑[i]_(`p[c1 ldisk, c2 ldisk])
| i <- lhanoi3 `c[c2 ldisk] `c[c1 ldisk]] ++
↑[`c[c1 ldisk]]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk)
| i <- lhanoi3 `c[c1 ldisk] ↓[c2]])
case : eqP => [lc1Elc2|/eqP lc1Dlc2].63 6e2 6c lc1Elc2 : c1 ldisk = c2 ldisk
size_lhanoi3 ↓[c1] ↓[c2] =
size [seq ↑[i]_(c2 ldisk) | i <- lhanoi3 ↓[c1] ↓[c2]]
by rewrite size_map IH.6ec (if lrel (c1 ldisk) (c2 ldisk)
then
(size_lhanoi3 ↓[c1] `c[`p[c1 ldisk, c2 ldisk]] +
size_lhanoi3 `c[`p[c1 ldisk, c2 ldisk]] ↓[c2]).+1
else
(size_lhanoi3 ↓[c1] `c[c2 ldisk] + (3 ^ n).-1 +
size_lhanoi3 `c[c1 ldisk] ↓[c2]).+2 ) =
size
(if lrel (c1 ldisk) (c2 ldisk)
then
[seq ↑[i]_(c1 ldisk)
| i <- lhanoi3 ↓[c1] `c[`p[c1 ldisk, c2 ldisk]]] ++
↑[`c[`p[c1 ldisk, c2 ldisk]]]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk)
| i <- lhanoi3 `c[`p[c1 ldisk, c2 ldisk]]
↓[c2]]
else
[seq ↑[i]_(c1 ldisk)
| i <- lhanoi3 ↓[c1] `c[c2 ldisk]] ++
↑[`c[c2 ldisk]]_(`p[c1 ldisk, c2 ldisk])
:: [seq ↑[i]_(`p[c1 ldisk, c2 ldisk])
| i <- lhanoi3 `c[c2 ldisk] `c[c1 ldisk]] ++
↑[`c[c1 ldisk]]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk)
| i <- lhanoi3 `c[c1 ldisk] ↓[c2]])
case : (boolP (lrel _ _)) => [lc1Rlc2|lc1NRlc2].63 6e2 6c 6ed lc1Rlc2 : lrel (c1 ldisk) (c2 ldisk)
(size_lhanoi3 ↓[c1] `c[`p[c1 ldisk, c2 ldisk]] +
size_lhanoi3 `c[`p[c1 ldisk, c2 ldisk]] ↓[c2]).+1 =
size
([seq ↑[i]_(c1 ldisk)
| i <- lhanoi3 ↓[c1] `c[`p[c1 ldisk, c2 ldisk]]] ++
↑[`c[`p[c1 ldisk, c2 ldisk]]]_(c2 ldisk)
:: [seq ↑[i]_(c2 ldisk)
| i <- lhanoi3 `c[`p[c1 ldisk, c2 ldisk]]
↓[c2]])
by rewrite size_cat /= !size_map !IH addnS.
rewrite size_cat /= size_cat /= !size_map size_app_lhanoi3_p
lsym (negPf lc1NRlc2).6fb (size_lhanoi3 ↓[c1] `c[c2 ldisk] + (3 ^ n).-1 +
size_lhanoi3 `c[c1 ldisk] ↓[c2]).+2 =
size (lhanoi3 ↓[c1] `c[c2 ldisk]) +
((3 ^ n).-1 * (c2 ldisk != c1 ldisk) +
(size (lhanoi3 `c[c1 ldisk] ↓[c2])).+1 ).+1
by rewrite eq_sym (negPf lc1Dlc2) muln1 !addnS addnA !IH.
Qed .
(* size on a perfect configuration depends which peg we consider *)
Lemma size_lhanoi3_p n p1 p2 :
size_lhanoi3 `c[p1, n] `c[p2] =
if lrel p1 p2 then (3 ^ n).-1 ./2 else (3 ^ n).-1 * (p1 != p2).672 size_lhanoi3 `c[p1 , n] `c[p2] =
(if lrel p1 p2
then ((3 ^ n).-1 )./2
else (3 ^ n).-1 * (p1 != p2))
Proof .706
by rewrite size_lhanoi3E size_app_lhanoi3_p. Qed .
Lemma gdist_lhanoi3_size n (c1 c2 : _ _ n) :
`d[c1, c2]_lmove = size_lhanoi3 c1 c2.62 `d[c1, c2]_lmove = size_lhanoi3 c1 c2
Proof .70b
apply /eqP; rewrite eqn_leq [size_lhanoi3 _ _]size_lhanoi3E.62 `d[c1, c2]_lmove <= size (lhanoi3 c1 c2) <=
`d[c1, c2]_lmove
rewrite gdist_path_le //=; last 2 first .62 path lmove c1 (lhanoi3 c1 c2)
- 714
by apply : path_lhanoi3.
- 71e
by apply : last_lhanoi3.
have /gpath_connect[p1 p1H] : connect lmove c1 c2 by apply : move_lconnect3.63 64 p1 : seq
(finfun_finType (ordinal_finType n)
(ordinal_finType 3 ))
p1H : gpath lmove c1 c2 p1
71b
rewrite (gpath_dist p1H) lhanoi3_min //; first by apply : gpath_path p1H.
by apply : gpath_last p1H.
Qed .
Lemma gdist_lhanoi3p n (p1 p2 : peg 3 ) :
`d[`c[p1, n], `c[p2, n]]_lmove =
if lrel p1 p2 then (3 ^ n).-1 ./2 else (3 ^ n).-1 * (p1 != p2).672 `d[`c[p1 , n], `c[p2 , n]]_lmove =
(if lrel p1 p2
then ((3 ^ n).-1 )./2
else (3 ^ n).-1 * (p1 != p2))
Proof .730
by rewrite gdist_lhanoi3_size size_lhanoi3_p. Qed .
End LHanoi3 .