Ltac: делайте что-то другое в каждой цели

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

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

Вот что у меня есть сейчас:

induction e;
    intros;
    pose (bool_dec (is_v_of_expr e1)) as ve1; destruct ve1;
    [> thing1 | thing 2].

что дает ошибку Incorrect number of goals (expected 26 tactics, was given 2).

Я пытаюсь сделать thing1 в первой цели из destruct и thing2 во второй цели из destruct для каждого случая, сгенерированного индукцией.

Проблема в том, что induction генерирует 13 подцелей, каждая из которых делится на 2 с помощью destruct. Локальный селектор [> thing1 | thing2 ] пытается сопоставить все подцели, а не только те, которые были созданы конкретной деструкцией.

Как я могу упорядочить тактику, чтобы destruct выполнялось для каждого случая, сгенерированного индукцией, затем thing1 запускалось для первой цели, сгенерированной разрушением, и thing2 запускалось для второй сгенерированной цели для каждого случая индукции.


dependent-type theorem-proving coq coq-tactic ltac
person jmite    schedule 28.07.2018    source источник

Ответы (1)


arrow_upward
2
arrow_downward

У вас есть две проблемы: (1) точки с запятой по умолчанию ассоциативны слева, и (2) синтаксис [> ] применяется ко всем сфокусированным целям, а не только к тем, которые были получены с помощью предыдущей тактики. (как указано выше) из Джейсона, это объяснение неверно, но ответ все еще работает :)

Вы можете решить эти проблемы, заменив [> ] на [ ] и правильно связав точки с запятой со скобками:

Goal ((True /\ True) /\ (True /\ True) /\ (True /\ True)).
  Fail (split; [|split]); split; [> exact I | exact I].
  (split; [|split]); (split; [exact I | exact I]).
Qed.

В вашем примере:

induction e; intros;
  pose (bool_dec (is_v_of_expr e1)) as ve1;
  (destruct ve1; [thing1 | thing 2]).
person Lily Chung    schedule 28.07.2018
comment
На самом деле ; полностью ассоциативен, а ; [...] связывается слабее, чем ;, и остается ассоциативным. Кроме того, все тактики неявно являются многоцелевыми и применяются ко всем целям, сфокусированным в данный момент. - person Jason Gross; 02.08.2018