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.

Rewrite system structure.

Module Type RS_Struct.

Declare Module Export L : L_Struct.

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.

Rewrite relation associated to a rewrite system and some of its properties.

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.

Instance subs_S_aeq : Proper (Logic.eq ==> S_aeq ==> S_aeq) subs.

Term vector rewriting modulo alpha-equivalence.

Infix "-->S" := (Vrel1 S) (at level 70).
Infix "==>S" := (clos_vaeq S) (at level 70).

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.

CP structure associated to a rewrite system.

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.

  Import LComp.

  Notation cp_aeq := (Proper (aeq ==> impl)) (only parsing).
  Notation cp_sn := (@cp_sn F X R_aeq).
  Notation cp_red := (@cp_red F X R_aeq).
  Notation cp_neutral := (@cp_neutral F X R_aeq neutral).
  Notation cp := (@cp F X aeq R_aeq neutral).

End CP_beta_eta_rewrite.