問題タブ [ltac]

可変長の引数リストをループする Ltac 定義を作成しようとしているときに、Coq 8.4pl2 で次の予期しない動作に遭遇しました。誰かが私にそれを説明できますか？

ある仮説が存在し、別の仮説が存在しない場合にルールを適用したい。この状態を確認するにはどうすればよいですか?

例えば：

そのような、この目標のために：

more_detail.2 番目の仮説 DET を導入します。

そして、連続する呼び出しmore_detail.は失敗します。

ただし、とmore_detail.の両方が存在することを常に確認する必要があります。つまり、一方のみが存在する場合は、別のルールを実行する必要があります。YZ

と：

私は、match構築の助けを借りて定式化された仮説のルールを書こうとしています:

どうすればそのような仮説を一致させることができますか? 次の簡単な方法は失敗します。

coq では、タクティックには、destruct複雑な帰納型をアンパックする場合でも、ユーザーが導入された変数に名前を割り当てることができる「連言選言導入パターン」を受け入れるバリアントがあります。

coq の Ltac 言語により、ユーザーはカスタム タクティクスを記述できます。に制御を渡す前に何かを実行する戦術を書きたい (実際には維持したい) と思いdestructます。

カスタム タクティックで、ユーザーが、タクティックがdestruct.

これを実現するLtac構文は何ですか?

Coq で単純型付けされたラムダ計算を形式化する演習を行っており、Ltac を使用して証明を自動化したいと考えています。進行定理を証明しながら：

このLtacコードを思いつきました：

==>(スモールステップセマンティクスによる) 評価の単一ステップを示します。各一致ケースの意図は次のとおりです。

1. コンストラクターの最初の項がステップするという仮説がある場合、任意のバイナリコンストラクターに一致します。
2. コンストラクターのステップの 2 番目の項とコンストラクターの最初の項が既に値であるという仮説がある場合、任意のバイナリコンストラクターに一致します。
3. コンストラクターの項がステップするという仮説がある場合、任意の単項コンストラクターに一致します。

ただし、このコードの動作を見ると、3 番目のケースもバイナリコンストラクターと一致しているように見えます。実際に単項コンストラクターのみに一致するように制限するにはどうすればよいですか?