如何证明对于所有 n m, n <= m -> m <= n -> n = m

Question

定理 le_trans: forall n m o, n <= m -> m <= o -> n <= o. Proof. intros n m o Lnm Lmo. generalize dependent Lnm.
概括依赖 n. 感应Lmo。 -介绍。应用Lnm。 -介绍。应用 le_S。适用国际人道主义法。应用Lnm。 问了。

如何证明： 定理 le_antisym: forall n m, n <= m -> m <= n -> n = m.

我不知道这两个命题之间是否有关系，是否需要用第一个命题来辅助证明第二个命题，如果有，如何证明，如果没有，如何证明

Answer 1

这些问题很有趣，但常常被忽视。它们很大程度上取决于

<=

的定义。使用 StdLib 中的归纳表征，可以进行如下操作：

Fact le_trans n m p : n <= m -> m <= p -> n <= p.
Proof. 
  induction 2.
  + trivial.
  + now constructor.
Qed.

Fact le_n_Sn n : n <= S n.
Proof. do 2 constructor. Qed. 

Fact le_S_inv n m :
      n <= m
   -> match n, m with 
      | 0, _     => True
      | S _, 0   => False
      | S n, S m => n <= m
      end.
Proof.
  induction 1 as [ | m H _ ]; destruct n; auto.
  apply le_trans with (2 := H), le_n_Sn.
Qed.

Fact le_anti n m : le n m -> le m n -> n = m.
Proof.
  induction n in m |- *; destruct m;
    intros ?%le_S_inv ?%le_S_inv; tauto || auto.
Qed.

反演引理

le_S_inv

在这里是一个关键工具。它包括研究归纳谓词和参数形状的模式匹配之间的相互作用。