The Coq mailing list

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

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:
> >
> > --8<--
> >
> > Lemma pred_numeric_not_stuck : forall (t : term),
> >    numeric t = true ->  error (one_step (Term_Pred t)) = false.
> > Proof.
> >    intros t H.
> >    induction t.
> > [...]
> >
> > I have 'error (one_step (Term_Pred t)) = false' as an induction
> > hypothesis but am unable to prove 'error (one_step (Term_Pred
> > (Term_Pred t))) = false' with it. 
> 
> 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:

Lemma pred_numeric_not_stuck : forall (t : term),
  numeric t = true -> error (one_step (Term_Pred t)) = false.
Proof.
  intros t H.
  induction t.
    (* case t = Term_Zero *)
    reflexivity.
    (* case t = Term_True *)
    inversion H.
    (* case t = Term_False *)
    inversion H.
    (* case t = Term_Succ *)
    unfold one_step. rewrite pred_numeric. reflexivity.
    apply (pred_numeric t H).
    (* case t = Term_Pred *)
    unfold one_step; fold (one_step (Term_Pred t)).
    rewrite H.
    destruct (one_step (Term_Pred t)); try reflexivity.
    apply IHt.
    assumption.
    (* case t = Term_IsZero *)
    inversion H.
    (* case t = Term_Cond *)
    inversion H.
Qed.


> Have you convinced yourself that you have a valid informal proof?  
> That's usually a good first step before formalizing.