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 .
(******************************************************************************)
(* *)
(* Generalised Hanoi Problem *)
(* *)
(******************************************************************************)
(* *)
(* We consider a generalisation of Hanoi problem : *)
(* a parameter n : the number of pegs *)
(* a parameter r : r p1 p2 tells that a disk can go from p1 -> p2 *)
(* *)
(* peg n == type for pegs (there are n pegs) *)
(* disk k == type for disks (there are k disk) *)
(* configuration k n == type for hanoi configuration with *)
(* k disks and n pegs *)
(* ldisk == the largest disk *)
(* sdisk == the smallest disk *)
(* d1 \larger d2 == disk d1 is larger than disk d2 *)
(* c d == the peg on which the disk d in the configuration c *)
(* `c[p] == a configuration with n disk where all the disks *)
(* `p[p1, p2] == pick a peg (if possible) that is diffenent from p1 *)
(* and p2 *)
(* are on peg p *)
(* on_top d c == the disk c is on top of its peg on the *)
(* configuration c *)
(* rrel == a regular relation between pegs, rrel p1 p2 is *)
(* true iff peg p1 is different from peg p2 *)
(* lrel == a linear relation between pegs, lrel p1 p2 is *)
(* true iff peg p1 is next to peg p2 *)
(* srel == a star relation between pegs, srel p1 p2 is *)
(* true iff p1 != p2 and p1 or p2 is the 0 peg *)
(* move r c1 c2 == checks if going from configuration c1 *)
(* to configuration c2 is a move compatible with *)
(* relation r (a relation over pegs) *)
(* cdisjoint c1 c2 == configurations c1 and c2 are on different pegs *)
(* cmerge c1 c2 == merge a configuration c1 with m disk and a *)
(* a configuration with n disks to get a configuration*)
(* with m + n disk *)
(* crshift c == right shift a configuration c with m + n disks, to *)
(* get a configuration with n disks taking the disks *)
(* larger than m *)
(* clshift c == right shift a configuration c with m + n disks, to *)
(* get a configuration with n disks taking the disks *)
(* smaller than m *)
(* ↑[c]_ p == lift a configuration by adding a largest disk on *)
(* peg p. This lifting is done from the largest one *)
(* so to accomodate the usual induction *)
(* ↓[c] == unlift a configuration by removing the largest *)
(* disk *)
(* plift i p == lift a configuration by adding a new empty peg i *)
(* *)
(******************************************************************************)
From mathcomp Require Import all_ssreflect finmap.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
From hanoi Require Import extra gdist.
Set Implicit Arguments .
Unset Strict Implicit .
Unset Printing Implicit Defensive .
Section GHanoi .
Variable q : nat.
(******************************************************************************)
(* The pegs are the elements of 'I_q *)
(******************************************************************************)
Definition peg := 'I_q.
Variable r : rel peg.
Hypothesis irH : irreflexive r.
Hypothesis symH : symmetric r.
Section Disk .
(******************************************************************************)
(* The disks are represented with the element of 'I_n with *)
(* the idea that disk d1 is larger than disk d2 is d2 <= d1. *)
(******************************************************************************)
Variable n : nat.
Definition disk := 'I_n.
Definition mk_disk m (H : m < n) : disk := Ordinal H.
(******************************************************************************)
(* Given a configuration c, the disks on the peg p can be reconstructed by *)
(* the list in decreasing order of the disk d such that c d = p *)
(******************************************************************************)
Definition configuration := {ffun disk -> peg}.
(* A perfect configuration is one where all the pegs are on a single peg p *)
Definition perfect p : configuration := [ffun d => p].
End Disk .
Arguments perfect [n].
Local Notation "`c[ p ] " := (perfect p)
(format "`c[ p ]" , at level 5 ).
(* The smallest disk *)
Definition sdisk {n } : disk n.+1 := ord0.
Lemma disk1_all (d : disk 1 ) : d = sdisk.q : nat
r : rel peg
irH : irreflexive r
symH : symmetric r
d : disk 1
d = sdisk
Proof .2
by apply /val_eqP; case : d => [] []. Qed .
Lemma configuration1_eq (c1 c2 : configuration 1 ) :
(c1 == c2) = (c1 sdisk == c2 sdisk).5 6 7 8 c1, c2 : configuration 1
(c1 == c2) = (c1 sdisk == c2 sdisk)
Proof .d
apply /eqP/eqP; first by move => /ffunP/(_ sdisk).f c1 sdisk = c2 sdisk -> c1 = c2
by move => H; apply /ffunP=> i; rewrite [i]disk1_all.
Qed .
(* The largest disk *)
Definition ldisk {n } : disk n.+1 := ord_max.
(******************************************************************************)
(* The disk d is on top of peg (c d) *)
(******************************************************************************)
Definition on_top n (d : disk n) (c : configuration n) :=
[forall d1 : disk n, (c d == c d1) ==> (d <= d1)].
Lemma on_topP n (d : disk n) (c : configuration n) :
reflect (forall d1 , c d = c d1 -> d <= d1) (on_top d c).5 6 7 8 n : nat
d : disk n
c : configuration n
reflect
(forall d1 : ordinal_finType n,
c d = c d1 -> d <= d1) (on_top d c)
Proof .18
apply : (iffP forallP) => [H d1 cdEcd1|H d1].5 6 7 8 1b 1c 1d H : forall x : ordinal_finType n,
(c d == c x) ==> (d <= x)
d1 : ordinal_finType n
cdEcd1 : c d = c d1
d <= d1
by have /implyP->// := H d1; apply /eqP.
by apply /implyP=> /eqP /H.
Qed .
(******************************************************************************)
(* A move is a relation between two configurations c1 c2: *)
(* there must exist a disk d1, that is the only one that has changed of *)
(* peg (c1 d1 != c2 d1) that is on top of c1 and c2 *)
(******************************************************************************)
Definition move {n } : rel (configuration n) :=
[rel c1 c2 | [exists d1 : disk n,
[&& r ((c1 : configuration n) d1) (c2 d1),
[forall d2 , (d1 != d2) ==> (c1 d2 == c2 d2)],
on_top d1 c1 &
on_top d1 c2]]].
Lemma moveP n (c1 c2 : configuration n) :
reflect
(exists d1 ,
[/\ r (c1 d1) (c2 d1),
forall d2 , d1 != d2 -> c1 d2 = c2 d2,
on_top d1 c1 &
on_top d1 c2])
(move c1 c2).5 6 7 8 1b c1, c2 : configuration n
reflect
(exists d1 : ordinal_finType n,
[/\ r (c1 d1) (c2 d1),
forall d2 : ordinal_finType n,
d1 != d2 -> c1 d2 = c2 d2, on_top d1 c1
& on_top d1 c2]) (move c1 c2)
Proof .31
apply : (iffP existsP) =>
[[d /and4P[H1 /forallP H2 H3 H4]]|[d [H1 H2 H3 H4]]]; exists d .5 6 7 8 1b 34 d : ordinal_finType n
H1 : r (c1 d) (c2 d)
H2 : forall x : ordinal_finType n,
(d != x) ==> (c1 x == c2 x)
H3 : on_top d c1
H4 : on_top d c2
[/\ r (c1 d) (c2 d),
forall d2 : ordinal_finType n,
d != d2 -> c1 d2 = c2 d2, on_top d c1
& on_top d c2]
by split => // d1 H; apply /eqP/(implyP (H2 _)).
rewrite H1 H3 H4 ! andbT /=; apply /forallP => d1; apply /implyP => H.5 6 7 8 1b 34 3b 3c 44 3e 3f 25 H : d != d1
c1 d1 == c2 d1
by rewrite H2.
Qed .
Lemma move_on_topl n d (c1 c2 : configuration n) :
move c1 c2 -> c1 d != c2 d -> on_top d c1.5 6 7 8 1b 3b 34
move c1 c2 -> c1 d != c2 d -> on_top d c1
Proof .50
case /moveP => d1 [H1 H2 H3 H4 H5].5 6 7 8 1b 3b 34 25 H1 : r (c1 d1) (c2 d1)
H2 : forall d2 : ordinal_finType n,
d1 != d2 -> c1 d2 = c2 d2
H3 : on_top d1 c1
H4 : on_top d1 c2
H5 : c1 d != c2 d
on_top d c1
rewrite (_ : d = d1); first by apply : H3.
apply /eqP; case : eqP => /eqP H //.5 6 7 8 1b 3b 34 25 59 5a 5b 5c 5d 4d
false
by case /eqP: H5; apply : H2; rewrite eq_sym.
Qed .
Lemma move_on_topr n d (c1 c2 : configuration n) :
move c1 c2 -> c1 d != c2 d -> on_top d c2.52 move c1 c2 -> c1 d != c2 d -> on_top d c2
Proof .69
case /moveP => d1 [H1 H2 H3 H4 H5].
rewrite (_ : d = d1); first by apply : H4.60
apply /eqP; case : eqP => /eqP H //.63
by case /eqP: H5; apply : H2; rewrite eq_sym.
Qed .
(* this holds if r is symmetric *)
Lemma move_sym n (c1 c2 : configuration n) : move c1 c2 = move c2 c1.33 move c1 c2 = move c2 c1
Proof .73
by apply /moveP/moveP=> [] [d [H1 H2 H3 H4]];
exists d ; split ; rewrite 1 ?symH 1 ?eq_sym // => e dDe; apply /sym_equal/H2.
Qed .
(* In a move, the disk that moves accomodates r *)
Lemma move_diskr n (d : disk n) (c1 c2 : configuration n) :
move c1 c2 -> c1 d != c2 d -> r (c1 d) (c2 d).5 6 7 8 1b 1c 34
move c1 c2 -> c1 d != c2 d -> r (c1 d) (c2 d)
Proof .78
case /moveP=> d1 [H1 H2 H3 H4] /eqP c1dDc2d.5 6 7 8 1b 1c 34 25 59 5a 5b 5c c1dDc2d : c1 d <> c2 d
r (c1 d) (c2 d)
by have [/eqP<-|/H2] := boolP (d1 == d).
Qed .
(* In a move, only one disk moves *)
Lemma move_disk1 n (d1 d2 : disk n) (c1 c2 : configuration n) :
move c1 c2 -> c1 d1 != c2 d1 -> d1 != d2 -> c1 d2 = c2 d2.move c1 c2 ->
c1 d1 != c2 d1 -> d1 != d2 -> c1 d2 = c2 d2
Proof .84
case /moveP=> d3 [H1 H2 H3 H4] c1d1Dc2d1 d1Dd2.5 6 7 8 1b 87 34 d3 : ordinal_finType n
H1 : r (c1 d3) (c2 d3)
H2 : forall d2 : ordinal_finType n,
d3 != d2 -> c1 d2 = c2 d2
H3 : on_top d3 c1
H4 : on_top d3 c2
c1d1Dc2d1 : c1 d1 != c2 d1
d1Dd2 : d1 != d2
c1 d2 = c2 d2
have [/eqP d3Ed1|d3Dd1] := boolP (d3 == d1); last first .5 6 7 8 1b 87 34 8e 8f 90 91 92 93 94 d3Dd1 : d3 != d1
95
by case /eqP: c1d1Dc2d1; apply : H2.
by apply : H2; rewrite d3Ed1.
Qed .
Lemma move_on_toplDl n (d d1 : disk n) (c1 c2 : configuration n) :
move c1 c2 -> c1 d != c2 d -> d1 < d -> c1 d1 != c1 d.move c1 c2 -> c1 d != c2 d -> d1 < d -> c1 d1 != c1 d
Proof .a3
move => c1Mc2 c1Dc2; rewrite eq_sym ltnNge; apply : contra => /eqP.5 6 7 8 1b a6 34 c1Mc2 : move c1 c2
c1Dc2 : c1 d != c2 d
c1 d = c1 d1 -> d <= d1
by have /on_topP := move_on_topl c1Mc2 c1Dc2; apply .
Qed .
Lemma move_on_toplDr n (d d1 : disk n) (c1 c2 : configuration n) :
move c1 c2 -> c1 d != c2 d -> d1 <= d -> c1 d1 != c2 d.a5 move c1 c2 -> c1 d != c2 d -> d1 <= d -> c1 d1 != c2 d
Proof .b1
move => c1Mc2 c1Dc2; rewrite leq_eqVlt => /orP[/val_eqP->//|dLd1].5 6 7 8 1b a6 34 ad ae dLd1 : d1 < d
c1 d1 != c2 d
move : (dLd1); rewrite eq_sym ltnNge (move_disk1 c1Mc2 c1Dc2) //; last first .
by rewrite neq_ltn dLd1 orbT.
apply : contra => /eqP.b8 c2 d = c2 d1 -> d <= d1
by have /on_topP := move_on_topr c1Mc2 c1Dc2; apply .
Qed .
Lemma move_on_toprDr n (d d1 : disk n) (c1 c2 : configuration n) :
move c1 c2 -> c1 d != c2 d -> d1 < d -> c2 d1 != c2 d.a5 move c1 c2 -> c1 d != c2 d -> d1 < d -> c2 d1 != c2 d
Proof .ca
move => c1Mc2 c1Dc2; rewrite eq_sym ltnNge; apply : contra => /eqP.
by have /on_topP := move_on_topr c1Mc2 c1Dc2; apply .
Qed .
Lemma move_on_toprDl n (d d1 : disk n) (c1 c2 : configuration n) :
move c1 c2 -> c1 d != c2 d -> d1 <= d -> c2 d1 != c1 d.a5 move c1 c2 -> c1 d != c2 d -> d1 <= d -> c2 d1 != c1 d
Proof .d2
move => c1Mc2 c1Dc2; rewrite leq_eqVlt => /orP[/val_eqP->//|dLd1].
by rewrite eq_sym.
move : (dLd1); rewrite ltnNge -(move_disk1 c1Mc2 c1Dc2) eq_sym //; last first .
by rewrite neq_ltn dLd1.
apply : contra => /eqP.
have /on_topP := move_on_topl c1Mc2 c1Dc2; apply .
Qed .
(* configuration on different pegs *)
Definition cdisjoint m n (c1 : configuration m) (c2 : configuration n) :=
[forall i , [forall j , c1 i != c2 j]].
Lemma cdisjointP m n (c1 : configuration m) (c2 : configuration n) :
reflect (forall i j , c1 i != c2 j) (cdisjoint c1 c2).5 6 7 8 m, n : nat
c1 : configuration m
c2 : configuration n
reflect
(forall (i : ordinal_finType m)
(j : ordinal_finType n), c1 i != c2 j)
(cdisjoint c1 c2)
Proof .ee
apply : (iffP forallP) => [H i j| H i].5 6 7 8 f1 f2 f3 H : forall x : ordinal_finType m,
[forall j , c1 x != c2 j]
i : ordinal_finType m
j : ordinal_finType n
c1 i != c2 j
by move /forallP : (H i); apply .
by apply /forallP=> j; apply : H.
Qed .
(* merging two configurations : c1 for the small disks, c2 for the big ones *)
Definition cmerge m n (c1 : configuration m) (c2 : configuration n) :=
[ffun i => match tsplit i with inl j => c1 j | inr j => c2 j end ].
(* right shifting a configuration : taking the disks smaller than n *)
Definition crshift m n (c : configuration (m + n)) : configuration n :=
[ffun i => c (trshift m i)].
(* left shifting a configuration : taking the disks larger than n *)
Definition clshift m n (c : configuration (m + n)) : configuration m :=
[ffun i => c (tlshift n i)].
(* Sanity check *)
Lemma cmergeK m n (c : configuration (m + n)) :
cmerge (clshift c) (crshift c) = c.5 6 7 8 f1 c : configuration (m + n)
cmerge (clshift c) (crshift c) = c
Proof .107
apply /ffunP=> i; rewrite !ffunE.5 6 7 8 f1 10a i : ordinal_finType (m + n)
match tsplit i with
| inl j => clshift c j
| inr j => crshift c j
end = c i
by case : tsplitP => [] j iE; rewrite !ffunE /=;
congr fun_of_fin; apply /val_eqP/eqP.
Qed .
Lemma tsplit_tlshift k m (x : 'I_k) : tsplit (tlshift m x) = inl x.tsplit (tlshift m x) = inl x
Proof .114
case : tsplitP=> [j /= jE|k1 /= /eqP].5 6 7 8 117 118 j : 'I_m
jE : x + m = j
inr j = inl x
by have := ltn_ord j; rewrite -jE ltnNge leq_addl.
rewrite eqn_add2r => /eqP H.
by congr (inl _); apply : val_inj.
Qed .
Lemma tsplit_trshift k m (x : 'I_k) : tsplit (trshift m x) = inr x.116 tsplit (trshift m x) = inr x
Proof .131
case : tsplitP => [j /= jE|k1 /= xE].
by congr (inr _); apply : val_inj.
by have := ltn_ord x; rewrite xE ltnNge leq_addl.
Qed .
Lemma on_top_merger m n x (c1 : configuration m) (c2 : configuration n) :
on_top (trshift m x) (cmerge c1 c2) = on_top x c2.on_top (trshift m x) (cmerge c1 c2) = on_top x c2
Proof .146
apply /on_topP/on_topP.148 (forall d1 : ordinal_finType (m + n),
cmerge c1 c2 (trshift m x) = cmerge c1 c2 d1 ->
trshift m x <= d1) ->
forall d1 : ordinal_finType n, c2 x = c2 d1 -> x <= d1
move => Hx d2 cxEcd2.5 6 7 8 f1 149 f2 f3 Hx : forall d1 : ordinal_finType (m + n),
cmerge c1 c2 (trshift m x) = cmerge c1 c2 d1 ->
trshift m x <= d1
d2 : ordinal_finType n
cxEcd2 : c2 x = c2 d2
x <= d2
150
have := Hx (trshift m d2).156 (cmerge c1 c2 (trshift m x) =
cmerge c1 c2 (trshift m d2) ->
trshift m x <= trshift m d2) -> x <= d2
150
by rewrite !ffunE !tsplit_trshift => /(_ cxEcd2).
move => H d; rewrite !ffunE tsplit_trshift /=.5 6 7 8 f1 149 f2 f3 H : forall d1 : ordinal_finType n,
c2 x = c2 d1 -> x <= d1
d : ordinal_finType (m + n)
c2 x =
match tsplit d with
| inl j => c1 j
| inr j => c2 j
end -> x <= d
case : tsplitP => [j -> H1 | k -> _].5 6 7 8 f1 149 f2 f3 166 167 j : 'I_n
H1 : c2 x = c2 j
x <= j
by apply : H.
by apply : leq_trans (ltnW _) (leq_addl _ _).
Qed .
Lemma move_merger m n (c : configuration n) (c1 c2 : configuration m) :
move (cmerge c c1) (cmerge c c2) = move c1 c2.5 6 7 8 f1 1d c1, c2 : configuration m
move (cmerge c c1) (cmerge c c2) = move c1 c2
Proof .179
apply /moveP/moveP => [] [d1 [H1d1 H2d1 H3d1 H4d1]]; last first .5 6 7 8 f1 1d 17c d1 : ordinal_finType m
H1d1 : r (c1 d1) (c2 d1)
H2d1 : forall d2 : ordinal_finType m,
d1 != d2 -> c1 d2 = c2 d2
H3d1 : on_top d1 c1
H4d1 : on_top d1 c2
exists d1 : ordinal_finType (n + m),
[/\ r (cmerge c c1 d1) (cmerge c c2 d1),
forall d2 : ordinal_finType (n + m),
d1 != d2 -> cmerge c c1 d2 = cmerge c c2 d2,
on_top d1 (cmerge c c1)
& on_top d1 (cmerge c c2)]
exists (trshift n d1 ); split => //; try by rewrite on_top_merger.182 r (cmerge c c1 (trshift n d1))
(cmerge c c2 (trshift n d1))
by rewrite !ffunE /= tsplit_trshift.
move => d2; rewrite !ffunE; case : tsplitP => // k d2E H.5 6 7 8 f1 1d 17c 183 184 185 186 187 d2 : ordinal_finType (n + m)
173 d2E : d2 = k
H : trshift n d1 != d2
c1 k = c2 k
189
apply : H2d1 => //; apply : contra H => /eqP->.5 6 7 8 f1 1d 17c 183 184 186 187 1a0 173 1a1
trshift n k == d2
189
by apply /eqP/val_eqP/eqP.18b exists d1 : ordinal_finType m,
[/\ r (c1 d1) (c2 d1),
forall d2 : ordinal_finType m,
d1 != d2 -> c1 d2 = c2 d2, on_top d1 c1
& on_top d1 c2]
move : H1d1; rewrite !ffunE.5 6 7 8 f1 1d 17c 18c 18e 18f 190
r
match tsplit d1 with
| inl j => c j
| inr j => c1 j
end
match tsplit d1 with
| inl j => c j
| inr j => c2 j
end ->
exists d1 : ordinal_finType m,
[/\ r (c1 d1) (c2 d1),
forall d2 : ordinal_finType m,
d1 != d2 -> c1 d2 = c2 d2, on_top d1 c1
& on_top d1 c2]
case : tsplitP => [j jE H1x|k _]; last by rewrite irH.5 6 7 8 f1 1d 17c 18c 18e 18f 190 11f jE : d1 = j
H1x : r (c1 j) (c2 j)
1ac
have d1E : (trshift n j) = d1 by apply /val_eqP/eqP.5 6 7 8 f1 1d 17c 18c 18e 18f 190 11f 1b6 1b7 d1E : trshift n j = d1
1ac
rewrite -d1E in H3d1 H4d1.5 6 7 8 f1 1d 17c 18c 18e 11f 1b6 1b7 1bc H3d1 : on_top (trshift n j) (cmerge c c1)
H4d1 : on_top (trshift n j) (cmerge c c2)
1ac
exists j ; split => //; try by rewrite -(on_top_merger _ c).1c0 forall d2 : ordinal_finType m,
j != d2 -> c1 d2 = c2 d2
move => d2 kDd2.5 6 7 8 f1 1d 17c 18c 18e 11f 1b6 1b7 1bc 1c1 1c2 d2 : ordinal_finType m
kDd2 : j != d2
95
have := H2d1 (trshift n d2).1ca (d1 != trshift n d2 ->
cmerge c c1 (trshift n d2) =
cmerge c c2 (trshift n d2)) -> c1 d2 = c2 d2
rewrite !ffunE tsplit_trshift => H.5 6 7 8 f1 1d 17c 18c 18e 11f 1b6 1b7 1bc 1c1 1c2 1cb 1cc H : d1 != trshift n d2 -> c1 d2 = c2 d2
95
apply : H.
apply : contra kDd2 => /eqP/val_eqP /=.5 6 7 8 f1 1d 17c 18c 18e 11f 1b6 1b7 1bc 1c1 1c2 1cb
d1 == d2 -> j == d2
by rewrite jE.
Qed .
Lemma path_merger m n (c1 : configuration m)
(c2 : configuration n) (cs : seq (configuration _)) :
path move (cmerge c1 c2) [seq cmerge c1 c | c <- cs] =
path move c2 cs.5 6 7 8 f1 f2 f3 cs : seq (configuration n)
path move (cmerge c1 c2) [seq cmerge c1 c | c <- cs] =
path move c2 cs
Proof .1e0
by elim : cs c2 => //= c3 cs IH c2; rewrite move_merger IH. Qed .
Lemma connect_merger m n (c : configuration m) (c1 c2 : configuration n) :
connect move c1 c2 -> connect move (cmerge c c1) (cmerge c c2).5 6 7 8 f1 c : configuration m
34 connect move c1 c2 ->
connect move (cmerge c c1) (cmerge c c2)
Proof .1e7
move => /connectP[x]; rewrite -(path_merger c) => Hp Hl.5 6 7 8 f1 1ea 34 x : seq
(finfun_finType (ordinal_finType n)
(ordinal_finType q))
Hp : path move (cmerge c c1)
[seq cmerge c c0 | c0 <- x]
Hl : c2 = last c1 x
connect move (cmerge c c1) (cmerge c c2)
apply /connectP; eexists ; first exact : Hp.1f0 cmerge c c2 =
last (cmerge c c1) [seq cmerge c c0 | c0 <- x]
by rewrite Hl [RHS]last_map.
Qed .
(* this should be equality *)
Lemma gdist_merger m n (c : configuration m) (c1 c2 : configuration n) :
connect move c1 c2 ->
`d[cmerge c c1, cmerge c c2]_move <= `d[c1, c2]_move.1e9 connect move c1 c2 ->
`d[cmerge c c1, cmerge c c2]_move <= `d[c1, c2]_move
Proof .1fa
move => /gpath_connect[p1 p1H].5 6 7 8 f1 1ea 34 p1 : seq
(finfun_finType (ordinal_finType n)
(ordinal_finType q))
p1H : gpath move c1 c2 p1
`d[cmerge c c1, cmerge c c2]_move <= `d[c1, c2]_move
rewrite (gpath_dist p1H) -(size_map (cmerge c)).201 `d[cmerge c c1, cmerge c c2]_move <=
size [seq cmerge c i | i <- p1]
apply : gdist_path_le; first by rewrite path_merger (gpath_path p1H).201 last (cmerge c c1) [seq cmerge c i | i <- p1] =
cmerge c c2
by rewrite [LHS]last_map (gpath_last p1H).
Qed .
Lemma on_top_mergel m n (c1 : configuration m) (c2 : configuration n) d :
cdisjoint c1 c2 -> on_top d c1 -> on_top (tlshift n d) (cmerge c1 c2).cdisjoint c1 c2 ->
on_top d c1 -> on_top (tlshift n d) (cmerge c1 c2)
Proof .20e
move => c1Dc2 /on_topP dTc; apply /on_topP => d1.5 6 7 8 f1 f2 f3 211 c1Dc2 : cdisjoint c1 c2
dTc : forall d1 : ordinal_finType m,
c1 d = c1 d1 -> d <= d1
d1 : ordinal_finType (m + n)
cmerge c1 c2 (tlshift n d) = cmerge c1 c2 d1 ->
tlshift n d <= d1
rewrite !ffunE tsplit_tlshift /=.217 c1 d =
match tsplit d1 with
| inl j => c1 j
| inr j => c2 j
end -> d + n <= d1
case : tsplitP => j -> c1dc1j; last first .5 6 7 8 f1 f2 f3 211 218 219 21a 11f c1dc1j : c1 d = c1 j
d + n <= j + n
by rewrite leq_add2r; apply : dTc.
by have /cdisjointP/(_ d j)/eqP[] := c1Dc2.
Qed .
Lemma on_top_mergel_inv m n (c1 : configuration m) (c2 : configuration n) d :
on_top (tlshift n d) (cmerge c1 c2) -> on_top d c1.on_top (tlshift n d) (cmerge c1 c2) -> on_top d c1
Proof .22f
move => /on_topP dTc; apply /on_topP => d1 Hc.5 6 7 8 f1 f2 f3 232 dTc : forall d1 : ordinal_finType (m + n),
cmerge c1 c2 (tlshift n d) = cmerge c1 c2 d1 ->
tlshift n d <= d1
183 Hc : c1 d = c1 d1
27
have := dTc (tlshift n d1).238 (cmerge c1 c2 (tlshift n d) =
cmerge c1 c2 (tlshift n d1) ->
tlshift n d <= tlshift n d1) -> d <= d1
by rewrite !ffunE !tsplit_tlshift /= leq_add2r; apply .
Qed .
Lemma move_mergel m n (c1 c2 : configuration m) (c : configuration n) :
move (cmerge c1 c) (cmerge c2 c) -> move c1 c2.5 6 7 8 f1 17c 1d
move (cmerge c1 c) (cmerge c2 c) -> move c1 c2
Proof .240
move => /moveP [x [H1x H2x H3x H4x]]; apply /moveP.5 6 7 8 f1 17c 1d x : ordinal_finType (m + n)
H1x : r (cmerge c1 c x) (cmerge c2 c x)
H2x : forall d2 : ordinal_finType (m + n),
x != d2 -> cmerge c1 c d2 = cmerge c2 c d2
H3x : on_top x (cmerge c1 c)
H4x : on_top x (cmerge c2 c)
1ac
move : H1x; rewrite !ffunE.5 6 7 8 f1 17c 1d 249 24b 24c 24d
r
match tsplit x with
| inl j => c1 j
| inr j => c j
end
match tsplit x with
| inl j => c2 j
| inr j => c j
end ->
exists d1 : ordinal_finType m,
[/\ r (c1 d1) (c2 d1),
forall d2 : ordinal_finType m,
d1 != d2 -> c1 d2 = c2 d2, on_top d1 c1
& on_top d1 c2]
case : tsplitP => [j | k kE J1x]; first by rewrite irH.5 6 7 8 f1 17c 1d 249 24b 24c 24d 173 kE : x = k + n
J1x : r (c1 k) (c2 k)
1ac
have xE : (tlshift n k) = x by apply /val_eqP/eqP.5 6 7 8 f1 17c 1d 249 24b 24c 24d 173 257 258 xE : tlshift n k = x
1ac
rewrite -xE in H3x H4x.5 6 7 8 f1 17c 1d 249 24b 173 257 258 25d H3x : on_top (tlshift n k) (cmerge c1 c)
H4x : on_top (tlshift n k) (cmerge c2 c)
1ac
exists k ; split => //; try by apply : on_top_mergel_inv; eassumption .261 forall d2 : ordinal_finType m,
k != d2 -> c1 d2 = c2 d2
move => d2 kDd2.5 6 7 8 f1 17c 1d 249 24b 173 257 258 25d 262 263 1cb kDd2 : k != d2
95
have := H2x (tlshift n d2).26b (x != tlshift n d2 ->
cmerge c1 c (tlshift n d2) =
cmerge c2 c (tlshift n d2)) -> c1 d2 = c2 d2
rewrite !ffunE tsplit_tlshift => H.5 6 7 8 f1 17c 1d 249 24b 173 257 258 25d 262 263 1cb 26c H : x != tlshift n d2 -> c1 d2 = c2 d2
95
apply : H.
apply : contra kDd2 => /eqP/val_eqP /=.5 6 7 8 f1 17c 1d 249 24b 173 257 258 25d 262 263 1cb
x == d2 + n -> k == d2
by rewrite kE eqn_add2r.
Qed .
Lemma move_mergel_inv m n (c1 c2 : configuration m)
(c : configuration n) :
cdisjoint c1 c -> cdisjoint c2 c ->
move c1 c2 -> move (cmerge c1 c) (cmerge c2 c).242 cdisjoint c1 c ->
cdisjoint c2 c ->
move c1 c2 -> move (cmerge c1 c) (cmerge c2 c)
Proof .280
move => c1Dc c2Dc /moveP[x [H1x H2x H3x H4x]]; apply /moveP.5 6 7 8 f1 17c 1d c1Dc : cdisjoint c1 c
c2Dc : cdisjoint c2 c
x : ordinal_finType m
H1x : r (c1 x) (c2 x)
H2x : forall d2 : ordinal_finType m,
x != d2 -> c1 d2 = c2 d2
H3x : on_top x c1
H4x : on_top x c2
exists d1 : ordinal_finType (m + n),
[/\ r (cmerge c1 c d1) (cmerge c2 c d1),
forall d2 : ordinal_finType (m + n),
d1 != d2 -> cmerge c1 c d2 = cmerge c2 c d2,
on_top d1 (cmerge c1 c)
& on_top d1 (cmerge c2 c)]
exists (tlshift n x ); split => //; try by apply /on_top_mergel.287 r (cmerge c1 c (tlshift n x))
(cmerge c2 c (tlshift n x))
by rewrite !ffunE /= tsplit_tlshift.
move => d2; rewrite !ffunE; case : tsplitP => // k d2E H.5 6 7 8 f1 17c 1d 288 289 28a 28b 28c 28d 28e d2 : ordinal_finType (m + n)
173 d2E : d2 = k + n
H : tlshift n x != d2
1a3
apply : H2x => //; apply : contra H => /eqP->.5 6 7 8 f1 17c 1d 288 289 28a 28b 28d 28e 29e 173 29f
tlshift n k == d2
by apply /eqP/val_eqP/eqP.
Qed .
Lemma path_mergel m n (c1 : configuration m)
(c2 : configuration n) (cs : seq (configuration _)) :
path move (cmerge c1 c2) [seq cmerge i c2 | i <- cs] ->
path move c1 cs.5 6 7 8 f1 f2 f3 cs : seq (configuration m)
path move (cmerge c1 c2) [seq cmerge i c2 | i <- cs] ->
path move c1 cs
Proof .2a7
by elim : cs c1 => //= c3 cs IH c1 /andP[/move_mergel-> /IH]. Qed .
Lemma path_mergel_inv m n (c1 : configuration m)
(c2 : configuration n) (cs : seq (configuration _)) :
all (fun i => cdisjoint i c2) (c1 :: cs) ->
path move c1 cs ->
path move (cmerge c1 c2) [seq cmerge i c2 | i <- cs].2a9 all ((cdisjoint (n:=n))^~ c2) (c1 :: cs) ->
path move c1 cs ->
path move (cmerge c1 c2) [seq cmerge i c2 | i <- cs]
Proof .2ae
elim : cs c1 => //= c3 cs IH c1 /and3P[c1Dc2 c3Dc2 Dcs]
/andP[/move_mergel_inv ->// /IH->//].5 6 7 8 f1 f3 c3 : configuration m
2aa IH : forall c1 : configuration m,
cdisjoint c1 c2 &&
all ((cdisjoint (n:=n))^~ c2) cs ->
path move c1 cs ->
path move (cmerge c1 c2)
[seq cmerge i c2 | i <- cs]
f2 218 c3Dc2 : cdisjoint c3 c2
Dcs : all ((cdisjoint (n:=n))^~ c2) cs
cdisjoint c3 c2 && all ((cdisjoint (n:=n))^~ c2) cs
by rewrite c3Dc2.
Qed .
Lemma on_top_shift m n (c : configuration (m + n)) d :
on_top d c ->
match tsplit d with
| inl d1 => on_top d1 (clshift c)
| inr d2 => on_top d2 (crshift c)
end .on_top d c ->
match tsplit d with
| inl d1 => on_top d1 (clshift c)
| inr d2 => on_top d2 (crshift c)
end
Proof .2bc
rewrite -{1 }[d](tsplitK d).2be on_top (tunsplit (tsplit d)) c ->
match tsplit d with
| inl d1 => on_top d1 (clshift c)
| inr d2 => on_top d2 (crshift c)
end
case : tsplitP => /= j dE /on_topP /= dT;
apply /on_topP => d1; rewrite !ffunE /= => H.5 6 7 8 f1 10a 2bf 16d dE : d = j
dT : forall d1 : 'I_(m + n),
c (trshift m j) = c d1 -> j <= d1
25 H : c (trshift m j) = c (trshift m d1)
j <= d1
by apply : dT H.
by have /= := dT _ H; rewrite leq_add2r.
Qed .
Lemma move_clshift m n (c1 c2 : configuration (m + n)) :
move c1 c2 -> (clshift c1) != (clshift c2) ->
move (clshift c1) (clshift c2).5 6 7 8 f1 c1, c2 : configuration (m + n)
move c1 c2 ->
clshift c1 != clshift c2 ->
move (clshift c1) (clshift c2)
Proof .2d8
move => /moveP [x].5 6 7 8 f1 2db 249
[/\ r (c1 x) (c2 x),
forall d2 : ordinal_finType (m + n),
x != d2 -> c1 d2 = c2 d2, on_top x c1
& on_top x c2] ->
clshift c1 != clshift c2 ->
move (clshift c1) (clshift c2)
rewrite -(tsplitK x).2e1 [/\ r (c1 (tunsplit (tsplit x)))
(c2 (tunsplit (tsplit x))),
forall d2 : ordinal_finType (m + n),
tunsplit (tsplit x) != d2 -> c1 d2 = c2 d2,
on_top (tunsplit (tsplit x)) c1
& on_top (tunsplit (tsplit x)) c2] ->
clshift c1 != clshift c2 ->
move (clshift c1) (clshift c2)
have := @on_top_shift _ _ c1 x.2e1 (on_top x c1 ->
match tsplit x with
| inl d1 => on_top d1 (clshift c1)
| inr d2 => on_top d2 (crshift c1)
end ) ->
[/\ r (c1 (tunsplit (tsplit x)))
(c2 (tunsplit (tsplit x))),
forall d2 : ordinal_finType (m + n),
tunsplit (tsplit x) != d2 -> c1 d2 = c2 d2,
on_top (tunsplit (tsplit x)) c1
& on_top (tunsplit (tsplit x)) c2] ->
clshift c1 != clshift c2 ->
move (clshift c1) (clshift c2)
have := @on_top_shift _ _ c2 x.2e1 (on_top x c2 ->
match tsplit x with
| inl d1 => on_top d1 (clshift c2)
| inr d2 => on_top d2 (crshift c2)
end ) ->
(on_top x c1 ->
match tsplit x with
| inl d1 => on_top d1 (clshift c1)
| inr d2 => on_top d2 (crshift c1)
end ) ->
[/\ r (c1 (tunsplit (tsplit x)))
(c2 (tunsplit (tsplit x))),
forall d2 : ordinal_finType (m + n),
tunsplit (tsplit x) != d2 -> c1 d2 = c2 d2,
on_top (tunsplit (tsplit x)) c1
& on_top (tunsplit (tsplit x)) c2] ->
clshift c1 != clshift c2 ->
move (clshift c1) (clshift c2)
case : tsplitP => /= [j xE c2H c1H [H1j H2j H3j H4j] c1Dc2|
k xE c2H c1H [H1k H2k H3k H4k] c1Dc2].5 6 7 8 f1 2db 249 16d xE : x = j
c2H : on_top x c2 -> on_top j (crshift c2)
c1H : on_top x c1 -> on_top j (crshift c1)
H1j : r (c1 (trshift m j)) (c2 (trshift m j))
H2j : forall d2 : 'I_(m + n),
trshift m j != d2 -> c1 d2 = c2 d2
H3j : on_top (trshift m j) c1
H4j : on_top (trshift m j) c2
c1Dc2 : clshift c1 != clshift c2
move (clshift c1) (clshift c2)
case /eqP: c1Dc2; apply /ffunP => i.5 6 7 8 f1 2db 249 16d 2f3 2f4 2f5 2f6 2f7 2f8 2f9 fb
clshift c1 i = clshift c2 i
2fc
rewrite !ffunE.309 c1 (tlshift n i) = c2 (tlshift n i)
2fc
apply /H2j/eqP/val_eqP; rewrite eqn_leq /= negb_and.309 ~~ (j <= i + n) || ~~ (i + n <= j)
2fc
by rewrite orbC -ltnNge (leq_trans (ltn_ord _)) // leq_addl.
apply /moveP; exists k ; split => [|d2 kDd2||]; rewrite ?ffunE //.5 6 7 8 f1 2db 249 173 2ff 300 301 302 303 304 305 2fa 1cb 26c
c1 (tlshift n d2) = c2 (tlshift n d2)
- 317
apply : H2k => /=.5 6 7 8 f1 2db 249 173 2ff 300 301 302 304 305 2fa 1cb 26c
tlshift n k != tlshift n d2
31b
by apply /eqP/val_eqP; rewrite /= eqn_add2r; apply /val_eqP/eqP.
- 327
apply : c1H; rewrite (_ : x = (tlshift n k)) //.5 6 7 8 f1 2db 249 173 2ff 300 302 303 304 305 2fa
x = tlshift n k
329
by apply /val_eqP/eqP => /=.
apply : c2H; rewrite (_ : x = (tlshift n k)) //.5 6 7 8 f1 2db 249 173 2ff 301 302 303 304 305 2fa
32f
by apply /val_eqP/eqP => /=.
Qed .
Lemma move_crshift m n (c1 c2 : configuration (m + n)) :
move c1 c2 -> (crshift c1) != (crshift c2) ->
move (crshift c1) (crshift c2).2da move c1 c2 ->
crshift c1 != crshift c2 ->
move (crshift c1) (crshift c2)
Proof .338
move => /moveP [x].2e1 [/\ r (c1 x) (c2 x),
forall d2 : ordinal_finType (m + n),
x != d2 -> c1 d2 = c2 d2, on_top x c1
& on_top x c2] ->
crshift c1 != crshift c2 ->
move (crshift c1) (crshift c2)
rewrite -(tsplitK x).2e1 [/\ r (c1 (tunsplit (tsplit x)))
(c2 (tunsplit (tsplit x))),
forall d2 : ordinal_finType (m + n),
tunsplit (tsplit x) != d2 -> c1 d2 = c2 d2,
on_top (tunsplit (tsplit x)) c1
& on_top (tunsplit (tsplit x)) c2] ->
crshift c1 != crshift c2 ->
move (crshift c1) (crshift c2)
have := @on_top_shift _ _ c1 x.2e1 (on_top x c1 ->
match tsplit x with
| inl d1 => on_top d1 (clshift c1)
| inr d2 => on_top d2 (crshift c1)
end ) ->
[/\ r (c1 (tunsplit (tsplit x)))
(c2 (tunsplit (tsplit x))),
forall d2 : ordinal_finType (m + n),
tunsplit (tsplit x) != d2 -> c1 d2 = c2 d2,
on_top (tunsplit (tsplit x)) c1
& on_top (tunsplit (tsplit x)) c2] ->
crshift c1 != crshift c2 ->
move (crshift c1) (crshift c2)
have := @on_top_shift _ _ c2 x.2e1 (on_top x c2 ->
match tsplit x with
| inl d1 => on_top d1 (clshift c2)
| inr d2 => on_top d2 (crshift c2)
end ) ->
(on_top x c1 ->
match tsplit x with
| inl d1 => on_top d1 (clshift c1)
| inr d2 => on_top d2 (crshift c1)
end ) ->
[/\ r (c1 (tunsplit (tsplit x)))
(c2 (tunsplit (tsplit x))),
forall d2 : ordinal_finType (m + n),
tunsplit (tsplit x) != d2 -> c1 d2 = c2 d2,
on_top (tunsplit (tsplit x)) c1
& on_top (tunsplit (tsplit x)) c2] ->
crshift c1 != crshift c2 ->
move (crshift c1) (crshift c2)
case : tsplitP => /= [j xE c2H c1H [H1j H2j H3j H4j] c1Dc2|
k xE c2H c1H [H1k H2k H3k H4k] c1Dc2]; last first .5 6 7 8 f1 2db 249 173 2ff 300 301 302 303 304 305 c1Dc2 : crshift c1 != crshift c2
move (crshift c1) (crshift c2)
case /eqP: c1Dc2; apply /ffunP => i.5 6 7 8 f1 2db 249 173 2ff 300 301 302 303 304 305 i : ordinal_finType n
crshift c1 i = crshift c2 i
352
rewrite !ffunE.358 c1 (trshift m i) = c2 (trshift m i)
352
apply /H2k/eqP/val_eqP; rewrite eqn_leq /= negb_and.358 ~~ (k + n <= i) || ~~ (i <= k + n)
352
by rewrite -ltnNge (leq_trans (ltn_ord _)) // leq_addl.
apply /moveP; exists j ; split => [|d2 kDd2||]; rewrite ?ffunE //.5 6 7 8 f1 2db 249 16d 2f3 2f4 2f5 2f6 2f7 2f8 2f9 350 158 1cc
c1 (trshift m d2) = c2 (trshift m d2)
- 367
by apply : H2j.
- 372
apply : c1H; rewrite (_ : x = (trshift m j)) //.5 6 7 8 f1 2db 249 16d 2f3 2f4 2f6 2f7 2f8 2f9 350
x = trshift m j
374
by apply /val_eqP/eqP => /=.
apply : c2H; rewrite (_ : x = (trshift m j)) //.5 6 7 8 f1 2db 249 16d 2f3 2f5 2f6 2f7 2f8 2f9 350
37a
by apply /val_eqP/eqP => /=.
Qed .
Fixpoint rm_rep (A : eqType) (a : A) (s : seq A) :=
if s is b :: s1 then
if a == b then rm_rep b s1 else b :: rm_rep b s1
else [::].
Lemma subseq_rm_rep (A : eqType) (a : A) s : subseq (rm_rep a s) s.
Proof .383
elim : s a => // b s IH a.5 6 7 8 386 b : A
388 IH : forall a : A, subseq (rm_rep a s) s
387 subseq (rm_rep a (b :: s)) (b :: s)
rewrite [rm_rep _ _]/=; case : (a == b).38e subseq (rm_rep b s) (b :: s)
by apply : subseq_trans (IH _) (subseq_cons _ _).
by rewrite /= eqxx IH.
Qed .
Lemma subset_rm_rep (A : eqType) (a : A) s : {subset rm_rep a s <= s}.385 {subset rm_rep a s <= s}
Proof .39d
by apply /mem_subseq/subseq_rm_rep. Qed .
Lemma size_rm_rep (A : eqType) (a : A) s : size (rm_rep a s) <= size s.385 size (rm_rep a s) <= size s
Proof .3a2
by apply /size_subseq/subseq_rm_rep. Qed .
Lemma size_rm_rep_cons (A : eqType) (a b : A) s :
size (rm_rep b s) <= size (rm_rep a (b :: s)).size (rm_rep b s) <= size (rm_rep a (b :: s))
Proof .3a7
by rewrite /=; case : (_ == _) => //=. Qed .
Lemma size_rm_rep_subset (A : finType) (a : A) (s1 : {set A}) (s2 : seq A) :
{subset s1 <= s2} -> a \notin s1 -> #|s1| <= size (rm_rep a s2).5 6 7 8 A : finType
387 s1 : {set A}
s2 : seq A
{subset s1 <= s2} ->
a \notin s1 -> #|s1| <= size (rm_rep a s2)
Proof .3ae
elim : s2 s1 a => /= [s1 a aS _|b s2 IH s1 a s1S aNIs1].5 6 7 8 3b1 3b2 387 aS : {subset s1 <= [::]}
#|s1| <= 0
rewrite leqn0 cards_eq0; apply /eqP/setP=> i.(i \in s1) = (i \in set0)
3bc
by rewrite inE; apply /idP => /aS.
case : eqP=> [aEb|aDb].5 6 7 8 3b1 38f 3b3 3bf 3b2 387 3c0 3c1 aEb : a = b
#|s1| <= size (rm_rep b s2)
rewrite -aEb; apply : IH => //.5 6 7 8 3b1 38f 3b3 3b2 387 3c0 3c1 3d0
{subset s1 <= s2}
3d2
move => i is1; have := is1; have := s1S _ is1; rewrite inE.5 6 7 8 3b1 38f 3b3 3b2 387 3c0 3c1 3d0 3c7 is1 : i \in s1
(i == b) || (i \in s2) -> i \in s1 -> i \in s2
3d2
by case /orP=> [/eqP->|//]; rewrite -aEb => aIs1; case /negP: aNIs1.
have [bIs1|bNIs1]/= := boolP (b \in s1); last first .5 6 7 8 3b1 38f 3b3 3bf 3b2 387 3c0 3c1 3d5 bNIs1 : b \notin s1
#|s1| <= (size (rm_rep b s2)).+1
apply : leq_trans (IH _ _ _ bNIs1) _ => //.
move => i is1; have := is1; have := s1S _ is1; rewrite inE.5 6 7 8 3b1 38f 3b3 3bf 3b2 387 3c0 3c1 3d5 3e9 3c7 3e0
3e1 3eb
by case /orP=> [/eqP->|//] => bIs1; case /negP: bNIs1.
rewrite (cardsD1 b) bIs1 ltnS.3ed #|s1 :\ b| <= size (rm_rep b s2)
apply : IH => [i|].5 6 7 8 3b1 38f 3b3 3b2 387 3c0 3c1 3d5 3ee 3c7
i \in s1 :\ b -> i \in s2
by rewrite !inE => /andP[iDb1 /s1S]; rewrite inE (negPf iDb1).
by rewrite !inE eqxx.
Qed .
Lemma last_rm_rep (A : eqType) (a : A) s : last a (rm_rep a s) = last a s.385 last a (rm_rep a s) = last a s
Proof .40a
by elim : s a => //= b l IH a; case : (_ =P _) => /= [->|_]; apply : IH.
Qed .
Lemma cat_rm_rep (A : eqType) (a : A) s1 s2 :
rm_rep a (s1 ++ s2) = rm_rep a s1 ++ rm_rep (last a s1) s2.rm_rep a (s1 ++ s2) =
rm_rep a s1 ++ rm_rep (last a s1) s2
Proof .40f
elim : s1 s2 a => //= b s1 IH s2 a.5 6 7 8 386 38f s1 : seq A
IH : forall (s2 : seq A) (a : A),
rm_rep a (s1 ++ s2) =
rm_rep a s1 ++ rm_rep (last a s1) s2
3b3 387 (if a == b
then rm_rep b (s1 ++ s2)
else b :: rm_rep b (s1 ++ s2)) =
(if a == b then rm_rep b s1 else b :: rm_rep b s1) ++
rm_rep (last b s1) s2
case : eqP => [aEb|aDb] /=; first by apply : IH.5 6 7 8 386 38f 419 41a 3b3 387 3d5
b :: rm_rep b (s1 ++ s2) =
b :: rm_rep b s1 ++ rm_rep (last b s1) s2
by congr (_ :: _); apply : IH.
Qed .
Lemma mem_rm_rep (A : eqType) (a b : A) s :
b != a -> b \in s -> b \in rm_rep a s.5 6 7 8 386 3aa s : seq_predType A
b != a -> b \in s -> b \in rm_rep a s
Proof .422
elim : s a => //= c s IH a bDa; rewrite inE.5 6 7 8 386 b, c : A
388 IH : forall a : A,
b != a -> b \in s -> b \in rm_rep a s
387 bDa : b != a
(b == c) || (b \in s) ->
b \in (if a == c then rm_rep c s else c :: rm_rep c s)
case : (boolP (b == c)) => /= [/eqP<- _|bDc bIs].42b b \in (if a == b then rm_rep b s else b :: rm_rep b s)
by rewrite eq_sym (negPf bDa) inE eqxx.
by have := IH _ bDc bIs; case : (_ == _); rewrite // inE orbC => ->.
Qed .
Lemma path_clshift m n (c : configuration (m + n)) cs :
path move c cs ->
path move (clshift c) (rm_rep (clshift c) [seq (clshift i) | i <- cs]).5 6 7 8 f1 10a cs : seq (configuration (m + n))
path move c cs ->
path move (clshift c)
(rm_rep (clshift c) [seq clshift i | i <- cs])
Proof .43e
elim : cs c => //= c1 cs IH c => /andP[cMc1 c1Pcs].5 6 7 8 f1 c1 : configuration (m + n)
441 IH : forall c : configuration (m + n),
path move c cs ->
path move (clshift c)
(rm_rep (clshift c) [seq clshift i | i <- cs])
10a cMc1 : move c c1
c1Pcs : path move c1 cs
path move (clshift c)
(if clshift c == clshift c1
then rm_rep (clshift c1) [seq clshift i | i <- cs]
else
clshift c1
:: rm_rep (clshift c1) [seq clshift i | i <- cs])
case : eqP => [->|/eqP cDc1 /=]; first by apply : IH.5 6 7 8 f1 448 441 449 10a 44a 44b cDc1 : clshift c != clshift c1
move (clshift c) (clshift c1) &&
path move (clshift c1)
(rm_rep (clshift c1) [seq clshift i | i <- cs])
by rewrite move_clshift //=; apply : IH.
Qed .
Lemma path_crshift m n (c : configuration (m + n)) cs :
path move c cs ->
path move (crshift c) (rm_rep (crshift c) [seq (crshift i) | i <- cs]).440 path move c cs ->
path move (crshift c)
(rm_rep (crshift c) [seq crshift i | i <- cs])
Proof .454
elim : cs c => //= c1 cs IH c => /andP[cMc1 c1Pcs].5 6 7 8 f1 448 441 IH : forall c : configuration (m + n),
path move c cs ->
path move (crshift c)
(rm_rep (crshift c) [seq crshift i | i <- cs])
10a 44a 44b path move (crshift c)
(if crshift c == crshift c1
then rm_rep (crshift c1) [seq crshift i | i <- cs]
else
crshift c1
:: rm_rep (crshift c1) [seq crshift i | i <- cs])
case : eqP => [->|/eqP cDc1 /=]; first by apply : IH.5 6 7 8 f1 448 441 45c 10a 44a 44b cDc1 : crshift c != crshift c1
move (crshift c) (crshift c1) &&
path move (crshift c1)
(rm_rep (crshift c1) [seq crshift i | i <- cs])
by rewrite move_crshift //=; apply : IH.
Qed .
Lemma path_shift m n (c : configuration (m + n)) cs :
path move c cs ->
size cs = (size (rm_rep (clshift c) [seq (clshift i) | i <- cs]) +
size(rm_rep (crshift c) [seq (crshift i) | i <- cs]))%nat.440 path move c cs ->
size cs =
size (rm_rep (clshift c) [seq clshift i | i <- cs]) +
size (rm_rep (crshift c) [seq crshift i | i <- cs])
Proof .465
elim : cs c => //= c1 cs IH c /andP[/moveP[d [d2H d2H1 d2H2 d2H3]] c1Pcs].5 6 7 8 f1 448 441 IH : forall c : configuration (m + n),
path move c cs ->
size cs =
size
(rm_rep (clshift c) [seq clshift i | i <- cs]) +
size
(rm_rep (crshift c) [seq crshift i | i <- cs])
10a 167 d2H : r (c d) (c1 d)
d2H1 : forall d2 : ordinal_finType (m + n),
d != d2 -> c d2 = c1 d2
d2H2 : on_top d c
d2H3 : on_top d c1
44b (size cs).+1 =
size
(if clshift c == clshift c1
then rm_rep (clshift c1) [seq clshift i | i <- cs]
else
clshift c1
:: rm_rep (clshift c1) [seq clshift i | i <- cs]) +
size
(if crshift c == crshift c1
then rm_rep (crshift c1) [seq crshift i | i <- cs]
else
crshift c1
:: rm_rep (crshift c1) [seq crshift i | i <- cs])
case : (tsplitP d) => [j dE | k dE].5 6 7 8 f1 448 441 46d 10a 167 46e 46f 470 471 44b 16d 2ca
472
rewrite ifT; last first .476 clshift c == clshift c1
apply /eqP/ffunP=> i; rewrite !ffunE.5 6 7 8 f1 448 441 46d 10a 167 46e 46f 470 471 44b 16d 2ca fb
c (tlshift n i) = c1 (tlshift n i)
47f
apply : d2H1; apply /eqP => /val_eqP /=.5 6 7 8 f1 448 441 46d 10a 167 46e 470 471 44b 16d 2ca fb
d == i + n -> False
47f
by rewrite dE eqn_leq andbC leqNgt (leq_trans (ltn_ord _)) ?leq_addl .
rewrite ifN /=; last first .476 crshift c != crshift c1
apply /eqP => /ffunP /(_ j); rewrite !ffunE => cE.5 6 7 8 f1 448 441 46d 10a 167 46e 46f 470 471 44b 16d 2ca cE : c (trshift m j) = c1 (trshift m j)
False
493
move : d2H; rewrite (_ : c d = c1 d) ?(irH) //.5 6 7 8 f1 448 441 46d 10a 167 46f 470 471 44b 16d 2ca 49a
c d = c1 d
493
by rewrite (_ : d = (trshift m j)) //=; apply /val_eqP/eqP.
rewrite addnS; congr _.+1 .476 size cs =
size (rm_rep (clshift c1) [seq clshift i | i <- cs]) +
size (rm_rep (crshift c1) [seq crshift i | i <- cs])
477
by apply : IH.
rewrite ifN /=; last first .479 clshift c != clshift c1
apply /eqP => /ffunP /(_ k); rewrite !ffunE => cE.5 6 7 8 f1 448 441 46d 10a 167 46e 46f 470 471 44b 173 47a cE : c (tlshift n k) = c1 (tlshift n k)
49b 4af
move : d2H; rewrite (_ : c d = c1 d) ?(irH) //.5 6 7 8 f1 448 441 46d 10a 167 46f 470 471 44b 173 47a 4b6
4a0 4af
by rewrite (_ : d = (tlshift n k)) //=; apply /val_eqP/eqP.
rewrite ifT; last first .479 crshift c == crshift c1
apply /eqP/ffunP=> i; rewrite !ffunE.5 6 7 8 f1 448 441 46d 10a 167 46e 46f 470 471 44b 173 47a 359
c (trshift m i) = c1 (trshift m i)
4c2
apply : d2H1; apply /eqP => /val_eqP /=.5 6 7 8 f1 448 441 46d 10a 167 46e 470 471 44b 173 47a 359
d == i -> False
4c2
by rewrite dE eqn_leq leqNgt (leq_trans (ltn_ord _)) ?leq_addl .
congr _.+1 .479 size cs =
(fix add (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| p.+1 => (add p m).+1
end )
(size
(rm_rep (clshift c1) [seq clshift i | i <- cs]))
(size
(rm_rep (crshift c1) [seq crshift i | i <- cs]))
by apply : IH.
Qed .
Lemma gdist_clshift n m (c1 c2 : configuration (m + n)) :
connect move c1 c2 ->
`d[clshift c1, clshift c2]_move <= `d[c1, c2]_move.connect move c1 c2 ->
`d[clshift c1, clshift c2]_move <= `d[c1, c2]_move
Proof .4d7
move => /gpath_connect[p pH].5 6 7 8 4da 2db p : seq
(finfun_finType (ordinal_finType (m + n))
(ordinal_finType q))
pH : gpath move c1 c2 p
`d[clshift c1, clshift c2]_move <= `d[c1, c2]_move
have := size_rm_rep (clshift c1) [seq (clshift i) | i <- p].4e0 size (rm_rep (clshift c1) [seq clshift i | i <- p]) <=
size [seq clshift i | i <- p] ->
`d[clshift c1, clshift c2]_move <= `d[c1, c2]_move
rewrite (gpath_dist pH) size_map; move /(leq_trans _); apply .4e0 `d[clshift c1, clshift c2]_move <=
size (rm_rep (clshift c1) [seq clshift i | i <- p])
apply : gdist_path_le; first by apply /path_clshift/(gpath_path pH).4e0 last (clshift c1)
(rm_rep (clshift c1) [seq clshift i | i <- p]) =
clshift c2
by rewrite last_rm_rep last_map (gpath_last pH).
Qed .
Lemma gdist_crshift n m (c1 c2 : configuration (m + n)) :
connect move c1 c2 ->
`d[crshift c1, crshift c2]_move <= `d[c1, c2]_move.4d9 connect move c1 c2 ->
`d[crshift c1, crshift c2]_move <= `d[c1, c2]_move
Proof .4f1
move => /gpath_connect[p pH].4e0 `d[crshift c1, crshift c2]_move <= `d[c1, c2]_move
have := size_rm_rep (crshift c1) [seq (crshift i) | i <- p].4e0 size (rm_rep (crshift c1) [seq crshift i | i <- p]) <=
size [seq crshift i | i <- p] ->
`d[crshift c1, crshift c2]_move <= `d[c1, c2]_move
rewrite (gpath_dist pH) size_map; move /(leq_trans _); apply .4e0 `d[crshift c1, crshift c2]_move <=
size (rm_rep (crshift c1) [seq crshift i | i <- p])
apply : gdist_path_le; first by apply /path_crshift/(gpath_path pH).4e0 last (crshift c1)
(rm_rep (crshift c1) [seq crshift i | i <- p]) =
crshift c2
by rewrite last_rm_rep last_map (gpath_last pH).
Qed .
Lemma gdist_cshift n m (c1 c2 : configuration (m + n)) :
connect move c1 c2 ->
`d[clshift c1, clshift c2]_move + `d[crshift c1, crshift c2]_move
<= `d[c1, c2]_move.4d9 connect move c1 c2 ->
`d[clshift c1, clshift c2]_move +
`d[crshift c1, crshift c2]_move <= `d[c1, c2]_move
Proof .506
move => /gpath_connect[p pH].4e0 `d[clshift c1, clshift c2]_move +
`d[crshift c1, crshift c2]_move <= `d[c1, c2]_move
rewrite (gpath_dist pH) (path_shift (gpath_path pH)).4e0 `d[clshift c1, clshift c2]_move +
`d[crshift c1, crshift c2]_move <=
size (rm_rep (clshift c1) [seq clshift i | i <- p]) +
size (rm_rep (crshift c1) [seq crshift i | i <- p])
apply : leq_add.
apply : gdist_path_le; first by apply /path_clshift/(gpath_path pH).
by rewrite last_rm_rep last_map (gpath_last pH).4fe
apply : gdist_path_le; first by apply /path_crshift/(gpath_path pH).501
by rewrite last_rm_rep last_map (gpath_last pH).
Qed .
Definition cliftrn m n p (c : configuration n) : configuration (m + n) :=
cmerge `c[p] c.
Definition cliftr n : _ -> _ -> configuration n.+1 := @cliftrn 1 n.
Notation " ↑[ c ]_ p" := (cliftr p c) (at level 5 , format "↑[ c ]_ p" ).
Definition cliftln m n p (c : configuration m) : configuration (m + n) :=
cmerge c `c[p].
Definition cliftl n c p : configuration (n + 1 ) := (@cliftln n 1 c p).
Lemma cliftr_ldisk n p (c : configuration n) : ↑[c]_p ldisk = p.
Proof .51a
rewrite ffunE; case : tsplitP => /= [j nE|t].
by have := ltn_ord j; rewrite {2 }nE ltnn.
by rewrite ffunE.
Qed .
Lemma on_top_liftrn n m p x (c : configuration n) :
on_top (trshift m x) (cliftrn m p c) = on_top x c.5 6 7 8 4da 51d 149 1d
on_top (trshift m x) (cliftrn m p c) = on_top x c
Proof .52f
exact : on_top_merger. Qed .
Lemma move_liftrn n m p (c1 c2 : configuration n) :
move (cliftrn m p c1) (cliftrn m p c2) = move c1 c2.5 6 7 8 4da 51d 34
move (cliftrn m p c1) (cliftrn m p c2) = move c1 c2
Proof .535
exact : move_merger. Qed .
Lemma path_liftrn n m p (c : configuration n) (cs : seq (configuration _)) :
path move (cliftrn m p c) (map (cliftrn m p) cs) =
path move c cs.5 6 7 8 4da 51d 1d 1e3
path move (cliftrn m p c)
[seq cliftrn m p i | i <- cs] = path move c cs
Proof .53b
exact : path_merger. Qed .
Lemma connect_liftrn n m p (c1 c2 : configuration n) :
connect move c1 c2 -> connect move (cliftrn m p c1) (cliftrn m p c2).537 connect move c1 c2 ->
connect move (cliftrn m p c1) (cliftrn m p c2)
Proof .541
exact : connect_merger. Qed .
Lemma gdist_liftrn n m p (c1 c2 : configuration n) :
connect move c1 c2 ->
`d[cliftrn m p c1, cliftrn m p c2]_move <= `d[c1, c2]_move.537 connect move c1 c2 ->
`d[cliftrn m p c1, cliftrn m p c2]_move <=
`d[c1, c2]_move
Proof .546
exact : gdist_merger. Qed .
Lemma move_liftr n p (c1 c2 : configuration n) :
move ↑[c1]_p ↑[c2]_p = move c1 c2.5 6 7 8 1b 51d 34
move ↑[c1]_p ↑[c2]_p = move c1 c2
Proof .54b
by exact : move_liftrn 1 p c1 c2. Qed .
Lemma perfect_liftr n p : ↑[`c[p]]_p = `c[p] :> configuration n.+1 .5 6 7 8 1b 51d
↑[`c[p]]_p = `c[p]
Proof .551
apply /ffunP => i; rewrite !ffunE.5 6 7 8 1b 51d i : ordinal_finType n.+1
match tsplit i with
| inl j => `c[p] j
| inr j => `c[p] j
end = p
by case : tsplitP => [j|k]; rewrite !ffunE.
Qed .
Definition cunliftr {n } (c : configuration n.+1 ) : configuration n :=
@crshift 1 n c.
Notation " ↓[ c ]" := (cunliftr c) (at level 5 , format "↓[ c ]" ).
Lemma cliftrK n p : cancel (cliftr p) (cunliftr : _ -> configuration n).553 cancel (cliftr p)
(cunliftr : configuration n.+1 -> configuration n)
Proof .55d
by move => c; apply /ffunP => i; rewrite !ffunE tsplit_trshift. Qed .
Lemma cunliftrK n (c : configuration n.+1 ) : ↑[↓[c]]_(c ldisk) = c.5 6 7 8 1b c : configuration n.+1
↑[↓[c]]_(c ldisk) = c
Proof .562
apply /ffunP => i; rewrite !ffunE.5 6 7 8 1b 565 55a
match tsplit i with
| inl j => `c[c ldisk] j
| inr j => ↓[c] j
end = c i
case : tsplitP => [] j iE; rewrite !ffunE; congr fun_of_fin;
apply /val_eqP/eqP => //=.5 6 7 8 1b 565 55a j : 'I_1
iE : i = j + n
n = i
by rewrite iE; case : (j) => [] [].
Qed .
Lemma cliftr_inj n p : injective (@cliftr n p).
Proof .575
by move => c1 c2 c1Ec2; rewrite -[c1](cliftrK p) c1Ec2 cliftrK. Qed .
Lemma map_eqr (T1 T2 : eqType) (f : T1 -> T2) (s1 s2 : seq T1) :
injective f ->
([seq f i | i <- s1] == [seq f i | i <- s2]) = (s1 == s2).5 6 7 8 T1, T2 : eqType
f : T1 -> T2
s1, s2 : seq T1
injective f ->
([seq f i | i <- s1] == [seq f i | i <- s2]) =
(s1 == s2)
Proof .57a
elim : s1 s2 => [[|] //|a s1 IH [|b s2]//=] fInj.5 6 7 8 57d 57e a : T1
s1 : seq T1
IH : forall s2 : seq T1,
injective f ->
([seq f i | i <- s1] == [seq f i | i <- s2]) =
(s1 == s2)
b : T1
s2 : seq T1
fInj : injective f
(f a :: [seq f i | i <- s1] ==
f b :: [seq f i | i <- s2]) = (a :: s1 == b :: s2)
rewrite !eqseq_cons IH //.585 (f a == f b) && (s1 == s2) = (a == b) && (s1 == s2)
case : (a =P b) => [->//|]; first by rewrite eqxx.585 a <> b ->
(f a == f b) && (s1 == s2) = false && (s1 == s2)
by case : (f a =P f b) => [/fInj|//].
Qed .
Lemma eq_map_liftr n p (cs1 cs2 : seq (configuration n)) :
([seq ↑[i]_p | i <- cs1] == [seq ↑[i]_p | i <- cs2]) = (cs1 == cs2).5 6 7 8 1b 51d cs1, cs2 : seq (configuration n)
([seq ↑[i]_p | i <- cs1] == [seq ↑[i]_p | i <- cs2]) =
(cs1 == cs2)
Proof .596
by apply /map_eqr/cliftr_inj. Qed .
Lemma perfect_unliftr n p : ↓[`c[p]] = `c[p] :> configuration n.
Proof .59d
by apply /ffunP => i; rewrite !ffunE. Qed .
Lemma s2f_liftr n (c : configuration n.+1 ) (p : peg) :
s2f ([set i | c i == p] :\ ord_max) = s2f [set i | cunliftr c i == p].5 6 7 8 1b 565 51d
s2f ([set i | c i == p] :\ ord_max) =
s2f [set i | ↓[c] i == p]
Proof .5a2
apply /fsetP=> i.5 6 7 8 1b 565 51d i : nat_choiceType
(i \in s2f ([set i | c i == p] :\ ord_max)) =
(i \in s2f [set i | ↓[c] i == p])
apply /imfsetP/imfsetP => [] [/= j].j \in [set i | c i == p] :\ ord_max ->
i = j ->
exists2 x : 'I_n, x \in [set i | ↓[c] i == p] & i = x
rewrite !inE => /andP[jDn /eqP cjEp] jEi.5 6 7 8 1b 565 51d 5ab 5b1 jDn : j != ord_max
cjEp : c j = p
jEi : i = j
exists2 x : 'I_n, x \in [set i | ↓[c] i == p] & i = x
5b3
have jLn : j < n.
rewrite -val_eqE /= in jDn.5 6 7 8 1b 565 51d 5ab 5b1 5bc 5bd jDn : j != n
5c2 5c3
by have := ltn_ord j; rewrite ltnS leq_eqVlt (negPf jDn).
exists (Ordinal jLn ) => //=; rewrite !inE ffunE; apply /eqP.5c5 c (trshift 1 (Ordinal jLn)) = p
5b3
by rewrite -cjEp; congr (c _); apply : val_eqP.
rewrite inE ffunE => /eqP cjEp iEj; exists (trshift 1 j ) => //.5 6 7 8 1b 565 51d 5ab 16d cjEp : c (trshift 1 j) = p
iEj : i = j
trshift 1 j \in [set i | c i == p] :\ ord_max
by rewrite !inE cjEp -val_eqE //= neq_ltn ltn_ord /=.
Qed .
Lemma codom_liftr n (c : configuration n.+1 ) (s : seq peg) :
codom c \subset s -> codom ↓[c] \subset s.codom c \subset s -> codom ↓[c] \subset s
Proof .5de
move => H; apply /subsetP => i /mapP[j _ ->].5 6 7 8 1b 565 5e1 H : codom c \subset s
i : ordinal_finType q
fc ↓[c] j \in s
by rewrite ffunE; apply : (subsetP H); apply : codom_f.
Qed .
Lemma move_ldisk n (c1 c2 : configuration n.+1 ) :
move c1 c2 -> c1 ldisk != c2 ldisk -> ↓[c1] = ↓[c2].5 6 7 8 1b c1, c2 : configuration n.+1
move c1 c2 -> c1 ldisk != c2 ldisk -> ↓[c1] = ↓[c2]
Proof .5ec
move => c1Mc2 c10Dc20.5 6 7 8 1b 5ef ad c10Dc20 : c1 ldisk != c2 ldisk
↓[c1] = ↓[c2]
apply /ffunP=> i; rewrite !ffunE /=.5 6 7 8 1b 5ef ad 5f6 359
c1 (trshift 1 i) = c2 (trshift 1 i)
apply : move_disk1 c1Mc2 c10Dc20 _.5 6 7 8 1b 5ef 359
ldisk != trshift 1 i
apply /eqP/val_eqP => /=.
by rewrite eqn_leq negb_and -ltnNge ltn_ord.
Qed .
Lemma move_unliftr n (c1 c2 : configuration n.+1 ) :
c1 ldisk = c2 ldisk -> move ↓[c1] ↓[c2] = move c1 c2.5ee c1 ldisk = c2 ldisk -> move ↓[c1] ↓[c2] = move c1 c2
Proof .607
by move => c1lEc2l; rewrite -(@move_liftr _ (c1 ldisk)) {2 }c1lEc2l !cunliftrK.
Qed .
Lemma path_move_rev (n : nat) (c : configuration n) cs :
path move (last c cs) (rev (belast c cs)) = path move c cs.5 6 7 8 1b 1d 1e3
path move (last c cs) (rev (belast c cs)) =
path move c cs
Proof .60c
by rewrite rev_path; apply : eq_path => c1 c2; exact : move_sym.
Qed .
Lemma path_liftr n p (c : configuration n) (cs : seq (configuration _)) :
path move ↑[c]_p [seq ↑[i]_p | i <- cs] = path move c cs.5 6 7 8 1b 51d 1d 1e3
path move ↑[c]_p [seq ↑[i]_p | i <- cs] =
path move c cs
Proof .612
by apply : (@path_merger 1 ). Qed .
Lemma connect_liftr n p (c1 c2 : configuration n) :
connect move c1 c2 -> connect move ↑[c1]_p ↑[c2]_p.54d connect move c1 c2 -> connect move ↑[c1]_p ↑[c2]_p
Proof .618
by apply : (@connect_merger 1 ). Qed .
Lemma gdist_liftr n p (c1 c2 : configuration n) :
connect move c1 c2 -> `d[↑[c1]_p, ↑[c2]_p]_move <= `d[c1, c2]_move .54d connect move c1 c2 ->
`d[↑[c1]_p, ↑[c2]_p]_move <= `d[c1, c2]_move
Proof .61d
by apply : (@gdist_merger 1 ). Qed .
Lemma path_unlift_eq n (c : configuration n.+1 ) (cs : seq (configuration _)) :
(forall c1 , c1 \in cs -> c1 ldisk = c ldisk)->
path move ↓[c] [seq ↓[i] | i <- cs] = path move c cs.5 6 7 8 1b 565 cs : seq (configuration n.+1 )
(forall
c1 : finfun_eqType (ordinal_finType n.+1 )
(ordinal_eqType q),
c1 \in cs -> c1 ldisk = c ldisk) ->
path move ↓[c] [seq ↓[i] | i <- cs] = path move c cs
Proof .622
move => H.5 6 7 8 1b 565 625 H : forall
c1 : finfun_eqType (ordinal_finType n.+1 )
(ordinal_eqType q),
c1 \in cs -> c1 ldisk = c ldisk
path move ↓[c] [seq ↓[i] | i <- cs] = path move c cs
rewrite -(@path_liftr _ (c ldisk)).62b path move ↑[↓[c]]_(c ldisk)
[seq ↑[i]_(c ldisk) | i <- [seq ↓[i] | i <- cs]] =
path move c cs
rewrite cunliftrK -map_comp.62b path move c
[seq ([eta cliftr (c ldisk)] \o [eta cunliftr]) i
| i <- cs] = path move c cs
congr path.62b [seq ([eta cliftr (c ldisk)] \o [eta cunliftr]) i
| i <- cs] = cs
elim : cs H => //= a cs IH H.5 6 7 8 1b c, a : configuration n.+1
625 IH : (forall c1 : {ffun 'I_n.+1 -> 'I_q},
c1 \in cs -> c1 ldisk = c ldisk) ->
[seq ([eta cliftr (c ldisk)] \o [eta cunliftr]) i
| i <- cs] = cs
H : forall c1 : {ffun 'I_n.+1 -> 'I_q},
c1 \in a :: cs -> c1 ldisk = c ldisk
↑[↓[a]]_(c ldisk)
:: [seq ([eta cliftr (c ldisk)] \o [eta cunliftr]) i
| i <- cs] = a :: cs
rewrite -{1 }(H a).63d ↑[↓[a]]_(a ldisk)
:: [seq ([eta cliftr (c ldisk)] \o [eta cunliftr]) i
| i <- cs] = a :: cs
by rewrite cunliftrK IH // => v Hv; apply : H; rewrite inE orbC Hv.
by rewrite inE eqxx.
Qed .
Lemma path_unlift n (c : configuration n.+1 ) (cs : seq (configuration _)) :
path move c cs ->
path move ↓[c] (rm_rep ↓[c] [seq ↓[i] | i <- cs]).624 path move c cs ->
path move ↓[c] (rm_rep ↓[c] [seq ↓[i] | i <- cs])
Proof .64d
by move => H; apply : path_crshift. Qed .
Lemma gdist_cunlift n (c1 c2 : configuration n.+1 ) :
connect move c1 c2 -> `d[↓[c1], ↓[c2]]_move <= `d[c1, c2]_move.5ee connect move c1 c2 ->
`d[↓[c1], ↓[c2]]_move <= `d[c1, c2]_move
Proof .652
by move => H; apply : gdist_crshift. Qed .
Lemma gdist_cunlift_eq n (c1 c2 : configuration n.+1 ) :
irreflexive r ->
connect move c1 c2 -> c1 ldisk = c2 ldisk ->
`d[c1, c2]_move = `d[↓[c1], ↓[c2]]_move.5ee irreflexive r ->
connect move c1 c2 ->
c1 ldisk = c2 ldisk ->
`d[c1, c2]_move = `d[↓[c1], ↓[c2]]_move
Proof .657
move => ir c1Cc2 c1Ec2; apply /eqP; rewrite eqn_leq gdist_cunlift // andbT.5 6 7 8 1b 5ef ir : irreflexive r
c1Cc2 : connect move c1 c2
c1Ec2 : c1 ldisk = c2 ldisk
`d[c1, c2]_move <= `d[↓[c1], ↓[c2]]_move
rewrite -{1 }[c1]cunliftrK -{1 }[c2]cunliftrK -c1Ec2.65e `d[↑[↓[c1]]_(c1 ldisk), ↑[↓[c2]]_(c1 ldisk)]_move <=
`d[↓[c1], ↓[c2]]_move
apply : gdist_liftr => //.65e connect move ↓[c1] ↓[c2]
case /connectP: c1Cc2 => p pH c2E.5 6 7 8 1b 5ef 65f 661 p : seq
(finfun_finType (ordinal_finType n.+1 )
(ordinal_finType q))
pH : path move c1 p
c2E : c2 = last c1 p
66a
apply /connectP; exists (rm_rep (↓[c1]) ([seq ↓[i] | i <- p])) => //.66e path move ↓[c1] (rm_rep ↓[c1] [seq ↓[i] | i <- p])
by apply : path_unlift.
by rewrite last_rm_rep c2E last_map.
Qed .
Lemma perfect_liftrn m n p :
cliftrn m p (`c[p]) = `c[p] :> configuration (m + n).5 6 7 8 f1 51d
cliftrn m p `c[p] = `c[p]
Proof .67d
by apply /ffunP => i; rewrite !ffunE; case : tsplitP => j; rewrite !ffunE.
Qed .
(* case distinction that depends if the largest disk has move *)
(* if it has not moved, we get the path on the unlifted configuration *)
(* uf it has moved, we get the decomposition till the first move *)
Inductive pathS_spec (n : nat) (c : configuration n.+1 )
(cs : seq (configuration n.+1 )) :
forall (b : bool), Type
:=
pathS_specW :
forall (p := c ldisk) (c1 := ↓[c]) (cs1 := [seq ↓[i] | i <- cs]),
cs = [seq ↑[i]_p | i <- cs1] -> path move c1 cs1 -> pathS_spec c cs true |
pathS_spec_move :
forall (p1 := c ldisk) p2 cs1 cs2
(c1 := ↓[c])
(c2 := ↑[last c1 cs1]_p2),
p1 != p2 -> r p1 p2 ->
cs = [seq ↑[i]_p1 | i <- cs1] ++ c2 :: cs2 ->
path move c1 cs1 -> move ↑[last c1 cs1]_p1 c2 ->
path move c2 cs2 ->
pathS_spec c cs true |
pathS_spec_false : pathS_spec c cs false.
(* Inversion theorem on a path for disk n.+1 *)
Lemma pathSP n (c : configuration n.+1 ) cs : pathS_spec c cs (path move c cs).624 pathS_spec c cs (path move c cs)
Proof .683
have [Hp|_] := boolP (path _ _ _); last by apply : pathS_spec_false.5 6 7 8 1b 565 625 Hp : path move c cs
pathS_spec c cs true
pose f (c1 : configuration n.+1 ) := c1 ldisk != c ldisk.5 6 7 8 1b 565 625 68b f := fun c1 : configuration n.+1 => c1 ldisk != c ldisk: configuration n.+1 -> bool
68c
have [Hh|/hasPn Hn] := boolP (has f cs); last first .5 6 7 8 1b 565 625 68b 691 Hn : {in cs,
forall
x : finfun_eqType (ordinal_finType n.+1 )
(ordinal_eqType q),
~~ f x}
68c
have csE : cs = [seq ↑[i]_(c ldisk) | i <- [seq ↓[i] | i <- cs]].695 cs = [seq ↑[i]_(c ldisk) | i <- [seq ↓[i] | i <- cs]]
rewrite -map_comp -[LHS]map_id.695 [seq x | x <- cs] =
[seq ([eta cliftr (c ldisk)] \o [eta cunliftr]) i
| i <- cs]
69f
apply /eq_in_map => x /Hn; rewrite negbK => /eqP <-/=.5 6 7 8 1b 565 625 68b 691 696 x : finfun_eqType (ordinal_finType n.+1 )
(ordinal_eqType q)
x = ↑[↓[x]]_(x ldisk)
69f
by rewrite cunliftrK.
apply : pathS_specW csE _.695 path move ↓[c] [seq ↓[i] | i <- cs]
697
by rewrite path_unlift_eq // => c1 /Hn; rewrite negbK => /eqP.
pose n1 := find f cs; pose lc1 := nth c cs n1.5 6 7 8 1b 565 625 68b 691 69a n1 := find f cs : nat
lc1 := nth c cs n1 : configuration n.+1
68c
pose p1 := c ldisk; pose p2 := lc1 ldisk.5 6 7 8 1b 565 625 68b 691 69a 6bb 6bc p1 := c ldisk : (fun => peg) ldisk
p2 := lc1 ldisk : (fun => peg) ldisk
68c
have p1Dp2 : p1 != p2.
by have := nth_find c Hh; rewrite eq_sym.
pose c1 := ↓[c].5 6 7 8 1b 565 625 68b 691 69a 6bb 6bc 6c1 6c2 6ca c1 := ↓[c] : configuration n
68c
pose lcs1 := take n1 cs; pose cs2 := drop n1.+1 cs.5 6 7 8 1b 565 625 68b 691 69a 6bb 6bc 6c1 6c2 6ca 6d2 lcs1 := take n1 cs : seq (configuration n.+1 )
cs2 := drop n1.+1 cs : seq (configuration n.+1 )
68c
have slcs1 : size lcs1 = n1 by rewrite size_take -has_find Hh.5 6 7 8 1b 565 625 68b 691 69a 6bb 6bc 6c1 6c2 6ca 6d2 6d7 6d8 slcs1 : size lcs1 = n1
68c
have Plcs1 c2 : c2 \in lcs1 -> c2 ldisk = p1.5 6 7 8 1b 565 625 68b 691 69a 6bb 6bc 6c1 6c2 6ca 6d2 6d7 6d8 6dd c2 : finfun_eqType (ordinal_finType n.+1 )
(ordinal_eqType q)
c2 \in lcs1 -> c2 ldisk = p1
move => c2Ilcs1p; move : (c2Ilcs1p).5 6 7 8 1b 565 625 68b 691 69a 6bb 6bc 6c1 6c2 6ca 6d2 6d7 6d8 6dd 6e2 c2Ilcs1p : c2 \in lcs1
6e3 6e4
rewrite -index_mem slcs1 => /(before_find c) /idP /negP.6eb ~~ f (nth c cs (index c2 lcs1)) -> c2 ldisk = p1
6e4
rewrite negbK => /eqP.6eb nth c cs (index c2 lcs1) ldisk = c ldisk ->
c2 ldisk = p1
6e4
by rewrite -[cs](cat_take_drop n1) nth_cat index_mem c2Ilcs1p nth_index.
pose cs1 := map cunliftr lcs1.5 6 7 8 1b 565 625 68b 691 69a 6bb 6bc 6c1 6c2 6ca 6d2 6d7 6d8 6dd 6e7 cs1 := [seq ↓[i] | i <- lcs1] : seq (configuration n)
68c
have lcs1E : lcs1 = [seq ↑[i]_p1 | i <- cs1].6fb lcs1 = [seq ↑[i]_p1 | i <- cs1]
rewrite -map_comp -[LHS]map_id.6fb [seq x | x <- lcs1] =
[seq ([eta cliftr p1] \o cunliftr) i | i <- lcs1]
701
apply /eq_in_map => x /Plcs1 H.5 6 7 8 1b 565 625 68b 691 69a 6bb 6bc 6c1 6c2 6ca 6d2 6d7 6d8 6dd 6e7 6fc 6ab H : x ldisk = p1
x = ([eta cliftr p1] \o cunliftr) x
701
by rewrite /= -H cunliftrK.
have csE : cs = [seq ↑[i]_p1 | i <- cs1] ++ lc1 :: cs2.703 cs = [seq ↑[i]_p1 | i <- cs1] ++ lc1 :: cs2
by rewrite -[cs](cat_take_drop n1.+1 ) -cat_rcons -lcs1E
(take_nth c) // -has_find.
have Hm : move (last c lcs1) lc1.718 move (last c lcs1) lc1
by move : Hp; rewrite csE lcs1E cat_path /= => /and3P[].
have lc1E : lc1 = cliftr p2 (last c1 cs1).723 lc1 = ↑[last c1 cs1]_p2
rewrite /p2.723 lc1 = ↑[last c1 cs1]_(lc1 ldisk)
72c
have Hd : (last c lcs1) ldisk != lc1 ldisk.723 last c lcs1 ldisk != lc1 ldisk
case : (lcs1) Plcs1 => //= a l -> //.5 6 7 8 1b 565 625 68b 691 69a 6bb 6bc 6c1 6c2 6ca 6d2 6d7 6d8 6dd 6fc 704 719 724 a : configuration n.+1
l : seq (configuration n.+1 )
last a l \in a :: l
738
by apply : mem_last.
rewrite last_map -[LHS]cunliftrK.73a ↑[↓[lc1]]_(lc1 ldisk) = ↑[↓[last c lcs1]]_(lc1 ldisk)
72c
congr cliftr.73a ↓[lc1] = ↓[last c lcs1]
72c
apply /ffunP=> i; rewrite !ffunE /=.5 6 7 8 1b 565 625 68b 691 69a 6bb 6bc 6c1 6c2 6ca 6d2 6d7 6d8 6dd 6e7 6fc 704 719 724 73b 359
lc1 (trshift 1 i) = last c lcs1 (trshift 1 i)
72c
apply /sym_equal/(move_disk1 Hm Hd).
apply /eqP/val_eqP => /=.
by rewrite eqn_leq negb_and -ltnNge ltn_ord.
have Hm1 : move ↑[last c1 cs1]_p1 ↑[last c1 cs1]_p2.72e move ↑[last c1 cs1]_p1 ↑[last c1 cs1]_p2
have ->: ↑[last ↓[c] cs1]_p1 = last c lcs1.72e ↑[last ↓[c] cs1]_p1 = last c lcs1
by rewrite -[in LHS]last_map -lcs1E cunliftrK.
by rewrite -lc1E.
apply : pathS_spec_move (p1Dp2) _ _ _ (Hm1) _ => //.
- 772
have := @move_diskr _ ldisk _ _ Hm1.762 (↑[last c1 cs1]_p1 ldisk != ↑[last c1 cs1]_p2 ldisk ->
r (↑[last c1 cs1]_p1 ldisk) (↑[last c1 cs1]_p2 ldisk)) ->
r (c ldisk) p2
775
by rewrite !cliftr_ldisk; apply .
- 782
by rewrite csE lc1E lcs1E.
- 787
rewrite path_unlift_eq => //.
by move : Hp; rewrite -[cs](cat_take_drop n1) cat_path => /andP[].
rewrite -lc1E.
by move : Hp; rewrite csE cat_path /= => /and3P[].
Qed .
(* we can restrict a path from n.+1 to n by removing all the moves of the *)
(* largest disk *)
Lemma pathS_restrict n (c : configuration n.+1 ) cs :
path move c cs ->
{cs'|
[/\ path move ↓[c] cs',
last ↓[c] cs' = ↓[last c cs] &
size cs' <= size cs ?=
iff (cs == [seq ↑[i]_(c ldisk) | i <- cs'])]}.624 path move c cs ->
{cs' : seq (configuration n)
| [/\ path move ↓[c] cs', last ↓[c] cs' = ↓[last c cs]
& size cs' <= size cs
?= iff (cs ==
[seq ↑[i]_(c ldisk) | i <- cs'])]}
Proof .799
elim : cs c => /= [c _|c1 cs IH c /andP[cMc1 /IH[cs1 [c1Pcs1 lccs1Mlc1cs S]]]].564 {cs' : seq (configuration n)
| [/\ path move ↓[c] cs', last ↓[c] cs' = ↓[c]
& size cs' <= 0
?= iff ([::] ==
[seq ↑[i]_(c ldisk) | i <- cs'])]}
by exists [::]; split ; rewrite ?setd_id //; apply : leqif_refl; rewrite !eqxx.
have [/eqP c1dEcd|c1dDcd] := boolP (c ldisk == c1 ldisk).5 6 7 8 1b 7a4 625 7a5 565 44a 7a6 7a7 7a8 7a9 c1dEcd : c ldisk = c1 ldisk
7aa
exists (cunliftr c1 :: cs1); split => //=.7b1 move ↓[c] ↓[c1] && path move ↓[c1] cs1
by rewrite move_unliftr // cMc1.7b1 (size cs1).+1 <= (size cs).+1
?= iff (c1 :: cs ==
↑[↓[c1]]_(c ldisk)
:: [seq ↑[i]_(c ldisk)
| i <- cs1])
7b3
by rewrite eqseq_cons c1dEcd cunliftrK eqxx.
have -> : cunliftr c = cunliftr c1 by apply : move_ldisk.7b5 {cs' : seq (configuration n)
| [/\ path move ↓[c1] cs',
last ↓[c1] cs' = ↓[last c1 cs]
& size cs' <= (size cs).+1
?= iff (c1 :: cs ==
[seq ↑[i]_(c ldisk) | i <- cs'])]}
exists cs1 ; split => //=.7b5 size cs1 <= (size cs).+1
?= iff (c1 :: cs ==
[seq ↑[i]_(c ldisk) | i <- cs1])
apply /leqifP; case : eqP=> [H|/= _]; last by rewrite ltnS S.5 6 7 8 1b 7a4 625 7a5 565 44a 7a6 7a7 7a8 7a9 7b6 H : c1 :: cs = [seq ↑[i]_(c ldisk) | i <- cs1]
size cs1 == (size cs).+1
by rewrite -[_.+1 ]/(size (c1 :: cs)) H size_map.
Qed .
(* we can restrict a path from n.+1 to n *)
Lemma pathS_restrictD n (c : configuration n.+1 ) c1 cs :
path move c cs -> c1 \in cs -> c1 ldisk != c ldisk ->
{cs'| [/\ path move ↓[c] cs',
last ↓[c] cs' = ↓[last c cs] & size cs' < size cs]}.5 6 7 8 1b 565 c1 : finfun_eqType (ordinal_finType n.+1 )
(ordinal_eqType q)
625 path move c cs ->
c1 \in cs ->
c1 ldisk != c ldisk ->
{cs' : seq (configuration n)
| [/\ path move ↓[c] cs', last ↓[c] cs' = ↓[last c cs]
& size cs' < size cs]}
Proof .7d4
move => cPcs c1Ics c1dDcd.5 6 7 8 1b 565 7d7 625 cPcs : path move c cs
c1Ics : c1 \in cs
c1dDcd : c1 ldisk != c ldisk
{cs' : seq (configuration n)
| [/\ path move ↓[c] cs', last ↓[c] cs' = ↓[last c cs]
& size cs' < size cs]}
have [cs1 [H1 H2 H3]] := pathS_restrict cPcs.5 6 7 8 1b 565 7d7 625 7de 7df 7e0 7a6 H1 : path move ↓[c] cs1
H2 : last ↓[c] cs1 = ↓[last c cs]
H3 : size cs1 <= size cs
?= iff (cs ==
[seq ↑[i]_(c ldisk) | i <- cs1])
7e1
exists cs1 ; split => //.
move /leqifP : H3; case : eqP => // cs1Ecs.5 6 7 8 1b 565 7d7 625 7de 7df 7e0 7a6 7e6 7e7 cs1Ecs : cs = [seq ↑[i]_(c ldisk) | i <- cs1]
size cs1 == size cs -> size cs1 < size cs
case /eqP: c1dDcd.5 6 7 8 1b 565 7d7 625 7de 7df 7a6 7e6 7e7 7f1
c1 ldisk = c ldisk
move : c1Ics; rewrite cs1Ecs => /mapP[x xIcs1 ->].5 6 7 8 1b 565 7d7 625 7de 7a6 7e6 7e7 7f1 x : finfun_eqType (ordinal_finType n)
(ordinal_eqType q)
xIcs1 : x \in cs1
↑[x]_(c ldisk) ldisk = c ldisk
by rewrite cliftr_ldisk.
Qed .
(* connect is symmetric *)
(* there should be a shorter proof since move n is symmetric *)
Lemma connect_sym n : connect_sym (@move n).
Proof .800
move => c1 c2.5 6 7 8 1b c1, c2 : finfun_finType (ordinal_finType n)
(ordinal_finType q)
connect move c1 c2 = connect move c2 c1
apply /connectP/connectP=> [] [p H1 H2].5 6 7 8 1b 809 p : seq
(finfun_finType (ordinal_finType n)
(ordinal_finType q))
H1 : path move c1 p
H2 : c2 = last c1 p
exists2
p : seq
(finfun_finType (ordinal_finType n)
(ordinal_finType q)),
path move c2 p & c1 = last c2 p
exists (rev (belast c1 p)); first by rewrite H2 path_move_rev.80e c1 = last c2 (rev (belast c1 p))
813
by case : (p) H2 => [->//|c3 p1 _]; rewrite rev_cons last_rcons.
exists (rev (belast c2 p)); first by rewrite H2 path_move_rev.815 c2 = last c1 (rev (belast c2 p))
by case : (p) H2 => [->//|c3 p1 _]; rewrite rev_cons last_rcons.
Qed .
End GHanoi .
Arguments perfect {q n}.
Arguments cunliftr {q n}.
Notation " ↑[ c ]_ p" := (cliftr p c) (at level 5 , format "↑[ c ]_ p" ).
Notation " ↓[ c ]" := (cunliftr c) (at level 5 , format "↓[ c ]" ).
Notation "`c[ p ] " := (perfect p) (format "`c[ p ]" , at level 5 ).
Notation "`c[ p , n ] " := ((perfect p) : configuration _ n)
(format "`c[ p , n ]" , at level 5 ).
Lemma on_top1 k (d : disk 1 ) (c : configuration k 1 ) : on_top d c.k : nat
9 c : configuration k 1
on_top d c
Proof .825
by apply /on_topP=> [] [] [] //=; case : d => [] []. Qed .
Lemma perfect_eqE n k (p1 p2 : peg k) : (`c[p1, n.+1 ] == `c[p2]) = (p1 == p2).(`c[p1 , n.+1 ] == `c[p2]) = (p1 == p2)
Proof .82d
apply /eqP/eqP => [|<-] // cp1Ecp2.830 831 cp1Ecp2 : `c[p1] = `c[p2]
p1 = p2
rewrite -(_ : `c[p1, n.+1 ] sdisk = p1); last by rewrite ffunE.
by rewrite cp1Ecp2 ffunE.
Qed .
Section PLift .
Variables n q : nat.
Variables i : disk q.+1 .
Variable r1 : rel (disk q).
Variable r2 : rel (disk q.+1 ).
Let p := lift i.
Hypothesis r2Rr1 : forall i j , r2 (p i) (p j) = r1 i j.
Definition plift (c : configuration q n) : configuration q.+1 n :=
[ffun j => p (c j)].
Lemma plift_on_top c1 x : on_top x (plift c1) = on_top x c1.n, q : nat
i : disk q.+1
r1 : rel (disk q)
r2 : rel (disk q.+1 )
p := lift i : 'I_q.+1 .-1 -> 'I_q.+1
r2Rr1 : forall i j : 'I_q.+1 .-1 ,
r2 (p i) (p j) = r1 i j
c1 : configuration q n
x : disk n
on_top x (plift c1) = on_top x c1
Proof .83f
apply /on_topP/on_topP => H d; have := H d; rewrite !ffunE => H1 H2; apply : H1.842 843 844 845 846 847 848 849 H : forall d1 : ordinal_finType n,
plift c1 x = plift c1 d1 -> x <= d1
3b H2 : c1 x = c1 d
p (c1 x) = p (c1 d)
by rewrite H2.
by apply : lift_inj H2.
Qed .
Lemma plift_move (c1 c2 : configuration q n) :
move r2 (plift c1) (plift c2) = move r1 c1 c2.842 843 844 845 846 847 c1, c2 : configuration q n
move r2 (plift c1) (plift c2) = move r1 c1 c2
Proof .85d
apply /moveP/moveP => [] [x [H1x H2x H3x H4x]]; exists x ; split => //.842 843 844 845 846 847 860 x : ordinal_finType n
H1x : r2 (plift c1 x) (plift c2 x)
H2x : forall d2 : ordinal_finType n,
x != d2 -> plift c1 d2 = plift c2 d2
H3x : on_top x (plift c1)
H4x : on_top x (plift c2)
r1 (c1 x) (c2 x)
- 864
by rewrite !ffunE in H1x; rewrite -r2Rr1.
- 881
by move => d2 xDd2; have := H2x _ xDd2; rewrite !ffunE => /lift_inj.
- 886
by rewrite plift_on_top in H3x.
- 88b
by rewrite plift_on_top in H4x.
- 890
by rewrite !ffunE r2Rr1.
- 895
by move => d2 /H2x; rewrite !ffunE => ->.
- 89a
by rewrite plift_on_top.
by rewrite plift_on_top.
Qed .
Lemma plift_path (c1 : configuration q n) cs :
path (move r2) (plift c1) [seq plift i | i <- cs] =
path (move r1) c1 cs.842 843 844 845 846 847 848 cs : seq (configuration q n)
path (move r2) (plift c1) [seq plift i | i <- cs] =
path (move r1) c1 cs
Proof .8a2
elim : cs c1 => //= c2 cs IH c1.842 843 844 845 846 847 c2 : configuration q n
8a5 IH : forall c1 : configuration q n,
path (move r2) (plift c1) [seq plift i | i <- cs] =
path (move r1) c1 cs
848 move r2 (plift c1) (plift c2) &&
path (move r2) (plift c2) [seq plift i | i <- cs] =
move r1 c1 c2 && path (move r1) c2 cs
by rewrite plift_move IH.
Qed .
Lemma gdist_plift (c1 c2 : configuration q n) :
connect (move r1) c1 c2 ->
`d[plift c1, plift c2]_(move r2) <= `d[c1, c2]_(move r1).85f connect (move r1) c1 c2 ->
`d[plift c1, plift c2]_(move r2) <=
`d[c1, c2]_(move r1)
Proof .8b0
move => /gpath_connect [p1 p1H].842 843 844 845 846 847 860 202 p1H : gpath (move r1) c1 c2 p1
`d[plift c1, plift c2]_(move r2) <=
`d[c1, c2]_(move r1)
rewrite (gpath_dist p1H) -(size_map plift).8b7 `d[plift c1, plift c2]_(move r2) <=
size [seq plift i | i <- p1]
apply : gdist_path_le; first by rewrite plift_path (gpath_path p1H).8b7 last (plift c1) [seq plift i | i <- p1] = plift c2
by rewrite last_map (gpath_last p1H).
Qed .
Lemma plift_perfect p1 : plift `c[p1] = `c[lift i p1].842 843 844 845 846 847 p1 : peg q
plift `c[p1] = `c[lift i p1]
Proof .8c3
by apply /ffunP => j; rewrite !ffunE. Qed .
Lemma cdisjoint_plift_perfect m c : cdisjoint (plift c) `c[i, m].842 843 844 845 846 847 m : nat
c : configuration q n
cdisjoint (plift c) `c[i , m]
Proof .8ca
apply /cdisjointP=> i1 j1; rewrite !ffunE /p; apply /eqP/val_eqP => /=.842 843 844 845 846 847 8cd 8ce i1 : ordinal_finType n
j1 : ordinal_finType m
bump i (c i1) != i
by rewrite eq_sym neq_bump.
Qed .
End PLift .
Section Crlift .
Variable q : nat.
Variable p : peg q.+1 .
Variable r1 : rel (disk q).
Variable r2 : rel (disk q.+1 ).
Hypothesis r2Irr : irreflexive r2.
Hypothesis r1Rr2 : forall i j : disk q, r1 i j = r2 (lift p i) (lift p j).
Lemma move_liftln m n (c1 c2 : configuration q m) :
move r2 (cliftln n p (plift p c1)) (cliftln n p (plift p c2)) =
move r1 c1 c2.5 p : peg q.+1
844 845 r2Irr : irreflexive r2
r1Rr2 : forall i j : disk q,
r1 i j = r2 (lift p i) (lift p j)
f1 c1, c2 : configuration q m
move r2 (cliftln n p (plift p c1))
(cliftln n p (plift p c2)) = move r1 c1 c2
Proof .8d9
apply /idP/idP=> H; last first .5 8dc 844 845 8dd 8de f1 8df H : move r1 c1 c2
move r2 (cliftln n p (plift p c1))
(cliftln n p (plift p c2))
apply : move_mergel_inv => //.8e5 cdisjoint (plift p c1) `c[p]
- 8ee
by apply : cdisjoint_plift_perfect.
- 8f8
by apply : cdisjoint_plift_perfect.
by rewrite (@plift_move _ _ _ r1).
have := move_mergel r2Irr H.8ea move r2 (plift p c1) (plift p c2) -> move r1 c1 c2
by rewrite (@plift_move _ _ _ r1).
Qed .
Lemma path_liftln m n (c : configuration q m) (cs : seq (configuration _ _)) :
path (move r2) (cliftln n p (plift p c)) (map (cliftln n p \o (plift p)) cs) =
path (move r1) c cs.5 8dc 844 845 8dd 8de f1 c : configuration q m
cs : seq (configuration q m)
path (move r2) (cliftln n p (plift p c))
[seq (cliftln n p \o plift p) i | i <- cs] =
path (move r1) c cs
Proof .907
by elim : cs c => //= c1 cs1 IH c; rewrite move_liftln IH. Qed .
Lemma connect_liftln m n (c1 c2 : configuration q m) :
connect (move r1) c1 c2 ->
connect (move r2) (cliftln n p (plift p c1))
(cliftln n p (plift p c2)).8db connect (move r1) c1 c2 ->
connect (move r2) (cliftln n p (plift p c1))
(cliftln n p (plift p c2))
Proof .90f
move => /connectP[x]; rewrite -(path_liftln n) => Hp Hl.5 8dc 844 845 8dd 8de f1 8df x : seq
(finfun_finType (ordinal_finType m)
(ordinal_finType q))
Hp : path (move r2) (cliftln n p (plift p c1))
[seq (cliftln n p \o plift p) i | i <- x]
1f3 connect (move r2) (cliftln n p (plift p c1))
(cliftln n p (plift p c2))
apply /connectP; eexists ; first exact : Hp.916 cliftln n p (plift p c2) =
last (cliftln n p (plift p c1))
[seq (cliftln n p \o plift p) i | i <- x]
by rewrite Hl [RHS]last_map.
Qed .
Lemma gdist_liftln m n (c1 c2 : configuration q m) :
connect (move r1) c1 c2 ->
gdist (move r2) (cliftln n p (plift p c1)) (cliftln n p (plift p c2)) <=
gdist (move r1) c1 c2.8db connect (move r1) c1 c2 ->
`d[cliftln n p (plift p c1), cliftln n p (plift p c2)]_
(move r2) <= `d[c1, c2]_(move r1)
Proof .91f
move => /gpath_connect[p1 p1H].5 8dc 844 845 8dd 8de f1 8df p1 : seq
(finfun_finType (ordinal_finType m)
(ordinal_finType q))
8b8 `d[cliftln n p (plift p c1), cliftln n p (plift p c2)]_
(move r2) <= `d[c1, c2]_(move r1)
rewrite (gpath_dist p1H) -(size_map (cliftln n p \o plift p)).926 `d[cliftln n p (plift p c1), cliftln n p (plift p c2)]_
(move r2) <=
size [seq (cliftln n p \o plift p) i | i <- p1]
apply : gdist_path_le; first by rewrite path_liftln (gpath_path p1H).926 last (cliftln n p (plift p c1))
[seq (cliftln n p \o plift p) i | i <- p1] =
cliftln n p (plift p c2)
by rewrite [LHS]last_map (gpath_last p1H).
Qed .
Lemma crliftn_perfect n m p1 : cliftln n p `c[p1] = cliftrn m p1 `c[p].5 8dc 844 845 8dd 8de 4da p1 : peg q.+1
cliftln n p `c[p1] = cliftrn m p1 `c[p]
Proof .932
by []. Qed .
End Crlift .
(******************************************************************************)
(* Other peg *)
(******************************************************************************)
Definition opeg n (p1 p2 : peg n) :=
odflt (if p1 <= p2 then p1 else p2) [pick i | (i != p1) && (i != p2)].
Lemma opeg_sym n (p1 p2 : peg n) : opeg p1 p2 = opeg p2 p1.
Proof .939
rewrite /opeg; case : ltngtP => H;
try by congr odflt; apply : eq_pick => p; rewrite andbC.odflt p1 [pick i | i != p1 & i != p2] =
odflt p2 [pick i | i != p2 & i != p1]
suff -> : p1 = p2 by [].
by apply /val_eqP/eqP.
Qed .
Lemma opegDl n (p1 p2 : peg n.+3 ) : opeg p1 p2 != p1.
Proof .949
rewrite /opeg; case : pickP => [x /andP[]//| HD].1b 94c HD : (fun i : ordinal_finType n.+3 =>
(i != p1) && (i != p2)) =1 xpred0
odflt (if p1 <= p2 then p1 else p2) None != p1
have D (p3 p4 : peg n.+3 ) : (p3 == p4) = (val p3 == val p4).(p3 == p4) = (val p3 == val p4)
by apply /eqP/idP => /val_eqP.
have := HD sdisk; have := HD (inord 1 ); have := HD (inord 2 ).95d (inord 2 != p1) && (inord 2 != p2) = false ->
(inord 1 != p1) && (inord 1 != p2) = false ->
(sdisk != p1) && (sdisk != p2) = false ->
odflt (if p1 <= p2 then p1 else p2) None != p1
rewrite !D /= !inordK //.95d (2 != p1) && (2 != p2) = false ->
(1 != p1) && (1 != p2) = false ->
(0 != p1) && (0 != p2) = false ->
(if p1 <= p2 then p1 else p2) != p1
by case : {HD}p1 => [] [|[|[|p1 Hp1]]] /=;
case : p2 => [] [|[|[|p2 Hp2]]].
Qed .
Lemma opegDr n (p1 p2 : peg n.+3 ) : opeg p1 p2 != p2.
Proof .96b
rewrite /opeg; case : pickP => [x /andP[]//| HD].952 odflt (if p1 <= p2 then p1 else p2) None != p2
have D (p3 p4 : peg n.+3 ) : (p3 == p4) = (val p3 == val p4).
by apply /eqP/idP => /val_eqP.
have := HD sdisk; have := HD (inord 1 ); have := HD (inord 2 ).95d (inord 2 != p1) && (inord 2 != p2) = false ->
(inord 1 != p1) && (inord 1 != p2) = false ->
(sdisk != p1) && (sdisk != p2) = false ->
odflt (if p1 <= p2 then p1 else p2) None != p2
rewrite !D /= !inordK //.95d (2 != p1) && (2 != p2) = false ->
(1 != p1) && (1 != p2) = false ->
(0 != p1) && (0 != p2) = false ->
(if p1 <= p2 then p1 else p2) != p2
by case : {HD}p1 => [] [|[|[|p1 Hp1]]] /=;
case : p2 => [] [|[|[|p2 Hp2]]].
Qed .
Notation "`p[ p1 , p2 ] " := (opeg p1 p2)
(format "`p[ p1 , p2 ]" , at level 5 ).
Lemma move_liftr_perfect q n (hrel : rel (peg q)) p1 p2 p3 :
hrel p1 p2 -> p1 != p3 -> p2 != p3 -> move hrel ↑[`c[p3, n]]_p1 ↑[`c[p3]]_p2.q, n : nat
hrel : rel (peg q)
p1, p2 : peg q
p3 : ordinal_eqType q
hrel p1 p2 ->
p1 != p3 ->
p2 != p3 -> move hrel ↑[`c[p3 , n]]_p1 ↑[`c[p3]]_p2
Proof .983
move => p1Rp2 p1Dp3 p2Dp3.986 987 988 989 p1Rp2 : hrel p1 p2
p1Dp3 : p1 != p3
p2Dp3 : p2 != p3
move hrel ↑[`c[p3 , n]]_p1 ↑[`c[p3]]_p2
apply : (@move_mergel_inv _ _ 1 ).98f cdisjoint `c[p1] `c[p3]
- 995
by apply /cdisjointP => i j; rewrite !ffunE.
- 99f
by apply /cdisjointP => i j; rewrite !ffunE.
apply /moveP; exists ldisk ; split ; try by apply : on_top1.98f hrel (`c[p1] ldisk) (`c[p2] ldisk)
by rewrite !ffunE.
by case => [] [].
Qed .
Lemma gdist_liftr_perfect q n (hrel : rel (peg q)) p1 p2 p3 :
irreflexive hrel -> hrel p1 p2 -> p1 != p3 -> p2 != p3 ->
`d[↑[perfect p3 : configuration q n]_p1, ↑[perfect p3]_p2]_(move hrel) = 1 .985 irreflexive hrel ->
hrel p1 p2 ->
p1 != p3 ->
p2 != p3 ->
`d[↑[`c[p3 , n]]_p1, ↑[`c[p3]]_p2]_(move hrel) = 1
Proof .9b1
move => hirr p1Rp2 p1Dp3 p2Dp3.986 987 988 989 hirr : irreflexive hrel
990 991 992 `d[↑[`c[p3 , n]]_p1, ↑[`c[p3]]_p2]_(move hrel) = 1
apply /eqP; rewrite eqn_leq; apply /andP; split .9b8 `d[↑[`c[p3]]_p1, ↑[`c[p3]]_p2]_(move hrel) <= 1
rewrite -[1 ]/(size [:: cliftr p2 `c[p3, n]]).9b8 `d[↑[`c[p3]]_p1, ↑[`c[p3]]_p2]_(move hrel) <=
size [:: ↑[`c[p3 , n]]_p2]
9bf
apply : gdist_path_le => //=.9b8 move hrel ↑[`c[p3]]_p1 ↑[`c[p3]]_p2 && true
9bf
by rewrite move_liftr_perfect.
case E : gdist => //.986 987 988 989 9b9 990 991 992 E : `d[↑[`c[p3]]_p1, ↑[`c[p3]]_p2]_(move hrel) = 0
0 < 0
move /eqP: E; rewrite gdist_eq0 => /eqP E.986 987 988 989 9b9 990 991 992 E : ↑[`c[p3]]_p1 = ↑[`c[p3]]_p2
9d2
have := cliftr_ldisk p1 `c[p3, n].9d6 ↑[`c[p3]]_p1 ldisk = p1 -> 0 < 0
rewrite E cliftr_ldisk => p2Ep1.986 987 988 989 9b9 990 991 992 9d7 p2Ep1 : p2 = p1
9d2
by have := hirr p1; rewrite -{2 }p2Ep1 p1Rp2.
Qed .
(*****************************************************************************)
(* Regular relation *)
(*****************************************************************************)
Section Rrel .
Variable n : nat.
Definition rrel : rel (peg n) := [rel x y | x != y].
Definition rirr : irreflexive rrel.
by move => x; apply /eqP.
Qed .
Definition rsym : symmetric rrel.
by move => x y; rewrite /rrel /= eq_sym.
Qed .
Definition rmove m : rel (configuration n m) := move rrel.
End Rrel .
Section Srel .
Variable n : nat.
Definition srel : rel (peg n) := [rel x y : peg n | (x != y) && (x * y == 0 )].
Definition sirr : irreflexive srel.
by move => x; apply /idP/negP; rewrite negb_and eqxx.
Qed .
Definition ssym : symmetric srel.
by move => x y; rewrite /srel /= mulnC eq_sym.
Qed .
Definition smove m : rel (configuration n m) := move srel.
End Srel .
(******************************************************************************)
(* Linear relation *)
(******************************************************************************)
Section Lrel .
Variable n : nat.
Definition lrel : rel (peg n) :=
[rel x y : peg n | (x.+1 == y) || (y.+1 == x)].
Definition lirr : irreflexive lrel.
Proof .9f3
by move => k; rewrite /lrel /= (gtn_eqF (leqnn _)). Qed .
Definition lsym : symmetric lrel.
Proof .9f8
by move => x y; rewrite /lrel /= orbC.
Qed .
Definition lmove m : rel (configuration n m) := move lrel.
End Lrel .
Arguments rmove {n m}.
Arguments lmove {n m}.
Arguments smove {n m}.
Lemma connect_move p n (c1 c2 : configuration p.+3 n) :
connect rmove c1 c2.p, n : nat
c1, c2 : configuration p.+3 n
connect rmove c1 c2
Proof .9fd
elim : n c1 c2 => [c1 c2 | n IH c1 c2].p : nat
c1, c2 : configuration p.+3 0
a02
rewrite (_ : c1 = c2) ?connect0 //.
by apply /ffunP=> [] [].
rewrite -[c1]cunliftrK -[c2]cunliftrK.a0c connect rmove ↑[↓[c1]]_(c1 ldisk) ↑[↓[c2]]_(c2 ldisk)
set p1 := c1 ldisk; set p2 := c2 ldisk.a00 a0d a0e p1 := c1 ldisk : (fun => peg p.+3 ) ldisk
p2 := c2 ldisk : (fun => peg p.+3 ) ldisk
connect rmove ↑[↓[c1]]_p1 ↑[↓[c2]]_p2
have [<-|/eqP p1Dp2] := p1 =P p2.a1d connect rmove ↑[↓[c1]]_p1 ↑[↓[c2]]_p1
by apply : connect_liftr => // i; rewrite rirr.
pose p3 := opeg p1 p2.a00 a0d a0e a1e a1f 6ca p3 := `p[p1, p2] : peg p.+3
a20
apply : connect_trans (_ : connect _ (cliftr p1 `c[p3]) _).a2e connect rmove ↑[↓[c1]]_p1 ↑[`c[p3]]_p1
apply : connect_liftr; first by apply : rirr.a2e connect (move (rrel (n:=p.+3 ))) ↓[c1] `c[p3]
a34
by apply : IH.
apply : connect_trans (_ : connect _ (cliftr p2 `c[p3]) _); last first .a2e connect rmove ↑[`c[p3]]_p2 ↑[↓[c2]]_p2
apply : connect_liftr; first by apply : rirr.a2e connect (move (rrel (n:=p.+3 ))) `c[p3] ↓[c2]
a42
by apply : IH.
apply : connect1.a2e rmove ↑[`c[p3]]_p1 ↑[`c[p3]]_p2
apply : move_liftr_perfect => //.
rewrite eq_sym; apply : opegDl.
rewrite eq_sym; apply : opegDr.
Qed .
Lemma gdist_leq_move p n (c1 c2 : configuration p.+3 n) :
`d[c1, c2]_rmove <= (2 ^ n).-1 .9ff `d[c1, c2]_rmove <= (2 ^ n).-1
Proof .a5b
elim : n c1 c2 => [c1 c2 | n IH c1 c2].a07 `d[c1, c2]_rmove <= (2 ^ 0 ).-1
rewrite (_ : c1 = c2) ?gdist0 //.
by apply /ffunP=> [] [] [].
rewrite -[c1]cunliftrK -[c2]cunliftrK.a65 `d[↑[↓[c1]]_(c1 ldisk), ↑[↓[c2]]_(c2 ldisk)]_rmove <=
(2 ^ n.+1 ).-1
set p1 := c1 ldisk; set p2 := c2 ldisk.a00 a66 a0e a1e a1f
`d[↑[↓[c1]]_p1, ↑[↓[c2]]_p2]_rmove <= (2 ^ n.+1 ).-1
have [<-|/eqP p1Dp2] := p1 =P p2.a74 `d[↑[↓[c1]]_p1, ↑[↓[c2]]_p1]_rmove <= (2 ^ n.+1 ).-1
apply : leq_trans.a74 `d[↑[↓[c1]]_p1, ↑[↓[c2]]_p1]_rmove <= ?Goal0
apply : gdist_liftr => [i|]; first by rewrite rirr.a74 connect (move (rrel (n:=p.+3 ))) ↓[c1] ↓[c2]
apply : connect_move.
apply : leq_trans; first by apply : IH.a74 (2 ^ n).-1 <= (2 ^ n.+1 ).-1
a7a
rewrite -ltnS !prednK ?expn_gt0 //.
by rewrite leq_exp2l.
pose p3 := opeg p1 p2.
apply : leq_trans.a9c `d[↑[↓[c1]]_p1, ↑[↓[c2]]_p2]_rmove <= ?Goal
apply : (@gdist_triangular _ _ _ _ (cliftr p1 `c[p3])).a9c `d[↑[↓[c1]]_p1, ↑[`c[p3]]_p1]_rmove +
`d[↑[`c[p3]]_p1, ↑[↓[c2]]_p2]_rmove <= (2 ^ n.+1 ).-1
rewrite expnS mul2n -addnn.a9c `d[↑[↓[c1]]_p1, ↑[`c[p3]]_p1]_rmove +
`d[↑[`c[p3]]_p1, ↑[↓[c2]]_p2]_rmove <=
(2 ^ n + 2 ^ n).-1
have tnP : 0 < 2 ^ n by rewrite expn_gt0.a00 a66 a0e a1e a1f 6ca a2f tnP : 0 < 2 ^ n
aab
rewrite -(prednK tnP) addSn /=.aaf `d[↑[↓[c1]]_p1, ↑[`c[p3]]_p1]_rmove +
`d[↑[`c[p3]]_p1, ↑[↓[c2]]_p2]_rmove <=
(2 ^ n).-1 + (2 ^ n).-1 .+1
apply : leq_add.aaf `d[↑[↓[c1]]_p1, ↑[`c[p3]]_p1]_rmove <= (2 ^ n).-1
apply : leq_trans.aaf `d[↑[↓[c1]]_p1, ↑[`c[p3]]_p1]_rmove <= ?Goal0
apply : gdist_liftr => [i|]; first by rewrite rirr.
by apply : connect_move.
by apply : IH.
apply : leq_trans.aaf `d[↑[`c[p3]]_p1, ↑[↓[c2]]_p2]_rmove <= ?Goal
apply : (@gdist_triangular _ _ _ _ (cliftr p2 `c[p3])).aaf `d[↑[`c[p3]]_p1, ↑[`c[p3]]_p2]_rmove +
`d[↑[`c[p3]]_p2, ↑[↓[c2]]_p2]_rmove <= (2 ^ n).-1 .+1
rewrite gdist_liftr_perfect ?ltnS //; last 3 first .aaf irreflexive (rrel (n:=p.+3 ))
- adb
by apply : rirr.
- ae5
by rewrite eq_sym opegDl.
- aea
by rewrite eq_sym opegDr.
apply : leq_trans.aaf `d[↑[`c[p3]]_p2, ↑[↓[c2]]_p2]_rmove <= ?Goal
apply : gdist_liftr => [i|]; first by rewrite rirr.
by apply : connect_move.
by apply : IH.
Qed .
Definition sorted (s : seq nat) :=
forall i j , i < size s -> j < size s -> (nth 0 s i < nth 0 s j) = (i < j).
Lemma sorted_cons a s : sorted (a :: s) -> sorted s.sorted (a :: s) -> sorted s
Proof .b02
by move => H i j iH jH; rewrite -[in RHS]ltnS -[in RHS]H.
Qed .
Lemma sorted_iota i j : sorted (iota i j).
Proof .b0a
move => i1 j1; rewrite size_iota => i1Lj j1Lj.i, j, i1, j1 : nat
i1Lj : i1 < j
j1Lj : j1 < j
(nth 0 (iota i j) i1 < nth 0 (iota i j) j1) =
(i1 < j1)
by rewrite !nth_iota // ltn_add2l.
Qed .
Lemma sorted_skip a b s : sorted (a :: b :: s) -> sorted (a :: s).sorted [:: a, b & s] -> sorted (a :: s)
Proof .b19
move => Hs [|i] [|j] iH jH //=; first by rewrite ltnn.b1c b06 Hs : sorted [:: a, b & s]
j : nat
iH : 0 < size (a :: s)
jH : j.+1 < size (a :: s)
(a < nth 0 s j) = (0 < j.+1 )
- b20
by rewrite (Hs 0 j.+2 ).
- b34
by rewrite (Hs i.+2 0 ).
by rewrite (Hs i.+2 j.+2 ).
Qed .
Lemma sorted_filter (s : seq nat) (p : pred nat) :
sorted s -> sorted (filter p s).sorted s -> sorted [seq x <- s | p x]
Proof .b3c
have F a s1 i :
sorted (a :: s1) -> i < size (filter p s1) -> a < nth 0 (filter p s1) i.sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
elim : s1 i => //= b s1 IH i abS.b06 b3f b1c b46 IH : forall i : nat,
sorted (a :: s1) ->
i < size [seq x <- s1 | p x] ->
a < nth 0 [seq x <- s1 | p x] i
b2b abS : sorted [:: a, b & s1]
i <
size
(if p b
then b :: [seq x <- s1 | p x]
else [seq x <- s1 | p x]) ->
a <
nth 0
(if p b
then b :: [seq x <- s1 | p x]
else [seq x <- s1 | p x]) i
b48
have [pbT|pbF] := boolP (p b).b06 b3f b1c b46 b50 b2b b51 pbT : p b
i < size (b :: [seq x <- s1 | p x]) ->
a < nth 0 (b :: [seq x <- s1 | p x]) i
case : i => [|i1] /= sH; first by rewrite (abS 0 1 ).b06 b3f b1c b46 b50 b51 b57 i1 : nat
sH : i1.+1 < (size [seq x <- s1 | p x]).+1
a < nth 0 [seq x <- s1 | p x] i1
b59
apply : IH => //.b06 b3f b1c b46 b51 b57 b62 b63
sorted (a :: s1)
b59
by apply : sorted_skip abS.
apply : IH.b06 b3f b1c b46 b2b b51 b5c
b69 b48
by apply : sorted_skip abS.
elim : s => //= a s IH aS.b3f b4b b05 b06 IH : sorted s -> sorted [seq x <- s | p x]
aS : sorted (a :: s)
sorted
(if p a
then a :: [seq x <- s | p x]
else [seq x <- s | p x])
have sS := sorted_cons aS.b3f b4b b05 b06 b78 b79 sS : sorted s
b7a
have [paT|paF] := boolP (p a); last by apply : IH.b3f b4b b05 b06 b78 b79 b7f paT : p a
sorted (a :: [seq x <- s | p x])
move => [|i] [|j] iH jH /=.b3f b4b b05 b06 b78 b79 b7f b84 iH, jH : 0 < size (a :: [seq x <- s | p x])
(a < a) = (0 < 0 )
- b87
by rewrite ltnn.
- b9c
by rewrite F.
- ba1
by rewrite ltnNge ltnW // F.
by rewrite ltnS (IH sS).
Qed .
Lemma enum_ord_inord m : (enum 'I_m.+1 ) = [seq inord i | i <- iota 0 m.+1 ].8cd
enum 'I_m.+1 = [seq inord i | i <- iota 0 m.+1 ]
Proof .ba9
rewrite -val_ord_enum -map_comp /=.bab enum 'I_m.+1 =
[seq ([eta inord] \o nat_of_ord (n:=m.+1 )) i
| i <- ord_enum m.+1 ]
rewrite enumT unlock /=.bab ord_enum m.+1 =
[seq ([eta inord] \o nat_of_ord (n:=m.+1 )) i
| i <- ord_enum m.+1 ]
elim : (ord_enum _) => //= a l <-.8cd a : 'I_m.+1
l : seq 'I_m.+1
a :: l = inord a :: l
by rewrite inord_val.
Qed .
(* To be reworked ! *)
Lemma sorted_enum_val (m : nat) (s : {set 'I_m}) (i j : 'I_#|s|) :
(enum_val i) < (enum_val j) = (i < j).8cd s : {set 'I_m}
i, j : 'I_#|s|
(enum_val i < enum_val j) = (i < j)
Proof .bbe
case : m s i j => [s|m s i j].forall i j : 'I_#|s|,
(enum_val i < enum_val j) = (i < j)
rewrite (_ : s = set0).bc8 forall i j : 'I_#|set0|,
(enum_val i < enum_val j) = (i < j)
case => m H j; apply : False_ind.bc9 8cd H : m < #|set0|
j : 'I_#|set0|
49b bd3
by rewrite cards0 in H.
by apply /setP=> [] [].
have := ltn_ord i; have := ltn_ord j; rewrite {2 4 }cardE.bcd j < size (enum s) ->
i < size (enum s) ->
(enum_val i < enum_val j) = (i < j)
rewrite /enum_val /= /(enum _) -enumT enum_ord_inord => iL jL.8cd bce bc2 iL : j <
size
[seq x <- [seq inord i | i <- iota 0 m.+1 ]
| mem s x]
jL : i <
size
[seq x <- [seq inord i | i <- iota 0 m.+1 ]
| mem s x]
(nth (enum_default i)
[seq x <- [seq inord i | i <- iota 0 m.+1 ]
| mem s x] i <
nth (enum_default j)
[seq x <- [seq inord i | i <- iota 0 m.+1 ]
| mem s x] j) = (i < j)
have <-// := @nth_map ('I_m.+1 ) (enum_default i) nat 0 (@nat_of_ord m.+1 ).be9 (nth 0
[seq i
| i <- [seq inord i | i <- iota 0 m.+1 ]
& mem s i] i <
nth (enum_default j)
[seq x <- [seq inord i | i <- iota 0 m.+1 ]
| mem s x] j) = (i < j)
have <-// := @nth_map ('I_m.+1 ) (enum_default j) nat 0 (@nat_of_ord m.+1 ).be9 (nth 0
[seq i
| i <- [seq inord i | i <- iota 0 m.+1 ]
& mem s i] i <
nth 0
[seq i
| i <- [seq inord i | i <- iota 0 m.+1 ]
& mem s i] j) = (i < j)
have F k1 k2 : k1 + k2 <= m.+1 ->
[seq (nat_of_ord i) | i <- [seq inord i0 | i0 <- iota k1 k2] & mem s i] =
(filter (fun i0 => mem s (inord i0)) (iota k1 k2)).8cd bce bc2 bea beb k1, k2 : nat
k1 + k2 <= m.+1 ->
[seq i
| i <- [seq inord i0 | i0 <- iota k1 k2]
& mem s i] =
[seq i0 <- iota k1 k2 | mem s (inord i0)]
elim : k2 k1 => //= k2 IH k1 k1k2Lm.8cd bce bc2 bea beb k2 : nat
IH : forall k1 : nat,
k1 + k2 <= m.+1 ->
[seq i
| i <- [seq inord i0 | i0 <- iota k1 k2]
& i \in s] =
[seq i0 <- iota k1 k2 | inord i0 \in s]
k1 : nat
k1k2Lm : k1 + k2.+1 <= m.+1
[seq i
| i <- if inord k1 \in s
then
inord k1
:: [seq i <- [seq inord i0
| i0 <- iota k1.+1 k2]
| i \in s]
else
[seq i <- [seq inord i0
| i0 <- iota k1.+1 k2]
| i \in s]] =
(if inord k1 \in s
then k1 :: [seq i0 <- iota k1.+1 k2 | inord i0 \in s]
else [seq i0 <- iota k1.+1 k2 | inord i0 \in s])
bfb
case : (_ \in _) => //=.c02 inord k1
:: [seq i
| i <- [seq inord i0 | i0 <- iota k1.+1 k2]
& i \in s] =
k1 :: [seq i0 <- iota k1.+1 k2 | inord i0 \in s]
rewrite inordK //.c02 k1
:: [seq i
| i <- [seq inord i0 | i0 <- iota k1.+1 k2]
& i \in s] =
k1 :: [seq i0 <- iota k1.+1 k2 | inord i0 \in s]
rewrite IH //.
by rewrite addSnnS.
by apply : leq_trans k1k2Lm; rewrite -addSnnS leq_addr.
apply : IH.8cd bce bc2 bea beb k2, k1 : nat
c06 c19 bfb
by rewrite addSnnS.
rewrite F //.bfd (nth 0 [seq i0 <- iota 0 m.+1 | mem s (inord i0)] i <
nth 0 [seq i0 <- iota 0 m.+1 | mem s (inord i0)] j) =
(i < j)
have : j < size ([seq i0 <- iota 0 m.+1 | mem s (inord i0)]).bfd j < size [seq i0 <- iota 0 m.+1 | mem s (inord i0)]
by move : iL; rewrite -F // size_map.
have : i < size ([seq i0 <- iota 0 m.+1 | mem s (inord i0)])
by move : jL; rewrite -F // size_map.bfd i < size [seq i0 <- iota 0 m.+1 | mem s (inord i0)] ->
j < size [seq i0 <- iota 0 m.+1 | mem s (inord i0)] ->
(nth 0 [seq i0 <- iota 0 m.+1 | mem s (inord i0)] i <
nth 0 [seq i0 <- iota 0 m.+1 | mem s (inord i0)] j) =
(i < j)
apply : sorted_filter => //.
by apply : sorted_iota.
Qed .
Section ISetd .
(* Number of disks *)
Variable n : nat.
(* Subset of disks *)
Variable sd : {set disk n}.
(* Number of pegs *)
Variable k : nat.
(* relations on peg *)
Variable rel : rel (peg k).
Definition cset (c : configuration k n) : configuration k #|sd| :=
[ffun i => c (enum_val i)].
Lemma on_top_cset c d (dIsd : d \in sd) :
on_top d c -> on_top (enum_rank_in dIsd d) (cset c).1b sd : {set disk n}
828 rel : ssrbool.rel (peg k)
c : configuration k n
3b dIsd : d \in sd
on_top d c -> on_top (enum_rank_in dIsd d) (cset c)
Proof .c3f
move => /= /on_topP dO.1b c42 828 c43 c44 3b c45 dO : forall d1 : ordinal_finType n,
c d = c d1 -> d <= d1
on_top (enum_rank_in dIsd d) (cset c)
apply /on_topP => /= d1 H.1b c42 828 c43 c44 3b c45 c4c d1 : 'I_#|[eta sd]|
H : cset c (enum_rank_in dIsd d) = cset c d1
enum_rank_in dIsd d <= d1
rewrite leq_eqVlt; case : eqP => //= /eqP dDd1.1b c42 828 c43 c44 3b c45 c4c c52 c53 dDd1 : enum_rank_in dIsd d != d1
enum_rank_in dIsd d < d1
rewrite -[d1](enum_valK_in dIsd) -sorted_enum_val !enum_rankK_in //; last first .
by apply : enum_valP.
rewrite ltn_neqAle.c58 (d != enum_val d1) && (d <= enum_val d1)
case : eqP => [/eqP /val_eqP dEd1 | /eqP dDd1' /=].1b c42 828 c43 c44 3b c45 c4c c52 c53 c59 dEd1 : d = enum_val d1
~~ true && (d <= enum_val d1)
by case /eqP: dDd1; rewrite {2 }dEd1 enum_valK_in.
rewrite !ffunE enum_rankK_in // in H.1b c42 828 c43 c44 3b c45 c4c c52 c59 c72 H : c d = c (enum_val d1)
c73
by apply : dO.
Qed .
Lemma move_cset (c1 c2 : configuration k n) :
move rel c1 c2 -> (cset c1) != (cset c2) ->
move rel (cset c1) (cset c2).1b c42 828 c43 c1, c2 : configuration k n
move rel c1 c2 ->
cset c1 != cset c2 -> move rel (cset c1) (cset c2)
Proof .c7d
move => /moveP [d [dH1 dH2 dH3 dH4]] c1Dc2.1b c42 828 c43 c80 3b dH1 : rel (c1 d) (c2 d)
dH2 : forall d2 : ordinal_finType n, d != d2 -> c1 d2 = c2 d2
dH3 : on_top d c1
dH4 : on_top d c2
c1Dc2 : cset c1 != cset c2
move rel (cset c1) (cset c2)
have [dIsd|dNIsd] := boolP (d \in sd); last first .1b c42 828 c43 c80 3b c87 c88 c89 c8a c8b dNIsd : d \notin sd
c8c
case /eqP: c1Dc2.1b c42 828 c43 c80 3b c87 c88 c89 c8a c91
cset c1 = cset c2
c92
apply /ffunP => i; rewrite !ffunE.1b c42 828 c43 c80 3b c87 c88 c89 c8a c91 i : ordinal_finType #|sd|
c1 (enum_val i) = c2 (enum_val i)
c92
apply : dH2.1b c42 828 c43 c80 3b c87 c89 c8a c91 c9f
d != enum_val i
c92
apply : contra dNIsd => /eqP->.1b c42 828 c43 c80 3b c87 c89 c8a c9f
enum_val i \in sd
by apply : enum_valP.
apply /moveP; exists (enum_rank_in dIsd d ); split => /=.cad rel (cset c1 (enum_rank_in dIsd d))
(cset c2 (enum_rank_in dIsd d))
- cb2
by rewrite !ffunE !enum_rankK_in //.
- cbe
move => /= d2 dDd2.1b c42 828 c43 c80 3b c87 c88 c89 c8a c8b c45 d2 : 'I_#|sd|
dDd2 : enum_rank_in dIsd d != d2
cset c1 d2 = cset c2 d2
cc0
rewrite !ffunE.cc5 c1 (enum_val d2) = c2 (enum_val d2)
cc0
apply : dH2.1b c42 828 c43 c80 3b c87 c89 c8a c8b c45 cc6 cc7
d != enum_val d2
cc0
rewrite -[d](enum_rankK_in dIsd) //.cd0 enum_val (enum_rank_in dIsd d) != enum_val d2
cc0
by apply /eqP => /enum_val_inj /eqP; rewrite (negPf dDd2).
- cd7
by apply : on_top_cset.
by apply : on_top_cset.
Qed .
Lemma path_cset (c : configuration _ _) cs :
path (move rel) c cs ->
path (move rel) (cset c) (rm_rep (cset c) [seq (cset i) | i <- cs]).1b c42 828 c43 c44 cs : seq (configuration k n)
path (move rel) c cs ->
path (move rel) (cset c)
(rm_rep (cset c) [seq cset i | i <- cs])
Proof .cdf
elim : cs c => //= c1 cs IH c => /andP[cMc1 c1Pcs].1b c42 828 c43 c1 : configuration k n
ce2 IH : forall c : configuration k n,
path (move rel) c cs ->
path (move rel) (cset c)
(rm_rep (cset c) [seq cset i | i <- cs])
c44 cMc1 : move rel c c1
c1Pcs : path (move rel) c1 cs
path (move rel) (cset c)
(if cset c == cset c1
then rm_rep (cset c1) [seq cset i | i <- cs]
else
cset c1 :: rm_rep (cset c1) [seq cset i | i <- cs])
case : eqP => [->|/eqP cDc1 /=]; first by apply : IH; rewrite ?c2V .1b c42 828 c43 ce9 ce2 cea c44 ceb cec cDc1 : cset c != cset c1
move rel (cset c) (cset c1) &&
path (move rel) (cset c1)
(rm_rep (cset c1) [seq cset i | i <- cs])
by rewrite move_cset => //=; first by apply : IH; rewrite ?c2V .
Qed .
Lemma gdist_cset c1 c2 cs :
last c1 cs = c2 -> path (move rel) c1 cs ->
`d[cset c1, cset c2]_(move rel) <= size cs.1b c42 828 c43 c80 ce2
last c1 cs = c2 ->
path (move rel) c1 cs ->
`d[cset c1, cset c2]_(move rel) <= size cs
Proof .cf5
move => cL cPcs.1b c42 828 c43 c80 ce2 cL : last c1 cs = c2
cPcs : path (move rel) c1 cs
`d[cset c1, cset c2]_(move rel) <= size cs
have := size_rm_rep (cset c1) [seq (cset i) | i <- cs].cfd size (rm_rep (cset c1) [seq cset i | i <- cs]) <=
size [seq cset i | i <- cs] ->
`d[cset c1, cset c2]_(move rel) <= size cs
rewrite size_map; move /(leq_trans _); apply .cfd `d[cset c1, cset c2]_(move rel) <=
size (rm_rep (cset c1) [seq cset i | i <- cs])
apply : gdist_path_le; first by apply : path_cset.cfd last (cset c1)
(rm_rep (cset c1) [seq cset i | i <- cs]) = cset c2
by rewrite last_rm_rep last_map cL.
Qed .
Lemma gpath_cset c1 c2 cs :
gpath (move rel) c1 c2 cs ->
`d[cset c1, cset c2]_(move rel) <= `d[c1, c2]_(move rel).1b c42 828 c43 c1, c2 : finfun_finType (ordinal_finType n)
(ordinal_finType k)
cs : seq
(finfun_finType (ordinal_finType n)
(ordinal_finType k))
gpath (move rel) c1 c2 cs ->
`d[cset c1, cset c2]_(move rel) <=
`d[c1, c2]_(move rel)
Proof .d0e
move => gH.1b c42 828 c43 d11 d12 gH : gpath (move rel) c1 c2 cs
`d[cset c1, cset c2]_(move rel) <=
`d[c1, c2]_(move rel)
rewrite (gpath_dist gH); apply : gdist_cset => //; first apply : gpath_last gH.
by apply : gpath_path gH.
Qed .
End ISetd .
Arguments gpath [T].
Section CSet .
(* Number of disks *)
Variable n : nat.
(* cut limit *)
Variable t : nat.
Variable tLn : t <= n.
(* Number of pegs *)
Variable k : nat.
(* relations on peg *)
Variable rel : rel (peg k).
Hypothesis irH : irreflexive rel.
Definition ccut (c : configuration k n) : configuration k t :=
[ffun i => c (widen_ord tLn i)].
Lemma ordinalK (d : disk n) (dLt : d < t) : widen_ord tLn (Ordinal dLt) = d.n, t : nat
tLn : t <= n
828 c43 irH : irreflexive rel
1c dLt : d < t
widen_ord tLn (Ordinal dLt) = d
Proof .d20
by apply : val_inj. Qed .
Lemma codom_cut (c : configuration k n) (s : seq (peg k)) :
codom c \subset s -> codom (ccut c) \subset s.d23 d24 828 c43 d25 c44 s : seq (peg k)
codom c \subset s -> codom (ccut c) \subset s
Proof .d2a
move => H; apply /subsetP => i /mapP[j _ ->].d23 d24 828 c43 d25 c44 d2d 5e8 i : ordinal_finType k
j : ordinal_finType t
ccut c j \in s
by rewrite ffunE; apply : (subsetP H); apply : codom_f.
Qed .
Lemma s2f_cut (c : configuration k n) (p : disk k) :
s2f ([set i | c i == p] :&: isO n t) =
s2f [set i | ccut c i == p].d23 d24 828 c43 d25 c44 p : disk k
s2f ([set i | c i == p] :&: isO n t) =
s2f [set i | ccut c i == p]
Proof .d38
apply /fsetP=> /= i.d23 d24 828 c43 d25 c44 d3b b2b
(i \in s2f ([set i | c i == p] :&: isO n t)) =
(i \in s2f [set i | ccut c i == p])
apply /imfsetP/imfsetP => [] /= [j]; rewrite !inE.d23 d24 828 c43 d25 c44 d3b b2b 16d
(c j == p) && (j < t) ->
i = j ->
exists2 x : 'I_t,
x \in [set i | ccut c i == p] & i = x
case /andP => cjEp jLt ->.d23 d24 828 c43 d25 c44 d3b b2b 16d cjEp : c j == p
jLt : j < t
exists2 x : 'I_t,
x \in [set i | ccut c i == p] & j = x
d48
by exists (Ordinal jLt ); rewrite //= inE !ffunE ordinalK.
rewrite !ffunE => cjEp ->; exists (widen_ord tLn j ) => //=.d23 d24 828 c43 d25 c44 d3b b2b d4b cjEp : c (widen_ord tLn j) == p
widen_ord tLn j \in [set i | c i == p] :&: isO n t
by rewrite !inE /= cjEp /=.
Qed .
Lemma on_top_cut c (d : disk n) (dLr : d < t) :
on_top d c -> on_top (Ordinal dLr) (ccut c).d23 d24 828 c43 d25 c44 1c dLr : d < t
on_top d c -> on_top (Ordinal dLr) (ccut c)
Proof .d5e
move => /= /on_topP dO.d23 d24 828 c43 d25 c44 1c d61 c4c
on_top (Ordinal dLr) (ccut c)
apply /on_topP => /= d1 H.d23 d24 828 c43 d25 c44 1c d61 c4c d1 : 'I_t
H : ccut c (Ordinal dLr) = ccut c d1
27
rewrite leq_eqVlt; case : eqP => //= /eqP dDd1.d23 d24 828 c43 d25 c44 1c d61 c4c d6d d6e dDd1 : d != d1
d < d1
rewrite ltn_neqAle dDd1 /=.
apply : (dO (widen_ord tLn d1)) => //.d72 c d = c (widen_ord tLn d1)
by move : H; rewrite !ffunE ordinalK.
Qed .
Lemma move_cut (c1 c2 : configuration k n) :
move rel c1 c2 -> (ccut c1) != (ccut c2) ->
move rel (ccut c1) (ccut c2).d23 d24 828 c43 d25 c80
move rel c1 c2 ->
ccut c1 != ccut c2 -> move rel (ccut c1) (ccut c2)
Proof .d7d
move => /moveP [d [dH1 dH2 dH3 dH4]] c1Dc2.d23 d24 828 c43 d25 c80 3b c87 c88 c89 c8a c1Dc2 : ccut c1 != ccut c2
move rel (ccut c1) (ccut c2)
have [dLt|tLd] := leqP t d.d23 d24 828 c43 d25 c80 3b c87 c88 c89 c8a d86 dLt : t <= d
d87
case /eqP: c1Dc2.d23 d24 828 c43 d25 c80 3b c87 c88 c89 c8a d8c
ccut c1 = ccut c2
apply /ffunP => i; rewrite !ffunE.d23 d24 828 c43 d25 c80 3b c87 c88 c89 c8a d8c i : ordinal_finType t
c1 (widen_ord tLn i) = c2 (widen_ord tLn i)
d96
apply : dH2.d23 d24 828 c43 d25 c80 3b c87 c89 c8a d8c d9d
d != widen_ord tLn i
d96
by rewrite -val_eqE /= neq_ltn (leq_trans _ dLt) // orbT.
apply /moveP; exists (Ordinal tLd ); split => /=.d98 rel (ccut c1 (Ordinal tLd)) (ccut c2 (Ordinal tLd))
- da8
by rewrite !ffunE // ordinalK.
- db4
move => /= d2; rewrite !ffunE -val_eqE /= => dDd2.d23 d24 828 c43 d25 c80 3b c87 c88 c89 c8a d86 d90 d2 : 'I_t
dDd2 : d != d2
c1 (widen_ord tLn d2) = c2 (widen_ord tLn d2)
db6
by apply : dH2; rewrite -val_eqE /=.
- dc0
by apply : on_top_cut.
by apply : on_top_cut.
Qed .
Lemma path_cut (c : configuration _ _) cs :
path (move rel) c cs ->
path (move rel) (ccut c) (rm_rep (ccut c) [seq (ccut i) | i <- cs]).d23 d24 828 c43 d25 c44 ce2
path (move rel) c cs ->
path (move rel) (ccut c)
(rm_rep (ccut c) [seq ccut i | i <- cs])
Proof .dc8
elim : cs c => //= c1 cs IH c => /andP[cMc1 c1Pcs].d23 d24 828 c43 d25 ce9 ce2 IH : forall c : configuration k n,
path (move rel) c cs ->
path (move rel) (ccut c)
(rm_rep (ccut c) [seq ccut i | i <- cs])
c44 ceb cec path (move rel) (ccut c)
(if ccut c == ccut c1
then rm_rep (ccut c1) [seq ccut i | i <- cs]
else
ccut c1 :: rm_rep (ccut c1) [seq ccut i | i <- cs])
case : eqP => [->|/eqP cDc1 /=]; first by apply : IH; rewrite ?c2V .d23 d24 828 c43 d25 ce9 ce2 dd1 c44 ceb cec cDc1 : ccut c != ccut c1
move rel (ccut c) (ccut c1) &&
path (move rel) (ccut c1)
(rm_rep (ccut c1) [seq ccut i | i <- cs])
by rewrite move_cut => //=; first by apply : IH; rewrite ?c2V .
Qed .
Lemma gdist_cut c1 c2 cs :
last c1 cs = c2 -> path (move rel) c1 cs ->
`d[ccut c1, ccut c2]_(move rel) <= size cs.d23 d24 828 c43 d25 c80 ce2
last c1 cs = c2 ->
path (move rel) c1 cs ->
`d[ccut c1, ccut c2]_(move rel) <= size cs
Proof .dda
move => cL cPcs.d23 d24 828 c43 d25 c80 ce2 cfe cff
`d[ccut c1, ccut c2]_(move rel) <= size cs
have := size_rm_rep (ccut c1) [seq (ccut i) | i <- cs].de2 size (rm_rep (ccut c1) [seq ccut i | i <- cs]) <=
size [seq ccut i | i <- cs] ->
`d[ccut c1, ccut c2]_(move rel) <= size cs
rewrite size_map; move /(leq_trans _); apply .de2 `d[ccut c1, ccut c2]_(move rel) <=
size (rm_rep (ccut c1) [seq ccut i | i <- cs])
apply : gdist_path_le; first by apply : path_cut.de2 last (ccut c1)
(rm_rep (ccut c1) [seq ccut i | i <- cs]) = ccut c2
by rewrite last_rm_rep last_map cL.
Qed .
Lemma gpath_cut c1 c2 cs :
gpath (move rel) c1 c2 cs ->
`d[ccut c1, ccut c2]_(move rel) <= `d[c1, c2]_(move rel).d23 d24 828 c43 d25 d11 d12
gpath (move rel) c1 c2 cs ->
`d[ccut c1, ccut c2]_(move rel) <=
`d[c1, c2]_(move rel)
Proof .df1
move => gH.d23 d24 828 c43 d25 d11 d12 d19
`d[ccut c1, ccut c2]_(move rel) <=
`d[c1, c2]_(move rel)
rewrite (gpath_dist gH); apply : gdist_cut => //; first apply : gpath_last gH.
by apply : gpath_path gH.
Qed .
Lemma tuc_subproof i : i < n - t -> i + t < n.d23 d24 828 c43 d25 b2b
i < n - t -> i + t < n
Proof .dff
by move => iLnt; rewrite -(subnK tLn) ltn_add2r. Qed .
Definition tuc_ord (i : disk (n - t)) : disk n :=
Ordinal (tuc_subproof (ltn_ord i)).
Lemma otuc_subproof i : i < n -> t <= i -> i - t < n - t.e01 i < n -> t <= i -> i - t < n - t
Proof .e05
move => iLn tLi; apply : ltn_sub2r => //.d23 d24 828 c43 d25 b2b iLn : i < n
tLi : t <= i
t < n
by apply : leq_ltn_trans iLn.
Qed .
Definition otuc (i : disk n) (tLi : t <= i) : disk (n - t) :=
Ordinal (otuc_subproof (ltn_ord i) tLi).
Lemma otucK (d : disk n) (tLd : t <= d) : tuc_ord (otuc tLd) = d.d23 d24 828 c43 d25 1c tLd : t <= d
tuc_ord (otuc tLd) = d
Proof .e11
by apply : val_inj; rewrite /= subnK. Qed .
Definition ctuc (c : configuration k n) : configuration k (n - t) :=
[ffun i => c (tuc_ord i)].
Lemma on_top_tuc c (d : disk n) (dLr : t <= d) :
on_top d c -> on_top (otuc dLr) (ctuc c).d23 d24 828 c43 d25 c44 1c dLr : t <= d
on_top d c -> on_top (otuc dLr) (ctuc c)
Proof .e18
move => /= /on_topP dO.d23 d24 828 c43 d25 c44 1c e1b c4c
on_top (otuc dLr) (ctuc c)
apply /on_topP => /= d1 H.d23 d24 828 c43 d25 c44 1c e1b c4c d1 : 'I_(n - t)
H : ctuc c (otuc dLr) = ctuc c d1
d - t <= d1
rewrite leq_eqVlt; case : eqP => //= /eqP dDd1.d23 d24 828 c43 d25 c44 1c e1b c4c e27 e28 dDd1 : d - t != d1
d - t < d1
rewrite ltn_neqAle dDd1 /= leq_subLR addnC.
apply : (dO (tuc_ord d1)) => //.
by move : H; rewrite !ffunE otucK.
Qed .
Lemma move_tuc (c1 c2 : configuration k n) :
move rel c1 c2 -> (ctuc c1) != (ctuc c2) ->
move rel (ctuc c1) (ctuc c2).d7f move rel c1 c2 ->
ctuc c1 != ctuc c2 -> move rel (ctuc c1) (ctuc c2)
Proof .e39
move => /moveP [d [dH1 dH2 dH3 dH4]] c1Dc2.d23 d24 828 c43 d25 c80 3b c87 c88 c89 c8a c1Dc2 : ctuc c1 != ctuc c2
move rel (ctuc c1) (ctuc c2)
have [dLt|tLd] := leqP t d; last first .d23 d24 828 c43 d25 c80 3b c87 c88 c89 c8a e41 d90
e42
case /eqP: c1Dc2.d23 d24 828 c43 d25 c80 3b c87 c88 c89 c8a d90
ctuc c1 = ctuc c2
apply /ffunP => i; rewrite !ffunE.d23 d24 828 c43 d25 c80 3b c87 c88 c89 c8a d90 i : ordinal_finType (n - t)
c1 (tuc_ord i) = c2 (tuc_ord i)
e4f
apply : dH2.d23 d24 828 c43 d25 c80 3b c87 c89 c8a d90 e56
d != tuc_ord i
e4f
by rewrite -val_eqE /= neq_ltn (leq_trans tLd _) // leq_addl.
apply /moveP; exists (otuc dLt ); split => /=.e51 rel (ctuc c1 (otuc dLt)) (ctuc c2 (otuc dLt))
- e61
by rewrite !ffunE // otucK.
- e6d
move => /= d2; rewrite !ffunE -val_eqE /= => dDd2.d23 d24 828 c43 d25 c80 3b c87 c88 c89 c8a e41 d8c d2 : 'I_(n - t)
dDd2 : d - t != d2
c1 (tuc_ord d2) = c2 (tuc_ord d2)
e6f
by apply : dH2; rewrite -val_eqE /= -(subnK dLt) eqn_add2r.
- e79
by apply : on_top_tuc.
by apply : on_top_tuc.
Qed .
Lemma path_tuc (c : configuration _ _) cs :
path (move rel) c cs ->
path (move rel) (ctuc c) (rm_rep (ctuc c) [seq (ctuc i) | i <- cs]).dca path (move rel) c cs ->
path (move rel) (ctuc c)
(rm_rep (ctuc c) [seq ctuc i | i <- cs])
Proof .e81
elim : cs c => //= c1 cs IH c => /andP[cMc1 c1Pcs].d23 d24 828 c43 d25 ce9 ce2 IH : forall c : configuration k n,
path (move rel) c cs ->
path (move rel) (ctuc c)
(rm_rep (ctuc c) [seq ctuc i | i <- cs])
c44 ceb cec path (move rel) (ctuc c)
(if ctuc c == ctuc c1
then rm_rep (ctuc c1) [seq ctuc i | i <- cs]
else
ctuc c1 :: rm_rep (ctuc c1) [seq ctuc i | i <- cs])
case : eqP => [->|/eqP cDc1 /=]; first by apply : IH; rewrite ?c2V .d23 d24 828 c43 d25 ce9 ce2 e89 c44 ceb cec cDc1 : ctuc c != ctuc c1
move rel (ctuc c) (ctuc c1) &&
path (move rel) (ctuc c1)
(rm_rep (ctuc c1) [seq ctuc i | i <- cs])
by rewrite move_tuc => //=; first by apply : IH; rewrite ?c2V .
Qed .
Lemma gdist_tuc c1 c2 cs :
last c1 cs = c2 -> path (move rel) c1 cs ->
`d[ctuc c1, ctuc c2]_(move rel) <= size cs.ddc last c1 cs = c2 ->
path (move rel) c1 cs ->
`d[ctuc c1, ctuc c2]_(move rel) <= size cs
Proof .e92
move => cL cPcs.de2 `d[ctuc c1, ctuc c2]_(move rel) <= size cs
have := size_rm_rep (ctuc c1) [seq (ctuc i) | i <- cs].de2 size (rm_rep (ctuc c1) [seq ctuc i | i <- cs]) <=
size [seq ctuc i | i <- cs] ->
`d[ctuc c1, ctuc c2]_(move rel) <= size cs
rewrite size_map; move /(leq_trans _); apply .de2 `d[ctuc c1, ctuc c2]_(move rel) <=
size (rm_rep (ctuc c1) [seq ctuc i | i <- cs])
apply : gdist_path_le; first by apply : path_tuc.de2 last (ctuc c1)
(rm_rep (ctuc c1) [seq ctuc i | i <- cs]) = ctuc c2
by rewrite last_rm_rep last_map cL.
Qed .
Lemma gpath_tuc c1 c2 cs :
gpath (move rel) c1 c2 cs ->
`d[ctuc c1, ctuc c2]_(move rel) <= `d[c1, c2]_(move rel).df3 gpath (move rel) c1 c2 cs ->
`d[ctuc c1, ctuc c2]_(move rel) <=
`d[c1, c2]_(move rel)
Proof .ea7
move => gH.df9 `d[ctuc c1, ctuc c2]_(move rel) <=
`d[c1, c2]_(move rel)
rewrite (gpath_dist gH); apply : gdist_tuc => //; first apply : gpath_last gH.dfc
by apply : gpath_path gH.
Qed .
Lemma size_cut_tuc (c : configuration _ _) cs :
path (move rel) c cs ->
size cs =
(size (rm_rep (ccut c) [seq (ccut i) | i <- cs]) +
size (rm_rep (ctuc c) [seq (ctuc i) | i <- cs]))%nat.dca path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
Proof .eb1
elim : cs c => //= c1 cs IH c /andP[/moveP[d [dH1 dH2 dH3 dH4]] c1Pcs].d23 d24 828 c43 d25 ce9 ce2 IH : forall c : configuration k n,
path (move rel) c cs ->
size cs =
size (rm_rep (ccut c) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c) [seq ctuc i | i <- cs])
c44 3b dH1 : rel (c d) (c1 d)
dH2 : forall d2 : ordinal_finType n, d != d2 -> c d2 = c1 d2
dH3 : on_top d c
dH4 : on_top d c1
cec (size cs).+1 =
size
(if ccut c == ccut c1
then rm_rep (ccut c1) [seq ccut i | i <- cs]
else
ccut c1 :: rm_rep (ccut c1) [seq ccut i | i <- cs]) +
size
(if ctuc c == ctuc c1
then rm_rep (ctuc c1) [seq ctuc i | i <- cs]
else
ctuc c1 :: rm_rep (ctuc c1) [seq ctuc i | i <- cs])
have cdDc1d : c d != c1 d.
by have /idP/negP := irH (c d); apply : contra => /eqP {2 }->.d23 d24 828 c43 d25 ce9 ce2 eb9 c44 3b eba ebb ebc ebd cec ec7
ebe
have [tLd|dLt] := leqP t d; last first .d23 d24 828 c43 d25 ce9 ce2 eb9 c44 3b eba ebb ebc ebd cec ec7 d26
ebe
rewrite ifN /= ?addSn ; last first .
apply /eqP => /ffunP /(_ (Ordinal dLt)).ecf ccut c (Ordinal dLt) = ccut c1 (Ordinal dLt) -> False
ed7
by rewrite !ffunE ordinalK => /eqP; rewrite (negPf cdDc1d).
rewrite ifT; last first .
apply /eqP/ffunP=> i; rewrite !ffunE dH2 //=.d23 d24 828 c43 d25 ce9 ce2 eb9 c44 3b eba ebb ebc ebd cec ec7 d26 e56
e5c ee6
apply /eqP => /val_eqP.eec val d == val (tuc_ord i) -> False
ee6
by rewrite /= eqn_leq [_ <= d]leqNgt (leq_trans dLt) ?andbF // leq_addl.
by congr (_.+1 ); apply : IH.d23 d24 828 c43 d25 ce9 ce2 eb9 c44 3b eba ebb ebc ebd cec ec7 e14
ebe
rewrite ifT; last first .
apply /eqP/ffunP=> i; rewrite !ffunE dH2 //.d23 d24 828 c43 d25 ce9 ce2 eb9 c44 3b eba ebb ebc ebd cec ec7 e14 d9d
da3 efc
by apply /eqP => /val_eqP; rewrite /= eqn_leq leqNgt (leq_trans (ltn_ord _)).
rewrite ifN /= ?addSn ; last first .
apply /eqP => /ffunP /(_ (otuc tLd)) /eqP.ef7 ctuc c (otuc tLd) == ctuc c1 (otuc tLd) -> False
f0a
by rewrite !ffunE otucK (negPf cdDc1d).
by rewrite addnS; congr (_.+1 ); apply : IH.
Qed .
Lemma gdist_cut_tuc c1 c2 cs :
last c1 cs = c2 -> path (move rel) c1 cs ->
`d[ccut c1, ccut c2]_(move rel) + `d[ctuc c1, ctuc c2]_(move rel) <= size cs.ddc last c1 cs = c2 ->
path (move rel) c1 cs ->
`d[ccut c1, ccut c2]_(move rel) +
`d[ctuc c1, ctuc c2]_(move rel) <= size cs
Proof .f15
move => cL cPcs.de2 `d[ccut c1, ccut c2]_(move rel) +
`d[ctuc c1, ctuc c2]_(move rel) <= size cs
rewrite (@size_cut_tuc c1) //.de2 `d[ccut c1, ccut c2]_(move rel) +
`d[ctuc c1, ctuc c2]_(move rel) <=
size (rm_rep (ccut c1) [seq ccut i | i <- cs]) +
size (rm_rep (ctuc c1) [seq ctuc i | i <- cs])
apply : leq_add.
apply : gdist_path_le; first by apply : path_cut.
by rewrite last_rm_rep last_map cL.e9f
apply : gdist_path_le; first by apply : path_tuc.ea2
by rewrite last_rm_rep last_map cL.
Qed .
Lemma gpath_cut_tuc c1 c2 cs :
gpath (move rel) c1 c2 cs ->
`d[ccut c1, ccut c2]_(move rel) + `d[ctuc c1, ctuc c2]_(move rel)
<= `d[c1,c2]_(move rel).df3 gpath (move rel) c1 c2 cs ->
`d[ccut c1, ccut c2]_(move rel) +
`d[ctuc c1, ctuc c2]_(move rel) <=
`d[c1, c2]_(move rel)
Proof .f29
move => gH.df9 `d[ccut c1, ccut c2]_(move rel) +
`d[ctuc c1, ctuc c2]_(move rel) <=
`d[c1, c2]_(move rel)
rewrite (gpath_dist gH).
apply : gdist_cut_tuc => //; first apply : gpath_last gH.dfc
by apply : gpath_path gH.
Qed .
End CSet .
Section ISet .
(* Number of disks *)
Variable n : nat.
(* Subset of disks *)
Variable sd : {set disk n}.
(* Number of pegs *)
Variable k : nat.
(* Subset of pegs *)
Variable sp : {set peg k}.
(* The subset is non empty *)
Variable p0 : peg k.
Variable p0Isp : p0 \in sp.
(* relations on peg *)
Variable rel1 : rel (peg k).
Variable rel2 : rel (peg #|sp|).
Hypothesis rel_compat :
forall p1 p2 , p1 \in sp -> p2 \in sp ->
rel1 p1 p2 -> rel2 (enum_rank_in p0Isp p1) (enum_rank_in p0Isp p2).
(* Valid conf : disk in sd are on pegs in sp *)
Definition cvalid (c : configuration k n) :=
[forall i , (i \in sd) ==> (c i \in sp)].
Lemma cvalidP (c : configuration k n) :
reflect (forall i , i \in sd -> c i \in sp)
(cvalid c).1b c42 828 sp : {set peg k}
p0 : peg k
p0Isp : p0 \in sp
rel1 : rel (peg k)
rel2 : rel (peg #|sp|)
rel_compat : forall p1 p2 : ordinal_finType k,
p1 \in sp ->
p2 \in sp ->
rel1 p1 p2 ->
rel2 (enum_rank_in p0Isp p1)
(enum_rank_in p0Isp p2)
c44 reflect
(forall i : ordinal_finType n,
i \in sd -> c i \in sp) (cvalid c)
Proof .f36
apply : (iffP forallP) => [H d|H d]; first by have /implyP := H d.1b c42 828 f39 f3a f3b f3c f3d f3e c44 H : forall i : ordinal_finType n,
i \in sd -> c i \in sp
3b (d \in sd) ==> (c d \in sp)
by apply /implyP/H.
Qed .
Definition cset2 (c : configuration k n) : configuration #|sp| #|sd| :=
[ffun i => enum_rank_in p0Isp (c (enum_val i))].
Lemma on_top_cset2 c d (dIsd : d \in sd) :
cvalid c -> on_top d c -> on_top (enum_rank_in dIsd d) (cset2 c).1b c42 828 f39 f3a f3b f3c f3d f3e c44 3b c45
cvalid c ->
on_top d c -> on_top (enum_rank_in dIsd d) (cset2 c)
Proof .f48
move => /= /cvalidP cV /on_topP dO.1b c42 828 f39 f3a f3b f3c f3d f3e c44 3b c45 cV : forall i : ordinal_finType n,
i \in sd -> c i \in sp
c4c on_top (enum_rank_in dIsd d) (cset2 c)
apply /on_topP => /= d1 H.1b c42 828 f39 f3a f3b f3c f3d f3e c44 3b c45 f51 c4c c52 H : cset2 c (enum_rank_in dIsd d) = cset2 c d1
c54
rewrite leq_eqVlt; case : eqP => //= /eqP dDd1.1b c42 828 f39 f3a f3b f3c f3d f3e c44 3b c45 f51 c4c c52 f57 c59
c5a
rewrite -[d1](enum_valK_in dIsd) -sorted_enum_val !enum_rankK_in //; last first .
by apply : enum_valP.
rewrite ltn_neqAle.
case : eqP => [/eqP /val_eqP dEd1 | /eqP dDd1' /=].1b c42 828 f39 f3a f3b f3c f3d f3e c44 3b c45 f51 c4c c52 f57 c59 c6d
c6e
by case /eqP: dDd1; rewrite {2 }dEd1 enum_valK_in.
rewrite !ffunE enum_rankK_in // in H.1b c42 828 f39 f3a f3b f3c f3d f3e c44 3b c45 f51 c4c c52 c59 c72 H : enum_rank_in p0Isp (c d) =
enum_rank_in p0Isp (c (enum_val d1))
c73
apply : dO.1b c42 828 f39 f3a f3b f3c f3d f3e c44 3b c45 f51 c52 c59 c72 f75
c d = c (enum_val d1)
apply : (@enum_rank_in_inj _ _ _ _ p0Isp p0Isp) => //.
by apply : cV.
by apply /cV/enum_valP.
Qed .
Lemma move_cset2 (c1 c2 : configuration k n) :
all cvalid [::c1; c2] ->
move rel1 c1 c2 -> (cset2 c1) != (cset2 c2) ->
move rel2 (cset2 c1) (cset2 c2).1b c42 828 f39 f3a f3b f3c f3d f3e c80
all cvalid [:: c1; c2] ->
move rel1 c1 c2 ->
cset2 c1 != cset2 c2 ->
move rel2 (cset2 c1) (cset2 c2)
Proof .f86
rewrite /=.f88 [&& cvalid c1, cvalid c2 & true] ->
move rel1 c1 c2 ->
cset2 c1 != cset2 c2 ->
move rel2 (cset2 c1) (cset2 c2)
move => /= /and3P[c1V c2V _] /moveP [d [dH1 dH2 dH3 dH4]] c1Dc2.1b c42 828 f39 f3a f3b f3c f3d f3e c80 c1V : cvalid c1
c2V : cvalid c2
3b dH1 : rel1 (c1 d) (c2 d)
c95 c89 c8a c1Dc2 : cset2 c1 != cset2 c2
move rel2 (cset2 c1) (cset2 c2)
have [dIsd|dNIsd] := boolP (d \in sd); last first .1b c42 828 f39 f3a f3b f3c f3d f3e c80 f93 f94 3b f95 c95 c89 c8a f96 c91
f97
case /eqP: c1Dc2.1b c42 828 f39 f3a f3b f3c f3d f3e c80 f93 f94 3b f95 c95 c89 c8a c91
cset2 c1 = cset2 c2
f9c
apply /ffunP => i; rewrite !ffunE.1b c42 828 f39 f3a f3b f3c f3d f3e c80 f93 f94 3b f95 c95 c89 c8a c91 c9f
enum_rank_in p0Isp (c1 (enum_val i)) =
enum_rank_in p0Isp (c2 (enum_val i))
f9c
apply : enum_val_inj.fa7 enum_val (enum_rank_in p0Isp (c1 (enum_val i))) =
enum_val (enum_rank_in p0Isp (c2 (enum_val i)))
f9c
rewrite !enum_rankK_in ?(cvalidP _ c1V) ?(cvalidP _ c2V) ?enum_valP //.
apply : dH2.1b c42 828 f39 f3a f3b f3c f3d f3e c80 f93 f94 3b f95 c89 c8a c91 c9f
ca5 f9c
apply : contra dNIsd => /eqP->.1b c42 828 f39 f3a f3b f3c f3d f3e c80 f93 f94 3b f95 c89 c8a c9f
caa f9c
by apply : enum_valP.
apply /moveP; exists (enum_rank_in dIsd d ); split => /=.f9e rel2 (cset2 c1 (enum_rank_in dIsd d))
(cset2 c2 (enum_rank_in dIsd d))
- fbc
rewrite !ffunE !enum_rankK_in //.f9e rel2 (enum_rank_in p0Isp (c1 d))
(enum_rank_in p0Isp (c2 d))
fbf
by apply : rel_compat=> //; [apply : (cvalidP _ c1V) |
apply : (cvalidP _ c2V)].
- fcc
move => /= d2 dDd2.1b c42 828 f39 f3a f3b f3c f3d f3e c80 f93 f94 3b f95 c95 c89 c8a f96 c45 cc6 cc7
cset2 c1 d2 = cset2 c2 d2
fce
rewrite !ffunE.fd3 enum_rank_in p0Isp (c1 (enum_val d2)) =
enum_rank_in p0Isp (c2 (enum_val d2))
fce
congr (enum_rank_in _ _).
apply : dH2.1b c42 828 f39 f3a f3b f3c f3d f3e c80 f93 f94 3b f95 c89 c8a f96 c45 cc6 cc7
cd1 fce
rewrite -[d](enum_rankK_in dIsd) //.
by apply /eqP => /enum_val_inj /eqP; rewrite (negPf dDd2).
- fe4
by apply : on_top_cset2.
by apply : on_top_cset2.
Qed .
Lemma path_cset2 (c : configuration _ _) cs :
all cvalid (c :: cs) ->
path (move rel1) c cs ->
path (move rel2) (cset2 c) (rm_rep (cset2 c) [seq (cset2 i) | i <- cs]).1b c42 828 f39 f3a f3b f3c f3d f3e c44 ce2
all cvalid (c :: cs) ->
path (move rel1) c cs ->
path (move rel2) (cset2 c)
(rm_rep (cset2 c) [seq cset2 i | i <- cs])
Proof .fec
elim : cs c => //= c1 cs IH c => /and3P[c1V c2V c3V] /andP[cMc1 c1Pcs].1b c42 828 f39 f3a f3b f3c f3d f3e ce9 ce2 IH : forall c : configuration k n,
cvalid c && all cvalid cs ->
path (move rel1) c cs ->
path (move rel2) (cset2 c)
(rm_rep (cset2 c) [seq cset2 i | i <- cs])
c44 c1V : cvalid c
c2V : cvalid c1
c3V : all cvalid cs
cMc1 : move rel1 c c1
c1Pcs : path (move rel1) c1 cs
path (move rel2) (cset2 c)
(if cset2 c == cset2 c1
then rm_rep (cset2 c1) [seq cset2 i | i <- cs]
else
cset2 c1
:: rm_rep (cset2 c1) [seq cset2 i | i <- cs])
case : eqP => [->|/eqP cDc1 /=]; first by apply : IH; rewrite ?c2V .1b c42 828 f39 f3a f3b f3c f3d f3e ce9 ce2 ff5 c44 ff6 ff7 ff8 ff9 ffa cDc1 : cset2 c != cset2 c1
move rel2 (cset2 c) (cset2 c1) &&
path (move rel2) (cset2 c1)
(rm_rep (cset2 c1) [seq cset2 i | i <- cs])
rewrite move_cset2 => //=; first by apply : IH; rewrite ?c2V .fff [&& cvalid c, cvalid c1 & true]
by rewrite c1V c2V.
Qed .
Lemma gdist_cset2 c1 c2 cs :
all cvalid (c1 :: cs) -> last c1 cs = c2 -> path (move rel1) c1 cs ->
`d[cset2 c1, cset2 c2]_(move rel2) <= size cs.1b c42 828 f39 f3a f3b f3c f3d f3e c80 ce2
all cvalid (c1 :: cs) ->
last c1 cs = c2 ->
path (move rel1) c1 cs ->
`d[cset2 c1, cset2 c2]_(move rel2) <= size cs
Proof .1007
move => cV cL cPcs.1b c42 828 f39 f3a f3b f3c f3d f3e c80 ce2 cV : all cvalid (c1 :: cs)
cfe cPcs : path (move rel1) c1 cs
`d[cset2 c1, cset2 c2]_(move rel2) <= size cs
have := size_rm_rep (cset2 c1) [seq (cset2 i) | i <- cs].100f size (rm_rep (cset2 c1) [seq cset2 i | i <- cs]) <=
size [seq cset2 i | i <- cs] ->
`d[cset2 c1, cset2 c2]_(move rel2) <= size cs
rewrite size_map; move /(leq_trans _); apply .100f `d[cset2 c1, cset2 c2]_(move rel2) <=
size (rm_rep (cset2 c1) [seq cset2 i | i <- cs])
apply : gdist_path_le; first by apply : path_cset2.100f last (cset2 c1)
(rm_rep (cset2 c1) [seq cset2 i | i <- cs]) =
cset2 c2
by rewrite last_rm_rep last_map cL.
Qed .
Lemma gpath_cset2 c1 c2 cs :
all cvalid (c1 :: cs) -> gpath (move rel1) c1 c2 cs ->
`d[cset2 c1, cset2 c2]_(move rel2) <= `d[c1, c2]_(move rel1).1b c42 828 f39 f3a f3b f3c f3d f3e ce9 c2 : finfun_finType (ordinal_finType n)
(ordinal_finType k)
ce2 all cvalid (c1 :: cs) ->
gpath (move rel1) c1 c2 cs ->
`d[cset2 c1, cset2 c2]_(move rel2) <=
`d[c1, c2]_(move rel1)
Proof .1020
move => cV gH.1b c42 828 f39 f3a f3b f3c f3d f3e ce9 1023 ce2 1010 gH : gpath (move rel1) c1 c2 cs
`d[cset2 c1, cset2 c2]_(move rel2) <=
`d[c1, c2]_(move rel1)
rewrite (gpath_dist gH); apply : gdist_cset2 => //; first apply : gpath_last gH.1029 path (move rel1) c1 cs
by apply : gpath_path gH.
Qed .
End ISet .
Section ISet2 .
(* Number of disks *)
Variable n : nat.
(* Subset of disks *)
Variable sd : {set disk n}.
(* Number of pegs *)
Variable k : nat.
(* Subsets of pegs *)
Variables sp1 sp2 : {set peg k}.
(* The subsets are non empty *)
Variable p1 p2 : peg k.
Variable p1Isp1 : p1 \in sp1.
Variable p2Isp2 : p2 \in sp2.
(* relations on peg *)
Variable rel1 : rel (peg k).
Variable rel2 : rel (peg #|sp1|).
Variable rel3 : rel (peg #|sp2|).
Hypothesis irH : irreflexive rel1.
Hypothesis rel2_compat :
forall pi pj , pi \in sp1 -> pj \in sp1 ->
rel1 pi pj -> rel2 (enum_rank_in p1Isp1 pi) (enum_rank_in p1Isp1 pj).
Hypothesis rel3_compat :
forall pi pj , pi \in sp2 -> pj \in sp2 ->
rel1 pi pj -> rel3 (enum_rank_in p2Isp2 pi) (enum_rank_in p2Isp2 pj).
Lemma size_cset2 (c : configuration _ _) cs :
all (cvalid sd sp1) (c :: cs) ->
all (cvalid (~: sd) sp2) (c :: cs) ->
path (move rel1) c cs ->
size cs =
(size (rm_rep (cset2 sd p1Isp1 c) [seq (cset2 sd p1Isp1 i) | i <- cs]) +
size (rm_rep (cset2 (~: sd) p2Isp2 c)
[seq (cset2 (~: sd) p2Isp2 i) | i <- cs]))%nat.1b c42 828 sp1, sp2 : {set peg k}
831 p1Isp1 : p1 \in sp1
p2Isp2 : p2 \in sp2
f3c rel2 : rel (peg #|sp1|)
rel3 : rel (peg #|sp2|)
irH : irreflexive rel1
rel2_compat : forall pi pj : ordinal_finType k,
pi \in sp1 ->
pj \in sp1 ->
rel1 pi pj ->
rel2 (enum_rank_in p1Isp1 pi)
(enum_rank_in p1Isp1 pj)
rel3_compat : forall pi pj : ordinal_finType k,
pi \in sp2 ->
pj \in sp2 ->
rel1 pi pj ->
rel3 (enum_rank_in p2Isp2 pi)
(enum_rank_in p2Isp2 pj)
c44 ce2 all (cvalid sd sp1) (c :: cs) ->
all (cvalid (~: sd) sp2) (c :: cs) ->
path (move rel1) c cs ->
size cs =
size
(rm_rep (cset2 sd p1Isp1 c)
[seq cset2 sd p1Isp1 i | i <- cs]) +
size
(rm_rep (cset2 (~: sd) p2Isp2 c)
[seq cset2 (~: sd) p2Isp2 i | i <- cs])
Proof .1031
elim : cs c => //= c1 cs IH c /and3P[c1V1 c2V1 c3V1]
/and3P[c1V2 c2V2 c3V2]
/andP[/moveP[d [dH1 dH2 dH3 dH4]] c1Pcs].1b c42 828 1034 831 1035 1036 f3c 1037 1038 1039 103a 103b ce9 ce2 IH : forall c : configuration k n,
cvalid sd sp1 c && all (cvalid sd sp1) cs ->
cvalid (~: sd) sp2 c &&
all (cvalid (~: sd) sp2) cs ->
path (move rel1) c cs ->
size cs =
size
(rm_rep (cset2 sd p1Isp1 c)
[seq cset2 sd p1Isp1 i | i <- cs]) +
size
(rm_rep (cset2 (~: sd) p2Isp2 c)
[seq cset2 (~: sd) p2Isp2 i | i <- cs])
c44 c1V1 : cvalid sd sp1 c
c2V1 : cvalid sd sp1 c1
c3V1 : all (cvalid sd sp1) cs
c1V2 : cvalid (~: sd) sp2 c
c2V2 : cvalid (~: sd) sp2 c1
c3V2 : all (cvalid (~: sd) sp2) cs
3b dH1 : rel1 (c d) (c1 d)
ec6 ebc ebd ffa (size cs).+1 =
size
(if cset2 sd p1Isp1 c == cset2 sd p1Isp1 c1
then
rm_rep (cset2 sd p1Isp1 c1)
[seq cset2 sd p1Isp1 i | i <- cs]
else
cset2 sd p1Isp1 c1
:: rm_rep (cset2 sd p1Isp1 c1)
[seq cset2 sd p1Isp1 i | i <- cs]) +
size
(if
cset2 (~: sd) p2Isp2 c == cset2 (~: sd) p2Isp2 c1
then
rm_rep (cset2 (~: sd) p2Isp2 c1)
[seq cset2 (~: sd) p2Isp2 i | i <- cs]
else
cset2 (~: sd) p2Isp2 c1
:: rm_rep (cset2 (~: sd) p2Isp2 c1)
[seq cset2 (~: sd) p2Isp2 i | i <- cs])
have cdDc1d : c d != c1 d.
by have /idP/negP := irH (c d); apply : contra => /eqP {2 }->.
have [dIsd|dNIsd] := boolP (d \in sd).1b c42 828 1034 831 1035 1036 f3c 1037 1038 1039 103a 103b ce9 ce2 1042 c44 1043 1044 1045 1046 1047 1048 3b 1049 ec6 ebc ebd ffa ec7 c45
104a
rewrite ifN /= ?addSn ; last first .1057 cset2 sd p1Isp1 c != cset2 sd p1Isp1 c1
apply /eqP => /ffunP /(_ (enum_rank_in dIsd d)).1057 cset2 sd p1Isp1 c (enum_rank_in dIsd d) =
cset2 sd p1Isp1 c1 (enum_rank_in dIsd d) -> False
105f
rewrite !ffunE enum_rankK_in // => /enum_rank_in_inj => H.1b c42 828 1034 831 1035 1036 f3c 1037 1038 1039 103a 103b ce9 ce2 1042 c44 1043 1044 1045 1046 1047 1048 3b 1049 ec6 ebc ebd ffa ec7 c45 H : c d \in sp1 -> c1 d \in sp1 -> c d = c1 d
49b 105f
case /eqP : cdDc1d; apply : H; first by have /cvalidP := c1V1; apply .1b c42 828 1034 831 1035 1036 f3c 1037 1038 1039 103a 103b ce9 ce2 1042 c44 1043 1044 1045 1046 1047 1048 3b 1049 ec6 ebc ebd ffa c45
c1 d \in sp1
105f
by have /cvalidP := c2V1; apply .
rewrite ifT; last first .1057 cset2 (~: sd) p2Isp2 c == cset2 (~: sd) p2Isp2 c1
apply /eqP/ffunP=> i; rewrite !ffunE dH2 //.1b c42 828 1034 831 1035 1036 f3c 1037 1038 1039 103a 103b ce9 ce2 1042 c44 1043 1044 1045 1046 1047 1048 3b 1049 ec6 ebc ebd ffa ec7 c45 i : ordinal_finType #|~: sd|
ca5 1077
have := enum_valP i; rewrite inE.107d enum_val i \notin sd -> d != enum_val i
1077
by apply : contra => /eqP<-.
by congr (_.+1 ); apply : IH; rewrite ?c2V1 ?c2V2 .
rewrite ifT; last first .105a cset2 sd p1Isp1 c == cset2 sd p1Isp1 c1
apply /eqP/ffunP=> i; rewrite !ffunE dH2 //.1b c42 828 1034 831 1035 1036 f3c 1037 1038 1039 103a 103b ce9 ce2 1042 c44 1043 1044 1045 1046 1047 1048 3b 1049 ec6 ebc ebd ffa ec7 c91 c9f
ca5 108d
apply : contra dNIsd => /eqP->.1b c42 828 1034 831 1035 1036 f3c 1037 1038 1039 103a 103b ce9 ce2 1042 c44 1043 1044 1045 1046 1047 1048 3b 1049 ec6 ebc ebd ffa ec7 c9f
caa 108d
by have := enum_valP i.
have dd : d \in ~: sd by rewrite inE.1b c42 828 1034 831 1035 1036 f3c 1037 1038 1039 103a 103b ce9 ce2 1042 c44 1043 1044 1045 1046 1047 1048 3b 1049 ec6 ebc ebd ffa ec7 c91 dd : d \in ~: sd
108f
rewrite ifN /= ?addSn ; last first .109e cset2 (~: sd) p2Isp2 c != cset2 (~: sd) p2Isp2 c1
apply /eqP => /ffunP /(_ (enum_rank_in dd d)).109e cset2 (~: sd) p2Isp2 c (enum_rank_in dd d) =
cset2 (~: sd) p2Isp2 c1 (enum_rank_in dd d) -> False
10a4
rewrite !ffunE enum_rankK_in // => /enum_rank_in_inj => H.1b c42 828 1034 831 1035 1036 f3c 1037 1038 1039 103a 103b ce9 ce2 1042 c44 1043 1044 1045 1046 1047 1048 3b 1049 ec6 ebc ebd ffa ec7 c91 109f H : c d \in sp2 -> c1 d \in sp2 -> c d = c1 d
49b 10a4
case /eqP : cdDc1d; apply : H.1b c42 828 1034 831 1035 1036 f3c 1037 1038 1039 103a 103b ce9 ce2 1042 c44 1043 1044 1045 1046 1047 1048 3b 1049 ec6 ebc ebd ffa c91 109f
c d \in sp2
by have /cvalidP := c1V2; apply .
by have /cvalidP := c2V2; apply .
by rewrite addnS; congr (_.+1 ); apply : IH; rewrite ?c2V1 ?c2V2 .
Qed .
Lemma gdist_cset22 c1 c2 cs :
all (cvalid sd sp1) (c1 :: cs) -> all (cvalid (~: sd) sp2) (c1 :: cs) ->
last c1 cs = c2 -> path (move rel1) c1 cs ->
`d[cset2 sd p1Isp1 c1, cset2 sd p1Isp1 c2]_(move rel2) +
`d[cset2 (~: sd) p2Isp2 c1, cset2 (~: sd) p2Isp2 c2]_(move rel3)
<= size cs.1b c42 828 1034 831 1035 1036 f3c 1037 1038 1039 103a 103b c80 ce2
all (cvalid sd sp1) (c1 :: cs) ->
all (cvalid (~: sd) sp2) (c1 :: cs) ->
last c1 cs = c2 ->
path (move rel1) c1 cs ->
`d[cset2 sd p1Isp1 c1, cset2 sd p1Isp1 c2]_(move rel2) +
`d[cset2 (~: sd) p2Isp2 c1, cset2 (~: sd) p2Isp2 c2]_
(move rel3) <= size cs
Proof .10bf
move => cV1 cV2 cL cPcs.1b c42 828 1034 831 1035 1036 f3c 1037 1038 1039 103a 103b c80 ce2 cV1 : all (cvalid sd sp1) (c1 :: cs)
cV2 : all (cvalid (~: sd) sp2) (c1 :: cs)
cfe 1011 `d[cset2 sd p1Isp1 c1, cset2 sd p1Isp1 c2]_(move rel2) +
`d[cset2 (~: sd) p2Isp2 c1, cset2 (~: sd) p2Isp2 c2]_
(move rel3) <= size cs
rewrite (size_cset2 cV1 cV2) //.10c7 `d[cset2 sd p1Isp1 c1, cset2 sd p1Isp1 c2]_(move rel2) +
`d[cset2 (~: sd) p2Isp2 c1, cset2 (~: sd) p2Isp2 c2]_
(move rel3) <=
size
(rm_rep (cset2 sd p1Isp1 c1)
[seq cset2 sd p1Isp1 i | i <- cs]) +
size
(rm_rep (cset2 (~: sd) p2Isp2 c1)
[seq cset2 (~: sd) p2Isp2 i | i <- cs])
apply : leq_add.10c7 `d[cset2 sd p1Isp1 c1, cset2 sd p1Isp1 c2]_(move rel2) <=
size
(rm_rep (cset2 sd p1Isp1 c1)
[seq cset2 sd p1Isp1 i | i <- cs])
apply : gdist_path_le; first by apply : path_cset2 rel2_compat _ _ _ _.10c7 last (cset2 sd p1Isp1 c1)
(rm_rep (cset2 sd p1Isp1 c1)
[seq cset2 sd p1Isp1 i | i <- cs]) =
cset2 sd p1Isp1 c2
10d3
by rewrite last_rm_rep last_map cL.10c7 `d[cset2 (~: sd) p2Isp2 c1, cset2 (~: sd) p2Isp2 c2]_
(move rel3) <=
size
(rm_rep (cset2 (~: sd) p2Isp2 c1)
[seq cset2 (~: sd) p2Isp2 i | i <- cs])
apply : gdist_path_le; first by apply : path_cset2 rel3_compat _ _ _ _.10c7 last (cset2 (~: sd) p2Isp2 c1)
(rm_rep (cset2 (~: sd) p2Isp2 c1)
[seq cset2 (~: sd) p2Isp2 i | i <- cs]) =
cset2 (~: sd) p2Isp2 c2
by rewrite last_rm_rep last_map cL.
Qed .
Lemma gpath_cset22 c1 c2 cs :
all (cvalid sd sp1) (c1 :: cs) -> all (cvalid (~: sd) sp2) (c1 :: cs) ->
gpath (move rel1) c1 c2 cs ->
`d[cset2 sd p1Isp1 c1, cset2 sd p1Isp1 c2]_(move rel2) +
`d[cset2 (~: sd) p2Isp2 c1, cset2 (~: sd) p2Isp2 c2]_(move rel3)
<= `d[c1,c2]_(move rel1).1b c42 828 1034 831 1035 1036 f3c 1037 1038 1039 103a 103b ce9 1023 ce2
all (cvalid sd sp1) (c1 :: cs) ->
all (cvalid (~: sd) sp2) (c1 :: cs) ->
gpath (move rel1) c1 c2 cs ->
`d[cset2 sd p1Isp1 c1, cset2 sd p1Isp1 c2]_(move rel2) +
`d[cset2 (~: sd) p2Isp2 c1, cset2 (~: sd) p2Isp2 c2]_
(move rel3) <= `d[c1, c2]_(move rel1)
Proof .10e3
move => cV1 cV2 gH.1b c42 828 1034 831 1035 1036 f3c 1037 1038 1039 103a 103b ce9 1023 ce2 10c8 10c9 102a
`d[cset2 sd p1Isp1 c1, cset2 sd p1Isp1 c2]_(move rel2) +
`d[cset2 (~: sd) p2Isp2 c1, cset2 (~: sd) p2Isp2 c2]_
(move rel3) <= `d[c1, c2]_(move rel1)
rewrite (gpath_dist gH).
apply : gdist_cset22 => //; first apply : gpath_last gH.
by apply : gpath_path gH.
Qed .
End ISet2 .