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