Library CoLoR.Util.Relation.AccUtil

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2005-02-17
  • Solange Coupet-Grimal and William Delobel, 2006-01-09
useful results on accessibility

Set Implicit Arguments.

Compatibility of accessibility wrt relation inclusion/equivalence.

Instance Acc_incl A : Proper (incl --> eq ==> impl) (@Acc A).

Instance Acc_same A : Proper (same ==> eq ==> iff) (@Acc A).

Lemma Acc_eq_rel : forall A (R S : relation A) x,
  (forall a b, R a b <-> S a b) -> Acc R x -> Acc S x.

Instance well_founded_incl A :
  Proper (incl --> impl) (@well_founded A).

Instance well_founded_same A : Proper (same ==> iff) (@well_founded A).

Transitive closure.

Section rtc.

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

  Lemma Acc_rtc : forall x y, clos_refl_trans R x y -> Acc R y -> Acc R x.

  Lemma Acc_tc_ind : forall P : A->Prop,
    (forall x, (forall y, clos_trans R y x -> P y) -> P x)
    -> forall x, Acc R x -> P x.

End rtc.

Symmetric product.

Section symprod.

  Variables (A B : Type) (leA : relation A) (leB : relation B).

  Notation Symprod := (symprod leA leB).

  Lemma Acc_symprod_fst x : Acc Symprod x -> Acc leA (fst x).

  Lemma Acc_symprod_snd x : Acc Symprod x -> Acc leB (snd x).

  Lemma Acc_symprod_invl x y : Acc Symprod (x,y) -> Acc leA x.

  Lemma Acc_symprod_invr x y : Acc Symprod (x,y) -> Acc leB y.

  Lemma Acc_symprod_inv x y : Acc Symprod (x,y) -> Acc leA x /\ Acc leB y.

End symprod.

Restricted accessibility.

Section RestrictedAcc.

  Variables (A : Type) (P : A -> Prop).

  Inductive Restricted_acc (R : relation A) : A -> Prop :=
  | Restricted_acc_cons : forall a,
    (forall a', P a' -> R a' a -> Restricted_acc R a') -> Restricted_acc R a.

  Lemma Restricted_acc_eq_acc : forall R a,
    Acc (fun a a' => P a /\ R a a') a <-> Restricted_acc R a.

End RestrictedAcc.

List of accessible arguments.

Definition Accs (A : Type) R l := forall a : A, In a l -> Acc R a.

Simulation and morphisms.

Section Accessibility.

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

  Definition mimic (P : relation A) := forall x x', P x x' ->
    forall y', R y' x' -> exists2 y, R y x & P y y'.

  Lemma Acc_mimic : forall x (P: relation A),
    Acc R x -> mimic P -> forall x', P x x' -> Acc R x'.

  Variables x y : A.

  Section AccHomo.

    Variable T : relation B.
    Variable z : B.
    Variable morphism : A -> B -> Prop.
    Variable comp : forall x y x',
      morphism x' x -> T y x -> exists2 y': A, R y' x' & morphism y' y.

    Lemma Acc_homo :
      forall x, Acc R x -> forall x', morphism x x' -> Acc T x'.

  End AccHomo.

  Section AccIso.

    Variable T : relation B.
    Variable z : B.
    Variable iso : A -> B -> Prop.
    Variable iso_comp : forall x y' x',
      iso x x' -> T y' x' -> {y: A | R y x & iso y y'}.

    Lemma Acc_iso : iso x z -> Acc R x -> Acc T z.

  End AccIso.

End Accessibility.

Wellfounded fixpoints: we extend Fix_F_inv to any relation eq.

Section Fix.

  Variables (A : Type) (R : relation A) (Rwf : well_founded R)
    (P : A -> Type) (F : forall x : A, (forall y : A, R y x -> P y) -> P x)
    (eq : forall x, relation (P x))
    (F_ext : forall x (f g : forall y, R y x -> P y),
      (forall y (p : R y x), eq (f y p) (g y p)) -> eq (F f) (F g)).

  Notation Fix_F := (Fix_F F).
  Notation Fix_F_eq := (Fix_F_eq F).
  Notation Fix := (Fix Rwf F).
  Infix "==" := eq (at level 70).

  Lemma Fix_F_inv : forall x (r s : Acc R x), Fix_F r == Fix_F s.

  Lemma Fix_eq : forall x, Fix x == F (fun y (p : R y x) => Fix y).

End Fix.

A well-founded relation is irreflexive.

Lemma wf_irrefl : forall A (R : relation A), well_founded R -> Irreflexive R.