Tom de Jong, 22 & 23 June 2024

We formalize what we've known for a long time: if the poset pictured below

   0   1   2   3   ...
     \ \   / /
      \ \ / /
         βŠ₯

is Ο‰-complete/directed complete, then Bishop's LPO holds.

\begin{code}

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

open import MLTT.Spartan

open import UF.FunExt
open import UF.PropTrunc

module DomainTheory.Taboos.ClassicalLiftingOfNaturalNumbers
        (pt : propositional-truncations-exist)
        (fe : Fun-Ext)
       where

open PropositionalTruncation pt

open import DomainTheory.Basics.Dcpo pt fe 𝓀₀

open import CoNaturals.Type renaming (β„•βˆž-to-β„•β†’πŸš to Ξ΅)
open import MLTT.Two-Properties
open import MLTT.Plus-Properties
open import Taboos.LPO

\end{code}

The poset is defined as follows. Notice that the set of natural numbers is
ordered discretely.

NB: In this file, and this file only, we denote this poset by β„•βŠ₯. In
CoNaturals/Sharp this notation is reserved for the lifting of the natural
numbers which constructively *does* yield a directed complete
poset. Classically, the constructions are equivalent, as formalized in
Lifting.Miscelanea-PropExt-FunExt. Indeed, this is the case *only* classically,
as this file shows by deriving a constructive taboo from the assumption that β„•βŠ₯
is directed complete.

\begin{code}

β„•βŠ₯ : 𝓀₀ Μ‡
β„•βŠ₯ = πŸ™{𝓀₀} + β„•

_βŠ‘_ : β„•βŠ₯ β†’ β„•βŠ₯ β†’ 𝓀₀ Μ‡
inl ⋆ βŠ‘ x = πŸ™
inr n βŠ‘ x = inr n ＝ x

\end{code}

We now state the main results, postponing the proof.

In fact, we show that just having upper bounds of Ο‰-chains (so not necessarily
least ones) gives LPO.

\begin{code}

β„•βŠ₯-is-Ο‰-complete-gives-LPO : is-Ο‰-complete _βŠ‘_ β†’ LPO

β„•βŠ₯-is-directed-complete-gives-LPO : is-directed-complete _βŠ‘_ β†’ LPO

β„•βŠ₯-has-upperbounds-for-Ο‰-chains-gives-LPO :
   ((Ξ± : β„• β†’ β„•βŠ₯)
       β†’ is-Ο‰-chain _βŠ‘_ Ξ±
       β†’ (Ξ£ x κž‰ β„•βŠ₯ , is-upperbound _βŠ‘_ x Ξ±))
 β†’ LPO

\end{code}

We need a few preliminaries before giving the proof.

\begin{code}

inr-not-βŠ‘-inl : {n : β„•} β†’ Β¬ (inr n βŠ‘ inl ⋆)
inr-not-βŠ‘-inl p = +disjoint (p ⁻¹)

βŠ‘-refl : (x : β„•βŠ₯) β†’ x βŠ‘ x
βŠ‘-refl (inl ⋆) = ⋆
βŠ‘-refl (inr n) = refl

βŠ‘-refl-＝ : {x y : β„•βŠ₯} β†’ x ＝ y β†’ x βŠ‘ y
βŠ‘-refl-＝ refl = βŠ‘-refl _

βŠ‘-trans : (x y z : β„•βŠ₯) β†’ x βŠ‘ y β†’ y βŠ‘ z β†’ x βŠ‘ z
βŠ‘-trans (inl ⋆) y z p q = ⋆
βŠ‘-trans (inr n) y z refl q = q

\end{code}

We now prove the main result.

In TypeTopology, LPO states that is decidable whether a decreasing binary sequence
u : β„•βˆž is finite or not. The equivalence with the traditional formulation is
formalized in Taboos.LPO.

We write Ξ΅ u n for evaluating the binary sequence u at index n.

Given such u, we construct Ο‡ : β„• β†’ β„•βŠ₯ such that

   β€’ Ο‡ n = βŠ₯ = inl ⋆ ⇔ Ξ΅ u n = ₁;
   β€’ Ο‡ n = inr m     ⇔ m is the least integer ≀ n such that Ξ΅ u m = β‚€.

We then show that Ο‡ is an Ο‰-chain and that from an upper bound we can decide,
via some case splitting, whether u is finite or not, i.e., whether u is always ₁
or attains β‚€ somewhere.

\begin{code}

