Add lemmas for representable relation

formalizations/guarded-cubical/Semantics/Concrete/DynNew.agda

@@ -17,12 +17,14 @@ open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Structure
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Transport
 
 open import Cubical.Relation.Binary
 open import Cubical.Data.Nat renaming (ℕ to Nat)
 open import Cubical.Data.Sum
 open import Cubical.Data.Unit
 open import Cubical.Data.Empty
+open import Cubical.Data.Sigma
 
 open import Common.LaterProperties
 --open import Common.Preorder.Base
@@ -37,6 +39,7 @@ open import Common.Poset.Constructions
 open import Common.Poset.Monotone
 open import Common.Poset.MonotoneRelation
 open import Semantics.MonotoneCombinators
+open import Semantics.Concrete.MonotonicityProofs
 
 open import Semantics.LockStepErrorOrdering k
 
@@ -44,6 +47,7 @@ open BinaryRelation
 open LiftPoset
 open ClockedCombinators k
 
+
 private
   variable
     ℓ ℓ' ℓX ℓX' : Level
@@ -62,6 +66,8 @@ DynP' D = ℕ ⊎p (▸' k (λ t → D t ==> 𝕃 (D t)))
 DynP : Poset ℓ-zero ℓ-zero
 DynP = fix DynP'
 
+
+
 unfold-DynP : DynP ≡ DynP' (next DynP)
 unfold-DynP = fix-eq DynP'
 
@@ -74,6 +80,46 @@ DynP-Sum = unfold-DynP
 ⟨DynP⟩-Sum : ⟨ DynP ⟩ ≡ Nat ⊎ (▹ (⟨ DynP ==> 𝕃 DynP ⟩)) -- MonFun DynP (𝕃 DynP)
 ⟨DynP⟩-Sum i = ⟨ DynP-Sum i ⟩
 
