问题标签 [ssreflect]

问问题

For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.

71 问题
Newest
Active
Bountied
318
Unanswered
0 投票
1 回答
166 浏览

coq - 从 ssreflect finset 中提取/使用成员资格证明

编辑：我通过引入一个结构，通过将所述元素的成员资格证明携带到一个集合来增加一个元素，从而使这个例子变得更加简单：

但是，我需要将此转换应用于任何给定的集合，而且我似乎也无法做到：

由于equip_set_with_Helin 允许我编写 uniq_cons 函数，因此将不胜感激有关此问题或原始问题的任何帮助。谢谢！

我有一个类型 dbranch，由有限类型 ft 上的序列和该序列的 uniq 证明组成。我希望能够，给定 ft 类型的元素 t 和 dbranch 上的 finset 以返回相同的集合，其中所有 dbranches 都已与 t 进行“cons-ed”。

我需要为分支编写一个 cons 函数，该函数将假设给定元素还不是分支的一部分作为参数。我不知道如何把它写成一个普通的函数，所以我把它当作一个证明。

然后我编写了 uniq_cons，它试图将 dcons 提升到一组 dbranches。然而，它的论点 H 的应用需要证明 b \in t （这是我代码中的占位符）。

b 在 t 中的事实应该是显而易见的，因为它直接出现在综合符号中。但是，我无法在 finset.va 中找到“提取”或使用该信息的方法，并且 Coq 无法自行完成。预先感谢您的帮助。

0 投票
1 回答
89 浏览

coq - 在 ssreflect finset 理解中使用条件

我有一个函数 f，它接受 fintype A 的 ax 和 P x 的证明来返回 fintype B 的元素。我想为所有满足 P 的 x 返回 fx 的 finset，可以这样写：

然而，这失败了，因为 Coq 没有用右边的信息填充占位符，而且我不知道如何明确地提供它。

在 ssreflect 代码和书中，我都没有找到有关如何执行此操作的指示。我意识到我可能可以通过使用 sigma-type {x : A ; P x} 并修改了一点 f，但感觉比它应该的更复杂。有没有一种简单/可读的方法来做到这一点？

0 投票
1 回答
83 浏览

coq - `0 1的更简单证明

我想知道该陈述的更短或更简单的证明forall a:nat, 0 < a -> 1 < a + 1。在 mathcomp/ssreflect 中。

我有以下证明，但希望存在更优雅的证明。

From mathcomp Require Import all_ssreflect.
Goal fora

我想知道该陈述的更短或更简单的证明forall a:nat, 0 < a -> 1 < a + 1。在 mathcomp/ssreflect 中。

我有以下证明，但希望存在更优雅的证明。

这个如何：

0 投票
1 回答
144 浏览

coq - 用户定义的枚举类型应该如何变成`finType`？

我想在 Coq/SSReflect 中创建一个归纳定义的枚举类型，例如

finType因为它显然是一个有限类型。我有三个解决方案可以做到这一点，但所有的解决方案都超出了我的预期，而且永远不会令人满意。

在第一个解决方案中，我为、 和eqType实现choiceType了mixin 。countTypefinType

它运作良好，但我想要一个更简单的解决方案。

第二种解决方案是只使用序数类型

但它需要在进一步的证明中进行相关案例分析（或者，需要定义一些我不想做的引理）。

作为第三种可能的解决方案，adhoc_seq_sub_finType可以使用。

但是，它定义了与原始归纳类型不同的类型E，这意味着我们总是需要在进一步的证明中将它们相互转换。此外，它需要我们实现eqType（这也很明显，可以默认没有任何实现）。

由于我想定义许多枚举类型，因此为每种类型都提供如此复杂的定义并不好。我期望的一个解决方案是在枚举类型的相应归纳定义中几乎完全给出了这样eqType的解决方案。finType

有什么好主意可以解决这个问题吗？

0 投票
2 回答
254 浏览

coq - Coq/SSReflect: How to do case analysis when reflecting && and /\

I have the following reflect predicate:

And I am trying to relate the boolean conjunction to the logical one and the following one-line proof goes through:

However, I don't understand how the last ; by case. is applied. When we examine the proof without the last ; by case.:

We get 6 subgoals (2 are trivially true):

I'm not sure how to proceed from here because they all are false - how can we prove that? I tried doing . case. individually but that doesn't work. How does ; by case admit these subgoals all at once?

Thank you.

0 投票
1 回答
27 浏览

coq - Simplifying expression with lists equality

My task is to implement an instance of equality type for the seq datatype. To do this I need to create a comparison function and a proof that this function is correct:

Result:

How to get rid of x' in both sides of equality: (x' :: xs = x' :: ys)?

I tried case: (x' :: xs = x' :: ys), but it didn't help.

0 投票
2 回答
49 浏览

coq - 用过滤器证明大小不等于 (size + 1)

有这个定理：

我得到了这个状态：

我怎样才能证明那size [seq x <- xs | a x]总是更少(size xs).+1)呢？所以，他们的平等总是错误的。

0 投票
1 回答
80 浏览

coq - 用 mathcomp 实例化一个 Zn 的交换环

我能够创建一个ComRingMixin，但是当我尝试将此类型声明为规范环时，Coq 抱怨：

x : phantom (GRing.Zmodule.class_of ?bT) (GRing.Zmodule.class ?bT) 术语“x”的类型为“phantom (GRing.Zmodule.class_of ?bT) (GRing.Zmodule.class ?bT)”，而预计其类型为“phantom (GRing.Zmodule.class_of 'I_n) ?b”。

这就是我到目前为止所拥有的，我能够定义操作并实例化 abelian 组 mixin 以及规范声明，但是对于环，我的代码失败了。

我究竟做错了什么？我以http://www-sop.inria.fr/teams/marelle/advanced-coq-17/lesson5.html为基础。

0 投票
2 回答
128 浏览

coq - 我们如何为依赖类型定义`eqType`？

我想将依赖类型定义为eqType. 例如，假设我们定义了以下依赖类型Tn：

为了做到这一点，我为eqType定义了一个相等函数：Tn_eqTn

然后我试图证明相等公理，Tn_eq但它失败了。

我在这里有一个错误：

我应该如何证明这个引理？

0 投票
1 回答
95 浏览

coq - 用 SSReflect 证明 OR 是可交换的

我正在尝试研究一些基础逻辑的东西，主要来自《使用 Z：规范、改进、证明》一书，但也试图了解更多关于 Coq 的信息。上面提到的《使用 Z》一书中的第一个证明之一是逻辑或是可交换的， P \/ Q => Q \/ P. 这本书使用自然演绎树表示法，所以假设 P，然后引入 Q 或 P，或者假设 Q，然后引入 Q 或 P，我已经将它翻译成 Coq，无论你如何称呼标准库，如下所示：

你在这里看到类似的东西。无论如何，试图把它翻译成 SSReflect，我有点卡住了：

我查看了我找到的 SSReflect 参考资料，没有看到任何明显看起来像是在尝试替换leftand的内容right。在 SSReflect 中编码这个证明的正确方法是什么？

编辑：我现在使用 SSreflect 有以下证明：

感觉这个比较啰嗦。有没有更好的方法来用 SSreflect 做到这一点？


12345678910