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
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** Nota : this file is OBSOLETE, and left only for compatibility.
Please consider using [Nat.div2] directly, and results about it
(see file PeanoNat). *)
Require Import PeanoNat Even.
Local Open Scope nat_scope.
Implicit Type n : nat.
(** Here we define [n/2] and prove some of its properties *)
Notation div2 := Nat.div2 (only parsing).
(** Since [div2] is recursively defined on [0], [1] and [(S (S n))], it is
useful to prove the corresponding induction principle *)
Lemma ind_0_1_SS :
forall P:nat -> Prop,
P 0 -> P 1 -> (forall n, P n -> P (S (S n))) -> forall n, P n.
Proof.
intros P H0 H1 H2.
fix 1.
destruct n as [|[|n]].
- exact H0.
- exact H1.
- apply H2, ind_0_1_SS.
Qed.
(** [0 <n => n/2 < n] *)
Lemma lt_div2 n : 0 < n -> div2 n < n.
Proof. apply Nat.lt_div2. Qed.
Hint Resolve lt_div2: arith.
(** Properties related to the parity *)
Lemma even_div2 n : even n -> div2 n = div2 (S n).
Proof.
rewrite Even.even_equiv. intros (p,->).
rewrite Nat.div2_succ_double. apply Nat.div2_double.
Qed.
Lemma odd_div2 n : odd n -> S (div2 n) = div2 (S n).
Proof.
rewrite Even.odd_equiv. intros (p,->).
rewrite Nat.add_1_r, Nat.div2_succ_double.
simpl. f_equal. symmetry. apply Nat.div2_double.
Qed.
Lemma div2_even n : div2 n = div2 (S n) -> even n.
Proof.
destruct (even_or_odd n) as [Ev|Od]; trivial.
apply odd_div2 in Od. rewrite <- Od. intro Od'.
elim (n_Sn _ Od').
Qed.
Lemma div2_odd n : S (div2 n) = div2 (S n) -> odd n.
Proof.
destruct (even_or_odd n) as [Ev|Od]; trivial.
apply even_div2 in Ev. rewrite <- Ev. intro Ev'.
symmetry in Ev'. elim (n_Sn _ Ev').
Qed.
Hint Resolve even_div2 div2_even odd_div2 div2_odd: arith.
Lemma even_odd_div2 n :
(even n <-> div2 n = div2 (S n)) /\
(odd n <-> S (div2 n) = div2 (S n)).
Proof.
split; split; auto using div2_odd, div2_even, odd_div2, even_div2.
Qed.
(** Properties related to the double ([2n]) *)
Notation double := Nat.double (only parsing).
Hint Unfold double Nat.double: arith.
Lemma double_S n : double (S n) = S (S (double n)).
Proof.
apply Nat.add_succ_r.
Qed.
Lemma double_plus n m : double (n + m) = double n + double m.
Proof.
apply Nat.add_shuffle1.
Qed.
Hint Resolve double_S: arith.
Lemma even_odd_double n :
(even n <-> n = double (div2 n)) /\ (odd n <-> n = S (double (div2 n))).
Proof.
revert n. fix 1. destruct n as [|[|n]].
- (* n = 0 *)
split; split; auto with arith. inversion 1.
- (* n = 1 *)
split; split; auto with arith. inversion_clear 1. inversion H0.
- (* n = (S (S n')) *)
destruct (even_odd_double n) as ((Ev,Ev'),(Od,Od')).
split; split; simpl div2; rewrite ?double_S.
+ inversion_clear 1. inversion_clear H0. auto.
+ injection 1. auto with arith.
+ inversion_clear 1. inversion_clear H0. auto.
+ injection 1. auto with arith.
Qed.
(** Specializations *)
Lemma even_double n : even n -> n = double (div2 n).
Proof proj1 (proj1 (even_odd_double n)).
Lemma double_even n : n = double (div2 n) -> even n.
Proof proj2 (proj1 (even_odd_double n)).
Lemma odd_double n : odd n -> n = S (double (div2 n)).
Proof proj1 (proj2 (even_odd_double n)).
Lemma double_odd n : n = S (double (div2 n)) -> odd n.
Proof proj2 (proj2 (even_odd_double n)).
Hint Resolve even_double double_even odd_double double_odd: arith.
(** Application:
- if [n] is even then there is a [p] such that [n = 2p]
- if [n] is odd then there is a [p] such that [n = 2p+1]
(Immediate: it is [n/2]) *)
Lemma even_2n : forall n, even n -> {p : nat | n = double p}.
Proof.
intros n H. exists (div2 n). auto with arith.
Defined.
Lemma odd_S2n : forall n, odd n -> {p : nat | n = S (double p)}.
Proof.
intros n H. exists (div2 n). auto with arith.
Defined.
(** Doubling before dividing by two brings back to the initial number. *)
Lemma div2_double n : div2 (2*n) = n.
Proof. apply Nat.div2_double. Qed.
Lemma div2_double_plus_one n : div2 (S (2*n)) = n.
Proof. apply Nat.div2_succ_double. Qed.
|
