フロイドの循環検出アルゴリズム

CycleDetection.v

Require Import ssreflect Nat Arith Lia.

Lemma iter_S A f : forall m x,
  @Nat.iter m A f (f x) = Nat.iter (S m) f x.
Proof. elim => //= ? IH ?. by rewrite IH. Qed.

Lemma iter_plus A f n x : forall m,
  @Nat.iter (m + n) A f x = Nat.iter m f (Nat.iter n f x).
Proof. by elim => //= ? ->. Qed.

(* P(n)を満たす最小の自然数nを線形探索する *)
Lemma nat_eps (P : nat -> Prop)
  (Hdec : forall n, { P n } + { ~ P n })
  (Hex : exists n, P n) :
  { n | P n & forall n', P n' -> n <= n' }.
Proof.
  refine (@Fix _
    (fun n m => S m = n /\ (forall m, m < n -> ~ P m)) _
    (fun n => (forall m, m < n -> ~ P m) -> { n | P n & forall n', P n' -> n <= n' })
    (fun n eps HnP =>
       match Hdec n with
       | left _ => exist2 _ _ n _ (fun n' => _)
       | right _ => let Hlb := fun m => _ in eps (S n) _ Hlb
       end) 0 _); eauto.
  Unshelve.
  - case Hex => n Hp m.
    remember (n - m) as d.
    generalize dependent m.
    induction d as [ | ? ] => m ?; constructor => ? [ ? Hnp ]; subst.
    + (have : (n < S m) by lia) => /Hnp. congruence.
    + apply /IHd. lia.
  - by case (le_lt_dec n n') => // Hlt /(HnP _ Hlt).
  - lia.
  - move => /le_S_n ?.
    case (Nat.eq_dec m n) => [ -> // | ? ].
    apply /HnP. lia.
Defined.

Section CycleDetection.
  Variable A : Set.
  Variable f : A -> A.
  Variable eq_dec : forall x y : A, { x = y } + { x <> y }.

  Definition eventually_periodic m0 l n : Prop :=
    l > 0 /\ forall m, m0 <= m -> iter (l + m) f n = iter m f n.

  Theorem tortoise_and_hare v
    (Hperiod : exists m l, eventually_periodic m l v /\ forall m' l', eventually_periodic m' l' v -> m <= m' /\ l <= l') :
    {'(m, l) | eventually_periodic m l v /\ forall m' l', eventually_periodic m' l' v -> m <= m' /\ l <= l' }.
  Proof.
    refine
      (let (m, Hm, _) :=
           (* ウサギとカメ *)
           nat_eps (fun m => @iter (S m + S m) _ f v = @iter (S m) _ f v)
                   (fun m => eq_dec (@iter (S m + S m) _ f v) (@iter (S m) _ f v)) _ in
       let (mu, Hmu, Hmu') :=
           (* ループの開始地点を見つける *)
           nat_eps (fun mu => @iter (S m + mu) _ f v = @iter mu _ f v)
                   (fun mu => eq_dec (@iter (S m + mu) _ f v) (@iter mu _ f v)) _ in
       let (l, Hl, Hl') :=
           (* ループの周期を測る *)
           nat_eps (fun l => @iter (S l + mu) _ f v = @iter mu _ f v)
                   (fun l => eq_dec (@iter (S l + mu) _ f v) (@iter mu _ f v)) _ in
       exist _ (mu, S l) _);
    move: Hperiod => [ mu' [ l' [ [ Hpos Hperiod ] Hleast ] ] ]; eauto.
    { exists ((mu' + 2) * l' - 1).
      set j := (mu' + 2) * l' - 1.
      have->: S j + S j = (mu' + 2) * l' + S j by lia.
      elim: (mu' + 2) => [ // | ? ? /= ].
      rewrite -plus_assoc Hperiod //. nia. }
    have : eventually_periodic mu (S l) v => [ | /Hleast [ ? Hlel ] ].
    { split => [ | m0 ? ]; auto with arith.
      have->: m0 = (m0 - mu) + mu by lia.
      have->: S l + (m0 - mu + mu) = (m0 - mu) + (S l + mu) by lia.
      by rewrite !(@iter_plus _ _ _ _ (m0 - mu)) Hl. }
    have : eventually_periodic mu (S m) v => [ | /Hleast [ Hlemu Hlem ] ].
    { split => [ | m0 ? ]; auto with arith.
      have->: m0 = (m0 - mu) + mu by lia.
      have->: S m + (m0 - mu + mu) = (m0 - mu) + (S m + mu) by lia.
      by rewrite !(@iter_plus _ _ _ _ (m0 - mu)) Hmu. }
    case (zerop (S m mod l')) => Hmod.
    - have : mu <= mu' => [ | /(le_antisym _ _ Hlemu) ? ]; subst.
      { apply /Hmu'.
        rewrite (Nat.div_mod (S m) l'). { lia. }
        rewrite Hmod -plus_n_O mult_comm.
        elim: (S m / l') => //= ? IH.
        by rewrite -plus_assoc iter_plus IH -iter_plus Hperiod. }
      have : S l <= l' => [ | /(le_antisym _ _ Hlel) <- // ].
      { rewrite (S_pred_pos l') //.
        apply /le_n_S /Hl'.
        by rewrite -S_pred_pos // Hperiod. }
    - have : forall i, i * l' <= S m -> iter (S m - i * l' + mu) f v = iter mu f v => [ | /(_ (S m / l')) ].
      { elim => // i IH ?.
        rewrite -IH. { lia. }
        have->: S m - i * l' + mu = l' + (S m - S i * l' + mu) by lia.
        rewrite Hperiod //. lia. }
      rewrite (mult_comm _ l') -Nat.mod_eq => [ | Hperiod' ]. { lia. }
      have : eventually_periodic mu (S m mod l') v => [ | /Hleast [ ? /le_not_lt [ ] ] ].
      { split => [ // | m0 ? ].
        have->: m0 = (m0 - mu) + mu by lia.
        have->: S m mod l' + (m0 - mu + mu) = (m0 - mu) + (S m mod l' + mu) by lia.
        rewrite !(@iter_plus _ _ _ _ (m0 - mu)) Hperiod' //.
        apply /Nat.mul_div_le. lia. }
      apply /Nat.mod_upper_bound. lia.
  Defined.
End CycleDetection.