latte-sets.rel

A relation from elements of a given type T to elements of U is formalized with type (==> T U :type).

This namespace provides some important properties about such relations.

dom

(dom [R (rel T U)])
(set-of [x T] (exists [y U] (R x y)))

Definition: The domain of relation R.

emptyrel

(emptyrel [T :type] [U :type])
(lambda [x T] (lambda [y U] p/absurd))

Definition: The empty relation.

emptyrel-prop

(emptyrel-prop [T :type] [U :type])
(forall [x T] (forall [y U] (not ((emptyrel T U) x y))))

Theorem:

equivalence

(equivalence [R (rel T T)])
(and* (reflexive R) (symmetric R) (transitive R))

Definition: An equivalence relation.

fetch-rel-type

(fetch-rel-type def-env ctx r-type)

fullrel

(fullrel [T :type] [U :type])
(lambda [x T] (lambda [y U] p/truth))

Definition: The full (total) relation between T and U.

fullrel-prop

(fullrel-prop [T :type] [U :type])
(forall [x T] (forall [y U] ((fullrel T U) x y)))

Theorem:

ident-equiv

(ident-equiv [T :type])
(equivalence (identity T))

Theorem: The indentity on T is an equivalence relation.

ident-refl

(ident-refl [T :type])
(reflexive (identity T))

Theorem:

ident-sym

(ident-sym [T :type])
(symmetric (identity T))

Theorem:

ident-trans

(ident-trans [T :type])
(transitive (identity T))

Theorem:

identity

(identity [T :type])
(lambda [x y T] (equal x y))

Definition: The indentity relation on T.

prod

(prod [s1 (set T)] [s2 (set U)])
(lambda [x T] (lambda [y U] (and (elem x s1) (elem y s2))))

Definition: The cartersian product of sets s1 and s2, i.e. s1s2.

psubrel

(psubrel [R1 (rel T U)] [R2 (rel T U)])
(and (subrel R1 R2) (not (releq R1 R2)))

Definition: The anti-reflexive variant of subrel.

psubrel-antirefl

(psubrel-antirefl [R (rel T U)])
(not (psubrel R R))

Theorem:

psubrel-antisym

(psubrel-antisym [R1 (rel T U)] [R2 (rel T U)])
(not (and (psubrel R1 R2) (psubrel R2 R1)))

Theorem:

psubrel-emptyrel

(psubrel-emptyrel [R (rel T U)])
(==> (psubrel (emptyrel T U) R) (not (releq R (emptyrel T U))))

Theorem:

psubrel-emptyrel-conv

(psubrel-emptyrel-conv [R (rel T U)])
(==> (not (releq R (emptyrel T U))) (psubrel (emptyrel T U) R))

Theorem:

psubrel-emptyrel-equiv

(psubrel-emptyrel-equiv [R (rel T U)])
(<=> (psubrel (emptyrel T U) R) (not (releq R (emptyrel T U))))

Theorem:

psubrel-trans

(psubrel-trans [R1 (rel T U)] [R2 (rel T U)] [R3 (rel T U)])
(==> (psubrel R1 R2) (psubrel R2 R3) (psubrel R1 R3))

Theorem:

ran

(ran [R (rel T U)])
(set-of [y U] (exists [x T] (R x y)))

Definition: The range of relation R.

rcomp

(rcomp [R1 (rel T U)] [R2 (rel U V)])
(lambda [x T] (lambda [z V] (exists [y U] (and (R1 x y) (R2 y z)))))

Definition: Sequential relational composition.

rcomp-assoc

(rcomp-assoc [R1 (rel T U)] [R2 (rel U V)] [R3 (rel V W)])
(releq (rcomp R1 (rcomp R2 R3)) (rcomp (rcomp R1 R2) R3))

Theorem: Relational composition is associative.

rcomp-assoc-subrel

(rcomp-assoc-subrel [R1 (rel T U)] [R2 (rel U V)] [R3 (rel V W)])
(subrel (rcomp R1 (rcomp R2 R3)) (rcomp (rcomp R1 R2) R3))

Theorem:

rcomp-assoc-suprel

(rcomp-assoc-suprel [R1 (rel T U)] [R2 (rel U V)] [R3 (rel V W)])
(subrel (rcomp (rcomp R1 R2) R3) (rcomp R1 (rcomp R2 R3)))

Theorem:

refl-closure

(refl-closure [R (rel T T)])
(lambda [x y T] (or (R x y) (equal x y)))

Definition: The reflexive closure of relation R.

refl-closure-smallest

(refl-closure-smallest [R (rel T T)])
(forall
 [S (rel T T)]
 (==> (subrel R S) (reflexive S) (subrel (refl-closure R) S)))

Theorem:

refl-closure-sub

(refl-closure-sub [R (rel T T)])
(subrel R (refl-closure R))

Theorem:

reflexive

(reflexive [R (rel T T)])
(forall [x T] (R x x))

Definition: A reflexive relation.

reflexive-refl-closure

(reflexive-refl-closure [R (rel T T)])
(reflexive (refl-closure R))

