Require Export Omega. Section def. Variable A : Set. Inductive vect : nat -> Set := | vnil : vect 0 | vcons : forall n : nat, vect n -> A -> vect (S n). End def. Fixpoint unzip (A B : Set) (n : nat) (v : vect (A * B) n) {struct v} : vect A n * vect B n := match v in (vect _ n) return (vect A n * vect B n) with | vnil => pair (vnil A) (vnil B) | vcons n' v' (x, y) => let (l1, l2) := unzip A B n' v' in pair (vcons A n' l1 x) (vcons B n' l2 y) end. Definition input1 := vnil (Z * Z). Definition input2 := vcons (Z * Z) 0 input1 (0%Z, 0%Z). Definition input3 := vcons (Z * Z) 1 input2 (2%Z, 4%Z). Definition input4 := vcons (Z * Z) 2 input3 (1%Z, 3%Z). Eval compute in input4. Eval compute in (unzip Z Z 3 input4). (*# let rec unzip l = match l with [] ->[],[] | (x,y)::xs -> let (l1,l2)=(unzip xs) in (x::l1,y::l2);; val unzip : ('a * 'b) list -> 'a list * 'b list = # unzip [(1,3); (2,4); (0,0)];; - : int list * int list = [1; 2; 0], [3; 4; 0] # *) Definition zip : forall (A B : Set) (n : nat), vect A n -> vect B n -> vect (A * B) n. intros A B. (* n v v'.*) fix 1. intros n; case n. intros; exact (vnil (A * B)). intros n0. intros v; inversion v. intros v'; inversion v' in H0. apply vcons. apply zip. exact H0. exact H3. exact (pair H1 H4). Defined. Eval compute in (let (l1, l2) := unzip Z Z 3 input4 in zip Z Z 3 l1 l2). (* Reduction only works if terms are transparent *) Definition eq_add_S_tr (n m : nat) (H : S n = S m) : n = m := f_equal pred H. Fixpoint zip2 (A B : Set) (n : nat) {struct n} : vect A n -> vect B n -> vect (A * B) n := match n return (vect A n -> vect B n -> vect (A * B) n) with | O => fun _ _ => vnil (A * B) | S n0 => fun v : vect A (S n0) => match v in (vect _ n) return (n = S n0 -> vect B (S n0) -> vect (A * B) (S n0)) with | vnil => fun H0 : 0 = S n0 => False_rec (vect B (S n0) -> vect (A * B) (S n0)) (O_S n0 H0) | vcons n1 v1 x1 => fun (H2 : S n1 = S n0) (v' : vect B (S n0)) => match v' in (vect _ n) return (n = S n0 -> vect (A * B) (S n0)) with | vnil => fun H3 : 0 = S n0 => False_rec (vect (A * B) (S n0)) (O_S n0 H3) | vcons n1' v1' x1' => fun H6 : S n1' = S n0 => vcons (A * B) n0 (zip2 A B n0 (eq_rec n1 (fun n : nat => vect A n) v1 n0 (eq_add_S_tr n1 n0 H2)) (eq_rec n1' (fun n : nat => vect B n) v1' n0 (eq_add_S_tr n1' n0 H6))) (x1, x1') end (refl_equal (S n0)) end (refl_equal (S n0)) end. Eval compute in (let (l1, l2) := unzip Z Z 3 input4 in zip2 Z Z 3 l1 l2). Fixpoint zip3 (A B : Set) (n : nat) (v : vect A n) {struct v} : vect B n -> vect (A * B) n := match v in (vect _ k) return (vect B k -> vect (A * B) k) with | vnil => fun v' => vnil (A * B) | vcons n1 v1 x1 => fun v' : vect B (S n1) => match v' in (vect _ k) return (k = S n1 -> vect (A * B) k) with | vnil => fun h => vnil (A * B) | vcons n2 v2 x2 => fun h => vcons (A * B) n2 (zip3 A B n2 (eq_rec n1 (fun n : nat => vect A n) v1 n2 (eq_add_S_tr n1 n2 (sym_eq h))) v2) (x1, x2) end (refl_equal (S n1)) end. Eval compute in (let (l1, l2) := unzip Z Z 3 input4 in zip3 Z Z 3 l1 l2). Fixpoint map (A B : Set) (f : A -> B) (n : nat) (v : vect A n) {struct v} : vect B n := match v in (vect _ k) return (vect B k) with | vnil => vnil B | vcons n0 v0 x0 => vcons B n0 (map A B f n0 v0) (f x0) end. Definition Svect (A : Set) := sigS (vect A). Section essai. Variable A : Set. Definition SVlt' : sigS (vect A) -> sigS (vect A) -> Prop. intros v v'. elim v. elim v'. intros. exact (x < x0). Defined. Definition SVlt (v v' : sigS (vect A)) := match v with | existS n _ => n end < match v' with | existS n _ => n end. End essai. (* Local Variables: mode: coq coq-prog-name: "/usr/local/coq-7.2/bin/coqtop -emacs -q -I ../AccDep" compile-command: "make definitions.vo" End:*)