Why unable to perform case analysis in rather simple case

Question

Well, the code

From mathcomp Require Import ssreflect ssrnat ssrbool eqtype.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Inductive nat_rels m n : bool -> bool -> bool -> Set :=
| CompareNatLt of m < n : nat_rels m n true false false
| CompareNatGt of m > n : nat_rels m n false true false
| CompareNatEq of m == n : nat_rels m n false false true.

Lemma natrelP m n : nat_rels m n (m < n) (m > n) (m == n).
Proof.
  case (leqP m n); case (leqP n m).
  move => H1 H2; move: (conj H1 H2) => {H1} {H2} /andP.
  rewrite -eqn_leq => /eqP /ssrfun.esym /eqP H.
    by rewrite H; constructor.
  move => H. rewrite leq_eqVlt => /orP. 
  case.

Error is Error: Case analysis on sort Set is not allowed for inductive definition or. The last goal before the case is

  m, n : nat
  H : m < n
  ============================
  m == n \/ m < n -> nat_rels m n true false (m == n)

I've already used this construction (rewrite leq_eqVlt => /orP; case) in very similar situation and it just worked:

Lemma succ_max_distr n m : (maxn n m).+1 = maxn (n.+1) (m.+1).
Proof.
  wlog : m n / m < n => H; last first.
  rewrite max_l /maxn; last by exact: ltnW.
  rewrite leqNgt.
  have: m.+1 < n.+2 by apply: ltnW.
    by move => ->.
    case: (leqP n m); last by apply: H.
  rewrite leq_eqVlt => /orP.  case.

1. What is the difference between two cases?
2. and Why "Case analysis on sort Set is not allowed for inductive definition or"?

Answer 1

The difference between the two cases is the sort of the goal (Set vs Prop) when you execute the case command. In the first situation your goal is nat_rels ... and you declared that inductive in Set; in the second situation your goal is an equality that lands in Prop.

The reason why you can't do a case analysis on \/ when the goal is in Set (the first situation) is because \/ has been declared as Prop-valued. The main restriction associated to such a declaration is that you cannot use informative content from a Prop to build something in Set (or more generally Type), so that Prop is compatible with an erasure-semantic at extraction time.

In particular, doing a case analysis on \/ gives away the side of the \/ that is valid, and you can't be allowed to use that information for building some data in Set.

You have at least two solutions at your disposal:

1. You could move your family nat_rels from Set to Prop if that's compatible with what you want to do later on.
2. Or you could use the fact that the hypothesis that you want to branch on is decidable and find a way to produce some {m == n} + { m <n } out of m <= n; here the notation { _ } + { _ } is the Set-valued disjunction of proposition.