Skip to content

Instantly share code, notes, and snippets.

@jozefg
Last active October 16, 2018 13:19
Show Gist options
  • Save jozefg/36f263f9540ea4e8012dfe83f54b5f2d to your computer and use it in GitHub Desktop.
Save jozefg/36f263f9540ea4e8012dfe83f54b5f2d to your computer and use it in GitHub Desktop.
module wf-too-strong where
open import Data.Product using (proj₁; proj₂; _,_; _×_; Σ-syntax)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Nat using (ℕ; zero; suc; _+_; _≤_; z≤n; s≤s; _≟_)
open import Data.Nat.Properties using (≤-antisym; ≤-refl; ≤-step)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Unit using (⊤; tt)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)
min : {A : Set} → (A → Set) → (A → A → Set) → A → Set
min {A} P _≤_ m = {x : A} → P x → m ≤ x
-- A problematic definition of well-foundedness
StrongWF : (A : Set) → (A → A → Set) → Set₁
StrongWF A _≤_ = (P : A → Set){a : A} → P a → Σ[ m ∈ A ] P m × min P _≤_ m
min-unique : (P : ℕ → Set){m n : ℕ} → P m → P n → min P _≤_ m → min P _≤_ n → n ≡ m
min-unique P p-m p-n min-m min-n = ≤-antisym (min-n p-m) (min-m p-n)
module parity where
data Even : ℕ → Set
data Odd : ℕ → Set
data Even where
zero : Even 0
suc-odd : {n : ℕ} → Odd n → Even (suc n)
data Odd where
suc-even : {n : ℕ} → Even n → Odd (suc n)
parity : (n : ℕ) → Even n ⊎ Odd n
parity zero = inj₁ zero
parity (suc n) with parity n
... | inj₁ p = inj₂ (suc-even p)
... | inj₂ p = inj₁ (suc-odd p)
not-both : (n : ℕ) → Even n → Odd n → ⊥
not-both zero n-even ()
not-both (suc n) (suc-odd n-odd) (suc-even n-even) = not-both n n-even n-odd
double : ℕ → ℕ
double zero = zero
double (suc n) = suc (suc (double n))
div-2 : {n : ℕ} → Even n → ℕ
div-2 zero = zero
div-2 (suc-odd (suc-even x)) = suc (div-2 x)
double-monotone : (m : ℕ) → m ≤ double m
double-monotone zero = z≤n
double-monotone (suc m) = s≤s (≤-step (double-monotone m))
double-even : (m : ℕ) → Even (double m)
double-even zero = zero
double-even (suc m) = suc-odd (suc-even (double-even m))
double-half : (m : ℕ)(is-even : Even (double m)) → div-2 is-even ≡ m
double-half zero zero = refl
double-half (suc m) (suc-odd (suc-even m-even)) rewrite double-half m m-even = refl
open parity
lift : (ℕ → Set) → ℕ → Set
lift P n with parity n
... | inj₁ even = P (div-2 even)
... | inj₂ odd = ⊤
lift-even : (P : ℕ → Set)(n : ℕ) → P n ≡ lift P (double n)
lift-even P n with parity (double n)
... | inj₁ x rewrite double-half n x = refl
... | inj₂ y = ⊥-elim (not-both _ (double-even n) y)
lift-odd : (P : ℕ → Set){n : ℕ} → Odd n → ⊤ ≡ lift P n
lift-odd P {n} odd with parity n
... | inj₁ x = ⊥-elim (not-both _ x odd)
... | inj₂ y = refl
∞-true : (ℕ → Set) → Set
∞-true P = (m : ℕ) → Σ[ n ∈ ℕ ] m ≤ n × P n
lift-is-∞-true : (P : ℕ → Set) → ∞-true (lift P)
lift-is-∞-true P m =
suc (double m) , ≤-step (double-monotone m) , subst (λ x → x) (lift-odd P (suc-even (double-even m))) tt
lift-above : ℕ → (ℕ → Set) → ℕ → Set
lift-above m P n = m ≤ n × P n
min-of-lift-above : (P : ℕ → Set)(m : ℕ) → min (lift-above m P) _≤_ m
min-of-lift-above _ _ prf = proj₁ prf
module _ (wf-nat : StrongWF ℕ _≤_) where
dec-min : (P : ℕ → Set){m : ℕ} → Σ[ n ∈ ℕ ] (P n) → min P _≤_ m → Dec (P m)
dec-min P {m} wit m-min with wf-nat P (proj₂ wit)
... | x , p-x , x-min with x ≟ m
... | yes prf = yes (subst P prf p-x)
... | no ¬prf = no λ p-m → ¬prf (min-unique P p-m p-x m-min x-min)
dec-infinite : (P : ℕ → Set) → ∞-true P → (n : ℕ) → Dec (P n)
dec-infinite P inf n with dec-min (lift-above n P) (inf n) (min-of-lift-above P n)
dec-infinite P inf n | yes (_ , prf) = yes prf
dec-infinite P inf n | no ¬prf = no λ prf → ¬prf (≤-refl , prf)
lem : (P : Set) → Dec P
lem P rewrite lift-even (λ _ → P) 0 = dec-infinite (lift λ _ → P) (lift-is-∞-true _) 0
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment