Как применить тактику к последовательности - PullRequest
Новая
       77

Как применить тактику к последовательности

0 голосов
/ 27 июня 2019

Глубоко погружаясь в test_nostutter_1 упражнения, я нашел способ решить это без повторов: 

Example test_nostutter_1: nostutter [3;1;4;1;5;6].
Proof.
  constructor 3.
  (* This will apply the tactics to the 2-nd subgoal *)
  2: {apply eqb_neq. auto. }
  constructor 3.
  2: {apply eqb_neq. auto. }
  constructor 3.
  2: {apply eqb_neq. auto. }
  constructor 3.
  2: {apply eqb_neq. auto. }
  constructor 2.
Qed.

Я решил поиграть с ним побольше, и в справочном руководстве по coq я обнаружил, что есть do тактика , которая может зациклить тактику несколько раз. 

do num expr

expr оценивается как v, что должно быть тактическим значением. Эта тактическая величина v применяется num раз. Предположим, что число> 1, после первого применение v, v применяется, по крайней мере, один раз, к сгенерированному подцели и так далее. Это терпит неудачу, если приложение v терпит неудачу прежде, чем num заявок было завершено.

Итак, я попробовал это: 

do 4 constructor 3; 2: {apply eqb_neq. auto. }

Но, к сожалению, это не удается. Только это работает: 

do 1 constructor 3.

Можно ли заставить его работать с помощью do?

1 Ответ

2 голосов
/ 28 июня 2019

Ответ

Есть несколько проблем в строке 

do 4 constructor 3; 2: {apply eqb_neq. auto. }

Прежде всего, вы не можете использовать 2: или {} после оператора цепочки ;,Самое близкое, что вы можете использовать, это последовательность с локальным приложением tac; [tac1 | tac2].Поскольку мы хотим что-то сделать только для второй ветви, мы можем опустить tac1 здесь.

Кроме того, вы не можете использовать точки внутри тактики.Точка отмечает конец оператора, но все выражение do является одним оператором.Вы должны всегда использовать оператор последовательности ; для объединения нескольких тактик.

Наконец, do n tac; tac работает как (do n tac); tac.Вы можете обернуть тактическое выражение в круглые скобки, например, do n (tac; tac), чтобы изменить поведение.

Так что это должно работать: 

do 4 (constructor 3; [ | apply eqb_neq; auto ]).

Отступление

Мыможет упростить линию несколькими способами.

  • auto могут быть предоставлены дополнительные теоремы для автоматизации.Любая цель, решаемая с помощью apply eqb_neq; auto, также может быть решена с помощью auto using eqb_neq. 
do 4 (constructor 3; [ | auto using eqb_neq ]).
  • Тактика auto никогда не заканчивается, поэтому ее можно безопасно использовать на обеих ветвях. 
do 4 (constructor 3; auto using eqb_neq).
  • repeat повторяется до тех пор, пока что-то не выйдет из строя или не останется никаких подцелей.Следующее будет повторяться до тех пор, пока третий конструктор больше не будет применим. 
repeat (constructor 3; auto using eqb_neq).
  • Мы можем позволить Coq выбрать, какой конструктор применить.Это может закончить (или почти закончить) доказательство. 
repeat (constructor; auto using eqb_neq).
  • Мы также можем сделать конструкторы nostutter автоматизированными с помощью auto с помощью команды Hint Constructors.Теперь мы можем auto все это.(Вы можете поместить команду подсказки сразу после определения nostutter, затем вы можете auto ее везде.) 
Hint Constructors nostutter.
auto using eqb_neq.
(* if the above fails, the following increases the search depth so it should succeed. *)
auto 6 using eqb_neq.
  • На самом деле, теорема eqb_neq ужезарегистрирован на auto.Так что мы можем просто: 
auto 6.
...