~ubuntu-branches/ubuntu/hardy/coq-doc/hardy

<code class="keyword">Definition</code> <a name="Zpower_nat"></a>Zpower_nat (z:<a href="Coq.ZArith.BinInt.html#Z">Z</a>) (n:<a href="Coq.Init.Datatypes.html#nat">nat</a>) := <a href="Coq.ZArith.Zmisc.html#iter_nat">iter_nat</a> n <a href="Coq.ZArith.BinInt.html#Z">Z</a> (fun x:<a href="Coq.ZArith.BinInt.html#Z">Z</a> => z * x) 1.

</code>

<code>Zpower_nat_is_exp</code> says <code>Zpower_nat</code> is a morphism for

<code>plus : nat->nat</code> and <code>Zmult : Z->Z</code>

</td></tr></table>

<code>

<code class="keyword">Lemma</code> <a name="Zpower_nat_is_exp"></a>Zpower_nat_is_exp :

forall (n m:<a href="Coq.Init.Datatypes.html#nat">nat</a>) (z:<a href="Coq.ZArith.BinInt.html#Z">Z</a>),

<a href="Coq.ZArith.Zpower.html#Zpower_nat">Zpower_nat</a> z (n + m) = <a href="Coq.ZArith.Zpower.html#Zpower_nat">Zpower_nat</a> z n * <a href="Coq.ZArith.Zpower.html#Zpower_nat">Zpower_nat</a> z m.

intros; elim n;

 [ simpl in |- *; elim (Zpower_nat z m); auto with zarith

| unfold Zpower_nat in |- *; intros; simpl in |- *; rewrite H;

apply Zmult_assoc ].

<code class="keyword">Qed</code>.

</code>

<code>Zpower_pos z n</code> is the n-th power of <code>z</code> when <code>n</code> is an binary

integer (type <code>positive</code>) and <code>z</code> a signed integer (type <code>Z</code>)

</td></tr></table>

<code>

<code class="keyword">Definition</code> <a name="Zpower_pos"></a>Zpower_pos (z:<a href="Coq.ZArith.BinInt.html#Z">Z</a>) (n:<a href="Coq.NArith.BinPos.html#positive">positive</a>) := <a href="Coq.ZArith.Zmisc.html#iter_pos">iter_pos</a> n <a href="Coq.ZArith.BinInt.html#Z">Z</a> (fun x:<a href="Coq.ZArith.BinInt.html#Z">Z</a> => z * x) 1.

</code>

This theorem shows that powers of unary and binary integers

are the same thing, modulo the function convert : <code>positive -> nat</code>

</td></tr></table>

<code>

<code class="keyword">Theorem</code> <a name="Zpower_pos_nat"></a>Zpower_pos_nat :

forall (z:<a href="Coq.ZArith.BinInt.html#Z">Z</a>) (p:<a href="Coq.NArith.BinPos.html#positive">positive</a>), <a href="Coq.ZArith.Zpower.html#Zpower_pos">Zpower_pos</a> z p = <a href="Coq.ZArith.Zpower.html#Zpower_nat">Zpower_nat</a> z (<a href="Coq.NArith.BinPos.html#nat_of_P">nat_of_P</a> p).

intros; unfold Zpower_pos in |- *; unfold Zpower_nat in |- *;

apply <a href="Coq.ZArith.Zmisc.html#iter_nat_of_P">iter_nat_of_P</a>.

<code class="keyword">Qed</code>.

</code>

Using the theorem <code>Zpower_pos_nat</code> and the lemma <code>Zpower_nat_is_exp</code> we

deduce that the function <code>[n:positive](Zpower_pos z n)</code> is a morphism

for <code>add : positive->positive</code> and <code>Zmult : Z->Z</code>

</td></tr></table>

<code>

<code class="keyword">Theorem</code> <a name="Zpower_pos_is_exp"></a>Zpower_pos_is_exp :

forall (n m:<a href="Coq.NArith.BinPos.html#positive">positive</a>) (z:<a href="Coq.ZArith.BinInt.html#Z">Z</a>),

<a href="Coq.ZArith.Zpower.html#Zpower_pos">Zpower_pos</a> z (n + m) = <a href="Coq.ZArith.Zpower.html#Zpower_pos">Zpower_pos</a> z n * <a href="Coq.ZArith.Zpower.html#Zpower_pos">Zpower_pos</a> z m.

intros.

rewrite (<a href="Coq.ZArith.Zpower.html#Zpower_pos_nat">Zpower_pos_nat</a> z n).

100

rewrite (<a href="Coq.ZArith.Zpower.html#Zpower_pos_nat">Zpower_pos_nat</a> z m).

101

rewrite (<a href="Coq.ZArith.Zpower.html#Zpower_pos_nat">Zpower_pos_nat</a> z (n + m)).

102

rewrite (<a href="Coq.NArith.Pnat.html#nat_of_P_plus_morphism">nat_of_P_plus_morphism</a> n m).

