Когда необходимо использовать `:` (двоеточие) в ssreflect/Coq?

Question

Я пытаюсь понять точное значение : (двоеточие) в Coq/ssreflect доказательствах в терминах не-ssreflect Coq.

Я читал, что это как-то связано с движением вещей к цели (как обобщение??) и является противоположностью =>, которые двигают вещи в гипотезы. Тем не менее, я часто нахожу это запутанным, потому что доказательства работают так или иначе с или без :, Ниже приведен пример из учебника:

Lemma tmirror_leaf2 t : tmirror (tmirror t) = Leaf -> t = Leaf.
Proof.
move=> e.
by apply: (tmirror_leaf (tmirror_leaf e)).
Qed.

где,

tmirror_leaf
     : forall t, tmirror t = Leaf -> t = Leaf

это лемма, которая говорит, что если зеркало дерева - это лист, то дерево - это лист.

Я не понимаю, зачем нам : здесь, а не просто сделать Coq apply, На самом деле, если я удалю :, это работает просто отлично. Почему это имеет значение?

Answer 1

Я думаю, что нашел ответ, читая документацию SSReflect. По сути, SSR пересмотрел тактику, как apply такой, что он воздействует на первую переменную цели, а не на что-то в контексте. Вот почему : используется в apply: XX. в пути ССР (что эквивалентно move: XX; apply.), и это также работает, если : опущен, поскольку это традиционный способ Coq.

Цитирование документации:

Кроме того, SSReflect переопределяет базовый вариант тактики Coq, elim и apply, чтобы они могли лучше использовать ':' и '=>'. Эта тактика Coq требует аргумента из контекста, но действует на цель. Их аналоги SSReflect вместо этого используют первую переменную или константу цели, поэтому они являются "чисто дедуктивными":

они не используют и не изменяют контекст доказательства. Без потерь, поскольку `:'может быть легко использован для предоставления требуемой переменной.

Answer 2

В самом деле, apply: H1 ... Hn для всех эффектов, эквивалентных move: H1 .. Hn; apply, Более интересное применение применять apply/H и его вариации, которые могут интерпретировать взгляды.