Next: Relation closures Up: Relations Previous: Relations

Definitions

relations.l uses the obvious definitions of binary relations and unary predicates to do a little algebra with the equality on relations given by pointwise (extensional) equality, induced by a pre-order given by inclusion. The logical operators and, or etc lift to relations, and we also have the tensor product composeRel and its left and right adjoints across the pre-order, impliesRel coimpliesRel, familiar as Hoare/He's weakest pre-specification etc. These may also be considered in the context of predicates, and functions-as-relations, giving existsfPred and so on. These are then used to prove sound a variety of obvious algebraic laws, and as an application to define "the transitive interior" of a relation.
``` ** Module lib_rel Imports lib_nat
Pred = ... : (Type)->Type
Rel = ... : (Type)->(Type)->Type
preserves = ... : {s|Type}{t|Type}(s->t)->(Rel s s)->(Rel t t)->Prop
WF = ... : {s|Type}(Rel s s)->Prop
TWF = ... : {s|Type}(Rel s s)->Prop
per = ... : {s|Type}(Rel s s)->Prop
equiv = ... : {s|Type}(Rel s s)->Prop
preorder = ... : {s|Type}(Rel s s)->Prop
PreorderEq = ... : {s|Type}{R:Rel s s}(preorder R)->Rel s s
SubPred = ... : {s|Type}(Pred s)->(Pred s)->Prop
reflSubPred = ... : {s|Type}refl (SubPred|s)
transSubPred = ... : {s|Type}trans (SubPred|s)
EqPred = ... : {s|Type}Rel (Pred s) (Pred s)
SubRel = ... : {s|Type}{t|Type}(Rel s t)->(Rel s t)->Prop
reflSubRel = ... : {s|Type}{t|Type}refl (SubRel|s|t)
transSubRel = ... : {s|Type}{t|Type}trans (SubRel|s|t)
EqRel = ... : {s|Type}{t|Type}Rel (Rel s t) (Rel s t)
andPred = ... : {s|Type}(Pred s)->(Pred s)->Pred s
orPred = ... : {s|Type}(Pred s)->(Pred s)->Pred s
impliesPred = ... : {s|Type}(Pred s)->(Pred s)->Pred s
notPred = ... : {s|Type}(Pred s)->Pred s
andPredI = ... :
{s|Type}{E,F,G|Pred s}(SubPred E F)->(SubPred E G)->
SubPred E (andPred F G)
andPredE1 = ... :
{s|Type}{E,F,G|Pred s}(SubPred E (andPred F G))->SubPred E F
andPredE2 = ... :
{s|Type}{E,F,G|Pred s}(SubPred E (andPred F G))->SubPred E G
orPredE = ... :
{s|Type}{E,F,G|Pred s}(SubPred F E)->(SubPred G E)->
SubPred (orPred F G) E
orPredI1 = ... :
{s|Type}{E,F,G|Pred s}(SubPred E F)->SubPred E (orPred F G)
orPredI2 = ... :
{s|Type}{E,F,G|Pred s}(SubPred E G)->SubPred E (orPred F G)
impliesPredI = ... :
{s|Type}{E,F,G|Pred s}(SubPred (andPred F G) E)->
SubPred F (impliesPred G E)
impliesPredE = ... :
{s|Type}{E,F,G|Pred s}(SubPred F (impliesPred G E))->
SubPred (andPred F G) E
existsf = ... : {s|Type}{t|Type}(t->s)->(Pred t)->Pred s
starf = ... : {s|Type}{t|Type}(t->s)->(Pred s)->Pred t
forallf = ... : {s|Type}{t|Type}(t->s)->(Pred t)->Pred s
existsfE = ... :
{s|Type}{t|Type}{F|Pred s}{H|Pred t}{f|t->s}
(SubPred (existsf f H) F)->SubPred H (starf f F)
existsfI = ... :
{s|Type}{t|Type}{F|Pred s}{H|Pred t}{f|t->s}
(SubPred H (starf f F))->SubPred (existsf f H) F
forallfE = ... :
{s|Type}{t|Type}{F|Pred s}{H|Pred t}{f|t->s}
(SubPred F (forallf f H))->SubPred (starf f F) H
forallfI = ... :
{s|Type}{t|Type}{F|Pred s}{H|Pred t}{f|t->s}
(SubPred (starf f F) H)->SubPred F (forallf f H)
op = ... : {s|Type}{t|Type}(Rel s t)->Rel t s
notRel = ... : {s|Type}{t|Type}(Rel s t)->Rel s t
andRel = ... : {s|Type}{t|Type}(Rel s t)->(Rel s t)->Rel s t
orRel = ... : {s|Type}{t|Type}(Rel s t)->(Rel s t)->Rel s t
composeRel = ... :
{s|Type}{t|Type}{u|Type}(Rel s t)->(Rel t u)->Rel s u
impliesRel = ... :
{s|Type}{t|Type}{u|Type}(Rel s t)->(Rel s u)->Rel t u
coimpliesRel = ... :
{s|Type}{t|Type}{u|Type}(Rel t u)->(Rel s u)->Rel s t
andRelI = ... :
{s|Type}{t|Type}{P,Q,R|Rel s t}(SubRel R P)->(SubRel R Q)->
SubRel R (andRel P Q)
andRelE1 = ... :
{s|Type}{t|Type}{P,Q,R|Rel s t}(SubRel R (andRel P Q))->SubRel R P
andRelE2 = ... :
{s|Type}{t|Type}{P,Q,R|Rel s t}(SubRel R (andRel P Q))->SubRel R Q
orRelE = ... :
{s|Type}{t|Type}{P,Q,R|Rel s t}(SubRel P R)->(SubRel Q R)->
SubRel (orRel P Q) R
orRelI1 = ... :
{s|Type}{t|Type}{P,Q,R|Rel s t}(SubRel R P)->SubRel R (orRel P Q)
orRelI2 = ... :
{s|Type}{t|Type}{P,Q,R|Rel s t}(SubRel R Q)->SubRel R (orRel P Q)
impliesRelI = ... :
{s|Type}{t|Type}{u|Type}{R|Rel s t}{S|Rel t u}{T|Rel s u}
(SubRel (composeRel R S) T)->SubRel S (impliesRel R T)
impliesRelE = ... :
{s|Type}{t|Type}{u|Type}{R|Rel s t}{S|Rel t u}{T|Rel s u}
(SubRel S (impliesRel R T))->SubRel (composeRel R S) T
coimpliesRelI = ... :
{s|Type}{t|Type}{u|Type}{R|Rel s t}{S|Rel t u}{T|Rel s u}
(SubRel (composeRel R S) T)->SubRel R (coimpliesRel S T)
coimpliesRelE = ... :
{s|Type}{t|Type}{u|Type}{R|Rel s t}{S|Rel t u}{T|Rel s u}
(SubRel R (coimpliesRel S T))->SubRel (composeRel R S) T
existsgh = ... :
{s|Type}{t|Type}{u|Type}{v|Type}(u->v->s)->(u->v->t)->(Rel u v)->
Rel s t
stargh = ... :
{s|Type}{t|Type}{u|Type}{v|Type}(u->v->s)->(u->v->t)->(Rel s t)->
Rel u v
forallgh = ... :
{s|Type}{t|Type}{u|Type}{v|Type}(u->v->s)->(u->v->t)->(Rel u v)->
Rel s t
existsghE = ... :
{s|Type}{t|Type}{u|Type}{v|Type}{P|Rel s t}{U|Rel u v}{g|u->v->s}
{h|u->v->t}(SubRel (existsgh g h U) P)->SubRel U (stargh g h P)
existsghI = ... :
{s|Type}{t|Type}{u|Type}{v|Type}{P|Rel s t}{U|Rel u v}{g|u->v->s}
{h|u->v->t}(SubRel U (stargh g h P))->SubRel (existsgh g h U) P
forallghE = ... :
{s|Type}{t|Type}{u|Type}{v|Type}{P|Rel s t}{U|Rel u v}{g|u->v->s}
{h|u->v->t}(SubRel P (forallgh g h U))->SubRel (stargh g h P) U
forallghI = ... :
{s|Type}{t|Type}{u|Type}{v|Type}{P|Rel s t}{U|Rel u v}{g|u->v->s}
{h|u->v->t}(SubRel (stargh g h P) U)->SubRel P (forallgh g h U)
KPred = ... : {s|Type}Prop->Pred s
KRelL = ... : {s|Type}{t|Type}(Pred s)->Rel s t
KRelR = ... : {s|Type}{t|Type}(Pred t)->Rel s t
leftKanPred = ... : {s|Type}{t|Type}(Rel s t)->(Pred s)->Pred t
rightKanPred = ... : {s|Type}{t|Type}(Rel s t)->(Pred s)->Pred t
notPredIE = ... :
{s|Type}{E,F|Pred s}(SubPred E F)->SubPred (notPred F) (notPred E)
notRelIE = ... :
{s|Type}{t|Type}{P,Q|Rel s t}(SubRel P Q)->
SubRel (notRel Q) (notRel P)
univPred = ... : {s|Type}Pred s
univRel = ... : {s|Type}{t|Type}Rel s t
emptyPred = ... : {s|Type}Pred s
emptyRel = ... : {s|Type}{t|Type}Rel s t
univPredI = ... : {s|Type}{F|Pred s}SubPred F (univPred|s)
emptyPredI = ... : {s|Type}{F|Pred s}SubPred (emptyPred|s) F
univRelI = ... : {s|Type}{t|Type}{R|Rel s t}SubRel R (univRel|s|t)
emptyRelI = ... : {s|Type}{t|Type}{R|Rel s t}SubRel (emptyRel|s|t) R
existfunit = ... :
{s|Type}{t|Type}{H|Pred t}{f|t->s}SubPred H (starf f (existsf f H))
existfcounit = ... :
{s|Type}{t|Type}{F|Pred s}{f|t->s}SubPred (existsf f (starf f F)) F
forallfunit = ... :
{s|Type}{t|Type}{F|Pred s}{f|t->s}SubPred F (forallf f (starf f F))
forallfcounit = ... :
{s|Type}{t|Type}{H|Pred t}{f|t->s}SubPred (starf f (forallf f H)) H
existghunit = ... :
{s|Type}{t|Type}{u|Type}{v|Type}{U|Rel u v}{g|u->v->s}{h|u->v->t}
SubRel U (stargh g h (existsgh g h U))
existghcounit = ... :
{s|Type}{t|Type}{u|Type}{v|Type}{P|Rel s t}{g|u->v->s}{h|u->v->t}
SubRel (existsgh g h (stargh g h P)) P
forallghunit = ... :
{s|Type}{t|Type}{u|Type}{v|Type}{P|Rel s t}{g|u->v->s}{h|u->v->t}
SubRel P (forallgh g h (stargh g h P))
forallghcounit = ... :
{s|Type}{t|Type}{u|Type}{v|Type}{U|Rel u v}{g|u->v->s}{h|u->v->t}
SubRel (stargh g h (forallgh g h U)) U
monotonePred = ... : {s|Type}{t|Type}((Pred s)->Pred t)->Prop
monotoneRel = ... :
{s|Type}{t|Type}{u|Type}{v|Type}((Rel s t)->Rel u v)->Prop
opMono = ... :
{s|Type}{t|Type}{P,Q|Rel s t}(SubRel P Q)->SubRel (op P) (op Q)
opInvol = ... : {s|Type}{t|Type}{P|Rel s t}SubRel P (op (op P))
composeRelMonoL = ... :
{s|Type}{t|Type}{u|Type}{P|Rel s t}
monotoneRel|t|u|s|u (composeRel P)
composeRelR = ... :
{s|Type}{t|Type}{u|Type}(Rel t u)->(Rel s t)->Rel s u
composeRelMonoR = ... :
{s|Type}{t|Type}{u|Type}{Q|Rel t u}
monotoneRel|s|t|s|u (composeRelR Q)
composeRelEqL1 = ... :
{s|Type}{t|Type}{P|Rel s t}SubRel (composeRel (Eq|s) P) P
composeRelEqL2 = ... :
{s|Type}{t|Type}{P|Rel s t}SubRel P (composeRel (Eq|s) P)
composeRelEqR1 = ... :
{s|Type}{t|Type}{P|Rel s t}SubRel (composeRel P (Eq|t)) P
composeRelEqR2 = ... :
{s|Type}{t|Type}{P|Rel s t}SubRel P (composeRel P (Eq|t))
composeRelAssoc1 = ... :
{s|Type}{t|Type}{u|Type}{v|Type}{P|Rel s t}{Q|Rel t u}{R|Rel u v}
SubRel (composeRel (composeRel P Q) R)
(composeRel P (composeRel Q R))
composeRelAssoc2 = ... :
{s|Type}{t|Type}{u|Type}{v|Type}{P|Rel s t}{Q|Rel t u}{R|Rel u v}
SubRel (composeRel P (composeRel Q R))
(composeRel (composeRel P Q) R)
opcompose1 = ... :
{s|Type}{t|Type}{u|Type}{P|Rel s t}{Q|Rel t u}
SubRel (composeRel (op Q) (op P)) (op (composeRel P Q))
opcompose2 = ... :
{s|Type}{t|Type}{u|Type}{P|Rel s t}{Q|Rel t u}
SubRel (op (composeRel P Q)) (composeRel (op Q) (op P))
ClosedL = ... : {s|Type}{t|Type}(Rel s s)->(Rel s t)->Prop
ClosedR = ... : {s|Type}{t|Type}(Rel t t)->(Rel s t)->Prop
symkernelRel = ... : {s|Type}(Rel s s)->Rel s s
prekernelRelR = ... :
{s|Type}{S:Rel s s}[P=impliesRel S S]
(preorder P /\ {Q:Rel s s}(ClosedR Q S)->SubRel Q P)
prekernelRelL = ... :
{s|Type}{S:Rel s s}[P=coimpliesRel S S]
(preorder P /\ {Q:Rel s s}(ClosedL Q S)->SubRel Q P)
kernelRel = ... :
{s|Type}{S:Rel s s}(sym S)->[kerS=symkernelRel S]
(equiv kerS /\ {Q:Rel s s}(ClosedL Q S)->(ClosedR Q S)->
SubRel Q kerS)
```

Conor McBride
11/13/1998