module Contractive where
open import Relation.Unary
open import Relation.Binary
import Relation.Binary.EqReasoning as EqR
import Induction.WellFounded as WF
open import Data.Function
record IsWellFoundedOrder {A} (_<_ : Rel A) : Set where
field
trans : Transitive _<_
isWellFounded : ∀ a → WF.Acc _<_ a
record OFE : Set1 where
field
carrier : Set
domain : Set
_<_ : Rel carrier
isWellFoundedOrder : IsWellFoundedOrder _<_
Eq : carrier → Rel domain
isEquivalence : ∀ a → IsEquivalence (Eq a)
open IsWellFoundedOrder isWellFoundedOrder public
open WF _<_ public using (WfRec)
open WF.All _<_ isWellFounded public
setoid : carrier → Setoid
setoid a = record { carrier = domain
; _≈_ = Eq a
; isEquivalence = isEquivalence a
}
module EqReasoning {a : carrier} where
open EqR (setoid a) public
open Setoid (setoid a) public using (refl; sym)
↓ : carrier → Pred carrier
↓ a = λ a' → a' < a
_≅_ : Rel domain
x ≅ y = ∀ a → Eq a x y
Family : Pred carrier → Set
Family I = ∀ x → x ∈ I → domain
lift : ∀ {I} → (carrier → domain) → Family I
lift P = λ x _ → P x
IsCoherent : ∀ {I} → Family I → Set
IsCoherent {I} fam = ∀ {a' a}
(a'∈I : a' ∈ I) (a∈I : a ∈ I) → a' < a →
Eq a' (fam a' a'∈I) (fam a a∈I)
IsLimit : ∀ {I} → Family I → domain → Set
IsLimit {I} fam y = ∀ {a'}
(a'∈I : a' ∈ I) → Eq a' (fam a' a'∈I) y
IsContractive : (domain → domain) → Set
IsContractive F = ∀ {x y a} →
(∀ {a'} → a' < a → Eq a' x y) → Eq a (F x) (F y)
record COFE : Set1 where
field
ofe : OFE
open OFE ofe
field
limU : (carrier → domain) → domain
isLimitU : ∀ {fam} →
IsCoherent {U} (lift fam) →
IsLimit {U} (lift fam) (limU fam)
lim↓ : ∀ a → Family (↓ a) → domain
isLimit↓ : ∀ a {fam : Family (↓ a)} →
IsCoherent fam → IsLimit fam (lim↓ a fam)
open OFE ofe public
record ContractiveFun (cofe : COFE) : Set where
open COFE cofe
field
F : domain → domain
isContractive : IsContractive F
open EqReasoning
fam : carrier → domain
fam = wfRec (const₁ domain) (λ a rec → F (lim↓ a rec))
fixpoint : domain
fixpoint = limU fam
postulate unfold : ∀ a → fam a ≅ F (lim↓ a (lift fam))
fam-isCoherent-↓ : ∀ a → IsCoherent {↓ a} (lift fam)
fam-isCoherent-↓ = wfRec P step
where
P : Pred carrier
P a = IsCoherent {↓ a} (lift fam)
step : ∀ a → WfRec P a → P a
step a rec {c} {b} c<a b<a c<b = begin
fam c ≈⟨ unfold c c ⟩
F (lim↓ c (lift fam)) ≈⟨ isContractive (λ {d} d<c → begin
lim↓ c (lift fam) ≈⟨ sym $ isLimit↓ c (rec c c<a) d<c ⟩
lift {↓ a} fam d
(trans d<c c<a) ≈⟨ isLimit↓ b (rec b b<a) (trans d<c c<b) ⟩
lim↓ b (lift fam) ∎) ⟩
F (lim↓ b (lift fam)) ≈⟨ sym $ unfold b c ⟩
fam b ∎
fam-isCoherent-U : IsCoherent {U} (lift fam)
fam-isCoherent-U {a'} {a} _ _ = wfRec P step a a'
where
P : Pred carrier
P a = ∀ a' → a' < a → Eq a' (fam a') (fam a)
step : ∀ a → WfRec P a → P a
step a rec a' a'<a = begin
fam a' ≈⟨ unfold a' a' ⟩
F (lim↓ a' (lift fam)) ≈⟨ isContractive (λ {b} b<a' → begin
lim↓ a' (lift fam) ≈⟨ sym $ isLimit↓ a' (fam-isCoherent-↓ a') b<a' ⟩
fam b ≈⟨ isLimit↓ a (fam-isCoherent-↓ a) (trans b<a' a'<a) ⟩
lim↓ a (lift fam) ∎) ⟩
F (lim↓ a (lift fam)) ≈⟨ sym $ unfold a a' ⟩
fam a ∎
isFixpoint : fixpoint ≅ F fixpoint
isFixpoint a = begin
fixpoint ≈⟨ sym $ isLimitU fam-isCoherent-U _ ⟩
fam a ≈⟨ unfold a a ⟩
F (lim↓ a (lift fam)) ≈⟨ isContractive (λ {a'} a'<a → begin
lim↓ a (lift fam) ≈⟨ sym $ isLimit↓ a (fam-isCoherent-↓ a) a'<a ⟩
fam a' ≈⟨ isLimitU fam-isCoherent-U _ ⟩
limU fam ∎) ⟩
F (limU fam) ≈⟨ refl ⟩
F fixpoint ∎
unique : ∀ x → x ≅ F x → x ≅ fixpoint
unique x isFix = wfRec P step
where
P = λ a → Eq a x fixpoint
step : ∀ a → WfRec P a → P a
step a rec = begin
x ≈⟨ isFix a ⟩
F x ≈⟨ isContractive (λ {a'} a'<a → rec a' a'<a) ⟩
F fixpoint ≈⟨ sym $ isFixpoint a ⟩
fixpoint ∎