问题标签 [coq-tactic]

我是 Coq 的新手。我对以下证明感到困惑：

结果显示：

使用 H0 和 H 的推论很明显，但我不知道如何使用 H0 来完成证明。非常感谢您的帮助！

定义一个新类型foo给了我一个递归原则foo_rect，它优雅地抽象了过来fix。cofix是否可以通过某种方式“翻转箭头”来定义同义等价物（抽象）？

输出：

我不确定这意味着什么 - 两者map都是interleave直接的核心递归函数，用于构建共归纳类型的值。有什么问题？

我目前正在使用 Coq 中的红黑树，并希望为列表配备一个订单，以便可以使用该模块nat将它们存储在红黑树中。MSetRBT

出于这个原因，我定义seq_lt如下：

到目前为止，我已经成功展示了：

也

但是，我正在努力证明以下内容：

我什至不确定最后一个引理是否可以使用归纳法，但我已经研究了几个小时，不知道从这一点开始。定义有seq_lt问题吗？

我想出了以下玩具证明脚本：

为什么我需要在myValue这里手动展开？提示还不够吗？

我正在研究一种可以创造两个新假设的策略

从那种形式的假设

这是我的 Ltac 代码：

wereh是要分解的假设，x新变量t的名称和新假设的名称。该策略按预期工作，但在证明结束时我得到了这个：

该evar策略似乎创建了一种名为 D 的新类型，而不是使用现有的类型。请注意，如果我使用

在 coqtop 中，它可以完美运行。

我试图证明 和 的等价性P \/ Q，~ P -> Q在排除中间的假设下，

其中Excluded Middle如下。

实际上，一个方向的证明不需要排中。在我试图证明另一个方向的过程中，当我试图在假设中利用排除中间时，我陷入了困境，

当前环境如下：

我知道在这种情况下，我们接下来要做的就是做一些类似P的“案例分析”，包括策略的使用left，right如果我的证明到目前为止还有意义的话。

提前感谢您的任何建议和建议！

该f_equal策略对于涉及归纳构造函数的等式证明无条件有用。a :: s = a' :: s将是这样一个目标，减少到a = a'.

将它与任意函数一起使用是另一回事。4 mod 2 = 2 mod 2会减少到4 = 2，这显然是荒谬的。

我想知道是否有一种方法可以仅在不丢失信息的情况下自动应用f_equal（或类似） ，例如归纳构造函数。

我不得不承认我不是很擅长共同归纳。我试图展示关于自然数的互模拟原理，但我被困在一对（对称）案例上。

当关注第一个被承认的案例时，上下文是这样的：

想法？

在 Ltac 中实施复​​杂的策略时，有一些 Ltac 命令或策略调用我预计会失败以及预期会失败（例如终止 arepeat或导致回溯）。这些故障通常在故障级别 0 时提出。

在更高级别引发的故障“逃离”周围try或repeat阻塞，并且对于发出意外故障的信号很有用。

我缺少的是一种运行策略tac并处理其失败的方法，即使在 0 级，也可以处于更高的级别，同时保留失败的信息。这将让我确保repeat不会因为我这边的 Ltac 编程错误而终止。

我可以在 Ltac 中实施这种失败提升级别的高阶策略吗？