work on weak bisimilarity file

formalizations/guarded-cubical/Semantics/WeakBisimilarity.agda

@@ -19,9 +19,10 @@ open import Cubical.Data.Empty as ⊥
 open import Cubical.Relation.Binary
 open import Cubical.Relation.Binary.Order.Poset
 
-open import Cubical.HITs.PropositionalTruncation renaming (elim to PTelim)
+open import Cubical.HITs.PropositionalTruncation renaming (elim to PTelim ; rec to PTrec)
 
 open import Common.Common
+open import Common.LaterProperties
 open import Semantics.Lift k
 
 private
@@ -34,6 +35,13 @@ private
 
 open BinaryRelation
 
+-- If θ l~ is an iterated delay of l for some l, then one time
+-- step later, l~ t is also an iterated delay
+lem-θ-δ : {X : Type ℓ} -> {l~ : ▹ L X} -> {l : L X} -> (n : ℕ) ->
+  (θ l~) ≡ (δL ^ (suc n)) l -> ▸ (λ t -> l~ t ≡ (δL ^ n) l)
+lem-θ-δ {l~ = l~} {l = l} n H t = inj-θL l~ (next ((δL ^ n) l)) H t
+
+
 -- Weak bisimilarity on Lift X, parameterized by a relation on X.
 -- 
 -- If this relation is instantiated with a PER on X, then the
@@ -84,13 +92,35 @@ module Bisim (X : Type ℓ) (R : X -> X -> Type ℓR) where
   θ-cong : {lx ly : ▹ (L X)} -> ▸ (λ t → (lx t) ≈ (ly t)) -> (θ lx) ≈ (θ ly)
   θ-cong {lx~} {ly~} H-later = ≈'→≈ (θ lx~) (θ ly~) H-later
 
+
+  -- In the definition of the relation, whenever we have a Σ n,
+  -- we only require that it is ≥ 0. But in fact we can show that
+  -- it must be at least 1.
+  -- It seems more convenient to define the ordering as we do
+  -- and then prove these lemmas after the fact.
+  θ≈η-lem-suc : {lx~ : ▹ L X} -> {y : X} -> θ lx~ ≈' η y ->
+    ∥ Σ[ n ∈ ℕ ] Σ[ x ∈ X ] ((θ lx~ ≡ (δL ^ (suc n)) (η x)) × R x y) ∥₁
+  θ≈η-lem-suc H = PTrec isPropPropTrunc (λ {
+    (zero , y , eq , xRy) → ⊥.rec (Lη≠Lθ (sym eq)) ;
+    (suc n , y , eq , xRy) → ∣ n , y , {!!} ∣₁}) H
+
+
+  -- Bisimilarity when one side is η
+  ≈'-η : ∀ lx y → lx ≈' η y →
+    ∥ Σ[ n ∈ ℕ ] Σ[ x ∈ X ] (lx ≡ (δL ^ n) (η x)) × (R x y) ∥₁ -- need propositional truncation
+  ≈'-η (η x) y Rxy = ∣ 0 , x , refl , lower Rxy ∣₁
+  ≈'-η (θ lx~) y H = PTrec isPropPropTrunc (λ
+    {(n , x , eq , Rxy) → ∣ n , x , eq , Rxy ∣₁}) H
+
+
+
   module PropValued (isPropValuedR : isPropValued R) where
-     lem : ∀ n m (x y : X) -> (δL ^ n) (η x) ≡ (δL ^ m) (η y) -> (n ≡ m) × (x ≡ y)
-     lem zero zero x y H = refl , inj-η x y H
-     lem zero (suc m) x y H = ⊥.rec (Lη≠Lθ H)
-     lem (suc n) zero x y H = ⊥.rec (Lη≠Lθ (sym H))
-     lem (suc n) (suc m) x y H = {!!} -- *not provable!!*
-     -- let IH = lem n m x y {!!} in {!!}
+     -- lem : ∀ n m (x y : X) -> (δL ^ n) (η x) ≡ (δL ^ m) (η y) -> (n ≡ m) × (x ≡ y)
+     -- lem zero zero x y H = refl , inj-η x y H
+     -- lem zero (suc m) x y H = ⊥.rec (Lη≠Lθ H)
+     -- lem (suc n) zero x y H = ⊥.rec (Lη≠Lθ (sym H))
+     -- lem (suc n) (suc m) x y H = {!!} -- *not provable!!*
+       -- let IH = lem n m x y {!!} in {!!}
 
      prop-≈'→prop-≈ : BinaryRelation.isPropValued _≈'_ -> BinaryRelation.isPropValued _≈_
      prop-≈'→prop-≈ = transport (λ i -> BinaryRelation.isPropValued (sym unfold-≈ i))
