[Agda] Agda dies trying to prove transitivity

[Andreas Abel]

Peter,

I would like to record this issue on the issue tracker, but the gist 
displays as empty for me.  Can you please record it at

   https://code.google.com/p/agda/issues

with a self-contained test case?

Thanks,
Andreas

On 04.06.2015 17:49, Peter Thiemann wrote:
> 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
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/