Library CoLoR.RPO.VRPO_Status

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 RPO with status


Inductive status_name : Set :=
| lexicographic : status_name
| multiset : status_name.

Module RPO (PT : VPrecedenceType).

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

  Parameter status : Sig -> status_name.

  Definition mytau f (r : relation term) : relation terms :=
    match status f with
    | lexicographic => lex r
    | multiset => mult (transp r)
    end.

  Parameter eq_st : forall f g, f =F= g -> status f = status g.

  Inductive lt_rpo : relation term :=
    | rpo1 : forall f g ss ts, g <F f ->
        (forall t, In t ts -> lt_rpo t (Fun f ss)) ->
        lt_rpo (Fun g ts) (Fun f ss)
    | rpo2_lex : forall f g, f =F= g -> status f = lexicographic ->
        forall ss ts, (forall t, In t ts -> lt_rpo t (Fun f ss)) ->
          lex lt_rpo ts ss -> lt_rpo (Fun g ts) (Fun f ss)
    | rpo2_mult : forall f g, f =F= g -> status f = multiset ->
        forall ss ts, mult (transp lt_rpo) ts ss ->
          lt_rpo (Fun g ts) (Fun f ss)
    | rpo3 : forall t f ss,
      ex (fun s => In s ss /\ (s = t \/ lt_rpo t s)) ->
      lt_rpo t (Fun f ss).

End RPO.


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

  Module P := PT.
  Module Export RPO := RPO PT.

  Definition tau := mytau.

  Lemma status_dec : forall f,
    {status f = lexicographic} + {status f = multiset}.

  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_rpo.


  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 : relation terms) :=
    forall l, Accs lt l -> Restricted_acc (Accs lt) R l.

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

End RPO_Model.