Created
October 20, 2023 18:01
-
-
Save AdamBrouwersHarries/b154a038ab71062fb675056690afe028 to your computer and use it in GitHub Desktop.
A short gist showing how we can encode the correctness of a sorting algorithm through Idris2's type system. We define a structure to track the correct ordering of the output, and use lienarity to ensure that the output is a permutation of the input.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module ISort | |
import Data.Linear.Interface | |
import Data.Linear.Notation | |
import Data.Linear.LNat | |
import Data.Linear.LEither | |
import Data.Linear.LMaybe | |
import Data.Linear.LVect | |
-- Some useful things defined for LNats | |
-- Comparisons between linear nats | |
infix 5 <@ | |
public export | |
(<@) : LNat -@ LNat -@ Bool | |
(<@) Zero Zero = False | |
(<@) Zero (Succ y) = y `seq` True | |
(<@) (Succ x) Zero = x `seq` False | |
(<@) (Succ x) (Succ y) = x <@ y | |
public export | |
fromNat : Nat -> LNat | |
fromNat 0 = Zero | |
fromNat (S k) = Succ (fromNat k) | |
public export | |
Num LNat where | |
(+) Zero y = y | |
(+) (Succ x) y = Succ (x + y) | |
(*) Zero y = y | |
(*) (Succ x) y = y + (x * y) | |
fromInteger i = fromNat $ integerToNat i | |
public export | |
lnatToInteger : LNat -> Integer | |
lnatToInteger Zero = 0 | |
lnatToInteger (Succ x) = 1 + lnatToInteger x | |
prim__integerToLNat : Integer -> LNat | |
prim__integerToLNat i | |
= if intToBool (prim__lte_Integer 0 i) | |
then believe_me i | |
else Zero | |
public export | |
integerToLNat : Integer -> LNat | |
integerToLNat 0 = Zero -- Force evaluation and hence caching of x at compile time | |
integerToLNat x | |
= if intToBool (prim__lte_Integer x 0) | |
then Zero | |
else Succ (assert_total (integerToLNat (prim__sub_Integer x 1))) | |
public export | |
Show LNat where | |
show n = show (the Integer (lnatToInteger n)) | |
-- Proofs about LNats | |
-- LTE etc copied from the Nat implementation | |
public export | |
data LTE : (1 n : LNat) -> (1 m : LNat) -> Type where | |
LTEZero : LTE Zero right | |
LTESucc : LTE left right -> LTE (Succ left) (Succ right) | |
public export | |
GTE : LNat -@ LNat -@ Type | |
GTE left right = LTE right left | |
public export | |
LT : LNat -@ LNat -@ Type | |
LT left right = LTE (Succ left) right | |
namespace LT | |
||| LT is defined in terms of LTE which makes it annoying to use. | |
||| This convenient view of allows us to avoid having to constantly | |
||| perform nested matches to obtain another LT subproof instead of | |
||| an LTE one. | |
public export | |
data View : LT m n -> Type where | |
LTZero : View (LTESucc LTEZero) | |
LTSucc : (lt : m `LT` n) -> View (LTESucc lt) | |
||| Deconstruct an LT proof into either a base case or a further *LT* | |
export | |
view : (lt : LT m n) -> View lt | |
view (LTESucc LTEZero) = LTZero | |
view (LTESucc lt@(LTESucc _)) = LTSucc lt | |
||| A convenient alias for trivial LT proofs | |
export | |
ltZero : Zero `LT` Succ m | |
ltZero = LTESucc LTEZero | |
public export | |
GT : LNat -@ LNat -@ Type | |
GT left right = LT right left | |
export | |
succNotLTEzero : Not (LTE (Succ m) Zero) | |
succNotLTEzero LTEZero impossible | |
export | |
fromLteSucc : LTE (Succ m) (Succ n) -> LTE m n | |
fromLteSucc (LTESucc x) = x | |
export | |
succNotLTEpred : {x : LNat} -> Not $ LTE (Succ x) x | |
succNotLTEpred {x = Zero} prf = succNotLTEzero prf | |
succNotLTEpred {x = Succ _} prf = succNotLTEpred $ fromLteSucc prf | |
public export | |
isLTE : (1 m : LNat) -> (1 n : LNat) -> Dec (LTE m n) | |
isLTE Zero n = consume n `seq` Yes LTEZero | |
isLTE (Succ k) Zero = consume k `seq` No succNotLTEzero | |
isLTE (Succ k) (Succ j) | |
= case isLTE k j of | |
No contra => No (contra . fromLteSucc) | |
Yes prf => Yes (LTESucc prf) | |
public export | |
isLTEBool : (1 m : LNat) -> (1 n : LNat) -> Bool | |
isLTEBool m n = case isLTE m n of | |
(Yes prf) => True | |
(No contra) => False | |
public export | |
isLT : (1 m : LNat) -> (1 n : LNat) -> Dec (LT m n) | |
isLT m n = isLTE (Succ m) n | |
public export | |
isGT : (1 m : LNat) -> (1 n : LNat) -> Dec (GT m n) | |
isGT m n = isLT n m | |
export | |
lteSuccRight : LTE n m -> LTE n (Succ m) | |
lteSuccRight LTEZero = LTEZero | |
lteSuccRight (LTESucc x) = LTESucc (lteSuccRight x) | |
export | |
lteSuccLeft : LTE (Succ n) m -> LTE n m | |
lteSuccLeft (LTESucc x) = lteSuccRight x | |
export | |
lteAddRight : (n : LNat) -> LTE n (n + m) | |
lteAddRight Zero = LTEZero | |
lteAddRight (Succ k) {m} = LTESucc (lteAddRight {m} k) | |
export | |
notLTEImpliesGT : {a, b : LNat} -> Not (a `LTE` b) -> a `GT` b | |
notLTEImpliesGT {a = Zero } not_z_lte_b = absurd $ not_z_lte_b LTEZero | |
notLTEImpliesGT {a = Succ a} {b = Zero } notLTE = LTESucc LTEZero | |
notLTEImpliesGT {a = Succ a} {b = Succ k} notLTE = LTESucc (notLTEImpliesGT (notLTE . LTESucc)) | |
infix 1 ## | |
-- Dependent pair of linear and linear | |
public export | |
record DPairLL (t : Type) (f : t -> Type) where | |
constructor (##) | |
1 fst : t | |
1 snd : f fst | |
public export | |
isLinLTE : (1 m : LNat) -> (1 n : LNat) -> DPairLL LNat (\x => DPairLL LNat (\y => (Dec $ LTE x y, x === m, y === n))) | |
isLinLTE Zero n = Zero ## (n ## (Yes LTEZero, Refl, Refl)) | |
isLinLTE (Succ x) Zero = (Succ x) ## (Zero ## (No succNotLTEzero, Refl, Refl)) | |
isLinLTE (Succ x) (Succ z) = case isLinLTE x z of | |
(x ## (y ## (Yes prf, Refl, Refl))) => (Succ x ## (Succ y ## (Yes (LTESucc prf), Refl, Refl))) | |
(x ## (y ## (No contra, Refl, Refl))) => (Succ x ## (Succ y ## (No (contra . fromLteSucc), Refl, Refl))) | |
-- Stuff with sorted vectors. | |
data LSortedVect : Nat -> LNat -> Type where | |
Nil : (1 e : LNat) -> LSortedVect 1 e | |
Cons : (1 e : LNat) -> (1 es : LSortedVect n o) -> (0 prf : LTE e o) -> LSortedVect (S n) e | |
-- Hints for interactive editing | |
%name LSortedVect xs, ys, zs, ws, es, ms | |
Show (LSortedVect l m) where | |
show sv = "[" ++ printSortedVect sv where | |
printSortedVect : LSortedVect n e -> String | |
printSortedVect ([] e) = (show e) ++ "]" | |
printSortedVect (Cons e es prf) = (show e) ++ "," ++ printSortedVect es | |
Show (DPairLL LNat (\m => LSortedVect l m)) where | |
show (_ ## snd) = show snd | |
-- Given a proof of Not (n <= m), produce a proof of m <= n | |
flipOrdContra : {n, m : LNat} -> Not (LTE n m) -> LTE m n | |
flipOrdContra f = lteSuccLeft $ notLTEImpliesGT f | |
-- Insert a new element into a sorted Vector. | |
-- Returns back a vector one element longer, with either the smallest element being `x`, or remaining unchanged. | |
insert : (1 x : LNat) -> (1 xs : LSortedVect l m) -> LEither (LSortedVect (S l) x) (LSortedVect (S l) m) | |
insert x ([] m) = case isLinLTE x m of | |
(x ## (m ## (Yes prf, Refl, Refl))) => Left $ Cons x (Nil m) prf | |
(x ## (m ## (No contra, Refl, Refl))) => Right $ Cons m (Nil x) (flipOrdContra contra) | |
insert x (Cons m ms p) = case isLinLTE x m of | |
(x ## (m ## ((Yes prf), (Refl, Refl)))) => Left $ Cons x (Cons m ms p) prf | |
(x ## (m ## ((No contra), (Refl, Refl)))) => case insert x ms of | |
(Left ms') => Right (Cons m ms' (flipOrdContra contra)) | |
(Right ms') => Right (Cons m ms' p) | |
isort : (xs : LVect (S n) LNat) -> DPairLL LNat (\m =>LSortedVect (S n) m) | |
isort (x :: []) = (x ## Nil x) | |
isort (x :: (y :: xs)) = let (m' ## sv) = isort (y :: xs) in | |
case insert x sv of | |
(Left z) => x ## z | |
(Right z) => m' ## z | |
sortedVector = isort [41, 2, 6, 3, 7, 3, 9, 11, 13, 29] |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment