The Coq mailing list

["Terrell, Jeffrey" <jeffrey.terrell AT kcl.ac.uk>]

Dear Cedric,

Thanks, and thanks to the other respondents too.

Your first solution works fine in most of my cases. However, I'd also like to 
be able to vary what Spec outputs depending on which constructor of Link is 
used.

If  Build_Link_1 is used, I'd like Spec to output
   forall x : X, D x /\ L x.

If Build_Link_2 is used, I'd like Spec to output
   forall x : X, D x /\ L (x :: nil)

Data is the same as before, but Link now has two constructors.

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

Inductive Link : Set -> Type :=
  Build_Link_1 : forall X : Set, (X -> Prop) -> Link X |
  Build_Link_2 : forall X : Set, (list X -> Prop) -> Link X.

Many thanks.

Regards,
Jeff.
---
Jeffrey Terrell
Department of Informatics
King's College, London

On 3 Oct 2012, at 17:21, AUGER Cédric wrote:

> 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.
>