103

apply <a href="Coq.ZArith.Zpower.html#Zpower_nat_is_exp">Zpower_nat_is_exp</a>.

104

<code class="keyword">Qed</code>.

105

106

107

<code class="keyword">Definition</code> <a name="Zpower"></a>Zpower (x y:<a href="Coq.ZArith.BinInt.html#Z">Z</a>) :=

108

match y with

109

| <a href="Coq.ZArith.BinInt.html#Zpos">Zpos</a> p => <a href="Coq.ZArith.Zpower.html#Zpower_pos">Zpower_pos</a> x p

110

| <a href="Coq.ZArith.BinInt.html#Z0">Z0</a> => 1

111

| <a href="Coq.ZArith.BinInt.html#Zneg">Zneg</a> p => 0

112

end.

113

114

115

<code class="keyword">Infix</code> "^" := <a href="Coq.ZArith.Zpower.html#Zpower">Zpower</a> : Z_scope.

116

117

118

<code class="keyword">Hint</code> <code class="keyword">Immediate</code> <a href="Coq.ZArith.Zpower.html#Zpower_nat_is_exp">Zpower_nat_is_exp</a>: zarith.

119

<code class="keyword">Hint</code> <code class="keyword">Immediate</code> <a href="Coq.ZArith.Zpower.html#Zpower_pos_is_exp">Zpower_pos_is_exp</a>: zarith.

120

<code class="keyword">Hint</code> Unfold Zpower_pos: zarith.

121

<code class="keyword">Hint</code> Unfold Zpower_nat: zarith.

122

123

124

<code class="keyword">Lemma</code> <a name="Zpower_exp"></a>Zpower_exp :

125

forall x n m:<a href="Coq.ZArith.BinInt.html#Z">Z</a>, n >= 0 -> m >= 0 -> x ^ (n + m) = x ^ n * x ^ m.

126

destruct n; destruct m; auto with zarith.

127

simpl in |- *; intros; apply <a href="Coq.ZArith.auxiliary.html#Zred_factor0">Zred_factor0</a>.

128

simpl in |- *; auto with zarith.

129

intros; compute in H0; absurd (Datatypes.Lt = Datatypes.Lt); auto with zarith.

130

intros; compute in H0; absurd (Datatypes.Lt = Datatypes.Lt); auto with zarith.

131

<code class="keyword">Qed</code>.

132

133

134

<code class="keyword">End</code> section1.

135

136

137

<code class="keyword">Infix</code> "^" := <a href="Coq.ZArith.Zpower.html#Zpower">Zpower</a> : Z_scope.

138

139

140

<code class="keyword">Hint</code> <code class="keyword">Immediate</code> <a href="Coq.ZArith.Zpower.html#Zpower_nat_is_exp">Zpower_nat_is_exp</a>: zarith.

141

<code class="keyword">Hint</code> <code class="keyword">Immediate</code> <a href="Coq.ZArith.Zpower.html#Zpower_pos_is_exp">Zpower_pos_is_exp</a>: zarith.

142

<code class="keyword">Hint</code> Unfold Zpower_pos: zarith.

143

<code class="keyword">Hint</code> Unfold Zpower_nat: zarith.

144

145

146

<code class="keyword">Section</code> Powers_of_2.

147

148

149

</code>

150

151

152

For the powers of two, that will be widely used, a more direct

153

calculus is possible. We will also prove some properties such

154

as <code>(x:positive) x < 2^x</code> that are true for all integers bigger

155

than 2 but more difficult to prove and useless.

156

</td></tr></table>

157

<code>

158

159

160

</code>

161

162

163

<code>shift n m</code> computes <code>2^n * m</code>, or <code>m</code> shifted by <code>n</code> positions

164

</td></tr></table>

165

<code>

166

167

168

<code class="keyword">Definition</code> <a name="shift_nat"></a>shift_nat (n:<a href="Coq.Init.Datatypes.html#nat">nat</a>) (z:<a href="Coq.NArith.BinPos.html#positive">positive</a>) := <a href="Coq.ZArith.Zmisc.html#iter_nat">iter_nat</a> n <a href="Coq.NArith.BinPos.html#positive">positive</a> <a href="Coq.NArith.BinPos.html#xO">xO</a> z.

169

<code class="keyword">Definition</code> <a name="shift_pos"></a>shift_pos (n z:<a href="Coq.NArith.BinPos.html#positive">positive</a>) := <a href="Coq.ZArith.Zmisc.html#iter_pos">iter_pos</a> n <a href="Coq.NArith.BinPos.html#positive">positive</a> <a href="Coq.NArith.BinPos.html#xO">xO</a> z.

170

<code class="keyword">Definition</code> <a name="shift"></a>shift (n:<a href="Coq.ZArith.BinInt.html#Z">Z</a>) (z:<a href="Coq.NArith.BinPos.html#positive">positive</a>) :=

