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)