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

Require Export Bvector.
Require Export ASignature.
Require Import ListUtil.
Require Import LogicUtil.
Require Import EqUtil.
Require Import BoolUtil.
Require Import NatUtil.
Require Import Max.

Local Unset Standard Proposition Elimination Names.

Notation variables := (list variable).

Section S.

Variable Sig : Signature.

terms

Require Import VecUtil.

Unset Elimination Schemes.
Inductive term : Type :=
| Var : variable term
| Fun : f : Sig, Vector.t term (arity f) term.
Set Elimination Scheme.

Notation terms := (Vector.t term).

induction principles

Section term_rect.

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

Hypotheses
(H1 : x, P (Var x))
(H2 : f v, Q v P (Fun f v))
(H3 : Q Vector.nil)
(H4 : t n (v : terms n), P t Q v Q (Vector.cons t v)).

Fixpoint term_rect t : P t :=
match t as t return P t with
| Var xH1 x
| Fun f v
let fix terms_rect n (v : terms n) {struct v} : Q v :=
match v as v return Q v with
| Vector.nilH3
| Vector.cons t' n' v'H4 (term_rect t') (terms_rect n' v')
end
in H2 f (terms_rect (arity f) v)
end.

End term_rect.

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

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

Proof.
intros. apply term_ind with (Q := Vforall P). exact H1. exact H2.
exact I. intros. simpl. split; assumption.
Qed.

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

Proof.
intros. apply term_ind
with (Q := fun n (ts : terms n) ⇒ t, Vin t ts P t).
exact H1. exact H2. contradiction. simpl. intuition. subst t1. exact H.
Qed.

equality

Lemma var_eq : x x', x = x' Var x = Var x'.

Proof.
intros. rewrite H. refl.
Qed.

Lemma args_eq : f v v', v = v' Fun f v = Fun f v'.

Proof.
intros. rewrite H. refl.
Qed.

Lemma fun_eq : f v w, Fun f v = Fun f w v = w.

Proof.
intros. inversion H. apply (inj_pairT2 (@eq_symbol_dec _) H1).
Qed.

Lemma symb_eq : f us g vs, Fun f us = Fun g vs f = g.

Proof.
intros. inversion H. refl.
Qed.

decidability of equality

Section beq.

Variable beq_var : variable variable bool.
Variable beq_var_ok : x y, beq_var x y = true x = y.

Variable beq_symb : Sig Sig bool.
Variable beq_symb_ok : f g, beq_symb f g = true f = g.

Fixpoint beq (t u : term) {struct t} :=
match t, u with
| Var x, Var ybeq_var x y
| Fun f ts, Fun g us
let fix beq_terms n (ts : terms n) p (us : terms p) {struct ts} :=
match ts, us with
| Vector.nil, Vector.niltrue
| Vector.cons t _ ts', Vector.cons u _ us'beq t u && beq_terms _ ts' _ us'
| _, _false
end
in beq_symb f g && beq_terms _ ts _ us
| _, _false
end.

Lemma beq_terms : n (ts : terms n) p (us : terms p),
(fix beq_terms n (ts : terms n) p (us : terms p) {struct ts} :=
match ts, us with
| Vector.nil, Vector.niltrue
| Vector.cons t _ ts', Vector.cons u _ us'beq t u && beq_terms _ ts' _ us'
| _, _false
end) _ ts _ us = beq_vec beq ts us.

Proof.
induction ts; destruct us; refl.
Qed.

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

Proof.
intros. rewrite <- beq_terms. refl.
Qed.

Lemma beq_ok : t u, beq t u = true t = u.

Proof.
intro t. pattern t. apply term_ind_forall2; destruct u.
simpl. rewrite beq_var_ok. intuition. inversion H. refl.
intuition; discriminate. intuition; discriminate.
rewrite beq_fun. split; intro. destruct (andb_elim H0).
rewrite beq_symb_ok in H1. subst f0. apply args_eq.
ded (beq_vec_ok_in1 H H2). rewrite <- H1. rewrite Vcast_refl_eq. refl.
inversion H0 as [[h0 h1]]. clear h1. subst f0. simpl.
apply andb_intro. apply (beq_refl beq_symb_ok).
apply beq_vec_ok_in2. exact H. refl.
Qed.

End beq.

Implicit Arguments beq_ok [beq_var beq_symb].

Notation beq_symb := (@beq_symb Sig).
Notation beq_symb_ok := (@beq_symb_ok Sig).

Definition beq_term := beq beq_nat beq_symb.

Lemma beq_term_ok : t u, beq_term t u = true t = u.

Proof.
exact (beq_ok beq_nat_ok beq_symb_ok).
Qed.

Lemma eq_term_dec : t u : term, {t=u}+{¬t=u}.