171

match n with

172

| <a href="Coq.ZArith.BinInt.html#Z0">Z0</a> => z

173

| <a href="Coq.ZArith.BinInt.html#Zpos">Zpos</a> p => <a href="Coq.ZArith.Zmisc.html#iter_pos">iter_pos</a> p <a href="Coq.NArith.BinPos.html#positive">positive</a> <a href="Coq.NArith.BinPos.html#xO">xO</a> z

174

| <a href="Coq.ZArith.BinInt.html#Zneg">Zneg</a> p => z

175

end.

176

177

178

<code class="keyword">Definition</code> <a name="two_power_nat"></a>two_power_nat (n:<a href="Coq.Init.Datatypes.html#nat">nat</a>) := <a href="Coq.ZArith.BinInt.html#Zpos">Zpos</a> (<a href="Coq.ZArith.Zpower.html#shift_nat">shift_nat</a> n 1).

179

<code class="keyword">Definition</code> <a name="two_power_pos"></a>two_power_pos (x:<a href="Coq.NArith.BinPos.html#positive">positive</a>) := <a href="Coq.ZArith.BinInt.html#Zpos">Zpos</a> (<a href="Coq.ZArith.Zpower.html#shift_pos">shift_pos</a> x 1).

180

181

182

<code class="keyword">Lemma</code> <a name="two_power_nat_S"></a>two_power_nat_S :

183

forall n:<a href="Coq.Init.Datatypes.html#nat">nat</a>, <a href="Coq.ZArith.Zpower.html#two_power_nat">two_power_nat</a> (<a href="Coq.Init.Datatypes.html#S">S</a> n) = 2 * <a href="Coq.ZArith.Zpower.html#two_power_nat">two_power_nat</a> n.

184

intro; simpl in |- *; apply <a href="Coq.Init.Logic.html#refl_equal">refl_equal</a>.

185

<code class="keyword">Qed</code>.

186

187

188

<code class="keyword">Lemma</code> <a name="shift_nat_plus"></a>shift_nat_plus :

189

forall (n m:<a href="Coq.Init.Datatypes.html#nat">nat</a>) (x:<a href="Coq.NArith.BinPos.html#positive">positive</a>),

190

<a href="Coq.ZArith.Zpower.html#shift_nat">shift_nat</a> (n + m) x = <a href="Coq.ZArith.Zpower.html#shift_nat">shift_nat</a> n (<a href="Coq.ZArith.Zpower.html#shift_nat">shift_nat</a> m x).

191

192

193

intros; unfold shift_nat in |- *; apply <a href="Coq.ZArith.Zmisc.html#iter_nat_plus">iter_nat_plus</a>.

194

<code class="keyword">Qed</code>.

195

196

197

<code class="keyword">Theorem</code> <a name="shift_nat_correct"></a>shift_nat_correct :

198

forall (n:<a href="Coq.Init.Datatypes.html#nat">nat</a>) (x:<a href="Coq.NArith.BinPos.html#positive">positive</a>), <a href="Coq.ZArith.BinInt.html#Zpos">Zpos</a> (<a href="Coq.ZArith.Zpower.html#shift_nat">shift_nat</a> n x) = <a href="Coq.ZArith.Zpower.html#Zpower_nat">Zpower_nat</a> 2 n * <a href="Coq.ZArith.BinInt.html#Zpos">Zpos</a> x.

199

200

201

unfold shift_nat in |- *; simple induction n;

202

[ simpl in |- *; trivial with zarith

203

| intros; replace (<a href="Coq.ZArith.Zpower.html#Zpower_nat">Zpower_nat</a> 2 (<a href="Coq.Init.Datatypes.html#S">S</a> n0)) with (2 * <a href="Coq.ZArith.Zpower.html#Zpower_nat">Zpower_nat</a> 2 n0);

204

[ rewrite <- Zmult_assoc; rewrite <- (H x); simpl in |- *; reflexivity

205

| auto with zarith ] ].

206

<code class="keyword">Qed</code>.

207

208

209

<code class="keyword">Theorem</code> <a name="two_power_nat_correct"></a>two_power_nat_correct :

210

forall n:<a href="Coq.Init.Datatypes.html#nat">nat</a>, <a href="Coq.ZArith.Zpower.html#two_power_nat">two_power_nat</a> n = <a href="Coq.ZArith.Zpower.html#Zpower_nat">Zpower_nat</a> 2 n.

211

212

213

intro n.

214

unfold two_power_nat in |- *.

215

rewrite (<a href="Coq.ZArith.Zpower.html#shift_nat_correct">shift_nat_correct</a> n).

216

omega.

217

<code class="keyword">Qed</code>.

218

219

</code>

220

221

222

Second we show that <code>two_power_pos</code> and <code>two_power_nat</code> are the same

223

</td></tr></table>

224

<code>

225

