Library CoLoR.MannaNess.ARedPair

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2009-07-03
rule elimination with reduction pairs

Set Implicit Arguments.


module type for reduction pairs

Module Type WeakRedPair.

  Parameter Sig : Signature.

  Notation term := (@term Sig).

  Parameter succ : relation term.
  Parameter wf_succ : WF succ.
  Parameter sc_succ : substitution_closed succ.

  Parameter bsucc : term -> term -> bool.
  Parameter bsucc_sub : rel_of_bool bsucc << succ.

  Parameter succeq : relation term.
  Parameter sc_succeq : substitution_closed succeq.
  Parameter cc_succeq : context_closed succeq.
  Parameter refl_succeq : reflexive succeq.

  Parameter succ_succeq_compat : absorbs_left succ succeq.

  Parameter bsucceq : term -> term -> bool.
  Parameter bsucceq_sub : rel_of_bool bsucceq << succeq.

  Parameter trans_succ : transitive succ.
  Parameter trans_succeq : transitive succeq.

End WeakRedPair.

properties of reduction pairs

Module WeakRedPairProps (Import WP : WeakRedPair).

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

  Lemma WF_wp_hd_red_mod : forall E R,
    forallb (brule bsucceq) E = true ->
    forallb (brule bsucceq) R = true ->
    WF (hd_red_mod E (filter (brule (neg bsucc)) R)) ->
    WF (hd_red_mod E R).

  Variable cc_succ : context_closed succ.

  Lemma WF_rp_red_mod : forall E R,
    forallb (brule bsucceq) E = true ->
    forallb (brule bsucceq) R = true ->
    WF (red_mod (filter (brule (neg bsucc)) E) (filter (brule (neg bsucc)) R))
    -> WF (red_mod E R).

  Lemma WF_rp_red : forall R,
    forallb (brule bsucceq) R = true ->
    WF (red (filter (brule (neg bsucc)) R)) ->
    WF (red R).

tactics for Rainbow

  Ltac do_prove_termination prove_cc_succ lemma :=
    apply lemma;
      match goal with
      | |- context_closed _ => prove_cc_succ
      | |- WF _ => idtac
      | |- _ = _ => check_eq || fail 10 "some rule is not in the ordering"
      end.

  Ltac prove_termination prove_cc_succ :=
    let prove := do_prove_termination prove_cc_succ in
    match goal with
    | |- WF (red _) => prove WF_rp_red
    | |- WF (red_mod _ _) => prove WF_rp_red_mod
    | |- WF (hd_red_mod _ _) => prove WF_wp_hd_red_mod
    | |- WF (hd_red_Mod _ _) =>
      try rewrite int_red_incl_red;
        rewrite hd_red_mod_of_hd_red_Mod;
          prove_termination prove_cc_succ
   end.

End WeakRedPairProps.

reduction pair associated to a monotone algebra


Module WP_MonAlg (Import MA : MonotoneAlgebraType) <: WeakRedPair.

  Definition Sig := Sig.

  Definition succ := IR I succ.
  Definition wf_succ := IR_WF I succ_wf.
  Definition sc_succ := @IR_substitution_closed _ _ MA.succ.

  Definition bsucc := bool_of_rel succ'_dec.

  Lemma bsucc_sub : rel_of_bool bsucc << succ.

  Definition succeq := IR I succeq.
  Definition sc_succeq := @IR_substitution_closed _ _ MA.succeq.
  Definition cc_succeq := @IR_context_closed _ _ _ monotone_succeq.
  Definition refl_succeq := @IR_reflexive _ _ _ refl_succeq.

  Lemma succ_succeq_compat : absorbs_left succ succeq.

  Definition bsucceq := bool_of_rel succeq'_dec.

  Lemma bsucceq_sub : rel_of_bool bsucceq << succeq.

  Definition trans_succ := IR_transitive trans_succ.
  Definition trans_succeq := IR_transitive trans_succeq.

End WP_MonAlg.

reduction pair associated to a non-permutative non-collapsing arguments filtering


