# Library CoLoR.Term.WithArity.AInterpretation

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Sebastien Hinderer, 2004-02-09
interpretation of algebraic terms with arity

Set Implicit Arguments.

Section S.

Variable Sig : Signature.

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

interpretation of symbols

Record interpretation : Type := mkInterpretation {
domain :> Type;
some_elt : domain;
fint : forall f : Sig, naryFunction1 domain (arity f)
}.

Variable I : interpretation.

valuations

Definition valuation := variable -> domain I.

Definition val_of_vec n (v : vector I n) : valuation := fun x =>
match le_lt_dec n x with
| left _ => some_elt I
| right h => Vnth v h
end.

Fixpoint val_of_vec2 n (v : vector I n) : valuation := fun x =>
match x, v with
| _, Vnil => some_elt I
| 0, Vcons a _ => a
| S x', Vcons _ v' => val_of_vec2 v' x'
end.

Lemma val_of_vec_eq : forall n (v : vector I n) x (h : x < n),
val_of_vec v x = Vnth v h.

Section vec_of_val.

Variable xint : valuation.

Definition restrict n : valuation := fun x =>
match le_lt_dec n x with
| left _ => some_elt I
| right _ => xint x
end.

Fixpoint vec_of_val (n : nat) : vector I n :=
match n as n return vector _ n with
| O => Vnil
| S n' => Vadd (vec_of_val n') (xint n')
end.

Lemma Vnth_vec_of_val : forall n x (H : x < n),
Vnth (vec_of_val n) H = xint x.

Definition fval n := val_of_vec (vec_of_val n).

End vec_of_val.

interpretation of terms

Section term_int.

Variable xint : valuation.

Fixpoint term_int t :=
match t with
| Var x => xint x
| Fun f ts => fint I f (Vmap term_int ts)
end.

End term_int.

Lemma term_int_eq : forall xint1 xint2 t,
(forall x, In x (vars t) -> xint1 x = xint2 x) ->
term_int xint1 t = term_int xint2 t.

Lemma term_int_eq_restrict_lt : forall xint t k,
maxvar t < k -> term_int xint t = term_int (restrict xint k) t.

Lemma term_int_eq_restrict : forall xint t,
term_int xint t = term_int (restrict xint (maxvar t + 1)) t.

Lemma term_int_eq_fval_lt : forall xint t k,
maxvar t < k -> term_int xint t = term_int (fval xint k) t.

Lemma term_int_eq_fval : forall xint t,
term_int xint t = term_int (fval xint (maxvar t + 1)) t.

Lemma Vmap_term_int_fval : forall v n k (ts : terms k),
n > maxvars ts -> Vmap (term_int (fval v n)) ts = Vmap (term_int v) ts.

End S.