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

Require Import LogicUtil.
Require Export ATerm.
Require Import NaryFunction.
Require Import VecUtil.
Require Import Arith.
Require Import List.
Require Import VecMax.

Section S.

Variable Sig : Signature.

Notation term := (term Sig). Notation terms := (Vector.t term).

interpretation of symbols

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

Variable I : interpretation.

Notation D := (domain I).

valuations

Definition valuation := variableD.

Fixpoint vec_of_val (xint : valuation) (n : nat) : Vector.t D n :=
match n as n0 return Vector.t _ n0 with
| OVector.nil
| S pVadd (vec_of_val xint p) (xint p)
end.

Lemma vec_of_val_eq : xint n x (H : lt x n),
Vnth (vec_of_val xint n) H = xint x.

Proof.
intros xint n. elim n.
intros x Hx. elimtype False. apply (lt_n_O _ Hx).
intros p Hrec x H0. simpl vec_of_val.
case (le_lt_eq_dec _ _ (le_S_n _ _ H0)); intro H1.
rewrite (Vnth_addl (vec_of_val xint p) (xint p) H0 H1). apply Hrec.
rewrite Vnth_addr. 2: assumption. rewrite H1. refl.
Qed.

Definition val_of_vec n (v : Vector.t D n) : valuation :=
fun xmatch le_lt_dec n x with
| left _some_elt I
| right hVnth v h
end.

Definition fval (xint : valuation) n := val_of_vec (vec_of_val xint n).

Definition restrict (xint : valuation) (n : nat) : valuation :=
fun xmatch le_lt_dec n x with
| left _some_elt I
| right hxint x
end.

interpretation of terms

Section term_int.

Variable xint : valuation.

Fixpoint term_int (t : term) : D :=
match t with
| Var xxint x
| Fun f ts
let fix terms_int n (ts : terms n) {struct ts} : Vector.t D n :=
match ts in Vector.t _ n return Vector.t D n with
| Vector.nilVector.nil
| Vector.cons t' n' ts'Vector.cons (term_int t') (terms_int n' ts')
end
in fint I f (terms_int (arity f) ts)
end.

Lemma term_int_fun : f ts,
term_int (Fun f ts) = fint I f (Vmap term_int ts).

Proof.
intros. simpl. apply (f_equal (fint I f)). induction ts. auto.
rewrite IHts. auto.
Qed.

End term_int.

Lemma term_int_eq : xint1 xint2 t,
( x, In x (vars t) → xint1 x = xint2 x) →
term_int xint1 t = term_int xint2 t.

Proof.
intros xint1 xint2 t. pattern t; apply term_ind_forall; clear t; intros.
simpl. apply H. simpl. intuition.
repeat rewrite term_int_fun. apply (f_equal (fint I f)). apply Vmap_eq.
apply Vforall_intro. intros. apply (Vforall_in H H1). intros. apply H0.
rewrite vars_fun. apply (vars_vec_in H2 H1).
Qed.

Lemma term_int_eq_restrict_lt : xint t k,
maxvar t < kterm_int xint t = term_int (restrict xint k) t.

Proof.
intros xint t. pattern t; apply term_ind_forall; clear t; intros.
simpl. unfold restrict. case (le_lt_dec k v); intro.
simpl in H. absurd (v<k); omega. refl.
repeat rewrite term_int_fun. apply (f_equal (fint I f)).
apply Vmap_eq. apply Vforall_intro. intros. apply (Vforall_in H H1).
rewrite maxvar_fun in H0. ded (Vin_map_intro (maxvar (Sig:=Sig)) H1).
ded (Vmax_in H2). unfold maxvars in H0. omega.
Qed.

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

Proof.
intros. apply term_int_eq_restrict_lt. omega.
Qed.

Lemma term_int_eq_fval_lt : xint t k,
maxvar t < kterm_int xint t = term_int (fval xint k) t.

Proof.
intros xint t. pattern t; apply term_ind_forall; clear t; intros.
simpl in ×. unfold fval, val_of_vec. case (le_lt_dec k v); intro.
absurd (v<k); omega. symmetry. apply vec_of_val_eq.
repeat rewrite term_int_fun. apply (f_equal (fint I f)).
apply Vmap_eq. apply Vforall_intro. intros. apply (Vforall_in H H1).
rewrite maxvar_fun in H0. ded (Vin_map_intro (maxvar (Sig:=Sig)) H1).
ded (Vmax_in H2). unfold maxvars in H0. omega.
Qed.

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

Proof.
intros. apply term_int_eq_fval_lt. omega.
Qed.

End S.

Implicit Arguments mkInterpretation [Sig domain].