Library CoLoR.Term.WithArity.AVariables

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2008-02-22
set of variables occuring in a term

Set Implicit Arguments.


sets of variables

Module XSet := FSetAVL.Make Nat_as_OT.
Module Export VarSetUtil := FSetUtil.Make XSet.

Lemma eqb_beq_nat x y : eqb x y = beq_nat x y.

Hint Rewrite eqb_beq_nat : mem.
Hint Rewrite beq_nat_ok : mem.
Hint Rewrite (beq_refl beq_nat_ok) : mem.

variables in a term

Section S.

Variable Sig : Signature.

Notation term := (term Sig).
Notation terms := (vector term).

Fixpoint vars t :=
  match t with
    | Var x => singleton x
    | Fun f ts =>
      let fix vars_vec n (ts : terms n) :=
        match ts with
          | Vnil => empty
          | Vcons u ts => union (vars u) (vars_vec _ ts)
        end
        in vars_vec _ ts
  end.

Definition vars_vec :=
  fix vars_vec n (ts : terms n) :=
  match ts with
    | Vnil => empty
    | Vcons u ts => union (vars u) (vars_vec _ ts)
  end.

Lemma vars_fun : forall f ts, vars (Fun f ts) = vars_vec ts.

Fixpoint vars_list ts :=
  match ts with
    | nil => empty
    | t :: ts' => union (vars t) (vars_list ts')
  end.

Lemma in_vars_mem : forall x (u : term),
  List.In x (ATerm.vars u) <-> mem x (vars u) = true.

Lemma mem_vars_vec : forall x n (ts : terms n),
  mem x (vars_vec ts) = true -> exists t, Vin t ts /\ mem x (vars t) = true.


Local Open Scope nat_scope.

Lemma mem_vars_size_sub_ge : forall s x u,
  mem x (vars u) = true -> size (sub s u) >= size (s x).


Lemma mem_vars_size_sub_gt : forall s x u,
  mem x (vars u) = true -> u <> Var x -> size (sub s u) > size (s x).


Lemma wf_term_var : forall s x u,
  s x = sub s u -> mem x (vars u) = true -> u = Var x.


Lemma vars_subs_elim : forall s x (v : term), mem x (vars (sub s v)) = true ->
  exists y, mem y (vars v) = true /\ mem x (vars (s y)) = true.

Lemma vars_subs_intro : forall s x y, mem x (vars (s y)) = true ->
  forall v : term, mem y (vars v) = true -> mem x (vars (sub s v)) = true.

Lemma notin_vars_subs_elim : forall s x (v : term),
  mem x (vars (sub s v)) = false ->
  forall y, mem y (vars v) = true -> mem x (vars (s y)) = false.

Lemma notin_vars_subs_intro : forall s x (v : term),
  (forall y, mem y (vars v) = true -> mem x (vars (s y)) = false) ->
  mem x (vars (sub s v)) = false.


Lemma vars_single : forall x v u,
  vars (sub (single x v) u) [=]
  if mem x (vars u) then union (vars v) (remove x (vars u)) else vars u.

Lemma vars_singles : forall x v us,
  vars_list (map (sub (single x v)) us) [=]
  if mem x (vars_list us) then union (vars v) (remove x (vars_list us))
    else vars_list us.



Notation rule := (rule Sig). Notation rules := (rules Sig).

Definition brule_preserve_vars (a : rule) :=
  subset (vars (rhs a)) (vars (lhs a)).

Definition brules_preserve_vars := forallb brule_preserve_vars.

Lemma vars_equiv : forall x (t : term),
  List.In x (ATerm.vars t) <-> In x (vars t).

Lemma brule_preserve_vars_ok' : forall l r,
  brule_preserve_vars (mkRule l r) = true
  <-> incl (ATerm.vars r) (ATerm.vars l).

Lemma brule_preserve_vars_ok : forall a : rule,
  brule_preserve_vars a = true <->
  incl (ATerm.vars (rhs a)) (ATerm.vars (lhs a)).

Lemma brules_preserve_vars_ok : forall R : rules,
  brules_preserve_vars R = true <-> rules_preserve_vars R.

End S.


Ltac rules_preserve_vars := rewrite <- brules_preserve_vars_ok;
  (check_eq || fail 10 "some rule does not preserve variables").