# Library CoLoR.Util.Relation.SN

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Frederic Blanqui, 2006-11-26
• Adam Koprowski & Hans Zantema, 2007-03
• Joerg Endrullis, 2008-07
Inductive definition of strong normalization (inverse of accessibility)

Set Implicit Arguments.

## Definition of strong normalization.

It is defined as accessibility but by orienting the relation the opposite way.

Section sn.

Variable (A : Type) (R : rel A).

Inductive SN x : Prop := SN_intro : (forall y, R x y -> SN y) -> SN x.

Definition WF := forall x, SN x.

End sn.

Instance SN_inv A (R : rel A) : Proper (R ==> impl) (SN R).

Instance SN_prop A (R E : relation A) : Equivalence E ->
Proper (E ==> E ==> impl) R -> Proper (E ==> impl) (SN R).

## If x is strongly normalizing wrt R, then there is no infinite

R-sequence starting from x. Proof obtained after the correction of Exercise 15.7 page 413 of the book Coq'Art by Yves Bertot and Pierre Casteran, http://www.labri.fr/perso/casteran/CoqArt/gen-rec/SRC/not_decreasing.v.

Section notIS.

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

Lemma SN_notNT : forall x, SN R x -> ~NT R x.

Lemma NT_notSN : forall x, NT R x -> ~SN R x.

Lemma WF_notIS : WF R -> forall f, ~IS R f.

Lemma WF_notEIS : WF R -> ~EIS R.

End notIS.

## Relation between SN and Acc.

Section acc.

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

Lemma SN_transp_Acc : forall x, SN (transp R) x -> Acc R x.

Lemma Acc_transp_SN : forall x, Acc (transp R) x -> SN R x.

Lemma WF_transp_wf : WF (transp R) -> well_founded R.

Lemma wf_transp_WF : well_founded (transp R) -> WF R.

End acc.

Section acc_transp.

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

Lemma SN_Acc_transp : forall x, SN R x -> Acc (transp R) x.

Lemma Acc_SN_transp : forall x, Acc R x -> SN (transp R) x.

Lemma WF_wf_transp : WF R -> well_founded (transp R).

Lemma wf_WF_transp : well_founded R -> WF (transp R).

End acc_transp.

## SN properties of inclusion.

Lemma WF_empty_rel A : WF (@empty_rel A).

Instance SN_inclusion A : Proper (inclusion --> eq ==> impl) (@SN A).

Lemma SN_incl A (S R : rel A) : R << S -> forall x, SN S x -> SN R x.

Instance SN_same A : Proper (same ==> eq ==> iff) (@SN A).

Lemma SN_same_ext A (R S : rel A) : R == S -> forall x, SN R x <-> SN S x.

Instance WF_incl A : Proper (incl --> impl) (@WF A).

Instance WF_same A : Proper (same ==> iff) (@WF A).

## SN properties of Rof.

Section inverse.

Variables (A B : Type) (f : A->B) (R : relation B).

Notation Rof := (Rof R f).

Lemma SN_Rof : forall b, SN R b -> forall a, b = f a -> SN Rof a.

Lemma SN_inverse : forall a, SN R (f a) -> SN Rof a.

Lemma WF_inverse : WF R -> WF Rof.

End inverse.

## SN properties of RoF.

Section rel_inverse.

Variables (A B : Type) (R : relation B) (F : A->B->Prop).

Notation RoF := (RoF R F).

Lemma SN_RoF : forall b, SN R b -> forall a, F a b -> SN RoF a.

Lemma SN_Inverse : forall a, (exists b, F a b /\ SN R b) -> SN RoF a.

Lemma WF_Inverse : WF R -> WF RoF.

End rel_inverse.

## SN properties of clos_refl_trans.

