Library CoLoR.Term.Lambda.LCompRewrite
CoLoR, a Coq library on rewriting and termination.
See the COPYRIGHTS and LICENSE files.
- Frederic Blanqui, 2013-05-06
Higher-order rewriting and its associated CP structure
Set Implicit Arguments.
We assume given a set of rules preserving free variables and
whose left-hand sides are of the form apps (Fun f) ls.
Parameter rule : relation Te.
Declare Instance fv_rule : Proper (rule --> Subset) fv.
Parameter lhs_fun : forall l r, rule l r -> F.
Parameter lhs_nb_args : forall l r, rule l r -> nat.
Parameter lhs_args : forall l r (h : rule l r), Tes (lhs_nb_args h).
Parameter lhs_ok : forall l r (h : rule l r),
l = apps (Fun (lhs_fun h)) (lhs_args h).
End RS_Struct.
Module Make (Export RS : RS_Struct).
Module Export A := LAlpha.Make L.
Lemma rule_ok : forall l r, rule l r ->
exists f n (ls : Tes n), l = apps (Fun f) ls.
Equations satisfied by lhs_fun, lhs_nb_args and lhs_args.
Lemma lhs_fun_eq : forall f n (ts : Tes n) r
(h : rule (apps (Fun f) ts) r), lhs_fun h = f.
Lemma lhs_nb_args_eq : forall f n (ts : Tes n) r
(h : rule (apps (Fun f) ts) r), lhs_nb_args h = n.
Lemma lhs_nb_args_eq_sym : forall f n (ts : Tes n) r
(h : rule (apps (Fun f) ts) r), n = lhs_nb_args h.
Lemma lhs_args_eq : forall f n (ts : Tes n) r (h : rule (apps (Fun f) ts) r),
lhs_args h = Vcast ts (lhs_nb_args_eq_sym h).
Rewriting is defined as the alpha-closure of the monotone
closure of the substitution closure of the set of rules.
Notation Sh := (clos_subs rule).
Infix "->Sh" := (clos_subs rule) (at level 70).
Notation succ := Datatypes.S.
Notation S := (clos_mon Sh).
Infix "->S" := (clos_mon Sh) (at level 70).
Notation S_aeq := (clos_aeq S).
Infix "=>S" := (clos_aeq S) (at level 70).
Rewriting is stable by substitution.
Term vector rewriting modulo alpha-equivalence.
Inversion lemma when rewriting a term of the form apps (Fun f) us.
Lemma rewrite_apps_fun : forall f n (us : Tes n) t,
apps (Fun f) us ->S t ->
(exists vs, t = apps (Fun f) vs /\ us -->S vs)
\/ (exists p (ls : Tes p) r s q (vs : Tes q) (h : p+q=n),
rule (apps (Fun f) ls) r
/\ us = Vcast (Vapp (Vmap (subs s) ls) vs) h
/\ t = apps (subs s r) vs).
Lemma rewrite_aeq_apps_fun : forall f n (us : Tes n) t,
apps (Fun f) us =>S t ->
(exists vs, t = apps (Fun f) vs /\ us ==>S vs)
\/ (exists p (ls : Tes p) r s q (vs : Tes q) (h : p+q=n),
rule (apps (Fun f) ls) r
/\ us ~~~ Vcast (Vapp (Vmap (subs s) ls) vs) h
/\ t ~~ apps (subs s r) vs).
End Make.
Module CP_beta_eta_rewrite (Import RS : RS_Struct) <: LComp.CP_Struct.
Module L := L.
Module Import S := Make RS.
Module Import B := LBeta.Make L.
Module Import E := LEta.Make L.
We consider the union of beta-reduction and rewriting.
Definition Rh := beta_top U eta_top U Sh.
Infix "->Rh" := Rh (at level 70).
Notation R := (clos_mon Rh).
Infix "->R" := (clos_mon Rh) (at level 70).
Notation R_aeq := (clos_aeq R).
Infix "=>R" := (clos_aeq R) (at level 70).
Lemma R_aeq_alt : R_aeq == beta_aeq U eta_aeq U S_aeq.
A term is neutral if it is not a Lam nor it is headed by a Fun.
Definition neutral (u : Te) :=
match u with
| Def.Lam _ _ => False
| _ =>
match head u with
| Def.Fun _ => False
| _ => True
end
end.
CP structure properties not involving reduction.
Instance neutral_aeq : Proper (aeq ==> impl) neutral.
Lemma neutral_var : forall x, neutral (Var x).
Lemma neutral_app : forall u v, neutral u -> neutral (App u v).
Lemma not_neutral_lam : forall x u, ~neutral (Lam x u).
Lemma neutral_beta : forall x u v, neutral (App (Lam x u) v).
Lemma not_neutral_apps_fun :
forall f n (ts : Tes n), ~neutral (apps (Fun f) ts).
CP structure properties involving reduction.
Instance subs_R_aeq : Proper (Logic.eq ==> R_aeq ==> R_aeq) subs.
Instance fv_Rh : Proper (Rh --> Subset) fv.
Lemma not_Rh_var x u : ~ Var x ->Rh u.
Lemma Rh_eh x u w : Lam x u ->Rh w -> Lam x u ->eh w.
Lemma Rh_bh x u v w : App (Lam x u) v ->Rh w -> App (Lam x u) v ->bh w.
Lemma not_Rh_app_neutral u v w : neutral u -> ~ App u v ->Rh w.
Term vector rewriting.
Infix "==>R" := (clos_vaeq R) (at level 70).
Lemma clos_vaeq_alt n :
@clos_vaeq n R == @clos_vaeq n beta U @clos_vaeq n eta U @clos_vaeq n S.
Inversion lemma for terms of the form apps (Fun f) us.
Lemma beta_eta_rewrite_aeq_apps_fun : forall f n (us : Tes n) t,
apps (Fun f) us =>R t ->
(exists vs, t = apps (Fun f) vs /\ us ==>R vs)
\/ (exists p (ls : Tes p) r s q (vs : Tes q) (h : p+q=n),
rule (apps (Fun f) ls) r
/\ us ~~~ Vcast (Vapp (Vmap (subs s) ls) vs) h
/\ t ~~ apps (subs s r) vs).
Some notations.