問題タブ [coqide]

ソフトウェア基盤の plf フォルダーにある coq でファイル hw5.v をコンパイルしようとしています。バインディングを解決したいので、次のコマンドを使用します。

coqc -Q.PLF hw5.v

しかし、それはコンパイルされず、エラーとして coqc: -Q.PLF: no such file or directory が表示されます。これは今までにないことです。man coqc または coqc -v を実行すると、正しい出力が得られます。ただし、-Q または -R では機能しません。これを解決するアイデアはありますか？私のコックのバージョンは: 8.9.1

それで、「計算論理入門」スクリプトを使って Coq を学ぼうとしていて、練習問題が与えられました。「forall ab, a + S b = S (a + b)」を証明することです。「nat_ind」の定義が与えられます。

私はこれを試み、この方法を使用して問題を解決しましたが、うまくいきました：

問題は、同じ問題を解決しなければならないということですが、帰納補題をすぐに適用する必要があり、それを行う前にイントロや帰納戦術を使用することはできません。どうすればいいですか？

最初の試行から最初の行を削除しようとしましたが、「現在の環境で参照 b が見つかりませんでした」というエラーがスローされます。

更新：私はどこかに行きました。これは私の現在のコードです：

最後のサブゴールは単なる nat であり、どうすればよいかまったくわかりません。