Last active
September 16, 2019 16:51
Star
You must be signed in to star a gist
Idris translation of "Dependently typed programming with finite sets"
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
||| 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