The Coq mailing list

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

Le Mon, 1 Aug 2011 15:42:44 +0000,
frank maltman 
<frank.maltman AT googlemail.com>
 a écrit :

> On Mon, 1 Aug 2011 16:14:15 +0200
> AUGER Cedric 
>Â <Cedric.Auger AT lri.fr>
>  wrote:
> 
> > Le Mon, 01 Aug 2011 08:58:39 -0400,
> > Adam Chlipala 
>Â >Â <adam AT chlipala.net>
> >  a écrit :
> > 
> > > frank maltman wrote:
> > > > However, I'm now stuck proving the first case that does
> > > > terminate:
> > > >
> > > 
> > > I don't think your question is really about Coq.  This proof
> > > strategy fails on paper, too.
> > > 
> > 
> > Hmm, that annoying if you consider this script:
> > 
> 
> Thanks, both of you.
> 
> I guess I am convinced I have an informal proof (there's one in the
> book, for a start) but at the same time, I'm likely convinced too
> easily. In this situation, I'm never sure if my approach is wrong or
> if I just don't know how to instruct coq properly. Seems as though
> it's the latter in this case.
> 

By the way, just some informal stuff, there are several ways to
simplify a term in coq, here I used an "unfold" followed by a "fold";
it has the great advantage that you make the simplification you
precisely want (simpl, tends to reduce all that can be reduced,
without recursion unrolling, often leading to better terms, but in
your case, it was an awful one), but the disadvantage that you have
to find the good way to use it (provide the term in which you want it
to be rewritten).

A good workaround is to build opaque, but specified functions.

For instance you could have defined:

Inductive numeric_spe: term -> Prop :=
| Pnum: forall t, numeric_spe t -> numeric_spe (Term_Pred t)
| Snum: forall t, numeric_spe t -> numeric_spe (Term_Succ t)
| Znum: numeric_spe Term_Zero
.

and then:

Definition numeric: forall t, {numeric_spe t}+{~ numeric_spe t}.
(*proof here*)
admit.
Qed. (* and not Defined *)

Then later, when doing a "simpl", numeric won't be unfolded;
the bad point is that it cannot reduce even "numeric Term_Zero"
the good point is that you can do "destruct (numeric t)."
then have whether "numeric_spe t", whether "~ numeric_spe t";
and then do some inversion/induction to go further.

There also are some other reduction tactics, "cbv" is the most
customizable one.