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 ghanoi gdist.

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

(******************************************************************************)
(*                                                                            *)
(*              Generalised Hanoi Problem with only 3 pegs                    *)
(*                                                                            *)
(******************************************************************************)


Section GHanoi3.

(******************************************************************************)
(*  The pegs are the three elements of 'I_3                                   *)
(******************************************************************************)

Implicit Type p : peg 3.
Let peg1 : peg 3 := ord0.
Let peg2 : peg 3 := inord 1.
Let peg3 : peg 3 := inord 2.

Lemma peg3E p : [\/ p = peg1, p = peg2 | p = peg3].
peg1:=ord0:peg 3
peg2:=inord 1:peg 3
peg3:=inord 2:peg 3
p:peg 3
[\/ p = peg1, p = peg2 | p = peg3]
Proof.
2
by case: p => [] [|[|[|]]] // H; [apply: Or31|apply: Or32|apply: Or33];
   apply/val_eqP; rewrite //= inordK.
Qed.

(* Finding the free peg that differs from p1 and p2 *)

Lemma opeg3E p p1 p2 : p1 != p2 -> (`p[p1, p2] == p) = ((p1 != p) && (p2 != p)).
567
p, p1, p2:peg 3
p1 != p2 -> (`p[p1, p2] == p) = (p1 != p) && (p2 != p)
Proof.
c
move=> p1Dp2.
567f
p1Dp2:p1 != p2
(`p[p1, p2] == p) = (p1 != p) && (p2 != p)
have D p3 p4 : (p3 == p4) = (val p3 == val p4).
567f16
p3, p4:peg 3
(p3 == p4) = (val p3 == val p4)
567f16
D:forall p3 p4, (p3 == p4) = (val p3 == val p4)
17
  by apply/eqP/idP => /val_eqP.
20
17
move: p1Dp2 (opegDl p1 p2) (opegDr p1 p2).
567f21
p1 != p2 ->
`p[p1, p2] != p1 ->
`p[p1, p2] != p2 ->
(`p[p1, p2] == p) = (p1 != p) && (p2 != p)
by case: (peg3E (opeg p1 p2)) => ->;
   case: (peg3E p1) => ->; 
   case: (peg3E p2) => ->; 
   case: (peg3E p) => ->; 
   rewrite !D /peg1 /peg2 /peg3 /= ?inordK.
Qed.

Lemma opeg3Kl p p1 p2 : p1 != p2 -> `p[`p[p1, p2], p1] = p2.
e
p1 != p2 -> `p[`p[p1, p2], p1] = p2
Proof.
2b
move=> p1Dp2; apply/eqP.
15
`p[`p[p1, p2], p1] == p2
by rewrite !opeg3E ?(eqxx, p1Dp2) // [in p2 != p1]eq_sym p1Dp2.
Qed.

Lemma opeg3Kr p p1 p2 : p1 != p2 -> `p[`p[p1, p2], p2] = p1.
e
p1 != p2 -> `p[`p[p1, p2], p2] = p1
Proof.
34
move=> p1Dp2; apply/eqP.
15
`p[`p[p1, p2], p2] == p1
by rewrite !opeg3E ?(eqxx, p1Dp2) // [in p2 != p1]eq_sym p1Dp2.
Qed.

Variable hrel : rel (peg 3).
Hypothesis hirr : irreflexive hrel.
Hypothesis hsym : symmetric hrel.

Let hmove {n} := @move 3 hrel n.
Let hmove_sym n (c1 c2 : configuration 3 n) : hmove c1 c2 = hmove c2 c1
  := move_sym hsym c1 c2.
Let hconnect n := connect (@hmove n).

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

