Require Import Sumbool.
Require Import RelDec.
Require Import RelUtil.
Require Import ListUtil.
Require Import RelMidex.
Require Import RelSub.
Require Import Path.
Require Import Arith.

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.

Proof.
unfold inclusion, trichotomy. intros. pose (H x y). pose (H y x). tauto.
Qed.

Section try_add_arc.

Variable R : relation A.

Inductive try_add_arc (x y : A) : A -> A -> Prop :=
| 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).

Proof.
unfold inclusion. intros. constructor. assumption.
Qed.

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.

Proof.
intros. inversion H. assumption. inversion H0. contradiction.
rewrite H3 in H7. contradiction.
Qed.

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

Proof.
intros. destruct (H y x). assumption. absurd (try_add_arc x y x y). assumption.
constructor 2; assumption.
Qed.

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.

Proof.
unfold is_restricted. intros. inversion H2. apply H1. assumption.
rewrite <- H5. rewrite <- H6. tauto.
Qed.

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

Proof.
repeat intro. destruct (X0 x0 y0). do 2 constructor. assumption.
destruct (X x0 y0). constructor 2. intro. inversion H; contradiction.
destruct (X0 y0 x0). constructor 2. intro. inversion H; contradiction.
destruct (X x x0). destruct (X y y0). rewrite e. rewrite e0.
constructor. constructor 2; assumption.
constructor 2. intro. inversion H; contradiction.
constructor 2. intro. inversion H; contradiction.
Qed.

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

Proof.
do 6 intro. destruct (H0 x0 y0). do 2 constructor. assumption.
destruct (H x0 y0). constructor 2. intro. inversion H3; contradiction.
destruct (H0 y0 x0). constructor 2. intro. inversion H4; contradiction.
destruct (H x x0). destruct (H y y0). rewrite H4. rewrite H5.
constructor. constructor 2; assumption.
constructor 2. intro. inversion H6; contradiction.
constructor 2. intro. inversion H5; contradiction.
Qed.

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

Proof.
unfold trichotomy. intros. destruct (H x y). tauto. destruct (H0 x y).
do 2 constructor. assumption.
destruct (H0 y x). do 2 constructor 2. constructor. assumption. constructor.
constructor 2; assumption.
Qed.

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

Proof.
unfold trichotomy, restriction. intros. tauto.
Qed.

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

Proof.
induction l; simpl; intros. inversion H0; tauto.
destruct H0. split. inversion H0. assumption. rewrite H5 in H. tauto.
apply IHl. pose sym_equal. pose (e A x a). tauto. assumption.
Qed.

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.

Proof.
unfold transitive. intros.
apply H with t; apply try_add_arc_sym with x y; assumption.
Qed.

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

Proof.
intros. induction n. inversion H1. destruct l. simpl in H2.
apply trans_try_add_arc_sym with x y z; assumption.
simpl in H1. pose (le_Sn_O (length l) H2). contradiction. apply IHn.
inversion H1. clear IHn H1 H4 H5 x0 y0.
destruct (path_repeat_free_length (try_add_arc x y) H z l z H3).
decompose [and] H1.
assert (length x0 <= S n). apply le_trans with (length l); assumption.
clear H1 H2 H3 H6 H7 H8.
destruct x0. exists (nil : list A). apply le_O_n. tauto.
destruct x0; simpl in * |- . exists (nil : list A). apply le_O_n. simpl.
apply sub_rel_try_add_arc. apply trans_try_add_arc_sym with x y a; tauto.
destruct H10. destruct H2.
inversion H1; inversion H2.
exists (a0::x0). simpl. apply le_S_n. assumption.
simpl. split. apply (sub_rel_try_add_arc). apply H0 with a; assumption.
assumption.
absurd (R a0 a). tauto. apply trans_tc_incl. assumption.
apply path_clos_trans with (x0++(z::nil)). apply path_app.
apply path_try_add_arc_path with x y. rewrite H13. tauto. assumption. simpl.
assumption.
absurd (R a z). tauto. apply trans_tc_incl. assumption.
apply path_clos_trans with (a0::x0). split. assumption.
apply path_try_add_arc_path with x y. rewrite H10. tauto. assumption.
rewrite H8 in H13. tauto.
Qed.

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

