← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to theories/Arith/Div2.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
theories/Arith/Div2.v
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(*i $Id: Div2.v 11735 2009-01-02 17:22:31Z herbelin $ i*)
 
10
 
 
11
Require Import Lt.
 
12
Require Import Plus.
 
13
Require Import Compare_dec.
 
14
Require Import Even.
 
15
 
 
16
Open Local Scope nat_scope.
 
17
 
 
18
Implicit Type n : nat.
 
19
 
 
20
(** Here we define [n/2] and prove some of its properties *)
 
21
 
 
22
Fixpoint div2 n : nat :=
 
23
  match n with
 
24
  | O => 0
 
25
  | S O => 0
 
26
  | S (S n') => S (div2 n')
 
27
  end.
 
28
 
 
29
(** Since [div2] is recursively defined on [0], [1] and [(S (S n))], it is
 
30
    useful to prove the corresponding induction principle *)
 
31
 
 
32
Lemma ind_0_1_SS :
 
33
  forall P:nat -> Prop,
 
34
    P 0 -> P 1 -> (forall n, P n -> P (S (S n))) -> forall n, P n.
 
35
Proof.
 
36
  intros P H0 H1 Hn.
 
37
  cut (forall n, P n /\ P (S n)).
 
38
  intros H'n n. elim (H'n n). auto with arith.
 
39
  
 
40
  induction n. auto with arith.
 
41
  intros. elim IHn; auto with arith.
 
42
Qed.
 
43
 
 
44
(** [0 <n  =>  n/2 < n] *)
 
45
 
 
46
Lemma lt_div2 : forall n, 0 < n -> div2 n < n.
 
47
Proof.
 
48
  intro n. pattern n in |- *. apply ind_0_1_SS.
 
49
  (* n = 0 *)
 
50
  inversion 1.
 
51
  (* n=1 *)
 
52
  simpl; trivial.
 
53
  (* n=S S n' *)
 
54
  intro n'; case (zerop n').
 
55
    intro n'_eq_0. rewrite n'_eq_0. auto with arith.
 
56
    auto with arith.
 
57
Qed.
 
58
 
 
59
Hint Resolve lt_div2: arith.
 
60
 
 
61
(** Properties related to the parity *)
 
62
 
 
63
Lemma even_div2 : forall n, even n -> div2 n = div2 (S n)
 
64
with odd_div2 : forall n, odd n -> S (div2 n) = div2 (S n).
 
65
Proof.
 
66
  destruct n; intro H.
 
67
    (* 0 *) trivial.
 
68
    (* S n *) inversion_clear H. apply odd_div2 in H0 as <-. trivial.
 
69
  destruct n; intro.
 
70
    (* 0 *) inversion H.
 
71
    (* S n *) inversion_clear H. apply even_div2 in H0 as <-. trivial.
 
72
Qed.
 
73
 
 
74
Lemma div2_even : forall n, div2 n = div2 (S n) -> even n
 
75
with div2_odd : forall n, S (div2 n) = div2 (S n) -> odd n.
 
76
Proof.
 
77
  destruct n; intro H.
 
78
    (* 0 *) constructor.
 
79
    (* S n *) constructor. apply div2_odd. rewrite H. trivial.
 
80
  destruct n; intro H.
 
81
    (* 0 *) discriminate.
 
82
    (* S n *) constructor. apply div2_even. injection H as <-. trivial.
 
83
Qed.
 
84
 
 
85
Hint Resolve even_div2 div2_even odd_div2 div2_odd: arith.
 
86
 
 
87
Lemma even_odd_div2 :
 
88
  forall n,
 
89
    (even n <-> div2 n = div2 (S n)) /\ (odd n <-> S (div2 n) = div2 (S n)).
 
90
Proof.
 
91
  auto decomp using div2_odd, div2_even, odd_div2, even_div2.
 
92
Qed.
 
93
 
 
94
 
 
95
 
 
96
(** Properties related to the double ([2n]) *)
 
97
 
 
98
Definition double n := n + n.
 
99
 
 
100
Hint Unfold double: arith.
 
101
 
 
102
Lemma double_S : forall n, double (S n) = S (S (double n)).
 
103
Proof.
 
104
  intro. unfold double in |- *. simpl in |- *. auto with arith.
 
105
Qed.
 
106
 
 
107
Lemma double_plus : forall n (m:nat), double (n + m) = double n + double m.
 
108
Proof.
 
109
  intros m n. unfold double in |- *.
 
110
  do 2 rewrite plus_assoc_reverse. rewrite (plus_permute n).
 
111
  reflexivity.
 
112
Qed.
 
113
 
 
114
Hint Resolve double_S: arith.
 
115
 
 
116
Lemma even_odd_double :
 
117
  forall n,
 
118
    (even n <-> n = double (div2 n)) /\ (odd n <-> n = S (double (div2 n))).
 
119
Proof.
 
120
  intro n. pattern n in |- *. apply ind_0_1_SS.
 
121
  (* n = 0 *)
 
122
  split; split; auto with arith.
 
123
  intro H. inversion H.
 
124
  (* n = 1 *)
 
125
  split; split; auto with arith.
 
126
  intro H. inversion H. inversion H1.
 
127
  (* n = (S (S n')) *)
 
128
  intros. destruct H as ((IH1,IH2),(IH3,IH4)).
 
129
  split; split.
 
130
  intro H. inversion H. inversion H1.
 
131
  simpl in |- *. rewrite (double_S (div2 n0)). auto with arith.
 
132
  simpl in |- *. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith.
 
133
  intro H. inversion H. inversion H1.
 
134
  simpl in |- *. rewrite (double_S (div2 n0)). auto with arith.
 
135
  simpl in |- *. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith.
 
136
Qed.
 
137
(** Specializations *)
 
138
 
 
139
Lemma even_double : forall n, even n -> n = double (div2 n).
 
140
Proof fun n => proj1 (proj1 (even_odd_double n)).
 
141
 
 
142
Lemma double_even : forall n, n = double (div2 n) -> even n.
 
143
Proof fun n => proj2 (proj1 (even_odd_double n)).
 
144
 
 
145
Lemma odd_double : forall n, odd n -> n = S (double (div2 n)).
 
146
Proof fun n => proj1 (proj2 (even_odd_double n)).
 
147
 
 
148
Lemma double_odd : forall n, n = S (double (div2 n)) -> odd n.
 
149
Proof fun n => proj2 (proj2 (even_odd_double n)).
 
150
 
 
151
Hint Resolve even_double double_even odd_double double_odd: arith.
 
152
 
 
153
(** Application: 
 
154
    - if [n] is even then there is a [p] such that [n = 2p]
 
155
    - if [n] is odd  then there is a [p] such that [n = 2p+1]
 
156
 
 
157
    (Immediate: it is [n/2]) *)
 
158
 
 
159
Lemma even_2n : forall n, even n -> {p : nat | n = double p}.
 
160
Proof.
 
161
  intros n H. exists (div2 n). auto with arith.
 
162
Defined.
 
163
 
 
164
Lemma odd_S2n : forall n, odd n -> {p : nat | n = S (double p)}.
 
165
Proof.
 
166
  intros n H. exists (div2 n). auto with arith.
 
167
Defined.
 
168
 
 
169
(** Doubling before dividing by two brings back to the initial number. *)
 
170
 
 
171
Lemma div2_double : forall n:nat, div2 (2*n) = n.
 
172
Proof.
 
173
  induction n.
 
174
  simpl; auto.
 
175
  simpl.
 
176
  replace (n+S(n+0)) with (S (2*n)).
 
177
  f_equal; auto.
 
178
  simpl; auto with arith.
 
179
Qed.
 
180
 
 
181
Lemma div2_double_plus_one : forall n:nat, div2 (S (2*n)) = n.
 
182
Proof.
 
183
  induction n.
 
184
  simpl; auto.
 
185
  simpl.
 
186
  replace (n+S(n+0)) with (S (2*n)).
 
187
  f_equal; auto.
 
188
  simpl; auto with arith.
 
189
Qed.