如何用ssreflect反思：无法用 "n=n0 "统一?x==?y

Question

EDIT：我找到了! 我都忘了还有个胁迫。请忽略这个:)

我正在学习ssreflect，在这里被卡住了，不知道该如何进行。我的证明状态如下。

 n, n0 : nat
  ============================
  n = n0 -> n == n0

一开始我试着moveeqP 因为我以为这样就能把eqP应用到n=n0上 "应用 "的意思是 "从eqP的反射中得到n==n0":

Illegal application (Non-functional construction): 
The expression "eqP ?i" of type "?x = ?y"
cannot be applied to the term
 "?y0" : "?T0"

我搞不清楚y0和T0应该是什么.

intros H. eapply (introT eqP) in H.

产生错误的

Unable to apply lemma of type "?x = ?y -> ?x == ?y"
on hypothesis of type "n = n0".

我试着将显式参数n0和n传递给eqP，只是想看看是否能成功，结果是

pose proof (eqP n n0).但这给出了一个错误的

In environment
n, n0 : nat
H : n = n0
The term "n" has type "nat"
while it is expected to have type
 "is_true (?x == ?y)".

所以，看起来 eqP 既想要又不想要显式实例的 ?x 和 ?y。我真的很感激一些概念性的解释，为什么 moveeqP 没有按照我认为的方式行事，以及 eqP 和 (introT eqP) 的类型到底是怎么回事。

如果相关的话，我正在导入

From mathcomp Require Import ssrnat ssreflect ssrfun ssrbool eqtype. 

从ssreflect。

谢谢你。

Answer 1

愚蠢的错误! 我有一个胁迫，我忘了，我的实际证明状态是Nat n = Nat n0 -> n ==n0。