在 COQ 中使用归纳法证明某事物小于或等于其他事物答案

【问题标题】：Prove something is less or equal to other thing using induction in COQ在 COQ 中使用归纳法证明某事物小于或等于其他事物
【发布时间】：2018-06-24 23:07:53
【问题描述】：

我需要证明一个公式的树的高度总是小于同一棵树的节点数，但是我在假设之后卡住了，不知道如何进行。有人可以帮我填写“录取通知书”吗？空格？

Require Import String.
Require Import Init.Nat.
Require Import PeanoNat.
Require Import Plus.
Require Import Le.

Theorem le_plus_trans2 : forall n m p, (n <= m) -> (n <= p + m).

Proof.
 intros n m p.
 intros x.
 apply le_trans with (m:= m).
 assumption.
 admit.
Qed.

【问题讨论】：

请去掉题名中的“使用归纳法”，以便对其他人有用。

标签： coq induction inequality

【解决方案1】：

如果您是Require Import Coq.omega.Omega，您可以将所有admits 替换为omega。

或者，如果您想要一个不那么麻烦的解决方案，您可以将您的 admits 替换为

 etransitivity; [ eassumption | apply le_plus_l || apply le_plus_r ].

也就是说，您可以将x <= x + y 和y <= x + y 用于x : nat 和y : nat。

编辑（在您更新问题之后）。你的问题现在包含一个完全不同的目标，但是这个目标仍然可以通过标准算术锤来解决。如果你Require Import Coq.omega.Omega，你的整个定理都被intros; omega.证明了

【讨论】：

我找到了一种使用 le_plus_trans 的方法，因为 k1
在问题已经得到回答后用另一个问题替换您的问题是一种糟糕的形式。但是，我已经用针对这种形式的所有问题的标准解决方案更新了我的答案：omega。
另外，您阅读我的原始答案了吗？您剩下的目标正是我在回答中提到的定理陈述le_plus_r。
很抱歉更改它，只是我的主要目标是完成整个证明。我读了它，但是我误读了 le_plus_r 的“定义”，所以这就是我感到困惑的原因。无论如何，非常感谢您的帮助和时间！
不用担心。我认为 StackOverflow 上的一般礼仪是，如果您发布的问题的完整答案给您留下了新的问题，则发布单独的问题。

【解决方案2】：

尝试使用Plus.le_plus_trans 和PeanoNat.Nat.add_comm。

【讨论】：

我用“le_plus_trans”做了，但现在我需要别的东西xD