Library CoLoR.Term.WithArity.AMorphism

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2009-05-07
algebra morphisms

Set Implicit Arguments.


Section Morphism.

we assume given a morphism between two signatures S1 and S2

  Variables S1 S2 : Signature.

  Variables (F : S1 -> S2) (HF : forall f, arity f = arity (F f)).

translation of terms in S1 into terms in S2

  Fixpoint Ft (t : term S1) : term S2 :=
    match t with
      | Var x => Var x
      | Fun f ts => Fun (F f) (Vcast (Vmap Ft ts) (HF f))
    end.

  Definition Fv := Vmap Ft.

translation of contexts in S1 into contexts in S2

  Lemma Fc_aux : forall i j n n', i+S j=n -> n=n' -> i+S j=n'.


  Fixpoint Fc (c : context S1) : context S2 :=
    match c with
      | Hole => Hole
      | @Cont _ f _ _ e v1 c' v2 =>
        Cont (F f) (Fc_aux e (HF f)) (Fv v1) (Fc c') (Fv v2)
    end.

  Lemma Ft_fill : forall t c, Ft (fill c t) = fill (Fc c) (Ft t).


  Definition Fr (a : rule S1) := let (l,r) := a in mkRule (Ft l) (Ft r).

  Definition Fl := map Fr.

  Definition Frs := image Fr.


  Instance Frs_equiv : Proper (equiv ==> equiv) Frs.


  Lemma Rules_Fl : forall R, of_list (Fl R) [=] Frs (of_list R).

  Lemma incl_Frs : forall R S, R [<=] S -> Frs R [<=] Frs S.

  Lemma Frs_app : forall R S a, Frs (union R S) a <-> Frs R a \/ Frs S a.


  Definition Fs (s : substitution S1) x := Ft (s x).

  Lemma Ft_sub : forall s t, Ft (sub s t) = sub (Fs s) (Ft t).

F preserves rewriting

  Lemma Fred : forall R t u, red R t u -> red (Frs R) (Ft t) (Ft u).

  Lemma Fhd_red : forall R t u, hd_red R t u -> hd_red (Frs R) (Ft t) (Ft u).

  Lemma Fred_rtc : forall R t u, red R # t u -> red (Frs R) # (Ft t) (Ft u).

  Lemma Fred_mod : forall E R t u,
    red_mod E R t u -> red_mod (Frs E) (Frs R) (Ft t) (Ft u).

  Lemma Fhd_red_mod : forall E R t u,
    hd_red_mod E R t u -> hd_red_mod (Frs E) (Frs R) (Ft t) (Ft u).

reflexion of termination

  Lemma Fred_WF : forall R, WF (red (Frs R)) -> WF (red R).

  Lemma Fred_mod_WF : forall E R,
    WF (red_mod (Frs E) (Frs R)) -> WF (red_mod E R).

  Lemma Fhd_red_mod_WF : forall E R,
    WF (hd_red_mod (Frs E) (Frs R)) -> WF (hd_red_mod E R).

finite versions


  Lemma Fred_WF_fin : forall R, WF (red (Fl R)) -> WF (red R).

  Lemma Fred_mod_WF_fin : forall E R,
    WF (red_mod (Fl E) (Fl R)) -> WF (red_mod E R).

  Lemma Fhd_red_mod_WF_fin : forall E R,
    WF (hd_red_mod (Fl E) (Fl R)) -> WF (hd_red_mod E R).

End Morphism.


preservation of termination

Import ARules.

Section Preserv.

  Variables S1 S2 : Signature.
  Variables (F : S1 -> S2) (HF : forall f, arity f = arity (F f)).
  Variables (G : S2 -> S1) (HG : forall f, arity f = arity (G f)).
  Variables (E R : set (rule S1)) (E' R' : set (rule S2)).
  Variables (hyp1 : Frs HG E' [<=] E) (hyp2 : Frs HF E [<=] E').
  Variables (hyp3 : Frs HG R' [<=] R) (hyp4 : Frs HF R [<=] R').

  Lemma WF_Fred : WF (red R) -> WF (red (Frs HF R)).

  Lemma WF_Fred_mod : WF (red_mod E R) -> WF (red_mod (Frs HF E) (Frs HF R)).

  Lemma WF_Fhd_red_mod :
    WF (hd_red_mod E R) -> WF (hd_red_mod (Frs HF E) (Frs HF R)).

End Preserv.

epimorphism

Section Epi.

  Variables S1 S2 : Signature.
  Variables (F : S1 -> S2) (HF : forall f, arity f = arity (F f)).
  Variables (G : S2 -> S1) (HG : forall f, arity f = arity (G f)).
  Variable FG : forall f, F (G f) = f.

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

  Lemma Ft_epi : forall t, Ft HF (Ft HG t) = t.

  Lemma Fv_epi : forall n (ts : vector (term S2) n), Fv HF (Fv HG ts) = ts.

  Lemma Fc_epi : forall c, Fc HF (Fc HG c) = c.

  Lemma Fr_epi : forall a, Fr HF (Fr HG a) = a.

  Lemma Fl_epi : forall l, Fl HF (Fl HG l) = l.

End Epi.


isomorphism

Section Iso.

  Variables S1 S2 : Signature.
  Variables (F : S1 -> S2) (HF : forall f, arity f = arity (F f)).
  Variables (G : S2 -> S1) (HG : forall f, arity f = arity (G f)).
  Variables (FG : forall f, F (G f) = f) (GF : forall f, G (F f) = f).

  Lemma Frs_epi : forall R, Frs HG (Frs HF R) [<=] R.

  Variables E R : set (rule S1).

  Lemma WF_Fred_iso : WF (red R) <-> WF (red (Frs HF R)).

  Lemma WF_Fred_mod_iso :
    WF (red_mod E R) <-> WF (red_mod (Frs HF E) (Frs HF R)).

  Lemma WF_Fhd_red_mod_iso :
    WF (hd_red_mod E R) <-> WF (hd_red_mod (Frs HF E) (Frs HF R)).

End Iso.