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.


Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.


Section sHanoi.

(*****************************************************************************)
(*  The pegs are the elements of 'I_n.+3                                     *)
(*****************************************************************************)

Variable m : nat.
Implicit Type p : peg m.+3.

Local Notation "c1 `--> c2" := (smove c1 c2)
    (format "c1  `-->  c2", at level 60).
Local Notation "c1 `-->* c2" := (connect smove c1 c2) 
    (format "c1  `-->*  c2", at level 60).

Let p0 : peg m.+3 := ord0.

Definition so1 p : (peg m.+3) := if (p == inord 1) then inord 2 else inord 1.

Lemma so1_cor p : so1 p != p0 /\ so1 p != p.
m:nat
p0:=ord0:peg m.+3
p:peg m.+3
so1 p != p0 /\ so1 p != p
Proof.
2
rewrite /so1; case: (p =P _) => [->|/eqP pD1]; split.
4
inord 2 != p0
4
inord 2 != inord 1
567
pD1:p != inord 1
inord 1 != p0
12
inord 1 != p
-
b by apply/eqP/val_eqP; rewrite /= !inordK.
4
10
1115
-
19 by apply/eqP/val_eqP; rewrite /= !inordK.
12
14
15
-
1e by apply/eqP/val_eqP; rewrite /= !inordK.
12
16
by rewrite eq_sym.
Qed.

Definition so2 p1 p2 : (peg m.+3) := 
if (p1 == inord 1) then 
  if (p2 == inord 2) then inord 3 else inord 2
else 
  if (p2 == inord 1) then
    if (p1 == inord 2) then inord 3 else inord 2
  else inord 1.

Lemma so2_cor p1 p2 : 
  0 < m ->
  [/\ so2 p1 p2 != p0, so2 p1 p2 != p1 & so2 p1 p2 != p2].
56
p1, p2:peg m.+3
0 < m ->
[/\ so2 p1 p2 != p0, so2 p1 p2 != p1
  & so2 p1 p2 != p2]
Proof.
26
move=> m_gt0.
5629
m_gt0:0 < m
[/\ so2 p1 p2 != p0, so2 p1 p2 != p1
  & so2 p1 p2 != p2]
rewrite /so2; case: (p1 =P _) => [->|/eqP p1D1];
  rewrite /so2; case: (p2 =P _) => [->|/eqP p2D].
2f
[/\ inord 3 != p0, inord 3 != inord 1
  & inord 3 != inord 2]
562930
p2D:p2 != inord 2
[/\ inord 2 != p0, inord 2 != inord 1 & inord 2 != p2]
562930
p1D1:p1 != inord 1
[/\ (if p1 == inord 2 then inord 3 else inord 2) != p0,
    (if p1 == inord 2 then inord 3 else inord 2) != p1
  & (if p1 == inord 2 then inord 3 else inord 2)
    != inord 1]
5629303d
p2D:p2 != inord 1
[/\ inord 1 != p0, inord 1 != p1 & inord 1 != p2]
-
33 by split; apply/eqP/val_eqP; rewrite /= !inordK.
38
3a
3b3f
-
45 by split; try (by rewrite eq_sym); apply/eqP/val_eqP; rewrite /= !inordK.
3c
3e
3f
-
4a case: (p1 =P _) => [->|/eqP p1D2].
3c
[/\ inord 3 != p0, inord 3 != inord 2
  & inord 3 != inord 1]
5629303d
p1D2:p1 != inord 2
[/\ inord 2 != p0, inord 2 != p1 & inord 2 != inord 1]
3f
    by split; apply/eqP/val_eqP; rewrite /= !inordK.
54
56
4c
  by split; try (by rewrite eq_sym); apply/eqP/val_eqP; rewrite /= !inordK.
40
42
by split; try (by rewrite eq_sym); apply/eqP/val_eqP; rewrite /= !inordK.
Qed. 

Lemma shanoi_connect_perfect n (c : configuration _ n) p : c `-->* `c[p].
56
n:nat
c:configuration m.+3 n
7
c `-->* `c[p]
Proof.
5e
have sirr := @sirr m.+3.
5661627
sirr:irreflexive (srel (n:=m.+3))
63
elim: n c p => [c p | n IH c p]; first by apply/eq_connect0/ffunP=> [] [[]].
566961
IH:forall (c : configuration m.+3 n) p,
c `-->* `c[p]
c:configuration m.+3 n.+1
7
63
pose p1 := c ldisk.
5669616e6f7
p1:=c ldisk:(fun=> peg m.+3) ldisk
63
rewrite -[c]cunliftrK -/p1 -[perfect p]cunliftrK perfect_unliftr ffunE.
73
↑[↓[c]]_p1 `-->* ↑[`c[p]]_p
have [<-|/eqP pDp1] := p =P p1; first by apply/connect_liftr/IH.
5669616e6f774
pDp1:p != p1
78
have [p1Ep0|/eqP p1Dp0] := p1 =P p0.
5669616e6f7747d
p1Ep0:p1 = p0
78
5669616e6f7747d
p1Dp0:p1 != p0
78
  rewrite p1Ep0.
