Library CoLoR.HORPO.HorpoComp

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Adam Koprowski, 2006-04-27
Some computability results instantiated for horpo.

Set Implicit Arguments.


Module HorpoComp (S : TermsSig.Signature)
  (Prec : Horpo.Precedence with Module S := S).

  Module Export Comp := Computability.Computability S Prec.

  Import List.

  Definition horpo_lt := transp horpo.
  Definition horpo_mul_lt := MultisetLT horpo.

  Notation "X << Y" := (horpo_lt X Y) (at level 55).
  Definition Htrans := clos_trans horpo.

  Definition Terms := list Term.
  Definition CompH := Computable horpo.
  Definition CompTerms (Ts: Terms) := AllComputable horpo Ts.
  Definition CompSubst (G: Subst) := forall Q, In (Some Q) G -> CompH Q.

  Definition WFterms := { Ts: Terms | CompTerms Ts }.
  Definition WFterms_to_mul (Ts: WFterms) := list2multiset (proj1_sig Ts).
  Coercion WFterms_to_mul: WFterms >-> Multiset.
  Definition H_WFterms_lt (M N: WFterms) := horpo_mul_lt M N.

  Hint Unfold horpo_lt horpo_mul_lt CompH CompTerms : horpo.

  Lemma horpo_comp_imp_acc M : CompH M -> AccR horpo M.

  Lemma horpo_comp_step_comp M N : CompH M -> M >> N -> CompH N.

  Lemma horpo_comp_manysteps_comp M N : CompH M -> M >>* N -> CompH N.

  Lemma horpo_comp_pflat N Ns : isPartialFlattening Ns N -> algebraic N ->
    AllComputable horpo Ns -> CompH N.

  Lemma horpo_neutral_comp_step : forall M, algebraic M -> isNeutral M ->
    (CompH M <-> (forall N, M >> N -> CompH N)).

  Lemma CompH_morph_aux : forall x1 x2 : Term, x1 ~ x2 -> CompH x1 -> CompH x2.

  Instance CompH_morph : Proper (terms_conv ==> iff) CompH.


  Lemma horpo_comp_conv: forall M M', CompH M -> M ~ M' -> CompH M'.

  Lemma horpo_var_comp : forall M, isVar M -> CompH M.

  Lemma horpo_comp_abs : forall M (Mabs: isAbs M), algebraic M ->
    (forall G (cs: correct_subst (absBody Mabs) G) T,
      isSingletonSubst T G -> CompH T ->
      CompH (subst cs)) -> CompH M.

  Lemma horpo_comp_lift : forall N, CompH N -> CompH (lift N 1).

  Lemma horpo_comp_app : forall M (Mapp: isApp M),
    CompH (appBodyL Mapp) -> CompH (appBodyR Mapp) -> CompH M.

  Lemma horpo_comp_algebraic : forall M, CompH M -> algebraic M.

  Lemma horpo_comp_units_comp M :
    (forall N, isAppUnit N M -> CompH N) -> CompH M.

End HorpoComp.