Chuangjie Xu, July 2016

\begin{code}

module DataTypes where

open import Preliminaries

\end{code}

Natural numbers

\begin{code}

data ℕ : Set where
 zero : ℕ
 succ : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

_+ℕ_ : ℕ → ℕ → ℕ
n +ℕ         = n
n +ℕ (succ m) = succ (n +ℕ m)

Lemma[0+ℕ] : (n : ℕ) →  +ℕ n ≡ n
Lemma[0+ℕ]         = refl
Lemma[0+ℕ] (succ n) = ap succ (Lemma[0+ℕ] n)

_×ℕ_ : ℕ → ℕ → ℕ
n ×ℕ         = 
n ×ℕ (succ m) = n +ℕ (n ×ℕ m)

Lemma[0×ℕ] : (n : ℕ) →  ×ℕ n ≡ 
Lemma[0×ℕ]         = refl
Lemma[0×ℕ] (succ n) = trans (Lemma[0+ℕ] ( ×ℕ n)) (Lemma[0×ℕ] n)

rec : {A : Set} → A → (ℕ → A → A) → ℕ → A
rec a f         = a
rec a f (succ n) = f n (rec a f n)

pred : ℕ → ℕ
pred         = 
pred (succ n) = n

infix  _≤_ _≥_

data _≤_ : ℕ → ℕ → Set where
 ≤-zero : {n : ℕ}   →  ≤ n
 ≤-succ : {n m : ℕ} → n ≤ m → succ n ≤ succ m

_≥_ : ℕ → ℕ → Set
n ≥ m = m ≤ n

\end{code}

List

\begin{code}

infixl  _₊_
infixr  _₊₊_

data List (A : Set) : Set where
 ε  : List A
 _₊_ : List A → A → List A

⟨_⟩ : {A : Set} → A → List A
⟨ x ⟩ = ε ₊ x

₊⁼ : {A : Set} {xs ys : List A} {x y : A}
   → xs ≡ ys → x ≡ y → (xs ₊ x) ≡ (ys ₊ y)
₊⁼ refl refl = refl

_₊₊_ : {A : Set} → List A → List A → List A
xs ₊₊  ε       = xs
xs ₊₊ (ys ₊ y) = (xs ₊₊ ys) ₊ y

recᴸ : {A B : Set} → A → (B → A → A) → List B → A
recᴸ a f  ε       = a
recᴸ a f (xs ₊ x) = f x (recᴸ a f xs)

length : {A : Set} → List A → ℕ
length  ε       = 
length (xs ₊ _) = succ (length xs)

head : {A : Set} → (xs : List A) → length xs ≥  → A
head  ε     ()
head (_ ₊ x) _  = x

data ∥_∈_∥ {A : Set} (a : A) : List A → Set where
 zero : {xs : List A} → ∥ a ∈ (xs ₊ a) ∥
 succ : {x : A} {xs : List A} → ∥ a ∈ xs ∥ → ∥ a ∈ (xs ₊ x) ∥

infix  _⊆_

_⊆_ : {A : Set} → List A → List A → Set
Γ ⊆ Δ = ∀{x} → ∥ x ∈ Γ ∥ → ∥ x ∈ Δ ∥

ε-⊆ : {A : Set} {xs : List A}
    → ε ⊆ xs
ε-⊆ ()

⊆-cons : {A : Set} {xs ys : List A} {a : A}
       → xs ⊆ ys → xs ₊ a ⊆ ys ₊ a
⊆-cons ξ  zero    = zero
⊆-cons ξ (succ i) = succ (ξ i)

⊆-exch : {A : Set} {xs : List A} {a b : A}
       → xs ₊ a ₊ b ⊆ xs ₊ b ₊ a
⊆-exch  zero           = succ zero
⊆-exch (succ zero)     = zero
⊆-exch (succ (succ i)) = succ (succ i)

⊆-refl : {A : Set} {xs : List A}
       → xs ⊆ xs
