Как смотреть на несколько целей одновременно?

avatar
Jason Hu
8 апреля 2018 в 00:42
406
1
5

Я рассматриваю возможность написания тактики, которая будет рассматривать несколько целей и принимать решения на основе этого. Однако, когда я использую match goal with и смотрю на цель, как мне сказать «пожалуйста, найдите другую цель, похожую на эту»?


Вернее, более общий вопрос: как я могу переключаться между целями в Ltac?

Источник
Heiko Becker
11 апреля 2018 в 14:25
0

Не могли бы вы привести минимальный пример, когда вы хотели бы «переключить» цели? После использования такой тактики, как destruct .. или induction ..., вы обычно видите все доступные цели и можете сфокусировать их, используя Focus n для n-й цели.

Jason Hu
11 апреля 2018 в 20:22
0

@nesreka, один простой случай: когда вы делаете dependent induction для определенного термина, индуктивная гипотеза может генерировать условие _ = _, которое в значительной степени ограничивает то, каким должен быть термин. после eapply гипотезы, из-за этого не так уж много вариантов остается, если она генерирует экзистенциальную переменную, в то время как auto/eauto недостаточно умны, чтобы понять это.

Heiko Becker
13 апреля 2018 в 06:40
0

Тогда может быть достаточно тактики типа all:? После выполнения dependent induction вы можете запустить ; subst, чтобы избавиться от равенств во всех ваших подцелях. Существует больше, чем all: тактика, которая определена в coq.inria.fr/distrib/current/refman/ltac.html#sec469 Дайте мне знать, подходит ли вам этот ответ, и я преобразовать его в один.

Jason Hu
13 апреля 2018 в 18:41
0

@nesreka subst не будет работать, ни селектор целей, так как он не участвует в потоке автопроверки. dependent induction часто включаются в более сложные структурные равенства и эвары, что здесь не совсем полезно. человек знает, что заполнять, и eauto иногда может заполнять правильно, если поиск доказательств случайно выполняется в правильном порядке. но это не детерминированное решение здесь.

Heiko Becker
16 апреля 2018 в 06:39
0

Можете ли вы объяснить, что вы имеете в виду под «не участвовать в процессе автоматического подтверждения»?

Jason Hu
16 апреля 2018 в 14:16
0

@nesreka попробуйте использовать селектор цели в тактике, и вы увидите. на самом деле селектор цели совершенно бесполезен, если доказательство автоматизировано с самого начала; и его использование также не имеет смысла, потому что тактика больше заботится о форме цели, чем о ее положении. я не думаю, что это обсуждение здесь плодотворно, поскольку мне уже ясно, что ответ отрицательный, и то, что вы сказали, не дает обходного пути для этого.

Heiko Becker
17 апреля 2018 в 09:28
0

Хорошо, не могли бы вы указать это как принятый ответ, что в настоящее время это невозможно? Или я могу ответить?

Jason Hu
17 апреля 2018 в 14:33
0

@nesreka, поскольку никто не дает ответа, который я хочу, и я прочитал весь refman, я не думаю, что в этом состоянии это возможно только в ltac.

Ответы (1)

avatar
Heiko Becker
25 апреля 2018 в 11:28
0

Как мы обсуждали в комментариях, это тот случай, когда достижение такого рода проверки текущей цели доказательства в настоящее время невозможно в Ltac.

Однако такую ​​тактику можно запрограммировать на уровне ocaml или на одном из новых тактических языков, таких как ltac2 или mtac.