ITP Exercise Sheet 05
Discussion: 11 June 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
Show that finite sets are closed under disjoint unions. Use the auxiliary functions imported above.
⊎-finite : FiniteL A → FiniteL B → FiniteL (A ⊎ B) ⊎-finite A-fin B-fin = {! !}
Finiteness of products
Show that finite sets are closed under products. Use the auxiliary functions imported above.
×-finite : FiniteL A → FiniteL B → FiniteL (A × B) ×-finite A-fin B-fin = {! !}
Finiteness and quantifiers
Complete the following proof from the lecture:
module Finite-Quantifiers-Blatt {X : Set ℓ} (P : X → Set ℓ) (P? : Decidable P) where Finite⇒Dec∀∈ : ∀ (l : List X) → Dec ((_∈ l) ⊆ P) Finite⇒Dec∀∈ = {! !} -- 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) -- Note: when using map′ you have to define the two directions separately -- in a 'where' block so that Agda's type inference works properly. Finite⇒decidable : FiniteL X → Dec (∀ x → P x) Finite⇒decidable = {! !}
ℕ not finite
Show that ℕ is not finite:
Hint: use the functions on ⊔ imported above.
ℕ-not-finite : ¬ FiniteL ℕ ℕ-not-finite = {! !}