問題タブ [coq-tactic]
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でif-then-elseを単純化するために不等式を使用する方法は?
私は証明の途中で、2 つのケースを生成しました。
(eq_id_decは本質的に に似ていますeq_nat_dec)。
e: Y = Xこれにより、それぞれ平等と不平等の仮定が追加された 2 つのケースが得られn: Y <> Xます。
rewrite e最初のケースでは、またはを簡単に使用できますrewrite <- e。
しかし、2番目のケースで不平等を効率的に利用するにはどうすればよいでしょうか? たとえば、次のような目標を考えてみましょう
?
unfold eq_id_dec私はいくつかのSを試しrewriteましたが、動けなくなりました。
coq - Coqで(n = n) = (m = m)を証明する方法は?
PropCoqのエビデンスなどについて混乱しています。それをどのように証明し(n = n) = (m = m)ますか？
私の意図は、これがどういうわけかであることを示すことですTrue=True。しかし、これは正しい定式化ですか？
私がこれまでに試したことは次のとおりです。
しかしsimpl.、何もしませreflexivityん。これは単なる例です。一般に、X可能であればどのタイプでもこれを証明する必要があります。
coq - Coqで存在変数を解決できるリングまたはフィールド戦術はありますか?
私はそれを知ってringおり、fieldのようないくつかの等式で使用できますa + x = b + y。存在変数の値を決定できる存在バージョンがあるかどうか疑問に思っていますか?
たとえば、次のものがあります。
?s = r2 * r2 - r1 * r1これで解決することがわかります。eringしかし、私が手動で計算する代わりに、Coq に計算をさせることができるような戦術はありますか?
coq - 「リライト[含意のある仮説]」の使い方
CIS 500 Software Foundations course CIS 500 Software Foundations course . 現在MoreCoqにいます。の部分がわかりませんrewrite IHl1。それはどのように機能していますか？以前に使用したときにこれが機能しないのはなぜsimplですか?