leonv/bsc-leon-vatthauer
1
0
Fork 0
mirror of https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git synced 2024-05-31 07:28:34 +02:00
Code Issues Projects Releases Packages Wiki Activity

Finished preservation proof

Browse source
This commit is contained in:
Leon Vatthauer 2024-02-03 14:33:10 +01:00
parent e5b707457c
commit 32feee45e5
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
1 changed files with 15 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
agda/src/Monad/Instance/Setoids/K.lagda.md
View file

@ -182,7 +182,7 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
delay-lift : ∀ {A : Setoid ℓ ℓ} {B : Elgot-Algebra} → A ⟶ ⟦ B ⟧ → Elgot-Algebra-Morphism (delay-algebras A) B delay-lift : ∀ {A : Setoid ℓ ℓ} {B : Elgot-Algebra} → A ⟶ ⟦ B ⟧ → Elgot-Algebra-Morphism (delay-algebras A) B
delay-lift {A} {B} f = record { h = delay-lift' ; preserves = λ {X} {g} {x} → ≡-trans ⟦ B ⟧ (preserves' {X} {g} {x}) (#-resp-≈ B (≡-refl (⟦ B ⟧ ⊎ₛ X))) } delay-lift {A} {B} f = record { h = delay-lift' ; preserves = λ {X} {g} {x} → preserves' {X} {g} {x} }
where where
open Elgot-Algebra B using (_#) open Elgot-Algebra B using (_#)
-- (f + id) ∘ out -- (f + id) ∘ out
@ -296,7 +296,7 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
where where
eq' : ∀ {n} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ [ inj₁ , inj₂ ∘′ μ ∘′ liftF ι ] (helper₁' (now (x , n))) ≡ (helper₁ ∘′ μ {A} ∘′ liftF ι) (now (y , n)) ] eq' : ∀ {n} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ [ inj₁ , inj₂ ∘′ μ ∘′ liftF ι ] (helper₁' (now (x , n))) ≡ (helper₁ ∘′ μ {A} ∘′ liftF ι) (now (y , n)) ]
eq' {zero} = inj₁ (cong f x∼y) eq' {zero} = inj₁ (cong f x∼y)
eq' {suc n} = inj₂ (∼-trans A (cong (μₛ∼ A) (∼-sym (Delayₛ∼ A) (lift-comp∼ {f = outer} {g = ιₛ'} {ι (x , n)} (∼-refl A)))) (∼-trans A identityˡ∼ (cong ιₛ' (x∼y , ≣-refl)))) -- (identityˡ∼ (cong ιₛ' (x∼y , ≣-refl)))) eq' {suc n} = inj₂ (∼-trans A (cong (μₛ∼ A) (∼-sym (Delayₛ∼ A) (lift-comp∼ {f = outer} {g = ιₛ'} {ι (x , n)} (∼-refl A)))) (∼-trans A identityˡ∼ (cong ιₛ' (x∼y , ≣-refl))))
eq (later∼ x∼y) = inj₂ (cong (μₛ∼ A) (cong (liftFₛ∼ ιₛ') (force∼ x∼y))) eq (later∼ x∼y) = inj₂ (cong (μₛ∼ A) (cong (liftFₛ∼ ιₛ') (force∼ x∼y)))
eq₂ : [ ⟦ B ⟧ ][ helper' # ⟨$⟩ z ≡ helper # ⟨$⟩ μ {A} (liftF (ι {A}) z)] eq₂ : [ ⟦ B ⟧ ][ helper' # ⟨$⟩ z ≡ helper # ⟨$⟩ μ {A} (liftF (ι {A}) z)]
@ -329,7 +329,19 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
preserves' {X} {g} {x} = ≡-trans ⟦ B ⟧ step₁ step₂ preserves' {X} {g} {x} = ≡-trans ⟦ B ⟧ step₁ step₂
where where
step₁ : [ ⟦ B ⟧ ][ (delay-lift' ∘ (iterₛ {A} {X} g)) ⟨$⟩ x ≡ ([ inj₁ₛ ∘ (helper #) , inj₂ₛ ]ₛ ∘ (disc-dom g)) # ⟨$⟩ x ] step₁ : [ ⟦ B ⟧ ][ (delay-lift' ∘ (iterₛ {A} {X} g)) ⟨$⟩ x ≡ ([ inj₁ₛ ∘ (helper #) , inj₂ₛ ]ₛ ∘ (disc-dom g)) # ⟨$⟩ x ]
step₁ = {! !} step₁ = ≡-trans ⟦ B ⟧ (≡-trans ⟦ B ⟧ (helper#∼-cong (iter-g-var g)) (sub-step₁ (disc-dom g) {inj₂ x})) (≡-sym ⟦ B ⟧ (#-Compositionality B {f = helper} {h = disc-dom g}))
where
sub-step₁ : (g : ‖ X ‖ ⟶ ((Delayₛ∼ A) ⊎ₛ ‖ X ‖)) → ∀ {x} → [ ⟦ B ⟧ ][ ((helper #) ∘ [ idₛ (Delayₛ∼ A) , iterₛ∼ g ]ₛ) ⟨$⟩ x
≡ ([ [ inj₁ₛ , inj₂ₛ ∘ inj₁ₛ ]ₛ ∘ helper , inj₂ₛ ∘ inj₂ₛ ]ₛ ∘ [ inj₁ₛ , g ]ₛ) # ⟨$⟩ x ]
sub-step₁ g {u} = ≡-sym ⟦ B ⟧ (#-Uniformity B {h = [ idₛ (Delayₛ∼ A) , iterₛ∼ g ]ₛ} (λ {y} → last-step {y}))
where
last-step : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ (Delayₛ∼ A) ][ [ inj₁ₛ , inj₂ₛ ∘ [ idₛ (Delayₛ∼ A) , iterₛ∼ g ]ₛ ]ₛ ∘ [ [ inj₁ₛ , inj₂ₛ ∘ inj₁ₛ ]ₛ ∘ helper , inj₂ₛ ∘ inj₂ₛ ]ₛ ∘ [ inj₁ₛ , g ]ₛ ⟨$⟩ x ≡ (helper ∘ [ idₛ (Delayₛ∼ A) , iterₛ∼ g ]ₛ) ⟨$⟩ x ]
last-step {inj₁ (now a)} = ≡-refl (⟦ B ⟧ ⊎ₛ (Delayₛ∼ A))
last-step {inj₁ (later a)} = ≡-refl (⟦ B ⟧ ⊎ₛ (Delayₛ∼ A))
last-step {inj₂ a} with g ⟨$⟩ a in eqb
... | inj₁ (now b) = ≡-refl (⟦ B ⟧ ⊎ₛ (Delayₛ∼ A))
... | inj₁ (later b) = ≡-refl (⟦ B ⟧ ⊎ₛ (Delayₛ∼ A))
... | inj₂ b = ≡-refl (⟦ B ⟧ ⊎ₛ (Delayₛ∼ A))
step₂ : [ ⟦ B ⟧ ][ ([ inj₁ₛ ∘ (helper #) , inj₂ₛ ]ₛ ∘ (disc-dom g)) # ⟨$⟩ x ≡ ([ inj₁ₛ ∘ delay-lift' , inj₂ₛ ]ₛ ∘ g) # ⟨$⟩ x ] step₂ : [ ⟦ B ⟧ ][ ([ inj₁ₛ ∘ (helper #) , inj₂ₛ ]ₛ ∘ (disc-dom g)) # ⟨$⟩ x ≡ ([ inj₁ₛ ∘ delay-lift' , inj₂ₛ ]ₛ ∘ g) # ⟨$⟩ x ]
step₂ = #-Uniformity B {h = ‖‖-quote} sub-step₂ step₂ = #-Uniformity B {h = ‖‖-quote} sub-step₂
where where
@ -337,8 +349,6 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
sub-step₂ {x} with g ⟨$⟩ x sub-step₂ {x} with g ⟨$⟩ x
... | inj₁ y = ≡-refl (⟦ B ⟧ ⊎ₛ X) ... | inj₁ y = ≡-refl (⟦ B ⟧ ⊎ₛ X)
... | inj₂ y = ≡-refl (⟦ B ⟧ ⊎ₛ X) ... | inj₂ y = ≡-refl (⟦ B ⟧ ⊎ₛ X)
comp-step : [ ⟦ B ⟧ ][ ([ inj₁ₛ ∘ (helper #) , inj₂ₛ ]ₛ ∘ disc-dom g) # ⟨$⟩ x ≡ ((([ ([ inj₁ₛ , (inj₂ₛ ∘ inj₁ₛ) ]ₛ ∘ helper) , (inj₂ₛ ∘ inj₂ₛ) ]ₛ ∘ [ inj₁ₛ , (disc-dom g) ]ₛ) #) ∘ inj₂ₛ) ⟨$⟩ x ]
comp-step = #-Compositionality B {f = helper} {h = disc-dom g}
<<_>> = Elgot-Algebra-Morphism.h <<_>> = Elgot-Algebra-Morphism.h