Proof.
intro. pattern t. apply term_rect with
(Q := fun n (ts : terms n) ⇒ u, {ts=u}+{¬ts=u}); clear t.
intros. destruct u. case (eq_nat_dec x n); intro. subst n. auto.
right. unfold not. intro. injection H. auto.
right. unfold not. intro. discriminate.
intros f ts H u. destruct u. right. unfold not. intro. discriminate.
case (eq_symbol_dec f f0); intro. subst f0. case (H t); intro. subst ts. auto.
right. intro. injection H0. intro. assert (ts=t).
Require Import Eqdep.
apply (inj_pair2 Sig (fun fterms (arity f))). hyp. auto.
right. unfold not. intro. injection H0. intros. auto.
intro. VOtac. auto.
intros. VSntac u. case (X (Vector.hd u)); intro. rewrite e.
case (X0 (Vector.tl u)); intro. rewrite e0. auto.
right. unfold not. intro. injection H0. intro. assert (v = Vector.tl u).
apply (inj_pair2 nat (fun nterms n)). assumption. auto.
right. unfold not. intro. injection H0. intros. auto.
Defined.

maximal variable index in a term

Require Import VecMax.

Fixpoint maxvar (t : term) : nat :=
match t with
| Var xx
| Fun f v
let fix maxvars (n : nat) (v : terms n) {struct v} : nats n :=
match v in Vector.t _ n return nats n with
| Vector.nilVector.nil
| Vector.cons t' n' v'Vector.cons (maxvar t') (maxvars n' v')
end
in Vmax (maxvars (arity f) v)
end.

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

Lemma maxvars_cons : t n (ts : terms n),
maxvars (Vector.cons t ts) = max (maxvar t) (maxvars ts).

Proof.
refl.
Qed.

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

Proof.
intros. simpl. apply (f_equal (@Vmax (arity f))).
induction ts. auto. rewrite IHts. auto.
Qed.

Lemma maxvar_var : k x, maxvar (Var x) k x k.

Proof.
intros. simpl. intuition.
Qed.

Definition maxvar_le k t := maxvar t k.

Lemma maxvar_le_fun : m f ts,
maxvar (Fun f ts) m Vforall (maxvar_le m) ts.

Proof.
intros until ts. rewrite maxvar_fun. intro. generalize (Vmax_forall H).
clear H. intro H. generalize (Vforall_map_elim H). intuition.
Qed.

Lemma maxvar_le_arg : f ts m t,
maxvar (Fun f ts) m Vin t ts maxvar t m.

Proof.
intros. assert (Vforall (maxvar_le m) ts). apply maxvar_le_fun. assumption.
change (maxvar_le m t). eapply Vforall_in with (n := arity f). apply H1.
assumption.
Qed.

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 xx :: nil
| Fun f v
let fix vars_vec n (ts : terms n) {struct ts} : variables :=
match ts with
| Vector.nilnil
| Vector.cons t' n' ts'vars t' ++ vars_vec n' ts'
end
in vars_vec (arity f) v
end.

Fixpoint vars_vec n (ts : terms n) {struct ts} : variables :=
match ts with
| Vector.nilnil
| Vector.cons t' _ ts'vars t' ++ vars_vec ts'
end.

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

Proof.
auto.
Qed.

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

Proof.
induction ts; intros; destruct m; simpl; try (refl || discriminate).
apply (f_equal (fun lvars h ++ l)). apply IHts.
Qed.

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

Proof.
induction ts1; intros; simpl. refl. rewrite app_ass.
apply (f_equal (fun lvars h ++ l)). apply IHts1.
Qed.

Lemma vars_vec_cons : t n (ts : terms n),
vars_vec (Vector.cons t ts) = vars t ++ vars_vec ts.

Proof.
intros. refl.
Qed.

Lemma in_vars_vec_elim : x n (ts : terms n),
In x (vars_vec ts) t, Vin t ts In x (vars t).

Proof.
induction ts; simpl; intros. contradiction. generalize (in_app_or H). intro.
destruct H0. h. intuition. generalize (IHts H0). intro.
destruct H1 as [t].
t. intuition.
Qed.

Lemma in_vars_vec_intro : x t n (ts : terms n),
In x (vars t) Vin t ts In x (vars_vec ts).

Proof.
intros. ded (Vin_elim H0). do 5 destruct H1. subst ts.
rewrite vars_vec_cast. rewrite vars_vec_app. simpl.
apply in_appr. apply in_appl. exact H.
Qed.

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

Proof.
induction ts; simpl; intros. contradiction. destruct H0. subst t.
apply in_appl. assumption. apply in_appr. apply IHts; assumption.
Qed.

Lemma vars_max : x t, In x (vars t) x maxvar t.

Proof.
intros x t. pattern t. apply term_ind with (Q := fun n (ts : terms n) ⇒
In x (vars_vec ts) x maxvars ts); clear t; intros.
simpl in ×. intuition. rewrite maxvar_fun. rewrite vars_fun in H0. auto.
destruct (in_app_or H1); unfold maxvars; simpl. apply le_max_intro_l. auto.
apply le_max_intro_r. auto.
Qed.

Lemma maxvar_in : x t n (v : terms n),
x maxvar t Vin t v x maxvars v.

Proof.
induction v; unfold maxvars; simpl; intros. contradiction. destruct H0.
subst t. apply le_max_intro_l. hyp. apply le_max_intro_r. apply IHv; hyp.
Qed.

Require Import ListMax.

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