Instance SN_inv_rtc A (R : rel A) : Proper (R# ==> impl) (SN R).

Instance SN_inv_rtc1 A (R : rel A) : Proper (R#1 ==> impl) (SN R).

## SN properties of clos_trans.

Section tc.

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

Lemma SN_tc : forall x, SN R x -> SN (R!) x.

Lemma WF_tc : WF R -> WF (R!).

Lemma SN_tc1 : forall x, SN R x -> SN (R!1) x.

End tc.

## SN properties of symprod (component-wise binary product).

Section symprod.

Variable (A B : Type) (gtA : relation A) (gtB : relation B).

Notation gt := (symprod gtA gtB).

Lemma SN_symprod : forall x, SN gtA x -> forall y, SN gtB y -> SN gt (x,y).

Lemma WF_symprod : WF gtA -> WF gtB -> WF gt.

Lemma SN_symprod_fst : forall x, SN gt x -> SN gtA (fst x).

Lemma SN_symprod_snd : forall x, SN gt x -> SN gtB (snd x).

Lemma SN_symprod_invl : forall x y, SN gt (x,y) -> SN gtA x.

Lemma SN_symprod_invr : forall x y, SN gt (x,y) -> SN gtB y.

Lemma SN_symprod_inv : forall x y, SN gt (x,y) -> SN gtA x /\ SN gtB y.

End symprod.

## SN properties of compose.

Section compose.

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

Lemma WF_compose_swap : WF (R @ S) -> WF (S @ R).

End compose.

## SN properties of absorbing relations.

Section compat.

Variable (A : Type) (E R : relation A) (Hcomp : E @ R << R).

Lemma SN_compat_inv : forall x,
SN (R @ E) x -> forall x', E x x' -> SN (R @ E) x'.

Lemma WF_compat_inv : WF R -> WF (R @ E).

End compat.

Section absorb.

Variables (A : Type) (R T : relation A) (absorb : R @ T << T).

Lemma SN_modulo_r : forall x x', SN (T @ R#) x -> R# x x' -> SN (T @ R#) x'.

Lemma absorb_SN_modulo_r : forall x, SN T x -> SN (T @ R#) x.

Lemma absorb_WF_modulo_r : WF T -> WF (T @ R#).

End absorb.

Section WF_mod_rev.

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

Lemma WF_mod_rev : WF (E# @ S) -> WF (S @ E#).

End WF_mod_rev.

## Properties of termination modulo.

Section modulo.

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

Lemma SN_modulo : forall x x', SN (E# @ R) x -> E# x x' -> SN (E# @ R) x'.

Lemma WF_union_mod : WF E -> WF (E# @ R) -> WF (R U E).

End modulo.

## SN properties of commuting relations.

Section commut.

Variables (A : Type) (R S : relation A) (commut : S @ R << R @ S).

Lemma SN_commut : forall x, SN R x -> forall x', S x x' -> SN R x'.

End commut.

Section commut_modulo.

Variables (A : Type) (R S : relation A) (commut : R @ S << S @ R).

Lemma SN_commut_modulo : forall x, SN S x -> SN (R# @ S) x.

Lemma WF_commut_modulo : WF S -> WF (R# @ S).

End commut_modulo.

## SN properties of Iter.

Section iter.

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

Lemma SN_iter_S : forall n x, SN (iter R n) x -> SN (iter R (S n)) x.

Lemma SN_iter_S' : forall n x, SN (iter R (S n)) x -> SN (iter R n) x.

Lemma SN_iter : forall n x, SN (iter R n) x -> SN R x.

Lemma WF_iter : forall n, WF (iter R n) -> WF R.

End iter.

## Extension of SN_intro to paths of fixed length.

Section path.

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

Lemma SN_path : forall n x,
(forall y l, length l = n -> path R x y l -> SN R y) -> SN R x.

End path.

## Modularity properties of relative termination.

Section wf_mod_shift.

Variable (A : Type) (R S T : relation A).

Lemma wf_mod_shift : WF (T# @ (R U S)) -> WF ((S U T)# @ R).

End wf_mod_shift.

Section wf_rel_mod.

Variable (A : Type) (R S R' S': relation A).

Lemma wf_rel_mod :
WF (S# @ R) -> WF ((R U S)# @ (R' U S')) -> WF ((S' U S)# @ (R' U R)).

End wf_rel_mod.

Section wf_rel_mod_simpl.

Variable (A : Type) (R R' S : relation A).

Lemma wf_rel_mod_simpl :
WF (S# @ R) -> WF ((R U S)# @ R') -> WF (S# @ (R' U R)).

End wf_rel_mod_simpl.

## Termination of the standard ordering on natural numbers.

Section ltof.

Variables (A : Type) (f : A -> nat).

Global Instance ltof_trans : Transitive (ltof f).

Lemma transp_ltof_wf : WF (transp (ltof f)).

End ltof.

Lemma WF_gt : WF gt.

## restrictPR terminates if P<=SNR.

Section restrict.

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

Lemma wf_restrict_sn : P [<=] SN R -> WF (restrict P R).

Lemma sn_restrict : Proper (R ==> impl) P ->
forall x, SN (restrict P R) x -> P x -> SN R x.

End restrict.

## opt preserves wellfoundedness.

Lemma wf_opt A (R : relation A) : WF R -> WF (opt R).