8

coq では、タクティックには、destruct複雑な帰納型をアンパックする場合でも、ユーザーが導入された変数に名前を割り当てることができる「連言選言導入パターン」を受け入れるバリアントがあります。

coq の Ltac 言語により、ユーザーはカスタム タクティクスを記述できます。に制御を渡す前に何かを実行する戦術を書きたい (実際には維持したい) と思いdestructます。

カスタム タクティックで、ユーザーが、タクティックがdestruct.

これを実現するLtac構文は何ですか?

4

1 に答える 1

7

リファレンス マニュアルで説明されているタクティック表記法を使用できます。例えば、

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.

生成された目標の 1 つを調べて、名前がどのように使用されているかを確認できます。

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-11T02:55:40.297 に答える