Library CoLoR.Filter.AFilterPerm

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2009-09-09
non-collapsing arguments filtering with permutations

Set Implicit Arguments.

Section S.

  Variable Sig : Signature.

  Section pi.

    Variable pi : forall f : Sig, list (N (arity f)).

Assumption: pi does not duplicate arguments.
This hyp is not really necessary but it makes the proof of weak monotony simpler. Otherwise, we also need to assume that the ordering is transitive.

    Definition non_dup := forall f, nodup (map N_val (pi f)).

    Variable hyp : non_dup.

filtered signature

    Definition filter_arity f := length (pi f).

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

    Notation Sig' := filter_sig. Notation term' := (term Sig').
    Notation term := (term Sig). Notation terms := (vector term).

term filtering

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

rule filtering

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

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

    Notation filter_rules := (map filter_rule).

properties of term filtering 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.

preservation of transitivity
preservation of well-foundedness

      Lemma WF_filter : WF succ -> WF fsucc.

stability by substitution

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

weak monotony wrt contexts
strong monotony wrt contexts

      Definition permut := forall f i,
        i < arity f -> In i (map N_val (pi f)).

      Lemma filter_strong_cont_closed :
        permut -> context_closed succ -> context_closed fsucc.

    End filter_ordering.

monotony wrt inclusion

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


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

building a filtering function

  Section build_pi.

    Variable raw_pi : Sig -> list nat.

    Definition valid := forall f x, In x (raw_pi f) -> arity f > x.

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

    Definition bvalid :=
      forallb (fun f => forallb (bgt_nat (arity f)) (raw_pi f)) Fs.

    Lemma bvalid_ok : bvalid = true <-> valid.

    Variable raw_pi_ok : bvalid = true.

    Definition build_nat_lts : forall n l,
      forallb (bgt_nat n) l = true -> list (N n).

    Lemma build_nat_lts_ok : forall n l (h : forallb (bgt_nat n) l = true),
      map N_val (build_nat_lts h) = l.

    Definition build_pi : forall f : Sig, list (N (arity f)).

    Lemma build_pi_ok : forall f, map N_val (build_pi f) = raw_pi f.

verifying arguments non-duplication

    Definition bnon_dup :=
      forallb (fun f => bnodup beq_nat (raw_pi f)) Fs.

    Lemma bnon_dup_ok : bnon_dup = true <-> non_dup build_pi.

verify if all filters are permutations

    Definition bpermut :=
      forallb (fun f =>
        bforall_lt (fun i => mem beq_nat i (raw_pi f)) (arity f)) Fs.

    Lemma bpermut_ok : bpermut = true <-> permut build_pi.

  End build_pi.

End S.


Ltac non_dup :=
  match goal with
    | |- non_dup (build_pi _ _) => rewrite <- bnon_dup_ok; check_eq
    | |- non_dup ?pi => unfold pi; non_dup
  end || fail 10 "duplicating arguments filter".

Ltac permut :=
  match goal with
    | |- permut (build_pi _ _) => rewrite <- bpermut_ok; check_eq
    | |- permut ?pi => unfold pi; permut
  end || fail 10 "non-permutative arguments filter".

Ltac filter p :=
  hd_red_mod; apply WF_hd_red_mod_filter with (pi:=p); [non_dup | idtac].

Ltac prove_cc_succ tac :=
  apply filter_strong_cont_closed; [non_dup | permut | tac].

signature functor

Module Type Filter.
  Parameter Sig : Signature.
  Parameter pi : forall f : Sig, list (N (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.