在Ssreflect中证明简单的不等式

Question

我在Coq中使用MathComp库进行反射时遇到了一些非常简单的问题。

假设我要证明这个定理：

From mathcomp Require Import ssreflect ssrbool ssrnat. 

Lemma example m n: n.+1 < m -> n < m. 
Proof. 
     have predn_ltn_k k: (0 < k.-1) -> (0 < k). 
      by case: k. 
     rewrite -subn_gt0 subnS => submn_pred_gt0. 
     by rewrite -subn_gt0; apply predn_ltn_k. 
Qed. 

这种做法似乎有点“非正统”给我这样一个简单的任务。有没有更好/更简单的方法来做到这一点？

Answer 1

是的，有一个更好的办法。你引理是ltnW : forall m n, m < n -> m <= n一个特殊情况：

Lemma example n m : n.+1 < m -> n < m. 
Proof. exact: ltnW. Qed. 

这工作，因为n < m是n.+1 <= m实际语法糖。

Answer 2

我没有练过ssreflect了很多，所以我真的不能告诉这是否可以golfed下来，但基本思路是n < n.+1 < m：

Require Import mathcomp.ssreflect.ssrnat. 
Require Import mathcomp.ssreflect.ssrbool. 
Require Import mathcomp.ssreflect.ssreflect. 

Lemma example m n: n.+1 < m -> n < m. 
Proof. 
move => ltSnm; apply: ltn_trans; by [apply ltnSn | apply ltSnm]. 
Qed.