Intro

{-# OPTIONS --allow-unsolved-metas --without-K #-}

Curry-Howard correspondence

Proof rules and the rules of type systems correspond to each other:

Logic Programs
cf. GLoIn cf. ThProg
Logical formulas A ∧ B → A Types of programs A × B → A
Proofs Γ ⊢ A ∧ B → A Typing: Γ ⊢ (λ p. p λ x y. x) : A × B → A
Implication A → B Function type A → B
Conjunction A ∧ B Product type A × B
Disjunction A ∨ B Union type A + B
Universal quantifier ∀x.φ(x) Polymorphism ∀ x.φ(x)

⇒ We prove mathematical statements by constructing programs of the appropriate type.

Syntax

  • Haskell-like
  • Identifiers: UTF-8 character strings separated by whitespace and .;{}()@"

Function types

Agda is dependently typed, which means that types can depend on values. Since 'Set' is itself a type, this lets us implement polymorphism:

id : ∀ (S : Set) → S → S
id S x = x

Here S is a value of type Set.

id' : ∀ (S : Set) → (S → S)
id' = λ S → λ x → x

The function type S → S itself also lives in Set:

Endofunction : Set → Set
Endofunction S = S → S

-- Definition using Endofunction:
id₂ : ∀ (S : Set) → Endofunction S
id₂ S x = x

Holes

Instead of top to bottom, one writes Agda programs from the outside in:

id₃ : ∀ (S : Set) → Endofunction S
id₃ S x = x -- Replace x by ? to create a hole

Operatoren

_∨_ : Set → Set → Set₁
A ∨ B = ∀ (C : Set) → (A → C) → (B → C) → C

_∧_ : Set → Set → Set₁
A ∧ B = ∀ (C : Set) → (A → B → C) → C
  • If a function X -> Y has X and Y at level ℓ, then (X → Y) is at level ℓ too
  • A function X -> Y means: ∀ (x : X) → Y
  • The parameter C is of type Set
  • => Set → Set ∈ Set₁

Modules

module Logic-Examples (A : Set) (B : Set) where
  ∨-comm : (A ∨ B) → (B ∨ A)
  ∨-comm A∨B C B→C A→C = A∨B C A→C B→C

Data types

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


_+_ : ℕ → ℕ → ℕ
zero + b = b
suc a + b = suc (a + b)

open import Data.Bool using (Bool; true; false)

_≡?_ : ℕ → ℕ → Bool
zero ≡? zero      = true
zero ≡? suc b     = false 
suc a ≡? zero     = false
suc a ≡? suc b    = a ≡? b

data _≡_ {ℓ} {X : Set ℓ} : X → X → Set ℓ where
  refl : ∀ (x : X) → x ≡ x

infix 4 _≡_

zero+a≡a : ∀ (a : ℕ) → zero + a ≡ a
zero+a≡a a = refl a

[End of lecture on 13 April 2026]

Implicit arguments

  • Function arguments can be omitted if they are determined automatically by unification.
  • Syntax:
  • {…} to mark an argument as implicit in a function definition
  • _ to let Agda figure out an explicit argument at a call site.
-- Functions preserve equality:
cong : ∀ {a b : ℕ} → (f : ℕ → ℕ) → a ≡ b → f a ≡ f b
cong f (refl a) = refl (f a)

-- When we call cong, the values of a and b follow
-- automatically from `a ≡ b`
a+zero≡a : ∀ (a : ℕ) → a + zero ≡ a
a+zero≡a zero = refl zero
a+zero≡a (suc a) =
  cong {a + zero} {a} suc (a+zero≡a a)
  -- identical to: cong {a + zero} {a} suc (a+zero≡a a)

Another example: the implicit carrier set in _≡_ above. In the stdlib the parameter of refl is implicit, since it is usually determined by the context, as for instance in the definition of sym:

sym : ∀ {X : Set} {a : X} {b} → a ≡ b → b ≡ a
sym (refl _) = refl _
--        ^         ^--- Agda infers the parameter from the context
--        '----  The value gets no name, but is still available:
--               a : ℕ   (not in scope)

trans : ∀ {X : Set} {a b c : X} → a ≡ b → b ≡ c → a ≡ c
trans (refl x) eq = eq

+-suc : ∀ a b → suc (a + b) ≡ (a + suc b)
+-suc zero b = refl (suc b)
+-suc (suc a) b = cong suc (+-suc a b)

+-comm₀ : ∀ a b → a + b ≡ b + a
+-comm₀ zero b = sym (a+zero≡a b)
+-comm₀ (suc a) b = trans (cong suc IH) (+-suc b a)
  where
    IH = +-comm₀ a b


subst : ∀ {a b : ℕ} → (P : ℕ → Set) → a ≡ b → P a → P b
subst P (refl a) = id (P a)

+-comm : ∀ a b → _≡_ (a + b) (b + a)
+-comm zero b = sym (a+zero≡a b)
+-comm (suc a) b = trans (cong suc (+-comm a b)) (+-suc b a)

Equational Reasoning

_∎ : ∀ {X : Set} (n : X) → n ≡ n
_∎ = refl
infix 3 _∎

_≡⟨_⟩_ : ∀ {X : Set} n {m} → n ≡ m → {ℓ : X} → m ≡ ℓ → n ≡ ℓ
n ≡⟨ n≡m ⟩ m≡ℓ = trans n≡m m≡ℓ 
infixr 2 _≡⟨_⟩_

+-comm' : ∀ a b → _≡_ (a + b) (b + a)
+-comm' zero b = sym (a+zero≡a b)
+-comm' (suc a) b =
        (suc a + b) ≡⟨ cong suc (+-comm' a b) ⟩
        suc (b + a) ≡⟨ +-suc b a ⟩
        (b + suc a) ∎

Warning: the equational chains in the stdlib start with begin_

Decision procedures

  • Embedding Bool ↪ Set
  • Correctness proof for _≡?_
  • Dot patterns
-- import Data.Empty
data ⊥ : Set where

-- import Data.Unit
data ⊤ : Set where
  tt : ⊤

Truth : Bool → Set
Truth false = ⊥
Truth true = ⊤

≡?-⇐ : ∀ a b → a ≡ b → Truth (a ≡? b)
≡?-⇐ zero a (refl a) = tt
≡?-⇐ (suc a) (suc a) (refl (suc a)) = ≡?-⇐ a a (refl _)

[End of lecture on 16 April 2026]

In ≡?-⇐ we use the principle of "forcing".

Converse direction:

≡?-⇒ : ∀ a b → Truth (a ≡? b) → a ≡ b
≡?-⇒ zero zero t = refl _
≡?-⇒ zero (suc b) ()   -- no '=' here, () ≡ "impossible pattern"
≡?-⇒ (suc a) (suc b) t = cong suc (≡?-⇒ a b t)

Level

import Level as L
open import Level using (Level)

weak-initial : {ℓ : Level} (X : Set ℓ) → Set (L.suc ℓ)
weak-initial {ℓ} X = ∀ (Y : Set ℓ) → (X → Y)

Functions

_∘_ : ∀ {ℓ₁ ℓ₂ ℓ₃} {X : Set ℓ₁} {Y : Set ℓ₂} {Z : Set ℓ₃} →
        (Y → Z) → (X → Y) → (X → Z)
(g ∘ f) x = g (f x)

∘-assoc : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} {W : Set ℓ₁} {X : Set ℓ₂} {Y : Set ℓ₃} {Z : Set ℓ₄}
          (f : W → X) (g : X → Y) (h : Y → Z) → h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f
∘-assoc f g h = refl _

Records

module Non-Dependent-Product where

The usual product is a record:

  record _×_ {ℓ ℓ' : Level} (X : Set ℓ) (Y : Set ℓ') : Set (ℓ L.⊔ ℓ') where
    constructor _,_
    field
      fst : X
      snd : Y

  module ×-properties {ℓ ℓ' : Level} (X : Set ℓ) (Y : Set ℓ') where
    swap : X × Y → Y × X
    swap (x , y) = y , x

    swap' : X × Y → Y × X
    swap' p =
      record
      { fst = p.snd
      ; snd = p.fst
      }
      where
        module p = _×_ p

Dependent-Product:

record Σ {ℓ ℓ' : Level} (X : Set ℓ) (P : X → Set ℓ') : Set (ℓ L.⊔ ℓ') where
  constructor _,_
  field
    fst : X
    snd : P fst

syntax Σ A (λ x → B) = Σ[ x ∈ A ] B

_×_ : {ℓ ℓ' : Level} (X : Set ℓ) (Y : Set ℓ')
      → Set (ℓ Level.⊔ ℓ')
X × Y = Σ X (λ x → Y)

∃ : {ℓ ℓ' : Level} {X : Set ℓ} (P : X → Set ℓ') → Set (ℓ L.⊔ ℓ')
∃ = Σ _
syntax ∃ (λ x → B) = ∃[ x ] B

Currying the dependent product = dependent functions:

module Dependent-Currying (X : Set) (P : X → Set) (Y : Set) where
  curry : (Σ[ x ∈ X ] (P x) → Y) → (∀ (x : X) → P x → Y)
  curry f x Px = f (x , Px)

  uncurry : (∀ (x : X) → P x → Y) → (Σ[ x ∈ X ] (P x) → Y)
  uncurry f (x , Px) = f x Px

  _⇔_ : Set → Set → Set
  X ⇔ Y = (X → Y) × (Y → X)

  [un]curry : (∀ (x : X) → P x → Y) ⇔ (∃[ x ] (P x) → Y)
  [un]curry = uncurry , curry

  uncurry∘curry≡id : uncurry ∘ curry ≡ id _
  uncurry∘curry≡id = refl (uncurry ∘ curry)

  curry∘uncurry≡id : curry ∘ uncurry ≡ id (∀ (x : X) → P x → Y)
  curry∘uncurry≡id = refl _

Functions

The relation f ≐ g expresses that the functions f and g are pointwise identical:

_≐_ : ∀ {ℓ₁ ℓ₂} {X : Set ℓ₁} {Y : Set ℓ₂} (f g : X → Y) → Set (ℓ₁ L.⊔ ℓ₂)
f ≐ g = ∀ x → f x ≡ g x

Stdlib

import Function.Base using (_∘_) -- ∘ allows composition of dependent functions

Agda Quellcode herunterladen