我如何編寫表現得像「毀滅......」一樣的戰術？

在coq中，destruct策略有一個變體，它接受一個「連接分離引入模式」，允許用戶爲引入的變量指定名稱，即使在解包複雜的歸納類型時也是如此。我如何編寫表現得像「毀滅......」一樣的戰術？

coq中的Ltac語言允許用戶編寫自定義策略。我想寫（實際上，保持）一種策略，在將控制交給destruct之前做一些事情。

我想我的自定義策略允許（或要求，以較爲簡單的）用戶提供一個引導模式，我的策略可以交給destruct。

什麼Ltac語法來實現這個？

2015-05-09 phs

您可以使用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指令指示勒柯克解釋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')

來源

2015-05-11 02:55:40

謝謝！我希望你不介意，但我在你的回答中包含了另一個更多參與（但很愚蠢）的例子。 – phs

根本不是！現在好多了。 –

我如何編寫表現得像「毀滅......」一樣的戰術？

回答

相關問題