(* In a move the largest disk has moved, all the smaller disks are pilled up *)
Lemma move_perfectr n (c1 c2 : configuration 3 n.+1) : 
  c1 `--> c2 -> c1 ldisk != c2 ldisk -> ↓[c2] = `c[`p[c1 ldisk, c2 ldisk]].
567
hrel:rel (peg 3)
hirr:irreflexive hrel
hsym:symmetric hrel
hmove:=[eta @move 3 hrel]:forall n : nat, rel (configuration 3 n)
hmove_sym:=fun (n : nat) (c1 : configuration 3 n) =>
[eta move_sym hsym c1]:forall (n : nat)
  (c1 c2 : configuration 3 n),
c1 `--> c2 = c2 `--> c1
hconnect:=fun n : nat => connect hmove:forall n : nat,
rel
  (finfun_finType (ordinal_finType n)
     (ordinal_finType 3))
n:nat
c1, c2:configuration 3 n.+1
c1 `--> c2 ->
c1 ldisk != c2 ldisk ->
↓[c2] = `c[`p[c1 ldisk, c2 ldisk]]
Proof.
3d
move=> c1Mc2 c1lDc2l.
5674041424344454647
c1Mc2:c1 `--> c2
c1lDc2l:c1 ldisk != c2 ldisk
↓[c2] = `c[`p[c1 ldisk, c2 ldisk]]
apply/ffunP => i; rewrite !ffunE.
56740414243444546474e4f
i:ordinal_finType n
c2 (extra.trshift 1 i) = `p[c1 ldisk, c2 ldisk]
have /ffunP/(_ i) := move_ldisk c1Mc2 c1lDc2l; rewrite !ffunE => c1Ec2.
56740414243444546474e4f55
c1Ec2:c1 (extra.trshift 1 i) =
c2 (extra.trshift 1 i)
56
apply/sym_equal/eqP; rewrite opeg3E //; apply/andP; split.
5a
c1 ldisk != c2 (extra.trshift 1 i)
5a
c2 ldisk != c2 (extra.trshift 1 i)
  rewrite -c1Ec2 /=; apply/eqP => c1lEc1r.
56740414243444546474e4f555b
c1lEc1r:c1 ldisk = c1 (extra.trshift 1 i)
False
60
  have /on_topP /(_ _ c1lEc1r) := move_on_topl c1Mc2 c1lDc2l.
66
ldisk <= extra.trshift 1 i -> False
60
  by rewrite /= leqNgt ltn_ord.
5a
62
apply/eqP => c2lEc2r.
56740414243444546474e4f555b
c2lEc2r:c2 ldisk = c2 (extra.trshift 1 i)
68
have /on_topP /(_ _ c2lEc2r):= move_on_topr c1Mc2 c1lDc2l.
73
6c
by rewrite /= leqNgt ltn_ord.
Qed.

Lemma move_perfectl n (c1 c2 : configuration 3 n.+1) : 
  c1 `--> c2 -> c1 ldisk != c2 ldisk -> 
  ↓[c1] = `c[`p[c1 ldisk, c2 ldisk]].
3f
c1 `--> c2 ->
c1 ldisk != c2 ldisk ->
↓[c1] = `c[`p[c1 ldisk, c2 ldisk]]
Proof.
79
rewrite hmove_sym eq_sym opeg_sym.
3f
c2 `--> c1 ->
c2 ldisk != c1 ldisk ->
↓[c1] = `c[`p[c2 ldisk, c1 ldisk]]
exact: move_perfectr.
Qed.

Inductive path3S_spec (n : nat)  (c : configuration 3 n.+1)
                                 (cs : seq (configuration 3 n.+1)) :
   forall (b : bool), Type  :=
| path3S_specW : 
    forall (c' := ↓[c]) (cs' := [seq ↓[i] | i <- cs]) (p := c ldisk),
      cs = [seq ↑[i]_p | i <- cs'] ->
      path hmove c' cs' -> path3S_spec c cs true 
| path3S_spec_move : 
    forall cs1 cs2
           (p1 := c ldisk) p2 (p3 :=`p[p1, p2])
           (c1 := ↓[c]) 
           (c2 := ↑[`c[p3]]_p2),
        p1 != p2 -> hrel p1 p2 ->
        last c1 cs1 = `c[p3] ->
        cs = [seq ↑[i]_p1 | i <- cs1] ++ c2 :: cs2 ->
        path hmove c1 cs1 -> path hmove c2 cs2 ->
        path3S_spec c cs true |
  path3S_spec_false : path3S_spec c cs false.

(* Inversion theorem on a path for disk n.+1 *)
Lemma path3SP  n (c : _ _ n.+1) cs : path3S_spec c cs (path hmove c cs).
56740414243444546
c:configuration 3 n.+1
cs:seq (configuration 3 n.+1)
path3S_spec c cs (path hmove c cs)
Proof.
82
case: pathSP=> //; try by constructor.
84
let p1 := c ldisk in
forall p2 (cs1 : seq (configuration 3 n))
  (cs2 : seq (configuration 3 n.+1)),
let c1 := ↓[c] in
let c2 := ↑[last c1 cs1]_p2 in
p1 != p2 ->
hrel p1 p2 ->
cs = [seq ↑[i1]_p1 | i1 <- cs1] ++ c2 :: cs2 ->
path (move hrel) c1 cs1 ->
move hrel ↑[last c1 cs1]_p1 c2 ->
path (move hrel) c2 cs2 -> path3S_spec c cs true
move=> p1 p2 cs1 cs2 c1 c2 p1Dp2 p1Rp2 csE c1Pcs1 lMc2 c2Pcs2.
567404142434445468586
p1:=c ldisk:peg 3
p2:peg 3
cs1:seq (configuration 3 n)
cs2:seq (configuration 3 n.+1)
c1:=↓[c]:configuration 3 n
c2:=↑[last c1 cs1]_p2:configuration 3 n.+1
16
p1Rp2:hrel p1 p2
csE:cs = [seq ↑[i]_p1 | i <- cs1] ++ c2 :: cs2
c1Pcs1:path (move hrel) c1 cs1
lMc2:move hrel ↑[last c1 cs1]_p1 c2
c2Pcs2:path (move hrel) c2 cs2
path3S_spec c cs true
have lc1cs1E : last c1 cs1 = `c[`p[p1, p2]].
90
last c1 cs1 = `c[`p[p1, p2]]
567404142434445468586919293949596169798999a9b
lc1cs1E:last c1 cs1 = `c[`p[p1, p2]]
9c
  have := move_perfectl lMc2.
90
(↑[last c1 cs1]_p1 ldisk != c2 ldisk ->
 ↓[↑[last c1 cs1]_p1] =
 `c[`p[↑[last c1 cs1]_p1 ldisk, c2 ldisk]]) ->
last c1 cs1 = `c[`p[p1, p2]]
a1
  by rewrite !cliftr_ldisk cliftrK; apply.
a3
9c
apply: path3S_spec_move (lc1cs1E) _ _ _  => //.
a3
cs =
[seq ↑[i]_(c ldisk) | i <- cs1] ++
↑[`c[`p[c ldisk, p2]]]_p2 :: ?Goal
a3
path hmove ↑[`c[`p[c ldisk, p2]]]_p2 ?Goal
-
ad by rewrite csE; congr (_ ++ cliftr _ _ :: _).
a3
path hmove ↑[`c[`p[c ldisk, p2]]]_p2 cs2
by rewrite -lc1cs1E.
Qed.

End GHanoi3.