1

を証明しようとしていますがP ?x、ここでP : A -> Propと?x : Aは存在変数です。を証明できるので、 に一般化するforall a:A, P a必要があります。P ?xforall a:A, P a

?x がインスタンス化された変数 x である場合、単純に を使用generalize xして を生成できforall x:A, P xます。しかし、試してみるとgeneralize ?x、Coq は構文エラーを返します。

これは可能ですか？私が調べたところ、Coq は、存在変数に関するステートメントを一般化する直感的な方法を提供していないようです。

どんな助けでも大歓迎です。

4

1 に答える 1

4

P ?xと同等ではなくforall x, P x、それによって暗示されることさえありません。を証明するには、成り立つP ?xものを見つける必要があります。あなたの仮説では、いくつかを見つけるだけで十分です。つまり、ドメインが空でないことを証明する必要があります (より正確には、ドメイン内に要素が存在することを証明する必要があります)。aP aa : A

ここで、 があればa : A、 を使用できますinstantiate (1 := A)。愚かな例:

Parameter A : Set.
Parameter P : A -> Prop.
Goal (forall a, P a) -> A -> exists x, P x.
Proof.
  intros H a. eexists. instantiate (1 := a). apply H.
Qed.
于 2012-08-31T15:03:23.420 に答える