gistfile1.hs

module Weird where

open import Coinduction
open import Function
open import Data.Empty
open import Data.Product
open import Data.Conat
open import Relation.Nullary
open import Relation.Unary
open import Relation.Binary using (module Setoid; _Respects_; _⇒_)
open Setoid setoid using () renaming (refl to ≈-refl; trans to ≈-trans)

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)

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

neither : ∀ {n} → ¬ Finite n → ¬ Infinite n → ⊥
neither f t = t (¬fin⇒inf f)

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

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

lowerBound : ∀ {p} {P : Coℕ → Set p} → Decidable P → Coℕ
lowerBound P? with P? zero
lowerBound P? | yes p = zero
lowerBound P? | no ¬p = suc (♯ lowerBound (P? ∘ suc ∘′ ♯_))

lowerBound-≤ : ∀ {p} {P : Coℕ → Set p} (R : P Respects _≈_) (P? : Decidable P) (exists : ∃ P) → lowerBound P? ≤ proj₁ exists
lowerBound-≤ R P? _ with P? zero
lowerBound-≤ R P? _            | yes p = z≤n
lowerBound-≤ R P? (zero  , pf) | no ¬p = ⊥-elim (¬p pf)
lowerBound-≤ R P? (suc n , pf) | no ¬p = s≤s (♯ lowerBound-≤ (R ∘′ suc ∘′ ♯_) _ (, R (suc (♯ ≈-refl)) pf))

lowerBound-Finite : ∀ {p} {P : Coℕ → Set p} (R : P Respects _≈_) (P? : Decidable P) → Finite (lowerBound P?) → P (lowerBound P?)
lowerBound-Finite R P? F with P? zero 
lowerBound-Finite R P? F       | yes p = p
lowerBound-Finite R P? (suc F) | no ¬p = R (suc (♯ ≈-refl)) (lowerBound-Finite (R ∘′ suc ∘′ ♯_) _ F)

proof : ∀ {p} {P : Coℕ → Set p} (R : P Respects _≈_) (P? : Decidable P) → ¬ P (lowerBound P?) → ¬ ∃ P
proof R P? ¬P (n , pf) = neither
  (λ fin → ¬P (lowerBound-Finite R P? fin))
  (λ inf → let ≈∞ = inf-∞ inf in 
           ¬P (R (≈-trans (∞≤n⇒n≈∞ (≤-trans (≈⇒≤ ≈∞) (lowerBound-≤ R P? (n , pf)))) ≈∞) pf))


impossible : ∀ {p} {P : Coℕ → Set p} (R : P Respects _≈_) (P? : Decidable P) → Dec (∃ P)
impossible R P? with P? (lowerBound P?)
impossible R P? | yes p = yes (, p)
impossible R P? | no ¬p = no  (proof R P? ¬p)





module Tests where
  open import Data.Nat hiding (_+_; _≤_; module _≤_)

  eqℕ? : (x : ℕ) (y : Coℕ) → Dec (fromℕ x ≈ y)
  eqℕ? zero zero = yes zero
  eqℕ? zero (suc y) = no (λ ())
  eqℕ? (suc x) zero = no (λ ())
  eqℕ? (suc x) (suc y) with eqℕ? x (♭ y)
  eqℕ? (suc x) (suc y) | yes p = yes (suc (♯ p))
  eqℕ? (suc x) (suc y) | no ¬p = no (λ { (suc n) → ¬p (♭ n) })

  false : Coℕ → Dec ⊥
  false n = no id
  
  P : Coℕ → Set
  P n = fromℕ 1 ≈ (n + n)
  
  P? : ∀ n → Dec (P n)
  P? n = eqℕ? 1 (n + n)
  
  +-R : ∀ {a b c d} → a ≈ b → c ≈ d → (a + c) ≈ (b + d)
  +-R zero c≈d = c≈d
  +-R (suc a≈b) c≈d = suc (♯ (+-R (♭ a≈b) c≈d))

  R : P Respects _≈_
  R x≈y p = ≈-trans p (+-R x≈y x≈y)
  
  x = impossible (flip ≈-trans) (eqℕ? 2) -- should say yes and give us a Coℕ 2
  y = impossible (λ _ → id) false -- should say no, since false is never true
  z = impossible R P? -- should say no, because P is never true, but the proof will be much more complicated :)