Library CoLoR.Conversion.ATerm_of_String

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2005-02-17
convert a string into an algebraic term

Set Implicit Arguments.


Section S.

string signature


Variable SSig : VSignature.Signature.

Notation letter := (symbol SSig). Notation string := (string SSig).
Notation srule := (rule SSig). Notation srules := (rules SSig).

corresponding algebraic signature

Definition ar (_ : letter) := 1.


Definition ASig_of_SSig := mkSignature ar (@VSignature.beq_symb_ok SSig).

Notation ASig := ASig_of_SSig.

Notation term := (term ASig). Notation terms := (vector term).
Notation context := (context ASig).


Lemma is_unary_sig : is_unary ASig.

Ltac arity := arity1 is_unary_sig.
Ltac is_unary := try (exact is_unary_sig).

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

conversion string <-> term

Fixpoint term_of_string (s : string) : term :=
  match s with
    | List.nil => Var 0
    | a :: w => @Fun ASig a (Vcons (term_of_string w) Vnil)
  end.

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

Lemma reset_term_of_string :
  forall s, reset (term_of_string s) = term_of_string s.


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_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 string <-> context

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_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
    | a :: w => Cont1 a (cont_of_string w)
  end.

conversion string <-> substitution
rules

Definition rule_of_srule (x : srule) :=
  mkRule (term_of_string (Srs.lhs x)) (term_of_string (Srs.rhs x)).

Definition trs_of_srs R := List.map rule_of_srule R.

Lemma rules_preserve_vars_trs_of_srs :
  forall R, rules_preserve_vars (trs_of_srs R).

Ltac preserve_vars := try (apply rules_preserve_vars_trs_of_srs).

rewriting

Section red_of_sred.

Variable R : srules.

Lemma red_of_sred : forall x y,
  Srs.red R x y -> red (trs_of_srs R) (term_of_string x) (term_of_string y).

Lemma rtc_red_of_sred : forall x y,
  Srs.red R # x y -> red (trs_of_srs R) # (term_of_string x) (term_of_string y).

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

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

End red_of_sred.

reflexion of termination
preservation of termination
signature functor

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

tactics for Rainbow

Ltac as_trs := rewrite WF_red_mod || rewrite WF_red.