Library CoLoR.Util.Relation.Union

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Joerg Endrullis, 2008-07-28
  • Frederic Blanqui, 2007-02-05
when the union of two wellfounded relations is wellfounded

Set Implicit Arguments.


Section S.

  Variables (A : Type) (R S : relation A).

When the two relations commute.

  Lemma SN_union_commut t :
    (forall x, SN S x -> SN R x) -> SN S t -> R @ S << S @ R -> SN (R U S) t.

  Lemma WF_union_commut : WF R -> WF S -> R @ S << S @ R -> WF (R U S).

When a relation absorbs the other.

  Lemma wf_union_absorb : WF R -> WF S -> R @ S << R -> WF (R U S).

Commutation and SN

  Lemma sn_comm_sntr :
    forall x, SN R x -> (forall y, R#1 x y -> SN S y) ->
      S@R << R!1@S#1 -> SN (R!1 U S!1) x.

  Lemma sn_comm_sn :
    forall x, SN R x -> (forall y, R#1 x y -> SN S y) ->
      S@R << R!1@S#1 -> SN (R U S) x.

End S.