module AnInfiniteOmniscientSet where

-- By Martin Escardo, 2 September 2011.
--
-- This is a formal constructive proof in the sense of ML type theory,
-- written in Agda notation.
--
-- It is based on the author's paper 
--
---------------------------------------------------------------
--      Infinite sets that satisfy the principle of omniscience 
--      in all varieties of constructive mathematics
---------------------------------------------------------------
--
--      http://www.cs.bham.ac.uk/~mhe/papers/omniscient.pdf
--
--
-- to be presented at the Types'2011 meeting in Bergen, Norway,
-- September 8-11,
--
-- Theorem-3·6 of that paper is proved in the module
-- DrinkerParadox. This module derives the main corollary, the fact
-- that the infinite set ℕ∞, defined in the module
-- GenericConvergentSequence, satisfies the principle of omniscience.
--
----------------------------------------------------------------------
-- You can click at any word or symbol to navigate to the module that
-- defines it in the html rendering of this set of agda modules.
----------------------------------------------------------------------
--
-- The agda files are collected together at
--
--      http://www.cs.bham.ac.uk/~mhe/papers/omniscient.zip



open import Logic
open import Equality
open import Naturals
open import Two
open import Cantor
open import GenericConvergentSequence
open import DrinkerParadox


Theorem[ℕ∞-is-omniscient] :
------------------------------------
  ∀(p : ₂ℕ → ₂) → extensional p →
   (∃ \(x : ₂ℕ) → x ∈ ℕ∞ ∧ p x ≡ ₀)
  ∨(∀  (x : ₂ℕ) → x ∈ ℕ∞ → p x ≡ ₁)
------------------------------------
Theorem[ℕ∞-is-omniscient] p extensionality-of-p =
 two-equality-cases case₀ case₁
 where e : ∃ \(x : ₂ℕ) → x ∈ ℕ∞ ∧
              (p x ≡ ₁ → ∀(y : ₂ℕ) → y ∈ ℕ∞ → p y ≡ ₁)
       e = Theorem-3·6 p extensionality-of-p

       x : ₂ℕ
       x = ∃-witness e

       m : x ∈ ℕ∞
       m = ∧-elim₀(∃-elim e)

       case₀ : p x ≡ ₀ → (∃ \(x : ₂ℕ) → x ∈ ℕ∞ ∧ p x ≡ ₀)
                      ∨  (∀  (x : ₂ℕ) → x ∈ ℕ∞ → p x ≡ ₁)
       case₀ r = ∨-intro₀(∃-intro x (∧-intro m r))

       case₁ : p x ≡ ₁ → (∃ \(x : ₂ℕ) → x ∈ ℕ∞ ∧ p x ≡ ₀)
                      ∨  (∀  (x : ₂ℕ) → x ∈ ℕ∞ → p x ≡ ₁)
       case₁ r = ∨-intro₁(∧-elim₁(∃-elim e) r)