Proof.
do 7 intro. apply H1 with x0. destruct (clos_trans_path H2).
apply trans_bound_path_try_add_arc with x y (length x1); try assumption.
apply bp_intro with x1; trivial.
Qed.

End try_add_arc.

Section try_add_arc_one_to_many.

Variable R : relation A.

Fixpoint try_add_arc_one_to_many (x : A)(l : list A){struct l} : relation A :=
match l with
| nil => R
| y::l' => clos_trans (try_add_arc (try_add_arc_one_to_many x l') x y)
end.

Lemma sub_rel_try_add_arc_one_to_many : forall x l,
  R << (try_add_arc_one_to_many x l).

Proof.
induction l; simpl; intros. apply inclusion_refl.
apply incl_trans with (try_add_arc_one_to_many x l). assumption.
apply incl_trans with (try_add_arc (try_add_arc_one_to_many x l) x a).
apply sub_rel_try_add_arc. apply tc_incl.
Qed.

Lemma restricted_try_add_arc_one_to_many : forall l x l',
  In x l -> incl l' l -> is_restricted R l ->
  is_restricted (try_add_arc_one_to_many x l') l.

Proof.
induction l'; simpl; intros. assumption. apply restricted_clos_trans.
apply restricted_try_add_arc. assumption. apply H0. simpl. tauto. apply IHl'.
assumption. exact (incl_cons_l_incl H0). assumption.
Qed.

Lemma try_add_arc_one_to_many_dec : eq_dec A -> forall x l l',
  In x l -> incl l' l -> is_restricted R l -> rel_dec R ->
  rel_dec (try_add_arc_one_to_many x l').

Proof.
induction l'; simpl; intros. assumption. pose (incl_cons_l_incl H0).
apply resticted_dec_clos_trans_dec with l. assumption.
apply try_add_arc_dec. assumption. apply IHl'; tauto.
apply restricted_try_add_arc. assumption. apply H0. simpl. tauto.
apply restricted_try_add_arc_one_to_many; simpl; tauto.
Qed.

Lemma try_add_arc_one_to_many_midex : eq_midex A -> forall x l l',
  In x l -> incl l' l -> is_restricted R l -> rel_midex R ->
  rel_midex (try_add_arc_one_to_many x l').

Proof.
induction l'; simpl; intros. assumption. pose (incl_cons_l_incl H1).
apply resticted_midex_clos_trans_midex with l. assumption.
apply try_add_arc_midex. assumption. apply IHl'; tauto.
apply restricted_try_add_arc. assumption. apply H1. simpl. tauto.
apply restricted_try_add_arc_one_to_many; simpl; tauto.
Qed.

Lemma try_add_arc_one_to_many_trichotomy : eq_midex A -> rel_midex R ->
  forall x y l l', In y l' -> In x l -> incl l' l -> is_restricted R l ->
    trichotomy (try_add_arc_one_to_many x l') x y.

Proof.
induction l'; simpl; intros. contradiction. pose (incl_cons_l_incl H3).
apply trichotomy_preserved
  with (try_add_arc (try_add_arc_one_to_many x l') x a).
apply tc_incl. destruct H1. rewrite H1.
apply try_add_arc_trichotomy. assumption.
apply try_add_arc_one_to_many_midex with l; assumption.
apply trichotomy_preserved with (try_add_arc_one_to_many x l').
apply sub_rel_try_add_arc. tauto.
Qed.

Lemma try_add_arc_one_to_many_irrefl : eq_midex A -> forall x l l',
  is_restricted R l -> transitive R -> irreflexive R ->
  irreflexive (try_add_arc_one_to_many x l').

Proof.
induction l'; simpl; intros. assumption.
apply try_add_arc_irrefl. assumption.
destruct l'; simpl. assumption. apply tc_trans. tauto.
Qed.

End try_add_arc_one_to_many.

Section try_add_arc_many_to_many.

Variable R : relation A.

Fixpoint try_add_arc_many_to_many (l' l: list A){struct l'}: relation A :=
  match l' with
    | nil => R
    | x::l'' => try_add_arc_one_to_many (try_add_arc_many_to_many l'' l) x l
  end.

Lemma sub_rel_try_add_arc_many_to_many : forall l l',
  R << (try_add_arc_many_to_many l' l).

Proof.
induction l'; simpl; intros. apply inclusion_refl.
apply incl_trans with (try_add_arc_many_to_many l' l). assumption.
apply sub_rel_try_add_arc_one_to_many.
Qed.

Lemma restricted_try_add_arc_many_to_many : forall l l', incl l' l ->
is_restricted R l -> is_restricted (try_add_arc_many_to_many l' l) l.

Proof.
induction l'; simpl; intros. assumption.
apply restricted_try_add_arc_one_to_many. apply H. simpl. tauto.
apply incl_refl.
apply IHl'. exact (incl_cons_l_incl H). assumption.
Qed.

Lemma try_add_arc_many_to_many_dec : eq_dec A -> forall l l',
  incl l' l -> is_restricted R l -> rel_dec R ->
  rel_dec (try_add_arc_many_to_many l' l).

Proof.
induction l'; simpl; intros. assumption. pose (incl_cons_l_incl H).
apply try_add_arc_one_to_many_dec with l. assumption. apply H. simpl. tauto.
apply incl_refl.
apply restricted_try_add_arc_many_to_many; assumption. tauto.
Qed.

Lemma try_add_arc_many_to_many_midex : eq_midex A -> forall l l',
  incl l' l -> is_restricted R l -> rel_midex R ->
  rel_midex (try_add_arc_many_to_many l' l).

Proof.
induction l'; simpl; intros. assumption. pose (incl_cons_l_incl H0).
apply try_add_arc_one_to_many_midex with l. assumption. apply H0. simpl. tauto.
apply incl_refl.
apply restricted_try_add_arc_many_to_many; assumption. tauto.
Qed.

Lemma try_add_arc_many_to_many_trichotomy : eq_midex A -> rel_midex R ->
  forall x y l l', is_restricted R l -> incl l' l -> In y l -> In x l' ->
    trichotomy (try_add_arc_many_to_many l' l) x y.

Proof.
induction l'; simpl; intros. contradiction. pose (incl_cons_l_incl H2).
destruct H4. rewrite H4.
apply try_add_arc_one_to_many_trichotomy with l; try assumption.
apply try_add_arc_many_to_many_midex; assumption.
rewrite <- H4. apply H2. simpl. tauto. apply incl_refl.
apply restricted_try_add_arc_many_to_many; assumption.
apply trichotomy_preserved with (try_add_arc_many_to_many l' l).
apply sub_rel_try_add_arc_one_to_many. tauto.
Qed.

Lemma try_add_arc_many_to_many_irrefl : eq_midex A -> forall l l',
  incl l' l -> is_restricted R l -> transitive R -> irreflexive R ->
  irreflexive (try_add_arc_many_to_many l' l).

Proof.
induction l'; simpl; intros. assumption. pose (incl_cons_l_incl H0).
apply try_add_arc_one_to_many_irrefl with l. assumption.
apply restricted_try_add_arc_many_to_many; assumption.
destruct l'; simpl. assumption. destruct l. pose (i a0). simpl in i0. tauto.
simpl. apply tc_trans. tauto.
Qed.

End try_add_arc_many_to_many.

Section LETS.

Variable R : relation A.
Variable l : list A.

Definition LETS := try_add_arc_many_to_many (clos_trans (restriction R l)) l l.

Lemma LETS_restriction_clos_trans : (clos_trans (restriction R l)) << LETS.

Proof.
intros. unfold LETS. apply sub_rel_try_add_arc_many_to_many.
Qed.

Lemma LETS_sub_rel : (restriction R l) << LETS.

Proof.
intros. unfold LETS.
apply incl_trans with (clos_trans (restriction R l)).
apply tc_incl. apply LETS_restriction_clos_trans.
Qed.

Lemma LETS_restricted : is_restricted LETS l.

Proof.
unfold LETS. intros. apply restricted_try_add_arc_many_to_many.
apply incl_refl.
apply restricted_clos_trans. apply restricted_restriction.
Qed.

Lemma LETS_transitive : transitive LETS.

Proof.
intros. unfold LETS. destruct l; simpl; apply tc_trans.
Qed.

Lemma LETS_irrefl : eq_midex A ->
  (irreflexive (clos_trans (restriction R l)) <-> irreflexive LETS).

Proof.
split;intros. unfold LETS.
apply try_add_arc_many_to_many_irrefl; try assumption. apply incl_refl.
apply restricted_clos_trans. apply restricted_restriction.
apply tc_trans.
apply incl_irrefl with LETS. apply LETS_restriction_clos_trans.
assumption.
Qed.

Lemma LETS_total : eq_midex A -> rel_midex R -> total LETS l.

Proof.
unfold LETS, total. intros. pose (R_midex_clos_trans_restriction_midex H H0 l).
apply try_add_arc_many_to_many_trichotomy; try assumption.
apply restricted_clos_trans.
apply restricted_restriction. apply incl_refl.
Qed.

Lemma LETS_dec : eq_dec A -> rel_dec R -> rel_dec LETS.

Proof.
intros. unfold LETS. apply try_add_arc_many_to_many_dec. assumption.
apply incl_refl.
apply restricted_clos_trans. apply restricted_restriction.
apply R_dec_clos_trans_restriction_dec; assumption.
Qed.

Lemma LETS_midex : eq_midex A -> rel_midex R -> rel_midex LETS.

Proof.
intros. unfold LETS. apply try_add_arc_many_to_many_midex. assumption.
apply incl_refl.
apply restricted_clos_trans. apply restricted_restriction.
apply R_midex_clos_trans_restriction_midex; assumption.
Qed.

End LETS.

Definition linear_extension R l R' :=
  is_restricted R' l /\ (restriction R l) << R' /\
  transitive R' /\ irreflexive R' /\ total R' l.

Lemma local_global_acyclic : forall R : relation A,
  (forall l, exists R',
    (restriction R l) << R' /\ transitive R' /\ irreflexive R') ->
  irreflexive (clos_trans R).

Proof.
intros. do 2 intro. destruct (clos_trans_path H0).
assert (clos_trans (restriction R (x::x::x0)) x x).
apply path_clos_trans with x0.
apply path_restriction. assumption. destruct (H (x::x::x0)). destruct H3.
destruct H4.
apply H5 with x. apply trans_tc_incl. assumption.
apply incl_tc with (restriction R (x :: x :: x0)). assumption.
assumption.
Qed.

Lemma total_order_eq_midex:
  (forall l, exists R,
    transitive R /\ irreflexive R /\ total R l /\ rel_midex R) ->
  eq_midex A.

Proof.
do 3 intro. destruct (H (x::y::nil)). decompose [and] H0.
destruct (H5 x y); destruct (H5 y x).
absurd (x0 x x). apply H3. apply H1 with y; assumption.
constructor 2. intro. rewrite H7 in H4. rewrite H7 in H6. contradiction.
constructor 2. intro. rewrite H7 in H4. rewrite H7 in H6. contradiction.
destruct (H2 x y); simpl; try tauto.
Qed.

Lemma linearly_extendable : forall R, rel_midex R ->
  (eq_midex A /\ irreflexive (clos_trans R) <->
    forall l, exists R', linear_extension R l R' /\ rel_midex R').

Proof.
unfold linear_extension. split; intros. exists (LETS R l). split. split.
apply LETS_restricted. split.
apply LETS_sub_rel. split. apply LETS_transitive. split.
destruct (LETS_irrefl R l).
tauto. apply H1. apply incl_irrefl with (clos_trans R).
unfold inclusion. apply incl_tc. apply incl_restriction. tauto.
apply LETS_total; tauto. apply LETS_midex; tauto.
split. apply total_order_eq_midex. intro. destruct (H0 l). exists x. tauto.
apply local_global_acyclic. intro. destruct (H0 l). exists x. tauto.
Qed.

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.

Proof.
unfold transitive, irreflexive, total, trichotomy. do 3 intro. destruct H.
pose (a (x::y::nil)).
assert ({x0 (x::y::nil) x y=true}+{x0 (x::y::nil) x y=false}).
case (x0 (x::y::nil) x y); tauto.
assert ({x0 (x::y::nil) y x=true}+{x0 (x::y::nil) y x=false}).
case (x0 (x::y::nil) y x); tauto.
destruct a0. destruct H2. pose (H3 x y). simpl in o.
destruct H. constructor 2. intro. rewrite H in e. rewrite H in H2.
exact (H2 y e).
destruct H0. constructor 2. intro. rewrite H in e0. rewrite H in H2.
exact (H2 y e0).
constructor. destruct o; try tauto. rewrite H in e. inversion e. destruct H.
assumption.
rewrite H in e0. inversion e0.
Qed.

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

Proof.
unfold LETS. do 7 intro. simpl in *|- . destruct H2.
assert (is_restricted (restriction R (x :: y :: nil)) (x::y::nil)).
apply restricted_restriction.
assert (is_restricted
  (try_add_arc (clos_trans (restriction R (x :: y :: nil))) y y) (x::y::nil)).
apply restricted_try_add_arc; simpl; try tauto. apply restricted_clos_trans.
assumption.
assert (is_restricted
  (try_add_arc (clos_trans (try_add_arc
    (clos_trans (restriction R (x :: y :: nil))) y y)) y x) (x::y::nil)).
apply restricted_try_add_arc; simpl; try tauto. apply restricted_clos_trans.
assumption.
assert (is_restricted (try_add_arc (clos_trans
  (try_add_arc (clos_trans (try_add_arc
    (clos_trans (restriction R (x :: y :: nil))) y y)) y x)) x y) (x::y::nil)).
apply restricted_try_add_arc; simpl; try tauto. apply restricted_clos_trans.
assumption.
assert (is_restricted (try_add_arc (clos_trans (try_add_arc (clos_trans
  (try_add_arc (clos_trans (try_add_arc (clos_trans
    (restriction R (x :: y :: nil))) y y)) y x)) x y)) x x) (x::y::nil)).
apply restricted_try_add_arc; simpl; try tauto. apply restricted_clos_trans.
assumption.
pose (clos_trans_restricted_pair H8 H2). inversion t; try tauto.
clear H10 H11 z t0.
pose (clos_trans_restricted_pair H7 H9). inversion t0. clear H11 H12 z t1.
pose (clos_trans_restricted_pair H6 H10). inversion t1; try tauto.
clear H12 H13 z t2.
pose (clos_trans_restricted_pair H5 H11). inversion t2. clear H13 H14 z t3.
assert (restriction R (x :: y :: nil) x y).
apply clos_trans_restricted_pair; assumption.
unfold restriction in H13. tauto. tauto.
absurd (clos_trans (try_add_arc (clos_trans (try_add_arc (clos_trans
  (restriction R (x :: y :: nil))) y y)) y x) y x).
assumption. constructor. constructor 2. intro. rewrite H14 in H10. tauto.
intro. pose (clos_trans_restricted_pair H5 H14). inversion t1; try tauto.
clear H16 H17 z t2.
pose (clos_trans_restricted_pair H4 H15). unfold restriction in r. tauto.
Qed.

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

Proof.
do 4 intro. assert (forall l, rel_dec (LETS R l)). intro.
apply LETS_dec; assumption.
pose (eq_dec_midex X). pose (rel_dec_midex X0).
exists (fun l x y => if (X1 l x y) then true else false). simpl. split.
do 5 intro. case (X1 (x :: y :: nil) x y). case (X1 (y :: x :: nil) x y).
do 2 intro. absurd (LETS R (x :: y :: nil) x y /\ LETS R (y :: x :: nil) x y).
apply LETS_antisym; assumption. tauto. do 3 intro. destruct H3. inversion H4.
do 2 intro. destruct H3. inversion H3. split.
do 3 intro. destruct (X1 l x y). apply (LETS_restricted R l x y). assumption.
inversion H0. split.
do 3 intro. destruct (X1 l x y). trivial. absurd (LETS R l x y). assumption.
apply LETS_restriction_clos_trans. apply tc_incl. assumption. split.
do 5 intro. destruct (X1 l x y). destruct (X1 l y z).
pose (LETS_transitive R l x y z l0 l1).
destruct (X1 l x z). trivial. contradiction. inversion H1. inversion H0. split.
do 2 intro. destruct (X1 l x x). absurd (LETS R l x x).
destruct (LETS_irrefl R l).
assumption. apply H1. apply incl_irrefl with (clos_trans R).
apply incl_tc. apply incl_restriction. assumption. assumption.
inversion H0.
do 4 intro. unfold trichotomy. destruct (X1 l x y). tauto. destruct (X1 l y x).
tauto.
destruct (LETS_total l e r x y); tauto.
Qed.

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

Proof.
intros. exists (let (f,s):= H in f). intros. destruct H. destruct a.
pose (H0 l). unfold linear_extension in *|-* . tauto.
Qed.

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

Proof.
unfold antisym_topo_sortable, linear_extension.
intros. assert (irreflexive (clos_trans R)). apply local_global_acyclic.
intro. exists (fun x y => (let (f,s):= H0 in f) l x y=true). destruct H0.
destruct a. pose (H1 l). tauto.
assert (eq_dec A). apply total_order_eq_dec. exists (let (f,s):= H0 in f).
intro. destruct H0.
destruct a. pose (H2 l). split; tauto.
do 2 intro. destruct (X x y). rewrite e. constructor 2. intro. apply (H1 y).
constructor. assumption.
destruct H0. destruct a. pose (H0 x y). decompose [and] (H2 (x::y::nil)).
destruct (sumbool_of_bool (x0 (x::y::nil) x y)).
destruct (sumbool_of_bool (x0 (y::x::nil) x y)).
constructor. destruct (H x y). assumption. destruct (H y x).
absurd (x0 (x :: y :: nil) y x=true).
intro. apply (H6 x). apply H4 with y; assumption. apply H5. unfold restriction.
simpl. tauto. generalize n0 e e0.
case (x0 (x :: y :: nil) x y); case (x0 (y :: x :: nil) x y); tauto.
constructor 2. intro. absurd (x0 (y :: x :: nil) x y=true). intro.
rewrite e0 in H9. inversion H9.
pose (H2 (y::x::nil)). decompose [and] a. apply H11. unfold restriction. simpl.
tauto.
constructor 2. intro. absurd (x0 (x::y:: nil) x y=true). intro.
rewrite e in H9. inversion H9.
apply H5. unfold restriction. simpl. tauto.
Qed.

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

Proof.
intros. apply total_order_eq_dec. exists (let (first,second):=H in first).
destruct H. intro. pose (l l0). destruct l1. split; tauto.
Qed.

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

Proof.
intros. apply local_global_acyclic. intro. destruct H.
exists (fun x0 y => x l x0 y=true). destruct (l0 l). tauto.
Qed.

End On_relation_completion.