私は次のような形の目標を持っている状況にいます:
exists x : T1, f x = y.
どこy : T2とf : T1 -> T2。秘訣は、コンストラクターが対応するような方法でT1andを定義しT2たことです。そのため、人間にとって、どの値がx等式を保持するかを簡単に確認できます。
しかし、私には多数のケースがあり、スクリプトを堅牢にしたいので、そのようなx.
のそのような値を見つけるために証明検索を使用するにはどうすればよいxですか?
今、私はこのようなものを持っています (CPDT のクラッシュ戦術を借りています):
Ltac postpone :=
match goal with
| [ |- ?X] => let H := fresh "Arg" in evar (H : X); apply H
end
(unshelve eexists; [(constructor; postpone) | (crush ; fail) ]).
つまり、 の evar を作成し、それをアンシェルブしx、コンストラクターを使用して解決し、コンストラクターによって生成されたすべてのサブゴールに evar を入力し、プルーフ サーチを使用して等価性を判断します。
ただし、これは次のようになります。Error: Tactic failure.私の意図はconstructor、間違ったコンストラクターを選択した場合crush、目標を解決しないため、failバックトラッキングをトリガーすることでした。しかし、これは起こっていないようです。最初にヒットしたときに失敗していfailます。
私の質問
証明探索で存在変数の値を見つけるには、どのような戦略を使用できますか? constructorのバックトラッキングを使用して、存在を保持する値を見つけるにはどうすればよいですか?