general results involving clocks

formalizations/guarded-cubical/Common/ClockProperties.agda

+{-# OPTIONS --rewriting --guarded #-}
+
+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+module Common.ClockProperties where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Data.Sum
+open import Cubical.Data.Sigma
+open import Cubical.Data.Bool hiding (_≤_)
+open import Cubical.Relation.Nullary
+open import Cubical.Data.Unit
+
+open import Cubical.Foundations.Isomorphism
+
+open import Common.Common
+open import Common.Later
+
+open import Agda.Builtin.Equality renaming (_≡_ to _≣_) hiding (refl)
+open import Agda.Builtin.Equality.Rewrite
+open import Cubical.Data.Equality.Conversion hiding (Iso ; funExt)
+-- open import Cubical.Data.Prod
+
+private
+  variable
+    ℓ ℓ' : Level
+
+
+{- remove -}
+
+-- Rewriting axioms used in the proofs:
+
+path-clock-irrel-bool-1 : {k k' : Clock} -> (b : Bool) ->
+  bool-clock-irrel (λ _ -> b) k k' ≡ refl
+path-clock-irrel-bool-1 b = isSetBool b b _ refl
+
+rewrite-clock-irrel-bool-1 : {k k' : Clock} -> (b : Bool) ->
+  bool-clock-irrel (λ _ -> b) k k' ≣ refl
+rewrite-clock-irrel-bool-1 {k = k} {k' = k'} b =
+  pathToEq (path-clock-irrel-bool-1 b)
+-- clock-irrel-beta-const bool-clock-irrel b k k'
+
+path-clock-irrel-bool-2 :
+    (M : Clock -> Bool) -> bool-clock-irrel M k0 k0 ≡ refl
+path-clock-irrel-bool-2 M =
+  isSetBool (M k0) (M k0) (bool-clock-irrel M k0 k0) refl
+
+rewrite-clock-irrel-bool-2 :
+    (M : Clock -> Bool) -> bool-clock-irrel M k0 k0 ≣ refl
+rewrite-clock-irrel-bool-2 M =
+  pathToEq (path-clock-irrel-bool-2 M)
+-- clock-irrel-beta-k0 bool-clock-irrel
+
+rewrite-force : ∀ {ℓ : Level} -> {A : Clock -> Type ℓ} (f : ∀ k -> A k) →
+  force' (λ k -> next (f k)) ≣ f
+rewrite-force f = pathToEq (force'-beta f)
+
+rewrite-transp : ∀ {ℓ : Level} {X : Type ℓ} →
+  transp (λ i → X) i0 ≣ id
+rewrite-transp = pathToEq (funExt (λ x -> transportRefl x))
+
+{-# REWRITE rewrite-clock-irrel-bool-1 #-}
+
+{-# REWRITE rewrite-clock-irrel-bool-2 #-}
+
+{-# REWRITE rewrite-force #-}
+
+{-# REWRITE rewrite-transp #-}
+
+
+{- end remove -}
+
+{- Iso definitions used in this file:
+
+ _Iso⟨_⟩_  : {ℓ ℓ' ℓ'' : Level} {B : Type ℓ'} {C : Type ℓ''}
+              (X : Type ℓ) →
+              Iso X B → Iso B C → Iso X C
+  _∎Iso     : {ℓ : Level} (A : Type ℓ) → Iso A A
+
+
+   Σ-Π-Iso   : {ℓ ℓ' ℓ'' : Level} {A : Type ℓ} {B : A → Type ℓ'}
+              {C : (a : A) → B a → Type ℓ''} →
+              Iso ((a : A) → Σ-syntax (B a) (C a))
+                  (Σ-syntax ((a : A) → B a) (λ f → (a : A) → C a (f a)))
+
+   codomainIsoDep
+            : {ℓ ℓ' ℓ'' : Level} {A : Type ℓ} {B : A → Type ℓ'}
+              {C : A → Type ℓ''} →
+              ((a : A) → Iso (B a) (C a)) → Iso ((a : A) → B a) ((a : A) → C a)
+
+   ⊎Iso      : {A.ℓa : Level} {A : Type A.ℓa} {C.ℓc : Level}
+              {C : Type C.ℓc} {B.ℓb : Level} {B : Type B.ℓb} {D.ℓd : Level}
+              {D : Type D.ℓd} →
+              Iso A C → Iso B D → Iso (A ⊎ B) (C ⊎ D)
+
+  Σ-cong-iso-fst
+            : {A.ℓ : Level} {A : Type A.ℓ} {B..1 : Level} {A' : Type B..1}
+              {B.ℓ : Level} {B : A' → Type B.ℓ} (isom : Iso A A') →
+              Iso (Σ A (B ∘ Iso.fun isom)) (Σ A' B)
+
+  Σ-cong-iso-snd
+            : {B'..1 : Level} {A : Type B'..1} {B.ℓ : Level} {B : A → Type B.ℓ}
+              {B'.ℓ : Level} {B' : A → Type B'.ℓ} →
+              ((x : A) → Iso (B x) (B' x)) → Iso (Σ A B) (Σ A B')
+
+-}
+
+
+-- The unit type is clock-irrelevant.
+Unit-clock-irrel : clock-irrel Unit
+Unit-clock-irrel M k k' with M k | M k'
+...  | tt | tt = refl
+
+
+
+bool2ty : Type ℓ -> Type ℓ -> Bool -> Type ℓ
+bool2ty A B true = A
+bool2ty A B false = B
+
+bool2ty-eq : {X : Type ℓ} {A B : X -> Type ℓ'} ->
+  (b : Bool) ->
+  (∀ (x : X) -> bool2ty (A x) (B x) b) ≡
+  bool2ty (∀ x -> A x) (∀ x -> B x) b
+bool2ty-eq {X} {A} {B} true = refl
+bool2ty-eq {X} {A} {B} false = refl
+
+bool2ty-A-A : (A : Type ℓ) (b : Bool) -> bool2ty A A b ≡ A
+bool2ty-A-A A true = refl
+bool2ty-A-A A false = refl
+
+
+Iso-⊎-ΣBool : {A B : Type ℓ} -> Iso (A ⊎ B) (Σ Bool (λ b -> bool2ty A B b))
+Iso-⊎-ΣBool {A = A} {B = B} = iso to inv sec retr
+  where
+    to : A ⊎ B → Σ Bool (λ b -> bool2ty A B b)
+    to (inl a) = true , a
+    to (inr b) = false , b
+
+    inv : Σ Bool (bool2ty A B) → A ⊎ B
+    inv (true , a) = inl a
+    inv (false , b) = inr b
+
+    sec : section to inv
+    sec (true , a) = refl
+    sec (false , b) = refl
+
+    retr : retract to inv
+    retr (inl a) = refl
+    retr (inr b) = refl
+
+
+
+∀clock-Σ : {A : Type} -> {B : A -> Clock -> Type} ->
+    clock-irrel A ->
+    (∀ (k : Clock) -> Σ A (λ a -> B a k)) ->
+    Σ A (λ a -> ∀ (k : Clock) -> B a k)
+∀clock-Σ {A} {B} H-clk-irrel p =
+    let a = fst (p k0) in
+      a , (λ k -> transport
+                   (λ i → B (H-clk-irrel (fst ∘ p) k k0 i) k)
+                   (snd (p k)))
+  -- NTS:  B (fst (p k)) k ≡ B (fst (p k0)) k
+  -- i.e. essentially need to show that fst (p k) ≡ fst (p k0)
+  -- This follows from clock irrelevance for A, with M = fst ∘ p of type Clock -> A
+
+
+
+
+Dist-Pi-Sigma : {S : Type} -> {A : S -> Type} -> {B : (s : S) -> A s -> Type} ->
+  Iso (∀ (s : S) -> (Σ[ x ∈ A s ] B s x))
+      (Σ[ x ∈ (∀ s -> A s) ] ( ∀ s -> B s (x s) ))
+Dist-Pi-Sigma = Σ-Π-Iso
+
+-- Turn an equality into an iso.
+Eq-Iso : {A B : Type ℓ} ->
+  A ≡ B -> Iso A B
+Eq-Iso {A = A} {B = B} H-eq = subst (Iso A) H-eq idIso
+-- same as: transport (cong (Iso A) H-eq) idIso
+
+
+-- Clock quantification distributes over products.
+Iso-∀clock-× : {A B : Clock → Type ℓ} →
+  Iso (∀ k → A k × B k) ((∀ k → A k) × (∀ k → B k))
+Iso.fun Iso-∀clock-× f = (λ k → f k .fst) , (λ k → f k .snd)
+Iso.inv Iso-∀clock-× (f , g) = λ k → f k , g k
+Iso.rightInv Iso-∀clock-× (f , g) = refl
+Iso.leftInv Iso-∀clock-× f = refl
+
+
+
+-- Clock quantification distributes over sigma types.
+-- This is simply an instance of the usual distributivity
+-- of pi-types over sigma types.
+∀k-Σ : {A : Clock → Type ℓ} → {B : (k : Clock) → A k → Type ℓ'} →
+  Iso
+    (∀ (k : Clock) → Σ (A k) (λ a → B k a))
+    (Σ (∀ k → A k) (λ f → ∀ k → B k (f k)))
+∀k-Σ {A = A} {B = B} = Σ-Π-Iso {A = Clock} {B = A} {C = B}
+
+
+-- Special case where the first type in the sigma is
+-- clock-irrelevant.
+Iso-∀clock-Σ : {A : Type ℓ} -> {B : A -> Clock -> Type ℓ'} ->
+  clock-irrel A ->
+  Iso
+    (∀ (k : Clock) -> Σ A (λ a -> B a k))
+    (Σ A (λ a -> ∀ (k : Clock) -> B a k))
+Iso-∀clock-Σ {A = A} {B = B} H-clk-irrel =
+  (∀ (k : Clock) -> Σ A (λ a -> B a k))
+     Iso⟨ Σ-Π-Iso {A = Clock} {B = λ k -> A} {C = λ k a -> B a k} ⟩
+     
+  (Σ ((k : Clock) → A) (λ f → (k : Clock) → B (f k) k))
+     Iso⟨ ( Σ-cong-iso-snd (λ f → codomainIsoDep (λ k → Eq-Iso (λ i → B (H-clk-irrel f k k0 i) k)))) ⟩
+
+  (Σ ((k : Clock) → A) (λ f → (k : Clock) → B (f k0) k))
+     Iso⟨ Σ-cong-iso-fst {B = λ a -> ∀ k' -> B a k'} (Iso-∀kA-A H-clk-irrel) ⟩
+     
+  (Σ A (λ a -> ∀ (k : Clock) -> B a k)) ∎Iso
+
+{- Note:
+          Σ-cong-iso-fst
+            : {A.ℓ : Level} {A : Type A.ℓ} {B..1 : Level} {A' : Type B..1}
+              {B.ℓ : Level} {B : A' → Type B.ℓ} (isom : Iso A A') →
+              Iso (Σ A (B ∘ Iso.fun isom)) (Σ A' B)
+
+    In this case, the isomorphism function associated with Iso-∀kA-A
+    takes f : (∀ (k : Clock) -> A) to A by applying f to k0.
+    This is why we need the intermediate step of transforming B (f k) k
+    into B (f k0) k.
+
+-}
+
+
+-- Action of the above isomorphism
+Iso-∀clock-Σ-fun : {A : Type ℓ} {B : A -> Clock -> Type ℓ'} ->
+  (H : clock-irrel A) ->
+  (f : (k : Clock) -> Σ A (λ a -> B a k)) ->
+  Iso.fun (Iso-∀clock-Σ {A = A} {B = B} H) f ≡ (fst (f k0) , λ k -> {!f k .snd!})
+Iso-∀clock-Σ-fun {A = A} {B = B} H f = ΣPathP (refl , (funExt (λ k -> {!!} ∙ {!!})))
+
+
+-- Clock quantification distributes over coproducts.
+Iso-Π-⊎-clk : {A B : Clock -> Type ℓ} ->
+  Iso
+    ((k : Clock) -> (A k ⊎ B k))
+    (((k : Clock) -> A k) ⊎ ((k : Clock) -> B k))
+Iso-Π-⊎-clk {A = A} {B = B} =
+  (∀ (k : Clock) -> (A k ⊎ B k))
+    Iso⟨ codomainIsoDep (λ k -> Iso-⊎-ΣBool) ⟩
+  (∀ (k : Clock) -> Σ[ b ∈ Bool ] bool2ty (A k) (B k) b )
+    Iso⟨ Iso-∀clock-Σ bool-clock-irrel ⟩
+  (Σ[ b ∈ Bool ] ∀ k -> bool2ty (A k) (B k) b)
+    Iso⟨ Σ-cong-iso-snd (λ b → Eq-Iso (bool2ty-eq b)) ⟩
+    --  (cong (Iso ((x : Clock) → bool2ty (A x) (B x) b)) (bool2ty-eq b))
+  (Σ[ b ∈ Bool ] bool2ty (∀ k -> A k) (∀ k -> B k) b)
+    Iso⟨ invIso Iso-⊎-ΣBool ⟩
+  (∀ k -> A k) ⊎ (∀ k -> B k) ∎Iso
+
+-- Action of the above isomorphism
+Iso-Π-⊎-clk-fun : {A B : Clock -> Type} -> {f : (k : Clock) -> (A k ⊎ B k) } ->
+  (H : ∀ k -> Σ[ a ∈ A k ] f k ≡ inl a) ->
+  Iso.fun Iso-Π-⊎-clk f ≡ inl λ k -> H k .fst
+Iso-Π-⊎-clk-fun {A} {B} {f} H = {!!}
+
+Iso-Π-⊎-clk-inv-inl : {A B : Clock -> Type} ->
+  {f : (k : Clock) → A k} ->
+  Iso.inv (Iso-Π-⊎-clk {B = B}) (inl f) ≡ λ k -> inl (f k)
+Iso-Π-⊎-clk-inv-inl {A = A} {B = B} {f = f} = funExt (λ k → cong inl {!!})
+-- (s : ((k : Clock) → A k) ⊎ ((k : Clock) → B k)) ->
+
+-- transport p a = transp (λ i → p i) i0 a
+--
+-- transp (λ i → A (transp (λ j → Clock) i k)) i0 (transp (λ i → A (transp (λ j → Clock) i k)) i0 (f k))
+
+-- transport (λ i → A (transp (λ j → Clock) i k))
+
+test :  {A B : Clock -> Type ℓ} → (((k : Clock) -> A k) ⊎ ((k : Clock) -> B k)) → ((k : Clock) -> (A k ⊎ B k))
+test (inl f) k = inl (f k)
+test (inr g) k = inr (g k)
+
+test' :  {A B : Clock -> Type ℓ} → ((k : Clock) -> (A k ⊎ B k)) → (((k : Clock) -> A k) ⊎ ((k : Clock) -> B k))
+test' {A = A} {B = B} f = aux (f k0)
+  where
+    aux : A k0 ⊎ B k0 → _
+    aux (inl a) = inl (λ k → {!!})
+    aux (inr b) = inr (λ k → {!!})