The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

To this thread where I gave incorrect advice, I wanted to try to make up 
for it by showing that the problem is actually quite simple to solve.  
Here is a nice automated solution that avoids all the issues that have 
been discussed in the ongoing thread.  The body of the main proof looks 
more complex than it is because of a weakness in Ltac pattern matching 
on [match] expressions, where a case for each constructor must be 
included, even if we don't want to specify any details of those cases.

Lemma numeric_not_stuck : forall t, numeric t = true -> match one_step t 
with
                                                          | Result_NF 
t' => numeric t' = true
                                                          | Result_Next 
t' => numeric t' = true
                                                          | 
Result_Error _ => False
                                                        end.
  induction t; simpl; intuition;
    repeat (match goal with
              | [ H : _ |- _ ] => rewrite H
              | [ _ : match ?E with Result_NF _ => _ | Result_Next _ => 
_ | Result_Error _ => _ end
                |- context[match ?E with Result_NF _ => _ | Result_Next 
_ => _ | Result_Error _ => _ end] ] => destruct E
              | [ _ : numeric ?E = true |- context[match ?E with 
Term_Zero => _ | Term_True => _ | Term_False => _
                                                     | Term_Succ _ => _ 
| Term_Pred _ => _ | Term_IsZero _ => _ | Term_Cond _ _ _ => _ end] ] =>
              destruct E
            end; simpl in *; intuition); discriminate.
Qed.

Lemma pred_numeric_not_stuck : forall (t : term),
  numeric t = true -> error (one_step (Term_Pred t)) = false.
  intros t Ht; generalize (numeric_not_stuck (Term_Pred t) Ht); 
destruct (one_step (Term_Pred t)); tauto.
Qed.