証明のコンテキストで仮説を再帰的に反転するための戦術を定義するのに問題があります。たとえば、次のような仮説を含む証明コンテキストがあるとします。
H1 : search_tree (node a (node b ll lr) (node c rl rr))
仮説を繰り返し反転して、仮説を含む証明コンテキストを取得したい
H1 : search_tree (node a (node b ll lr) (node c rl rr))
H2 : search_tree (node b ll lr)
H3 : search_tree (node c rl rr)
H4 : lt_tree a (node b ll lr)
H5 : gt_tree a (node c rl rr)
H6 : lt_tree b ll
H7 : gt_tree b lr
H8 : lt_tree c rl
H9 : gt_tree c rr
もちろん、この証明コンテキストを取得するのは、反転戦術を繰り返し適用することで簡単です。ただし、仮説を反転すると、異なる仮説が異なるサブゴールに入れられることがあり、それぞれを反転するかどうかは、反転によって提供される情報の性質によって異なります。
明らかな問題は、証明コンテキストに対する無差別なパターンマッチングが非終了を引き起こすことです。たとえば、元の仮説を反転した後も保持したい場合、以下は機能しません。
Ltac invert_all :=
match goal with
| [ H1 : context [ node ?a ?l ?r ] |- ?goal ] => invert H1; invert_all
| _ => idtac
end.
これを行う簡単な方法はありますか？明らかな解決策は、すでに反転した仮説のスタックを保持することです。もう1つの解決策は、特定の深さまで仮説を反転することです。これにより、Ltacでの再帰呼び出しが削除されます。