"İmha ..." gibi davranan taktikleri nasıl yazarım?

Question

Coq içinde, destruct taktiğinin, karmaşık endüktif tiplerin paketlerini açarken bile kullanıcının tanıtılan değişkenlere adlar atamasına izin veren bir "eşzamanlı ayırma giriş düzenini" kabul eden bir varyantı vardır.

Coq içindeki Ltac dili, kullanıcının özel taktik yazmasına izin verir. Denetimi destruct'a teslim etmeden önce bir şey yapan bir taktiği yazmak istiyorum.

Özel taktiğimin, taktiklerimin destruct'a verebileceği bir tanıtım deseni sağlamasına izin vermesini (veya hangisi daha kolaysa) gerektirmesini isterim.

Ne Ltac sözdizimi bunu başarır?

Answer 1

reference manual'da açıklanan taktik notasyonları kullanabilirsiniz. Örneğin,

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 yönergesi bir intro deseni olarak bar yorumlamak Coq talimatını verir. Böylece, foo numaralı çağrı, destruct H as (HA & HB & HC) numaralı telefonu aramada sonuçlanır.

Daha karmaşık bir tanıtım modelini gösteren daha uzun bir örnek.

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. 

Adların nasıl kullanıldığını görmek için oluşturulan hedeflerden birini denetleyebiliriz.

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