The Coq mailing list

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

Dear Pierre,

Thanks for your response. However, your definition of Spec produced the 
following error (term "D" is the one after end).

Error:
In environment
X : Set
d : Data X
l : Link X
X0 : Set
D : X0 -> Prop
The term "D" has type "X0 -> Prop" while it is expected to have type
 "X -> Prop".

I'm running Coq version 8.3 (December 2011).

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

On 3 Oct 2012, at 17:15, Pierre Boutillier wrote:

> Hi, 
> 
> Your problem is a good example to describe what has been improved in the 
> pattern matching compiler in Coq 8.4 and why we are still in the middle of 
> something.
> 
> 
> Your problem basically is that you want to keep the link between the type 
> of d and l while you are matching over d and then l and D while you are 
> matching over l
> 
> In coq 8.4 you sometime can do it by saying
>> match d,l with Build_Data X0 D,l' => 
> and l' is not l even is you do not destruct it. It is a copy of l : Link X 
> in Link X0
> 
> But it does not work every time and you still sometime need to write the 
> underlying commutative cut ourself as 
>>    match l' with Build_Link X L => fun D' =>
>>      …. end D
> 
> (Situations where you even have to write explicitly the type annotation 
> occur)
> 
> In the end the term you're trying to write is
> --8<----
> 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,l with Build_Data X D,l' => 
>     match l' with Build_Link X L => fun D' =>
>        forall x : X, D' x /\ L x
>     end D
>  end.
> --8<-----
> 
> Hugo Herbelin and I are working to allow you to write 
> 
> Definition Spec (X : Set) (d : Data X) (l : Link X) : Prop :=
>  match d,l with Build_Data X D, Build_Link X L => 
>        forall x : X, D x /\ L x
>     end.
> 
> and this will be in the change log (CF: Cedric and Daniel) :-p.
> 
> Pierre B.
> Le 3 oct. 2012 à 17:51, "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
>> 
>> 
> 
>