Control.Relation.ReflexiveClosure

Utility for describing chains of values linked via
a transitive relation.

Reexports

Definitions

data ReflexiveClosure : (a -> a -> Type) -> a -> a -> Type

  The reflexive closure of a (typically transitive) relation.
  
  This converts a transitive relation into a preorder.
  For instance, if `(<)` is a transitive relation over the integers,
  `ReflexiveClosure (<)` (corresponding to `(<=)` is a transitive,
  reflexive relation over the integers.

Totality: total
Visibility: public export
Constructors:

Rel : (0 _ : rel x y) -> ReflexiveClosure rel x y

Refl : ReflexiveClosure rel x x

Hints:

Trichotomous a rel => Antisymmetric a (ReflexiveClosure rel)

Reflexive a (ReflexiveClosure rel)

Transitive a rel => Transitive a (ReflexiveClosure rel)

fromEq : (0 _ : x = y) -> ReflexiveClosure rel x y

Totality: total
Visibility: public export

0 strictLeft : Transitive a rel => rel x y -> ReflexiveClosure rel y z -> rel x z

Totality: total
Visibility: public export

0 strictRight : Transitive a rel => ReflexiveClosure rel x y -> rel y z -> rel x z

Totality: total
Visibility: public export

data Chain : (a -> a -> Type) -> a -> a -> Type

  A chain of values, linke by relation `ReflexiveClosure rel`.

Totality: total
Visibility: public export
Constructors:

Nil : Chain rel x x

(::) : (0 x : a) -> Chain rel y z -> {auto 0 _ : ReflexiveClosure rel x y} -> Chain rel x z

data IsStrict : Chain rel x y -> Type

  Witness that at least one link in a chain of values
  linked via `ReflexiveClosure rel` is string, and
  therefore (if `rel` is transitive), `rel x y` holds.
  
  For instance, assume `rel` is `(<)` over the integers.
  Then `ReflexiveClosure rel` corresponds to `(<=)`.
  If we have the chain `w <= x <= y <= z` and we can
  show that one of the inequalities is strict (for instance,
  that `y < z`), then we can not only show that `w <= z` but
  that `w < z`.

Totality: total
Visibility: public export
Constructors:

Here : IsStrict (x :: c)

There : IsStrict c -> IsStrict (x :: c)

0 chain : Preorder a rel => Chain rel x y -> rel x y

  If `x` and `y` are linked via a preorder `rel` over a chain
  of values, then `rel x y` holds.

Totality: total
Visibility: public export

0 weak : Transitive a rel => Chain rel x y -> ReflexiveClosure rel x y

  If `x` and `y` are linked via `ReflexiveClosure rel` for a transitive
  relation `rel` over a chain of values, then `ReflexiveClosure rel x y` holds.

Totality: total
Visibility: public export

0 strict : Transitive a rel => (c : Chain rel x y) -> IsStrict c => rel x y

  If `x` and `y` are linked via `ReflexiveClosure rel` for a transitive
  relation `rel` over a chain of values, and at least one link ist
  strict, the `rel x y` holds.

Totality: total
Visibility: public export