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

Question

Я пытаюсь понять точный смысл : (двоеточие) в Coq/ssreflect доказательствах в терминах non-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. в пути ssr (что эквивалентно move: XX; apply.), и оно также работает, если : опущено, как это традиционный способ Coq.

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

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

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

Answer 2

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