Add interfaces to declare generic level polymorphic n-ary functions

[NotBad4U]

Implementation of N-ary functions and relations based on Guillaume Allais, "Generic Level Polymorphic N-ary Functions" (TyDe 2019).

This API provides n-ary functions that automatically reconstruct the representation of their input types through unification.

It helps to define fully level polymorphic n-ary versions of congruence, substitution and the combinators for indexed families,
that are used by programs such as SMT solvers. Lemmas provided in the rest of the library such as Eq.lp are implemented for fixed arities, and the implementation here aims to provide similar lemmas for N-ary Combinators.

[fblanqui]

Thanks Alessio. Here are some remarks:

[fblanqui]

Various functions can be declared as injective: arrows, sets_ident, ArrowI.

Please add an example using the unification rules.

[NotBad4U]

I think we have a better API now.

[NotBad4U]

I think we can merge this one

[fblanqui]

Hi Alessio.

Your unification rules are unsound: (fun unit b) can be an arrow type (if b so is).
And Arrow is not injective (nor arrows) since arrows unit (a ~> a) == a ~> a == arrows (a::unit) a.
However (\b,arrows a b) and (\a,arrows a b) are both injective since arrows a b == arrows a b' => b == b' and arrows a b == arrows a' b => a == a'.

I also propose some renamings: Sets -> VSet, sets -> vset, arrows -> fun, Arrow -> Fun, cong_n -> refl_cong, subst_n -> refl_subs, compose_n -> comp.

I already fixed all this. Can I push on your branch?

[NotBad4U]

unit (a ~> a) == a ~> a == arrows (a::unit) a

good catch

I also propose some renamings: Sets -> VSet, sets -> vset, arrows -> fun, Arrow -> Fun, cong_n -> refl_cong, subst_n -> refl_subs, compose_n -> comp.

No problem changing the name; I just followed the one in the paper when I implemented it during my PhD to make things easier.

Yes feel free to commit on top of mine

[fblanqui]

It is perhaps possible for the user to only give the arity instead of the domain by defining functions on n instead of on ts.

[NotBad4U]

It is perhaps possible for the user to only give the arity instead of the domain by defining functions on n instead of on ts.

I've thought about that too, but I haven't found a way to implement it yet.

[fblanqui]

One problem to get this feature is to have Lambdapi infer that any meta ?X:VSet 0 can be instantiated by unit (◃ now).

[fblanqui]

Remark: List.Arr n a b is the same as NaryFun.Fun n (vcst a) b.