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.

Instance irreflexive_incl A : Proper (incl --> impl) (@irreflexive A).

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.