1 files changed, 54 insertions, 0 deletions
diff --git a/src/Problem7.agda b/src/Problem7.agda
new file mode 100644
index 0000000..4566abb
--- /dev/null
+++ b/src/Problem7.agda
@@ -0,0 +1,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)