Preliminaries

Chuangjie Xu, August 2017

\begin{code}

module Preliminaries where

\end{code}

Identity types

\begin{code}

infix 2 _≡_

data _≡_ {A : Set} (a : A) : A → Set where
 refl : a ≡ a

sym : {A : Set} {x y : A}
    → x ≡ y → y ≡ x
sym refl = refl

trans : {A : Set} {x y z : A}
      → x ≡ y → y ≡ z → x ≡ z
trans refl p = p

ap : {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
ap f refl = refl

transport : {A : Set} (P : A → Set) {x y : A}
          → x ≡ y → P x → P y
transport P refl p = p

infix  3 _∎
infixr 2 _≡⟨_⟩_

_≡⟨_⟩_ : ∀ {A} (x {y z} : A) → x ≡ y → y ≡ z → x ≡ z
_ ≡⟨ x≡y ⟩ y≡z = trans x≡y y≡z

_∎ : ∀ {A} (x : A) → x ≡ x
_∎ _ = refl

\end{code}

Function composition

\begin{code}

infixr 10 _∘_

_∘_ : {X Y Z : Set} → (Y → Z) → (X → Y) → (X → Z)
(g ∘ f) x = g (f x)

\end{code}

Σ-types and binary products

\begin{code}

infixr 1 _,_

record Σ {A : Set} (B : A → Set) : Set where
 constructor _,_
 field
  pr₁ : A
  pr₂ : B pr₁

open Σ public

infixr 1 _×_ _∧_

_×_ : Set → Set → Set
A × B = Σ \(a : A) → B

_∧_ : Set → Set → Set
_∧_ = _×_

\end{code}

Empty type and negation

\begin{code}

data 𝟘 : Set where

¬ : Set → Set
¬ A = A → 𝟘

𝟘rec : {A : Set} → 𝟘 → A
𝟘rec ()

\end{code}

Coproducts

\begin{code}

infixr 1 _∨_

data _∨_ (A B : Set) : Set where
 inl : A → A ∨ B
 inr : B → A ∨ B

if : {A B C : Set} → A ∨ B → C → C → C
if (inl _) c₀ c₁ = c₀
if (inr _) c₀ c₁ = c₁

ifᵈ-specᴸ : {A C : Set} (w : ¬ A ∨ A) {c₀ c₁ : C}
          → ¬ A → if w c₀ c₁ ≡ c₀
ifᵈ-specᴸ (inl _) _ = refl
ifᵈ-specᴸ (inr a) f = 𝟘rec (f a)

ifᵈ-specᴿ : {A C : Set} (w : ¬ A ∨ A) {c₀ c₁ : C}
          → A → if w c₀ c₁ ≡ c₁
ifᵈ-specᴿ (inl f) a = 𝟘rec (f a)
ifᵈ-specᴿ (inr _) _ = refl

case : {A B C : Set} → (A → C) → (B → C) → A ∨ B → C
case f g (inl a) = f a
case f g (inr b) = g b

\end{code}

Natural numbers

\begin{code}

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

{-# BUILTIN NATURAL ℕ #-}

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

infixl 10 _+_

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

infixl 10 _-_

_-_ : ℕ → ℕ → ℕ
0      - m      = 0
succ n - 0      = succ n
succ n - succ m = n - m

Lm[n+1-n=1] : (n : ℕ) → succ n - n ≡ 1
Lm[n+1-n=1]  0       = refl
Lm[n+1-n=1] (succ n) = Lm[n+1-n=1] n

Lm[k+1=n+1-m→k=n-m] : {n m k : ℕ} → succ k ≡ succ n - m → k ≡ n - m
Lm[k+1=n+1-m→k=n-m] {0}      {0}      refl = refl
Lm[k+1=n+1-m→k=n-m] {0}      {succ m} ()
Lm[k+1=n+1-m→k=n-m] {succ n} {0}      refl = refl
Lm[k+1=n+1-m→k=n-m] {succ n} {succ m} e    = Lm[k+1=n+1-m→k=n-m] {n} e

infix 2 _≤_ _≥_ _<_ _>_

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

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

_>_ : ℕ → ℕ → Set
n > m = ¬ (n ≤ m)

_<_ : ℕ → ℕ → Set
n < m = m > n

≤refl : {n : ℕ} → n ≤ n
≤refl {0}      = ≤zero
≤refl {succ n} = ≤succ ≤refl

≤-trans : {n m k : ℕ} → n ≤ m → m ≤ k → n ≤ k
≤-trans  ≤zero     s        = ≤zero
≤-trans (≤succ r) (≤succ s) = ≤succ (≤-trans r s)

<-≤-trans : {n m k : ℕ} → n < m → m ≤ k → n < k
<-≤-trans r  ≤zero     _        = r ≤zero
<-≤-trans r (≤succ u) (≤succ v) = <-≤-trans (λ z → r (≤succ z)) u v

≤succʳ : {n m : ℕ} → n ≤ m → n ≤ succ m
≤succʳ  ≤zero    = ≤zero
≤succʳ (≤succ r) = ≤succ (≤succʳ r)

≤pred : {n m : ℕ} → succ n ≤ succ m → n ≤ m
≤pred (≤succ r) = r

<pred : {n m : ℕ} → succ n < succ m → n < m
<pred f r = f (≤succ r)

Lm[<→Σ] : {n m : ℕ} → n < m → Σ \k → succ k ≡ m - n
Lm[<→Σ] {m}      {0}      r = 𝟘rec (r ≤zero)
Lm[<→Σ] {0}      {succ m} r = m , refl
Lm[<→Σ] {succ n} {succ m} r = Lm[<→Σ] (<pred r)

Lm[≤-dec] : (n m : ℕ) → (n > m) ∨ (n ≤ m)
Lm[≤-dec]  0        m       = inr ≤zero
Lm[≤-dec] (succ n)  0       = inl (λ ())
Lm[≤-dec] (succ n) (succ m) = case c₀ c₁ (Lm[≤-dec] n m)
 where
  c₀ : n > m → (succ n > succ m) ∨ (succ n ≤ succ m)
  c₀ r = inl (λ s → r (≤pred s))
  c₁ : n ≤ m → (succ n > succ m) ∨ (succ n ≤ succ m)
  c₁ r = inr (≤succ r)

Lm[≤-cases] : {n m : ℕ}
            → n ≤ m → n ≡ m ∨ n < m
Lm[≤-cases] {0}      {0}       ≤zero    = inl refl
Lm[≤-cases] {0}      {succ m}  ≤zero    = inr (λ ())
Lm[≤-cases] {succ n} {succ m} (≤succ r) = case claim₀ claim₁ IH
 where
  IH : n ≡ m ∨ n < m
  IH = Lm[≤-cases] r
  claim₀ : n ≡ m → succ n ≡ succ m ∨ succ n < succ m
  claim₀ e = inl (ap succ e)
  claim₁ : n < m → succ n ≡ succ m ∨ succ n < succ m
  claim₁ f = inr (f ∘ ≤pred)

Lm[n=m→n+1>m] : {n m : ℕ} → n ≡ m → succ n > m
Lm[n=m→n+1>m] {0}      refl ()
Lm[n=m→n+1>m] {succ n} refl r  = Lm[n=m→n+1>m] refl (≤pred r)

Lm[n=m>k→n>k] : {n m k : ℕ} → n ≡ m → m > k → n > k
Lm[n=m>k→n>k] refl r = r

Lm[n<m→n+1≤m] : {n m : ℕ} → n < m → succ n ≤ m
Lm[n<m→n+1≤m] {n}      {0}      f = 𝟘rec (f ≤zero)
Lm[n<m→n+1≤m] {0}      {succ m} f = ≤succ ≤zero
Lm[n<m→n+1≤m] {succ n} {succ m} f = ≤succ (Lm[n<m→n+1≤m] (f ∘ ≤succ))

Lm[n+1≤m→n≤m] : {n m : ℕ} → succ n ≤ m → n ≤ m
Lm[n+1≤m→n≤m] {0}      (≤succ r) = ≤zero
Lm[n+1≤m→n≤m] {succ n} (≤succ r) = ≤succ (Lm[n+1≤m→n≤m] r)

Lm[n<m→n<m+1] : {n m : ℕ} → n < m → n < succ m
Lm[n<m→n<m+1] f r = f (Lm[n+1≤m→n≤m] r)

Lm[n≤m→n<m+1] : {n m : ℕ} → n ≤ m → n < succ m
Lm[n≤m→n<m+1]  ≤zero    ()
Lm[n≤m→n<m+1] (≤succ r) (≤succ s) = Lm[n≤m→n<m+1] r s

max : ℕ → ℕ → ℕ
max  0        m       = m
max (succ n)  0       = succ n
max (succ n) (succ m) = succ (max n m)

max-spec₀ : (n m : ℕ) → n ≤ max n m
max-spec₀  0        m       = ≤zero
max-spec₀ (succ n)  0       = ≤refl
max-spec₀ (succ n) (succ m) = ≤succ (max-spec₀ n m)

max-spec₁ : (n m : ℕ) → m ≤ max n m
max-spec₁  0        m       = ≤refl
max-spec₁ (succ n)  0       = ≤zero
max-spec₁ (succ n) (succ m) = ≤succ (max-spec₁ n m)

\end{code}

Infinite lists

\begin{code}

_ᴺ : Set → Set
A ᴺ = ℕ → A

ℕᴺ : Set
ℕᴺ = ℕ ᴺ

0ʷ : ℕᴺ
0ʷ i = 0

head : {A : Set} → A ᴺ → A
head α = α 0

tail : {A : Set} → A ᴺ → A ᴺ
tail α i = α (succ i)

\end{code}

Finite lists

\begin{code}

data _* (A : Set) : Set where
 ⟨⟩  : A *
 _,_ : A → A * → A *

ℕ* : Set
ℕ* = ℕ *

⟨_⟩ : {A : Set} → A → A *
⟨ x ⟩ = x , ⟨⟩

∣_∣ : {A : Set} → A * → ℕ
∣ ⟨⟩ ∣     = 0
∣ _ , xs ∣ = succ ∣ xs ∣

_✷_ : {A : Set} → A * → A * → A *
⟨⟩ ✷ ys = ys
(x , xs) ✷ ys = x , xs ✷ ys

_✶_ : {A : Set} → A * → A → A *
xs ✶ x = xs ✷ ⟨ x ⟩

Lm[|xs✶x|=|xs|+1] : {A : Set} (xs : A *) {x : A}
                  → ∣ xs ✶ x ∣ ≡ succ ∣ xs ∣
Lm[|xs✶x|=|xs|+1] ⟨⟩       = refl
Lm[|xs✶x|=|xs|+1] (_ , xs) = ap succ (Lm[|xs✶x|=|xs|+1] xs)

_✵_ : {A : Set} → A * → A ᴺ → A ᴺ
⟨⟩ ✵ α = α
((a , as) ✵ α)  0       = a
((a , as) ✵ α) (succ i) = (as ✵ α) i

infix 10 _≼_

data _≼_ {A : Set} : A * → A * → Set where
 ≼base : {ys : A *} → ⟨⟩ ≼ ys
 ≼step : {xs ys : A *} {a : A} → xs ≼ ys → (a , xs) ≼ (a , ys)

Lm[≼-✷] : {A : Set} (xs : A *) {ys : A *} → xs ≼ (xs ✷ ys)
Lm[≼-✷] ⟨⟩       = ≼base
Lm[≼-✷] (x , xs) = ≼step (Lm[≼-✷] xs)

Lm[≼→∣≤∣] : {A : Set} {u v : A *} → u ≼ v → ∣ u ∣ ≤ ∣ v ∣
Lm[≼→∣≤∣]  ≼base    = ≤zero
Lm[≼→∣≤∣] (≼step r) = ≤succ (Lm[≼→∣≤∣] r)

data _∋_ {A : Set} : A * → A ᴺ → Set where
 ∋base : {α : A ᴺ} → ⟨⟩ ∋ α
 ∋step : {a : A} {u : A *} {α : A ᴺ} → a ≡ head α → u ∋ tail α → (a , u) ∋ α

Lm[∋-✵] : {A : Set} (u : A *) {α : A ᴺ} → u ∋ (u ✵ α)
Lm[∋-✵]  ⟨⟩     = ∋base
Lm[∋-✵] (a , u) = ∋step refl (Lm[∋-✵] u)

Lm[∋-✷✵] : {A : Set} (u : A *) {v : A *} {α : A ᴺ} → u ∋ ((u ✷ v) ✵ α)
Lm[∋-✷✵]  ⟨⟩     = ∋base
Lm[∋-✷✵] (a , u) = ∋step refl (Lm[∋-✷✵] u)

Lm[≼→∋] : {A : Set} {u v : A *} {α : A ᴺ} → u ≼ v → u ∋ (v ✵ α)
Lm[≼→∋]  ≼base    = ∋base
Lm[≼→∋] (≼step r) = ∋step refl (Lm[≼→∋] r)

Lm[∋≤→≡] : {A : Set} {u : A *} {α β : A ᴺ}
         → u ∋ α → {n : ℕ} → n < ∣ u ∣ → (u ✵ β) n ≡ α n
Lm[∋≤→≡]  ∋base               r = 𝟘rec (r ≤zero)
Lm[∋≤→≡] (∋step e v) {0}      r = e
Lm[∋≤→≡] (∋step e v) {succ n} r = Lm[∋≤→≡] v (<pred r)

\end{code}

Decidable predicates as boolean-valued functions

\begin{code}

data 𝟚 : Set where
 𝟎 𝟏 : 𝟚

Lm[0≢1] : ¬ (𝟎 ≡ 𝟏)
Lm[0≢1] ()

¬² : 𝟚 → 𝟚
¬² 𝟎 = 𝟏
¬² 𝟏 = 𝟎

_∧²_ : 𝟚 → 𝟚 → 𝟚
𝟎 ∧² b = 𝟎
𝟏 ∧² b = b

∧²intro : {a b : 𝟚} → a ≡ 𝟏 → b ≡ 𝟏 → (a ∧² b) ≡ 𝟏
∧²intro refl refl = refl

∧²elim₀ : {a b : 𝟚} → (a ∧² b) ≡ 𝟏 → a ≡ 𝟏
∧²elim₀ {𝟎} ()
∧²elim₀ {𝟏} _ = refl

∧²elim₁ : {a b : 𝟚} → (a ∧² b) ≡ 𝟏 → b ≡ 𝟏
∧²elim₁ {𝟎} {𝟎} ()
∧²elim₁ {𝟏} {𝟎} ()
∧²elim₁ {𝟎} {𝟏} _ = refl
∧²elim₁ {𝟏} {𝟏} _ = refl

∧²elim₁' : {a b : 𝟚} → (a ∧² b) ≡ 𝟎 → a ≡ 𝟏 → b ≡ 𝟎
∧²elim₁' e refl = e


_≤²_ : ℕ → ℕ → 𝟚
0      ≤² m      = 𝟏
succ n ≤² 0      = 𝟎
succ n ≤² succ m = n ≤² m

_≥²_ : ℕ → ℕ → 𝟚
n ≥² m = m ≤² n

_>²_ : ℕ → ℕ → 𝟚
n >² m = ¬² (n ≤² m)

_<²_ : ℕ → ℕ → 𝟚
n <² m = m >² n

<²elim : {n m : ℕ} → (n <² m) ≡ 𝟏 → n < m
<²elim {n}      {0}      ()
<²elim {0}      {succ m} _  ()
<²elim {succ n} {succ m} e  (≤succ r) = <²elim e r

<²elim' : {n m : ℕ} → (n <² m) ≡ 𝟎 → n ≥ m
<²elim' {n}      {0}      _ = ≤zero
<²elim' {0}      {succ m} ()
<²elim' {succ n} {succ m} e = ≤succ (<²elim' e)

<²intro : {n m : ℕ} → n < m → (n <² m) ≡ 𝟏
<²intro {n}      {0}      r = 𝟘rec (r ≤zero)
<²intro {0}      {succ m} r = refl
<²intro {succ n} {succ m} r = <²intro (<pred r)

Lm[1∨0] : {b : 𝟚} → b ≡ 𝟏 ∨ b ≡ 𝟎
Lm[1∨0] {𝟎} = inr refl
Lm[1∨0] {𝟏} = inl refl

infix 2 _∈_ _∉_

_∈_ _∉_ : {A : Set} → A → (A → 𝟚) → Set
a ∈ Q = Q a ≡ 𝟏
a ∉ Q = Q a ≡ 𝟎

decidable-predicate : {A : Set} (Q : A → 𝟚) {a : A}
                    → a ∈ Q ∨ a ∉ Q
decidable-predicate _ = Lm[1∨0]

\end{code}