isabelle - Isabelle 中的商类型模式是什么？

Question

Isabelle 中的“商类型模式”是什么？

我在互联网上找不到任何解释。

score 8 · Accepted Answer

如果你能从你看到这句话的地方引用一点的话会更好。我知道“模式匹配”，也知道“商类型”，但我不知道“商类型模式”。

我宁愿不要求澄清，然后等待，所以我选择了三个词中的两个，“商类型”。如果我走错了路，它仍然是一个有价值的主题，也是 Isabelle/HOL 的重要组成部分。

有quotient_type关键字，它允许您定义具有等价关系的新类型。

它是商包的一部分，从 isar-ref.pdf 的第 248 页开始描述。恰好有一个 Wiki 页面Quotient_type。

Brian Hufmann 和 Ondřej Kunčar 给出了更复杂的描述。转到 Kunčar 的网页，查看标题为Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL的两份 PDF ，它们并不完全相同。

碰巧举重类型和商类型密切相关，而且不容易理解，这就是为什么我试着在这里和那里学习一点，就像现在一样，以更好地理解这一切。

HOL中的整数和有理数都是商类型，我选择一个作为例子，整数

您可以从查看Int.thy开始。

对于商类型，您需要一个等价关系，它定义了一个集合，并且intrel用于为 type 定义该集合int。

definition intrel :: "(nat * nat) => (nat * nat) => bool" where
  "intrel = (%(x, y) (u, v). x + v = u + y)"

这是基于自然数的整数的经典定义。整数是自然数的有序对（以及我在下面描述的集合），并且根据该定义它们是相等的。

例如，非正式地，(2,3) = (4,5)因为2 + 5 = 4 + 3。

我让你感到无聊，你在等待好东西。这是其中的一部分，使用quotient_type：

quotient_type int = "nat * nat" / "intrel"
  morphisms Rep_Integ Abs_Integ

这两个态射发挥作用，如果你想紧张你的大脑，并真正了解发生了什么，我就是这样做的。有很多函数和quotient_type生成的简单规则，你必须做很多工作才能找到它们，比如使用find_theorems命令。

函数将Abs有序对抽象为int. 检查这些：

lemma "Abs_Integ(1,0) = (1::int)"
  by(metis one_int_def) 
  
lemma "Abs_Integ(x,0) + Abs_Integ(y,0) ≥ (0::int)"
  by(smt int_def)

它们表明，int在引擎的引擎盖下，an 确实是有序的一对。

现在我展示了这些态射的显式类型，以及Abs_int和Rep_int，它们int不仅显示为有序对，而且显示为一组有序对。

term "Abs_int   :: (nat * nat) set => int"  
term "Abs_Integ :: (nat * nat) => int"

term "Rep_int   :: int => (nat * nat) set"
term "Rep_Integ :: int => (nat * nat)"

我又让你厌烦了，但我有一种情感需要展示更多的例子。如果有序对的分量相差 1，则两个正整数相等，例如：

lemma "Abs_Integ(1,0) = Abs_Integ(3,2)"
  by(smt nat.abs_eq split_conv) 
 
lemma "Abs_Integ(4,3) = Abs_Integ(3,2)"
  by(smt nat.abs_eq split_conv)

如果您添加Abs_Integ(4,3)and ，您会期望什么Abs_Integ(3,2)？这个：

lemma "Abs_Integ(2,3) + Abs_Integ(3,4) = Abs_Integ(2 + 3, 3 + 4)"
  by(metis plus_int.abs_eq plus_int_def split_conv)

plus_int证明中的内容在 Int.thy 的第44 行中定义。

lift_definition plus_int :: "int => int => int"
  is "%(x, y) (u, v). (x + u, y + v)"

这个吊装是怎么回事？这会让我陷入这种解释的“几天”，而我才刚刚开始理解它。

正如我所说，这些find_theorems节目隐藏了很多东西：

thm "plus_int.abs_eq"  

find_theorems name: "Int.plus_int*"

更多示例，但这些是为了强调，在引擎的引擎盖下，int一个等价类作为一个集合连接到一个等价类，我在intrel上面使用它来定义正确的集合：

term "Abs_int::(nat * nat) set => int"
term "Abs_int {(x,y). x + 3 = 2 + y}" (*(2,3)*)
term "Abs_int {(x,y). x + 4 = 3 + y}" (*(3,4)*)

lemma "Abs_int {(x,y). x + 3 = 2 + y} = Abs_int {(x,y). x + 100 = 99 + y}"
  by(auto)

这个auto证明很简单，但在下一个证明中对我来说没有什么神奇之处，尽管它很简单。

