問題タブ [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 - 可変アリティの戦術
複数の仮説を一度にクリアする戦術が欲しいとしますclear_multiple H1, H2, H3.。次のように、ペアを使用してそれを実行しようとしました。
しかし、問題は、次のように括弧を配置する必要があることProdです。
私の質問は、Prods を使用せずにそれを行う方法ですか?
この質問を確認しましたが、必要な引数の数がわからないため、正確には必要ありません。
coq - Coq で方程式の両辺に群要素を掛ける Ltac の書き方
このグループの定義を使用すると、次のようになります。
そして、この定理を証明すると:
与えられた等式 (目標自体または仮説) に与えられた項を乗算するプロセスを自動化する Ltac をどのように記述すればよいでしょうか?
理想的には、証明でこの Ltac を使用すると、次のようになります。
coq - ltac の unfold 表記
表記の扱いが異なることに気付きました。たとえば、<は通常の定義の単なる表記でありunfold "<"、次の例のように機能します。
ただし、次の例のように<=、表記法が型に関連付けられておりle、何らかの理由unfold "<="で機能しません。
で失敗しUnable to interpret "<=" as a referenceます。
ltac コマンドで変換できます4 <= 5か?le 4 5