Inductive.agda

module Inductive where

open import Data.Empty
open import Data.Unit
open import Data.Nat
open import Data.Fin using (Fin; zero; suc)
open import Data.Product
open import Data.Sum

module Inductive
  (A : Set) -- datatype's type parameter
  (n : ℕ) -- number of constructors
  (X : (i : Fin n) → Set) -- constructors' parameter type
  (H : (i : Fin n) → X i → Set) -- constructors' hypothesis type
  (o : (i : Fin n) → X i → A) -- constructors' output argument
  (M : (i : Fin n) → X i → Set) -- datatype's recursion parameter type
  (μ : (i : Fin n) → (x : X i) → H i x → M i x → A) -- datatype's recursion output argument
  where
  
  data Inductive : A → Set where
    con : (i : Fin n) (x : X i) (h : H i x)
          (r : (m : M i x) → Inductive (μ i x h m)) →
          Inductive (o i x)


module Even where
  open Inductive

  pattern #0 = zero
  pattern #1 = suc zero

  Even : ℕ → Set
  Even =
    Inductive
      -- type parameter
      ℕ
      -- number of constructors
      2
      -- constructor parameter type
      (λ { #0 → ⊤ ;
           #1 → ℕ })
      -- constructor hypothesis type
      (λ { #0 tt → ⊤ ;
           #1 n  → ⊤ })
      -- constructor output argument
      (λ { #0 tt → 0 ;
           #1 n  → suc (suc n) })
      -- recursion parameter type
      (λ { #0 tt → ⊥ ;
           #1 n  → ⊤ })
      -- recursion output argument
      (λ { #0 tt tt () ;
           #1 n  tt tt → n })

  Even-z : Even 0
  Even-z = con #0 tt tt (λ ())

  Even-ss : ∀ {n} → Even n → Even (suc (suc n))
  Even-ss {n} e = con #1 n tt λ tt → e

  Even-2 : Even 2
  Even-2 = Even-ss Even-z

  -- correctness

  data EvenD : ℕ → Set where
    EvenD-z  : EvenD 0
    EvenD-ss : ∀ {n} → EvenD n → EvenD (suc (suc n))

  to : ∀ {n} → Even n → EvenD n
  to (con #0 tt tt r) = EvenD-z
  to (con #1 x h r) = EvenD-ss (to (r tt))

  from : ∀ {n} → EvenD n → Even n
  from EvenD-z = Even-z
  from (EvenD-ss EvenD-n) = Even-ss (from EvenD-n)

module Bst where
  open Inductive

  data tree : Set where
    leaf : tree
    node : ℕ → tree → tree → tree

  pattern #0 = zero
  pattern #1 = suc #0
  
  Bst : (ℕ × ℕ × tree) → Set
  Bst =
    Inductive
      -- type parameter
      (ℕ × ℕ × tree)
      -- number of constructors
      2
      -- constructor parameter type
      (λ { #0 → ℕ × ℕ ;
           #1 → ℕ × ℕ × ℕ × tree × tree })
      -- constructor hypothesis type
      (λ { #0 (lo , hi) → Fin 1 ;
           #1 (lo , hi , x , l , r) → lo < x × x < hi })
      -- constructor output argument
      (λ { #0 (lo , hi) → (lo , hi , leaf) ;
           #1 (lo , hi , x , l , r) → (lo , hi , node x l r) })
      -- recursion parameter type
      (λ { #0 (lo , hi) → Fin 0 ;
           #1 (lo , hi , x , l , r) → Fin 2 })
      -- recursion output argument
      (λ { #0 (lo , hi) #0 () ;
           #1 (lo , hi , x , l , r) (lo<x , x<hi) #0 → (lo , x , l) ;
           #1 (lo , hi , x , l , r) (lo<x , x<hi) #1 → (x  , hi , r) })

  Bst-leaf : ∀ {lo hi} → Bst (lo , hi , leaf)
  Bst-leaf {lo} {hi} = con #0 (lo , hi) #0 (λ ())

  Bst-node : ∀ {lo hi x l r} → (lo < x) → (x < hi) → Bst (lo , x , l) → Bst (x , hi , r) → Bst (lo , hi , node x l r)
  Bst-node {lo} {hi} {x} {l} {r} lo<x x<hi Bst-l Bst-r = con #1 (lo , hi , x , l , r) (lo<x , x<hi) (λ { #0 → Bst-l ; #1 → Bst-r })
  
  -- correctness

  data BstD : ℕ → ℕ → tree → Set where
    BstD-leaf : ∀ {lo hi} → BstD lo hi leaf
    BstD-node : ∀ {lo hi x l r} → (lo < x) → (x < hi) → BstD lo x l → BstD x hi r → BstD lo hi (node x l r)

  to : ∀ {lo hi t} → Bst (lo , hi , t) → BstD lo hi t
  to (con #0 x h r) = BstD-leaf
  to (con #1 (lo , hi , x , tₗ , tᵣ) (lo<x , x<hi) r) = BstD-node lo<x x<hi (to (r #0)) (to (r #1))

  from : ∀ {lo hi t} → BstD lo hi t → Bst (lo , hi , t)
  from BstD-leaf = Bst-leaf
  from (BstD-node lo<x x<hi bstₗ bstᵣ) = Bst-node lo<x x<hi (from bstₗ) (from bstᵣ)