Proof.
intro t. pattern t.
set (Q := fun n (ts : terms n) ⇒ maxvars ts = lmax (vars_vec ts)).
apply term_ind with (Q := Q); clear t.
intro. simpl. apply (sym_equal (max_l (le_O_n x))).
intros f ts H. rewrite maxvar_fun. rewrite vars_fun. assumption.
unfold Q. auto.
intros t n ts H1 H2. unfold Q. simpl. rewrite lmax_app.
unfold Q in H2. rewrite maxvars_cons. rewrite H1. rewrite H2. refl.
Qed.

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 ybeq_nat x y
| Fun f ts
let fix var_occurs_in_terms n (ts : terms n) :=
match ts with
| Vector.nilfalse
| Vector.cons t _ ts'var_occurs_in t || var_occurs_in_terms _ ts'
end
in var_occurs_in_terms _ ts
end.

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) {struct ts} :=
match ts with
| Vector.nil ⇒ 0
| Vector.cons u p usnb_symb_occs u + nb_symb_occs_terms p us
end
in 1 + nb_symb_occs_terms _ ts
end.

Fixpoint nb_symb_occs_terms n (ts : terms n) {struct ts} :=
match ts with
| Vector.nil ⇒ 0
| Vector.cons u p usnb_symb_occs u + nb_symb_occs_terms us
end.

Lemma nb_symb_occs_fix : n (ts : terms n),
(fix nb_symb_occs_terms n (ts : terms n) {struct ts} :=
match ts with
| Vector.nil ⇒ 0
| Vector.cons u p usnb_symb_occs u + nb_symb_occs_terms p us
end) _ ts = nb_symb_occs_terms ts.

Proof.
induction ts; simpl; intros. refl. rewrite IHts. refl.
Qed.

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

Proof.
intros. simpl. rewrite nb_symb_occs_fix. refl.
Qed.

Lemma Vin_nb_symb_occs_terms_ge : n (ts : terms n) t,
Vin t ts nb_symb_occs_terms ts nb_symb_occs t.

Proof.
induction ts; simpl; intros. contradiction. destruct H. subst h. omega.
ded (IHts _ H). omega.
Qed.

size of a term

Fixpoint size t :=
match t with
| Var x ⇒ 1
| Fun f ts
let fix size_terms n (ts : terms n) {struct ts} :=
match ts with
| Vector.nil ⇒ 0
| Vector.cons u p ussize u + size_terms p us
end
in 1 + size_terms _ ts
end.

Fixpoint size_terms n (ts : terms n) {struct ts} :=
match ts with
| Vector.nil ⇒ 0
| Vector.cons u _ ussize u + size_terms us
end.

Lemma size_fix : n (ts : terms n),
(fix size_terms n (ts : terms n) {struct ts} :=
match ts with
| Vector.nil ⇒ 0
| Vector.cons u p ussize u + size_terms p us
end) _ ts = size_terms ts.

Proof.
induction ts; simpl; intros. refl. rewrite IHts. refl.
Qed.

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

Proof.
intros. simpl. rewrite size_fix. refl.
Qed.

Lemma size_non_zero : t, size t > 0.

Proof.
intro. pattern t. apply term_ind with (Q := fun n (ts : terms n) ⇒
size_terms ts 0); clear t.
intro. simpl. omega.
intros. rewrite size_fun. omega.
simpl. omega.
intros. simpl. omega.
Qed.

Lemma Vin_size_terms_ge : n (ts : terms n) t,
Vin t ts size_terms ts size t.

Proof.
induction ts; simpl; intros. contradiction. destruct H. subst h. omega.
ded (IHts _ H). omega.
Qed.

Implicit Arguments Vin_size_terms_ge [n ts t].

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

Proof.
destruct ts. intros; omega.
destruct ts. intros; omega.
simpl. intros.

ded (size_non_zero h). ded (size_non_zero h0).
destruct H. subst t. omega. destruct H. subst t. omega.
ded (Vin_size_terms_ge H). omega.
Qed.

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

Proof.
induction ts. intro. destruct m. intro. castrefl h. intro. discriminate.
intro. destruct m. intro. discriminate. intro. inversion h0. simpl. rewrite IHts.
refl.
Qed.

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

Proof.
induction ts; simpl; intros. refl. rewrite IHts. omega.
Qed.

direct subterms of a term

Definition direct_subterms (t : term) : list term :=
match t with
| Var xnil
| Fun f fslist_of_vec fs
end.

End S.

implicit arguments

Implicit Arguments Var [Sig].
Implicit Arguments maxvar_var [Sig k x].
Implicit Arguments maxvar_le_fun [Sig m f ts].
Implicit Arguments maxvar_le_arg [Sig f ts m t].
Implicit Arguments in_vars_vec_elim [Sig x n ts].
Implicit Arguments in_vars_vec_intro [Sig x t n ts].
Implicit Arguments vars_vec_in [Sig x t n ts].
Implicit Arguments vars_max [Sig x t].
Implicit Arguments Vin_nb_symb_occs_terms_ge [Sig n ts t].
Implicit Arguments Vin_size_terms_ge [Sig n ts t].
Implicit Arguments Vin_size_terms_gt [Sig n ts t].

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.