Library CoLoR.Term.WithArity.AUnary

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2005-02-17
properties of systems with unary symbols only

Set Implicit Arguments.


tactics

Ltac arity1 hyp :=
  match goal with
    | e : ?i + S ?j = arity ?f |- _ =>
      ded (hyp f); assert (i=0); [omega | subst i; assert (j=0);
        [omega | subst j; VOtac]]
end.

we assume a signature with unary symbols only

Section S.

Variable Sig : Signature.

Notation term := (term Sig). Notation terms := (vector term).
Notation context := (context Sig).
Notation substitution := (substitution Sig).
Notation rule := (rule Sig). Notation rules := (list rule).

Definition is_unary := forall f : Sig, 1 = arity f.

Variable is_unary_sig : is_unary.

Ltac arity := arity1 is_unary_sig.

boolean function checking is_unary

Definition bis_unary Fs := forallb (fun f : Sig => beq_nat 1 (arity f)) Fs.

Lemma bis_unary_ok : forall (Fs : list Sig) (Fs_ok : forall f, In f Fs),
  bis_unary Fs = true <-> is_unary.

unary function application

Definition Fun1 f (t : term) :=
  @Fun Sig f (Vcast (Vcons t Vnil) (is_unary_sig f)).

Lemma sub_fun1 : forall s f u, sub s (Fun1 f u) = Fun1 f (sub s u).

Lemma vars_fun1 : forall f u, vars (Fun1 f u) = vars u.

Lemma maxvar_fun1 : forall f t, maxvar (Fun1 f t) = maxvar t.

specific induction principle

Section term_ind.

Variables (P : term -> Prop)
  (Hvar : forall x, P (Var x))
  (Hfun : forall f t, P t -> P (Fun1 f t)).


Lemma term_ind_forall : forall t, P t.

End term_ind.

unique variable of a term

Fixpoint var (t : term) : variable :=
  match t with
    | Var x => x
    | Fun _ ts => Vmap_first 0 var ts
  end.

Lemma var_fun1 : forall f u, var (Fun1 f u) = var u.

Lemma var_fill : forall c t, var (fill c t) = var t.

Lemma var_sub : forall s t, var (sub s t) = var (s (var t)).

Lemma vars_var : forall t, vars t = var t :: nil.

Lemma maxvar_var : forall t, maxvar t = var t.

unary context application

Lemma cont_aux : forall f : Sig, 0 + S 0 = arity f.

Lemma cont_aux_eq : forall f, cont_aux f = is_unary_sig f.

Definition Cont1 f c := Cont f (cont_aux f) Vnil c Vnil.

Lemma fill_cont1 : forall f c t, fill (Cont1 f c) t = Fun1 f (fill c t).

biggest context of a term

Fixpoint cont (t : term) : context :=
  match t with
    | Var _ => Hole
    | Fun f ts => Cont1 f (Vmap_first Hole cont ts)
  end.

Lemma cont_fun1 : forall f t, cont (Fun1 f t) = Cont1 f (cont t).

Lemma subc_cont : forall s (c : context), subc s c = c.

Lemma term_cont_var : forall t, t = fill (cont t) (Var (var t)).

Lemma sub_cont : forall s t, sub s t = fill (cont t) (s (var t)).


Lemma term_sub_cont : forall x t,
  t = sub (single x (Var (var t))) (fill (cont t) (Var x)).

Lemma fill_var_elim : forall x c d (u : term), fill c (Var x) = fill d u ->
  exists e, c = comp d e.


Lemma fill_eq_cont : forall (t : term) c d, fill c t = fill d t <-> c = d.


Lemma maxvar_fill : forall (t : term) c, maxvar (fill c t) = maxvar t.

equivalent definition of rewriting (when rules preserve variables)

Section red.

Variables (R : rules) (hR : rules_preserve_vars R).

Lemma rules_preserve_vars_var : forall l r, In (mkRule l r) R -> var r = var l.


Definition red1 t u := exists l, exists r, exists c, exists d,
  In (mkRule l r) R /\ t = fill (comp c (comp (cont l) d)) (Var (var t))
  /\ u = fill (comp c (comp (cont r) d)) (Var (var t)).


Lemma red1_ok : forall t u, red R t u <-> red1 t u.


Lemma red1_eq : red R == red1.

End red.


equivalent definition of rewriting modulo (when rules preserve variables)

Section red_mod.

