Prouver l'inégalité simple dans Ssreflect

Question

J'ai des problèmes avec des preuves assez simples dans Coq, en utilisant la bibliothèque MathComp pour la réflexion.

Supposons que je veux prouver Lemme:

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. 

Cette approche me semble un peu « peu orthodoxe » à une tâche simple. Existe-t-il un moyen meilleur/plus simple de le faire?

Answer 1

Oui, il y a une meilleure façon. Votre lemme est un cas particulier de ltnW : forall m n, m < n -> m <= n:

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

Cela fonctionne parce que le sucre est n < m en fait syntaxique pour n.+1 <= m.

Answer 2

Je n'ai pas pratiqué ssreflect beaucoup donc je ne peux pas vraiment dire si cela peut être golfed vers le bas mais, fondamentalement, l'idée est que 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.