(* Higher Order Universal Algebra     *)
(* Venanzio Capretta and Amy Felty    *)
(* September 2006, Coq version 8.0pl3 *)

Require Export Arith.
Require Export Max.
Require Export Streams.
Require Export List.
Require Export Bool.
Require Export Sumbool.

Set Implicit Arguments.

(* Definition of Higher-Order Signatures *)

Section Signature_Definition.

Variables sort operation: Set.

Record arg_type: Set := arg_sequent {
  arg_bindings: list sort;
  arg_result: sort
}.

Record operation_type: Set := op_rule {
  op_arguments: list arg_type;
  op_result: sort
}.

Definition arg_list_sorts (al:list arg_type): list sort :=
  map arg_result al.

Definition op_arg_sorts (ot:operation_type): list sort :=
  arg_list_sorts (op_arguments ot).

(* Sort-Dependent Lists *)

Variable F: sort -> Set.

Inductive sort_list: list sort -> Set :=
  sort_nil: sort_list nil
| sort_cons: forall (A:sort)(As:list sort),
               F A -> sort_list As -> sort_list (A::As).

Definition sl_head_type (As:list sort): Set :=
match As with
  nil => unit
| cons A As => F A
end.

Definition sl_head_aux (As:list sort)(al:sort_list As): sl_head_type As :=
match al in (sort_list As) return (sl_head_type As) with
  sort_nil => tt
| sort_cons A As a al => a
end.

Definition sl_head (A:sort)(As:list sort): sort_list (A::As) -> F A :=
  fun al => sl_head_aux al.

Definition sl_tail_type (As:list sort): Set :=
match As with
  nil => unit
| cons A As => sort_list As
end.

Definition sl_tail_aux (As:list sort)(al:sort_list As): sl_tail_type As :=
match al in (sort_list As) return (sl_tail_type As) with
  sort_nil => tt
| sort_cons A As a al => al
end.

Definition sl_tail (A:sort)(As:list sort): sort_list (A::As) -> sort_list As :=
  fun al => sl_tail_aux al.

Definition sl_decomposition (As:list sort): sort_list As -> sort_list As :=
match As return sort_list As -> sort_list As with
  nil => fun l => sort_nil
| cons A As => fun l => sort_cons (sl_head l) (sl_tail l)
end.

Lemma sl_decomposition_id:
  forall (As:list sort)(al:sort_list As), al = sl_decomposition al.
Proof.
induction al; trivial.
Qed.

Lemma sl_nil_id:
  forall (al:sort_list nil), al = sort_nil.
Proof.
intro al; rewrite sl_decomposition_id with (al:=al); auto.
Qed.

Lemma sl_head_tail_id:
  forall (A:sort)(As:list sort)(al:sort_list (A::As)),
    al = sort_cons (sl_head al) (sl_tail al).
Proof.
intros A As al.
apply sl_decomposition_id with (al:=al).
Qed.

Fixpoint sl_and (P:forall A:sort, F A -> Prop)(As:list sort){struct As}:
                       sort_list As -> Prop :=
match As return (sort_list As -> Prop) with
  nil => fun _ => True
| cons A As => fun al => (P A (sl_head al)) /\ (sl_and P (sl_tail al))
end.

Definition arg_map: arg_type -> Set :=
  fun T => sort_list (arg_bindings T) -> F (arg_result T).

(* Curried version of arg_map. *)

Fixpoint at_curry_aux (As:list sort): sort -> Set :=
match As with
  nil => fun B => F B
| cons A As => fun B => F A -> at_curry_aux As B
end.

Definition at_curry: arg_type -> Set :=
  fun T => at_curry_aux (arg_bindings T) (arg_result T).

Fixpoint uncurry_at_aux (As:list sort)(B:sort)(al:sort_list As){struct al}:
  (at_curry_aux As B) -> F B :=
match al in (sort_list As) return (at_curry_aux As B) -> F B with
  sort_nil => fun c => c
| sort_cons A As a al => fun g => uncurry_at_aux B al (g a)
end.

Definition uncurry_arg_type: forall T:arg_type, at_curry T -> arg_map T :=
  fun T g al => uncurry_at_aux (arg_result T) al g.

(* lists of function arguments. *)
Inductive args_map: list arg_type -> Set :=
  meta_nil: args_map nil
| meta_cons: forall (T:arg_type)(Ts:list arg_type),
               arg_map T -> args_map Ts -> args_map (T::Ts).

Definition am_split_type (Ts:list arg_type): Set :=
match Ts with
  nil => unit
| cons T Ts => prod (arg_map T) (args_map Ts)
end.

Definition am_split (Ts:list arg_type)(hs:args_map Ts):
  am_split_type Ts :=
match hs in (args_map Ts) return am_split_type Ts with
  meta_nil => tt
| meta_cons T Ts h hs => (h,hs)
end.

Definition am_head (T:arg_type)(Ts:list arg_type)(hs:args_map (T::Ts)):
  arg_map T := fst (am_split hs).

Definition am_tail (T:arg_type)(Ts:list arg_type)(hs:args_map (T::Ts)):
  args_map Ts := snd (am_split hs).

Definition am_join (Ts:list arg_type): am_split_type Ts -> args_map Ts :=
match Ts return am_split_type Ts -> args_map Ts with
  nil => fun _ => meta_nil
| cons T Ts => fun p => meta_cons (fst p) (snd p)
end.

Lemma am_split_id:
  forall (Ts: list arg_type)(hs: args_map Ts),
    hs = am_join Ts (am_split hs).
Proof.
intros Ts hs; case hs; trivial.
Qed.

Lemma am_nil_id:
  forall (hs:args_map nil), hs = meta_nil.
Proof.
intro hs; simpl.
rewrite am_split_id with (hs:=hs).
trivial.
Qed.

Lemma am_head_tail_id:
  forall (T:arg_type)(Ts:list arg_type)(hs:args_map (T::Ts)),
    hs = meta_cons (am_head hs) (am_tail hs).
Proof.
intros T Ts hs; simpl.
change (hs = am_join (T::Ts) (am_split hs)).
apply am_split_id.
Qed.

Fixpoint am_ext_eq (Ts:list arg_type){struct Ts}:
  args_map Ts -> args_map Ts -> Prop :=
match Ts return args_map Ts -> args_map Ts -> Prop with
  nil => fun _ _ => True
| cons T Ts => fun hs1 hs2 => 
               (forall al:sort_list (arg_bindings T),
                  am_head hs1 al = am_head hs2 al) /\
               (am_ext_eq (am_tail hs1) (am_tail hs2))
end.

(* Higher-Order operations on F. *)

Definition ho_op_aux (Ts:list arg_type)(C:sort): Set :=
  args_map Ts -> F C.

