From b176f8e6f75ec34eb8e3e6259a3b9bb245f7868c Mon Sep 17 00:00:00 2001
From: akaiDing <tingtind@umich.edu>
Date: Fri, 13 Oct 2023 20:09:25 -0400
Subject: [PATCH] Add lemmas for representable relation
---
.../Semantics/Concrete/DynNew.agda | 94 +++++++++++++++++--
.../Concrete/MonotonicityProofs.agda | 71 ++++++++++----
2 files changed, 138 insertions(+), 27 deletions(-)
diff --git a/formalizations/guarded-cubical/Semantics/Concrete/DynNew.agda b/formalizations/guarded-cubical/Semantics/Concrete/DynNew.agda
index fad9ca3..22b665b 100644
--- a/formalizations/guarded-cubical/Semantics/Concrete/DynNew.agda
+++ b/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)
diff --git a/formalizations/guarded-cubical/Semantics/Concrete/MonotonicityProofs.agda b/formalizations/guarded-cubical/Semantics/Concrete/MonotonicityProofs.agda
index 07948b8..7a9f763 100644
--- a/formalizations/guarded-cubical/Semantics/Concrete/MonotonicityProofs.agda
+++ b/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 ⟩} ->
--
GitLab