[Agda] Agda dies trying to prove transitivity

[Nils Anders Danielsson]

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).

-- 
/NAD