idris proofs: a tale of alists with guaranteed unique values and a bunch of misc

  • How to actually use absurd.
  • How to use the “No contra” result from DecEq in a with rule.
  • How to use Idris’ DPair.
module Data.AListimport Data.Bool
import Decidable.Equality
keyInList : Eq a => a -> List (Pair a b) -> Bool
keyInList k [] = False
keyInList k ((k1, v1) :: others) =
if k == k1 then
True
else
keyInList k others
allKeysUniqueInList : Eq a => List (Pair a b) -> Bool
allKeysUniqueInList [] = True
allKeysUniqueInList ((k, v) :: others) =
let
headIsUnique = not (keyInList k others)
tailsAreUnique = allKeysUniqueInList others
in
tailsAreUnique && headIsUnique
kvCons : a -> b -> List (Pair a b) -> List (Pair a b)
kvCons k v l = (k,v) :: l
appendBreak : Eq a => (k : a) -> (v : b) -> (l : List (Pair a b)) -> (p : allKeysUniqueInList l = True) -> (DPair (List (Pair a b)) (\l => allKeysUniqueInList l = True))
appendBreak k v l p with (decEq (keyInList k l) True)
appendBreak k v l p | Yes prf = (l ** p)
appendBreak k v l p | No contra =
let
cproof = invertContraBool (keyInList k l) True contra
in
(kvCons k v l ** outProof k l p cproof)
where
outProof : (k : a) -> (l : List (Pair a b)) -> (p : allKeysUniqueInList l = True) -> (kp : not (keyInList k l) = True) -> (allKeysUniqueInList l && not (keyInList k l) = True)
outProof k l p kp =
rewrite kp in
rewrite p in
Refl
public export
proveList : Eq a => (l : List (Pair a b)) -> Maybe (DPair (List (Pair a b)) (\l => allKeysUniqueInList l = True))
proveList l with (decEq (allKeysUniqueInList l) True)
proveList l | Yes prf = Just (l ** prf)
proveList l | No _ = Nothing
public export
addIfUnique : Eq a => (k : a) -> (v : b) -> (l : DPair (List (Pair a b)) (\l => allKeysUniqueInList l = True)) -> DPair (List (Pair a b)) (\l => allKeysUniqueInList l = True)
addIfUnique k v (l ** p) = appendBreak k v l p
---------------------------------------
-- Decidability specialized on bool
---------------------------------------
||| You can reverse decidability when bool is involved.
-- Given a contra on bool equality (a = b) -> Void, produce a proof of the opposite (that (not a) = b)
public export
invertContraBool : (a : Bool) -> (b : Bool) -> (a = b -> Void) -> (not a = b)
invertContraBool False False contra = absurd $ contra Refl
invertContraBool False True contra = Refl
invertContraBool True False contra = Refl
invertContraBool True True contra = absurd $ contra Refl
Idris’ documentation for Prelude.Uninhabited, including the “absurd” function and Uninhabited typeclass.
public export
invertContraBool : (a : Bool) -> (b : Bool) -> (a = b -> Void) -> (not a = b)
invertContraBool False False contra = absurd $ contra Refl
public export
invertContraBool : (a : Bool) -> (b : Bool) -> (a = b -> Void) -> (not a = b)
invertContraBool a b contra = invertContraBool_ a b contra
where
fEf : False = False
fEf = Refl
tEt : True = True
tEt = Refl
invertContraBool_ : (a : Bool) -> (b : Bool) -> (a = b -> Void) -> (not a = b)
invertContraBool_ False False contra = absurd (contra fEf)
invertContraBool_ False True contra = Refl
invertContraBool_ True False contra = Refl
invertContraBool_ True True contra = absurd (contra tEt)
appendBreak : Eq a => (k : a) -> (v : b) -> (l : List (Pair a b)) -> (p : allKeysUniqueInList l = True) -> (DPair (List (Pair a b)) (\l => allKeysUniqueInList l = True))
appendBreak k v l p with (decEq (keyInList k l) True)
appendBreak k v l p | Yes prf = (l ** p)
appendBreak k v l p | No contra =
let
cproof = invertContraBool (keyInList k l) True contra
in
(kvCons k v l ** outProof k l p cproof)
where
outProof : (k : a) -> (l : List (Pair a b)) -> (p : allKeysUniqueInList l = True) -> (kp : not (keyInList k l) = True) -> (allKeysUniqueInList l && not (keyInList k l) = True)
outProof k l p kp =
rewrite kp in
rewrite p in
Refl
cproof : not (keyInList k l) = True
cproof = invertContraBool (keyInList k l) True contra
outProof : (k : a) -> (l : List (Pair a b)) -> (p : allKeysUniqueInList l = True) -> (kp : not (keyInList k l) = True) -> (allKeysUniqueInList l && not (keyInList k l) = True)
outProof k l p kp =
rewrite kp in
rewrite p in
Refl
allKeysUniqueInList ((k, v) :: others) =
let
headIsUnique = not (keyInList k others)
tailsAreUnique = allKeysUniqueInList others
in
tailsAreUnique && headIsUnique
proofPair : (v : a) -> (f : a -> Bool) -> (p : f v = True) -> (v ** f v = True)
proofPair v f p = MkDPair v p
λΠ> :t proofPair
Data.AList.proofPair : (v : a) -> (f : (a -> Bool)) -> f v = True -> DPair a (\v => f v = True)
DPair (List (Pair a b)) (\l => allKeysUniqueInList l = True)
addIfUnique k v (l ** p) = appendBreak k v l p -- Good
addIfUnique k v (MkDPair l p) = appendBreak k v l p-- also good
public export
proveList : Eq a => (l : List (Pair a b)) -> Maybe (DPair (List (Pair a b)) (\l => allKeysUniqueInList l = True))
proveList l with (decEq (allKeysUniqueInList l) True)
proveList l | Yes prf = Just (l ** prf) -- (MkDPair l prf) works too
proveList l | No _ = Nothing

--

--

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store