Library CoLoR.HORPO.Horpo

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

Set Implicit Arguments.


Module Type Precedence.

  Declare Module S : TermsSig.Signature.
  Declare Module Export P : Poset with Definition A := S.FunctionSymbol.

  Parameter Ord_wf : well_founded (transp gtA).
  Parameter Ord_dec : forall a b, {gtA a b} + {~gtA a b}.

End Precedence.

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

  Module Export T := Terms.Terms S.

  Module MSetCore := MultisetList.MultisetList TermsEqset_dec.
  Module Export MSet := MultisetTheory.Multiset MSetCore.

  Module Export MSetOrd := MultisetOrder.MultisetOrder MSetCore.

  Module Import Lex := PairLex.LexicographicOrder Subterm_Ord Subterm_Ord.

  Definition TermMul := Multiset.
  Implicit Type TM : TermMul.

  Definition TermList := list Term.
  Implicit Type TL : TermList.

  Notation "f >#> g" := (Prec.P.O.gtA f g) (at level 30).
  Reserved Notation "M >-> N" (at level 30).
  Reserved Notation "M >> N" (at level 30).
  Reserved Notation "M >>= N" (at level 30).
  Reserved Notation "M {>>} N" (at level 30).
  Reserved Notation "M [>>] N" (at level 30).

  Inductive horpoArgs : Term -> TermList -> Prop :=

  | HArgsNil: forall M, M [>>] nil

  | HArgsConsEqT: forall M N TL, M >> N -> M [>>] TL -> M [>>] (N :: TL)

  | HArgsConsNotEqT: forall M N TL,
    (exists2 M', isArg M' M & M' >>= N) -> M [>>] TL -> M [>>] (N :: TL)
    where "M [>>] N" := (horpoArgs M N)

  with prehorpo : relation Term :=

  | HSub: forall M N,
    isFunApp M -> (exists2 M', isArg M' M & M' >>= N) -> M >-> N

  | HFun: forall M N f g,
    term (appHead M) = ^f -> term (appHead N) = ^g -> f >#> g ->
    M [>>] (appArgs N) -> M >-> N

  | HMul: forall M N f,
    term (appHead M) = ^f -> term (appHead N) = ^f ->
    list2multiset (appArgs M) {>>} list2multiset (appArgs N) -> M >-> N

  | HAppFlat: forall M N Ns,
    isFunApp M -> isPartialFlattening Ns N -> M [>>] Ns -> M >-> N

  | HApp: forall M N (MApp: isApp M) (NApp: isApp N),
    ~isFunApp M -> ~isFunApp N ->
    {{appBodyL MApp, appBodyR MApp}} {>>} {{appBodyL NApp, appBodyR NApp}} ->
    M >-> N

  | HAbs: forall M N (MAbs: isAbs M) (NAbs: isAbs N),
    absBody MAbs >> absBody NAbs -> M >-> N

  | HBeta: forall M N,
    M -b-> N -> M >-> N

    where "M >-> N" := (prehorpo M N)

  with horpo : relation Term :=

  | Horpo: forall M N,
    type M = type N -> env M = env N -> algebraic M -> algebraic N ->
    M >-> N -> M >> N
    where "M >> N" := (horpo M N)

  with horpoMul : relation TermMul :=

  | HMulOrd: forall (M N: TermMul),
    MSetOrd.MultisetGT horpo M N -> M {>>} N
    where "M {>>} N" := (horpoMul M N)

  with horpoRC : relation Term :=

  | horpoRC_step: forall M N, M >> N -> M >>= N

  | horpoRC_refl: forall M, M >>= M

    where "M >>= N" := (horpoRC M N).

  Notation "M >>* N" := (clos_trans horpo M N) (at level 30).

  Scheme horpoArgs_Ind := Minimality for horpoArgs Sort Prop
    with prehorpo_Ind := Minimality for prehorpo Sort Prop
    with horpo_Ind := Minimality for horpo Sort Prop.

  Hint Constructors horpoRC horpo prehorpo horpoArgs : horpo.

  Lemma horpo_prehorpo : forall M N, M >> N -> M >-> N.

  Lemma horpo_type_preserving : forall M N, M >> N -> type M = type N.

  Lemma horpo_RC_type_preserving : forall M N, M >>= N -> type M = type N.

  Lemma horpo_env_preserving : forall M N, M >> N -> env M = env N.

  Lemma horpo_algebraic_left : forall M N, M >> N -> algebraic M.

  Lemma horpo_algebraic_right : forall M N, M >> N -> algebraic N.

  Lemma horpo_RC_env_preserving : forall M N, M >>= N -> env M = env N.

  Lemma horpo_eq_compat : forall M M' N N',
    M = M' -> N = N' -> M >> N -> M' >> N'.

  Instance horpo_eq_compat' : Proper (eq ==> eq ==> impl) horpo.


  Lemma prehorpo_var_normal : forall N M, isVar M -> ~ (M >-> N).

  Lemma horpo_var_normal : forall M N, isVar M -> ~(M >> N).

  Lemma term_neq_type : forall M N, type M <> type N -> M <> N.

  Lemma horpo_RC : forall M N, M >>= N -> M >> N \/ M = N.

  Lemma horpo_algebraic_preserving : forall M N, algebraic M ->
    M >> N -> algebraic N.

  Lemma beta_imp_horpo : forall M N, algebraic M -> M -b-> N -> M >> N.

  Lemma horpo_app_inv : forall M N (Mapp: isApp M) (Napp: isApp N),
    ~isFunApp M -> algebraic M ->
    ~isFunApp N -> algebraic N ->
    appBodyL Mapp >>= appBodyL Napp /\
    appBodyR Mapp >>= appBodyR Napp /\
    (appBodyL Mapp >> appBodyL Napp \/ appBodyR Mapp >> appBodyR Napp) ->
    M >> N.

  Lemma horpo_app : forall M N (Mapp: isApp M) (Napp: isApp N),
    type M = type N ->
    {{appBodyL Mapp, appBodyR Mapp}} {>>} {{appBodyL Napp, appBodyR Napp}} ->
    appBodyL Mapp >>= appBodyL Napp /\
    appBodyR Mapp >>= appBodyR Napp /\
    (appBodyL Mapp >> appBodyL Napp \/ appBodyR Mapp >> appBodyR Napp).

  Lemma horpo_app_reduct : forall M N (Mapp: isApp M), M >> N ->
    ~isFunApp M \/ isArrowType (type M) ->
    (exists MLabs: isAbs (appBodyL Mapp),
      N = lower (subst (beta_subst M Mapp MLabs)) (beta_lowering M Mapp MLabs)) \/
    exists Napp: isApp N,
      (appBodyL Mapp = appBodyL Napp /\ appBodyR Mapp >> appBodyR Napp) \/
      (appBodyL Mapp >> appBodyL Napp /\ appBodyR Mapp = appBodyR Napp) \/
      (appBodyL Mapp >> appBodyL Napp /\ appBodyR Mapp >> appBodyR Napp).

  Lemma horpo_abs_reduct : forall M (Mabs: isAbs M) N, M >> N ->
    exists Nabs: isAbs N, absBody Mabs >> absBody Nabs.

  Lemma horpo_args_conv : forall M N Ms Ns Q, M ~(Q) N ->
    (forall MsX, In MsX Ms -> env MsX = env M) ->
    (forall NsX, In NsX Ns -> env NsX = env N) ->
    conv_list Ms Ns Q ->
    (forall L L' R R', (subterm L M \/ (L = M /\ In R Ms)) ->
      L ~(Q) L' -> R ~(Q) R' -> L >> R -> env L' = env R' -> L' >> R'
    ) -> M [>>] Ms -> N [>>] Ns.

  Lemma horpo_conv_comp_aux : forall M N M' N' Q,
    (forall L L' R R' Q, (subterm L M \/ (L = M /\ subterm R N)) ->
      L ~(Q) L' -> R ~(Q) R' -> L >> R -> env L' = env R' -> L' >> R'
    ) -> M ~(Q) M' -> N ~(Q) N' -> M >> N -> env M' = env N' -> M' >> N'.

  Lemma horpo_conv_comp : forall M N M' N' Q,
    M ~(Q) M' -> N ~(Q) N' -> M >> N -> env M' = env N' -> M' >> N'.

  Lemma horpo_args_subst : forall M Ms Ns G (MG: correct_subst M G),
    subst_list Ms Ns G ->
    (forall L R (CL: correct_subst L G) (CR: correct_subst R G),
      (subterm L M \/ (L = M /\ In R Ms)) -> L >> R -> subst CL >> subst CR) ->
    M [>>] Ms -> subst MG [>>] Ns.

  Lemma horpo_subst_stable_aux : forall M N G (MG: correct_subst M G)
    (NG: correct_subst N G), algebraicSubstitution G ->
    (forall L R G (LG: correct_subst L G) (RG: correct_subst R G),
      algebraicSubstitution G -> (subterm L M \/ (L = M /\ subterm R N)) ->
      L >> R -> subst LG >> subst RG) ->
    M >> N -> subst MG >> subst NG.

  Lemma horpo_subst_stable : forall M N G (MS: correct_subst M G)
    (NS: correct_subst N G),
    algebraicSubstitution G -> M >> N -> subst MS >> subst NS.

  Lemma horpo_args_var_consistent : forall M Ns,
    (forall L R, (subterm L M \/ (L = M /\ In R Ns)) -> L >> R ->
      envSubset (activeEnv R) (activeEnv L)) ->
    M [>>] Ns -> forall N', In N' Ns -> envSubset (activeEnv N') (activeEnv M).

  Lemma horpo_var_consistent_aux : forall M N,
    (forall M' N', (subterm M' M \/ (M' = M /\ subterm N' N)) ->
      M' >> N' -> envSubset (activeEnv N') (activeEnv M')) ->
    M >> N -> envSubset (activeEnv N) (activeEnv M).

  Lemma horpo_var_consistent : forall M N,
    M >> N -> envSubset (activeEnv N) (activeEnv M).

  Lemma horpoArgs_dec : forall M Ns,
    (forall Marg N, subterm Marg M -> {Marg >>= N} + {~Marg >>= N}) ->
    (forall N, In N Ns -> {M >> N} + {~M >> N}) -> {M [>>] Ns} + {~M [>>] Ns}.

  Section ClausesDec.

    Variables M N : Term.
    Variable IH : forall L R,
      (subterm L M \/ (L = M /\ subterm R N)) -> {L >> R} + {~L >> R}.
    Variable Mfa : isFunApp M.

    Lemma IH_horpoRC : forall L R, (subterm L M \/ (L = M /\ subterm R N)) ->
      {L >>= R} + {~L >>= R}.

    Let Psub := exists2 M', isArg M' M & M' >>= N.
    Lemma HSub_dec : { Psub } + { ~Psub }.

    Lemma HAppFlat_dec : {Ns : list Term | isPartialFlattening Ns N & M [>>] Ns}
      + {~exists2 Ns: list Term, isPartialFlattening Ns N & M [>>] Ns }.

    Lemma HMul_dec : { f: FunctionSymbol | term (appHead M) = ^f
      /\ term (appHead N) = ^f /\
         list2multiset (appArgs M) {>>} list2multiset (appArgs N)} +
      { term (appHead M) <> term (appHead N) \/
        ~list2multiset (appArgs M) {>>} list2multiset (appArgs N) }.

    Lemma HFun_dec: { fg: FunctionSymbol * FunctionSymbol |
      term (appHead M) = ^(fst fg) /\
      term (appHead N) = ^(snd fg) /\ fst fg >#> snd fg /\ M [>>] (appArgs N)}
    + { ~isFunApp N \/ (forall f g, term (appHead M) = ^f ->
      term (appHead N) = ^g -> ~f >#> g) \/ ~M [>>] (appArgs N) }.

  End ClausesDec.

  Lemma prehorpo_dec : forall M N,
    (forall L R, (subterm L M \/ (L = M /\ subterm R N)) ->
      {L >> R} + {~L >> R}) -> env M = env N -> type M = type N ->
    algebraic M -> algebraic N -> {M >-> N} + {~ M >-> N}.

  Lemma horpo_dec: forall M N, {M >> N} + {~ M >> N}.

  Lemma horpo_monotonous : algebraic_monotonicity horpo.

  Hint Resolve horpo_prehorpo horpo_type_preserving horpo_eq_compat
    horpo_env_preserving horpo_algebraic_preserving horpo_var_normal
    horpo_app_reduct horpo_abs_reduct horpo_monotonous horpo_conv_comp
    horpo_subst_stable horpo_var_consistent : horpo.

End Horpo.