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
ℕᴺ =

: ℕᴺ
i = 0

head : {A : Set}  A   A

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}