Listen

{-# OPTIONS --allow-unsolved-metas #-}
open import Level using (Level)
import Relation.Binary.PropositionalEquality as ≡
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Function.Base using (_∘_)
open import Data.Product hiding (map)
open import Function.Bundles using (_⇔_; mk⇔)

module Lists where

Der Parameter an das folgende Modul bewirkt, dass im folgenden List in abhängigkeit von X definiert ist.

module List-Definition {ℓ : Level} (X : Set ℓ) where
  data List : Set ℓ where
    [] : List                    -- nil
    _∷_ : X → List → List        -- cons

  [_] : X → List
  [ x ] = x ∷ []

module _ {ℓ : Level} {X : Set ℓ} where
  open List-Definition X
  _++_ : List → List → List
  _++_ [] ys = ys
  _++_ (x ∷ xs) ys = x ∷ (_++_ xs ys)

  ++-assoc : ∀ x y z → (x ++ y) ++ z ≡ x ++ (y ++ z)
  ++-assoc [] y z = ≡.refl
  ++-assoc (x-h ∷ x-t) y z = ≡.cong (x-h ∷_) (++-assoc x-t y z)

  x++[]≡x : ∀ {x} → x ++ [] ≡ x
  x++[]≡x {[]} = ≡.refl
  x++[]≡x {x ∷ xs} rewrite (x++[]≡x {xs}) = ≡.refl
  -- x++[]≡x {x ∷ xs} = ≡.cong (x ∷_) x++[]≡x
  -- x++[]≡x {x ∷ xs} = ≡.cong (x ∷_) (x++[]≡x {xs})

  ∷-injectiveʳ : ∀ {x} {y₁ y₂} → x ∷ y₁ ≡ x ∷ y₂ → y₁ ≡ y₂
  ∷-injectiveʳ ≡.refl = ≡.refl

  ++-injectiveʳ : ∀ x {y₁} {y₂} → x ++ y₁ ≡ x ++ y₂ → y₁ ≡ y₂
  ++-injectiveʳ [] eq = eq
  ++-injectiveʳ (x ∷ xs) eq =
    ++-injectiveʳ xs (∷-injectiveʳ eq)

  _∷ʳ_ : List → X → List
  xs ∷ʳ x = xs ++ [ x ]

  -- hier im Modul lässt sich `map` nicht definieren,
  -- da Listen stets über `X` sind


module Map-Definition {ℓ ℓ'} {X : Set ℓ} {Y : Set ℓ'} where
  open List-Definition
  map : (f : X → Y) → List X → List Y
  map f [] = []
  map f (x ∷ xs) = f x ∷ map f xs

  map-++ : (f : X → Y) → ∀ (xs₁ xs₂ : List X)
           → map f (xs₁ ++ xs₂) ≡ (map f xs₁ ++ map f xs₂)
  map-++ f [] zs = ≡.refl
  map-++ f (x ∷ xs) zs = ≡.cong ((f x) ∷_) (map-++ f xs zs)

Ende der Vorlesung am 20. April 2026

Reverse

Welche Eigenschaften sollte reverse erfüllen?

• rev ∘ rev ≐ id
• rev [] ≡ []
• rev (xs ++ ys) ≡ rev ys ++ rev xs

Welche Eigenschaft definiert reverse auf eindeutige Weise?

module Reverse {ℓ : Level} (X : Set ℓ) where
  open List-Definition {ℓ} X

  rev' : List → List
  rev' [] = []
  rev' (x ∷ xs) = rev' xs ∷ʳ x

  rev-acc : List → List → List
  rev-acc [] acc = acc
  rev-acc (x ∷ xs) acc = rev-acc xs (x ∷ acc)

  rev : List → List
  rev x = rev-acc x []

  rev[] : rev [] ≡ []
  rev[] = ≡.refl

  -- rev preserves ++ in the first argument:
  rev-acc-++₁ : ∀ xs ys zs → rev-acc (xs ++ ys) zs ≡ rev-acc ys (rev-acc xs zs)
  rev-acc-++₁ [] ys zs = ≡.refl
  rev-acc-++₁ (x ∷ xs) ys zs = rev-acc-++₁ xs ys (x ∷ zs)

  -- rev preserves ++ in the second argument:
  rev-acc-++₂ : ∀ xs ys zs → rev-acc xs ys ++ zs ≡ rev-acc xs (ys ++ zs)
  rev-acc-++₂ [] ys zs = ≡.refl
  rev-acc-++₂ (x ∷ xs) ys zs = rev-acc-++₂ xs (x ∷ ys) zs
    where
      open ≡.≡-Reasoning
      longer-solution = 
        begin
        (rev-acc (x ∷ xs) ys ++ zs) ≡⟨⟩
        rev-acc xs (x ∷ ys) ++ zs ≡⟨ rev-acc-++₂ xs (x ∷ ys) zs ⟩
        rev-acc xs (x ∷ (ys ++ zs)) ≡⟨⟩
        rev-acc (x ∷ xs) (ys ++ zs)
        ∎

  rev-++ : ∀ xs ys → rev (xs ++ ys) ≡ rev ys ++ rev xs
  rev-++ xs ys =
    begin
    rev (xs ++ ys) ≡⟨⟩
    rev-acc (xs ++ ys) [] ≡⟨ rev-acc-++₁ xs ys [] ⟩
    rev-acc ys (rev-acc xs []) ≡⟨⟩
    rev-acc ys (rev xs) ≡⟨⟩
    rev-acc ys ([] ++ rev xs) ≡⟨ rev-acc-++₂ ys [] (rev xs)  ⟨
    -- ... ⟨ <- Klammer andersherum = sym
    (rev-acc ys []) ++ (rev xs) ≡⟨⟩
    (rev ys ++ rev xs)
    ∎
    where
      open ≡.≡-Reasoning

Ende der Vorlesung am 23. April 2026

  open import Relation.Binary.PropositionalEquality using (_≗_)
  ++-antitone : (List → List) → Set ℓ
  ++-antitone f = ∀ x y → f (x ++ y) ≡ f y ++ f x

  _preveres-[-] : (List → List) → Set ℓ
  _preveres-[-] f = ∀ x → f [ x ] ≡ [ x ]

  only-rev++ : ∀ f → f preveres-[-] → ++-antitone f → f ≗ rev
  only-rev++ f _ f-++ [] = ++-injectiveʳ (f []) (begin
    (f [] ++ f []) ≡⟨ f-++ [] [] ⟨
    f ([] ++ []) ≡⟨⟩
    f [] ≡⟨ x++[]≡x ⟨ -- <- Notation für sym
    (f [] ++ [])
    ∎)
    where open ≡.≡-Reasoning
  only-rev++ f f-[-] f-++ (x ∷ xs) =
    begin
    f (x ∷ xs) ≡⟨ f-++ _ _ ⟩
    f xs ++ f [ x ]  ≡⟨ ≡.cong₂ _++_ IH (f-[-] x) ⟩
    rev xs ++ rev [ x ]  ≡⟨ rev-++ [ x ] xs ⟨
    rev (x ∷ xs)
    ∎
    where
      open ≡.≡-Reasoning
      IH = (only-rev++ f f-[-] f-++ xs)

  record _UniquelyDefinedBy_ (r : List → List)
                           (P : (List → List) → Set ℓ)
                           : Set ℓ where
    field
      r-P : P r
      only-r : ∀ f → P f → f ≗ r

  record Spec (r : List → List) : Set ℓ where
    field
      prop-1 : r preveres-[-]
      prop-2 : ++-antitone r

  rev-unique-spec : rev UniquelyDefinedBy Spec
  rev-unique-spec = record
    { r-P = record { prop-1 = λ x → ≡.refl ; prop-2 = rev-++ }
    ; only-r = λ f f-Spec → only-rev++ f
             (Spec.prop-1 f-Spec)
             (f-Spec .Spec.prop-2) -- flipped function application
    }

Dependently-Typed Recursive Data-Types

Datentypen	Beispiele	Beispiele mit Dependent Types
Funktionen	A → B	∀ (x : A) → B x
Records	_×_	Σ
Rec. DT	List	_∈_ , _≤_

Die Element-Beziehung _∈_ definieren wir wie folgt:

module List-Membership {ℓ} (X : Set ℓ) where
  private
    variable ℓ' : Level

  open import Level using (_⊔_)
  open List-Definition {ℓ} X

  data Any (P : X → Set ℓ') : List → Set (ℓ ⊔ ℓ') where
    here : ∀ {x} {xs} → P x → Any P (x ∷ xs)
    there : ∀ {x} {xs} → Any P xs → Any P (x ∷ xs)

  _∈_ : (x : X) → List → Set ℓ
  x ∈ list = Any (x ≡_) list

  open Reverse {ℓ} X

  rev-P-acc : ∀ {P : X → Set ℓ} xs acc → Any P acc → Any P (rev-acc xs acc)
  rev-P-acc [] acc P-acc = P-acc
  rev-P-acc (x ∷ xs) acc P-acc = rev-P-acc xs (x ∷ acc) (there P-acc)

  rev-P : ∀ {P : X → Set ℓ} xs acc → Any P xs → Any P (rev-acc xs acc)
  rev-P [] _ () -- <- absurd pattern; no constructor of 'Any' possible
  rev-P (x ∷ xs) acc (here P-x) = rev-P-acc xs (x ∷ acc) (here P-x)
  rev-P (x ∷ xs) acc (there any-P-xs) = rev-P xs (x ∷ acc) any-P-xs

  rev-∈ : ∀ x xs → (x ∈ xs) → x ∈ rev xs
  rev-∈ x xs = rev-P {x ≡_} xs []

Weiteres Beispiel einer rekursiven Datenstruktur mittels Dependent Types:

module ℕ-≤ where

  open import Data.Nat.Base using (ℕ; zero; suc)
  data _≤₁_ : ℕ → ℕ → Set where
    z≤n : ∀ n → zero ≤₁ n
    s≤s : ∀ n m → n ≤₁ m → suc n ≤₁ suc m
    -- intuition: left-aligned length comparison:
    --      s s s z
    --      _≤₁_  
    --      s s s s s s s s z
    --            '-- z≤n --'

  data _≤₂_ : ℕ → ℕ → Set where
    n≤n : ∀ n → n ≤₂ n
    ≤-s : ∀ n m → n ≤₂ m → n ≤₂ suc m
    -- intuition: right-aligned length comparison
    --            s s s s z
    --          _≤₂_
    --      s s s s s s s z
    --            '- n≤n -'

Ende der Vorlesung am 27.04.2026

Definitionen in der Agda standard library

import Data.List using (List; []; _∷_; _++_; reverse)
import Data.List.Properties using (reverse-++; ++-identityʳ)
import Data.List.Membership.Propositional using (_∈_)
import Data.List.Relation.Unary.Any using (Any; here; there)
import Data.Nat using (_≤_; _≤′_)

Agda Quellcode herunterladen