Семантика tac1 ; tac2 заключается в запуске tac1, а затем tac2 для всех подцелей, созданных tac1. Таким образом, вы можете столкнуться с множеством случаев:
После бега не осталось голов tac1
Если после запуска tac1 не осталось целей, то tac2 никогда не запускается, и Coq просто молча завершает работу. Например, в этом первом выводе у нас есть бесполезный ; intros в конце (действительного) доказательства:
Goal forall (A : Prop), A -> (A /\ A /\ A /\ A /\ A).
intros ; repeat split ; assumption ; intros.
Qed.
Если мы изолируем это, мы получим Error: No such goal., потому что мы пытаемся применить тактику, когда нечего доказывать!
Goal forall (A : Prop), A -> (A /\ A /\ A /\ A /\ A).
intros ; repeat split ; assumption.
intros. (* Error! *)
После бега tac1 осталась ровно одна цель.
Если после запуска tac1 осталась ровно одна цель, то tac1 ; tac2 ведет себя как tac1. tac2. Основное отличие состоит в том, что если tac2 терпит неудачу, то же самое происходит и с tac1 ; tac2, потому что последовательность из двух тактик рассматривается как единое целое, которое может либо преуспеть в целом, либо потерпеть неудачу в целом. Но если tac2 преуспеет, то это в значительной степени эквивалентно.
Например. Следующее доказательство является действительным:
Goal forall (A : Prop), A -> (A /\ A /\ A /\ A /\ A).
intros.
repeat split ; assumption.
Qed.
Бег tac1 порождает более одной цели.
Наконец, если при запуске tac1 создается несколько целей, то tac2 применяется ко всем сгенерированным подцелям. В нашем текущем примере мы можем заметить, что если мы отключим последовательность тактик после repeat split, то у нас на руках будет 5 голов. Это означает, что нам нужно скопировать / вставить assumption пять раз, чтобы воспроизвести доказательство, данное ранее, с использованием ;:
Goal forall (A : Prop), A -> (A /\ A /\ A /\ A /\ A).
intros ; repeat split.
assumption.
assumption.
assumption.
assumption.
assumption.
Qed.
person
gallais
schedule
29.03.2016
