Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Some proofs of simple things from set theory, including how to define power sets and subsets. All in Idris.
module Set2
--
-- This module has some proofs of things from set theory. Inspired by
-- chapter 13 of the book Type Theory and Formal Proofs.
--
-- A power set of some given set s.
PowerSet : (s : Type) -> Type
PowerSet s = s -> Type
-- | A predicate that says whether a given x is an element of the powerset v.
Element : {s : Type} -> (x : s) -> (v : PowerSet s) -> Type
Element x v = v x
-- | A predicate that says whether v is a subset of w.
Subset : {s : Type} -> (v : PowerSet s) -> (w : PowerSet s) -> Type
Subset {s} v w = (x : s) -> Element x v -> Element x w
-- | A function for creating a new subset of a given s that is the complement
-- of a subset v.
Complement : {s : Type} -> PowerSet s -> PowerSet s
Complement {s} v x = Not (Element x v)
-- | A function for creating a set which is the difference between two subsets
-- of s.
Difference : {s : Type} -> PowerSet s -> PowerSet s -> PowerSet s
Difference v w x = (Element x v, Not (Element x w))
-- | A predicate for determining if two subsets of some s are equal.
IS : {s : Type} -> (v : PowerSet s) -> (w : PowerSet s) -> Type
IS v w = (Subset v w, Subset w v)
-- A proof that says if you have two subsets of s, v and w, then for all
-- elements of s y, if y is an element of the difference of v and w, then y is
-- a element of v.
proofdiffsub : {s : Type} -> (myv : PowerSet s) -> (myw : PowerSet s) -> (y : s) -> Difference myv myw y -> Element y myv
proofdiffsub _ _ _ (myvy, _) = myvy
-- | A proof that says if you are given two subsets of s, v and w, and you know
-- that v is a subset of the complement of w, then for all x in s, if you know
-- that x is a element of v, then you know that x is an element of the
-- difference between v and w.
proofdiffcompl : {s : Type} -> (vv : PowerSet s) -> (ww : PowerSet s) -> Subset vv (Complement ww) -> (x : s) -> Element x vv -> Difference vv ww x
proofdiffcompl vv ww subcompl x vvx = (vvx, subcompl x vvx)
-- | A proof that if you have two subsets of a given s, v and w, and you know v
-- is a subset of the complement of w, then you know that the difference
-- between v and w is the same as v itself.
proofdiff : {s : Type} -> (v : PowerSet s) -> (w : PowerSet s) -> Subset v (Complement w) -> IS (Difference v w) v
proofdiff {s} v w subcompl = (proofdiffsub v w, proofdiffcompl v w subcompl)
@cdepillabout

This comment has been minimized.

Copy link
Owner Author

@cdepillabout cdepillabout commented Dec 4, 2018

These can be loaded into idris by using :l from the repl after running it with the following command:

$ nix-shell -p idris --run idris

This is using whatever version of idris is in the nixpkgs from NixOS-18.09 from around 2018-12-04.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment