How do I write tactics that behave like "destruct ... as"?

Question

In coq, the destruct tactic has a variant accepting an "conjunctive disjunctive introduction pattern" that allows the user to assign names to introduced variables, even when unpacking complex inductive types.

The Ltac language in coq allows the user to write custom tactics. I'd like to write (in truth, maintain) a tactic that does something before handing control off to destruct.

I would like my custom tactic to allow (or require, whichever is easier) the user to supply an introduction pattern that my tactic can hand to destruct.

What Ltac syntax accomplishes this?

Answer 1

You can use tactic notations, described in the reference manual. For instance,

Tactic Notation "foo" simple_intropattern(bar) :=
  match goal with
  | H : ?A /\ ?B |- _ =>
    destruct H as bar
  end.

Goal True /\ True /\ True -> True.
intros. foo (HA & HB & HC).

The simple_intropattern directive instructs Coq to interpret bar as an intro pattern. Thus, the call to foo results in calling destruct H as (HA & HB & HC).

Here's a longer example showing a more complex introduction pattern.

Tactic Notation "my_destruct" hyp(H) "as" simple_intropattern(pattern) :=
  destruct H as pattern.

Inductive wondrous : nat -> Prop :=
  | one         : wondrous 1
  | half        : forall n k : nat,         n = 2 * k -> wondrous k -> wondrous n
  | triple_one  : forall n k : nat, 3 * n + 1 = k     -> wondrous k -> wondrous n.

Lemma oneness : forall n : nat, n = 0 \/ wondrous n.
Proof.
  intro n.
  induction n as [ | n IH_n ].

  (* n = 0 *)
  left. reflexivity.

  (* n <> 0 *)
  right. my_destruct IH_n as
    [ H_n_zero
    | [
      | n' k H_half       H_wondrous_k
      | n' k H_triple_one H_wondrous_k ] ].

Admitted.

We can inspect one of the generated goals to see how the names are being used.

oneness < Show 4.
subgoal 4 is:

  n : nat
  n' : nat
  k : nat
  H_triple_one : 3 * n' + 1 = k
  H_wondrous_k : wondrous k
  ============================
   wondrous (S n')