Library CoLoR.Util.Relation.Total

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Stephane Le Roux, 2006-02-23
on the total completion of a relation: Consider a decidable (resp. middle-excluding) relation over an arbitrary set. Equality on the set is decidable (resp. middle-excluding) and the relation is acyclic iff its restriction to any finite set has a decidable (resp. middle-excluding) irreflexive linear extension.

Set Implicit Arguments.

Section On_relation_completion.

Variable A : Set.


Section total.

Variable R : relation A.

Definition trichotomy x y : Prop := R x y \/ x=y \/ R y x.

Definition total l : Prop := forall x y, In x l -> In y l -> trichotomy x y.

End total.

Lemma trichotomy_preserved : forall R R' x y,
  R << R' -> trichotomy R x y -> trichotomy R' x y.


Section try_add_arc.

Variable R : relation A.

Inductive try_add_arc (x y : A) : relation A :=
| keep : forall z t, R z t -> try_add_arc x y z t
| try_add : x<>y -> ~R y x -> try_add_arc x y x y.

Lemma sub_rel_try_add_arc : forall x y, R << try_add_arc x y.

Lemma try_add_arc_sym : forall x y z t,
  try_add_arc x y z t -> try_add_arc x y t z -> R z t.

Lemma not_try_add_arc : rel_midex R -> forall x y, x<>y ->
  ~try_add_arc x y x y -> R y x.

Lemma restricted_try_add_arc : forall x y l,
  In x l -> In y l -> is_restricted R l -> is_restricted (try_add_arc x y) l.

Lemma try_add_arc_dec : eq_dec A -> forall x y, rel_dec R ->
  rel_dec (try_add_arc x y).

Lemma try_add_arc_midex : eq_midex A -> forall x y, rel_midex R ->
  rel_midex (try_add_arc x y).

Lemma try_add_arc_trichotomy : eq_midex A -> rel_midex R ->
  forall x y, trichotomy (try_add_arc x y) x y.

Lemma trichotomy_restriction : forall x y l,
  In x l -> In y l -> trichotomy R x y -> trichotomy (restriction R l) x y.

Lemma path_try_add_arc_path : forall t x y l z,
  ~(x=z \/ In x l) \/ ~(y=t \/ In y l) -> path (try_add_arc x y) z t l ->
  path R z t l.

Lemma trans_try_add_arc_sym : forall x y z t,
  transitive R -> try_add_arc x y z t -> try_add_arc x y t z -> R z z.

Lemma trans_bpath_try_add_arc : eq_midex A -> forall x y z n,
  transitive R -> bpath (try_add_arc x y ) n z z -> R z z.

Lemma try_add_arc_irrefl : eq_midex A -> forall x y,
  transitive R -> irreflexive R -> irreflexive (clos_trans (try_add_arc x y)).

End try_add_arc.

try_add_arc_one_to_many: multiple try_add_arc with one list
try_add_arc_many_to_many: multiple try_add_arc with two lists
Linear Extension and Topological Sorting
Linear Extension
Topological Sorting

Definition topo_sortable R :=
  {F : list A -> A -> A -> bool |
    forall l, linear_extension R l (fun x y => F l x y = true)}.

Definition antisym R SC := forall x y : A, x<>y -> ~R x y -> ~R y x ->
  ~(SC (x::y::nil) x y /\ SC (y::x::nil) x y).

Definition antisym_topo_sortable R :=
  {F : list A -> A -> A -> bool |
    let G := (fun l x y => F l x y = true) in
      antisym R G /\ forall l, linear_extension R l (G l)}.

Lemma total_order_eq_dec :
  {F : list A -> A -> A -> bool |
    forall l, let G := fun x y => F l x y = true in
      transitive G /\ irreflexive G /\ total G l} -> eq_dec A.

Lemma LETS_antisym : forall R, antisym R (LETS R).

Lemma possible_antisym_topo_sort : forall R, eq_dec A -> rel_dec R ->
  irreflexive (clos_trans R) -> antisym_topo_sortable R.

Lemma antisym_topo_sortable_topo_sortable : forall R,
  antisym_topo_sortable R -> topo_sortable R.

Lemma antisym_topo_sortable_rel_dec : forall R,
  rel_midex R -> antisym_topo_sortable R -> rel_dec R.

Lemma rel_dec_topo_sortable_eq_dec : forall R,
  rel_dec R -> topo_sortable R -> eq_dec A.

Lemma rel_dec_topo_sortable_acyclic : forall R,
  rel_dec R -> topo_sortable R -> irreflexive (clos_trans R).

End On_relation_completion.