Library CoLoR.RPO.VMPO

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Solange Coupet-Grimal and William Delobel, 2006-01-09
Model of MPO statisfying Hypotheses in RPO_Types


Module MPO (PT : VPrecedenceType).

  Module Export P := VPrecedence PT.
  Module Export S := Status PT.

  Inductive lt_mpo : relation term :=
    | mpo1 : forall f g ss ts, g <F f ->
        (forall t, In t ts -> lt_mpo t (Fun f ss)) ->
        lt_mpo (Fun g ts) (Fun f ss)
    | mpo2 : forall f g, f =F= g ->
        forall ss ts, mult (transp lt_mpo) ts ss ->
          lt_mpo (Fun g ts) (Fun f ss)
    | mpo3 : forall t f ss,
        ex (fun s => In s ss /\ (s = t \/ lt_mpo t s)) ->
        lt_mpo t (Fun f ss).

  Definition mytau (f : Sig) (r : relation term) := mult (transp r).

End MPO.



Module MPO_Model (PT : VPrecedenceType) <: RPO_Model with Module P := PT.

  Module P := PT.
  Module Export MPO := MPO PT.

  Definition tau := mytau.

  Lemma tau_dec : forall f R ts ss,
    (forall t s, In t ts -> In s ss -> {R t s} + {~R t s}) ->
    {tau f R ts ss} + {~tau f R ts ss}.

  Lemma status_eq : forall f g, f =F= g -> tau f = tau g.

  Definition lt := lt_mpo.


  Lemma lt_roots : forall f g, g <F f ->
    forall ss ts, (forall t, In t ts -> lt t (Fun f ss)) -> lt (Fun g ts) (Fun f ss).

  Lemma lt_status : forall f g, f =F= g ->
    forall ss ts, (forall t, In t ts -> lt t (Fun f ss)) ->
      tau f lt ts ss -> lt (Fun g ts) (Fun f ss).

  Lemma lt_subterm : forall f ss t,
    ex (fun s => In s ss /\ (s = t \/ lt t s)) -> lt t (Fun f ss).

  Lemma lt_decomp : forall s t, lt s t ->
    ((ex (fun f => ex (fun g => ex (fun ss => ex (fun ts =>
      ltF f g /\
      (forall s, In s ss -> lt s (Fun g ts)) /\
      s = Fun f ss /\
      t = Fun g ts
    )))))
    \/
    ex (fun f => ex (fun g => ex (fun ss => ex (fun ts =>
      f =F= g /\
      (forall s, In s ss -> lt s (Fun g ts)) /\
      tau f lt ss ts /\
      s = Fun f ss /\
      t = Fun g ts)))))
    \/
    ex (fun f => ex (fun ts => ex (fun t' => In t' ts /\ (s = t' \/ lt s t')) /\
      t = Fun f ts)).


  Lemma SPO_to_status_SPO : forall f (r : relation term),
    forall ss,
      (forall s, In s ss -> (forall t u, r s t -> r t u -> r s u) /\ (r s s -> False)) ->
      (forall ts us, tau f r ss ts -> tau f r ts us -> tau f r ss us) /\ (tau f r ss ss -> False).

  Lemma mono_axiom : forall f (r : relation term),
    forall ss ts, one_less r ss ts -> tau f r ss ts.


  Definition wf_ltF := ltF_wf.
  Definition leF_dec := leF_dec.

  Definition lifting R := forall l, Accs lt l -> Restricted_acc (Accs lt) R l.

  Lemma status_lifting : forall f, lifting (tau f lt).

End MPO_Model.