Arend - HoTT-based dependent type language (part 2)
In the first part of the article about the Arend language, we examined the simplest inductive types, recursive functions, classes and sets.
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
keyword. We will determine the type of
by comparing with the sample, inspired by the definition from the already mentioned article about ordered lists.
Note: Arend was able to automatically infer that the
type is contained in the
universe. This happened because all three patterns in the
definition are mutually exclusive, and the
constructor has two parameters, both of which belong to
.
Let us prove some obvious property of the
predicate, say that the tail of an ordered list is itself an ordered list (this property will be useful to us in the future).
In the
we used pattern matching on the
list and the
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
construction already mentioned above and the extensionality property for dependent
pairs.
The
property
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
operator
used in Arend to access the sigma type projector with number n (in our case, the sigma type is
, and the expression
means the first component of this type is an expression of type
).
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.
The
predicate introduced by us has the following intuitive meaning:
exactly means that the list
is the result of inserting the element a inside the list
(at any position). Thus,
can be taken as a specification of the insert function.
Clearly, the
data type really defines the “be permutation” relationship: the
constructor
exactly that
and
are mutually permutable if
and
are obtained by inserting the same element a into some lists
and
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.
The transitivity property is also fulfilled for
, 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.
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.
The
construction allows matching with a sample of an arbitrary expression (
can be used only at the highest level of a function definition and only for its parameters). If you ask Arend to check the
type, the following error message will be displayed.
The problem is that in the
class
definition of
given using the
operator , which, in turn, is determined using propositional truncation. As already mentioned, for types belonging to the
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
, 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
instead of the truncated
:
Does this definition
in anything from the original
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
orders
difference between
and
is actually not at all. Note that the
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
is itself a statement (
is a statement, so as in the definition of the
class
we demanded that the media
a set!).
In the listing above,
is the designation for the ex falso quodlibet principle, which is defined in the Logic module. Since the
type does not have constructors in the definition (see section 1.2), it is not necessary to go through cases in the definition of
:
Since we now know that
is a statement, we can derive the
property from the usual
property of decidable orders. To do this, we can use the
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
function is a statement).
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
and
can be found in the LinearOrder module):
Now let's try to
how the meaning of the
class would have changed if we had written the definition of the totality field through the un-truncated
construction.
In this case, the type
no longer a statement, because in case of equal values of
and
both alternatives in the definition of
can be implemented, and the choice of the left or right branch in the proof of
absolutely arbitrary and remains at the discretion of the user - there is no reason to prefer one
constructor to another.
Now it’s clear what the difference between
and
. Two ordered sets
:
are always equal when it is possible to prove the equality of the sets
and the orders
Given on them (this is the desired property). On the other hand, for
:
it is
to prove the equality of
and
only in cases where, in addition to all elements
from
equality
and
.
Thus, it turns out that the class
intuitively needs to be considered not as a “linearly ordered set”, but as a “linearly ordered set together with the choice for each element
field
left or right branch
in the implementation of
".
We now proceed to implement the sorting algorithm. Let's try to fix the naive implementation of the
function from the previous section using the proved
(in this case, due to the more successful arrangement of brackets in the definition of
, we have reduced the number of cases considered).
Let us now try to implement an analog of this definition for ordered lists. We will use the special
construct, which allows us to add new local variables to the context.
We left an incomplete fragment in the proof (indicated by the expression
) In the place where we need to show that the list
ordered. Although in the context there is evidence of the ordering of the
list, it remains for us to verify that
does not exceed the value of the first element of the
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
function).
It turns out that
much easier to implement if we prove the ordering of the resulting list in parallel with the proof of the
specification. Change the signature of
and write proof of this specification in the simplest cases:
For a single fragment left without proof, Arend will output the following context value:
To complete the proof, we will have to use the power of the
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
and
in each of
instead of
and
will match the corresponding samples).
The
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
clauses, the corresponding sample will be substituted for the
variable. Without this construction, such a replacement would not be carried out, and the goal of all the
clauses would coincide with the goal in place of the
expression itself.
In the above block of code, the complicated first arguments to the
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
. Moreover, in the context of the first goal, there are premises
and in the context of the second - premises
Intuitively clear: to prove the first goal, it is enough to substitute the variable
into the correct statement
instead of the y variable, and then switch to the propositionally truncated type
using the
function defined in Section 1.3 . To prove the second goal, just substitute in
instead of the variable
variable
.
To formalize the described expression substitution operation, a special
function exists in the standard Arend library. Consider her signature:
In our case, instead of the variable
we need to substitute the type
(it can be omitted explicitly if the other
arguments are specified), and instead of
, the expression
.
Implementation of the insertion sorting algorithm together with the specification does not cause any special difficulties: in order to sort the list
, we first sort the tail of the list
using a recursive call to
, and then insert the element
inside this list with preserving the order for help access to the already implemented
function.
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
function if instead of the strict
orders we used the non-strict
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
.
The answer to this question is as follows: it is still possible to build an
analogue for
, however, for this we would have to prove that the type of the
function is a statement (this would allow us in the definition of
to make a comparison with the sample according to the
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
into the ordered list
. 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.
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:
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
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
, 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.
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.
All Articles