coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: AUGER Cédric <sedrikov AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Matching parameters of dependent types with common stem
- Date: Thu, 4 Oct 2012 13:58:57 +0200
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).
- [Coq-Club] Matching parameters of dependent types with common stem, Terrell, Jeffrey, 10/03/2012
- Re: [Coq-Club] Matching parameters of dependent types with common stem, Pierre Boutillier, 10/03/2012
- Re: [Coq-Club] Matching parameters of dependent types with common stem, Terrell, Jeffrey, 10/03/2012
- Re: [Coq-Club] Matching parameters of dependent types with common stem, Adam Chlipala, 10/03/2012
- Re: [Coq-Club] Matching parameters of dependent types with common stem, Terrell, Jeffrey, 10/03/2012
- Re: [Coq-Club] Matching parameters of dependent types with common stem, Robbert Krebbers, 10/03/2012
- Re: [Coq-Club] Matching parameters of dependent types with common stem, AUGER Cédric, 10/03/2012
- Re: [Coq-Club] Matching parameters of dependent types with common stem, Terrell, Jeffrey, 10/04/2012
- Re: [Coq-Club] Matching parameters of dependent types with common stem, AUGER Cédric, 10/04/2012
- Re: [Coq-Club] Matching parameters of dependent types with common stem, Terrell, Jeffrey, 10/04/2012
- Re: [Coq-Club] Matching parameters of dependent types with common stem, Pierre Boutillier, 10/03/2012
Archive powered by MHonArc 2.6.18.