Skip to content

Instantly share code, notes, and snippets.

@TOTBWF
Last active June 10, 2021 14:36
Show Gist options
  • Save TOTBWF/6890425f52066fa3bbfdd3e629565a4e to your computer and use it in GitHub Desktop.
Save TOTBWF/6890425f52066fa3bbfdd3e629565a4e to your computer and use it in GitHub Desktop.
Agda proof of the Knaster-Tarski Fixpoint Theorem
-- A proof of the Knaster-Tarski Fixpoint Theorem
-- See https://en.wikipedia.org/wiki/Knaster%E2%80%93Tarski_theorem
module Fixpoint where
open import Level
open import Data.Product
open import Relation.Binary
open import Relation.Binary.Morphism
record IsCompleteLattice {a i ℓ₁ ℓ₂} {A : Set a}
(_≈_ : Rel A ℓ₁) -- The underlying equality
(_≤_ : Rel A ℓ₂) -- The partial order.
(⋀ : {I : Set i} → (I → A) → A)
(⋁ : {I : Set i} → (I → A) → A)
: Set (a ⊔ suc i ⊔ ℓ₁ ⊔ ℓ₂) where
field
sup : ∀ {I : Set i} {P : I → A} → (xi : I) → ⋀ P ≤ P xi
inf : ∀ {I : Set i} {P : I → A} → (xi : I) → P xi ≤ ⋁ P
supremum : ∀ {I : Set i} {P : I → A} → (x : A) → (∀ {xi} → x ≤ P xi) → x ≤ ⋀ P
infinum : ∀ {I : Set i} {P : I → A} → (x : A) → (∀ {xi} → P xi ≤ x) → ⋁ P ≤ x
record CompleteLattice c i ℓ₁ ℓ₂ : Set (suc (c ⊔ i ⊔ ℓ₁ ⊔ ℓ₂)) where
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁
_≤_ : Rel Carrier ℓ₂
⋀ : {I : Set i} → (I → Carrier) → Carrier
⋁ : {I : Set i} → (I → Carrier) → Carrier
isPartialOrder : IsPartialOrder _≈_ _≤_
isCompleteLattice : IsCompleteLattice _≈_ _≤_ ⋀ ⋁
open IsPartialOrder isPartialOrder public
open IsCompleteLattice isCompleteLattice public
record Fixpoint {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) (F : A → A) : Set (a ⊔ ℓ) where
field
point : A
isFixpoint : F point ≈ point
module _ {c ℓ₁ ℓ₂} (L : CompleteLattice c (c ⊔ ℓ₂) ℓ₁ ℓ₂) where
open CompleteLattice L
tarski-fixpoint : ∀ {F : Carrier → Carrier} → IsOrderMonomorphism _≈_ _≈_ _≤_ _≤_ F → Fixpoint _≈_ F
tarski-fixpoint {F = F} monotone = record
{ point = point
; isFixpoint =
let fix-≤ = supremum (F point) λ {(x , Fx≤x)} → trans (monotone.mono (sup (x , Fx≤x))) Fx≤x
fix-≥ = sup ((F point) , monotone.mono fix-≤)
in antisym fix-≤ fix-≥
}
where
module monotone = IsOrderMonomorphism monotone
point : Carrier
point = ⋀ {Σ[ x ∈ Carrier ] (F x ≤ x)} proj₁
least-fixpoint : ∀ {F : Carrier → Carrier} → (monotone : IsOrderMonomorphism _≈_ _≈_ _≤_ _≤_ F) → (x : Fixpoint _≈_ F) → Fixpoint.point (tarski-fixpoint monotone) ≤ Fixpoint.point x
least-fixpoint {F = F} monotone x = sup ((Fixpoint.point x) , reflexive (Fixpoint.isFixpoint x))
where
module monotone = IsOrderMonomorphism monotone
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment