The Coq mailing list

[Vincent Demange <vincent.demange AT ensiie.fr>]

Hi the list,


Here is another solution, generating exactly the goals you want and
without relying on Ltac (see below).

The main idea is to prove the following statement:

(forall n > k, P n) -> P k -> ... -> P 0 -> forall n, P n

[Note the reverse order to ease the proof.]

Thanks to Mr. Forest for doing the hard work in seconds !


Vincent.


----8<------------------------------------------------------

Require Import Arith.


Fixpoint cases_aux (P: nat -> Type) (k:nat) {struct k} : Type := 
  match k with 
      | 0 => P 0 -> forall n, P n
      | S k' => P k -> cases_aux P k'
  end.

Definition cases P k := (forall n, n>k -> P n) -> cases_aux P k.

Lemma magic k P : cases P k.
Proof.
  unfold cases.
  induction k as [ | k' IHk'].

    intros Hinfty H0 .
    intros [ | n].
      exact H0.
      apply Hinfty.
      apply lt_0_Sn.
  
    intros Hinfty H_S_k'.
    fold cases_aux.
    apply IHk'.
    intros n H.
    do 2 red in H.
    case (le_lt_eq_dec (S k') n H); clear H; intro H.
      apply Hinfty, H.
      subst.
      apply H_S_k'.
Qed.


Section example.

  Variable P: nat -> Prop.

  Lemma example: forall n, P n.
  Proof.
  apply (magic 5).
  (* six goals to prove *)
  Admitted.

End example.