Library CoLoR.DP.ADPUnif

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)

    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.


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