问题标签 [coq]

我发现 Coq 在隐式参数方面存在某种不一致的行为。

该Let定义id1似乎没有t隐含，而当您替换时Let不会Definition发生错误。我有什么问题还是这是一个错误？

这是一个更大的证明的简化片段，它捕获了有问题的行为。

当您替换rewrite prop2为rewrite propcoq 时，会出现神秘错误。然而，在我看来，coq 应该forall e : t, True在重写步骤之后屈服。谁能帮我这个？

编辑：我可能应该说我目前是如何解决这个问题的。我定义了一个显示排列相等的原则，

然后在证明上下文中应用引理，这在下面给我带来了麻烦，并表明 eta 等价项是相等的。因此，当术语嵌套在记录中时，问题似乎显示出 eta 等价性。但我不擅长处理记录，所以我可能会遗漏一些东西。

原来的：

我无法证明嵌套在记录字段中的 eta 等效项的相等性。作为参考，eta-reduction 可以通过自反性独立证明：

在我当前的证明上下文中，我有两条记录，我必须证明它们的相等性。完全破坏和展开，证明上下文和当前子目标如下所示：

必须建立的平等是

因为这些等式可以通过反身性来建立，所以我不确定问题出在哪里。但是，我怀疑有些地方出了问题，因为尝试替换λ x : U, perm0 x为会perm0生成适当的子目标，但不会替换记录中的术语。此外，使用 eqa_reduction 重写会导致有关抽象的错误，从而导致错误类型的术语或嵌套的依赖参数。

我已经尽可能地简化了上下文并将其粘贴在下面。除了风格问题和我仍然是初学者的事实之外，我认为当前的开发没有任何问题。

最后，我要感谢大家在 Coq 方面帮助我并耐心等待。

我是 Coq 的新手，有一个关于破坏策略的快速问题。假设我有一个count函数可以计算给定自然数在自然数列表中出现的次数：

我想证明以下定理：

如果我要证明 n = 0 的类似定理，我可以简单地将 y 破坏为 0 或 S y'。对于一般情况，我想做的是 destruct (beq_nat ny) 为真或假，但我似乎无法让它工作——我错过了一些 Coq 语法。

有任何想法吗？

我在定义在证明上下文中递归反转假设的策略时遇到了麻烦。例如，假设我有一个包含如下假设的证明上下文：

并希望反复反转假设以获得包含假设的证明上下文

当然，通过重复应用反转策略很容易获得这个证明上下文。然而，有时倒置一个假设会将不同的假设放入不同的子目标中，而是否对每个子目标进行倒置取决于倒置提供的信息的性质。

明显的问题是，不加选择地对证明上下文进行模式匹配会导致不终止。例如，如果希望在反转原始假设后保留原始假设，则以下内容将不起作用：

是否有捷径可寻？显而易见的解决方案是保留一堆已经倒置的假设。另一种解决方案是仅将假设反转到特定深度，这将删除 Ltac 中的递归调用。

背景：我正在做软件基础的练习。

在最后一行之前，我的子目标是：

我想把它变成这样：

但是，当我尝试单步执行rewrite -> neg_move时，会产生此错误：

错误：无法找到变量 y 的实例。

我敢肯定这真的很简单，但我做错了什么？（请不要为解决问题而放弃任何东西evenb_n__oddb_Sn，除非我做错了）。

作为一个粗略且未经指导的背景，在HoTT中，人们从归纳定义的类型中推断出到底是什么

这允许非常一般的构造

这Lemma transport 将是HoTT“替换”或“重写”策略的核心；据我所知，诀窍是，假设一个你或我可以抽象地识别为的目标

弄清楚什么是必要的依赖类型 G，这样我们就可以apply (transport G H). 到目前为止，我所知道的只是

不够笼统。也就是说，第一个idtac经常被使用。

问题是

[有没有| 什么是]正确的事？

减少这种类型有什么技巧吗？我那里有一个多余x的。

Monad 是一个类型类：(Set -> Set) -> Type

我有一个问题： Record和Definition

我有这个定义：

我为它写了一个布尔函数。

在哪里beq_term : term -> term -> bool.

所以我对beq_rule实际返回的确切类型的定义beq_term不是我想要的。我希望它为我返回一个类型： rule -> rule -> bool.

所以我改变了规则的定义Record：

和

我的问题是：

1）我第一个定义的ruleusedDefinition和另一个 used有什么不同Record？

2）如果我想定义规则，Definition我可以在定义中给出别名lhs和rhs喜欢Record吗？