Library CoLoR.Conversion.VTerm_of_ATerm

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2005-12-05
from algebraic terms to varyadic terms

Set Implicit Arguments.


Section S.

algebraic signature


  Variable ASig : Signature.

  Notation aterm := (term ASig). Notation aterms := (vector aterm).
  Notation AFun := (@Fun ASig).

corresponding varyadic signature


  Definition VSig_of_ASig := mkSignature (@ASignature.beq_symb_ok ASig).

  Notation VSig := VSig_of_ASig.

  Notation vterm := (term VSig). Notation vterms := (list vterm).
  Notation VFun := (@Fun VSig).

conversion of terms

  Fixpoint vterm_of_aterm (t : aterm) : vterm :=
    match t with
      | ATerm.Var x => Var x
      | ATerm.Fun f v =>
        let fix vterms_of_aterms n (ts : aterms n) : vterms :=
          match ts with
            | Vnil => List.nil
            | Vcons t' ts' => vterm_of_aterm t' :: vterms_of_aterms _ ts'
          end
          in VFun f (vterms_of_aterms (arity f) v)
    end.

  Fixpoint vterms_of_aterms n (ts : aterms n) : vterms :=
    match ts with
      | Vnil => List.nil
      | Vcons t' ts' => vterm_of_aterm t' :: vterms_of_aterms ts'
    end.

  Lemma vterm_fun : forall f ts,
    vterm_of_aterm (AFun f ts) = VFun f (vterms_of_aterms ts).

  Lemma vterms_cast : forall n (ts : aterms n) m (h : n=m),
    vterms_of_aterms (Vcast ts h) = vterms_of_aterms ts.

  Lemma vterms_app : forall n1 (ts1 : aterms n1) n2 (ts2 : aterms n2),
    vterms_of_aterms (Vapp ts1 ts2)
    = vterms_of_aterms ts1 ++ vterms_of_aterms ts2.

  Lemma vterms_map : forall (A : Set) (f : A -> aterm) n (v : vector A n),
    vterms_of_aterms (Vmap f v)
    = List.map (fun x => vterm_of_aterm (f x)) (list_of_vec v).

  Lemma vterms_length : forall n (ts : aterms n),
    length (vterms_of_aterms ts) = n.

conversion of contexts


  Notation acont := (@context ASig).
  Notation ACont := (@Cont ASig).
  Notation afill := fill.


  Notation vcont := (@context VSig).
  Notation VCont := (@Cont VSig).

  Fixpoint vcont_of_acont (c : acont) : vcont :=
    match c with
      | AContext.Hole => Hole
      | @AContext.Cont _ f i j _ ts1 d ts2 =>
        VCont f (vterms_of_aterms ts1) (vcont_of_acont d) (vterms_of_aterms ts2)
    end.

  Lemma vterm_fill : forall t c,
    vterm_of_aterm (afill c t) = fill (vcont_of_acont c) (vterm_of_aterm t).

conversion of substitutions


  Notation asubs := (@substitution ASig).
  Notation asub := (@sub ASig).


  Notation vsubs := (@substitution VSig).
  Notation vsub := (@sub VSig).

  Definition vsubs_of_asubs (s : asubs) x := vterm_of_aterm (s x).

  Lemma vterm_subs : forall s t,
    vterm_of_aterm (asub s t) = vsub (vsubs_of_asubs s) (vterm_of_aterm t).

conversion of rules


  Notation arule := (@ATrs.rule ASig).
  Notation ared := (@ATrs.red ASig).


  Notation vrule := (@VTrs.rule VSig).
  Notation vred := (@VTrs.red VSig).

  Definition vrule_of_arule (rho : arule) : vrule :=
    let (l,r) := rho in mkRule (vterm_of_aterm l) (vterm_of_aterm r).

  Variable R : list arule.

  Definition vrules_of_arules := List.map vrule_of_arule R.

  Notation S := vrules_of_arules.

  Lemma vred_of_ared : forall t u,
    ared R t u -> vred S (vterm_of_aterm t) (vterm_of_aterm u).

preservation of termination


  Lemma SN_vred_imp_SN_ared : forall t,
    SN (vred S) t -> forall u, t = vterm_of_aterm u -> SN (ared R) u.

  Lemma WF_vred_imp_WF_ared : WF (vred S) -> WF (ared R).

End S.