Is there a three-valued case analysis on patterns (a < b) (a = b) (a > b)?

Question

I want my students to prove some stuff overs Binary Search Trees. Most of the proofs require to perform a case analysis on some arithmetic inequality over three cases:

• a < b (recursive call in the left subtree of the BST)
• a = b (the key satisfies the target property)
• a > b (recursive call in the right subtree of the BST)

To do that i've written a kind of ugly tactic that checks if the goal contains nested ifs that correspond to these three cases:

(* This is some syntactic sugar for nested if like:
   if a <? b then      (* adds hypothesis a<?b *)
   else if a >? b then (* adds hypothesis b<?a *)
   else                (* adds hypothesis a=b *) *)
Ltac case_ineq :=
  match goal with
  | [ |- context[if ?X <? ?Y then _ else if ?Y <? ?X then _ else _ ]] =>
      case_eq (X <? Y); intros;
      [> | case_eq (Y <? X); intros;
           [> | assert (X = Y);
                only 1 : (apply not_lt_nor_gt_is_eq; assumption)]]
  end.

Where not_lt_nor_gt_is_eq is an auxilliary lemma i've proven by myself stated as follows (the proof is irrelevant):

Lemma not_lt_nor_gt_is_eq : forall x k,
  (x <? k) = false -> (k <? x) = false <-> x = k.

I'am not entirely satisfied with this solution as it is very sensitive to how students will write code, and its also too long to my taste.

So my question is:

• Is there any stdlib tactic that does something similar?
• If not, could you improve on mine?

Answer 1

The lt_eq_lt_dec function from the Arith library returns a sum type that represents three possible cases: a < b, a = b, or a > b.

Require Import Arith String.

Definition three_valued_case_analysis (a b : nat) : string :=
  match lt_eq_lt_dec a b with
  | inleft (left _) => "a < b"
  | inleft (right _) => "a = b"
  | inright _ => "a > b"
  end.

Answer 2

lia can handle this and other similar inequalities:

Require Import Lia.

Example lia_example: forall n, n < 3 \/ 3 <= n < 9 \/ n >= 9.
lia.
Qed.