The Coq mailing list

[Jeffrey Terrell <jeff AT kc.com>]

Dear Cedric,

Just to be clear, are you suggesting that the specification is

forall b : B, exists q : Q, rendition b q?

If so, how would you prove it?

Regards,
Jeff.

On 13/12/2010 14:32, AUGER Cedric wrote:
> Le Mon, 13 Dec 2010 13:35:14 +0000,
> Jeffrey 
> Terrell<jeff AT kc.com>
>   a écrit :
>
> > Dear Yves,
> >
> > Thanks for your response. Yes, you are right. I *was* thinking of
> > process rather than property. I knew something was amiss but I wasn't
> > sure what it was.
> >
> > What I'm essentially trying to do is to define the specification of a
> > mapping between a linked (i.e. ordered) list of Bs and a linked list
> > of Qs. For example:
> >
> > b1 ->  b2 ->  b3
> > |     |     |
> > v     v     v
> > q1 ->  q2 ->  q3
> >
> > b1 is mapped to q1
> > b2 is mapped to q2, and q1 is linked to q2
> > b3 is mapped to q3, and q2 is linked to q3
> >
> > Links are represented as option types.
> >
> > Inductive B : Set :=
> >      Build_B : option B ->  B.
> >
> > Inductive Q : Set :=
> >      Build_Q : option Q ->  Q.
> >
> > I'm actually more interested in the *specification* of this
> > transformation than its implementation:
> >
> > Fixpoint X (b : B) : Q :=
> >      match (R1 b) with |
> >         None =>  Build_Q None |
> >         Some b' =>  Build_Q (Some (X b'))
> >      end.
> >
> > Definition b3 : B := Build_B None.
> > Definition b2 : B := Build_B (Some b3).
> > Definition b1 : B := Build_B (Some b2).
> >
> > Eval compute in (b1).
> > Eval compute in (X b1).
> >
> > Is it possible to specify the transformation using an inductive
> > predicate, a sort of recursive rendition of
> >
> > forall b : B, exists q : Q,
> >      match (R1 b) with |
> >         None =>  True |
> >         Some b' =>  exists q' : Q, (Some q' = (S1 q) /\
> >            match (R1 b') with |
> >               None =>  True |
> >               Some b'' =>  exists q'' : Q, (Some q'' = (S1
> > q') /\ ... ))?
> >
> > (R1 and S1 return the option fields of objects of type B and Q
> > respectively.) I'm aware that this specification is process-oriented,
> > but I'm not sure how else to express it. Thanks.
> >
> > Regards,
> > Jeff.
> You can do something like:
>
> Inductive rendition : B ->  Q ->  Prop :=
> | End_of_rendition: rendition (Build_B None) (Build_Q None)
> | Rending: forall b q, rendition b q ->  rendition (Build_B (Some b))
> (Build_Q (Some q)).
>
> By the way for such types, you may find useful to have:
> Record B : Type := { R1: option B }.
>
> then you can use b.(R1) instead of (R1 b), and {|R1 := Some b|} instead
> of Build_B (Some b), so that you won't have to write the R1 function.