問題タブ [apply-script]

補題があり、たとえばmylem: foo ?a = bar ?aが 2 回出現するゴールにそれを適用する必要があるとしますが、これらの位置の 1 つだけです。複雑な式になる可能性のある, ...をすべて書き出す必要なく、それを行う 2 つの方法を知っています。foobaz (foo (f p q)) (foo (g r s))pq

• 適切な数 (ここでは 0 または 1) のコマンドapply (subst mylem)が続きます。back
• を使用します。apply (subst mylem[where a = 'foo x y', standard])ここで、xおよびyはバインドされていない名前です。

ここでの使用はsubstデモンストレーションのためだけです。私は本当に補題を変更したいと思っています。たとえば、ruleこの方法で曖昧さをなくしたい複数の可能な一致がある場合に使用します。

どちらのアプローチも、私には悪いスタイルに見えます。それを達成するためのより良い方法はありますか？

単純な帰納的に定義された集合について補題があるとしましょう:

(「⋀x y」ビットが残ることは私にとって重要です。補題は、長い適用チェーンの途中で私の証明の状態を実際に述べているからです。)

この補題の証明を開始するのに問題があります。ルール誘導で進めたいと思います。

最初の試み

書いてみた

しかし、それはうまくいきません:inductメソッドは失敗します。x次のように、y明示的に修正してからメソッドを呼び出すことで、これを回避できることがわかりましinductた。

ただし、実際には適用チェーンの途中なので、構造化された証明ブロックには入りたくありません。

2 回目の試行

代わりにメソッドを使用してみましinduct_tacたが、残念ながら、ルールを希望どおりにinduct_tac適用できません。foo.induct入力すると

最初のサブゴールは

qux x []これは私が望むものではありません:の代わりに欲しかったのですqux x y。このinduct方法はこれを正しく行いましたが、上記で説明した他の問題がありました。