# 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:

### 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:

### functional

`(functional [R (rel T U)])`
``````(forall [x T] (q/unique (lambda [y U] (R x y))))
``````

Definition:

### funrel

`(funrel [f (==> T U)])`
``````(lambda [x T] (lambda [y U] (equal (f x) y)))
``````

Definition: The relation corresponding to function `f`.

### funrel-functional

`(funrel-functional [f (==> T U)])`
``````(functional (funrel f))
``````

Theorem:

### 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. `s1``s2`.

### 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:

### relfun

`(relfun [R (rel T U)] [fproof (functional R)])`
``````(lambda [x T] (q/the (fproof x)))
``````

Definition: The function corresponding to a total, functional relation.

### relfun-img

`(relfun-img [R (rel T U)] [fproof (functional R)])`
``````(forall
[x T]
(forall [y U] (==> (R x y) (equal ((relfun R fproof) x) y))))
``````

Theorem: The image of a functional relation

### relfun-img-prop

`(relfun-img-prop [R (rel T U)] [fproof (functional R)])`
``````(forall [x T] (R x ((relfun R fproof) x)))
``````

Theorem: The property of the relational/functional image.

### relfunrel-equal

`(relfunrel-equal [f (==> T U)])`
``````(equal f (relfun (funrel f) (funrel-functional f)))
``````

Theorem: This is the intentional variant of relfunrel-ext-equal.

### relfunrel-ext-equal

`(relfunrel-ext-equal [f (==> T U)])`
``````(forall
[x T]
(equal (f x) ((relfun (funrel f) (funrel-functional f)) x)))
``````

Theorem: This is the extensional equality of a function `f` and its relational characterization.

### 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. `R1``R2`

### 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.