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[_] = {! !}

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 = {! !}
  vec-to-fin : ∀ {k} → (Vec X k) → (Fin k → X)
  vec-to-fin = {! !}

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 = {! !}

  iso-on-vec : ∀ {k} → fin-to-vec ∘ vec-to-fin {k} ≗ id
  iso-on-vec = {! !}

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 = {! !}

peirce⇒¬¬-elim : ∀ A → (∀ B → peirce A B) → ¬¬-elim A
peirce⇒¬¬-elim A = {! !}

¬¬-elim⇒contraposition⁻¹ : (∀ A → ¬¬-elim A) → ∀ A B → contraposition⁻¹ A B
¬¬-elim⇒contraposition⁻¹ ¬¬A→A A B = {! !}

contraposition⁻¹⇒LEM : (∀ A B → contraposition⁻¹ A B) → (∀ A → LEM A)
contraposition⁻¹⇒LEM contra A = {! !}

Agda Quellcode herunterladen