Come faccio a scrivere tattiche che si comportano come "destruct ... as"?

Question

In coq, la tattica destruct ha una variante che accetta un "modello di introduzione disgiuntivo congiuntivo" che consente all'utente di assegnare nomi alle variabili introdotte, anche quando si decomprimono tipi complessi induttivi.

Il linguaggio Ltac in coq consente all'utente di scrivere tattiche personalizzate. Mi piacerebbe scrivere (in verità, mantenere) una tattica che fa qualcosa prima di passare il controllo a destruct.

Vorrei che la mia tattica personalizzata consenta (o richieda, a seconda di quale sia più semplice) all'utente di fornire un modello di presentazione che la mia tattica può trasmettere a destruct.

Quale sintassi di Ltac raggiunge questo risultato?

Answer 1

È possibile utilizzare le notazioni tattiche, descritte nello reference manual. Per esempio,

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

La direttiva simple_intropattern istruisce Coq a interpretare bar come un pattern di introduzione. Pertanto, la chiamata a foo provoca la chiamata destruct H as (HA & HB & HC).

Ecco un esempio più lungo che mostra un modello di introduzione più complesso.

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. 

Possiamo ispezionare uno degli obiettivi generati per vedere come vengono utilizzati i nomi.

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