The Coq mailing list

[Eric Jaeger <eric.jaeger AT ssi.gouv.fr>]

Hi all,

I'm currently trying to revisit some Coq code to improve automation
(digging further in Ltac) and notations. I've for example several
definitions to relate a predicate and a boolean function deciding this
predicate:

Definition implements1(T:Type)(P:T->Type)(f:T->bool):=
 ((forall (t:T), f t=true->P t) * (forall (t:T), f t=false->P
t->False))%type.

Definition implements2(T1 T2:Type)(P:T1->T2->Type)(f:T1->T2->bool):=
 ((forall (t1:T1)(t2:T2), f t1 t2=true->P t1 t2) *
  (forall (t1:T1)(t2:T2), f t1 t2=false->P t1 t2->False))%type.

...

That is, one definition per arity.

1/ Is there an elegant way to merge these definitions (possibly
internally relying  on currification, but noting that I do not want to
use A*B->C instead of A->B->C at top level) ?

2/ If not, is there a way to use some forms of "polymorphic" coercions
(e.g. a generic currification) ?

3/ If not, is there a way to define a single notation for all these
definitions? E.g. "P>>>f" would mean "implem1 P f" or "implem2 P f",
etc., according to the arity of P.

4/ If not, is there a way to use Ltac to define interesting tactics to
address my problem? I've already a tactic "arity" returning the number
of variables for a predicate/boolean function, but I've not discovered
any way to use it to solve my problem.

  Thanks in advance for any answer, Eric