Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Interpretation of constructors of type forall

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Interpretation of constructors of type forall


chronological Thread 
  • From: bertot <Yves.Bertot AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Interpretation of constructors of type forall
  • Date: Sat, 11 Dec 2010 09:26:39 +0100

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.




Archive powered by MhonArc 2.6.16.

Top of Page