(* VECTORS *) (* Venanzio Capretta, Jun 2005 *) (* Coq version 8.0 *) (* There are three definition of vectors/finite sequences: vector: inductive definition; Vector: functional definition (functions on finite types); tuples: recursive products. *) Require Import Arith. Require Import Max. Inductive vector (A:Set): nat -> Set := vec_nil: vector A 0 | vec_cons: forall n:nat, vector A n -> A -> vector A (S n). Implicit Arguments vec_cons. Definition vector_head: forall (A:Set)(n:nat),(vector A (S n)) -> A. intros A n v; inversion_clear v. exact H0. Defined. Implicit Arguments vector_head [A n]. Definition vector_tail: forall (A:Set)(n:nat),(vector A (S n)) -> (vector A n). intros A n v; inversion_clear v. exact H. Qed. Implicit Arguments vector_tail [A n]. (* Finite types *) Inductive Finite: nat -> Set := fin_zero: forall n:nat, Finite (S n) | fin_succ: forall n:nat, Finite n -> Finite (S n). Implicit Arguments fin_succ [n]. Lemma fin_0_empty: (Finite 0) -> False. Proof. intro i; inversion i. Qed. Fixpoint nat_finite (n:nat){struct n}: forall k:nat, k Finite n := match n return (forall k:nat, k Finite n) with O => fun (k:nat)(h:k False_rec (Finite O) (lt_n_O k h) | (S n') => fun k:nat => match k return (k<(S n') -> Finite (S n')) with O => fun _ => (fin_zero n') | (S k') => fun h:S k' < S n' => fin_succ (nat_finite n' k' (lt_S_n k' n' h)) end end. Implicit Arguments nat_finite [n]. Fixpoint finite_nat (n:nat)(i:Finite n){struct i}: nat := match i with fin_zero n => 0 | fin_succ n i' => S (finite_nat n i') end. Implicit Arguments finite_nat [n]. Lemma nat_finite_id: forall (n k:nat)(h:k match n return (Finite n) -> Prop with O => fun i:(Finite 0) => True | (S n) => fun i:(Finite (S n)) => i=fin_zero n \/ exists j:Finite n, i=fin_succ j end) : forall n:nat, (Finite n) -> Prop). cut (forall (n:nat)(i:Finite n),(Q n i)). intros HQ n i; apply (HQ (S n) i). induction i. simpl; left; trivial. simpl; right. exists i; trivial. Qed. (* To construct a vector in one go: vector_make n a1 ... an *) Fixpoint pow_fun (n:nat)(A B:Set){struct n}: Set := match n with 0 => B | (S n) => A -> pow_fun n A B end. Fixpoint pow_fun_map (n:nat)(A B C:Set){struct n}: (B->C) -> pow_fun n A B -> pow_fun n A C := match n return (B->C) -> pow_fun n A B -> pow_fun n A C with O => fun f => f | (S n) => fun f => fun pf => fun a:A => pow_fun_map n A B C f (pf a) end. Fixpoint vector_make (A:Set)(n:nat){struct n}: pow_fun n A (vector A n) := match n return pow_fun n A (vector A n) with 0 => vec_nil A | (S n) => fun a:A => pow_fun_map n A (vector A n) (vector A (S n)) (fun v => vec_cons v a) (vector_make A n) end. Implicit Arguments vector_make [A]. Section Vectors. Variable A:Set. Definition Vector: nat -> Set := fun n:nat => (Finite n) -> A. Definition vec_proj: forall n:nat, Vector n -> Finite n -> A := fun n v i => v i. Definition vector_0: Vector 0 := fun i:(Finite 0) => False_rec A (fin_0_empty i). End Vectors. Implicit Arguments vec_proj [A n]. Fixpoint vector_max (m:nat): Vector nat m -> nat := match m return (Vector nat m)->nat with O => fun _ => 0 | S m => fun v => max (v (fin_zero m)) (vector_max m (fun j => (v (fin_succ j)))) end. Implicit Arguments vector_max [m]. Lemma vector_max_le: forall (m:nat)(v:Vector nat m)(i:Finite m), v i <= (vector_max v). Proof. induction i; simpl. apply le_max_l. apply le_trans with (vector_max (fun j : Finite n => v (fin_succ j))). apply (IHi (fun j : Finite n => v (fin_succ j))). apply le_max_r; auto. Qed. (* Tuples: Another way to describe vectors *) Section Tuples. Variable A:Set. Fixpoint Tuple (n:nat){struct n}: Set := match n with O => unit | (S n') => (A*(Tuple n'))%type end. Fixpoint tuple_proj (n:nat){struct n}: forall k:nat, k Tuple n -> A := match n return (forall k:nat, k Tuple n -> A) with O => fun (k:nat)(h:k False_rec A (lt_n_O k h) | (S n') => fun k:nat => match k return (k<(S n') -> Tuple (S n') -> A) with O => fun (h:0<(S n'))(v:Tuple (S n')) => (fst v) | (S k') => fun (h:S k' < S n')(v:Tuple (S n')) => (tuple_proj n' k' (lt_S_n k' n' h) (snd v)) end end. End Tuples. Implicit Arguments tuple_proj [A n]. Section Function_Tuples. Variables A B:Set. Fixpoint mult_app (n:nat){struct n}: Tuple (A->B) n -> A -> Tuple B n := match n return Tuple (A->B) n -> A -> Tuple B n with 0 => fun (f:unit)(a:A) => tt | (S n') => fun (f:(A->B)*(Tuple (A->B) n')) (a:A) => let (f0,f'):=f in (f0 a, mult_app n' f' a) end. End Function_Tuples. Implicit Arguments mult_app [A B n].