编辑：我找到了！我忘记了强制。请忽略这个:)

我正在学习 ssreflect 并坚持如何在这里进行。我的证明状态如下：

起初，我尝试了 move/eqP，因为我认为这会将 eqP “应用”到 n=n0，其中“应用”的意思是“从 eqP 给出的反射中获取 n==n0”。然而，这种尝试产生了：

我对 y0 和 T0 应该是什么感到困惑。我也试过

intros H. eapply (introT eqP) in H.

产生了错误

我试图将显式参数 n0 和 n 传递给 eqP，只是为了看看它是否可以工作，

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

因此，似乎 eqP 既想要又不想要 ?x 和 ?y 的显式实例化。我真的很感激一些概念上的解释，为什么 move/eqP 的行为不像我认为的那样，以及 eqP 和 (introT eqP) 的类型实际上发生了什么。

如果相关，我正在导入

来自 ssreflect。

谢谢你。

当我的证明状态是这种形式时， H -> goal 我经常使用 intros H. *some tactic* H. 一些策略可能是“反转”或“应用 _ in”等的模式。如果有一些策略将这两个步骤结合起来会很好，即引入最高假设，然后对其应用特定的策略。我在 ssreflect 文档中查看了 move，因为 move 可以做类似的有用的事情，但没有找到任何东西。有这样的战术吗？

谢谢。

我很困惑为什么 assert 和 cut 在这种情况下表现不同。我试图用 ssreflect seq 库来证明这个引理。

以上工作正常。然而，

产生错误 Error: Not a proposition or a type.

为什么会这样？我认为 assert 和 cut 都会将任意目标作为参数，但显然情况并非如此。这两种策略在其工作目标方面有何不同？

谢谢你。

我正在尝试从涉及字符串的自定义类型中创建一个 ssreflect OrdType 。我假设 ssreflect 中有一些内置的字符串顺序类型，但我在任何地方都找不到。我在 Coq 的标准库中看到了一个，但我不知道定义是否转移到了 ssreflect 库。我宁愿使用 ssreflect 而不是 Coq 标准库。有人可以指点我在哪里看吗？谢谢。

我已经在 Coq 中编写了一些项目，但我之前没有使用过 ssreflect 并且我遇到了麻烦。

我有一个带有索引的数据结构。下面是简化版。

我选择使用序数而不是 nat，因为否则我必须有一个单独的字段来证明它们在范围内，否则我必须在其他属性的声明中考虑这种情况。但是序数使我的一切都变得非常困难。

花了一天左右的时间，我才发现我可以用它们来构建它们，inord而不是制作无数的x < n引理。

有了引理，我至少能够达到我的问题是我无法证明这一点的地步forall i : 1 < 2, Ordinal i = Ordinal lt_1_2。

inord展开后，我无法找到进一步评估的方法tnth。我也没有找到任何有用的引理。

我是否将序数用于错误的目的？如果没有，我应该如何使用它们？

最小化的例子

没有 MRE，因为这是关于我应该做的事情。在下面的（最小化）尝试之前，我尝试了各种方法，序数似乎是一个很好的解决方案。

我不知道如何从这里继续。我认为我应该能够充分评估 tnth，但我不能。

我被这个非常简单的引理所困扰，想知道最好的方法是什么。

我使用 nix 版本 2.3.7 在 MacOS High Sierra 上运行带有 Proof General 的 mathcomp 8.12。为此，我使用以下 shell 命令：

在带有 MacOS Catalina 的新 Mac 上，我使用 https://dev.to/louy2/installing-nix-on-macos-catalina-2acb 中提供的（我希望）正确建议安装了 nix 版本 2.3.10。运行与以前相同的 nix-shell 命令，我设法让 Proof General 运行。但是下面的 Coq/SSReflect 代码在第 3 行失败了。

带有一条消息说明

另一个奇怪的行为是，如果我删除违规Require并继续，那么在环境中找不到 addnBAC 引理（但是，还有其他引理，例如 subnDA！）。

关于这里可能有什么问题的任何建议？我尝试通过更改 -p 选项进入 8.13，但得到了相同的结果。

在 Ilya Sergey 的Programs and Proofs中，引入了ssrnat's 命令.+1并用于定义自然数上的一些函数。虽然它的用法在那里得到了很好的解释，但我也对它是如何定义的，更重要的是它是如何工作的很感兴趣。在那一章的前面介绍了nat类型，我们可以用 " " 来验证定义Print nat.，它产生：

然而，.+1命令“ Print .+1.”或“ Print +1.”产生：

甚至试图通过在其前面添加一个自然数来规避这一点，例如在 " Definition one: nat := 1." 后跟 " Print one.+1." 产生：

但是，我想这个命令是在库中定义的，而不是语言的原语，所以感觉应该能够像其他任何人一样检查它的定义。

如果是这种情况，为什么命令不起作用以及如何.+1打印定义？

注意：如果不可能，解释为什么也可以作为答案（以及命令的代码/工作的资源）。

我想在运行 Catalina 的 Mac 上升级 Emacs（目前是 26.1，来自 emacsformacosx.com，直接从 High Sierra 导入，使用 PG 4.5-git），并发现 Apple 通过引入这个版本的 Mac OS 使 Emacs 变得困难“检查恶意软件”，似乎很难绕过。

我恢复到我以前的 Emacs 版本，但是，从那时起，.+1SSReflect 的符号nat在 PG 的 Coq 目标缓冲区中没有正确显示（不过，我自己的符号得到了适当的管理）。succn它改为显示为标准构造函数。

有谁知道问题可能是什么（FWIW，我正在使用 CoQ 的 NixOS 版本）？

我正在尝试使用 CoQ/SSReflect 证明nat来证明rat. 中的当前证明状态Open Scope ring_scope是

并且，使用Set Printing All，它显示为

我一直在尝试使用各种rewrite，例如ler_nat, PoszM, intrM，但收效甚微。谁能给我一些关于如何进行的提示？

PS：我无法提供一个最小的工作示例，因为我并没有完全掌握我在这里所做的事情；）