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").