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.

Require Import RelExtras.
Require Import ListExtras.
Require Import Computability.
Require Import Horpo.
Require Import Setoid.

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

  Module Comp := Computability.Computability S Prec.
  Export Comp.
  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) := Q, In (Some Q) GCompH Q.

  Definition WFterms := { Ts: Terms | CompTerms Ts }.
  Definition WFterms_to_mul (Ts: WFterms) : Multiset := 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 MAccR horpo M.

    intros M Mcomp.
    apply comp_imp_acc; eauto with horpo.

  Lemma horpo_comp_step_comp : M N, CompH MM >> NCompH N.

    intros M N Mcomp MN.
    unfold CompH; apply comp_step_comp with M; eauto with horpo.

  Lemma horpo_comp_manysteps_comp : M N, CompH MM >>* NCompH N.

    intros M N Mcomp M_N.
    unfold CompH; apply comp_manysteps_comp with M; eauto with horpo.

  Lemma horpo_comp_pflat : N Ns, isPartialFlattening Ns Nalgebraic N
    AllComputable horpo NsCompH N.

    intros N Ns NsN Nnorm NsC; unfold CompH.
    apply comp_pflat with Ns; trivial.

  Lemma horpo_neutral_comp_step : M, algebraic MisNeutral M
    (CompH M ( N, M >> NCompH N)).

    intros M Mneutral; unfold CompH.
    apply neutral_comp_step; eauto with horpo.

  Lemma CompH_morph_aux : x1 x2 : Term, x1 ¬ x2CompH x1CompH x2.

    intros t t' teqt' H_t.
    unfold CompH.
    apply Computable_morph_aux with t; eauto with horpo.

  Add Morphism CompH
    with signature terms_conv ==> iff
      as CompH_morph.

    intros; split; apply CompH_morph_aux; auto using terms_conv_sym.

  Lemma horpo_comp_conv: M M', CompH MM ¬ M'CompH M'.

    rewrite <- H0; trivial.

  Lemma horpo_var_comp : M, isVar MCompH M.

    intros M Mvar; unfold CompH.
    apply var_comp; eauto with horpo.

  Lemma horpo_comp_abs : M (Mabs: isAbs M), algebraic M
    ( G (cs: correct_subst (absBody Mabs) G) T,
      isSingletonSubst T GCompH T
      CompH (subst cs)) → CompH M.

    intros M Mnorm Mabs H; unfold CompH.
    eapply comp_abs; eauto with horpo.

  Lemma horpo_comp_lift : N, CompH NCompH (lift N 1).

    setoid_replace (lift N 1) with N using relation terms_conv; trivial.
    apply terms_conv_sym; apply terms_lift_conv.

  Lemma horpo_comp_app : M (Mapp: isApp M),
    CompH (appBodyL Mapp) → CompH (appBodyR Mapp) →
    CompH M.

    intros M Mapp Ml Mr; unfold CompH.
    apply comp_app with Mapp; trivial.

  Lemma horpo_comp_algebraic : M, CompH Malgebraic M.

    apply comp_algebraic with horpo; trivial.

  Lemma horpo_comp_units_comp : M, ( N, isAppUnit N MCompH N) →
    CompH M.

    intros M Munits; unfold CompH.
    apply comp_units_comp; trivial.

End HorpoComp.