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

minor

Browse source
This commit is contained in:
Leon Vatthauer 2024-03-12 16:18:07 +01:00
parent 32e29aedb8
commit 98cdfffdb9
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
2 changed files with 14 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
agda/src/Monad/Instance/Setoids/Delay.lagda.md
View file

@ -44,7 +44,7 @@ module _ (A : Set c) where
later : Delay′ → Delay
record Delay′ : Set c where
coinductive
constructor dela
constructor delay
field force : Delay
open Delay′ public

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

@ -115,7 +115,7 @@ Now we show that `iter` defines an Elgot algebra structure on `Delay≈`
iter≈-fixpoint : ∀ {A X : Setoid ℓ ℓ} {f : X ⟶ (Delay≈.₀ A ⊎ₛ X)} {x : ∣ X ∣} → [ A ][ iter {A} {X} < f > x ≈ [ Function.id , iter {A} {X} < f > ] (f ⟨$⟩ x) ]
iter≈-fixpoint {A} {X} {f} {x} with < f > x in eqx
... | inj₁ a = ≈-refl A
... | inj₂ a = ≈-trans A (≈-sym A later-self) (≈-refl A)
... | inj₂ a = ≈-sym A later-self
-- iter satisfies the uniformity law
iter-uni : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delay≈.₀ A ⊎ₛ X)} {g : Y ⟶ (Delay≈.₀ A ⊎ₛ Y)} {h : X ⟶ Y}
@ -335,24 +335,20 @@ Now we show that helper # is iteration preserving:
preserves' {X} {g} {x} = ≡-trans ⟦ B ⟧ step₁ step₂
where
step₁ : [ ⟦ B ⟧ ][ (delay-lift≈ ∘ (iter≈ {A} {X} g)) ⟨$⟩ x ≡ ([ inj₁ₛ ∘ (helper #) , inj₂ₛ ]ₛ ∘ (disc-dom g)) # ⟨$⟩ x ]
step₁ = ≡-trans ⟦ B ⟧ (≡-trans ⟦ B ⟧ (cong (helper #) (iter-g-var g)) (sub-step₁ (disc-dom g) {inj₂ x})) (≡-sym ⟦ B ⟧ (#-Compositionality B {f = helper} {h = disc-dom g}))
step₁ = ≡-trans ⟦ B ⟧ (≡-trans ⟦ B ⟧ (cong (helper #) (iter-g-var g)) (≡-sym ⟦ B ⟧ (#-Uniformity B {h = [ idₛ (Delay∼.₀ A) , iter∼ (disc-dom g) ]ₛ} (λ {y} → by-uni {y})))) (≡-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))
by-uni : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ (Delay∼.₀ A) ][ [ inj₁ₛ , inj₂ₛ ∘ [ idₛ (Delay∼.₀ A) , iter∼ (disc-dom g) ]ₛ ]ₛ ∘ [ [ inj₁ₛ , inj₂ₛ ∘ inj₁ₛ ]ₛ ∘ helper , inj₂ₛ ∘ inj₂ₛ ]ₛ ∘ [ inj₁ₛ , (disc-dom g) ]ₛ ⟨$⟩ x ≡ (helper ∘ [ idₛ (Delay∼.₀ A) , iter∼ (disc-dom g) ]ₛ) ⟨$⟩ x ]
by-uni {inj₁ (now a)} = ≡-refl (⟦ B ⟧ ⊎ₛ (Delay∼.₀ A))
by-uni {inj₁ (later a)} = ≡-refl (⟦ B ⟧ ⊎ₛ (Delay∼.₀ A))
by-uni {inj₂ a} with (disc-dom 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₂ = #-Uniformity B {h = ‖‖-quote} sub-step₂
step₂ = #-Uniformity B {h = ‖‖-quote} by-uni
where
sub-step₂ : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ X ][([ inj₁ₛ , inj₂ₛ ]ₛ ∘ ([ inj₁ₛ ∘ (helper #) , inj₂ₛ ]ₛ ∘ (disc-dom g))) ⟨$⟩ x ≡ ([ inj₁ₛ ∘ delay-lift≈ , inj₂ₛ ]ₛ ∘ g) ⟨$⟩ x ]
sub-step₂ {x} with g ⟨$⟩ x
by-uni : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ X ][([ inj₁ₛ , inj₂ₛ ]ₛ ∘ ([ inj₁ₛ ∘ (helper #) , inj₂ₛ ]ₛ ∘ (disc-dom g))) ⟨$⟩ x ≡ ([ inj₁ₛ ∘ delay-lift≈ , inj₂ₛ ]ₛ ∘ g) ⟨$⟩ x ]
by-uni {x} with g ⟨$⟩ x
... | inj₁ y = ≡-refl (⟦ B ⟧ ⊎ₛ X)
... | inj₂ y = ≡-refl (⟦ B ⟧ ⊎ₛ X)
open Elgot-Algebra-Morphism using (preserves) renaming (h to <<_>>)
@ -393,7 +389,7 @@ Only uniqueness of delaylift is left now:
cong helper-now (later∼ eq) = inj₂ (force∼ eq)
iter-id : ∀ {x} → [ A ][ x ≈ iter≈ ([ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x ]
iter-id {now x} = ≈-refl A
iter-id {now x} = ≈-refl A
iter-id {later x} = later≈ λ { .force≈ → iter-id }
-- the 'meat' of this proof: