mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
Work on delay example
This commit is contained in:
parent
1e7e156f0b
commit
d299a7d09a
SSH key fingerprint:
SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
1 changed files with 48 additions and 61 deletions
|
|
@ -1,6 +1,6 @@
|
|||
<!--
|
||||
```agda
|
||||
{-# OPTIONS --allow-unsolved-metas --guardedness --exact-split #-}
|
||||
{-# OPTIONS --allow-unsolved-metas --guardedness #-}
|
||||
|
||||
open import Level
|
||||
open import Category.Ambient using (Ambient)
|
||||
|
|
@ -24,6 +24,7 @@ import Relation.Binary.PropositionalEquality as Eq
|
|||
open Eq using (_≡_)
|
||||
open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax)
|
||||
open import Codata.Musical.Notation
|
||||
import Category.Monad.Partiality
|
||||
```
|
||||
-->
|
||||
|
||||
|
|
@ -51,71 +52,57 @@ module Monad.Instance.K.Instance.Delay' {c ℓ} where
|
|||
laterˡ : ∀ {x y} → x ≈ (♭ y) → x ≈ later y
|
||||
laterʳ : ∀ {x y} → (♭ x) ≈ y → later x ≈ y
|
||||
|
||||
≈w-refl : (a : Delay C) → a ≈ a
|
||||
≈w-refl (now x) = now refl
|
||||
≈w-refl (later x) = later (♯ ≈w-refl (♭ x))
|
||||
-- later can be dropped
|
||||
laterʳ⁻¹ : ∀ {x : Delay C} {y} → x ≈ later y → x ≈ ♭ y
|
||||
laterʳ⁻¹ {.(later _)} {y} (later x≈y) = laterʳ (♭ x≈y)
|
||||
laterʳ⁻¹ {x} {y} (laterˡ x≈y) = x≈y
|
||||
laterʳ⁻¹ {.(later _)} {y} (laterʳ x≈y) = laterʳ (laterʳ⁻¹ x≈y)
|
||||
|
||||
≈w-sym : (a b : Delay C) → a ≈ b → b ≈ a
|
||||
≈w-sym .(now _) .(now _) (now eq) = now (sym eq)
|
||||
≈w-sym (later x) (later y) (later eq) = later (♯ (≈w-sym (♭ x) (♭ y) (♭ eq)))
|
||||
≈w-sym x (later y) (laterˡ eq) = laterʳ (≈w-sym x (♭ y) eq)
|
||||
≈w-sym (later x) y (laterʳ eq) = laterˡ (≈w-sym (♭ x) y eq)
|
||||
laterˡ⁻¹ : ∀ {x} {y : Delay C} → later x ≈ y → ♭ x ≈ y
|
||||
laterˡ⁻¹ {x} {.(later _)} (later x≈y) = laterˡ (♭ x≈y)
|
||||
laterˡ⁻¹ {x} {.(later _)} (laterˡ x≈y) = laterˡ (laterˡ⁻¹ x≈y)
|
||||
laterˡ⁻¹ {x} {y} (laterʳ x≈y) = x≈y
|
||||
|
||||
module Trans where
|
||||
-- TODO later-trans from stdlib https://agda.github.io/agda-stdlib/v1.7.3/Category.Monad.Partiality.html#2311
|
||||
now-trans : ∀ {a b c} → a ≈ b → b ≈ now c → a ≈ now c
|
||||
now-trans {now x} {now x₁} {c} (now x₂) (now x₃) = now (IsEquivalence.trans (Setoid.isEquivalence A) x₂ x₃)
|
||||
now-trans {now x} {later x₁} {c} (laterˡ a≈b) (laterʳ b≈c) = now-trans a≈b b≈c
|
||||
now-trans {later x} {now x₁} {c} (laterʳ a≈b) (now x₂) = laterʳ (now-trans a≈b (now x₂))
|
||||
now-trans {later x} {later x₁} {c} (later x₂) (laterʳ b≈c) = laterʳ (now-trans (♭ x₂) b≈c)
|
||||
now-trans {later x} {later x₁} {c} (laterˡ a≈b) (laterʳ b≈c) = now-trans a≈b b≈c
|
||||
now-trans {later x} {later x₁} {c} (laterʳ a≈b) (laterʳ b≈c) = laterʳ (now-trans a≈b (laterʳ b≈c))
|
||||
≈w-trans : (a b c : Delay C) → a ≈ b → b ≈ c → a ≈ c
|
||||
≈w-trans (now _) (now _) (now _) (now a∼b) (now b∼c) = now (IsEquivalence.trans (Setoid.isEquivalence A) a∼b b∼c)
|
||||
≈w-trans (now a) (now b) (later c) (now a∼b) (laterˡ b≈c) = laterˡ (≈w-trans (now a) (now b) (♭ c) (now a∼b) b≈c)
|
||||
≈w-trans (now a) (later b) (now c) (laterˡ a≈b) (laterʳ b≈c) = ≈w-trans (now a) (♭ b) (now c) a≈b b≈c
|
||||
≈w-trans (now a) (later b) (later c) (laterˡ a≈b) (later b≈c) = laterˡ (≈w-trans (now a) (♭ b) (♭ c) a≈b (♭ b≈c))
|
||||
≈w-trans (now a) (later b) (later c) (laterˡ a≈b) (laterˡ b≈c) = laterˡ (≈w-trans (now a) {! !} (♭ c) a≈b {! !})
|
||||
≈w-trans (now a) (later b) (later c) (laterˡ a≈b) (laterʳ b≈c) = {! !}
|
||||
≈w-trans (later x) (now x₁) (now x₂) a≈b b≈c = {! !}
|
||||
≈w-trans (later x) (now x₁) (later x₂) a≈b b≈c = {! !}
|
||||
≈w-trans (later x) (later x₁) (now x₂) a≈b b≈c = {! !}
|
||||
≈w-trans (later x) (later x₁) (later x₂) a≈b b≈c = {! !}
|
||||
later⁻¹ : ∀ {x y : ∞ (Delay C)} → later x ≈ later y → ♭ x ≈ ♭ y
|
||||
later⁻¹ {x} {y} (later x≈y) = ♭ x≈y
|
||||
later⁻¹ {x} {y} (laterˡ x≈y) = laterˡ⁻¹ x≈y
|
||||
later⁻¹ {x} {y} (laterʳ x≈y) = laterʳ⁻¹ x≈y
|
||||
|
||||
≈-refl : (a : Delay C) → a ≈ a
|
||||
≈-refl (now x) = now refl
|
||||
≈-refl (later x) = later (♯ ≈-refl (♭ x))
|
||||
|
||||
-- data _≈w_ {A : Setoid c ℓ} : Delay (Setoid.Carrier A) → Delay (Setoid.Carrier A) → Set ℓ where
|
||||
-- now : ∀ {x y} → Setoid._≈_ A x y → (now x) ≈w (now y)
|
||||
-- later : ∀ {x y} → ∞ (_≈w_ {A} (♭ x) (♭ y)) → (later x) ≈w (later y)
|
||||
-- laterˡ : ∀ {x y} → _≈w_ {A} x (♭ y) → x ≈w later y
|
||||
-- laterʳ : ∀ {x y} → _≈w_ {A} (♭ x) y → later x ≈w y
|
||||
≈-sym : (a b : Delay C) → a ≈ b → b ≈ a
|
||||
≈-sym .(now _) .(now _) (now eq) = now (sym eq)
|
||||
≈-sym (later x) (later y) (later eq) = later (♯ (≈-sym (♭ x) (♭ y) (♭ eq)))
|
||||
≈-sym x (later y) (laterˡ eq) = laterʳ (≈-sym x (♭ y) eq)
|
||||
≈-sym (later x) y (laterʳ eq) = laterˡ (≈-sym (♭ x) y eq)
|
||||
|
||||
-- ≈w-refl : ∀ {A : Setoid c ℓ} (a : Delay (Setoid.Carrier A)) → _≈w_ {A} a a
|
||||
-- ≈w-refl {A} (now x) = now (IsEquivalence.refl (Setoid.isEquivalence A) {x})
|
||||
-- ≈w-refl {A} (later x) = later (♯ ≈w-refl (♭ x))
|
||||
-- later-trans from stdlib https://agda.github.io/agda-stdlib/v1.7.3/Category.Monad.Partiality.html#2311
|
||||
now-trans : ∀ {a b c} → a ≈ b → b ≈ now c → a ≈ now c
|
||||
now-trans {now x} {now x₁} {c} (now x₂) (now x₃) = now (IsEquivalence.trans (Setoid.isEquivalence A) x₂ x₃)
|
||||
now-trans {now x} {later x₁} {c} (laterˡ a≈b) (laterʳ b≈c) = now-trans a≈b b≈c
|
||||
now-trans {later x} {now x₁} {c} (laterʳ a≈b) (now x₂) = laterʳ (now-trans a≈b (now x₂))
|
||||
now-trans {later x} {later x₁} {c} (later x₂) (laterʳ b≈c) = laterʳ (now-trans (♭ x₂) b≈c)
|
||||
now-trans {later x} {later x₁} {c} (laterˡ a≈b) (laterʳ b≈c) = now-trans a≈b b≈c
|
||||
now-trans {later x} {later x₁} {c} (laterʳ a≈b) (laterʳ b≈c) = laterʳ (now-trans a≈b (laterʳ b≈c))
|
||||
mutual
|
||||
later-trans : ∀ {a b : Delay C} {c : ∞ (Delay C)} → a ≈ b → b ≈ (later c) → a ≈ (later c)
|
||||
later-trans {later a} {later b} {c} (later a≈b) b≈c = later (♯ ≈-trans (♭ a) (♭ b) (♭ c) (♭ a≈b) (later⁻¹ b≈c))
|
||||
{-# CATCHALL #-}
|
||||
later-trans {a} {later b} {c} (laterˡ a≈b) b≈c = later-trans a≈b (laterˡ⁻¹ b≈c)
|
||||
{-# CATCHALL #-}
|
||||
later-trans {later a} {b} {c} (laterʳ a≈b) b≈c = later (♯ ≈-trans (♭ a) b (♭ c) a≈b (laterʳ⁻¹ b≈c))
|
||||
{-# CATCHALL #-}
|
||||
later-trans {a} {b} {c} a≈b (laterˡ b≈c) = laterˡ (≈-trans a b (♭ c) a≈b b≈c)
|
||||
|
||||
-- ≈w-sym : ∀ {A : Setoid c ℓ} (a b : Delay (Setoid.Carrier A)) → _≈w_ {A} a b → _≈w_ {A} b a
|
||||
-- ≈w-sym {A} .(now _) .(now _) (now eq) = now (IsEquivalence.sym (Setoid.isEquivalence A) eq)
|
||||
-- ≈w-sym {A} (later x) (later y) (later eq) = later (♯ (≈w-sym (♭ x) (♭ y) (♭ eq)))
|
||||
-- ≈w-sym {A} x (later y) (laterˡ eq) = laterʳ (≈w-sym x (♭ y) eq)
|
||||
-- ≈w-sym {A} (later x) y (laterʳ eq) = laterˡ (≈w-sym (♭ x) y eq)
|
||||
|
||||
-- ≈w-trans : ∀ {A : Setoid c ℓ} (a b c : Delay (Setoid.Carrier A)) → _≈w_ {A} a b → _≈w_ {A} b c → _≈w_ {A} a c
|
||||
-- ≈w-trans {A} .(now _) .(now _) .(now _) (now eq₁) (now eq₂) = now (IsEquivalence.trans (Setoid.isEquivalence A) eq₁ eq₂)
|
||||
-- ≈w-trans {A} (now x) (now y) (later z) (now eq₁) (laterˡ eq₂) = laterˡ (≈w-trans (now x) (now y) (♭ z) (now eq₁) eq₂)
|
||||
-- ≈w-trans {A} (later x) (later y) (later z) (later eq₁) (later eq₂) = later (♯ (≈w-trans (♭ x) (♭ y) (♭ z) (♭ eq₁) (♭ eq₂)))
|
||||
-- ≈w-trans {A} (later x) (later y) (later z) (later eq₁) (laterˡ eq₂) = laterˡ (≈w-trans (later x) (later y) (♭ z) (later eq₁) eq₂)
|
||||
-- -- ≈w-trans {A} .(later _) .(later _) c (later x) (laterʳ eq₂) = {! !}
|
||||
-- ≈w-trans {A} (later x) (later y) z (later eq₁) (laterʳ eq₂) = {! !}
|
||||
-- ≈w-trans {A} a .(later _) .(later _) (laterˡ eq₁) (later x) = {! !}
|
||||
-- ≈w-trans {A} a .(later _) .(later _) (laterˡ eq₁) (laterˡ eq₂) = {! !}
|
||||
-- ≈w-trans {A} a .(later _) c (laterˡ eq₁) (laterʳ eq₂) = {! !}
|
||||
-- ≈w-trans {A} .(later _) .(now _) .(now _) (laterʳ eq₁) (now x) = {! !}
|
||||
-- ≈w-trans {A} .(later _) .(later _) .(later _) (laterʳ eq₁) (later x) = {! !}
|
||||
-- ≈w-trans {A} .(later _) b .(later _) (laterʳ eq₁) (laterˡ eq₂) = {! !}
|
||||
-- ≈w-trans {A} .(later _) .(later _) c (laterʳ eq₁) (laterʳ eq₂) = {! !}
|
||||
|
||||
-- delay-setoid : Setoid c ℓ → Setoid c ℓ
|
||||
-- delay-setoid A = record { Carrier = Delay Carrier ; _≈_ = _≈w_ {A} ; isEquivalence = record { refl = λ {x} → ≈w-refl x ; sym = λ {x y} → ≈w-sym x y ; trans = {! !} } }
|
||||
-- where open Setoid A
|
||||
≈-trans : ∀ (a b c : Delay C) → a ≈ b → b ≈ c → a ≈ c
|
||||
≈-trans a b (now c) a≈b b≈c = now-trans a≈b b≈c
|
||||
≈-trans a b (later c) a≈b b≈c = later-trans a≈b b≈c
|
||||
|
||||
delay-setoid : Setoid c ℓ → Setoid c ℓ
|
||||
delay-setoid A = record { Carrier = Delay Carrier ; _≈_ = _≈_ {A} ; isEquivalence = record { refl = λ {x} → ≈-refl x ; sym = λ {x y} → ≈-sym x y ; trans = λ {x y z} → ≈-trans x y z } }
|
||||
where
|
||||
open Setoid A using (Carrier)
|
||||
open Equality
|
||||
```
|
||||
Loading…
Reference in a new issue