The Coq mailing list

[gallais <guillaume.allais AT ens-lyon.org>]

Hi,

This is what I came up with. It's slower than the "magic" Ltac function
but you do get a nice "n <= k" assumption in the last case rather than
a huge series of S constructors.

Cheers,

--
gallais


Require Import Arith.

Section case_analysis_up_to.

Variable (P : nat -> Prop).

Fixpoint holds_up_to (n : nat) :=
match n with
  | O   => True
  | S k => P k /\ holds_up_to k
end.

Lemma lookup : forall n, holds_up_to n ->
  forall k, k < n -> P k.
Proof.
intros n ih k lt ; induction lt.
  apply ih.
  apply IHlt, ih.
Qed.

Lemma case_up_to : forall k,
  holds_up_to k ->
  (forall n, k <= n -> P n) ->
  forall n, P n.
Proof.
intros k ih Pn n ; destruct (le_lt_dec k n) as [above | under].
 apply Pn, above.
 eapply lookup; eauto.
Qed.

End case_analysis_up_to.

Ltac case_up_to k := eapply case_up_to with k; [simpl; repeat split|].



On 1 June 2013 05:56, 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!