問題タブ [logical-foundations]

質問する

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.

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

coq - Coq: 非公式な証明を形式化するのに役立ちます

出力：

n は偶数でも非偶数でもかまいません。

  • n が偶数の場合、m も偶数です。定理によりev_sum(n+m) も偶数です。

  • n が偶数でない場合は、(n' + 1) の形式になります。n' は偶数です。m も偶数ではなく、(m' + 1) の形をしています。ここで、m' は偶数です。したがって、それらの合計は次のようになります。

    n + m = n' + 1 + m' + 1 => n + m = (n' + m') + 2.

偶数 ((n' + m') + 2)。( n apply ev_SS' + m') になったら。n' が偶数で m' が偶数であることがわかっているので、apply ev_sum. そして、これは定理を証明します。

この非公式な証明を coq でどのように記述しますか?


12345678910