The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

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.