The Coq mailing list

[Yucheng Zhang <yczhang89 AT gmail.com>]

On Jun 1, 2013, at 12:56 PM, Math Prover 
<mathprover AT gmail.com>
 wrote:
>   Now, I want to tactic "magic", s.t. "magic n k" gives me the cases: n=0, 
> n=1, ..., n=k-1, and n>=k.

I've got a "magic" that's close to your need.

Ltac magic n k :=
  match k with
    | O => idtac
    | S ?k' => destruct n; [ | magic n k' ]
  end.

(* An example *)
Parameter P : nat -> Prop.

Goal forall n:nat, P n.
Proof.
  intro.
  magic n 10.
  Abort.