问题标签 [coq-tactic]

我读到类型的归纳原理只是关于命题的定理P。List所以我构造了一个基于右（或反向）列表构造函数的归纳原理。

归纳原理本身是：

但是现在，我在使用这个定理时遇到了麻烦。我不知道如何调用它来达到与induction策略相同的效果。

例如，我试过：

但在最后一行，我得到：

定义和应用自定义归纳原则的正确步骤是list_ind_rcons什么？

谢谢

我的问题与如何exist在一组条件/假设中构造一个术语有关。

我有以下中间证明状态：

在我的脑海中，我知道因为H0,x是 的见证人(exists x : X, P x -> False)，我想介绍一个名字：

基于以上推理，然后用 withapply H in w生成False假设中的 a，最后inversion生成False.

但我不知道使用什么策略/语法来介绍w上面的见证。到目前为止，我能达到的最好的就是Check (ex_intro _ (fun x => P x -> False) x H0)).给出False.

有人可以解释如何引入存在条件，或者完成证明的另一种方法吗？

谢谢。

PS我要证明整个定理的是：

我正在编写一种策略来查找与绑定列表中的键关联的值。就像是：

不幸的是，我不知道密钥的确切形式；相反，我知道一个与之匹配的模式。更准确地说，我正在寻找的关键是调用类型类方法的结果，但我事先不知道将使用哪个实例。在下面的示例中，我知道关键是对 的调用show "a"，但我不知道使用什么实例：

assoc除了传递一个检查匹配的ltac之外，我可以在这里使用一个技巧吗？理想情况下，它看起来像(show (Show := _) "a")，或者可能(fun inst => show (Show := inst) "a")。

只有在命令成功后，有没有办法在 Ltac 中打印（使用idtac？）一条消息？就像是

这几乎可以工作，除了多个子目标会导致打印多条消息：

仅过滤第一个目标似乎有效......

...除非它没有：

我可能可以将这两种模式合二为一，但我不太热衷于 100% 的点球命中率。这仍然不能解决完全实现目标的策略的情况。

（我最感兴趣的是 8.5 之前的 Coq 的答案，因为在 8.5Info和类似版本中为此提供了很好的设施。即使在 8.5 中，能够仅在某些点打印调试消息也会很有趣）

我是 Coq 证明系统的初学者（大约 4 天）。我已经很努力了，但我无法证明以下内容。

据我所知，我们需要证明 + 的双射性，这样我们才能以某种方式使用f(b) = f(c) -> b = c. 我该怎么做呢 ？

我在下面有一个证明，还有三个子目标要做。证明是关于用这里演示的简单算术语言优化 away plus 0( ) 的正确性。是“算术表达式”并且是“算术评估”。optimize_0plusaexpaeval

，其中optimize_0plus是：

我的作战计划是应用optimize_0plus在当前子目标的 LHS 中，并获得：

（但我不知道如何在 Coq 中做到这一点）。

然后，通过 some simpl，得到：

并应用归纳假设IHa1并IHa2完成证明。

我的问题是：

我如何告诉 Coq 只应用optimize_0plus一次的定义，并且不做多也不做少？

我试过simpl optimize_0plus了，但它给出了一个很长的match陈述，这似乎做得太多了。而且我不喜欢rewrite每次都使用这种策略来建立引理，因为这种计算恰好是纸笔的一步。

笔记：

1.这与我之前的问题有关，但那里关于使用的答案simpl XXX似乎在这里不起作用。这似乎是一个更复杂的案例。

2.原始网站提供了有效的证明。但是那里的证明似乎比必要的复杂，因为它开始对条款a1等进行案例分析。

所以，我关心的不是真正证明这个简单的定理，而是如何像在纸上一样直观地证明这一点。

- 更新 -

感谢@gallais，我原来的计划是不正确的，因为可以改变

至

仅适用于a1is not的情况ANum 0。案件须按注 2 所引之课程网站0另行处理。destruct a1.

但是，对于下面列出的其他情况，我仍然有同样的问题，我认为我的原始计划应该可行：

对于这 5 种情况中的每一种，似乎一个应用程序（beta减少？？）optimize_0plus应该允许我们改变例如（for AMinus）

至

， 正确的？

如果是这样，我该如何做这个一步减少？

注意：我试过

而且我什至无法得到aeval (AMinus (optimize_0plus a1) (optimize_0plus a2))我想Eval在证明中使用的。

I have some equalities (=) and unequalities (<>) in the hypotheses such as:

I want to use tactics like assumption, but sometimes the expected (un)equality in the goal is in the other direction like:

My question is:

Is it possible to automatically introduce the symmetric forms of (un)equality above into the hypotheses?

If not, is it possible to use Notation to write a tactical to do this.

So far, I can do this manually like this:

But it is really tedious and noisy. I don't know enough about how to automate this or if there is a better way.

我在证明期间处于需要对列表长度进行案例分析的情况l。

1. 当length l < 2它是一种情况（其中二进制操作+不适用）
2. 当length l >= 2它是另一种情况时（适用二进制操作）

我如何使用destruct或其他一些策略来做到这一点，并获得两种情况，即真假？

我试过：

但没有一个奏效。

I am reading/testing a proof in Coq

The specific functions/definitions don't matter as they are not used. After a few steps, the theorem is transformed to a form where the inner existential quantifier is changed to a universal:

This is basically,

Although this is not exactly replacing exists i with forall i verbatim, I am kind of surprised. I was wondering if this kind of replacing existential quantifier with universals always possible, or when is this possible? What's the general rule/technique for this conversion?

(I vaguely remember something called skolemization but didn't quite understand it when learning it.)

The steps in Coq (8.4) to transform the theorem are:

I have just run into the issue of the Coq induction discarding information about constructed terms while reading a proof from here.

The authors used something like:

to rewrite a hypothesis H before the actual induction induction H. I really don't like the idea of having to introduce a trivial equality as it looks like black magic.

Some search here in SO shows that actually the remember trick is necessary. One answer here, however, points out that the new dependent induction can be used to avoid the remember trick. This is nice, but the dependent induction itself now seems a bit magical.

I have a hard time trying to understand how dependent induction works. The documentation gives an example where dependent induction is required:

I can verify how induction fails and dependent induction works in this case. But I can't use the remember trick to replicate the dependent induction result.

What I tried so far to mimic the remember trick is:

But this doesn't work. Anyone can explain how dependent induction works here in terms of the remember-ing?