ITP Exercise Sheet 03

Discussion: 7 May 2026

{-# OPTIONS --allow-unsolved-metas #-}
open import Level using (Level)
open import Data.Nat
open import Data.List
open import Data.Product
open import Data.Bool hiding (_≤_; _<_)
open import Relation.Nullary.Decidable using (Dec; map′; yes; no)
open import Function.Base using (_∘_; id)
import Level as L
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Negation
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Unary.Any using (Any; here; there)


module _ where

private
  variable
    a b c : Level
    A : Set a
    B : Set b
    C : Set c

n-ary Operation

Define a type of n-ary operations on a type X:

_-ary-on_ : ℕ → {ℓ : Level} → (X : Set ℓ) → Set ℓ
_-ary-on_ = -- <LSG>
  _-ary-on'_
  where
   _-ary-on'_ : ℕ → {ℓ : Level} → (X : Set ℓ) → Set ℓ
   _-ary-on'_ zero X = X
   _-ary-on'_ (suc k) X = X → k -ary-on' X
  -- </LSG>

-- <COMMENT>
_ :  -ary-on ℕ
_ = _+_ -- addition is binary on ℕ
_ :  -ary-on ℕ
_ = (λ x → x) -- identity is unary on ℕ
_ :  -ary-on Set
_ = ¬_ -- negation is a unary operation on sets 
_ :  -ary-on Bool
_ = true
-- </COMMENT>

Injectivity

-- <LSG>
open import Data.Unit
open import Data.Empty
-- </LSG>
module injectivity where

  _injective : (f : A → B) → Set _
  _injective f = -- <LSG>
    ∀ x x' → f x ≡ f x' → x ≡ x'
    -- </LSG>

  ∘-injective : {f : A → B} {g : B → C} → f injective → g injective → (g ∘ f) injective
  ∘-injective {f = f} = -- <LSG>
    λ f-inj g-inj x x' → f-inj x x' ∘ g-inj (f x) (f x')
    -- </LSG>

  ∘-cancelˡ-injective : {f : A → B} {g : B → C} → (g ∘ f) injective → f injective
  ∘-cancelˡ-injective {g = g} = -- <LSG>
    λ g∘f-inj x x' → g∘f-inj x x' ∘ cong g
    -- </LSG>
  no-∘-cancelʳ-injective : Σ[ A ∈ Set ] Σ[ B ∈ Set ] Σ[ C ∈ Set ]
                           Σ[ f ∈ (A → B) ] Σ[ g ∈ (B → C) ]
                           ((g ∘ f) injective × ¬ g injective)
  no-∘-cancelʳ-injective = _ , _ , _ , -- <LSG>
    f , g , (λ x x' x₁ → refl) , λ g-inj → h (g-inj true false refl)
    where
      f : ⊥ → Bool
      f ()
      g : Bool → ⊤
      g _ = tt
      h : true ≡ false → ⊥
      h ()
    -- </LSG>

Surjectivity

Define and prove the corresponding properties for surjectivity

module surjectivity where
  -- <LSG>
  _surjective : (f : A → B) → Set _
  _surjective f = ∀ y → ∃[ x ] y ≡ f x

  ∘-surjective : {f : A → B} {g : B → C} → f surjective → g surjective → (g ∘ f) surjective
  ∘-surjective {g = g} f-surj g-surj z =
    let y , z≡g[y] = g-surj z in
    let x , y≡f[x] = f-surj y in
    x , subst (λ - → z ≡ g -) y≡f[x] z≡g[y]
  -- </LSG>

  ∘-cancelʳ-surjective : {f : A → B} {g : B → C} → (g ∘ f) surjective → g surjective
  ∘-cancelʳ-surjective {f = f} g∘f-surj =
    Data.Product.map f id ∘ g∘f-surj
    -- ^- short version of:
    -- let x , z≡g[f[x]] = g∘f-surj z in
    -- f x , z≡g[f[x]]

  open import Function.Base using (case_of_)
  no-∘-cancelˡ-surjective : Σ[ A ∈ Set ] Σ[ B ∈ Set ] Σ[ C ∈ Set ]
                            Σ[ f ∈ (A → B) ] Σ[ g ∈ (B → C) ]
                            ((g ∘ f) surjective × ¬ f surjective)
  no-∘-cancelˡ-surjective = _ , _ , _ , f , g
    , (λ y → tt , refl)
    , λ f-surj → case (f-surj true) of λ ()
    where
      f : ⊤ → Bool
      f tt = false
      g : Bool → ⊤
      g _ = tt

Index-based access

Define a (total) function that returns the k-th element of a list.

_at[_] : (l : List A) → (k : ℕ) → k < length l → A
_at[_] = -- <LSG>
  _at[_]'
  where
  _at[_]' : (l : List A) → (k : ℕ) → k < length l → A
  ((x ∷ l) at[ zero ]') k<l = x
  ((x ∷ l) at[ suc k ]') (s≤s k<l) = (l at[ k ]') k<l
  -- </LSG>

Deciding membership

Decide whether a given element occurs in a list. (Hint: when case-splitting on something of type Dec x, it is advisable to enter the cases yes and no manually.)

module decide-∈ (A : Set a) (_≟_ : ∀ (x y : A) → Dec (x ≡ y)) where
    _∈?_ : (x : A) (l : List A) → Dec (x ∈ l)
    _∈?_ = -- <LSG>
      helper
      where
      helper : (x : A) (l : List A) → Dec (x ∈ l)
      helper x [] = no (λ ())
      helper x (y ∷ l) with (x ≟ y)
      ... | (yes refl) = yes (here refl)
      ... | (no x≢y) = map′ there
                (λ { (here x≡y) → ⊥-elim (x≢y x≡y)
                   ; (there x∈l) → x∈l}
                   ) (helper x l)
      -- </LSG>

Agda Quellcode herunterladen