Chuangjie Xu, 2012.

This is an Agda formalization of Theorem 8.2 of the extended version
of [1].

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

[1] Martin Escardo. 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.

    https://doi.org/10.2178/jsl.7803040

\begin{code}

{-# OPTIONS --safe --without-K #-}

open import MLTT.Spartan
open import UF.FunExt

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

open import CoNaturals.Type
open import MLTT.Two-Properties
open import Notation.CanonicalMap
open import NotionsOfDecidability.Complemented
open import NotionsOfDecidability.Decidable
open import TypeTopology.GenericConvergentSequenceCompactness fe
open import UF.DiscreteAndSeparated

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

\end{code}

TODO. The name of the following fact is that of the reference [1]
above. It deserves a better name, or at least a better synonym.

\begin{code}

abstract
 Theorem-8Β·2 : (p : β„•βˆž β†’ 𝟚) β†’ is-decidable ((n : β„•) β†’ p (ΞΉ n) ＝ ₁)
 Theorem-8Β·2 p = cases claimβ‚€ claim₁ (Lemma-8Β·1 p)
  where
   claimβ‚€ : (Ξ£ x κž‰ β„•βˆž , (x β‰  ∞) Γ— (p x ＝ β‚€))
          β†’ is-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) ＝ ₁) β†’ is-decidable ((n : β„•) β†’ p (ΞΉ n) ＝ ₁)
   claim₁ f = inl f

\end{code}

Some examples:

\begin{code}

module examples where

    to-β„• : {A : 𝓀 Μ‡ } β†’ is-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 : β„•βˆž β†’ 𝟚)
                 β†’ is-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.


Added by Martin Escardo 5th September 2024. The following version is
more convenient in practice.

\begin{code}


abstract
 Theorem-8Β·2' : (A : β„•βˆž β†’ 𝓀 Μ‡ )
              β†’ is-complemented A
              β†’ is-decidable ((n : β„•) β†’ A (ΞΉ n))
 Theorem-8Β·2' {𝓀} A Ξ΄ = IV
  where
   p : β„•βˆž β†’ 𝟚
   p = complement ∘ characteristic-map A δ

   I : is-decidable ((n : β„•) β†’ p (ΞΉ n) ＝ ₁)
   I = Theorem-8Β·2 p

   II : ((n : β„•) β†’ p (ΞΉ n) ＝ ₁) β†’ (n : β„•) β†’ A (ΞΉ n)
   II b n = characteristic-map-propertyβ‚€ A Ξ΄ (ΞΉ n) (complement₁ (b n))

   III : ((n : β„•) β†’ A (ΞΉ n)) β†’ (n : β„•) β†’ p (ΞΉ n) ＝ ₁
   III a n = complement₁-back (characteristic-map-propertyβ‚€-back A Ξ΄ (ΞΉ n) (a n))

   IV : is-decidable ((n : β„•) β†’ A (ΞΉ n))
   IV = map-decidable II III I

\end{code}