4

Coq 8.5pl1 を使用しています。

人為的ではあるが実例となる例を作るために、

(* fix so simpl will automatically unfold. *)
Definition double := fix f n := 2*n.

Theorem contrived n : double (2 + n) = 2 + double (1 + n).

ここで、引数を double に単純化するだけで、それ以外の部分は単純化しません。（たとえば、残りはすでに慎重に正しい形に入れられているためです。）

simpl.
   S (S (n + S (S (n + 0)))) = S (S (S (n + S (n + 0))))

これにより、外側の (2 + ...) が (S (S ...)) に変換され、ダブル展開が行われました。

次のようにして、それらの1つに一致させることができます。

match goal with | |- (double ?A) = _ => simpl A end.
   double (S (S n)) = 2 + double (1 + n)

それらすべてを単純化したいというのはどうすればよいでしょうか。つまり、手に入れたい

   double (S (S n)) = 2 + double (S n)

double への呼び出しごとに個別のパターンを配置する必要はありません。

double 自体を除いて単純化できます

remember double as x; simpl; subst x.
   double (S (S n)) = S (S (double (S n)))
4

2 に答える 2

5

不透明/透明なアプローチ

この回答とこの回答の結果を組み合わせると、次の解決策が得られます。

Opaque double.
simpl (double _).
Transparent double.

のパターン機能を使用してsimpl、その「アクション ドメイン」を絞り込み、Opaque/Transparentの展開を禁止 (または許可) しdoubleます。

カスタム戦術アプローチ

引数を単純化するためのカスタム戦術を定義することもできます:

(* simplifies the first argument of a function *)
Ltac simpl_arg_of function :=
  repeat multimatch goal with
         | |- context [function ?A] =>
              let A' := eval cbn -[function] in A in
                change A with A'
         end.

このlet A' := ...構造は、ネストされた関数を単純化から保護するために必要です。簡単なテストを次に示します。

Fact test n :
    82 + double (2 + n)
  =
    double (1 + double (1 + 20)) + double (1 * n).
Proof.
  simpl_arg_of double.

上記の結果は

82 + double (S (S n)) = double (S (double 21)) + double (n + 0)

context [function ?A] => simpl Aの定義のようなものを使用していたらsimpl_arg_of、得られたでしょう

82 + double (S (S n)) = double 43 + double (n + 0)

代わりは。

引数ディレクティブ アプローチ

コメントで @eponier が示唆しているように、さらに別の形式のsimpl--を利用できますsimpl <qualid>。これは、マニュアルで次のように定義されています。

これはsimpl、ヘッドオカレンスが展開可能な定数qualidである適用可能なサブタームにのみ適用されます(そのような表記法が存在する場合、文字列を使用した表記法によって定数を参照できます)。

Opaque/アプローチはそれTransparentでは機能しませんが、ディレクティブをdouble使用して展開をブロックできます。Arguments

Arguments double : simpl never.
simpl double.
于 2016-12-31T11:04:06.653 に答える
2

ここでは、ssreflect パターン選択言語と書き換えメカニズムが役立つことがあります。たとえば、パターン + simpl operator を使用して、より細かい制御を行うことができます/=。

From mathcomp Require Import ssreflect.
Definition double := fix f n := 2*n.
Theorem contrived n : double (2 + n) = 2 + double (1 + n).
rewrite ![_+n]/=.

表示されます:

n : nat
============================
double (S (S n)) = 2 + double (S n)

匿名の書き換えルールも使用できます。

rewrite (_ : double (2+n) = 2 + double (1+n)) //.

私は個人的に、より小さな補題で書き直しを因数分解します。

Lemma doubleE n : double n = n + n.
Proof. by elim: n => //= n ihn; rewrite -!plus_n_Sm -plus_n_O. Qed.

Lemma doubleS n : double (1 + n) = 2 + double n.
Proof. by rewrite !doubleE /= -plus_n_Sm. Qed.

Theorem contrived n : double (1+n) = 2 + double n.
rewrite doubleS.
于 2016-12-31T14:43:19.197 に答える