Library CoLoR.Term.WithArity.ATerm

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Sebastien Hinderer, 2004-02-09
  • Frederic Blanqui, 2005-02-17
algebraic terms with fixed arity

Set Implicit Arguments.


Notation variables := (list variable) (only parsing).

Section S.

  Variable Sig : Signature.

terms



  Inductive term : Type :=
  | Var : variable -> term
  | Fun : forall f : Sig, vector term (arity f) -> term.


  Notation terms := (vector term).

induction principles

  Section term_rect.

    Variables
      (P : term -> Type)
      (Q : forall n, terms n -> Type).

    Hypotheses
      (H1 : forall x, P (Var x))
      (H2 : forall f v, Q v -> P (Fun f v))
      (H3 : Q Vnil)
      (H4 : forall t n (v : terms n), P t -> Q v -> Q (Vcons t v)).

    Fixpoint term_rect t : P t :=
      match t as t return P t with
        | Var x => H1 x
        | Fun f v =>
          let fix terms_rect n (v : terms n) : Q v :=
            match v as v return Q v with
              | Vnil => H3
              | Vcons t' v' => H4 (term_rect t') (terms_rect _ v')
            end
            in H2 f (terms_rect (arity f) v)
      end.

  End term_rect.

  Definition term_ind (P : term -> Prop) (Q : forall n, terms n -> Prop) :=
    term_rect P Q.

  Section term_ind_comb.

    Variables
      (Pt : term -> Prop)
      (Ps : forall n, terms n -> Prop).

    Hypotheses
      (Hvar : forall x, Pt (Var x))
      (Hfun : forall f ts, Ps ts -> Pt (Fun f ts))
      (Hnil : Ps Vnil)
      (Hcns : forall t n (ts : terms n), Pt t -> Ps ts -> Ps (Vcons t ts)).

    Lemma term_ind_comb : (forall t, Pt t) /\ (forall n (ts : terms n), Ps ts).

  End term_ind_comb.

  Lemma term_ind_forall : forall (P : term -> Prop)
    (H1 : forall v, P (Var v))
    (H2 : forall f v, Vforall P v -> P (Fun f v)),
    forall t, P t.

  Lemma term_ind_forall_cast : forall (P : term -> Prop)
    (Hvar : forall x, P (Var x))
    (Hfun : forall f n (ts : terms n) (h : n = arity f),
      Vforall P ts -> P (Fun f (Vcast ts h))),
    forall t, P t.

  Lemma term_ind_forall2 : forall (P : term -> Prop)
    (H1 : forall v, P (Var v))
    (H2 : forall f v, (forall t, Vin t v -> P t) -> P (Fun f v)),
    forall t, P t.

equality

  Lemma var_eq : forall x x', x = x' -> Var x = Var x'.

  Lemma args_eq : forall f v v', v = v' -> Fun f v = Fun f v'.

  Lemma fun_eq : forall f v w, Fun f v = Fun f w -> v = w.

  Lemma symb_eq : forall f us g vs, Fun f us = Fun g vs -> f = g.

  Lemma fun_eq_cast : forall f g m (ts : terms m) n (us : terms n)
    (p : m = arity f) (q : n = arity g) (r : m=n), f = g ->
    us = Vcast ts r -> Fun f (Vcast ts p) = Fun g (Vcast us q).

  Lemma fun_eq_intro : forall f ts g us (h : f = g),
    us = Vcast ts (f_equal (@arity Sig) h) -> Fun f ts = Fun g us.

  Lemma symb_arg_eq : forall f us g vs (h : f = g),
    Fun f us = Fun g vs -> vs = Vcast us (f_equal (@arity Sig) h).

decidability of equality

  Fixpoint beq_term (t u : term) :=
    match t, u with
      | Var x, Var y => beq_nat x y
      | Fun f ts, Fun g us =>
        let fix beq_terms n (ts : terms n) p (us : terms p) :=
          match ts, us with
            | Vnil, Vnil => true
            | Vcons t ts', Vcons u us' =>
              beq_term t u && beq_terms _ ts' _ us'
            | _, _ => false
          end
          in beq_symb f g && beq_terms _ ts _ us
      | _, _ => false
    end.

  Lemma beq_terms : forall n (ts : terms n) p (us : terms p),
    (fix beq_terms n (ts : terms n) p (us : terms p) :=
      match ts, us with
        | Vnil, Vnil => true
        | Vcons t ts', Vcons u us' => beq_term t u && beq_terms _ ts' _ us'
        | _, _ => false
      end) _ ts _ us = beq_vec beq_term ts us.

  Lemma beq_fun : forall f ts g us,
    beq_term (Fun f ts) (Fun g us) = beq_symb f g && beq_vec beq_term ts us.

  Lemma beq_term_ok : forall t u, beq_term t u = true <-> t = u.

  Definition eq_term_dec := dec_beq beq_term_ok.



