У меня проблемы с определением тактики рекурсивного инвертирования гипотез в контексте доказательства.Например, предположим, что у меня есть контекст доказательства, содержащий такую гипотезу, как:
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
Конечнополучить этот контекст доказательства легко, многократно применяя тактику обращения.Однако иногда инвертирование гипотезы приводит к тому, что разные гипотезы помещаются в разные подзадачи, и от того, будет ли инвертироваться каждая из них, зависит природа информации, предоставляемой инверсией.
Очевидная проблема заключается в том, что сопоставление образцов без разбора с контекстом доказательства приведет кnontermination.Например, следующее не сработает, если вы захотите сохранить исходные гипотезы после их инвертирования:
Ltac invert_all :=
match goal with
| [ H1 : context [ node ?a ?l ?r ] |- ?goal ] => invert H1; invert_all
| _ => idtac
end.
Есть ли простой способ сделать это?Очевидным решением было бы сохранить стопку уже перевернутых гипотез.Другое решение состоит в том, чтобы инвертировать гипотезы только до определенной глубины, что позволило бы удалить рекурсивные вызовы в Ltac.