Coq：我如何证明所有n m：nat，n> m->S n> S m？

问题描述

因此，我一直在学习使用Coq，直到现在为止，我一直在使用自己定义的自然类型，因此，我不清楚100％可以使用默认自然类型做什么。但是，程序修订点需要它，而我最终需要利用（n> m）->（S n> S m）这个事实（对人类来说是显而易见的）。我似乎无法证明这一点-我运行类似

Theorem gt_triv : forall n m : nat,n > m -> (S n) > (S m).
intros.

然后我有了一个假设n > m和一个目标证明(S n) > (S m)，但是我似乎对此无能为力（除了将其展开为S (S m) <= S n之外，它没有似乎更有用）-我不知道我什至会运行什么命令。

谢谢您的建议。

解决方法

证明此陈述的最快方法是使用专门用于线性整数算术的库或自动策略。

第一个例子。

Require Import Arith.

Search (S _ > S _).  (* This is not needed,*)
  (* but this is how you can find the relevant theorem. *)

Theorem gt_triv : forall n m: nat,n > m -> S n > S m.
Proof.
exact gt_n_S.
Qed.

另一种解决方案是观察gt_triv的语句包含变量中仿射公式之间的比较。现有的称为lia的自动策略可以解决这一问题。因此，另一个解决方案将具有以下完整的脚本。

Require Import Lia. 
Theorem gt_triv : forall n m: nat,n > m -> S n > S m.
Proof.
lia.
Qed.

,

如果您发现您的定理是n S n y的定义会展开为S y

Theorem gt_triv : forall n m : nat,n <= m -> S n <= S m.
  intros.
  (* By definition of leb in the relation n <= m,m is the only one which is 
      inductively defined,we should stick n and do induction on m *)
  generalize dependent n.
  induction m.
  intros.
  destruct n.
  apply le_n.
  (* there is no x + 1 <= 0 *)
  inversion H.
  intros.
  (* notice we need a n <= m to solve our goal,but we only have a n <= S m,therefore
      by our definition H is constructed by n <= m (by construction of le_S) or n = m (by construction of le_n)*)
  inversion H.
  (*trivially both are equal*)
  apply le_n.
  (* our induction hypothesis give us S n <= S m,so S n <= S (S m) is trivial by constructor le_S*)
  apply (le_S _ _ (IHm _ H1)).
Qed.

现在，您要证明的定理变得非常简单：

Theorem gt_really_triv : forall n m : nat,n > m -> (S n) > (S m).
intros.
apply gt_triv.
trivial.
Qed.

有很多方法可以证明该定理，您无需使用我的定义。我建议您再尝试一次以其他方式证明该定理，例如，您可以对自然使用双重归纳原理。

,

Theorem gt_triv : forall n m : nat,n > m -> (S n) > (S m).
  induction 1.
  - apply le_n.
  - apply le_S,IHle.
Qed.