Library CoLoR.Term.WithArity.ASN

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Sebastien Hinderer, 2004-02-09
  • Frederic Blanqui, 2005-02-17
general results on the strong normalization of rewrite relations

Set Implicit Arguments.


Section S.

  Variable Sig : Signature.

  Notation term := (term Sig). Notation terms := (vector term).
  Notation rule := (rule Sig). Notation rules := (list rule).

  Variable R : rules.

  Notation Red := (@red Sig R). Notation SNR := (SN Red).

every subterm of an sn term is sn

  Lemma subterm_eq_sn : forall t, SNR t -> forall u, subterm_eq u t -> SNR u.

  Lemma sub_sn : forall l x s, In x (vars l) -> SNR (sub s l) -> SNR (s x).

  Lemma sub_fun_sn : forall f ts x s,
    In x (vars (Fun f ts)) -> Vforall SNR (Vmap (sub s) ts) -> SNR (s x).

strongly normalizing terms when no lhs is a variable

  Variable hyp1 : forallb (@is_notvar_lhs Sig) R = true.

variables are sn

  Lemma sn_var : forall v, SNR (Var v).

undefined symbol whose arguments are sn


  Lemma sn_args_sn_fun : forall f, defined f R = false ->
    forall ts, Vforall SNR ts -> SNR (Fun f ts).

application of an sn substitution to a term without defined symbols

  Lemma no_call_sub_sn : forall t, calls R t = nil -> forall s,
    (forall x, In x (vars t) -> SNR (s x)) -> SNR (sub s t).

given a substitution s that is sn on vars r, if sub s (Fun g vs) is SN whenever Fun g vs is a call in r such that Vmap (sub s) vs are SN, then sub s (Fun g vs) is SN whenever Fun g vs is a call in r


  Lemma calls_sn_args : forall r s, (forall x, In x (vars r) -> SNR (s x))
    -> (forall g vs, In (Fun g vs) (calls R r)
      -> Vforall SNR (Vmap (sub s) vs) -> SNR (sub s (Fun g vs)))
    -> forall g vs, In (Fun g vs) (calls R r) -> Vforall SNR (Vmap (sub s) vs).

  Lemma calls_sn : forall r s, (forall x, In x (vars r) -> SNR (s x))
    -> (forall g vs, In (Fun g vs) (calls R r)
      -> Vforall SNR (Vmap (sub s) vs) -> SNR (sub s (Fun g vs)))
    -> forall a, In a (calls R r) -> SNR (sub s a).

relation with the subterm ordering


  Notation supterm := (@supterm Sig).

  Lemma WF_supterm : WF supterm.

  Lemma supterm_red : supterm @ red R << red R @ supterm.

  Lemma SN_red_supterm : forall x, SN (red R) x -> SN (red R U supterm) x.

  Lemma WF_red_supterm : WF (red R) -> WF (red R U supterm).

End S.