Finiteness

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

open import Level using (Level; Lift)
import Level as L
open import Data.Nat
open import Data.Bool
open import Data.Unit
open import Data.List as List
open import Data.List.Properties as List
open import Data.List.Membership.Propositional
import Data.List.Membership.Propositional.Properties as List
open import Data.List.Relation.Unary.Any
open import Data.Empty
open import Data.Product as Σ
open import Data.Sum as ⊎
open import Function.Base using (_∘_; flip; case_of_)
open import Relation.Binary.PropositionalEquality
open import Relation.Unary using (_⊆_)
open import Function.Definitions using (Injective; Surjective)

module Finite where

private
  variable
    ℓ ℓ' ℓ'' : Level
    A : Set ℓ
    B : Set ℓ'
    C : Set ℓ''

Finite sets with a fixed number of elements

Fin (1 + k) = { 0 } ∪ { suc(i) | i ∈ Fin k }

module Fin-Redef where
  data Fin : ℕ → Set where
    zero : ∀ {k : ℕ} → Fin (suc k)
    suc : ∀ {k : ℕ} → (i : Fin k) → Fin (suc k)

  List' : Set → Set
  List' X = Σ[ n ∈ ℕ ] (Fin n) → X

Vector

module Vec-Redef where
  data Vec (X : Set) : ℕ → Set where
    [] : Vec X 
    _∷_ : ∀ {n : ℕ} → (x : X) → (tl : Vec X n) → Vec X (suc n)

  -- Blatt 04:
  -- Vec X n ≡ Fin n → X

Definitions of Finiteness

open import Data.Fin hiding (_+_)

record Finite (X : Set ℓ) : Set ℓ where
  field
    k : ℕ
    f : Fin k → X
    f-surj : ∀ x → ∃[ i ] f i ≡ x

record FiniteL (X : Set ℓ) : Set ℓ where
  field
    elems : List X
    all-contained : ∀ (x : X) → x ∈ elems

Ende der Vorlesung am 11.05.2026

module ⊆-redef where
  Pred : ∀ {ℓ'} → Set ℓ' → (ℓ : Level) → Set (ℓ' L.⊔ L.suc ℓ)
  Pred A ℓ = A → Set ℓ

  _⊆'_ : Pred A ℓ → Pred A ℓ' → Set _
  P ⊆' Q = ∀ {x} → P x → Q x

  import Relation.Unary using (_⊆_; _∈_; Pred)

-- Im(f) = { b ∈ B ∣ The set { a ∈ A ∣ f(a) = b } is non-empty }
Im[_] : (f : A → B) → (B → Set _)
Im[ f ] b = ∃[ a ] f a ≡ b

-- `_∈ l` is the predicate describing whether x is
--- mentioned in the list l
list⇒fin : ∀ {X : Set ℓ}
           → (l : List X)
           → Σ[ f ∈ (Fin (length l) → X) ] (_∈ l) ⊆ Im[ f ]
list⇒fin [] = (λ ()) , λ ()
list⇒fin {X = X} (x ∷ l) = f' , λ
  { {y} (here refl) → zero , refl
  ; {y} (there y∈l) →
    let j , f[j]≡y = proj₂ IH y∈l in
    suc j , f[j]≡y
  }
  where
    IH : Σ[ f ∈ (Fin (length l) → X) ] (_∈ l) ⊆ Im[ f ]
    IH = list⇒fin l
    f = proj₁ IH

    f' : Fin (length (x ∷ l)) → X
    f' i = case i of λ -- demonstration of case_of_
           { zero → x
           ; (suc i-1) → proj₁ IH i-1
           }

FiniteL⇒Finite : ∀ {X : Set ℓ}
           → FiniteL X → Finite X
FiniteL⇒Finite {X = X} finitelist =
  record
  { k = length elems
  ; f = proj₁ prop
  ; f-surj = λ x → proj₂ prop (all-contained x)
  }
  where
    open FiniteL finitelist
    prop : Σ[ f ∈ (Fin (length elems) → X) ] (_∈ elems) ⊆ Im[ f ]
    prop = list⇒fin elems

Ende der Vorlesung am 18.05.2026

-- (Fin k → X)       →      List X
-- [ 0 ↦ x₀        ]
-- [ 1 ↦ x₁        ]
-- [   ⋮           ] ↦ x₀ ∷ x₁ ∷ ...  ∷ x_{k-1} ∷ []
-- [ k-1 ⋮ x_{k-1} ]
fin⇒list : ∀ {X : Set ℓ} 
           → (k : ℕ)
           → (f : Fin k → X)
           → Σ[ l ∈ List X ]  Im[ f ] ⊆ (_∈ l)
fin⇒list zero f = [] , λ { () }
fin⇒list (suc k) f =
  let l , Im[g]⊆l = IH in
  f zero ∷ l  , λ {x} → λ
    { (zero , f[0]≡x) → here (sym f[0]≡x)
    ; (suc i , f[1+i]≡x) → there (Im[g]⊆l (i , f[1+i]≡x))
    }
  where
    x₀ : _
    x₀ = f zero
    g = f ∘ suc
    IH = fin⇒list k g 


Finite⇒FiniteL : ∀ {X : Set ℓ}
           → Finite X → FiniteL X
Finite⇒FiniteL {X = X} k↠X =
  let
    l , Im[f]⊆l = fin⇒list k f
  in
  record
  { elems = l
  ; all-contained = λ x →
    let i , f[i]=x = f-surj x in
    Im[f]⊆l (i , f[i]=x)
  }
  where
    open Finite k↠X
    -- k : ℕ
    -- k = Finite.k k↠X
    -- f : Fin k → X
    -- f = Finite.f k↠X

Decidability

open import Relation.Nullary using (Dec; yes; no; ¬_; map′)
open import Relation.Unary using (Decidable)

Finite⇒Dec : ∀ {X : Set ℓ} → Finite X → Dec X
Finite⇒Dec record { k = zero ; f = f ; f-surj = f-surj } =
  no (λ x → case (f-surj x) of λ ())
Finite⇒Dec record { k = (suc k) ; f = f ; f-surj = f-surj } =
  yes (f zero)

Ende der Vorlesung am 21.05.2026

Quantifiers

module Finite-Quantifiers {X : Set ℓ} (P : X → Set ℓ) (P? : Decidable P) where
  -- => Blatt 05
  -- Finite⇒Dec∀∈ : ∀ (l : List X) → Dec ((_∈ l) ⊆ P)
  -- Finite⇒Dec∀∈ [] = yes (λ ())
  -- Finite⇒Dec∀∈ (x ∷ l) with (P? x)
  -- ... | no ¬Px = no (λ x∷l⊆P → ¬Px (x∷l⊆P (here refl)))
  -- ... | yes Px = map′ {!!} {!!} (Finite⇒Dec∀∈ l)

  -- Finite⇒decidable : FiniteL X → Dec (∀ x → P x)
  -- Finite⇒decidable = {!!}

Alternative (and more) complicated solutions

Idea: strengthen the induction hypothesis by generalizing from "all elements of A" to "all elements satisfying a predicate P ⊆ A".

Stdlib

import Data.Fin using (Fin)
import Data.Vec using (Vec)

Agda Quellcode herunterladen