Positivity checker performance [Re: [Agda] Agda dies trying to prove transitivity]

[Andreas Abel]

I got hold of the test case and reported the bug under

   https://code.google.com/p/agda/issues/detail?id=1560

The discussion will continue on the bug tracker.

Cheers,
Andreas

On 11.06.2015 09:50, Andreas Abel wrote:
> 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


-- 
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/