4

ある仮説が存在し、別の仮説が存在しない場合にルールを適用したい。この状態を確認するにはどうすればよいですか?

例えば：

Variable X Y : Prop.
Axiom A: X -> Y.
Axiom B: X -> Z.

Ltac more_detail :=
    match goal with
     |[H1:X,<not H2:Y>|-_]  =>
      let H' := fresh "DET" in assert Y as H'
                                   by (apply A;assumption)
     |[H1:X,<not H2:Z>|-_]  =>
      let H' := fresh "DET" in assert Z as H'
                                   by (apply B;assumption)
    end.

そのような、この目標のために：

> Goal X->True. intros.

H:X
=====
True

more_detail.2 番目の仮説 DET を導入します。

H:X
DET:Y
DET0:Z
=====
True

そして、連続する呼び出しmore_detail.は失敗します。

ただし、とmore_detail.の両方が存在することを常に確認する必要があります。つまり、一方のみが存在する場合は、別のルールを実行する必要があります。YZ

Goal X->Y->True. intros.

H:X
H1:Y
=====
True

> more_detail.

H:X
H1:Y
DET:Z
=====
True

と：

> Goal X->Z->True. intros.

H:X
H0:Z
=====
True

> more_detail.

H:X
H0:Z
DET:Y
=====
True
4

1 に答える 1

9

これは一般的な Ltac パターンです。戦術を使用してfail、いくつかの条件が一致したときに分岐を実行しないようにすることができます。

Variable X Y Z : Prop.
Hypothesis A : X -> Y.
Hypothesis B : X -> Z.

Ltac does_not_have Z :=
  match goal with
  | _ : Z |- _ => fail 1
  | |- _ => idtac
  end.

Ltac more_detail :=
  match goal with
  | H : X |- _ =>
    first [ does_not_have Y;
            let DET := fresh "DET" in
            assert (DET := A H)
          | does_not_have Z;
            let DET := fresh "DET" in
            assert (DET := B H) ]
  end.

Goal X -> True.
intros X. more_detail. more_detail.
(* This fails *)
more_detail.
Abort.

このdoes_not_haveタクティックは否定的な一致として機能します。引数がコンテキストに存在しない場合にのみ成功します。仕組みは次のとおりですH : Z。コンテキストに が存在する場合、最初の分岐が一致します。単純にfailorfail 0を呼び出すと、そのブランチは失敗しますが、Ltac は同じ の他のブランチを試すことができmatchます。を使用するfail 1と、現在のブランチと一致全体が失敗します。コンテキストに が存在しない場合H : Z、最初の分岐は一致せず、Coq はそれをスキップして 2 番目の分岐を試みます。このブランチは何もしないので、実行はmatch.

ではmore_detail、firstタクティカルを使用して のいくつかの呼び出しを組み合わせることができますdoes_not_have。コンテキストに対応する仮説が含まれている場合、の各ブランチfirstは失敗するため、全体としての構築はmatch否定的なパターンでの効果があります。

于 2015-02-09T15:23:10.807 に答える