Require Export definitions. Require Export lemmas. (* these induction principles relies on properties of dependent lists established in lemmas.v *) Lemma induc : forall (A : Set) (P : forall n : nat, vect A n -> vect A n -> Prop), P 0 (vnil A) (vnil A) -> (forall (n : nat) (v v' : vect A n), P n v v' -> forall a a' : A, P (S n) (vcons A n v a) (vcons A n v' a')) -> forall (n : nat) (v v' : vect A n), P n v v'. intros A P Hnil Hvcons n v. elim v. intros v'. replace v' with (vnil A); [ idtac | rewrite uniq; auto ]. exact Hnil. intros n0 v0 HR a v'. elim (decompose A n0 v'). intros ve Hve; elim Hve; intros xe Heq. rewrite Heq. apply Hvcons. apply HR. Qed. Lemma induc2 : forall (A B : Set) (P : forall n : nat, vect A n -> vect B n -> Prop), P 0 (vnil A) (vnil B) -> (forall (n : nat) (v : vect A n) (v' : vect B n), P n v v' -> forall (a : A) (b : B), P (S n) (vcons A n v a) (vcons B n v' b)) -> forall (n : nat) (v : vect A n) (v' : vect B n), P n v v'. intros A B P Hnil Hvcons n. elim n. intros v v'. replace v with (vnil A); [ idtac | rewrite uniq; auto ]. replace v' with (vnil B); [ idtac | rewrite uniq; auto ]. exact Hnil. intros n0 HR v v'. elim (decompose A n0 v). intros ve Hve; elim Hve; intros xe Heq. rewrite Heq. elim (decompose B n0 v'). intros ve' Hve'; elim Hve'; intros xe' Heq'. rewrite Heq'. apply Hvcons. apply HR. Qed. (* using induc2 *) Lemma unzip_zip3 : forall (A B : Set) (n : nat) (v : vect A n) (v' : vect B n), unzip A B n (zip3 A B n v v') = (v, v'). intros A B n v v'. eapply (induc2 A B (fun (n : nat) (v : vect A n) (v' : vect B n) => unzip A B n (zip3 A B n v v') = (v, v'))). simpl in |- *; trivial. intros. simpl in |- *. rewrite H; trivial. Qed. (* using induc2 *) Lemma unzip_zip2 : forall (A B : Set) (n : nat) (v : vect A n) (v' : vect B n), unzip A B n (zip2 A B n v v') = (v, v'). intros A B n v v'. eapply (induc2 A B (fun (n : nat) (v : vect A n) (v' : vect B n) => unzip A B n (zip2 A B n v v') = (v, v'))). simpl in |- *; trivial. intros. simpl in |- *. rewrite H; trivial. Qed. (* using induc2 *) Lemma unzip_zip : forall (A B : Set) (n : nat) (v : vect A n) (v' : vect B n), unzip A B n (zip A B n v v') = (v, v'). intros A B n v v'. eapply (induc2 A B (fun (n : nat) (v : vect A n) (v' : vect B n) => unzip A B n (zip A B n v v') = (v, v'))). simpl in |- *; trivial. intros. simpl in |- *. rewrite H; trivial. Qed. (* one_step is not mandatory but makes the proofs clearer *) Lemma one_step : forall (A B : Set) (n0 : nat) (v0 : vect (A * B) n0) (a : A * B), unzip A B (S n0) (vcons (A * B) n0 v0 a) = (let (x, y) := a in let (l1', l2') := unzip A B n0 v0 in (vcons A n0 l1' x, vcons B n0 l2' y)). intros A B n0 v0 a; auto. Qed. (* by induction on v *) Lemma zip_unzip2 : forall (A B : Set) (n : nat) (v : vect (A * B) n), let (l1, l2) := unzip A B n v in zip2 A B n l1 l2 = v. intros A B n v. elim v. simpl in |- *; auto. intros n0 v0. intros. simpl in |- *. generalize H; clear H. case (unzip A B n0 v0). case a; intros ax ay. simpl in |- *. intros v1 v2 HR. rewrite HR. trivial. Qed. Lemma zip_unzip : forall (A B : Set) (n : nat) (v : vect (A * B) n), let (l1, l2) := unzip A B n v in zip A B n l1 l2 = v. intros A B n v. elim v. simpl in |- *; auto. intros n0 v0. intros. rewrite one_step. generalize H; clear H. case (unzip A B n0 v0). case a; intros ax ay. simpl in |- *. intros v1 v2 HR. rewrite HR. trivial. Qed. Lemma zip3_unzip : forall (A B : Set) (n : nat) (v : vect (A * B) n), let (l1, l2) := unzip A B n v in zip3 A B n l1 l2 = v. intros A B n v. elim v. simpl in |- *; auto. intros n0 v0. intros. rewrite one_step. generalize H; clear H. case (unzip A B n0 v0). case a; intros ax ay. simpl in |- *. intros v1 v2 HR. rewrite HR. trivial. Qed. (* Local Variables: mode: coq coq-prog-name: "/usr/local/coq-7.2/bin/coqtop -emacs -q" compile-command: "make exp.vo" End: *)