lemma "Abs_int {(x,y). x + 3 = 2 + y} + Abs_int {(x,y). x + 4 = 3 + y}
        = Abs_int {(x,y). x + 7 = 5 + y}"
apply(auto simp add: plus_int.abs_eq plus_int_def intrel_def)
oops

可能我需要做的就是利用默认情况下不是简单规则的东西。

如果quotient_type不是您正在谈论的“商类型模式”，那么至少通过查看上面find_theorems返回的所有内容，我从中得到了一些东西Int.plus_int*。

score 1 · Accepted Answer

什么是商类型？

商类型是一种根据现有类型定义新类型的方法。这样，我们就不必公理化新类型。例如，人们可能会发现使用自然数来构建整数是合理的，因为它们可以被视为“自然数+负数”。然后您可能想要使用整数来构建有理数，因为它们可以被视为“整数+商”。等等。

商类型使用“较低类型”上的给定等价关系来确定“较高类型”的相等含义。

更准确地说：商类型是一种抽象类型，其相等性由其基础表示上的某种等价关系决定。

这个定义一开始可能过于抽象，所以我们将使用整数作为基础示例。

示例：来自 Naturals 的整数

如果要定义整数，最标准的方法是使用有序的自然数对，例如 (a,b)，它直观地表示“ab”。例如，对 (2,4) 表示的数字是 -2，因为直观上 2-4 = -2。按照同样的逻辑，(0,2) 也表示“-2”，(1,3) 或 (10,12) 也是如此，因为 0-2 = 1-3 = 10-12 = -2。

然后我们可以说“两对 (a,b) 和 (x,y) 表示相同的整数当且仅当 a - b = x - y ”。但是，减法运算在自然数中可能很奇怪（自然数中的“2-3”是什么？）。为了避免这种奇怪，将'a - b = x - y'重写为'a + y = x + b'，现在只使用加法。因此，当 'a + y = x + b' 时，两对 (a,b) 和 (x,y) 表示相同的整数。例如，(7,9) 表示与 (1,3) 相同的整数，因为 '7 + 3 = 1 + 9'。

这导致了整数的商定义：整数是由一对有序自然数表示的类型。当且仅当 a+y = x+b 时，由 (a,b) 和 (x,y) 表示的两个整数相等。

整数类型派生自作为其表示的“有序自然数对”类型。我们可以称整数本身为它的抽象。整数的相等性被定义为只要一些基础表示“（a，b）”和“（x，y）”遵循等价关系“a+y = x+b”。

从这个意义上说，整数“-3”由“(0,3)”和“(2,5)”表示，我们可以通过注意到 0+5 = 3+2 来证明这一点。另一方面，'(0,3)' 和 '(6,10)' 不代表同一个整数，因为 '0+10 ≠ 3+6'。这反映了'-3≠-4'的事实。

从技术上讲，整数'-3'不是特指'(0,3)'，也不是'(1,4)'，也不是'(10,13)'，而是整个等价类。我的意思是'-3'是包含其所有表示的集合（即-3 = {（0,3），（1,4），（2,5），（3,6），（4， 7），...}）。'(0,3)' 被称为'-3'的表示，'-3' 是'(0,3)' 的抽象。

态射：Isabelle 中的Rep和Abs

Rep和Abs是我们在表示和它们所表示的抽象之间转换的方式。更准确地说，它们是从等价类到其表示之一的映射，反之亦然。我们称它们为态射。

Rep获取一个抽象对象（等价类），例如“-3”，并将其转换为它的一种表示形式，例如“(0,3)”。Abs则相反，采用诸如“(3,10)”之类的表示，并将其映射到其抽象对象，即“-7”。Int.thy（Isabelle 的整数实现）将这些定义为Rep_Integ和Abs_Integ用于整数。

请注意，陈述“ (2,3) = (8,9)”是荒谬的。由于这些是有序对，这意味着“2 = 8”和“3 = 9”。另一方面，陈述' Abs_Integ(2,3) = Abs_Integ(8,9)'非常正确，因为我们只是说'（2,3）'的整数抽象与整数抽象'（8,9）'相同，即'-1' .

' ' 的更精确的表述Abs_Integ(2,3) = Abs_Integ(8,9)是：“ '(2,3)' 和 '(8,9)' 在整数关系下属于同一个等价类”。我们通常称这个类为“-1”。

重要的是要注意，'-1' 只是“(0,1) 的等价类”的方便简写，同样，“5”只是“(5,0) 的等价类的简写” 和 '-15' 是“'(0,15)' 的等价类的简写。我们称 '(0,1)'、'(5,0)' 和 '(0,15) 为规范表示. 所以说“ Abs_Integ(2,3) = -1”实际上只是“”的一个很好的缩写Abs_Integ(2,3) = Abs_Integ(0,1)。

