-
-
Save cartazio/5907091 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 :) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment