Skip to content

Instantly share code, notes, and snippets.

@copumpkin
Last active March 14, 2023 09:32
Show Gist options
  • Save copumpkin/4647315 to your computer and use it in GitHub Desktop.
Save copumpkin/4647315 to your computer and use it in GitHub Desktop.
Work in progress on seemingly impossible Agda, à la Escardó with a Luke Palmer flavor
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 :)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment