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,

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.

restrict P R terminates if P <= SN R.

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