Library CoLoR.Term.WithArity.ABterm

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.

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.

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.

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

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.

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.