# Library CoLoR.DP.AHDE

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Frederic Blanqui, 2008-09-25
• Leo Ducas, 2007-08-06
a simple over graph of the DP graph based on the equality of head symbols ("hde" stands for head equality)

Set Implicit Arguments.

definition of the hde over graph

Section prop_def.

Variable Sig : Signature.

Variable D : rules Sig.

Definition hde r1 r2 := In r1 D /\ In r2 D /\
match rhs r1 with
| Var _ => True
| Fun f _ =>
match lhs r2 with
| Var _ => True
| Fun g _ => f=g
end
end.

Lemma hde_restricted : is_restricted hde D.

Notation eq_rule_dec := (@eq_rule_dec Sig).
Notation eq_symb_dec := (@eq_symb_dec Sig).

Lemma hde_dec : forall r1 r2, {hde r1 r2} + {~hde r1 r2}.

End prop_def.

correctness

Section prop_correct.

Variable Sig : Signature.

Variables R D : rules Sig.

Lemma int_red_hd_rules_graph_incl_hde :
hd_rules_graph (int_red R #) D << hde D.

End prop_correct.

correctness with marked symbols
definition of hde as a boolean function

Section bool_def.

Variable Sig : Signature.

Variables D : rules Sig.

Definition hd_eq (u v : term Sig) :=
match u with
| Var _ => true
| Fun f _ =>
match v with
| Var _ => true
| Fun g _ => beq_symb f g
end
end.

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

Definition hde_bool r1 r2 :=
mem r1 D && mem r2 D && hd_eq (rhs r1) (lhs r2).

Lemma hde_bool_correct_aux : forall x y, hde D x y <-> Graph hde_bool x y.

End bool_def.

correctness

Section bool_correct.

Variable Sig : Signature.

Variables R D : rules Sig.

Lemma hde_bool_correct : hd_rules_graph (int_red R #) D << Graph (hde_bool D).

correctness with marked symbols
tactics

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