blob: 4566abb16040276b23a894b3066039d418ec15b3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
|
{-# OPTIONS --safe #-}
module Problem7 where
open import Data.Product
open import Data.Nat
open import Data.Nat.Properties using (+-comm)
open import Function.Base using (_∘_)
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Nullary
repeat : ∀{A : Set}(f : A → A) → ℕ → A → A
repeat f zero x = x
repeat f (suc n) x = f (repeat f n x)
-- `repeat f` commutes with `g` if `f` commutes with `g`
repeat-comm :
{A : Set} (f g : A → A) (comm : f ∘ g ≗ g ∘ f) (n : ℕ) →
repeat f n ∘ g ≗ g ∘ repeat f n
repeat-comm f g comm zero x = refl
repeat-comm f g comm (suc n) x =
trans
(cong f (repeat-comm f g comm n x))
(comm (repeat f n x))
module _ (T : Set)(f : T → T) where
hare tortoise : T × T → T × T
hare p = ( proj₁ p , f (proj₂ p) )
tortoise p = ( f (proj₁ p) , proj₂ p )
data Run : T × T → (length : ℕ) → Set where
empty : ∀{c} → Run (c , c) 0
step : ∀{n}{p} → Run (tortoise p) n → Run p (suc n)
Loop : ℕ → Set
Loop n = ∃[ i ] Run (i , i) n
race : T × T → T × T
race p = hare (hare (tortoise p))
-- The invariant for the race.
invariant : (x : T) (n : ℕ) → Run (repeat race n (x , x)) n
invariant x zero = empty
invariant x (suc n) =
let run = invariant (f (f x)) n in
step (subst (λ - → Run - n)
(repeat-comm race (tortoise ∘ race) (λ _ → refl) n (x , x))
run)
goal : ∀{x c : T} n → repeat race n (x , x) ≡ (c , c) → Loop n
goal {x} n prf = -, subst (λ - → Run - n) prf (invariant x n)
|
