The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Eric Jaeger wrote:
> 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) ?
>    

This might fit the bill, for a slight simplification where I change your 
"predicates" to return [Prop] instead of [Type]:

Fixpoint multi (dom : Type) (n : nat) (ran : Type) : Type :=
  match n with
    | O => ran
    | S n' => dom -> multi dom n' ran
  end.

Fixpoint agree (dom : Type) (n : nat) : multi dom n Prop -> multi dom n 
bool -> Prop :=
  match n with
    | O => fun P b => IF P then b = true else b = false
    | S n' => fun Pf Bf => forall x : dom, agree dom n' (Pf x) (Bf x)
  end.

Eval compute in agree nat 0.
Eval compute in agree nat 1.
Eval compute in agree nat 2.