The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

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