4

次の定理を証明したい.

Theorem Frobenius (A: Set) (q: Prop) (p: A -> Prop) :
  (q \/ forall x : A, p x) -> (forall x : A, q \/ p x).

私はすでに次の証拠を手に入れました：

Proof.
intro.
intro.
destruct H.
left.
assumption.

でも今はどうしたらいいのかわからない状況です。以下のものは私の処分です：

A : Set
q : Prop
p : A -> Prop
H : forall x : A, p x
x : A

そして、次のサブゴールを証明したいと思います。

q \/ p x

指定された前提で forall 量指定子を削除するにはどうすればよいですか

forall x : A, p x

つまり、具体的な x : A をどのようにプラグインして、 px を推測できるようにできますか?

4

2 に答える 2

2

( ) を使用して、普遍的に量化xされた inをインスタンス化できます。 Hspecializespecialize (H x)

于 2016-03-14T19:02:09.510 に答える
0

おそらく最も単純な？

Theorem Frobenius (A: Set) (q: Prop) (p: A -> Prop) :
  (q \/ forall x : A, p x) -> (forall x : A, q \/ p x).
intro H.

elim H.
intros Hl x.
left.
exact Hl.

intros Hr x.
right.
apply Hr.
于 2016-03-14T20:00:49.253 に答える