在有关Arend语言
的文章的第一部分中 ，我们研究了最简单的归纳类型，递归函数，类和集合。
2. Arend中的排序列表
2.1 Arend中的有序列表
我们将有序列表的类型定义为一对，由一个列表及其排序证明组成。 正如我们已经说过的，在Arend中，依赖对是使用
\Sigma关键字定义的。 通过与示例进行比较，我们得到了
Sorted类型的定义，灵感来自已经提到的
有关有序列表的文章中的定义
。 \func SortedList (O : LinearOrder.Dec) => \Sigma (l : List O) (Sorted l) \data Sorted {A : LinearOrder.Dec} (xs : List A) \elim xs | nil => nilSorted | :-: x nil => singletonSorted | :-: x1 (:-: x2 xs) => consSorted ((x1 = x2) || (x1 < x2)) (Sorted (x2 :-: xs))
注意：Arend能够自动推断
\Prop Universe中包含
Sorted类型。 发生这种情况是因为
Sorted定义中的所有三个模式都是互斥的，并且
consSorted构造函数具有两个参数，它们都属于
\Prop 。
让我们证明
Sorted谓词的一些显而易见的属性，说一个有序列表的尾部本身就是一个有序列表（此属性将来对我们很有用）。
\func tail-sorted {O : LinearOrder.Dec} (x : O) (xs : List O) (A : Sorted (x :-: xs)) : Sorted xs \elim xs, A | nil, _ => nilSorted | :-: _ _, consSorted _ xs-sorted => xs-sorted
在
tail-sorted我们同时在
xs列表和
Sorted谓词上使用了模式匹配，此外，我们使用了“ _”
跳过字符 ，它可以代替未使用的变量。
有人可能会问，在Arend中是否有可能证明有序列表的属性（如第1.3节所述），这是一个事实的示例，如果没有不重要的注释，就无法在Agda中证明这一事实。 回想一下，该属性声称要证明通过相关对定义的有序列表的相等性，足以检查对中第一个组成部分的相等性。
有人认为，由于上述
inProp构造和相关
SigmaExt对的可扩展性，在Arend中很容易获得此属性。
\func sorted-equality {A : LinearOrder.Dec} (l1 l2 : SortedList A) (P : l1.1 = l2.1) : l1 = l2 => SigmaPropExt Sorted l1 l2 P
SigmaPropExt属性在标准库的
Paths模块中得到证明，
HoTT书第二章
中的许多其他事实，包括
功能可扩展性 ，也得到了证明。
Arend中使用.n运算符来访问编号为n的sigma类型的投影仪（在我们的示例中，sigma类型为
SortedList A ，表达式
l1.1表示该类型的第一个组件是
List A类型的表达式）。
2.2实现“ be permutation”属性
现在，让我们尝试在Arend上实现列表排序功能。 自然，我们不希望有一个简单的排序算法实现，而是要有一个实现和一些特性的证明。
显然，此算法必须至少具有2个属性：
1.算法的结果应为有序列表。
2.结果列表应该是原始列表的排列。
首先，让我们尝试在Arend上实现列表的“ be permutation”属性。 为此，我们调整
从此处获取的Arend定义。
\truncated \data InsertSpec {A : \Set} (xs : List A) (a : A) (ys : List A) : \Prop \elim xs, ys | xs, :-: y ys => insertedHere (a = y) (xs = ys) | :-: x xs, :-: y ys => insertedThere (x = y) (InsertSpec xs a ys) \truncated \data Perm {A : \Set} (xs ys : List A) : \Prop | permInsert (xs' ys' : List A) (a : A) (Perm xs' ys') (InsertSpec xs' a xs) (InsertSpec ys' a ys) | permTrivial (xs = ys)
我们引入的
InsertSpec谓词具有以下直观含义：
InsertSpec xs a ys恰好意味着列表
ys是将元素a插入列表
xs （在任何位置）的结果。 因此，
InsertSpec可以用作插入函数的规范。
显然，
Perm数据类型确实定义了“ be permutation”关系：
permInsert构造函数精确地指出，如果通过将
xs和
ys插入到一些列表
xs'和
ys'来获得
xs和
ys ，则
xs和
ys是可以相互置换的。较短的长度，这已经是彼此的排列。
对于我们对“ be permutation”属性的定义，很容易验证对称性。
\func Perm-symmetric {A : \Set} {xs ys : List A} (P : Perm xs ys) : Perm ys xs \elim P | permTrivial xs=ys => permTrivial (inv xs=ys) | permInsert perm-xs'-ys' xs-spec ys-spec => permInsert (Perm-symmetric perm-xs'-ys') ys-spec xs-spec
Perm也满足传递性属性，但其验证要复杂得多。 由于此属性在排序算法的实现中不起作用，因此我们将其留给读者作为练习。
\func Perm-transitive {A : \Set} (xs ys zs : List A) (P1 : Perm xs ys) (P2 : Perm ys zs) : Perm xs zs => {?}
2.3与样品相比同态水平的变化
现在，让我们尝试实现一个将元素插入到有序列表中的函数，以使结果列表保持有序。 让我们从以下简单的实现开始。
\func insert {O : LinearOrder.Dec} (xs : List O) (y : O) : List O \elim xs | nil => y :-: nil | :-: x xs' => \case LinearOrder.trichotomy xy \with { | byLeft x=y => x :-: insert xs' y | byRight (byLeft x<y) => x :-: insert xs' y | byRight (byRight y<x) => y :-: x :-: xs' }
\case构造允许与任意表达式的样本匹配（
\elim只能在函数定义的最高级别及其参数使用）。 如果您要求Arend检查
insert类型，将显示以下错误消息。
[ERROR] Data type '||' is truncated to the universe \Prop which does not fit in the universe of the eliminator type: List OE In: | byLeft x-leq-y => x :-: insert xs' y While processing: insert
问题在于，在
LinearOrder.Dec类中
LinearOrder.Dec使用
||运算符给出了
trichotomy LinearOrder.Dec定义 ，而后者是使用命题截断法确定的。 如前所述，对于属于
\Prop Universe的类型，仅当结果表达式的类型本身是断言时才允许与Arend中的模式匹配（对于上面的函数，结果的类型为
List OE且此类型为集合）。
有什么办法可以解决这个问题？ 解决此问题的最简单方法是更改三分法属性的定义。 考虑以下三分法的定义，使用非截断类型
Or代替截断的
|| ：
\func set-trichotomy {A : StrictPoset} (xy : A) => ((x = y) `Or` (x < y)) `Or` (y < x)
此定义
trichotomy通过
||通过原始
trichotomy定义
trichotomy什么
trichotomy吗？ ？ 如果仅使命题复杂化并阻止我们使用模式匹配，为什么还要使用命题截断类型呢？
首先，让我们尝试回答第一个问题：对于严格的
StrictPoset订单
StrictPoset trichotomy和
set-trichotomy之间
StrictPoset区别实际上根本没有。 请注意，
set-trichotomy类型是一个语句。 此事实来自以下事实：由于顺序公理，三分法定义中的所有三个替代方案都是互斥的，并且三种类型
x = y, x < y, y < x本身都是一个语句（
x = y是一个语句，所以就像在
BaseSet类的定义中
BaseSet我们要求将媒体
E集合！）。
\func set-trichotomy-isProp {A : StrictPoset} (xy : A) (l1 l2 : set-trichotomy xy): l1 = l2 \elim l1, l2 | inl (inl l1), inl (inl l2) => pmap (\lam z => inl (inl z)) (Path.inProp l1 l2) | inl (inr l1), inl (inr l2) => pmap (\lam z => inl (inr z)) (Path.inProp l1 l2) | inr l1, inr l2 => pmap inr (Path.inProp l1 l2) | inl (inl l1), inl (inr l2) => absurd (lt-eq-false l1 l2) | inl (inr l1), inl (inl l2) => absurd (lt-eq-false l2 l1) | inl (inl l1), inr l2 => absurd (lt-eq-false (inv l1) l2) | inr l1, inl (inl l2) => absurd (lt-eq-false (inv l2) l1) | inl (inr l1), inr l2 => absurd (lt-lt-false l1 l2) | inr l1, inl (inr l2) => absurd (lt-lt-false l2 l1) \where { \func lt-eq-false {A : StrictPoset} {xy : A} (l1 : x = y) (l2 : x < y) : Empty => A.<-irreflexive x (transport (x <) (inv l1) l2) \func lt-lt-false {A : StrictPoset} {xy : A} (l1 : x < y) (l2 : y < x) : Empty => A.<-irreflexive x (A.<-transitive _ _ _ l1 l2) }
在上面的清单中，
absurd是ex quodlibet原则的名称，该原则在
Logic模块中定义。 由于
Empty类型的定义中没有构造函数（请参见第1.2节），因此无需在
absurd的定义中进行个案研究：
\func absurd {A : \Type} (x : Empty) : A
由于我们现在知道
set-trichotomy是一条语句，因此我们可以从可判定订单的常规
trichotomy属性中得出
set-trichotomy属性。 为此，我们可以使用
\return \level构造，该构造告诉Arend计时器在这一点上模式匹配是允许的操作（在这种情况下，我们必须证明
set-trichotomy-property函数的结果是一条语句）。
\func set-trichotomy-property {A : LinearOrder.Dec} (xy : A) : set-trichotomy xy => \case A.trichotomy xy \return \level (set-trichotomy xy) (set-trichotomy-isProp xy) \with { | byLeft x=y => inl (inl x=y) | byRight (byLeft x<y) => inl (inr x<y) | byRight (byRight y<x) => inr (y<x) }
现在让我们尝试回答第二个问题，即为什么在公式化数学对象的属性时，最好不使用普通的，命题截断的结构。 为此，请考虑一下非线性线性订单定义的
TotalOrder可以在
LinearOrder模块中找到
Lattice和
TotalOrder完整定义）：
\class TotalOrder \extends Lattice { | totality (xy : E) : x <= y || y <= x }
现在让我们想象一下，如果我们通过未截断的
Or构造编写了totality字段的定义，
TotalOrder类的含义将如何改变。
\class BadTotalOrder \extends Lattice { | badTotality (xy : E) : (x <= y) `Or` (y <= x) }
在这种情况下，类型
(x <= y) `Or` (y <= x)不再是语句，因为 如果
x和
y值相等
y则可以执行
badTotality定义中的两种选择，并且
badTotality证明中的左分支或右分支的选择绝对
badTotality任意的，并且由用户自行决定-没有理由偏向于一个
Or一个构造函数。
现在，很清楚
TotalOrder和
BadTotalOrder之间的区别
BadTotalOrder 。 两个有序集合
O1 O2 ：
TotalOrder在可以证明集合
O1.E, O2.E和订单
O1.<, O2.<相等的情况下总是相等的（这是所需的属性）。 另一方面，对于
O1 O2 ：
BadTotalOrder只有当除了
E所有元素
x都
x O1.badTotality xx和
O2.badTotality xx时，才有
BadTotalOrder证明
O1和
O2相等。
因此，事实证明，类
BadTotalOrder直观上不需要被视为“线性有序集”，而应被视为“线性有序集以及
E左或右分支
x字段
E每个元素
x的选择，
Or在
badTotality xx的实现中”。
2.4排序算法
现在，我们继续实现排序算法。 让我们尝试使用久经考验的
set-trichotomy-property修复上一部分中
insert函数的简单实现（在这种情况下，由于
set-trichotomy定义中括号的更成功排列，我们减少了考虑的案例数）。
\func insert {O : LinearOrder.Dec} (xs : List O) (y : O) : List O \elim xs | nil => y :-: nil | :-: x xs' => \case set-trichotomy-property xy \with { | inr y<x => y :-: x :-: xs' | inl x<=y => x :-: insert xs' y }
现在，让我们尝试为有序列表实现一个类似的定义。 我们将
\let … \in构造中使用特殊的
\let … \in ，这允许我们向上下文添加新的局部变量。
\func insert {O : LinearOrder.Dec} (xs : SortedList O) (y : O) : SortedList O \elim xs | (nil, _) => (y :-: nil, singletonSorted) | (:-: x xs', xs-sorted) => \case set-trichotomy-property xy \with { | inr y<x => (y :-: x :-: xs', consSorted (byRight y<x) xs-sorted) | inl x<=y => \let (result, result-sorted) => insert (xs', tail-sorted x xs' xs-sorted) y \in (x :-: result, {?})
我们在证明中留下了一个不完整的片段（由表达式
{?} ），在要显示列表
x :-: result 。 尽管在上下文中有证据表明
result列表是有序的，但是我们仍然需要验证
x是否不超过
result列表的第一个元素的值，这在上下文中从前提中很难遵循（要查看当前目标中的所有前提，这就是我们所说的）当前的计算分支-您需要从
insert函数请求类型检查。
事实证明，如果我们与
insert规范的证明并行地证明结果列表的顺序，
insert将更容易实现。 在最简单的情况下，请更改
insert的签名并写上此规范的证明：
\func insert {O : LinearOrder.Dec} (xs : SortedList O) (y : O) : \Sigma (ys : SortedList O) (InsertSpec xs.1 y ys.1) \elim xs | (nil, _) => ((y :-: nil, singletonSorted), insertedHere idp idp) | (:-: x xs', xs-sorted) => \case set-trichotomy-property xy \with { | inr y<x => ((y :-: x :-: xs', consSorted (byRight y<x) xs-sorted), insertedHere idp idp) | inl x<=y => \let ((result, result-sorted), result-spec) => insert (xs', tail-sorted x xs' xs-sorted) y \in ((x :-: result, {?}), insertedThere idp result-spec)
对于没有证据的单个片段，Arend将输出以下上下文值：
Expected type: Sorted (x :-: (insert (\this, tail-sorted x \this \this) \this).1.1) Context: result-sorted : Sorted (insert (\this, tail-sorted \this \this \this) \this).1.1 xs-sorted : Sorted (x :-: xs') x : O x<=y : Or (x = y) (O.< xy) O : Dec result : List O y : O xs' : List O result-spec : InsertSpec xs' y (insert (xs', tail-sorted \this xs' \this) y).1.1
为了完成证明，我们将不得不使用
\case运算符
的全部功能 ：我们将使用具有5个不同变量的模式匹配，并且由于某些变量的类型可能取决于其他变量的值，因此我们将使用从属模式匹配。
冒号的结构明确表明要比较的某些变量的类型如何取决于其他变量的值（因此，在每种
\case ，在
xs-sorted, result-spec和
result-sorted的变量类型中
xs-sorted, result-spec而不是
xs'和
result将与相应的样本匹配）。
\return构造将用于匹配模式的变量与预期结果的类型相关联。 换句话说，在当前目标中，在每个
\case子句中，相应的样本将替换为
result变量。 没有这种构造，就不会进行这种替换，并且所有
\case子句的目标都将与目标相同，而不是
\case expression本身。
\func insert {O : LinearOrder.Dec} (xs : SortedList O) (y : O) : \Sigma (ys : SortedList O) (InsertSpec xs.1 y ys.1) \elim xs | (nil, _) => ((y :-: nil, singletonSorted), insertedHere idp idp) | (:-: x xs', xs-sorted) => \case set-trichotomy-property xy \with { | inr y<x => ((y :-: x :-: xs', consSorted (byRight y<x) xs-sorted), insertedHere idp idp) | inl x<=y => \let ((result, result-sorted), result-spec) => insert (xs', tail-sorted x xs' xs-sorted) y \in ((x :-: result, \case result \as result, xs' \as xs', xs-sorted : Sorted (x :-: xs'), result-spec : InsertSpec xs' y result, result-sorted : Sorted result \return Sorted (x :-: result) \with { | nil, _, _, _, _ => singletonSorted | :-: r rs, _, _, insertedHere y=r _, result-sorted => consSorted (transport (\lam z => (x = z) || (x < z)) y=r (Or-to-|| x<=y)) result-sorted | :-: r rs, :-: x' _, consSorted x<=x' _, insertedThere x2=r _, result-sorted => consSorted (transport (\lam z => (x = z) || (x < z)) x2=r x<=x') result-sorted }), insertedThere idp result-spec)
在上面的代码块中，模式比较的最后两段中
consSorted构造函数的复杂的第一个参数值得附加注释。 要理解这两个表达式的含义，我们将它们替换为表达式
{?}并要求Arend计时器确定两个位置的目标。
您可以看到当前目标在那里和那里都是类型
(x = r) || O.< xr (x = r) || O.< xr 。 此外，在第一个目标的背景下，有前提
x<=y : Or (x = y) (O.< xy) y=r : y = r
在第二个前提下
x<=x' : (x = x') || O.< xx' x2=r : x' = r.
直观直观：要证明第一个目标，只需将变量
r替换为正确的语句
Or (x = y) (O.< xy) ，然后切换到命题截断类型
||就足够了
Or (x = y) (O.< xy) 使用第1.3节中定义
Or-to-||函数 。 为了证明第二个目标，只需替换为
(x = x') || O.< x x' (x = x') || O.< x x'而不是变量
r x'变量
r 。
为了形式化描述的表达式替换操作，标准Arend库中存在一个特殊的
transport函数。 考虑她的签名：
\func transport {A : \Type} (B : A -> \Type) {aa' : A} (p : a = a') (b : B a) : B a'
在我们的例子中，我们需要替换类型
OE （如果指定了其他
transport参数，则可以显式省略），而不是变量
A而不是
B ，表达式
\lam (z : O) => (x = z) || (x < z) \lam (z : O) => (x = z) || (x < z) 。
插入排序算法及其规范的实现不再引起任何特殊的困难：为了对列表
x :-: xs'排序，我们首先使用对
insertSort的递归调用对列表
xs'的尾部进行排序，然后将
x元素插入此列表中，同时保留顺序。帮助访问已经实现的
insert功能。
\func insertSort {O : LinearOrder.Dec} (xs : List O) : \Sigma (result : SortedList O) (Perm xs result.1) \elim xs | nil => ((nil, nilSorted), permTrivial idp) | :-: x xs' => \let | (ys, perm-xs'-ys) => insertSort xs' | (zs, zs-spec) => insert ys x \in (zs, permInsert perm-xs'-ys (insertedHere idp idp) zs-spec)
我们实现了最初的目标，并在Arend上对列表进行了排序。 可以
从此处在一个文件中下载本段给出的整个Arend代码。
有人可能会问，如果我们使用非严格的
TotalOrder订单代替严格的
LinearOrder.Dec订单，那么
insert如何更改
insert函数的实现？ 我们记得，在总计函数的定义中，使用了截断运算
|| 是非常重要的，也就是说，该定义不等于用
||代替的定义。 由
Or 。
这个问题的答案如下：仍然可以为
TotalOrder构建一个
insert类似物，但是为此，我们必须证明
insert函数的类型是一个语句（这将使我们在
insert的定义中可以根据
totality xy语句与样本进行比较）。
换句话说，我们将不得不证明只有一个有序列表才能达到相等，这是将元素
y插入有序列表
xs 。 显而易见，这是一个真实的事实，但是其正式证明不再那么琐碎。 我们将对此事实的验证留给有兴趣的读者练习。
3.结论性意见
在本简介中，我们熟悉了Arend语言的主要结构，并学习了如何使用类机制。 我们设法实现了最简单的算法及其规范的证明。 因此，我们表明Arend非常适合解决“日常”问题，例如程序验证。
我们没有提到Arend的所有功能。 例如，对于
带有条件的类型 ，我们几乎一言不发
，这些条件允许您将各种类型的构造函数“粘合”到这些构造函数的某些特殊参数值中。 例如，使用条件如下的类型给出Arend中整数类型的实现：
\data Int | pos Nat | neg Nat \with { zero => pos zero }
该定义表示整数由自然数类型的两个副本组成，其中标识了“正”和“负”零。 这样的定义比标准Coq库中的定义要方便得多，在标准Coq库中，自然数的“负副本”必须“移动一个”，以使这些副本不相交（当
neg 1表示-1而不是-2时更方便）。 。
我们没有说关于在类及其实例中推导谓词和同伦水平的算法。 我们几乎也没有提到间隔
I的类型，尽管它在间隔类型的理论中起着关键作用，间隔是Arend的逻辑基础。 要了解这种类型的重要性，只需提及Arend类型中的间隔是通过间隔的概念来定义的。 , , , (.. ).
:
,
HoTT JetBrains Research.