<code class="keyword">Lemma</code> <a name="shift_pos_nat"></a>shift_pos_nat :

226

forall p x:<a href="Coq.NArith.BinPos.html#positive">positive</a>, <a href="Coq.ZArith.Zpower.html#shift_pos">shift_pos</a> p x = <a href="Coq.ZArith.Zpower.html#shift_nat">shift_nat</a> (<a href="Coq.NArith.BinPos.html#nat_of_P">nat_of_P</a> p) x.

227

228

229

unfold shift_pos in |- *.

230

unfold shift_nat in |- *.

231

intros; apply <a href="Coq.ZArith.Zmisc.html#iter_nat_of_P">iter_nat_of_P</a>.

232

<code class="keyword">Qed</code>.

233

234

235

<code class="keyword">Lemma</code> <a name="two_power_pos_nat"></a>two_power_pos_nat :

236

forall p:<a href="Coq.NArith.BinPos.html#positive">positive</a>, <a href="Coq.ZArith.Zpower.html#two_power_pos">two_power_pos</a> p = <a href="Coq.ZArith.Zpower.html#two_power_nat">two_power_nat</a> (<a href="Coq.NArith.BinPos.html#nat_of_P">nat_of_P</a> p).

237

238

239

intro; unfold two_power_pos in |- *; unfold two_power_nat in |- *.

240

apply <a href="Coq.Init.Logic.html#f_equal">f_equal</a> with (f:= <a href="Coq.ZArith.BinInt.html#Zpos">Zpos</a>).

241

apply <a href="Coq.ZArith.Zpower.html#shift_pos_nat">shift_pos_nat</a>.

242

<code class="keyword">Qed</code>.

243

244

245

</code>

246

247

248

Then we deduce that <code>two_power_pos</code> is also correct

249

</td></tr></table>

250

<code>

251

252

253

<code class="keyword">Theorem</code> <a name="shift_pos_correct"></a>shift_pos_correct :

254

forall p x:<a href="Coq.NArith.BinPos.html#positive">positive</a>, <a href="Coq.ZArith.BinInt.html#Zpos">Zpos</a> (<a href="Coq.ZArith.Zpower.html#shift_pos">shift_pos</a> p x) = <a href="Coq.ZArith.Zpower.html#Zpower_pos">Zpower_pos</a> 2 p * <a href="Coq.ZArith.BinInt.html#Zpos">Zpos</a> x.

255

256

257

intros.

258

rewrite (<a href="Coq.ZArith.Zpower.html#shift_pos_nat">shift_pos_nat</a> p x).

259

rewrite (<a href="Coq.ZArith.Zpower.html#Zpower_pos_nat">Zpower_pos_nat</a> 2 p).

260

apply <a href="Coq.ZArith.Zpower.html#shift_nat_correct">shift_nat_correct</a>.

261

<code class="keyword">Qed</code>.

262

263

264

<code class="keyword">Theorem</code> <a name="two_power_pos_correct"></a>two_power_pos_correct :

265

forall x:<a href="Coq.NArith.BinPos.html#positive">positive</a>, <a href="Coq.ZArith.Zpower.html#two_power_pos">two_power_pos</a> x = <a href="Coq.ZArith.Zpower.html#Zpower_pos">Zpower_pos</a> 2 x.

266

267

268

intro.

269

rewrite <a href="Coq.ZArith.Zpower.html#two_power_pos_nat">two_power_pos_nat</a>.

270

rewrite <a href="Coq.ZArith.Zpower.html#Zpower_pos_nat">Zpower_pos_nat</a>.

271

apply <a href="Coq.ZArith.Zpower.html#two_power_nat_correct">two_power_nat_correct</a>.

272

<code class="keyword">Qed</code>.

273

274

275

</code>

276

277

278

Some consequences

279

</td></tr></table>

280

<code>

281

282

283

<code class="keyword">Theorem</code> <a name="two_power_pos_is_exp"></a>two_power_pos_is_exp :

284

forall x y:<a href="Coq.NArith.BinPos.html#positive">positive</a>,

285

<a href="Coq.ZArith.Zpower.html#two_power_pos">two_power_pos</a> (x + y) = <a href="Coq.ZArith.Zpower.html#two_power_pos">two_power_pos</a> x * <a href="Coq.ZArith.Zpower.html#two_power_pos">two_power_pos</a> y.

286

intros.

287

rewrite (<a href="Coq.ZArith.Zpower.html#two_power_pos_correct">two_power_pos_correct</a> (x + y)).

288

rewrite (<a href="Coq.ZArith.Zpower.html#two_power_pos_correct">two_power_pos_correct</a> x).

289

rewrite (<a href="Coq.ZArith.Zpower.html#two_power_pos_correct">two_power_pos_correct</a> y).

290

apply <a href="Coq.ZArith.Zpower.html#Zpower_pos_is_exp">Zpower_pos_is_exp</a>.

