4

Coq タクティックを使用するapply ... with場合、私が見た例はすべて、インスタンス化する変数の名前を明示的に指定することを含みます。たとえば、等式の推移性に関する定理があるとします。

Theorem trans_eq : forall (X:Type) (n m o : X),
  n = m -> m = o -> n = o.

それにapply：

Example test: forall n m: nat,
  n = 1 -> 1 = m -> n = m.
Proof.
  intros n m. 
  apply trans_eq with (m := 1). Qed.

最後の行で、インスタンス化する変数の名前はorまたはその他の名前ではなく、 でapply trans_eq with (m := 1).あることを覚えておく必要があります。mony

私にとって、定理の元のステートメントで使用されているかどうm n oかx y zは問題ではありません。それらはダミー変数または関数の仮パラメーターのようなものだからです。また、定理を定義するときに、私が使用した特定の名前や、他の誰かが別のファイルに書き留めた特定の名前を思い出せないことがあります。

たとえば、変数をその位置で参照して、次のようなものを使用できる方法はありますか?

apply trans_eq with (@1 := 1)

上記の例では？

ちなみに、私は試しました：apply trans_eq with (1 := 1).そして得ましたError: No such binder.

ありがとう。

4

2 に答える 2

6

適切な引数を使用して補題を特殊化できます。は_、特殊化したくないすべての引数に使用されます (推論できるため)。は、@暗黙の引数を特殊化するために必要です。

Example test: forall n m: nat,
  n = 1 -> 1 = m -> n = m.
Proof.
  intros n m. 
  apply (@trans_eq _ _ 1). 
Qed.
于 2015-10-06T23:16:16.220 に答える