Как сделать шаг через точку с запятой в тактике? - PullRequest
Новая
       72

Как сделать шаг через точку с запятой в тактике?

4 голосов
/ 20 сентября 2019

при построении доказательства в кокиде, я не нашел способа сделать шаг, хотя 

T1; T2; T3; ...; Tn.

одна тактика за одну тактику.Поэтому очень трудно построить правильное доказательство, как в коде выше.Итак, мой вопрос:

  • Есть ли способ пошагового выполнения кода выше или
  • Как создать доказательство, как код выше?

Впередодна команда или переход к курсору не работают.

1 Ответ

7 голосов
/ 20 сентября 2019

t1 ; t2 - это не то же самое, что сначала t1, а затем t2.Если вы хотите сделать это, вы можете сделать t1. t2., и это способ пройти через них.

Точка с запятой служит трем целям, указанным для t1 ; t2:

  • Itприменяется t2 во всех подцелях, сгенерированных t1;
  • , и позволяет откатить назад, если t2 потерпит неудачу, он попытается использовать другой success для t1и примените t2 снова к сгенерированным подцелям;
  • в-третьих, это самый простой способ записать тактику, представляющую последовательность тактик.

Если вам повезет иэто первый или третий случай, затем вы можете изменить сценарий, заменив 

t1 ; t2

на 

t1. all: t2.

с помощью селекторов целей.Таким образом, первый шаг позволит вам увидеть цели, сгенерированные t1, а второй покажет, как t2 влияет на них.Если вам нужна большая точность, вы также можете сфокусировать одну из подцелей, чтобы увидеть t2 в действии.

Когда происходит возврат, становится намного сложнее понять, что происходит, но я полагаю, что этого можно избежать приво-первых, или ограничивается простыми случаями.Например, можно сказать, что цель можно закрыть, применив правило введения (constructor), и тогда это должно быть легко.Если применяются несколько вступительных правил / конструкторов, выполнение 

constructor. easy.

может привести к сбою, а 

constructor ; easy.

может быть успешным.В самом деле, если easy не удастся на первом конструкторе, coq попробует второй и т. Д.

Чтобы ответить на ваш вопрос о том, как их написать, я полагаю, это может быть результатом проб и ошибок,и может в основном происходить из факторизации или автоматизации сценариев проверки.Допустим, у вас есть следующий сценарий проверки: 

split.
- constructor.
  + assumption.
  + eassumption.
- constructor. eassumption.

Возможно, вы захотите обобщить его следующим образом: 

split ; constructor ; eassumption.

Лично я не обязательно рекомендую его, поскольку его становится сложнее поддерживать итруднее читать другим пользователям из-за того, что они не могут пройти.Я бы ограничил эти два случая, когда доказательство является принципиальным (например, применяя конструктор и покончим с ним), и прибегал к селекторам целей для факторизации.

...