The Coq mailing list

[Jeffrey Terrell <jeff AT kc.com>]

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.

On 11/12/2010 08:26, bertot wrote:
> Your example, is interesting for experimentation or didactical purposes, but 
> it
> goes against usual practice.
>
> In fact, the constructor Trav_S can never be used, because you will never be
> able to produce a proof of
> Trav(Build_B (Some b))
>
> I believe you really wanted to write a constructor
>
> Trav_S_yves : forall b : B, Trav b -> Trav (Build_B (Some b))
>
> I believe you are reading the arrow "->" in your constructor in the wrong way.
> You think
> "the problem of proving (Trav(Build_B (Some b))) should reduce to the problem 
> of
> proving
> Trav b"
>
> But the arrow does not have this meaning. It is an implication (A -> B) means,
> "it is enough to prove A if you want to have B". So when applying this schema 
> to
> you needs, the sentence should be
>
> "It is enough to prove Trav b if you want to prove (Trav(Build_B (Some b)))"
>
> So you should really write the constructor I suggest. Am I right?
>
> Yves
>
> PS. In other words, I believe you confused "Inductive" for "Fixpoint", when
> describing an Inductive type, you are not describing a process, the "->" does
> not capture the same rough meaning as "=>" as used in pattern-matching. In 
> fact,
> it is the other way round. The very name that you chose "Trav" shows that you
> are thinking in terms of process instead of in terms of properties.
>
> PS2. Here is a proof that Trav is not satisfied for terms of the form
> Build_B(Some _ ), but I suggest you don't read it until you have really
> understood what inductive types are...
>
>
> Lemma Trav_not_Some : forall b, ~Trav(Build_B (Some b)).
> Proof.
> assert (M: forall b, Trav b -> forall b', b <> Build_B(Some b')).
> intros b H; induction H.
> intros; discriminate.
> destruct (IHTrav b); reflexivity.
> intros b H; case (M (Build_B(Some b)) H b); reflexivity.
> Qed.
>
> PS3. I really thank you for your question, it helps me clarifying a problem 
> that
> I often encounter with my students.
>
> On 10/12/10 4:31 PM, Jeffrey Terrell wrote:
> > Hi,
> >
> > In the definition of Trav below, how should one interpret Trav_S?
> >
> > Inductive B : Set :=
> > Build_B : option B -> B.
> >
> > Inductive Trav : B -> Prop :=
> > Trav_N : Trav (Build_B None) |
> > Trav_S : forall b : B, Trav (Build_B (Some b)) -> Trav b.
> >
> > It strikes me as confusing to think of it as a constructor, because unlike
> > Trav_N, it doesn't actually construct an object of type Trav <b>. It seems
> > more appropriate to think of it as an object of type
> >
> > forall b : B, Trav (Build_B (Some b)) -> Trav b
> >
> > from which terms of type
> >
> > Trav (Build_B (Some b')) -> Trav b'
> >
> > can be produced by applying Trav_S to b'.
> >
> > Thanks.
> >
> > Regards,
> > Jeff.