Skip to content

Instantly share code, notes, and snippets.

@msakai
Last active Feb 12, 2021
Embed
What would you like to do?
{-
https://twitter.com/andrejbauer/status/1358357606536986624
Today's exercise in constructive math: characterize the maximal
elements of Plotkin's domain T^ω := {(A,B) ∈ P(ℕ) × P(ℕ) | A ∩ B = ∅},
ordered by pairwise ⊆. Coq definitions are in the picture.
Hint: they are *not* just those that satisfy A ∪ B = ℕ.
-}
module Tomega where
open import Data.Empty
open import Data.Nat hiding (_≤_)
open import Data.Product
open import Function
open import Relation.Binary
open import Relation.Nullary using (¬_)
open import Relation.Unary
open import Level
record T^ω : Set₁ where
field
yes : Pred ℕ 0ℓ
no : Pred ℕ 0ℓ
disjoint : n ¬ (yes n × no n)
open T^ω
_≤_ : Rel T^ω 0ℓ
x ≤ y = (yes x ⊆ yes y) × (no x ⊆ no y)
maximal : Pred T^ω (Level.suc 0ℓ)
maximal x = y (x ≤ y) (y ≤ x)
maximal′ : Pred T^ω 0ℓ
maximal′ x = ( {n} ¬ yes x n no x n) × ( {n} ¬ no x n yes x n)
maximal→maximal′ : x maximal x maximal′ x
maximal→maximal′ x x-is-maximal = (¬yes→no , ¬no→yes)
where
¬yes→no : {n} ¬ yes x n no x n
¬yes→no = proj₂ y≤x
where
y : T^ω
y = record
{ yes = yes x
; no = λ n ¬ (yes x n)
; disjoint = λ n ( yes-x-n , ¬yes-x-n ) ¬yes-x-n yes-x-n
}
x≤y : x ≤ y
x≤y = (id , (λ {n} no-x-n yes-x-n disjoint x n (yes-x-n , no-x-n)))
y≤x : y ≤ x
y≤x = x-is-maximal y x≤y
¬no→yes : {n} ¬ no x n yes x n
¬no→yes = proj₁ y≤x
where
y : T^ω
y = record
{ yes = λ n ¬ (no x n)
; no = no x
; disjoint = λ n ( ¬no-x-n , no-x-n ) ¬no-x-n no-x-n
}
x≤y : x ≤ y
x≤y = ((λ {n} yes-x-n no-x-n disjoint x n (yes-x-n , no-x-n)) , id)
y≤x : y ≤ x
y≤x = x-is-maximal y x≤y
maximal′→maximal : x maximal′ x maximal x
maximal′→maximal x x-is-maximal′ y x≤y = (yes-y⊆yes-x , no-y⊆no-x)
where
yes-y⊆yes-x : yes y ⊆ yes x
yes-y⊆yes-x {n} yes-y-n = proj₂ x-is-maximal′ (λ no-x-n disjoint y n (yes-y-n , proj₂ x≤y no-x-n))
no-y⊆no-x : no y ⊆ no x
no-y⊆no-x {n} no-y-n = proj₁ x-is-maximal′ (λ yes-x-n disjoint y n (proj₁ x≤y yes-x-n , no-y-n))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment