Library CoLoR.Filter.AFilterBool

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

Set Implicit Arguments.


Section S.

  Variable Sig : Signature.

filtering function

  Variable pi : forall f, bools (@arity Sig f).

filtered signature

  Definition filter_arity f := Vtrue (pi f).

  Definition filter_sig := mkSignature filter_arity (@beq_symb_ok Sig).
  Notation Sig' := filter_sig.

  Notation term' := (ATerm.term Sig'). Notation Fun' := (@Fun Sig').
  Notation term := (term Sig). Notation terms := (vector term).

  Notation context' := (context Sig'). Definition Cont' := (@Cont Sig').
  Notation context := (context Sig).

term filtering

  Fixpoint filter (t : term) : term' :=
    match t with
      | Var x => Var x
      | Fun f ts => Fun' f (Vfilter (pi f) (Vmap filter ts))
    end.

rule filtering

  Notation rule' := (rule Sig'). Notation rules' := (list rule').
  Notation rule := (rule Sig). Notation rules := (list rule).

  Definition filter_rule a := mkRule (filter (lhs a)) (filter (rhs a)).

  Notation filter_rules := (List.map filter_rule).

properties wrt substitutions

  Definition filter_subs s (x : variable) := filter (s x).

  Lemma filter_sub : forall s t,
    filter (sub s t) = sub (filter_subs s) (filter t).

filter ordering

  Section filter_ordering.

    Variable succ : relation term'.

    Definition filter_ord : relation term :=
      fun t u => succ (filter t) (filter u).

    Notation fsucc := filter_ord.

transitivity
well-foundedness


    Lemma WF_filter : WF succ -> WF fsucc.

stability by substitution
compatibility


    Lemma filter_comp : forall R : rules,
      compat succ (filter_rules R) -> compat fsucc R.

properties wrt contexts

    Section filter_cont.

      Variables (f : Sig) (i j : nat) (e : i + S j = arity f)
        (v1 : terms i) (c : context) (v2 : terms j) (t : term).

      Let bs := Vbreak (n1:=i) (n2:=S j) (Vcast (pi f) (sym_eq e)).
      Let v1' := Vfilter (fst bs) (Vmap filter v1).
      Let t' := filter (fill c t).
      Let v2' := Vfilter (Vtail (snd bs)) (Vmap filter v2).
      Let h := trans_eq (Vtrue_break (n1:=i) (n2:=S j)
        (Vcast (pi f) (sym_eq e))) (Vtrue_cast (pi f) (sym_eq e)).

      Section filter_cont_true.

        Variable H : Vhead (snd bs) = true.

        Definition e_true := trans_eq (plus_reg_l_inv (Vtrue (fst bs))
          (Vtrue_Sn_true (snd bs) H)) h.

        Lemma filter_cont_true : filter (fill (Cont f e v1 c v2) t)
          = fill (Cont' f e_true v1' Hole v2') t'.

      End filter_cont_true.

      Section filter_cont_false.

        Variable H : Vhead (snd bs) = false.

        Definition e_false := trans_eq (plus_reg_l_inv (Vtrue (fst bs))
          (Vtrue_Sn_false (snd bs) H)) h.

        Lemma filter_cont_false : filter (fill (Cont f e v1 c v2) t)
          = Fun' f (Vcast (Vapp v1' v2') e_false).

      End filter_cont_false.

    End filter_cont.


stability wrt contexts
monotony wrt inclusion

  Lemma incl_filter : forall R S, R << S -> filter_ord R << filter_ord S.

weak stability wrt contexts

  Section weak_cont_closed.

    Variable succ : relation term'.

    Notation fsucc := (filter_ord succ).
    Notation succ_eq := (clos_refl succ).
    Notation fsucc_eq := (filter_ord succ_eq).

    Lemma filter_ord_rc : reflexive fsucc_eq.

    Lemma rc_filter_ord : inclusion (clos_refl fsucc) fsucc_eq.

    Lemma filter_weak_cont_closed :
      weak_context_closed succ succ_eq -> weak_context_closed fsucc fsucc_eq.

reduction ordering
rewriting

  Section red.

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

    Lemma red_incl_filter_red_rc : red R << filter_ord (red R' %).

    Lemma red_rtc_incl_filter_red_rtc : red R # << filter_ord (red R' #).

    Lemma hd_red_incl_filter_hd_red : hd_red R << filter_ord (hd_red R').

  End red.

rewriting modulo

  Section red_mod.

    Variable E R : rules.
    Notation E' := (filter_rules E).
    Notation R' := (filter_rules R).

    Lemma hd_red_mod_filter : hd_red_mod E R << filter_ord (hd_red_mod E' R').

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

  End red_mod.

End S.


tactics

Ltac filter p := hd_red_mod; apply WF_hd_red_mod_filter with (pi:=p).

signature functor

Module Type Filter.
  Parameter Sig : Signature.
  Parameter pi : forall f : Sig, bools (arity f).
End Filter.

Module Make (S : FSIG) (F : Filter with Definition Sig := S.Sig) <: FSIG.
  Definition Sig := filter_sig F.pi.
  Definition Fs := S.Fs.
  Definition Fs_ok := S.Fs_ok.
End Make.