@@ -103,13 +133,67 @@ module Bisim (X : Type ℓ) (R : X -> X -> Type ℓR) where
        let x = (isPropValuedR a b (lower p) (lower q)) in isoInvInjective LiftIso p q x
      prop' IH (η a) (θ lb~) p q = isPropPropTrunc p q --ΣPathP ({!snd q .snd .fst!} , {!!})
      prop' IH (θ la~) (η b) p q = isPropPropTrunc p q
-     prop' IH (θ la~) (θ lb~) p q =
-       λ i t → prop-≈'→prop-≈ (IH t) (la~ t) (lb~ t) (p t) (q t) i
+     prop' IH (θ la~) (θ lb~) p q = isProp▸ (λ t -> prop-≈'→prop-≈ (IH t) (la~ t) (lb~ t)) p q
+       -- or, more explicitly: λ i t → prop-≈'→prop-≈ (IH t) (la~ t) (lb~ t) (p t) (q t) i
 
      prop :  BinaryRelation.isPropValued _≈_
      prop = prop-≈'→prop-≈ (fix prop')
 
 
+     absurd : ∀ X -> ▹ (▹ X) → ▹ X
+     absurd X llx = λ t -> {!llx t t!}
+    
+
+     ≈'-δ^n-η-sufficient : (x y : X) (n : ℕ) →
+       R x y → (δL ^ n) (η x) ≈' η y
+     ≈'-δ^n-η-sufficient x y zero H = lift H
+     ≈'-δ^n-η-sufficient x y (suc n) H = ∣ suc n , x , refl , H ∣₁
+
+     lem : ∀ n x y → δL ((δL ^ n) (η x)) ≈' η y → (δL ^ n) (η x) ≈' η y
+     lem n x y H =
+       PTrec (prop-≈→prop-≈' prop _ _)
+             (λ {(n' , x' , eq) →
+               {!!}})
+             H
+
+
+     -- If lx ≈ ly, then lx ≈ δL ly.
+     -- This is more general than the corresponding "homogeneous" version
+     -- i.e., x ≈ (δL x). This proof is more involved because we need to
+     -- consider both lx and ly, which leads to complications in the case
+     -- where lx is θ and ly is η, because when we add a θ on the right,
+     -- now both sides are a θ and so we change to a different case of
+     -- the relation than the one used to prove the assumption lx ≈ ly.
+     δ-closed-r : ▹ ((lx ly : L X) -> lx ≈' ly -> lx ≈' (δL ly)) ->
+                     (lx ly : L X) -> lx ≈' ly -> lx ≈' (δL ly)
+     δ-closed-r _ (η x) (η y) lx≈'ly = ∣ 1 , y , refl , lower lx≈'ly ∣₁ 
+
+     δ-closed-r _ (η x) (θ ly~) lx≈'ly =
+       PTrec isPropPropTrunc (λ {(n , y , eq , xRy) -> ∣ suc n , y , cong δL eq  , xRy ∣₁}) lx≈'ly
+
+     δ-closed-r _ (θ lx~) (η y) lx≈'ly =      -- lx≈'ly : θ lx~ ≈' η y
+       let lem1 = θ≈η-lem-suc lx≈'ly in
+       PTrec (prop-≈→prop-≈' prop _ _)
+             (λ {(n , x , eq , xRy) ->              -- eq : θ lx~ ≡ δL ((δL ^ n) (η x))
+               let lem2 = lem-θ-δ n eq in
+                 λ t -> transport (λ i -> sym (lem2 t) i ≈ (η y)) (≈'→≈ _ _ (≈'-δ^n-η-sufficient x y n xRy)) })
+             lem1
+
+       {-
+       λ t ->
+       PTrec (prop _ _) (λ {(n , x , eq , xRy) ->
+         let lem1 = θ≈η-lem-suc lx≈'ly in
+         let lem2 = lem-θ-δ n {!!} in
+         PTrec (prop _ _) (λ {(n' , x' , eq') -> {!lem-θ-δ n' eq' t!}}) lem1}) lx≈'ly
+         -}
+    
+
+     δ-closed-r IH (θ lx~) (θ ly~) lx≈'ly =
+       λ t -> ≈'→≈ _ _ (transport
+         (cong₂ _≈'_ refl (congS θ (next-Mt≡M ly~ t)))
+         (IH t (lx~ t) (ly~ t) (≈→≈' _ _ (lx≈'ly t))))
+
+
   module Reflexive (isReflR : isRefl R) where
 
      ≈'-refl : ▹ (isRefl _≈'_) -> isRefl _≈'_
@@ -126,9 +210,15 @@ module Bisim (X : Type ℓ) (R : X -> X -> Type ℓR) where
       λ t → ≈'→≈ (lx~ t) (θ lx~)
       (transport (λ i → (lx~ t) ≈' θ (next-Mt≡M lx~ t i)) (IH t (lx~ t)))
 
+     -- The "homogeneous" version of the above property about closure
+     -- under δ.
      x≈δx : (lx : L X) -> lx ≈ (δL lx)
      x≈δx lx = ≈'→≈ lx (δL lx) (fix x≈'δx lx)
 
+     x≈δ^nx : (n : ℕ) -> (lx : L X) -> lx ≈ (δL ^ n) lx
+     x≈δ^nx zero lx = ≈-refl lx
+     x≈δ^nx (suc n) lx = {!!}
+
   module Symmetric (isSymR : isSym R) where
 
     symmetric' :
@@ -151,6 +241,9 @@ module Bisim (X : Type ℓ) (R : X -> X -> Type ℓR) where
       ≈'→≈ _ _ (fix symmetric' lx ly (≈→≈' _ _ lx≈ly))
 
 
+
+
+
 -- A version of weak bisimilarity on Lift X that seems to *not* be
 -- propositional. The issue is that in the two cases involving Σ, we cannot
 -- prove that the natural number n and the value of type X are unique.
@@ -179,7 +272,9 @@ module NonPropBisim (X : Type ℓ) (R : X -> X -> Type ℓR) where
 
 
 
-{-
+
+
+
 module BisimSum (X : Type ℓ) (R : X -> X -> Type ℓR) where
 
   -- Weak bisimilarity as a sum type
@@ -187,8 +282,8 @@ module BisimSum (X : Type ℓ) (R : X -> X -> Type ℓR) where
   module Inductive (rec :  ▹ (L X -> L X -> Type (ℓ-max ℓ ℓR))) where 
     _≈'_ : L X -> L X -> Type (ℓ-max ℓ ℓR)
     l ≈' l' =  (Σ[ x ∈ X ] Σ[ y ∈ X ] (l ≡ η x) × (l' ≡ η y) × R x y) ⊎
-               ((Σ[ x ∈ X ] Σ[ y ∈ X ] Σ[ n ∈ ℕ ] (l ≡ η x)            × (l' ≡ (δL ^ n) (η y)) × R x y) ⊎
-               ((Σ[ x ∈ X ] Σ[ y ∈ X ] Σ[ n ∈ ℕ ] (l ≡ (δL ^ n) (η x)) × (l' ≡ η y)            × R x y) ⊎
+              ((Σ[ x ∈ X ] ((l  ≡ η x) × ∥ Σ[ n ∈ ℕ ] Σ[ y ∈ X ] ((l' ≡ (δL ^ n) (η y)) × R x y) ∥₁)) ⊎
+              ((Σ[ y ∈ X ] ((l' ≡ η y) × ∥ Σ[ n ∈ ℕ ] Σ[ x ∈ X ] ((l  ≡ (δL ^ n) (η x)) × R x y) ∥₁)) ⊎
                (Σ[ lx~ ∈ ▹ (L X) ] Σ[ ly~ ∈ ▹ (L X) ] (l ≡ θ lx~) × (l' ≡ θ ly~) × (▸ (λ t -> rec t (lx~ t) (ly~ t))))))
 
   _≈_ : L X → L X → Type (ℓ-max ℓ ℓR)
@@ -221,12 +316,13 @@ module _ (X : Type ℓ) (R : X -> X -> Type ℓR) where
         lem : ▹ ((l l' : L X) -> l ≈' l' -> l ≈S' l') ->
                  (l l' : L X) -> l ≈' l' -> l ≈S' l'
         lem _ (η x) (η y) H = inl (x , (y , (refl , (refl , (lower H)))))
-        lem _ (η x) (θ ly~) (n , y , eq , xRy) = inr (inl (x , y , n , refl , eq , xRy))
-        lem _ (θ lx~) (η y) (n , x , eq , xRy) = inr (inr (inl (x , y , n , eq , refl , xRy)))
+        lem _ (η x) (θ ly~) H = inr (inl (x , refl , H))
+        lem _ (θ lx~) (η y) H = inr (inr (inl (y , refl , H)))
         lem IH (θ lx~) (θ ly~) H =
           inr (inr (inr (lx~ , ly~ , refl , refl ,
                          λ t -> BSum.≈'→≈ (lx~ t) (ly~ t) (IH t (lx~ t) (ly~ t) (B.≈→≈' _ _ (H t))))))
-        
+
+{-
   ≈Sum→≈ : (l l' : L X) -> l ≈S l' -> l ≈ l'
   ≈Sum→≈ l l' l≈Sl' = {!!}
     where
@@ -234,9 +330,9 @@ module _ (X : Type ℓ) (R : X -> X -> Type ℓR) where
                 (l l' : L X) -> l ≈S' l' -> l ≈' l'
       lem _ l l' (inl (x , y , eq1 , eq2 , Rxy)) = (transport (λ i -> (sym eq1 i) ≈' (sym eq2 i)) (lift Rxy))
       lem _ l l' (inr (inl (x , y , n , eq1 , eq2 , Rxy))) = {!!} -- NTS that l' is of the form θ(...)
+-}
 
 
--}
 
 {-
 module _ (X : Type) (R : X -> X -> Type ℓR) where
@@ -245,3 +341,54 @@ module _ (X : Type) (R : X -> X -> Type ℓR) where
   
 
   
+-- Global version:
+-- lx ≈g ly <-->
+-- lx ≡ η^gl x × ly ≡ η^gl y × x ≈ y  +
+-- lx ≡ η^gl x × ly ≡ (δ^gl)^n (η^gl y) × x ≈ y   +
+-- ly ≡ η^gl y × lx ≡ (δ^gl)^n (η^gl x) × x ≈ y   +
+-- lx ≡ δ^gl lx' × ly ≡ δ^gl ly' × lx' ≈g ly'
+
+-- ∀k. Σ[ l1~ ∈ ▹ L k X ] Σ[ l2~ ∈ ▹ L k X ]
+--   (l1^g k ≡ θ l1~) × (l2^g k ≡ θ l2~) × (▸k_t [ l1~ t ≈_k l2~ t ])
+
+-- Σ[ l1'^g ∈ ∀k. L k X ] Σ[ l2'^g ∈ ∀k. L k Y ]
+--   ∀k. ((l1^g ≡ δ^gl l1'^g) × (l2^g ≡ δ^gl l2'^g) × (▸k_t [ l1'^g k ≈_k l2'^g k ]))
+
+
+
+
+
+
+-- Σ[ l1'^g ∈ ∀k. L k X ] Σ[ l2'_g ∈ ∀k. L k Y ]
+--   (l1^g ≡ δ^gl l1'^g) × (l2^g ≡ δ^gl l2'^g) × (l1'^g ≈g l2'^g)
+--
+-- ∀k. Σ[ l1 ∈ L k X ] Σ[ l2 ∈ L k Y]
+--   (l1^g k ≡ δ k l1) × (l2^g k ≡ δ k l2) × (l1 ≈_k l2)
+--
+-- ∀k. ▹ Σ[ l1 ∈ L k X ] Σ[ l2 ∈ L k Y]
+--   (l1^g k ≡ δ k l1) × (l2^g k ≡ δ k l2) × (l1 ≈_k l2)
+--
+-- ∀k. Σ[ l1~ ∈ ▹ L k X ] Σ[ l2~ ∈ ▹ L k X ]
+--   ▸_t [ (l1^g k ≡ δ k (l1~ t)) × (l2^g k ≡ δ k (l2~ t)) × (l1~ t ≈_k l2~ t) ]
+--
+-- ∀k. Σ[ l1~ ∈ ▹ L k X ] Σ[ l2~ ∈ ▹ L k X ]
+--   ▸_t [ l1^g k ≡ δ k (l1~ t) ] × ▸_t [ l2^g k ≡ δ k (l2~ t) ] × ▸_t [ l1~ t ≈_k l2~ t ]
+--
+-- ∀k. Σ[ l1~ ∈ ▹ L k X ] Σ[ l2~ ∈ ▹ L k X ] 
+--   (l1^g k ≡ δ k (l1~ ◇)) × (l2^g k ≡ δ k (l2~ ◇)) × ▸_t [ l1~ t ≈_k l2~ t ]
+--
+-- ∀k. Σ[ l1~ ∈ ▹ L k X ] Σ[ l2~ ∈ ▹ L k X ]
+--   (l1^g k ≡ θ k l1~) × (l2^g k ≡ θ k l2~) × ▸_t [ l1~ t ≈_k l2~ t ]
+ 
+
+-- ∀k. (▸_t [ l1^g k ≡ δ k (l1~ t) ] × ▸_t [ l2^g k ≡ δ k (l2~ t) ] × ▸_t [ l1~ t ≈_k l2~ t ])
+
+-- ∀k. ▸_t [ l1^g k ≡ δ k (l1~ t) ] × ∀k. ▸_t [ l2^g k ≡ δ k (l2~ t) ] × ∀k. ▸_t [ l1~ t ≈_k l2~ t ]
+
+-- ∀k. ▸_t [ l1^g k ≡ θ k l1~ ] × ∀k. ▸_t [ l2^g k ≡ θ k l2~ ] × ∀k. ▸_t [ l1~ t ≈_k l2~ t ]
+
+-- ∀k. (l1^g k ≡ θ k l1~) × ∀k. l2^g k ≡ θ k l2~ × ∀k. ▸_t [ l1~ t ≈_k l2~ t ]
+
+
+
+-- ... × (θ l1~) ≈_k (θ l2~)