+
+
+case : {ℓA ℓB ℓC : Level} -> {A : Type ℓA} {B : Type ℓB} {C : Type ℓC} ->
+  (A -> C) -> (B -> C) -> ((A ⊎ B) -> C)
+case f g =  λ { (inl a) → f a ; (inr b) → g b }
+
+
+Rel-DynP-lem : ∀ d d' -> rel DynP d d' ->
+      (Σ[ n ∈ ⟨ ℕ ⟩ ]
+      (Σ[ n' ∈ ⟨ ℕ ⟩ ]
+      (transport ⟨DynP⟩-Sum d ≡ inl n)
+      × (transport ⟨DynP⟩-Sum d' ≡ inl n')
+      × (n ≡ n'))) ⊎
+      (Σ[ f~ ∈ ⟨ ▹' k ((DynP ==> 𝕃 DynP)) ⟩ ]
+      (Σ[ g~ ∈ ⟨ ▹' k ((DynP ==> 𝕃 DynP)) ⟩ ]
+      (transport ⟨DynP⟩-Sum d ≡ inr f~)
+      × (transport ⟨DynP⟩-Sum d' ≡ inr g~)
+      × (▸ (λ t → f~ t ≤mon g~ t))))
+Rel-DynP-lem d d' d≤d' =
+  let dSum = transport ⟨DynP⟩-Sum d in let d'Sum = transport ⟨DynP⟩-Sum d' in
+  let dSum≤d'Sum = rel-transport DynP-Sum d≤d' in (rel-sum dSum d'Sum dSum≤d'Sum)
+
+
+⊎p-rel-lem-l : {ℓA ℓ'A ℓB ℓ'B : Level} {A : Poset ℓA ℓ'A} {B : Poset ℓB ℓ'B} ->
+  (a : ⟨ A ⟩) ->
+  (x : ⟨ A ⟩ ⊎ ⟨ B ⟩) ->
+  rel (A ⊎p B) (inl a) x ->
+  Σ[ a' ∈ ⟨ A ⟩ ] (x ≡ inl a') × rel A a a'
+⊎p-rel-lem-l a (inl a') H = a' , (refl , (lower H))
+
+⊎p-rel-lem-r : {ℓA ℓ'A ℓB ℓ'B : Level} {A : Poset ℓA ℓ'A} {B : Poset ℓB ℓ'B} ->
+  (b : ⟨ B ⟩) ->
+  (x : ⟨ A ⟩ ⊎ ⟨ B ⟩) ->
+  rel (A ⊎p B) (inr b) x ->
+  Σ[ b' ∈ ⟨ B ⟩ ] (x ≡ inr b') × rel B b b'
+⊎p-rel-lem-r b (inr b') H = b' , (refl , (lower H))
+
+
+
+
 InjNat : ⟨ ℕ ==> DynP ⟩
 InjNat = mCompU (mTransport (sym DynP-Sum)) σ1
 
@@ -83,28 +129,60 @@ InjArr = mCompU (mTransport (sym DynP-Sum)) (mCompU σ2 Next)
 ProjNat : ⟨ DynP ==> 𝕃 ℕ ⟩
 ProjNat = mCompU (Case' mRet (K _ ℧)) (mTransport DynP-Sum)
 
-
 ▹g→g : MonFun ((▸'' k) (DynP ==> 𝕃 DynP)) (𝕃 (DynP ==> 𝕃 DynP))
 ▹g→g = record {
    f = λ f~ -> θ (λ t -> η (f~ t)) ;
-   isMon = λ {f~} {g~} f~≤g~ → ord-θ-monotone _ (λ t -> ord-η-monotone _ (f~≤g~ t))
-        -- ord-θ-monotone _ (λ t -> ord-η-monotone _ (f~≤g~ t))
-   }
+   isMon = λ {f~} {g~} f~≤g~ → ord-θ-monotone _ (λ t -> ord-η-monotone _ (f~≤g~ t)) }
+
+ProjNat-nat : ∀ d n ->
+  transport ⟨DynP⟩-Sum d ≡ inl n ->
+  MonFun.f ProjNat d ≡ η n
+ProjNat-nat d n eq =
+  cong₂ (MonFun.f {X = DynP} {Y = 𝕃 ℕ})
+        (refl {x = ProjNat})
+        ((sym (transport⁻Transport ⟨DynP⟩-Sum d)) ∙ λ i -> transport⁻ ⟨DynP⟩-Sum (eq i))
+  ∙ λ i → MonFun.f {!!} (transportTransport⁻ ⟨DynP⟩-Sum (inl n) i)
+
+ProjNat-fun : ∀ d g~ ->
+  transport ⟨DynP⟩-Sum d ≡ inr g~ ->
+  MonFun.f ProjNat d ≡ ℧
+ProjNat-fun d g~ eq =
+  cong₂ (MonFun.f {X = DynP} {Y = 𝕃 ℕ})
+        (refl {x = ProjNat})
+        ((sym (transport⁻Transport ⟨DynP⟩-Sum d)) ∙ λ i -> transport⁻ ⟨DynP⟩-Sum (eq i))
+  ∙ λ i → MonFun.f (Case' mRet (K {!𝕃 (DynP ==> 𝕃 DynP)!} ℧)) (transportTransport⁻ ⟨DynP⟩-Sum (inr g~) i)
 
 ProjArr : ⟨ DynP ==> 𝕃 (DynP ==> 𝕃 DynP) ⟩
 ProjArr = mCompU (Case' (K _ ℧) ▹g→g) (mTransport DynP-Sum)
- 
-    
+
+
+ProjArr-nat : ∀ d n ->
+  transport ⟨DynP⟩-Sum d ≡ inl n ->
+  MonFun.f ProjArr d ≡ ℧
+ProjArr-nat d n eq =
+  cong₂ (MonFun.f {X = DynP} {Y = 𝕃 (DynP ==> 𝕃 DynP)})
+        (refl {x = ProjArr})
+        ((sym (transport⁻Transport ⟨DynP⟩-Sum d)) ∙ λ i -> transport⁻ ⟨DynP⟩-Sum (eq i))
+  ∙ λ i → MonFun.f (Case' (K ℕ ℧) ▹g→g) (transportTransport⁻ ⟨DynP⟩-Sum (inl n) i)
+
 
 ProjArr-fun : ∀ d g~ ->
   transport ⟨DynP⟩-Sum d ≡ inr g~ ->
   MonFun.f ProjArr d ≡ θ (λ t -> η (g~ t))
-ProjArr-fun d g~ eq = {!!} ∙
+ProjArr-fun d g~ eq =
+  cong₂ (MonFun.f {X = DynP} {Y = 𝕃 (DynP ==> 𝕃 DynP)})
+        (refl {x = ProjArr})
+        ((sym (transport⁻Transport ⟨DynP⟩-Sum d)) ∙ λ i -> transport⁻ ⟨DynP⟩-Sum (eq i))
+  ∙ (λ i -> MonFun.f (Case' (K ℕ ℧) ▹g→g) (transportTransport⁻ ⟨DynP⟩-Sum (inr g~) i))
+
+--  MonFun.f ProjArr (transport⁻ ⟨DynP⟩-Sum (inr g~)) ≡ _y_510
+
+  {-{!!} ∙
   -- (λ i -> MonFun.f (mCompU (Case' (K _ ℧) aux) (mTransport DynP-Sum)) d) ∙
   (congS ((λ { (inl a) → MonFun.f (K ℕ ℧) a
              ; (inr b) → MonFun.f ▹g→g b
          })) eq) ∙
-  {!!}
+  refl -}
 -- MonFun.f ProjArr d ≡ θ (λ t → η (g~ t))
 
 -- (transp (λ i → ⟨ DynP-Sum i ⟩) i0 d)

formalizations/guarded-cubical/Semantics/Concrete/MonotonicityProofs.agda

@@ -106,14 +106,15 @@ module ClockedProofs (k : Clock) where
 
   ret-monotone : {A : Poset ℓA ℓ'A} ->
     (a a' : ⟨ A ⟩) ->
-    (rAA : ⟨ A ⟩ -> ⟨ A ⟩ -> Type ℓR) ->
+    rel A a a' ->
     rel (𝕃 A) (ret a) (ret a')
-  ret-monotone = {!!}
+  ret-monotone {A = A} = λ a a' a≤a' →
+    LiftRelation.Properties.ord-η-monotone ⟨ A ⟩ ⟨ A ⟩ _ a≤a'
 
   _×rel_ : {A : Type ℓA} {A' : Type ℓA'} {B : Type ℓB} {B' : Type ℓB'} ->
     (R : A -> A' -> Type ℓR1) -> (S : B -> B' -> Type ℓR2) ->
     (p : A × B) -> (p' : A' × B') -> Type (ℓ-max ℓR1 ℓR2)
-  (R ×rel S) (a , b) (a' , b') = R a a' × S b b' --R a a' , S b b' won't work
+  (R ×rel S) (a , b) (a' , b') = R a a' × S b b'
 
   lift×-monotone-het : {A : Poset ℓA ℓ'A} {A' : Poset ℓA' ℓ'A'}
     {B : Poset ℓB ℓ'B} {B' : Poset ℓB' ℓ'B'} ->
@@ -124,7 +125,17 @@ module ClockedProofs (k : Clock) where
     ((_ LiftRelation.≾ _) R ×rel (_ LiftRelation.≾ _) S) (lift× lab) (lift× la'b')
   lift×-monotone-het {A = A} {A' = A'} {B = B} {B' = B'} R S lab la'b' lab≤la'b' =
     let fixed = fix monotone-lift×' in
-    transport {!!} {!!}
+    -- transport⁻Transport
+    transport (sym (λ i → LiftP'.unfold-≾ {!i!} {!!} {!!}))
+      (fixed lab la'b' (transport (λ i → LiftP'.unfold-≾ i lab la'b') lab≤la'b'))
+--(sym λ i → LiftP'.unfold-≾ {!!} {!unfold-lift×-inv i!} {!!})
+{-
+(LiftP1'._≾_ ×rel LiftP2'._≾_) (lift× lab) (lift× la'b') ≡
+      Σ
+      (lift×' (next lift×) lab .fst ≾'P1' lift×' (next lift×) la'b' .fst)
+      (λ _ →
+         lift×' (next lift×) lab .snd ≾'P2' lift×' (next lift×) la'b' .snd)
+-}
     where
       _≾'LA_  = LiftPoset._≾'_ A
       _≾'LA'_ = LiftPoset._≾'_ A'
@@ -142,12 +153,29 @@ module ClockedProofs (k : Clock) where
       monotone-lift×' :
         ▹ ((lab : ⟨ 𝕃 (A ×p B) ⟩) -> (la'b' : ⟨ 𝕃 (A' ×p B') ⟩) ->
           lab ≾'P' la'b' ->
-          (lift×' (next lift×) lab .fst ≾'P1' {!!}) × ({!!} ≾'P2' {!!})) ->
-          -- {!? ≾'P1' ?!} × {! ? ≾'P2' ?!}) ->
+          (lift×' (next lift×) lab .fst ≾'P1' lift×' (next lift×) la'b' .fst)
+          × (lift×' (next lift×) lab .snd ≾'P2' lift×' (next lift×) la'b' .snd)) ->
         (lab : ⟨ 𝕃 (A ×p B) ⟩) -> (la'b' : ⟨ 𝕃 (A' ×p B') ⟩) ->
           lab ≾'P' la'b' ->
-          {!!}
-      monotone-lift×' = {!!}
+          (lift×' (next lift×) lab .fst ≾'P1' lift×' (next lift×) la'b' .fst)
+          × (lift×' (next lift×) lab .snd ≾'P2' lift×' (next lift×) la'b' .snd)
+      monotone-lift×' IH (η (a , b)) (η (a' , b')) (x , y) =
+       transport (λ i → LiftP1'.unfold-≾ i (η a) (η a')) (LiftP1'.Properties.ord-η-monotone x)
+        , transport (λ i → LiftP2'.unfold-≾ i (η b) (η b')) (LiftP2'.Properties.ord-η-monotone y)
+      monotone-lift×' IH ℧ l' l≤l' = tt* , tt*
+      monotone-lift×' IH (θ p) (θ p') l≤l' =
+        (λ t → transport
+          (λ i → (sym LiftP1'.unfold-≾) i
+            ((sym unfold-lift×) i (p t) .fst)
+            ((sym unfold-lift×) i (p' t) .fst))
+          (IH t (p t) (p' t)
+            (transport (λ i → LiftP'.unfold-≾ i (p t) (p' t)) (l≤l' t)) .fst))
+        , λ t → transport
+          (λ i → (sym LiftP2'.unfold-≾) i
+            ((sym unfold-lift×) i (p t) .snd)
+            ((sym unfold-lift×) i (p' t) .snd))
+          (IH t (p t) (p' t)
+            (transport (λ i → LiftP'.unfold-≾ i (p t) (p' t)) (l≤l' t)) .snd)
 
 --todo: follow ext-monotone-het
   lift×-inv-monotone-het : {A : Poset ℓA ℓ'A} {A' : Poset ℓA' ℓ'A'}
@@ -183,7 +211,14 @@ module ClockedProofs (k : Clock) where
         (p : ⟨ 𝕃 A ×p 𝕃 B ⟩) -> (p' : ⟨ 𝕃 A' ×p 𝕃 B' ⟩) ->
           ((p .fst ≾'P1' p' .fst) × (p .snd ≾'P2' p' .snd)) ->
           lift×-inv' (next lift×-inv) p ≾'P' lift×-inv' (next lift×-inv) p'
-      monotone-lift×-inv' IH (η a , η b) (η a' , η b') (la≤la' , lb≤lb') = transport (λ i → LiftP'.unfold-≾ i {!lift×-inv (η a , η b )!} {!!}) {!!}
+      monotone-lift×-inv' IH (η a1 , η b1) (η a2 , η b2) (a1≤a2 , b1≤b2) =
+        transport
+          (λ i → LiftP'.unfold-≾ {!i!} (lift×-inv (η a1 , η b1)) (lift×-inv (η a2 , η b2)))
+          {!!}
+        {-
+        lift×-inv' (next lift×-inv) (η a1 , η b1) ≾'P'
+        lift×-inv' (next lift×-inv) (η a2 , η b2)
+        -}
       monotone-lift×-inv' IH ((η a) , (θ lb~)) ((η a') , (θ lb'~)) (la≤la' , lb≤lb') = {!!}
       monotone-lift×-inv' IH (℧ , _) (℧ , _) (la≤la' , lb≤lb') = {!!}
       monotone-lift×-inv' IH (_ , ℧) (_ , ℧) (la≤la' , lb≤lb') = {!!}
@@ -225,8 +260,7 @@ module ClockedProofs (k : Clock) where
 
 
       monotone-ext' :
-        ▹ (
-            (la : ⟨ 𝕃 A ⟩) -> (la' : ⟨ 𝕃 A' ⟩)  ->
+        ▹ ((la : ⟨ 𝕃 A ⟩) -> (la' : ⟨ 𝕃 A' ⟩)  ->
             (la ≾'LALA' la') ->
             (ext' f  (next (ext f))  la) ≾'LBLB'
             (ext' f' (next (ext f')) la')) ->
@@ -234,11 +268,11 @@ module ClockedProofs (k : Clock) where
           (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)
-        {-transport
+      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*
+        (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
@@ -247,8 +281,6 @@ module ClockedProofs (k : Clock) where
           (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 :
@@ -257,7 +289,8 @@ module ClockedProofs (k : Clock) where
     (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' = {!!}
+  ext-monotone {A = A} {B = B} f f' f≤f' la la' la≤la' =
+    ext-monotone-het {A = A} {A' = A} {B = B} {B' = B} (rel A) (rel B) f f' f≤f' la la' la≤la'
 
   lift×-monotone : {A : Poset ℓA ℓ'A} {B : Poset ℓB ℓ'B} ->
     (l l' : ⟨ 𝕃 (A ×p B) ⟩) ->
@@ -269,7 +302,7 @@ module ClockedProofs (k : Clock) where
     (l l' : ⟨ 𝕃 A ×p 𝕃 B ⟩) ->
     rel (𝕃 A ×p 𝕃 B) l l' ->
     rel (𝕃 (A ×p B)) (lift×-inv l) (lift×-inv l')
-  lift×-inv-monotone = {!!} 
+  lift×-inv-monotone = {!!}
   
   bind-monotone :
     {la la' : ⟨ 𝕃 A ⟩} ->