The Coq mailing list

[Math Prover <mathprover AT gmail.com>]

Hi,

  In my assumptions, I have something like this:

...

n: nat

========== (1/1)

...

  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.

  So, if I were to type "magic n k", I would get:

n=0

========= (1/k+1)

...

n=1

========= (2/k+1)

...

....

n=k-1

======= (k/k+1)

....

H: n>=k

========= (k+1/k+1)

......

My question: is there anyway to do this with Ltac? In particular, although I see how to use match/try/repeat in ltac, I don't see how do I can do looping / testing of arguments? (i.e. how to embed "Z.leb n k" into my ltac).

Thanks!