Library CoLoR.SemLab.AFlatCont

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2009-07-02
flat context closure (Sternagel & Middeldorp, RTA'08)

Set Implicit Arguments.


flat context closure of a rule

Section S.

  Variable Sig : Signature.

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

  Lemma flat_cont_aux : forall n i, i < n -> i + S (n - S i) = n.

  Definition flat_cont_symb n (f : Sig) i (h : i < arity f) :=
    Cont f (flat_cont_aux h) (fresh n i) Hole (fresh (n+i) (arity f - S i)).


  Variables (some_symbol : Sig) (arity_some_symbol : arity some_symbol > 0)
            (n : nat).

  Definition one_flat_cont := flat_cont_symb n arity_some_symbol.

  Definition flat_conts_symb n f :=
    map (fun x => flat_cont_symb n (N_prf x)) (L (arity f)).

  Variables (Fs : list Sig) (Fs_ok : forall x : Sig, In x Fs).

  Definition flat_conts n := flat_map (flat_conts_symb n) Fs.

  Definition flat_cont_rule (a : rule) c :=
    let (l,r) := a in mkRule (fill c l) (fill c r).

  Definition is_root_preserving (a : rule) := let (l,r) := a in
    match l, r with
      | Fun f _, Fun g _ => beq_symb f g
      | _, _ => true
    end.

  Definition flat_rule n (a : rule) :=
    if is_root_preserving a then a :: nil
      else map (flat_cont_rule a) (flat_conts n).

  Definition flat_rules R := flat_map (flat_rule (S n)) R.

  Lemma root_preserving : forall R a,
    is_root_preserving a = true -> In a R -> In a (flat_rules R).

main theorem for standard rewriting

  Section red.

    Variables (R : rules) (hyp : n >= maxvar_rules R).

    Lemma red_flat : red (flat_rules R) << red R.

    Definition red_flat_cont := Rof (red (flat_rules R)) (fill one_flat_cont).

    Lemma red_one_flat_cont_intro : red R << red_flat_cont.

    Lemma rtc_red_one_flat_cont_intro : forall t u, red R # t u ->
      red (flat_rules R) # (fill one_flat_cont t) (fill one_flat_cont u).

    Lemma WF_red_flat : WF (red R) <-> WF (red (flat_rules R)).

  End red.

main theorem for rewriting modulo

  Section red_mod.

    Variables E R : rules.
    Variable hypE : n >= maxvar_rules E.
    Variable hypR : n >= maxvar_rules R.

    Lemma WF_red_mod_flat :
      WF (red_mod E R) <-> WF (red_mod (flat_rules E) (flat_rules R)).

  End red_mod.

End S.

functorization

Module Type FlatCC.
  Parameter Sig : Signature.
  Parameter Fs : list Sig.
  Parameter Fs_ok : forall x : Sig, In x Fs.
  Parameter some_symbol : Sig.
  Parameter arity_some_symbol : arity some_symbol > 0.
End FlatCC.

Module FlatCCProps (Import F : FlatCC).

  Notation rules := (rules Sig).

  Section red_mod.

    Variables E R : rules.

    Let n := max (maxvar_rules E) (maxvar_rules R).

    Definition flat_mod_rules := flat_rules n Fs.

    Lemma WF_red_mod_flat :
      WF (red_mod E R) <-> WF (red_mod (flat_mod_rules E) (flat_mod_rules R)).

  End red_mod.

  Section red.

    Variable R : rules.

    Let n := maxvar_rules R.

    Definition flat_rules := flat_rules n Fs R.

    Lemma WF_red_flat : WF (red R) <-> WF (red flat_rules).

  End red.

  Ltac flat_cc :=
    match goal with
      | |- WF (red_mod _ _) => rewrite WF_red_mod_flat
      | |- WF (red _) => rewrite WF_red_flat
    end.

End FlatCCProps.