Proving that if an element normalizes in at most n steps then it normalizes in at most (n+1) steps.

Of course, the above is trivial IRL. However, if "at most n steps" is formalized indirectly in Coq, the proof can be nontrivial.


Module Termination.


Parameter T : Set.


Parameter R : T -> T -> Prop.


Fixpoint terminates (n : nat) (gamma : T) : Prop :=
  match n with
    | O => False
    | S n' =>
      forall gamma' : T,
        (R gamma gamma' -> terminates n' gamma')
  end.

The proposition "terminates n gamma" means that gamma reduces to a normal form in at most (n-1) steps. The "at most" part of the definition is very implicit in the way the second case is written. Proving that this is actually the case:

Theorem terminates_monotone : forall n gamma,

  terminates n gamma -> terminates (S n) gamma.

i.e. that if gamma normalizes in at most (n-1) steps then it normalizes in at most n steps, is not trivial and it shows why it pays to think about a proof before jumping into it. Here is the proof I came up with:

  induction n.

  inversion 1.

  intros.

  simpl.

  intros.

  simpl in H.

  specialize (H gamma' H0).

  specialize (IHn gamma' H).

  simpl in IHn.

  specialize (IHn gamma'0 H1).

  assumption.

Qed.

End Termination.

after some scribbling on paper. As an open question, how can we make the proof more automatic by making use of Ltac? The "intelligent" parts of the proof seem to be the choice of "n" as an induction parameter and the specializations of the different hypothesis, so these would probably need to be kept (or brute-forced).