---------------------------------------------------
             EXECUTING PROOFS AS COMPUTER PROGRAMS
      ---------------------------------------------------

               Uniform Continuity in Type Theory
               ---------------------------------

                         Chuangjie Xu

           14-16 Monday 20th November 2017, HS B 252

          http://www.math.lmu.de/~xu/teaching/agda17/

---------------------
    Preliminaries
---------------------

Import the minimal library for today's lecture

\begin{code}

open import Preliminaries

\end{code}

------------------------------------------------------------
    Two formulations of the uniform-continuity principle
------------------------------------------------------------

\begin{code}

CH-UC : Type
CH-UC = (f : 𝟚ᴺ  )  Σ \(n : )  (α β : 𝟚ᴺ)  α ≡[ n ] β  f α  f β

UC : Type
UC = (f : 𝟚ᴺ  )   (Σ \(n : )  (α β : 𝟚ᴺ)  α ≡[ n ] β  f α  f β) 

\end{code}

-------------------------------------------
    The two formulations are equivalent
-------------------------------------------

One direction is easy.

\begin{code}

Theorem[CH-UC→UC] : CH-UC  UC
Theorem[CH-UC→UC] chuc f =  chuc f 

\end{code}

For the converse, we need the following:

MainLemma. For any type family A : ℕ → Type such that

    (1) A(n) is a proposition for all n,

    (2) if A(n) then A(m) is decidable for all i < n,

  we have

      ∥ Σ(n:ℕ).A(n) ∥ → Σ(n:ℕ).A(n).

Proof sketch: Given n with A(n), we can find the minimal k with A(k),
using the decidability of A(m) for m < n. Since “having a minimal k
with A(k)” is a proposition (proved using function extensionality),
the elimination rule of ∥-∥ gives the desired result.

\begin{code}

MainLemma : (A :   Type)
           ((n : )  isProp (A n))
           ((n : )  A n  (m : )  m  n  A m + ¬ (A m))
            (Σ \(n : )  A n)   Σ \(n : )  A n
MainLemma A pA dA h = claim₂ (claim₁ h)
 where
  claim₀ : (Σ \(n : )  A n)  Σ-min \(k : )  A k
  claim₀ (n , an) = Lemma[Σ-min] A n an (dA n an)
  claim₁ :  (Σ \(n : )  A n)   Σ-min \(k : )  A k
  claim₁ = ∥∥-elim (Σ-min-isProp A pA) claim₀
  claim₂ : (Σ-min \(k : )  A k)  Σ \(n : )  A n
  claim₂ (k , ak , _) = k , ak

\end{code}

Since Uc(f) : ℕ → Type, defined by

  Uc(f,n) = (α β : 𝟚ᴺ) → α ≡[ n ] β → f α ≡ f β

satisfies (1) and (2), with the aid of function extensionality, the
two formulations of the uniform-continuity principle are equivalent.

\begin{code}

Uc : (𝟚ᴺ  )    Type
Uc f n = (α β : 𝟚ᴺ)  α ≡[ n ] β  f α  f β

Uc-isProp : (f : 𝟚ᴺ  )
           (n : )  isProp (Uc f n)
Uc-isProp f n p q = funext  α  funext  β  funext  en  ℕ-isSet (p α β en) (q α β en))))

Uc-≤-decidable : (f : 𝟚ᴺ  )
                (n : )  Uc f n  (m : )  m  n  Uc f m + ¬ (Uc f m)
Uc-≤-decidable f  0       u0  _ _ = inl  α β _  u0 α β ≡[zero])
Uc-≤-decidable f (succ n) usn m r = case c₀ c₁ (Lemma[n≤m+1→n≤m∨n≡m+1] r)
 where
  c₀ : m  n  Uc f m + ¬ (Uc f m)
  c₀ r' = case sc₀ sc₁ ds
   where
    ds : ((s : 𝟚^ n)  f (s * )  f (s * )) + ¬ ((s : 𝟚^ n)  f (s * )  f (s * ))
    ds = Lemma[𝟚^-dec] n  _  ℕ-discrete)
    sc₀ : ((s : 𝟚^ n)  f (s * )  f (s * ))  Uc f m + ¬ (Uc f m)
    sc₀ ψ = Uc-≤-decidable f n un m r'
     where
      un : (α β : 𝟚ᴺ)  α ≡[ n ] β  f α  f β
      un α β en = case d₀ d₁ 𝟚-discrete
       where
        d₀ : α n  β n  f α  f β
        d₀ e = usn α β (≡[succ]' en e)
        d₁ : α n  β n  f α  f β
        d₁ g = case sd₀ sd₁ 𝟚-discrete
         where
          s : 𝟚^ n
          s = take n α
          sd₀ : α n  𝟎  f α  f β
          sd₀ eαn = trans claim₁ (trans (ψ s) (sym claim₃))
           where
            eβn : β n  𝟏
            eβn = Lemma[b≢0→b≡1]  e  g (trans eαn (sym e)))
            claim₀ : α ≡[ succ n ] (s * )
            claim₀ = ≡[succ]' (Lemma[*-take-≡[]] n) (trans eαn (Lemma[*-take-0] n))
            claim₁ : f α  f (s * )
            claim₁ = usn α (s * ) claim₀
            claim₂ : β ≡[ succ n ] (s * )
            claim₂ = ≡[succ]' (Lemma[≡[]-*-take-≡[]] en) (trans eβn (Lemma[*-take-0] n))
            claim₃ : f β  f (s * )
            claim₃ = usn β (s * ) claim₂
          sd₁ : α n  𝟎  f α  f β
          sd₁ fαn = trans claim₁ (trans (sym (ψ s)) (sym claim₃))
           where
            eαn : α n  𝟏
            eαn = Lemma[b≢0→b≡1] fαn
            eβn : β n  𝟎
            eβn = Lemma[b≢1→b≡0]  e  g (trans eαn (sym e)))
            claim₀ : α ≡[ succ n ] (s * )
            claim₀ = ≡[succ]' (Lemma[*-take-≡[]] n) (trans eαn (Lemma[*-take-0] n))
            claim₁ : f α  f (s * )
            claim₁ = usn α (s * ) claim₀
            claim₂ : β ≡[ succ n ] (s * )
            claim₂ = ≡[succ]' (Lemma[≡[]-*-take-≡[]] en) (trans eβn (Lemma[*-take-0] n))
            claim₃ : f β  f (s * )
            claim₃ = usn β (s * ) claim₂
    sc₁ : ¬ ((s : 𝟚^ n)  f (s * )  f (s * ))  Uc f m + ¬ (Uc f m)
    sc₁ φ = inr goal
     where
      claim : (s : 𝟚^ n)  (s * ) ≡[ m ] (s * )
      claim s = Lemma[≡[]-≤] (Lemma[*-≡[]] s) r'
      goal : ¬ ((α β : 𝟚ᴺ)  α ≡[ m ] β  f α  f β)
      goal um = φ  s  um (s * ) (s * ) (claim s))
  c₁ : m  succ n  Uc f m + ¬ (Uc f m)
  c₁ e = inl (transport (Uc f) (sym e) usn)

Theorem[UC→CH-UC] : UC  CH-UC
Theorem[UC→CH-UC] uc f = MainLemma (Uc f) (Uc-isProp f) (Uc-≤-decidable f) (uc f)

\end{code}