ITP Blatt 05
Besprechung: am 11.06.2026
{-# OPTIONS --allow-unsolved-metas #-} open import Level as L using (Level) open import Data.Product open import Data.Sum open import Data.Nat open import Data.Nat.Properties using (m≤m⊔n; m≤n⊔m; ≤-trans) open import Data.List open import Data.List as List using (List; _++_; cartesianProduct) open import Data.List.Relation.Unary.Any open import Data.List.Membership.Propositional open import Data.List.Membership.Propositional.Properties using (∈-++⁺ˡ; ∈-++⁺ʳ; ∈-map⁺; ∈-cartesianProduct⁺) open import Relation.Nullary using (¬_; Dec; yes; no; map′) open import Relation.Binary.PropositionalEquality open import Relation.Binary.Definitions hiding (Decidable) open import Relation.Unary using (_⊆_; Decidable) module _ where private variable ℓ ℓ' ℓ'' : Level A : Set ℓ B : Set ℓ' C : Set ℓ'' open import Finite
Finiteness of sums
Zeigen Sie, dass endliche Mengen unter Disjunktion Vereinigungen abgeschlossen sind. Nutzen Sie die oben importierten Hilfsfunktionen.
⊎-finite : FiniteL A → FiniteL B → FiniteL (A ⊎ B) ⊎-finite A-fin B-fin = -- <LSG> record { elems = List.map inj₁ A.elems ++ List.map inj₂ B.elems ; all-contained = λ { (inj₁ a) → ∈-++⁺ˡ (∈-map⁺ inj₁ (A.all-contained a)) ; (inj₂ b) → ∈-++⁺ʳ _ (∈-map⁺ inj₂ (B.all-contained b)) } } where module A = FiniteL A-fin module B = FiniteL B-fin -- </LSG>
Finiteness of products
Zeigen Sie, dass endliche Mengen unter Produkten abgeschlossen sind. Nutzen Sie die oben importierten Hilfsfunktionen.
×-finite : FiniteL A → FiniteL B → FiniteL (A × B) ×-finite A-fin B-fin = -- <LSG> record { elems = cartesianProduct A.elems B.elems ; all-contained = λ (a , b) → ∈-cartesianProduct⁺ (A.all-contained a) (B.all-contained b) } where module A = FiniteL A-fin module B = FiniteL B-fin -- </LSG>
Finiteness and quantifiers
Vervollständigen Sie folgenden Beweis aus der Vorlesung:
module Finite-Quantifiers-Blatt {X : Set ℓ} (P : X → Set ℓ) (P? : Decidable P) where -- <LSG> 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′ extend restrict (Finite⇒Dec∀∈' l) where extend : (_∈ l) ⊆ P → (_∈ (x ∷ l)) ⊆ P extend l⊆P (here refl) = Px extend l⊆P (there y∈l) = l⊆P y∈l restrict : (_∈ (x ∷ l)) ⊆ P → (_∈ l) ⊆ P restrict x∷l⊆P y∈l = x∷l⊆P (there y∈l) -- </LSG> Finite⇒Dec∀∈ : ∀ (l : List X) → Dec ((_∈ l) ⊆ P) Finite⇒Dec∀∈ = -- <LSG> Finite⇒Dec∀∈' -- </LSG> -- 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) -- Hinweis: beim verwenden von map′ müssen Sie die beiden Richtungen -- extra in 'where' definieren, damit Agda's Typinferenz richtig funktioniert. -- <LSG> Finite⇒decidable' : FiniteL X → Dec (∀ x → P x) Finite⇒decidable' record { elems = elems ; all-contained = all-contained } = map′ forward backward (Finite⇒Dec∀∈ elems) where forward : (_∈ elems) ⊆ P → (∀ x → P x) forward elems⊆P x = elems⊆P (all-contained x) backward : (∀ x → P x) → (_∈ elems) ⊆ P backward ∀P {y} _ = ∀P y -- </LSG> Finite⇒decidable : FiniteL X → Dec (∀ x → P x) Finite⇒decidable = -- <LSG> Finite⇒decidable' -- </LSG>
ℕ not finite
Zeigen Sie, dass ℕ nicht endlich ist:
Tipp: Nutzen Sie oben importierte funktionen zu ⊔.
-- <LSG> max : List ℕ → ℕ max [] = 0 max (x ∷ xs) = x ⊔ (max xs) max-≤ : ∀ xs {y} → y ∈ xs → y ≤ max xs max-≤ [] () max-≤ (x ∷ xs) (here refl) = m≤m⊔n x _ max-≤ (x ∷ xs) (there y∈xs) = ≤-trans (max-≤ xs y∈xs) (m≤n⊔m x (max xs)) not-≤ : ∀ k → ¬ (1 + k ≤ k) not-≤ zero () not-≤ (suc k) (s≤s le) = not-≤ k le -- </LSG> ℕ-not-finite : ¬ FiniteL ℕ ℕ-not-finite = -- <LSG> λ { record { elems = elems ; all-contained = all-contained } → not-≤ (max elems) (max-≤ elems (all-contained (1 + max elems))) } -- </LSG>