Code of Dependently typed programming in Agda

AgdaBasics.agda

module AgdaBasics where

data Bool : Set where
  true  : Bool
  false : Bool

not : Bool → Bool
not true  = false
not false = true

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

{-# BUILTIN NATURAL Nat #-}

1' : Nat
1' = suc zero

2' : Nat
2' = suc 1'

3' : Nat
3' = suc 2'

4' : Nat
4' = suc 3'

5' : Nat
5' = suc 4'

infixl 40 _+_
_+_ : Nat → Nat → Nat
zero  + m = m
suc n + m = suc (n + m)

infixl 60 _*_
_*_ : Nat → Nat → Nat
zero  * m = zero
suc n * m = m + (n * m)

infixr 20 _or_
_or_ : Bool → Bool → Bool
false or x = x
true  or _ = true

infix 5 if_then_else_
if_then_else_ : {A : Set} → Bool → A → A → A
if true  then x else y = x
if false then x else y = y

infixr 40 _∷_
data List (A : Set) : Set where
  []   : List A
  _∷_ : A → List A → List A

data _* (α : Set) : Set where
  ε   : α *
  _◁_ : α → α * → α *

-- 型 (A : Set) と 具体的な値 A を受け取り，具体的な値 A を返す函数
identity : (A : Set) → A → A
identity A x = x

zero' : Nat
zero' = identity Nat zero

identity₂ : (A : Set) → A → A
identity₂ = λ A x → x

identity₃ : (A : Set) → A → A
identity₃ = λ (A : Set) (x : A) → x

identity₄ : (A : Set) → A → A
identity₄ = λ (A : Set) x → x 

-- apply の型は，(A : Set) と (B : A → Set) の間の「→」 を省略している．省略せずに
-- かくとつぎのようになる．
-- apply : (A : Set) → (B : A → Set) → ((x : A) → B x) → (a : A) → B a
-- apply は，
-- Set型の値A(IntやBool等)，
-- A型の具体的な値(1, true, 'a'など)を受け取りSet型の値を返す函数B，
-- A型の値xを受け取ってxに函数Bを適用した値を返す函数，
-- A型の値a
-- の計4つの引数を受け取り，値aに函数Bを適用した値を返す函数を表す．
apply : (A : Set) → (B : A → Set) → ((x : A) → B x) → (a : A) → B a
apply A B f a = f a

id : {A : Set} → A → A
id x = x

true' : Bool
true' = id true

silly : {A : Set} {x : A} → A
silly {_} {x} = x

false' : Bool
false' = silly {x = false}

one : Nat
one = identity _ (suc zero)

_∘_ : {A : Set} {B : A → Set} {C : (x : A) → B x → Set}
      (f : {x : A} (y : B x) → C x y) (g : (x : A) → B x)
      (x : A) → C x (g x)
(f ∘ g) x = f (g x)

plus-two = suc ∘ suc

map : {A B : Set} → (A → B) → List A → List B
map f []        = []
map f (x ∷ xs) = f x ∷ map f xs

_++_ : {A : Set} → List A → List A → List A
[]        ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

data Vec (A : Set) : Nat → Set where
  []   : Vec A zero
  _∷_ : {n : Nat} → A → Vec A n → Vec A (suc n)

head : {A : Set} {n : Nat} → Vec A (suc n) → A
head (x ∷ xs) = x

vmap : {A B : Set} {n : Nat} → (A → B) → Vec A n → Vec B n
vmap f []        = []
vmap f (x ∷ xs) = f x ∷ vmap f xs

data Vec₂ (A : Set) : Nat → Set where
  nil  : Vec₂ A zero
  cons : (n : Nat) → A → Vec₂ A n → Vec₂ A (suc n)

vmap₂ : {A B : Set} (n : Nat) → (A → B) → Vec₂ A n → Vec₂ B n
vmap₂ .zero f nil              = nil
vmap₂ .(suc n) f (cons n x xs) = cons n (f x) (vmap₂ n f xs)

vmap₃ : {A B : Set} (n : Nat) → (A → B) → Vec₂ A n → Vec₂ B n
vmap₃ zero    f nil            = nil
vmap₃ (suc n) f (cons .n x xs) = cons n (f x) (vmap₃ n f xs)

data Image_∋_ {A B : Set} (f : A → B) : B → Set where
  im : (x : A) → Image f ∋ f x

inv : {A B : Set} (f : A → B) (y : B) → Image f ∋ y → A
inv f .(f x) (im x) = x

ans : Nat
ans = inv (id) (suc (suc (suc zero))) (im (suc (suc (suc zero))))

data Fin : Nat → Set where
  fzero : {n : Nat} → Fin (suc n)
  fsuc  : {n : Nat} → Fin n → Fin (suc n)

finExa1 : Fin 4'
finExa1 = (fsuc (fsuc fzero))

magic : {A : Set} → Fin zero → A
magic ()

data Empty : Set where
  empty : Fin zero → Empty

magic' : {A : Set} → Empty → A
magic' (empty ())

_!_ : {n : Nat} {A : Set} → Vec A n → Fin n → A
[] ! ()                       -- [] はVecの二つ目の引数に zero をもらっている
(x ∷ xs) ! fzero = x         --  から，n には zero が入っている．Fin zero 
(x ∷ xs) ! fsuc i = xs ! i   --  のときは，Fin 型の値は存在しないので () を使う．

tabulate : {n : Nat} {A : Set} → (Fin n → A) → Vec A n
tabulate {zero}  f = []
tabulate {suc n} f = f fzero ∷ tabulate (f ∘ fsuc)

tabExa1 : Fin (suc zero) → Bool
tabExa1 fzero = true
tabExa1 (fsuc x) = false

tabExa2 : Fin (suc (suc (suc zero))) → Bool
tabExa2 fzero = true
tabExa2 (fsuc x) = false

data   False : Set where
record True  : Set where

trivial : True
trivial = record {}

trivial2 : False  -- False を証明することはできない
trivial2 = {!!}   -- この { } を埋めることはできない

isTrue : Bool -> Set
isTrue true  = True
isTrue false = False

_<_ : Nat → Nat → Bool
_     < zero  = false
zero  < _     = true
suc m < suc n = m < n

length : {A : Set} → List A → Nat
length []       = zero
length (x ∷ xs) = suc (length xs)

lookup : {A : Set} (xs : List A) (n : Nat) →
         isTrue (n < length xs) → A
lookup [] n ()
lookup (x ∷ xs) zero    p = x
lookup (x ∷ xs) (suc n) p = lookup xs n p

ExampleList : List Bool
ExampleList = true ∷ true ∷ true ∷ false ∷ []


lookupExa1 : Bool
lookupExa1 = lookup ExampleList (suc (suc (suc zero))) record{}

data _==_ {A : Set} (x : A) : A → Set where
  refl : x == x

data _≤_ : Nat → Nat → Set where
  leq-zero : {n : Nat}   → zero ≤ n
  leq-suc  : {m n : Nat} → m ≤ n → suc m ≤ suc n

ExaEq0 : (suc (suc (suc zero))) == (suc (suc zero)) + (suc zero)
ExaEq0 = refl

ExaLeq1 : (suc (suc zero)) ≤ (suc (suc zero))
ExaLeq1 = leq-suc (leq-suc leq-zero)

ExaLeq2 : (suc zero) ≤ (suc zero) + (suc zero) + (suc zero)
ExaLeq2 = leq-suc leq-zero

leq-trans : {l m n : Nat} → l ≤ m → m ≤ n → l ≤ n
leq-trans leq-zero _ = leq-zero
leq-trans (leq-suc p) (leq-suc q) = leq-suc (leq-trans p q)

ExaLeqTrans : zero ≤ (suc (suc zero))
ExaLeqTrans = leq-trans leq-zero (leq-suc leq-zero)

min : Nat → Nat → Nat
min x y with x < y
min x y | true  = x
min x y | false = y

filter : {A : Set} → (A → Bool) → List A → List A
filter p [] = []
filter p (x ∷ xs) with p x
... | true  = x ∷ filter p xs
... | false = filter p xs

data _≠_ : Nat → Nat → Set where
  z≠s : {n : Nat} → zero ≠ suc n
  s≠z : {n : Nat} → suc n ≠ zero
  s≠s : {m n : Nat} → m ≠ n → suc m ≠ suc n

ExaNeq0 : (suc zero) ≠ (suc (suc zero))
ExaNeq0 = s≠s z≠s

data Equal? (n m : Nat) : Set where
  eq  : n == m → Equal? n m
  neq : n ≠  m → Equal? n m

ExaEq? : Set
ExaEq? = Equal? zero zero

equal? : (n m : Nat) → Equal? n m
equal? zero zero       = eq refl
equal? zero (suc m)    = neq z≠s
equal? (suc n) zero    = neq s≠z
equal? (suc n) (suc m) with equal? n m
equal? (suc n) (suc .n) | eq refl = eq refl
equal? (suc n) (suc m)  | neq p   = neq (s≠s p)

infix 20 _⊆_
data _⊆_ {A : Set} : List A → List A → Set where
  stop : [] ⊆ []
--  drop : ∀ {xs y ys} → xs ⊆ ys →     xs ⊆ y ∷ ys
  drop : forall {xs y ys} → xs ⊆ ys →     xs ⊆ y ∷ ys
--  keep : ∀ {x xs ys} → xs ⊆ ys → x ∷ xs ⊆ x ∷ ys
  keep : forall {x xs ys} → xs ⊆ ys → x ∷ xs ⊆ x ∷ ys
-- ∀ {x y} a b → A is shor for {x : _} {y : _} (a : _) (b : _) → A

ExaSub0 : (true ∷ []) ⊆ (true ∷ [])
ExaSub0 = keep stop

ExaSub1 : (false ∷ []) ⊆ (true ∷ false ∷ [])
ExaSub1 = drop (keep stop)

ExampleListA : List Bool
ExampleListA = true ∷ false ∷ true ∷ []

ExampleListB : List Bool
ExampleListB = true ∷ false ∷ true ∷ false ∷ true ∷ []

ExampleListC : List Bool
ExampleListC = true ∷ false ∷ true ∷ false ∷ false ∷ []

ExaSub2 : ExampleListA ⊆ ExampleListB
ExaSub2 = drop (drop (keep (keep (keep stop))))

ExaSub3 : ExampleListA ⊆ ExampleListC
ExaSub3 = keep (keep (keep (drop (drop stop))))

lem-filter : {A : Set} (p : A → Bool) (xs : List A) → filter p xs ⊆ xs
lem-filter p []        = stop
lem-filter p (x ∷ xs) with p x
... | true  = keep (lem-filter p xs)
... | false = drop (lem-filter p xs)

-- lem-plus-zero : (n : Nat) → n + zero == n
-- lem-plus-zero zero    = refl
-- lem-plus-zero (suc n) with n + zero | lem-plus-zero n
-- ____________________       ________   ________________
--             ↑                     
-- suc (n + zero) == (suc n)  n + zero   帰納法の仮定 
-- という命題                   をkと抽象    lem-plus-zero n の証明がある，と仮定
--
-- ... | k | l = {!!}
-- 
-- この後，l で case split すれば良い．

lem-plus-zero : (n : Nat) → n + zero == n
lem-plus-zero zero    = refl
lem-plus-zero (suc n) with n + zero | lem-plus-zero n
lem-plus-zero (suc n) | .n | refl = refl


module M where
  data Maybe (A : Set) : Set where
    nothing : Maybe A
    just    : A → Maybe A

  maybe : {A B : Set} → B → (A → B) → Maybe A → B
  maybe z f nothing  = z
  maybe z f (just x) = f x

module A where
  private
    internal : Nat
    internal = zero

  exported : Nat → Nat
  exported n = n + internal 

mapMaybe₁ : {A B : Set} → (A → B) → M.Maybe A → M.Maybe B
mapMaybe₁ f M.nothing  = M.nothing
mapMaybe₁ f (M.just x) = M.just (f x)

mapMaybe₂ : {A B : Set} → (A → B) → M.Maybe A → M.Maybe B
mapMaybe₂ f m = let open M in maybe nothing (just ∘ f) m

open M

mapMaybe₃ : {A B : Set} → (A → B) → Maybe A → Maybe B
mapMaybe₃ f m = maybe nothing (just ∘ f) m

open M hiding (maybe)
          renaming (Maybe to _option; nothing to none; just to some)

mapOption : {A B : Set} → (A → B) → A option → B option
mapOption f none     = none
mapOption f (some x) = just (f x)

mtrue : Maybe Bool
mtrue = mapOption not (just false)

module Sort (A : Set) (_<_ : A → A → Bool) where
  insert : A → List A → List A
  insert y [] = y ∷ []
  insert y (x ∷ xs) with x < y
  ... | true  = x ∷ insert y xs
  ... | false = y ∷ x ∷ xs

  sort : List A → List A
  sort []       = []
  sort (x ∷ xs) = insert x (sort xs)

sort₁ : (A : Set) (_<_ : A → A → Bool) → List A → List A
sort₁ = Sort.sort

module SortNat = Sort Nat _<_

sort₂ : List Nat → List Nat
sort₂ = SortNat.sort

NatListExample : List Nat
NatListExample = suc zero ∷ suc (suc (suc zero)) ∷ suc (suc zero) ∷ []


open Sort Nat _<_ renaming (insert to insertNat; sort to sortNat)

sort₃ : List Nat → List Nat
sort₃ = sortNat

module Lists (A : Set) (_<_ : A → A → Bool) where
  open Sort A _<_ public
  minimum : List A → Maybe A
  minimum xs with sort xs
  ... | []     = nothing
  ... | y ∷ ys = just y

import Logic using (_∧_; _∨_)

--open Logic using (_∧_; _∨_)  -- 左記の様に open すると コンストラクタが使えない?

-- OrExample : Bool ∨ Bool
-- OrExample = {!!}

record Point : Set where
  field x : Nat
        y : Nat

mkPoint : Nat → Nat → Point
mkPoint a b = record {x = a; y = b}

-- module Point (p : Point) where
--   x : Nat
--   y : Nat

PointExample : Point
PointExample = mkPoint zero (suc (suc zero))

getX : Point → Nat
getX = Point.x

getY : Point → Nat
getY = Point.y

abs² : Point → Nat
abs² p = let open Point p in x * x + y * y

record Monad (M : Set → Set) : Set₁ where
  field
    return : {A : Set} → A → M A
    _⟫=_   : {A B : Set} → M A → (A → M B) → M B

  mapM : {A B : Set} → (A → M B) → List A → M (List B)
  mapM f []        = return []
  mapM f (x ∷ xs) = f x ⟫= λ y → mapM f xs ⟫= λ ys → return (y ∷ ys)

mapM' : {M : Set → Set} → Monad M →
        {A B : Set} → (A → M B) → List A → M (List B)
mapM' Mon f xs = Monad.mapM Mon f xs

-- Exerceise 2.1
-- 行列を転置させる函数を定義せよ

Matrix : Set → Nat → Nat → Set
Matrix A n m = Vec (Vec A n) m

transposition : Matrix
transposition = {!!}

-- Exerceise 2.2

lem-!-tab : ∀ {A n} (f : Fin n → A) (i : Fin n) → (tabulate f ! i) == f i
lem-!-tab f fzero    = refl  
lem-!-tab f (fsuc i) = lem-!-tab (f ∘ fsuc) i

-- _!_ : {n : Nat} {A : Set} → Vec A n → Fin n → A
-- []      ! ()
-- (x ∷ xs) fzero    = x
-- (x ∷ xs) (fsuc i) = xs ! i 

-- tabulate : {n : Nat} {A : Set} → (Fin n → A) → Vec A n
-- tabulate {zero}  f = []
-- tabulate {suc n} f = f fzero ∷ tabulate (f ∘ fsuc)

-- (tabulate f ! fzero) == f fzero ⇒⇒⇒ (f fzero == f fzero) 
--
-- f    : Fin n → A
-- fsuc : {n : Nat} → Fin n → Fin (suc n)

-- lem-plus-zero : (n : Nat) → n + zero == n
-- lem-plus-zero zero    = refl
-- lem-plus-zero (suc n) with n + zero | lem-plus-zero n
-- lem-plus-zero (suc n) | .n | refl = refl

lem-tab-! : ∀ {A n} (xs : Vec A n) → tabulate (_!_ xs) == xs
lem-tab-! []        = refl
lem-tab-! (x ∷ xs) with tabulate (_!_ xs) | lem-tab-! xs
lem-tab-! (x ∷ xs) | .xs | refl = refl

-- tabulate (_!_ []) == [] ⇒⇒⇒ [] == []
--


-- infix 20 _⊆_
-- data _⊆_ {A : Set} : List A → List A → Set where
--  stop : [] ⊆ []
--  drop : ∀ {xs y ys} → xs ⊆ ys →     xs ⊆ y ∷ ys
--  keep : ∀ {x xs ys} → xs ⊆ ys → x ∷ xs ⊆ x ∷ ys
-- ∀ {x y} a b → A is shor for {x : _} {y : _} (a : _) (b : _) → A

⊆-refl : {A : Set} {xs : List A} → xs ⊆ xs
⊆-refl {A} {xs = []}      = stop           -- [] ⊆ [] の証明． xs = [] だから
⊆-refl {A} {xs = x ∷ xs} = keep (⊆-refl {A} {xs})

⊆-trans : {A : Set} {xs ys zs : List A} → xs ⊆ ys → ys ⊆ zs → xs ⊆ zs
⊆-trans p stop = p
⊆-trans stop (drop q) = drop q
⊆-trans (drop p) (drop q) = drop (⊆-trans (drop p) q)
⊆-trans (keep p) (drop q) = drop (⊆-trans (keep p) q)
⊆-trans (drop p) (keep q) = drop (⊆-trans p q)
⊆-trans (keep p) (keep q) = keep (⊆-trans p q)

infixr 30 _∷_ 
data SubList {A : Set} : List A → Set where
  []₂   : SubList []
  _∷₂_ : ∀ x {xs} → SubList xs → SubList (x ∷ xs)
  skip  : ∀ {x xs} → SubList xs → SubList (x ∷ xs)

forget : {A : Set} {xs : List A} → SubList xs → List A
forget []₂        = []
forget (x ∷₂ xs) = x ∷ forget xs
forget (skip xs)  = forget xs

lem-forget : {A : Set} {xs : List A} (zs : SubList xs) → forget zs ⊆ xs
lem-forget []₂       = stop
lem-forget (x ∷₂ zs) = keep (lem-forget zs)
lem-forget (skip zs) = drop (lem-forget zs)

filter' : {A : Set} → (A → Bool) → (xs : List A) → SubList xs
filter' p []        = []₂
filter' p (x ∷ xs) with p x
... | true  = x ∷₂ filter' p xs
... | false = skip (filter' p xs)

complement : {A : Set} {xs : List A} → SubList xs → SubList xs
complement {A} {[]} []₂ = []₂
complement {A} {x ∷ xs} (.x ∷₂ zs) = skip (complement zs)
complement {A} {x ∷ xs} (skip zs) = x ∷₂ complement zs

ListExa : List Nat
ListExa = 0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ []

SubListExa : SubList ListExa
SubListExa = skip (1 ∷₂ skip (3 ∷₂ skip []₂))

-- input tips: ⇒ (\r=)
-- C-u C-x =