Library CoLoR.Term.WithArity.ACalls

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2004-12-22
symbols defined by a set of rules, list of calls in a rhs

Set Implicit Arguments.


Section S.

Variable Sig : Signature.

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

check whether f is defined by l

Fixpoint defined (f : Sig) (l : rules) : bool :=
  match l with
    | nil => false
    | r :: l' =>
      match lhs r with
        | Var _ => defined f l'
        | Fun g ts => beq_symb g f || defined f l'
      end
  end.

Lemma lhs_fun_defined : forall (f : Sig) us r R,
  In (mkRule (Fun f us) r) R -> defined f R = true.

Lemma defined_app : forall f l1 l2,
 defined f (l1 ++ l2) = defined f l1 || defined f l2.

Lemma defined_equiv : forall f R,
 defined f R = true <-> exists v, exists r, In (mkRule (Fun f v) r) R.

Fixpoint list_defined (l : rules) : list Sig :=
  match l with
    | nil => nil
    | r :: l' =>
      match lhs r with
        | Var _ => list_defined l'
        | Fun f ts => f :: list_defined l'
      end
  end.

Lemma defined_list_ok :
 forall R f, defined f R = true <-> In f (list_defined R).

list of calls to a defined symbol in a term

Variable R : rules.

Fixpoint calls (t : term) : list term :=
  match t with
    | Var v => nil
    | Fun f ts =>
      let fix vcalls n (ts : terms n) : list term :=
        match ts with
          | Vnil => nil
          | Vcons u ts' => calls u ++ vcalls _ ts'
        end
      in match defined f R with
           | true => t :: vcalls (arity f) ts
           | false => vcalls (arity f) ts
         end
  end.

Fixpoint vcalls n (ts : terms n) : list term :=
  match ts with
    | Vnil => nil
    | Vcons u ts' => calls u ++ vcalls ts'
  end.

Lemma calls_fun : forall f ts, calls (Fun f ts) =
  match defined f R with
    | true => Fun f ts :: vcalls ts
    | false => vcalls ts
  end.

Definition undefined t :=
  match t with
  | Fun f _ => negb (defined f R)
  | _ => false
  end.

Definition undefined_lhs a := undefined (lhs a).
Definition undefined_rhs a := undefined (rhs a).

properties

Lemma in_vcalls : forall x t n (ts : terms n),
  In x (calls t) -> Vin t ts -> In x (vcalls ts).

Lemma in_vcalls_nil : forall x n (v : terms n),
  Vin x v -> vcalls v = nil -> calls x = nil.


Lemma in_calls : forall x t, In x (calls t)
  -> exists g, exists vs, x = Fun g vs /\ defined g R = true.


Lemma in_calls_defined : forall t g vs,
  In (Fun g vs) (calls t) -> defined g R = true.

Lemma in_calls_subterm : forall u t, In u (calls t) -> subterm_eq u t.

Lemma subterm_in_calls : forall g us, defined g R = true
  -> forall t, subterm_eq (Fun g us) t -> In (Fun g us) (calls t).

End S.