Basic properties of relations


Require Import Vbase List Relations Classical.
Set Implicit Arguments.

Definitions of relations
Make arguments implicit
Arguments clos_trans [A] R x y.
Arguments clos_refl_trans [A] R x y.
Arguments reflexive [A] R.
Arguments symmetric [A] R.
Arguments transitive [A] R.
Arguments inclusion [A] R1 R2.
Arguments same_relation {A} R1 R2.
Arguments union [A] R1 R2 x y.

Definition immediate X (rel : relation X) (a b: X) :=
  rel a b ( c (R1: rel a c) (R2: rel c b), False).

Definition irreflexive X (rel : relation X) := x, rel x x False.

Definition acyclic X (rel : relation X) := irreflexive (clos_trans rel).

Definition is_total X (cond: X Prop) (rel: relation X) :=
   a (IWa: cond a)
         b (IWb: cond b) (NEQ: a b),
    rel a b rel b a.

Definition restr_subset X (cond: X Prop) (rel rel': relation X) :=
   a (IWa: cond a)
         b (IWb: cond b) (REL: rel a b),
    rel' a b.

Definition restr_rel X (cond : X Prop) (rel : relation X) : relation X :=
  fun a brel a b cond a cond b.

Definition restr_eq_rel A B (f : A B) rel x y :=
  rel x y f x = f y.

Definition upward_closed (X: Type) (rel: relation X) (P: X Prop) :=
   x y (REL: rel x y) (POST: P y), P x.

Definition max_elt (X: Type) (rel: relation X) (a: X) :=
   b (REL: rel a b), False.

Notation "r 'UNION1' ( a , b )" :=
  (fun x yx = a y = b r x y) (at level 100).

Notation "a <--> b" := (same_relation a b) (at level 110).

Definition seq (X:Type) (r1 r2 : relation X) : relation X :=
  fun x y z, r1 x z r2 z y.

Definition clos_refl A (R: relation A) x y := x = y R x y.

Very basic properties of relations

Lemma r_refl A (R: relation A) x : clos_refl R x x.
Proof. vauto. Qed.

Lemma r_step A (R: relation A) x y : R x y clos_refl R x y.
Proof. vauto. Qed.

Hint Immediate r_refl r_step.

Section BasicProperties.

Variable A : Type.
Variable dom : A Prop.
Variables r r' r'' : relation A.

Lemma clos_trans_mon a b :
  clos_trans r a b
  ( a b, r a b r' a b)
  clos_trans r' a b.
Proof.
  induction 1; ins; eauto using clos_trans.
Qed.

Lemma clos_refl_trans_mon a b :
  clos_refl_trans r a b
  ( a b, r a b r' a b)
  clos_refl_trans r' a b.
Proof.
  induction 1; ins; eauto using clos_refl_trans.
Qed.

Lemma clos_refl_transE a b :
  clos_refl_trans r a b a = b clos_trans r a b.
Proof.
  split; ins; desf; vauto; induction H; desf; vauto.
Qed.

Lemma clos_trans_in_rt a b :
  clos_trans r a b clos_refl_trans r a b.
Proof.
  induction 1; vauto.
Qed.

Lemma rt_t_trans a b c :
  clos_refl_trans r a b clos_trans r b c clos_trans r a c.
Proof.
  ins; induction H; eauto using clos_trans.
Qed.

Lemma t_rt_trans a b c :
  clos_trans r a b clos_refl_trans r b c clos_trans r a c.
Proof.
  ins; induction H0; eauto using clos_trans.
Qed.

Lemma t_step_rt x y :
  clos_trans r x y z, r x z clos_refl_trans r z y.
Proof.
  split; ins; desf.
    by apply clos_trans_tn1 in H; induction H; desf; eauto using clos_refl_trans.
  by rewrite clos_refl_transE in *; desf; eauto using clos_trans.
Qed.

Lemma t_rt_step x y :
  clos_trans r x y z, clos_refl_trans r x z r z y.
Proof.
  split; ins; desf.
    by apply clos_trans_t1n in H; induction H; desf; eauto using clos_refl_trans.
  by rewrite clos_refl_transE in *; desf; eauto using clos_trans.
Qed.

Lemma clos_trans_of_transitive (T: transitive r) x y :
  clos_trans r x y r x y.
Proof.
  induction 1; eauto.
Qed.

Lemma ct_of_transitive (T: transitive r) x y :
  clos_trans r x y r x y.
Proof.
  by split; ins; eauto using t_step; eapply clos_trans_of_transitive.
Qed.

Lemma crt_of_transitive (T: transitive r) x y :
  clos_refl_trans r x y clos_refl r x y.
Proof.
  by ins; rewrite clos_refl_transE, ct_of_transitive; ins.
Qed.

Lemma clos_trans_eq :
   B (f : A B)
    (H: a b (SB: r a b), f a = f b) a b
    (C: clos_trans r a b),
  f a = f b.
Proof.
  ins; induction C; eauto; congruence.
Qed.

Lemma trans_irr_acyclic :
  irreflexive r transitive r acyclic r.
Proof.
  eby repeat red; ins; eapply H, clos_trans_of_transitive.
Qed.

Lemma restr_rel_trans :
  transitive r transitive (restr_rel dom r).
Proof.
  unfold restr_rel; red; ins; desf; eauto.
Qed.

Lemma upward_clos_trans P :
  upward_closed r P upward_closed (clos_trans r) P.
Proof.
  ins; induction 1; eauto.
Qed.

Lemma max_elt_clos_trans a b:
  max_elt r a clos_trans r a b False.
Proof.
  ins; apply clos_trans_t1n in H0; induction H0; eauto.
Qed.

Lemma is_total_restr :
  is_total dom r
  is_total dom (restr_rel dom r).
Proof.
  red; ins; eapply H in NEQ; eauto; desf; vauto.
Qed.

Lemma clos_trans_restrD f x y :
  clos_trans (restr_rel f r) x y f x f y.
Proof.
  unfold restr_rel; induction 1; ins; desf.
Qed.

Lemma clos_trans_restr_eqD B (f: A B) x y :
  clos_trans (restr_eq_rel f r) x y f x = f y.
Proof.
  unfold restr_eq_rel; induction 1; ins; desf; congruence.
Qed.

Lemma irreflexive_inclusion:
  inclusion r r'
  irreflexive r'
  irreflexive r.
Proof.
  unfold irreflexive, inclusion; eauto.
Qed.

Lemma irreflexive_union :
  irreflexive (union r r') irreflexive r irreflexive r'.
Proof.
  unfold irreflexive, union; repeat split;
  try red; ins; desf; eauto.
Qed.

Lemma irreflexive_seqC :
  irreflexive (seq r r') irreflexive (seq r' r).
Proof.
  unfold irreflexive, seq; repeat split;
  try red; ins; desf; eauto.
Qed.

Lemma clos_trans_inclusion :
  inclusion r (clos_trans r).
Proof.
  vauto.
Qed.

Lemma clos_trans_inclusion_clos_refl_trans:
  inclusion (clos_trans r) (clos_refl_trans r).
Proof.
  by red; ins; apply clos_trans_in_rt.
Qed.

Lemma clos_trans_monotonic :
  inclusion r r'
  inclusion (clos_trans r) (clos_trans r').
Proof.
  by red; ins; eapply clos_trans_mon.
Qed.

Lemma inclusion_seq_trans t :
  transitive t
  inclusion r t
  inclusion r' t
  inclusion (seq r r') t.
Proof.
  unfold seq; red; ins; desf; eauto.
Qed.

Lemma inclusion_seq_rt :
  inclusion r (clos_refl_trans r'')
  inclusion r' (clos_refl_trans r'')
  inclusion (seq r r') (clos_refl_trans r'').
Proof.
  unfold seq; red; ins; desf; eapply rt_trans; eauto.
Qed.

Lemma inclusion_union_l :
  inclusion r r''
  inclusion r' r''
  inclusion (union r r') r''.
Proof.
  unfold union; red; intros; desf; auto.
Qed.

Lemma inclusion_union_r :
  inclusion r r' inclusion r r''
  inclusion r (union r' r'').
Proof.
  unfold union; red; intros; desf; auto.
Qed.

Lemma inclusion_step_rt :
  inclusion r r'
  inclusion r (clos_refl_trans r').
Proof.
  unfold seq; red; ins; desf; eauto using rt_step.
Qed.

Lemma inclusion_r_rt :
  inclusion r r'
  inclusion (clos_refl r) (clos_refl_trans r').
Proof.
  unfold seq, clos_refl; red; ins; desf; eauto using rt_step, rt_refl.
Qed.

Lemma inclusion_rt_rt :
  inclusion r r'
  inclusion (clos_refl_trans r) (clos_refl_trans r').
Proof.
  red; ins; eapply clos_refl_trans_mon; eauto.
Qed.

Lemma inclusion_step_t :
  inclusion r r'
  inclusion r (clos_trans r').
Proof.
  unfold seq; red; ins; desf; eauto using t_step.
Qed.

Lemma inclusion_t_t :
  inclusion r r'
  inclusion (clos_trans r) (clos_trans r').
Proof.
  red; ins; eapply clos_trans_mon; eauto.
Qed.

Lemma inclusion_acyclic :
  inclusion r r'
  acyclic r'
  acyclic r.
Proof.
  repeat red; ins; eapply H0, clos_trans_mon; eauto.
Qed.

End BasicProperties.

Lemma clos_trans_of_clos_trans1 A (r r' : relation A) x y :
  clos_trans (fun a bclos_trans r a b r' a b) x y
  clos_trans (fun a br a b r' a b) x y.
Proof.
  split; induction 1; desf;
  eauto using clos_trans, clos_trans_mon.
Qed.

Lemma clos_trans_of_clos_trans A (r : relation A) x y :
  clos_trans (clos_trans r) x y
  clos_trans r x y.
Proof.
  apply ct_of_transitive; vauto.
Qed.

Lemma inclusion_union :
   {A : Type} (R1 R1' R2 R2' : relation A)
         (HINC1 : inclusion R1' R1)
         (HINC2 : inclusion R2' R2),
    inclusion (union R2' R1') (union R2 R1).
Proof.
  intros.
  intros x y HUN.
  inversion HUN; [left; auto | right; auto].
Qed.

Lemma inclusion_restr_rel_l :
   {A : Type} (dom : A Prop) (R1 R1' : relation A)
         (HINC: inclusion R1' R1),
    inclusion (restr_rel dom R1') R1.
Proof.
  unfold inclusion, seq, clos_refl, restr_rel; ins; desf; eauto.
Qed.

Lemma inclusion_seq_refl :
   (A : Type) (R1 R2 R3 : relation A)
         (INC1: inclusion R1 R3)
         (INC2: inclusion R2 R3)
         (TRANS: transitive R3),
    inclusion (seq R1 (clos_refl R2)) R3.
Proof.
  unfold inclusion, seq, clos_refl; ins; desf; eauto.
Qed.

Lemma inclusion_rt_l X (r r' : relation X) :
   reflexive r'
   inclusion (seq r r') r'
   inclusion (clos_refl_trans r) r'.
Proof.
  red; ins; eapply clos_rt_rt1n in H1; induction H1; ins; eapply H0; vauto.
Qed.

Lemma inclusion_rt_rt2 :
   (A : Type) (r t : relation A),
  inclusion r (clos_refl_trans t)
  inclusion (clos_refl_trans r) (clos_refl_trans t).
Proof.
  red; ins; induction H0; eauto using clos_refl_trans.
Qed.

Hint Resolve
     inclusion_acyclic inclusion_restr_rel_l
     inclusion_step_t inclusion_union_r inclusion_union
     inclusion_seq_refl : inclusion.

Hint Resolve inclusion_rt_rt inclusion_r_rt inclusion_step_rt : inclusion.

Set up setoid rewriting

Require Import Setoid.

Lemma same_relation_refl A : reflexive (@same_relation A).
Proof. split; ins. Qed.

Lemma same_relation_sym A : symmetric (@same_relation A).
Proof. unfold same_relation; split; ins; desf. Qed.

Lemma same_relation_trans A : transitive (@same_relation A).
Proof. unfold same_relation; split; ins; desf; red; eauto. Qed.

Add Parametric Relation (X : Type) : (relation X) (@same_relation X)
 reflexivity proved by (@same_relation_refl X)
 symmetry proved by (@same_relation_sym X)
 transitivity proved by (@same_relation_trans X)
 as same_rel.

Add Parametric Morphism X : (@inclusion X) with
  signature same_relation ==> same_relation ==> iff as inclusion_mor.
Proof.
  unfold same_relation; ins; desf; split; red; ins; desf; eauto.
Qed.

Add Parametric Morphism X : (@union X) with
  signature same_relation ==> same_relation ==> same_relation as union_mor.
Proof.
  unfold same_relation, union; ins; desf; split; red; ins; desf; eauto.
Qed.

Add Parametric Morphism X : (@seq X) with
  signature same_relation ==> same_relation ==> same_relation as seq_mor.
Proof.
  unfold same_relation, seq; ins; desf; split; red; ins; desf; eauto.
Qed.

Add Parametric Morphism X P : (@restr_rel X P) with
  signature same_relation ==> same_relation as restr_rel_mor.
Proof.
  unfold same_relation, restr_rel; ins; desf; split; red; ins; desf; eauto.
Qed.

Add Parametric Morphism X : (@clos_trans X) with
  signature same_relation ==> same_relation as clos_trans_mor.
Proof.
  unfold same_relation; ins; desf; split; red; ins; desf; eauto using clos_trans_mon.
Qed.

Add Parametric Morphism X : (@clos_refl_trans X) with
  signature same_relation ==> same_relation as clos_relf_trans_mor.
Proof.
  unfold same_relation; ins; desf; split; red; ins; desf; eauto using clos_refl_trans_mon.
Qed.

Add Parametric Morphism X : (@clos_refl X) with
  signature same_relation ==> same_relation as clos_relf_mor.
Proof.
  unfold same_relation, clos_refl; ins; desf; split; red; ins; desf; eauto.
Qed.

Add Parametric Morphism X : (@irreflexive X) with
  signature same_relation ==> iff as irreflexive_mor.
Proof.
  unfold same_relation; ins; desf; split; red; ins; desf; eauto.
Qed.

Add Parametric Morphism X : (@acyclic X) with
  signature same_relation ==> iff as acyclic_mor.
Proof.
  unfold acyclic; ins; rewrite H; reflexivity.
Qed.

Add Parametric Morphism X : (@clos_trans X) with
  signature same_relation ==> eq ==> eq ==> iff
      as clos_trans_mor'.
Proof.
  unfold same_relation; ins; desf; split; ins; desf; eauto using clos_trans_mon.
Qed.

Add Parametric Morphism X : (@clos_refl_trans X) with
  signature same_relation ==> eq ==> eq ==> iff
      as clos_refl_trans_mor'.
Proof.
  unfold same_relation; ins; desf; split; ins; desf; eauto using clos_refl_trans_mon.
Qed.

Lemma same_relation_restr X (f : X Prop) rel rel' :
   ( x (CONDx: f x) y (CONDy: f y), rel x y rel' x y)
   (restr_rel f rel <--> restr_rel f rel').
Proof.
  unfold restr_rel; split; red; ins; desf; rewrite H in *; eauto.
Qed.

Lemma union_restr X (f : X Prop) rel rel' :
  union (restr_rel f rel) (restr_rel f rel')
  <--> restr_rel f (union rel rel').
Proof.
  split; unfold union, restr_rel, inclusion; ins; desf; eauto.
Qed.

Lemma clos_trans_restr X (f : X Prop) rel (UC: upward_closed rel f) :
  clos_trans (restr_rel f rel)
  <--> restr_rel f (clos_trans rel).
Proof.
  split; unfold union, restr_rel, inclusion; ins; desf; eauto.
    split; [|by apply clos_trans_restrD in H].
    by eapply clos_trans_mon; eauto; unfold restr_rel; ins; desf.
  clear H0; apply clos_trans_tn1 in H.
  induction H; eauto 10 using clos_trans.
Qed.

Lemma seq_union_l X (r1 r2 r : relation X) :
  seq (union r1 r2) r <--> union (seq r1 r) (seq r2 r).
Proof.
  unfold seq, union; split; red; ins; desf; eauto.
Qed.

Lemma seq_union_r X (r r1 r2 : relation X) :
  seq r (union r1 r2) <--> union (seq r r1) (seq r r2).
Proof.
  unfold seq, union; split; red; ins; desf; eauto.
Qed.

Lemma seqA X (r1 r2 r3 : relation X) :
  seq (seq r1 r2) r3 <--> seq r1 (seq r2 r3).
Proof.
  unfold seq, union; split; red; ins; desf; eauto.
Qed.

Lemma unionA X (r1 r2 r3 : relation X) :
  union (union r1 r2) r3 <--> union r1 (union r2 r3).
Proof.
  unfold seq, union; split; red; ins; desf; eauto.
Qed.

Lemma unionC X (r1 r2 : relation X) :
  union r1 r2 <--> union r2 r1.
Proof.
  unfold seq, union; split; red; ins; desf; eauto.
Qed.

Lemma rtE_left X (r r' : relation X) :
  seq r (clos_refl_trans r') <--> union r (seq (seq r r') (clos_refl_trans r')).
Proof.
  split; unfold union, seq, inclusion; ins; desf; eauto using clos_refl_trans.
  rewrite clos_refl_transE, t_step_rt in *; desf; eauto 8.
Qed.

Lemma rtE_right X (r r' : relation X) :
  seq (clos_refl_trans r') r <--> union r (seq (clos_refl_trans r') (seq r' r)).
Proof.
  split; unfold union, seq, inclusion; ins; desf; eauto using clos_refl_trans.
  rewrite clos_refl_transE, t_rt_step in *; desf; eauto 8.
Qed.

Lemma t_step_rt2 X (r : relation X) :
  clos_trans r <--> seq r (clos_refl_trans r).
Proof.
  split; unfold seq, inclusion; ins; rewrite t_step_rt in *; ins.
Qed.

Lemma seqFr X (r : relation X) :
  seq (fun _ _False) r <--> (fun _ _False).
Proof.
  split; unfold seq, inclusion; ins; desf.
Qed.

Lemma seqrF X (r : relation X) :
  seq r (fun _ _False) <--> (fun _ _False).
Proof.
  split; unfold seq, inclusion; ins; desf.
Qed.

Lemma unionrF X (r : relation X) :
  union r (fun _ _False) <--> r.
Proof.
  split; unfold union, inclusion; ins; desf; eauto.
Qed.

Lemma unionFr X (r : relation X) :
  union (fun _ _False) r <--> r.
Proof.
  split; unfold union, inclusion; ins; desf; eauto.
Qed.

Lemma crt_seq_swap X (r r' : relation X) :
  seq (clos_refl_trans (seq r r')) r <-->
  seq r (clos_refl_trans (seq r' r)).
Proof.
  split; ins; unfold seq; red; ins; desf.

  revert y H0; rename H into J; apply clos_rt_rtn1 in J.
  induction J; desf; eauto using rt_refl.
  ins; eapply IHJ in H; desf; eauto 10 using clos_refl_trans.

  revert x H; rename H0 into J; apply clos_rt_rt1n in J.
  induction J; desf; eauto using rt_refl.
  ins; eapply IHJ in H0; desf; eauto 10 using clos_refl_trans.
Qed.

Lemma crt_double X (r : relation X) :
  clos_refl_trans r <-->
  seq (clos_refl r) (clos_refl_trans (seq r r)).
Proof.
  unfold seq, clos_refl; split; red; ins; desc.
  rename H into J; apply clos_rt_rt1n in J; induction J; desf;
  eauto 8 using clos_refl_trans.
  eapply rt_trans with z; [desf; vauto|clear H];
  induction H0; desf; vauto.
Qed.

Hint Rewrite seqFr seqrF unionrF unionFr : samerel.

Lemmas about cycles


Lemma min_cycle X (rel rel' : relation X) (dom : X Prop)
    (TOT: is_total dom rel')
    (T : transitive rel')
    (INCL: inclusion rel' (clos_trans rel))
    (INV: a b (R: rel a b) (R': rel' b a), False) :
    acyclic rel
    acyclic (restr_rel (fun x¬ dom x) rel)
    ( x (CYC: rel x x) (D: dom x), False)
    ( c1 b1 (R: rel c1 b1) b2
       (S : clos_refl rel' b1 b2) c2
       (R': rel b2 c2) (S': clos_refl_trans (restr_rel (fun x¬ dom x) rel) c2 c1)
       (D1 : dom b1) (D2: dom b2) (ND1: ¬ dom c1) (ND2: ¬ dom c2), False).
Proof.
  split; intros A; repeat split; ins; desc; eauto.
    by intros x P; eapply A, clos_trans_mon; eauto; unfold restr_rel; ins; desf.
    by eauto using t_step.
    eapply (A c1), t_trans, rt_t_trans, t_rt_trans; eauto using t_step;
      try (by eapply clos_refl_trans_mon; eauto; unfold restr_rel; ins; desf).
    by red in S; desf; eauto using clos_refl_trans, clos_trans_in_rt.
  assert (INCL': a b (R: rel a b) (D: dom a) (D': dom b), rel' a b).
    by ins; destruct (classic (a = b)) as [|N];
       [|eapply TOT in N]; desf; exfalso; eauto.
  intros x P.

  assert (J: clos_refl_trans (restr_rel (fun x : X¬ dom x) rel) x x
             rel' x x dom x dom x
          dom x ( m n k, clos_refl rel' x m rel m n
            clos_refl_trans (restr_rel (fun x : X¬ dom x) rel) n k
             clos_refl rel k x
             dom m ¬ dom n ¬ dom k)
          ( k m,
            clos_refl_trans (restr_rel (fun x : X¬ dom x) rel) x k
            rel k m clos_refl rel' m x
            ¬ dom k dom m dom x)
          ( k m m' n,
            clos_refl_trans (restr_rel (fun x : X¬ dom x) rel) x k
            rel k m clos_refl rel' m m' rel m' n
            clos_refl_trans (restr_rel (fun x : X¬ dom x) rel) n x
            ¬ dom k dom m dom m' ¬ dom n)).
    by vauto.
  revert P J; generalize x at 1 4 6 8 11 13 14 16.
  unfold restr_rel in *; ins; apply clos_trans_tn1 in P; induction P; eauto.
  { rename x0 into x; desf; eauto.
    destruct (classic (dom x)); rewrite clos_refl_transE in *; desf; eauto using clos_trans.
      by destruct (clos_trans_restrD J); desf.
    by destruct (clos_trans_restrD J); eapply A, t_trans, t_step; vauto.

    unfold clos_refl in J3; desf.
      by eapply A1 with (c1 := x) (b2 := m); eauto using rt_trans, rt_step.
    destruct (classic (dom x)).
      by eapply A1 with (c1 := k) (b2 := m); eauto;
         unfold clos_refl in *; desf; eauto.
    by eapply A1 with (c1 := x) (b2 := m); eauto using rt_trans, rt_step.

    destruct (classic (dom y)).
      by rewrite clos_refl_transE in J; desf;
         destruct (clos_trans_restrD J); desf.
    by eapply A1 with (c1 := k) (b2 := x); eauto 8 using rt_trans, rt_step.

    destruct (classic (dom x)).
      by rewrite clos_refl_transE in J3; desf; destruct (clos_trans_restrD J3); desf.
    destruct (classic (dom y)).
      by rewrite clos_refl_transE in J; desf; destruct (clos_trans_restrD J); desf.
    by eapply A1 with (c1 := k) (b2 := m'); eauto 8 using rt_trans, rt_step.
  }
  eapply clos_tn1_trans in P; desf.
  {
    destruct (classic (dom y)).
      rewrite clos_refl_transE in J; desf.
        destruct (classic (dom x0)).
          by eapply IHP; right; left; eauto using t_step.
        eapply IHP; do 2 right; left; split; ins.
        by eexists y,x0,x0; repeat eexists; vauto; eauto using clos_trans_in_rt.
      destruct (clos_trans_restrD J).
      apply IHP; right; right; left; split; ins.
      by eexists y,z,x0; repeat eexists; vauto; eauto using clos_trans_in_rt.
    rewrite clos_refl_transE in J; desf.
      destruct (classic (dom x0)).
        eapply IHP; do 3 right; left.
        by eexists y,x0; repeat eexists; vauto; eauto using clos_trans_in_rt.
      by eapply IHP; left; vauto.
    by destruct (clos_trans_restrD J); eapply IHP; left;
       eauto 8 using rt_trans, rt_step, clos_trans_in_rt.
  }
  {
    destruct (classic (dom y)).
      by apply IHP; eauto 8 using clos_trans.
    apply IHP; do 3 right; left; eexists y, z;
    repeat eexists; vauto; eauto using clos_trans_in_rt.
  }
  { destruct (classic (dom y)).
      by eapply IHP; do 2 right; left; split; ins; eexists m; repeat eexists;
         eauto; red in J0; red; desf; eauto.
    destruct (classic (dom x0)).

    destruct (classic (m = x0)) as [|NEQ]; subst.
      by eapply IHP; do 3 right; left; eexists y,z; repeat eexists; vauto.
    eapply TOT in NEQ; desf.
      by eapply IHP; do 3 right; left; eexists y,z; repeat eexists; vauto;
         eauto; red; red in J0; desf; eauto.
    by red in J3; desf; eapply A1 with (c1 := k) (b2 := m);
       eauto 8 using rt_trans, rt_step, clos_trans_in_rt.

    by eapply IHP; do 4 right; eexists y,z; repeat eexists; vauto;
       unfold clos_refl in *; desf; vauto.
  }

  { destruct (classic (dom z)).
      by rewrite clos_refl_transE in J; desf;
         destruct (clos_trans_restrD J); desf.
    destruct (classic (y = m)) as [|NEQ]; desf.
      by unfold clos_refl in *; desf; eauto.
    destruct (classic (dom y)).
      eapply TOT in NEQ; desf.
        by unfold clos_refl in *; desf;
           apply IHP; right; left; eauto using t_rt_trans, t_step.
      by eapply A1 with (c1 := k) (b2 := y);
         eauto 8 using rt_trans, rt_step, clos_trans_in_rt.
    by eapply IHP; do 3 right; left; eexists k, m; repeat eexists; vauto.
  }

    destruct (classic (dom x0)).
      by rewrite clos_refl_transE in J3; desf; destruct (clos_trans_restrD J3); desf.
    destruct (classic (dom z)).
      by rewrite clos_refl_transE in J; desf; destruct (clos_trans_restrD J); desf.
    destruct (classic (y = m)) as [|NEQ]; desf.
      by eapply IHP; do 2 right; left; split; ins; eexists m', n; repeat eexists; vauto.
    destruct (classic (dom y)).
      eapply TOT in NEQ; desf.
        by unfold clos_refl in *; desf; eapply IHP; do 2 right; left; split; ins;
           eexists m', n; repeat eexists; vauto;
           eauto using rt_trans, clos_trans_in_rt.
      by eapply A1 with (c1 := k) (b2 := y);
         eauto 8 using rt_trans, rt_step, clos_trans_in_rt.
    by eapply IHP; do 4 right; eexists k,m,m'; repeat eexists; vauto.
Qed.

Lemma path_decomp_u1 X (rel : relation X) a b c d :
  clos_trans (rel UNION1 (a, b)) c d
  clos_trans rel c d
  clos_refl_trans rel c a clos_refl_trans rel b d.
Proof.
  induction 1; desf; eauto using clos_trans, clos_refl_trans, clos_trans_in_rt.
Qed.

Lemma cycle_decomp_u1 X (rel : relation X) a b c :
  clos_trans (rel UNION1 (a, b)) c c
  clos_trans rel c c clos_refl_trans rel b a.
Proof.
  ins; apply path_decomp_u1 in H; desf; eauto using clos_refl_trans.
Qed.

Lemma path_decomp_u_total :
   X (rel1 : relation X) dom rel2 (T: is_total dom rel2)
    (D: a b (REL: rel2 a b), dom a dom b) x y
    (C: clos_trans (fun a brel1 a b rel2 a b) x y),
    clos_trans rel1 x y
    ( m n,
      clos_refl_trans rel1 x m clos_trans rel2 m n clos_refl_trans rel1 n y)
    ( m n,
      clos_refl_trans rel1 m n clos_trans rel2 n m).
Proof.
  ins; induction C; desf; eauto 8 using rt_refl, clos_trans.
  by right; left; m, n; eauto using clos_trans_in_rt, rt_trans.
  by right; left; m, n; eauto using clos_trans_in_rt, rt_trans.

  destruct (classic (m = n0)) as [|NEQ]; desf.
  by right; left; m0, n; eauto using t_trans, rt_trans.
  eapply T in NEQ; desf.
    by right; right; n0, m; eauto 8 using clos_trans, rt_trans.
    by right; left; m0, n; eauto 8 using clos_trans, rt_trans.
    by apply t_step_rt in IHC0; desf; eapply D in IHC0; desf.
    by apply t_rt_step in IHC4; desf; eapply D in IHC6; desf.
Qed.

Lemma cycle_decomp_u_total :
   X (rel1 : relation X) dom rel2 (T: is_total dom rel2)
    (D: a b (REL: rel2 a b), dom a dom b) x
    (C: clos_trans (fun a brel1 a b rel2 a b) x x),
    clos_trans rel1 x x
    ( m n, clos_refl_trans rel1 m n clos_trans rel2 n m).
Proof.
  ins; exploit path_decomp_u_total; eauto; ins; desf; eauto 8 using rt_trans.
Qed.

Lemma clos_trans_disj_rel :
   X (rel rel' : relation X)
    (DISJ: x y (R: rel x y) z (R': rel' y z), False) x y
    (R: clos_trans rel x y) z
    (R': clos_trans rel' y z),
    False.
Proof.
  ins; induction R; eauto; induction R'; eauto.
Qed.

Lemma path_decomp_u_1 :
   X (rel rel' : relation X)
    (DISJ: x y (R: rel x y) z (R': rel' y z), False) x y
    (T: clos_trans (union rel rel') x y),
    clos_trans rel x y clos_trans rel' x y
     z, clos_trans rel' x z clos_trans rel z y.
Proof.
  unfold union; ins.
  induction T; desf; eauto 6 using clos_trans;
    try by exfalso; eauto using clos_trans_disj_rel.
Qed.

Lemma cycle_decomp_u_1 :
   X (rel rel' : relation X)
    (DISJ: x y (R: rel x y) z (R': rel' y z), False) x
    (T: clos_trans (union rel rel') x x),
    clos_trans rel x x clos_trans rel' x x.
Proof.
  ins; exploit path_decomp_u_1; eauto; ins; desf; eauto.
  exfalso; eauto using clos_trans_disj_rel.
Qed.

Lemma cycle_disj :
   X (rel : relation X)
    (DISJ: x y (R: rel x y) z (R': rel y z), False) x
    (T: clos_trans rel x x), False.
Proof.
  ins; inv T; eauto using clos_trans_disj_rel.
Qed.

Lemma clos_trans_restr_trans_mid :
   X (rel rel' : relation X) f x y
    (A : clos_trans (restr_rel f (fun x yrel x y rel' x y)) x y)
    z (B : rel y z) w
    (C : clos_trans (restr_rel f (fun x yrel x y rel' x y)) z w),
    clos_trans (restr_rel f (fun x yrel x y rel' x y)) x w.
Proof.
  ins; eapply t_trans, t_trans; vauto.
  eapply t_step; repeat split; eauto.
    by apply clos_trans_restrD in A; desc.
  by apply clos_trans_restrD in C; desc.
Qed.

Lemma clos_trans_restr_trans_cycle :
   X (rel rel' : relation X) f x y
    (A : clos_trans (restr_rel f (fun x yrel x y rel' x y)) x y)
    (B : rel y x),
    clos_trans (restr_rel f (fun x yrel x y rel' x y)) x x.
Proof.
  ins; eapply t_trans, t_step; eauto.
  by red; apply clos_trans_restrD in A; desf; auto.
Qed.

Lemma path_tur :
   X (r r' : relation X) (adom bdom : X Prop)
         (T: transitive r)
         (A: x y (R: r' x y), adom x)
         (B: x y (R: r' x y), bdom y) x y
    (P: clos_trans (fun x yr x y r' x y) x y),
    r x y
     z,
      clos_trans (fun x yr x y adom y r' x y) x z
      (z = y r z y bdom z).
Proof.
  ins; apply clos_trans_tn1 in P; induction P; desf; eauto 14 using clos_trans; clear P.
  apply clos_trans_t1n in IHP; induction IHP; intuition; desf; eauto 14 using clos_trans.
Qed.

Lemma path_ur :
   X (r r' : relation X) (adom bdom : X Prop)
         (A: x y (R: r' x y), adom x)
         (B: x y (R: r' x y), bdom y) x y
    (P: clos_trans (fun x yr x y r' x y) x y),
    clos_trans r x y
     z,
      clos_trans (fun x yclos_trans r x y adom y r' x y) x z
      (z = y clos_trans r z y bdom z).
Proof.
  ins; eapply path_tur; ins; vauto.
  by eapply clos_trans_mon; eauto; instantiate; ins; desf; eauto using t_step.
Qed.

Lemma path_tur2 :
   X (r r' : relation X) (adom bdom : X Prop)
         (T: transitive r')
         (A: x y (R: r x y), adom x)
         (B: x y (R: r x y), bdom y) x y
    (P: clos_trans (fun x yr x y r' x y) x y),
    r' x y
     z,
      (x = z r' x z adom z)
      clos_trans (fun x yr x y r' x y bdom x) z y.
Proof.
  ins; apply clos_trans_t1n in P; induction P; desf; eauto 14 using clos_trans; clear P.
  apply clos_trans_tn1 in IHP0; induction IHP0; intuition; desf; eauto 14 using clos_trans.
Qed.

Lemma path_ur2 :
   X (r r' : relation X) (adom bdom : X Prop)
         (A: x y (R: r x y), adom x)
         (B: x y (R: r x y), bdom y) x y
    (P: clos_trans (fun x yr x y r' x y) x y),
    clos_trans r' x y
     z,
      (x = z clos_trans r' x z adom z)
      clos_trans (fun x yr x y clos_trans r' x y bdom x) z y.
Proof.
  ins; eapply path_tur2; ins; vauto.
  by eapply clos_trans_mon; eauto; instantiate; ins; desf; eauto using t_step.
Qed.

Lemma cycle_ur :
   X (r r' : relation X) (adom : X Prop)
         (A: x y (R: r x y), adom x)
         (B: x y (R: r x y), adom y) x
    (P: clos_trans (fun x yr x y r' x y) x x),
    clos_trans r' x x
     x,
      clos_trans (fun x yr x y clos_trans r' x y adom x adom y) x x.
Proof.
  ins; eapply path_ur2 with (adom:=adom) (bdom:=adom) in P; desf; eauto.
  eapply clos_trans_mon,
    path_tur with (adom:=adom) (bdom:=adom) (r':=r)
                  (r:=fun a bclos_trans r' a b adom a) in P0;
  desf; try split; ins; desc; vauto; try tauto.
  right; z; eapply clos_trans_mon; eauto; instantiate; ins; tauto.

  assert (adom z) by (eapply t_step_rt in P0; desf; eauto).
  right; eexists; eapply clos_trans_mon; [eapply t_trans, P0|]; vauto;
  instantiate; ins; tauto.

  eapply clos_trans_mon with
    (r' := fun x yclos_trans r' x y adom x r x y) in P0; try tauto.
  eapply path_tur with (adom:=adom) (bdom:=adom) in P0; desf; eauto using clos_trans.

  assert (adom x) by (eapply t_rt_step in P0; desf; eauto).
  right; x; eapply clos_trans_mon; [eapply t_trans, P0|]; vauto;
  instantiate; ins; tauto.

  right; z0; eapply clos_trans_mon; [eapply t_trans, P0|];
  eauto 8 using clos_trans; instantiate; ins; tauto.

  by red; ins; desf; vauto.
Qed.

Lemma restr_eq_union :
   X (rel rel' : relation X) B (f: X B) x y
         (R: x y, rel' x y f x = f y),
   restr_eq_rel f (fun x yrel x y rel' x y) x y
   restr_eq_rel f rel x y rel' x y.
Proof.
  unfold restr_eq_rel; ins; intuition.
Qed.

Lemma clos_trans_restr_eq_union :
   X (rel rel' : relation X) B (f: X B)
         (R: x y, rel' x y f x = f y),
   clos_trans (restr_eq_rel f (fun x yrel x y rel' x y)) <-->
   clos_trans (fun x yrestr_eq_rel f rel x y rel' x y).
Proof.
  split; red; ins; eapply clos_trans_mon; eauto; ins; instantiate;
  rewrite restr_eq_union in *; eauto.
Qed.

Lemma acyclic_mon X (rel rel' : relation X) :
  acyclic rel inclusion rel' rel acyclic rel'.
Proof.
  eby repeat red; ins; eapply H, clos_trans_mon.
Qed.

Extension of a partial order to a total order

Section one_extension.

  Variable X : Type.
  Variable elem : X.
  Variable rel : relation X.

  Definition one_ext : relation X :=
    fun x y
      clos_trans rel x y
       clos_refl_trans rel x elem ¬ clos_refl_trans rel y elem.

  Lemma one_ext_extends x y : rel x y one_ext x y.
  Proof. vauto. Qed.

  Lemma one_ext_trans : transitive one_ext.
  Proof.
    red; ins; unfold one_ext in *; desf; desf;
      intuition eauto using clos_trans_in_rt, t_trans, rt_trans.
  Qed.

  Lemma one_ext_irr : acyclic rel irreflexive one_ext.
  Proof.
    red; ins; unfold one_ext in *; desf; eauto using clos_trans_in_rt.
  Qed.

  Lemma one_ext_total_elem :
     x, x elem one_ext elem x one_ext x elem.
  Proof.
    unfold one_ext; ins; rewrite !clos_refl_transE; tauto.
  Qed.

End one_extension.

Fixpoint tot_ext X (dom : list X) (rel : relation X) : relation X :=
  match dom with
    | nilclos_trans rel
    | x::lone_ext x (tot_ext l rel)
  end.

Lemma tot_ext_extends :
   X dom (rel : relation X) x y, rel x y tot_ext dom rel x y.
Proof.
  induction dom; ins; eauto using t_step, one_ext_extends.
Qed.

Lemma tot_ext_trans X dom (rel : relation X) : transitive (tot_ext dom rel).
Proof.
  induction dom; ins; vauto; apply one_ext_trans.
Qed.

Lemma tot_ext_irr :
   X (dom : list X) rel, acyclic rel irreflexive (tot_ext dom rel).
Proof.
  induction dom; ins.
  apply one_ext_irr, trans_irr_acyclic; eauto using tot_ext_trans.
Qed.

Lemma tot_ext_total :
   X (dom : list X) rel, is_total (fun xIn x dom) (tot_ext dom rel).
Proof.
  induction dom; red; ins; desf.
  eapply one_ext_total_elem in NEQ; desf; eauto.
  eapply not_eq_sym, one_ext_total_elem in NEQ; desf; eauto.
  eapply IHdom in NEQ; desf; eauto using one_ext_extends.
Qed.

Lemma tot_ext_inv :
   X dom rel (x y : X),
    acyclic rel tot_ext dom rel x y ¬ rel y x.
Proof.
  red; ins; eapply tot_ext_irr, tot_ext_trans, tot_ext_extends; eauto.
Qed.

Misc properties

Lemma clos_trans_imm :
   X (R : relation X) (I: irreflexive R)
         (T: transitive R) L (ND: NoDup L) a b
         (D: c, R a c R c b In c L)
         (REL: R a b),
    clos_trans (immediate R) a b.
Proof.
  intros until 3; induction ND; ins; vauto.
  destruct (classic (R a x R x b)) as [|N]; desf;
    [apply t_trans with x|]; eapply IHND; ins;
    exploit (D c); eauto; intro; desf; exfalso; eauto.
Qed.

Preferential union

Definition pref_union X (r r' : relation X) x y :=
  r x y r' x y ¬ r y x.

Lemma acyclic_pref_union :
   X (r r' : relation X) (dom : X Prop)
         (IRR: irreflexive r)
         (T: transitive r)
         (TOT: is_total dom r)
         (DL: x y (R: r' x y), dom x ¬ dom y),
    acyclic (pref_union r r').
Proof.
  ins; unfold pref_union.
  assert (EQ: restr_rel (fun x¬ dom x)
                    (fun x yr x y r' x y ¬ r y x)
          <--> restr_rel (fun x¬ dom x) r).
    unfold restr_rel; split; red; ins; desf; eauto.
    by exploit DL; eauto; ins; desf.

  apply min_cycle with (dom := dom) (rel' := r);
    repeat split; repeat red; ins; desf; eauto using t_step;
    try rewrite EQ in *;
    repeat match goal with
          | H : clos_trans _ _ _ |- _
            rewrite (ct_of_transitive (restr_rel_trans T)) in H
          | H : clos_refl_trans _ _ _ |- _
            rewrite (crt_of_transitive (restr_rel_trans T)) in H
          | H : r' _ _ |- _apply DL in H; desf
        end;
    unfold restr_rel, clos_refl in *; desf; eauto.
Qed.

Lemma in_pref_union :
   X (r r' : relation X) (dom : X Prop)
         (IRR: irreflexive r)
         (T: transitive r)
         (TOT: is_total dom r)
         (DL: x y (R: r' x y), dom x ¬ dom y) x y
         (R: clos_trans (pref_union r r') x y)
         (D: dom y),
    r x y.
Proof.
  unfold pref_union; ins; apply clos_trans_t1n in R; induction R; desf; eauto.
    by eapply DL in H; desf.
  apply clos_t1n_trans in R.
  assert (K:=DL _ _ H); desc.
  destruct (classic (x = z)) as [|N]; [|apply TOT in N]; desf; ins.
    by exfalso; eauto.
  exfalso; eapply acyclic_pref_union with (r:=r), t_trans, t_trans; vauto.
Qed.

Remove duplicate list elements (classical)

Fixpoint undup A dec (l: list A) :=
  match l with nilnil
    | x :: l
      if In_dec dec x l then undup dec l else x :: undup dec l
  end.

Lemma In_undup X dec (x: X) l : In x (undup dec l) In x l.
Proof.
  induction l; ins; des_if; ins; rewrite IHl; split; ins; desf; vauto.
Qed.

Lemma NoDup_undup X dec (l : list X) : NoDup (undup dec l).
Proof.
  induction l; ins; desf; constructor; eauto; rewrite In_undup; eauto.
Qed.

Lemma clos_trans_imm2 :
   X (dec : x y : X, {x = y} + {x y})
         (R : relation X) (I: irreflexive R)
         (T: transitive R) L a b
         (D: c, R a c R c b In c L)
         (REL: R a b),
    clos_trans (immediate R) a b.
Proof.
  ins; eapply clos_trans_imm with (L := undup dec L); ins;
  try rewrite In_undup; eauto using NoDup_undup.
Qed.

Lemma total_immediate_unique:
   X (eq_X_dec: (x y: X), {x=y} + {xy}) (rel: X X Prop) (P: X Prop)
         (Tot: is_total P rel)
         a b c (pa: P a) (pb: P b) (pc: P c)
         (iac: immediate rel a c)
         (ibc: immediate rel b c),
    a = b.
Proof.
  ins; destruct (eq_X_dec a b); eauto.
  exfalso; unfold immediate in *; desf.
  eapply Tot in n; eauto; desf; eauto.
Qed.

Lemma path_ut :
   X (r r' : relation X) (T: transitive r') x y
    (P: clos_refl_trans (fun x yr x y r' x y) x y),
     z w,
      clos_refl_trans r x z
      clos_refl_trans (fun x y z, r' x z clos_trans r z y) z w
      (w = y r' w y).
Proof.
  ins; induction P; eauto 8 using rt_refl.
    by desf; eauto 8 using rt_refl, rt_step.
  clear P1 P2; desf.

  rewrite clos_refl_transE in IHP2; desf;
  [rewrite clos_refl_transE, t_step_rt in IHP0; desf; eauto 8|
   rewrite clos_refl_transE, t_rt_step in IHP4; desf;
   eauto 8 using rt_trans, clos_trans_in_rt];
  (repeat eexists; [eauto|eapply rt_trans, rt_trans|vauto]); eauto;
  apply rt_step; eauto using t_trans.

  rewrite clos_refl_transE in IHP2; desf;
  [rewrite clos_refl_transE, t_step_rt in IHP0; desf; eauto 8|];
  (repeat eexists; [eauto|eapply rt_trans, rt_trans|vauto]); eauto;
  apply rt_step; eauto.

  rewrite clos_refl_transE in IHP2; desf; eauto 8 using rt_trans;
  rewrite clos_refl_transE, t_rt_step in IHP4; desf;
  eauto 8 using rt_trans, clos_trans_in_rt;
  (repeat eexists; [eauto|eapply rt_trans,rt_trans|right; eauto]); eauto;
  apply rt_step; eauto using t_trans.

  rewrite clos_refl_transE in IHP2; desf; eauto 8 using rt_trans;
  [rewrite clos_refl_transE, t_step_rt in IHP0; desf; eauto 8|];
  (repeat eexists; [eauto|eapply rt_trans,rt_trans|right; eauto]); eauto;
  apply rt_step; eauto using t_trans.
Qed.

Lemma path_ut2 :
   X (r r' : relation X) (T: transitive r') x y
    (P: clos_trans (fun x yr x y r' x y) x y),
    clos_trans r x y
     z w w',
      clos_refl_trans r x z
      clos_refl_trans (fun x y z, r' x z clos_trans r z y) z w
      r' w w'
      clos_refl_trans r w' y.
Proof.
  ins.
  rewrite t_rt_step in P; desc;
  eapply path_ut in P; ins; desf;
  try (by right; repeat eexists; eauto using clos_refl_trans, clos_trans_in_rt).

  rewrite clos_refl_transE in P1; desf.
    by rewrite t_rt_step; eauto.
  right; rewrite t_rt_step in P1; desf.
  by repeat eexists; eauto using clos_refl_trans, clos_trans_in_rt.

  by right; eexists _, _, y; repeat eexists;
     eauto using clos_refl_trans, clos_trans_in_rt.
Qed.

Lemma path_utd :
   X (r r' : relation X) (T: transitive r') dom
         (F: is_total dom r')
         (R: a b, r' a b dom a dom b) x y
    (P: clos_trans (fun x yr x y r' x y) x y),
    clos_trans r x y
    ( z w, clos_refl_trans r x z r' z w clos_refl_trans r w y)
    ( z w, r' z w clos_refl_trans r w z).
Proof.
  ins; induction P; desf; eauto 9 using clos_trans, clos_refl_trans, clos_trans_in_rt.
  right; destruct (classic (z1 = w)) as [|NEQ]; desf; eauto 8 using clos_refl_trans.
  eapply F in NEQ; desf; eauto 8 using clos_refl_trans.
  eapply R in IHP4; desf.
  eapply R in IHP0; desf.
Qed.

Lemma cycle_utd :
   X (r: relation X) (A: acyclic r)
         r' (T: transitive r') (IRR: irreflexive r') dom
         (F: is_total dom r')
         (R: a b, r' a b dom a dom b) x
    (P: clos_trans (fun x yr x y r' x y) x x),
   z w, r' z w clos_trans r w z.
Proof.
  ins; eapply path_utd in P; eauto; desf;
  try rewrite clos_refl_transE in *; desf;
  eauto using clos_trans; exfalso; eauto.
Qed.

Notation "P +++ Q" := (union P Q) (at level 50, left associativity).

Lemma acyclic_case_split A (R : relation A) f :
  acyclic R
  acyclic (restr_rel f R) ( x (NEG: ¬ f x) (CYC: clos_trans R x x), False).
Proof.
  unfold restr_rel; repeat split; repeat red; ins; desc; eauto.
    by eapply H, clos_trans_mon; eauto; instantiate; ins; desf.
  destruct (classic (f x)) as [X|X]; eauto.
  assert (M: clos_refl_trans (fun a bR a b f a f b) x x) by vauto.
  generalize X; revert H0 M X; generalize x at 2 3 5; ins.
  apply clos_trans_tn1 in H0; induction H0; eauto 6 using rt_t_trans, t_step.
  destruct (classic (f y)); eauto 6 using clos_refl_trans.
  eapply H1; eauto.
  eapply t_rt_trans, rt_trans; eauto using t_step, clos_trans_in_rt, clos_tn1_trans.
  by eapply clos_refl_trans_mon; eauto; instantiate; ins; desf.
Qed.

Lemma seqA2 X (r r' r'' : relation X) x y :
  seq (seq r r') r'' x y seq r (seq r' r'') x y.
Proof.
  unfold seq; split; ins; desf; eauto 8.
Qed.

Lemma path_unc X (r r' : relation X)
  (A: seq r r <--> (fun x yFalse))
  (B: seq r' r' <--> (fun x yFalse)) :
  clos_refl_trans (union r r') <-->
  clos_refl_trans (seq r r') +++
  (clos_refl_trans (seq r' r) +++
   (seq r (clos_refl_trans (seq r' r)) +++
    seq r' (clos_refl_trans (seq r r')))).
Proof.
  split.
    eapply inclusion_rt_l; [by vauto|].
    rewrite seq_union_l, !seq_union_r, <- !seqA, <- !t_step_rt2.
    rewrite (rtE_left r (seq r r')), (rtE_left r' (seq r' r)), <- !seqA.
    rewrite A, B, ?seqFr, ?unionrF, ?unionFr.
    by unfold union, seq; red; ins; desf;
       eauto 6 using clos_trans_in_rt, rt_refl.
  repeat first [apply inclusion_union_l|apply inclusion_seq_rt|
                eapply inclusion_rt_rt2]; vauto.
Qed.

Lemma pathp_unc X (r r' : relation X)
  (A: seq r r <--> (fun x yFalse))
  (B: seq r' r' <--> (fun x yFalse)) :
  clos_trans (union r r') <-->
  clos_trans (seq r r') +++
  (clos_trans (seq r' r) +++
   (seq r (clos_refl_trans (seq r' r)) +++
    seq r' (clos_refl_trans (seq r r')))).
Proof.
  rewrite t_step_rt2, path_unc; ins.
  rewrite seq_union_l, !seq_union_r, <- !seqA, <- !t_step_rt2.
  rewrite (rtE_left r (seq r r')), (rtE_left r' (seq r' r)), <- !seqA.
  rewrite A, B, ?seqFr, ?unionrF, ?unionFr.
  by unfold union, seq; split; red; ins; desf; eauto 8 using rt_refl.
Qed.

Lemma acyclic_unc X (r r' : relation X)
  (A: seq r r <--> (fun x yFalse))
  (B: seq r' r' <--> (fun x yFalse)) :
  acyclic (union r r') acyclic (seq r r').
Proof.
  unfold acyclic.
  rewrite pathp_unc, !irreflexive_union; ins.
  rewrite (irreflexive_seqC r), (irreflexive_seqC r').
  rewrite rtE_right, seqA, A, !seqrF, unionrF.
  rewrite rtE_right, seqA, B, !seqrF, unionrF.
  unfold seq, irreflexive; repeat split; ins; desf;
  eauto using t_step.

  apply t_rt_step in H0; desf; apply (H z0).
  exploit (proj2 (crt_seq_swap r r') z0 z); [by eexists x; vauto|].
  by intros [? ?]; desf; eapply rt_t_trans, t_step; eauto.

  eapply A; vauto.
  eapply B; vauto.
Qed.


This page has been generated by coqdoc