[Agda] Agda dies trying to prove transitivity

[Peter Thiemann]

On 05.06.2015 12:16, Nils Anders Danielsson wrote:
> On 2015-06-04 17:49, Peter Thiemann wrote:
>> 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.
>
> Agda analyses your definition to see how the arguments are used. This
> information can later be used by the positivity checker (and perhaps
> other things). However, in this case it takes a lot of time. A graph
> with 343 nodes and 961 edges is constructed, and then the transitive
> closure of this graph is computed (and used by the analysis). I tried to
> print the transitive closure (using -vtc.pos.graph:50), but Agda ran out
> of memory.
>
> Perhaps this analysis can be sped up. However, I suspect that you have
> no need for the analysis. One option is to add a pragma that turns off
> the analysis for a given definition (but it may not be so easy for users
> to figure out that this pragma is available and useful).
>

Checking positivity shouldn't be needed for this case as the actual
type construction is straightforward. Such a pragma would be helpful,
because I don't see a reasonable way to finish the proof.

I already tried to split the proof and only prove a few cases in each
definition (and leave holes for the remaining ones). However, in such
an approach I'm told that the termination checker does not work reliably.

I guess that splitting up in mutually recursive subfunctions that handle
individual cases wouldn't work, either, because the positivity checker
would collect all mutually recursive functions and analyze them together.

-Peter