Work in progress on seemingly impossible Agda, à la Escardó with a Luke Palmer flavor

Weird.agda

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.Nullary.Negation
open import Relation.Unary as U
open import Relation.Binary as B using (module Setoid; _Respects_; _⇒_; _=[_]⇒_)
import Relation.Binary.PropositionalEquality as PropEq

open PropEq using (_≡_) renaming (sym to ≡-sym)
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)

weird : ∀ {a b p} {A : Set a} {B : Set b} 
          (f : Coℕ → A) (fpf : _≈_ =[ f ]⇒ _≡_) 
          (g : Coℕ → B) (gpf : _≈_ =[ g ]⇒ _≡_)
          {P : A → B → Set p} 
        → (∀ x y → Dec (P x y)) → Dec (∀ x → P (f x) (g x))
weird f fpf g gpf {P} P? with impossible (λ eq ¬p p → ¬p (PropEq.subst₂ P (≡-sym (fpf eq)) (≡-sym (gpf eq)) p)) (λ x → ¬? (P? (f x) (g x)))
weird f fpf g gpf     P? | yes (w , pf) = no (λ f → pf (f w))
weird f fpf g gpf {P} P? | no ¬p = yes helper
  where
  helper : ∀ n → P (f n) (g n)
  helper n with P? (f n) (g n)
  helper n | yes p = p
  helper n | no ¬p′ = ⊥-elim (¬p (n , ¬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 :)