{- \section{Introduction}
In this document, we prove the correctness of insertion sort.
\subsection{Preliminaries}
In the sections below, we rely on various definitions stated in the
following separate documents:
-}
--#include "Sorting/predikatlogik.alfa"
--#include "Sorting/satslogik.alfa"
--#include "Sorting/decide.alfa"
--#include "Sorting/nat.alfa"
{- \section{Miscellaneuos definitions and lemmas}
Here we define what a list is, what it means for a list to be sorted (ordered)
and how to insert a new element at the right position in a sorted list.
-}
List (A::Set) :: Set
= data Nil | Cons (x::A) (xs::List A)
singleton (A::Set)(x::A) :: List A
= Cons@_ x Nil@_
IsLeAll (x::Nat)(xs::List Nat) :: Prop
= case xs of {
(Nil) -> Triviality;
(Cons x' xs') -> And (LeNat x x') (IsLeAll x xs');}
IsSorted (xs::List Nat) :: Prop
= case xs of {
(Nil) -> Triviality;
(Cons x xs') -> And (IsLeAll x xs') (IsSorted xs');}
{-
Regarding the above definition of what it means for a list to be sorted, it is
worth noting that, for empty lists, there is nothing to prove, and for
non-empty lists, there are two things to prove.
-}
insert (x::Nat)(xs::List Nat) :: List Nat
= case xs of {
(Nil) -> singleton Nat x;
(Cons x' xs') -> ifLt (List Nat) x x' (Cons@_ x xs) (Cons@_ x' (insert x xs'));}
IsLeFirst (a::Nat)
(x::Nat)
(xs::List Nat)
(ax::LeNat a x)
(p::IsSorted (Cons@_ x xs))
:: IsLeAll a (Cons@_ x xs)
= case xs of {
(Nil) ->
let ndgoal :: IsLeAll a (Cons@_ x Nil@_)
= AndIntro (LeNat a x) (IsLeAll a Nil@_)
(let ndgoal :: LeNat a x
= ax
in ndgoal)
(let ndgoal :: IsLeAll a Nil@_
= trivial
in ndgoal)
in ndgoal;
(Cons x' xs') ->
let ndgoal :: IsLeAll a (Cons@_ x (Cons@_ x' xs'))
= AndIntro (LeNat a x) (IsLeAll a (Cons@_ x' xs'))
(let ndgoal :: LeNat a x
= ax
in ndgoal)
(let ndgoal :: IsLeAll a (Cons@_ x' xs')
= AndElim (IsLeAll x (Cons@_ x' xs')) (IsSorted (Cons@_ x' xs'))
(IsLeAll a (Cons@_ x' xs'))
(let ndgoal :: IsSorted (Cons@_ x xs)
= p
in ndgoal)
(\(h::IsLeAll x (Cons@_ x' xs')) ->
\(h'::IsSorted (Cons@_ x' xs')) ->
let ndgoal :: IsLeAll a (Cons@_ x' xs')
= AndElim (LeNat x x') (IsLeAll x xs')
(IsLeAll a (Cons@_ x' xs'))
(let ndgoal :: And (LeNat x x') (IsLeAll x xs')
= h
in ndgoal)
(\(h0::LeNat x x') ->
\(h1::IsLeAll x xs') ->
let ndgoal :: IsLeAll a (Cons@_ x' xs')
= IsLeFirst a x' xs'
(let ndgoal :: LeNat a x'
= letrans a x x'
(let ndgoal :: LeNat a x
= ax
in ndgoal)
(let ndgoal :: LeNat x x'
= h0
in ndgoal)
in ndgoal)
(let ndgoal :: IsSorted (Cons@_ x' xs')
= h'
in ndgoal)
in ndgoal)
in ndgoal)
in ndgoal)
in ndgoal;}
ThInsertInSorted (x::Nat)(xs::List Nat)(p::IsSorted xs)
:: IsSorted (insert x xs)
= case xs of {
(Nil) ->
let ndgoal :: IsSorted (insert x Nil@_)
= AndIntro (IsLeAll x Nil@_) (IsSorted Nil@_)
(let ndgoal :: IsLeAll x Nil@_
= trivial
in ndgoal)
(let ndgoal :: IsSorted Nil@_
= trivial
in ndgoal)
in ndgoal;
(Cons x' xs') ->
ifLtCase (List Nat) (\(h::List Nat) -> IsSorted h) x x'
(Cons@_ x (Cons@_ x' xs'))
(Cons@_ x' (insert x xs'))
(\(h::LeNat x x') ->
let ndgoal :: IsSorted (Cons@_ x (Cons@_ x' xs'))
= AndIntro (IsLeAll x (Cons@_ x' xs')) (IsSorted (Cons@_ x' xs'))
(let ndgoal :: IsLeAll x (Cons@_ x' xs')
= IsLeFirst x x' xs'
(let ndgoal :: LeNat x x'
= h
in ndgoal)
(let ndgoal :: IsSorted (Cons@_ x' xs')
= p
in ndgoal)
in ndgoal)
(let ndgoal :: IsSorted (Cons@_ x' xs')
= p
in ndgoal)
in ndgoal)
(\(h::Not (LeNat x x')) ->
let indhyp :: IsSorted (insert x xs')
= let ndgoal :: IsSorted (insert x xs')
= ThInsertInSorted x xs'
(let ndgoal :: IsSorted xs'
= And2Elim (IsLeAll x' xs') (IsSorted xs')
(let ndgoal :: And (IsLeAll x' xs') (IsSorted xs')
= p
in ndgoal)
in ndgoal)
in ndgoal
lemma1 :: LeNat x' x
= leSym x x' h
lemma2 (x'::Nat)(x::Nat)(xs'::List Nat)(px::LeNat x' x)(pxs::IsLeAll x' xs')
:: IsLeAll x' (insert x xs')
= case xs' of {
(Nil) ->
let ndgoal :: IsLeAll x' (insert x Nil@_)
= AndIntro (LeNat x' x) (IsLeAll x' Nil@_) px trivial
in ndgoal;
(Cons x0 xs0) ->
ifLtCase (List Nat) (\(h'::List Nat) -> IsLeAll x' h') x x0
(Cons@_ x (Cons@_ x0 xs0))
(Cons@_ x0 (insert x xs0))
(\(h'::LeNat x x0) ->
let ndgoal :: IsLeAll x' (Cons@_ x (Cons@_ x0 xs0))
= AndIntro (LeNat x' x) (IsLeAll x' (Cons@_ x0 xs0))
(let ndgoal :: LeNat x' x
= px
in ndgoal)
(let ndgoal :: IsLeAll x' (Cons@_ x0 xs0)
= pxs
in ndgoal)
in ndgoal)
(\(h'::Not (LeNat x x0)) ->
let ndgoal :: IsLeAll x' (Cons@_ x0 (insert x xs0))
= AndElim (LeNat x' x0) (IsLeAll x' xs0)
(IsLeAll x' (Cons@_ x0 (insert x xs0)))
(let ndgoal :: And (LeNat x' x0) (IsLeAll x' xs0)
= pxs
in ndgoal)
(\(h0::LeNat x' x0) ->
\(h1::IsLeAll x' xs0) ->
let ndgoal :: IsLeAll x' (Cons@_ x0 (insert x xs0))
= AndIntro (LeNat x' x0) (IsLeAll x' (insert x xs0))
(let ndgoal :: LeNat x' x0
= h0
in ndgoal)
(let ndgoal :: IsLeAll x' (insert x xs0)
= lemma2 x' x xs0
(let ndgoal :: LeNat x' x
= px
in ndgoal)
(let ndgoal :: IsLeAll x' xs0
= h1
in ndgoal)
in ndgoal)
in ndgoal)
in ndgoal);}
in let ndgoal :: IsSorted (Cons@_ x' (insert x xs'))
= AndIntro (IsLeAll x' (insert x xs')) (IsSorted (insert x xs'))
(let ndgoal :: IsLeAll x' (insert x xs')
= lemma2 x' x xs'
(let ndgoal :: LeNat x' x
= lemma1
in ndgoal)
(let ndgoal :: IsLeAll x' xs'
= And1Elim (IsLeAll x' xs') (IsSorted xs')
(let ndgoal :: And (IsLeAll x' xs') (IsSorted xs')
= p
in ndgoal)
in ndgoal)
in ndgoal)
(let ndgoal :: IsSorted (insert x xs')
= indhyp
in ndgoal)
in ndgoal);}
{- \section{Definitions and lemmas relating to permutations}
-}
count (x::Nat)(xs::List Nat) :: Nat
= case xs of {
(Nil) -> Zero@_;
(Cons x' xs') -> ifEq Nat x x' (Succ@_ (count x xs')) (count x xs');}
Permutation (xs::List Nat)(ys::List Nat) :: Prop
= ForAll Nat (\(n::Nat) -> EqNat (count n xs) (count n ys))
ThPermNil :: Permutation Nil@_ Nil@_
= let ndgoal :: Permutation Nil@_ Nil@_
= ForAllIntro Nat (\(n::Nat) -> EqNat (count n Nil@_) (count n Nil@_))
(\(any::Nat) ->
let ndgoal :: EqNat (count any Nil@_) (count any Nil@_)
= trivial
in ndgoal)
in ndgoal
ThPermCons (x::Nat)(ys::List Nat)(zs::List Nat)(p::Permutation ys zs)
:: Permutation (Cons@_ x ys) (Cons@_ x zs)
= {-#H#-}ForAllIntro Nat
(\(n::Nat) -> EqNat (count n (Cons@_ x ys)) (count n (Cons@_ x zs)))
(\(n::Nat) ->
ifEqCase Nat (\(h::Nat) -> EqNat h (count n (Cons@_ x zs))) n x
(Succ@_ (count n ys))
(count n ys)
(\(h::EqNat n x) ->
ifEqCase Nat (\(h'::Nat) -> EqNat (Succ@_ (count n ys)) h') n x
(Succ@_ (count n zs))
(count n zs)
(\(h'::EqNat n x) ->
ForAllElim Nat (\(h0::Nat) -> EqNat (count h0 ys) (count h0 zs)) n p)
(\(h'::Not (EqNat n x)) ->
AbsurdityElim (EqNat (Succ@_ (count n ys)) (count n zs))
(ImpliesElim (EqNat n x) Absurdity h' h)))
(\(h::Not (EqNat n x)) ->
ifEqCase Nat (\(h'::Nat) -> EqNat (count n ys) h') n x (Succ@_ (count n zs))
(count n zs)
(\(h'::EqNat n x) ->
AbsurdityElim (EqNat (count n ys) (Succ@_ (count n zs)))
(ImpliesElim (EqNat n x) Absurdity h h'))
(\(h'::Not (EqNat n x)) ->
ForAllElim Nat (\(h0::Nat) -> EqNat (count h0 ys) (count h0 zs)) n p)))
ThPermTrans (xs::List Nat)
(ys::List Nat)
(zs::List Nat)
(xy::Permutation xs ys)
(yz::Permutation ys zs)
:: Permutation xs zs
= ForAllIntro Nat (\(n::Nat) -> EqNat (count n xs) (count n zs))
(\(any::Nat) ->
trans (count any xs) (count any ys) (count any zs)
(ForAllElim Nat (\(h::Nat) -> EqNat (count h xs) (count h ys)) any xy)
(ForAllElim Nat (\(h::Nat) -> EqNat (count h ys) (count h zs)) any yz))
ThPermSwap (x1::Nat)(x2::Nat)(xs::List Nat)
:: Permutation (Cons@_ x1 (Cons@_ x2 xs)) (Cons@_ x2 (Cons@_ x1 xs))
= {-#H#-}ForAllIntro Nat
(\(n::Nat) ->
EqNat (count n (Cons@_ x1 (Cons@_ x2 xs))) (count n (Cons@_ x2 (Cons@_ x1 xs))))
(\(any::Nat) ->
ifEqCase Nat (\(h'::Nat) -> EqNat h' (count any (Cons@_ x2 (Cons@_ x1 xs)))) any
x1
(Succ@_ (count any (Cons@_ x2 xs)))
(count any (Cons@_ x2 xs))
(\(h'::EqNat any x1) ->
ifEqCase Nat (\(h::Nat) -> EqNat (Succ@_ (count any (Cons@_ x2 xs))) h) any x2
(Succ@_ (count any (Cons@_ x1 xs)))
(count any (Cons@_ x1 xs))
(\(h::EqNat any x2) ->
ifEqCase Nat (\(h0::Nat) -> EqNat h0 (count any (Cons@_ x1 xs))) any x2
(Succ@_ (count any xs))
(count any xs)
(\(h0::EqNat any x2) ->
ifEqCase Nat (\(h1::Nat) -> EqNat (Succ@_ (count any xs)) h1) any x1
(Succ@_ (count any xs))
(count any xs)
(\(h1::EqNat any x1) -> refl (count any xs))
(\(h1::Not (EqNat any x1)) ->
AbsurdityElim (EqNat (Succ@_ (count any xs)) (count any xs))
(ImpliesElim (EqNat any x1) Absurdity h1 h')))
(\(h0::Not (EqNat any x2)) ->
AbsurdityElim (EqNat (count any xs) (count any (Cons@_ x1 xs)))
(ImpliesElim (EqNat any x2) Absurdity h0 h)))
(\(h::Not (EqNat any x2)) ->
ifEqCase Nat (\(h0::Nat) -> EqNat (Succ@_ (count any (Cons@_ x2 xs))) h0) any x1
(Succ@_ (count any xs))
(count any xs)
(\(h0::EqNat any x1) ->
ifEqCase Nat (\(h1::Nat) -> EqNat h1 (count any xs)) any x2
(Succ@_ (count any xs))
(count any xs)
(\(h1::EqNat any x2) ->
AbsurdityElim (EqNat (Succ@_ (count any xs)) (count any xs))
(ImpliesElim (EqNat any x2) Absurdity h h1))
(\(h1::Not (EqNat any x2)) -> refl (count any xs)))
(\(h0::Not (EqNat any x1)) ->
AbsurdityElim (EqNat (Succ@_ (count any (Cons@_ x2 xs))) (count any xs))
(ImpliesElim (EqNat any x1) Absurdity h0 h'))))
(\(h'::Not (EqNat any x1)) ->
ifEqCase Nat (\(h0::Nat) -> EqNat (count any (Cons@_ x2 xs)) h0) any x2
(Succ@_ (count any (Cons@_ x1 xs)))
(count any (Cons@_ x1 xs))
(\(h0::EqNat any x2) ->
ifEqCase Nat (\(h::Nat) -> EqNat h (Succ@_ (count any (Cons@_ x1 xs)))) any x2
(Succ@_ (count any xs))
(count any xs)
(\(h::EqNat any x2) ->
ifEqCase Nat (\(h1::Nat) -> EqNat (count any xs) h1) any x1
(Succ@_ (count any xs))
(count any xs)
(\(h1::EqNat any x1) ->
AbsurdityElim (EqNat (count any xs) (Succ@_ (count any xs)))
(ImpliesElim (EqNat any x1) Absurdity h' h1))
(\(h1::Not (EqNat any x1)) -> refl (count any xs)))
(\(h::Not (EqNat any x2)) ->
AbsurdityElim (EqNat (count any xs) (Succ@_ (count any (Cons@_ x1 xs))))
(ImpliesElim (EqNat any x2) Absurdity h h0)))
(\(h::Not (EqNat any x2)) ->
ifEqCase Nat (\(h0::Nat) -> EqNat h0 (count any (Cons@_ x1 xs))) any x2
(Succ@_ (count any xs))
(count any xs)
(\(h0::EqNat any x2) ->
AbsurdityElim (EqNat (Succ@_ (count any xs)) (count any (Cons@_ x1 xs)))
(ImpliesElim (EqNat any x2) Absurdity h h0))
(\(h0::Not (EqNat any x2)) ->
ifEqCase Nat (\(h1::Nat) -> EqNat (count any xs) h1) any x1
(Succ@_ (count any xs))
(count any xs)
(\(h1::EqNat any x1) ->
AbsurdityElim (EqNat (count any xs) (Succ@_ (count any xs)))
(ImpliesElim (EqNat any x1) Absurdity h' h1))
(\(h1::Not (EqNat any x1)) -> refl (count any xs))))))
ThPermInsert (x::Nat)(xs::List Nat) :: Permutation (Cons@_ x xs) (insert x xs)
= case xs of {
(Nil) ->
ForAllIntro Nat
(\(n::Nat) -> EqNat (count n (Cons@_ x Nil@_)) (count n (insert x Nil@_)))
(\(any::Nat) -> refl (count any (Cons@_ x Nil@_)));
(Cons x' xs') ->
ifLtCase (List Nat) (\(h::List Nat) -> Permutation (Cons@_ x (Cons@_ x' xs')) h)
x
x'
(Cons@_ x (Cons@_ x' xs'))
(Cons@_ x' (insert x xs'))
(\(h::LeNat x x') ->
ForAllIntro Nat
(\(n::Nat) ->
EqNat (count n (Cons@_ x (Cons@_ x' xs'))) (count n (Cons@_ x (Cons@_ x' xs'))))
(\(any::Nat) -> refl (count any (Cons@_ x (Cons@_ x' xs')))))
(\(h::Not (LeNat x x')) ->
let indhyp :: Permutation (Cons@_ x xs') (insert x xs')
= ThPermInsert x xs'
in let it :: Permutation (Cons@_ x (Cons@_ x' xs')) (Cons@_ x' (insert x xs'))
= ThPermTrans (Cons@_ x (Cons@_ x' xs')) (Cons@_ x' (Cons@_ x xs'))
(Cons@_ x' (insert x xs'))
(ThPermSwap x x' xs')
(ThPermCons x' (Cons@_ x xs') (insert x xs') indhyp)
in it);}
{-
\section{The sorting algorithm, the correctness criterion and
the correctness proof}
-}
sort (xs::List Nat) :: List Nat
= case xs of {
(Nil) -> Nil@_;
(Cons x xs') -> insert x (sort xs');}
SortSpec (xs::List Nat)(ys::List Nat) :: Prop
= And (Permutation xs ys) (IsSorted ys)
-- %% Although SortLemma is only used in ThSortIsCorrect, I made it global to be able to specify linearization properties for it.
SortLemma (x::Nat)(xs'::List Nat)(h::Permutation xs' (sort xs'))
:: Permutation (Cons@_ x xs') (sort (Cons@_ x xs'))
= let ndgoal :: Permutation (Cons@_ x xs') (sort (Cons@_ x xs'))
= ThPermTrans (Cons@_ x xs') (Cons@_ x (sort xs')) (sort (Cons@_ x xs'))
(let ndgoal :: Permutation (Cons@_ x xs') (Cons@_ x (sort xs'))
= ThPermCons x xs' (sort xs')
(let ndgoal :: Permutation xs' (sort xs')
= h
in ndgoal)
in ndgoal)
(let ndgoal :: Permutation (Cons@_ x (sort xs')) (sort (Cons@_ x xs'))
= ThPermInsert x (sort xs')
in ndgoal)
in ndgoal
ThSortIsCorrect (xs::List Nat) :: SortSpec xs (sort xs)
= case xs of {
(Nil) ->
let ndgoal :: SortSpec Nil@_ (sort Nil@_)
= AndIntro (Permutation Nil@_ (sort Nil@_)) (IsSorted (sort Nil@_))
(let ndgoal :: Permutation Nil@_ (sort Nil@_)
= ThPermNil
in ndgoal)
(let ndgoal :: IsSorted (sort Nil@_)
= trivial
in ndgoal)
in ndgoal;
(Cons x xs') ->
let indhyp :: SortSpec xs' (sort xs')
= ThSortIsCorrect xs'
in let ndgoal :: SortSpec (Cons@_ x xs') (sort (Cons@_ x xs'))
= AndElim (Permutation xs' (sort xs')) (IsSorted (sort xs'))
(SortSpec (Cons@_ x xs') (sort (Cons@_ x xs')))
(let ndgoal :: SortSpec xs' (sort xs')
= indhyp
in ndgoal)
(\(h::Permutation xs' (sort xs')) ->
\(h'::IsSorted (sort xs')) ->
let ndgoal :: SortSpec (Cons@_ x xs') (sort (Cons@_ x xs'))
= AndIntro (Permutation (Cons@_ x xs') (sort (Cons@_ x xs')))
(IsSorted (sort (Cons@_ x xs')))
(let ndgoal :: Permutation (Cons@_ x xs') (sort (Cons@_ x xs'))
= SortLemma x xs'
(let ndgoal :: Permutation xs' (sort xs')
= h
in ndgoal)
in ndgoal)
(let ndgoal :: IsSorted (sort (Cons@_ x xs'))
= ThInsertInSorted x (sort xs')
(let ndgoal :: IsSorted (sort xs')
= h'
in ndgoal)
in ndgoal)
in ndgoal)
in ndgoal;}
-- \section{A simple corollary}
ThSorting
:: ForAll (List Nat)
(\(xs::List Nat) -> Exists (List Nat) (\(ys::List Nat) -> SortSpec xs ys))
= let ndgoal
:: ForAll (List Nat)
(\(xs::List Nat) -> Exists (List Nat) (\(ys::List Nat) -> SortSpec xs ys))
= ForAllIntro (List Nat)
(\(xs::List Nat) -> Exists (List Nat) (\(ys::List Nat) -> SortSpec xs ys))
(\(xs::List Nat) ->
let ndgoal :: Exists (List Nat) (\(ys::List Nat) -> SortSpec xs ys)
= ExistsIntro (List Nat) (\(ys::List Nat) -> SortSpec xs ys) (sort xs)
(let ndgoal :: SortSpec xs (sort xs)
= ThSortIsCorrect xs
in ndgoal)
in ndgoal)
in ndgoal
sortfun :: List Nat -> List Nat
= \(xs::List Nat) -> sort xs
ThSorting2 =
ExistsIntro (List Nat -> List Nat)
(\(f::List Nat -> List Nat) ->
ForAll (List Nat) (\(xs::List Nat) -> SortSpec xs (f xs)))
sortfun
(ForAllIntro (List Nat) (\(xs::List Nat) -> SortSpec xs (sort xs))
(\(any::List Nat) -> ThSortIsCorrect any))
{-# Alfa hiding on
var "if" hide 2
con "Nil" as "[]"
con "Cons" infix rightassoc 5 as ":"
var "ThPermTrans" hide 3
var "ThPermCons" hide 3
var "ThPermInsert" hide 2
var "ThInsertInSorted" hide 2
var "Permutation" infix 4 as "~" with symbolfont
var "List" mixfix 0 as "[_]"
var "IsLeFirst" hide 3
var "singleton" hide 1 mixfix 0 as "[_]"
var "listInd" hide 2
var "SortLemma" hide 2
#-}
{-# GF Eng insert x xs = mkPN (["the list with"]++x.s!pnv++["inserted into"]++xs.s!pnv) #-}
{-# GF Eng IsLeAll x xs = mkSent (x.s!pnv++["is less than or equal to all the elements of"]++xs.s!pnv) #-}
{-# GF Eng IsLeFirst a x xs ax p =
mkText (ax.s!text++"."++p.s!text++
[". This means that "]++
a.s!pnv++["is less than or equal to all the elements of the list with"]++
x.s!pnv++["prepended to"]++xs.s!pnv) #-}
{-# GF Eng SortLemma x xs' h =
mkText (h.s!text++[". Use SortLemma"]) #-}
{-# GF Eng ThInsertInSorted x xs p =
mkText (p.s!text++[". Use the correctness of insertion"]) #-}
{-# GF Eng ThPermNil = mkThm ["the permutation of empty list theorem"] #-}
{-# GF Eng ThPermCons x ys zs p =
mkText (p.s!text++
[". We can now use the theorem about prepending an element to permutations"]) #-}
{-# GF Eng ThPermTrans xs ys zs xy yz =
mkText (indent("·"++xy.s!text++"."++newParagraph++"·"++yz.s!text)++
[". By the transitivity of the permutation relation,"]++
zs.s!pnv++"is a permutation of"++xs.s!pnv) #-}
{-# GF Eng ThPermInsert x xs = mkThm ["the theorem that inserting yields a permutation of prepending"] #-}
{-# GF Sve IsLeAll x xs = mkSent (x.s!pn++["är mindre än alla element i"]++xs.s!pn) #-}
{-# GF Sve CCCons x xs = mkPN (["listan med"]++x.s!pn++["insatt först i"]++xs.s!pn) en #-}
{-# GF Sve singleton A x = mkPN (["enelementslistan med"]++x.s!pn) en #-}
{-# GF Sve CCNil = mkPN ["den tomma listan"] en #-}
{-# GF Sve List A = {s = tbl {n => ("list"+nomReg1!n)++"av" ++ A.s ! (cn pl)} ; form = CN en} #-}
{-# GF Eng ThSortIsCorrect xs = mkThm(["the correctness of insertion sort applied to"]++xs.s!pnv) #-}
{-# GF Eng ThSorting = mkThm ["a sorting theorem"] #-}
{-# GF Eng SortSpec xs ys = mkSent(ys.s!pnv++["is a sorted version of"]++xs.s!pnv) #-}
{-# GF Eng sort xs = mkPN(["insertion sort applied to"]++xs.s!pnv) #-}
{-# GF Eng sortfun xs = mkPN(["insertion sort"]) #-}
{-# GF Eng List A = mkCN(tbl {n=>("list"+nomReg!n)++"of"++A.s!(cn pl)}) #-}
{-# GF Eng Permutation xs ys = mkSent(ys.s!pnv++["is a permutation of"]++xs.s!pnv) #-}
{-# GF Eng count x xs = mkPN(["the number of occurences of"]++x.s!pnv++"in"++xs.s!pnv) #-}
{-# GF Eng singleton A x = mkPN(["the singleton list containing"]++x.s!pnv) #-}
{-# GF Eng IsSorted xs = mkSent (xs.s!pnv ++ ["is sorted"]) #-}
{-# GF Eng CCCons x xs = mkPN (["the list with"]++x.s!pnv++["prepended to"]++xs.s!pnv) #-}
{-# GF Eng CCNil = mkPN ["the empty list"] #-}