Coq：我如何证明 forall n m : nat, (n > m) -> (S n > S m)？
Coq: How do I prove that forall n m : nat, (n > m) -> (S n > S m)?
所以我一直在学习使用 Coq，直到现在我一直在使用我自己定义的自然类型，所以我不是 100% 清楚默认自然类型可以做什么。不过，Program Fixpoint 需要它，而我最终需要利用 (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，这似乎并没有多大用处）-我什至不知道我什至 运行 的命令是什么。
感谢任何建议。
如果你注意到你的定理是 n <= m -> S n <= S m 的推论，一旦你说过 x > y 的定义展开为 S y <= x。所以，要证明上面的引理，只需要对m进行归纳即可。
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.
这个定理有很多方法可以证明，你不需要用我的定义。我建议您再尝试一次使用其他方法证明该定理，例如，您可以对自然数使用双重归纳原理。
证明此陈述的最快方法是使用专门用于线性整数运算的库或自动化策略。
第一个例子。
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.
Theorem gt_triv : forall n m : nat, n > m -> (S n) > (S m).
induction 1.
- apply le_n.
- apply le_S, IHle.
Qed.
所以我一直在学习使用 Coq，直到现在我一直在使用我自己定义的自然类型，所以我不是 100% 清楚默认自然类型可以做什么。不过，Program Fixpoint 需要它，而我最终需要利用 (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，这似乎并没有多大用处）-我什至不知道我什至 运行 的命令是什么。
感谢任何建议。
如果你注意到你的定理是 n <= m -> S n <= S m 的推论，一旦你说过 x > y 的定义展开为 S y <= x。所以，要证明上面的引理，只需要对m进行归纳即可。
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.
这个定理有很多方法可以证明，你不需要用我的定义。我建议您再尝试一次使用其他方法证明该定理，例如，您可以对自然数使用双重归纳原理。
证明此陈述的最快方法是使用专门用于线性整数运算的库或自动化策略。
第一个例子。
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.
Theorem gt_triv : forall n m : nat, n > m -> (S n) > (S m).
induction 1.
- apply le_n.
- apply le_S, IHle.
Qed.