search

snu-sf / paco

A Coq library for parametric coinduction
https://github.com/snu-sf/paco
Other
43 stars 10 forks source link

Code duplication #12

Open Lysxia opened 6 years ago

Lysxia commented 6 years ago

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 commented 6 years ago

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 commented 6 years ago

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

minkiminki commented 6 years ago

@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 commented 6 years ago

That's impressive!

Lysxia commented 6 years ago

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 commented 5 years ago

@Lysxia It would be great if we can reduced the duplication with your idea. I reduced the duplication in other way https://github.com/snu-sf/paco/commit/6130d579bee261b21f752c919a03798e792b7526, 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 commented 4 years ago

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.