gistfile1.hs

module Impossible where

open import Coinduction
open import Function
open import Data.Empty
open import Data.Conat
open import Data.Bool
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Product
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Nullary.Negation
open import Relation.Binary
open import Relation.Binary.PropositionalEquality hiding (setoid)

-- Woo fugly

module ≈ = Setoid setoid

module _ where
  data _≤_ : Coℕ → Coℕ → Set where
    z≤n : ∀ {n} → zero ≤ n
    s≤s : ∀ {m n} (m≤n : ∞ (♭ m ≤ ♭ n)) → suc m ≤ suc n

  n≤∞ : ∀ n → n ≤ ∞ℕ
  n≤∞ zero = z≤n
  n≤∞ (suc n) = s≤s (♯ (n≤∞ (♭ n)))

  ∞≤n⇒n≈∞ : ∀ {n} → ∞ℕ ≤ n → n ≈ ∞ℕ
  ∞≤n⇒n≈∞ (s≤s ∞≤n) = suc (♯ ∞≤n⇒n≈∞ (♭ ∞≤n))

  ≈⇒≤ : _≈_ ⇒ _≤_
  ≈⇒≤ zero = z≤n
  ≈⇒≤ (suc m≈n) = s≤s (♯ (≈⇒≤ (♭ m≈n)))

  ≤-refl : ∀ n → n ≤ n
  ≤-refl zero = z≤n
  ≤-refl (suc n) = s≤s (♯ (≤-refl (♭ n)))

  ≤-trans : ∀ {i j k} → i ≤ j → j ≤ k → i ≤ k
  ≤-trans z≤n j≤k = z≤n
  ≤-trans (s≤s i≤j) (s≤s j≤k) = s≤s (♯ (≤-trans (♭ i≤j) (♭ j≤k)))

  

data Finite : Coℕ → Set where
  zero : Finite zero
  suc  : ∀ {n} (r : Finite (♭ n)) → Finite (suc n)

data Infinite : Coℕ → Set where
  suc : ∀ {n} (r : ∞ (Infinite (♭ n))) → Infinite (suc n)

either : ∀ {n} → Finite n → Infinite n → ⊥
either (suc f) (suc i) = either f (♭ i)

¬fin⇒inf : ∀ {n} → ¬ Finite n → Infinite n
¬fin⇒inf {zero}  f = ⊥-elim (f zero)
¬fin⇒inf {suc n} f = suc (♯ (¬fin⇒inf {♭ n} (f ∘ suc)))

finite? : ∀ n → ¬ ¬ (Dec (Finite n))
finite? zero    r = r (yes zero)
finite? (suc n) r = r (no (λ f → r (yes f)))


lowerBound : (Coℕ → Bool) → Coℕ
lowerBound p? with p? zero
lowerBound p? | true  = zero
lowerBound p? | false = suc rec
  module lowerBound where
  -- We can't have anonymous ♯ if we need to prove things about this function
  p?∘suc : Coℕ → Bool
  p?∘suc n = p? (suc (♯ n))

  rec : ∞ Coℕ
  rec = ♯ lowerBound p?∘suc

module _ {p? : Coℕ → Bool} (p?-cong : ∀ {x y} → x ≈ y → p? x ≡ p? y) where
  open lowerBound p?

  p?∘suc-cong : ∀ {x y} → x ≈ y → p?∘suc x ≡ p?∘suc y
  p?∘suc-cong eq = p?-cong (suc (♯ eq))

lowerBound-≤ : (p? : Coℕ → Bool) (p?-cong : ∀ {x y} → x ≈ y → p? x ≡ p? y) → ∀ n → (pn : T (p? n)) → lowerBound p? ≤ n
lowerBound-≤ p? p?-cong n pn with p? zero | inspect p? zero
lowerBound-≤ p? p?-cong n       pn | true  | [ _  ] = z≤n
lowerBound-≤ p? p?-cong zero    pn | false | [ eq ] rewrite eq = ⊥-elim pn
lowerBound-≤ p? p?-cong (suc n) pn | false | [ eq ] = s≤s (♯ (lowerBound-≤ p?∘suc (p?∘suc-cong p?-cong) (♭ n) (subst T (p?-cong (suc (♯ ≈.refl))) pn)))
  where open lowerBound p?

lowerBound-fin : (p? : Coℕ → Bool) (p?-cong : ∀ {x y} → x ≈ y → p? x ≡ p? y) → Finite (lowerBound p?) → T (p? (lowerBound p?))
lowerBound-fin p? p?-cong fin with p? zero | inspect p? zero
lowerBound-fin p? p?-cong fin       | true  | [ eq ] rewrite eq = _
lowerBound-fin p? p?-cong (suc fin) | false | [ _  ] = subst T (p?-cong (suc (♯ ≈.refl))) (lowerBound-fin p?∘suc (p?∘suc-cong p?-cong) fin)
  where open lowerBound p?

