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
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 0 _∷_ : ∀ {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
Decidability
Quantifiers
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)