coq - Coqの自由変数

Question

Coqを使用して、自由変数、たとえばn:Uが項/式eに存在するかどうかを取得/チェックする関数/コマンドはありますか? 共有してください。

たとえば、この「n は e の自由名には現れない」と Coq で述べたいと思います。

ありがとう、

ウィラヤット

Answer 1

Coq用語で自由変数について話していると仮定しましょう：

初歩的なCoq証明（外部を何も使用しない）を扱う場合、操作するのは、証明コンテキストの外側で、閉じた項、つまり束縛変数のみを持つ項です。証明モードeで、目標の用語に自由変数があるように見える場合n（変数nが証明コンテキストのどこかにあることを意味します）、generalize戦術を使用してバインディングを明示的にする（そして目標用語を閉じる）ことができます。

より高度なケースでは、バニラの少ない証明に、仮定またはパラメーターの形式の自由変数が含まれる場合があります。その場合、を使用してそれらをリストできますPrint Assumptions。

一方、特定の言語で用語の概念を表すためにCoq用語を使用することについて話している場合（たとえば、そのような言語を形式化する場合）、単に言語の自由変数に特別な扱いをする必要があります。

言語の用語の帰納的定義で特定のコンストラクターを指定すると、一部の用語に自由変数があるかどうかを簡単に示すことができます。言語の置換と自由変数を表すという（それほど些細なことではない）概念に慣れていない場合は、TAPLからBCPierceのSFコース、POPLMarkチャレンジの結果に至るまで、精度のレベルが上がるポインターを見つけることができます。