-
Notifications
You must be signed in to change notification settings - Fork 1
/
ghanoi3.v
129 lines (110 loc) · 4.34 KB
/
ghanoi3.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
From mathcomp Require Import all_ssreflect.
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].
Proof.
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)).
Proof.
move=> p1Dp2.
have D p3 p4 : (p3 == p4) = (val p3 == val p4).
by apply/eqP/idP => /val_eqP.
move: p1Dp2 (opegDl p1 p2) (opegDr p1 p2).
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.
Proof.
move=> p1Dp2; apply/eqP.
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.
Proof.
move=> p1Dp2; apply/eqP.
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]].
Proof.
move=> c1Mc2 c1lDc2l.
apply/ffunP => i; rewrite !ffunE.
have /ffunP/(_ i) := move_ldisk c1Mc2 c1lDc2l; rewrite !ffunE => c1Ec2.
apply/sym_equal/eqP; rewrite opeg3E //; apply/andP; split.
rewrite -c1Ec2 /=; apply/eqP => c1lEc1r.
have /on_topP /(_ _ c1lEc1r) := move_on_topl c1Mc2 c1lDc2l.
by rewrite /= leqNgt ltn_ord.
apply/eqP => c2lEc2r.
have /on_topP /(_ _ c2lEc2r):= move_on_topr c1Mc2 c1lDc2l.
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]].
Proof.
rewrite hmove_sym eq_sym opeg_sym.
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).
Proof.
case: pathSP=> //; try by constructor.
move=> p1 p2 cs1 cs2 c1 c2 p1Dp2 p1Rp2 csE c1Pcs1 lMc2 c2Pcs2.
have lc1cs1E : last c1 cs1 = `c[`p[p1, p2]].
have := move_perfectl lMc2.
by rewrite !cliftr_ldisk cliftrK; apply.
apply: path3S_spec_move (lc1cs1E) _ _ _ => //.
- by rewrite csE; congr (_ ++ cliftr _ _ :: _).
by rewrite -lc1cs1E.
Qed.
End GHanoi3.