The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hello, here is another solution that is more complex but eventually builds simpler terms. You can define the function splitnat that builds the disjunction recursively, and then prove that it always produces a provable property. Then the tactic is just asserting (splitnat n k).

Best regards

Pierre

---------------8X---------------

Require Import Arith.

Fixpoint splitnat_ n k {struct k}: Prop :=
match k with
| O => n = O
| S k' => n = k \/ (splitnat_ n k')
end.

Definition splitnat n k := (splitnat_ n k) \/ n>k.

Lemma splitnat_ok : forall k n, splitnat n k.
  intros k.
  induction k;intros;simpl.
  - unfold splitnat.
    simpl.
    destruct (zerop n);auto.
  - unfold splitnat.
    simpl.
    unfold splitnat in IHk.
    destruct (IHk n).
    + left. right. assumption.
    + destruct H.
      * left. left. reflexivity.
      * right. auto with arith.
Qed.

(* testing the built property *)

Variable a:nat.
Eval compute in (splitnat a 4).

(* making use of splitnat *)

Ltac nsplit n k :=
  let h := fresh "hsplit" in
  ((assert (h:splitnat n k) by apply splitnat_ok); unfold splitnat in h; simpl in h).

(*example*)

Lemma trying: forall n m:nat, n = m.
Proof.
  intros n.
  nsplit n 4.
 
 

2013/6/1 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.