どのようにして証明するか(forall x、P x/\ Q x) - >(forall x 、P x)何時間も試していて、Coqが消化できるものに前例を分解する方法を理解することはできません。 (私は明らかに、初心者くさいよ:)証明方法(forall x、P x) - (forall x、P x)
4
A
答えて
4
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.
2
が実際に
elim (H x).
2
を試してみて、私はこの見つかったとき、私はこの1つを考え出し:レッスン5では
Mathematics for Computer Scientists 2
が、彼は正確に解決を同じ問題があり、 "P x"から "P x/\ Q x - > P x"にゴールを書き換える "cut(P x/\ Q x)"を使います。そこからあなたはいくつかの操作を行うことができ、目的がちょうど "P x/\ Q x"のときは "forall x:P x/\ Q x"を適用することができ、残りは単純です。
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))
Intuitivlyに、すべてのxに対して、P(x)とQ(x)を保持している場合、すべてのxに対して、P(x)が成立します。
関連する問題
- 1. Coqに∀x(P(x)とQ(x))を書くにはどうすればいいですか?
- 2. が増分ポインタをDeferencingた(* p ++ = X)P
- 3. Pythonのデータフレーム:</p> <pre><code>df['x_norm'] = df.apply(lambda x: (x['X'] - x['X'].mean())/(x['X'].max() - x['X'].min()),axis=1) </code></pre> <p>が、次のエラーを得た:ラムダ
- 4. SSL証明書 - OS X Mavericks
- 5. は、私は例が</p> <pre><code>COL1 COL2 A X A X A X A X A X B X B X B X C X C X C X </code></pre> <p>Iされて、私はタイプA、BおよびCを持つSQLデータベースから情報を取得しようとしている
- 6. JAXBアンマーシャリングX、X *
- 7. Xページ認証
- 8. Java:Calc x in sin(x)
- 9. (function(x:<_))= xと(function(x:_))= xの違いは何ですか?
- 10. X.509証明書の生成
- 11. JavaでX.509証明書を読む
- 12. x 509ルート証明書確認
- 13. Xを法とする階(X)はXに等しいか?
- 14. OS Xアプリケーション認証
- 15. Mac OS X内でPEM形式のgoogle oauth X.509証明書を作成
- 16. x = x + yとx = y + xが時々異なるのはなぜですか?
- 17. Javascriptを:X = obj.fn対obj.fn(); X()
- 18. AngularJS: `{{x + '、' + y}}対{{x}}、{{y}} '
- 19. OS XでのリンカエラーX
- 20. "X x(42)"と "X x = 42"を使用したオブジェクト構成の違い?
- 21. Windows XPでx.509証明書を取得する方法
- 22. X.509証明書でcsrファイルを生成する方法
- 23. X.509証明書のSHA-1指紋の計算方法は?
- 24. Java keytoolコマンドラインインターフェイスでx.509証明書を生成する方法
- 25. PHP 5.2.xと5.3.x
- 26. OCAML:let func a x =(a x);;の違いfunc a x =((fun a - > a)x);;
- 27. Android:時間のミリ秒からX日 - X時間 - x分 - X秒の残り
- 28. x = 0x80000000の場合、〜(x-1)と〜x + 1の差
- 29. 各xについて...次へFor Each x ...次へx
- 30. シャドーイングの `let`バインディングを使用するこのコードはなぜハングアップしますか?インタプリタで</p> <pre><code>j = let x = 4 in let x = x * x in x </code></pre> <p>を:
∧(U + 2227:論理AND)と∀(U + 2200:FOR ALL)をお探しですか? –