diff options
Diffstat (limited to 'coqprime/Coqprime/Iterator.v')
| -rw-r--r-- | coqprime/Coqprime/Iterator.v | 180 |
1 files changed, 0 insertions, 180 deletions
diff --git a/coqprime/Coqprime/Iterator.v b/coqprime/Coqprime/Iterator.v deleted file mode 100644 index ed5261bcc..000000000 --- a/coqprime/Coqprime/Iterator.v +++ /dev/null @@ -1,180 +0,0 @@ - -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) - -Require Export List. -Require Export Permutation. -Require Import Arith. - -Section Iterator. -Variables A B : Set. -Variable zero : B. -Variable f : A -> B. -Variable g : B -> B -> B. -Hypothesis g_zero : forall a, g a zero = a. -Hypothesis g_trans : forall a b c, g a (g b c) = g (g a b) c. -Hypothesis g_sym : forall a b, g a b = g b a. - -Definition iter := fold_right (fun a r => g (f a) r) zero. -Hint Unfold iter . - -Theorem iter_app: forall l1 l2, iter (app l1 l2) = g (iter l1) (iter l2). -intros l1; elim l1; simpl; auto. -intros l2; rewrite g_sym; auto. -intros a l H l2; rewrite H. -rewrite g_trans; auto. -Qed. - -Theorem iter_permutation: forall l1 l2, permutation l1 l2 -> iter l1 = iter l2. -intros l1 l2 H; elim H; simpl; auto; clear H l1 l2. -intros a l1 l2 H1 H2; apply f_equal2 with ( f := g ); auto. -intros a b l; (repeat rewrite g_trans). -apply f_equal2 with ( f := g ); auto. -intros l1 l2 l3 H H0 H1 H2; apply trans_equal with ( 1 := H0 ); auto. -Qed. - -Lemma iter_inv: - forall P l, - P zero -> - (forall a b, P a -> P b -> P (g a b)) -> - (forall x, In x l -> P (f x)) -> P (iter l). -intros P l H H0; (elim l; simpl; auto). -Qed. -Variable next : A -> A. - -Fixpoint progression (m : A) (n : nat) {struct n} : list A := - match n with 0 => nil - | S n1 => cons m (progression (next m) n1) end. - -Fixpoint next_n (c : A) (n : nat) {struct n} : A := - match n with 0 => c | S n1 => next_n (next c) n1 end. - -Theorem progression_app: - forall a b n m, - le m n -> - b = next_n a m -> - progression a n = app (progression a m) (progression b (n - m)). -intros a b n m; generalize a b n; clear a b n; elim m; clear m; simpl. -intros a b n H H0; apply f_equal2 with ( f := progression ); auto with arith. -intros m H a b n; case n; simpl; clear n. -intros H1; absurd (0 < 1 + m); auto with arith. -intros n H0 H1; apply f_equal2 with ( f := @cons A ); auto with arith. -Qed. - -Let iter_progression := fun m n => iter (progression m n). - -Theorem iter_progression_app: - forall a b n m, - le m n -> - b = next_n a m -> - iter (progression a n) = - g (iter (progression a m)) (iter (progression b (n - m))). -intros a b n m H H0; unfold iter_progression; rewrite (progression_app a b n m); - (try apply iter_app); auto. -Qed. - -Theorem length_progression: forall z n, length (progression z n) = n. -intros z n; generalize z; elim n; simpl; auto. -Qed. - -End Iterator. -Arguments iter [A B]. -Arguments progression [A]. -Arguments next_n [A]. -Hint Unfold iter . -Hint Unfold progression . -Hint Unfold next_n . - -Theorem iter_ext: - forall (A B : Set) zero (f1 : A -> B) f2 g l, - (forall a, In a l -> f1 a = f2 a) -> iter zero f1 g l = iter zero f2 g l. -intros A B zero f1 f2 g l; elim l; simpl; auto. -intros a l0 H H0; apply f_equal2 with ( f := g ); auto. -Qed. - -Theorem iter_map: - forall (A B C : Set) zero (f : B -> C) g (k : A -> B) l, - iter zero f g (map k l) = iter zero (fun x => f (k x)) g l. -intros A B C zero f g k l; elim l; simpl; auto. -intros; apply f_equal2 with ( f := g ); auto with arith. -Qed. - -Theorem iter_comp: - forall (A B : Set) zero (f1 f2 : A -> B) g l, - (forall a, g a zero = a) -> - (forall a b c, g a (g b c) = g (g a b) c) -> - (forall a b, g a b = g b a) -> - g (iter zero f1 g l) (iter zero f2 g l) = - iter zero (fun x => g (f1 x) (f2 x)) g l. -intros A B zero f1 f2 g l g_zero g_trans g_sym; elim l; simpl; auto. -intros a l0 H; rewrite <- H; (repeat rewrite <- g_trans). -apply f_equal2 with ( f := g ); auto. -(repeat rewrite g_trans); apply f_equal2 with ( f := g ); auto. -Qed. - -Theorem iter_com: - forall (A B : Set) zero (f : A -> A -> B) g l1 l2, - (forall a, g a zero = a) -> - (forall a b c, g a (g b c) = g (g a b) c) -> - (forall a b, g a b = g b a) -> - iter zero (fun x => iter zero (fun y => f x y) g l1) g l2 = - iter zero (fun y => iter zero (fun x => f x y) g l2) g l1. -intros A B zero f g l1 l2 H H0 H1; generalize l2; elim l1; simpl; auto; - clear l1 l2. -intros l2; elim l2; simpl; auto with arith. -intros; rewrite H1; rewrite H; auto with arith. -intros a l1 H2 l2; case l2; clear l2; simpl; auto. -elim l1; simpl; auto with arith. -intros; rewrite H1; rewrite H; auto with arith. -intros b l2. -rewrite <- (iter_comp - _ _ zero (fun x => f x a) - (fun x => iter zero (fun (y : A) => f x y) g l1)); auto with arith. -rewrite <- (iter_comp - _ _ zero (fun y => f b y) - (fun y => iter zero (fun (x : A) => f x y) g l2)); auto with arith. -(repeat rewrite H0); auto. -apply f_equal2 with ( f := g ); auto. -(repeat rewrite <- H0); auto. -apply f_equal2 with ( f := g ); auto. -Qed. - -Theorem iter_comp_const: - forall (A B : Set) zero (f : A -> B) g k l, - k zero = zero -> - (forall a b, k (g a b) = g (k a) (k b)) -> - k (iter zero f g l) = iter zero (fun x => k (f x)) g l. -intros A B zero f g k l H H0; elim l; simpl; auto. -intros a l0 H1; rewrite H0; apply f_equal2 with ( f := g ); auto. -Qed. - -Lemma next_n_S: forall n m, next_n S n m = plus n m. -intros n m; generalize n; elim m; clear n m; simpl; auto with arith. -intros m H n; case n; simpl; auto with arith. -rewrite H; auto with arith. -intros n1; rewrite H; simpl; auto with arith. -Qed. - -Theorem progression_S_le_init: - forall n m p, In p (progression S n m) -> le n p. -intros n m; generalize n; elim m; clear n m; simpl; auto. -intros; contradiction. -intros m H n p [H1|H1]; auto with arith. -subst n; auto. -apply le_S_n; auto with arith. -Qed. - -Theorem progression_S_le_end: - forall n m p, In p (progression S n m) -> lt p (n + m). -intros n m; generalize n; elim m; clear n m; simpl; auto. -intros; contradiction. -intros m H n p [H1|H1]; auto with arith. -subst n; auto with arith. -rewrite <- plus_n_Sm; auto with arith. -rewrite <- plus_n_Sm; auto with arith. -generalize (H (S n) p); auto with arith. -Qed. |