Skip to content

Instantly share code, notes, and snippets.

@umazalakain
Last active January 11, 2021 10:53
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save umazalakain/3ddc7c43d772b83d3b9b282f78ab088e to your computer and use it in GitHub Desktop.
Save umazalakain/3ddc7c43d772b83d3b9b282f78ab088e to your computer and use it in GitHub Desktop.
{-
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 + 12
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...
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment