В языке тактики coq, в чем разница между вступлением и вступлением - PullRequest
Новая
       5

В языке тактики coq, в чем разница между вступлением и вступлением

0 голосов
/ 26 апреля 2018

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

intro

и

intros?

1 Ответ

0 голосов
/ 26 апреля 2018

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
...