<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">Hi all,<div><br></div><div>I'm looking at a coinductively defined type</div><div><br></div><div><pre class="line-pre" style="box-sizing: border-box; font-family: Consolas, 'Liberation Mono', Menlo, Courier, monospace; font-size: 12px; margin-top: 0px; margin-bottom: 0px; width: 1525px; color: rgb(51, 51, 51); line-height: 16.7999992370605px; widows: 1; background-color: rgb(255, 255, 255); position: static; z-index: auto; "><div class="line" id="file-transitivity-LC7" style="box-sizing: border-box;">data SType' : Set where
</div><div class="line" id="file-transitivity-LC8" style="box-sizing: border-box;"> Skip : SType'
</div><div class="line" id="file-transitivity-LC9" style="box-sizing: border-box;"> Semi : ∞ SType' → ∞ SType' → SType'
</div><div class="line" id="file-transitivity-LC10" style="box-sizing: border-box;"> Case : ∞ SType' → ∞ SType' → SType'</div></pre></div><div><br></div><div>for which I want to establish a non-trivial equivalence relation </div><div><br></div><div><pre class="line-pre" style="box-sizing: border-box; font-family: Consolas, 'Liberation Mono', Menlo, Courier, monospace; font-size: 12px; margin-top: 0px; margin-bottom: 0px; width: 1525px; color: rgb(51, 51, 51); line-height: 16.7999992370605px; widows: 1; background-color: rgb(255, 255, 255); position: static; z-index: auto; "><div class="line" id="file-transitivity-LC14" style="box-sizing: border-box;">data _∼_ : SType' → SType' → Set where
</div><div class="line" id="file-transitivity-LC15" style="box-sizing: border-box;"> ∼-Skip : Skip ∼ Skip
</div><div class="line" id="file-transitivity-LC16" style="box-sizing: border-box;"> ∼-Case : ∀ {s₁ s₁' s₂ s₂'} → ∞ (♭ s₁ ∼ ♭ s₁') → ∞ (♭ s₂ ∼ ♭ s₂') → Case s₁ s₂ ∼ Case s₁' s₂'
</div><div class="line" id="file-transitivity-LC17" style="box-sizing: border-box;"> ∼-Semi : ∀ {s₁ s₁' s₂ s₂'} → ∞ (♭ s₁ ∼ ♭ s₁') → ∞ (♭ s₂ ∼ ♭ s₂') → Semi s₁ s₂ ∼ Semi s₁' s₂'
</div><div class="line" id="file-transitivity-LC18" style="box-sizing: border-box;"> ∼-Semi-Skip-Left-Left : ∀ {s₁ s₂ s₃} → ∞ (♭ s₁ ∼ Skip) → ∞ (♭ s₂ ∼ s₃) → Semi s₁ s₂ ∼ s₃
</div><div class="line" id="file-transitivity-LC19" style="box-sizing: border-box;"> ∼-Semi-Skip-Right-Left : ∀ {s₁ s₂ s₃} → ∞ (♭ s₂ ∼ Skip) → ∞ (♭ s₁ ∼ s₃) → Semi s₁ s₂ ∼ s₃
</div><div class="line" id="file-transitivity-LC20" style="box-sizing: border-box;"> ∼-Semi-Skip-Left-Right : ∀ {s₁ s₂ s₃} → ∞ (♭ s₁ ∼ Skip) → ∞ (♭ s₂ ∼ s₃) → s₃ ∼ Semi s₁ s₂
</div><div class="line" id="file-transitivity-LC21" style="box-sizing: border-box;"> ∼-Semi-Skip-Right-Right : ∀ {s₁ s₂ s₃} → ∞ (♭ s₂ ∼ Skip) → ∞ (♭ s₁ ∼ s₃) → s₃ ∼ Semi s₁ s₂
</div><div class="line" id="file-transitivity-LC22" style="box-sizing: border-box;"> ∼-Semi-Case-Left : ∀ {s₁ s₂ s₃ sl1 sl2 sr}
</div><div class="line" id="file-transitivity-LC23" style="box-sizing: border-box;"> → ∞ (♭ sl1 ∼ Semi s₁ s₃) → ∞ (♭ sl2 ∼ Semi s₂ s₃) → ∞ (♭ sr ∼ Case s₁ s₂) → Case sl1 sl2 ∼ Semi sr s₃
</div><div class="line" id="file-transitivity-LC24" style="box-sizing: border-box;"> ∼-Semi-Case-Right : ∀ {s₁ s₂ s₃ sl1 sl2 sr}
</div><div class="line" id="file-transitivity-LC25" style="box-sizing: border-box;"> → ∞ (♭ sl1 ∼ Semi s₁ s₃) → ∞ (♭ sl2 ∼ Semi s₂ s₃) → ∞ (♭ sr ∼ Case s₁ s₂) → Semi sr s₃ ∼ Case sl1 sl2</div></pre></div><div><br></div><div>When it comes to proving the equivalence properties, reflexivity and symmetry are straightforward, but for transitivity</div><div>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 </div><div>terminate any more. </div><div>Is there something obviously wrong about these definitions?</div><div>The full code may be found here: <a href="https://gist.github.com/28c0643956315b70c0e6.git">https://gist.github.com/28c0643956315b70c0e6.git</a></div><div><br></div><div>I'm running version 2.3.2.2</div><div><br></div><div>-Peter</div><div><br></div><div><br></div><div></div></body></html>