# Library CoLoR.Term.WithArity.ABterm

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Sebastien Hinderer, 2004-04-28
• Frederic Blanqui, 2005-01-28
terms whose variable indexes are bounded

Set Implicit Arguments.

Section S.

Variable Sig : Signature.

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

Section bterm.

Variable k : nat.

Inductive bterm : Type :=
| BVar : forall x : nat, x<=k -> bterm
| BFun : forall f : Sig, vector bterm (arity f) -> bterm.

induction principles

Notation bterms := (vector bterm).

Section bterm_rect_def.

Variables
(P : bterm -> Type)
(Q : forall n : nat, bterms n -> Type).

Hypotheses
(H1 : forall x (h : x<=k), P (BVar h))
(H2 : forall (f : Sig) (v : bterms (arity f)), Q v -> P (BFun f v))
(H3 : Q Vnil)
(H4 : forall (t : bterm) n (v : bterms n), P t -> Q v -> Q (Vcons t v)).

Fixpoint bterm_rect (t : bterm) : P t :=
match t as t return P t with
| BVar h => H1 h
| BFun f v =>
let fix bterms_rect n (v : bterms n) : Q v :=
match v as v return Q v with
| Vnil => H3
| Vcons t' v' => H4 (bterm_rect t') (bterms_rect _ v')
end
in H2 f (bterms_rect (arity f) v)
end.

End bterm_rect_def.

Definition bterm_ind (P : bterm -> Prop) (Q : forall n, bterms n -> Prop) :=
bterm_rect P Q.

injection of bterm into term

Fixpoint term_of_bterm (bt : bterm) : term :=
match bt with
| @BVar v _ => Var v
| BFun f bts => Fun f (Vmap term_of_bterm bts)
end.

injection of term into bterm

Notation max_le := (maxvar_le k).

Fixpoint inject_term (t : term) : max_le t -> bterm :=
match t as t0 return max_le t0 -> bterm with
| Var x => fun H => BVar (maxvar_var H)
| Fun f ts => fun H =>
let fix inject_terms n (ts : terms n) :
Vforall max_le ts -> bterms n :=
match ts as v in vector _ n0
return Vforall max_le v -> bterms n0 with
| Vnil => fun _ => Vnil
| Vcons t' ts' => fun H =>
Vcons (inject_term (proj1 H)) (inject_terms _ ts' (proj2 H))
end
in BFun f (inject_terms (arity f) ts (maxvar_le_fun H))
end.

Fixpoint inject_terms (n : nat) (ts : terms n) :
Vforall max_le ts -> bterms n :=
match ts as v in vector _ n0
return Vforall max_le v -> bterms n0 with
| Vnil => fun _ => Vnil
| Vcons t' ts' => fun H =>
Vcons (inject_term (proj1 H)) (inject_terms ts' (proj2 H))
end.

Lemma inject_term_eq : forall f ts (H : max_le (Fun f ts)),
inject_term H = BFun f (inject_terms (maxvar_le_fun H)).

Lemma inject_terms_nth : forall i n (ts : terms n) (H : Vforall max_le ts)
(ip : i < n), Vnth (inject_terms H) ip = inject_term (Vforall_nth ip H).

interpretation of bterm's

Variables (I : interpretation Sig) (xint : valuation I).

Notation D := (domain I).
Notation fint := (fint I).

Fixpoint bterm_int (t : bterm) { struct t } : D :=
match t with
| @BVar x _ => xint x
| BFun f v => fint f (Vmap bterm_int v)
end.

End bterm.

relation between bterm_int and term_int

Section term_int.

Variables (I : interpretation Sig) (xint : valuation I).

Notation D := (domain I).

Let P (t : term) := forall (k : nat) (H : maxvar_le k t),
bterm_int xint (inject_term H) = term_int xint t.

Let Q (n1 : nat) (ts : terms n1) :=
forall (k : nat) (H : Vforall (maxvar_le k) ts),
Vmap (bterm_int xint) (inject_terms H) = Vmap (term_int xint) ts.

Lemma term_int_eq_bterm_int : forall t, P t.

End term_int.

Fixpoint bterm_le k (bt : bterm k) l (h0 : k <= l) : bterm l :=
match bt with
| BVar h => BVar (le_trans h h0)
| BFun f bts => BFun f (Vmap (fun bt => @bterm_le k bt l h0) bts)
end.

Fixpoint bterms_le k n (bts : vector (bterm k) n) l (h0 : k <= l)
: vector (bterm l) n :=
match bts in vector _ n return vector (bterm l) n with
| Vnil => Vnil
| Vcons bt bts' => Vcons (bterm_le bt h0) (bterms_le bts' h0)
end.

Definition bterm_plus k bt l := bterm_le bt (le_plus_r k l).

Definition bterms_plus k n (bts : vector (bterm k) n) l
:= bterms_le bts (le_plus_r k l).

End S.