Variables (E R : rules)
  (hE : rules_preserve_vars E) (hR : rules_preserve_vars R).


Definition red_mod1 := red1 E # @ red1 R.

Lemma red_mod1_eq : red_mod E R == red_mod1.

End red_mod.

some properties of renamings

Definition is_renaming (s : substitution) := forall x, exists y, s x = Var y.

Lemma is_ren_single_var : forall x y, is_renaming (single x (Var y)).

Section renaming.

Variables (s : substitution) (hs : is_renaming s).

Lemma size_sub : forall t, size (sub s t) = size t.

Section red.

Variables (R : rules) (hR : rules_preserve_vars R).

Lemma red_ren : forall t u,
  red R (sub s t) u -> exists v, red R t v /\ sub s v = u.


Lemma rtc_red_ren : forall t u,
  red R # (sub s t) u -> exists v, red R # t v /\ sub s v = u.


Lemma SN_red_ren : forall t : term, SN (red R) t -> SN (red R) (sub s t).

End red.


Section red_mod.

Variables (E R : rules)
  (hE : rules_preserve_vars E) (hR : rules_preserve_vars R).

Lemma red_mod_ren : forall t u, red_mod E R (sub s t) u ->
  exists v, red_mod E R t v /\ sub s v = u.



Lemma SN_red_mod_ren : forall t : term,
  SN (red_mod E R) t -> SN (red_mod E R) (sub s t).

End red_mod.

End renaming.


equivalence with rewriting on terms with at most 0 as variable

Definition red0 (R : rules) t u := red R t u /\ maxvar t = 0.

Lemma red0_incl_red : forall R, red0 R << red R.

Section red0.


Variables (R : rules) (hR : rules_preserve_vars R).

Lemma red0_maxvar : forall t u, red0 R t u -> maxvar u = 0.

Lemma WF_red0 : WF (red R) <-> WF (red0 R).

End red0.

Definition red_mod0 (E R : rules) t u := red_mod E R t u /\ maxvar t = 0.

Lemma red_mod0_incl_red_mod : forall E R, red_mod0 E R << red_mod E R.

Section red_mod0.

Variables (E R : rules)
  (hE : rules_preserve_vars E) (hR : rules_preserve_vars R).

Lemma red_mod0_maxvar : forall t u, red_mod0 E R t u -> maxvar u = 0.

Lemma WF_red_mod0 : WF (red_mod E R) <-> WF (red_mod0 E R).

End red_mod0.

equivalence with rewriting on rules with at most 0 as variable

Section reset.

Definition reset t := sub (swap (var t) 0) t.

Definition reset_rule (a : rule) := mkRule (reset (lhs a)) (reset (rhs a)).

Definition reset_rules := map reset_rule.

Lemma reset_fun1 : forall f t, reset (Fun1 f t) = Fun1 f (reset t).

Lemma var_reset : forall t, var (reset t) = 0.

Lemma maxvar_reset : forall t, maxvar (reset t) = 0.

Lemma maxvar_reset_rules : forall R a, In a (reset_rules R) ->
  maxvar (lhs a) = 0 /\ maxvar (rhs a) = 0.

Section red.

Variable R : rules.
Variable hR : rules_preserve_vars R.

Lemma rules_preserve_vars_reset : rules_preserve_vars (reset_rules R).

Lemma red_reset : forall t u, red R t u <-> red (reset_rules R) t u.

Lemma red_reset_eq : red R == red (reset_rules R).

Lemma hd_red_reset : forall t u, hd_red R t u <-> hd_red (reset_rules R) t u.

Lemma hd_red_reset_eq : hd_red R == hd_red (reset_rules R).

End red.

Variable E R : rules.
Variable hE : rules_preserve_vars E.
Variable hR : rules_preserve_vars R.

Lemma red_mod_reset_eq : red_mod E R == red_mod (reset_rules E) (reset_rules R).

Lemma hd_red_mod_reset_eq :
  hd_red_mod E R == hd_red_mod (reset_rules E) (reset_rules R).

Lemma red_mod_reset : forall t u,
  red_mod E R t u <-> red_mod (reset_rules E) (reset_rules R) t u.

Lemma hd_red_mod_reset : forall t u,
  hd_red_mod E R t u <-> hd_red_mod (reset_rules E) (reset_rules R) t u.

End reset.

End S.


tactics for Rainbow

Ltac is_unary Fs_ok := rewrite <- (bis_unary_ok Fs_ok); check_eq.