問題タブ [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.

95 問題
Newest
Active
Bountied
318
Unanswered
0 投票する
1 に答える
64 参照

coq - サブゴールはすべて満たされているが、証明に焦点を当てることはできない

やや長い証明を書き終えましたが、試行するたびにQedエラーメッセージが表示されますError: This proof is focused, but cannot be unfocused this way。プルーフのフォーカスを外す他の方法はありますか? 私の証明は厳密ですが、私は単に認められたものを使用すべきですか? 参考までに、私はCoqIDE 8.6を使用しています

0 投票する
1 に答える
57 参照

coq - 同一の 2 つの仮説を統合することはできません

コンテキスト内に 2 つの仮説がありますが、1 つの仮説applyを別の仮説にしようとすると、エラーが発生しますunable to unify。私はそれらを統一できるはずです。2つの仮説は次のとおりです。

IHl : forallb func l = true -> All (fun x : X => func x = true) l H1 : All (fun x : X => func x = true) l

私の目標は、IHl を H1 に適用して、IHl から前提を取得することです。


12345678910