Library CoLoR.Util.Relation.RelUtil

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2005-02-17
  • Adam Koprowski and Hans Zantema, 2007-03
  • Joerg Endrullis and Dimitri Hendriks, 2008-07
General definitions and results about relations.

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.

Definition empty_rel {A} : rel A := fun x y => False.

Relation associated to a boolean function.

Definition rel_of_bool A (f : A->A->bool) : rel A :=
  fun x y => f x y = true.

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.

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.

Strict part.

Definition strict_part A (R : rel A) : rel A := fun x y => R x y /\ ~R y x.

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.