3

In vanilla Coq, I'd write

Require Import Coq.Arith.Arith.
Goal nat -> nat -> False.
  intros n m.
  destruct (lt_eq_lt_dec n m) as [[?|?]|?].

to get three goals, one for n < m, one for n = m, and one for m < n. In ssreflect, I'd start with

From Coq.ssr Require Import ssreflect ssrbool.
From mathcomp.ssreflect Require Import eqtype ssrnat.
Goal nat -> nat -> False.
  move => n m.

What's the standard/canonical way to divide this into three cases, for n < m, n == m, and m < n, in ssreflect?

Jason Gross
  • 5,928
  • 1
  • 26
  • 53

1 Answers1

4

You can use ltngtP:

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
Goal nat -> nat -> False.
  move => n m.
  case: (ltngtP n m) => [n_lt_m|m_lt_n|n_eq_m].

In accordance with the ssreflect style, this lemma automatically simplifies comparison functions such as n < m, n == m, etc. in the goal.

Cyril
  • 367
  • 2
  • 7
Arthur Azevedo De Amorim
  • 23,012
  • 3
  • 33
  • 39
  • 3
    You may prefer to feed the expression you are interested as the index of the ltngtP predicate, thus `case: (n < m) / ltngtP => ...` , it usually comes in handy [and helps understanding the default behavior for just `case: ltngtP`. – ejgallego Sep 27 '21 at 18:18
  • 1
    Also the last case will give you `n = m`, i.e., the propositional equality. If you need `n==m`, change the last part to `...|/eqP n_eq_m].` – Alexander Gryzlov Sep 27 '21 at 18:37
  • I recommend `From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.` for the imports, (note that `order` is not necessary here, `ssrfun` is mandatory, and `mathcomp` ones should be priviledged over Coq's (which might be older)) – Cyril Dec 01 '21 at 20:36