Last active
January 11, 2021 10:53
-
-
Save umazalakain/3ddc7c43d772b83d3b9b282f78ab088e to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{- | |
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... | |
-} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment