blob: 4cf30d692cf648925713bd1cff8552844578535b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
|
(*************************************************************)
(* 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 Coqprime.Iterator.
Require Import Coq.ZArith.ZArith.
Require Export Coqprime.UList.
Open Scope Z_scope.
Theorem next_n_Z: forall n m, next_n Zsucc n m = n + Z_of_nat m.
intros n m; generalize n; elim m; clear n m.
intros n; simpl; auto with zarith.
intros m H n.
replace (n + Z_of_nat (S m)) with (Zsucc n + Z_of_nat m); auto with zarith.
rewrite <- H; auto with zarith.
rewrite inj_S; auto with zarith.
Qed.
Theorem Zprogression_end:
forall n m,
progression Zsucc n (S m) =
app (progression Zsucc n m) (cons (n + Z_of_nat m) nil).
intros n m; generalize n; elim m; clear n m.
simpl; intros; apply f_equal2 with ( f := @cons Z ); auto with zarith.
intros m1 Hm1 n1.
apply trans_equal with (cons n1 (progression Zsucc (Zsucc n1) (S m1))); auto.
rewrite Hm1.
replace (Zsucc n1 + Z_of_nat m1) with (n1 + Z_of_nat (S m1)); auto with zarith.
replace (Z_of_nat (S m1)) with (1 + Z_of_nat m1); auto with zarith.
rewrite inj_S; auto with zarith.
Qed.
Theorem Zprogression_pred_end:
forall n m,
progression Zpred n (S m) =
app (progression Zpred n m) (cons (n - Z_of_nat m) nil).
intros n m; generalize n; elim m; clear n m.
simpl; intros; apply f_equal2 with ( f := @cons Z ); auto with zarith.
intros m1 Hm1 n1.
apply trans_equal with (cons n1 (progression Zpred (Zpred n1) (S m1))); auto.
rewrite Hm1.
replace (Zpred n1 - Z_of_nat m1) with (n1 - Z_of_nat (S m1)); auto with zarith.
replace (Z_of_nat (S m1)) with (1 + Z_of_nat m1); auto with zarith.
rewrite inj_S; auto with zarith.
Qed.
Theorem Zprogression_opp:
forall n m,
rev (progression Zsucc n m) = progression Zpred (n + Z_of_nat (pred m)) m.
intros n m; generalize n; elim m; clear n m.
simpl; auto.
intros m Hm n.
rewrite (Zprogression_end n); auto.
rewrite distr_rev.
rewrite Hm; simpl; auto.
case m.
simpl; auto.
intros m1;
replace (n + Z_of_nat (pred (S m1))) with (Zpred (n + Z_of_nat (S m1))); auto.
rewrite inj_S; simpl; (unfold Zpred; unfold Zsucc); auto with zarith.
Qed.
Theorem Zprogression_le_init:
forall n m p, In p (progression Zsucc n m) -> (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 zarith.
generalize (H _ _ H1); auto with zarith.
Qed.
Theorem Zprogression_le_end:
forall n m p, In p (progression Zsucc n m) -> (p < n + Z_of_nat m).
intros n m; generalize n; elim m; clear n m; auto.
intros; contradiction.
intros m H n p H1; simpl in H1 |-; case H1; clear H1; intros H1;
auto with zarith.
subst n; auto with zarith.
apply Zle_lt_trans with (p + 0); auto with zarith.
apply Zplus_lt_compat_l; red; simpl; auto with zarith.
apply Zlt_le_trans with (Zsucc n + Z_of_nat m); auto with zarith.
rewrite inj_S; rewrite Zplus_succ_comm; auto with zarith.
Qed.
Theorem ulist_Zprogression: forall a n, ulist (progression Zsucc a n).
intros a n; generalize a; elim n; clear a n; simpl; auto with zarith.
intros n H1 a; apply ulist_cons; auto.
intros H2; absurd (Zsucc a <= a); auto with zarith.
apply Zprogression_le_init with ( 1 := H2 ).
Qed.
Theorem in_Zprogression:
forall a b n, ( a <= b < a + Z_of_nat n ) -> In b (progression Zsucc a n).
intros a b n; generalize a b; elim n; clear a b n; auto with zarith.
simpl; auto with zarith.
intros n H a b.
replace (a + Z_of_nat (S n)) with (Zsucc a + Z_of_nat n); auto with zarith.
intros [H1 H2]; simpl; auto with zarith.
case (Zle_lt_or_eq _ _ H1); auto with zarith.
rewrite inj_S; auto with zarith.
Qed.
|
