Library CoLoR.Term.WithArity.ADuplicateSymb

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Leo Ducas, 2007-08-06
Duplicate/mark symbols to distinguish internal reductions from head reductions

Set Implicit Arguments.


Section S.

Variable Sig : Signature.

Notation rules := (rules Sig).

signature of symbols marked as head or internal

Inductive dup_symb : Type :=
| hd_symb : symbol Sig -> dup_symb
| int_symb : symbol Sig -> dup_symb.

Definition dup_ar s :=
  match s with
    | hd_symb s' => arity s'
    | int_symb s' => arity s'
  end.

Definition beq_dup_symb (f g : dup_symb) : bool :=
  match f, g with
    | hd_symb f', hd_symb g' => beq_symb f' g'
    | int_symb f', int_symb g' => beq_symb f' g'
    | _, _ => false
  end.

Lemma beq_dup_symb_ok : forall f g, beq_dup_symb f g = true <-> f = g.

Definition dup_sig := mkSignature dup_ar beq_dup_symb_ok.

Notation Sig' := dup_sig. Notation Fun' := (@Fun Sig').

function marking all symbols as internal

Fixpoint dup_int_term t :=
  match t with
    | Var x => Var x
    | Fun f v => Fun' (int_symb f) (Vmap dup_int_term v)
  end.

Lemma dup_int_term_fun : forall f v,
  dup_int_term (Fun f v) = Fun' (int_symb f) (Vmap dup_int_term v).

function marking all symbols as internal except the head symbol

Definition dup_hd_term t :=
  match t with
    | Var x => Var x
    | Fun f v => Fun' (hd_symb f) (Vmap dup_int_term v)
  end.

Lemma dup_hd_term_fun : forall f v,
  dup_hd_term (Fun f v) = Fun' (hd_symb f) (Vmap dup_int_term v).

function marking substitutions

Definition dup_int_subst (s : substitution Sig) n := dup_int_term (s n).

Lemma dup_int_subst_spec : forall s t,
  sub (dup_int_subst s) (dup_int_term t) = dup_int_term (sub s t).

Lemma dup_int_subst_hd_dup : forall s f v,
  sub (dup_int_subst s) (dup_hd_term (Fun f v))
  = dup_hd_term (sub s (Fun f v)).

function marking contexts

Fixpoint dup_int_context c :=
  match c with
    | Hole => Hole
    | @Cont _ f _ _ H v c' w => @Cont Sig' (int_symb f) _ _ H
      (Vmap dup_int_term v) (dup_int_context c') (Vmap dup_int_term w)
  end.

Lemma dup_int_context_spec : forall c s l,
  dup_int_term (fill c (sub s l)) =
  fill (dup_int_context c) (sub (dup_int_subst s) (dup_int_term l)).

Definition dup_hd_context c :=
  match c with
    | Hole => Hole
    | @Cont _ f _ _ H v c' w => @Cont Sig' (hd_symb f) _ _ H
      (Vmap dup_int_term v) (dup_int_context c') (Vmap dup_int_term w)
  end.

functions marking rules

Definition dup_int_rule r :=
  mkRule (dup_int_term (lhs r)) (dup_int_term (rhs r)).

Definition dup_hd_rule r :=
  mkRule (dup_hd_term (lhs r)) (dup_hd_term (rhs r)).

Definition dup_int_rules := map dup_int_rule.

Definition dup_hd_rules := map dup_hd_rule.

reduction properties reflected by marking

Section red.

Variable R : rules.

Variable hyp : forallb (@is_notvar_lhs Sig) R = true.
Variable hyp' : forallb (@is_notvar_rhs Sig) R = true.

Lemma hd_red_dup_hd_red : forall t u, hd_red R t u ->
  hd_red (dup_hd_rules R) (dup_hd_term t) (dup_hd_term u).

Lemma red_dup_int_red : forall t u,
  red R t u -> red (dup_int_rules R) (dup_int_term t) (dup_int_term u).

Lemma int_red_dup_int_red : forall t u,
  int_red R t u -> red (dup_int_rules R) (dup_hd_term t) (dup_hd_term u).

End red.

preservation of termination by marking

Section WF.

Variables E R : rules.

Variable no_lhs_var : forallb (@is_notvar_lhs Sig) R = true.
Variable no_rhs_var : forallb (@is_notvar_rhs Sig) R = true.

Lemma WF_duplicate_hd_int_red :
  WF (hd_red_mod (dup_int_rules E) (dup_hd_rules R))
  -> WF (hd_red_Mod (int_red E #) R).

End WF.

basic functions on marked rules

Notation term' := (term Sig'). Notation rule' := (ATrs.rule Sig').

Definition is_int_symb (t : term') :=
  match t with
    | Fun (int_symb _) _ => true
    | _ => false
  end.

Definition is_int_symb_lhs (a : rule') := is_int_symb (lhs a).
Definition is_int_symb_rhs (a : rule') := is_int_symb (rhs a).

Definition is_hd_symb (t : term') :=
  match t with
    | Fun (hd_symb _) _ => true
    | _ => false
  end.

Definition is_hd_symb_lhs (a : rule') := is_hd_symb (lhs a).
Definition is_hd_symb_rhs (a : rule') := is_hd_symb (rhs a).

change marking of the top of a term

Definition mark (t : term') : term' :=
  match t with
    | Fun (int_symb f) ts => Fun' (hd_symb f) ts
    | t => t
  end.

Definition mark_rule (a : rule') : rule' :=
  let (l,r) := a in mkRule (mark l) (mark r).

Definition mark_rules := map mark_rule.

Definition unmark (t : term') : term' :=
  match t with
    | Fun (hd_symb f) ts => Fun' (int_symb f) ts
    | t => t
  end.

Definition unmark_rule (a : rule') : rule' :=
  let (l,r) := a in mkRule (unmark l) (unmark r).

Definition unmark_rules := map unmark_rule.

relation between (red R) and (int_red R) when R is_lhs_int_symb_headed

Section int_red.

Variable R : @ATrs.rules Sig'.

Variable int_hyp : forallb is_int_symb_lhs R = true.

Lemma dup_int_rules_int_red : forall f v t,
  red R (Fun' (hd_symb f) v) t -> int_red R (Fun' (hd_symb f) v) t.

Lemma dup_int_rules_int_red_rtc_aux : forall u t, red R # u t ->
  forall f v, u = Fun' (hd_symb f) v ->
    int_red R # u t /\ exists w, t = Fun' (hd_symb f) w.

Lemma dup_int_rules_int_red_rtc : forall f v t,
  red R # (Fun' (hd_symb f) v) t -> int_red R # (Fun' (hd_symb f) v) t.

End int_red.

properties of (red (dup_int_rules R))

Section red_dup.

Variable R : rules.

Notation R' := (dup_int_rules R).

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

Lemma red_dup_int_hd_symb : forall f us v,
  red R' (Fun' (hd_symb f) us) v -> exists vs, v = Fun' (hd_symb f) vs.

Lemma rtc_red_dup_int_hd_symb_aux : forall f u v, red R' # u v ->
  forall us, u = Fun' (hd_symb f) us -> exists vs, v = Fun' (hd_symb f) vs.

Lemma rtc_red_dup_int_hd_symb : forall f us v,
  red R' # (Fun' (hd_symb f) us) v -> exists vs, v = Fun' (hd_symb f) vs.

End red_dup.

End S.


tactics

Ltac mark := apply WF_duplicate_hd_int_red; [refl | refl | idtac].

signature functor

Module Make (S : FSIG) <: FSIG.

  Definition Sig := dup_sig S.Sig.

  Definition Fs :=
    fold_left (fun l f => hd_symb S.Sig f :: int_symb S.Sig f :: l) S.Fs nil.

  Lemma Fs_ok : forall f : Sig, In f Fs.

End Make.