问题标签 [ssreflect]

有这个引理

我怎样才能转换n %% 4 * 5 - n %% 4 * 4为n %% 4？然后将是小菜一碟。

我不能将 Ssreflect 的重写与 setoid 一起使用。虽然我认为这些信息与解决问题无关，但我在 coq 中使用了这种类别理论的表述：https ://github.com/jwiegley/category-theory 。

据我所知，如果RewriteRelation可以解析出合适的Typeclass实例，Ssreflect的重写可以使用用户定义的等价关系。

使用默认的重写策略代替工作（即使没有手动声明实例，因为类似的东西已经在库中声明）。

什么好笑的：

这工作正常。

为什么 SSReflect 不使用我手动声明为通过用户定义的等效重写的 RewriteRelation 实例？提前致谢。

编辑： 我已经弄清楚为什么 Ssreflect 看不到我的关系。显然，您可以添加要与 Ssreflect 的重写一起使用的关系，仅Add Parametric Relation在手册中记录，并且RewriteRelation实例不会更改任何内容。我试图使用公理创建一个假关系并将其添加Add Parametric Relation并rewriting正常工作。但现在我又遇到了麻烦。我希望能够使用的关系具有类型crelation (x ~> y)（即(x ~> y) -> (x ~> y) -> Type），但要使用Add Parametric Relation我需要一个具有类型的术语relation (x ~> y)（即(x ~> y) -> (x ~> y) -> Prop。为什么在标准库中定义了两种不同类型的关系（relation和crelation）？我怎么能将 a 转换crelation为 arelation没有得到宇宙不一致错误？而且我仍然不明白为什么上面的例子False有效。

我想计算巨大（特定）矩阵的乘积。从复杂性的角度来看，产品应该采用元素表达式的形式。

我试图用mxvec/对矩阵进行“矢量化”，vec_mx并通过一维流计算乘积。但是索引访问被enum ('I_p * 'I_q).

我想知道第 n 个值，enum ('I_p * 'I_q)因为我想以基础字段中的原始表达式的形式描述矩阵的乘法。

我该怎么做呢？特别是，我如何证明这个陈述？

如果我做类似的事情 -From mathcomp Require Import ssreflect.它会给我以下错误。

但如果我这样做 -Require Import ssreflect.它编译得很好。这可能是因为我安装了 ssreflect 但不完全是我想要的方式。

但问题是我想要第一种工作方式，因为我有很多这样编写的程序，而且每一个都改变行似乎不合逻辑。

这就是我的 .emacs 文件中的内容 - （我想也许我需要添加任何东西，比如 mathcomp/ssreflect 的路径。我不知道）

如果有人可以帮助我开始From mathcomp Require Import ssreflect.工作，那对我真的很有帮助。

Coq 有一些方便的策略来自动证明算术引理，例如lia：

但是，该策略不直接支持 SSReflect 样式的布尔反射语句：

可以通过使用视图转换为非 SSR 格式来解决它们：

然而，这是非常手动的。是否有某种技术/方法/策略可以自动将引理应用lia到 SSR 样式语句中？

假设下溢得到妥善管理，在序数上重写的最佳方法是\sum_(i...) (F i - G i)什么？(\sum_(i...) F i - \sum_(i...) G i)bigop

更准确地说，关于这些下溢，我对以下引理感兴趣：

Lemma big_split_subn (n : nat) (P : 'I_n -> bool) (F G : 'I_n -> nat) : (forall i : 'I_n, P i -> G i <= F i) -> \sum_(i < n | P i) (F i - G i) = \sum_(i < n | P i) F i - \sum_(i < n | P i) G i.

似乎big_split应该适用于加法（或 Z 中的减法，big_distrl与 -1 一起使用），但我需要将它用于（有界）自然的减法。

提前感谢您的任何建议。

再见，

皮埃尔

我陷入了这样的目标平等（我认为细节并不重要）：

我如何摆脱tcastandtuple回到简单seq（我尝试了这个val_inj技巧，但这似乎并没有删除类型转换）？

提前致谢。

再见，

皮埃尔

我想删除tcast一个“引理”，例如下面的一个。但这甚至不进行类型检查，因为依赖类型的“约束”。

事实上，我想到的应用程序的一个更重要的例子，它会进行类型检查，将是以下引理：

这很简单seq，但在这里我找不到如何在 tuple.v 或 fintype.v 中继续使用引理。

那么，tcast当这些表达似乎不适合通过val_inj案例分析处理时，解决这些表达的正确方法是什么（见上一篇文章）？在第一个例子中，我是否有引入两个版本的f, 后来证明在序列上是相等的（如果是，那么最好的方法是什么）？

提前感谢您的任何建议。

皮埃尔

我找不到标准库 == 函数，它被重载并返回布尔值（或 sumbool，或我可以计算的东西）。我希望能够做到

和

无需指定参数的类型。如果 Coq 没有平等类型的这个功能，我会感到惊讶。有人可以告诉我在哪里可以找到它吗？我觉得它与 ssreflect 有关，但我无法弄清楚。

谢谢。

例如，coq 在其标准库中有一个 Classical 包，其中包含经典逻辑中的引理，例如与 forall 相关且存在的引理（https://coq.inria.fr/library/Coq.Logic.Classical_Pred_Type.html）。

我的问题是 mathcomp 或 ssreflect 本身是否有类似的支持。到目前为止，我发现的只是https://github.com/coq/stdlib2/blob/master/src/bool.v#L548中的一些定义和引理

谢谢