(* 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].