На языке тактики coq в чем разница между интро и интро

На языке тактики Coq, в чем разница между

intro

и

intros?


coq coq-tactic
person nixon    schedule 26.04.2018    source источник

Ответы (1)


arrow_upward
10
arrow_downward

intro и intros ведут себя по-разному, если аргумент не указан

Согласно справочному руководству:

Если цель не является продуктом и не начинается с определения let, тактика intro применяет тактику hnf до тех пор, пока не может быть применена тактика intro или цель не может быть сведена к голове.

С другой стороны, intros, как вариант тактики intro,

повторяет intro, пока не встретит головную постоянную. Он никогда не уменьшает константы напора и никогда не выходит из строя.

Пример:

Goal not False.
  (* does nothing *)
  intros.
  (* unfolds `not`, revealing `False -> False`;
     moves the premise to the context *)      
  intro.
Abort.

Примечание: и intro, и intros делают одно и то же, если указан аргумент (intro contra / intros contra).

intros является многовариантным, intro может принимать только 0 или 1 аргумент

Goal True -> True -> True.
  Fail intro t1 t2.
  intros t1 t2.  (* or `intros` if names do not matter *)
Abort.

intro не поддерживает вводные шаблоны

Goal False -> False.
  Fail intro [].
  intros [].
Qed.

Некоторую информацию о вводных шаблонах можно найти в руководстве или в книге Основы программного обеспечения. См. также этот пример нетривиальной комбинации нескольких интро-паттерны.

intros не поддерживает переключатели after / before / at top / at bottom

Допустим, у нас есть такое состояние доказательства

H1 : True
H2 : True /\ True
H3 : True /\ True /\ True
==========
True /\ True /\ True /\ True -> True

тогда, например. intro H4 after H3 изменит состояние доказательства следующим образом:

H1 : True
H2 : True /\ True
H4 : True /\ True /\ True /\ True 
H3 : True /\ True /\ True
==========
True

и intro H4 after H1 произведет

H4 : True /\ True /\ True /\ True 
H1 : True
H2 : True /\ True
H3 : True /\ True /\ True
==========
True
person Anton Trunov    schedule 26.04.2018
comment
В руководстве немного неверно сказано, что intros повторяет intro - оно никогда не разворачивает определения, поэтому repeat intro отличается от intros. То, что он повторяет, это intro без шага hnf. - person Tej Chajed; 26.04.2018
comment
Я думаю, что в руководстве сказано то, что вы говорите во втором предложении: оно никогда не уменьшает постоянные напора ... - person Anton Trunov; 26.04.2018
comment
Да, это помогает прояснить ситуацию, но я все же думаю, что intros не повторяет intro, и в руководстве можно было бы подчеркнуть эту разницу (я считаю, что неожиданное развертывание имеет большое значение). Эта разница действительно удивила меня, когда я столкнулся с github.com/coq/coq/issues/5394. - person Tej Chajed; 26.04.2018