πŸ“₯ Download raw
{-# OPTIONS --cubical-compatible #-}
module Padova2025.Explorations.Uncountability.Impossible.Toy where

open import Padova2025.ProgrammingBasics.Booleans
open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Lists
open import Padova2025.ProgrammingBasics.HigherOrder
open import Padova2025.ProvingBasics.Termination.Gas
open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Equality.General
open import Padova2025.ProvingBasics.Negation
open import Padova2025.ProvingBasics.Connectives.Disjunction
open import Padova2025.ProvingBasics.Connectives.Existential
open import Padova2025.Explorations.Uncountability.Applications

_β—‚_ : Bool β†’ Cantor β†’ Cantor
x β—‚ xs = Ξ» { zero β†’ x ; (succ n) β†’ xs n }

{-# NON_TERMINATING #-}
Ξ΅ : (Cantor β†’ Bool) β†’ Cantor
Ξ΅ P = x β—‚ Ξ΅ (P ∘ (x β—‚_))
  where
  x : Bool
  x = P (false β—‚ Ξ΅ (P ∘ (false β—‚_)))

has-root? : (Cantor β†’ Bool) β†’ Bool
has-root? P = not (P (Ξ΅ P))

root : (Cantor β†’ Bool) β†’ Maybe (List Bool)
root P with P (Ξ΅ P)
... | false = just (map (Ρ P) (zero ∷ one ∷ two ∷ three ∷ four ∷ []))
... | true  = nothing

xor : Bool β†’ Bool β†’ Bool
xor false false = false
xor false true  = true
xor true  false = true
xor true  true  = false

_β‰—?_ : (Cantor β†’ Bool) β†’ (Cantor β†’ Bool) β†’ Bool
P β‰—? Q = not (has-root? (Ξ» xs β†’ not (xor (P xs) (Q xs))))

private
  {-# NON_TERMINATING #-}
  trust-≑ : (a b : Bool) β†’ a ≑ b
  trust-≑ false false = refl
  trust-≑ true  true  = refl
  trust-≑ false true  = trust-≑ false true
  trust-≑ true  false = trust-≑ true  false

  {-# NON_TERMINATING #-}
  trust-β‰’ : {A : Set} {x y : A} β†’ x β‰’ y
  trust-β‰’ eq = trust-β‰’ eq

_β‰—!?_ : (P Q : Cantor β†’ Bool) β†’ ((xs : Cantor) β†’ P xs ≑ Q xs) ⊎ (Ξ£[ xs ∈ Cantor ] P xs β‰’ Q xs)
P β‰—!? Q with P β‰—? Q
... | true  = left  (Ξ» xs β†’ trust-≑ (P xs) (Q xs))
... | false = right (Ξ΅ (Ξ» xs β†’ not (xor (P xs) (Q xs))) , trust-β‰’)