Library hanoi.ghanoi3

From mathcomp Require Import all_ssreflect.
From hanoi Require Import ghanoi gdist.

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

Section GHanoi3.

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

Lemma peg3E p : [\/ p = peg1 , p = peg2 | p = peg3 ].
Proof.
by case: p ⇒ [] [|[|[|]]] // H; [apply: Or31|apply: Or32|apply: Or33];
   apply/val_eqP; rewrite //= inordK.
Qed.

Lemma opeg3E p p1 p2 : p1 != p2 → (`p [p1 , p2 ] == p ) = ((p1 != p ) && (p2 != p )).
Proof.
move⇒ p1Dp2.
have D p3 p4 : (p3 == p4 ) = (val p3 == val p4 ).
  by apply/eqP/idP ⇒ /val_eqP.
move: p1Dp2 (opegDl p1 p2) (opegDr p1 p2).
by case: (peg3E (opeg p1 p2)) ⇒ ->;
   case: (peg3E p1) ⇒ ->;
   case: (peg3E p2) ⇒ ->;
   case: (peg3E p) ⇒ ->;
   rewrite !D /peg1 /peg2 /peg3 /= ?inordK.
Qed.

Lemma opeg3Kl p p1 p2 : p1 != p2 → `p [`p [p1 , p2 ], p1 ] = p2.
Proof.
move⇒ p1Dp2; apply/eqP.
by rewrite !opeg3E ?(eqxx, p1Dp2) // [in p2 != p1]eq_sym p1Dp2.
Qed.

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

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

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

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

Lemma move_perfectr n (c1 c2 : configuration 3 n.+1) :
  c1 `--> c2 → c1 ldisk != c2 ldisk → ↓[c2 ] = `c [`p [c1 ldisk , c2 ldisk ]].
Proof.
move⇒ c1Mc2 c1lDc2l.
apply/ffunP ⇒ i; rewrite !ffunE.
have /ffunP/(_ i) := move_ldisk c1Mc2 c1lDc2l; rewrite !ffunE ⇒ c1Ec2.
apply/sym_equal/eqP; rewrite opeg3E //; apply/andP; split.
  rewrite -c1Ec2 /=; apply/eqP ⇒ c1lEc1r.
  have /on_topP /(_ _ c1lEc1r) := move_on_topl c1Mc2 c1lDc2l.
  by rewrite /= leqNgt ltn_ord.
apply/eqP ⇒ c2lEc2r.
have /on_topP /(_ _ c2lEc2r):= move_on_topr c1Mc2 c1lDc2l.
by rewrite /= leqNgt ltn_ord.
Qed.

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

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

Lemma path3SP n (c : _ _ n.+1) cs : path3S_spec c cs (path hmove c cs).
Proof.
case: pathSP⇒ //; try by constructor.
move⇒ p1 p2 cs1 cs2 c1 c2 p1Dp2 p1Rp2 csE c1Pcs1 lMc2 c2Pcs2.
have lc1cs1E : last c1 cs1 = `c [`p [p1, p2]].
  have := move_perfectl lMc2.
  by rewrite !cliftr_ldisk cliftrK; apply.
apply: path3S_spec_move (lc1cs1E) _ _ _ ⇒ //.
- by rewrite csE; congr (_ ++ cliftr _ _ :: _).
by rewrite -lc1cs1E.
Qed.

End GHanoi3.