Skip to content

Instantly share code, notes, and snippets.

@fetburner
Created May 20, 2020 10:07
Show Gist options
  • Save fetburner/7fec993afc9e4a7d037e1eb90721ec8a to your computer and use it in GitHub Desktop.
Save fetburner/7fec993afc9e4a7d037e1eb90721ec8a to your computer and use it in GitHub Desktop.
フロイドの循環検出アルゴリズム
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment