Как написать тактику, которая ведет себя как «destruct ... as»?

Question

В coq, тактика destruct имеет вариант, принимающий «конъюнктивный дизъюнктивный шаблон введения», который позволяет пользователю присваивать имена введенным переменным даже при распаковке сложных индуктивных типов.

Язык Ltac в coq позволяет пользователю писать пользовательскую тактику. Я бы хотел написать (по правде говоря, сохранить) тактику, которая что-то делает, прежде чем передать управление destruct.

Я бы хотел, чтобы моя пользовательская тактика позволяла (или требовала, в зависимости от того, что будет проще) пользователю предоставить шаблон внедрения, который моя тактика может передать destruct.

Какой синтаксис Ltac выполняет это?

Answer 1

Вы можете использовать тактические обозначения, описанные в reference manual. Например,

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). 

директива simple_intropattern инструктирует Coq интерпретировать bar как шаблон интро. Таким образом, вызов foo приводит к вызову destruct H as (HA & HB & HC).

Вот более длинный пример, показывающий более сложный образец внедрения.

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. 

Мы можем проверить один из сгенерированных целей, чтобы узнать, как используются имена.

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')