Module Type Filter.
  Parameter Sig : Signature.
  Parameter pi : forall f, vector bool (@arity Sig f).
  Declare Module WP : WeakRedPair with Definition Sig := filter_sig pi.
End Filter.


Module WP_Filter (Import F : Filter) <: WeakRedPair.

  Definition Sig := Sig.

  Import WP.

  Definition succ := filter_ord succ.
  Definition wf_succ := WF_filter wf_succ.
  Definition sc_succ := filter_subs_closed sc_succ.

  Definition bsucc t u := bsucc (filter pi t) (filter pi u).

  Lemma bsucc_sub : rel_of_bool bsucc << succ.

  Definition succeq := filter_ord succeq.
  Definition sc_succeq := filter_subs_closed sc_succeq.
  Definition cc_succeq := filter_cont_closed refl_succeq cc_succeq.

  Lemma refl_succeq : reflexive succeq.

  Lemma succ_succeq_compat : absorbs_left succ succeq.

  Definition bsucceq t u := bsucceq (filter pi t) (filter pi u).

  Lemma bsucceq_sub : rel_of_bool bsucceq << succeq.

  Lemma trans_succ : transitive succ.

  Lemma trans_succeq : transitive succeq.

End WP_Filter.

reduction pair associated to a permutative non-collapsing arguments filtering


Module Type Perm.
  Parameter Sig : Signature.
  Parameter pi : forall f : Sig, list (N (arity f)).
  Parameter pi_ok : non_dup pi.
  Declare Module WP : WeakRedPair with Definition Sig := filter_sig pi.
End Perm.


Module WP_Perm (Import F : Perm) <: WeakRedPair.

  Definition Sig := Sig.

  Import WP.

  Definition succ := filter_ord succ.
  Definition wf_succ := WF_filter wf_succ.
  Definition sc_succ := filter_subs_closed sc_succ.

  Definition bsucc t u := bsucc (filter pi t) (filter pi u).

  Lemma bsucc_sub : rel_of_bool bsucc << succ.

  Definition succeq := filter_ord succeq.
  Definition sc_succeq := filter_subs_closed sc_succeq.
  Definition cc_succeq := filter_weak_cont_closed pi_ok refl_succeq cc_succeq.

  Lemma refl_succeq : reflexive succeq.

  Lemma succ_succeq_compat : absorbs_left succ succeq.

  Definition bsucceq t u := bsucceq (filter pi t) (filter pi u).

  Lemma bsucceq_sub : rel_of_bool bsucceq << succeq.

  Lemma trans_succ : transitive succ.

  Lemma trans_succeq : transitive succeq.

End WP_Perm.

reduction pair associated to collapsing arguments filtering


Module Type Proj.
  Parameter Sig : Signature.
  Parameter pi : forall f : Sig, option {k | k < arity f}.
  Declare Module WP : WeakRedPair with Definition Sig := Sig.
End Proj.


Module WP_Proj (Import P : Proj) <: WeakRedPair.

  Definition Sig := Sig.

  Import WP.

  Definition succ := proj_ord pi succ.
  Definition wf_succ := WF_proj pi wf_succ.
  Definition sc_succ := proj_subs_closed pi sc_succ.

  Definition bsucc t u := bsucc (proj pi t) (proj pi u).

  Lemma bsucc_sub : rel_of_bool bsucc << succ.

  Definition succeq := proj_ord pi succeq.
  Definition sc_succeq := proj_subs_closed pi sc_succeq.
  Definition cc_succeq := proj_cont_closed pi refl_succeq cc_succeq.

  Lemma refl_succeq : reflexive succeq.

  Lemma succ_succeq_compat : absorbs_left succ succeq.

  Definition bsucceq t u := bsucceq (proj pi t) (proj pi u).

  Lemma bsucceq_sub : rel_of_bool bsucceq << succeq.

  Lemma trans_succ : transitive succ.

  Lemma trans_succeq : transitive succeq.

End WP_Proj.

reduction pair associated to VRPO_Prover