CODEWITHSUNDEEP
coqssreflect
VHarisop
VHarisop

Reputation: 2826

Proving simple inequality in Ssreflect

I'm having trouble with some pretty simple proofs in Coq, using the MathComp library for reflection.

Suppose I want to prove this Lemma:

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.

This approach seems a little "unorthodox" to me for such a simple task. Is there a better/simpler way to do this?

Upvotes: 1

Views: 183

Answers (2)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23612

Yes, there is a better way. Your lemma is a special case of ltnW : forall m n, m < n -> m <= n:

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

This works because n < m is actually syntactic sugar for n.+1 <= m.

Upvotes: 5

gallais
gallais

Reputation: 12113

I haven't practiced ssreflect a lot so I can't really tell whether this can be golfed down but basically the idea is that 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.

Upvotes: 1

Related Questions