Exercise Sheet 08

Discussion: 16 July 2026.

{-# OPTIONS --allow-unsolved-metas --guardedness #-}

open import Level using (0ℓ)
open import Axiom.ExcludedMiddle using (ExcludedMiddle)
open import Data.Unit using (tt)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product
open import Data.Sum using (inj₁; inj₂)
open import Data.Maybe using (Maybe; just; nothing; Is-just; to-witness; _<∣>_)
open import Data.Maybe.Relation.Unary.Any using (just)
open import Relation.Binary using (_⇔_)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (yes; no; contradiction; ¬_)
open import Function.Base

module _ where

open import Partial

private
  variable
    A B X Y : Set

From spans to Maybe

We have already shown:

import Partial using (from-Maybe)

Prove the converse direction under the assumption of the law of excluded middle:

module Span→Maybe (lem : ExcludedMiddle 0ℓ) where
  ⊇⟶⇒⇀ : (A ⊇⟶ B) → (A ⇀ B)
  ⊇⟶⇒⇀ f a = -- <LSG>
    solution
    where
    open _⊇⟶_ f
    solution : Maybe _
    solution with lem {Is-defined a}
    ... | yes a↓ = just (app (a , a↓))
    ... | no _ = nothing
    -- </LSG>

  module properties (f : A ⊇⟶ B) where
    open import Relation.Unary using (_⊆_)
    open _⊇⟶_ f
    g : A ⇀ B
    g = ⊇⟶⇒⇀ f

    dom-⊆ : Is-defined ⊆ (Is-just ∘ g)
    dom-⊆ {a} x∈dom[f] with lem {Is-defined a}
    ... | yes a↓ = just tt
    ... | no a↑ = contradiction x∈dom[f] a↑

    dom-⊇ : (Is-just ∘ g) ⊆ Is-defined
    dom-⊇ {a} g[a]-is-just with lem {Is-defined a}
    dom-⊇ {a} g[a]-is-just | yes x∈dom[f] = x∈dom[f]
    dom-⊇ {a} () | no _

    same-value : ∀ a → (a↓ : Is-defined a)
               → g a ≡ just (app (a , a↓))
    same-value a a↓ with lem {Is-defined a}
    ... | yes a↓′ = cong just (well-defined refl)
    ... | no a↑ = contradiction a↓ a↑

Step indexing is wlog

Given an arbitrary map f, turn it into a monotone one:

module Stabilize {A : Set} (f : ℕ → Maybe A) where
  stabilized : ℕ → Maybe A
  stabilized = -- <LSG>
    solution
    where
    solution : ℕ → Maybe A
    solution zero = f zero
    solution (suc n) = solution n <∣> f (suc n)
    -- </LSG>

  stabilized-is-mono : is-mono stabilized
  stabilized-is-mono = -- <LSG>
    solution
    where
    solution : is-mono stabilized
    solution n s[n]↓ with stabilized n | s[n]↓
    ... | just _ | _ = refl
    -- </LSG>

  stabilized-complete : ∀ n → Is-just (f n) → Is-just (stabilized n)
  stabilized-complete = -- <LSG>
    solution
    where
    <∣>-just-right : ∀ {x y : Maybe A} → Is-just y → Is-just (x <∣> y)
    <∣>-just-right {x = just _} _ = just tt
    <∣>-just-right {x = nothing} y↓ = y↓

    solution : ∀ n → Is-just (f n) → Is-just (stabilized n)
    solution zero f[0]↓ = f[0]↓
    solution (suc n) f[1+n]↓ = <∣>-just-right f[1+n]↓
    -- </LSG>

  stabilized-sound : ∀ n → Is-just (stabilized n) → ∃[ k ] f k ≡ stabilized n
  stabilized-sound = -- <LSG>
    solution
    where
    solution : ∀ n → Is-just (stabilized n) → ∃[ k ] f k ≡ stabilized n
    solution zero _ = zero , refl
    solution (suc n) _ with stabilized n in s[n]≡
    ... | just _ =
      let k , f[k]≡s[n] = solution n (subst Is-just (sym s[n]≡) (just tt)) in
      k , trans f[k]≡s[n] s[n]≡
    ... | nothing = suc n , refl
    -- </LSG>

Agda Quellcode herunterladen