Bisimulation for Conat (one way)

agda · Feb 5, 2019 · 31f7de1 · 31f7de1
1 parent 6b35102
commit 31f7de1
Show file tree

Hide file tree

Showing 2 changed files with 32 additions and 9 deletions.
diff --git a/Cubical/Codata/Conat/Base.agda b/Cubical/Codata/Conat/Base.agda
@@ -7,16 +7,15 @@ open import Cubical.Data.Sum
 open import Cubical.Core.Everything
 
 record Conat : Set
-Prev = Unit ⊎ Conat
+Conat′ = Unit ⊎ Conat
 record Conat where
   coinductive
   constructor conat
-  field prev : Prev
+  field force : Conat′
 open Conat public
 
 pattern zero  = inl tt
 pattern suc n = inr n
 
 succ : Conat → Conat
-prev (succ a) = inr a
-
+force (succ a) = inr a
diff --git a/Cubical/Codata/Conat/Properties.agda b/Cubical/Codata/Conat/Properties.agda
@@ -3,16 +3,17 @@ module Cubical.Codata.Conat.Properties where
 
 open import Cubical.Data.Unit
 open import Cubical.Data.Sum
+open import Cubical.Data.Empty
 
 open import Cubical.Core.Everything
 
 open import Cubical.Codata.Conat.Base
 
-Unwrap-prev : Prev -> Set
+Unwrap-prev : Conat′ -> Set
 Unwrap-prev  zero   = Unit
 Unwrap-prev (suc _) = Conat
 
-unwrap-prev : (n : Prev) -> Unwrap-prev n
+unwrap-prev : (n : Conat′) -> Unwrap-prev n
 unwrap-prev  zero   = _
 unwrap-prev (suc x) = x
 
@@ -24,17 +25,40 @@ private -- tests
   succOne≡two : succ one ≡ two
   succOne≡two i = two
 
-  predTwo≡one : unwrap-prev (prev two) ≡ one
+  predTwo≡one : unwrap-prev (force two) ≡ one
   predTwo≡one i = one
 
 ∞ : Conat
-prev ∞ = suc ∞
+force ∞ = suc ∞
 
 ∞+1≡∞ : succ ∞ ≡ ∞
-prev (∞+1≡∞ _) = suc ∞
+force (∞+1≡∞ _) = suc ∞
 
 ∞+2≡∞ : succ (succ ∞) ≡ ∞
 ∞+2≡∞ = compPath (cong succ ∞+1≡∞) ∞+1≡∞
 
 -- TODO: plus for conat, ∞ + ∞ ≡ ∞
 
+mutual
+  record _~_ (x y : Conat) : Set where
+    coinductive
+    field
+      force : force x ~′ force y
+
+
+  _~′_ : Conat′ → Conat′ → Set
+  (inl _) ~′ (inl _) = Unit
+  (inr x) ~′ (inr y) = x ~ y
+  _ ~′ _ = ⊥
+
+open _~_ public
+
+mutual
+  bisim : ∀ {x y} → x ~ y → x ≡ y
+  force (bisim {x} {y} eq i) = bisim′ (force eq) i
+
+  bisim′ : ∀ {x y} → x ~′ y → x ≡ y
+  bisim′ {zero} {zero} eq = refl
+  bisim′ {zero} {suc x} ()
+  bisim′ {suc x} {zero} ()
+  bisim′ {suc x} {suc y} eq i = suc (bisim eq i)