有没有关于模式的三值案例分析（a < b) (a = b) (a > b）？

Question

我希望我的学生通过二叉搜索树证明一些东西。 大多数证明需要对三种情况下的算术不等式进行案例分析：

• 一个< b (recursive call in the left subtree of the BST)
• a = b（密钥满足目标属性）
• a > b（BST 右子树递归调用）

为此，我编写了一种丑陋的策略来检查目标是否包含嵌套的 if 对应这三种情况：

(* 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.

其中

not_lt_nor_gt_is_eq

是一个辅助引理，我自己证明如下（证明无关紧要）：

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

我对这个解决方案并不完全满意，因为它对学生如何编写代码非常敏感，而且它对我来说也太长了。

所以我的问题是：

• 是否有任何 stdlib 策略可以做类似的事情？
• 如果没有，你能改进我的吗？

Answer 1

lt_eq_lt_dec

库中的

Arith

函数返回表示三种可能情况的总和类型：

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

可以处理这个和其他类似的不等式：

Require Import Lia.

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