还值得注意的是，映射Rep是一对一的。这意味着Rep_Integ(-1)总是会产生相同的表示对，通常是规范的“（0,1）”。选择的特定对并不重要，但它总是会选择相同的。知道这一点很有用，因为它暗示该陈述Rep_Integ(i) = Rep_Integ(i)总是正确的。

`quotient_type`伊莎贝尔的命令

' quotient_type' 使用指定的类型和等价关系创建商类型。因此quotient_type int = "nat × nat" / "intrel"创建商类型，作为关系( )下int的等价类。手册的第 11.9.1 节详细介绍了有关该命令的细节。nat × natintrelwhere "intrel = (λ(a,b) (x,y). a+y = x+b)"

值得注意的是，您实际上必须证明提供的关系 ( intrel) 是等价的。

这是一个来自的用法示例Int.thy，它定义了整数，它是态射，并证明这intrel是一个等价关系：

(* Definition *)
quotient_type int = "nat × nat" / "intrel"
  morphisms Rep_Integ Abs_Integ
(* Proof that 'intrel' is indeed an equivalence *)
proof (rule equivpI)
  show "reflp intrel" by (auto simp: reflp_def)
  show "symp intrel" by (auto simp: symp_def)
  show "transp intrel" by (auto simp: transp_def)
qed

定义和引理：提升和转移包

现在，前面的解释表明Rep和Abs应该出现在任何地方，对吧？这些转换对于证明商类型的属性至关重要。但是，它们在 2000 行中出现的次数不到 10 次Int.thy。为什么？

lift_definition证明方法transfer就是答案。它们来自Lifting和Transfer包。这些包做了很多，但出于我们的目的，它们的作用是从您的定义和定理中隐藏Rep和Abs 。

在 Isabelle 中使用商类型时的要点是，您想要[1]定义一些操作，[2]用表示类型证明一些有用的引理，然后[3] 完全忘记这些表示，只使用抽象类型。在证明有关抽象类型的定理时，您应该使用前面显示的属性和引理。

要获得[1]，lift_definition可以帮助您定义操作。具体来说，它允许您使用表示类型定义函数，并自动将其“提升”为抽象类型。

例如，您可以这样定义整数的加法：

lift_definition int_plus:: "int ⇒ int ⇒ int"
  is "λ(a,b)(c,d). (a+c, b+d)"

这个定义是用来表示的nat × nat ⇒ nat × nat ⇒ nat × nat，但是 ' lift_definition' 会自动将它“提升”到int ⇒ int ⇒ int。

需要注意的重要一点是，您必须证明该函数在应用后仍然遵循等价关系（即 if 'x ≃ y' then 'fx ≃ f y'）。例如，上面的定义会提示你证明“如果'(a,b) ≃ (x,y)' and '(c,d) ≃ (u,v)', then '(a+c,b +d) ≃ (x+u,y+v)' " （如果看起来不像，请尝试使用apply clarify）。

关于它的lift_definition好处之一是它仅在底层表示方面起作用，因此您不必担心抽象和表示之间的转换。因此缺少Rep_Integ和Abs_Integ。Int.thy

它还transfer为函数设置了规则。这就是您获得[2]的方式：证明属性而不必担心Rep和Abs。使用transfer证明方法，您可以将关于抽象的引理带到表示级别，并在那里证明所需的属性。

例如，您可以在形式中声明加法的交换性int_plus x y = int_plus y x，然后使用该transfer方法将该语句降低到表示级别，在 a 之后clarify看起来像intrel (a + c, b + d) (c + a, d + b)。然后我们可以通过简化的定义来证明intrel：

lemma plus_comm: "int_plus x y = int_plus y x"
  apply transfer
  apply clarify
  by (simp add: intrel_def)

要获得[3]，您只需使用抽象类型的这些引理和属性，而不用担心实际的表示。

在此之后，您甚至会忘记您正在使用商类型，因为您只需要抽象类型及其属性。通常，抽象类型上的几个引理就足够了，而且Int.thy会给你带来的不仅仅是一把。

参考文献和进一步阅读

论文“商类型”的第 1 节很好地概述了该主题（并在其他部分中深入探讨）。
《Isabelle/HOL 商数重访》的介绍也很好地解释了' Rep '和' Abs '的目的。
“ Lifting and Transfer ”也是一本很好的读物，介绍了如何隐藏这些以及 Isabelle 中商类型背后的自动化。
当对特定命令的作用有疑问时， Isabelle 的参考手册（带有一些ctrl+f）也是一个很好的来源。

isabelle - Isabelle 中的商类型模式是什么？

2 回答 2