时间戳

首页 > 解决方案 > Coq：如何证明 forall nm, n <= m \/ m <= n

coq - Coq：如何证明 forall nm, n <= m \/ m <= n

问题描述

如何证明

定理 le_total：对于所有 nm，n <= m \ / m <= n。

以下是我可能有帮助的定理：

Inductive le : nat -> nat -> Prop :=
 | le_n (n : nat)                : le n n
 | le_S (n m : nat) (H : le n m) : le n (S m).

Notation "n <= m" := (le n m).

Theorem le_le_S : forall n m,
 n <= m -> S n <= S m.
Proof.
 intros n m H. induction H.
 - (* le_n *)
   apply le_n.
 - (* le_S *)
   apply le_S. apply IHle.  Qed.

(** **** Exercise: 1 star, standard (le_trans) *)

Lemma le_trans : forall m n o, m <= n -> n <= o -> m <= o.
Proof.
 intros m n o Lmn Lno.
 generalize dependent Lmn.
 generalize dependent m.
 induction Lno.
 -intros. apply Lmn.
 -intros. apply le_S. apply IHLno. apply Lmn.
Qed.
(** [] *)

(** **** Exercise: 1 star, standard (O_le_n) *)
Theorem O_le_n : forall n,
 0 <= n.
Proof.
 intros. induction n.
 apply le_n.
 apply le_S. apply IHn.
Qed.

我能够达到一个点，即在 n 上使用归纳可以让我到达一个好位置，但我不知道在那之后该去哪里。

标签： coq

解决方案

我的猜测是你的归纳假设不够普遍。关于两个变量（在这种情况下）的一些结果n需要m归纳在n上m。所以一开始，而不是

Proof.
  intros n m.
  induction n.

做：

Proof.
  intros n.
  induction n.

推荐阅读