291

<code class="keyword">Qed</code>.

292

293

294

</code>

295

296

297

The exponentiation <code>z -> 2^z</code> for <code>z</code> a signed integer.

298

For convenience, we assume that <code>2^z = 0</code> for all <code>z < 0</code>

299

We could also define a inductive type <code>Log_result</code> with

300

3 contructors <code> Zero | Pos positive -> | minus_infty</code>

301

but it's more complexe and not so useful.

302

</td></tr></table>

303

<code>

304

305

<code class="keyword">Definition</code> <a name="two_p"></a>two_p (x:<a href="Coq.ZArith.BinInt.html#Z">Z</a>) :=

306

match x with

307

| <a href="Coq.ZArith.BinInt.html#Z0">Z0</a> => 1

308

| <a href="Coq.ZArith.BinInt.html#Zpos">Zpos</a> y => <a href="Coq.ZArith.Zpower.html#two_power_pos">two_power_pos</a> y

309

| <a href="Coq.ZArith.BinInt.html#Zneg">Zneg</a> y => 0

310

end.

311

312

313

<code class="keyword">Theorem</code> <a name="two_p_is_exp"></a>two_p_is_exp :

314

forall x y:<a href="Coq.ZArith.BinInt.html#Z">Z</a>, 0 <= x -> 0 <= y -> <a href="Coq.ZArith.Zpower.html#two_p">two_p</a> (x + y) = <a href="Coq.ZArith.Zpower.html#two_p">two_p</a> x * <a href="Coq.ZArith.Zpower.html#two_p">two_p</a> y.

315

simple induction x;

316

[ simple induction y; simpl in |- *; auto with zarith

317

| simple induction y;

318

    [ unfold two_p in |- *; rewrite (Zmult_comm (two_power_pos p) 1);

319

rewrite (Zmult_1_l (two_power_pos p)); auto with zarith

320

| unfold Zplus in |- *; unfold two_p in |- *; intros;

321

apply two_power_pos_is_exp

322

| intros; unfold Zle in H0; unfold Zcompare in H0;

323

absurd (Datatypes.Gt = Datatypes.Gt); trivial with zarith ]

324

| simple induction y;

325

    [ simpl in |- *; auto with zarith

326

| intros; unfold Zle in H; unfold Zcompare in H;

327

absurd (Datatypes.Gt = Datatypes.Gt); trivial with zarith

328

| intros; unfold Zle in H; unfold Zcompare in H;

329

absurd (Datatypes.Gt = Datatypes.Gt); trivial with zarith ] ].

330

<code class="keyword">Qed</code>.

331

332

333

<code class="keyword">Lemma</code> <a name="two_p_gt_ZERO"></a>two_p_gt_ZERO : forall x:<a href="Coq.ZArith.BinInt.html#Z">Z</a>, 0 <= x -> <a href="Coq.ZArith.Zpower.html#two_p">two_p</a> x > 0.

334

simple induction x; intros;

335

[ simpl in |- *; omega

336

| simpl in |- *; unfold two_power_pos in |- *; apply Zorder.Zgt_pos_0

337

| absurd (0 <= <a href="Coq.ZArith.BinInt.html#Zneg">Zneg</a> p);

338

    [ simpl in |- *; unfold Zle in |- *; unfold Zcompare in |- *;

339

do 2 unfold not in |- *; auto with zarith

340

| assumption ] ].

341

<code class="keyword">Qed</code>.

342

343

344

<code class="keyword">Lemma</code> <a name="two_p_S"></a>two_p_S : forall x:<a href="Coq.ZArith.BinInt.html#Z">Z</a>, 0 <= x -> <a href="Coq.ZArith.Zpower.html#two_p">two_p</a> (<a href="Coq.ZArith.BinInt.html#Zsucc">Zsucc</a> x) = 2 * <a href="Coq.ZArith.Zpower.html#two_p">two_p</a> x.

345

intros; unfold Zsucc in |- *.

346

rewrite (<a href="Coq.ZArith.Zpower.html#two_p_is_exp">two_p_is_exp</a> x 1 H (Zorder.Zle_0_pos 1)).

347

apply <a href="Coq.ZArith.BinInt.html#Zmult_comm">Zmult_comm</a>.

348

<code class="keyword">Qed</code>.

349

350

351

<code class="keyword">Lemma</code> <a name="two_p_pred"></a>two_p_pred : forall x:<a href="Coq.ZArith.BinInt.html#Z">Z</a>, 0 <= x -> <a href="Coq.ZArith.Zpower.html#two_p">two_p</a> (<a href="Coq.ZArith.BinInt.html#Zpred">Zpred</a> x) < <a href="Coq.ZArith.Zpower.html#two_p">two_p</a> x.

352

