为何Isabelle的preorder类要求同时提供less和less_eq？

问题背景 #

Isabelle/HOL中的preorder类继承自ord类，要求同时提供less_eq（即≤）和less（即<）两种关系，定义如下：

class ord =
  fixes less_eq :: "'a ⇒ 'a ⇒ bool"
    and less :: "'a ⇒ 'a ⇒ bool"

class preorder = ord +
  assumes less_le_not_le: "x < y ⟷ x ≤ y ∧ ¬ (y ≤ x)"
  and order_refl [iff]: "x ≤ x"
  and order_trans: "x ≤ y ⟹ y ≤ z ⟹ x ≤ z"

如果已经有一个满足自反性、传递性的≤关系，想证明它属于preorder类，却被强制定义对应的<，会觉得额外工作量冗余。以下针对核心疑问逐一解答：

1. 为什么Isabelle要同时要求less_eq和less？ #

• 体系一致性：Isabelle的序类体系从基础的ord到preorder、partial_order、linorder等，统一将两种序关系作为核心符号，确保所有序相关的定理、工具都能基于这套统一的符号体系复用，避免不同场景下符号混乱。
• 实用便利性：数学中<和≤都是高频使用的关系，提前绑定两种符号后，可直接调用大量已预定义的关于<的引理，无需每次手动推导转换规则。

2. 有没有简便方法从给定的≤推导出对应的<？ #

有，直接用preorder类要求的等价式定义<即可，证明过程几乎无额外工作量：

1. 用definition快速定义<：

definition less :: "'a ⇒ 'a ⇒ bool" where
  "less x y ≡ x ≤ y ∧ ¬ (y ≤ x)"

2. 证明该定义满足less_le_not_le公理：

lemma less_le_not_le: "x < y ⟷ x ≤ y ∧ ¬ (y ≤ x)"
  unfolding less_def by simp

完成这两步后，结合已有的≤的自反性、传递性证明，就能顺利将你的类型归入preorder类。

3. 是否应自定义仅要求≤的preorder类？ #

不推荐自定义这类类，原因如下：

• 自定义类会脱离Isabelle的标准序类生态，无法使用大量已有的自动化工具（如simp规则、order_trans的自动链式推导）和预证明定理，后续扩展或复用代码时会遇到更多阻碍。
• 如果只是需要在局部证明中使用仅基于≤的预序关系，可以使用你提到的partial_preorder local，它仅要求≤满足自反性和传递性，适合局部场景，无需全局修改类体系。

内容的提问来源于stack exchange，提问作者Mathieu Paturel