In the first part of the article about the Arend language, we examined the simplest inductive types, recursive functions, classes and sets.
2. Sorting Lists in Arend
2.1 Ordered Lists in Arend
We define the type of ordered lists as a pair consisting of a list and proof of its ordering. As we said before, in Arend, dependent pairs are defined using the
\Sigma keyword. We will determine the type of
Sorted by comparing with the sample, inspired by the definition from the already mentioned
article about ordered lists. \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))
Note: Arend was able to automatically infer that the
Sorted type is contained in the
\Prop universe. This happened because all three patterns in the
Sorted definition are mutually exclusive, and the
consSorted constructor has two parameters, both of which belong to
\Prop .
Let us prove some obvious property of the
Sorted predicate, say that the tail of an ordered list is itself an ordered list (this property will be useful to us in the future).
\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
In the
tail-sorted we used pattern matching on the
xs list and the
Sorted predicate at the same time, in addition, we used
the skip symbol “_”, which can be substituted for unused variables.
One may ask if it is possible in Arend to prove the property of ordered lists, mentioned in section 1.3 as an example of a fact that cannot be proved in Agda without annotations of immateriality. Recall that this property states that to prove the equality of ordered lists defined through dependent pairs, it is sufficient to verify the equality of the first components of the pairs.
It is argued that in Arend this property is easily obtained as a consequence of the
inProp construction already mentioned above and the extensionality property for dependent
SigmaExt pairs.
\func sorted-equality {A : LinearOrder.Dec} (l1 l2 : SortedList A) (P : l1.1 = l2.1) : l1 = l2 => SigmaPropExt Sorted l1 l2 P
The
SigmaPropExt property
SigmaPropExt proved in the
Paths module of the standard library, and many other facts from the second chapter
of the HoTT book , including the
property of functional extensionality , are also proved there.
The
.n operator
.n used in Arend to access the sigma type projector with number n (in our case, the sigma type is
SortedList A , and the expression
l1.1 means the first component of this type is an expression of type
List A ).
2.2 Implementation of the “be permutation” property
Now let's try to implement the list sorting function on Arend. Naturally, we want to have not a simple implementation of the sorting algorithm, but an implementation together with a proof of some properties.
Clearly, this algorithm must have at least 2 properties:
1. The result of the algorithm should be an ordered list.
2. The resulting list should be a permutation of the original list.
First, let’s try to implement the “be permutation” property of lists on Arend. To do this, we adapt the definition taken
from here for 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)
The
InsertSpec predicate introduced by us has the following intuitive meaning:
InsertSpec xs a ys exactly means that the list
ys is the result of inserting the element a inside the list
xs (at any position). Thus,
InsertSpec can be taken as a specification of the insert function.
Clearly, the
Perm data type really defines the “be permutation” relationship: the
permInsert constructor
permInsert exactly that
xs and
ys are mutually permutable if
xs and
ys are obtained by inserting the same element a into some lists
xs' and
ys' shorter lengths, which are already permutations of each other.
For our definition of the “be permutation” property, it is easy to verify the symmetry property.
\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
The transitivity property is also fulfilled for
Perm , however, its verification is much more complicated. Since this property does not play any role in the implementation of our sorting algorithm, we leave it to the reader as an exercise.
\func Perm-transitive {A : \Set} (xs ys zs : List A) (P1 : Perm xs ys) (P2 : Perm ys zs) : Perm xs zs => {?}
2.3 Change in homotopy levels when compared with the sample
Now let's try to implement a function that inserts an element into an ordered list so that the resulting list remains ordered. Let's start with the following naive implementation.
\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' }
The
\case construction allows matching with a sample of an arbitrary expression (
\elim can be used only at the highest level of a function definition and only for its parameters). If you ask Arend to check the
insert type, the following error message will be displayed.
[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
The problem is that in the
LinearOrder.Dec class
LinearOrder.Dec definition of
trichotomy given using the
|| operator , which, in turn, is determined using propositional truncation. As already mentioned, for types belonging to the
\Prop universe, matching with a pattern in Arend is allowed only if the type of the resulting expression is itself an assertion (for the function above, the result is of type
List OE , and this type is a set).
Is there any way around this problem? The easiest way to solve this is to change the definition of the property of trichotomy. Consider the following definition of trichotomy, using the un-truncated type
Or instead of the truncated
|| :
\func set-trichotomy {A : StrictPoset} (xy : A) => ((x = y) `Or` (x < y)) `Or` (y < x)
Does this definition
trichotomy in anything from the original
trichotomy definition through
|| ? Why did we even use a propositionally truncated type if it only complicates our life and prevents us from using pattern matching?
Let's try to answer the first question for a start: for strict
StrictPoset orders
StrictPoset difference between
trichotomy and
set-trichotomy is actually not at all. Note that the
set-trichotomy type is a statement. This fact follows from the fact that all three alternatives in the definition of trichotomy are mutually exclusive due to axioms of order, and each of the three types
x = y, x < y, y < x is itself a statement (
x = y is a statement, so as in the definition of the
BaseSet class
BaseSet we demanded that the media
E a set!).
\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) }
In the listing above,
absurd is the designation for the ex falso quodlibet principle, which is defined in the
Logic module. Since the
Empty type does not have constructors in the definition (see section 1.2), it is not necessary to go through cases in the definition of
absurd :
\func absurd {A : \Type} (x : Empty) : A
Since we now know that
set-trichotomy is a statement, we can derive the
set-trichotomy property from the usual
trichotomy property of decidable orders. To do this, we can use the
\return \level construction, which tells the Arend timer that at this point the pattern matching is a permitted operation (we have to show proof that the result of the
set-trichotomy-property function is a statement).
\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) }
Let us now try to answer the second question, namely, why, when formulating the properties of mathematical objects, it is preferable to use not ordinary, but propositionally truncated constructions. Consider for this a fragment of the definition of non-strict linear orders (full definitions of
Lattice and
TotalOrder can be found in the
LinearOrder module):
\class TotalOrder \extends Lattice { | totality (xy : E) : x <= y || y <= x }
Now let's try to
TotalOrder how the meaning of the
TotalOrder class would have changed if we had written the definition of the totality field through the un-truncated
Or construction.
\class BadTotalOrder \extends Lattice { | badTotality (xy : E) : (x <= y) `Or` (y <= x) }
In this case, the type
(x <= y) `Or` (y <= x) no longer a statement, because in case of equal values of
x and
y both alternatives in the definition of
badTotality can be implemented, and the choice of the left or right branch in the proof of
badTotality absolutely arbitrary and remains at the discretion of the user - there is no reason to prefer one
Or constructor to another.
Now it’s clear what the difference between
TotalOrder and
BadTotalOrder . Two ordered sets
O1 O2 :
TotalOrder are always equal when it is possible to prove the equality of the sets
O1.E, O2.E and the orders
O1.<, O2.< Given on them (this is the desired property). On the other hand, for
O1 O2 :
BadTotalOrder it is
BadTotalOrder to prove the equality of
O1 and
O2 only in cases where, in addition to all elements
x from
E equality
O1.badTotality xx and
O2.badTotality xx .
Thus, it turns out that the class
BadTotalOrder intuitively needs to be considered not as a “linearly ordered set”, but as a “linearly ordered set together with the choice for each element
x field
E left or right branch
Or in the implementation of
badTotality xx ".
2.4 Sort Algorithm
We now proceed to implement the sorting algorithm. Let's try to fix the naive implementation of the
insert function from the previous section using the proved
set-trichotomy-property (in this case, due to the more successful arrangement of brackets in the definition of
set-trichotomy , we have reduced the number of cases considered).
\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 us now try to implement an analog of this definition for ordered lists. We will use the special
\let … \in construct, which allows us to add new local variables to the context.
\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, {?})
We left an incomplete fragment in the proof (indicated by the expression
{?} ) In the place where we need to show that the list
x :-: result ordered. Although in the context there is evidence of the ordering of the
result list, it remains for us to verify that
x does not exceed the value of the first element of the
result list, which is not so easy to follow from the premises in the context (to see all the premises in the current target - this is what we call present branch of calculations - you need to request type checking from the
insert function).
It turns out that
insert much easier to implement if we prove the ordering of the resulting list in parallel with the proof of the
insert specification. Change the signature of
insert and write proof of this specification in the simplest cases:
\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)
For a single fragment left without proof, Arend will output the following context value:
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
To complete the proof, we will have to use the
power of the
\case operator
to the full extent: we will use pattern matching with 5 different variables, and since the types of some variables may depend on the values of other variables, we will use dependent pattern matching.
The colon construction explicitly indicates how the type of some variables to be compared depends on the values of other variables (thus, in the type of variables
xs-sorted, result-spec and
result-sorted in each of
\case instead of
xs' and
result will match the corresponding samples).
The
\return construct associates the variables used to match the pattern with the type of expected result. In other words, for the current target, in each of the
\case clauses, the corresponding sample will be substituted for the
result variable. Without this construction, such a replacement would not be carried out, and the goal of all the
\case clauses would coincide with the goal in place of the
\case expression itself.
\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)
In the above block of code, the complicated first arguments to the
consSorted constructor in the last two paragraphs of pattern matching deserve additional comment. To understand what both of these expressions mean, we replace them with the expression
{?} And ask the Arend timer for determining targets at both positions.
You can see that both there and there the current target is the type
(x = r) || O.< xr (x = r) || O.< xr . Moreover, in the context of the first goal, there are premises
x<=y : Or (x = y) (O.< xy) y=r : y = r
and in the context of the second - premises
x<=x' : (x = x') || O.< xx' x2=r : x' = r.
Intuitively clear: to prove the first goal, it is enough to substitute the variable
r into the correct statement
Or (x = y) (O.< xy) instead of the y variable, and then switch to the propositionally truncated type
|| using the
Or-to-|| function defined in Section 1.3 . To prove the second goal, just substitute in
(x = x') || O.< x x' (x = x') || O.< x x' instead of the variable
x' variable
r .
To formalize the described expression substitution operation, a special
transport function exists in the standard Arend library. Consider her signature:
\func transport {A : \Type} (B : A -> \Type) {aa' : A} (p : a = a') (b : B a) : B a'
In our case, instead of the variable
A we need to substitute the type
OE (it can be omitted explicitly if the other
transport arguments are specified), and instead of
B , the expression
\lam (z : O) => (x = z) || (x < z) \lam (z : O) => (x = z) || (x < z) .
Implementation of the insertion sorting algorithm together with the specification does not cause any special difficulties: in order to sort the list
x :-: xs' , we first sort the tail of the list
xs' using a recursive call to
insertSort , and then insert the element
x inside this list with preserving the order for help access to the already implemented
insert function.
\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)
We fulfilled the original goal and implemented sorting lists on Arend. The entire Arend code given in this section can be downloaded in one file
from here .
One might ask how one would have to change the implementation of the
insert function if instead of the strict
LinearOrder.Dec orders we used the non-strict
TotalOrder orders? As we recall, in the definition of the totality function, the use of the truncated operation
|| was quite significant, that is, this definition is not equivalent to a definition in which instead of
|| used by
Or .
The answer to this question is as follows: it is still possible to build an
insert analogue for
TotalOrder , however, for this we would have to prove that the type of the
insert function is a statement (this would allow us in the definition of
insert to make a comparison with the sample according to the
totality xy statement).
In other words, we would have to prove that there is only one ordered list, up to equality, which is the result of inserting the element
y into the ordered list
xs . It is easy to see that this is a true fact, but its formal proof is no longer so trivial. We leave verification of this fact as an exercise for the interested reader.
3. Concluding observations
In this introduction, we got acquainted with the main constructs of the Arend language, and also learned how to use the class mechanism. We managed to implement the simplest algorithm along with the proof of its specification. Thus, we have shown that Arend is quite suitable for solving "everyday" problems, such as, for example, program verification.
We have mentioned not all Arend features and features. For example, we said almost nothing about
types with conditions that allow you to “glue” various type constructors with some special parameter values for these constructors. For example, an implementation of the integer type in Arend is given using types with conditions as follows:
\data Int | pos Nat | neg Nat \with { zero => pos zero }
This definition says that integers consist of two copies of the type of natural numbers, in which "positive" and "negative" zeros are identified. Such a definition is much more convenient than the definition from the standard Coq library, where the “negative copy” of natural numbers has to be “shifted by one” so that these copies do not intersect (it is much more convenient when
neg 1 notation stands for -1, not -2) .
We did not say anything about the algorithm for deriving predicative and homotopy levels of classes and their instances. We also hardly mentioned the type of interval
I , although it plays a key role in the theory of types with an interval, which are the logical basis of Arend. To understand how important this type is, it’s enough to mention that in Arend type equality is defined through the concept of an interval.
Comparison with the sample in a variable having the type of interval is carried out according to rather specific rules, which we also did not say anything about in this article (the so-called homotopy comparison with the sample).Posted by Sergey Sinchuk , Senior Researcher , HoTT and Dependent Types at JetBrains Research.