agda-spa/Fixedpoint.agda
Danila Fedorin 512cd22be5 Fix definition of 'less than' to not involve a third variable.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-07 21:04:13 -08:00

82 lines
4.4 KiB
Agda
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

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
⊥ᴬ : A
⊥ᴬ = proj₁ (proj₁ (proj₁ fixedHeight))
⊥ᴬ≼ : (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 (proj₂ fixedHeight) (ChainA.step x≺⊥ᴬ ≈-refl (proj₂ (proj₁ fixedHeight))))
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 (proj₂ fixedHeight) 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₂ a : A) (a≈fa : a f a) (a₂≼a : a₂ a)
(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₂) a
stepPreservesLess 0 _ _ _ _ _ _ c g+hᶜ≡sh _ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n (proj₂ fixedHeight) c)
stepPreservesLess (suc g') hᶜ a₁ a₂ a a≈fa a₂≼a c g+hᶜ≡sh a₂≼fa₂ rewrite sym (+-suc g' hᶜ)
with ≈-dec a₂ (f a₂)
... | yes _ = a₂≼a
... | no _ = stepPreservesLess g' _ _ _ a a≈fa (≼-cong ≈-refl (≈-sym a≈fa) (Monotonicᶠ a₂≼a)) _ _ _
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 ⊥ᴬ))