module taste-it where
open import Data.Product
open import Data.Sum
open import Data.Nat
open import Data.Nat.Properties
open import Data.Empty
open import Data.Unit using (⊤; tt)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

min : {A : Set} → (A → Set) → (A → A → Set) → A → Set
min {A} P _≤_ m  = (x : A) → P x → m ≤ x

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 m n p-m p-n min-m min-n = ≤-antisym (min-n m p-m) (min-m n p-n)

-- WTS that if StrongWF ℕ _≤_ then every predicate on ℕ is decidable.
postulate wf-nat : StrongWF ℕ _≤_
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

div-2 : {n : ℕ} → Even n → ℕ
div-2 zero = zero
div-2 (suc-odd (suc-even x)) = suc (div-2 x)

double : ℕ → ℕ
double zero = zero
double (suc n) = suc (suc (double n))

≤-weaken : {m n : ℕ} → m ≤ n → m ≤ suc n
≤-weaken prf = ≤′⇒≤ (≤′-step (≤⇒≤′ prf))

double-monotone : (m : ℕ) → m ≤ double m
double-monotone zero = z≤n
double-monotone (suc m) = s≤s (≤-weaken (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

lift : (ℕ → Set) → ℕ → Set
lift P n with parity n
... | inj₁ even = P (div-2 even)
... | inj₂ odd = ⊤

lift-is-lift-even : (P : ℕ → Set)(n : ℕ) → P n ≡ lift P (double n)
lift-is-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-is-lift-odd : (P : ℕ → Set){n : ℕ} → Odd n → ⊤ ≡ lift P n
lift-is-lift-odd P {n} odd with parity n
... | inj₁ x = ⊥-elim (not-both _ x odd)
... | inj₂ y = refl

infinitely-true : (ℕ → Set) → Set
infinitely-true P = (m : ℕ) → Σ[ n ∈ ℕ ] m ≤ n × P n

lift-is-infinitely-true : (P : ℕ → Set) → infinitely-true (lift P)
lift-is-infinitely-true P m =
  suc (double m) , ≤-weaken (double-monotone m) , subst (λ x → x) (lift-is-lift-odd P (suc-even (double-even m))) tt

lift-greater : ℕ → (ℕ → Set) → ℕ → Set
lift-greater m P n = m ≤ n × P n

min-of-lift-greater : (P : ℕ → Set)(m : ℕ) → min (lift-greater m P) _≤_ m
min-of-lift-greater P m x prf = proj₁ prf

dec-min : (P : ℕ → Set)(n : ℕ) → P n → (m : ℕ) → min P _≤_ m → P m ⊎ (P m → ⊥)
dec-min P n P-wit m is-min = dec-P
  where min-of-P : Σ[ x ∈ ℕ ] P x × min P _≤_ x
        min-of-P = wf-nat P n P-wit
        eq-min : Dec (proj₁ min-of-P ≡ m)
        eq-min = proj₁ min-of-P ≟ m
        dec-P : P m ⊎ (P m → ⊥)
        dec-P with eq-min
        dec-P | yes prf = inj₁ (subst P prf (proj₁ (proj₂ min-of-P)))
        dec-P | no ¬prf = inj₂ λ p-m → (¬prf (min-unique P m (proj₁ min-of-P) p-m (proj₁ (proj₂ min-of-P)) is-min (proj₂ (proj₂ min-of-P))))

dec-infinite : (P : ℕ → Set) → infinitely-true P → (n : ℕ) → P n ⊎ (P n → ⊥)
dec-infinite P inf n with dec-min (lift-greater n P) (proj₁ (inf n)) (proj₂ (inf n)) n (min-of-lift-greater P n)
dec-infinite P inf n | inj₁ (_ , prf) = inj₁ prf
dec-infinite P inf n | inj₂ ¬prf = inj₂ λ prf → ¬prf (≤-refl , prf)

dec : (P : ℕ → Set)(n : ℕ) → P n ⊎ (P n → ⊥)
dec P n with dec-infinite (lift P) (lift-is-infinitely-true P) (double n)
... | prf rewrite (lift-is-lift-even P n) = prf