# Library CoLoR.Term.WithArity.AInfSeq

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Frederic Blanqui, 2011-05-06
Properties of infinite sequences of terms. Uses classical logic, the axiom of indefinite description, and the axiom WF_notIS for WF_absorb.

Set Implicit Arguments.

Section S.

Variable Sig : Signature.

Notation term := (term Sig).
Notation subterm_eq := (@subterm_eq Sig).
Notation supterm_eq := (@supterm_eq Sig).

general boolean conditions for which WF (hd_red_mod R D) is equivalent to WF (hd_red_Mod (int_red R #) D)

Section WF_hd_red_mod_of_WF_hd_red_Mod_int.

Variables R D : rules Sig.

Lemma undef_red_is_int_red :
forall (hyp1 : forallb (@is_notvar_lhs Sig) R = true),
forall t u, red R t u ->
undefined R t = true -> int_red R t u /\ undefined R u = true.

Lemma undef_rtc_red_is_rtc_int_red
(hyp1 : forallb (@is_notvar_lhs Sig) R = true) :
forall t u, red R # t u ->
undefined R t = true -> int_red R # t u /\ undefined R u = true.

Lemma WF_hd_red_Mod_int :
forall (hyp1 : forallb (@is_notvar_lhs Sig) R = true)
(hyp2 : forallb (undefined_rhs R) D = true),
WF (hd_red_Mod (int_red R #) D) -> WF (hd_red_mod R D).

End WF_hd_red_mod_of_WF_hd_red_Mod_int.

subtype of minimal non-terminating terms

Section NTM.

Variable R : relation term.

Record NTM : Type := mkNTM {
NTM_val :> term;
NTM_prop :> NT_min R NTM_val }.

End NTM.

get a minimal non-terminating subterm

Section NT_min.

Variables (R : relation term) (t : term) (ht : NT R t).

Lemma NT_min_intro : exists u, subterm_eq u t /\ NT_min R u.

Definition min_term :=
proj1_sig (constructive_indefinite_description _ NT_min_intro).

Lemma NT_min_term : NT_min R min_term.

Lemma subterm_eq_min_term : subterm_eq min_term t.

Definition min_NTM := mkNTM NT_min_term.

End NT_min.

get a minimal infinite (R @ supterm_eq)-sequence from an infinite R-sequence

Section IS_Min_supterm.

Variable R : relation term.

Definition Rsup : relation (NTM R) := R @ supterm_eq.

Lemma Rsup_left_total : forall t, exists u, Rsup t u.

Lemma IS_Min_supterm : forall f,
IS R f -> exists g, IS (R @ supterm_eq) g /\ Min R g.

End IS_Min_supterm.

get an infinite (red R)-sub-sequence from an infinite (int_red R)-sequence

Lemma NT_int_red_subterm_NT_red : forall (R : rules Sig) f,
IS (int_red R) f -> exists u, subterm u (f 0) /\ NT (red R) u.

get a minimal infinite (hd_red_mod R (dp R))-sequence from a minimal infinite R-sequence

Section IS_Min_dp.

Variable R : rules Sig.

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

Lemma min_hd_red_dp : forall t u v, NT_min (red R) t -> hd_red R t u ->
subterm_eq v u -> NT_min (red R) v -> hd_red (dp R) t v.

Definition Rdp : relation (NTM (red R)) := hd_red_Mod (int_red R #) (dp R).

Lemma Rdp_left_total : forall t, exists u, Rdp t u.

Lemma IS_Min_dp : forall f, IS (red R) f ->
exists g, IS (hd_red_Mod (int_red R #) (dp R)) g /\ Min (red R) g.

End IS_Min_dp.

End S.