intros; apply <a href="Coq.ZArith.Wf_Z.html#natlike_ind">natlike_ind</a> with (P:= fun x:<a href="Coq.ZArith.BinInt.html#Z">Z</a> => <a href="Coq.ZArith.Zpower.html#two_p">two_p</a> (<a href="Coq.ZArith.BinInt.html#Zpred">Zpred</a> x) < <a href="Coq.ZArith.Zpower.html#two_p">two_p</a> x);

353

[ simpl in |- *; unfold Zlt in |- *; auto with zarith

354

| intros; elim (<a href="Coq.ZArith.Zorder.html#Zle_lt_or_eq">Zle_lt_or_eq</a> 0 x0 H0);

355

[ intros;

356

replace (<a href="Coq.ZArith.Zpower.html#two_p">two_p</a> (<a href="Coq.ZArith.BinInt.html#Zpred">Zpred</a> (<a href="Coq.ZArith.BinInt.html#Zsucc">Zsucc</a> x0))) with (<a href="Coq.ZArith.Zpower.html#two_p">two_p</a> (<a href="Coq.ZArith.BinInt.html#Zsucc">Zsucc</a> (<a href="Coq.ZArith.BinInt.html#Zpred">Zpred</a> x0)));

357

[ rewrite (<a href="Coq.ZArith.Zpower.html#two_p_S">two_p_S</a> (<a href="Coq.ZArith.BinInt.html#Zpred">Zpred</a> x0));

358

[ rewrite (<a href="Coq.ZArith.Zpower.html#two_p_S">two_p_S</a> x0); [ omega | assumption ]

359

| apply Zorder.Zlt_0_le_0_pred; assumption ]

360

| rewrite <- (<a href="Coq.ZArith.BinInt.html#Zsucc_pred">Zsucc_pred</a> x0); rewrite <- (<a href="Coq.ZArith.BinInt.html#Zpred_succ">Zpred_succ</a> x0);

361

trivial with zarith ]

362

| intro Hx0; rewrite <- Hx0; simpl in |- *; unfold Zlt in |- *;

363

auto with zarith ]

364

| assumption ].

365

<code class="keyword">Qed</code>.

366

367

368

<code class="keyword">Lemma</code> <a name="Zlt_lt_double"></a>Zlt_lt_double : forall x y:<a href="Coq.ZArith.BinInt.html#Z">Z</a>, 0 <= x < y -> x < 2 * y.

369

intros; omega. <code class="keyword">Qed</code>.

370

371

372

<code class="keyword">End</code> Powers_of_2.

373

374

375

<code class="keyword">Hint</code> Resolve <a href="Coq.ZArith.Zpower.html#two_p_gt_ZERO">two_p_gt_ZERO</a>: zarith.

376

<code class="keyword">Hint</code> <code class="keyword">Immediate</code> <a href="Coq.ZArith.Zpower.html#two_p_pred">two_p_pred</a> <a href="Coq.ZArith.Zpower.html#two_p_S">two_p_S</a>: zarith.

377

378

379

<code class="keyword">Section</code> power_div_with_rest.

380

381

382

</code>

383

384

385

Division by a power of two.

386

To <code>n:Z</code> and <code>p:positive</code>, <code>q</code>,<code>r</code> are associated such that

387

388

</td></tr></table>

389

<code>

390

391

392

</code>

393

394

395

Invariant: <code>d*q + r = d'*q + r /\ d' = 2*d /\ 0<= r < d /\ 0 <= r' < d'</code>

396

</td></tr></table>

397

<code>

398

<code class="keyword">Definition</code> <a name="Zdiv_rest_aux"></a>Zdiv_rest_aux (qrd:<a href="Coq.ZArith.BinInt.html#Z">Z</a> * <a href="Coq.ZArith.BinInt.html#Z">Z</a> * <a href="Coq.ZArith.BinInt.html#Z">Z</a>) :=

399

let (qr, d) := qrd in

400

let (q, r) := qr in

401

(match q with

402

| <a href="Coq.ZArith.BinInt.html#Z0">Z0</a> => (0, r)

403

| <a href="Coq.ZArith.BinInt.html#Zpos">Zpos</a> <a href="Coq.NArith.BinPos.html#xH">xH</a> => (0, d + r)

404

| <a href="Coq.ZArith.BinInt.html#Zpos">Zpos</a> (<a href="Coq.NArith.BinPos.html#xI">xI</a> n) => (<a href="Coq.ZArith.BinInt.html#Zpos">Zpos</a> n, d + r)

405

| <a href="Coq.ZArith.BinInt.html#Zpos">Zpos</a> (<a href="Coq.NArith.BinPos.html#xO">xO</a> n) => (<a href="Coq.ZArith.BinInt.html#Zpos">Zpos</a> n, r)

406

| <a href="Coq.ZArith.BinInt.html#Zneg">Zneg</a> <a href="Coq.NArith.BinPos.html#xH">xH</a> => (-1, d + r)

407

| <a href="Coq.ZArith.BinInt.html#Zneg">Zneg</a> (<a href="Coq.NArith.BinPos.html#xI">xI</a> n) => (<a href="Coq.ZArith.BinInt.html#Zneg">Zneg</a> n - 1, d + r)

408

| <a href="Coq.ZArith.BinInt.html#Zneg">Zneg</a> (<a href="Coq.NArith.BinPos.html#xO">xO</a> n) => (<a href="Coq.ZArith.BinInt.html#Zneg">Zneg</a> n, r)

409

end, 2 * d).

