问题标签 [coq]

我正在尝试使用 Function 使用度量来定义递归定义，但出现错误：

我在底部发布了整个源代码，但我的功能是

我知道问题出在 foralls 上：如果我用 True 替换它们，它就可以工作。我也知道如果我的右手边使用含义（->），我会得到同样的错误。Fixpoint 适用于 foralls，但不允许我定义度量。

有什么建议吗？

正如所承诺的，我的完整代码是：

我正在使用 Coq Proof Assistant 来实现（小型）编程语言的模型（扩展了 Bruno De Fraine、Erik Ernst、Mario Südholt 的 Featherweight Java 的实现）。使用该策略时不断出现的一件事induction是如何保留包装在类型构造函数中的信息。

我有一个子类型 Prop 实现为

extendsJava 中的类扩展机制在哪里，typ代表了两种不同的可用类型，

我希望保留类型信息的一个例子是在induction对一个假设使用该策略时，例如

例如在

using丢弃有关和的induction H.所有信息。案件变成uvst_refl

如您所见，与 中的构造函数相关的信息u以及与中的构造函数相关的信息都丢失了。更糟糕的是，由于这个 Coq 无法看到这一点，并且在这种情况下实际上必须是相同的。vtypHtuv

当inversion在 Coq 上使用该策略时，H成功地看到了这一点u并且v是相同的。然而，这种策略在这里并不适用，因为我需要induction生成的归纳假设来证明st_trans和st_extends案例。

有没有一种策略可以结合最好的inversion和induction生成归纳假设并推导等式，而不会破坏有关构造函数中包含的内容的信息？或者，有没有办法手动获取我需要的信息？info inversion H并且info induction H两者都表明许多转换是自动应用的（尤其是使用inversion）。这些使我在构建的同时尝试了该change策略let ... in，但没有任何进展。

我无法理解构造函数的原理及其工作原理。

例如，在 Coq 中，我们被教导这样定义自然数：

并且被告知这S是一个构造函数，但这究竟是什么意思？

如果我这样做：

我知道它是4和类型nat。

这是如何工作的，Coq 是如何知道它(S (S (S (S O))))代表的4？

我想这个问题的答案是 Coq 中一些非常聪明的背景魔法。

我有一组作为参数：

现在我想定义另一个参数，它是 Q 的一个子集。比如：

我该如何定义？我想我可以稍后将限制添加为公理，但直接用 F 的类型表示它似乎更自然。

我看到了一个非常奇怪的语法：(name:type1) type2 in type 和 [name:type] expr 在表达式中，看起来像是 Pi 和 Lambda 的替代语法，但经过几个小时的搜索，我在文档中没有找到任何东西，一切都是徒劳。

它是什么意思，在哪里定义？（对不起，我失去了示例用法的链接）

我在 Coq 中玩耍，试图创建一个排序列表。我只想要一个接受列表[1,2,3,2,4]并返回类似内容的函数Sorted [1,2,3,4]- 即取出坏部分，但实际上并未对整个列表进行排序。

我想我会先定义一个lesseqtype的函数(m n : nat) -> option (m <= n)，然后我可以很容易地对其进行模式匹配。也许这是个坏主意。

我现在遇到的问题的症结在于（片段，底部的整个功能）

不是类型检查；它说它期待一个option (m <= n)，但它Some (le_n 0)有 type option (0 <= 0)。我不明白，因为在这种情况下显然两者m和n都是零，但我不知道如何告诉 Coq。

整个功能是：

也许我正在超越自己，只需要在解决这个问题之前继续阅读。

我无法理解为什么我的 Coq 代码没有按照下面代码中的预期执行。

• 我试图使示例尽可能简化，但是当我使它变得更简单时，问题就不再出现了。
• 它使用 CompCert 1.8 文件。
• 这在 Coq 8.2-pl2 下发生在我身上。

这是代码：

这不起作用：

失败rewrite H1：

这虽然有效：

此外，就在 之后eauto，我的目标如下所示：

因此，rewrite H1; discriminate两次有效，但在eauto使用分号后“管道”它不起作用。

我希望这个问题至少有意义。谢谢！

完整代码：

我需要定义一个没有容易测量的参数的递归函数。我保留了一个已使用参数的列表，以确保每个参数最多使用一次，并且输入空间是有限的。

使用措施(inpspacesize - (length l))最有效，但我陷入了一种情况。看来我错过了前几层l已正确构建的信息，即没有重复，所有条目都来自输入空间。

现在我正在寻找一个可以满足我需要的列表替换。

编辑我现在将其简化为以下内容：

我的nats 小于给定的max，需要确保每个数字最多调用一次该函数。我想出了以下几点：

当我试图以归纳方式证明我无法将元素插入完整列表时（IH 无法使用或我找不到我需要的信息）时，我一直卡住。由于我认为这种不可插入性对于显示终止至关重要，因此我仍然没有找到可行的解决方案。

关于如何以不同方式证明这一点或重组上述内容的任何建议？

我试图在列表中搜索一个对象，然后如果找到它可能返回 true；否则为假。

但是，我试图想出的是不正确的。我真的很感激一些指导。我需要该函数通过将列表的头部与相关元素进行比较来搜索元素列表，如果不匹配，则递归地将列表的其余部分通过函数并重复，通过匹配列表的头部。

非常感谢您的指导和帮助。

先感谢您

这应该是一个简单的问题。我是 Coq 的新手。

我想在 Coq 中定义独占或（据我所知，这不是预定义的）。重要的部分是允许多个命题（例如 Xor ABCD）。

我还需要两个属性：

我目前无法为未定义数量的变量定义函数。我试图为两个、三个、四个和五个变量手动定义它（这就是我需要的数量）。但是随后证明这些属性是一件痛苦的事情，而且似乎效率很低。