The Coq mailing list

[Math Prover <mathprover AT gmail.com>]

Pierre:

  I haven't had a chance to test this out in Coq (only read your code so far).

  As I was reading over your solution, I really like the following points:

(1) This starts abstracting out / splitting two parts:

  (a) for all n, n satisfies some property P [which is some disjunction]

  (b) therefore, we can express n as the disjunction

(2) The "heavy lifting" is pushed into Fixpoint/Lemma, keeping the Ltac simple. Thus, for more complicated splits (say over objects that are not even nats), this is far easier to debug.

I appreciate you sharing this, I found the two points above rather instructive. Thanks!

On Sat, Jun 1, 2013 at 2:44 AM, Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:

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.