问题标签 [ssreflect]

基本上，我想在某些情况下观察伪多项式除法的结果（比如 3 x^2+2 x +1 和 2 x +1）。多项式之间的伪除法在 Ssreflect 1.4 的 polydiv.v 中的 edivp 中实现。我希望代码应该如下所示：

但是，由于类型统一失败，代码停留在定义 p 上。任何帮助是极大的赞赏。

以下代码来自perm.vSsreflect Coq 库。我想知道这个结果是什么。

在 ssreflect 的所有 coq 代码中都有这个语句

是什么GroupScope？如果它是另一个文件，我可以从哪里下载它？

我试图:从非 ssreflect Coq 的角度理解 Coq/ssreflect 证明中（冒号）的确切含义。

我读到它与将事物移向目标有关（例如泛化？？），并且与=>将事物移向假设相反。但是，我经常觉得它令人困惑，因为无论有没有:. 以下是教程中的示例：

在哪里，

是一个引理，如果一棵树的镜子是一片叶子，那么这棵树就是一片叶子。

我不明白为什么我们需要:here 而不仅仅是做 Coq apply。事实上，如果我删除:，它工作得很好。为什么会有所作为？

我正在阅读 ssreflect 教程，内容如下：

下面，我们通过将命题陈述翻译成它的布尔对应物来证明……，这很容易用蛮力证明。这种证明技术称为反射。Ssreflect 的设计允许并且 ssreflect 的精神建议广泛使用这种技术。

这（反射）是否意味着 ssreflect 假定排中（forall A:Prop, A \/ ~A）？

看起来确实如此，因为所有布尔值都满足 EM 如果是这样，那么对于遵循 ssreflect 样式来说，这将是一个很大的假设。

另外，我不太了解它下面的“本地”或“小规模”部分：

由于它通常在本地用于有效地处理小部分证明（而不是在整体证明结构中使用），因此这称为小规模反射，因此称为 ssreflect。

小部分与整体证明结构是什么意思。这是否意味着我们有时可以在本地假设 EM 而不会造成任何伤害，并且通常不使用 EM，或者这里的 local 是否意味着其他东西？

另外，我在 Coq 方面经验不足，不太明白这种“蛮力”风格在“布尔对应物”（主要基于case我目前所读到的分析）如何比普通的 Coq 方式更有效。对我来说，蛮力不是很直观，也不容易事先猜到，直到你看到结果。

有什么具体的例子来说明这里的效率吗？

我试图了解组合的 ssreflect 策略应该如何“分解”（或者它们首先是如何组合的）。我遇到的问题之一是了解战术的顺序和关联性。

有时，我觉得顺序是从右到左。例如

似乎相当于

忽略 no-op move，就好像我们AiB在按顺序应用函数一样，apply : AiB.可以看作 apply (: AiB).. 也就是说，我们首先将 AiB 移动到目标中，然后apply在其中调用目标AiB。

但是，我在其他场合感到困惑：

根据教程，这个对 进行案例分析(EM (P y))，然后//尝试解决琐碎的子目标。然后？？move =>将其余的引入上下文？这里的操作顺序是什么？

让，是EM_吗？我读对了吗，战术应用的“正确顺序”是什么？(EM (P y))(move=> notPy (// ( case (:EM_) ) ) )

顺序有点扭曲，一般来说notPy不一致。有没有办法在合法的 ssreflect 中从右到左写上面的内容？

我正在阅读和玩 ssreflect 教程，遇到了使用 {} 引用的东西，我不太明白：

谁能解释一下{HPa}做什么HPa？

顺便说一句，上下文是要引入“观点”？？？。我尝试删除{}，它仍然有效，但会产生不同的东西。而且我不知道在哪里可以找到诸如括号之类的文档@。

在我看来，ssreflect当我们进行依赖模式匹配时，隐式构造函数字段会变成显式字段，并且设置各种隐式选项不会影响这种行为。

以下代码适用于 Coq 8.6：

当我 import 时它停止工作ssreflect，因为它需要一个额外的字段用于cons模式append：

这是什么原因，有没有办法在模式匹配中仍然隐含？

我在 Coq 中使用 MathComp 库进行反射时遇到了一些非常简单的证明问题。

假设我想证明这个引理：

对于如此简单的任务，这种方法对我来说似乎有点“非正统”。有没有更好/更简单的方法来做到这一点？

我正在使用数学组件库，并试图证明这一点：

最后一次重写失败并显示错误消息：

错误：重写时的依赖类型错误(fun _pattern_value_ : nat => is_true (#|S| <= _pattern_value_)

关于重写失败的原因或此错误消息的解释的任何想法？