ITP Exercise Sheet 04

Discussion: 21 May 2026

{-# OPTIONS --allow-unsolved-metas #-}
open import Level using (Level)
open import Data.Nat
open import Data.Fin
open import Data.List
open import Data.Empty
open import Data.Vec hiding (length)
open import Data.Product
open import Data.Unit
open import Data.Sum
open import Data.Bool hiding (_≤_; _<_)
open import Function.Base using (_∘_; id; case_of_; _∋_)
import Level as L
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Negation

module _ where

private
  variable
    ℓ ℓ' ℓ'' : Level
    A : Set ℓ
    B : Set ℓ'
    C : Set ℓ''

Fin-access

Define index access into a list using Data.Fin:

_at[_] : (l : List A) → Fin (length l) → A
_at[_] = -- <LSG>
  h
  where
    h : (l : List A) → Fin (length l) → A
    h (x ∷ l) zero = x
    h (x ∷ l) (suc k) = h l k
  -- </LSG>

Fin vs Vec

We consider the two representations of lists of length k: via Vec and as maps Fin k → -. Define the translations:

module Fin-vs-Vec (X : Set ℓ) where
  fin-to-vec : ∀ {k} → (Fin k → X) → (Vec X k)
  fin-to-vec = -- <LSG>
    h
    where
    h : ∀ {k} → (Fin k → X) → (Vec X k)
    h {zero} f = []
    h {suc k} f = f zero ∷ h (f ∘ suc)
    -- </LSG>
  vec-to-fin : ∀ {k} → (Vec X k) → (Fin k → X)
  vec-to-fin = -- <LSG>
    h
    where
    h : ∀ {k} → (Vec X k) → (Fin k → X)
    h {zero} [] = λ ()
    h {suc k} (x ∷ v) zero = x
    h {suc k} (x ∷ v) (suc i) = h v i
    -- </LSG>

Prove that the two maps are inverse to each other:

  iso-on-fin : ∀ k (f : Fin k → X) → vec-to-fin (fin-to-vec f) ≗ f
  iso-on-fin = -- <LSG>
    iso-on-fin'
    where
    iso-on-fin' : ∀ k (f : Fin k → X) → vec-to-fin (fin-to-vec f) ≗ f
    iso-on-fin' zero f ()
    iso-on-fin' (suc k) f zero = refl
    iso-on-fin' (suc k) f (suc x) = iso-on-fin' k (f ∘ suc) x
    -- </LSG>

  iso-on-vec : ∀ {k} → fin-to-vec ∘ vec-to-fin {k} ≗ id
  iso-on-vec = -- <LSG>
    iso-on-vec'
    where
    iso-on-vec' : ∀ {k} → fin-to-vec ∘ vec-to-fin {k} ≗ id
    iso-on-vec' [] = refl
    iso-on-vec' (x ∷ v) = cong (x ∷_) (iso-on-vec' v)
    -- </LSG>

Logic

We consider the following laws of propositional logic:

LEM : ∀ (A : Set) → Set
LEM A = A ⊎ ¬ A

peirce : ∀ (A B : Set) → Set
peirce A B = ((A → B) → A) → A

¬¬-elim : ∀ (A : Set) → Set
¬¬-elim A = ¬ ¬ A → A

contraposition⁻¹ : ∀ (A B : Set) → Set
contraposition⁻¹ A B = (¬ B → ¬ A) → (A → B)

deMorgan : ∀ (A B : Set) → Set
deMorgan A B = ¬ (A × B) → (¬ A ⊎ ¬ B)

Show that they are equivalent to each other:

LEM⇒peirce : ∀ A B  → (∀ A → LEM A) → peirce A B
LEM⇒peirce A B LEM = -- <LSG>
  case (LEM A) of λ
  { (inj₁ a) → λ x → a
  ; (inj₂ ¬a) → λ x → x (⊥-elim ∘ ¬a)
  }
  -- </LSG>

peirce⇒¬¬-elim : ∀ A → (∀ B → peirce A B) → ¬¬-elim A
peirce⇒¬¬-elim A = -- <LSG>
  h
  where
    h : (∀ B → peirce A B) → ¬¬-elim A
    h p ¬¬A = p (¬ A) (λ f → ⊥-elim (¬¬A λ a → f a a))
  -- </LSG>

¬¬-elim⇒contraposition⁻¹ : (∀ A → ¬¬-elim A) → ∀ A B → contraposition⁻¹ A B
¬¬-elim⇒contraposition⁻¹ ¬¬A→A A B = -- <LSG>
  h
    where
    h : contraposition⁻¹ A B
    h f g = ¬¬A→A B (λ z → f z g)
  -- </LSG>

contraposition⁻¹⇒LEM : (∀ A B → contraposition⁻¹ A B) → (∀ A → LEM A)
contraposition⁻¹⇒LEM contra A = -- <LSG>
  contra ⊤ (LEM A) (λ ¬lem _ → (¬lem ∘ inj₂) (¬lem ∘ inj₁)) tt
  -- </LSG>
-- <LSG>
contraposition⁻¹⇒deMorgan : (∀ A B → contraposition⁻¹ A B) → (∀ A B → deMorgan A B)
contraposition⁻¹⇒deMorgan contr A B = contr (¬ (A × B)) (¬ A ⊎ ¬ B) helper
  where
    helper : ¬ (¬ A ⊎ ¬ B) → ¬ ¬ (A × B) 
    helper = λ ¬d ¬k → ¬d (inj₁ (λ a → ¬d (inj₂ λ b → ¬k (a , b))))

    open import Logic using (module ¬¬-do)
    open ¬¬-do
    helper' : ¬ (¬ A ⊎ ¬ B) → ¬ ¬ (A × B) 
    helper' ¬d = do
      a ← (¬ ¬ A) ∋ ¬d ∘ inj₁
      b ← (¬ ¬ B) ∋ ¬d ∘ inj₂
      return ((A × B) ∋ (a , b))

Agda Quellcode herunterladen