The Coq mailing list

[Math Prover <mathprover AT gmail.com>]

Another stupid question from me:

(1)  "magic n 10"

(2)  "magic n (length (1::2::3::4::5::6::7::8::9::10::nil))"

(1) works. (2) somehow does not work. Is there somewhat I can embed a simpl/compute/cbv somewhere so that "length (1::2::...::nil))" gets simplified to 10 before it hits ltac (or have ltac handle this case as well?)

Thanks!

On Fri, May 31, 2013 at 11:50 PM, Math Prover <mathprover AT gmail.com> wrote:

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.