2

exist私の質問は、条件/仮説のセットで用語を構築する方法に関連しています。

次の中間証明状態があります。

X : Type
P : X -> Prop
H : (exists x : X, P x -> False) -> False
x : X
H0 : P x -> False
______________________________________(1/1)
P x

H0のおかげで、xが の証人であることはわかっているので(exists x : X, P x -> False)、名前を紹介したいと思います。

w: (exists x : X, P x -> False)

上記の推論に基づいて、それを とともに使用して、仮説でapply H in wを生成し、最後にを生成します。FalseinversionFalse

しかし、上記の証人を紹介するためにどの戦術/構文を使用すればよいかわかりませんw。これまでに到達できる最高のものはCheck (ex_intro _ (fun x => P x -> False) x H0)).、False.

誰かが存在条件を導入する方法、または証明を完了するための代替方法を説明できますか?

ありがとう。

PS定理全体を証明するために私が持っているのは次のとおりです。

Theorem not_exists_dist :
  excluded_middle ->
  forall (X:Type) (P : X -> Prop),
    ~ (exists x, ~ P x) -> (forall x, P x).
Proof.
  unfold excluded_middle. unfold not. 
  intros exm X P H x.

  destruct (exm (P x)).
    apply H0.
    Check (H (ex_intro _ (fun x => P x -> False)  x H0)).
4

2 に答える 2

2

assert次の戦術を使用できます。

assert(w: exists x, P x -> False).

このステートメントを新しいサブゴールで証明するよう求めwられ、既存のゴールに追加されます。この種の自明な証明では、証明を直接インライン化できます。

assert(w: exists x, P x -> False) by (exists x; exact H0).
于 2015-10-15T06:52:52.067 に答える