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