410

411

412

<code class="keyword">Definition</code> <a name="Zdiv_rest"></a>Zdiv_rest (x:<a href="Coq.ZArith.BinInt.html#Z">Z</a>) (p:<a href="Coq.NArith.BinPos.html#positive">positive</a>) :=

413

let (qr, d) := <a href="Coq.ZArith.Zmisc.html#iter_pos">iter_pos</a> p _ <a href="Coq.ZArith.Zpower.html#Zdiv_rest_aux">Zdiv_rest_aux</a> (x, 0, 1) in qr.

414

415

416

<code class="keyword">Lemma</code> <a name="Zdiv_rest_correct1"></a>Zdiv_rest_correct1 :

417

forall (x:<a href="Coq.ZArith.BinInt.html#Z">Z</a>) (p:<a href="Coq.NArith.BinPos.html#positive">positive</a>),

418

let (qr, d) := <a href="Coq.ZArith.Zmisc.html#iter_pos">iter_pos</a> p _ <a href="Coq.ZArith.Zpower.html#Zdiv_rest_aux">Zdiv_rest_aux</a> (x, 0, 1) in d = <a href="Coq.ZArith.Zpower.html#two_power_pos">two_power_pos</a> p.

419

420

421

intros x p; rewrite (<a href="Coq.ZArith.Zmisc.html#iter_nat_of_P">iter_nat_of_P</a> p _ <a href="Coq.ZArith.Zpower.html#Zdiv_rest_aux">Zdiv_rest_aux</a> (x, 0, 1));

422

rewrite (<a href="Coq.ZArith.Zpower.html#two_power_pos_nat">two_power_pos_nat</a> p); elim (<a href="Coq.NArith.BinPos.html#nat_of_P">nat_of_P</a> p);

423

simpl in |- *;

424

[ trivial with zarith

425

| intro n; rewrite (<a href="Coq.ZArith.Zpower.html#two_power_nat_S">two_power_nat_S</a> n); unfold Zdiv_rest_aux at 2 in |- *;

426

elim (<a href="Coq.ZArith.Zmisc.html#iter_nat">iter_nat</a> n (<a href="Coq.ZArith.BinInt.html#Z">Z</a> * <a href="Coq.ZArith.BinInt.html#Z">Z</a> * <a href="Coq.ZArith.BinInt.html#Z">Z</a>) <a href="Coq.ZArith.Zpower.html#Zdiv_rest_aux">Zdiv_rest_aux</a> (x, 0, 1));

427

destruct a; intros; apply <a href="Coq.Init.Logic.html#f_equal">f_equal</a> with (f:= fun z:<a href="Coq.ZArith.BinInt.html#Z">Z</a> => 2 * z);

428

assumption ].

429

<code class="keyword">Qed</code>.

430

431

432

<code class="keyword">Lemma</code> <a name="Zdiv_rest_correct2"></a>Zdiv_rest_correct2 :

433

forall (x:<a href="Coq.ZArith.BinInt.html#Z">Z</a>) (p:<a href="Coq.NArith.BinPos.html#positive">positive</a>),

434

let (qr, d) := <a href="Coq.ZArith.Zmisc.html#iter_pos">iter_pos</a> p _ <a href="Coq.ZArith.Zpower.html#Zdiv_rest_aux">Zdiv_rest_aux</a> (x, 0, 1) in

435

let (q, r) := qr in x = q * d + r /\ 0 <= r < d.

436

437

438

intros;

439

apply <a href="Coq.ZArith.Zmisc.html#iter_pos_invariant">iter_pos_invariant</a> with

440

(f:= <a href="Coq.ZArith.Zpower.html#Zdiv_rest_aux">Zdiv_rest_aux</a>)

441

(Inv:= fun qrd:<a href="Coq.ZArith.BinInt.html#Z">Z</a> * <a href="Coq.ZArith.BinInt.html#Z">Z</a> * <a href="Coq.ZArith.BinInt.html#Z">Z</a> =>

442

let (qr, d) := qrd in

443

let (q, r) := qr in x = q * d + r /\ 0 <= r < d);

444

