0 | module Data.Permutation

  2 | import Data.DPair

  3 | import Data.Nat

  4 | import Data.Vect

  5 | import Data.List

  6 | import Data.List.Quantifiers

  7 | import Data.Vect.Quantifiers

  9 | %default total

 11 | public export

 12 | factorial : Integer -> Integer

 13 | factorial 0 = 1

 14 | factorial 1 = 1

 15 | factorial k = product [2..k]

 28 | public export

 29 | data Permutation : (n : Nat) -> Type where

 30 |   Nil : Permutation Z

 31 |   (::) : Fin (S n) -> Permutation n -> Permutation (S n)

 35 | public export

 36 | toVect : Permutation n -> Vect n Nat

 37 | toVect Nil = Nil

 38 | toVect (i :: is) = finToNat i :: toVect is

 41 | public export

 42 | toList : Permutation n -> List Nat

 43 | toList = toList . toVect

 54 | public export

 55 | permSeq : Permutation n -> Vect n (Fin n)

 56 | permSeq [] = []

 57 | permSeq (i :: is) =

 58 |   i :: map (\i' => if finToNat i' >= finToNat i

 59 |                    then FS i'

 60 |                    else weaken i') (permSeq is)

 67 | public export

 68 | fromPermSeq : Vect n (Fin n) -> Maybe (Permutation n)

 69 | fromPermSeq [] = Just [] -- Prevent definition from unwrapping at compile time

 70 | fromPermSeq [_] = Just [FZ] -- (& save some time in these trivial cases)

 71 | fromPermSeq seq = if unique seq then Just $ inversions seq else Nothing

 72 |   where

 73 |     unique : forall n. Eq a => Vect n a -> Bool

 74 |     unique [] = True

 75 |     unique (x :: xs) = all (/= x) xs && unique xs

 77 |     inversions : Vect n' (Fin n) -> Permutation n'

 78 |     inversions [] = []

 79 |     inversions (x :: xs) =

 80 |       natToFinLt (count (< x) xs) @{believe_me Oh} :: inversions xs

 83 | public export

 84 | lehmerCode : Permutation n -> Integer

 85 | lehmerCode [] = 0

 86 | lehmerCode [_] = 0

 87 | lehmerCode p =

 88 |   let ns = dropWhile isZero $ toList p

 89 |   in go 0 (length ns) ns

 90 |   where

 91 |     go : Integer -> Nat -> List Nat -> Integer

 92 |     go res d [] = res

 93 |     go res d (n :: ns) = go (natToInteger n + natToInteger d * res) (pred d) ns

 96 | public export

 97 | fromLehmerCode : {n : Nat} -> (x : Integer) ->

 98 |                   {auto 0 ok : So (x >= 0 && x < factorial (natToInteger n))} -> Permutation n

 99 | fromLehmerCode {n=0} _ = []

100 | fromLehmerCode {n=1} _ = [FZ]

101 | fromLehmerCode x = go Z [] x

102 |   where

103 |     go : {n : Nat} -> (d : Nat) -> Permutation d -> Integer -> Permutation (d + n)

104 |     go {n=0} d ns _ = rewrite plusZeroRightNeutral d in ns

105 |     go {n=1} d ns x = rewrite plusCommutative d 1 in

106 |       fromJust (integerToFin x _) @{believe_me $ ItIsJust {x=()}} :: ns

107 |     go {n=S n} d ns x =

108 |       let q = x `div` natToInteger (S d)

109 |           r = natToFinLt (integerToNat (x `mod` natToInteger (S d))) @{believe_me Oh}

110 |       in rewrite sym $ plusSuccRightSucc d n in go {n} (S d) (r :: ns) q

118 | public export

119 | identity : {n : Nat} -> Permutation n

120 | identity {n=0} = []

121 | identity {n=S _} = FZ :: identity

124 | public export

125 | inverse : Permutation n -> Permutation n

126 | inverse [] = []

127 | inverse [_] = [FZ]

128 | inverse p =

129 |   let ns = permSeq p

130 |   in rewrite sym $ lengthCorrect ns in invtable Z (finToNat <$> toList ns) (length ns)

131 |   where

132 |     invtable : Nat -> List Nat -> (n' : Nat) -> Permutation n'

133 |     invtable _ _ Z = []

134 |     invtable i ns (S _) =

135 |       let ns' = takeWhile (/= i) ns

136 |       in natToFinLt (count (> i) ns') @{believe_me Oh} :: invtable (S i) ns _

142 | public export

143 | compose : Permutation n -> Permutation n -> Permutation n

144 | compose [] [] = []

145 | compose [_] [_] = [FZ]

146 | compose p p' =

147 |   let ns = permSeq p

148 |       ns' = permSeq p'

149 |   in fromJust (fromPermSeq $ map (`index` ns) ns') @{believe_me $ ItIsJust {x=()}}

155 | public export

156 | horiz : Permutation m -> Permutation n -> Permutation (m + n)

157 | horiz [] p' = p'

158 | horiz (i :: is) p' = weakenN n i :: horiz is p'

166 | public export

167 | permuteVect : Permutation n -> Vect n a -> Vect n a

168 | permuteVect [] [] = []

169 | permuteVect [_] [x] = [x]

170 | permuteVect p xs =

171 |   let invt = permSeq $ inverse p

172 |   in map (`index` xs) invt

175 | public export

176 | permuteList : (xs : List a) -> Permutation (length xs) -> List a

177 | permuteList [] [] = []

178 | permuteList [x] [_] = [x]

179 | permuteList xs p =

180 |   let invt = toList $ permSeq $ inverse p

181 |   in map (index' xs) invt

184 | public export

185 | permuteHVect : {0 ts : Vect n _} -> (p : Permutation n) ->

186 |                 All q ts -> All q (permuteVect p ts)

187 | permuteHVect [] [] = []

188 | permuteHVect [_] [x] = [x]

189 | permuteHVect p xs =

190 |   replace {p = Vect.Quantifiers.All.All q} (believe_me $ Refl {x=()}) $

191 |     fromVect $ permuteVect p $ toVect xs

192 |   where

193 |     toVect : forall n. {0 ts : Vect n _} -> All q ts -> Vect n (Exists q)

194 |     toVect [] = []

195 |     toVect (x :: xs) = Evidence _ x :: toVect xs

197 |     fromVect : forall n. (xs : Vect n (Exists q)) -> All q (map Exists.fst xs)

198 |     fromVect [] = []

199 |     fromVect (Evidence _ x :: xs) = x :: fromVect xs

202 | public export

203 | permuteHList : {0 ts : List _} -> (p : Permutation (length ts)) ->

204 |                 All q ts -> All q (permuteList ts p)

205 | permuteHList [] [] = []

206 | permuteHList [_] [x] = [x]

207 | permuteHList p xs =

208 |   replace {p = List.Quantifiers.All.All q} (believe_me $ Refl {x=()}) $

209 |     fromList $ permuteList (toList xs) $ replace {p = Permutation} (believe_me $ Refl {x=()}) p

210 |   where

211 |     toList : forall ts. All q ts -> List (Exists q)

212 |     toList [] = []

213 |     toList (x :: xs) = Evidence _ x :: toList xs

215 |     fromList : (xs : List (Exists q)) -> All q (map Exists.fst xs)

216 |     fromList [] = []

217 |     fromList (Evidence _ x :: xs) = x :: fromList xs

228 | permSeqInv : (p : Permutation n) -> fromPermSeq (permSeq p) = Just p

229 | permSeqInv p = believe_me $ Refl {x = Just p}

232 | fromPermSeqInv : (seq : Vect n (Fin n)) -> IsJust (fromPermSeq seq) ->

233 |                   permSeq (fromJust (fromPermSeq seq)) = seq

234 | fromPermSeqInv seq prf = believe_me $ Refl {x=seq}

237 | lehmerCodeBounded : (p : Permutation n) -> So (lehmerCode p >= 0 && lehmerCode p < factorial (natToInteger n))

238 | lehmerCodeBounded _ = believe_me Oh

241 | lehmerCodeInv : (p : Permutation n) -> fromLehmerCode (lehmerCode p) @{lehmerCodeBounded p} = p

242 | lehmerCodeInv p = believe_me $ Refl {x=p}

245 | lehmerCodeId : lehmerCode (identity {n}) = 0

246 | lehmerCodeId = believe_me $ Refl {x=0}

249 | fromLehmerCodeInv : (x : Integer) -> So (x >= 0 && x < factorial (natToInteger n)) => lehmerCode (fromLehmerCode {n} x) = x

250 | fromLehmerCodeInv x = believe_me $ Refl {x}

254 | compAssoc : (p,q,r : Permutation n) -> compose (compose p q) r = compose p (compose q r)

255 | compAssoc p q r = believe_me $ Refl {x = compose p (compose q r)}

258 | compIdLeft : (p : Permutation n) -> compose (identity {n}) p = p

259 | compIdLeft p = believe_me $ Refl {x=p}

262 | compIdRight : (p : Permutation n) -> compose (identity {n}) p = p

263 | compIdRight p = believe_me $ Refl {x=p}

266 | compInvLeft : (p : Permutation n) -> compose (inverse p) p = identity {n}

267 | compInvLeft p = believe_me $ Refl {x = identity {n}}

270 | compInvRight : (p : Permutation n) -> compose p (inverse p) = identity {n}

271 | compInvRight p = believe_me $ Refl {x = identity {n}}

275 | congCons : (0 _ : i ~=~ j) -> (0 _ : p ~=~ q) ->

276 |             Permutation.(::) i p ~=~ Permutation.(::) j q

277 | congCons Refl Refl = Refl

279 | fzRefl : (0 _ : m = n) -> Fin.FZ {k=m} ~=~ Fin.FZ {k=n}

280 | fzRefl Refl = Refl

282 | congFS : (0 _ : i ~=~ j) -> Fin.FS i ~=~ Fin.FS j

283 | congFS Refl = Refl

287 | horizBothId : {m : _} -> horiz (identity {n=m}) (identity {n}) = identity {n = m + n}

288 | horizBothId {m=0} = Refl

289 | horizBothId {m=S _} = cong (FZ ::) horizBothId

292 | horizComp : (p,p' : Permutation m) -> (q,q' : Permutation n) ->

293 |             horiz (compose p p') (compose q q') = compose (horiz p q) (horiz p' q')

294 | horizComp p p' q q' = believe_me $ Refl {x = compose (horiz p q) (horiz p' q')}

297 | horizAssoc : (p : Permutation m) -> (q : Permutation n) -> (r : Permutation o) ->

298 |               horiz (horiz p q) r ~=~ horiz p (horiz q r)

299 | horizAssoc [] q r = Refl

300 | horizAssoc (i :: p) q r = congCons (weakenPlus i) (horizAssoc p q r)

301 |   where

302 |     weakenPlus : (x : Fin _) -> weakenN o (weakenN n x) ~=~ weakenN (n + o) x

303 |     weakenPlus FZ = fzRefl (sym $ plusAssociative _ _ _)

304 |     weakenPlus (FS x) = congFS (weakenPlus x)

307 | horizUnitl : (p : Permutation n) -> horiz [] p = p

308 | horizUnitl _ = Refl

311 | horizUnitr : (p : Permutation n) -> horiz p [] ~=~ p

312 | horizUnitr [] = Refl

313 | horizUnitr (i :: p) = congCons (weakenZ i) (horizUnitr p)

314 |   where

315 |     weakenZ : (x : Fin _) -> weakenN 0 x ~=~ x

316 |     weakenZ FZ = fzRefl (plusZeroRightNeutral _)

317 |     weakenZ (FS x) = congFS (weakenZ x)

321 | permuteVectId : (xs : Vect n a) -> permuteVect Permutation.identity xs = xs

322 | permuteVectId xs = believe_me $ Refl {x=xs}

325 | permuteVectComp : (p,q : Permutation n) -> (xs : Vect n a) ->

326 |                   permuteVect (compose p q) xs = permuteVect p (permuteVect q xs)

327 | permuteVectComp p q xs = believe_me $ Refl {x = permuteVect (compose p q) xs}

330 | permuteVectHoriz : (p : Permutation m) -> (xs : Vect m a) -> (q : Permutation n) -> (ys : Vect n a) ->

331 |                     permuteVect p xs ++ permuteVect q ys = permuteVect (horiz p q) (xs ++ ys)

332 | permuteVectHoriz p xs q ys = believe_me $ Refl {x = permuteVect (horiz p q) (xs ++ ys)}

335 | permuteListId : (xs : List a) -> permuteList xs Permutation.identity = xs

336 | permuteListId xs = believe_me $ Refl {x=xs}

339 | permuteListLength : (xs : List a) -> (p : Permutation _) -> length (permuteList xs p) = length xs

340 | permuteListLength xs p = believe_me $ Refl {x = length xs}

343 | permuteListComp : (xs : List a) -> (p,q : Permutation _) ->

344 |                   permuteList xs (compose p q)

345 |                   = permuteList (permuteList xs q) (rewrite permuteListLength xs q in p)

346 | permuteListComp xs p q = believe_me $ Refl {x = permuteList xs (compose p q)}