Require Import Vbase List Relations Classical.
Set Implicit Arguments.

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 X 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 b ⇒ rel 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 y ⇒ x = a ∧ y = b ∨ r x y) (at level 100).

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

Lemma clos_trans_mon A (r r' : relation A) a b :
  clos_trans A r a b →
  (∀ a b, r a b → r' a b) →
  clos_trans A r' a b.

Lemma clos_refl_trans_mon A (r r' : relation A) a b :
  clos_refl_trans A r a b →
  (∀ a b, r a b → r' a b) →
  clos_refl_trans A r' a b.

Lemma clos_refl_transE A r a b :
  clos_refl_trans A r a b ↔ a = b ∨ clos_trans A r a b.

Lemma clos_trans_in_rt A r a b :
  clos_trans A r a b → clos_refl_trans A r a b.

Lemma rt_t_trans A r a b c :
  clos_refl_trans A r a b → clos_trans A r b c → clos_trans A r a c.

Lemma t_rt_trans A r a b c :
  clos_trans A r a b → clos_refl_trans A r b c → clos_trans A r a c.

Lemma t_step_rt A R x y :
  clos_trans A R x y ↔ ∃ z, R x z ∧ clos_refl_trans A R z y.

Lemma t_rt_step A R x y :
  clos_trans A R x y ↔ ∃ z, clos_refl_trans A R x z ∧ R z y.

Lemma clos_trans_of_transitive A R (T: transitive A R) x y :
  clos_trans A R x y → R x y.

Lemma clos_trans_eq :
  ∀ X (rel: relation X) Y (f : X → Y)
         (H: ∀ a b (SB: rel a b), f a = f b) a b
         (C: clos_trans _ rel a b),
    f a = f b.

Lemma trans_irr_acyclic :
  ∀ A R, irreflexive R → transitive A R → acyclic R.

Lemma restr_rel_trans :
  ∀ X dom rel, transitive X rel → transitive X (restr_rel dom rel).

Lemma clos_trans_of_clos_trans1 :
  ∀ X rel1 rel2 x y,
    clos_trans X (fun a b ⇒ clos_trans _ rel1 a b ∨ rel2 a b) x y ↔
    clos_trans X (fun a b ⇒ rel1 a b ∨ rel2 a b) x y.

Lemma upward_clos_trans:
  ∀ X (rel: X → X → Prop) P,
    upward_closed rel P → upward_closed (clos_trans _ rel) P.

Lemma max_elt_clos_trans:
  ∀ X rel a b
         (hmax: max_elt rel a)
         (hclos: clos_trans X rel a b),
    False.

Lemma is_total_restr :
  ∀ X (dom : X → Prop) rel,
    is_total dom rel →
    is_total dom (restr_rel dom rel).

Lemma clos_trans_restrD :
  ∀ X rel f x y, clos_trans X (restr_rel f rel) x y → f x ∧ f y.

Lemma clos_trans_restr_eqD :
  ∀ A rel B (f: A → B) x y, clos_trans _ (restr_eq_rel f rel) x y → f x = f y.

Lemma irreflexive_inclusion:
  ∀ X (R1 R2: relation X),
  inclusion X R1 R2 →
  irreflexive R2 →
  irreflexive R1.

Lemma clos_trans_inclusion:
  ∀ X (R: relation X),
  inclusion X R (clos_trans X R).

Lemma clos_trans_inclusion_clos_refl_trans:
  ∀ X (R: relation X),
  inclusion X (clos_trans X R) (clos_refl_trans X R).

Lemma clos_trans_monotonic:
  ∀ X (R1 R2: relation X),
  inclusion X R1 R2 →
  inclusion X (clos_trans X R1) (clos_trans X R2).

Require Import Setoid.

Lemma same_relation_refl: ∀ A, reflexive _ (same_relation A).

Lemma same_relation_sym: ∀ A, symmetric _ (same_relation A).

Lemma same_relation_trans: ∀ A, transitive _ (same_relation A).

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 : (@union X) with
  signature (@same_relation X) ⇒ (@same_relation X) ⇒ (@same_relation X) as union_mor.

Add Parametric Morphism X P : (@restr_rel X P) with
  signature (@same_relation X) ⇒ (@same_relation X) as restr_rel_mor.

Add Parametric Morphism X : (@clos_trans X) with
  signature (@same_relation X) ⇒ (@same_relation X) as clos_trans_mor.

Add Parametric Morphism X : (@clos_refl_trans X) with
  signature (@same_relation X) ⇒ (@same_relation X) as clos_relf_trans_mor.

Add Parametric Morphism X : (@irreflexive X) with
  signature (@same_relation X) ⇒ iff as irreflexive_mor.

Add Parametric Morphism X : (@acyclic X) with
  signature (@same_relation X) ⇒ iff as acyclic_mor.

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').

Lemma union_restr X f rel rel' :
  union X (restr_rel f rel) (restr_rel f rel')
  <-→ restr_rel f (union _ rel rel').

Lemma clos_trans_restr X f rel (UC: upward_closed rel f) :
  clos_trans X (restr_rel f rel)
  <-→ restr_rel f (clos_trans _ rel).

Lemma path_decomp_u1 X (rel : relation X) a b c d :
  clos_trans X (rel UNION1 (a, b)) c d →
  clos_trans X rel c d ∨
  clos_refl_trans X rel c a ∧ clos_refl_trans X rel b d.

Lemma cycle_decomp_u1 X (rel : relation X) a b c :
  clos_trans X (rel UNION1 (a, b)) c c →
  clos_trans X rel c c ∨ clos_refl_trans X rel b a.

Lemma path_decomp_u_total :
  ∀ X rel1 dom rel2 (T: is_total dom rel2)
    (D: ∀ a b (REL: rel2 a b), dom a ∧ dom b) x y
    (C: clos_trans X (fun a b ⇒ rel1 a b ∨ rel2 a b) x y),
    clos_trans X rel1 x y ∨
    (∃ m n,
      clos_refl_trans X rel1 x m ∧ clos_trans X rel2 m n ∧ clos_refl_trans X rel1 n y) ∨
    (∃ m n,
      clos_refl_trans X rel1 m n ∧ clos_trans X rel2 n m).

Lemma cycle_decomp_u_total :
  ∀ X rel1 dom rel2 (T: is_total dom rel2)
    (D: ∀ a b (REL: rel2 a b), dom a ∧ dom b) x
    (C: clos_trans X (fun a b ⇒ rel1 a b ∨ rel2 a b) x x),
    clos_trans X rel1 x x ∨
    (∃ m n, clos_refl_trans X rel1 m n ∧ clos_trans X rel2 n m).

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.

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 X (union X 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.

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 X (union X rel rel') x x),
    clos_trans _ rel x x ∨ clos_trans _ rel' x x.

Lemma cycle_disj :
  ∀ X (rel : relation X)
    (DISJ: ∀ x y (R: rel x y) z (R': rel y z), False) x
    (T: clos_trans X rel x x), False.

Lemma clos_trans_restr_trans_mid :
  ∀ X (rel rel' : relation X) f x y
    (A : clos_trans _ (restr_rel f (fun x y ⇒ rel x y ∨ rel' x y)) x y)
    z (B : rel y z) w
    (C : clos_trans _ (restr_rel f (fun x y ⇒ rel x y ∨ rel' x y)) z w),
    clos_trans _ (restr_rel f (fun x y ⇒ rel x y ∨ rel' x y)) x w.

Lemma clos_trans_restr_trans_cycle :
  ∀ X (rel rel' : relation X) f x y
    (A : clos_trans _ (restr_rel f (fun x y ⇒ rel x y ∨ rel' x y)) x y)
    (B : rel y x),
    clos_trans _ (restr_rel f (fun x y ⇒ rel x y ∨ rel' x y)) x x.

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 y ⇒ rel x y ∨ rel' x y) x y ↔
   restr_eq_rel f rel x y ∨ rel' x y.

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 y ⇒ rel x y ∨ rel' x y)) <-→
   clos_trans _ (fun x y ⇒ restr_eq_rel f rel x y ∨ rel' x y).

Lemma acyclic_mon X (rel rel' : relation X) :
  acyclic rel → inclusion _ rel' rel → acyclic rel'.

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.

  Lemma one_ext_trans : transitive _ one_ext.

  Lemma one_ext_irr : acyclic rel → irreflexive one_ext.

  Lemma one_ext_total_elem :
    ∀ x, x ≠ elem → one_ext elem x ∨ one_ext x elem.

End one_extension.

Fixpoint tot_ext X (dom : list X) (rel : relation X) : relation X :=
  match dom with
    | nil ⇒ clos_trans _ rel
    | x::l ⇒ one_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.

Lemma tot_ext_trans : ∀ X dom rel, transitive X (tot_ext dom rel).

Lemma tot_ext_irr :
  ∀ X (dom : list X) rel, acyclic rel → irreflexive (tot_ext dom rel).

Lemma tot_ext_total :
  ∀ X (dom : list X) rel, is_total (fun x ⇒ In x dom) (tot_ext dom rel).

Lemma tot_ext_inv :
  ∀ X dom rel (x y : X),
    acyclic rel → tot_ext dom rel x y → ¬ rel y x.

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.

Require Import extralib.

Fixpoint undup A dec (l: list A) :=
  match l with nil ⇒ nil
    | 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.

Lemma NoDup_undup X dec (l : list X) : NoDup (undup dec l).

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.

Lemma total_immediate_unique:
  ∀ X (eq_X_dec: ∀ (x y: X), {x=y} + {x≠y}) (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.