7

Prop についての代入定理を証明しようとしていますが、惨めに失敗しています。次の定理は coq で証明できますか? そうでない場合は、その理由を教えてください。

  Theorem prop_subst:
    forall (f : Prop -> Prop) (P Q : Prop), 
      (P <-> Q) -> ((f P) <-> (f Q)).

ポイントは、証明は論理的には帰納法によるものだということです。私が見る限り、プロップは帰納的に定義されていません。そのような定理は Coq でどのように証明されるでしょうか?

4

3 に答える 3

8

答えは次のとおりです。私が探していたプロパティは命題拡張性と呼ばれ、それを意味しforall p q : Prop, (p <-> q) -> (p = q)ます。逆は些細なことです。Library Coq.Logic.ClassicalFactsこれは、古典的な、つまり非直観主義的な論理からの他の事実とともに、 で定義されているものです。上記の定義は と呼ばれprop_extensionality、次のように使用できますAxiom EquivThenEqual: prop_extensionality。これで、 を適用したり、書き換えに使用したりできますEquivThenEqual。拡張性について指摘してくれた Kristopher Micinski に感謝します。

于 2012-06-17T17:09:44.130 に答える
4

あなたが探しているのは「延長性」と呼ばれるものです:

http://coq.inria.fr/V8.1/faq.html#htoc41

http://coq.inria.fr/stdlib/Coq.Logic.FunctionalExtensionality.html

http://en.wikipedia.org/wiki/拡張性

編集：

Coq FAQ に記載されているように、述語拡張性を認めることができます。

于 2012-06-17T16:27:34.213 に答える