Nachweis einfache Ungleichheit in Ssreflect

Question

Ich habe Probleme mit einigen ziemlich einfachen Beweise in Coq, mit der MathComp-Bibliothek für die Reflexion.

Angenommen ich dieses Lemma beweisen wollen:

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. 

Dieser Ansatz scheint ein wenig „unorthodox“ mir für eine solche einfache Aufgabe. Gibt es einen besseren/einfacheren Weg dies zu tun?

Answer 1

Ja, es einen besseren Weg gibt. Ihre Lemma ist ein Spezialfall von ltnW : forall m n, m < n -> m <= n:

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

Das funktioniert, weil n < m für n.+1 <= m tatsächlich syntaktischen Zucker ist.

Answer 2

Ich habe nicht ssreflect viel geübt, so kann ich nicht wirklich sagen, ob diese golfed gelegt werden kann, aber im Grunde ist die Idee, dass 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.