The Coq mailing list

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

Le Mon, 13 Dec 2010 18:22:47 +0000,
Jeffrey Terrell 
<jeff AT kc.com>
 a écrit :

> Dear Cedric,
> 
> Just to be clear, are you suggesting that the specification is
> 
> forall b : B, exists q : Q, rendition b q?

I am not sure of what you whished, but that was what I suggested.

> 
> If so, how would you prove it?
> 
> Regards,
> Jeff.
> 

In your case, as you build your inductive type with type constructors
(here option),
you should define your own induction principle like:
>>>
Lemma B_induction: forall (P: B -> Prop), P (Build_B None) ->
                   (forall b, P b -> P (Build_B (Some b))) ->
                   forall b, P b.
Proof.
 intros P PNone PSome.
 refine (fix B_ind2 b := match b as b0 return P b0 with
                         | Build_B None => PNone
                         | Build_B (Some b) => PSome b (B_ind2 b)
                         end).
Qed.
<<<
It is hideous isn't it?
Then the following is straight forward:
>>>
Lemma rendition_proof : forall b, exists q, rendition b q.
Proof.
 intro b; pattern b; apply B_induction.
   exists (Build_Q None); constructor.
   intros.
    destruct H.
    exists (Build_Q (Some x)); constructor.
    assumption.
 Qed.
<<<
If you define your type as without type constructors, let us say:
>>>
Inductive B: Type :=
Build_B: option_B -> B
with option_B: Type :=
| None_B: option_B
| Some_B: B -> option_B
.
<<<
Then things are easier, but you will lack all theorems associated to
your previous structure (a common example is for trees, as list of
trees; either you define your induction principles (see Induction
Scheme in the manual), either you "inline" the definition of lists as
above, but you won't have fold_right, hd, tl and so on, unless you
redefine them).

Another solution is the fix tactic, but take a look at the "unblocked,
thanks!" parallel thread on the coq-club mailing list.
>>>
Lemma rendition_proof : forall b, exists q, rendition b q.
Proof.
 fix 1.
 intro b; destruct b.
 destruct o.
   destruct (rendition_proof b).
    exists (Build_Q (Some x)).
    apply Rending. (*or "constructor 2"; as you whish*)
    assumption.
   exists (Build_Q None).
    apply End_of_rendition. (*or "constructor 1"; as you whish*)
 Qed.
<<<
There may be other ways to do that, but if you understand the 3 of
them, then you shouldn't have problems with such inductions.

The solution I like best is the third one, but if you are not used to
it, it can be painful to deal with guardedness.
The solution I find the simplest is the second one, since you won't
have to deal with guardedness at all, but it can be long to define such
types and you won't be able to use the library on "option" type (that
said, there is not much on option type in the libraries, and even in
the case of trees, a big part of the library becomes useless, as you
cannot deal with recursion on them).
I do not use the first solution, even if it is the first that came in
my mind.