How to write a tactic that behaves like "destruct ... as"?

Question

In coq, destruct tactics has an option that adopts a “conjunctive disjunctive introduction pattern” that allows the user to assign variables to introduce names, even when unpacking complex inductive types.

Ltac's coq language allows the user to write custom tactics. I would like to write (in truth, save) a tactic that does something before transferring control to destruct .

I would like my custom tactics to allow (or require, depending on which it would be easier) for the user to present an implementation pattern that my tactics can convey to destruct .

What Ltac syntax does this?

Answer 1

You can use the tactical designations 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 insertion pattern. So calling foo leads to calling destruct H as (HA & HB & HC) .

Here is a longer example showing a more complex implementation pattern.

 Tactic Notation "my_destruct" hyp(H) "as" simple_intropattern(pattern) := destruct H as pattern. Inductive wondrous : nat -> Prop := | one : wondrous 1 | half : forall nk : nat, n = 2 * k -> wondrous k -> wondrous n | triple_one : forall nk : 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 check one of the generated goals to find out how the names are 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')