# 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.