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

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

Variable I : interpretation.

Notation D := (domain I).

Definition valuation := variable → D.

Fixpoint vec_of_val (xint : valuation) (n : nat) : Vector.t D n :=
  match n as n0 return Vector.t _ n0 with
    | O ⇒ Vector.nil
    | S p ⇒ Vadd (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 x ⇒ match le_lt_dec n x with
    | left _ ⇒ some_elt I
    | right h ⇒ Vnth v h
  end.

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

Definition restrict (xint : valuation) (n : nat) : valuation :=
  fun x ⇒ match le_lt_dec n x with
    | left _ ⇒ some_elt I
    | right h ⇒ xint x
  end.

Section term_int.

Variable xint : valuation.

Fixpoint term_int (t : term) : D :=
  match t with
    | Var x ⇒ xint 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.nil ⇒ Vector.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 < k → term_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 < k → term_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].