# Basic properties of relations

Require Import Vbase List Relations Classical.
Set Implicit Arguments.

Definitions of relations
Make arguments implicit

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.

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

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.

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.

Lemma clos_refl_transE a b :
clos_refl_trans r a b a = b clos_trans r a b.

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

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

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

Lemma t_step_rt x y :
clos_trans r x y z, r x z clos_refl_trans r z y.

Lemma t_rt_step x y :
clos_trans r x y z, clos_refl_trans r x z r z y.

Lemma clos_trans_of_transitive (T: transitive r) x y :
clos_trans r x y r x y.

Lemma ct_of_transitive (T: transitive r) x y :
clos_trans r x y r x y.

Lemma crt_of_transitive (T: transitive r) x y :
clos_refl_trans r x y clos_refl r x y.

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.

Lemma trans_irr_acyclic :
irreflexive r transitive r acyclic r.

Lemma restr_rel_trans :
transitive r transitive (restr_rel dom r).

Lemma upward_clos_trans P :
upward_closed r P upward_closed (clos_trans r) P.

Lemma max_elt_clos_trans a b:
max_elt r a clos_trans r a b False.

Lemma is_total_restr :
is_total dom r
is_total dom (restr_rel dom r).

Lemma clos_trans_restrD f x y :
clos_trans (restr_rel f r) x y f x f y.

Lemma clos_trans_restr_eqD B (f: A B) x y :
clos_trans (restr_eq_rel f r) x y f x = f y.

Lemma irreflexive_inclusion:
inclusion r r'
irreflexive r'
irreflexive r.

Lemma irreflexive_union :
irreflexive (union r r') irreflexive r irreflexive r'.

Lemma irreflexive_seqC :
irreflexive (seq r r') irreflexive (seq r' r).

Lemma clos_trans_inclusion :
inclusion r (clos_trans r).

Lemma clos_trans_inclusion_clos_refl_trans:
inclusion (clos_trans r) (clos_refl_trans r).

Lemma clos_trans_monotonic :
inclusion r r'
inclusion (clos_trans r) (clos_trans r').

Lemma inclusion_seq_trans t :
transitive t
inclusion r t
inclusion r' t
inclusion (seq r r') t.

Lemma inclusion_seq_rt :
inclusion r (clos_refl_trans r'')
inclusion r' (clos_refl_trans r'')
inclusion (seq r r') (clos_refl_trans r'').

Lemma inclusion_union_l :
inclusion r r''
inclusion r' r''
inclusion (union r r') r''.

Lemma inclusion_union_r :
inclusion r r' inclusion r r''
inclusion r (union r' r'').

Lemma inclusion_step_rt :
inclusion r r'
inclusion r (clos_refl_trans r').

Lemma inclusion_r_rt :
inclusion r r'
inclusion (clos_refl r) (clos_refl_trans r').

Lemma inclusion_rt_rt :
inclusion r r'
inclusion (clos_refl_trans r) (clos_refl_trans r').

Lemma inclusion_step_t :
inclusion r r'
inclusion r (clos_trans r').

Lemma inclusion_t_t :
inclusion r r'
inclusion (clos_trans r) (clos_trans r').

Lemma inclusion_acyclic :
inclusion r r'
acyclic r'
acyclic r.

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.

Lemma clos_trans_of_clos_trans A (r : relation A) x y :
clos_trans (clos_trans r) x y
clos_trans r x y.

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

Lemma inclusion_restr_rel_l :
{A : Type} (dom : A Prop) (R1 R1' : relation A)
(HINC: inclusion R1' R1),
inclusion (restr_rel dom R1') R1.

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.

Lemma inclusion_rt_l X (r r' : relation X) :
reflexive r'
inclusion (seq r r') r'
inclusion (clos_refl_trans r) r'.

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

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

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 : (@inclusion X) with
signature same_relation same_relation iff as inclusion_mor.

Add Parametric Morphism X : (@union X) with
signature same_relation same_relation same_relation as union_mor.

Add Parametric Morphism X : (@seq X) with
signature same_relation same_relation same_relation as seq_mor.

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

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

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

Add Parametric Morphism X : (@clos_refl X) with
signature same_relation same_relation as clos_relf_mor.

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

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

Add Parametric Morphism X : (@clos_trans X) with
signature same_relation eq eq iff
as clos_trans_mor'.

Add Parametric Morphism X : (@clos_refl_trans X) with
signature same_relation eq eq iff
as clos_refl_trans_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 : X Prop) rel rel' :
union (restr_rel f rel) (restr_rel f rel')
restr_rel f (union rel rel').

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

Lemma seq_union_l X (r1 r2 r : relation X) :
seq (union r1 r2) r union (seq r1 r) (seq r2 r).

Lemma seq_union_r X (r r1 r2 : relation X) :
seq r (union r1 r2) union (seq r r1) (seq r r2).

Lemma seqA X (r1 r2 r3 : relation X) :
seq (seq r1 r2) r3 seq r1 (seq r2 r3).

Lemma unionA X (r1 r2 r3 : relation X) :
union (union r1 r2) r3 union r1 (union r2 r3).

Lemma unionC X (r1 r2 : relation X) :
union r1 r2 union r2 r1.

Lemma rtE_left X (r r' : relation X) :
seq r (clos_refl_trans r') union r (seq (seq r r') (clos_refl_trans r')).

Lemma rtE_right X (r r' : relation X) :
seq (clos_refl_trans r') r union r (seq (clos_refl_trans r') (seq r' r)).

Lemma t_step_rt2 X (r : relation X) :
clos_trans r seq r (clos_refl_trans r).

Lemma seqFr X (r : relation X) :
seq (fun _ _False) r (fun _ _False).

Lemma seqrF X (r : relation X) :
seq r (fun _ _False) (fun _ _False).

Lemma unionrF X (r : relation X) :
union r (fun _ _False) r.

Lemma unionFr X (r : relation X) :
union (fun _ _False) r r.

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

Lemma crt_double X (r : relation X) :
clos_refl_trans r
seq (clos_refl r) (clos_refl_trans (seq r r)).

Hint Rewrite seqFr seqrF unionrF unionFr : samerel.

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

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.

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.

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

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

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

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.

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.

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.

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.

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

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

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.

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.

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.

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.

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

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

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.

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

Lemma tot_ext_trans X dom (rel : relation X) : transitive (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 xIn 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.

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.

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

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.

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.

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} + {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.

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

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.

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

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.

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

Lemma seqA2 X (r r' r'' : relation X) x y :
seq (seq r r') r'' x y seq r (seq r' r'') x y.

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

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

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