Library CoLoR.HORPO.HorpoWf

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Adam Koprowski, 2006-04-27
This file is the development of the proof of well-foundedness of the higher-order recursive path ordering due to Jouannaud and Rubio.

Set Implicit Arguments.

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

  Module Export HC := HorpoComp.HorpoComp S Prec.

  Lemma acc_mul_acc_wfmul_aux : forall (M: Multiset),
    Acc horpo_mul_lt M ->
    forall (WM: WFterms), M = WM -> Acc H_WFterms_lt WM.

  Lemma acc_mul_acc_wfterms : forall (WM: WFterms),
    Acc horpo_mul_lt WM -> Acc H_WFterms_lt WM.

  Lemma wf_MulLt_WFterms : well_founded H_WFterms_lt.

  Module H_WFmul_ord <: Ord.

    Module SetWF <: SetA.
      Definition A := WFterms.
    End SetWF.
    Module S := Eqset_def SetWF.
    Definition A := WFterms.
    Definition gtA := transp H_WFterms_lt.
    Definition gtA_eqA_compat := Eqset_def_gtA_eqA_compat gtA.

  End H_WFmul_ord.

  Module Lex := PairLex.LexicographicOrder Prec.P.O H_WFmul_ord.
  Import Lex.

  Lemma compTerms : forall M N Ns, M [>>] Ns -> CompTerms (appArgs M) ->
    (forall n, In n Ns -> subterm n N) ->
    (forall N', subterm N' N -> M >> N' -> CompH N') ->
    CompTerms Ns.

  Lemma arg_mul_arg : forall m M, m in (list2multiset (appArgs M)) -> isArg m M.

  Lemma argsComp_appComp_aux :
    forall Px: pair,
      (forall Py: pair, Py <lex Px ->
        forall M, algebraic M -> term (appHead M) = ^fst Py ->
          appArgs M = proj1_sig (snd Py) -> CompH M) ->
    forall M N,
      algebraic M -> term (appHead M) = ^fst Px -> appArgs M = proj1_sig (snd Px) ->
      (forall N', subterm N' N -> M >> N' -> CompH N') ->
      M >> N -> CompH N.

  Lemma argsComp_appComp_ind : forall (P: pair) M,
    algebraic M -> term (appHead M) = Fun (fst P) ->
    appArgs M = proj1_sig (snd P) -> CompH M.

  Lemma argsComp_appComp : forall M, algebraic M -> isFunS (appHead M) ->
    (forall P, isArg P M -> CompH P) -> CompH M.

  Lemma subst_comp : forall M G (MG: correct_subst M G),
    algebraic M -> CompSubst G -> algebraicSubstitution G ->
    CompH (subst MG).

  Lemma horpo_beta_wf : forall M, algebraic M -> SN.SN horpo M.

End HorpoWf.