Code duplication

[Lysxia]

It seems paco's code is actually generated by the python scripts, and the code duplication leads to somwhat long compile times. Instead of copying mostly the same code for each arity, have you considered a generalization in pure Coq (say, indexing predicates by the arity as a nat)? What are the difficulties with that approach?

[Lysxia]

In fact it seems possible to derive the n-ary relations from the 1-ary one.

I'm experimenting with it here: https://github.com/Lysxia/coq-recursion-schemes/blob/544c146d0426a5e7983829d9fab9eb60028ca721/theories/PCofix.v

[jeehoonkang]

That's very interesting. I'll bring this issue to @gilhur. Thanks for contribution!

[minkiminki]

@Lysxia The situation is more compilcated.
Unlike your implementation, we should define a dependent product and predicate(k+1th argument's type is depending on previous k arguments),
and I think it's theoretically impossible in Coq(I'm not sure).

However, following your idea, we can define and prove n-ary paco with 1-ary paco for each n.
(In current implementation, every n-ary paco is defined separately and n-ary lemmas are proved using "cofix" keyword, which makes compilation time very long.)

I implemented this idea in #13. In my test, compilation time is reduced a lot(75sec -> 17sec).

[Lysxia]

That's impressive!

[Lysxia]

Here's a new version generalizing over dependent products: https://github.com/Lysxia/coq-recursion-schemes/blob/2de29c486f201d1fde6e50c43c5a8108f5381c6b/theories/PCofix.v

I couldn't figure out the right type-inference behavior though. So now my hope is to somehow get paco0, paco1, paco2, etc to be the only duplicated bits, and the same lemmas can be used with all of them.

[minkiminki]

@Lysxia
It would be great if we can reduced the duplication with your idea. I reduced the duplication in other way 6130d57, but I think your suggestion is more general.
But as you mentioned in other issue #16, the bottleneck is in the other place... So the benefits will not be great.

[Lysxia]

I've been taking a look at this again, and I'm wondering whether there's a reason for the way some properties are stated. For example:

(* paco_internal.v *)
monotone gf :=  forall x0 r r' (IN : gf r x0) (LE : r <1= r'), gf r' x0

Why not write this instead:

monotone gf := forall r r', (r <1= r') -> (gf r <1= gf r')

I think this would make things easier to generalize.