⊆-refl i = i

⊆-trans : {A : Set} {xs ys zs : List A}
        → xs ⊆ ys → ys ⊆ zs → xs ⊆ zs
⊆-trans r s i = s (r i)

⊆-ext : {A : Set} {xs : List A} (ys : List A) {a : A}
      → xs ₊₊ ys ⊆ xs ₊ a ₊₊ ys
⊆-ext  ε       = succ
⊆-ext (ys ₊ y) = ⊆-cons (⊆-ext ys)

⊆-ext₊₊ : {A : Set} {xs : List A} (ys zs : List A)
        → xs ₊₊ ys ⊆ xs ₊₊ ys ₊₊ zs
⊆-ext₊₊ ys  ε       = ⊆-refl
⊆-ext₊₊ ys (zs ₊ z) = ⊆-trans (⊆-ext₊₊ ys zs) succ

⊆-₊₊ : {A : Set} {xs ys : List A} (zs : List A)
     → xs ⊆ ys → xs ₊₊ zs ⊆ ys ₊₊ zs
⊆-₊₊  ε       r = r
⊆-₊₊ (zs ₊ z) r = ⊆-cons (⊆-₊₊ zs r)

ε₊₊ : {A : Set} {xs : List A} → xs ≡ ε ₊₊ xs
ε₊₊ {xs = ε}      = refl
ε₊₊ {xs = xs ₊ x} = ₊⁼ ε₊₊ refl

⊆-exch-end : {A : Set} {xs : List A} (ys : List A) {a : A}
           → xs ₊ a ₊₊ ys ⊆ xs ₊₊ ys ₊ a
⊆-exch-end  ε       = ⊆-refl
⊆-exch-end (ys ₊ y) = ⊆-trans (⊆-cons (⊆-exch-end ys)) ⊆-exch

⊆-exch-mid : {A : Set} {xs : List A} (ys : List A) {a : A}
           → xs ₊₊ ys ₊ a ⊆ xs ₊ a ₊₊ ys
⊆-exch-mid  ε       = ⊆-refl
⊆-exch-mid (ys ₊ y) = ⊆-trans ⊆-exch (⊆-cons (⊆-exch-mid ys))

⊆-₊₊' : {A : Set} {xs ys : List A} {zs : List A}
      → xs ⊆ ys → zs ₊₊ xs ⊆ zs ₊₊ ys
⊆-₊₊'                {zs = ε} r = transport² _⊆_ ε₊₊ ε₊₊ r
⊆-₊₊' {xs = xs} {ys} {zs ₊ z} r = ⊆-trans (⊆-exch-end xs) (⊆-trans (⊆-cons (⊆-₊₊' r)) (⊆-exch-mid ys))

⊆-₊₊r : {A : Set} {xs : List A} (ys : List A)
      → xs ⊆ xs ₊₊ ys
⊆-₊₊r  ε       = ⊆-refl
⊆-₊₊r (ys ₊ y) = ⊆-trans (⊆-₊₊r ys) succ

⊆-ext₊₊' : {A : Set} {xs : List A} (ys zs : List A)
         → xs ₊₊ zs ⊆ xs ₊₊ ys ₊₊ zs
⊆-ext₊₊' ys  ε       = ⊆-₊₊r ys
⊆-ext₊₊' ys (zs ₊ z) = ⊆-cons (⊆-ext₊₊' ys zs)

⊆-exch₊₊ : {A : Set} {xs : List A} (ys : List A) {a b : A}
         → xs ₊ a ₊ b ₊₊ ys ⊆ xs ₊ b ₊ a ₊₊ ys
⊆-exch₊₊ ys = ⊆-₊₊ ys ⊆-exch

\end{code}

Booleans

\begin{code}

data 𝟚 : Set where
 ⊤ ⊥ : 𝟚

if : {A : Set} → A → A → 𝟚 → A
if x y ⊤ = x
if x y ⊥ = y

\end{code}