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