DepTypes.agda

{-
FATA @ UoG                      Uma Zalakain
--------------------------------------------
Theorem Proving with Dependent Types in Agda
-}


{-
Agda
  is a "pure dependently typed total functional programming language"
  is a "proof assistant" / "interactive theorem prover" (like Coq and Idris)
  is used for "machine verification" / "mechanisation"
  has syntax à la Haskell (with `:` for `is of type` instead of `::` >_>)
  is interactive! program writing <-> type checking
-}


{-
Pure functional programming language
-}

data List (A : Set) : Set where -- `A : Set` reads `A is a type`
  []  : List A
  _∷_ : A → List A → List A

variable
  A B : Set
  P : A → Set

map : (A → B) → List A → List B
map f xs = {!!}

{-
Proof assistant
  based on Martin-Löf Type Theory
  dependent types: term → type
-}

data 𝟘 : Set where -- aka `⊥` (bottom) aka `empty set` aka `initial object`

absurd : 𝟘 → A
absurd b = {!!}

data 𝟙 : Set where -- aka `⊤` (top) aka `singleton` aka `void` aka `terminal object`
  tt : 𝟙

data 𝟚 : Set where -- aka `boolean` aka `bit`
  true  : 𝟚
  false : 𝟚

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

Even : ℕ → Set
Even n = {!!}

half : (n : ℕ) → Even n → ℕ
half n En = {!!}

{-
Totality:
  every possible input must deliver a result
  ensures soundness
  makes type checking decidable
  do we lose turing completeness? no!
-}

{-# NON_COVERING #-}
headUnsafe : List A → A
headUnsafe (x ∷ xs) = x

unsound : 𝟘
unsound = headUnsafe []

{-# TERMINATING #-}
unsound′ : 𝟘
unsound′ = unsound′


{-
Constructive logic
  through the Curry-Howard correspondence
  existence is constructed / witnessed
  no law of excluded middle (∀ toBe → toBe ⊎ ¬ toBe)
  no double negation elimination (¬ ¬ A → A)
  showing that non-existence is impossible provides no data
-}

_⇒_ : Set → Set → Set -- aka `function abstraction` aka `arrow`
A ⇒ B = A → B

¬_ : Set → Set
¬ A = A ⇒ 𝟘

data Π (A : Set) (P : A → Set) : Set where
  ∀Π : (∀ a → P a) → Π A P

data Σ (A : Set) (P : A → Set) : Set where
  _,_ : ∀ a → P a → Σ A P

_×_ : Set → Set → Set
A × B = Σ A (λ _ → B)

infix 5 _⊎_
data _⊎_ (A : Set) (B : Set) : Set where
  inl : A → A ⊎ B
  inr : B → A ⊎ B

doubleneg-intro : A → ¬ ¬ A
doubleneg-intro a = {!!}

not-all-ℕs-are-even : ¬ Π ℕ Even
not-all-ℕs-are-even p = {!!}

there-exists-an-even-ℕ : Σ ℕ Even
there-exists-an-even-ℕ = {!!}

all-ℕ-are-either-even-or-not-even : ∀ n → Even n ⊎ ¬ Even n
all-ℕ-are-either-even-or-not-even n = {!!}

{-
Propositional (intensional) equality
-}

infix 10 _≡_
data _≡_ : A → A → Set where
  refl : {x : A} → x ≡ x

_≢_ : A → A → Set
x ≢ y = ¬ (x ≡ y)

sym : {x y : A} → x ≡ y → y ≡ x
sym eq = {!!}

trans : {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans eq qe = {!!}

cong : {x y : A} (f : A → B) → x ≡ y → f x ≡ f y
cong f eq = {!!}

subst : {x y : A} → x ≡ y → P x → P y
subst eq px = {!!}

-- Constructors are disjoint
zero-suc : ∀ {n} → zero ≢ suc n
zero-suc eq = {!!}

-- Constructors are injective
suc-injective : ∀ {n m} → suc n ≡ suc m → n ≡ m
suc-injective eq = {!!}


{-
Definitional equality
-}

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

{-# BUILTIN NATURAL ℕ #-}
1+1≡2 : 1 + 1 ≡ 2
1+1≡2 = {!!}

{-
Definitional vs propositional
-}

+-idˡ : ∀ {n} → 0 + n ≡ n
+-idˡ = {!!}

+-idʳ : ∀ {n} → n ≡ n + 0
+-idʳ = {!!}

{-
Tools: equational reasoning
  also available in other flavours (preorders etc)
-}

infix  3 _∎
infixr 2 step-≡
infix  1 begin_

begin_ : ∀{x y : A} → x ≡ y → x ≡ y
begin_ x≡y = x≡y

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

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

+-suc : ∀ n m → suc (n + m) ≡ n + suc m
+-suc zero m = refl
+-suc (suc n) m = cong suc (+-suc n m)

+-comm : ∀ n m → n + m ≡ m + n
+-comm zero m = {!!}
+-comm (suc n) m = begin
  suc (n + m)    ≡⟨ {!!} ⟩
  (m + suc n)    ∎

{-
Applications to programming:
  - restrict domain of arguments (eg division)
  - explicitly maintain invariants
  - assert functional properties
-}

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

replicate : A → (n : ℕ) → Vec A n
replicate x n = {!!}

head : ∀ {n} → Vec A (suc n) → A
head xs = {!!}

_++_ : ∀ {n m} → Vec A n → Vec A m → Vec A (n + m)
xs ++ ys = {!!}

data Fin : ℕ → Set where
  zero : ∀ {n} → Fin (suc n)
  suc  : ∀ {n} → Fin n → Fin (suc n)

_!_ : ∀ {n} → Vec A n → Fin n → A
xs ! i = {!!}

{-
Applications to theorem proving

  Great educational tool!

  Programming Languages theory
    - formalisation of programming languages
    - verification of metatheoretical properties

  Homotopy Type Theory
    - univalent foundations
    - equality between types (cubical: computes!)
    - topological results

  Topology, category theory, number theory, group theory, analysis...
-}