The Coq mailing list

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

Le Thu, 4 Oct 2012 11:39:24 +0000,
"Terrell, Jeffrey" 
<jeffrey.terrell AT kcl.ac.uk>
 a écrit :

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

Definition Spec (X : Set) (D : Data X) (L : Link X) :=
  let l : X -> Prop := match L with Build_Link_1 _ f => f
                                   | Build_Link_2 _ f => fun x => f
(cons x nil) end in
  let d : X -> Prop := match D with Build_Data _ d => d end in
  forall x, l x /\ d x.

✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂ ✂

Once again for this example, X should be set as a parameter (some
other personne also did this remark).