private
 module construction (u : β„•βˆž) where

  Ο‡ : β„• β†’ β„•βŠ₯
  Ο‡ n = 𝟚-equality-cases I II
   where
    I : Ξ΅ u n ＝ β‚€ β†’ β„•βŠ₯
    I p = inr (size (bounded-is-finite fe n u p))
    II : Ξ΅ u n ＝ ₁ β†’ β„•βŠ₯
    II _ = inl ⋆

  module _
          {n : β„•}
          (p : Ξ΅ u n ＝ β‚€)
         where

   Ο‡-numeral : β„•
   Ο‡-numeral = size (bounded-is-finite fe n u p)

   Ο‡-eq : Ο‡ n ＝ inr Ο‡-numeral
   Ο‡-eq = 𝟚-equality-casesβ‚€ p

   Ο‡-numeral-eq : β„•-to-β„•βˆž Ο‡-numeral ＝ u
   Ο‡-numeral-eq = size-property (bounded-is-finite fe n u p)

  Ο‡-otherwise : {n : β„•} β†’ Ξ΅ u n ＝ ₁ β†’ Ο‡ n ＝ inl ⋆
  Ο‡-otherwise p = 𝟚-equality-cases₁ p

  Ο‡-is-Ο‰-chain : (n : β„•) β†’ Ο‡ n βŠ‘ Ο‡ (succ n)
  Ο‡-is-Ο‰-chain n = 𝟚-equality-cases I II
   where
    II : Ξ΅ u n ＝ ₁ β†’ Ο‡ n βŠ‘ Ο‡ (succ n)
    II p = transport⁻¹ (_βŠ‘ Ο‡ (succ n)) (Ο‡-otherwise p) ⋆
    I : Ξ΅ u n ＝ β‚€ β†’ Ο‡ n βŠ‘ Ο‡ (succ n)
    I p = βŠ‘-refl-＝ I₁
     where
      q : Ξ΅ u (succ n) ＝ β‚€
      q = stays-zero u p
      I₁ = Ο‡ n               ＝⟨ Ο‡-eq p ⟩
           inr (Ο‡-numeral p) ＝⟨ Iβ‚‚ ⟩
           inr (Ο‡-numeral q) ＝⟨ (Ο‡-eq q) ⁻¹ ⟩
           Ο‡ (succ n)        ∎
       where
        Iβ‚‚ = ap inr (β„•-to-β„•βˆž-lc (Ο‡-numeral-eq p βˆ™ (Ο‡-numeral-eq q) ⁻¹))

  inl-case : is-upperbound _βŠ‘_ (inl ⋆) Ο‡
           β†’ is-decidable (is-finite' u)
  inl-case ub = inr I
   where
    I : Β¬ (is-finite' u)
    I (n , refl) = inr-not-βŠ‘-inl II
     where
      p : Ξ΅ u n ＝ β‚€
      p = β„•-to-β„•βˆž-diagonalβ‚€ n
      II : inr (Ο‡-numeral p) βŠ‘ inl ⋆
      II = transport (_βŠ‘ inl ⋆) (Ο‡-eq p) (ub n)

  inr-case : {m : β„•} β†’ is-upperbound _βŠ‘_ (inr m) Ο‡
           β†’ is-decidable (is-finite' u)
  inr-case {m} ub = 𝟚-equality-cases I II
   where
    I : Ξ΅ u m ＝ β‚€ β†’ is-decidable (is-finite' u)
    I p = inl (Ο‡-numeral p , ((Ο‡-numeral-eq p) ⁻¹))
    II : Ξ΅ u m ＝ ₁ β†’ is-decidable (is-finite' u)
    II p = inr III
     where
      III : Β¬ is-finite' u
      III (n , refl) = diff (inr-lc eq)
       where
        q : Ξ΅ u n ＝ β‚€
        q = β„•-to-β„•βˆž-diagonalβ‚€ n

        eq = inr n             ＝⟨ (ap inr (β„•-to-β„•βˆž-lc (Ο‡-numeral-eq q)))⁻¹ ⟩
             inr (Ο‡-numeral q) ＝⟨ transport (_βŠ‘ inr m) (Ο‡-eq q) (ub n) ⟩
             inr m             ∎

        diff : n β‰  m
        diff e = zero-is-not-one (β‚€     ＝⟨ (β„•-to-β„•βˆž-diagonalβ‚€ n) ⁻¹ ⟩
                                  Ρ u n ＝⟨ ap (Ρ u) e ⟩
                                  Ρ u m ＝⟨ p ⟩
                                  ₁     ∎)

\end{code}

This completes the technical details and we are ready to give the proofs.

\begin{code}

β„•βŠ₯-has-upperbounds-for-Ο‰-chains-gives-LPO Ξ½ seq =
 equality-cases s (I s s-is-ub) (II s s-is-ub)
  where
   open construction seq
   module _
           (s : β„•βŠ₯)
           (s-is-ub : is-upperbound _βŠ‘_ s Ο‡)
          where
    I : (u : πŸ™) β†’ s ＝ inl u β†’ is-decidable (is-finite' seq)
    I ⋆ refl = inl-case s-is-ub
    II : (m : β„•) β†’ s ＝ inr m β†’ is-decidable (is-finite' seq)
    II m refl = inr-case s-is-ub

   s : β„•βŠ₯
   s = pr₁ (Ξ½ Ο‡ Ο‡-is-Ο‰-chain)
   s-is-ub : is-upperbound _βŠ‘_ s Ο‡
   s-is-ub = prβ‚‚ (Ξ½ Ο‡ Ο‡-is-Ο‰-chain)

β„•βŠ₯-is-Ο‰-complete-gives-LPO comp =
 β„•βŠ₯-has-upperbounds-for-Ο‰-chains-gives-LPO
  (Ξ» Ξ± c β†’ the-sup _βŠ‘_ (comp Ξ± c) ,
           sup-is-upperbound _βŠ‘_ (sup-property _βŠ‘_ (comp Ξ± c)))

β„•βŠ₯-is-directed-complete-gives-LPO comp =
 β„•βŠ₯-is-Ο‰-complete-gives-LPO
  (Ξ» Ξ± c β†’ comp β„• Ξ± (Ο‰-chains-are-directed _βŠ‘_ βŠ‘-refl βŠ‘-trans Ξ± c))

\end{code}