问题标签 [coq-tactic]

我正在做一个证明，在那里我生成了两个案例

（eq_id_dec本质上类似于eq_nat_dec）。

e: Y = X这给出了两种情况，分别增加了平等和不平等的假设n: Y <> X。

在第一种情况下，我可以轻松使用rewrite eor rewrite <- e。

但是我怎样才能有效地利用第二种情况下的不等式呢？例如，考虑一个目标，例如

?

我尝试unfold eq_id_dec了一些rewriteS 但卡住了。

我对PropCoq 中的证据等感到困惑。我们如何证明这一点(n = n) = (m = m)？

我的意图是表明这是某种方式True=True。但这甚至是正确的表述？

到目前为止我尝试的是：

但simpl.什么都不做，reflexivity也不做。X这只是一个例子，一般来说，如果可能的话，我需要为任何类型证明这一点。

在目标是存在的证明中，我有以下内容，并且目标属性是假设之一。

我知道我可以exists y. apply H.证明当前的目标，但我想知道是否有更智能的策略可以直接使用假设来证明这里的存在目标，比如eapply H？

由于这是一个统一，因此不必将X部分写入exists X..

如果不存在这样的策略，我该如何编写？

我在证明期间有以下内容，我需要替换为normal_form step t，value t因为有一个已证明的定理是等价的。

等价定理是：

现在，我可以使用这个定理来重写normal_form假设中的出现，但不能重写目标中的出现。那是

根据假设工作，但rewrite nf_same_as_value.在目标上给出：

这里的rewrite目标在理论上是不可能的，还是一个实施问题？

- 编辑 -

我在这里的困惑是，如果我们定义normal_form step = value，重写就会起作用。如果我们定义forall t, normal_form step t <-> value t，则rewrite作品 ifnormal_form step没有在存在论中被引用，但如果它在存在论中则不起作用。

改编@Matt 的例子，

令我困惑的是为什么最后一步必须失败。

这种失败与功能扩展性有关吗？

错误消息特别令人困惑：

只有一个子项匹配R1 _ _，即 R1 x x。

此外，根据@larsr，如果eexists使用重写工作

这里eexists添加了什么？

我过去常常用info_auto一种策略来显示在幕后实际执行的步骤auto。然而，这似乎不再适用于 Coq 8.5 (beta3)。

以下示例用于 Coq 8.4：

并给我必要的步骤，例如apply @eq_refl.。

使用 Coq8.5，我收到警告：

按照提示使用Info 1 auto.，我得到：

在消息视图中。在其他情况下，我有时会得到类似的东西

但两者都没有帮助/信息，因为我无法应用这些来手动完成证明。

info_auto在 Coq 8.5中复制旧功能的正确方法是什么？

What I am looking for is an auto-like tactic that can prove simple equalities like:

So far, what I've tried manually is to use ring_simplify and field_simplify to prove equalities. Even this doesn't work out well (Coq 8.5b3). The example below works:

But it was necessary to use field_simplfy twice before reflexivity. The first field_simplfiy gives me:

which is not subject to reflexivity.

The example below does not work, field_simplify seems to do nothing on the goal, and therefore, reflexivity can't be used.

Again, is there an automatic way to achieve this, like an field_auto?

是否可以切换当前目标或子目标以在 Coq 中进行证明？

例如，我有一个这样的目标（来自 eexists）：

我要做的是首先split证明正确的合取。我认为这将给出存在变量的值?s，而左连词应该只是一个简化。

但split默认情况下，将左合取设置?s > 0为当前目标。

我知道我可以2:在第二个子目标上添加战术前缀，但这很尴尬，因为

1) 我看不到目标#2 的假设和

2) 如果它在不同的上下文中，goal#2 可能是第三个或第 k_th 个目标。证明不会是便携式的。

这就是为什么我想将第二个目标设置为当前目标。

顺便说一句，我正在使用 CoqIDE (8.5)。

我知道这一点，ring并且field可以用于某些等式，例如a + x = b + y. 我想知道是否有它的存在版本可以确定存在变量的值？

例如，我有以下内容：

我可以弄清楚这?s = r2 * r2 - r1 * r1可以解决这个问题。但是有没有这样的策略ering可以让 Coq 进行计算而不是我手动进行呢？

完成 CIS 500 软件基础课程CIS 500 软件基础课程。目前在MoreCoq上。我不明白这rewrite IHl1部分。它是如何工作的？为什么这在以前使用时不起作用simpl？

我试图了解组合的 ssreflect 策略应该如何“分解”（或者它们首先是如何组合的）。我遇到的问题之一是了解战术的顺序和关联性。

有时，我觉得顺序是从右到左。例如

似乎相当于

忽略 no-op move，就好像我们AiB在按顺序应用函数一样，apply : AiB.可以看作 apply (: AiB).. 也就是说，我们首先将 AiB 移动到目标中，然后apply在其中调用目标AiB。

但是，我在其他场合感到困惑：

根据教程，这个对 进行案例分析(EM (P y))，然后//尝试解决琐碎的子目标。然后？？move =>将其余的引入上下文？这里的操作顺序是什么？

让，是EM_吗？我读对了吗，战术应用的“正确顺序”是什么？(EM (P y))(move=> notPy (// ( case (:EM_) ) ) )

顺序有点扭曲，一般来说notPy不一致。有没有办法在合法的 ssreflect 中从右到左写上面的内容？