Definition ho_op (ot:operation_type): Set :=
  ho_op_aux (op_arguments ot) (op_result ot).

(* Curried form. *)

Fixpoint ho_curry_aux (Ts:list arg_type): sort -> Set :=
match Ts with
  nil => F
| cons T Ts => fun C => at_curry T -> ho_curry_aux Ts C
end.

Definition ho_curry (ot:operation_type): Set :=
  ho_curry_aux (op_arguments ot) (op_result ot).

(* Partial application *)
Definition partial_app (T:arg_type)(Ts:list arg_type)(C:sort):
  arg_map T -> ho_op_aux (T::Ts) C -> ho_op_aux Ts C :=
fun a g al => g (meta_cons a al).

Fixpoint curry_ho_aux (Ts:list arg_type)(C:sort){struct Ts}:
  ho_op_aux Ts C -> ho_curry_aux Ts C :=
match Ts return ho_op_aux Ts C -> ho_curry_aux Ts C with
  nil => fun g => g meta_nil
| cons T Ts => fun g a => curry_ho_aux (partial_app (uncurry_arg_type T a) g)
end.

Definition curry_ho (ot:operation_type): ho_op ot -> ho_curry ot :=
  curry_ho_aux (Ts:=op_arguments ot) (C:=op_result ot).

End Signature_Definition.

Unset Implicit Arguments.

Notation "[]" := (nil) : hoas_scope.
Notation "[ x ]" := (cons x nil) : hoas_scope.
Notation "[ x , .. , y ]" := (cons x .. (cons y nil) ..) : hoas_scope.

Notation "A '|--' B" := (arg_sequent A B) (at level 31) : hoas_scope.
Notation "A '//' B" := (op_rule A B) (at level 33) : hoas_scope.

Record Signature: Type := signature {
  sig_sort: Set;
  sig_dec: forall s1 s2:sig_sort, {s1=s2}+{s1<>s2};
  sig_operation: Set;
  sig_rule: sig_operation -> operation_type sig_sort
}.

Section Higher_Order_Universal_Algebra.

Open Scope hoas_scope.

Variable sign: Signature.

Let sort := sig_sort sign.
Let sort_dec := sig_dec sign.
Let operation := sig_operation sign.
Let rule := sig_rule sign.

Inductive Term: sort -> Set :=
  var: forall A:sort, nat -> Term A
| bnd: forall A:sort, nat -> Term A
| opr: forall f:operation,
         TermList (op_arguments (rule f)) -> Term (op_result (rule f))
with TermList: list (arg_type sort) -> Set :=
  nil_term: TermList nil
| cons_term: forall (T:arg_type sort)(Ts:list (arg_type sort)),
               Term (arg_result T) -> TermList Ts -> TermList (T::Ts).

(* Mutual Induction Principle for Term and TermList *)
Section Term_TermList_Induction.

Variables 
  (P: forall A:sort, Term A -> Prop)
  (Ps: forall Ts:list (arg_type sort), TermList Ts -> Prop).

Hypotheses
  (Pvar: forall A i, P A (var A i))
  (Pbnd: forall A i, P A (bnd A i))
  (Popr: forall f ts, Ps _ ts -> P _ (opr f ts))
  (Psnil: Ps nil nil_term)
  (Pscons: forall T Ts t ts, P _ t -> Ps _ ts -> Ps (T::Ts) (cons_term _ _ t ts)).

Fixpoint Term_mutual_ind (A:sort)(t:Term A){struct t}: P A t :=
match t in Term A return P A t with
  var A i => Pvar A i
| bnd A i => Pbnd A i
| opr f ts => Popr f ts (TermList_mutual_ind _ ts)
end
with TermList_mutual_ind (Ts:list (arg_type sort))
                         (ts:TermList Ts){struct ts}: Ps Ts ts := 
match ts in TermList Ts return Ps Ts ts with
  nil_term => Psnil
| cons_term T Ts t ts =>
    Pscons T Ts t ts (Term_mutual_ind _ t) (TermList_mutual_ind _ ts)
end.

Theorem Term_TermList_ind:
  (forall A t, P A t) /\ (forall Ts ts, Ps Ts ts).
Proof.
split; [exact Term_mutual_ind | exact TermList_mutual_ind].
Qed.

Theorem Term_mututal_ind: forall A t, P A t.
Proof.
exact (proj1 Term_TermList_ind).
Qed.

End Term_TermList_Induction.

