CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Frederic Blanqui, 2008-10-08
over graph based on unification

Set Implicit Arguments.

Section S.

Variable N : nat.
over graph based on unification

Section unif.

Variable Sig : Signature.

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

Variables R D : rules.

Definition connectable u v := unifiable (ren_cap R (S (maxvar v)) u) v.

Definition dpg_unif (r1 r2 : rule) :=
In r1 D /\ In r2 D /\ connectable (rhs r1) (lhs r2).

Variable hypR : forallb (@is_notvar_lhs Sig) R = true.

Lemma dpg_unif_correct : hd_rules_graph (red R #) D << dpg_unif.

over graph using a finite number of unification steps

Definition ren_cap (r1 r2 : rule) :=
ren_cap R (S (maxvar (lhs r2))) (rhs r1).

Definition unifiable_N r1 r2 :=
iter_step N (mk_problem (ren_cap r1 r2) (lhs r2)).

Definition connectable_N r1 r2 :=
match unifiable_N r1 r2 with
| None => false
| Some (_, nil) => true
| _ => hd_eq (rhs r1) (lhs r2)
end.

Notation mem := (mem (@beq_rule Sig)).
Notation mem_ok := (mem_ok (@beq_rule_ok Sig)).

Definition dpg_unif_N r1 r2 := mem r1 D && mem r2 D && connectable_N r1 r2.

Variable hypD : forallb (undefined_rhs R) D = true.

Lemma successfull_hd_eq : forall x r1 r2, In r1 D -> In r2 D ->
successfull (iter_step x (mk_problem (ren_cap r1 r2) (lhs r2))) = true ->
hd_eq (rhs r1) (lhs r2) = true.

Lemma dpg_unif_N_correct : hd_rules_graph (red R #) D << Graph dpg_unif_N.

End unif.

with marked symbols

Section mark.

Variable Sig : Signature.

Notation Sig' := (dup_sig Sig).

Lemma undefined_hd_symb_dup_int_rules : forall f R,
@defined Sig' (hd_symb Sig f) (dup_int_rules R) = false.

Variables R D : rules Sig.

Notation R' := (dup_int_rules R). Notation D' := (dup_hd_rules D).

Variable hypR : forallb (@is_notvar_lhs Sig') R' = true.
Variable hypD : forallb (@is_notvar_rhs Sig') D' = true.

Lemma dpg_unif_N_mark_correct :
hd_rules_graph (red R' #) D' << Graph (dpg_unif_N R' D').

End mark.

End S.

tactics

Ltac dpg_unif_N_correct :=
(apply dpg_unif_N_mark_correct || apply dpg_unif_N_correct);
(check_eq || fail 10 "a LHS is a variable").