Created
October 19, 2023 21:44
-
-
Save AdamBrouwersHarries/d5d515c745de2871fe5c4d5c1264c06e to your computer and use it in GitHub Desktop.
A partial attempt at writing a constructively sorted vector, where sorting ensures 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 Linear.Reproduction | |
import Data.Linear.Interface | |
import Data.Linear.Notation | |
import Data.Linear.LNat | |
import Data.Linear.LEither | |
import Data.Linear.LMaybe | |
-- 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)) | |
isLinLTE Zero n = Zero ## (n ## Yes LTEZero) | |
isLinLTE (Succ x) Zero = (Succ x) ## (Zero ## No succNotLTEzero) | |
isLinLTE (Succ x) (Succ z) = case isLinLTE x z of | |
(x ## (y ## (Yes prf))) => (Succ x ## (Succ y ## Yes (LTESucc prf))) | |
(x ## (y ## (No contra))) => (Succ x ## (Succ y ## No (contra . fromLteSucc))) | |
-- 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 | |
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 | |
-- 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))) => Left $ Cons x (Nil m) prf | |
(x ## (m ## (No contra))) => Right $ Cons m (Nil x) (flipOrdContra contra) | |
insert x (Cons m es prf) = ?asdfasdfkljh |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
This breaks on line 198, as follows: