1
私はBenjamin Pierceの第1巻、Software Foundationsを使って作業していますが、IndPropの章のいくつかの問題を抱えています。残念ながら、私はより良い場所を知りません：誰もヒントはありますか？ソフトウェア基盤：leb_completeとleb_correctを証明する
Theorem leb_complete : forall n m,
leb n m = true -> n <= m.
Proof.
(* FILL IN HERE *) Admitted.
Theorem leb_correct : forall n m,
n <= m ->
leb n m = true.
Proof.
(* FILL IN HERE *) Admitted.
これらは、オンラインテキストブックの練習問題です。解決策を提示しないでください。しかし、始める場所があると便利です。
あなたはfreenodeの上#coq IRCチャンネルに質問をすることができ、また、そこにある[このCoqのチャンネル]（https://functionalprogramming.slack.com/messages/C046CF6FP） Coqのためのチャンネル（私はこの質問がうんざりに適しているかどうかはわかりませんが）。それらは検索エンジンによってアクセス可能であってはなりません。 –
これは、すべての自然数のプロパティを証明する必要がある場合です。[オブジェクトを定義するだけなので、組み合わせ理論に従わない]ので、通常、誘導は通常適切なツールです。ただし、2つの数字があることに注意してください。誘導仮説が必要です。「n」がすべての「m」をカバーできるほど一般的であるとしましょう。これは重要なステップです.Coqの誘導戦略は実際にはうまく機能しません。 – ejgallego