diff options
Diffstat (limited to 'coqprime/Coqprime/Iterator.v')
-rw-r--r-- | coqprime/Coqprime/Iterator.v | 40 |
1 files changed, 20 insertions, 20 deletions
diff --git a/coqprime/Coqprime/Iterator.v b/coqprime/Coqprime/Iterator.v index 96d3e5655..dbfde2c38 100644 --- a/coqprime/Coqprime/Iterator.v +++ b/coqprime/Coqprime/Iterator.v @@ -9,7 +9,7 @@ Require Export List. Require Export Permutation. Require Import Arith. - + Section Iterator. Variables A B : Set. Variable zero : B. @@ -18,17 +18,17 @@ 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. @@ -36,7 +36,7 @@ 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 -> @@ -45,14 +45,14 @@ Lemma iter_inv: 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 -> @@ -64,9 +64,9 @@ 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 -> @@ -76,11 +76,11 @@ Theorem iter_progression_app: 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. Implicit Arguments iter [A B]. Implicit Arguments progression [A]. @@ -88,21 +88,21 @@ Implicit 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) -> @@ -115,7 +115,7 @@ 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) -> @@ -142,7 +142,7 @@ 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 -> @@ -151,14 +151,14 @@ Theorem iter_comp_const: 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. @@ -167,7 +167,7 @@ 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. |