Chuangjie Xu, 2012.

This is an Agda formalization of Theorem 8.2 of the extended version
of Escardo's paper "Infinite sets that satisfy the principle of
omniscience in all varieties of constructive mathematics", Journal of
Symbolic Logic, volume 78, number 3, September 2013, pages 764-784.

The theorem says that, for any p : β„•βˆž β†’ 𝟚, the proposition
(n : β„•) β†’ p (ΞΉ n) ≑ ₁ is decidable where ΞΉ : β„• β†’ ∞ is the inclusion.

\begin{code}

{-# OPTIONS --without-K --exact-split --safe --auto-inline #-}

open import SpartanMLTT
open import UF-FunExt

module ADecidableQuantificationOverTheNaturals (fe : funext 𝓀₀ 𝓀₀) where

open import Two-Properties
open import GenericConvergentSequence
open import CompactTypes
open import GenericConvergentSequence
open import ConvergentSequenceCompact fe
open import DecidableAndDetachable
open import DiscreteAndSeparated
open import CanonicalMapNotation
open import UF-PropTrunc

Lemma-8Β·1 : (p : β„•βˆž β†’ 𝟚) β†’ (Ξ£ x κž‰ β„•βˆž , (x β‰’ ∞) Γ— (p x ≑ β‚€))
                         + ((n : β„•) β†’ p (ΞΉ n) ≑ ₁)
Lemma-8Β·1 p = cases claimβ‚€ claim₁ claimβ‚‚
 where
  claimβ‚€ : (Ξ£ y κž‰ β„•βˆž , p y β‰’ p (Succ y))
         β†’ (Ξ£ x κž‰ β„•βˆž , (x β‰’ ∞) Γ— (p x ≑ β‚€)) + ((n : β„•) β†’ p (ΞΉ n) ≑ ₁)
  claimβ‚€ e = inl (𝟚-equality-cases caseβ‚€ case₁)
   where
    x : β„•βˆž
    x = pr₁ e

    ne : p x β‰’ p (Succ x)
    ne = prβ‚‚ e

    caseβ‚€ : p x ≑ β‚€ β†’ Ξ£ x κž‰ β„•βˆž , (x β‰’ ∞) Γ— (p x ≑ β‚€)
    caseβ‚€ r = x , (s , r)
     where
      s : x β‰’ ∞
      s t = ne (ap p (t βˆ™ (Succ-∞-is-∞ fe)⁻¹ βˆ™ (ap Succ t)⁻¹))

    case₁ : p x ≑ ₁ β†’ Ξ£ x κž‰ β„•βˆž , (x β‰’ ∞) Γ— (p x ≑ β‚€)
    case₁ r = (Succ x) , (s , s')
     where
      s : Succ x β‰’ ∞
      s t = ne (ap p (Succ-lc (t βˆ™ (Succ-∞-is-∞ fe)⁻¹) βˆ™ t ⁻¹))

      s' : p (Succ x) ≑ β‚€
      s' = different-from-₁-equal-β‚€ (Ξ» t β†’ ne (r βˆ™ t ⁻¹))

  claim₁ : ((y : β„•βˆž) β†’ p y ≑ p (Succ y)) β†’
            (Ξ£ x κž‰ β„•βˆž , (x β‰’ ∞) Γ— (p x ≑ β‚€)) + ((n : β„•) β†’ p (ΞΉ n) ≑ ₁)
  claim₁ f = 𝟚-equality-cases caseβ‚€ case₁
   where
    caseβ‚€ : p Zero ≑ β‚€ β†’
            (Ξ£ x κž‰ β„•βˆž , (x β‰’ ∞) Γ— (p x ≑ β‚€)) + ((n : β„•) β†’ p (ΞΉ n) ≑ ₁)
    caseβ‚€ r = inl (Zero , (s , r))
     where
      s : Zero β‰’ ∞
      s t = ∞-is-not-finite 0 (t ⁻¹)

    case₁ : p Zero ≑ ₁ β†’
            (Ξ£ x κž‰ β„•βˆž , (x β‰’ ∞) Γ— (p x ≑ β‚€)) + ((n : β„•) β†’ p (ΞΉ n) ≑ ₁)
    case₁ r = inr by-induction
     where
      by-induction : (n : β„•) β†’ p (ΞΉ n) ≑ ₁
      by-induction 0 = r
      by-induction (succ n) = (f (ΞΉ n))⁻¹ βˆ™ by-induction n

  claimβ‚‚ : (Ξ£ y κž‰ β„•βˆž , p y β‰’ p (Succ y)) + ((y : β„•βˆž) β†’ p y ≑ p (Succ y))
  claimβ‚‚ = g (β„•βˆž-compact q)
   where
    fact : (y : β„•βˆž) β†’ (p y β‰’ p (Succ y)) + Β¬ (p y β‰’ p (Succ y))
    fact y = ¬-preserves-decidability (𝟚-is-discrete (p y) (p (Succ y)))

    f : Ξ£ q κž‰ (β„•βˆž β†’ 𝟚), ((y : β„•βˆž) β†’ (q y ≑ β‚€ β†’ p y β‰’ p (Succ y))
                                  Γ— (q y ≑ ₁ β†’ Β¬ (p y β‰’ p (Succ y))))
    f = characteristic-function fact

    q : β„•βˆž β†’ 𝟚
    q = pr₁ f

    g : (Ξ£ y κž‰ β„•βˆž , q y ≑ β‚€) + ((y : β„•βˆž) β†’ q y ≑ ₁)
     β†’ (Ξ£ y κž‰ β„•βˆž , p y β‰’ p (Succ y)) + ((y : β„•βˆž) β†’ p y ≑ p (Succ y))
    g (inl (y , r)) = inl (y , (pr₁ (prβ‚‚ f y) r))
    g (inr h ) = inr (Ξ» y β†’ discrete-is-¬¬-separated
                             𝟚-is-discrete
                             (p y) (p (Succ y))
                             (prβ‚‚ (prβ‚‚ f y) (h y)))

abstract
 Theorem-8Β·2 : (p : β„•βˆž β†’ 𝟚) β†’ decidable ((n : β„•) β†’ p (ΞΉ n) ≑ ₁)
 Theorem-8Β·2 p = cases claimβ‚€ claim₁ (Lemma-8Β·1 p)
  where
   claimβ‚€ : (Ξ£ x κž‰ β„•βˆž , (x β‰’ ∞) Γ— (p x ≑ β‚€)) β†’
             decidable ((n : β„•) β†’ p (ΞΉ n) ≑ ₁)
   claimβ‚€ e = inr c₁
    where
     x : β„•βˆž
     x = pr₁ e

     cβ‚€ : Β¬ ((n : β„•) β†’ x β‰’ ΞΉ n)
     cβ‚€ = Ξ» g β†’ pr₁ (prβ‚‚ e) (not-finite-is-∞ fe g)

     c₁ : Β¬ ((n : β„•) β†’ p (ΞΉ n) ≑ ₁)
     c₁ g = cβ‚€ d
      where
       d : (n : β„•) β†’ x β‰’ ΞΉ n
       d n r = equal-β‚€-different-from-₁ (prβ‚‚ (prβ‚‚ e)) (ap p r βˆ™ g n)

   claim₁ : ((n : β„•) β†’ p (ΞΉ n) ≑ ₁) β†’ decidable ((n : β„•) β†’ p (ΞΉ n) ≑ ₁)
   claim₁ f = inl f

\end{code}

Some examples:

\begin{code}

module examples where

    to-β„• : {A : 𝓀 Μ‡ } β†’ decidable A β†’ β„•
    to-β„• (inl _) = 0
    to-β„• (inr _) = 1

\end{code}

    0 means that (n : β„•) β†’ p (ΞΉ n) ≑ ₁
    1 means that Β¬ ((n : β„•) β†’ p (ΞΉ n) ≑ ₁)

\begin{code}

    eval : (β„•βˆž β†’ 𝟚) β†’ β„•
    eval p = to-β„• (Theorem-8Β·2 p)

    pβ‚€ : β„•βˆž β†’ 𝟚
    pβ‚€ _ = β‚€

    p₁ : β„•βˆž β†’ 𝟚
    p₁ _ = ₁

\end{code}

    If the first boolean is less than or equal to the second
    then it has value ₁; otherwise, it has value β‚€.

\begin{code}

    _<=_ : 𝟚 β†’ 𝟚 β†’ 𝟚
    β‚€ <= y = ₁
    ₁ <= β‚€ = β‚€
    ₁ <= ₁ = ₁

\end{code}

    If the two booleans are equal then it has value ₁;
    otherwise, it has value β‚€.

\begin{code}

    _==_ : 𝟚 β†’ 𝟚 β†’ 𝟚
    β‚€ == β‚€ = ₁
    β‚€ == ₁ = β‚€
    ₁ == β‚€ = β‚€
    ₁ == ₁ = ₁

    pβ‚‚ : β„•βˆž β†’ 𝟚
    pβ‚‚ (Ξ± , _) = Ξ± 10 <= Ξ± 1

    p₃ : β„•βˆž β†’ 𝟚
    p₃ (Ξ± , _) = Ξ± 0 <= Ξ± 1

    pβ‚„ : β„•βˆž β†’ 𝟚
    pβ‚„ (Ξ± , _) = Ξ± 5 == Ξ± 100

    to-something : (p : β„•βˆž β†’ 𝟚) β†’ decidable ((n : β„•) β†’ p (ΞΉ n) ≑ ₁) β†’ (p (ΞΉ 17) ≑ ₁) + β„•
    to-something p (inl f) = inl (f 17)
    to-something p (inr _) = inr 1070

    eval1 : (p : β„•βˆž β†’ 𝟚) β†’ (p (ΞΉ 17) ≑ ₁) + β„•
    eval1 p = to-something p (Theorem-8Β·2 p)

\end{code}

    Despite the fact that we use function extensionality, eval pi
    evaluates to a numeral for i=0,...,4.