# 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.