agda-spa/Fixedpoint.agda

88 lines
4.5 KiB
Agda
Raw Normal View History

open import Data.Nat as Nat using (; suc; _+_; _≤_)
open import Lattice
module Fixedpoint {a} {A : Set a}
{h : }
{_≈_ : A A Set a}
{_⊔_ : A A A} {_⊓_ : A A A}
(≈-dec : IsDecidable _≈_)
(flA : IsFiniteHeightLattice A h _≈_ _⊔_ _⊓_)
(f : A A)
(Monotonicᶠ : Monotonic (IsFiniteHeightLattice._≼_ flA)
(IsFiniteHeightLattice._≼_ flA) f) where
open import Data.Nat.Properties using (+-suc; +-comm)
open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
open import Data.Empty using (⊥-elim)
open import Relation.Binary.PropositionalEquality using (_≡_; sym)
open import Relation.Nullary using (Dec; ¬_; yes; no)
open IsFiniteHeightLattice flA
import Chain
module ChainA = Chain _≈_ ≈-equiv _≺_ ≺-cong
private
open ChainA.Height fixedHeight
using ()
renaming
( to ⊥ᴬ
; longestChain to longestChainᴬ
; bounded to boundedᴬ
)
⊥ᴬ≼ : (a : A) ⊥ᴬ a
⊥ᴬ≼ a with ≈-dec a ⊥ᴬ
... | yes a≈⊥ᴬ = ≼-cong a≈⊥ᴬ ≈-refl (≼-refl a)
... | no a̷≈⊥ᴬ with ≈-dec ⊥ᴬ (a ⊥ᴬ)
... | yes ⊥ᴬ≈a⊓⊥ᴬ = ≈-trans (⊔-comm ⊥ᴬ a) (≈-trans (≈-⊔-cong (≈-refl {a}) ⊥ᴬ≈a⊓⊥ᴬ) (absorb-⊔-⊓ a ⊥ᴬ))
... | no ⊥ᴬ̷≈a⊓⊥ᴬ = ⊥-elim (ChainA.Bounded-suc-n boundedᴬ (ChainA.step x≺⊥ᴬ ≈-refl longestChainᴬ))
where
⊥ᴬ⊓a̷≈⊥ᴬ : ¬ (⊥ᴬ a) ⊥ᴬ
⊥ᴬ⊓a̷≈⊥ᴬ = λ ⊥ᴬ⊓a≈⊥ᴬ ⊥ᴬ̷≈a⊓⊥ᴬ (≈-trans (≈-sym ⊥ᴬ⊓a≈⊥ᴬ) (⊓-comm _ _))
x≺⊥ᴬ : (⊥ᴬ a) ⊥ᴬ
x≺⊥ᴬ = (≈-trans (⊔-comm _ _) (≈-trans (≈-refl {⊥ᴬ (⊥ᴬ a)}) (absorb-⊔-⊓ ⊥ᴬ a)) , ⊥ᴬ⊓a̷≈⊥ᴬ)
-- using 'g', for gas, here helps make sure the function terminates.
-- since A forms a fixed-height lattice, we must find a solution after
-- 'h' steps at most. Gas is set up such that as soon as it runs
-- out, we have exceeded h steps, which shouldn't be possible.
doStep : (g hᶜ : ) (a₁ a₂ : A) (c : ChainA.Chain a₁ a₂ hᶜ) (g+hᶜ≡h : g + hᶜ suc h) (a₂≼fa₂ : a₂ f a₂) Σ A (λ a a f a)
doStep 0 hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n boundedᴬ c)
doStep (suc g') hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite sym (+-suc g' hᶜ)
with ≈-dec a₂ (f a₂)
... | yes a₂≈fa₂ = (a₂ , a₂≈fa₂)
... | no a₂̷≈fa₂ = doStep g' (suc hᶜ) a₁ (f a₂) c' g+hᶜ≡sh (Monotonicᶠ a₂≼fa₂)
where
a₂≺fa₂ : a₂ f a₂
a₂≺fa₂ = (a₂≼fa₂ , a₂̷≈fa₂)
c' : ChainA.Chain a₁ (f a₂) (suc hᶜ)
c' rewrite +-comm 1 hᶜ = ChainA.concat c (ChainA.step a₂≺fa₂ ≈-refl (ChainA.done (≈-refl {f a₂})))
fix : Σ A (λ a a f a)
fix = doStep (suc h) 0 ⊥ᴬ ⊥ᴬ (ChainA.done ≈-refl) (+-comm (suc h) 0) (⊥ᴬ≼ (f ⊥ᴬ))
aᶠ : A
aᶠ = proj₁ fix
aᶠ≈faᶠ : aᶠ f aᶠ
aᶠ≈faᶠ = proj₂ fix
private
stepPreservesLess : (g hᶜ : ) (a₁ a₂ b : A) (b≈fb : b f b) (a₂≼a : a₂ b)
(c : ChainA.Chain a₁ a₂ hᶜ) (g+hᶜ≡h : g + hᶜ suc h)
(a₂≼fa₂ : a₂ f a₂)
proj₁ (doStep g hᶜ a₁ a₂ c g+hᶜ≡h a₂≼fa₂) b
stepPreservesLess 0 _ _ _ _ _ _ c g+hᶜ≡sh _ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n boundedᴬ c)
stepPreservesLess (suc g') hᶜ a₁ a₂ b b≈fb a₂≼b c g+hᶜ≡sh a₂≼fa₂ rewrite sym (+-suc g' hᶜ)
with ≈-dec a₂ (f a₂)
... | yes _ = a₂≼b
... | no _ = stepPreservesLess g' _ _ _ b b≈fb (≼-cong ≈-refl (≈-sym b≈fb) (Monotonicᶠ a₂≼b)) _ _ _
aᶠ≼ : (a : A) a f a aᶠ a
aᶠ≼ a a≈fa = stepPreservesLess (suc h) 0 ⊥ᴬ ⊥ᴬ a a≈fa (⊥ᴬ≼ a) (ChainA.done ≈-refl) (+-comm (suc h) 0) (⊥ᴬ≼ (f ⊥ᴬ))