{-# 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)