Intro
=====
```
{-# OPTIONS --allow-unsolved-metas --without-K #-}
```

Curry-Howard-Korrespondenz
--------------------------

Beweis-Regeln und Regeln von Typsystemen stehen in Korrespondenz zueinander:

| Logik                      | Programme                                       |
| -------------------------- | ----------------------------------------------- |
| vgl. GLoIn                 | vgl. ThProg                                     |
| Logische Formeln A ∧ B → A | Typen von Programmen A × B → A                  |
| Beweise Γ ⊢ A ∧ B → A      | Typisierung:  Γ ⊢ (λ p. p λ x y. x) : A × B → A |
| Implikation A → B          | Funktionstyp A → B                              |
| Konjunktion A ∧ B          | Produkt-Typ A × B                               |
| Disjunktion A ∨ B          | Union-Typ A + B                                 |
| Allquantor  ∀x.φ(x)        | Polymorphismus ∀ x.φ(x)                         |

⇒ Wir beweisen mathematische Aussagen, indem wir Programme mit dem
passenden Typ konstruieren.


Syntax
------

* Haskell-artig
* Identifier: UTF-8-Zeichenkennten getrennt durch *Leerzeichen* und `.;{}()@"`

Funktionstypen
--------------

Agda ist dependently-typed, das bedeutet, dass Typen von Werten abhängen können.
Da 'Set' ist selbst ein Typ, lässt sich damit Polymorphismus, implementieren:
```
id : ∀ (S : Set) → S → S
id S x = x
```

Hier ist `S` ein Wert vom Typ `Set`.
```
id' : ∀ (S : Set) → (S → S)
id' = λ S → λ x → x
```

Der Funktionstyp `S → S` selbst liegt auch in `Set`:
```
Endofunction : Set → Set
Endofunction S = S → S
```

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

Holes
-----
Statt von oben nach unten schreibt man Agda-Programme von außen nach innen:

```
id₃ : ∀ (S : Set) → Endofunction S
id₃ S x = x -- Ersetzen Sie x durch ? um ein Hole zu erzeugen
```

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

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

* Funktion X -> Y und X und Y auf level ℓ, dann ist (X → Y) auch auf Level ℓ
* Funktion X -> Y bedeutet: ∀ (x : X) → Y
* Parameter C ist vom Typ 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
```


Datentypen
----------

```
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
```

[Ende der Vorlesung am 13. April 2026]

Implizite Argumente
-------------------
* Funktionsargumente können weggelassen werden, wenn sich diese durch die
  Unifikation automatisch ergeben.
* Syntax:
  - `{…}` um in der Funktionsdefinition ein Argument als implizit zu markieren
  - `_` um beim Funktionsaufruf ein explizites Argument von Agda finden zu lassen.

```
-- Funktionen erhalten Gleichheit:
cong : ∀ {a b : ℕ} → (f : ℕ → ℕ) → a ≡ b → f a ≡ f b
cong f (refl a) = refl (f a)

-- Wenn wir cong aufurufen, dann ergeben sich die Werte für
-- a und b automatisch aus `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)
  -- identisch zu: cong {a + zero} {a} suc (a+zero≡a a)
```

Weiteres Beispiel: Implizite Grundmenge bei `_≡_` oben.
In der stdlib ist der Parameter an refl implizit, da er sich meist aus
dem Kontext ergibt, wie z. B. in der Definition von `sym`:

```
sym : ∀ {X : Set} {a : X} {b} → a ≡ b → b ≡ a
sym (refl _) = refl _
--        ^         ^--- Agda leitet den Parameter aus dem Kontext ab
--        '----  Der Wert bekommt keinen Namen, steht aber trotzdem zur Verfügung:
--               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)

```

Gleichungsketten
----------------
```
_∎ : ∀ {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) ∎

```
Warnung: die Gleichungsketten in der stdlib beginnen mit `begin_`

Entscheidungsprozeduren
-----------------------

* Einbettung Bool ↪ Set
* Korrektheitsbeweis von `_≡?_`
* Dot-Pattern

```
-- 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 _)
```
[Ende der Vorlesung am 16. April 2026]

In `≡?-⇐` nutzen wir das Prinzip des "Fordings".

Rückrichtung:
```
≡?-⇒ : ∀ a b → Truth (a ≡? b) → a ≡ b
≡?-⇒ zero zero t = refl _
≡?-⇒ zero (suc b) ()   -- hier kein '=', () ≡ "unmögliches 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)

```

Funktionen
----------
```
_∘_ : ∀ {ℓ₁ ℓ₂ ℓ₃} {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
```
Das übliche Produkt ist ein 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 des Dependent-Products = 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 _
```

Funktionen
----------
Die Relation `f ≐ g` beschreibt, dass die Funktionen `f` und `g` Punktweise
identisch sind:
```
_≐_ : ∀ {ℓ₁ ℓ₂} {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
```