[Agda] Agda dies trying to prove transitivity

[Peter Thiemann]

Hi all,

I'm looking at a coinductively defined type

data SType' : Set where
  Skip : SType'
  Semi : ∞ SType' → ∞ SType' → SType'
  Case : ∞ SType' → ∞ SType' → SType'

for which I want to establish a non-trivial equivalence relation 

data _∼_ : SType' → SType' → Set where
  ∼-Skip : Skip ∼ Skip
  ∼-Case : ∀ {s₁ s₁' s₂ s₂'} → ∞ (♭ s₁ ∼ ♭ s₁') → ∞ (♭ s₂ ∼ ♭ s₂') → Case s₁ s₂ ∼ Case s₁' s₂'
  ∼-Semi : ∀ {s₁ s₁' s₂ s₂'} → ∞ (♭ s₁ ∼ ♭ s₁') → ∞ (♭ s₂ ∼ ♭ s₂') → Semi s₁ s₂ ∼ Semi s₁' s₂'
  ∼-Semi-Skip-Left-Left : ∀ {s₁ s₂ s₃} → ∞ (♭ s₁ ∼ Skip) → ∞ (♭ s₂ ∼ s₃) → Semi s₁ s₂ ∼ s₃
  ∼-Semi-Skip-Right-Left : ∀ {s₁ s₂ s₃} → ∞ (♭ s₂ ∼ Skip) → ∞ (♭ s₁ ∼ s₃) → Semi s₁ s₂ ∼ s₃
  ∼-Semi-Skip-Left-Right : ∀ {s₁ s₂ s₃} → ∞ (♭ s₁ ∼ Skip) → ∞ (♭ s₂ ∼ s₃) → s₃ ∼ Semi s₁ s₂
  ∼-Semi-Skip-Right-Right : ∀ {s₁ s₂ s₃} → ∞ (♭ s₂ ∼ Skip) → ∞ (♭ s₁ ∼ s₃) → s₃ ∼ Semi s₁ s₂
  ∼-Semi-Case-Left : ∀ {s₁ s₂ s₃ sl1 sl2 sr} 
    → ∞ (♭ sl1 ∼ Semi s₁ s₃) → ∞ (♭ sl2 ∼ Semi s₂ s₃) → ∞ (♭ sr ∼ Case s₁ s₂) → Case sl1 sl2 ∼ Semi sr s₃
  ∼-Semi-Case-Right : ∀ {s₁ s₂ s₃ sl1 sl2 sr}
    → ∞ (♭ sl1 ∼ Semi s₁ s₃) → ∞ (♭ sl2 ∼ Semi s₂ s₃) → ∞ (♭ sr ∼ Case s₁ s₂) → Semi sr s₃ ∼ Case sl1 sl2

When it comes to proving the equivalence properties, reflexivity and symmetry are straightforward, but for transitivity
I run into problems with Agda. I particular, as soon as I have proved some number of cases, the type checker does not appear to 
terminate any more. 
Is there something obviously wrong about these definitions?
The full code may be found here: https://gist.github.com/28c0643956315b70c0e6.git

I'm running version 2.3.2.2

-Peter


-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150604/4b0d91bc/attachment.html