Library hanoi.ghanoi
From mathcomp Require Import all_ssreflect finmap.
From hanoi Require Import extra gdist.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Section GHanoi.
Variable q : nat.
Definition peg := 'I_q.
Variable r : rel peg.
Hypothesis irH : irreflexive r.
Hypothesis symH : symmetric r.
Section Disk.
Variable n : nat.
Definition disk := 'I_n.
Definition mk_disk m (H : m < n) : disk := Ordinal H.
Definition configuration := {ffun disk → peg}.
Definition perfect p : configuration := [ffun d ⇒ p].
End Disk.
Arguments perfect [n].
Local Notation "`c[ p ] " := (perfect p)
(format "`c[ p ]", at level 5).
Definition sdisk {n} : disk n.+1 := ord0.
Lemma disk1_all (d : disk 1) : d = sdisk.
Proof. by apply/val_eqP; case: d ⇒ [] []. Qed.
Lemma configuration1_eq (c1 c2 : configuration 1) :
(c1 == c2) = (c1 sdisk == c2 sdisk).
Proof.
apply/eqP/eqP; first by move⇒ /ffunP/(_ sdisk).
by move⇒ H; apply/ffunP⇒ i; rewrite [i]disk1_all.
Qed.
Definition ldisk {n} : disk n.+1 := ord_max.
Definition on_top n (d : disk n) (c : configuration n) :=
[∀ d1 : disk n, (c d == c d1) ==> (d ≤ d1)].
Lemma on_topP n (d : disk n) (c : configuration n) :
reflect (∀ d1, c d = c d1 → d ≤ d1) (on_top d c).
Proof.
apply: (iffP forallP) ⇒ [H d1 cdEcd1|H d1].
by have /implyP->// := H d1; apply/eqP.
by apply/implyP⇒ /eqP /H.
Qed.
Definition move {n} : rel (configuration n) :=
[rel c1 c2 | [∃ d1 : disk n,
[&& r ((c1 : configuration n) d1) (c2 d1),
[∀ d2, (d1 != d2) ==> (c1 d2 == c2 d2)],
on_top d1 c1 &
on_top d1 c2]]].
Lemma moveP n (c1 c2 : configuration n) :
reflect
(∃ d1,
[/\ r (c1 d1) (c2 d1),
∀ d2, d1 != d2 → c1 d2 = c2 d2,
on_top d1 c1 &
on_top d1 c2])
(move c1 c2).
Proof.
apply: (iffP existsP) ⇒
[[d /and4P[H1 /forallP H2 H3 H4]]|[d [H1 H2 H3 H4]]]; ∃ d.
by split ⇒ // d1 H; apply/eqP/(implyP (H2 _)).
rewrite H1 H3 H4 ! andbT /=; apply/forallP ⇒ d1; apply/implyP ⇒ H.
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.
Proof.
case/moveP ⇒ d1 [H1 H2 H3 H4 H5].
rewrite (_ : d = d1); first by apply: H3.
apply/eqP; case: eqP ⇒ /eqP H //.
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.
Proof.
case/moveP ⇒ d1 [H1 H2 H3 H4 H5].
rewrite (_ : d = d1); first by apply: H4.
apply/eqP; case: eqP ⇒ /eqP H //.
by case/eqP: H5; apply: H2; rewrite eq_sym.
Qed.
Lemma move_sym n (c1 c2 : configuration n) : move c1 c2 = move c2 c1.
Proof.
by apply/moveP/moveP⇒ [] [d [H1 H2 H3 H4]];
∃ d; split; rewrite 1?symH 1?eq_sym // ⇒ e dDe; apply/sym_equal/H2.
Qed.
Lemma move_diskr n (d : disk n) (c1 c2 : configuration n) :
move c1 c2 → c1 d != c2 d → r (c1 d) (c2 d).
Proof.
case/moveP⇒ d1 [H1 H2 H3 H4] /eqP c1dDc2d.
by have [/eqP<-|/H2] := boolP (d1 == d).
Qed.
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.
Proof.
case/moveP⇒ d3 [H1 H2 H3 H4] c1d1Dc2d1 d1Dd2.
have [/eqP d3Ed1|d3Dd1] := boolP (d3 == d1); last first.
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.
Proof.
move⇒ c1Mc2 c1Dc2; rewrite eq_sym ltnNge; apply: contra ⇒ /eqP.
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.
Proof.
move⇒ c1Mc2 c1Dc2; rewrite leq_eqVlt ⇒ /orP[/val_eqP->//|dLd1].
move: (dLd1); rewrite eq_sym ltnNge (move_disk1 c1Mc2 c1Dc2) //; last first.
by rewrite neq_ltn dLd1 orbT.
apply: contra ⇒ /eqP.
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.
Proof.
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.
Proof.
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.
Definition cdisjoint m n (c1 : configuration m) (c2 : configuration n) :=
[∀ i, [∀ j, c1 i != c2 j]].
Lemma cdisjointP m n (c1 : configuration m) (c2 : configuration n) :
reflect (∀ i j, c1 i != c2 j) (cdisjoint c1 c2).
Proof.
apply: (iffP forallP) ⇒ [H i j| H i].
by move/forallP : (H i); apply.
by apply/forallP⇒ j; apply: H.
Qed.
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].
Definition crshift m n (c : configuration (m + n)) : configuration n :=
[ffun i ⇒ c (trshift m i)].
Definition clshift m n (c : configuration (m + n)) : configuration m :=
[ffun i ⇒ c (tlshift n i)].
Lemma cmergeK m n (c : configuration (m + n)) :
cmerge (clshift c) (crshift c) = c.
Proof.
apply/ffunP⇒ i; rewrite !ffunE.
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.
Proof.
case: tsplitP⇒ [j /= jE|k1 /= /eqP].
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.
Proof.
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.
Proof.
apply/on_topP/on_topP.
move⇒ Hx d2 cxEcd2.
have := Hx (trshift m d2).
by rewrite !ffunE !tsplit_trshift ⇒ /(_ cxEcd2).
move⇒ H d; rewrite !ffunE tsplit_trshift /=.
case: tsplitP ⇒ [j → H1 | k → _].
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.
Proof.
apply/moveP/moveP ⇒ [] [d1 [H1d1 H2d1 H3d1 H4d1]]; last first.
∃ (trshift n d1); split ⇒ //; try by rewrite on_top_merger.
by rewrite !ffunE /= tsplit_trshift.
move⇒ d2; rewrite !ffunE; case: tsplitP ⇒ // k d2E H.
apply: H2d1 ⇒ //; apply: contra H ⇒ /eqP→.
by apply/eqP/val_eqP/eqP.
move: H1d1; rewrite !ffunE.
case: tsplitP ⇒ [j jE H1x|k _]; last by rewrite irH.
have d1E : (trshift n j) = d1 by apply/val_eqP/eqP.
rewrite -d1E in H3d1 H4d1.
∃ j; split ⇒ //; try by rewrite -(on_top_merger _ c).
move⇒ d2 kDd2.
have := H2d1 (trshift n d2).
rewrite !ffunE tsplit_trshift ⇒ H.
apply: H.
apply: contra kDd2 ⇒ /eqP/val_eqP /=.
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.
Proof. 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).
Proof.
move⇒ /connectP[x]; rewrite -(path_merger c) ⇒ Hp Hl.
apply/connectP; eexists; first exact: Hp.
by rewrite Hl [RHS]last_map.
Qed.
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.
Proof.
move⇒ /gpath_connect[p1 p1H].
rewrite (gpath_dist p1H) -(size_map (cmerge c)).
apply: gdist_path_le; first by rewrite path_merger (gpath_path p1H).
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).
Proof.
move⇒ c1Dc2 /on_topP dTc; apply/on_topP ⇒ d1.
rewrite !ffunE tsplit_tlshift /=.
case: tsplitP ⇒ j → c1dc1j; last first.
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.
Proof.
move⇒ /on_topP dTc; apply/on_topP ⇒ d1 Hc.
have := dTc (tlshift n 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.
Proof.
move⇒ /moveP [x [H1x H2x H3x H4x]]; apply/moveP.
move: H1x; rewrite !ffunE.
case: tsplitP ⇒ [j | k kE J1x]; first by rewrite irH.
have xE : (tlshift n k) = x by apply/val_eqP/eqP.
rewrite -xE in H3x H4x.
∃ k; split ⇒ //; try by apply: on_top_mergel_inv; eassumption.
move⇒ d2 kDd2.
have := H2x (tlshift n d2).
rewrite !ffunE tsplit_tlshift ⇒ H.
apply: H.
apply: contra kDd2 ⇒ /eqP/val_eqP /=.
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).
Proof.
move⇒ c1Dc c2Dc /moveP[x [H1x H2x H3x H4x]]; apply/moveP.
∃ (tlshift n x); split ⇒ //; try by apply/on_top_mergel.
by rewrite !ffunE /= tsplit_tlshift.
move⇒ d2; rewrite !ffunE; case: tsplitP ⇒ // k d2E H.
apply: H2x ⇒ //; apply: contra H ⇒ /eqP→.
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.
Proof. 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].
Proof.
elim: cs c1 ⇒ //= c3 cs IH c1 /and3P[c1Dc2 c3Dc2 Dcs]
/andP[/move_mergel_inv ->// /IH->//].
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.
Proof.
rewrite -{1}[d](tsplitK d).
case: tsplitP ⇒ /= j dE /on_topP /= dT;
apply/on_topP ⇒ d1; rewrite !ffunE /= ⇒ H.
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).
Proof.
move⇒ /moveP [x].
rewrite -(tsplitK x).
have := @on_top_shift _ _ c1 x.
have := @on_top_shift _ _ c2 x.
case: tsplitP ⇒ /= [j xE c2H c1H [H1j H2j H3j H4j] c1Dc2|
k xE c2H c1H [H1k H2k H3k H4k] c1Dc2].
case/eqP: c1Dc2; apply/ffunP ⇒ i.
rewrite !ffunE.
apply/H2j/eqP/val_eqP; rewrite eqn_leq /= negb_and.
by rewrite orbC -ltnNge (leq_trans (ltn_ord _)) // leq_addl.
apply/moveP; ∃ k; split⇒ [|d2 kDd2||]; rewrite ?ffunE //.
- apply: H2k ⇒ /=.
by apply/eqP/val_eqP; rewrite /= eqn_add2r; apply/val_eqP/eqP.
- apply: c1H; rewrite (_ : x = (tlshift n k)) //.
by apply/val_eqP/eqP ⇒ /=.
apply: c2H; rewrite (_ : x = (tlshift n k)) //.
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).
Proof.
move⇒ /moveP [x].
rewrite -(tsplitK x).
have := @on_top_shift _ _ c1 x.
have := @on_top_shift _ _ c2 x.
case: tsplitP ⇒ /= [j xE c2H c1H [H1j H2j H3j H4j] c1Dc2|
k xE c2H c1H [H1k H2k H3k H4k] c1Dc2]; last first.
case/eqP: c1Dc2; apply/ffunP ⇒ i.
rewrite !ffunE.
apply/H2k/eqP/val_eqP; rewrite eqn_leq /= negb_and.
by rewrite -ltnNge (leq_trans (ltn_ord _)) // leq_addl.
apply/moveP; ∃ j; split⇒ [|d2 kDd2||]; rewrite ?ffunE //.
- by apply: H2j.
- apply: c1H; rewrite (_ : x = (trshift m j)) //.
by apply/val_eqP/eqP ⇒ /=.
apply: c2H; rewrite (_ : x = (trshift m j)) //.
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.
elim: s a ⇒ // b s IH a.
rewrite [rm_rep _ _]/=; case: (a == b).
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}.
Proof. by apply/mem_subseq/subseq_rm_rep. Qed.
Lemma size_rm_rep (A : eqType) (a : A) s : size (rm_rep a s) ≤ size s.
Proof. 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)).
Proof. 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).
Proof.
elim: s2 s1 a ⇒ /= [s1 a aS _|b s2 IH s1 a s1S aNIs1].
rewrite leqn0 cards_eq0; apply/eqP/setP⇒ i.
by rewrite inE; apply/idP ⇒ /aS.
case: eqP⇒ [aEb|aDb].
rewrite -aEb; apply: IH ⇒ //.
move⇒ i is1; have := is1; have := s1S _ is1; rewrite inE.
by case/orP⇒ [/eqP->|//]; rewrite -aEb ⇒ aIs1; case/negP: aNIs1.
have [bIs1|bNIs1]/= := boolP (b \in s1); last first.
apply: leq_trans (IH _ _ _ bNIs1) _ ⇒ //.
move⇒ i is1; have := is1; have := s1S _ is1; rewrite inE.
by case/orP⇒ [/eqP->|//] ⇒ bIs1; case/negP: bNIs1.
rewrite (cardsD1 b) bIs1 ltnS.
apply: IH ⇒ [i|].
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.
Proof.
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.
Proof.
elim: s1 s2 a ⇒ //= b s1 IH s2 a.
case: eqP ⇒ [aEb|aDb] /=; first by apply: IH.
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.
Proof.
elim: s a ⇒ //= c s IH a bDa; rewrite inE.
case: (boolP (b == c)) ⇒ /= [/eqP<- _|bDc bIs].
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]).
Proof.
elim: cs c ⇒ //= c1 cs IH c ⇒ /andP[cMc1 c1Pcs].
case: eqP ⇒ [->|/eqP cDc1 /=]; first by apply: IH.
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]).
Proof.
elim: cs c ⇒ //= c1 cs IH c ⇒ /andP[cMc1 c1Pcs].
case: eqP ⇒ [->|/eqP cDc1 /=]; first by apply: IH.
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.
Proof.
elim: cs c ⇒ //= c1 cs IH c /andP[/moveP[d [d2H d2H1 d2H2 d2H3]] c1Pcs].
case: (tsplitP d) ⇒ [j dE | k dE].
rewrite ifT; last first.
apply/eqP/ffunP⇒ i; rewrite !ffunE.
apply: d2H1; apply/eqP ⇒ /val_eqP /=.
by rewrite dE eqn_leq andbC leqNgt (leq_trans (ltn_ord _)) ?leq_addl.
rewrite ifN /=; last first.
apply/eqP ⇒ /ffunP /(_ j); rewrite !ffunE ⇒ cE.
move: d2H; rewrite (_ : c d = c1 d) ?(irH) //.
by rewrite (_ : d = (trshift m j)) //=; apply/val_eqP/eqP.
rewrite addnS; congr _.+1.
by apply: IH.
rewrite ifN /=; last first.
apply/eqP ⇒ /ffunP /(_ k); rewrite !ffunE ⇒ cE.
move: d2H; rewrite (_ : c d = c1 d) ?(irH) //.
by rewrite (_ : d = (tlshift n k)) //=; apply/val_eqP/eqP.
rewrite ifT; last first.
apply/eqP/ffunP⇒ i; rewrite !ffunE.
apply: d2H1; apply/eqP ⇒ /val_eqP /=.
by rewrite dE eqn_leq leqNgt (leq_trans (ltn_ord _)) ?leq_addl.
congr _.+1.
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.
Proof.
move⇒ /gpath_connect[p pH].
have := size_rm_rep (clshift c1) [seq (clshift i) | i <- p].
rewrite (gpath_dist pH) size_map; move/(leq_trans _); apply.
apply: gdist_path_le; first by apply/path_clshift/(gpath_path pH).
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.
Proof.
move⇒ /gpath_connect[p pH].
have := size_rm_rep (crshift c1) [seq (crshift i) | i <- p].
rewrite (gpath_dist pH) size_map; move/(leq_trans _); apply.
apply: gdist_path_le; first by apply/path_crshift/(gpath_path pH).
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.
Proof.
move⇒ /gpath_connect[p pH].
rewrite (gpath_dist pH) (path_shift (gpath_path pH)).
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).
apply: gdist_path_le; first by apply/path_crshift/(gpath_path pH).
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.
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.
Proof. 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.
Proof. 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.
Proof. 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).
Proof. 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.
Proof. exact: gdist_merger. Qed.
Lemma move_liftr n p (c1 c2 : configuration n) :
move ↑[c1]_p ↑[c2]_p = move c1 c2.
Proof. by exact: move_liftrn 1 p c1 c2. Qed.
Lemma perfect_liftr n p : ↑[`c[p]]_p = `c[p] :> configuration n.+1.
Proof.
apply/ffunP ⇒ i; rewrite !ffunE.
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).
Proof. by move⇒ c; apply/ffunP ⇒ i; rewrite !ffunE tsplit_trshift. Qed.
Lemma cunliftrK n (c : configuration n.+1) : ↑[↓[c]]_(c ldisk) = c.
Proof.
apply/ffunP ⇒ i; rewrite !ffunE.
case: tsplitP ⇒ [] j iE; rewrite !ffunE; congr fun_of_fin;
apply/val_eqP/eqP ⇒ //=.
by rewrite iE; case: (j) ⇒ [] [].
Qed.
Lemma cliftr_inj n p : injective (@cliftr n p).
Proof. 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).
Proof.
elim: s1 s2 ⇒ [[|] //|a s1 IH [|b s2]//=] fInj.
rewrite !eqseq_cons IH //.
case: (a =P b) ⇒ [->//|]; first by rewrite eqxx.
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).
Proof. by apply/map_eqr/cliftr_inj. Qed.
Lemma perfect_unliftr n p : ↓[`c[p]] = `c[p] :> configuration n.
Proof. 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].
Proof.
apply/fsetP⇒ i.
apply/imfsetP/imfsetP ⇒ [] [/= j].
rewrite !inE ⇒ /andP[jDn /eqP cjEp] jEi.
have jLn : j < n.
rewrite -val_eqE /= in jDn.
by have := ltn_ord j; rewrite ltnS leq_eqVlt (negPf jDn).
∃ (Ordinal jLn) ⇒ //=; rewrite !inE ffunE; apply/eqP.
by rewrite -cjEp; congr (c _); apply: val_eqP.
rewrite inE ffunE ⇒ /eqP cjEp iEj; ∃ (trshift 1 j) ⇒ //.
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.
Proof.
move⇒ H; apply/subsetP ⇒ i /mapP[j _ ->].
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].
Proof.
move⇒ c1Mc2 c10Dc20.
apply/ffunP⇒ i; rewrite !ffunE /=.
apply: move_disk1 c1Mc2 c10Dc20 _.
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.
Proof.
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.
Proof.
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.
Proof. 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.
Proof. 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 .
Proof. by apply: (@gdist_merger 1). Qed.
Lemma path_unlift_eq n (c : configuration n.+1) (cs : seq (configuration _)) :
(∀ c1, c1 \in cs → c1 ldisk = c ldisk)->
path move ↓[c] [seq ↓[i] | i <- cs] = path move c cs.
Proof.
move⇒ H.
rewrite -(@path_liftr _ (c ldisk)).
rewrite cunliftrK -map_comp.
congr path.
elim: cs H ⇒ //= a cs IH H.
rewrite -{1}(H a).
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]).
Proof. 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.
Proof. 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.
Proof.
move⇒ ir c1Cc2 c1Ec2; apply/eqP; rewrite eqn_leq gdist_cunlift // andbT.
rewrite -{1}[c1]cunliftrK -{1}[c2]cunliftrK -c1Ec2.
apply: gdist_liftr ⇒ //.
case/connectP: c1Cc2 ⇒ p pH c2E.
apply/connectP; ∃ (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).
Proof.
by apply/ffunP ⇒ i; rewrite !ffunE; case: tsplitP ⇒ j; rewrite !ffunE.
Qed.
Inductive pathS_spec (n : nat) (c : configuration n.+1)
(cs : seq (configuration n.+1)) :
∀ (b : bool), Type
:=
pathS_specW :
∀ (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 :
∀ (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.
Lemma pathSP n (c : configuration n.+1) cs : pathS_spec c cs (path move c cs).
Proof.
have [Hp|_] := boolP (path _ _ _); last by apply: pathS_spec_false.
pose f (c1 : configuration n.+1) := c1 ldisk != c ldisk.
have [Hh|/hasPn Hn] := boolP (has f cs); last first.
have csE : cs = [seq ↑[i]_(c ldisk) | i <- [seq ↓[i] | i <- cs]].
rewrite -map_comp -[LHS]map_id.
apply/eq_in_map ⇒ x /Hn; rewrite negbK ⇒ /eqP <-/=.
by rewrite cunliftrK.
apply: pathS_specW csE _.
by rewrite path_unlift_eq // ⇒ c1 /Hn; rewrite negbK ⇒ /eqP.
pose n1 := find f cs; pose lc1 := nth c cs n1.
pose p1 := c ldisk; pose p2 := lc1 ldisk.
have p1Dp2 : p1 != p2.
by have := nth_find c Hh; rewrite eq_sym.
pose c1 := ↓[c].
pose lcs1 := take n1 cs; pose cs2 := drop n1.+1 cs.
have slcs1 : size lcs1 = n1 by rewrite size_take -has_find Hh.
have Plcs1 c2 : c2 \in lcs1 → c2 ldisk = p1.
move⇒ c2Ilcs1p; move: (c2Ilcs1p).
rewrite -index_mem slcs1 ⇒ /(before_find c) /idP /negP.
rewrite negbK ⇒ /eqP.
by rewrite -[cs](cat_take_drop n1) nth_cat index_mem c2Ilcs1p nth_index.
pose cs1 := map cunliftr lcs1.
have lcs1E : lcs1 = [seq ↑[i]_p1 | i <- cs1].
rewrite -map_comp -[LHS]map_id.
apply/eq_in_map ⇒ x /Plcs1 H.
by rewrite /= -H cunliftrK.
have csE : 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.
by move: Hp; rewrite csE lcs1E cat_path /= ⇒ /and3P[].
have lc1E : lc1 = cliftr p2 (last c1 cs1).
rewrite /p2.
have Hd : (last c lcs1) ldisk != lc1 ldisk.
case: (lcs1) Plcs1 ⇒ //= a l → //.
by apply: mem_last.
rewrite last_map -[LHS]cunliftrK.
congr cliftr.
apply/ffunP⇒ i; rewrite !ffunE /=.
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.
have ->: ↑[last ↓[c] cs1]_p1 = last c lcs1.
by rewrite -[in LHS]last_map -lcs1E cunliftrK.
by rewrite -lc1E.
apply: pathS_spec_move (p1Dp2) _ _ _ (Hm1) _ ⇒ //.
- have := @move_diskr _ ldisk _ _ Hm1.
by rewrite !cliftr_ldisk; apply.
- by rewrite csE lc1E lcs1E.
- 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.
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'])]}.
Proof.
elim: cs c ⇒ /= [c _|c1 cs IH c /andP[cMc1 /IH[cs1 [c1Pcs1 lccs1Mlc1cs S]]]].
by ∃ [::]; split; rewrite ?setd_id //; apply: leqif_refl; rewrite !eqxx.
have [/eqP c1dEcd|c1dDcd] := boolP (c ldisk == c1 ldisk).
∃ (cunliftr c1 :: cs1); split⇒ //=.
by rewrite move_unliftr // cMc1.
by rewrite eqseq_cons c1dEcd cunliftrK eqxx.
have → : cunliftr c = cunliftr c1 by apply: move_ldisk.
∃ cs1; split⇒ //=.
apply/leqifP; case: eqP⇒ [H|/= _]; last by rewrite ltnS S.
by rewrite -[_.+1]/(size (c1 :: cs)) H size_map.
Qed.
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]}.
Proof.
move⇒ cPcs c1Ics c1dDcd.
have [cs1 [H1 H2 H3]] := pathS_restrict cPcs.
∃ cs1; split ⇒ //.
move/leqifP : H3; case: eqP ⇒ // cs1Ecs.
case/eqP: c1dDcd.
move: c1Ics; rewrite cs1Ecs ⇒ /mapP[x xIcs1 ->].
by rewrite cliftr_ldisk.
Qed.
Lemma connect_sym n : connect_sym (@move n).
Proof.
move⇒ c1 c2.
apply/connectP/connectP⇒ [] [p H1 H2].
∃ (rev (belast c1 p)); first by rewrite H2 path_move_rev.
by case: (p) H2 ⇒ [->//|c3 p1 _]; rewrite rev_cons last_rcons.
∃ (rev (belast c2 p)); first by rewrite H2 path_move_rev.
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 ]", only parsing, at level 5).
Lemma on_top1 k (d : disk 1) (c : configuration k 1) : on_top d c.
Proof. by apply/on_topP⇒ [] [] [] //=; case: d ⇒ [] []. Qed.
Lemma perfect_eqE n k (p1 p2 : peg k) : (`c[p1, n.+1] == `c[p2]) = (p1 == p2).
Proof.
apply/eqP/eqP ⇒ [|<-] // cp1Ecp2.
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 : ∀ 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.
Proof.
apply/on_topP/on_topP ⇒ H d; have := H d; rewrite !ffunE ⇒ H1 H2; apply: H1.
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.
Proof.
apply/moveP/moveP ⇒ [] [x [H1x H2x H3x H4x]]; ∃ x; split ⇒ //.
- by rewrite !ffunE in H1x; rewrite -r2Rr1.
- by move⇒ d2 xDd2; have := H2x _ xDd2; rewrite !ffunE ⇒ /lift_inj.
- by rewrite plift_on_top in H3x.
- by rewrite plift_on_top in H4x.
- by rewrite !ffunE r2Rr1.
- by move⇒ d2 /H2x; rewrite !ffunE ⇒ →.
- 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.
Proof.
elim: cs c1 ⇒ //= c2 cs IH c1.
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).
Proof.
move⇒ /gpath_connect [p1 p1H].
rewrite (gpath_dist p1H) -(size_map plift).
apply: gdist_path_le; first by rewrite plift_path (gpath_path p1H).
by rewrite last_map (gpath_last p1H).
Qed.
Lemma plift_perfect p1 : plift `c[p1] = `c[lift i p1].
Proof. by apply/ffunP ⇒ j; rewrite !ffunE. Qed.
Lemma cdisjoint_plift_perfect m c : cdisjoint (plift c) `c[i, m].
Proof.
apply/cdisjointP⇒ i1 j1; rewrite !ffunE /p; apply/eqP/val_eqP ⇒ /=.
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 : ∀ 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.
Proof.
apply/idP/idP⇒ H; last first.
apply: move_mergel_inv ⇒ //.
- by apply: cdisjoint_plift_perfect.
- by apply: cdisjoint_plift_perfect.
by rewrite (@plift_move _ _ _ r1).
have := move_mergel r2Irr H.
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.
Proof. 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)).
Proof.
move⇒ /connectP[x]; rewrite -(path_liftln n) ⇒ Hp Hl.
apply/connectP; eexists; first exact: Hp.
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.
Proof.
move⇒ /gpath_connect[p1 p1H].
rewrite (gpath_dist p1H) -(size_map (cliftln n p \o plift p)).
apply: gdist_path_le; first by rewrite path_liftln (gpath_path p1H).
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].
Proof. by []. Qed.
End Crlift.
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.
rewrite /opeg; case: ltngtP ⇒ H;
try by congr odflt; apply: eq_pick ⇒ p; rewrite andbC.
suff → : p1 = p2 by [].
by apply/val_eqP/eqP.
Qed.
Lemma opegDl n (p1 p2 : peg n.+3) : opeg p1 p2 != p1.
Proof.
rewrite /opeg; case: pickP ⇒ [x /andP[]//| HD].
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).
rewrite !D /= !inordK //.
by case: {HD}p1 ⇒ [] [|[|[|p1 Hp1]]] /=;
case: p2 ⇒ [] [|[|[|p2 Hp2]]].
Qed.
Lemma opegDr n (p1 p2 : peg n.+3) : opeg p1 p2 != p2.
Proof.
rewrite /opeg; case: pickP ⇒ [x /andP[]//| HD].
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).
rewrite !D /= !inordK //.
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.
Proof.
move⇒ p1Rp2 p1Dp3 p2Dp3.
apply: (@move_mergel_inv _ _ 1).
- by apply/cdisjointP ⇒ i j; rewrite !ffunE.
- by apply/cdisjointP ⇒ i j; rewrite !ffunE.
apply/moveP; ∃ ldisk; split; try by apply: on_top1.
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.
Proof.
move⇒ hirr p1Rp2 p1Dp3 p2Dp3.
apply/eqP; rewrite eqn_leq; apply/andP; split.
rewrite -[1]/(size [:: cliftr p2 `c[p3, n]]).
apply: gdist_path_le ⇒ //=.
by rewrite move_liftr_perfect.
case E : gdist ⇒ //.
move/eqP: E; rewrite gdist_eq0 ⇒ /eqP E.
have := cliftr_ldisk p1 `c[p3, n].
rewrite E cliftr_ldisk ⇒ p2Ep1.
by have := hirr p1; rewrite -{2}p2Ep1 p1Rp2.
Qed.
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.
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. by move⇒ k; rewrite /lrel /= (gtn_eqF (leqnn _)). Qed.
Definition lsym : symmetric lrel.
Proof. 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.
Proof.
elim: n c1 c2 ⇒ [c1 c2 | n IH c1 c2].
rewrite (_ : c1 = c2) ?connect0 //.
by apply/ffunP⇒ [] [].
rewrite -[c1]cunliftrK -[c2]cunliftrK.
set p1 := c1 ldisk; set p2 := c2 ldisk.
have [<-|/eqP p1Dp2] := p1 =P p2.
by apply: connect_liftr ⇒ // i; rewrite rirr.
pose p3 := opeg p1 p2.
apply: connect_trans (_ : connect _ (cliftr p1 `c[p3]) _).
apply: connect_liftr; first by apply: rirr.
by apply: IH.
apply: connect_trans (_ : connect _ (cliftr p2 `c[p3]) _); last first.
apply: connect_liftr; first by apply: rirr.
by apply: IH.
apply: connect1.
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.
Proof.
elim: n c1 c2 ⇒ [c1 c2 | n IH c1 c2].
rewrite (_ : c1 = c2) ?gdist0 //.
by apply/ffunP⇒ [] [] [].
rewrite -[c1]cunliftrK -[c2]cunliftrK.
set p1 := c1 ldisk; set p2 := c2 ldisk.
have [<-|/eqP p1Dp2] := p1 =P p2.
apply: leq_trans.
apply: gdist_liftr ⇒ [i|]; first by rewrite rirr.
apply: connect_move.
apply: leq_trans; first by apply: IH.
rewrite -ltnS !prednK ?expn_gt0 //.
by rewrite leq_exp2l.
pose p3 := opeg p1 p2.
apply: leq_trans.
apply: (@gdist_triangular _ _ _ _ (cliftr p1 `c[p3])).
rewrite expnS mul2n -addnn.
have tnP : 0 < 2 ^ n by rewrite expn_gt0.
rewrite -(prednK tnP) addSn /=.
apply: leq_add.
apply: leq_trans.
apply: gdist_liftr ⇒ [i|]; first by rewrite rirr.
by apply: connect_move.
by apply: IH.
apply: leq_trans.
apply: (@gdist_triangular _ _ _ _ (cliftr p2 `c[p3])).
rewrite gdist_liftr_perfect ?ltnS //; last 3 first.
- by apply: rirr.
- by rewrite eq_sym opegDl.
- by rewrite eq_sym opegDr.
apply: leq_trans.
apply: gdist_liftr ⇒ [i|]; first by rewrite rirr.
by apply: connect_move.
by apply: IH.
Qed.
Definition sorted (s : seq nat) :=
∀ 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.
Proof. 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.
move⇒ i1 j1; rewrite size_iota ⇒ i1Lj j1Lj.
by rewrite !nth_iota // ltn_add2l.
Qed.
Lemma sorted_skip a b s : sorted (a :: b :: s) → sorted (a :: s).
Proof.
move⇒ Hs [|i] [|j] iH jH //=; first by rewrite ltnn.
- by rewrite (Hs 0 j.+2).
- 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).
Proof.
have F a s1 i :
sorted (a :: s1) → i < size (filter p s1) → a < nth 0 (filter p s1) i.
elim: s1 i ⇒ //= b s1 IH i abS.
have [pbT|pbF] := boolP (p b).
case: i ⇒ [|i1] /= sH; first by rewrite (abS 0 1).
apply: IH ⇒ //.
by apply: sorted_skip abS.
apply: IH.
by apply: sorted_skip abS.
elim: s ⇒ //= a s IH aS.
have sS := sorted_cons aS.
have [paT|paF] := boolP (p a); last by apply: IH.
move⇒ [|i] [|j] iH jH /=.
- by rewrite ltnn.
- by rewrite F.
- 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].
Proof.
rewrite -val_ord_enum -map_comp /=.
rewrite enumT unlock /=.
elim: (ord_enum _) ⇒ //= a l <-.
by rewrite inord_val.
Qed.
Lemma sorted_enum_val (m : nat) (s : {set 'I_m}) (i j : 'I_#|s|) :
(enum_val i) < (enum_val j) = (i < j).
Proof.
case: m s i j ⇒ [s|m s i j].
rewrite (_ : s = set0).
case⇒ m H j; apply: False_ind.
by rewrite cards0 in H.
by apply/setP⇒ [] [].
have := ltn_ord i; have := ltn_ord j; rewrite {2 4}cardE.
rewrite /enum_val /= /(enum _) -enumT enum_ord_inord ⇒ iL jL.
have <-// := @nth_map ('I_m.+1) (enum_default i) nat 0 (@nat_of_ord m.+1).
have <-// := @nth_map ('I_m.+1) (enum_default j) nat 0 (@nat_of_ord m.+1).
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)).
elim: k2 k1 ⇒ //= k2 IH k1 k1k2Lm.
case: (_ \in _) ⇒ //=.
rewrite inordK //.
rewrite IH //.
by rewrite addSnnS.
by apply: leq_trans k1k2Lm; rewrite -addSnnS leq_addr.
apply: IH.
by rewrite addSnnS.
rewrite F //.
have : 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.
apply: sorted_filter ⇒ //.
by apply: sorted_iota.
Qed.
Section ISetd.
Variable n : nat.
Variable sd : {set disk n}.
Variable k : nat.
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).
Proof.
move⇒ /= /on_topP dO.
apply/on_topP ⇒ /= d1 H.
rewrite leq_eqVlt; case: eqP ⇒ //= /eqP dDd1.
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' /=].
by case/eqP: dDd1; rewrite {2}dEd1 enum_valK_in.
rewrite !ffunE enum_rankK_in // in H.
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).
Proof.
move ⇒ /moveP [d [dH1 dH2 dH3 dH4]] c1Dc2.
have [dIsd|dNIsd] := boolP (d \in sd); last first.
case/eqP: c1Dc2.
apply/ffunP ⇒ i; rewrite !ffunE.
apply: dH2.
apply: contra dNIsd ⇒ /eqP→.
by apply: enum_valP.
apply/moveP; ∃ (enum_rank_in dIsd d); split ⇒ /=.
- by rewrite !ffunE !enum_rankK_in //.
- move⇒ /= d2 dDd2.
rewrite !ffunE.
apply: dH2.
rewrite -[d](enum_rankK_in dIsd) //.
by apply /eqP ⇒ /enum_val_inj /eqP; rewrite (negPf dDd2).
- 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]).
Proof.
elim: cs c ⇒ //= c1 cs IH c ⇒ /andP[cMc1 c1Pcs].
case: eqP ⇒ [->|/eqP cDc1 /=]; first by apply: IH; rewrite ?c2V.
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.
Proof.
move⇒ cL cPcs.
have := size_rm_rep (cset c1) [seq (cset i) | i <- cs].
rewrite size_map; move/(leq_trans _); apply.
apply: gdist_path_le; first by apply: path_cset.
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).
Proof.
move⇒ gH.
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.
Variable n : nat.
Variable t : nat.
Variable tLn : t ≤ n.
Variable k : nat.
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.
Proof. 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.
Proof.
move⇒ H; apply/subsetP ⇒ i /mapP[j _ ->].
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].
Proof.
apply/fsetP⇒ /= i.
apply/imfsetP/imfsetP ⇒ [] /= [j]; rewrite !inE.
case/andP ⇒ cjEp jLt →.
by ∃ (Ordinal jLt); rewrite //= inE !ffunE ordinalK.
rewrite !ffunE ⇒ cjEp ->; ∃ (widen_ord tLn j) ⇒ //=.
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).
Proof.
move⇒ /= /on_topP dO.
apply/on_topP ⇒ /= d1 H.
rewrite leq_eqVlt; case: eqP ⇒ //= /eqP dDd1.
rewrite ltn_neqAle dDd1 /=.
apply: (dO (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).
Proof.
move ⇒ /moveP [d [dH1 dH2 dH3 dH4]] c1Dc2.
have [dLt|tLd] := leqP t d.
case/eqP: c1Dc2.
apply/ffunP ⇒ i; rewrite !ffunE.
apply: dH2.
by rewrite -val_eqE /= neq_ltn (leq_trans _ dLt) // orbT.
apply/moveP; ∃ (Ordinal tLd); split ⇒ /=.
- by rewrite !ffunE // ordinalK.
- move⇒ /= d2; rewrite !ffunE -val_eqE /= ⇒ dDd2.
by apply: dH2; rewrite -val_eqE /=.
- 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]).
Proof.
elim: cs c ⇒ //= c1 cs IH c ⇒ /andP[cMc1 c1Pcs].
case: eqP ⇒ [->|/eqP cDc1 /=]; first by apply: IH; rewrite ?c2V.
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.
Proof.
move⇒ cL cPcs.
have := size_rm_rep (ccut c1) [seq (ccut i) | i <- cs].
rewrite size_map; move/(leq_trans _); apply.
apply: gdist_path_le; first by apply: path_cut.
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).
Proof.
move⇒ gH.
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.
Proof. 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.
Proof.
move⇒ iLn tLi; apply: ltn_sub2r ⇒ //.
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.
Proof. 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).
Proof.
move⇒ /= /on_topP dO.
apply/on_topP ⇒ /= d1 H.
rewrite leq_eqVlt; case: eqP ⇒ //= /eqP dDd1.
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).
Proof.
move ⇒ /moveP [d [dH1 dH2 dH3 dH4]] c1Dc2.
have [dLt|tLd] := leqP t d; last first.
case/eqP: c1Dc2.
apply/ffunP ⇒ i; rewrite !ffunE.
apply: dH2.
by rewrite -val_eqE /= neq_ltn (leq_trans tLd _) // leq_addl.
apply/moveP; ∃ (otuc dLt); split ⇒ /=.
- by rewrite !ffunE // otucK.
- move⇒ /= d2; rewrite !ffunE -val_eqE /= ⇒ dDd2.
by apply: dH2; rewrite -val_eqE /= -(subnK dLt) eqn_add2r.
- 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]).
Proof.
elim: cs c ⇒ //= c1 cs IH c ⇒ /andP[cMc1 c1Pcs].
case: eqP ⇒ [->|/eqP cDc1 /=]; first by apply: IH; rewrite ?c2V.
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.
Proof.
move⇒ cL cPcs.
have := size_rm_rep (ctuc c1) [seq (ctuc i) | i <- cs].
rewrite size_map; move/(leq_trans _); apply.
apply: gdist_path_le; first by apply: path_tuc.
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).
Proof.
move⇒ gH.
rewrite (gpath_dist gH); apply: gdist_tuc ⇒ //; first apply: gpath_last gH.
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.
Proof.
elim: cs c ⇒ //= c1 cs IH c /andP[/moveP[d [dH1 dH2 dH3 dH4]] c1Pcs].
have cdDc1d : c d != c1 d.
by have /idP/negP := irH (c d); apply: contra ⇒ /eqP {2}->.
have [tLd|dLt] := leqP t d; last first.
rewrite ifN /= ?addSn; last first.
apply/eqP ⇒ /ffunP /(_ (Ordinal dLt)).
by rewrite !ffunE ordinalK ⇒ /eqP; rewrite (negPf cdDc1d).
rewrite ifT; last first.
apply/eqP/ffunP⇒ i; rewrite !ffunE dH2 //=.
apply/eqP ⇒ /val_eqP.
by rewrite /= eqn_leq [_ ≤ d]leqNgt (leq_trans dLt) ?andbF // leq_addl.
by congr (_.+1); apply: IH.
rewrite ifT; last first.
apply/eqP/ffunP⇒ i; rewrite !ffunE dH2 //.
by apply/eqP ⇒ /val_eqP; rewrite /= eqn_leq leqNgt (leq_trans (ltn_ord _)).
rewrite ifN /= ?addSn; last first.
apply/eqP ⇒ /ffunP /(_ (otuc tLd)) /eqP.
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.
Proof.
move⇒ cL cPcs.
rewrite (@size_cut_tuc c1) //.
apply: leq_add.
apply: gdist_path_le; first by apply: path_cut.
by rewrite last_rm_rep last_map cL.
apply: gdist_path_le; first by apply: path_tuc.
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).
Proof.
move⇒ gH.
rewrite (gpath_dist gH).
apply: gdist_cut_tuc ⇒ //; first apply: gpath_last gH.
by apply: gpath_path gH.
Qed.
End CSet.
Section ISet.
Variable n : nat.
Variable sd : {set disk n}.
Variable k : nat.
Variable sp : {set peg k}.
Variable p0 : peg k.
Variable p0Isp : p0 \in sp.
Variable rel1 : rel (peg k).
Variable rel2 : rel (peg #|sp|).
Hypothesis rel_compat :
∀ p1 p2, p1 \in sp → p2 \in sp →
rel1 p1 p2 → rel2 (enum_rank_in p0Isp p1) (enum_rank_in p0Isp p2).
Definition cvalid (c : configuration k n) :=
[∀ i, (i \in sd) ==> (c i \in sp)].
Lemma cvalidP (c : configuration k n) :
reflect (∀ i, i \in sd → c i \in sp)
(cvalid c).
Proof.
apply: (iffP forallP) ⇒ [H d|H d]; first by have /implyP := H d.
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).
Proof.
move⇒ /= /cvalidP cV /on_topP dO.
apply/on_topP ⇒ /= d1 H.
rewrite leq_eqVlt; case: eqP ⇒ //= /eqP dDd1.
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' /=].
by case/eqP: dDd1; rewrite {2}dEd1 enum_valK_in.
rewrite !ffunE enum_rankK_in // in H.
apply: dO.
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).
Proof.
rewrite /=.
move⇒ /= /and3P[c1V c2V _] /moveP [d [dH1 dH2 dH3 dH4]] c1Dc2.
have [dIsd|dNIsd] := boolP (d \in sd); last first.
case/eqP: c1Dc2.
apply/ffunP ⇒ i; rewrite !ffunE.
apply: enum_val_inj.
rewrite !enum_rankK_in ?(cvalidP _ c1V) ?(cvalidP _ c2V) ?enum_valP //.
apply: dH2.
apply: contra dNIsd ⇒ /eqP→.
by apply: enum_valP.
apply/moveP; ∃ (enum_rank_in dIsd d); split ⇒ /=.
- rewrite !ffunE !enum_rankK_in //.
by apply: rel_compat⇒ //; [apply: (cvalidP _ c1V) |
apply: (cvalidP _ c2V)].
- move⇒ /= d2 dDd2.
rewrite !ffunE.
congr (enum_rank_in _ _).
apply: dH2.
rewrite -[d](enum_rankK_in dIsd) //.
by apply /eqP ⇒ /enum_val_inj /eqP; rewrite (negPf dDd2).
- 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]).
Proof.
elim: cs c ⇒ //= c1 cs IH c ⇒ /and3P[c1V c2V c3V] /andP[cMc1 c1Pcs].
case: eqP ⇒ [->|/eqP cDc1 /=]; first by apply: IH; rewrite ?c2V.
rewrite move_cset2 ⇒ //=; first by apply: IH; rewrite ?c2V.
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.
Proof.
move⇒ cV cL cPcs.
have := size_rm_rep (cset2 c1) [seq (cset2 i) | i <- cs].
rewrite size_map; move/(leq_trans _); apply.
apply: gdist_path_le; first by apply: path_cset2.
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).
Proof.
move⇒ cV gH.
rewrite (gpath_dist gH); apply: gdist_cset2 ⇒ //; first apply: gpath_last gH.
by apply: gpath_path gH.
Qed.
End ISet.
Section ISet2.
Variable n : nat.
Variable sd : {set disk n}.
Variable k : nat.
Variables sp1 sp2 : {set peg k}.
Variable p1 p2 : peg k.
Variable p1Isp1 : p1 \in sp1.
Variable p2Isp2 : p2 \in sp2.
Variable rel1 : rel (peg k).
Variable rel2 : rel (peg #|sp1|).
Variable rel3 : rel (peg #|sp2|).
Hypothesis irH : irreflexive rel1.
Hypothesis rel2_compat :
∀ 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 :
∀ 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.
Proof.
elim: cs c ⇒ //= c1 cs IH c /and3P[c1V1 c2V1 c3V1]
/and3P[c1V2 c2V2 c3V2]
/andP[/moveP[d [dH1 dH2 dH3 dH4]] c1Pcs].
have cdDc1d : c d != c1 d.
by have /idP/negP := irH (c d); apply: contra ⇒ /eqP {2}->.
have [dIsd|dNIsd] := boolP (d \in sd).
rewrite ifN /= ?addSn; last first.
apply/eqP ⇒ /ffunP /(_ (enum_rank_in dIsd d)).
rewrite !ffunE enum_rankK_in // ⇒ /enum_rank_in_inj ⇒ H.
case/eqP : cdDc1d; apply: H; first by have /cvalidP := c1V1; apply.
by have /cvalidP := c2V1; apply.
rewrite ifT; last first.
apply/eqP/ffunP⇒ i; rewrite !ffunE dH2 //.
have := enum_valP i; rewrite inE.
by apply: contra ⇒ /eqP<-.
by congr (_.+1); apply: IH; rewrite ?c2V1 ?c2V2.
rewrite ifT; last first.
apply/eqP/ffunP⇒ i; rewrite !ffunE dH2 //.
apply: contra dNIsd ⇒ /eqP→.
by have := enum_valP i.
have dd : d \in ~: sd by rewrite inE.
rewrite ifN /= ?addSn; last first.
apply/eqP ⇒ /ffunP /(_ (enum_rank_in dd d)).
rewrite !ffunE enum_rankK_in // ⇒ /enum_rank_in_inj ⇒ H.
case/eqP : cdDc1d; apply: H.
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.
Proof.
move⇒ cV1 cV2 cL cPcs.
rewrite (size_cset2 cV1 cV2) //.
apply: leq_add.
apply: gdist_path_le; first by apply: path_cset2 rel2_compat _ _ _ _.
by rewrite last_rm_rep last_map cL.
apply: gdist_path_le; first by apply: path_cset2 rel3_compat _ _ _ _.
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).
Proof.
move⇒ cV1 cV2 gH.
rewrite (gpath_dist gH).
apply: gdist_cset22 ⇒ //; first apply: gpath_last gH.
by apply: gpath_path gH.
Qed.
End ISet2.