为什么isabelle的预购需要提供less_and_less_eq

Question

Isabelle 的

preorder

课程需要同时提供

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"

--- https://www.isa-afp.org/sessions/hol/#Orderings.html#Orderings.preorder.intro_of_class|事实

但是真的很烦人。我有一个

<=

关系，我想证明这是一个预购，但 Isabelle 强迫我定义一个相应的

<

。我可以，但（就我而言，很多）我不需要额外的工作。

为什么伊莎贝尔强迫我这样做？有没有一种好方法可以从给定的

<

导出虚拟

<=

。我应该定义自己的

preorder

只需要

<=

吗？

有一个本地叫

partial_preorder

，只需要

<=

，就像我需要的那样，但它不是一个类。

Answer 1

Isabelle 迫使我定义一个相应的

<

。我可以，但（就我而言，很多）我不需要额外的工作。

从技术上讲，

<

并不是真正的额外工作，不是吗？ 类公理

‹x < y ⟷ x ≤ y ∧ ¬ (y ≤ x)›

并没有真正为

<

的实现留下选择。

让我们考虑以下具有逐点比较的两分量 nat 向量的最小示例：

datatype nat_vec2 =
  Vec nat nat

fun nat_vec_lesseq where
  ‹nat_vec_lesseq (Vec m1 m2) (Vec n1 n2) ⟷ m1 ≤ n1 ∧ m2 ≤ n2›

将其实例化为预购只需要几行，我们在其中说明哪些函数应该扮演

≤

和

<

的角色（为此 我们必须使用神奇的名称

less_eq_nat_vec2

和

less_nat_vec2

），然后证明类公理：

instantiation nat_vec2 :: preorder
begin

definition ‹less_eq_nat_vec2 ≡ nat_vec_lesseq›
definition ‹less_nat_vec2 m n ≡ nat_vec_lesseq m n ∧ ¬ nat_vec_lesseq n m›

instance proof
  fix m n::nat_vec2
  show ‹(m < n) = (m ≤ n ∧ ¬ n ≤ m)›
    unfolding less_nat_vec2_def less_eq_nat_vec2_def by blast
next
  fix m::nat_vec2
  show ‹m ≤ m›
    unfolding less_eq_nat_vec2_def by (cases m, simp)
next
  fix m n p::nat_vec2
  assume ‹m ≤ n› ‹n ≤ p›
  thus ‹m ≤ p›
    unfolding less_eq_nat_vec2_def by (cases m, cases n, cases p, auto)
qed

end

你是对的，

<

需要一些样板。 但它只有一行定义，两行用于实例证明的第一种情况！

对于每个定义的预订单来说，这些行实际上都是相同的。 （人们只需要针对不同的实例化调整神奇的变量名称..）另一方面，其他情况（自反性和传递性）可能会更加复杂，具体取决于使用的顺序。

因此，提供

<

并没有多大意义，因为它实际上并没有增加很多额外的工作。

特别是，定义自己的

preorder

来解决这个问题，肯定会需要更多的工作，因为它使理论与内置排序类的所有便利性脱节。 （例如派生

min

、

max

等）

简短回答标题中关于

ord

背后的设计决策的问题： 我假设

<

的良好全局中缀概念取决于它是类接口的一部分，而不是被定义为订单的派生常量（例如常量名称

min

和

max

）。 但我从来没有真正理解《伊莎贝尔》中“继承”符号的精确规则；所以这只是一个猜测。