如何在Coq中添加平等的双方

问题描述

这似乎是一个非常简单的问题，但是我找不到任何有用的东西。

我有一条语句

  n-x = n 
  

想证明

 （n-x）+ x = n + x 
  

我无法找到定理允许这样做。

解决方案

您应该看看重写策略（然后也许是自反性）。 / p>

编辑：有关重写的更多信息：

• 您可以重写H 重写-> H 从左向右重写


• 您可以重写<-H 从右向重写left



• 您可以使用模式策略仅选择要重写目标的特定实例。例如，仅重写第二个 n ，可以执行以下步骤

  
  
  

  模式n为2。 b $ b重写<-H。

在您的情况下，解决方案要简单得多。

This seems like a really simple question, but I wasn't able to find anything useful.

I have the statement

n - x = n

and would like to prove

(n - x) + x = n + x

I haven't been able to find what theorem allows for this.

解决方案

You should have a look at the rewrite tactic (and then maybe reflexivity).

EDIT: more info about rewrite:

• You can rewrite H rewrite -> H to rewrite from left to right
• You can rewrite <- H to rewrite from right to left

• You can use the pattern tactic to only select specific instances of the goal to rewrite. For example, to only rewrite the second n, you can perform the following steps

  pattern n at 2.rewrite <- H.

In your case, the solution is much simpler.

这篇关于如何在Coq中添加平等的双方的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！