Library CoLoR.Conversion.String_of_ATerm

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2009-10-14
conversion of a TRS with unary symbols only into an SRS

Set Implicit Arguments.


Section S.

term signature

  Variable ASig : Signature.

  Notation term := (term ASig). Notation context := (context ASig).
  Notation rule := (rule ASig). Notation rules := (list rule).

  Variable is_unary_sig : is_unary ASig.

  Notation Fun1 := (Fun1 is_unary_sig). Notation Cont1 := (Cont1 is_unary_sig).
  Notation cont := (cont is_unary_sig). Notation red1 := (red1 is_unary_sig).
  Notation term_ind_forall := (term_ind_forall is_unary_sig).

corresponding string signature

  Definition SSig_of_ASig := VSignature.mkSignature (@beq_symb_ok ASig).

  Notation SSig := SSig_of_ASig. Notation string := (string SSig).
  Notation srule := (Srs.rule SSig).

conversion term <-> string

  Fixpoint term_of_string (s : string) : term :=
    match s with
      | List.nil => Var 0
      | a :: w => Fun1 a (term_of_string w)
    end.

  Lemma var_term_of_string : forall s, var (term_of_string s) = 0.

  Fixpoint string_of_term (t : term) : string :=
    match t with
      | Var _ => List.nil
      | Fun f ts => f :: Vmap_first List.nil string_of_term ts
    end.

  Lemma string_of_term_fun1 : forall f t,
    string_of_term (Fun1 f t) = f :: string_of_term t.

  Lemma string_of_term_epi : forall s, string_of_term (term_of_string s) = s.

  Lemma term_of_string_epi : forall t, maxvar t = 0 ->
    term_of_string (string_of_term t) = t.


  Lemma string_of_term_sub : forall s l,
    string_of_term (sub s l) = string_of_term l ++ string_of_term (s (var l)).

conversion context <-> string

  Fixpoint string_of_cont (c : context) : string :=
    match c with
      | Hole => List.nil
      | @Cont _ f _ _ _ _ d _ => f :: string_of_cont d
    end.

  Lemma string_of_cont_cont : forall t,
    string_of_cont (cont t) = string_of_term t.

  Lemma string_of_cont_comp : forall c d,
    string_of_cont (comp c d) = string_of_cont c ++ string_of_cont d.

  Lemma string_of_term_fill : forall t c,
    string_of_term (fill c t) = string_of_cont c ++ string_of_term t.

  Fixpoint cont_of_string (s : string) : context :=
    match s with
      | List.nil => Hole
      | f :: s' => Cont1 f (cont_of_string s')
    end.

conversion string <-> substitution

  Definition sub_of_string s := single 0 (term_of_string s).

  Lemma term_of_string_fill : forall c s,
    term_of_string (SContext.fill c s) = fill (cont_of_string (lft c))
    (sub (sub_of_string (rgt c)) (term_of_string s)).

rules

  Definition srule_of_rule (x : rule) :=
    Srs.mkRule (string_of_term (lhs x)) (string_of_term (rhs x)).

  Definition srs_of_trs := List.map srule_of_rule.

invariance under reset


  Lemma string_of_term_reset :
    forall t, string_of_term (reset t) = string_of_term t.

  Lemma srule_of_rule_reset :
    forall a, srule_of_rule (reset_rule a) = srule_of_rule a.

  Lemma srs_of_trs_reset : forall R, srs_of_trs (reset_rules R) = srs_of_trs R.


  Section reset.

    Variables (R : rules) (h1 : rules_preserve_vars R)
      (h2 : forall l r, List.In (mkRule l r) R -> maxvar l = 0).

    Lemma red_of_sred_reset : forall t u,
      Srs.red (srs_of_trs R) t u -> red R (term_of_string t) (term_of_string u).

  End reset.

rewriting

  Section sred_of_red.

    Variables (R : rules) (hR : rules_preserve_vars R).

    Lemma sred_of_red : forall t u,
      red R t u -> Srs.red (srs_of_trs R) (string_of_term t) (string_of_term u).

    Lemma rtc_sred_of_red : forall t u, red R # t u ->
      Srs.red (srs_of_trs R) # (string_of_term t) (string_of_term u).

    Lemma red_of_sred : forall t u,
      Srs.red (srs_of_trs R) t u -> red R (term_of_string t) (term_of_string u).

    Lemma rtc_red_of_sred : forall t u, Srs.red (srs_of_trs R) # t u ->
      red R # (term_of_string t) (term_of_string u).

  End sred_of_red.

reflexion of termination

  Variables (R : rules) (hR : rules_preserve_vars R).

  Section red_mod.

    Variables (E : rules) (hE : rules_preserve_vars E).

    Lemma sred_mod_of_red_mod : forall x y, red_mod E R x y -> Srs.red_mod
      (srs_of_trs E) (srs_of_trs R) (string_of_term x) (string_of_term y).

    Lemma WF_red_mod_of_WF_sred_mod :
      WF (Srs.red_mod (srs_of_trs E) (srs_of_trs R)) -> WF (red_mod E R).

preservation of termination

    Lemma red_mod_of_sred_mod : forall t u,
      Srs.red_mod (srs_of_trs E) (srs_of_trs R) t u ->
      red_mod E R (term_of_string t) (term_of_string u).

    Lemma WF_sred_mod_of_WF_red_mod :
      WF (red_mod E R) -> WF (Srs.red_mod (srs_of_trs E) (srs_of_trs R)).

    Lemma WF_red_mod :
      WF (red_mod E R) <-> WF (Srs.red_mod (srs_of_trs E) (srs_of_trs R)).

  End red_mod.

  Lemma WF_red : WF (red R) <-> WF (Srs.red (srs_of_trs R)).

End S.

signature functor

Module Make (S : ASignature.FSIG) <: VSignature.FSIG.
  Definition Sig := SSig_of_ASig S.Sig.
  Definition Fs := S.Fs.
  Definition Fs_ok := S.Fs_ok.
End Make.

tactics for Rainbow


Ltac as_srs_cond Fs_ok :=
  match goal with
    | |- is_unary _ => is_unary Fs_ok
    | |- rules_preserve_vars _ => rules_preserve_vars
    | |- WF _ => idtac
  end.

Ltac as_srs Fs_ok :=
  (rewrite WF_red_mod || rewrite WF_red); as_srs_cond Fs_ok.