81
↑[↓[c]]_p0 `-->* ↑[`c[p]]_p
83
  case: (so1_cor p) => sDp0 sDp.
5669616e6f7747d82
sDp0:so1 p != p0
sDp:so1 p != p
8a
83
  apply: connect_trans (_ : connect _ ↑[`c[so1 p]]_p _); last first.
8e
↑[`c[so1 p]]_p `-->* ↑[`c[p]]_p
8e
↑[↓[c]]_p0 `-->* ↑[`c[so1 p]]_p
84
    by apply/connect_liftr/IH.
8e
97
83
  apply: connect_trans (_ : connect _ ↑[`c[so1 p]]_p0 _).
8e
↑[↓[c]]_p0 `-->* ↑[`c[so1 p]]_p0
8e
↑[`c[so1 p]]_p0 `-->* ↑[`c[so1 p]]_p
84
    by apply/connect_liftr/IH.
8e
a1
83
  apply/connect1/move_liftr_perfect; try by rewrite eq_sym.
8e
srel p0 p
83
  by rewrite /srel /= eq_sym -p1Ep0 pDp1.
85
78
have [pEp0|/eqP pDp0] := p =P p0.
5669616e6f7747d86
pEp0:p = p0
78
5669616e6f7747d86
pDp0:p != p0
78
  case: (so1_cor p1) => sDp0 sDp1.
5669616e6f7747d86b0
sDp0:so1 p1 != p0
sDp1:so1 p1 != p1
78
b1
  apply: connect_trans (_ : connect _ ↑[`c[so1 p1]]_p1 _).
b8
↑[↓[c]]_p1 `-->* ↑[`c[so1 p1]]_p1
b8
↑[`c[so1 p1]]_p1 `-->* ↑[`c[p]]_p
b2
    by apply/connect_liftr/IH.
b8
c1
b1
  apply: connect_trans (_ : connect _ ↑[`c[so1 p1]]_p _).
b8
↑[`c[so1 p1]]_p1 `-->* ↑[`c[so1 p1]]_p
b8
↑[`c[so1 p1]]_p `-->* ↑[`c[p]]_p
b2
    apply/connect1/move_liftr_perfect; try by rewrite eq_sym.
b8
srel p1 p
b8
p != so1 p1
cab2
      by rewrite /srel /= eq_sym pDp1 pEp0 muln0.
b8
d2
c9
    by rewrite eq_sym pEp0.
b8
cb
b1
  by apply/connect_liftr/IH.
b3
78
apply: connect_trans (_ : connect _ ↑[`c[p]]_p1 _).
b3
↑[↓[c]]_p1 `-->* ↑[`c[p]]_p1
b3
↑[`c[p]]_p1 `-->* ↑[`c[p]]_p
  by apply/connect_liftr/IH.
b3
e2
apply: connect_trans (_ : connect _ ↑[`c[p]]_p0 _).
b3
↑[`c[p]]_p1 `-->* ↑[`c[p]]_p0
b3
↑[`c[p]]_p0 `-->* ↑[`c[p]]_p
  apply/connect1/move_liftr_perfect; try by rewrite eq_sym.
b3
srel p1 p0
ea
  by rewrite /srel /= p1Dp0 muln0.
b3
ec
apply: connect_trans (_ : connect _ ↑[`c[p1]]_p0 _).
b3
↑[`c[p]]_p0 `-->* ↑[`c[p1]]_p0
b3
↑[`c[p1]]_p0 `-->* ↑[`c[p]]_p
  by apply/connect_liftr/IH.
b3
fa
apply: connect_trans (_ : connect _ ↑[`c[p1]]_p _).
b3
↑[`c[p1]]_p0 `-->* ↑[`c[p1]]_p
b3
↑[`c[p1]]_p `-->* ↑[`c[p]]_p
  apply/connect1/move_liftr_perfect; try by rewrite // eq_sym.
b3
a8
102
  by rewrite /srel /= eq_sym pDp0.
b3
104
by apply/connect_liftr/IH.
Qed.

Lemma shanoi_connect n (c1 c2 : configuration m.+3 n) : c1 `-->* c2.
5661
c1, c2:configuration m.+3 n
c1 `-->* c2
Proof.
10c
apply: connect_trans (shanoi_connect_perfect _ p0) _.
10e
`c[p0] `-->* c2
rewrite (connect_sym (@ssym m.+3)).
10e
connect (move (srel (n:=m.+3))) c2 `c[p0]
apply: shanoi_connect_perfect.
Qed.

End sHanoi.