quand le `:` (deux-points) est-il nécessaire dans ssreflect/Coq?

Question

J'essaie de comprendre la signification exacte du : (deux points) dans les preuves de Coq/ssreflect en termes de Coq non-ssreflect. J'ai lu que cela a quelque chose à voir avec le déplacement de choses vers l'objectif (comme généraliser ??) et est l'opposé de =>, qui déplacent les choses vers les hypothèses. Cependant, je trouve souvent cela confus parce que les preuves fonctionnent de toute façon avec ou sans le :. Voici un exemple d'un tutoriel:

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

où,

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

est un lemme qui dit que si le miroir d'un arbre est une feuille, puis l'arbre est une feuille.

Je ne comprends pas pourquoi nous avons besoin du : ici et ne faisons pas simplement le Coq apply. En fait, si je supprime le :, cela fonctionne très bien. Pourquoi fait-il une différence?

Answer 1

Je pense avoir trouvé la réponse en lisant la documentation de SSReflect. Essentiellement, SSR a redéfini les tactiques telles que apply de telle sorte qu'il fonctionne sur la première variable de l'objectif plutôt que sur quelque chose dans le contexte. C'est pourquoi le : est utilisé dans apply: XX. de manière SSR (ce qui équivaut à move: XX; apply.), et cela fonctionne également si : est omis car c'est la méthode traditionnelle de Coq.

Citant la documentation:

De plus, la tactique ssreflect redéfinit Coq de base cas, élim et appliquer afin qu'ils puissent mieux tirer parti des ':' et '=>'. Ces tactiques Coq requièrent un argument du contexte mais opèrent sur l'objectif . Leurs homologues SSReflect utilisent à la place la première variable ou constante , donc ils sont "purement déductifs":

ils n'utilisent pas ou ne modifient pas le contexte de preuve. Il n'y a pas de perte puisque `: 'peut facilement être utilisé pour fournir la variable requise.

Answer 2

En effet, apply: H1 ... Hn est à tous les effets équivalents à move: H1 .. Hn; apply. Une application plus intéressante d'appliquer est apply/H et ses variations, qui peuvent interpréter les vues.