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

[Andreas Abel]

Peter,

I improved the performance of the positivity checker.  Can you get the 
*maintenance* version from github and try again?

   http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Download

Cheers,
Andreas

On 11.06.2015 17:46, Andreas Abel wrote:
> 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/