[SOLVED] Is there a three-valued case analysis on patterns (a

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

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?

Solution

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.