The Coq mailing list

[Math Prover <mathprover AT gmail.com>]

Very nice/clever, thanks!

On Fri, May 31, 2013 at 11:39 PM, Yucheng Zhang <yczhang89 AT gmail.com> wrote:

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.