maximal variable index in a term

  Fixpoint maxvar (t : term) : nat :=
    match t with
      | Var x => x
      | Fun f v => Vmax (Vmap maxvar v)
    end.

  Definition maxvars n (ts : terms n) := Vmax (Vmap maxvar ts).

  Lemma maxvars_cons : forall t n (ts : terms n),
    maxvars (Vcons t ts) = max (maxvar t) (maxvars ts).

  Lemma maxvar_fun : forall f ts, maxvar (Fun f ts) = maxvars ts.

  Lemma maxvar_var : forall k x, maxvar (Var x) <= k -> x <= k.

  Definition maxvar_le k t := maxvar t <= k.

  Lemma maxvar_le_fun : forall m f ts,
    maxvar (Fun f ts) <= m -> Vforall (maxvar_le m) ts.

  Lemma maxvar_le_arg : forall f ts m t,
    maxvar (Fun f ts) <= m -> Vin t ts -> maxvar t <= m.

  Lemma maxvars_cast : forall n (ts : terms n) p (e : n=p),
    maxvars (Vcast ts e) = maxvars ts.

list of variables in a term: a variable occurs in the list as much as it has occurrences in t

  Fixpoint vars (t : term) : variables :=
    match t with
      | Var x => x :: nil
      | Fun f v =>
        let fix vars_vec n (ts : terms n) : variables :=
          match ts with
            | Vnil => nil
            | Vcons t' ts' => vars t' ++ vars_vec _ ts'
          end
          in vars_vec (arity f) v
    end.

  Fixpoint vars_vec n (ts : terms n) : variables :=
    match ts with
      | Vnil => nil
      | Vcons t' ts' => vars t' ++ vars_vec ts'
    end.

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

  Lemma vars_vec_cast : forall n (ts : terms n) m (h : n=m),
    vars_vec (Vcast ts h) = vars_vec ts.

  Lemma vars_vec_app : forall n1 (ts1 : terms n1) n2 (ts2 : terms n2),
    vars_vec (Vapp ts1 ts2) = vars_vec ts1 ++ vars_vec ts2.

  Lemma vars_vec_cons : forall t n (ts : terms n),
    vars_vec (Vcons t ts) = vars t ++ vars_vec ts.

  Lemma in_vars_vec_elim : forall x n (ts : terms n),
    In x (vars_vec ts) -> exists t, Vin t ts /\ In x (vars t).

  Lemma vars_vec_in : forall x t n (ts : terms n),
    In x (vars t) -> Vin t ts -> In x (vars_vec ts).

  Lemma vars_max : forall x t, In x (vars t) -> x <= maxvar t.

  Lemma maxvar_in : forall x t n (v : terms n),
    x <= maxvar t -> Vin t v -> x <= maxvars v.

  Lemma maxvar_lmax : forall t, maxvar t = lmax (vars t).

boolean function testing if a variable occurs in a term

  Section var_occurs_in.

    Variable x : variable.

    Fixpoint var_occurs_in t :=
      match t with
        | Var y => beq_nat x y
        | Fun f ts =>
          let fix var_occurs_in_terms n (ts : terms n) :=
            match ts with
              | Vnil => false
              | Vcons t ts' => var_occurs_in t || var_occurs_in_terms _ ts'
            end
            in var_occurs_in_terms _ ts
      end.

    Fixpoint var_occurs_in_terms n (ts : terms n) :=
      match ts with
        | Vnil => false
        | Vcons t ts' => var_occurs_in t || var_occurs_in_terms ts'
      end.

    Lemma var_occurs_in_fun :
      forall f ts, var_occurs_in (Fun f ts) = var_occurs_in_terms ts.

    Lemma var_occurs_in_ok : forall t,
      var_occurs_in t = true <-> In x (vars t).

  End var_occurs_in.

