Jak pisać taktyki, które zachowują się jak "zniszczenie ... jak"?

Question

Zgodnie z taktyką, taktyka destruct ma wariant akceptujący "łączący rozłączny wzór wprowadzający", który umożliwia użytkownikowi przypisywanie nazw wprowadzanych zmiennych, nawet podczas rozpakowywania złożonych typów indukcyjnych.

Język Ltac w coq pozwala użytkownikowi pisać niestandardowe taktyki. Chciałbym napisać (w rzeczywistości, utrzymywać) taktykę, która robi coś przed przekazaniem kontroli do destruct.

Chciałbym, aby moja niestandardowa taktyka pozwalała (lub wymagała, w zależności od tego, która z nich jest łatwiejsza) od dostarczenia wzoru wprowadzenia, który moja taktyka może przekazać pod destruct.

Co robi syntaktyka Ltac?

Answer 1

Możesz używać notatek taktycznych, opisanych w reference manual. Na przykład,

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

Dyrektywa simple_intropattern instruuje Coq interpretować bar jako wzór intro. Tak więc wywołanie foo powoduje wywołanie destruct H as (HA & HB & HC).

Oto dłuższy przykład pokazujący bardziej złożony wzór wprowadzania.

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. 

Możemy sprawdzić jeden z wygenerowanych celów, aby zobaczyć, jak używane są nazwy.

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