The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Wed, 3 Oct 2012 15:51:11 +0000,
"Terrell, Jeffrey" 
<jeffrey.terrell AT kcl.ac.uk>
 a écrit :

> Hi,
> 
> How could Spec be made to return the proposition
> 
> forall x : X, D x /\ L x?
> 
> Clearly, the way I've defined it is nonsense. However, I don't know
> how to exploit the fact that parameters d and l are both dependent on
> parameter X.
> 
> Inductive Data : Set -> Type :=
>    Build_Data : forall X : Set, (X -> Prop) -> Data X.
> 
> Inductive Link : Set -> Type :=
>    Build_Link : forall X : Set, (X -> Prop) -> Link X.
> 
> Definition Spec (X : Set) (d : Data X) (l : Link X) : Prop :=
>    match d with Build_Data X D => 
>       match l with Build_Link X L =>
>          forall x : X, D x /\ L x
>       end
>    end.
> 
> Many thanks.
> 
> Regards,
> Jeff.
> ---
> Jeffrey Terrell
> Department of Informatics
> King's College, London
> 
> 

I guess you want to do this:

Definition Spec (X : Set) (d : Data X) (l : Link X) : Prop :=
   let D : X -> Prop := match d with Build_Data X D => D end in
   let L : X -> Prop := match l with Build_Link X L => L end in
   forall x : X, D x /\ L x.

===================
Note that I assume your true stuff is more complex than your example.
If not, there is something easier:

Inductive Data (X : Set) : Type :=
    Build_Data : (X -> Prop) -> Data X.

Inductive Link (X : Set) : Type :=
    Build_Link : (X -> Prop) -> Link X.

And then you do not have dependant type anymore.