6

Coqのドキュメントには、組み込みの命名メカニズムに依存しないように一般的な警告が記載されていますが、命名メカニズムの変更によって過去の証明が無効にならないように、自分の名前を選択してください。

フォームの式を検討するときはremember Expr as v、変数vを式に設定しますExpr。しかし、仮定の名前は自動的に選択され、のようなものなので、次Heqvのようになります。

Heqv: v = Expr

代わりに自分の名前を選択するにはどうすればよいHeqvですか？コマンドを使用していつでも好きな名前に変更できますがrename、Coqに組み込まれている名前付けメカニズムの将来の変更に関係なく証明を維持することはできません。

4

1 に答える 1

5

個別の平等を取り除くことができる場合は、を試してくださいset (name := val)。unfoldの代わりにを使用rewriteして、値を元の場所に戻します。

以上の平等が必要な場合、rewrite <-これを行う組み込みの戦術はありません。ただし、手動で行うことも、戦術/表記法を作成することもできます。これを一緒に投げました。（注：私は専門家ではありません。これはもっと簡単にできるかもしれません。）

Tactic Notation "remember_as_eq" constr(expr) ident(vname) ident(eqname) :=
  let v     := fresh in
  let HHelp := fresh in
    set (v := expr);
    (assert (HHelp : sigT (fun x => x = v)) by ( apply (existT _ v); reflexivity));
    inversion HHelp as [vname eqname];
    unfold v in *; clear v HHelp;
    rewrite <- eqname in *.

remember_as_eq (2+2) four Heqfourと同じ結果を得るには、asを使用しremember (2+2) as fourます。

注：より多くのケースを処理するように更新されました。古いバージョンは、値と目標タイプのいくつかの組み合わせで失敗しました。これでは機能するが、これでは機能しない別のケースを見つけた場合は、コメントを残してくださいrewrite。

于 2012-07-17T01:09:28.577 に答える