Library CoLoR.Term.WithArity.ASubterm

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Sidi Ould-Biha, 2010-04-27
Properties of the subterm relation.

Set Implicit Arguments.


Section S.

  Variable Sig : Signature.

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

list of immediate subterms

  Fixpoint subterm_lst t :=
    match t with
      | Var _ => nil
      | Fun f ts =>
        let fix subterm_lst_vec k (us : terms k) {struct us} : list term :=
          match us with
            | Vnil => nil
            | Vcons u1 us' => subterm_lst u1 ++ subterm_lst_vec _ us'
          end
          in list_of_vec ts ++ subterm_lst_vec (arity f) ts
    end.

  Fixpoint subterm_lst_vec k (us : terms k) : list term :=
    match us with
      | Vnil => nil
      | Vcons u1 us' => subterm_lst u1 ++ subterm_lst_vec us'
    end.

  Lemma subterm_lst_fun : forall F ts,
    subterm_lst (Fun F ts) = list_of_vec ts ++ subterm_lst_vec ts.

list of immediate subterms

  Lemma In_subterm_lst_vec_elim : forall v n (ts : terms n),
    In v (subterm_lst_vec ts) ->
    exists i, exists p : i < n, In v (subterm_lst (Vnth ts p)).

  Lemma In_subterm_lst_vec_intro : forall n (ts : terms n) v i (p : i < n),
    In v (subterm_lst (Vnth ts p)) -> In v (subterm_lst_vec ts).

the supterm relation is finitely branching

  Notation supterm := (@supterm Sig).

  Lemma fin_branch_supterm : finitely_branching supterm.

End S.