API tools faq
paste
Advertisement
Guest User

Untitled

a guest
Jul 3rd, 2015
194
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 9.15 KB | None | 0 0
raw download clone embed print report
  1. module Bug where
  2.  
  3. open import Coinduction
  4.  
  5. -- an stype
  6.  
  7. data SType' : Set where
  8. Skip : SType'
  9. Semi : ∞ SType' → ∞ SType' → SType'
  10. Case : ∞ SType' → ∞ SType' → SType'
  11.  
  12. -- equivalence
  13.  
  14. data _∼_ : SType' → SType' → Set where
  15. ∼-Skip : Skip ∼ Skip
  16. ∼-Case : ∀ {s₁ s₁' s₂ s₂'} → ∞ (♭ s₁ ∼ ♭ s₁') → ∞ (♭ s₂ ∼ ♭ s₂') → Case s₁ s₂ ∼ Case s₁' s₂'
  17. ∼-Semi : ∀ {s₁ s₁' s₂ s₂'} → ∞ (♭ s₁ ∼ ♭ s₁') → ∞ (♭ s₂ ∼ ♭ s₂') → Semi s₁ s₂ ∼ Semi s₁' s₂'
  18. ∼-Semi-Skip-Left-Left : ∀ {s₁ s₂ s₃} → ∞ (♭ s₁ ∼ Skip) → ∞ (♭ s₂ ∼ s₃) → Semi s₁ s₂ ∼ s₃
  19. ∼-Semi-Skip-Right-Left : ∀ {s₁ s₂ s₃} → ∞ (♭ s₂ ∼ Skip) → ∞ (♭ s₁ ∼ s₃) → Semi s₁ s₂ ∼ s₃
  20. ∼-Semi-Skip-Left-Right : ∀ {s₁ s₂ s₃} → ∞ (♭ s₁ ∼ Skip) → ∞ (♭ s₂ ∼ s₃) → s₃ ∼ Semi s₁ s₂
  21. ∼-Semi-Skip-Right-Right : ∀ {s₁ s₂ s₃} → ∞ (♭ s₂ ∼ Skip) → ∞ (♭ s₁ ∼ s₃) → s₃ ∼ Semi s₁ s₂
  22. ∼-Semi-Case-Left : ∀ {s₁ s₂ s₃ sl1 sl2 sr}
  23. → ∞ (♭ sl1 ∼ Semi s₁ s₃) → ∞ (♭ sl2 ∼ Semi s₂ s₃) → ∞ (♭ sr ∼ Case s₁ s₂) → Case sl1 sl2 ∼ Semi sr s₃
  24. ∼-Semi-Case-Right : ∀ {s₁ s₂ s₃ sl1 sl2 sr}
  25. → ∞ (♭ sl1 ∼ Semi s₁ s₃) → ∞ (♭ sl2 ∼ Semi s₂ s₃) → ∞ (♭ sr ∼ Case s₁ s₂) → Semi sr s₃ ∼ Case sl1 sl2
  26.  
  27. -- reflexivity
  28.  
  29. ∼-refl : (s : SType') → s ∼ s
  30. ∼-refl Skip = ∼-Skip
  31. ∼-refl (Semi x x₁) = ∼-Semi (♯ ∼-refl (♭ x)) (♯ ∼-refl (♭ x₁))
  32. ∼-refl (Case s₁ s₂) = ∼-Case (♯ ∼-refl (♭ s₁)) (♯ ∼-refl (♭ s₂))
  33.  
  34. -- symmetry
  35.  
  36. ∼-sym : ∀ {s₁ s₂} → s₁ ∼ s₂ → s₂ ∼ s₁
  37. ∼-sym ∼-Skip = ∼-Skip
  38. ∼-sym (∼-Case s₁' s₂') = ∼-Case (♯ ∼-sym (♭ s₁')) (♯ ∼-sym (♭ s₂'))
  39. ∼-sym (∼-Semi s₁' s₂') = ∼-Semi (♯ ∼-sym (♭ s₁')) (♯ ∼-sym (♭ s₂'))
  40. ∼-sym (∼-Semi-Skip-Left-Left s₁∼s₂ s₁∼s₃) = ∼-Semi-Skip-Left-Right s₁∼s₂ s₁∼s₃
  41. ∼-sym (∼-Semi-Skip-Right-Left s₁∼s₂ s₁∼s₃) = ∼-Semi-Skip-Right-Right s₁∼s₂ s₁∼s₃
  42. ∼-sym (∼-Semi-Skip-Left-Right s₁∼s₂ s₁∼s₃) = ∼-Semi-Skip-Left-Left s₁∼s₂ s₁∼s₃
  43. ∼-sym (∼-Semi-Skip-Right-Right s₁∼s₂ s₁∼s₃) = ∼-Semi-Skip-Right-Left s₁∼s₂ s₁∼s₃
  44. ∼-sym (∼-Semi-Case-Left sl1 sl2 sr) = ∼-Semi-Case-Right sl1 sl2 sr
  45. ∼-sym (∼-Semi-Case-Right sl1 sl2 sr) = ∼-Semi-Case-Left sl1 sl2 sr
  46.  
  47. -- transitivity
  48.  
  49. ∼-trans : ∀ {s₁ s₂ s₃} → s₁ ∼ s₂ → s₂ ∼ s₃ → s₁ ∼ s₃
  50. ∼-trans ∼-Skip ∼-Skip = ∼-Skip
  51. ∼-trans ∼-Skip (∼-Semi-Skip-Left-Right x x₁) = ∼-Semi-Skip-Left-Right x x₁
  52. ∼-trans ∼-Skip (∼-Semi-Skip-Right-Right x x₁) = ∼-Semi-Skip-Right-Right x x₁
  53. ∼-trans (∼-Case x x₁) (∼-Case x₂ x₃) = ∼-Case (♯ ∼-trans (♭ x) (♭ x₂)) (♯ ∼-trans (♭ x₁) (♭ x₃))
  54. ∼-trans (∼-Case x x₁) (∼-Semi-Skip-Left-Right x₂ x₃) = ∼-Semi-Skip-Left-Right x₂ (♯ ∼-trans (♭ x₃) (∼-Case (♯ ∼-sym (♭ x)) (♯ ∼-sym (♭ x₁))))
  55. ∼-trans (∼-Case x x₁) (∼-Semi-Skip-Right-Right x₂ x₃) = ∼-Semi-Skip-Right-Right x₂ (♯ ∼-trans (♭ x₃) (∼-Case (♯ ∼-sym (♭ x)) (♯ ∼-sym (♭ x₁))))
  56. ∼-trans (∼-Case x x₁) (∼-Semi-Case-Left x₂ x₃ x₄) = ∼-Semi-Case-Left (♯ ∼-trans (♭ x) (♭ x₂)) (♯ ∼-trans (♭ x₁) (♭ x₃)) x₄
  57. ∼-trans (∼-Semi x x₁) (∼-Semi x₂ x₃) = ∼-Semi (♯ ∼-trans (♭ x) (♭ x₂)) (♯ ∼-trans (♭ x₁) (♭ x₃))
  58. ∼-trans (∼-Semi x x₁) (∼-Semi-Skip-Left-Left x₂ x₃) = ∼-Semi-Skip-Left-Left (♯ ∼-trans (♭ x) (♭ x₂)) (♯ ∼-trans (♭ x₁) (♭ x₃))
  59. ∼-trans (∼-Semi x x₁) (∼-Semi-Skip-Right-Left x₂ x₃) = ∼-Semi-Skip-Right-Left (♯ ∼-trans (♭ x₁) (♭ x₂)) (♯ ∼-trans (♭ x) (♭ x₃))
  60. ∼-trans (∼-Semi x x₁) (∼-Semi-Skip-Left-Right x₂ x₃) = ∼-Semi-Skip-Left-Right x₂ (♯ ∼-trans (♭ x₃) (∼-Semi (♯ ∼-sym (♭ x)) (♯ ∼-sym (♭ x₁))))
  61. ∼-trans (∼-Semi x x₁) (∼-Semi-Skip-Right-Right x₂ x₃) = ∼-Semi-Skip-Right-Right x₂ (♯ ∼-trans (♭ x₃) (∼-Semi (♯ ∼-sym (♭ x)) (♯ ∼-sym (♭ x₁))))
  62. ∼-trans (∼-Semi x x₁) (∼-Semi-Case-Right x₂ x₃ x₄) = ∼-Semi-Case-Right (♯ ∼-trans (♭ x₂) (∼-Semi (♯ ∼-refl _) (♯ ∼-sym (♭ x₁)))) (♯ ∼-trans (♭ x₃) (∼-Semi (♯ ∼-refl _) (♯ ∼-sym (♭ x₁)))) (♯ ∼-trans (♭ x) (♭ x₄))
  63. ∼-trans (∼-Semi-Skip-Left-Left x x₁) ∼-Skip = ∼-Semi-Skip-Left-Left x x₁
  64. ∼-trans (∼-Semi-Skip-Left-Left x x₁) (∼-Case x₂ x₃) = ∼-Semi-Skip-Left-Left x (♯ ∼-trans (♭ x₁) (∼-Case x₂ x₃))
  65. ∼-trans (∼-Semi-Skip-Left-Left x x₁) (∼-Semi x₂ x₃) = ∼-Semi-Skip-Left-Left x (♯ ∼-trans (♭ x₁) (∼-Semi x₂ x₃))
  66. ∼-trans (∼-Semi-Skip-Left-Left x x₁) (∼-Semi-Skip-Left-Left x₂ x₃) = ∼-Semi-Skip-Left-Left x (♯ ∼-trans (♭ x₁) (∼-Semi-Skip-Left-Left x₂ x₃))
  67. ∼-trans (∼-Semi-Skip-Left-Left x x₁) (∼-Semi-Skip-Right-Left x₂ x₃) = ∼-Semi-Skip-Left-Left x (♯ ∼-trans (♭ x₁) (∼-Semi-Skip-Right-Left x₂ x₃))
  68. ∼-trans (∼-Semi-Skip-Left-Left x x₁) (∼-Semi-Skip-Left-Right x₂ x₃) = ∼-Semi-Skip-Left-Left x (♯ ∼-trans (♭ x₁) (∼-Semi-Skip-Left-Right x₂ x₃))
  69. ∼-trans (∼-Semi-Skip-Left-Left x x₁) (∼-Semi-Skip-Right-Right x₂ x₃) = ∼-Semi-Skip-Left-Left x (♯ ∼-trans (♭ x₁) (∼-Semi-Skip-Right-Right x₂ x₃))
  70. ∼-trans (∼-Semi-Skip-Left-Left x x₁) (∼-Semi-Case-Left x₂ x₃ x₄) = ∼-Semi-Skip-Left-Left x (♯ ∼-trans (♭ x₁) (∼-Semi-Case-Left x₂ x₃ x₄))
  71. ∼-trans (∼-Semi-Skip-Left-Left x x₁) (∼-Semi-Case-Right x₂ x₃ x₄) = ∼-Semi-Skip-Left-Left x (♯ ∼-trans (♭ x₁) (∼-Semi-Case-Right x₂ x₃ x₄))
  72. ∼-trans (∼-Semi-Skip-Right-Left x x₁) ∼-Skip = ∼-Semi-Skip-Right-Left x x₁
  73. ∼-trans (∼-Semi-Skip-Right-Left x x₁) (∼-Case x₂ x₃) = ∼-Semi-Skip-Right-Left x (♯ ∼-trans (♭ x₁) (∼-Case x₂ x₃))
  74. ∼-trans (∼-Semi-Skip-Right-Left x x₁) (∼-Semi x₂ x₃) = ∼-Semi-Skip-Right-Left x (♯ ∼-trans (♭ x₁) (∼-Semi x₂ x₃))
  75. ∼-trans (∼-Semi-Skip-Right-Left x x₁) (∼-Semi-Skip-Left-Left x₂ x₃) = {!!}
  76. ∼-trans (∼-Semi-Skip-Right-Left x x₁) (∼-Semi-Skip-Right-Left x₂ x₃) = {!!}
  77. ∼-trans (∼-Semi-Skip-Right-Left x x₁) (∼-Semi-Skip-Left-Right x₂ x₃) = {!!}
  78. ∼-trans (∼-Semi-Skip-Right-Left x x₁) (∼-Semi-Skip-Right-Right x₂ x₃) = {!!}
  79. ∼-trans (∼-Semi-Skip-Right-Left x x₁) (∼-Semi-Case-Left x₂ x₃ x₄) = {!!}
  80. ∼-trans (∼-Semi-Skip-Right-Left x x₁) (∼-Semi-Case-Right x₂ x₃ x₄) = {!!}
  81. ∼-trans (∼-Semi-Skip-Left-Right x x₁) (∼-Semi x₂ x₃) = ∼-Semi-Skip-Left-Right (♯ ∼-trans (∼-sym (♭ x₂)) (♭ x)) (♯ ∼-trans (∼-sym (♭ x₃)) (♭ x₁))
  82. ∼-trans (∼-Semi-Skip-Left-Right x x₁) (∼-Semi-Skip-Left-Left x₂ x₃) = {!!}
  83. ∼-trans (∼-Semi-Skip-Left-Right x x₁) (∼-Semi-Skip-Right-Left x₂ x₃) = {!!}
  84. ∼-trans (∼-Semi-Skip-Left-Right x x₁) (∼-Semi-Skip-Left-Right x₂ x₃) = {!!}
  85. ∼-trans (∼-Semi-Skip-Left-Right x x₁) (∼-Semi-Skip-Right-Right x₂ x₃) = {!!}
  86. ∼-trans (∼-Semi-Skip-Left-Right x x₁) (∼-Semi-Case-Right x₂ x₃ x₄) = {!!}
  87. ∼-trans (∼-Semi-Skip-Right-Right x x₁) (∼-Semi x₂ x₃) = ∼-Semi-Skip-Right-Right (♯ ∼-trans (∼-sym (♭ x₃)) (♭ x)) (♯ ∼-trans (∼-sym (♭ x₂)) (♭ x₁))
  88. ∼-trans (∼-Semi-Skip-Right-Right x x₁) (∼-Semi-Skip-Left-Left x₂ x₃) = {!!}
  89. ∼-trans (∼-Semi-Skip-Right-Right x x₁) (∼-Semi-Skip-Right-Left x₂ x₃) = {!!}
  90. ∼-trans (∼-Semi-Skip-Right-Right x x₁) (∼-Semi-Skip-Left-Right x₂ x₃) = {!!}
  91. ∼-trans (∼-Semi-Skip-Right-Right x x₁) (∼-Semi-Skip-Right-Right x₂ x₃) = {!!}
  92. ∼-trans (∼-Semi-Skip-Right-Right x x₁) (∼-Semi-Case-Right x₂ x₃ x₄) = {!!}
  93. ∼-trans (∼-Semi-Case-Left x x₁ x₂) (∼-Semi x₃ x₄) = ∼-Semi-Case-Left {!!} (♯ ∼-trans (♭ x₁) (∼-Semi (♯ ∼-refl _) x₄)) (♯ ∼-trans (∼-sym (♭ x₃)) (♭ x₂))
  94. ∼-trans (∼-Semi-Case-Left x x₁ x₂) (∼-Semi-Skip-Left-Left x₃ x₄) = {!!}
  95. ∼-trans (∼-Semi-Case-Left x x₁ x₂) (∼-Semi-Skip-Right-Left x₃ x₄) = {!!}
  96. ∼-trans (∼-Semi-Case-Left x x₁ x₂) (∼-Semi-Skip-Left-Right x₃ x₄) = {!!}
  97. ∼-trans (∼-Semi-Case-Left x x₁ x₂) (∼-Semi-Skip-Right-Right x₃ x₄) = {!!}
  98. ∼-trans (∼-Semi-Case-Left x x₁ x₂) (∼-Semi-Case-Right x₃ x₄ x₅) = {!!}
  99. ∼-trans (∼-Semi-Case-Right x x₁ x₂) (∼-Case x₃ x₄) = ∼-Semi-Case-Right (♯ ∼-trans (∼-sym (♭ x₃)) (♭ x)) (♯ ∼-trans (∼-sym (♭ x₄)) (♭ x₁)) x₂
  100. ∼-trans (∼-Semi-Case-Right x x₁ x₂) (∼-Semi-Skip-Left-Right x₃ x₄) = {!!}
  101. ∼-trans (∼-Semi-Case-Right x x₁ x₂) (∼-Semi-Skip-Right-Right x₃ x₄) = {!!}
  102. ∼-trans (∼-Semi-Case-Right x x₁ x₂) (∼-Semi-Case-Left x₃ x₄ x₅) = {!!}
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!