wf-too-strong.agda

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