From 232664e96fe4cc25dd476f8d54866600a6530a7b Mon Sep 17 00:00:00 2001
From: Eric Giovannini <ecg19@seas.upenn.edu>
Date: Thu, 30 Mar 2023 17:20:32 -0400
Subject: [PATCH] More code refactoring/cleanup
---
.../guarded-cubical/Results/Coinductive.agda | 10 +-
.../Results/IntensionalAdequacy.agda | 8 +-
.../Semantics/ErrorDomains.agda | 69 ++
.../guarded-cubical/Semantics/Lift.agda | 127 +++
.../Semantics/Monotone/Base.agda | 82 ++
.../Semantics/Monotone/Lemmas.agda | 403 +++++++++
.../Semantics/Monotone/MonFunCombinators.agda | 417 +++++++++
.../guarded-cubical/Semantics/Predomains.agda | 84 ++
.../guarded-cubical/Semantics/Semantics.agda | 9 +-
.../Semantics/StrongBisimulation.agda | 821 +-----------------
10 files changed, 1228 insertions(+), 802 deletions(-)
create mode 100644 formalizations/guarded-cubical/Semantics/ErrorDomains.agda
create mode 100644 formalizations/guarded-cubical/Semantics/Lift.agda
create mode 100644 formalizations/guarded-cubical/Semantics/Monotone/Base.agda
create mode 100644 formalizations/guarded-cubical/Semantics/Monotone/Lemmas.agda
create mode 100644 formalizations/guarded-cubical/Semantics/Monotone/MonFunCombinators.agda
create mode 100644 formalizations/guarded-cubical/Semantics/Predomains.agda
diff --git a/formalizations/guarded-cubical/Results/Coinductive.agda b/formalizations/guarded-cubical/Results/Coinductive.agda
index d5e1989..ae807c3 100644
--- a/formalizations/guarded-cubical/Results/Coinductive.agda
+++ b/formalizations/guarded-cubical/Results/Coinductive.agda
@@ -15,8 +15,12 @@ open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Structure
open import Cubical.Data.Empty
-open import Results.IntensionalAdequacy
+open import Semantics.Predomains
open import Semantics.StrongBisimulation
+open import Semantics.Lift
+
+open import Results.IntensionalAdequacy
+
private
variable
@@ -178,7 +182,7 @@ module _ {X : Type} (H-irrel : clock-irrel X) where
-- Bisimilarity relation on Machines.
-module Bisim (X : Predomain k0) (H-irrel : clock-irrel ⟨ X ⟩) where
+module Bisim (X : Predomain) (H-irrel : clock-irrel ⟨ X ⟩) where
-- Mutually define coinductive bisimilarity of machines
@@ -188,7 +192,7 @@ module Bisim (X : Predomain k0) (H-irrel : clock-irrel ⟨ X ⟩) where
record _≋_ (m m' : Machine ⟨ X ⟩) : Type
_≋''_ : State ⟨ X ⟩ -> State ⟨ X ⟩ -> Type
- result x ≋'' result x' = rel k0 X x x'
+ result x ≋'' result x' = rel X x x'
error ≋'' error = ⊤
running m ≋'' running m' = m ≋ m' -- using the coinductive bisimilarity on machines
_ ≋'' _ = ⊥
diff --git a/formalizations/guarded-cubical/Results/IntensionalAdequacy.agda b/formalizations/guarded-cubical/Results/IntensionalAdequacy.agda
index 7b4a0d6..dcb58df 100644
--- a/formalizations/guarded-cubical/Results/IntensionalAdequacy.agda
+++ b/formalizations/guarded-cubical/Results/IntensionalAdequacy.agda
@@ -26,10 +26,12 @@ open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Function
import Semantics.StrongBisimulation
-import Common.MonFuns
+import Semantics.Monotone.Base
import Syntax.GradualSTLC
open import Common.Common
+open import Semantics.Predomains
+open import Semantics.Lift
-- TODO move definition of Predomain to a module that
-- isn't parameterized by a clock!
@@ -199,7 +201,7 @@ module AdequacyLockstep
open Semantics.StrongBisimulation
open Semantics.StrongBisimulation.LiftPredomain
- _≾-gl_ : {p : Predomain k0} -> (L℧F ⟨ p ⟩) -> (L℧F ⟨ p ⟩) -> Type
+ _≾-gl_ : {p : Predomain} -> (L℧F ⟨ p ⟩) -> (L℧F ⟨ p ⟩) -> Type
_≾-gl_ {p} lx ly = ∀ (k : Clock) -> _≾_ k p (lx k) (ly k)
-- _≾'_ : {k : Clock} -> L℧ k Nat → L℧ k Nat → Type
@@ -299,7 +301,7 @@ module AdequacyBisim where
-- Some properties of the global bisimilarity relation
- module GlobalBisim (p : Predomain k0) where
+ module GlobalBisim (p : Predomain) where
_≈-gl_ : (L℧F ⟨ p ⟩) -> (L℧F ⟨ p ⟩) -> Type
_≈-gl_ lx ly = ∀ (k : Clock) -> _≈_ k p (lx k) (ly k)
diff --git a/formalizations/guarded-cubical/Semantics/ErrorDomains.agda b/formalizations/guarded-cubical/Semantics/ErrorDomains.agda
new file mode 100644
index 0000000..89c6f66
--- /dev/null
+++ b/formalizations/guarded-cubical/Semantics/ErrorDomains.agda
@@ -0,0 +1,69 @@
+
+{-# OPTIONS --cubical --rewriting --guarded #-}
+
+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+open import Common.Later
+
+module Semantics.ErrorDomains (k : Clock) where
+
+open import Cubical.Relation.Binary.Poset
+open import Cubical.Foundations.Structure
+
+open import Semantics.Predomains
+open import Cubical.Data.Sigma
+
+
+open import Semantics.Monotone.Base
+
+-- Error domains
+
+record ErrorDomain : Setâ‚ where
+ field
+ X : Predomain
+ module X = PosetStr (X .snd)
+ _≤_ = X._≤_
+ field
+ ℧ : X .fst
+ ℧⊥ : ∀ x → ℧ ≤ x
+ θ : MonFun (▸''_ k X) X
+
+
+-- Underlying predomain of an error domain
+
+𕌠: ErrorDomain -> Predomain
+𕌠d = ErrorDomain.X d
+
+{-
+arr : Predomain -> ErrorDomain -> ErrorDomain
+arr dom cod =
+ record {
+ X = arr' dom (𕌠cod) ;
+ ℧ = const-err ;
+ ℧⊥ = const-err-bot ;
+ θ = {!!} }
+ where
+ -- open LiftOrder
+ const-err : ⟨ arr' dom (𕌠cod) ⟩
+ const-err = record {
+ f = λ _ -> ErrorDomain.℧ cod ;
+ isMon = λ _ -> reflexive (𕌠cod) (ErrorDomain.℧ cod) }
+
+ const-err-bot : (f : ⟨ arr' dom (𕌠cod) ⟩) -> rel (arr' dom (𕌠cod)) const-err f
+ const-err-bot f = λ x y x≤y → ErrorDomain.℧⊥ cod (MonFun.f f y)
+-}
+
+
+{-
+-- Predomain to lift Error Domain
+
+ð•ƒâ„§ : Predomain → ErrorDomain
+ð•ƒâ„§ X = record {
+ X = 𕃠X ; ℧ = ℧ ; ℧⊥ = ord-bot X ;
+ θ = record { f = θ ; isMon = λ t -> {!!} } }
+ where
+ -- module X = PosetStr (X .snd)
+ -- open Relation X
+ open LiftPredomain
+-}
diff --git a/formalizations/guarded-cubical/Semantics/Lift.agda b/formalizations/guarded-cubical/Semantics/Lift.agda
new file mode 100644
index 0000000..9b45cc8
--- /dev/null
+++ b/formalizations/guarded-cubical/Semantics/Lift.agda
@@ -0,0 +1,127 @@
+{-# OPTIONS --cubical --rewriting --guarded #-}
+
+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+open import Common.Later
+
+module Semantics.Lift (k : Clock) where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Relation.Nullary
+open import Cubical.Data.Empty hiding (rec)
+
+private
+ variable
+ l : Level
+ A B : Set l
+private
+ ▹_ : Set l → Set l
+ â–¹_ A = â–¹_,_ k A
+
+
+ -- Lift monad
+
+data L℧ (X : Set) : Set where
+ η : X → L℧ X
+ ℧ : L℧ X
+ θ : ▹ (L℧ X) → L℧ X
+
+
+-- Delay function
+δ : {X : Type} -> L℧ X -> L℧ X
+δ = θ ∘ next
+
+-- Similar to caseNat,
+-- defined at https://agda.github.io/cubical/Cubical.Data.Nat.Base.html#487
+caseL℧ : {X : Set} -> {ℓ : Level} -> {A : Type ℓ} ->
+ (aη a℧ aθ : A) → (L℧ X) → A
+caseL℧ aη a℧ aθ (η x) = aη
+caseL℧ aη a℧ aθ ℧ = a℧
+caseL℧ a0 a℧ aθ (θ lx~) = aθ
+
+-- Similar to znots and snotz, defined at
+-- https://agda.github.io/cubical/Cubical.Data.Nat.Properties.html
+℧≠θ : {X : Set} -> {lx~ : ▹ (L℧ X)} -> ¬ (℧ ≡ θ lx~)
+℧≠θ {X} {lx~} eq = subst (caseL℧ X (L℧ X) ⊥) eq ℧
+
+θ≠℧ : {X : Set} -> {lx~ : ▹ (L℧ X)} -> ¬ (θ lx~ ≡ ℧)
+θ≠℧ {X} {lx~} eq = subst (caseL℧ X ⊥ (L℧ X)) eq (θ lx~)
+
+
+-- TODO: Does this make sense?
+pred : {X : Set} -> (lx : L℧ X) -> ▹ (L℧ X)
+pred (η x) = next ℧
+pred ℧ = next ℧
+pred (θ lx~) = lx~
+
+pred-def : {X : Set} -> (def : ▹ (L℧ X)) -> (lx : L℧ X) -> ▹ (L℧ X)
+pred-def def (η x) = def
+pred-def def ℧ = def
+pred-def def (θ lx~) = lx~
+
+
+-- TODO: This uses the pred function above, and I'm not sure whether that
+-- function makes sense.
+inj-θ : {X : Set} -> (lx~ ly~ : ▹ (L℧ X)) ->
+ θ lx~ ≡ θ ly~ ->
+ ▸ (λ t -> lx~ t ≡ ly~ t)
+inj-θ lx~ ly~ H = let lx~≡ly~ = cong pred H in
+ λ t i → lx~≡ly~ i t
+
+ret : {X : Set} -> X -> L℧ X
+ret = η
+
+
+ext' : (A -> L℧ B) -> ▹ (L℧ A -> L℧ B) -> L℧ A -> L℧ B
+ext' f rec (η x) = f x
+ext' f rec ℧ = ℧
+ext' f rec (θ l-la) = θ (rec ⊛ l-la)
+
+ext : (A -> L℧ B) -> L℧ A -> L℧ B
+ext f = fix (ext' f)
+
+
+bind : L℧ A -> (A -> L℧ B) -> L℧ B
+bind {A} {B} la f = ext f la
+
+mapL : (A -> B) -> L℧ A -> L℧ B
+mapL f la = bind la (λ a -> ret (f a))
+
+unfold-ext : (f : A -> L℧ B) -> ext f ≡ ext' f (next (ext f))
+unfold-ext f = fix-eq (ext' f)
+
+
+ext-eta : ∀ (a : A) (f : A -> L℧ B) ->
+ ext f (η a) ≡ f a
+ext-eta a f =
+ fix (ext' f) (ret a) ≡⟨ (λ i → unfold-ext f i (ret a)) ⟩
+ (ext' f) (next (ext f)) (ret a) ≡⟨ refl ⟩
+ f a ∎
+
+ext-err : (f : A -> L℧ B) ->
+ bind ℧ f ≡ ℧
+ext-err f =
+ fix (ext' f) ℧ ≡⟨ (λ i → unfold-ext f i ℧) ⟩
+ (ext' f) (next (ext f)) ℧ ≡⟨ refl ⟩
+ ℧ ∎
+
+
+ext-theta : (f : A -> L℧ B)
+ (l : ▹ (L℧ A)) ->
+ bind (θ l) f ≡ θ (ext f <$> l)
+ext-theta f l =
+ (fix (ext' f)) (θ l) ≡⟨ (λ i → unfold-ext f i (θ l)) ⟩
+ (ext' f) (next (ext f)) (θ l) ≡⟨ refl ⟩
+ θ (fix (ext' f) <$> l) ∎
+
+
+mapL-eta : (f : A -> B) (a : A) ->
+ mapL f (η a) ≡ η (f a)
+mapL-eta f a = ext-eta a λ a → ret (f a)
+
+mapL-theta : (f : A -> B) (la~ : ▹ (L℧ A)) ->
+ mapL f (θ la~) ≡ θ (mapL f <$> la~)
+mapL-theta f la~ = ext-theta (ret ∘ f) la~
+
diff --git a/formalizations/guarded-cubical/Semantics/Monotone/Base.agda b/formalizations/guarded-cubical/Semantics/Monotone/Base.agda
new file mode 100644
index 0000000..6864216
--- /dev/null
+++ b/formalizations/guarded-cubical/Semantics/Monotone/Base.agda
@@ -0,0 +1,82 @@
+{-# OPTIONS --cubical --rewriting --guarded #-}
+
+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+
+module Semantics.Monotone.Base where
+
+open import Cubical.Relation.Binary.Poset
+open import Cubical.Data.Sigma
+open import Cubical.Foundations.Structure
+
+open import Semantics.Predomains
+
+private
+ variable
+ â„“ : Level
+
+-- Monotone functions from X to Y
+record MonFun (X Y : Predomain) : Set where
+ module X = PosetStr (X .snd)
+ module Y = PosetStr (Y .snd)
+ _≤X_ = X._≤_
+ _≤Y_ = Y._≤_
+ field
+ f : (X .fst) → (Y .fst)
+ isMon : ∀ {x y} → x ≤X y → f x ≤Y f y
+
+-- Use reflection to show that this is a sigma type
+-- Look for proof in standard library to show that
+-- Sigma type with a proof that RHS is a prop, then equality of a pair
+-- follows from equality of the LHS's
+-- Specialize to the case of monotone functions and fill in the proof
+-- later
+
+
+
+-- Monotone relations between predomains X and Y
+-- (antitone in X, monotone in Y).
+record MonRel {â„“' : Level} (X Y : Predomain) : Type (â„“-suc â„“') where
+ module X = PosetStr (X .snd)
+ module Y = PosetStr (Y .snd)
+ _≤X_ = X._≤_
+ _≤Y_ = Y._≤_
+ field
+ R : ⟨ X ⟩ -> ⟨ Y ⟩ -> Type ℓ'
+ isAntitone : ∀ {x x' y} -> R x y -> x' ≤X x -> R x' y
+ isMonotone : ∀ {x y y'} -> R x y -> y ≤Y y' -> R x y'
+
+predomain-monrel : (X : Predomain) -> MonRel X X
+predomain-monrel X = record {
+ R = rel X ;
+ isAntitone = λ {x} {x'} {y} x≤y x'≤x → transitive X x' x y x'≤x x≤y ;
+ isMonotone = λ {x} {y} {y'} x≤y y≤y' -> transitive X x y y' x≤y y≤y' }
+
+
+compRel : {X Y Z : Type} ->
+ (R1 : Y -> Z -> Type â„“) ->
+ (R2 : X -> Y -> Type â„“) ->
+ (X -> Z -> Type â„“)
+compRel {ℓ} {X} {Y} {Z} R1 R2 x z = Σ[ y ∈ Y ] R2 x y × R1 y z
+
+CompMonRel : {X Y Z : Predomain} ->
+ MonRel {â„“} Y Z ->
+ MonRel {â„“} X Y ->
+ MonRel {â„“} X Z
+CompMonRel {â„“} {X} {Y} {Z} R1 R2 = record {
+ R = compRel (MonRel.R R1) (MonRel.R R2) ;
+ isAntitone = antitone ;
+ isMonotone = {!!} }
+ where
+ antitone : {x x' : ⟨ X ⟩} {z : ⟨ Z ⟩} ->
+ compRel (MonRel.R R1) (MonRel.R R2) x z ->
+ rel X x' x ->
+ compRel (MonRel.R R1) (MonRel.R R2) x' z
+ antitone (y , xR2y , yR1z) x'≤x = y , (MonRel.isAntitone R2 xR2y x'≤x) , yR1z
+
+ monotone : {x : ⟨ X ⟩} {z z' : ⟨ Z ⟩} ->
+ compRel (MonRel.R R1) (MonRel.R R2) x z ->
+ rel Z z z' ->
+ compRel (MonRel.R R1) (MonRel.R R2) x z'
+ monotone (y , xR2y , yR1z) z≤z' = y , xR2y , (MonRel.isMonotone R1 yR1z z≤z')
diff --git a/formalizations/guarded-cubical/Semantics/Monotone/Lemmas.agda b/formalizations/guarded-cubical/Semantics/Monotone/Lemmas.agda
new file mode 100644
index 0000000..15e0791
--- /dev/null
+++ b/formalizations/guarded-cubical/Semantics/Monotone/Lemmas.agda
@@ -0,0 +1,403 @@
+{-# OPTIONS --cubical --rewriting --guarded #-}
+
+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+open import Common.Later
+
+module Semantics.Monotone.Lemmas (k : Clock) where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Nat renaming (â„• to Nat) hiding (_^_)
+
+open import Cubical.Relation.Binary
+open import Cubical.Relation.Binary.Poset
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Transport
+
+open import Cubical.Data.Unit
+open import Cubical.Data.Sigma
+open import Cubical.Data.Empty
+
+open import Cubical.Foundations.Function
+
+open import Semantics.Predomains
+open import Semantics.Lift k
+open import Semantics.Monotone.Base
+open import Semantics.StrongBisimulation k
+open import Syntax.GradualSTLC
+open import Syntax.SyntacticTermPrecision k
+
+private
+ variable
+ l : Level
+ A B : Set l
+private
+ ▹_ : Set l → Set l
+ â–¹_ A = â–¹_,_ k A
+
+open LiftPredomain
+
+{-
+test : (A B : Type) -> (eq : A ≡ B) -> (x : A) -> (T : (A : Type) -> A -> Type) ->
+ (T A x) -> (T B (transport eq x))
+test A B eq x T Tx = transport (λ i -> T (eq i) (transport-filler eq x i)) Tx
+
+-- transport (λ i -> T (eq i) ?) Tx
+-- Goal : eq i
+-- Constraints:
+-- x = ?8 (i = i0) : A
+-- ?8 (i = i1) = transp (λ i₠→ eq iâ‚) i0 x : B
+
+
+-- transport-filler : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B) (x : A)
+-- → PathP (λ i → p i) x (transport p x)
+
+
+test' : (A B : Predomain) -> (S : Type) ->
+ (eq : A ≡ B) ->
+ (x : ⟨ A ⟩) ->
+ (T : (A : Predomain) -> ⟨ A ⟩ -> Type) ->
+ (T A x) -> T B (transport (λ i -> ⟨ eq i ⟩) x)
+test' A B S eq x T Tx = transport
+ (λ i -> T (eq i) (transport-filler (λ j → ⟨ eq j ⟩) x i))
+ Tx
+-}
+
+
+-- If A ≡ B, then we can translate knowledge about a relation on A
+-- to its image in B obtained by transporting the related elements of A
+-- along the equality of the underlying sets of A and B
+rel-transport :
+ {A B : Predomain} ->
+ (eq : A ≡ B) ->
+ {a1 a2 : ⟨ A ⟩} ->
+ rel A a1 a2 ->
+ rel B
+ (transport (λ i -> ⟨ eq i ⟩) a1)
+ (transport (λ i -> ⟨ eq i ⟩) a2)
+rel-transport {A} {B} eq {a1} {a2} a1≤a2 =
+ transport (λ i -> rel (eq i)
+ (transport-filler (λ j -> ⟨ eq j ⟩) a1 i)
+ (transport-filler (λ j -> ⟨ eq j ⟩) a2 i))
+ a1≤a2
+
+rel-transport-sym : {A B : Predomain} ->
+ (eq : A ≡ B) ->
+ {b1 b2 : ⟨ B ⟩} ->
+ rel B b1 b2 ->
+ rel A
+ (transport (λ i → ⟨ sym eq i ⟩) b1)
+ (transport (λ i → ⟨ sym eq i ⟩) b2)
+rel-transport-sym eq {b1} {b2} b1≤b2 = rel-transport (sym eq) b1≤b2
+
+
+mTransport : {A B : Predomain} -> (eq : A ≡ B) -> ⟨ A ==> B ⟩
+mTransport {A} {B} eq = record {
+ f = λ b → transport (λ i -> ⟨ eq i ⟩) b ;
+ isMon = λ {b1} {b2} b1≤b2 → rel-transport eq b1≤b2 }
+
+
+mTransportSym : {A B : Predomain} -> (eq : A ≡ B) -> ⟨ B ==> A ⟩
+mTransportSym {A} {B} eq = record {
+ f = λ b → transport (λ i -> ⟨ sym eq i ⟩) b ;
+ isMon = λ {b1} {b2} b1≤b2 → rel-transport (sym eq) b1≤b2 }
+
+
+-- Transporting the domain of a monotone function preserves monotonicity
+mon-transport-domain : {A B C : Predomain} ->
+ (eq : A ≡ B) ->
+ (f : MonFun A C) ->
+ {b1 b2 : ⟨ B ⟩} ->
+ (rel B b1 b2) ->
+ rel C
+ (MonFun.f f (transport (λ i → ⟨ sym eq i ⟩ ) b1))
+ (MonFun.f f (transport (λ i → ⟨ sym eq i ⟩ ) b2))
+mon-transport-domain eq f {b1} {b2} b1≤b2 =
+ MonFun.isMon f (rel-transport (sym eq) b1≤b2)
+
+mTransportDomain : {A B C : Predomain} ->
+ (eq : A ≡ B) ->
+ MonFun A C ->
+ MonFun B C
+mTransportDomain {A} {B} {C} eq f = record {
+ f = g eq f;
+ isMon = mon-transport-domain eq f }
+ where
+ g : {A B C : Predomain} ->
+ (eq : A ≡ B) ->
+ MonFun A C ->
+ ⟨ B ⟩ -> ⟨ C ⟩
+ g eq f b = MonFun.f f (transport (λ i → ⟨ sym eq i ⟩ ) b)
+
+
+
+
+
+
+-- rel (𕃠B) (ext f la) (ext f' la') ≡ _A_1119
+-- ord (ext f la) (ext f' la') ≡
+-- ord' (next ord) (ext' f (next (ext f)) la) (ext' f (next (ext f)) la')
+
+
+-- ext respects monotonicity, in a general, heterogeneous sense
+ext-monotone-het : {A A' B B' : Predomain} ->
+ (rAA' : ⟨ A ⟩ -> ⟨ A' ⟩ -> Type) -> (rBB' : ⟨ B ⟩ -> ⟨ B' ⟩ -> Type) ->
+ (f : ⟨ A ⟩ -> ⟨ (𕃠B) ⟩) -> (f' : ⟨ A' ⟩ -> ⟨ (𕃠B') ⟩) ->
+ fun-order-het A A' (𕃠B) (𕃠B') rAA' (LiftRelation._≾_ B B' rBB') f f' ->
+ (la : ⟨ 𕃠A ⟩) -> (la' : ⟨ 𕃠A' ⟩) ->
+ (LiftRelation._≾_ A A' rAA' la la') ->
+ LiftRelation._≾_ B B' rBB' (ext f la) (ext f' la')
+ext-monotone-het {A} {A'} {B} {B'} rAA' rBB' f f' f≤f' la la' la≤la' =
+ let fixed = fix (monotone-ext') in
+ transport
+ (sym (λ i -> LiftBB'.unfold-≾ i (unfold-ext f i la) (unfold-ext f' i la')))
+ (fixed la la' (transport (λ i → LiftAA'.unfold-≾ i la la') la≤la'))
+ where
+
+
+ -- Note that these four have already been
+ -- passed (next _≾_) as a parameter (this happened in
+ -- the defintion of the module ð•ƒ, where we said
+ -- open Inductive (next _≾_) public)
+ _≾'LA_ = LiftPredomain._≾'_ A
+ _≾'LA'_ = LiftPredomain._≾'_ A'
+ _≾'LB_ = LiftPredomain._≾'_ B
+ _≾'LB'_ = LiftPredomain._≾'_ B'
+
+ module LiftAA' = LiftRelation A A' rAA'
+ module LiftBB' = LiftRelation B B' rBB'
+
+ -- The heterogeneous lifted relations
+ _≾'LALA'_ = LiftAA'.Inductive._≾'_ (next LiftAA'._≾_)
+ _≾'LBLB'_ = LiftBB'.Inductive._≾'_ (next LiftBB'._≾_)
+
+
+ monotone-ext' :
+ â–¹ (
+ (la : ⟨ 𕃠A ⟩) -> (la' : ⟨ 𕃠A' ⟩) ->
+ (la ≾'LALA' la') ->
+ (ext' f (next (ext f)) la) ≾'LBLB'
+ (ext' f' (next (ext f')) la')) ->
+ (la : ⟨ 𕃠A ⟩) -> (la' : ⟨ 𕃠A' ⟩) ->
+ (la ≾'LALA' la') ->
+ (ext' f (next (ext f)) la) ≾'LBLB'
+ (ext' f' (next (ext f')) la')
+ monotone-ext' IH (η x) (η y) x≤y =
+ transport
+ (λ i → LiftBB'.unfold-≾ i (f x) (f' y))
+ (f≤f' x y x≤y)
+ monotone-ext' IH ℧ la' la≤la' = tt
+ monotone-ext' IH (θ lx~) (θ ly~) la≤la' = λ t ->
+ transport
+ (λ i → (sym (LiftBB'.unfold-≾)) i
+ (sym (unfold-ext f) i (lx~ t))
+ (sym (unfold-ext f') i (ly~ t)))
+ (IH t (lx~ t) (ly~ t)
+ (transport (λ i -> LiftAA'.unfold-≾ i (lx~ t) (ly~ t)) (la≤la' t)))
+
+
+
+-- ext respects monotonicity (in the usual homogeneous sense)
+-- This can be rewritten to reuse the above result!
+ext-monotone : {A B : Predomain} ->
+ (f f' : ⟨ A ⟩ -> ⟨ (𕃠B) ⟩) ->
+ fun-order A (𕃠B) f f' ->
+ (la la' : ⟨ 𕃠A ⟩) ->
+ rel (𕃠A) la la' ->
+ rel (𕃠B) (ext f la) (ext f' la')
+ext-monotone {A} {B} f f' f≤f' la la' la≤la' =
+ let fixed = fix (monotone-ext' f f' f≤f') in
+ transport
+ (sym (λ i -> unfold-≾ B i (unfold-ext f i la) (unfold-ext f' i la')))
+ (fixed la la' (transport (λ i → unfold-≾ A i la la') la≤la'))
+ where
+
+ -- bring the homogeneous lifted relations into scope
+ _≾LA_ = LiftPredomain._≾_ A
+ _≾LB_ = LiftPredomain._≾_ B
+
+ -- Note that these next two have already been
+ -- passed (next _≾_) as a parameter (this happened in
+ -- the defintion of the module ð•ƒ, where we said
+ -- open Inductive (next _≾_) public)
+ _≾'LA_ = LiftPredomain._≾'_ A
+ _≾'LB_ = LiftPredomain._≾'_ B
+
+ monotone-ext' :
+ (f f' : ⟨ A ⟩ -> ⟨ (𕃠B) ⟩) ->
+ (fun-order A (𕃠B) f f') ->
+ â–¹ (
+ (la la' : ⟨ 𕃠A ⟩) ->
+ la ≾'LA la' ->
+ (ext' f (next (ext f)) la) ≾'LB
+ (ext' f' (next (ext f')) la')) ->
+ (la la' : ⟨ 𕃠A ⟩) ->
+ la ≾'LA la' ->
+ (ext' f (next (ext f)) la) ≾'LB
+ (ext' f' (next (ext f')) la')
+ monotone-ext' f f' f≤f' IH (η x) (η y) x≤y =
+ transport
+ (λ i → unfold-≾ B i (f x) (f' y))
+ (f≤f' x y x≤y)
+ monotone-ext' f f' f≤f' IH ℧ la' la≤la' = tt
+ monotone-ext' f f' f≤f' IH (θ lx~) (θ ly~) la≤la' = λ t ->
+ transport
+ (λ i → (sym (unfold-≾ B)) i
+ (sym (unfold-ext f) i (lx~ t))
+ (sym (unfold-ext f') i (ly~ t)))
+ (IH t (lx~ t) (ly~ t)
+ (transport (λ i -> unfold-≾ A i (lx~ t) (ly~ t)) (la≤la' t)))
+
+
+
+{-
+ext-monotone' : {A B : Predomain} ->
+ {la la' : ⟨ 𕃠A ⟩} ->
+ (f f' : ⟨ A ⟩ -> ⟨ (𕃠B) ⟩) ->
+ rel (𕃠A) la la' ->
+ fun-order A (𕃠B) f f' ->
+ rel (𕃠B) (ext f la) (ext f' la')
+ext-monotone' {A} {B} {la} {la'} f f' la≤la' f≤f' =
+ let fixed = fix (monotone-ext' f f' f≤f') in
+ --transport
+ --(sym (λ i -> ord B (unfold-ext f i la) (unfold-ext f' i la')))
+ (fixed la la' (transport (λ i → unfold-ord A i la la') la≤la'))
+ where
+ monotone-ext' :
+ (f f' : ⟨ A ⟩ -> ⟨ (𕃠B) ⟩) ->
+ (fun-order A (𕃠B) f f') ->
+ â–¹ (
+ (la la' : ⟨ 𕃠A ⟩) ->
+ ord' A (next (ord A)) la la' ->
+ ord B
+ (ext f la)
+ (ext f' la')) ->
+ (la la' : ⟨ 𕃠A ⟩) ->
+ ord' A (next (ord A)) la la' ->
+ ord B
+ (ext f la)
+ (ext f' la')
+ monotone-ext' f f' f≤f' IH (η x) (η y) x≤y = {!!} -- (f≤f' x y x≤y)
+ monotone-ext' f f' f≤f' IH ℧ la' la≤la' = transport (sym (λ i -> unfold-ord B i (ext f ℧) (ext f' la'))) {!!}
+ -- transport (sym (λ i → unfold-ord B i (ext' f (next (ext f)) ℧) (ext' f' (next (ext f')) la'))) tt
+ monotone-ext' f f' f≤f' IH (θ lx~) (θ ly~) la≤la' = {!!} -- λ t -> ?
+-}
+
+
+bind-monotone : {A B : Predomain} ->
+ {la la' : ⟨ 𕃠A ⟩} ->
+ (f f' : ⟨ A ⟩ -> ⟨ (𕃠B) ⟩) ->
+ rel (𕃠A) la la' ->
+ fun-order A (𕃠B) f f' ->
+ rel (𕃠B) (bind la f) (bind la' f')
+bind-monotone {A} {B} {la} {la'} f f' la≤la' f≤f' =
+ ext-monotone f f' f≤f' la la' la≤la'
+
+
+mapL-monotone-het : {A A' B B' : Predomain} ->
+ (rAA' : ⟨ A ⟩ -> ⟨ A' ⟩ -> Type) -> (rBB' : ⟨ B ⟩ -> ⟨ B' ⟩ -> Type) ->
+ (f : ⟨ A ⟩ -> ⟨ B ⟩) -> (f' : ⟨ A' ⟩ -> ⟨ B' ⟩) ->
+ fun-order-het A A' B B' rAA' rBB' f f' ->
+ (la : ⟨ 𕃠A ⟩) -> (la' : ⟨ 𕃠A' ⟩) ->
+ (LiftRelation._≾_ A A' rAA' la la') ->
+ LiftRelation._≾_ B B' rBB' (mapL f la) (mapL f' la')
+mapL-monotone-het {A} {A'} {B} {B'} rAA' rBB' f f' f≤f' la la' la≤la' =
+ ext-monotone-het rAA' rBB' (ret ∘ f) (ret ∘ f')
+ (λ a a' a≤a' → LiftRelation.Properties.ord-η-monotone B B' rBB' (f≤f' a a' a≤a'))
+ la la' la≤la'
+
+
+-- This is a special case of the above
+mapL-monotone : {A B : Predomain} ->
+ {la la' : ⟨ 𕃠A ⟩} ->
+ (f f' : ⟨ A ⟩ -> ⟨ B ⟩) ->
+ rel (𕃠A) la la' ->
+ fun-order A B f f' ->
+ rel (𕃠B) (mapL f la) (mapL f' la')
+mapL-monotone {A} {B} {la} {la'} f f' la≤la' f≤f' =
+ bind-monotone (ret ∘ f) (ret ∘ f') la≤la'
+ (λ a1 a2 a1≤a2 → ord-η-monotone B (f≤f' a1 a2 a1≤a2))
+
+-- As a corollary/special case, we can consider the case of a single
+-- monotone function.
+monotone-bind-mon : {A B : Predomain} ->
+ {la la' : ⟨ 𕃠A ⟩} ->
+ (f : MonFun A (𕃠B)) ->
+ (rel (𕃠A) la la') ->
+ rel (𕃠B) (bind la (MonFun.f f)) (bind la' (MonFun.f f))
+monotone-bind-mon f la≤la' =
+ bind-monotone (MonFun.f f) (MonFun.f f) la≤la' (mon-fun-order-refl f)
+
+{-
+-- bind respects monotonicity
+
+monotone-bind : {A B : Predomain} ->
+ {la la' : ⟨ 𕃠A ⟩} ->
+ (f f' : MonFun A (𕃠B)) ->
+ rel (𕃠A) la la' ->
+ rel (arr' A (𕃠B)) f f' ->
+ rel (𕃠B) (bind la (MonFun.f f)) (bind la' (MonFun.f f'))
+monotone-bind {A} {B} {la} {la'} f f' la≤la' f≤f' =
+ {!!}
+
+ where
+
+ monotone-ext' :
+
+ (f f' : MonFun A (𕃠B)) ->
+ (rel (arr' A (𕃠B)) f f') ->
+ â–¹ (
+ (la la' : ⟨ 𕃠A ⟩) ->
+ ord' A (next (ord A)) la la' ->
+ ord' B (next (ord B))
+ (ext' (MonFun.f f) (next (ext (MonFun.f f))) la)
+ (ext' (MonFun.f f') (next (ext (MonFun.f f'))) la')) ->
+ (la la' : ⟨ 𕃠A ⟩) ->
+ ord' A (next (ord A)) la la' ->
+ ord' B (next (ord B))
+ (ext' (MonFun.f f) (next (ext (MonFun.f f))) la)
+ (ext' (MonFun.f f') (next (ext (MonFun.f f'))) la')
+ monotone-ext' f f' f≤f' IH (η x) (η y) x≤y =
+ transport
+ (λ i → unfold-ord B i (MonFun.f f x) (MonFun.f f' y))
+ (f≤f' x y x≤y)
+ monotone-ext' f f' f≤f' IH ℧ la' la≤la' = tt
+ monotone-ext' f f' f≤f' IH (θ lx~) (θ ly~) la≤la' = λ t ->
+ transport
+ (λ i → (sym (unfold-ord B)) i
+ (sym (unfold-ext (MonFun.f f)) i (lx~ t))
+ (sym (unfold-ext (MonFun.f f')) i (ly~ t)))
+ --(ext (MonFun.f f) (lx~ t))
+ --(ext (MonFun.f f') (ly~ t)))
+ (IH t (lx~ t) (ly~ t)
+ (transport (λ i -> unfold-ord A i (lx~ t) (ly~ t)) (la≤la' t)))
+ -- (IH t (θ lx~) {!θ ly~!} la≤la')
+-}
+-- unfold-ord : ord ≡ ord' (next ord)
+
+
+
+-- For the η case:
+-- Goal:
+-- ord' B (λ _ → fix (ord' B)) (MonFun.f f x) (MonFun.f f' y)
+
+-- Know: (x₠y₠: fst A) →
+-- rel A x₠y₠→
+-- fix (ord' B) (MonFun.f f xâ‚) (MonFun.f f' yâ‚)
+
+
+-- For the θ case:
+-- Goal:
+-- ord B
+-- ext (MonFun.f f)) (lx~ t)
+-- ext (MonFun.f f')) (ly~ t)
+
+-- Know: IH : ...
+-- la≤la' : (tâ‚ : Tick k) → fix (ord' A) (lx~ tâ‚) (ly~ tâ‚)
+
+-- The IH is in terms of ord' (i.e., ord' A (next (ord A)) la la')
+-- but the assumption la ≤ la' in the θ case is equivalent to
+-- (tâ‚ : Tick k) → fix (ord' A) (lx~ tâ‚) (ly~ tâ‚)
+
+
diff --git a/formalizations/guarded-cubical/Semantics/Monotone/MonFunCombinators.agda b/formalizations/guarded-cubical/Semantics/Monotone/MonFunCombinators.agda
new file mode 100644
index 0000000..c019add
--- /dev/null
+++ b/formalizations/guarded-cubical/Semantics/Monotone/MonFunCombinators.agda
@@ -0,0 +1,417 @@
+{-# OPTIONS --cubical --rewriting --guarded #-}
+
+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+open import Common.Later
+
+module Semantics.Monotone.MonFunCombinators (k : Clock) where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Nat renaming (â„• to Nat)
+
+open import Cubical.Relation.Binary
+open import Cubical.Relation.Binary.Poset
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Transport
+
+open import Cubical.Data.Unit
+-- open import Cubical.Data.Prod
+open import Cubical.Data.Sigma
+open import Cubical.Data.Empty
+
+open import Cubical.Foundations.Function
+
+open import Common.Common
+
+open import Semantics.Lift k
+open import Semantics.Predomains
+open import Semantics.Monotone.Base
+open import Semantics.Monotone.Lemmas k
+
+open import Semantics.StrongBisimulation k
+
+
+private
+ variable
+ l : Level
+ A B : Set l
+private
+ ▹_ : Set l → Set l
+ â–¹_ A = â–¹_,_ k A
+
+open MonFun
+
+open LiftPredomain
+
+-- abstract
+
+-- Composing monotone functions
+mCompU : {A B C : Predomain} -> MonFun B C -> MonFun A B -> MonFun A C
+mCompU f1 f2 = record {
+ f = λ a -> f1 .f (f2 .f a) ;
+ isMon = λ x≤y -> f1 .isMon (f2 .isMon x≤y) }
+ where open MonFun
+
+mComp : {A B C : Predomain} ->
+ -- MonFun (arr' B C) (arr' (arr' A B) (arr' A C))
+ ⟨ (B ==> C) ==> (A ==> B) ==> (A ==> C) ⟩
+mComp = record {
+ f = λ fBC →
+ record {
+ f = λ fAB → mCompU fBC fAB ;
+ isMon = λ {f1} {f2} f1≤f2 ->
+ λ a1 a2 a1≤a2 → MonFun.isMon fBC (f1≤f2 a1 a2 a1≤a2) } ;
+ isMon = λ {f1} {f2} f1≤f2 →
+ λ fAB1 fAB2 fAB1≤fAB2 →
+ λ a1 a2 a1≤a2 ->
+ f1≤f2 (MonFun.f fAB1 a1) (MonFun.f fAB2 a2)
+ (fAB1≤fAB2 a1 a2 a1≤a2) }
+
+
+
+ -- ð•ƒ's return as a monotone function
+mRet : {A : Predomain} -> ⟨ A ==> 𕃠A ⟩
+mRet {A} = record { f = ret ; isMon = ord-η-monotone A }
+
+
+ -- Delay as a monotone function
+Δ : {A : Predomain} -> ⟨ 𕃠A ==> 𕃠A ⟩
+Δ {A} = record { f = δ ; isMon = λ x≤y → ord-δ-monotone A x≤y }
+
+ -- Lifting a monotone function functorially
+_~->_ : {A B C D : Predomain} ->
+ ⟨ A ==> B ⟩ -> ⟨ C ==> D ⟩ -> ⟨ (B ==> C) ==> (A ==> D) ⟩
+pre ~-> post = {!!}
+ -- λ f -> mCompU post (mCompU f pre)
+
+
+ -- Extending a monotone function to ð•ƒ
+mExtU : {A B : Predomain} -> MonFun A (𕃠B) -> MonFun (𕃠A) (𕃠B)
+mExtU f = record {
+ f = λ la -> bind la (MonFun.f f) ;
+ isMon = monotone-bind-mon f }
+
+mExt : {A B : Predomain} -> ⟨ (A ==> 𕃠B) ==> (𕃠A ==> 𕃠B) ⟩
+mExt = record {
+ f = mExtU ;
+ isMon = λ {f1} {f2} f1≤f2 -> ext-monotone (MonFun.f f1) (MonFun.f f2) f1≤f2 }
+
+ -- mBind : ⟨ 𕃠A ==> (A ==> 𕃠B) ==> 𕃠B ⟩
+
+ -- Monotone successor function
+mSuc : ⟨ ℕ ==> ℕ ⟩
+mSuc = record {
+ f = suc ;
+ isMon = λ {n1} {n2} n1≤n2 -> λ i -> suc (n1≤n2 i) }
+
+
+ -- Combinators
+
+U : {A B : Predomain} -> ⟨ A ==> B ⟩ -> ⟨ A ⟩ -> ⟨ B ⟩
+U f = MonFun.f f
+
+_$_ : {A B : Predomain} -> ⟨ A ==> B ⟩ -> ⟨ A ⟩ -> ⟨ B ⟩
+_$_ = U
+
+S : (Γ : Predomain) -> {A B : Predomain} ->
+ ⟨ Γ ×d A ==> B ⟩ -> ⟨ Γ ==> A ⟩ -> ⟨ Γ ==> B ⟩
+S Γ f g =
+ record {
+ f = λ γ -> MonFun.f f (γ , (U g γ)) ;
+ isMon = λ {γ1} {γ2} γ1≤γ2 ->
+ MonFun.isMon f (γ1≤γ2 , (MonFun.isMon g γ1≤γ2)) }
+
+ {- λ {γ1} {γ2} γ1≤γ2 →
+ let fγ1≤fγ2 = MonFun.isMon f γ1≤γ2 in
+ fγ1≤fγ2 (MonFun.f g γ1) (MonFun.f g γ2) (MonFun.isMon g γ1≤γ2) } -}
+
+
+_!_<*>_ : {A B : Predomain} ->
+ (Γ : Predomain) -> ⟨ Γ ×d A ==> B ⟩ -> ⟨ Γ ==> A ⟩ -> ⟨ Γ ==> B ⟩
+Γ ! f <*> g = S Γ f g
+
+infixl 20 _<*>_
+
+
+K : (Γ : Predomain) -> {A : Predomain} -> ⟨ A ⟩ -> ⟨ Γ ==> A ⟩
+K _ {A} = λ a → record {
+ f = λ γ → a ;
+ isMon = λ {a1} {a2} a1≤a2 → reflexive A a }
+
+
+Id : {A : Predomain} -> ⟨ A ==> A ⟩
+Id = record { f = id ; isMon = λ x≤y → x≤y }
+
+
+Curry : {Γ A B : Predomain} -> ⟨ (Γ ×d A) ==> B ⟩ -> ⟨ Γ ==> A ==> B ⟩
+Curry {Γ} g = record {
+ f = λ γ →
+ record {
+ f = λ a → MonFun.f g (γ , a) ;
+ -- For a fixed γ, f as defined directly above is monotone
+ isMon = λ {a} {a'} a≤a' → MonFun.isMon g (reflexive Γ _ , a≤a') } ;
+
+ -- The outer f is monotone in γ
+ isMon = λ {γ} {γ'} γ≤γ' → λ a a' a≤a' -> MonFun.isMon g (γ≤γ' , a≤a') }
+
+Uncurry : {Γ A B : Predomain} -> ⟨ Γ ==> A ==> B ⟩ -> ⟨ (Γ ×d A) ==> B ⟩
+Uncurry f = record {
+ f = λ (γ , a) → MonFun.f (MonFun.f f γ) a ;
+ isMon = λ {(γ1 , a1)} {(γ2 , a2)} (γ1≤γ2 , a1≤a2) ->
+ let fγ1≤fγ2 = MonFun.isMon f γ1≤γ2 in
+ fγ1≤fγ2 a1 a2 a1≤a2 }
+
+
+App : {A B : Predomain} -> ⟨ ((A ==> B) ×d A) ==> B ⟩
+App = Uncurry Id
+
+
+Swap : (Γ : Predomain) -> {A B : Predomain} -> ⟨ Γ ==> A ==> B ⟩ -> ⟨ A ==> Γ ==> B ⟩
+Swap Γ f = record {
+ f = λ a →
+ record {
+ f = λ γ → MonFun.f (MonFun.f f γ) a ;
+ isMon = λ {γ1} {γ2} γ1≤γ2 ->
+ let fγ1≤fγ2 = MonFun.isMon f γ1≤γ2 in
+ fγ1≤fγ2 a a (reflexive _ a) } ;
+ isMon = λ {a1} {a2} a1≤a2 ->
+ λ γ1 γ2 γ1≤γ2 -> {!!} } -- γ1 γ2 γ1≤γ2 → {!!} }
+
+
+SwapPair : {A B : Predomain} -> ⟨ (A ×d B) ==> (B ×d A) ⟩
+SwapPair = record {
+ f = λ { (a , b) -> b , a } ;
+ isMon = λ { {a1 , b1} {a2 , b2} (a1≤a2 , b1≤b2) → b1≤b2 , a1≤a2} }
+
+
+-- Apply a monotone function to the first or second argument of a pair
+
+With1st : {Γ A B : Predomain} ->
+ ⟨ Γ ==> B ⟩ -> ⟨ Γ ×d A ==> B ⟩
+-- ArgIntro1 {_} {A} f = Uncurry (Swap A (K A f))
+With1st {_} {A} f = mCompU f π1
+
+With2nd : {Γ A B : Predomain} ->
+ ⟨ A ==> B ⟩ -> ⟨ Γ ×d A ==> B ⟩
+With2nd f = mCompU f π2
+-- ArgIntro2 {Γ} f = Uncurry (K Γ f)
+
+{-
+Cong2nd : {Γ A A' B : Predomain} ->
+ ⟨ Γ ×d A ==> B ⟩ -> ⟨ A' ==> A ⟩ -> ⟨ Γ ×d A' ==> B ⟩
+Cong2nd = {!!}
+-}
+
+
+
+IntroArg' : {Γ B B' : Predomain} ->
+ ⟨ Γ ==> B ⟩ -> ⟨ B ==> B' ⟩ -> ⟨ Γ ==> B' ⟩
+IntroArg' {Γ} {B} {B'} fΓB fBB' = S Γ (With2nd fBB') fΓB
+-- S : ⟨ Γ ×d A ==> B ⟩ -> ⟨ Γ ==> A ⟩ -> ⟨ Γ ==> B ⟩
+
+IntroArg : {Γ B B' : Predomain} ->
+ ⟨ B ==> B' ⟩ -> ⟨ (Γ ==> B) ==> (Γ ==> B') ⟩
+IntroArg f = Curry (mCompU f App)
+
+
+PairAssocLR : {A B C : Predomain} ->
+ ⟨ A ×d B ×d C ==> A ×d (B ×d C) ⟩
+PairAssocLR = record {
+ f = λ { ((a , b) , c) → a , (b , c) } ;
+ isMon = λ { {(a1 , b1) , c1} {(a2 , b2) , c2} ((a1≤a2 , b1≤b2) , c1≤c2) →
+ a1≤a2 , (b1≤b2 , c1≤c2)} }
+
+PairAssocRL : {A B C : Predomain} ->
+ ⟨ A ×d (B ×d C) ==> A ×d B ×d C ⟩
+PairAssocRL = record {
+ f = λ { (a , (b , c)) -> (a , b) , c } ;
+ isMon = λ { {a1 , (b1 , c1)} {a2 , (b2 , c2)} (a1≤a2 , (b1≤b2 , c1≤c2)) →
+ (a1≤a2 , b1≤b2) , c1≤c2} }
+
+PairCong : {Γ A A' : Predomain} ->
+ ⟨ A ==> A' ⟩ -> ⟨ (Γ ×d A) ==> (Γ ×d A') ⟩
+PairCong f = record {
+ f = λ { (γ , a) → γ , (f $ a)} ;
+ isMon = λ { {γ1 , a1} {γ2 , a2} (γ1≤γ2 , a1≤a2) → γ1≤γ2 , isMon f a1≤a2 }}
+
+{-
+PairCong : {Γ A A' : Predomain} ->
+ ⟨ A ==> A' ⟩ -> ⟨ (Γ ×d A) ==> (Γ ×d A') ⟩
+PairCong f = Uncurry (mCompU {!!} {!!})
+-- Goal:
+-- Γ ==> (A ==> Γ ×d A')
+-- Write it as : Γ ==> (A ==> (A' ==> Γ ×d A'))
+-- i.e. Γ ==> A' ==> Γ ×d A'
+-- Pair : ⟨ A ==> B ==> A ×d B ⟩
+-}
+
+TransformDomain : {Γ A A' B : Predomain} ->
+ ⟨ Γ ×d A ==> B ⟩ ->
+ ⟨ ( A ==> B ) ==> ( A' ==> B ) ⟩ ->
+ ⟨ Γ ×d A' ==> B ⟩
+TransformDomain fΓ×A->B f = Uncurry (IntroArg' (Curry fΓ×A->B) f)
+
+
+
+ -- Convenience versions of comp, ext, and ret using combinators
+
+mComp' : (Γ : Predomain) -> {A B C : Predomain} ->
+ ⟨ (Γ ×d B ==> C) ⟩ -> ⟨ (Γ ×d A ==> B) ⟩ -> ⟨ (Γ ×d A ==> C) ⟩
+mComp' Γ {A} {B} {C} f g = S {!!} (mCompU f aux) g
+ where
+ aux : ⟨ Γ ×d A ×d B ==> Γ ×d B ⟩
+ aux = mCompU π1 (mCompU (mCompU PairAssocRL (PairCong SwapPair)) PairAssocLR)
+
+ aux2 : ⟨ Γ ×d B ==> C ⟩ -> ⟨ Γ ×d A ×d B ==> C ⟩
+ aux2 h = mCompU f aux
+
+
+_∘m_ : {Γ A B C : Predomain} ->
+ ⟨ (Γ ×d B ==> C) ⟩ -> ⟨ (Γ ×d A ==> B) ⟩ -> ⟨ (Γ ×d A ==> C) ⟩
+_∘m_ {Γ} = mComp' Γ
+
+_$_∘m_ : (Γ : Predomain) -> {A B C : Predomain} ->
+ ⟨ (Γ ×d B ==> C) ⟩ -> ⟨ (Γ ×d A ==> B) ⟩ -> ⟨ (Γ ×d A ==> C) ⟩
+Γ $ f ∘m g = mComp' Γ f g
+infixl 20 _∘m_
+
+
+mExt' : (Γ : Predomain) -> {A B : Predomain} ->
+ ⟨ (Γ ×d A ==> 𕃠B) ⟩ -> ⟨ (Γ ×d 𕃠A ==> 𕃠B) ⟩
+mExt' Γ f = TransformDomain f mExt
+
+mRet' : (Γ : Predomain) -> { A : Predomain} -> ⟨ Γ ==> A ⟩ -> ⟨ Γ ==> 𕃠A ⟩
+mRet' Γ a = {!!} -- _ ! K _ mRet <*> a
+
+Bind : (Γ : Predomain) -> {A B : Predomain} ->
+ ⟨ Γ ==> 𕃠A ⟩ -> ⟨ Γ ×d A ==> 𕃠B ⟩ -> ⟨ Γ ==> 𕃠B ⟩
+Bind Γ la f = S Γ (mExt' Γ f) la
+
+Comp : (Γ : Predomain) -> {A B C : Predomain} ->
+ ⟨ Γ ×d B ==> C ⟩ -> ⟨ Γ ×d A ==> B ⟩ -> ⟨ Γ ×d A ==> C ⟩
+Comp Γ f g = {!!}
+
+
+
+
+
+-- Mapping a monotone function
+mMap : {A B : Predomain} -> ⟨ (A ==> B) ==> (𕃠A ==> 𕃠B) ⟩
+mMap {A} {B} = Curry (mExt' (A ==> B) ((With2nd mRet) ∘m App))
+-- Curry (mExt' {!!} {!!}) -- mExt' (mComp' (Curry {!!}) {!!}) -- mExt (mComp mRet f)
+
+
+mMap' : {Γ A B : Predomain} ->
+ ⟨ (Γ ×d A ==> B) ⟩ -> ⟨ (Γ ×d 𕃠A ==> 𕃠B) ⟩
+mMap' f = {!!}
+
+Map : {Γ A B : Predomain} ->
+ ⟨ (Γ ×d A ==> B) ⟩ -> ⟨ (Γ ==> 𕃠A) ⟩ -> ⟨ (Γ ==> 𕃠B) ⟩
+Map {Γ} f la = S Γ (mMap' f) la -- Γ ! mMap' f <*> la
+
+
+ {-
+ -- Montone function between function spaces
+ mFun : {A A' B B' : Predomain} ->
+ MonFun A' A ->
+ MonFun B B' ->
+ MonFun (arr' A B) (arr' A' B')
+ mFun fA'A fBB' = record {
+ f = λ fAB → {!!} ; -- mComp (mComp fBB' fAB) fA'A ;
+ isMon = λ {fAB-1} {fAB-2} fAB-1≤fAB-2 →
+ λ a'1 a'2 a'1≤a'2 ->
+ MonFun.isMon fBB'
+ (fAB-1≤fAB-2
+ (MonFun.f fA'A a'1)
+ (MonFun.f fA'A a'2)
+ (MonFun.isMon fA'A a'1≤a'2))}
+
+ -- NTS :
+ -- In the space of monotone functions from A' to B', we have
+ -- mComp (mComp fBB' f1) fA'A) ≤ (mComp (mComp fBB' f2) fA'A)
+ -- That is, given a'1 and a'2 of type ⟨ A' ⟩ with a'1 ≤ a'2 we
+ -- need to show that
+ -- (fBB' ∘ fAB-1 ∘ fA'A)(a'1) ≤ (fBB' ∘ fAB-2 ∘ fA'A)(a'2)
+ -- By monotonicity of fBB', STS that
+ -- (fAB-1 ∘ fA'A)(a'1) ≤ (fAB-2 ∘ fA'A)(a'2)
+ -- which follows by assumption that fAB-1 ≤ fAB-2 and monotonicity of fA'A
+ -}
+
+ -- Embedding of function spaces is monotone
+mFunEmb : (A A' B B' : Predomain) ->
+ ⟨ A' ==> 𕃠A ⟩ ->
+ ⟨ B ==> B' ⟩ ->
+ ⟨ (A ==> 𕃠B) ==> (A' ==> 𕃠B') ⟩
+mFunEmb A A' B B' fA'LA fBB' =
+ Curry (Bind ((A ==> 𕃠B) ×d A')
+ (mCompU fA'LA π2)
+ (Map (mCompU fBB' π2) ({!!})))
+ -- _ $ (mExt' _ (_ $ (mMap' (K _ fBB')) ∘m Id)) ∘m (K _ fA'LA)
+ -- mComp' (mExt' (mComp' (mMap' (K fBB')) Id)) (K fA'LA)
+
+mFunProj : (A A' B B' : Predomain) ->
+ ⟨ A ==> A' ⟩ ->
+ ⟨ B' ==> 𕃠B ⟩ ->
+ ⟨ (A' ==> 𕃠B') ==> 𕃠(A ==> 𕃠B) ⟩
+mFunProj A A' B B' fAA' fB'LB = {!!}
+ -- mRet' (mExt' (K fB'LB) ∘m Id ∘m (K fAA'))
+
+ --
+
+ {-
+ record {
+ f = λ f -> {!!} ; -- mComp (mExt (mComp (mMap fBB') f)) fA'LA ;
+ isMon = λ {f1} {f2} f1≤f2 ->
+ λ a'1 a'2 a'1≤a'2 ->
+ ext-monotone
+ (mapL (MonFun.f fBB') ∘ MonFun.f f1)
+ (mapL (MonFun.f fBB') ∘ MonFun.f f2)
+ ({!!})
+ (MonFun.isMon fA'LA a'1≤a'2) }
+ -}
+
+ -- mComp (mExt (mComp (mMap fBB') f1)) fA'LA ≤ mComp (mExt (mComp (mMap fBB') f2)) fA'LA
+ -- ((ext ((mapL fBB') ∘ f1)) ∘ fA'LA) (a'1) ≤ ((ext ((mapL fBB') ∘ f2)) ∘ fA'LA) (a'2)
+
+
+{-
+ -- Properties
+bind-unit-l : {Γ A B : Predomain} ->
+ (f : ⟨ Γ ×d A ==> 𕃠B ⟩) ->
+ (a : ⟨ Γ ==> A ⟩) ->
+ rel (Γ ==> 𕃠B)
+ (Bind Γ (mRet' Γ a) f)
+ (Γ ! f <*> a)
+bind-unit-l = {!!}
+
+bind-unit-r : {Γ A B : Predomain} ->
+ (la : ⟨ Γ ==> 𕃠A ⟩) ->
+ rel (Γ ==> 𕃠A)
+ la
+ (Bind Γ la (mRet' _ π2))
+bind-unit-r la = {!!}
+
+
+bind-Ret' : {Γ A : Predomain} ->
+ (la : ⟨ Γ ==> 𕃠A ⟩) ->
+ (a : ⟨ Γ ×d A ==> A ⟩) ->
+ rel (Γ ==> 𕃠A)
+ la
+ (Bind Γ la ((mRet' _ a)))
+bind-Ret' = {!!}
+
+
+bind-K : {Γ A B : Predomain} ->
+ (la : ⟨ Γ ==> 𕃠A ⟩) ->
+ (lb : ⟨ 𕃠B ⟩) ->
+ rel (Γ ==> 𕃠B)
+ (K Γ lb)
+ (Bind Γ la ((K (Γ ×d A) lb)))
+bind-K = {!!}
+
+ {- Goal: rel (⟦ Γ ⟧ctx ==> 𕃠⟦ B ⟧ty) ⟦ err [ N ] ⟧tm
+ (Bind ⟦ Γ ⟧ctx ⟦ N ⟧tm (Curry ⟦ err ⟧tm))
+ -}
+
+-}
diff --git a/formalizations/guarded-cubical/Semantics/Predomains.agda b/formalizations/guarded-cubical/Semantics/Predomains.agda
new file mode 100644
index 0000000..316544e
--- /dev/null
+++ b/formalizations/guarded-cubical/Semantics/Predomains.agda
@@ -0,0 +1,84 @@
+{-# OPTIONS --cubical --rewriting --guarded #-}
+
+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+module Semantics.Predomains where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.Relation.Binary
+open import Cubical.Relation.Binary.Poset
+
+open import Common.Later
+
+-- Define predomains as posets
+Predomain : Setâ‚
+Predomain = Poset â„“-zero â„“-zero
+
+
+-- The relation associated to a predomain d
+rel : (d : Predomain) -> (⟨ d ⟩ -> ⟨ d ⟩ -> Type)
+rel d = PosetStr._≤_ (d .snd)
+
+reflexive : (d : Predomain) -> (x : ⟨ d ⟩) -> (rel d x x)
+reflexive d x = IsPoset.is-refl (PosetStr.isPoset (str d)) x
+
+transitive : (d : Predomain) -> (x y z : ⟨ d ⟩) ->
+ rel d x y -> rel d y z -> rel d x z
+transitive d x y z x≤y y≤z =
+ IsPoset.is-trans (PosetStr.isPoset (str d)) x y z x≤y y≤z
+
+
+
+-- Theta for predomains
+
+module _ (k : Clock) where
+
+ private
+ variable
+ l : Level
+
+ ▹_ : Set l → Set l
+ â–¹_ A = â–¹_,_ k A
+
+
+
+ isSet-poset : {ℓ ℓ' : Level} -> (P : Poset ℓ ℓ') -> isSet ⟨ P ⟩
+ isSet-poset P = IsPoset.is-set (PosetStr.isPoset (str P))
+
+
+ ▸' : ▹ Predomain → Predomain
+ ▸' X = (▸ (λ t → ⟨ X t ⟩)) ,
+ posetstr ord
+ (isposet isset-later {!!} ord-refl ord-trans ord-antisym)
+ where
+
+ ord : ▸ (λ t → ⟨ X t ⟩) → ▸ (λ t → ⟨ X t ⟩) → Type ℓ-zero
+ -- ord x1~ x2~ = ▸ (λ t → (str (X t) PosetStr.≤ (x1~ t)) (x2~ t))
+ ord x1~ x2~ = ▸ (λ t → (PosetStr._≤_ (str (X t)) (x1~ t)) (x2~ t))
+
+
+ isset-later : isSet (▸ (λ t → ⟨ X t ⟩))
+ isset-later = λ x y p1 p2 i j t →
+ isSet-poset (X t) (x t) (y t) (λ i' → p1 i' t) (λ i' → p2 i' t) i j
+
+ ord-refl : (a : ▸ (λ t → ⟨ X t ⟩)) -> ord a a
+ ord-refl a = λ t ->
+ IsPoset.is-refl (PosetStr.isPoset (str (X t))) (a t)
+
+ ord-trans : BinaryRelation.isTrans ord
+ ord-trans = λ a b c ord-ab ord-bc t →
+ IsPoset.is-trans
+ (PosetStr.isPoset (str (X t))) (a t) (b t) (c t) (ord-ab t) (ord-bc t)
+
+ ord-antisym : BinaryRelation.isAntisym ord
+ ord-antisym = λ a b ord-ab ord-ba i t ->
+ IsPoset.is-antisym
+ (PosetStr.isPoset (str (X t))) (a t) (b t) (ord-ab t) (ord-ba t) i
+
+
+ -- Delay for predomains
+ ▸''_ : Predomain → Predomain
+ â–¸'' X = â–¸' (next X)
+
diff --git a/formalizations/guarded-cubical/Semantics/Semantics.agda b/formalizations/guarded-cubical/Semantics/Semantics.agda
index f8b1242..ec86c7c 100644
--- a/formalizations/guarded-cubical/Semantics/Semantics.agda
+++ b/formalizations/guarded-cubical/Semantics/Semantics.agda
@@ -28,11 +28,16 @@ open import Cubical.Foundations.Function
open import Common.Common
+open import Semantics.Predomains
+open import Semantics.Lift k
open import Semantics.StrongBisimulation k
open import Syntax.GradualSTLC
-- open import SyntacticTermPrecision k
-open import Common.Lemmas k
-open import Common.MonFuns k
+
+open import Semantics.Monotone.Base
+open import Semantics.Monotone.Lemmas k
+open import Semantics.Monotone.MonFunCombinators k
+
private
variable
diff --git a/formalizations/guarded-cubical/Semantics/StrongBisimulation.agda b/formalizations/guarded-cubical/Semantics/StrongBisimulation.agda
index 0e4b10b..66ce873 100644
--- a/formalizations/guarded-cubical/Semantics/StrongBisimulation.agda
+++ b/formalizations/guarded-cubical/Semantics/StrongBisimulation.agda
@@ -4,6 +4,7 @@
{-# OPTIONS --allow-unsolved-metas #-}
open import Common.Later
+open import Semantics.Monotone.Base
module Semantics.StrongBisimulation(k : Clock) where
@@ -31,6 +32,9 @@ open import Cubical.Data.Unit.Properties
open import Agda.Primitive
open import Common.Common
+open import Semantics.Predomains
+open import Semantics.Lift k
+open import Semantics.ErrorDomains
private
variable
@@ -44,397 +48,6 @@ private
-Predomain' : {â„“ â„“' : Level} -> Type (â„“-max (â„“-suc â„“) (â„“-suc â„“'))
-Predomain' {â„“} {â„“'} = Poset â„“ â„“'
-
--- The relation associated to a predomain d
-rel' : (d : Predomain') -> (⟨ d ⟩ -> ⟨ d ⟩ -> Type)
-rel' d = PosetStr._≤_ (d .snd)
-
-reflexive' : (d : Predomain') -> (x : ⟨ d ⟩) -> (rel' d x x)
-reflexive' d x = IsPoset.is-refl (PosetStr.isPoset (str d)) x
-
-transitive' : (d : Predomain') -> (x y z : ⟨ d ⟩) ->
- rel' d x y -> rel' d y z -> rel' d x z
-transitive' d x y z x≤y y≤z =
- IsPoset.is-trans (PosetStr.isPoset (str d)) x y z x≤y y≤z
-
-test : Predomain' -> Predomain' -> Predomain'
-test A B =
- (Path Predomain' A B) ,
- posetstr (λ p1 p2 → rel' A {!p1 i0!} {!!} × {!!})
- (isposet {!!} {!!} (λ a → {!!}) {!!} {!!})
-
-
-
-
-
-
-
-
-
--- Define predomains as posets
-
-
-Predomain : Setâ‚
-Predomain = Poset â„“-zero â„“-zero
-
-
--- The relation associated to a predomain d
-rel : (d : Predomain) -> (⟨ d ⟩ -> ⟨ d ⟩ -> Type)
-rel d = PosetStr._≤_ (d .snd)
-
-reflexive : (d : Predomain) -> (x : ⟨ d ⟩) -> (rel d x x)
-reflexive d x = IsPoset.is-refl (PosetStr.isPoset (str d)) x
-
-transitive : (d : Predomain) -> (x y z : ⟨ d ⟩) ->
- rel d x y -> rel d y z -> rel d x z
-transitive d x y z x≤y y≤z =
- IsPoset.is-trans (PosetStr.isPoset (str d)) x y z x≤y y≤z
-
--- Monotone functions from X to Y
-
-record MonFun (X Y : Predomain) : Set where
- module X = PosetStr (X .snd)
- module Y = PosetStr (Y .snd)
- _≤X_ = X._≤_
- _≤Y_ = Y._≤_
- field
- f : (X .fst) → (Y .fst)
- isMon : ∀ {x y} → x ≤X y → f x ≤Y f y
-
--- Use reflection to show that this is a sigma type
--- Look for proof in standard library to show that
--- Sigma type with a proof that RHS is a prop, then equality of a pair
--- follows from equality of the LHS's
--- Specialize to the case of monotone functions and fill in the proof
--- later
-
-
--- Monotone relations between predomains X and Y
--- (antitone in X, monotone in Y).
-record MonRel {â„“' : Level} (X Y : Predomain) : Type (â„“-suc â„“') where
- module X = PosetStr (X .snd)
- module Y = PosetStr (Y .snd)
- _≤X_ = X._≤_
- _≤Y_ = Y._≤_
- field
- R : ⟨ X ⟩ -> ⟨ Y ⟩ -> Type ℓ'
- isAntitone : ∀ {x x' y} -> R x y -> x' ≤X x -> R x' y
- isMonotone : ∀ {x y y'} -> R x y -> y ≤Y y' -> R x y'
-
-predomain-monrel : (X : Predomain) -> MonRel X X
-predomain-monrel X = record {
- R = rel X ;
- isAntitone = λ {x} {x'} {y} x≤y x'≤x → transitive X x' x y x'≤x x≤y ;
- isMonotone = λ {x} {y} {y'} x≤y y≤y' -> transitive X x y y' x≤y y≤y' }
-
-
-compRel : {X Y Z : Type} ->
- (R1 : Y -> Z -> Type â„“) ->
- (R2 : X -> Y -> Type â„“) ->
- (X -> Z -> Type â„“)
-compRel {ℓ} {X} {Y} {Z} R1 R2 x z = Σ[ y ∈ Y ] R2 x y × R1 y z
-
-CompMonRel : {X Y Z : Predomain} ->
- MonRel {â„“} Y Z ->
- MonRel {â„“} X Y ->
- MonRel {â„“} X Z
-CompMonRel {â„“} {X} {Y} {Z} R1 R2 = record {
- R = compRel (MonRel.R R1) (MonRel.R R2) ;
- isAntitone = antitone ;
- isMonotone = {!!} }
- where
- antitone : {x x' : ⟨ X ⟩} {z : ⟨ Z ⟩} ->
- compRel (MonRel.R R1) (MonRel.R R2) x z ->
- rel X x' x ->
- compRel (MonRel.R R1) (MonRel.R R2) x' z
- antitone (y , xR2y , yR1z) x'≤x = y , (MonRel.isAntitone R2 xR2y x'≤x) , yR1z
-
- monotone : {x : ⟨ X ⟩} {z z' : ⟨ Z ⟩} ->
- compRel (MonRel.R R1) (MonRel.R R2) x z ->
- rel Z z z' ->
- compRel (MonRel.R R1) (MonRel.R R2) x z'
- monotone (y , xR2y , yR1z) z≤z' = y , xR2y , (MonRel.isMonotone R1 yR1z z≤z')
-
-
-{-
-record IsMonFun {X Y : Predomain} (f : ⟨ X ⟩ → ⟨ Y ⟩) : Type (ℓ-max ℓ ℓ') where
- no-eta-equality
- constructor ismonfun
-
- module X = PosetStr (X .snd)
- module Y = PosetStr (Y .snd)
- _≤X_ = X._≤_
- _≤Y_ = Y._≤_
-
- field
- isMon : ∀ {x y} → x ≤X y → f x ≤Y f y
-
-record MonFunStr (â„“' : Level) (X Y : Predomain) : Type (â„“-max â„“ (â„“-suc â„“')) where
-
- constructor monfunstr
-
- field
- f : ⟨ X ⟩ -> ⟨ Y ⟩
- isMonFun : IsMonFun {â„“'} f
-
- open IsMonFun isMonFun public
-
-MonF : ∀ ℓ ℓ' -> Predomain -> Predomain -> Type (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ'))
-MonF â„“ â„“' X Y = TypeWithStr â„“ {!!}
--}
-
-{-
-lem-later : {X~ : â–¹ Type} ->
- (x~ y~ : ▸ X~) -> (x~ ≡ y~) ≡ ( ▸ λ t -> ( x~ t ≡ y~ t ))
-lem-later = ?
--}
-
-
-isSet-poset : {ℓ ℓ' : Level} -> (P : Poset ℓ ℓ') -> isSet ⟨ P ⟩
-isSet-poset P = IsPoset.is-set (PosetStr.isPoset (str P))
-
-
--- Theta for predomains
-
-▸' : ▹ Predomain → Predomain
-▸' X = (▸ (λ t → ⟨ X t ⟩)) ,
- posetstr ord
- (isposet isset-later {!!} ord-refl ord-trans ord-antisym)
- where
-
- ord : ▸ (λ t → ⟨ X t ⟩) → ▸ (λ t → ⟨ X t ⟩) → Type ℓ-zero
- -- ord x1~ x2~ = ▸ (λ t → (str (X t) PosetStr.≤ (x1~ t)) (x2~ t))
- ord x1~ x2~ = ▸ (λ t → (PosetStr._≤_ (str (X t)) (x1~ t)) (x2~ t))
-
-
- isset-later : isSet (▸ (λ t → ⟨ X t ⟩))
- isset-later = λ x y p1 p2 i j t →
- isSet-poset (X t) (x t) (y t) (λ i' → p1 i' t) (λ i' → p2 i' t) i j
-
- ord-refl : (a : ▸ (λ t → ⟨ X t ⟩)) -> ord a a
- ord-refl a = λ t ->
- IsPoset.is-refl (PosetStr.isPoset (str (X t))) (a t)
-
- ord-trans : BinaryRelation.isTrans ord
- ord-trans = λ a b c ord-ab ord-bc t →
- IsPoset.is-trans
- (PosetStr.isPoset (str (X t))) (a t) (b t) (c t) (ord-ab t) (ord-bc t)
-
- ord-antisym : BinaryRelation.isAntisym ord
- ord-antisym = λ a b ord-ab ord-ba i t ->
- IsPoset.is-antisym
- (PosetStr.isPoset (str (X t))) (a t) (b t) (ord-ab t) (ord-ba t) i
-
-
--- Delay for predomains
-▸''_ : Predomain → Predomain
-â–¸'' X = â–¸' (next X)
-
-
--- Error domains
-
-record ErrorDomain : Setâ‚ where
- field
- X : Predomain
- module X = PosetStr (X .snd)
- _≤_ = X._≤_
- field
- ℧ : X .fst
- ℧⊥ : ∀ x → ℧ ≤ x
- θ : MonFun (▸'' X) X
-
-
--- Lift monad
-
-data L℧ (X : Set) : Set where
- η : X → L℧ X
- ℧ : L℧ X
- θ : ▹ (L℧ X) → L℧ X
-
--- Similar to caseNat,
--- defined at https://agda.github.io/cubical/Cubical.Data.Nat.Base.html#487
-caseL℧ : {X : Set} -> {ℓ : Level} -> {A : Type ℓ} ->
- (aη a℧ aθ : A) → (L℧ X) → A
-caseL℧ aη a℧ aθ (η x) = aη
-caseL℧ aη a℧ aθ ℧ = a℧
-caseL℧ a0 a℧ aθ (θ lx~) = aθ
-
--- Similar to znots and snotz, defined at
--- https://agda.github.io/cubical/Cubical.Data.Nat.Properties.html
-℧≠θ : {X : Set} -> {lx~ : ▹ (L℧ X)} -> ¬ (℧ ≡ θ lx~)
-℧≠θ {X} {lx~} eq = subst (caseL℧ X (L℧ X) ⊥) eq ℧
-
-θ≠℧ : {X : Set} -> {lx~ : ▹ (L℧ X)} -> ¬ (θ lx~ ≡ ℧)
-θ≠℧ {X} {lx~} eq = subst (caseL℧ X ⊥ (L℧ X)) eq (θ lx~)
-
-
--- Does this make sense?
-pred : {X : Set} -> (lx : L℧ X) -> ▹ (L℧ X)
-pred (η x) = next ℧
-pred ℧ = next ℧
-pred (θ lx~) = lx~
-
-pred-def : {X : Set} -> (def : ▹ (L℧ X)) -> (lx : L℧ X) -> ▹ (L℧ X)
-pred-def def (η x) = def
-pred-def def ℧ = def
-pred-def def (θ lx~) = lx~
-
-
--- Uses the pred function above, and I'm not sure whether that
--- function makes sense.
-inj-θ : {X : Set} -> (lx~ ly~ : ▹ (L℧ X)) ->
- θ lx~ ≡ θ ly~ ->
- ▸ (λ t -> lx~ t ≡ ly~ t)
-inj-θ lx~ ly~ H = let lx~≡ly~ = cong pred H in
- λ t i → lx~≡ly~ i t
-
-
-
-ret : {X : Set} -> X -> L℧ X
-ret = η
-
-{-
-bind' : ∀ {A B} -> (A -> L℧ B) -> ▹ (L℧ A -> L℧ B) -> L℧ A -> L℧ B
-bind' f bind_rec (η x) = f x
-bind' f bind_rec ℧ = ℧
-bind' f bind_rec (θ l_la) = θ (bind_rec ⊛ l_la)
-
--- fix : ∀ {l} {A : Set l} → (f : ▹ k , A → A) → A
-bind : L℧ A -> (A -> L℧ B) -> L℧ B
-bind {A} {B} la f = (fix (bind' f)) la
-
-ext : (A -> L℧ B) -> L℧ A -> L℧ B
-ext f la = bind la f
--}
-
-ext' : (A -> L℧ B) -> ▹ (L℧ A -> L℧ B) -> L℧ A -> L℧ B
-ext' f rec (η x) = f x
-ext' f rec ℧ = ℧
-ext' f rec (θ l-la) = θ (rec ⊛ l-la)
-
-ext : (A -> L℧ B) -> L℧ A -> L℧ B
-ext f = fix (ext' f)
-
-
-bind : L℧ A -> (A -> L℧ B) -> L℧ B
-bind {A} {B} la f = ext f la
-
-mapL : (A -> B) -> L℧ A -> L℧ B
-mapL f la = bind la (λ a -> ret (f a))
-
-unfold-ext : (f : A -> L℧ B) -> ext f ≡ ext' f (next (ext f))
-unfold-ext f = fix-eq (ext' f)
-
-
-ext-eta : ∀ (a : A) (f : A -> L℧ B) ->
- ext f (η a) ≡ f a
-ext-eta a f =
- fix (ext' f) (ret a) ≡⟨ (λ i → unfold-ext f i (ret a)) ⟩
- (ext' f) (next (ext f)) (ret a) ≡⟨ refl ⟩
- f a ∎
-
-ext-err : (f : A -> L℧ B) ->
- bind ℧ f ≡ ℧
-ext-err f =
- fix (ext' f) ℧ ≡⟨ (λ i → unfold-ext f i ℧) ⟩
- (ext' f) (next (ext f)) ℧ ≡⟨ refl ⟩
- ℧ ∎
-
-
-ext-theta : (f : A -> L℧ B)
- (l : ▹ (L℧ A)) ->
- bind (θ l) f ≡ θ (ext f <$> l)
-ext-theta f l =
- (fix (ext' f)) (θ l) ≡⟨ (λ i → unfold-ext f i (θ l)) ⟩
- (ext' f) (next (ext f)) (θ l) ≡⟨ refl ⟩
- θ (fix (ext' f) <$> l) ∎
-
-
-
-mapL-eta : (f : A -> B) (a : A) ->
- mapL f (η a) ≡ η (f a)
-mapL-eta f a = ext-eta a λ a → ret (f a)
-
-mapL-theta : (f : A -> B) (la~ : ▹ (L℧ A)) ->
- mapL f (θ la~) ≡ θ (mapL f <$> la~)
-mapL-theta f la~ = ext-theta (ret ∘ f) la~
-
-
--- Strong bisimulation relation/ordering for the lift monad
-
-{-
-U : Predomain -> Type
-U p = ⟨ p ⟩
--}
-
-{-
-module LiftOrder (p : Predomain) where
-
- module X = PosetStr (p .snd)
- open X using (_≤_)
- -- _≤_ = X._≤_
-
- module Inductive (rec : ▹ (L℧ (U p) -> L℧ (U p) -> Type)) where
-
- _≾'_ : L℧ (U p) -> L℧ (U p) -> Type
- ℧ ≾' _ = Unit
- η x ≾' η y = x ≤ y
- θ lx ≾' θ ly = ▸ (λ t -> rec t (lx t) (ly t))
- η _ ≾' _ = ⊥
- θ _ ≾' _ = ⊥
-
- open Inductive
- _≾_ : L℧ (U p) -> L℧ (U p) -> Type
- _≾_ = fix _≾'_
-
- ≾-refl : BinaryRelation.isRefl _≾_
-
- ≾-refl' : ▹ (BinaryRelation.isRefl _≾_) ->
- BinaryRelation.isRefl _≾_
- ≾-refl' IH (η x) =
- transport (sym (λ i -> fix-eq _≾'_ i (η x) (η x)))
- (IsPoset.is-refl (X.isPoset) x)
- ≾-refl' IH ℧ =
- transport (sym (λ i -> fix-eq _≾'_ i ℧ ℧))
- tt
- ≾-refl' IH (θ lx~) =
- transport (sym (λ i -> fix-eq _≾'_ i (θ lx~) (θ lx~)))
- λ t → IH t (lx~ t)
-
- ≾-refl = fix ≾-refl'
-
-
- ℧-bot : (l : L℧ (U p)) -> ℧ ≾ l
- ℧-bot l = transport (sym λ i → fix-eq _≾'_ i ℧ l) tt
-
-
-
--- Predomain to lift predomain
-
-ð•ƒâ„§' : Predomain -> Predomain
-ð•ƒâ„§' X = L℧ (X .fst) ,
- posetstr (LiftOrder._≾_ X)
- (isposet {!!} {!!} ≾-refl {!!} {!!})
- where open LiftOrder X
-
-
--- Predomain to lift Error Domain
-
-ð•ƒâ„§ : Predomain → ErrorDomain
-ð•ƒâ„§ X = record {
- X = ð•ƒâ„§' X ; ℧ = ℧ ; ℧⊥ = ℧-bot ;
- θ = record { f = θ ; isMon = λ t -> {!!} } }
- where
- -- module X = PosetStr (X .snd)
- -- open Relation X
- open LiftOrder X
-
-𕌠: ErrorDomain -> Predomain
-𕌠d = ErrorDomain.X d
--}
-
-- Flat predomain from a set
@@ -455,17 +68,9 @@ UnitP : Predomain
UnitP = flat (Unit , isSetUnit)
--- Underlying predomain of an error domain
-
-𕌠: ErrorDomain -> Predomain
-𕌠d = ErrorDomain.X d
-
-
-- Predomains from arrows (need to ensure monotonicity)
-
-
-- Ordering on functions between predomains. This does not require that the
-- functions are monotone.
fun-order-het : (P1 P1' P2 P2' : Predomain) ->
@@ -478,8 +83,6 @@ fun-order-het P1 P1' P2 P2' rel-P1P1' rel-P2P2' fP1P2 fP1'P2' =
rel-P2P2' (fP1P2 p) (fP1'P2' p')
-
-
-- TODO can define this in terms of fun-order-het
fun-order : (P1 P2 : Predomain) -> (⟨ P1 ⟩ -> ⟨ P2 ⟩) -> (⟨ P1 ⟩ -> ⟨ P2 ⟩) -> Type ℓ-zero
fun-order P1 P2 f1 f2 =
@@ -497,6 +100,7 @@ mon-fun-order-refl : {P1 P2 : Predomain} ->
fun-order P1 P2 f f
mon-fun-order-refl {P1} {P2} f f-mon = λ x y x≤y → f-mon x≤y
-}
+
fun-order-trans : {P1 P2 : Predomain} ->
(f g h : ⟨ P1 ⟩ -> ⟨ P2 ⟩) ->
@@ -534,8 +138,8 @@ mon-fun-order-trans : {P1 P2 : Predomain} ->
mon-fun-order P1 P2 f g ->
mon-fun-order P1 P2 g h ->
mon-fun-order P1 P2 f h
-mon-fun-order-trans f g h f≤g g≤h =
- fun-order-trans (MonFun.f f) (MonFun.f g) (MonFun.f h) f≤g g≤h
+mon-fun-order-trans {P1} {P2} f g h f≤g g≤h =
+ fun-order-trans {P1} {P2} (MonFun.f f) (MonFun.f g) (MonFun.f h) f≤g g≤h
-- Predomain of monotone functions between two predomains
@@ -556,13 +160,9 @@ arr' P1 P2 =
(Hf2-f3 x y H≤xy))
{!!}))
where
- -- Two functions from P1 to P2 are related if, when given inputs
- -- that are related (in P1), the outputs are related (in P2)
open MonFun
module P1 = PosetStr (P1 .snd)
module P2 = PosetStr (P2 .snd)
- _≤P1_ = P1._≤_
- _≤P2_ = P2._≤_
_==>_ : Predomain -> Predomain -> Predomain
@@ -591,32 +191,8 @@ FunRel {A} {A'} {B} {B'} RAA' RBB' =
MonRel.isMonotone RBB' (f≤f' a a' a≤a') {!!} } -- (f'≤g' a' a' (reflexive A' a')) }
-arr : Predomain -> ErrorDomain -> ErrorDomain
-arr dom cod =
- record {
- X = arr' dom (𕌠cod) ;
- ℧ = const-err ;
- ℧⊥ = const-err-bot ;
- θ = {!!} }
- where
- -- open LiftOrder
- const-err : ⟨ arr' dom (𕌠cod) ⟩
- const-err = record {
- f = λ _ -> ErrorDomain.℧ cod ;
- isMon = λ _ -> reflexive (𕌠cod) (ErrorDomain.℧ cod) }
-
- const-err-bot : (f : ⟨ arr' dom (𕌠cod) ⟩) -> rel (arr' dom (𕌠cod)) const-err f
- const-err-bot f = λ x y x≤y → ErrorDomain.℧⊥ cod (MonFun.f f y)
-
-
-
--- Delay function
-δ : {X : Type} -> L℧ X -> L℧ X
-δ = θ ∘ next
- where open L℧
-
-
+
-- Lifting a heterogeneous relation between A and B to a
-- relation between L A and L B
-- (We may be able to reuse this logic to define the homogeneous ordering on 𕃠below)
@@ -671,37 +247,6 @@ module LiftPredomain (p : Predomain) where
module X = PosetStr (p .snd)
open X using (_≤_)
- -- _≤_ = X._≤_
-
- {-
- ord' : ▹ ( L℧ ⟨ p ⟩ → L℧ ⟨ p ⟩ → Type) ->
- L℧ ⟨ p ⟩ → L℧ ⟨ p ⟩ → Type
- ord' _ ℧ _ = Unit
- ord' _ (η x) (η y) = x ≤ y
- ord' _ (η _) _ = ⊥
- ord' rec (θ lx~) (θ ly~) = ▸ (λ t -> (rec t) (lx~ t) (ly~ t))
- -- or: ▸ ((rec ⊛ lx~) ⊛ ly~)
- ord' _ (θ _) _ = ⊥
-
- ord : L℧ ⟨ p ⟩ → L℧ ⟨ p ⟩ → Type
- ord = fix ord'
- -}
-
- -- _≾_ : L℧ ⟨ p ⟩ -> L℧ ⟨ p ⟩ -> Type
- -- _≾_ = LiftRelation._≾_ p p (_≤_)
-
- -- unfold-ord : ord ≡ ord' (next ord)
- -- unfold-ord = fix-eq ord'
-
- {-
- ≈->≈' : {lx ly : L℧ ⟨ d ⟩} ->
- lx ≈ ly -> lx ≈' ly
- ≈->≈' {lx} {ly} lx≈ly = transport (λ i → unfold-≈ i lx ly) lx≈ly
-
- ≈'->≈ : {lx ly : L℧ ⟨ d ⟩} ->
- lx ≈' ly -> lx ≈ ly
- ≈'->≈ {lx} {ly} lx≈'ly = transport (sym (λ i → unfold-≈ i lx ly)) lx≈'ly
- -}
-- Open the more general definitions from the heterogeneous
@@ -714,10 +259,6 @@ module LiftPredomain (p : Predomain) where
open Inductive (next _≾_) public
open Properties public
- {-
- ord-η-monotone : {x y : ⟨ p ⟩} -> x ≤ y -> (η x) ≾ (η y)
- ord-η-monotone {x} {y} x≤y = transport (sym λ i → unfold-≾ i (η x) (η y)) x≤y
- -}
-- TODO move to heterogeneous lifting module
ord-δ-monotone : {lx ly : L℧ ⟨ p ⟩} -> lx ≾ ly -> (δ lx) ≾ (δ ly)
@@ -729,12 +270,6 @@ module LiftPredomain (p : Predomain) where
Inductive._≾'_ (next _≾_) (δ lx) (δ ly)
ord-δ-monotone' {lx} {ly} lx≤ly = λ t → lx≤ly
- {-
- ord-bot : (lx : L℧ ⟨ p ⟩) -> ℧ ≾ lx
- ord-bot lx = transport (sym λ i → unfold-≾ i ℧ lx) tt
- -}
-
- -- lift-ord : (A -> A -> Type) -> (L℧ A -> L℧ A -> Type)
ord-refl-ind : ▹ ((a : L℧ ⟨ p ⟩) -> a ≾ a) ->
(a : L℧ ⟨ p ⟩) -> a ≾ a
@@ -797,7 +332,7 @@ module LiftRelMon
-- Bring the heterogeneous relation between 𕃠A and 𕃠B into scope
open LiftRelation A B (MonRel.R RAB)
using (_≾_ ; module Inductive ; module Properties) -- brings _≾_ into scope
- open Inductive (next _≾_) -- brings _≾'_ into scope
+ open Inductive (next _≾_) -- brings _≾'_ into scope
open Properties -- brings conversion between _≾_ and _≾'_ into scope
-- Bring the homogeneous lifted relations on A and B into scope
@@ -812,47 +347,31 @@ module LiftRelMon
_≾'LA_ = LiftPredomain._≾'_ A
_≾'LB_ = LiftPredomain._≾'_ B
-
R : MonRel (𕃠A) (𕃠B)
R = record {
R = _≾_ ;
- isAntitone = {!!} ;
+ isAntitone = λ {la} {la'} {lb} la≤lb la'≤la -> {!!} ;
isMonotone = {!!} }
-
- antitone' :
- ▹ ({la la' : L℧ ⟨ A ⟩} -> {lb : L℧ ⟨ B ⟩} ->
- la ≾' lb -> la' ≾'LA la -> la' ≾' lb) ->
- {la la' : L℧ ⟨ A ⟩} -> {lb : L℧ ⟨ B ⟩} ->
- la ≾' lb -> la' ≾'LA la -> la' ≾' lb
- antitone' IH {η a2} {η a1} {η a3} la≤lb la'≤la =
- MonRel.isAntitone RAB la≤lb la'≤la
- antitone' IH {la} {℧} {lb} la≤lb la'≤la = tt
- antitone' IH {θ la2~} {θ la1~} {θ lb~} la≤lb la'≤la =
- λ t → ≾'->≾ (IH t (≾->≾' (la≤lb t)) ({!!} ))
-
- monotone : {!!}
- monotone = {!!}
+ where
+ antitone' :
+ ▹ ({la la' : L℧ ⟨ A ⟩} -> {lb : L℧ ⟨ B ⟩} ->
+ la ≾' lb -> la' ≾'LA la -> la' ≾' lb) ->
+ {la la' : L℧ ⟨ A ⟩} -> {lb : L℧ ⟨ B ⟩} ->
+ la ≾' lb -> la' ≾'LA la -> la' ≾' lb
+ antitone' IH {η a2} {η a1} {η a3} la≤lb la'≤la =
+ MonRel.isAntitone RAB la≤lb la'≤la
+ antitone' IH {la} {℧} {lb} la≤lb la'≤la = tt
+ antitone' IH {θ la2~} {θ la1~} {θ lb~} la≤lb la'≤la =
+ λ t → ≾'->≾ (IH t {!!} {!!})
+
+ monotone : {!!}
+ monotone = {!!}
-- isAntitone : ∀ {x x' y} -> R x y -> x' ≤X x -> R x' y
-- isMonotone : ∀ {x y y'} -> R x y -> y ≤Y y' -> R x y'
--- Predomain to lift Error Domain
-
-ð•ƒâ„§ : Predomain → ErrorDomain
-ð•ƒâ„§ X = record {
- X = 𕃠X ; ℧ = ℧ ; ℧⊥ = ord-bot X ;
- θ = record { f = θ ; isMon = λ t -> {!!} } }
- where
- -- module X = PosetStr (X .snd)
- -- open Relation X
- open LiftPredomain
-
-
-
-
-
-- Product of predomains
@@ -903,23 +422,6 @@ A ×d B =
IsPoset.is-trans B.isPoset b1 b2 b3 b1≤b2 b2≤b3
- {-
- order : ⟨ A ⟩ × ⟨ B ⟩ → ⟨ A ⟩ × ⟨ B ⟩ → Type ℓ-zero
- order (a1 , b1) (a2 , b2) = (a1 A.≤ a2) ⊎ ((a1 ≡ a2) × b1 B.≤ b2)
-
- order-trans : BinaryRelation.isTrans order
- order-trans (a1 , b1) (a2 , b2) (a3 , b3) (inl a1≤a2) (inl a2≤a3) =
- inl (IsPoset.is-trans A.isPoset a1 a2 a3 a1≤a2 a2≤a3)
- order-trans (a1 , b1) (a2 , b2) (a3 , b3) (inl a1≤a2) (inr (a2≡a3 , b2≤b3)) =
- inl (transport (λ i → a1 A.≤ a2≡a3 i) a1≤a2)
- order-trans (a1 , b1) (a2 , b2) (a3 , b3) (inr (a1≡a2 , b1≤b2)) (inl a2≤a3) =
- inl (transport (sym (λ i → a1≡a2 i A.≤ a3)) a2≤a3)
- order-trans (a1 , b1) (a2 , b2) (a3 , b3) (inr (a1≡a2 , b1≤b2)) (inr (a2≡a3 , b2≤b3)) =
- inr (
- (a1 ≡⟨ a1≡a2 ⟩ a2 ≡⟨ a2≡a3 ⟩ a3 ∎) ,
- IsPoset.is-trans B.isPoset b1 b2 b3 b1≤b2 b2≤b3)
- -}
-
is-poset : IsPoset order
is-poset = isposet
isSet-prod
@@ -1060,25 +562,12 @@ module Bisimilarity (d : Predomain) where
≈'->≈ : {lx ly : L℧ ⟨ d ⟩} ->
lx ≈' ly -> lx ≈ ly
≈'->≈ {lx} {ly} lx≈'ly = transport (sym (λ i → unfold-≈ i lx ly)) lx≈'ly
-
- {-
- ≈-℧ : (lx : L℧ ⟨ d ⟩) ->
- lx ≈' ℧ -> (lx ≡ ℧) ⊎ (Σ Nat λ n -> lx ≡ (δ ^ n) ℧)
- ≈-℧ ℧ H = inl refl
- ≈-℧ (θ x) H = inr H
- -}
- -- Simpler version of the above:
≈-℧ : (lx : L℧ ⟨ d ⟩) ->
lx ≈' ℧ -> (Σ Nat λ n -> lx ≡ (δ ^ n) ℧)
≈-℧ ℧ H = zero , refl
≈-℧ (θ x) H = H
-{-
- bisim-θ : (lx~ ly~ : L℧ ⟨ d ⟩) ->
- ▸ (λ t → lx~ t ≈ ly~ t) ->
- θ lx~ ≈ θ ly~
--}
symmetric' :
▹ ((lx ly : L℧ ⟨ d ⟩) -> lx ≈' ly -> ly ≈' lx) ->
@@ -1095,12 +584,9 @@ module Bisimilarity (d : Predomain) where
n , y , H-eq , (isEquivRel.symmetric isEqRel x y H-rel)
symmetric : (lx ly : L℧ ⟨ d ⟩) -> lx ≈ ly -> ly ≈ lx
- symmetric = fix (subst {!!} {!!})
-
- -- fix (transport {!!} symmetric')
+ symmetric = {!!} -- fix {k} (subst {!!} {!!})
{-
-
ord-trans = fix (transport (sym (λ i ->
(▹ ((a b c : L℧ ⟨ p ⟩) →
unfold-ord i a b → unfold-ord i b c → unfold-ord i a c) →
@@ -1160,9 +646,6 @@ module Bisimilarity (d : Predomain) where
(fix x≈'δx)
- -- ¬_ : Set → Set
- -- ¬ A = A → ⊥
-
contradiction : {A : Type} -> A -> ¬ A -> ⊥
contradiction HA ¬A = ¬A HA
@@ -1187,8 +670,8 @@ module Bisimilarity (d : Predomain) where
fixθ-lem1 : (n : Nat) ->
- (▹ (¬ (θ (next (fix θ)) ≡ (δ ^ n) ℧))) ->
- ¬ (θ (next (fix θ)) ≡ (δ ^ n) ℧)
+ (▹ (¬ (θ {Nat} (next (fix θ)) ≡ (δ ^ n) ℧))) ->
+ ¬ (θ {Nat} (next (fix θ)) ≡ (δ ^ n) ℧)
fixθ-lem1 zero _ H-eq = θ≠℧ H-eq
fixθ-lem1 (suc n) IH H-eq =
let tmp = inj-θ (next (fix θ)) (next ((δ ^ n) ℧)) H-eq in {!!}
@@ -1196,254 +679,4 @@ module Bisimilarity (d : Predomain) where
℧-fixθ : ¬ (℧ ≈' θ (next (fix θ)))
℧-fixθ (n , H-eq) = {!!}
-
-
-
-
-
-
-
-
-
-
-{-
- lem1 :
- ▹ ((lx : L℧ ⟨ d ⟩) -> lx ≾' θ (next lx)) ->
- (lx : L℧ ⟨ d ⟩) -> lx ≾' θ (next lx)
- lem1 _ (η x) = 1 , (x , (refl , (reflexive d x)))
- lem1 _ ℧ = tt
- lem1 IH (θ lx~) = {!!}
-
-
- lem2 :
- (lx~ ly~ : ▹ L℧ ⟨ d ⟩) ->
- (n : Nat) ->
- θ lx~ ≾' θ ly~ ->
- θ ly~ ≡ (δ ^ n) ℧ ->
- Σ Nat λ m -> θ lx~ ≡ (δ ^ m) ℧
- lem2 lx ly n lx≤ly H-eq-δ = {!!}
-
- lem3 :
- (lx~ ly~ : ▹ L℧ ⟨ d ⟩) ->
- (n : Nat) ->
- (x' : ⟨ d ⟩) ->
- θ lx~ ≾' θ ly~ ->
- θ lx~ ≡ (δ ^ n) (η x') ->
- Σ Nat λ m -> Σ ⟨ d ⟩ λ y' -> θ ly~ ≡ (δ ^ m) (η y')
- lem3 = {!!}
-
-
- trans-ind :
- ▹ ((lx ly lz : L℧ ⟨ d ⟩) ->
- lx ≾' ly -> ly ≾' lz -> lx ≾' lz) ->
- (lx ly lz : L℧ ⟨ d ⟩) ->
- lx ≾' ly -> ly ≾' lz -> lx ≾' lz
- trans-ind IH ℧ ly lz lx≤ly ly≤lz = tt
- trans-ind IH (η x) (η y) (η z) lx≤ly ly≤lz =
- IsPoset.is-trans D.isPoset x y z lx≤ly ly≤lz
-
- trans-ind IH lx ℧ lz = {!!} -- not possible unless x is ℧
- trans-ind IH lx ly ℧ = {!!} -- not possible unless lx and ly are ℧
-
- trans-ind IH (θ lx~) (θ ly~) (θ lz~) = {!!} -- follows by induction
- {-
- λ t -> transport (sym λ i → unfold-ord i (lx~ t) (lz~ t))
- (IH t (lx~ t) (ly~ t) (lz~ t)
- (transport (λ i -> unfold-ord i (lx~ t) (ly~ t)) (ord-ab t))
- (transport (λ i -> unfold-ord i (ly~ t) (lz~ t)) (ord-bc t)))
-
- -}
-
- trans-ind IH (η x) (θ ly~) (η z) (n , y' , H-eq-δ , H-y'≤z) (m , inl H-℧) =
- {!-- contradiction: θ ly~ ≡ δ^m ℧ and also ≡ δ^n (η y')!}
- trans-ind IH (η x) (θ ly~) (η z)
- (n , y' , H-eq-δ1 , H-y'≤z)
- (m , inr (y'' , H-eq-δ2 , H-y''≤z)) =
- {! -- we have m ≡ n and y'== y'', so x ≤ z by transitivity!}
-
- trans-ind IH (η x) (θ ly~) (θ lz~) (n , y' , H-eq-δ , H-x≤y') ly≤lz =
- let (m , y'' , eq) = lem3 ly~ lz~ n y' ly≤lz H-eq-δ in {!!}
-
- trans-ind IH (θ lx~) (θ ly~) (η z) lx≤ly ly≤lz = {!!}
-
- trans-ind IH (θ lx~) (η y) (θ lz~) lx≤ly ly≤lz = {!!}
--}
-
-
-
-{-
--- Extensional relation (two terms are error-related "up to thetas")
-module ExtRel (d : Predomain) where
-
- open Bisimilarity d
- open 𕃠d
-
- _⊴_ : L℧ ⟨ d ⟩ -> L℧ ⟨ d ⟩ -> Type
- x ⊴ y = Σ (L℧ ⟨ d ⟩) λ p -> Σ (L℧ ⟨ d ⟩) λ q ->
- (x ≈ p) × (p ≾ q) × (q ≈ y)
-
--}
-
-
-
-
-{-
--- Weak bisimulation relaion
--- Define compositionally
-
-module WeakRel (d : ErrorDomain) where
-
- -- make this a module so we can avoid having to make the IH
- -- a parameter of the comparison function
- module Inductive (IH : ▹ (L℧ (U d) -> L℧ (U d) -> Type)) where
-
- open ErrorDomain d renaming (θ to θ')
-
- _≾'_ : L℧ (U d) -> L℧ (U d) -> Type
- ℧ ≾' _ = Unit
-
- η x ≾' η y = x ≤ y
-
- θ lx ≾' θ ly = ▸ (λ t -> IH t (lx t) (ly t))
- -- or equivalently: θ lx ≾' θ ly = ▸ ((IH ⊛ lx) ⊛ ly)
-
- η x ≾' θ t = Σ ℕ λ n -> Σ (U d) (λ y -> (θ t ≡ (δ ^ n) (η y)) × (x ≤ y))
-
- -- need to account for error (θ s ≡ delay of η x or delay of ℧, in which case we're done)
- θ s ≾' η y = Σ ℕ λ n ->
- (θ s ≡ (δ ^ n) L℧.℧) ⊎
- (Σ (U d) (λ x -> (θ s ≡ (δ ^ n) (η x)) × (x ≤ y)))
-
- _ ≾' ℧ = ⊥
-
- _≾_ : L℧ (U d) -> L℧ (U d) -> Type
- _≾_ = fix _≾'_
- where open Inductive
-
--}
-
-{-
-
-
-Lemma A:
-
-If lx ≈ ly and ly ≡ δ^n (℧), then
-lx = δ^m (℧) for some m ≥ 0.
-
-Proof. By induction on n.
-
- First note that if lx ≡ ℧, then we are finished (taking m = 0).
- If lx ≡ η x', this contradicts the assumption that lx ≈ δ^n (℧).
-
- Hence, we may assume lx = (θ lx~). By definition of the relation, we have
-
- ▸t [lx~ t ≈ δ^(n-1) (℧)],
-
- so by induction, we have lx~ t ≡ δ^m (℧) for some m,
- and thus lx~ ≡ δ^(m+1) (℧)
-
-
-
-Lemma B:
-
-If lx ≈ ly and
-
-
-
-Claim: The weak bisimulation relation is transitive,
-
-i.e. if lx ≈ ly ≈ lz, then lx ≈ lz.
-
-Proof.
-
-By Lob induction.
-Consider cases on lx, ly, and lz.
-
-
-Case η x ≈ η y ≈ η z:
- We have x ≤ y ≤ z, so by transitivity of the underlying relation we
- have x ≤ z, so η x ≈ η z
-
-Case ℧ ≈ ly ≈ lz:
- Trivial by definition of the relation.
-
-Case ly = ℧ or lz = ℧:
- Impossible by definition of the relation.
-
-Case (θ lx~) ≈ (θ ly~) ≈ (θ lz~):
- By definition of the relation, STS that
- ▸t [(lx~ t) ≈ (lz~ t)]
-
- We know
- ▸t [(lx~ t) ≈ (ly~ t)] and
- ▸t [(ly~ t) ≈ (lz~ t)],
-
- so the conclusion follows by the IH.
-
-
- (1) (2)
-Case (η x) ≈ (θ ly~) ≈ (η z):
-
- By (2), we have that either
- (θ ly~) ≡ δ^n ℧ or (θ ly~) ≡ δ^n (η y') where y' ≤ z.
-
- But by (1), we have (θ ly~) ≡ δ^n (η y') where x ≤ y'.
- Thus the second case above must hold, and we have by
- transitivity of the underlying relation that x ≤ z,
- so (η x) ≈ (η z).
-
-
- (1) (2)
-Case (η x) ≈ (θ ly~) ≈ (θ lz~):
-
-
-
-
- (1) (2)
-Case (θ lx~) ≈ (η y) ≈ (θ lz~):
-
- We need to show that
-
- ▸t [(lx~ t) ≈ (lz~ t)].
-
- By (1), either (θ lx~) ≡ δ^n (℧) for some n ≥ 1, or
- (θ lx~) ≡ δ^n (η x') where x' ≤ y.
-
- By (2), (θ lz~) ≡ δ^m (η z') for some m ≥ 1 and y ≤ z'.
-
- Suppose n ≤ m. Then after n "steps" of unfolding thetas
- on both sides, we will be left with either ℧ or η x' on the left,
- and δ^(m-n)(η z') on the right.
- In the former case we are finished since ℧ is the bottom element,
- and in the latter case we can use transitivity of the underlying
- relation to conclude x' ≤ z' and hence η x' ≈ δ^(m-n)(η z').
-
- Now suppose n > m. Then after m steps of unfolding,
- we will be left with either δ^(n-m)(℧) or δ(n-m)(η x') on the left,
- and η z' on the right.
- In the former case we are finished by definition of the relation.
- In the latter case we again use transitivity of the underlying relation.
-
-
-
- (1) (2)
-Case (θ lx~) ≈ (θ ly~) ≈ (η z):
-
- By (2), either (θ ly~) ≡ δ^n (℧), or
- (θ ly~) ≡ δ^n (η y') where y' ≤ z.
-
- In the former case, (1) and Lemma A imply that
- (θ lx~) ≡ δ^m (℧) for some m, and we are finished
- by definiton of the relation.
-
- In the latter case, (1) and Lemma B imply that
- (θ lx~) ≡ δ^m (η x') for some m and some x'
- with x' ≤ y'.
- Then by transitivity of the underlying relation
- we have x' ≤ z, so we are finished.
-
-
-
-
--}
--
GitLab