ITP Blatt 04

Besprechung: am 21.05.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

Definieren Sie Index-Zugriff auf eine Liste mittels 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

Wir betrachten die zwei Darstellungen von Listen der Länge k, mittels Vec sowie als Abbildungen Fin k → -. Definieren Sie die Übersetzungen:

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>

Beweisen Sie, dass die beiden Abbildungen invers zueinander sind:

  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

Wir betrachten die folgenden aussagenlogischen Gesetze:

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)

Zeigen sie, dass diese äquivalent zueinander sind:

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