問題タブ [ltac]
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 - Ltac パターン マッチング: なぜ「forall x, ?P x」は「forall x, x」と一致しないのですか?
私は素朴に成功することを期待checkForall Hしますが、そうではありません。
Adam Chlipalaは、彼の著書Certified Programming with Dependent Typesで、依存型に対するパターン マッチングの制限について説明しています。
問題は、統合変数にローカルにバインドされた変数が含まれていない可能性があることです。
これが私がここで見ている動作の理由ですか?
coq - ltac : オプションの引数の戦術
coq で 1 つまたは 3 つの引数を取る Ltac タクティックを作成したいと考えています。モジュールについて読んだことltac_No_argがありLibTacticsますが、それを正しく理解していれば、次の方法で戦術を呼び出す必要があります。
これはあまり便利ではありません。
このような結果を得る方法はありますか? :
coq - Ltac : forall 仮説をインスタンス化する
私は2つの新しい仮説を作成する戦術に取り組んでいます
その形の仮説から
これが私のLtacコードです：
was はh、分解する仮説x、新しい変数tの名前、および新しい仮説の名前です。戦術は意図したとおりに機能しますが、証明の最後に次のようになります。
このevar戦術は、既存のタイプを使用する代わりに、D という名前の新しいタイプを作成したようです。私が使用する場合は注意してください
代わりにcoqtopでは完全に機能します。
coq - ltac の単一出現を書き換える
rewriteltac で呼び出して 1 つのオカレンスのみを書き換えるにはどうすればよいですか? coqのドキュメントに何か言及されていると思いますrewrite atが、実際に実際に使用できておらず、例もありません。
これは私がやろうとしていることの例です: