問題タブ [coqide]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
coq - Coq: リストペアの証明
私はこの帰納的述語とその (強い) 仕様の証明の一部を書きました:
問題は、Coq が のようなものを受け入れないため、定理が正しいとは思わないことです{n0 n1: nat | ...}。それを修正する方法はありますか、それとも私の考えが間違っていますか?
述語は正しいと思いますSumPairsが、よくわからないので、どのように機能するかの例を次に示します: 入力[(1,2),(3,4)]、期待される出力[3,7]
coq - エラー メッセージ: 不足している引数の数が正しくありません (1 が必要です)
次のコードを実行すると、エラー メッセージが表示されました。
どうしたら解決できるのか気になります。ありがとう。
coq - Coqで自動化戦術を使用せずにこのDeMorganの法則を証明する方法は?
これは私がここで証明しようとしている法則です:
どの方向に向かうべきかわからないところまでの私のコードは次のとおりです。
サブゴールとして示されているものと、私が持っている前提は証明可能であるように見えますが、動きは何ですか?
exfalso.、その後に行ってみましapply H.た。これにより、 の別の前提x : Xと のサブゴールが得られpxます。
後で何をすべきかわからない。助けてくれてありがとう！