Library CoLoR.Filter.AProj

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2005-05-13
arguments filtering with projections only

Set Implicit Arguments.


Section S.

Variable Sig : Signature.

Notation term := (term Sig). Notation terms := (vector term).
Notation rule := (rule Sig). Notation rules := (list rule).

projection function

Section proj.

  Variable pi : forall f : Sig, option {k | k < arity f}.

  Fixpoint proj t :=
    match t with
      | Var _ => t
      | Fun f ts =>
        match pi f with
          | None => Fun f (Vmap proj ts)
          | Some o => let (_, h) := o in proj (Vnth ts h)
        end
    end.

  Definition proj_rule a := mkRule (proj (lhs a)) (proj (rhs a)).

  Definition proj_rules := (map proj_rule).

properties wrt substitutions

  Definition psub s (x : variable) := proj (s x).

  Lemma proj_sub : forall s t,
    proj (sub s t) = sub (psub s) (proj t).

projection ordering

  Section proj_ordering.

    Variable succ : relation term.

    Definition proj_ord : relation term := fun t u => succ (proj t) (proj u).

    Notation psucc := proj_ord.

transitivity
well-foundedness

    Lemma WF_proj : WF succ -> WF psucc.

stability by substitution
compatibility

    Lemma proj_comp : forall R : rules,
      compat succ (proj_rules R) -> compat psucc R.

stability wrt contexts
monotony wrt inclusion

  Lemma incl_proj : forall R S, R << S -> proj_ord R << proj_ord S.

rewriting

  Section red.

    Variable R : rules. Notation R' := (proj_rules R).

    Lemma red_incl_proj_red_rc : red R << proj_ord (red R' %).

    Lemma red_rtc_incl_proj_red_rtc : red R # << proj_ord (red R' #).

    Lemma hd_red_incl_proj_hd_red : hd_red R << proj_ord (hd_red R').

  End red.

rewriting modulo

  Section red_mod.

    Variable E R : rules.

    Notation E' := (proj_rules E).
    Notation R' := (proj_rules R).

    Lemma hd_red_mod_proj : hd_red_mod E R << proj_ord (hd_red_mod E' R').

    Lemma WF_hd_red_mod_proj : WF (hd_red_mod E' R') -> WF (hd_red_mod E R).

  End red_mod.

End proj.

building a projection

Variable raw_pi : Sig -> option nat.

Definition valid := forall f k, raw_pi f = Some k -> k < arity f.

Section pi.

  Variable hyp : valid.

  Definition mk_proj (f : Sig) k := @exist _ (fun k => k < arity f) k.


  Definition build_pi : forall f : Sig, option {k | k < arity f}.


End pi.

Variable Fs : list Sig.
Variable Fs_ok : forall f : Sig, In f Fs.

Definition bvalid_symb f :=
  match raw_pi f with
    | Some k => bgt_nat (arity f) k
    | None => true
  end.

Definition bvalid := forallb bvalid_symb Fs.

Lemma bvalid_ok : bvalid = true <-> valid.

End S.


tactics

Ltac proj p := hd_red_mod; apply WF_hd_red_mod_proj with (pi:=p).

Ltac valid Fs_ok :=
  match goal with
    | |- valid ?p => rewrite <- (@bvalid_ok _ p _ Fs_ok);
      (check_eq || fail 10 "invalid projection")
  end.