Coqで（forall x、P x / \ Q x）->（forall x、P x）をどのように証明しますか？何時間も試してみましたが、Coqが消化できるものに先行詞を分解する方法を理解できません。（私は初心者です、明らかに:)
質問する
3194 次
5 に答える
6
Hを適用するだけでより迅速に実行できますが、このスクリプトはより明確になるはずです。
Lemma foo : forall (A:Type) (P Q: A-> Prop), (forall x, P x /\ Q x) -> (forall x, P x).
intros.
destruct (H x).
exact H0.
Qed.
于 2010-06-03T20:14:39.693 に答える
2
試す
elim (H x).
于 2009-05-07T19:49:37.770 に答える
2
実際、私はこれを見つけたときにこれを理解しました：
レッスン5では、彼はまったく同じ問題を解決し、「cut（P x / \ Q x）」を使用して、目標を「Px」から「Px / \ Qx->Px」に書き直します。そこからいくつかの操作を行うことができ、目標が「P x / \ Q x」だけの場合は、「forall x：P x / \ Q x」を適用でき、残りは簡単です。
于 2009-05-09T17:11:08.583 に答える
2
Assume ForAll x: P(x) /\ Q(x)
var x;
P(x) //because you assumed it earlier
ForAll x: P(x)
(ForAll x: P(x) /\ Q(x)) => (ForAll x: P(x))
直感的には、すべてのxについて、P（x）およびQ（x）が成り立つ場合、すべてのxについて、P（x）が成り立ちます。
于 2010-06-03T20:24:19.437 に答える
-1
ここに答えがあります：
Lemma fa_dist_and (A : Set) (P : A -> Prop) (Q: A -> Prop):
(forall x, P x) /\ (forall x, Q x) <-> (forall x : A, P x /\ Q x).
Proof.
split.
intro H.
(destruct H).
intro H1.
split.
(apply H).
(apply H0).
intro H.
split.
intro H1.
(apply H).
intro H1.
(apply H).
Qed.
このファイルで他の解決された演習を見つけることができます：https ：//cse.buffalo.edu/~knepley/classes/cse191/ClassNotes.pdf
于 2019-10-27T20:56:27.737 に答える