(* (newvar A' A t) gives the first variable of sort A' that is free in t *)
Fixpoint newvar (A' A:sort)(t:Term A){struct t}: nat :=
match t with
  var A'' i => if (sort_dec A'' A') then S i else 0
| bnd A'' i => 0
| opr f args => newvar_list A' (op_arguments (rule f)) args
end
with newvar_list (A':sort)(Ts:list (arg_type sort))(ts:TermList Ts){struct ts}: nat :=
match ts with
  nil_term => 0
| cons_term T Ts t ts => max (newvar A' (arg_result T) t) (newvar_list A' Ts ts)
end.

(* Increment of the binding index when going under an abstraction:
   As is the list of sorts of the bound variables *)
Fixpoint bind_inc (As:list sort)(A':sort)(j:nat){struct As}: nat :=
match As with
  nil => j
| cons A As => if (sort_dec A A') then S (bind_inc As A' j)
                                  else (bind_inc As A' j)
end.

(* (var_swap A' i j A t) swaps
     the free variable (var A' i) and
     the bound  variable (bnd A' j) in the term t
*)
Fixpoint var_swap (A':sort)(i j:nat)(A:sort)(t:Term A){struct t}: Term A:=
match t in (Term A) return (Term A) with
  var A'' i' => if (sort_dec A'' A')
                then if (eq_nat_dec i' i) then (bnd A'' j) else (var A'' i')
                else (var A'' i')
| bnd A'' j' => if (sort_dec A'' A')
                then if (eq_nat_dec j' j) then (var A'' i) else (bnd A'' j')
                else (bnd A'' j')
| opr f args => opr f (var_swap_list A' i j (op_arguments (rule f)) args)
end
with var_swap_list (A':sort)(i j:nat)(Ts:list (arg_type sort))
                   (ts:TermList Ts){struct ts}: TermList Ts :=
match ts in (TermList Ts) return (TermList Ts) with
  nil_term => nil_term
| cons_term T Ts t ts =>
    cons_term T Ts (var_swap A' i (bind_inc (arg_bindings T) A' j)
                             (arg_result T) t
                   )
                   (var_swap_list A' i j Ts ts)
end.

(* Binding of Metavariables *)

Definition one_arg_bind (A B:sort)(Cs:list sort):
  (Term A -> Term B) -> Term B :=
fun g => let i := newvar A B (g (bnd A 0)) in
         let j := bind_inc Cs A 0 in
         var_swap A i j B (g (var A i)).

Definition indices : list sort -> Set 
  := sort_list (sort:=sort) (fun _ => nat).

(* Incrementing the indices of a list of variables *)
Fixpoint bind_incs (Bs As:list sort){struct As}: indices As -> indices As :=
match As return indices As -> indices As with
  nil => fun xs => xs
| cons A As => fun xs => sort_cons (F:=fun _ => nat) A (bind_inc Bs A (sl_head xs)) (bind_incs Bs As (sl_tail xs))
end.

(* (swapvar A' i As vs xs)
   checks if (var A' i) is one of the variables in vs;
   in that case it returns the corresponding variable in xs,
   otherwise it returns (var A' i).

*)
Fixpoint swapvar (A':sort)(i:nat)(As:list sort){struct As}:
  indices As -> indices As -> Term A' :=
match As return indices As -> indices As -> Term A' with
  nil => fun _ _ => (var A' i)
| cons A As => fun vs xs =>
                 if (sort_dec A' A)
                 then if (eq_nat_dec i (sl_head vs))
                      then (bnd A' (sl_head xs))
                      else (swapvar A' i As (sl_tail vs) (sl_tail xs))
                 else (swapvar A' i As (sl_tail vs) (sl_tail xs))
end.

(* Similarly for bound variables. *)
Fixpoint swapbnd (A':sort)(i:nat)(As:list sort){struct As}:
  indices As -> indices As -> Term A' :=
match As return indices As -> indices As -> Term A' with
  nil => fun _ _ => (bnd A' i)
| cons A As => fun vs xs =>
                 if (sort_dec A' A)
                 then if (eq_nat_dec i (sl_head xs))
                      then (bnd A' (sl_head vs))
                      else (swapbnd A' i As (sl_tail vs) (sl_tail xs))
                 else (swapbnd A' i As (sl_tail vs) (sl_tail xs))
end.

(* Swapping of several variables 
   (vars_swap As vs xs A t) where
       vs:indices As are free variabless 
       xs:indices As are deBruijn variabless
    simultaneously swaps vs and xs in t
*)
Fixpoint vars_swap (As:list sort)(vs xs:indices As)(A:sort)(t:Term A){struct t}: Term A:=
match t in (Term A) return (Term A) with
  var A' i => swapvar A' i As vs xs
| bnd A' j => swapbnd A' j As vs xs
| opr f args => opr f (vars_swap_list As vs xs (op_arguments (rule f)) args)
end
with vars_swap_list (As:list sort)(vs xs:indices As)(Ts:list (arg_type sort))
                    (ts:TermList Ts){struct ts}: TermList Ts :=
match ts in (TermList Ts) return (TermList Ts) with
  nil_term => nil_term
| cons_term T Ts t ts =>
    cons_term T Ts (vars_swap As vs (bind_incs (arg_bindings T) As xs)
                              (arg_result T) t
                   )
                   (vars_swap_list As vs xs Ts ts)
end.

Lemma vars_swap_nil:
  forall A t, vars_swap nil (sort_nil _) (sort_nil _) A t = t.
Proof.
intros A t.
apply Term_mutual_ind with
  (P:= fun A t =>  vars_swap nil (sort_nil _) (sort_nil _) A t = t)
  (Ps:= fun Ts ts => vars_swap_list nil (sort_nil _) (sort_nil _) Ts ts = ts);
 clear t; clear A; simpl.
trivial.
trivial.
intros f ts IH; rewrite IH; trivial.
trivial.
intros T Ts t ts IHt IHts.
  rewrite IHt; rewrite IHts; trivial.
Qed.

(* List of bound variables *)
Fixpoint bind_vars (As:list sort){struct As}: indices As :=
match As return indices As with
  nil => sort_nil (fun _ => nat)
| cons A As => sort_cons (F:=fun _ => nat) A (bind_inc As A 0) (bind_vars As)
end.

(* Turning a list of indices into a list of variable terms. *)
Fixpoint vars (As:list sort)(is:indices As){struct is}: sort_list Term As :=
match is in (sort_list _ As) return (sort_list Term As) with
  sort_nil => sort_nil Term
| sort_cons A As i is => sort_cons A (var A i) (vars As is)
end.

(* Similarly for bound variables. *)
Fixpoint bnds (As:list sort)(is:indices As){struct is}: sort_list Term As :=
match is in (sort_list _ As) return (sort_list Term As) with
  sort_nil => sort_nil Term
| sort_cons A As i is => sort_cons A (bnd A i) (bnds As is)
end.

(* Several new variables.
   We use the increment function to differentiate them.
*)
Fixpoint newvars (As:list sort){struct As}: forall A:sort, Term A -> indices As :=
match As return forall A:sort, Term A -> indices As with
  nil => fun _ _ => sort_nil (fun _ => nat)
| cons A' As => fun A t =>
    sort_cons (F:=fun _ => nat)
              A' (bind_inc As A' (newvar A' A t))
              (newvars As A t)
end.

Definition bind_args (As:list sort)(B:sort):
  (sort_list Term As -> Term B) -> Term B :=
fun g => let xs := bind_vars As in
         let vs := newvars As B (g (bnds As xs)) in
         vars_swap As vs xs B (g (vars As vs)).

Lemma bind_args_extensional:
  forall As B g1 g2,
    (forall al, g1 al = g2 al) -> (bind_args As B g1) = (bind_args As B g2).
Proof.
intros As B g1 g2 H; unfold bind_args.
rewrite (H (bnds As (bind_vars As))).
rewrite (H (vars As (newvars As B (g2 (bnds As (bind_vars As)))))).
trivial.
Qed.

Definition meta_arg: arg_type sort -> Set :=
  arg_map Term.

Definition meta_args: list (arg_type sort) -> Set :=
  args_map Term.

(* bind ([A1, .. , Ak] |-- B) (fun x1 .. xk => b) : Term B *)
Definition bind:
  forall T:(arg_type sort), meta_arg T -> Term (arg_result T) :=
fun T => bind_args (arg_bindings T) (arg_result T) .

Lemma bind_extensional:
  forall T h1 h2,
    (forall al:sort_list Term (arg_bindings T), h1 al = h2 al) ->
    bind T h1 = bind T h2.
Proof.
intros T h1 h2 H; unfold bind.
apply bind_args_extensional.
exact H.
Qed.

Lemma bind_no_args_id:
  forall (B:sort)(g:meta_arg ([]|--B)),
    bind ([]|--B) g = g (sort_nil _).
Proof.
intros B g; unfold bind.
unfold bind_args.
simpl.
rewrite vars_swap_nil.
trivial.
Qed.

(* binds ([[A11, .. ,A1k1]|--B1, .. , [An1, .. ,Ankn]|--Bn])
            {fun x11 .. x1k1 => b1 , .. , fun xn1 .. xnkn => bn}
     : TermList [ B1 , .. , Bn ]
*)
Fixpoint binds (Ts: list (arg_type sort))(args: meta_args Ts){struct args}:
  TermList Ts :=
match args in (args_map _ Ts) return TermList Ts with
  meta_nil => nil_term
| (meta_cons T Ts a args) => cons_term _ _ (bind T a) (binds Ts args)
end.


Lemma binds_extensional:
  forall Ts hs1 hs2,
    am_ext_eq hs1 hs2 -> binds Ts hs1 = binds Ts hs2.
Proof.
intros Ts; elim Ts; clear Ts; simpl.
intros; rewrite am_nil_id with (hs:=hs1);
        rewrite am_nil_id with (hs:=hs2); trivial.
intros T Ts IH hs1 hs2 [H1 H2].
rewrite am_head_tail_id with (hs:=hs1);
  rewrite am_head_tail_id with (hs:=hs2); simpl.
rewrite bind_extensional with (h1:= (am_head hs1))(h2:=(am_head hs2)).
rewrite (IH (am_tail hs1) (am_tail hs2)).
trivial.
exact H2.
exact H1.
Qed.

(* Higher order operation *)
Definition Opr:
  forall (f : operation), ho_op Term (rule f)
:= fun f gs => (opr f (binds _ gs)).

(* Curried version of Opr. *)

Definition Opr_curry:
  forall (f:operation), ho_curry Term (rule f)
:= fun f => curry_ho (Opr f).
    




























Lemma Opr_extensional:
  forall f hs1 hs2, am_ext_eq hs1 hs2 -> Opr f hs1 = Opr f hs2.
Proof.
intros f hs1 hs2 H.
unfold Opr; simpl.
rewrite binds_extensional with (hs1:=hs1) (hs2:=hs2); auto.
Qed.

(* (apvalue A' i As xs ts)
   checks if (bnd A' i) is one of the variables in xs;
   in that case it returns the corresponding term in ts,
   otherwise it returns (bnd A' i).

*)
Fixpoint apvalue (A':sort)(i:nat)(As:list sort){struct As}:
  indices As -> sort_list Term As -> Term A' :=
match As return indices As -> sort_list Term As -> Term A' with
  nil => fun _ _ => (bnd A' i)
| cons A As => fun xs ts =>
                 match (sort_dec A A') with
                   left h => if (eq_nat_dec i (sl_head xs))
                             then eq_rec A (fun A => Term A)
                                         (sl_head ts) A' h
                             else (apvalue A' i As (sl_tail xs) (sl_tail ts))
                 | right _ =>  (apvalue A' i As (sl_tail xs) (sl_tail ts))
                 end
end.

(* Simultaneous substitution of several deBruijn variables *)
Fixpoint sub (B:sort)(t:Term B)
             (As:list sort)(xs:indices As)(ts:sort_list Term As)
             {struct t}:Term B :=
match t in Term B return Term B with
  var A i => var A i
| bnd A j => apvalue A j As xs ts
| opr f us => opr f (subs _ us As xs ts)
end
with subs (Ts: list (arg_type sort))(us:TermList Ts)
          (As:list sort)(xs:indices As)(ts:sort_list Term As)
          {struct us}:TermList Ts:=
match us in TermList Ts return TermList Ts with
  nil_term => nil_term
| cons_term T Ts u us =>
    cons_term T Ts (sub _ u As (bind_incs (arg_bindings T) As xs) ts)
                   (subs Ts us As xs ts)
end.

(* meta-application *)
Fixpoint aps (Ts:list (arg_type sort))(ts:TermList Ts){struct ts}:
  meta_args Ts :=
match ts in TermList Ts return meta_args Ts with
  nil_term => meta_nil _
| cons_term T Ts t ts => meta_cons (sub _ t _ (bind_vars (arg_bindings T)))
                                   (aps Ts ts)
end.

(* Normal form for a list of functions. *)
Definition nfun (Ts:list (arg_type sort)): meta_args Ts -> meta_args Ts :=
  fun hs => aps Ts (binds Ts hs).

(* USE OF THE NOTION OF A LIST OF FRESH VARIABLES *)
(* Several lemmas to prove *)

Fixpoint fresh_var (A:sort)(i:nat)(B:sort)(t:Term B){struct t}: Prop :=
match t with
  var A' i' => (A<>A') \/ (i<>i')
| bnd A' j  => True
| opr f ts => fresh_var_list A i _ ts
end
with fresh_var_list (A:sort)(i:nat)(Ts:list (arg_type sort))
                    (ts:TermList Ts){struct ts}: Prop :=
match ts with
  nil_term => True
| cons_term T Ts t ts => (fresh_var A i _ t) /\ (fresh_var_list A i _ ts)
end.

(* when an index is not in a list of indices *)
Fixpoint not_in_vars (A:sort)(i:nat)(As:list sort)
                     (is:indices As){struct is}: Prop :=
match is with
  sort_nil => True
| sort_cons A' As i' is => ((A<>A')\/(i<>i')) /\ (not_in_vars A i As is)
end.

(* when a list of indices doesn't have repetitions *)
Fixpoint independent_indices (As:list sort){struct As}: indices As -> Prop :=
match As return indices As -> Prop with
  nil => fun _ => True
| cons A As => fun is => (independent_indices As (sl_tail is)) /\
                         (not_in_vars A (sl_head is) As (sl_tail is))
end.

(* When a list of variables is fresh for a term *)
Fixpoint fresh_vars (As:list sort)(is:indices As){struct is}:
  forall (B:sort), Term B -> Prop :=
match is with
  sort_nil => fun _ _ => True
| sort_cons A As i is => fun B t => (fresh_var A i B t) /\
                             (not_in_vars A i As is) /\
                             (fresh_vars As is B t)
end.

Fixpoint fresh_vars_list 
  (As:list sort)(is:indices As)
  (Ts:list (arg_type sort))(ts:TermList Ts){struct ts}: Prop :=
match ts with
  nil_term => independent_indices As is
| cons_term T Ts t ts => (fresh_vars As is _ t) /\
                        (fresh_vars_list As is Ts ts)
end.

Lemma bind_inc_S_gt:
  forall (As:list sort)(A:sort)(i:nat),
     bind_inc As A (S i) > i.
Proof.
intros As; elim As; simpl.
intros _ i; apply le_gt_S.
auto.
clear As; intros A As IH A' i.
case (sort_dec A A').
intros _; red.
red.
apply le_S.
apply gt_le_S.
apply IH.
intros _; apply IH.
Qed.

(* Surprisingly, this is not in the Arith library. *)
Lemma gt_neq: forall n m:nat, n>m -> n<>m.
Proof.
intros n m Hgt Heq.
elim (le_not_gt n m).
rewrite Heq; apply le_n.
exact Hgt.
Qed.

Lemma bind_inc_monotone:
  forall (As:list sort)(A':sort)(j1 j2:nat),
    j1 <= j2 -> bind_inc As A' j1 <= bind_inc As A' j2.
Proof.
intros As; elim As; clear As; simpl.
trivial.
intros A As IH A' j1 j2 H.
case (sort_dec A A').
intros _; apply le_n_S; apply IH.
exact H.
intros _; apply IH.
exact H.
Qed.

Lemma fresh_newvar_aux:
forall (A:sort)(As:list sort),
  (forall (B:sort)(t:Term B)(i:nat),
    i >= newvar A B t ->
    fresh_var A (bind_inc As A i) B t) /\
  (forall (Ts:list (arg_type sort))(ts:TermList Ts)(i:nat),
    i >= newvar_list A Ts ts ->
    fresh_var_list A (bind_inc As A i) Ts ts).
Proof.
intros A As.
apply Term_TermList_ind with
  (P  := fun B t => forall i, i >= newvar A B t ->
           fresh_var A (bind_inc As A i) B t)
  (Ps := fun Ts ts => forall i, i >= newvar_list A Ts ts ->
           fresh_var_list A (bind_inc As A i) Ts ts);
simpl.

(* var *)
intros A' i i'; case (sort_dec A' A).
intro Heq; right.
apply gt_neq.
apply le_gt_trans with (m := bind_inc As A (S i)).
apply bind_inc_monotone.
exact H.
apply bind_inc_S_gt.
intro H; left; apply sym_not_eq; exact H.

(* bnd *)
trivial.

(* opr *)
intros f ts IH.
exact IH.

(* nil_term *)
trivial.

(* cons_term *)
intros T Ts t ts IHt IHts i Hi.
split.
apply IHt.
red.
apply le_trans with (max (newvar A (arg_result T) t) (newvar_list A Ts ts)).
apply le_max_l.
exact Hi.
apply IHts.
red.
apply le_trans with (max (newvar A (arg_result T) t) (newvar_list A Ts ts)).
apply le_max_r.
exact Hi.
Qed.

Lemma fresh_newvar:
  forall (A:sort)(As:list sort)(B:sort)(t:Term B),
    fresh_var A (bind_inc As A (newvar A B t)) B t.
Proof.
intros A As; generalize (fresh_newvar_aux A As); intros [H Hs].
intros B t; apply H.
auto.
Qed.

Lemma fresh_newvar_list:
  forall (A:sort)(As:list sort)(Ts:list (arg_type sort))(ts:TermList Ts),
    fresh_var_list A (bind_inc As A (newvar_list A Ts ts)) Ts ts.
Proof.
intros A As; generalize (fresh_newvar_aux A As); intros [H Hs].
intros Ts ts; apply Hs.
auto.
Qed.

Lemma distinct_newvars_aux:
  forall (A:sort)(As:list sort)(B:sort)(t:Term B)(i:nat),
    i >= (bind_inc As A (newvar A B t)) ->
    not_in_vars A i As (newvars As B t).
Proof.
intros A As; elim As; clear As; simpl.
trivial.
intros A' As IH B t i; case (sort_dec A' A); intros H Hi; split.

right; rewrite H.
apply gt_neq.
red.
red.
exact Hi.

apply IH.
red.
apply le_trans with (S (bind_inc As A (newvar A B t))).
apply le_S; apply le_n.
exact Hi.

left; apply sym_not_eq; exact H.

apply IH.
exact Hi.
Qed.

Lemma distinct_newvars:
  forall (A:sort)(As:list sort)(B:sort)(t:Term B),
    not_in_vars A (bind_inc As A (newvar A B t)) As (newvars As B t).
Proof.
intros A As B t.
apply distinct_newvars_aux with (i:=(bind_inc As A (newvar A B t))).
auto.
Qed.

(* new variables are always fresh *)
Lemma newvars_fresh:
  forall (As:list sort)(B:sort)(t:Term B),
    fresh_vars As (newvars As B t) B t.
Proof.
intro As; elim As; simpl; clear As.
trivial.
intros A As IH B t; split.
apply fresh_newvar.
split.
apply distinct_newvars.
apply IH.
Qed.

Lemma fresh_vars_swapvar_id:
  forall (As:list sort)(is js:indices As)(A':sort)(i:nat),
    fresh_vars As is A' (var A' i) ->
    var A' i = swapvar A' i As is js.
Proof.
intros As; elim As; clear As; simpl.
trivial.
intros A As IH is js A' i.
rewrite sl_head_tail_id with (al:=is);rewrite sl_head_tail_id with (al:=js); simpl.
case (sort_dec A' A).
intro HA; rewrite HA.
case (eq_nat_dec i (sl_head is)).
intros Hi [H1 _].
case H1.
intro HnA; elim HnA; trivial.
intro Hni; elim Hni; trivial.
symmetry; exact Hi.
intros _ [_ [_ H3]].
apply IH.
exact H3.
intros _ [_ [_ H3]].
apply IH.
exact H3.
Qed.

Lemma apvalue_cases:
  forall A' i' As is js,
    (apvalue A' i' As js (vars As is)) = bnd A' i' \/
    (exists k:nat, (apvalue A' i' As js (vars As is)) = var A' k /\
               ~ (not_in_vars A' k As is)).
Proof.
intros A' i' As; elim As; clear As; simpl.
intros; left; trivial.
intros A As IH is js.
rewrite sl_head_tail_id with (al:=is); rewrite sl_head_tail_id with (al:=js).
simpl.
case (sort_dec A A').
intro Heq; case Heq.
case (eq_nat_dec i' (sl_head js)).
intro Hi'; right.
exists (sl_head is).
simpl.
split.
trivial.
intros [H1 _].
case H1; intro H; elim H; trivial.

generalize is; generalize js; clear is; clear js; rewrite Heq.
intros js; intros is.
case (IH (sl_tail is) (sl_tail js)).
intros Hbnd _; left; exact Hbnd.
intros [k [H1 H2]] H; right.
exists k; split.
exact H1.
intros [_ Hniv]; elim H2; exact Hniv.

intro HA; rewrite sl_head_tail_id with (al:=is); rewrite sl_head_tail_id with (al:=js); simpl.
case (IH (sl_tail is) (sl_tail js)).
intro IH1; left; exact IH1.
intros [k [IH1 IH2]]; right.
exists k; split.
exact IH1.
intros [_ H]; elim IH2; exact H.
Qed.

Lemma apvalue_vars_swap_cons:
  forall A' (i':nat) A As i is j js,
  (A'<>A \/ i'<>j) ->
  not_in_vars A i As is ->
  (vars_swap (A::As) (sort_cons (F:=fun _ => nat) A i is)
                     (sort_cons (F:=fun _ => nat) A j js)
  A' (apvalue A' i' As js (vars As is)))
  =
  (vars_swap As is js
  A' (apvalue A' i' As js (vars As is))).
Proof.
intros A' i' A As i is j js H1 H2.
case (apvalue_cases A' i' As is js).
intro H; rewrite H.
simpl.
case H1.
intros HA; case (sort_dec A' A).
intro HAn; elim HA; exact HAn.
trivial.
intro Hi'; case (eq_nat_dec i' j).
intro Hi'n; elim Hi'; exact Hi'n.
case (sort_dec A' A).
trivial.
trivial.
intros [k [Hk1 Hk2]].
rewrite Hk1; simpl.
case (sort_dec A' A).
intro HA; case (eq_nat_dec k i).
intro Hk; rewrite Hk in Hk2; elim Hk2; rewrite HA; exact H2.
trivial.
trivial.
Qed.

Lemma apvalue_bnd_id:
  forall A' i As is js,
    independent_indices As is ->
    (bnd A' i) = vars_swap As is js A' (apvalue A' i As js (vars As is)).
Proof.
intros A i As; elim As; clear As; simpl.
trivial.
intros A' As IH.
case (sort_dec A' A).
intro Heq; generalize IH; clear IH; case Heq; clear Heq; intro IH.
intros is js Hind;
  rewrite sl_head_tail_id with (al:=is);
  rewrite sl_head_tail_id with (al:=js);
  case (eq_nat_dec i (sl_head js)).
intro Hi; rewrite <- Hi; simpl.
case (eq_nat_dec i i).
intros _; simpl.
case (sort_dec A' A').
intros _; simpl.
case (eq_nat_dec (sl_head is) (sl_head is)).
trivial.
intro H; elim H; trivial.
intro H; elim H; trivial.
intro H; elim H; trivial.
intro Hi; simpl.
case (eq_nat_dec i (sl_head js)).
intro Hijs; rewrite <- Hijs; simpl.
case (sort_dec A' A').
intros _; simpl.
case (eq_nat_dec (sl_head is) (sl_head is)).
trivial.
intro H; elim H; trivial.
intro H; elim H; trivial.
intros _; simpl.

case Hind; intros H1 H2.
rewrite apvalue_vars_swap_cons.
apply IH.
exact H1.
right; exact Hi.
exact H2.

intros HA is js; rewrite sl_head_tail_id with (al:=is).
rewrite sl_head_tail_id with (al:=js).
simpl.
intros [Hind H].
rewrite apvalue_vars_swap_cons.
apply IH.
exact Hind.
left; apply sym_not_eq; exact HA.
exact H.
Qed.

Fixpoint fresh_vars_list' (As:list sort)(is:indices As){struct is}:
  forall (Ts:list (arg_type sort)), TermList Ts -> Prop :=
match is with
  sort_nil => fun _ _ => True
| sort_cons A As i is => fun Ts ts =>
    (fresh_var_list A i Ts ts)/\
    (not_in_vars A i As is) /\
    (fresh_vars_list' As is Ts ts)
end.

Lemma fvl'_independent_indices:
  forall As is Ts ts,
    fresh_vars_list' As is Ts ts -> independent_indices As is.
Proof.
intros As is; elim is; clear is; clear As; simpl.
trivial.
intros A As i is IH Ts ts [H1 [H2 H3]]; split.
apply IH with (ts:=ts).
exact H3.
exact H2.
Qed.

Lemma independent_indices_fvl':
  forall As is,
    independent_indices As is ->  fresh_vars_list' As is [] nil_term.
Proof.
intros As is; elim is; clear is; clear As; simpl.
trivial.
intros A As i is IH [H1 H2]; repeat split.
exact H2.
apply IH.
exact H1.
Qed.

Lemma fresh_vars_list_equiv:
  forall As is Ts ts,
    fresh_vars_list' As is Ts ts <-> fresh_vars_list As is Ts ts.
Proof.
intros As is; elim is; clear is; clear As; simpl.
intros Ts ts; elim ts; clear ts; clear Ts; simpl.
split; trivial.
intros T Ts t ts [IHl IHr].
split.
intros _; split.
trivial.
apply IHl; trivial.
trivial.

intros A As i is IHis Ts ts.
elim ts; clear ts; clear Ts; simpl.
split.
intros [_ [H1 H2]]; repeat split.
apply fvl'_independent_indices with (ts:=nil_term).
exact H2.
exact H1.

intros [H1 H2]; repeat split.
exact H2.
apply independent_indices_fvl'; exact H1.

intros T Ts t ts IHts.
generalize (IHis (T::Ts) (cons_term T Ts t ts)); intros [IHis1 IHis2].
split.
intros [[H1 H2] [H3 H4]].
generalize (IHis1 H4); simpl; intros [HH1 HH2].
repeat split.
exact H1.
exact H3.
exact HH1.
apply (proj1 IHts).
repeat split.
exact H2.
exact H3.
generalize (IHis Ts ts); intros [His1 His2].
apply His2.
exact HH2.

intros [[H1 [H2 H3]] H4]; repeat split.
exact H1.
generalize (proj2 IHts H4); intros [HH1 [HH2 HH3]].
exact HH1.
exact H2.
apply IHis2.
simpl.
split.
exact H3.
apply (proj1 (IHis Ts ts)).
exact (proj2 (proj2 (proj2 IHts H4))).
Qed.

Lemma fresh_vars_opr_list:
  forall As is f ts,
    fresh_vars As is _ (opr f ts) -> fresh_vars_list As is _ ts.
Proof.
intros As is f ts.
generalize (fresh_vars_list_equiv As is (op_arguments (rule f)) ts).
intros [HH1 HH2].
intro H; apply HH1.
generalize H; clear H; clear HH1; clear HH2.
generalize ts; clear ts; generalize f; clear f;
  elim is; clear is; clear As; simpl.
trivial.
intros A As i is IH f ts.
intros [H1 [H2 H3]]; repeat split.
exact H1.
exact H2.
apply IH.
exact H3.
Qed.

Lemma bind_vars_bnds_aux:
  forall (As:list sort)(is: indices As),
  (forall (B:sort)(t:Term B), forall js:indices As,
     independent_indices As is ->
     fresh_vars As is B t -> 
     t = vars_swap As is js B (sub B t As js (vars As is)))  /\
  (forall (Ts:list (arg_type sort))(ts:TermList Ts), forall js:indices As,
     independent_indices As is ->
     fresh_vars_list As is Ts ts ->
     ts = vars_swap_list As is js Ts (subs Ts ts As js (vars As is))).
Proof.
intros As is.
apply Term_TermList_ind with
  (P := fun B t => forall js,
          independent_indices As is ->
          fresh_vars As is B t -> 
          t = vars_swap As is js B (sub B t As js (vars As is)))
  (Ps := fun Ts ts => forall js,
          independent_indices As is ->
          fresh_vars_list As is Ts ts ->
          ts = vars_swap_list As is js Ts (subs Ts ts As js (vars As is))).
(* var *)
intros A i; elim is; clear is; clear As; simpl.
trivial.
intros A' As i' is IH js _.
case (sort_dec A A').
intro HA; rewrite HA.
case (eq_nat_dec i i').
intro Hi; rewrite Hi.
intros [H1 _]; case H1.
intro H; elim H; trivial.
intro H; elim H; trivial.
intros Hi [_ [_ H3]]; apply fresh_vars_swapvar_id; exact H3.
intros HA [_ [_ H3]]; apply fresh_vars_swapvar_id; exact H3.
(* bnd *)
intros A i js Hind _; unfold sub; simpl.
apply apvalue_bnd_id.
exact Hind.
(* opr *)
intros f ts IH js Hind H.
simpl.
rewrite <- IH.
trivial.
exact Hind.
apply fresh_vars_opr_list.
exact H.
(* nil_term *)
simpl.
trivial.
(* cons_term *)
intros T Ts t ts IHt IHts js Hind [H1 H2]; simpl.
rewrite <- IHt with (js := (bind_incs (arg_bindings T) As js)).
rewrite <- IHts.
trivial.
exact Hind.
exact H2.
exact Hind.
exact H1.
Qed.

Lemma bind_vars_bnds:
  forall (As:list sort)(B:sort)(t:Term B)(is js: indices As),
    independent_indices As is ->
    fresh_vars As is B t -> 
    t = vars_swap As is js B (sub B t As js (vars As is)).
Proof.
intros As B t is js.
generalize (bind_vars_bnds_aux As is); intros [H _]; apply H.
Qed.

(* Substituting deBruijn variables doesn't elimitate free variables *)

Lemma fresh_var_sub:
  forall (A:sort)(i:nat)(B:sort)(t:Term B)
         (Cs:list sort)(js:indices Cs)(al:sort_list Term Cs),
    fresh_var A i B (sub B t Cs js al) -> fresh_var A i B t.
Proof.
intros A i.
generalize (Term_mutual_ind
       (fun B t =>
          forall (Cs:list sort)(js:indices Cs)(al:sort_list Term Cs),
          fresh_var A i B (sub B t Cs js al) -> fresh_var A i B t)
       (fun Ts ts =>
           forall (Cs:list sort)(js:indices Cs)(al:sort_list Term Cs),
           fresh_var_list A i Ts (subs Ts ts Cs js al) ->
           fresh_var_list A i Ts ts)).
intro Hind.
intros B t Cs js al H.
apply Hind with (js:=js)(al:=al); simpl.
trivial.
trivial.
intros f ts IH.
intros Cs' js' al' H'.
apply IH with (js:=js')(al:=al').
exact H'.
trivial.

intros T Ts t' ts IH1 IH2.
intros Cs' js' al' [H1 H2].
split.
apply IH1 with (js:=(bind_incs (arg_bindings T) Cs' js'))(al:=al').
exact H1.
apply IH2 with (js:=js')(al:=al').
exact H2.
exact H.
Qed.

Lemma fresh_sub:
  forall (As:list sort)(is:indices As)(B:sort)(t:Term B)
         (Cs:list sort)(js:indices Cs)(al:sort_list Term Cs),
    fresh_vars As is B (sub B t Cs js al) -> fresh_vars As is B t.
Proof.
intros As is; elim is; clear is; clear As; simpl.
trivial.
intros A As i is IH B t Cs js al [H1 [H2 H3]]; repeat split.
apply fresh_var_sub with (js:=js)(al:=al).
exact H1.
exact H2.
apply IH with (js:=js)(al:=al); exact H3.
Qed.

(* In particular for the generated free variables *)
Lemma new_vars_fresh:
  forall (As:list sort)(B:sort)(t:Term B)
         (js:indices As)(al:sort_list Term As),
    fresh_vars As (newvars As B (sub B t As js al)) B t.
Proof.
intros As B t js al.
apply fresh_sub with (js:=js)(al:=al).
apply newvars_fresh.
Qed.

Lemma newvars_independent:
  forall As A' t, independent_indices As (newvars As A' t).
Proof.
intro As; elim As; clear As; simpl.
trivial.
intros A As IH A' t; split.
apply IH.
apply distinct_newvars.
Qed.

Lemma bind_sub_id_aux:
  forall (As:list sort)(B:sort)(t:Term B),
    t = bind (As|--B) (sub B t As (bind_vars As)).
Proof.
intros As B t.
unfold bind.
unfold bind_args.
apply bind_vars_bnds.

simpl.
apply newvars_independent.

simpl.
apply new_vars_fresh.
Qed.

Lemma bind_sub_id:
  forall (T:arg_type sort)(t:Term (arg_result T)),
    t = bind T (sub _ t _ (bind_vars (arg_bindings T))).
Proof.
intros T; case T; apply bind_sub_id_aux.
Qed.

Theorem binds_aps_id:
  forall (Ts: list (arg_type sort))(ts:TermList Ts),
    ts = binds Ts (aps Ts ts).
Proof.
induction ts; simpl.
trivial.
rewrite <- bind_sub_id.
rewrite <- IHts.
trivial.
Qed.

(* RECURSION *)

Section De_Bruijn_Recursion.

Variable H: sort -> Set.

Definition TLfam: list (arg_type sort) -> Set :=
  fun Ts => sort_list H (map (arg_result (sort:=sort)) Ts).

Hypotheses 
  (Hvar: forall (s:sort), nat -> H s)
  (Hbnd: forall (s:sort), nat -> H s)
  (Hopr: forall (f:operation), TermList (op_arguments (rule f)) ->
           TLfam (op_arguments (rule f)) -> H (op_result (rule f))).

Fixpoint debruijn_term_recursion (A:sort)(t:Term A){struct t}: H A :=
match t in (Term A) return (H A) with
  var A i => Hvar A i
| bnd A i => Hbnd A i
| opr f ts => Hopr f ts (debruijn_term_list_recursion _ ts)
end
with debruijn_term_list_recursion (Ts:list (arg_type sort))
                                  (ts:TermList Ts){struct ts}: TLfam Ts:=
match ts in (TermList Ts) return (TLfam Ts) with
  nil_term => sort_nil H
| cons_term T Ts t ts =>
    sort_cons (arg_result T)
              (debruijn_term_recursion _ t)
              (debruijn_term_list_recursion Ts ts)
end.

End De_Bruijn_Recursion.

Section Higher_Order_Recursion.

Variable F: sort -> Set.

(* An assignment gives a value in type (F s)
   for every dangling variable (bnd s i)
*)
Definition Assignment := forall (s : sort), Stream (F s).

Definition new_assign: Assignment -> forall A:sort, F A -> Assignment :=
fun (alpha : Assignment)(A : sort)(a : F A) =>
fun (A' : sort) =>
match sort_dec A' A with
| left h =>
    eq_rec_r (fun X: sort => Stream (F X)) 
             (Cons a (alpha A)) h
| right _ => alpha A'
end.

Fixpoint modify_assignment
  (alpha:Assignment)(As:list sort)(al:sort_list F As){struct al}: Assignment :=
match al with
  sort_nil => alpha
| sort_cons A As a al => new_assign (modify_assignment alpha As al) A a
end.

Variables 
  (Fvar : forall (s : sort), nat -> F s)
  (FOpr: forall (f:operation), meta_args (op_arguments (rule f)) ->
           args_map F (op_arguments (rule f)) -> (F (op_result (rule f)))).

Let H: sort -> Set := fun A => Assignment -> F A.

Fixpoint strapp (Ts:list (arg_type sort)){struct Ts}:
  TLfam H Ts -> Assignment -> args_map F Ts :=
match Ts return TLfam H Ts -> Assignment -> args_map F Ts with
  nil => fun rs alpha => meta_nil F
| cons T Ts =>  fun rs alpha =>
    meta_cons (fun al => (sl_head rs) (modify_assignment alpha _ al))
              (strapp Ts (sl_tail rs) alpha)
end.

Let Hvar: forall A : sort, nat -> H A :=
      fun A i alpha => Fvar A i.
Let Hbnd: forall A : sort, nat -> H A :=
      fun A i alpha => Str_nth i (alpha A).
Let Hopr: forall f : operation,
          TermList (op_arguments (rule f)) ->
          TLfam H (op_arguments (rule f)) -> H (op_result (rule f)) :=
      fun f ts rs alpha => FOpr f (aps _ ts) (strapp _ rs alpha).

Definition term_recursion: Assignment -> forall (A:sort), Term A -> F A :=
  fun alpha A t => debruijn_term_recursion H Hvar Hbnd Hopr A t alpha.

Definition term_list_recursion:
  Assignment -> forall ts:list (arg_type sort),
                  meta_args ts -> args_map F ts :=
  fun alpha Ts ts =>
    strapp _ (debruijn_term_list_recursion H Hvar Hbnd Hopr Ts (binds Ts ts))
           alpha.

(* Reduction Rules *)

Theorem var_reduction:
  forall (alpha:Assignment)(A:sort)(i:nat),
    term_recursion alpha A (var A i) = Fvar A i.
Proof.
auto.
Qed.

Theorem bnd_reduction:
  forall (alpha:Assignment)(A:sort)(i:nat),
    term_recursion alpha A (bnd A i) = Str_nth i (alpha A).
Proof.
auto.
Qed.

Theorem Opr_reduction:
  forall (alpha:Assignment)
         (f:operation)
         (hs: meta_args (op_arguments (rule f))),
  term_recursion alpha (op_result (rule f)) (Opr f hs)
  = FOpr f (nfun _ hs) (term_list_recursion alpha _ hs).
Proof.
auto.
Qed.

Theorem list_nil_reduction:
  forall alpha:Assignment,
    term_list_recursion alpha nil (meta_nil Term)
    = meta_nil F.
Proof.
auto.
Qed.

Theorem list_cons_reduction:
forall (alpha:Assignment)(T: arg_type sort)(Ts: list (arg_type sort))
       (h: meta_arg T)(hs:meta_args Ts),
  term_list_recursion alpha (T::Ts) (meta_cons h hs)
  = meta_cons
      (fun aa => term_recursion (modify_assignment alpha (arg_bindings T) aa)
                                (arg_result T) (bind T h))
      (term_list_recursion alpha Ts hs).
Proof.
auto.
Qed.

End Higher_Order_Recursion.

(* INDUCTION *)

Variable P: forall (s:sort), Term s -> Prop.

(* TLpred extends the predicate P to lists of terms
   We ignore the bindings: IS THIS CORRECT?
*)

Fixpoint TLpred (Ts:list (arg_type sort))(ts:TermList Ts){struct ts}: Prop :=
match ts with
  nil_term => True
| cons_term T Ts t ts => (P _ t) /\ (TLpred Ts ts)
end.

Section De_Bruijn_Induction.

Hypotheses 
  (Hvar: forall (s:sort)(i:nat), P s (var s i))
  (Hbnd: forall (s:sort)(i:nat), P s (bnd s i))
  (Hopr: forall (f:operation)(ts:TermList (op_arguments (rule f))),
           TLpred _ ts -> P _ (opr f ts)).

Fixpoint
  debruijn_term_induction (s:sort)(t:Term s){struct t}: P s t :=
match t in (Term s) return (P s t) with
  var s i => Hvar s i
| bnd s i => Hbnd s i
| opr f ts => Hopr f ts (debruijn_term_list_induction _ ts)
end
with
  debruijn_term_list_induction (Ts:list (arg_type sort))(ts:TermList Ts){struct ts}: TLpred Ts ts:=
match ts in (TermList Ts) return (TLpred Ts ts) with
  nil_term => I
| cons_term a al t ts => conj (debruijn_term_induction _ t) (debruijn_term_list_induction al ts)
end.

End De_Bruijn_Induction.

Theorem term_induction:
  (forall (s:sort)(i:nat), P s (var s i)) ->
  (forall (s:sort)(i:nat), P s (bnd s i)) ->
  (forall (f:operation)(tl:meta_args (op_arguments (rule f))),
             TLpred _ (binds _ tl) -> P _ (Opr f tl))
  -> forall (s:sort)(t:Term s), P s t.
Proof.
intros Hvar Hbnd Hopr s t; apply debruijn_term_induction; clear t.
exact Hvar.
exact Hbnd.
intros f tl; rewrite binds_aps_id with (ts:=tl).
apply Hopr with (tl:= aps (op_arguments (rule f)) tl).
Qed.

End Higher_Order_Universal_Algebra.

Implicit Arguments newvar [sign A].
Implicit Arguments one_arg_bind [sign A B].
Implicit Arguments bind_args [sign].

Implicit Arguments nil_term [sign].
Implicit Arguments cons_term [sign Ts].