number of symbol occurrences in a term

  Fixpoint nb_symb_occs t :=
    match t with
      | Var x => 0
      | Fun f ts =>
        let fix nb_symb_occs_terms n (ts : terms n) :=
          match ts with
            | Vnil => 0
            | Vcons u us => nb_symb_occs u + nb_symb_occs_terms _ us
          end
          in 1 + nb_symb_occs_terms _ ts
    end.

  Fixpoint nb_symb_occs_terms n (ts : terms n) :=
    match ts with
      | Vnil => 0
      | Vcons u us => nb_symb_occs u + nb_symb_occs_terms us
    end.

  Lemma nb_symb_occs_fix : forall n (ts : terms n),
    (fix nb_symb_occs_terms n (ts : terms n) :=
      match ts with
        | Vnil => 0
        | Vcons u us => nb_symb_occs u + nb_symb_occs_terms _ us
      end) _ ts = nb_symb_occs_terms ts.

  Lemma nb_symb_occs_fun : forall f ts,
    nb_symb_occs (Fun f ts) = 1 + nb_symb_occs_terms ts.

  Lemma Vin_nb_symb_occs_terms_ge : forall n (ts : terms n) t,
    Vin t ts -> nb_symb_occs_terms ts >= nb_symb_occs t.

list of symbols occurring in a term

  Fixpoint symbs (t : term) : list Sig :=
    match t with
      | Var x => nil
      | Fun f v =>
        let fix symbs_vec n (ts : terms n) : list Sig :=
          match ts with
            | Vnil => nil
            | Vcons t' ts' => symbs t' ++ symbs_vec _ ts'
          end
          in f :: symbs_vec (arity f) v
    end.

  Fixpoint symbs_vec n (ts : terms n) : list Sig :=
    match ts with
      | Vnil => nil
      | Vcons t' ts' => symbs t' ++ symbs_vec ts'
    end.

  Lemma symbs_fun : forall f ts, symbs (Fun f ts) = f :: symbs_vec ts.

  Lemma symbs_vec_cast : forall n (ts : terms n) m (h : n=m),
    symbs_vec (Vcast ts h) = symbs_vec ts.

  Lemma symbs_vec_app : forall n1 (ts1 : terms n1) n2 (ts2 : terms n2),
    symbs_vec (Vapp ts1 ts2) = symbs_vec ts1 ++ symbs_vec ts2.

  Lemma symbs_vec_cons : forall t n (ts : terms n),
    symbs_vec (Vcons t ts) = symbs t ++ symbs_vec ts.

  Lemma in_symbs_vec_elim : forall x n (ts : terms n),
    In x (symbs_vec ts) -> exists t, Vin t ts /\ In x (symbs t).

  Lemma symbs_vec_in : forall x t n (ts : terms n),
    In x (symbs t) -> Vin t ts -> In x (symbs_vec ts).

size of a term

  Fixpoint size t :=
    match t with
      | Var x => 1
      | Fun f ts =>
        let fix size_terms n (ts : terms n) :=
          match ts with
            | Vnil => 0
            | Vcons u us => size u + size_terms _ us
          end
          in 1 + size_terms _ ts
    end.

  Fixpoint size_terms n (ts : terms n) :=
    match ts with
      | Vnil => 0
      | Vcons u us => size u + size_terms us
    end.

  Lemma size_fix : forall n (ts : terms n),
    (fix size_terms n (ts : terms n) :=
      match ts with
        | Vnil => 0
        | Vcons u us => size u + size_terms _ us
      end) _ ts = size_terms ts.

  Lemma size_fun : forall f ts, size (Fun f ts) = 1 + size_terms ts.

  Lemma size_non_zero : forall t, size t > 0.

  Lemma Vin_size_terms_ge : forall n (ts : terms n) t,
    Vin t ts -> size_terms ts >= size t.


  Lemma Vin_size_terms_gt : forall n (ts : terms n) t,
    Vin t ts -> n > 1 -> size_terms ts > size t.

  Lemma size_terms_cast : forall n (ts : terms n) m (h : n=m),
    size_terms (Vcast ts h) = size_terms ts.

  Lemma size_terms_app : forall n (ts : terms n) m (us : terms m),
    size_terms (Vapp ts us) = size_terms ts + size_terms us.

  Lemma term_ind_size : forall (P : term -> Prop),
    (forall n, (forall t, size t <= n -> P t) -> forall t, size t <= S n -> P t)
    -> forall t, P t.

direct subterms of a term

  Definition direct_subterms (t : term) : list term :=
    match t with
      | Var x => nil
      | Fun f fs => list_of_vec fs
    end.

End S.

implicit arguments


tactics

Ltac Funeqtac :=
  match goal with
    | H : @Fun _ ?f _ = @Fun _ ?f _ |- _ => ded (fun_eq H); clear H
    | H : @Fun _ ?f _ = @Fun _ ?g _ |- _ =>
      ded (symb_eq H); try ((subst g || subst f); ded (fun_eq H); clear H)
  end.