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.