[ intro x0; elim x0; intro y0; elim y0; intros q r d;

445

unfold Zdiv_rest_aux in |- *; elim q;

446

[ omega

447

| destruct p0;

448

[ rewrite BinInt.Zpos_xI; intro; elim H; intros; split;

449

          [ rewrite H0; rewrite Zplus_assoc; rewrite Zmult_plus_distr_l;

450

rewrite Zmult_1_l; rewrite Zmult_assoc;

451

rewrite (Zmult_comm (Zpos p0) 2); apply refl_equal

452

| omega ]

453

| rewrite BinInt.Zpos_xO; intro; elim H; intros; split;

454

          [ rewrite H0; rewrite Zmult_assoc; rewrite (Zmult_comm (Zpos p0) 2);

455

apply refl_equal

456

| omega ]

457

| omega ]

458

| destruct p0;

459

[ rewrite BinInt.Zneg_xI; unfold Zminus in |- *; intro; elim H; intros;

460

split;

461

[ rewrite H0; rewrite <a href="Coq.ZArith.BinInt.html#Zplus_assoc">Zplus_assoc</a>;

462

apply <a href="Coq.Init.Logic.html#f_equal">f_equal</a> with (f:= fun z:<a href="Coq.ZArith.BinInt.html#Z">Z</a> => z + r);

463

do 2 rewrite <a href="Coq.ZArith.BinInt.html#Zmult_plus_distr_l">Zmult_plus_distr_l</a>; rewrite <a href="Coq.ZArith.BinInt.html#Zmult_assoc">Zmult_assoc</a>;

464

rewrite (<a href="Coq.ZArith.BinInt.html#Zmult_comm">Zmult_comm</a> (<a href="Coq.ZArith.BinInt.html#Zneg">Zneg</a> p0) 2); rewrite <- <a href="Coq.ZArith.BinInt.html#Zplus_assoc">Zplus_assoc</a>;

465

apply <a href="Coq.Init.Logic.html#f_equal">f_equal</a> with (f:= fun z:<a href="Coq.ZArith.BinInt.html#Z">Z</a> => 2 * <a href="Coq.ZArith.BinInt.html#Zneg">Zneg</a> p0 * d + z);

466

omega

467

| omega ]

468

| rewrite BinInt.Zneg_xO; unfold Zminus in |- *; intro; elim H; intros;

469

split;

470

          [ rewrite H0; rewrite Zmult_assoc; rewrite (Zmult_comm (Zneg p0) 2);

471

apply refl_equal

472

| omega ]

473

| omega ] ]

474

| omega ].

475

<code class="keyword">Qed</code>.

476

477

478

<code class="keyword">Inductive</code> <a name="Zdiv_rest_proofs"></a>Zdiv_rest_proofs (x:<a href="Coq.ZArith.BinInt.html#Z">Z</a>) (p:<a href="Coq.NArith.BinPos.html#positive">positive</a>) : Set :=

479

<a name="Zdiv_rest_proof"></a>Zdiv_rest_proof :

480

forall q r:<a href="Coq.ZArith.BinInt.html#Z">Z</a>,

481

x = q * <a href="Coq.ZArith.Zpower.html#two_power_pos">two_power_pos</a> p + r ->

482

0 <= r -> r < <a href="Coq.ZArith.Zpower.html#two_power_pos">two_power_pos</a> p -> Zdiv_rest_proofs x p.

483

484

485

<code class="keyword">Lemma</code> <a name="Zdiv_rest_correct"></a>Zdiv_rest_correct : forall (x:<a href="Coq.ZArith.BinInt.html#Z">Z</a>) (p:<a href="Coq.NArith.BinPos.html#positive">positive</a>), <a href="Coq.ZArith.Zpower.html#Zdiv_rest_proofs">Zdiv_rest_proofs</a> x p.

486

intros x p.

487

generalize (<a href="Coq.ZArith.Zpower.html#Zdiv_rest_correct1">Zdiv_rest_correct1</a> x p); generalize (<a href="Coq.ZArith.Zpower.html#Zdiv_rest_correct2">Zdiv_rest_correct2</a> x p).

488

elim (<a href="Coq.ZArith.Zmisc.html#iter_pos">iter_pos</a> p (<a href="Coq.ZArith.BinInt.html#Z">Z</a> * <a href="Coq.ZArith.BinInt.html#Z">Z</a> * <a href="Coq.ZArith.BinInt.html#Z">Z</a>) <a href="Coq.ZArith.Zpower.html#Zdiv_rest_aux">Zdiv_rest_aux</a> (x, 0, 1)).

489

simple induction a.

490

intros.

491

elim H; intros H1 H2; clear H.

492

rewrite H0 in H1; rewrite H0 in H2; elim H2; intros;

493

apply <a href="Coq.ZArith.Zpower.html#Zdiv_rest_proof">Zdiv_rest_proof</a> with (q:= a0) (r:= b); assumption.

494

<code class="keyword">Qed</code>.

495

496

497

<code class="keyword">End</code> power_div_with_rest.</code>

498

<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://www.lri.fr/~filliatr/coqdoc/">coqdoc</a>

499

</body>

500

</html>

b'\\ No newline at end of file'

Older »