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

fixed definition of iter

Browse source
This commit is contained in:
Leon Vatthauer 2024-01-07 15:55:54 +01:00
parent f56bd7f1aa
commit 45d281fc5a
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
1 changed files with 20 additions and 48 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -38,7 +38,7 @@ module Monad.Instance.Setoids.K' {ℓ : Level} where
force (iter′ {A} {X} f x) = iter {A} {X} f x force (iter′ {A} {X} f x) = iter {A} {X} f x
iter {A} {X} f x with f x iter {A} {X} f x with f x
... | inj₁ a = a ... | inj₁ a = a
... | inj₂ b = later (iter′ {A} {X} f x) ... | inj₂ b = later (iter′ {A} {X} f b)
conflict : ∀ {ℓ''} (X Y : Setoid ℓ ℓ) {Z : Set ℓ''} conflict : ∀ {ℓ''} (X Y : Setoid ℓ ℓ) {Z : Set ℓ''}
{x : ∣ X ∣} {y : ∣ Y ∣} → [ X ⊎ₛ Y ][ inj₁ x ≡ inj₂ y ] → Z {x : ∣ X ∣} {y : ∣ Y ∣} → [ X ⊎ₛ Y ][ inj₁ x ≡ inj₂ y ] → Z
@ -69,17 +69,18 @@ module Monad.Instance.Setoids.K' {ℓ : Level} where
... | inj₁ a | inj₁ b = inj₁-helper f x≡y eqx eqy ... | inj₁ a | inj₁ b = inj₁-helper f x≡y eqx eqy
... | inj₁ a | inj₂ b = absurd-helper f x≡y eqx eqy ... | inj₁ a | inj₂ b = absurd-helper f x≡y eqx eqy
... | inj₂ a | inj₁ b = absurd-helper f (≡-sym X x≡y) eqy eqx ... | inj₂ a | inj₁ b = absurd-helper f (≡-sym X x≡y) eqy eqx
... | inj₂ a | inj₂ b = later≈ (iter-cong′ f x≡y) ... | inj₂ a | inj₂ b = later≈ (iter-cong′ {A} {X} f (inj₂-helper f x≡y eqx eqy))
iterₛ : ∀ {A X : Setoid ℓ ℓ} → (X ⟶ (Delayₛ A ⊎ₛ X)) → X ⟶ Delayₛ A iterₛ : ∀ {A X : Setoid ℓ ℓ} → (X ⟶ (Delayₛ A ⊎ₛ X)) → X ⟶ Delayₛ A
iterₛ {A} {X} f = record { _⟨$⟩_ = iter {A} {X} (f ._⟨$⟩_) ; cong = iter-cong {A} {X} f } iterₛ {A} {X} f = record { _⟨$⟩_ = iter {A} {X} (f ._⟨$⟩_) ; cong = iter-cong {A} {X} f }
iter-fixpoint : ∀ {A X : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ iter {A} {X} (f ._⟨$⟩_) x ≈ [ Function.id , iter {A} {X} (f ._⟨$⟩_) ] ((f ._⟨$⟩_) y) ] iter-fixpoint : ∀ {A X : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ iter {A} {X} < f > x ≈ [ Function.id , iter {A} {X} < f > ] (f ⟨$⟩ y) ]
iter-fixpoint {A} {X} {f} {x} {y} x≡y with (f ._⟨$⟩_) x in eqx | (f ._⟨$⟩_) y in eqy iter-fixpoint {A} {X} {f} {x} {y} x≡y with (f ._⟨$⟩_) x in eqx | (f ._⟨$⟩_) y in eqy
... | inj₁ a | inj₁ b = inj₁-helper f x≡y eqx eqy ... | inj₁ a | inj₁ b = inj₁-helper f x≡y eqx eqy
... | inj₁ a | inj₂ b = absurd-helper f x≡y eqx eqy ... | inj₁ a | inj₂ b = absurd-helper f x≡y eqx eqy
... | inj₂ a | inj₁ b = absurd-helper f (≡-sym X x≡y) eqy eqx ... | inj₂ a | inj₁ b = absurd-helper f (≡-sym X x≡y) eqy eqx
... | inj₂ a | inj₂ b = ≈-trans A (≈-sym A later-self) (iter-cong f {! !}) ... | inj₂ a | inj₂ b = ≈-trans A (≈-sym A later-self) (iter-cong f (inj₂-helper f x≡y eqx eqy))
iter-resp-≈ : ∀ {A X : Setoid ℓ ℓ} (f g : X ⟶ (Delayₛ A ⊎ₛ X)) → f ≋ g → ∀ {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ iter {A} {X} (f ._⟨$⟩_) x ≈ iter {A} {X} (g ._⟨$⟩_) y ] iter-resp-≈ : ∀ {A X : Setoid ℓ ℓ} (f g : X ⟶ (Delayₛ A ⊎ₛ X)) → f ≋ g → ∀ {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ iter {A} {X} (f ._⟨$⟩_) x ≈ iter {A} {X} (g ._⟨$⟩_) y ]
iter-resp-≈′ : ∀ {A X : Setoid ℓ ℓ} (f g : X ⟶ (Delayₛ A ⊎ₛ X)) → f ≋ g → ∀ {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ iter {A} {X} (f ._⟨$⟩_) x ≈′ iter {A} {X} (g ._⟨$⟩_) y ] iter-resp-≈′ : ∀ {A X : Setoid ℓ ℓ} (f g : X ⟶ (Delayₛ A ⊎ₛ X)) → f ≋ g → ∀ {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ iter {A} {X} (f ._⟨$⟩_) x ≈′ iter {A} {X} (g ._⟨$⟩_) y ]
@ -97,63 +98,35 @@ module Monad.Instance.Setoids.K' {ℓ : Level} where
where where
helper : [ Delayₛ A ⊎ₛ X ][ inj₂ a ≡ inj₁ b ] helper : [ Delayₛ A ⊎ₛ X ][ inj₂ a ≡ inj₁ b ]
helper rewrite (≣-sym eqy) | (≣-sym eqx) = f≋g x≡y helper rewrite (≣-sym eqy) | (≣-sym eqx) = f≋g x≡y
... | inj₂ a | inj₂ b = later≈ (iter-resp-≈′ f g f≋g x≡y) ... | inj₂ a | inj₂ b = later≈ (iter-resp-≈′ f g f≋g (drop-inj₂ helper))
iter-folding' : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {h : Y ⟶ X ⊎ₛ Y} {x y : ∣ X ⊎ₛ Y ∣} → [ X ⊎ₛ Y ][ x ≡ y ] → [ A ][ iter {A} {X ⊎ₛ Y} [ inj₁ ∘f iter {A} {X} (f ._⟨$⟩_) , inj₂ ∘f (h ._⟨$⟩_) ] x ≈ iter {A} {X ⊎ₛ Y} [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘f (f ._⟨$⟩_) , (inj₂ ∘f (h ._⟨$⟩_)) ] y ]
iter-folding′ : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {h : Y ⟶ X ⊎ₛ Y} {x y : ∣ X ⊎ₛ Y ∣} → [ X ⊎ₛ Y ][ x ≡ y ] → [ A ][ iter {A} {X ⊎ₛ Y} [ inj₁ ∘f iter {A} {X} (f ._⟨$⟩_) , inj₂ ∘f (h ._⟨$⟩_) ] x ≈′ iter {A} {X ⊎ₛ Y} [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘f (f ._⟨$⟩_) , (inj₂ ∘f (h ._⟨$⟩_)) ] y ]
force≈ (iter-folding′ {A} {X} {Y} {f} {h} {x} {y} x≡y) = iter-folding' {A} {X} {Y} {f} {h} x≡y
iter-folding' {A} {X} {Y} {f} {h} {inj₁ x} {inj₁ y} ix≡iy with f ⟨$⟩ x in eqx | f ⟨$⟩ y in eqy
... | inj₁ a | inj₁ b = inj₁-helper f (drop-inj₁ ix≡iy) eqx eqy
... | inj₁ a | inj₂ b = absurd-helper f (drop-inj₁ ix≡iy) eqx eqy
... | inj₂ a | inj₁ b = absurd-helper f (≡-sym X (drop-inj₁ ix≡iy)) eqy eqx
... | inj₂ a | inj₂ b = later≈ helper
where where
helper' : ∀ (b : ∣ X ∣) → [ A ][ iter < f > b ≈′ iter [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ < f > , inj₂ ∘′ < h > ] (inj₁ b) ] helper : [ Delayₛ A ⊎ₛ X ][ inj₂ a ≡ inj₂ b ]
helper'' : ∀ (b : ∣ X ∣) → [ A ][ iter < f > b ≈ iter [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ < f > , inj₂ ∘′ < h > ] (inj₁ b) ] helper rewrite (≣-sym eqy) | (≣-sym eqx) = f≋g x≡y
helper'' b with f ⟨$⟩ b in eqb
... | inj₁ c = ≈-refl A
... | inj₂ c = later≈ (helper' b)
force≈ (helper' b) with f ⟨$⟩ b in eqb
... | inj₁ c = ≈-refl A
... | inj₂ c = later≈ (helper' b)
helper : [ A ][ iter < f > x ≈′ iter [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ < f > , inj₂ ∘′ < h > ] (inj₁ y) ]
force≈ helper = ≈-trans A (iter-cong f (drop-inj₁ ix≡iy)) (helper'' y)
iter-folding' {A} {X} {Y} {f} {h} {inj₂ x} {inj₂ y} ix≡iy with h ⟨$⟩ x in eqx | h ⟨$⟩ y in eqy
... | inj₁ a | inj₁ b = later≈ {! iter-folding′ {A} {X} {Y} {f} {h} {inj₁ a} {inj₁ b} helper !}
where
helper : [ X ⊎ₛ Y ][ inj₁ a ≡ inj₁ b ]
helper rewrite (≣-sym eqx) | (≣-sym eqy) = cong h (drop-inj₂ ix≡iy)
... | inj₁ a | inj₂ b = absurd-helper h (drop-inj₂ ix≡iy) eqx eqy
... | inj₂ a | inj₁ b = absurd-helper h (≡-sym Y (drop-inj₂ ix≡iy)) eqy eqx
... | inj₂ a | inj₂ b = later≈ {! !}
where
helper' : [ A ][ iter [ inj₁ ∘′ iter < f > , inj₂ ∘′ < h > ] (inj₂ x) ≈′ iter [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ < f > , inj₂ ∘′ < h > ] (inj₂ y) ]
force≈ helper' = later≈ {! iter-folding' {A} {X} {Y} {f} {h} {inj₂ a} {inj₂ b} ? !}
helper : [ X ⊎ₛ Y ][ inj₂ a ≡ inj₂ b ]
helper rewrite (≣-sym eqx) | (≣-sym eqy) = cong h (drop-inj₂ ix≡iy)
iter-folding : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {h : Y ⟶ X ⊎ₛ Y} {x y : ∣ X ⊎ₛ Y ∣} → [ X ⊎ₛ Y ][ x ≡ y ] → [ A ][ iter {A} {X ⊎ₛ Y} [ inj₁ ∘f iter {A} {X} (f ._⟨$⟩_) , inj₂ ∘f (h ._⟨$⟩_) ] x ≈ iter {A} {X ⊎ₛ Y} [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘f (f ._⟨$⟩_) , (inj₂ ∘f (h ._⟨$⟩_)) ] y ] iter-folding : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {h : Y ⟶ X ⊎ₛ Y} {x y : ∣ X ⊎ₛ Y ∣} → [ X ⊎ₛ Y ][ x ≡ y ] → [ A ][ iter {A} {X ⊎ₛ Y} [ inj₁ ∘f iter {A} {X} (f ._⟨$⟩_) , inj₂ ∘f (h ._⟨$⟩_) ] x ≈ iter {A} {X ⊎ₛ Y} [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘f (f ._⟨$⟩_) , (inj₂ ∘f (h ._⟨$⟩_)) ] y ]
iter-folding′ : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {h : Y ⟶ X ⊎ₛ Y} {x y : ∣ X ⊎ₛ Y ∣} → [ X ⊎ₛ Y ][ x ≡ y ] → [ A ][ iter {A} {X ⊎ₛ Y} [ inj₁ ∘f iter {A} {X} (f ._⟨$⟩_) , inj₂ ∘f (h ._⟨$⟩_) ] x ≈′ iter {A} {X ⊎ₛ Y} [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘f (f ._⟨$⟩_) , (inj₂ ∘f (h ._⟨$⟩_)) ] y ]
force≈ (iter-folding′ {A} {X} {Y} {f} {h} {x} {y} x≡y) = iter-folding {A} {X} {Y} {f} {h} x≡y
iter-folding {A} {X} {Y} {f} {h} {inj₁ x} {inj₁ y} ix≡iy with f ⟨$⟩ x in eqx | f ⟨$⟩ y in eqy iter-folding {A} {X} {Y} {f} {h} {inj₁ x} {inj₁ y} ix≡iy with f ⟨$⟩ x in eqx | f ⟨$⟩ y in eqy
... | inj₁ a | inj₁ b = inj₁-helper f (drop-inj₁ ix≡iy) eqx eqy ... | inj₁ a | inj₁ b = inj₁-helper f (drop-inj₁ ix≡iy) eqx eqy
... | inj₁ a | inj₂ b = absurd-helper f (drop-inj₁ ix≡iy) eqx eqy ... | inj₁ a | inj₂ b = absurd-helper f (drop-inj₁ ix≡iy) eqx eqy
... | inj₂ a | inj₁ b = absurd-helper f (≡-sym X (drop-inj₁ ix≡iy)) eqy eqx ... | inj₂ a | inj₁ b = absurd-helper f (≡-sym X (drop-inj₁ ix≡iy)) eqy eqx
... | inj₂ a | inj₂ b = later≈ {! !} -- later≈ (♯ ≈-trans A (iter-cong f (inj₂-helper f (drop-inj₁ ix≡iy) eqx eqy)) (helper b)) ... | inj₂ a | inj₂ b = later≈ (≈→≈′ A (≈-trans A (iter-cong f (inj₂-helper f (drop-inj₁ ix≡iy) eqx eqy)) (helper b)))
where where
helper : ∀ (b : ∣ X ∣) → [ A ][ iter {A} {X} (f ._⟨$⟩_) b ≈ iter {A} {X ⊎ₛ Y} [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ (f ._⟨$⟩_) , inj₂ ∘′ (h ._⟨$⟩_) ] (inj₁ b) ] helper : ∀ (b : ∣ X ∣) → [ A ][ iter < f > b ≈ iter [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ < f > , inj₂ ∘′ < h > ] (inj₁ b) ]
helper' : ∀ (b : ∣ X ∣) → [ A ][ iter < f > b ≈′ iter [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ < f > , inj₂ ∘′ < h > ] (inj₁ b) ]
helper b with f ⟨$⟩ b in eqb helper b with f ⟨$⟩ b in eqb
... | inj₁ c = ≡-refl (Delayₛ A) ... | inj₁ c = ≈-refl A
... | inj₂ c = later≈ {! !} -- later≈ (♯ helper c) ... | inj₂ c = later≈ (helper' c)
force≈ (helper' b) = helper b
iter-folding {A} {X} {Y} {f} {h} {inj₂ x} {inj₂ y} ix≡iy with h ⟨$⟩ x in eqx | h ⟨$⟩ y in eqy iter-folding {A} {X} {Y} {f} {h} {inj₂ x} {inj₂ y} ix≡iy with h ⟨$⟩ x in eqx | h ⟨$⟩ y in eqy
... | inj₁ a | inj₁ b = {! !} -- later≈ (♯ iter-folding {A} {X} {Y} {f} {h} {inj₁ a} {inj₁ b} helper) ... | inj₁ a | inj₁ b = later≈ (iter-folding′ {A} {X} {Y} {f} {h} {inj₁ a} {inj₁ b} helper)
where where
helper : [ X ⊎ₛ Y ][ inj₁ a ≡ inj₁ b ] helper : [ X ⊎ₛ Y ][ inj₁ a ≡ inj₁ b ]
helper rewrite (≣-sym eqx) | (≣-sym eqy) = cong h (drop-inj₂ ix≡iy) helper rewrite (≣-sym eqx) | (≣-sym eqy) = cong h (drop-inj₂ ix≡iy)
... | inj₁ a | inj₂ b = absurd-helper h (drop-inj₂ ix≡iy) eqx eqy ... | inj₁ a | inj₂ b = absurd-helper h (drop-inj₂ ix≡iy) eqx eqy
... | inj₂ a | inj₁ b = absurd-helper h (≡-sym Y (drop-inj₂ ix≡iy)) eqy eqx ... | inj₂ a | inj₁ b = absurd-helper h (≡-sym Y (drop-inj₂ ix≡iy)) eqy eqx
... | inj₂ a | inj₂ b = {! !} -- later≈ (♯ iter-folding {A} {X} {Y} {f} {h} {inj₂ a} {inj₂ b} helper) ... | inj₂ a | inj₂ b = later≈ (iter-folding′ {A} {X} {Y} {f} {h} helper)
where where
helper : [ X ⊎ₛ Y ][ inj₂ a ≡ inj₂ b ] helper : [ X ⊎ₛ Y ][ inj₂ a ≡ inj₂ b ]
helper rewrite (≣-sym eqx) | (≣-sym eqy) = cong h (drop-inj₂ ix≡iy) helper rewrite (≣-sym eqx) | (≣-sym eqy) = cong h (drop-inj₂ ix≡iy)
@ -191,5 +164,4 @@ module Monad.Instance.Setoids.K' {ℓ : Level} where
; *-lift = {! !} ; *-lift = {! !}
; *-uniq = {! !} ; *-uniq = {! !}
} }
``` ```