Theorem:

rel

(rel [T :type] [U :type])
(==> T U :type)

Definition: The type of relations.

rel-equal

(rel-equal [R1 (rel T U)] [R2 (rel T U)])
(forall [P (==> (rel T U) :type)] (<=> (P R1) (P R2)))

Definition: A Leibniz-stype equality for relations.

It says that two relations R1 and R2 are equal iff for any predicate P then (P R1) if and only if (P R2).

Note that the identification with seteq is non-trivial, and requires an axiom.

rel-equal-implies-releq

(rel-equal-implies-releq [R1 (rel T U)] [R2 (rel T U)])
(==> (rel-equal R1 R2) (releq R1 R2))

Theorem:

rel-equal-implies-subrel

(rel-equal-implies-subrel [R1 (rel T U)] [R2 (rel T U)])
(==> (rel-equal R1 R2) (subrel R1 R2))

Theorem:

rel-equal-prop

(rel-equal-prop [R1 (rel T U)] [R2 (rel T U)] [P (==> (rel T U) :type)])
(==> (rel-equal R1 R2) (P R1) (P R2))

Theorem:

rel-equal-refl

(rel-equal-refl [R (rel T U)])
(rel-equal R R)

Theorem:

rel-equal-releq

(rel-equal-releq [R1 (rel T U)] [R2 (rel T U)])
(<=> (rel-equal R1 R2) (releq R1 R2))

Theorem: Coincidence of Leibniz-style and subset-based equality for relations.

rel-equal-sym

(rel-equal-sym [R1 (rel T U)] [R2 (rel T U)])
(==> (rel-equal R1 R2) (rel-equal R2 R1))

Theorem:

rel-equal-trans

(rel-equal-trans [R1 (rel T U)] [R2 (rel T U)] [R3 (rel T U)])
(==> (rel-equal R1 R2) (rel-equal R2 R3) (rel-equal R1 R3))

Theorem:

releq

(releq [R1 (rel T U)] [R2 (rel T U)])
(and (subrel R1 R2) (subrel R2 R1))

Definition: Subset-based equality on relations.

releq-implies-rel-equal

(releq-implies-rel-equal [R1 (rel T U)] [R2 (rel T U)])
(==> (releq R1 R2) (rel-equal R1 R2))

Axiom: As for the set case (cf. sets/seteq-implies-set-equal), going from the subset-based equality to the (thus more general) leibniz-style one requires an axiom.

releq-refl

(releq-refl [R (rel T U)])
(releq R R)

Theorem:

releq-sym

(releq-sym [R1 (rel T U)] [R2 (rel T U)])
(==> (releq R1 R2) (releq R2 R1))

Theorem:

releq-trans

(releq-trans [R1 (rel T U)] [R2 (rel T U)] [R3 (rel T U)])
(==> (releq R1 R2) (releq R2 R3) (releq R1 R3))

Theorem:

subrel

(subrel [R1 (rel T U)] [R2 (rel T U)])
(forall [x T] (forall [y U] (==> (R1 x y) (R2 x y))))

Definition: The subset ordering for relations, i.e. R1R2

subrel-emptyrel-lower-bound

(subrel-emptyrel-lower-bound [R (rel T U)])
(subrel (emptyrel T U) R)

Theorem: The empty relation is a subset of every other relations.

subrel-fullrel-upper-bound

(subrel-fullrel-upper-bound [R (rel T U)])
(subrel R (fullrel T U))

Theorem: The full relation is a superset of every other relations.

subrel-prop

(subrel-prop [P (==> T U :type)] [R1 (rel T U)] [R2 (rel T U)])
(==>
 (forall [x T] (forall [y U] (==> (R2 x y) (P x y))))
 (subrel R1 R2)
 (forall [x T] (forall [y U] (==> (R1 x y) (P x y)))))

Theorem: Preservation of properties on relational subsets.

subrel-refl

(subrel-refl [R (rel T U)])
(subrel R R)

Theorem:

subrel-trans

(subrel-trans [R1 (rel T U)] [R2 (rel T U)] [R3 (rel T U)])
(==> (subrel R1 R2) (subrel R2 R3) (subrel R1 R3))

Theorem:

symm-closure

(symm-closure [R (rel T T)])
(lambda [x y T] (or (R x y) (R y x)))

Definition: The symmetric closure of relation R.

symm-closure-smallest

(symm-closure-smallest [R (rel T T)])
(forall
 [S (rel T T)]
 (==> (subrel R S) (symmetric S) (subrel (symm-closure R) S)))

Theorem:

symm-closure-sub

(symm-closure-sub [R (rel T T)])
(subrel R (symm-closure R))

Theorem:

symmetric

(symmetric [R (rel T T)])
(forall [x y T] (==> (R x y) (R y x)))

Definition: A symmetric relation.

symmetric-symm-closure

(symmetric-symm-closure [R (rel T T)])
(symmetric (symm-closure R))

Theorem:

transitive

(transitive [R (rel T T)])
(forall [x y z T] (==> (R x y) (R y z) (R x z)))

Definition: A transitive relation.