The Coq mailing list

[Math Prover <mathprover AT gmail.com>]

In working towards this, I have written the following lemmas:

Lemma lem__nat_lt_geq:

  forall (n k: nat),

    (n < k)%nat \/ (n >= k)%nat.

  induction n as [| n IHn]; intros k; crush;

  destruct k; crush; destruct (IHn k); crush. Qed.

Lemma lem__nat_lt_des:

  forall (k n: nat),

    (n < S k)%nat ->

    (n = k)%nat \/ (n < k)%nat.

  induction k; crush. Qed.

What I need is one application of "lem__nat_lt_geq" (easy to do), and repeated applications/or-destruction of "lem__nat_lt_des" -- which I'm not sure how to do.

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

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!