lowerBound-inf : (p? : Coℕ → Bool) (p?-cong : ∀ {x y} → x ≈ y → p? x ≡ p? y) → T (not (p? (lowerBound p?))) → Infinite (lowerBound p?)
lowerBound-inf p? p?-cong ¬plb with p? zero | inspect p? zero
lowerBound-inf p? p?-cong ¬plb | true  | [ eq ] rewrite eq = ⊥-elim ¬plb
lowerBound-inf p? p?-cong ¬plb | false | [ eq ] = suc (♯ lowerBound-inf p?∘suc (p?∘suc-cong p?-cong) (subst T (cong not (p?-cong (suc (♯ ≈.refl)))) ¬plb))
  where open lowerBound p?

inf-∞ : ∀ {i} → Infinite i → i ≈ ∞ℕ
inf-∞ (suc r) = suc (♯ inf-∞ (♭ r))

∞≤n : ∀ {i j} → Infinite i → i ≤ j → Infinite j
∞≤n (suc r) (s≤s i≤j) = suc (♯ (∞≤n (♭ r) (♭ i≤j)))

lowerBound-not : (p? : Coℕ → Bool) (p?-cong : ∀ {x y} → x ≈ y → p? x ≡ p? y) → T (not (p? (lowerBound p?))) → ∀ n → T (p? n) → ⊥
lowerBound-not p? p?-cong ¬plb n pn = wtf pn z
  where
  x : T (not (p? ∞ℕ))
  x = subst (T ∘ not) (p?-cong (inf-∞ (lowerBound-inf p? p?-cong ¬plb))) ¬plb

  y : Infinite n
  y = ∞≤n (lowerBound-inf p? p?-cong ¬plb) (lowerBound-≤ p? p?-cong n pn)

  z : T (not (p? n))
  z = subst (T ∘ not) (p?-cong (≈.sym (inf-∞ y))) x

  wtf : ∀ {b} → T b → T (not b) → ⊥
  wtf {true}  x y = y
  wtf {false} x y = x

lowerBound-yes : (p? : Coℕ → Bool) (p?-cong : ∀ {x y} → x ≈ y → p? x ≡ p? y) → ∀ n → T (p? n) → ¬ ¬ (T (p? (lowerBound p?)))
lowerBound-yes p? p?-cong n pn = ¬¬-map (y p? p?-cong n pn) (finite? (lowerBound p?))
  where
  y : (p? : Coℕ → Bool) (p?-cong : ∀ {x y} → x ≈ y → p? x ≡ p? y) → ∀ n → T (p? n) → Dec (Finite (lowerBound p?)) → T (p? (lowerBound p?))
  y p? p?-cong n pn (no ¬p) = subst T (p?-cong (≈.sym (≈.trans (inf-∞ (¬fin⇒inf ¬p)) (≈.sym (inf-∞ (∞≤n (¬fin⇒inf ¬p) (lowerBound-≤ p? p?-cong n pn))))))) pn
  y p? p?-cong n pn (yes p) with p? zero | inspect p? zero
  y p? p?-cong n pn (yes p) | true  | [ eq ] rewrite eq = _
  y p?₁ p?-cong₁ zero pn₁ (yes (suc p)) | false | [ eq ] rewrite eq = ⊥-elim pn₁
  y p?₁ p?-cong₁ (suc n₁) pn₁ (yes (suc p)) | false | [ eq ] = subst T (p?-cong₁ (suc (♯ ≈.refl))) (y p?∘suc (p?∘suc-cong p?-cong₁) (♭ n₁) (subst T (p?-cong₁ (suc (♯ ≈.refl))) pn₁) (yes p))
    where open lowerBound p?₁

dec : (p? : Coℕ → Bool) -> ∀ n -> Dec (T (p? n))
dec p? n with p? n
... | true = yes _
... | false = no (λ ())

convert : ∀ {b} -> ¬ (T b) -> T (not b)
convert {true} ¬b = ¬b _
convert {false} ¬b = _

search : (p? : Coℕ → Bool) (p?-cong : ∀ {x y} → x ≈ y → p? x ≡ p? y) -> Dec (∃ \ n -> T (p? n))
search p? p?-cong with dec p? (lowerBound p?)
search p? p?-cong | yes p = yes ((lowerBound p?) , p)
search p? p?-cong | no ¬p = no (λ x → lowerBound-not p? p?-cong (convert ¬p) (proj₁ x) (proj₂ x))