Skip to content

Instantly share code, notes, and snippets.

@cheery
Last active September 16, 2019 16:51
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save cheery/696db4cd50370e19adaa77909eb6f908 to your computer and use it in GitHub Desktop.
Idris translation of "Dependently typed programming with finite sets"
||| The Idris translation of Denis Firsov's paper
||| "Dependently Typed Programming with Finite Sets"
||| http://firsov.ee/finset/finset.pdf
module FiniteSets
%default total
%access public export
-- This is after I did some cleanup and adapted some of the ideas into Idris.
-- It also aligns roughly with what I need right now.
||| Notion of a proposition: proofs are unique.
Prop : Type -> Type
Prop t = (p1:t) -> (p2:t) -> p1 = p2
||| Given some decidable property p, we can define
||| squashed version of it, a "quotient".
squish : (Dec p) -> Type
squish (Yes d) = ()
squish (No _) = Void
auto_check : (d:Dec p) -> {auto q:(squish d)} -> p
auto_check (Yes prf) {q = ()} = prf
auto_check (No contra) {q = q} = absurd q
Uninhabited (LTE (S n) n) where
uninhabited (LTESucc n) = uninhabited n
-- injective and surjective function definitions.
-- These don't seem to work too well with dependent types.
Injective : {t,u:Type} -> (t -> u) -> Type
Injective f {t} = (x,y:t) -> (f x = f y) -> (x = y)
-- I may change this.. it's more convenient with inverse function separate.
Surjective : {t,u:Type} -> (t -> u) -> Type
Surjective f {t} {u} = (y:u) -> (x:t ** f x = y)
||| Conditive statement is logically equivalent to it's contrapositive.
contrapositive : (a -> b) -> Not b -> Not a
contrapositive f nb a = nb (f a)
data Nth : (xs : List a) -> Type where
XZ : Nth (x :: xs)
XS : Nth xs -> Nth (x :: xs)
Uninhabited (Nth []) where
uninhabited XZ impossible
uninhabited (XS _) impossible
indexer : (xs:List t) -> Nth xs -> t
indexer [] n = absurd n
indexer (x :: xs) XZ = x
indexer (x :: xs) (XS y) = indexer xs y
nth : {xs:List t} -> Nth xs -> t
nth {xs} n = indexer xs n
DecEq (Nth xs) where
decEq XZ XZ = Yes Refl
decEq XZ (XS _) = No (\a => case a of Refl impossible)
decEq (XS _) XZ = No (\a => case a of Refl impossible)
decEq (XS x) (XS y) = case decEq x y of
(Yes prf) => Yes (cong prf)
(No contra) => No (\a => case a of Refl => contra Refl)
||| Proof of no duplicates in a list.
NoDup : List t -> Type
NoDup xs = Injective (indexer xs)
-- ||| Proofs that there are no duplicates in a given list.
-- NoDup : {t : Type} -> List t -> Type
-- NoDup {t} xs = (x : t) -> Prop (x ∈ xs)
||| List containment is a convenience.
data In : a -> (xs : List a) -> Type where
Here : In x (x :: xs)
There : In y xs -> In y (x :: xs)
at_nth : {xs:List t} -> (x:Nth xs) -> In (nth x) xs
at_nth XZ = Here
at_nth (XS k) = There (at_nth k)
index_of : In x xs -> Nth xs
index_of Here = XZ
index_of (There k) = XS (index_of k)
index_of_valid : (k:Nth xs) -> index_of (at_nth k) = k
index_of_valid XZ = Refl
index_of_valid (XS y) = cong {f=XS} (index_of_valid y)
Uninhabited (In x []) where
uninhabited Here impossible
uninhabited (There _) impossible
||| Proof that list/set contains every inhabitant.
All : (t : Type) -> List t -> Type
All t xs = (x : t) -> (x `In` xs)
||| Type is listable if there's an enumeration of all values in it.
||| The definition is made bit more usable with requiring 'NoDup'.
Listable : (t : Type) -> Type
Listable t = (xs : List t ** (All t xs, NoDup xs))
||| All indexers are injective.
all_injective : (f:All t xs) -> (x:t) -> (y:t) -> (f x = f y) -> (x = y)
all_injective f x y prf with (f x, f y) proof fxy
all_injective f x x Refl | (Here, Here) = Refl
all_injective f x x Refl | (Here, There _) = Refl
all_injective f x x Refl | (There _, Here) = Refl
all_injective f x x Refl | (There _, There _) = Refl
interface DecIn t where
total decIn : (x : t) -> (xs:List t) -> Dec (x `In` xs)
not_here_or_there : Not (x = y) -> Not (In x ys) -> In x (y::ys) -> Void
not_here_or_there x y Here = x Refl
not_here_or_there x y (There z) = y z
||| With decidable equality you have decidable inclusion.
DecEq t => DecIn t where
decIn x [] = No uninhabited
decIn x (y::ys) = case decEq x y of
(Yes Refl) => Yes Here
(No x_not_y) => case decIn x ys of
(Yes that) => Yes (There that)
(No x_not_in_ys) => No (not_here_or_there x_not_y x_not_in_ys)
||| Remove duplicates from a list
remdup : (DecIn t) => List t -> List t
remdup [] = []
remdup (x :: xs) = case decIn x xs of
(Yes _) => remdup xs
(No _) => x :: remdup xs
||| remdup does not remove items from list.
remdup_complete : (DecIn t) => (x : t) -> (xs : List t)
-> (x `In` xs) -> (x `In` remdup xs)
remdup_complete x [] xin = absurd xin
remdup_complete z (z :: xs) Here with (decIn z xs)
remdup_complete z (z :: xs) Here | (Yes zin) = remdup_complete z xs zin
remdup_complete z (z :: xs) Here | (No _) = Here
remdup_complete x (z :: xs) (There xin) with (decIn z xs)
remdup_complete x (z :: xs) (There xin) | (Yes zin) = remdup_complete x xs xin
remdup_complete x (z :: xs) (There xin) | (No contra) = There (remdup_complete x xs xin)
||| remdup does not add new items into the list.
remdup_sound : (DecIn t) => (x : t) -> (xs : List t)
-> (x `In` remdup xs) -> x `In` xs
remdup_sound x [] inrd = absurd inrd
remdup_sound x (z :: xs) inrd with (decIn z xs)
remdup_sound x (z :: xs) inrd | (Yes _) = There (remdup_sound x xs inrd)
remdup_sound z (z :: xs) Here | (No _) = Here
remdup_sound x (z :: xs) (There inrd) | (No _) = There (remdup_sound x xs inrd)
||| remDup does what we expect it to do.
remdup_progress : (DecIn t) => (xs : List t)
-> NoDup (remdup xs)
remdup_progress [] xn _ _ = absurd xn
remdup_progress (x :: xs) xn yn pf with (decIn x xs)
remdup_progress (x :: xs) xn yn pf | (Yes prf) = remdup_progress xs xn yn pf
remdup_progress (x :: xs) XZ XZ pf | (No contra) = Refl
remdup_progress (x :: xs) XZ (XS yn) pf | (No contra) =
absurd (contra (remdup_sound x xs (rewrite pf in at_nth yn)))
remdup_progress (x :: xs) (XS xn) XZ pf | (No contra) =
absurd (contra (remdup_sound x xs (rewrite sym pf in at_nth xn)))
remdup_progress (x :: xs) (XS xn) (XS yn) pf | (No contra) =
cong (remdup_progress xs xn yn pf)
||| In an empty list, there are no duplicates.
empty_dnd : NoDup []
empty_dnd x p1 p2 = absurd p1
indexer_theorem : (xin:In x xs) -> indexer xs (index_of xin) = x
indexer_theorem {xs = []} xin = absurd xin
indexer_theorem {xs = (x :: xs)} Here = Refl
indexer_theorem {xs = (y :: xs)} (There xin) = indexer_theorem xin
indexer_theorem_2 : (x:t) -> (z:Nth xs) -> (x = indexer xs z) -> (x `In` xs)
indexer_theorem_2 x XZ prf = rewrite sym prf in Here
indexer_theorem_2 x (XS z) prf = There (indexer_theorem_2 x z prf)
prove_dnd : (x:t) -> (xsdnd : NoDup xs) -> (x_not_in_xs : In x xs -> Void)
-> (y : Nth (x :: xs)) -> (z : Nth (x :: xs)) -> (indexer (x :: xs) y = indexer (x :: xs) z) -> y = z
prove_dnd x xsdnd x_not_in_xs XZ XZ prf = Refl
prove_dnd x xsdnd x_not_in_xs XZ (XS z) prf = absurd (x_not_in_xs (indexer_theorem_2 x z prf))
prove_dnd x xsdnd x_not_in_xs (XS y) XZ prf = absurd (x_not_in_xs (indexer_theorem_2 x y (sym prf)))
prove_dnd x xsdnd x_not_in_xs (XS y) (XS z) prf = cong (xsdnd y z prf)
||| Decide whether there are no duplicates in a list.
dec_dnd : (DecEq t) => (xs : List t) -> Dec (NoDup xs)
dec_dnd [] = Yes empty_dnd
dec_dnd (x :: xs) = case decIn x xs of
(Yes xin) => No (\assum =>
case assum (XS (index_of xin)) XZ (indexer_theorem xin) of Refl impossible)
(No x_not_in_xs) => case dec_dnd xs of
(No xs_not_dnd) => No (\xsdnd => absurd$xs_not_dnd (\zin1,zin2,zpf =>
case xsdnd (XS zin1) (XS zin2) zpf of Refl => Refl))
(Yes xsdnd) => Yes (prove_dnd x xsdnd x_not_in_xs)
data Set : (t -> Type) -> Type where
H : (xs:List t)
-> .{complete:(x:t) -> p x -> x `In` xs} -- These are hidden, so that
-> .{sound:(x:t) -> x `In` xs -> p x} -- the whole thing doesn't
-> .{dnd:NoDup xs} -- fly at our face in REPL.
-> Set p
%name Set s1, s2, s3
||| Set elements are values from an entire list.
entire : List t -> t -> Type
entire xs x = x `In` xs
from_list : DecEq t => (xs:List t) -> Set (entire xs)
from_list xs = H (remdup xs)
{complete=(\x, p_x => remdup_complete x xs p_x)}
{sound=(\x, xin => remdup_sound x xs xin)}
{dnd=(remdup_progress xs)}
Sized (Set a) where
size (H xs) = length xs
||| Pick value from a list satisfying some property.
pick : {p:t -> Type} -> (f:(x:t) -> Dec (p x)) -> List t -> Maybe t
pick f [] = Nothing
pick f (x :: xs) = case f x of
(Yes _) => Just x
(No _) => pick f xs
pick_complete : {p:t -> Type} -> (f:(x:t) -> Dec (p x)) -> (xs:List t)
-> (pick f xs = Nothing) -> (x:t) -> p x -> (x `In` xs) -> Void
pick_complete f [] comp x fxt xin = absurd xin
pick_complete f (w :: xs) comp x fxt xin with (f w)
pick_complete _ (_ :: _) Refl _ _ _ | (Yes _) impossible
pick_complete f (x :: xs) comp x fxt Here | (No contra) = contra fxt
pick_complete f (w :: xs) comp x fxt (There xin) | (No contra) =
pick_complete f xs comp x fxt xin
pick_sound : {p:t -> Type} -> (f:(x:t) -> Dec (p x)) -> (xs:List t)
-> (x:t) -> (pick f xs = Just x) -> (x `In` xs)
pick_sound f [] x prf = absurd prf
pick_sound f (y :: xs) x prf with (f y)
pick_sound f (x :: xs) x Refl | (Yes py) = Here
pick_sound f (y :: xs) x prf | (No contra) = There (pick_sound f xs x prf)
pick_progress : {p:t -> Type} -> (f:(x:t) -> Dec (p x)) -> (xs:List t)
-> (x:t) -> (pick f xs = Just x) -> (p x)
pick_progress f [] x prf = absurd prf
pick_progress f (y :: xs) x prf with (f y)
pick_progress f (x :: xs) x Refl | (Yes z) = z
pick_progress f (y :: xs) x prf | (No contra) = pick_progress f xs x prf
||| Locates a value from set, matching some value.
locate : {p,q:t -> Type} -> (f:(x:t) -> Dec (q x)) -> Set p -> Maybe t
locate {t} f (H xs) = pick f xs
locate_complete : {p,q:t -> Type} -> (f:(x:t) -> Dec (q x)) -> (s1:Set p)
-> locate f s1 = Nothing -> ((x:t) -> p x -> q x -> Void)
locate_complete {q} f (H xs {complete}) prf x px qx =
pick_complete {p=q} f xs prf x qx (complete x px)
locate_sound : {p,q:t -> Type} -> (f:(x:t) -> Dec (q x)) -> (s1:Set p)
-> (x:t) -> locate f s1 = Just x -> (p x)
locate_sound {q} f (H xs {sound}) x prf =
sound x (pick_sound {p=q} f xs x prf)
locate_progress : {p,q:t -> Type} -> (f:(x:t) -> Dec (q x)) -> (s1:Set p)
-> (x:t) -> locate f s1 = Just x -> (q x)
locate_progress {q} f (H xs) x prf =
pick_progress {p=q} f xs x prf
conj : (p,q:t -> Type) -> t -> Type
conj p q x = (p x, q x)
every : {p:t -> Type} -> (f:(x:t) -> Dec (p x)) -> List t -> List t
every f [] = []
every f (x :: xs) = case f x of
(Yes _) => x :: every f xs
(No _) => every f xs
every_complete : {p:t -> Type} -> (f:(x:t) -> Dec (p x)) -> (xs:List t)
-> (x:t) -> p x -> (x `In` xs) -> (x `In` every f xs)
every_complete f [] x y z = z
every_complete f (w :: xs) x px xin with (f w)
every_complete f (x :: xs) x px Here | (Yes prf) = Here
every_complete f (w :: xs) x px (There xin) | (Yes prf) = There (every_complete f xs x px xin)
every_complete f (x :: xs) x px Here | (No contra) = absurd (contra px)
every_complete {p} f (w :: xs) x px (There xin) | (No contra) = every_complete f xs x px xin
every_sound : {p:t -> Type} -> (f:(x:t) -> Dec (p x)) -> (xs:List t)
-> (x:t) -> (x `In` every f xs) -> (x `In` xs)
every_sound f [] x xin = xin
every_sound f (z :: xs) x xin with (f z)
every_sound f (x :: xs) x Here | (Yes pz) = Here
every_sound f (z :: xs) x (There xin) | (Yes pz) = There (every_sound f xs x xin)
every_sound f (z :: xs) x xin | (No contra) = There (every_sound f xs x xin)
every_progress : {p:t -> Type} -> (f:(x:t) -> Dec (p x)) -> (xs:List t)
-> (x:t) -> (x `In` every f xs) -> (p x)
every_progress f [] x xin = absurd xin
every_progress f (z :: xs) x xin with (f z)
every_progress f (x :: xs) x Here | (Yes p_x) = p_x
every_progress f (z :: xs) x (There xin) | (Yes p_z) = every_progress f xs x xin
every_progress f (_ :: xs) x xin | (No _) = every_progress f xs x xin
dnd_tail : NoDup (x::xs) -> NoDup (xs)
dnd_tail dnd xin yin fxfy = case dnd (XS xin) (XS yin) fxfy of Refl => Refl
nth_index_of : (k:In x xs) -> x = nth (index_of k)
nth_index_of Here = Refl
nth_index_of (There y) = nth_index_of y
every_dnd : {p:t -> Type} -> (f:(x:t) -> Dec (p x)) -> (xs:List t)
-> NoDup xs -> NoDup (every f xs)
every_dnd f [] dnd xin yin fxfy = dnd xin yin fxfy
every_dnd f (y :: xs) dnd xin yin fxfy with (f y)
every_dnd f (y :: xs) dnd XZ XZ fxfy | (Yes prf) = Refl
every_dnd f (y :: xs) dnd XZ (XS yin) fxfy | (Yes prf) =
case every_sound f xs y (indexer_theorem_2 y yin fxfy) of
yin2 => case dnd XZ (XS (index_of yin2)) (nth_index_of yin2) of
Refl impossible
every_dnd f (y :: xs) dnd (XS xin) XZ fxfy | (Yes prf) =
case every_sound f xs y (indexer_theorem_2 y xin (sym fxfy)) of
xin2 => case dnd XZ (XS (index_of xin2)) (nth_index_of xin2) of
Refl impossible
every_dnd f (y :: xs) dnd (XS xin) (XS yin) fxfy | (Yes prf) =
case every_dnd f xs (dnd_tail dnd {xs=xs}) xin yin fxfy of Refl => Refl
every_dnd f (y :: xs) dnd xin yin fxfy | (No contra) =
every_dnd f xs (dnd_tail dnd {xs=xs}) xin yin fxfy
subset : {p,q:t -> Type} -> ((x:t) -> Dec (q x)) -> Set p -> Set (conj p q)
subset {q} f (H xs {complete} {sound} {dnd}) = H (every {p=q} f xs)
{complete=(\x, (p_x,q_x) => every_complete {p=q} f xs x q_x (complete x p_x))}
{sound=(\x, xin => (sound x (every_sound {p=q} f xs x xin),
every_progress {p=q} f xs x xin))}
{dnd=(every_dnd {p=q} f xs dnd)}
-- TODO: The next task is to prove that the set is going to shrink if it is quaranteed to lose an item.
subset_shrinks : {p,q:t -> Type} -> ((x:t) -> Dec (q x))
-> (x:t) -> (p x) -> (Not (q x))
-> (s1:Set p)
-> (s2:Set (conj p q))
-> (size s2) `Smaller` (size s1)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment