quox/quox-nat.agda

open import Axiom.Extensionality.Propositional

module _ (ext : ∀ {a b} → Extensionality a b) where

open import Prelude hiding (zero; suc)
open import Data.W renaming (induction to induction′)
open import Data.Container
open import Data.Container.Relation.Unary.All ; open □

variable
  𝓀 ℓ : Level
  A B : Set 𝓀
  P Q : A → Set ℓ
  C : Container 𝓀 ℓ


data Tag : Set where `zero `suc : Tag

Body : Tag → Set
Body t = case t of λ {`zero → ⊥ ; `suc → ⊤}

Repr : Container lzero lzero
Repr = Tag ▷ Body

Nat : Set
Nat = W Repr

Nat′ : Set
Nat′ = ⟦ Repr ⟧ Nat

zero : Nat
zero = sup (`zero , λ ())

suc : Nat → Nat
suc n = sup (`suc , const n)

induction : 
  (P : W C → Set ℓ) →
  (IH : (t : ⟦ C ⟧ (W C)) → □ C P t → P (sup t)) →
  (w : W C) → P w
induction P IH = induction′ P (λ {t} → IH t)


elim : (P : Nat → Set ℓ) →
       (Z : P zero) →
       (S : ∀ n → P n → P (suc n)) →
       (n : Nat) → P n
elim P Z S = induction _ λ (tag , body) →
  body |>
  (case tag
   return (λ t → (n′ : Body t → Nat) →
                  □ Repr P (t , n′) →
                  P (sup (t , n′)))
   of λ where
     `zero → λ n′ _  → ≡.subst (λ n′ → P (sup (`zero , n′))) (ext λ ()) Z
     `suc  → λ n′ IH → S (n′ tt) (IH .proof tt))

pred : Nat → Nat
pred = induction _ λ n@(tag , body) _ →
  body |>
  (case tag
   return (λ t → (Body t → Nat) → Nat)
   of λ where
     `zero _ → zero
     `suc  n → n tt)

Subterms : (A : Set 𝓀) (P : A → Set ℓ) → Set _
Subterms A P = Σ[ x ∈ A ] (P x → W (A ▷ P))

subterms : W (A ▷ P) → Subterms A P
subterms = induction _ λ t IH → t

natSub : Nat → List Nat
natSub n =
  case subterms n of λ where
    (`zero , body) → []
    (`suc  , body) → [ body tt ]
  where open List