# 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.