Library CoLoR.Util.Relation.RelUtil
CoLoR, a Coq library on rewriting and termination.
See the COPYRIGHTS and LICENSE files.
General definitions and results about relations.
- Frederic Blanqui, 2005-02-17
- Adam Koprowski and Hans Zantema, 2007-03
- Joerg Endrullis and Dimitri Hendriks, 2008-07
Set Implicit Arguments.
Notations for some relations and operations on relations.
Notation rel := relation.
Notation incl := inclusion.
Infix "<<" := incl (at level 50) : relation_scope.
Notation same := same_relation.
Infix "==" := same (at level 70).
Infix "U" := union (at level 45) : relation_scope.
Notation "x #" := (clos_refl_trans x) (at level 35) : relation_scope.
Notation "x !" := (clos_trans x) (at level 35) : relation_scope.
Open Scope relation_scope.
Properties of incl.
Instance incl_refl A : Reflexive (@incl A).
Ltac incl_refl := apply incl_refl.
Instance incl_trans A : Transitive (@incl A).
Ltac incl_trans S := apply incl_trans with S; try incl_refl.
Instance incl_same A : Proper (same ==> same ==> impl) (@incl A).
Lemma incl_elim A (R S : rel A) : R << S -> forall x y, R x y -> S x y.
Properties of same.
Lemma rel_eq A (R S : rel A) : R == S <-> forall x y, R x y <-> S x y.
Instance same_equiv A : Equivalence (@same A).
Basic meta-theorems.
Lemma eq_incl_refl_rel A (R : rel A) : Reflexive R -> eq << R.
Lemma sym A (R : rel A) x y : Symmetric R -> (R x y <-> R y x).
Morphisms wrt incl and same.
Instance refl_same A : Proper (same ==> impl) (@Reflexive A).
Instance sym_same A : Proper (same ==> impl) (@Symmetric A).
Instance trans_same A : Proper (same ==> impl) (@Transitive A).
Instance equiv_same A : Proper (same ==> impl) (@Equivalence A).
Properties of Proper.
Lemma prop2_incl A B C (f : A -> B -> C) :
Proper (incl --> incl --> incl ==> impl)
(fun R S T => Proper (R ==> S ==> T) f).
Lemma prop3_incl A B C D (f : A -> B -> C -> D) :
Proper (incl --> incl --> incl --> incl ==> impl)
(fun R S T V => Proper (R ==> S ==> T ==> V) f).
Lemma prop4_incl A B C D E (f : A -> B -> C -> D -> E) :
Proper (incl --> incl --> incl --> incl --> incl ==> impl)
(fun R S T V W => Proper (R ==> S ==> T ==> V ==> W) f).
Instance prop_rel_same A (E : rel A) :
Proper (same ==> impl) (Proper (E ==> E ==> impl)).
Lemma prop_subrel A (R S : rel A) :
Equivalence S -> subrelation R S -> Proper (R ==> R ==> impl) S.
Lemma prop_rel_sym A B (f : A -> B -> Prop) R S :
Symmetric R -> Symmetric S
-> Proper (R ==> S ==> impl) f -> Proper (R ==> S ==> iff) f.
Instance equiv_prop A (R : rel A) :
Transitive R -> Symmetric R -> Proper (R ==> R ==> impl) R.
Empty relation.
Relation associated to a boolean function.
Boolean function associated to a decidable relation.
Section bool_of_rel.
Variables (A : Type) (R : rel A) (R_dec : rel_dec R).
Definition bool_of_rel t u := if R_dec t u then true else false.
Lemma bool_of_rel_true x y : bool_of_rel x y = true <-> R x y.
Lemma bool_of_rel_false x y : bool_of_rel x y = false <-> ~R x y.
Lemma bool_of_rel_refl x : Reflexive R -> bool_of_rel x x = true.
Global Instance bool_of_rel_prop :
Symmetric R -> Transitive R -> Proper (R ==> R ==> Logic.eq) bool_of_rel.
End bool_of_rel.
Definition of some properties on relations.
Definition classic_left_total A B (R : A -> B -> Prop) :=
forall x, exists y, R x y.
Definition left_total A B (R : A -> B -> Prop) :=
forall x, {y | R x y}.
Definition functional A B (R : A -> B -> Prop) :=
forall x y z, R x y -> R x z -> y = z.
Definition finitely_branching A B (R : A -> B -> Prop) :=
forall x, {l | forall y, R x y <-> In y l}.
Definition irreflexive A (R : rel A) := forall x, ~R x x.
Definition asymmetric A (R : rel A) := forall x y, R x y -> ~R y x.
Predicate saying that f is an infinite sequence of R-steps.
Definition IS A (R : rel A) f := forall i, R (f i) (f (S i)).
Definition EIS A (R : rel A) := exists f, IS R f.
Definition NT A (R : rel A) x := exists f, f 0 = x /\ IS R f.
Definition EIS A (R : rel A) := exists f, IS R f.
Definition NT A (R : rel A) x := exists f, f 0 = x /\ IS R f.
Predicate saying that f and g describe an infinite sequence
of R-steps modulo E: for all i, f(i) E g(i) R f(i+1).
Definition ISMod A (E R : rel A) (f g : nat -> A) :=
forall i, E (f i) (g i) /\ R (g i) (f (S i)).
Definition quasi_ordering A (R : rel A) := reflexive R /\ transitive R.
Definition ordering A (R : rel A) :=
reflexive R /\ transitive R /\ antisymmetric R.
Definition strict_ordering A (R : rel A) := irreflexive R /\ transitive R.
forall i, E (f i) (g i) /\ R (g i) (f (S i)).
Definition quasi_ordering A (R : rel A) := reflexive R /\ transitive R.
Definition ordering A (R : rel A) :=
reflexive R /\ transitive R /\ antisymmetric R.
Definition strict_ordering A (R : rel A) := irreflexive R /\ transitive R.
Strict part.
Intersection.
Definition intersection A (R S : rel A) : rel A := fun x y => R x y /\ S x y.
Lemma intersection_dec A (R S : rel A) (Rdec : rel_dec R) (Sdec : rel_dec S) :
rel_dec (intersection R S).
Finitely branching relations.
Section finitely_branching.
Variables (A : Type) (R : rel A) (FB : finitely_branching R).
Definition sons x := proj1_sig (FB x).
Lemma in_sons_R : forall x y, In y (sons x) -> R x y.
Lemma R_in_sons : forall x y, R x y -> In y (sons x).
End finitely_branching.
Equivalence relation associated to a PreOrder.
Definition inter_transp A (R : rel A) : rel A := fun x y => R x y /\ R y x.
Lemma inter_transp_refl A (R : rel A) :
Reflexive R -> Reflexive (inter_transp R).
Lemma inter_transp_sym A (R : rel A) : Symmetric (inter_transp R).
Lemma inter_transp_trans A (R : rel A) :
Transitive R -> Transitive (inter_transp R).
Lemma inter_transp_incl A (R : rel A) : inter_transp R << R.
Properties of IS.
Instance IS_incl A : Proper (incl ==> Logic.eq ==> impl) (@IS A).
Instance IS_same A : Proper (same ==> Logic.eq ==> impl) (@IS A).
Instance EIS_same A : Proper (same ==> impl) (@EIS A).
Lemma NT_IS_elt A (R : rel A) f k : IS R f -> NT R (f k).
Lemma red_NT A (R : rel A) t u : R t u -> NT R u -> NT R t.
Properties of irreflexive.
Monotony.
Definition monotone A B (R : rel A) (S : rel B) f :=
forall x y, R x y -> S (f x) (f y).
Lemma monotone_transp A B (R : rel A) (S : rel B) f :
monotone R S f -> monotone (transp R) (transp S) f.
Composition.
Definition compose A (R S : rel A) : rel A :=
fun x y => exists z, R x z /\ S z y.
Infix "@" := compose (at level 40) : relation_scope.
Instance compose_incl A : Proper (incl ==> incl ==> incl) (@compose A).
Ltac comp := apply compose_incl; try incl_refl.
Instance compose_same A : Proper (same ==> same ==> same) (@compose A).
Definition absorbs_right A (R S : rel A) := R @ S << R.
Definition absorbs_left A (R S : rel A) := S @ R << R.
Lemma comp_assoc A (R S T : rel A) : (R @ S) @ T << R @ (S @ T).
Lemma comp_assoc' A (R S T : rel A) : R @ (S @ T) << (R @ S) @ T.
Ltac assoc :=
match goal with
| |- (?s @ ?t) @ ?u << _ => incl_trans (s @ (t @ u)); try apply comp_assoc
| |- ?s @ (?t @ ?u) << _ => incl_trans ((s @ t) @ u); try apply comp_assoc'
| |- _ << (?s @ ?t) @ ?u => incl_trans (s @ (t @ u)); try apply comp_assoc'
| |- _ << ?s @ (?t @ ?u) => incl_trans ((s @ t) @ u); try apply comp_assoc
end.
Lemma absorbs_left_rtc A (R S : rel A) : R @ S << S -> R# @ S << S.
Lemma absorbs_right_rtc A (R S : rel A) : S @ R << S -> S @ R# << S.
Properties of union.
Instance union_incl A : Proper (incl ==> incl ==> incl) (@union A).
Ltac union := apply union_incl; try incl_refl.
Instance union_same A : Proper (same ==> same ==> same) (@union A).
Lemma union_commut A (R S : rel A) : R U S == S U R.
Lemma union_assoc A (R S T : rel A) : (R U S) U T == R U (S U T).
Lemma comp_union_l A (R S T : rel A) : (R U S) @ T == (R @ T) U (S @ T).
Lemma comp_union_r A (R S T : rel A) : T @ (R U S) == (T @ R) U (T @ S).
Lemma union_empty_r A (R : rel A) : R U empty_rel == R.
Lemma union_empty_l A (R : rel A) : empty_rel U R == R.
Lemma incl_union_l A (R S T : rel A) : R << S -> R << S U T.
Lemma incl_union_r A (R S T : rel A) : R << T -> R << S U T.
Lemma union_incl_eq A (R R' S : rel A) : R U R' << S <-> R << S /\ R' << S.
Reflexive closure.
Definition clos_refl A (R : rel A) : rel A := eq U R.
Notation "x %" := (clos_refl x) (at level 35) : relation_scope.
Instance rc_incl A : Proper (incl ==> incl) (@clos_refl A).
Instance rc_same A : Proper (same ==> same) (@clos_refl A).
Instance rc_refl A (R : rel A) : Reflexive (R%).
Instance rc_trans A (R : rel A) : Transitive R -> Transitive (R%).
Lemma incl_rc A (R : rel A) : R << R%.
Compatibility closure.
Section comp_clos.
Variables (A : Type) (E : rel A) (E_eq : Equivalence E).
Inductive comp_clos (R : rel A) : rel A :=
| comp_clos_intro u u' v v' : E u u' -> E v v' -> R u' v' -> comp_clos R u v.
Lemma comp_clos_intro_refl (R : rel A) t u : R t u -> comp_clos R t u.
Lemma comp_clos_eq R : same (comp_clos R) (E @ (R @ E)).
Lemma incl_comp_clos R : R << comp_clos R.
Global Instance comp_clos_incl : Proper (incl ==> incl) comp_clos.
Global Instance comp_clos_same : Proper (same ==> same) comp_clos.
Lemma comp_clos_union R S :
same (comp_clos (R U S)) (comp_clos R U comp_clos S).
Global Instance comp_clos_prop R : Proper (E ==> E ==> impl) (comp_clos R).
End comp_clos.
Properties of clos_trans.
Instance tc_trans A (R : rel A) : Transitive (R!).
Instance tc_incl A : Proper (incl ==> incl) (@clos_trans A).
Instance tc_same A : Proper (same ==> same) (@clos_trans A).
Lemma incl_tc A (R S : rel A) : R << S -> R << S!.
Lemma trans_tc_incl A (R : rel A) : Transitive R -> R! << R.
Lemma trans_comp_incl A (R : rel A) : Transitive R -> R @ R << R.
Lemma absorbs_left_tc A (R S : rel A) : R @ S << S -> R! @ S << S.
Lemma tc_absorbs_left A (R S : rel A) : R @ S << S -> R @ S! << S!.
Lemma trans_intro A (R : rel A) : R @ R << R <-> Transitive R.
Lemma comp_tc_idem A (R : rel A) : R! @ R! << R!.
Lemma tc_min A (R S : rel A) : R << S -> Transitive S -> R! << S.
Lemma trans_tc A (R : rel A) : Transitive R -> R! == R.
Lemma tc_idem A (R : rel A) : R!! == R!.
Lemma tc_eq A (R S : rel A) : S << R -> R << S! -> R! == S!.
Lemma tc_incl_trans A (R S : rel A) : Transitive S -> R << S -> R! << S.
Instance tc_prop A (E R : rel A) : Reflexive E ->
Proper (E ==> E ==> impl) R -> Proper (E ==> E ==> impl) (R!).
Lemma tc_prop_iff A (R E : rel A) : Equivalence E
-> Proper (E ==> E ==> iff) R -> Proper (E ==> E ==> iff) (clos_trans R).
Lemma tc_step_l A (R : rel A) x y :
R! x y -> R x y \/ (exists2 z, R x z & R! z y).
Lemma tc_step_r A (R : rel A) x y :
R! x y -> R x y \/ (exists2 z, R! x z & R z y).
Lemma tc_transp A (R : rel A) : transp (R!) == (transp R)!.
Symmetric closure of a relation.
Section clos_sym.
Variable (A : Type) (R : rel A).
Inductive clos_sym : rel A :=
| s_step : forall x y, R x y -> clos_sym x y
| s_sym : forall x y, clos_sym y x -> clos_sym x y.
Global Instance sc_sym : Symmetric clos_sym.
End clos_sym.
Reflexive, transitive and symmetric closure of a relation.
Section clos_equiv.
Variable (A : Type) (R : rel A).
Inductive clos_equiv : rel A :=
| e_step : forall x y, R x y -> clos_equiv x y
| e_refl : forall x, clos_equiv x x
| e_trans : forall x y z, clos_equiv x y -> clos_equiv y z -> clos_equiv x z
| e_sym : forall x y, clos_equiv x y -> clos_equiv y x.
Global Instance ec_equiv : Equivalence clos_equiv.
End clos_equiv.
Instance ec_incl A : Proper (incl ==> incl) (@clos_equiv A).
Lemma ec_min A (R S : rel A) : Equivalence S -> R << S -> clos_equiv R << S.
Properties of clos_refl_trans.
Instance rtc_refl A (R : rel A) : Reflexive (R#).
Instance rtc_trans A (R : rel A) : Transitive (R#).
Instance rtc_incl A : Proper (incl ==> incl) (@clos_refl_trans A).
Instance rtc_same A : Proper (same ==> same) (@clos_refl_trans A).
Lemma incl_rtc A (R : rel A) : R << R#.
Lemma tc_incl_rtc A (R : rel A) : R! << R#.
Lemma tc_split A (R : rel A) : R! << R @ R#.
Lemma rc_incl_rtc A (R : rel A) : R% << R#.
Lemma rtc_split A (R : rel A) : R# << eq U R!.
Lemma rtc_split_eq A (R : rel A) : R# == eq U R!.
Lemma rtc_split2 A (R : rel A) : R# << eq U R @ R#.
Lemma tc_split_inv A (R : rel A) : R# @ R << R!.
Lemma tc_merge A (R : rel A) : R @ R# << R!.
Lemma rtc_transp A (R : rel A) : transp (R#) << (transp R)#.
Lemma incl_rtc_rtc A (R S : rel A) : R << S# -> R# << S#.
Lemma comp_rtc_idem A (R : rel A) : R# @ R# << R#.
Lemma trans_rtc_incl A (R : rel A) : Reflexive R -> Transitive R -> R# << R.
Lemma rtc_invol A (R : rel A) : R # # == R #.
Lemma rtc_intro_seq A (R : rel A) f i : forall j, i <= j ->
(forall k, i <= k < j -> R (f k) (f (1+k))) -> R# (f i) (f j).
Lemma rtc_min A (R S : rel A) : PreOrder S -> R << S -> R# << S.
Instance rtc_sym A (R : rel A) : Symmetric R -> Symmetric (R#).
Quasi-ordering closure.
Section qo_clos.
Variables (A : Type) (E : rel A) (E_eq : Equivalence E).
Inductive qo_clos (R : rel A) : rel A :=
| qo_step : R << qo_clos R
| qo_refl : E << qo_clos R
| qo_trans : Transitive (qo_clos R).
Variable R : rel A.
Global Instance qo_clos_preorder : PreOrder (qo_clos R).
Variable R_prop : Proper (E ==> E ==> impl) R.
Global Instance qo_clos_prop : Proper (E ==> E ==> impl) (qo_clos R).
Global Instance qo_clos_prop_iff : Proper (E ==> E ==> iff) (qo_clos R).
Lemma qo_clos_inv : forall t u,
qo_clos R t u -> E t u \/ exists v, R t v /\ qo_clos R v u.
End qo_clos.
Properties of transp.
Instance transp_incl A : Proper (incl ==> incl) (@transp A).
Instance transp_same A : Proper (same ==> same) (@transp A).
Lemma transp_refl A (R : rel A) : Reflexive R -> Reflexive (transp R).
Lemma transp_trans A (R : rel A) : Transitive R -> Transitive (transp R).
Lemma transp_sym A (R : rel A) : Symmetric R -> Symmetric (transp R).
Lemma transp_invol A (R : rel A) : transp (transp R) == R.
Lemma transp_union A (R S : rel A) : transp (R U S) == transp R U transp S.
Relations between closures, union and composition.
Lemma rtc_comp_permut A (R S : rel A) : R# @ (R# @ S)# << (R# @ S)# @ R#.
Lemma rtc_union A (R S : rel A) : (R U S)# << (R# @ S)# @ R#.
Lemma rtc_comp A (R S : rel A) : R# @ S << S U R! @ S.
Lemma union_fact A (R S : rel A) : R U R @ S << R @ S%.
Lemma union_fact2 A (R S : rel A) : R @ S U R << R @ S%.
Lemma incl_rc_rtc A (R S : rel A) : R << S! -> R% << S#.
Lemma incl_tc_rtc A (R S : rel A) : R << S# -> R! << S#.
Lemma rtc_comp_modulo A (R S : rel A) : R# @ (R# @ S)! << (R# @ S)!.
Lemma tc_union A (R S : rel A) : (R U S)! << R! U (R# @ S)! @ R#.
Commutation properties.
Section commut.
Variables (A : Type) (R S : rel A) (commut : R @ S << S @ R).
Lemma commut_rtc : R# @ S << S @ R#.
Lemma commut_rtc_inv : R @ S# << S# @ R.
Lemma commut_tc : R! @ S << S @ R!.
Lemma commut_tc_inv : R @ S! << S! @ R.
Lemma commut_comp T : R @ (S @ T) << (S @ R) @ T.
Lemma comp_incl_assoc T V : R @ S << T -> R @ (S @ V) << T @ V.
End commut.
Inverse image.
Section inverse_image.
Variables (A B : Type) (R : rel B) (f : A->B).
Definition Rof : rel A := fun a a' => R (f a) (f a').
Lemma Rof_refl : Reflexive R -> Reflexive Rof.
Lemma Rof_trans : Transitive R -> Transitive Rof.
Lemma Rof_sym : Symmetric R -> Symmetric Rof.
Lemma Rof_preorder : PreOrder R -> PreOrder Rof.
Lemma Rof_equiv : Equivalence R -> Equivalence Rof.
Variable F : A -> B -> Prop.
Definition RoF : rel A :=
fun a a' => exists b', F a' b' /\ forall b, F a b -> R b b'.
End inverse_image.
Instance Rof_incl A B : Proper (incl ==> Logic.eq ==> incl) (@Rof A B).
Alternative definition of the transitive closure, more convenient
for some inductive proofs.
Inductive clos_trans1 A (R : rel A) : rel A :=
| t1_step : forall x y, R x y -> clos_trans1 R x y
| t1_trans : forall x y z, R x y -> clos_trans1 R y z -> clos_trans1 R x z.
Notation "x !1" := (clos_trans1 x) (at level 35) : relation_scope.
Instance tc1_trans A (R : rel A) : Transitive (R!1).
Lemma tc1_eq A (R : rel A) x y : R!1 x y <-> R! x y.
Alternative definition of the reflexive and transitive closure,
more convenient for some inductive proofs.
Inductive clos_refl_trans1 A (R : rel A) : rel A :=
| rt1_refl : forall x, clos_refl_trans1 R x x
| rt1_trans : forall x y z,
R x y -> clos_refl_trans1 R y z -> clos_refl_trans1 R x z.
Notation "x #1" := (clos_refl_trans1 x) (at level 9) : relation_scope.
Instance rtc1_preorder A (R : rel A) : PreOrder (R#1).
Lemma rtc1_eq A (R : rel A) x y : R#1 x y <-> R# x y.
Lemma tc1_incl_rtc1 A (R : rel A) : R!1 << R#1.
Lemma rtc1_union A (R S : rel A) : (R U S)#1 << (S#1 @ R)#1 @ S#1.
Lemma union_rel_rt1_left A (R S : rel A) : R#1 << (R U S)#1.
Lemma union_rel_rt1_right A (R S : rel A) : S#1 << (R U S)#1.
Lemma incl_rt1_union_union A (R S : rel A) : (R!1 U S!1)#1 << (R U S)#1.
Lemma incl_union_rt1_union A (R S : rel A) : (R U S)#1 << (R!1 U S!1)#1.
Lemma comm_s_rt1 A (R S : rel A) :
S@(R!1) << (R!1)@(S!1) -> (S!1)@(R!1) << (R!1)@(S!1).
Lemma comm_s_r A (R S : rel A) :
S@R << (R!1)@(S#1) -> (R U S)#1 @ R @ (R U S)#1 << (R!1) @ (R U S)#1.
Extension to option A of a relation on A so that it is
reflexive on None.
Section opt_r.
Variables (A : Type) (R : rel A).
Inductive opt_r : rel (option A) :=
| opt_r_None : opt_r None None
| opt_r_Some : forall a b, R a b -> opt_r (Some a) (Some b).
Global Instance opt_r_refl : Reflexive R -> Reflexive opt_r.
Global Instance opt_r_sym : Symmetric R -> Symmetric opt_r.
Global Instance opt_r_trans : Transitive R -> Transitive opt_r.
Global Instance Some_prop : Proper (R ==> opt_r) (@Some A).
End opt_r.
Extension of a relation on A to option A so that it is
irreflexive on None.
Section opt.
Variables (A : Type) (R : rel A).
Inductive opt : rel (option A) :=
| opt_intro : forall x y, R x y -> opt (Some x) (Some y).
Global Instance opt_trans : Transitive R -> Transitive opt.
Global Instance opt_sym : Symmetric R -> Symmetric opt.
Global Instance opt_opt_r E : Proper (E ==> E ==> impl) R ->
Proper (opt_r E ==> opt_r E ==> impl) opt.
Lemma opt_absorbs_right_opt_r E : R @ E << R -> opt @ opt_r E << opt.
Lemma opt_absorbs_left_opt_r E : E @ R << R -> opt_r E @ opt << opt.
End opt.
Instance opt_incl A : Proper (incl ==> incl) (@opt A).
Instance opt_prop A (E1 E2 R : rel A) :
Proper (E1 ==> E2 ==> impl) R -> Proper (opt E1 ==> opt E2 ==> impl) (opt R).
Lemma opt_absorbs_right A (R E : rel A) :
R @ E << R -> opt R @ opt E << opt R.
Lemma opt_absorbs_left A (R E : rel A) :
E @ R << R -> opt E @ opt R << opt R.
Restriction of a relation to some set.
Section restrict.
Variables (A : Type) (P : A -> Prop) (R : rel A).
Definition restrict : rel A := fun x y => P x /\ R x y.
Global Instance restrict_prop E :
Proper (E ==> impl) P -> Proper (E ==> E ==> impl) R ->
Proper (E ==> E ==> impl) restrict.
End restrict.
Lemma restrict_union A (P : A -> Prop) R S :
restrict P (R U S) == restrict P R U restrict P S.