Library CoLoR.Conversion.AReverse

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2009-10-16
unary TRS reversing

Set Implicit Arguments.


Section S.

  Variable Sig : Signature.

  Variable is_unary_sig : is_unary Sig.

  Notation term := (term Sig).
  Notation rule := (rule Sig). Notation rules := (list rule).

  Notation SSig := (SSig_of_ASig Sig).

  Definition rev_Sig := ASig_of_SSig SSig.

  Notation Sig' := rev_Sig.

signature isomorphism between Sig and Sig'

  Lemma is_unary_sig' : is_unary Sig'.

  Definition F (f : Sig) : Sig' := f.

  Lemma HF : forall f, arity f = arity (F f).

  Definition G (f : Sig') : Sig := f.

  Lemma HG : forall f, arity f = arity (G f).

  Lemma FG : forall f, F (G f) = f.

  Lemma GF : forall f, G (F f) = f.

isomorphism properties


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

  Lemma rule_of_srule_epi : forall a,
    maxvar (lhs a) = 0 -> maxvar (rhs a) = 0 ->
    rule_of_srule (srule_of_rule a) = Fr HF a.

  Lemma trs_of_srs_epi : forall R,
    (forall a, In a R -> maxvar (lhs a) = 0 /\ maxvar (rhs a) = 0) ->
    trs_of_srs (srs_of_trs R) = Fl HF R.

term and rule reversal

  Definition reverse_term (t : term) :=
    ATerm_of_String.term_of_string (ListUtil.rev' (string_of_term t)).

  Definition reverse_rule (e : rule) :=
    let (l,r) := e in mkRule (reverse_term l) (reverse_term r).

  Definition reverse_trs := List.map reverse_rule.

  Notation reverse_srule := (@SReverse.reverse SSig).
  Notation reverse_srs := (List.map reverse_srule).

preservation of variables
relations with reset
termination

  Variables R : rules.
  Variable hR : rules_preserve_vars R.

  Section red_mod.

    Variables E : rules.
    Variable hE : rules_preserve_vars E.

    Lemma WF_red_mod_rev_eq :
      WF (red_mod (reverse_trs E) (reverse_trs R)) <-> WF (red_mod E R).

  End red_mod.

  Lemma WF_red_rev_eq : WF (red (reverse_trs R)) <-> WF (red R).

End S.

tactics for Rainbow


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

Ltac rev_tac Fs_ok :=
  (rewrite <- WF_red_rev_eq || rewrite <- WF_red_mod_rev_eq);
  rev_tac_cond Fs_ok.