Verified QuickSort on Agda
Good day, dear habrauzer!
Having read several books on typed lambda calculus, namely on dependent types, I saw an interesting pattern: everywhere the first example is the definition of the βsorted listβ type. Everything would be fine, but there was nothing beyond this definition. So I thought up to fill this gap and implement a function that accepts the list, and returns another list and two proofs. One proves that the result is a permutation of the input, and the other proves that the result is a sorted list.
')
In this section, I will provide the basic types that will be used further, and some auxiliary functions. Also here will be shown some interesting syntactic charms of Agda. For those who are not very familiar with Agda, I recommend watching the video / slides of Jan Malakhovsky at the SPbHUG / FProg 2012-07 meeting - in my opinion, this is the only introduction to Agda in Russian (well, I havenβt met again). Or browse through the manual from the Agda site (it is not large) or this tutorial .
Here we have a list. The definition is taken from the standard library. As you can see, the elements of the list can be values ββof any type, even types and types of types and so on. This is possible due to the use of high-order polymorphism: the parameter a is introduced, which is responsible for the level, that is, the usual types are of type Set 0 , Set 0 is of type Set 1 , etc.
Also in this definition you can see how in Agda operators are declared, namely through underscores, in which place there will be arguments. It should be noted that this method allows you to define very different and very interesting forms, such as a function that returns a list from a single element [_] .
It should be noted that for all operators (combinators with underscores) you can specify the priority and associativity. Also in Agda, any Unicode sequence without spaces and brackets (round and curly) is a term.
You should also pay attention to the parentheses and curly braces: curly brackets in the type indication say that this argument is implicit and will be output by the compiler.
This definition of the predicate is "sorted list". Designers should be considered as axioms. We have axioms nil and one which say that the empty list and the list with one element are sorted. We also see that the Sorted type depends on the predicate _β€_ , which is responsible for the order β something like the comparison function, but dependently type (the arguments are values ββof the usual type, and the result is some type whose value is proof). Axiom two says the following: if we have evidence that x β€ y ( x β€ y is a type, and a value of type x β€ y is proof that x β€ y . See the Curry-Howard isomorphism ), and proof that some list with head y is sorted (this proof is a value of type Sorted _β€_ (y l)) , then the list x β· y β· l will also be sorted.
Type (predicate) "permutation". Arguments are two lists. Input axioms: refl - the list is a permutation of itself; perm - if we have a proof that some list l is a permutation of another list lβ ++ xβ β· xβ β· lβ (proof of this is a value of type Permutation l (lβ ++ xβ β· xβ β· lβ) ), then if you rearrange two arbitrary element in places, we get that the new list is a permutation of the first one.
Well, everything is simple - it is not dependent type - analog of Either in Haskell.
This is an analogue of a tuple. The record is used, since this type can have only one constructor. This definition uses the dependent type: the first element is a value, and the second is the proof of the execution of a predicate on this element. But, of course, you donβt have to use it this way, you can just like a regular tuple (through _ Γ _ ) - then the dependence between the elements is ignored. syntax allows new syntaxes to be defined if there are few simple possibilities.
Finally, we describe the type of the sort function: this function accepts (implicitly) a predicate that determines the order, also a function that for input values ββreturns a proof that the first is greater than the second or that the second is greater than the first. I think the reader guessed that this function will be used to build evidence of the sorting of the result list. Also, of course, one of the input parameters is a list that will be sorted.
The sort function returns a list and two proofs (sorting and permutations).
Of course, no implementation of this function will be here - not that I would be sorry to show the code, I feel sorry for myself to explain it. Therefore, I will give proofs (implementations) of some auxiliary functions that I needed while writing the sort function.
As you can see, everything is simple: only one axiom that says that two objects are equal, if they are one and the same. Also here auxiliary functions are defined for working with proofs of equivalence. I think it's more understandable here. Let me explain only with the example of β‘-elim : the only value of the argument of the type x β‘ y can be refl , which has one implicit parameter, which in the β‘-elim refl _ p line is equal to both x and y , therefore, p has the same value type and P x and P y , and if the value of p is of type P y , then in this situation it will be the result of the function β‘-elim .
Here $ is nothing more than an application operator, like in Haskell. It is clear from the definition that this function (or, one can say, the lemma) proves for three arbitrary lists the associativity of the concatenation operation. I want to note that during the compilation terms are partially reduced using the existing definitions. In this function, the following happens:
term
has a type
and we need a type
or
this given that
further, the compiler, using the definition of concatenation, reduces these terms to some general form.
Try with a term using concatenation definition,
get a term
It should also be borne in mind that the concatenation operation is right associative - but this is not important for understanding.
These features are more interesting. Here I just want to note that if we consider types as theorems or lemmas, and terms of a corresponding type as evidence, then it is obvious that there can be any number of proofs of a certain statement (as well as terms of a corresponding type). For example, it seems to me that the function above can be proved easier It is also interesting that the βsorted listβ type I cited is a kind of singleton: each type has one representative. As for the permutation, for one type there can be an infinite number of different terms (for example, you can rearrange the same elements twice so that the lists will not change).
Finally, the resolving procedure for determining the order on natural numbers. (Pay attention to how variables are named - all that there is a term without spaces.) The predicate is _β€_ . Two axioms are introduced, one of which says that any number is greater than or equal to zero, and the other that if one number is greater than the other, then the ratio will remain if you add one to them.
It also uses a with construction - but I think its use is very clear.
From myself I will say that it is very interesting to write such programs.
Having read several books on typed lambda calculus, namely on dependent types, I saw an interesting pattern: everywhere the first example is the definition of the βsorted listβ type. Everything would be fine, but there was nothing beyond this definition. So I thought up to fill this gap and implement a function that accepts the list, and returns another list and two proofs. One proves that the result is a permutation of the input, and the other proves that the result is a sorted list.
Formal description
')
In this section, I will provide the basic types that will be used further, and some auxiliary functions. Also here will be shown some interesting syntactic charms of Agda. For those who are not very familiar with Agda, I recommend watching the video / slides of Jan Malakhovsky at the SPbHUG / FProg 2012-07 meeting - in my opinion, this is the only introduction to Agda in Russian (well, I havenβt met again). Or browse through the manual from the Agda site (it is not large) or this tutorial .
List definitions
data List {a} (A : Set a) : Set a where [] : List A _β·_ : (x : A) (xs : List A) β List A [_] : β {a} {A : Set a} β A β List A [ x ] = x β· [] _++_ : β {a} {A : Set a} β List A β List A β List A [] ++ ys = ys (x β· xs) ++ ys = x β· (xs ++ ys) Here we have a list. The definition is taken from the standard library. As you can see, the elements of the list can be values ββof any type, even types and types of types and so on. This is possible due to the use of high-order polymorphism: the parameter a is introduced, which is responsible for the level, that is, the usual types are of type Set 0 , Set 0 is of type Set 1 , etc.
Also in this definition you can see how in Agda operators are declared, namely through underscores, in which place there will be arguments. It should be noted that this method allows you to define very different and very interesting forms, such as a function that returns a list from a single element [_] .
It should be noted that for all operators (combinators with underscores) you can specify the priority and associativity. Also in Agda, any Unicode sequence without spaces and brackets (round and curly) is a term.
You should also pay attention to the parentheses and curly braces: curly brackets in the type indication say that this argument is implicit and will be output by the compiler.
Type "sorted list"
data Sorted {A} (_β€_ : A β A β Set) : List A β Set where nil : Sorted _β€_ [] one : {x : A} β Sorted _β€_ [ x ] two : {x : A} β β {yl} β x β€ y β Sorted _β€_ (y β· l) β Sorted _β€_ (x β· y β· l) This definition of the predicate is "sorted list". Designers should be considered as axioms. We have axioms nil and one which say that the empty list and the list with one element are sorted. We also see that the Sorted type depends on the predicate _β€_ , which is responsible for the order β something like the comparison function, but dependently type (the arguments are values ββof the usual type, and the result is some type whose value is proof). Axiom two says the following: if we have evidence that x β€ y ( x β€ y is a type, and a value of type x β€ y is proof that x β€ y . See the Curry-Howard isomorphism ), and proof that some list with head y is sorted (this proof is a value of type Sorted _β€_ (y l)) , then the list x β· y β· l will also be sorted.
Type "permutation"
data Permutation {A} : List A β List A β Set where refl : β {l} β Permutation ll perm : β {l} lβ xβ xβ lβ β Permutation l (lβ ++ xβ β· xβ β· lβ) β Permutation l (lβ ++ xβ β· xβ β· lβ) Type (predicate) "permutation". Arguments are two lists. Input axioms: refl - the list is a permutation of itself; perm - if we have a proof that some list l is a permutation of another list lβ ++ xβ β· xβ β· lβ (proof of this is a value of type Permutation l (lβ ++ xβ β· xβ β· lβ) ), then if you rearrange two arbitrary element in places, we get that the new list is a permutation of the first one.
Type "amount"
data _β_ {ab} (A : Set a) (B : Set b) : Set (a β b) where injβ : (x : A) β A β B injβ : (y : B) β A β B Well, everything is simple - it is not dependent type - analog of Either in Haskell.
Type Product
record Ξ£ {ab} (A : Set a) (B : A β Set b) : Set (a β b) where constructor _,_ field projβ : A projβ : B projβ syntax Ξ£ A (Ξ» x β B) = Ξ£[ x βΆ A ] B _Γ_ : β {ab} (A : Set a) (B : Set b) β Set (a β b) A Γ B = Ξ£[ _ βΆ A ] B This is an analogue of a tuple. The record is used, since this type can have only one constructor. This definition uses the dependent type: the first element is a value, and the second is the proof of the execution of a predicate on this element. But, of course, you donβt have to use it this way, you can just like a regular tuple (through _ Γ _ ) - then the dependence between the elements is ignored. syntax allows new syntaxes to be defined if there are few simple possibilities.
Sort function
sort : {A : Set} {_β€_ : A β A β Set} β (β xy β (x β€ y) β (y β€ x)) β (l : List A) β Ξ£[ l' βΆ List A ] (Sorted _β€_ l' Γ Permutation l l') Finally, we describe the type of the sort function: this function accepts (implicitly) a predicate that determines the order, also a function that for input values ββreturns a proof that the first is greater than the second or that the second is greater than the first. I think the reader guessed that this function will be used to build evidence of the sorting of the result list. Also, of course, one of the input parameters is a list that will be sorted.
The sort function returns a list and two proofs (sorting and permutations).
Implement the sort function
Of course, no implementation of this function will be here - not that I would be sorry to show the code, I feel sorry for myself to explain it. Therefore, I will give proofs (implementations) of some auxiliary functions that I needed while writing the sort function.
A working source can be found here.
Used by Agda-2.3.1 and Standard Library-0.6
{-# OPTIONS --no-termination-check #-} module QuickSort where open import IO.Primitive using () renaming (putStrLn to putCoStrLn) open import Data.String using (toCostring; String) renaming (_++_ to _+s+_) open import Data.List open import Data.Nat open import Data.Nat.Show open import Data.Sum open import Data.Product open import Relation.Binary.Core open import Function data Sorted {A} (_β€_ : A β A β Set) : List A β Set where nil : Sorted _β€_ [] one : {x : A} β Sorted _β€_ [ x ] two : {x : A} β β {yl} β x β€ y β Sorted _β€_ (y β· l) β Sorted _β€_ (x β· y β· l) data Permutation {A} : List A β List A β Set where refl : β {l} β Permutation ll perm : β {l} lβ xβ xβ lβ β Permutation l (lβ ++ xβ β· xβ β· lβ) β Permutation l (lβ ++ xβ β· xβ β· lβ) β‘-elim : β {l} {A : Set l} {xy : A} β x β‘ y β (P : A β Set l) β P x β P y β‘-elim refl _ p = p β‘-sym : β {l} {A : Set l} {xy : A} β x β‘ y β y β‘ x β‘-sym refl = refl β‘-trans : β {l} {A : Set l} {xyz : A} β x β‘ y β y β‘ z β x β‘ z β‘-trans refl refl = refl ++-assoc : β {l} {A : Set l} (lβ lβ lβ : List A) β (lβ ++ lβ) ++ lβ β‘ lβ ++ (lβ ++ lβ) ++-assoc [] lβ lβ = refl ++-assoc (h β· t) lβ lβ = β‘-elim (β‘-sym $ ++-assoc t lβ lβ) (Ξ» x β h β· x β‘ h β· t ++ (lβ ++ lβ)) refl decNat : (xy : β) β (x β€ y) β (y β€ x) decNat zero y = injβ zβ€n decNat (suc x) (suc y) with decNat xy ... | injβ p = injβ (sβ€sp) ... | injβ p = injβ (sβ€sp) decNat (suc x) zero = injβ zβ€n perm-trans : β {A} {lβ lβ lβ : List A} β Permutation lβ lβ β Permutation lβ lβ β Permutation lβ lβ perm-trans p refl = p perm-trans pβ (perm lβ xβ xβ lβ pβ) = perm lβ xβ xβ lβ $ perm-trans pβ pβ perm-sym : β {A} {lβ lβ : List A} β Permutation lβ lβ β Permutation lβ lβ perm-sym refl = refl perm-sym (perm lβ xβ xβ lβ p) = perm-trans (perm lβ xβ xβ lβ refl) (perm-sym p) perm-del-ins-r : β {A} (lβ : List A) (x : A) (lβ lβ : List A) β Permutation (lβ ++ x β· lβ ++ lβ) (lβ ++ lβ ++ x β· lβ) perm-del-ins-r lβ x [] lβ = refl perm-del-ins-r lβ x (h β· t) lβ = perm-trans pβ pβ
where pβ : Permutation (lβ ++ x β· h β· t ++ lβ) (lβ ++ h β· x β· t ++ lβ) pβ = perm lβ hx (t ++ lβ) refl pβ : Permutation ((lβ ++ [ h ]) ++ x β· t ++ lβ) ((lβ ++ [ h ]) ++ t ++ x β· lβ) pβ = perm-del-ins-r (lβ ++ [ h ]) xt lβ pβ : (lβ ++ [ h ]) ++ t ++ x β· lβ β‘ lβ ++ h β· t ++ x β· lβ pβ = ++-assoc lβ [ h ] (t ++ x β· lβ) pβ : (lβ ++ [ h ]) ++ x β· t ++ lβ β‘ lβ ++ h β· x β· t ++ lβ pβ = ++-assoc lβ [ h ] (x β· t ++ lβ) pβ : Permutation ((lβ ++ [ h ]) ++ x β· t ++ lβ) (lβ ++ h β· t ++ x β· lβ) pβ = β‘-elim pβ (Ξ» y β Permutation ((lβ ++ [ h ]) ++ x β· t ++ lβ) y) pβ pβ
: Permutation (lβ ++ h β· x β· t ++ lβ) (lβ ++ h β· t ++ x β· lβ) pβ
= β‘-elim pβ (Ξ» y β Permutation y (lβ ++ h β· t ++ x β· lβ)) pβ perm-del-ins-l : β {A} (lβ lβ : List A) (x : A) (lβ : List A) β Permutation (lβ ++ lβ ++ x β· lβ) (lβ ++ x β· lβ ++ lβ) perm-del-ins-l lβ lβ x lβ = perm-sym $ perm-del-ins-r lβ x lβ lβ perm-++ : β {A} {xβ yβ xβ yβ : List A} β Permutation xβ yβ β Permutation xβ yβ β Permutation (xβ ++ xβ) (yβ ++ yβ) perm-++ refl refl = refl perm-++ (perm {xβ} lβ eβ eβ lβ p) (refl {zβ}) = perm-trans pβ
pβ where pβ : Permutation (xβ ++ zβ) ((lβ ++ eβ β· eβ β· lβ) ++ zβ) pβ = perm-++ p refl pβ : (lβ ++ eβ β· eβ β· lβ) ++ zβ β‘ lβ ++ (eβ β· eβ β· lβ) ++ zβ pβ = ++-assoc lβ (eβ β· eβ β· lβ) zβ pβ : lβ ++ (eβ β· eβ β· lβ) ++ zβ β‘ lβ ++ eβ β· (eβ β· lβ) ++ zβ pβ = β‘-elim (++-assoc [ eβ ] (eβ β· lβ) zβ) (Ξ» x β lβ ++ (eβ β· eβ β· lβ) ++ zβ β‘ lβ ++ x) refl pβ : lβ ++ eβ β· (eβ β· lβ) ++ zβ β‘ lβ ++ eβ β· eβ β· lβ ++ zβ pβ = β‘-elim (++-assoc [ eβ ] lβ zβ) (Ξ» x β lβ ++ eβ β· (eβ β· lβ) ++ zβ β‘ lβ ++ eβ β· x) refl gβ : (lβ ++ eβ β· eβ β· lβ) ++ zβ β‘ lβ ++ (eβ β· eβ β· lβ) ++ zβ gβ = ++-assoc lβ (eβ β· eβ β· lβ) zβ gβ : lβ ++ (eβ β· eβ β· lβ) ++ zβ β‘ lβ ++ eβ β· (eβ β· lβ) ++ zβ gβ = β‘-elim (++-assoc [ eβ ] (eβ β· lβ) zβ) (Ξ» x β lβ ++ (eβ β· eβ β· lβ) ++ zβ β‘ lβ ++ x) refl gβ : lβ ++ eβ β· (eβ β· lβ) ++ zβ β‘ lβ ++ eβ β· eβ β· lβ ++ zβ gβ = β‘-elim (++-assoc [ eβ ] lβ zβ) (Ξ» x β lβ ++ eβ β· (eβ β· lβ) ++ zβ β‘ lβ ++ eβ β· x) refl pβ
: Permutation (xβ ++ zβ) (lβ ++ eβ β· eβ β· lβ ++ zβ) pβ
= β‘-elim (β‘-trans pβ $ β‘-trans pβ pβ) (Permutation (xβ ++ zβ)) pβ pβ : Permutation (lβ ++ eβ β· eβ β· lβ ++ zβ) (lβ ++ eβ β· eβ β· lβ ++ zβ) pβ = perm lβ eβ eβ (lβ ++ zβ) refl pβ : Permutation (lβ ++ eβ β· eβ β· lβ ++ zβ) ((lβ ++ eβ β· eβ β· lβ) ++ zβ) pβ = β‘-elim (β‘-sym $ β‘-trans gβ $ β‘-trans gβ gβ) (Permutation (lβ ++ eβ β· eβ β· lβ ++ zβ)) pβ perm-++ {_} {xβ} {yβ} .{_} .{_} pβ (perm {xβ} lβ eβ eβ lβ pβ) = β‘-elim pβ (Permutation (xβ ++ xβ)) pβ where p' : Permutation (xβ ++ xβ) (yβ ++ lβ ++ eβ β· eβ β· lβ) p' = perm-++ pβ pβ pβ : yβ ++ lβ ++ eβ β· eβ β· lβ β‘ (yβ ++ lβ) ++ eβ β· eβ β· lβ pβ = β‘-sym $ ++-assoc yβ lβ (eβ β· eβ β· lβ) pβ : Permutation (xβ ++ xβ) ((yβ ++ lβ) ++ eβ β· eβ β· lβ) pβ = β‘-elim pβ (Permutation (xβ ++ xβ)) p' pβ
: Permutation ((yβ ++ lβ) ++ eβ β· eβ β· lβ) ((yβ ++ lβ) ++ eβ β· eβ β· lβ) pβ
= perm (yβ ++ lβ) eβ eβ lβ refl pβ : Permutation (xβ ++ xβ) ((yβ ++ lβ) ++ eβ β· eβ β· lβ) pβ = perm-trans pβ pβ
pβ : (yβ ++ lβ) ++ eβ β· eβ β· lβ β‘ yβ ++ lβ ++ eβ β· eβ β· lβ pβ = ++-assoc yβ lβ (eβ β· eβ β· lβ) ++-[] : β {l} {A : Set l} (l : List A) β l ++ [] β‘ l ++-[] [] = refl ++-[] (h β· t) = β‘-trans pβ pβ where pβ : (h β· t) ++ [] β‘ h β· t ++ [] pβ = ++-assoc [ h ] t [] pβ : h β· t ++ [] β‘ h β· t pβ = β‘-elim (++-[] t) (Ξ» x β h β· t ++ [] β‘ h β· x) refl data ConstrainedList {A} (P : A β Set) : List A β Set where [] : ConstrainedList P [] _β·_ : {x : A} {xs : List A} (p : P x) β ConstrainedList P xs β ConstrainedList P (x β· xs) infix 2 _β_ data _β_ {A} : A β List A β Set where exact : β ht β h β h β· t cons : β h {xl} β x β l β x β h β· l create-β : β {A} (lβ : List A) (x : A) (lβ : List A) β x β (lβ ++ x β· lβ) create-β [] x lβ = exact x lβ create-β (hβ β· tβ) x lβ = cons hβ $ create-β tβ x lβ perm-β : β {A l l'} {x : A} β x β l β Permutation l' l β x β l' perm-β p refl = p perm-β {A} .{lβ ++ xβ β· xβ β· lβ} {l'} {x} pβ (perm lβ xβ xβ lβ pβ) = perm-β (loop lβ xβ xβ lβ pβ) pβ where loop : β lβ xβ xβ lβ β x β lβ ++ xβ β· xβ β· lβ β x β lβ ++ xβ β· xβ β· lβ loop [] .x xβ lβ (exact .x .(xβ β· lβ)) = cons xβ $ exact x lβ loop [] .xβ .x .lβ (cons xβ (exact .x lβ)) = exact x (xβ β· lβ) loop [] .xβ .xβ lβ (cons xβ (cons xβ p)) = cons xβ $ cons xβ p loop (.x β· tβ) xβ xβ lβ (exact .x .(tβ ++ xβ β· xβ β· lβ)) = exact x (tβ ++ xβ β· xβ β· lβ) loop (.hβ β· tβ) xβ xβ lβ (cons hβ p) = cons hβ $ loop tβ xβ xβ lβ p constr-β : β {A l} {x : A} β β {P} β ConstrainedList P l β x β l β P x constr-β [] () constr-β (p β· _) (exact _ _) = p constr-β (_ β· cl) (cons _ p) = constr-β cl p sortedHelperβ : β {A _β€_} {h : A} β β {l'} β Sorted _β€_ l' β β {l} β Permutation ll' β ConstrainedList (Ξ» x β x β€ h) l β β {g'} β Sorted _β€_ (h β· g') β Sorted _β€_ (l' ++ h β· g') sortedHelperβ {_} {_β€_} {h} {l'} sl' pll' cl {g'} sg' = loop [] l' refl sl' where loop : β lβ lβ β lβ ++ lβ β‘ l' β Sorted _β€_ lβ β Sorted _β€_ (lβ ++ h β· g') loop _ .[] _ nil = sg' loop lβ .(x β· []) p (one {x}) = two (constr-β cl $ perm-β xβl' pll') sg' where xβl' : x β l' xβl' = β‘-elim p (Ξ» l β x β l) (create-β lβ x []) loop lβ .(x β· y β· l) pβ‘ (two {x} {y} {l} xβ€y ps) = two xβ€y $ loop (lβ ++ [ x ]) (y β· l) p' ps where p' : (lβ ++ [ x ]) ++ y β· l β‘ l' p' = β‘-trans (++-assoc lβ [ x ] (y β· l)) pβ‘ sortedHelperβ : β {A _β€_} {h : A} β β {l'} β Sorted _β€_ l' β β {l} β Permutation ll' β ConstrainedList (Ξ» x β x β€ h) l β β {g'} β Sorted _β€_ g' β β {g} β Permutation gg' β ConstrainedList (Ξ» x β h β€ x) g β Sorted _β€_ (l' ++ h β· g') sortedHelperβ sl' pll' cl nil _ _ = sortedHelperβ sl' pll' cl one sortedHelperβ sl' pll' cl {h β· t} sg' pgg' cg = sortedHelperβ sl' pll' cl $ two (constr-β cg $ perm-β (exact ht) pgg') sg' quickSort : {A : Set} {_β€_ : A β A β Set} β (β xy β (x β€ y) β (y β€ x)) β (l : List A) β Ξ£[ l' βΆ List A ] (Sorted _β€_ l' Γ Permutation l l') quickSort _ [] = [] , nil , refl quickSort {A} {_β€_} _β€?_ (h β· t) = loop t [] [] [] [] refl where loop : β ilg β ConstrainedList (Ξ» x β x β€ h) l β ConstrainedList (Ξ» x β h β€ x) g β Permutation t ((l ++ g) ++ i) β Ξ£[ l' βΆ List A ] (Sorted _β€_ l' Γ Permutation (h β· t) l') loop [] lg cl cg p = l' ++ h β· g' , sortedHelperβ sl' pll' cl sg' pgg' cg , perm-trans pβ pβ where lSort = quickSort _β€?_ l gSort = quickSort _β€?_ g l' = projβ lSort g' = projβ gSort sl' = projβ $ projβ lSort sg' = projβ $ projβ gSort pll' = projβ $ projβ lSort pgg' = projβ $ projβ gSort pβ : Permutation (l ++ g) (l' ++ g') pβ = perm-++ pll' pgg' pβ : Permutation t (l' ++ g') pβ = perm-trans (β‘-elim (++-[] (l ++ g)) (Ξ» x β Permutation tx) p) pβ pβ : Permutation (h β· t) (h β· l' ++ g') pβ = perm-++ (refl {_} {[ h ]}) pβ pβ : Permutation (h β· l' ++ g') (l' ++ h β· g') pβ = perm-del-ins-r [] hl' g' loop (h' β· t) lg cl cg p with h' β€? h ... | injβ h'β€h = loop t (h' β· l) g (h'β€h β· cl) cg (perm-trans p p') where p' : Permutation ((l ++ g) ++ h' β· t) (h' β· (l ++ g) ++ t) p' = perm-del-ins-l [] (l ++ g) h' t ... | injβ hβ€h' = loop tl (h' β· g) cl (hβ€h' β· cg) (perm-trans p p') where pβ : l ++ g ++ h' β· t β‘ (l ++ g) ++ h' β· t pβ = β‘-sym $ ++-assoc lg (h' β· t) pβ : l ++ (h' β· g) ++ t β‘ (l ++ h' β· g) ++ t pβ = β‘-sym $ ++-assoc l (h' β· g) t pβ : (h' β· g) ++ t β‘ h' β· g ++ t pβ = ++-assoc [ h' ] gt pβ : l ++ h' β· g ++ t β‘ l ++ (h' β· g) ++ t pβ = β‘-sym $ β‘-elim pβ (Ξ» x β l ++ x β‘ l ++ h' β· g ++ t) refl pβ
: Permutation (l ++ g ++ h' β· t) (l ++ h' β· g ++ t) pβ
= perm-del-ins-l lgh' t pβ : Permutation ((l ++ g) ++ h' β· t) (l ++ h' β· g ++ t) pβ = β‘-elim pβ (Ξ» x β Permutation x (l ++ h' β· g ++ t)) pβ
p' : Permutation ((l ++ g) ++ h' β· t) ((l ++ h' β· g) ++ t) p' = β‘-elim (β‘-trans pβ pβ) (Ξ» x β Permutation ((l ++ g) ++ h' β· t) x) pβ showl : List β β String showl [] = "[]" showl (h β· t) = show h +s+ "β·" +s+ showl t lβ : List β lβ = 19 β· 6 β· 13 β· 2 β· 8 β· 15 β· 1 β· 10 β· 11 β· 2 β· 17 β· 4 β· [ 3 ] lβ = quickSort decNat lβ main = putCoStrLn β toCostring $ showl $ projβ lβ Propositional Equivalence
data _β‘_ {a} {A : Set a} (x : A) : A β Set a where refl : x β‘ x β‘-cong : β {ab} {A : Set a} {B : Set b} {xy} β x β‘ y β (f : A β B) β fx β‘ fy β‘-cong refl _ = refl β‘-elim : β {l} {A : Set l} {xy : A} β x β‘ y β (P : A β Set l) β P x β P y β‘-elim refl _ p = p β‘-sym : β {l} {A : Set l} {xy : A} β x β‘ y β y β‘ x β‘-sym refl = refl β‘-trans : β {l} {A : Set l} {xyz : A} β x β‘ y β y β‘ z β x β‘ z β‘-trans refl refl = refl As you can see, everything is simple: only one axiom that says that two objects are equal, if they are one and the same. Also here auxiliary functions are defined for working with proofs of equivalence. I think it's more understandable here. Let me explain only with the example of β‘-elim : the only value of the argument of the type x β‘ y can be refl , which has one implicit parameter, which in the β‘-elim refl _ p line is equal to both x and y , therefore, p has the same value type and P x and P y , and if the value of p is of type P y , then in this situation it will be the result of the function β‘-elim .
Associative concatenation operation
++-assoc : β {l} {A : Set l} (lβ lβ lβ : List A) β (lβ ++ lβ) ++ lβ β‘ lβ ++ (lβ ++ lβ) ++-assoc [] lβ lβ = refl ++-assoc (h β· t) lβ lβ = β‘-cong (++-assoc t lβ lβ) (Ξ» x β h β· x) Here $ is nothing more than an application operator, like in Haskell. It is clear from the definition that this function (or, one can say, the lemma) proves for three arbitrary lists the associativity of the concatenation operation. I want to note that during the compilation terms are partially reduced using the existing definitions. In this function, the following happens:
term
β‘-cong (++-assoc t lβ lβ) (Ξ» x β h β· x) has a type
h β· (t ++ lβ) ++ lβ β‘ h β· t ++ (lβ ++ lβ) and we need a type
(lβ ++ lβ) ++ lβ β‘ lβ ++ (lβ ++ lβ) or
((h β· t) ++ lβ) ++ lβ β‘ (h β· t) ++ (lβ ++ lβ) this given that
lβ = h β· t further, the compiler, using the definition of concatenation, reduces these terms to some general form.
Try with a term using concatenation definition,
((h β· t) ++ lβ) ++ lβ β‘ (h β· t) ++ (lβ ++ lβ) get a term
h β· (t ++ lβ) ++ lβ β‘ h β· t ++ (lβ ++ lβ) It should also be borne in mind that the concatenation operation is right associative - but this is not important for understanding.
The transitivity and symmetry of the permutation
perm-trans : β {A} {lβ lβ lβ : List A} β Permutation lβ lβ β Permutation lβ lβ β Permutation lβ lβ perm-trans p refl = p perm-trans pβ (perm lβ xβ xβ lβ pβ) = perm lβ xβ xβ lβ $ perm-trans pβ pβ perm-sym : β {A} {lβ lβ : List A} β Permutation lβ lβ β Permutation lβ lβ perm-sym refl = refl perm-sym (perm lβ xβ xβ lβ p) = perm-trans (perm lβ xβ xβ lβ refl) (perm-sym p) "Long" rearrangement left and right
perm-del-ins-r : β {A} (lβ : List A) (x : A) (lβ lβ : List A) β Permutation (lβ ++ x β· lβ ++ lβ) (lβ ++ lβ ++ x β· lβ) perm-del-ins-r lβ x [] lβ = refl perm-del-ins-r lβ x (h β· t) lβ = perm-trans pβ pβ
where pβ : Permutation (lβ ++ x β· h β· t ++ lβ) (lβ ++ h β· x β· t ++ lβ) pβ = perm lβ hx (t ++ lβ) refl pβ : Permutation ((lβ ++ [ h ]) ++ x β· t ++ lβ) ((lβ ++ [ h ]) ++ t ++ x β· lβ) pβ = perm-del-ins-r (lβ ++ [ h ]) xt lβ pβ : (lβ ++ [ h ]) ++ t ++ x β· lβ β‘ lβ ++ h β· t ++ x β· lβ pβ = ++-assoc lβ [ h ] (t ++ x β· lβ) pβ : (lβ ++ [ h ]) ++ x β· t ++ lβ β‘ lβ ++ h β· x β· t ++ lβ pβ = ++-assoc lβ [ h ] (x β· t ++ lβ) pβ : Permutation ((lβ ++ [ h ]) ++ x β· t ++ lβ) (lβ ++ h β· t ++ x β· lβ) pβ = β‘-elim pβ (Ξ» y β Permutation ((lβ ++ [ h ]) ++ x β· t ++ lβ) y) pβ pβ
: Permutation (lβ ++ h β· x β· t ++ lβ) (lβ ++ h β· t ++ x β· lβ) pβ
= β‘-elim pβ (Ξ» y β Permutation y (lβ ++ h β· t ++ x β· lβ)) pβ perm-del-ins-l : β {A} (lβ lβ : List A) (x : A) (lβ : List A) β Permutation (lβ ++ lβ ++ x β· lβ) (lβ ++ x β· lβ ++ lβ) perm-del-ins-l lβ lβ x lβ = perm-sym $ perm-del-ins-r lβ x lβ lβ These features are more interesting. Here I just want to note that if we consider types as theorems or lemmas, and terms of a corresponding type as evidence, then it is obvious that there can be any number of proofs of a certain statement (as well as terms of a corresponding type). For example, it seems to me that the function above can be proved easier It is also interesting that the βsorted listβ type I cited is a kind of singleton: each type has one representative. As for the permutation, for one type there can be an infinite number of different terms (for example, you can rearrange the same elements twice so that the lists will not change).
Order on natural numbers
data β : Set where zero : β suc : β β β data _β€_ : β β β β Set where zβ€n : β {n} β zero β€ n sβ€s : β {mn} (mβ€n : m β€ n) β suc m β€ suc n decNat : (xy : β) β (x β€ y) β (y β€ x) decNat zero y = injβ zβ€n decNat (suc x) (suc y) with decNat xy ... | injβ p = injβ (sβ€sp) ... | injβ p = injβ (sβ€sp) decNat (suc x) zero = injβ zβ€n Finally, the resolving procedure for determining the order on natural numbers. (Pay attention to how variables are named - all that there is a term without spaces.) The predicate is _β€_ . Two axioms are introduced, one of which says that any number is greater than or equal to zero, and the other that if one number is greater than the other, then the ratio will remain if you add one to them.
It also uses a with construction - but I think its use is very clear.
That's all:)
From myself I will say that it is very interesting to write such programs.
Source: https://habr.com/ru/post/148769/
All Articles