Some proofs of simple things from set theory, including how to define power sets and subsets. All in Idris.

set-proof-example.idr

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)

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.