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

<code class="keyword">Fixpoint</code> <a name="Psucc"></a>Psucc (x:<a href="Coq.NArith.BinPos.html#positive">positive</a>) : <a href="Coq.NArith.BinPos.html#positive">positive</a> :=

match x with

| <a href="Coq.NArith.BinPos.html#xI">xI</a> x' => <a href="Coq.NArith.BinPos.html#xO">xO</a> (Psucc x')

| <a href="Coq.NArith.BinPos.html#xO">xO</a> x' => <a href="Coq.NArith.BinPos.html#xI">xI</a> x'

| <a href="Coq.NArith.BinPos.html#xH">xH</a> => <a href="Coq.NArith.BinPos.html#xO">xO</a> <a href="Coq.NArith.BinPos.html#xH">xH</a>

end.

</code>

Addition

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

<code>

<code class="keyword">Fixpoint</code> <a name="Pplus"></a>Pplus (x y:<a href="Coq.NArith.BinPos.html#positive">positive</a>) {struct x} : <a href="Coq.NArith.BinPos.html#positive">positive</a> :=

match x, y with

| <a href="Coq.NArith.BinPos.html#xI">xI</a> x', <a href="Coq.NArith.BinPos.html#xI">xI</a> y' => <a href="Coq.NArith.BinPos.html#xO">xO</a> (Pplus_carry x' y')

| <a href="Coq.NArith.BinPos.html#xI">xI</a> x', <a href="Coq.NArith.BinPos.html#xO">xO</a> y' => <a href="Coq.NArith.BinPos.html#xI">xI</a> (Pplus x' y')

| <a href="Coq.NArith.BinPos.html#xI">xI</a> x', <a href="Coq.NArith.BinPos.html#xH">xH</a> => <a href="Coq.NArith.BinPos.html#xO">xO</a> (<a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> x')

| <a href="Coq.NArith.BinPos.html#xO">xO</a> x', <a href="Coq.NArith.BinPos.html#xI">xI</a> y' => <a href="Coq.NArith.BinPos.html#xI">xI</a> (Pplus x' y')

| <a href="Coq.NArith.BinPos.html#xO">xO</a> x', <a href="Coq.NArith.BinPos.html#xO">xO</a> y' => <a href="Coq.NArith.BinPos.html#xO">xO</a> (Pplus x' y')

| <a href="Coq.NArith.BinPos.html#xO">xO</a> x', <a href="Coq.NArith.BinPos.html#xH">xH</a> => <a href="Coq.NArith.BinPos.html#xI">xI</a> x'

| <a href="Coq.NArith.BinPos.html#xH">xH</a>, <a href="Coq.NArith.BinPos.html#xI">xI</a> y' => <a href="Coq.NArith.BinPos.html#xO">xO</a> (<a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> y')

| <a href="Coq.NArith.BinPos.html#xH">xH</a>, <a href="Coq.NArith.BinPos.html#xO">xO</a> y' => <a href="Coq.NArith.BinPos.html#xI">xI</a> y'

| <a href="Coq.NArith.BinPos.html#xH">xH</a>, <a href="Coq.NArith.BinPos.html#xH">xH</a> => <a href="Coq.NArith.BinPos.html#xO">xO</a> <a href="Coq.NArith.BinPos.html#xH">xH</a>

end

with <a name="Pplus_carry"></a>Pplus_carry (x y:<a href="Coq.NArith.BinPos.html#positive">positive</a>) {struct x} : <a href="Coq.NArith.BinPos.html#positive">positive</a> :=

match x, y with

| <a href="Coq.NArith.BinPos.html#xI">xI</a> x', <a href="Coq.NArith.BinPos.html#xI">xI</a> y' => <a href="Coq.NArith.BinPos.html#xI">xI</a> (Pplus_carry x' y')

| <a href="Coq.NArith.BinPos.html#xI">xI</a> x', <a href="Coq.NArith.BinPos.html#xO">xO</a> y' => <a href="Coq.NArith.BinPos.html#xO">xO</a> (Pplus_carry x' y')

| <a href="Coq.NArith.BinPos.html#xI">xI</a> x', <a href="Coq.NArith.BinPos.html#xH">xH</a> => <a href="Coq.NArith.BinPos.html#xI">xI</a> (<a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> x')

| <a href="Coq.NArith.BinPos.html#xO">xO</a> x', <a href="Coq.NArith.BinPos.html#xI">xI</a> y' => <a href="Coq.NArith.BinPos.html#xO">xO</a> (Pplus_carry x' y')

100

| <a href="Coq.NArith.BinPos.html#xO">xO</a> x', <a href="Coq.NArith.BinPos.html#xO">xO</a> y' => <a href="Coq.NArith.BinPos.html#xI">xI</a> (Pplus x' y')

101

| <a href="Coq.NArith.BinPos.html#xO">xO</a> x', <a href="Coq.NArith.BinPos.html#xH">xH</a> => <a href="Coq.NArith.BinPos.html#xO">xO</a> (<a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> x')

102

| <a href="Coq.NArith.BinPos.html#xH">xH</a>, <a href="Coq.NArith.BinPos.html#xI">xI</a> y' => <a href="Coq.NArith.BinPos.html#xI">xI</a> (<a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> y')

103

| <a href="Coq.NArith.BinPos.html#xH">xH</a>, <a href="Coq.NArith.BinPos.html#xO">xO</a> y' => <a href="Coq.NArith.BinPos.html#xO">xO</a> (<a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> y')

104

| <a href="Coq.NArith.BinPos.html#xH">xH</a>, <a href="Coq.NArith.BinPos.html#xH">xH</a> => <a href="Coq.NArith.BinPos.html#xI">xI</a> <a href="Coq.NArith.BinPos.html#xH">xH</a>

105

end.

106

107

108

<code class="keyword">Infix</code> "+" := <a href="Coq.NArith.BinPos.html#Pplus">Pplus</a> : positive_scope.

109

110

111

Open <code class="keyword">Local</code> Scope positive_scope.

112

113

114

</code>

115

116

117

From binary positive numbers to Peano natural numbers

118

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

119

<code>

120

121

122

<code class="keyword">Fixpoint</code> <a name="Pmult_nat"></a>Pmult_nat (x:<a href="Coq.NArith.BinPos.html#positive">positive</a>) (pow2:<a href="Coq.Init.Datatypes.html#nat">nat</a>) {struct x} : <a href="Coq.Init.Datatypes.html#nat">nat</a> :=

123

match x with

124

| <a href="Coq.NArith.BinPos.html#xI">xI</a> x' => (pow2 + Pmult_nat x' (pow2 + pow2))%nat

125

| <a href="Coq.NArith.BinPos.html#xO">xO</a> x' => Pmult_nat x' (pow2 + pow2)%nat

126

| <a href="Coq.NArith.BinPos.html#xH">xH</a> => pow2

127

end.

128

129

130

<code class="keyword">Definition</code> <a name="nat_of_P"></a>nat_of_P (x:<a href="Coq.NArith.BinPos.html#positive">positive</a>) := <a href="Coq.NArith.BinPos.html#Pmult_nat">Pmult_nat</a> x 1.

131

132

133

</code>

134

135

136

From Peano natural numbers to binary positive numbers

137

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

138

<code>

139

140

141

<code class="keyword">Fixpoint</code> <a name="P_of_succ_nat"></a>P_of_succ_nat (n:<a href="Coq.Init.Datatypes.html#nat">nat</a>) : <a href="Coq.NArith.BinPos.html#positive">positive</a> :=

142

match n with

143

| <a href="Coq.Init.Datatypes.html#O">O</a> => <a href="Coq.NArith.BinPos.html#xH">xH</a>

144

| <a href="Coq.Init.Datatypes.html#S">S</a> x' => <a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> (P_of_succ_nat x')

145

end.

146

147

148

</code>

149

150

151

Operation x -> 2*x-1

152

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

153

<code>

154

155

156

<code class="keyword">Fixpoint</code> <a name="Pdouble_minus_one"></a>Pdouble_minus_one (x:<a href="Coq.NArith.BinPos.html#positive">positive</a>) : <a href="Coq.NArith.BinPos.html#positive">positive</a> :=

157

match x with

158

| <a href="Coq.NArith.BinPos.html#xI">xI</a> x' => <a href="Coq.NArith.BinPos.html#xI">xI</a> (<a href="Coq.NArith.BinPos.html#xO">xO</a> x')

159

| <a href="Coq.NArith.BinPos.html#xO">xO</a> x' => <a href="Coq.NArith.BinPos.html#xI">xI</a> (Pdouble_minus_one x')

160

| <a href="Coq.NArith.BinPos.html#xH">xH</a> => <a href="Coq.NArith.BinPos.html#xH">xH</a>

161

end.

162

163

164

</code>

165

166

167

Predecessor

168

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

169

<code>

170

171

172

<code class="keyword">Definition</code> <a name="Ppred"></a>Ppred (x:<a href="Coq.NArith.BinPos.html#positive">positive</a>) :=

173

match x with

174

| <a href="Coq.NArith.BinPos.html#xI">xI</a> x' => <a href="Coq.NArith.BinPos.html#xO">xO</a> x'

175

| <a href="Coq.NArith.BinPos.html#xO">xO</a> x' => <a href="Coq.NArith.BinPos.html#Pdouble_minus_one">Pdouble_minus_one</a> x'

176

| <a href="Coq.NArith.BinPos.html#xH">xH</a> => <a href="Coq.NArith.BinPos.html#xH">xH</a>

177

end.

178

179

180

</code>

181

182

183

An auxiliary type for subtraction

184

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

185

<code>

186

187

188

<code class="keyword">Inductive</code> <a name="positive_mask"></a>positive_mask : Set :=

189

| <a name="IsNul"></a>IsNul : positive_mask

190

| <a name="IsPos"></a>IsPos : <a href="Coq.NArith.BinPos.html#positive">positive</a> -> positive_mask

191

| <a name="IsNeg"></a>IsNeg : positive_mask.

192

193

194

</code>

195

196

197

Operation x -> 2*x+1

198

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

199

<code>

200

201

202

<code class="keyword">Definition</code> <a name="Pdouble_plus_one_mask"></a>Pdouble_plus_one_mask (x:<a href="Coq.NArith.BinPos.html#positive_mask">positive_mask</a>) :=

203

match x with

204

| <a href="Coq.NArith.BinPos.html#IsNul">IsNul</a> => <a href="Coq.NArith.BinPos.html#IsPos">IsPos</a> <a href="Coq.NArith.BinPos.html#xH">xH</a>

205

| <a href="Coq.NArith.BinPos.html#IsNeg">IsNeg</a> => <a href="Coq.NArith.BinPos.html#IsNeg">IsNeg</a>

206

| <a href="Coq.NArith.BinPos.html#IsPos">IsPos</a> p => <a href="Coq.NArith.BinPos.html#IsPos">IsPos</a> (<a href="Coq.NArith.BinPos.html#xI">xI</a> p)

207

end.

208

209

210

</code>

211

212

213

Operation x -> 2*x

214

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

215

<code>

216

217

218

<code class="keyword">Definition</code> <a name="Pdouble_mask"></a>Pdouble_mask (x:<a href="Coq.NArith.BinPos.html#positive_mask">positive_mask</a>) :=

219

match x with

220

| <a href="Coq.NArith.BinPos.html#IsNul">IsNul</a> => <a href="Coq.NArith.BinPos.html#IsNul">IsNul</a>

221

| <a href="Coq.NArith.BinPos.html#IsNeg">IsNeg</a> => <a href="Coq.NArith.BinPos.html#IsNeg">IsNeg</a>

222

| <a href="Coq.NArith.BinPos.html#IsPos">IsPos</a> p => <a href="Coq.NArith.BinPos.html#IsPos">IsPos</a> (<a href="Coq.NArith.BinPos.html#xO">xO</a> p)

223

end.

224

225

226

</code>

227

228

229

Operation x -> 2*x-2

230

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

231

<code>

232

233

234

<code class="keyword">Definition</code> <a name="Pdouble_minus_two"></a>Pdouble_minus_two (x:<a href="Coq.NArith.BinPos.html#positive">positive</a>) :=

235

match x with

236

| <a href="Coq.NArith.BinPos.html#xI">xI</a> x' => <a href="Coq.NArith.BinPos.html#IsPos">IsPos</a> (<a href="Coq.NArith.BinPos.html#xO">xO</a> (<a href="Coq.NArith.BinPos.html#xO">xO</a> x'))

237

| <a href="Coq.NArith.BinPos.html#xO">xO</a> x' => <a href="Coq.NArith.BinPos.html#IsPos">IsPos</a> (<a href="Coq.NArith.BinPos.html#xO">xO</a> (<a href="Coq.NArith.BinPos.html#Pdouble_minus_one">Pdouble_minus_one</a> x'))

238

| <a href="Coq.NArith.BinPos.html#xH">xH</a> => <a href="Coq.NArith.BinPos.html#IsNul">IsNul</a>

239

end.

240

241

242

</code>

243

244

245

Subtraction of binary positive numbers into a positive numbers mask

246

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

247

<code>

248

249

250

<code class="keyword">Fixpoint</code> <a name="Pminus_mask"></a>Pminus_mask (x y:<a href="Coq.NArith.BinPos.html#positive">positive</a>) {struct y} : <a href="Coq.NArith.BinPos.html#positive_mask">positive_mask</a> :=

251

match x, y with

252

| <a href="Coq.NArith.BinPos.html#xI">xI</a> x', <a href="Coq.NArith.BinPos.html#xI">xI</a> y' => <a href="Coq.NArith.BinPos.html#Pdouble_mask">Pdouble_mask</a> (Pminus_mask x' y')

253

| <a href="Coq.NArith.BinPos.html#xI">xI</a> x', <a href="Coq.NArith.BinPos.html#xO">xO</a> y' => <a href="Coq.NArith.BinPos.html#Pdouble_plus_one_mask">Pdouble_plus_one_mask</a> (Pminus_mask x' y')

254

| <a href="Coq.NArith.BinPos.html#xI">xI</a> x', <a href="Coq.NArith.BinPos.html#xH">xH</a> => <a href="Coq.NArith.BinPos.html#IsPos">IsPos</a> (<a href="Coq.NArith.BinPos.html#xO">xO</a> x')

255

| <a href="Coq.NArith.BinPos.html#xO">xO</a> x', <a href="Coq.NArith.BinPos.html#xI">xI</a> y' => <a href="Coq.NArith.BinPos.html#Pdouble_plus_one_mask">Pdouble_plus_one_mask</a> (Pminus_mask_carry x' y')

256

| <a href="Coq.NArith.BinPos.html#xO">xO</a> x', <a href="Coq.NArith.BinPos.html#xO">xO</a> y' => <a href="Coq.NArith.BinPos.html#Pdouble_mask">Pdouble_mask</a> (Pminus_mask x' y')

257

| <a href="Coq.NArith.BinPos.html#xO">xO</a> x', <a href="Coq.NArith.BinPos.html#xH">xH</a> => <a href="Coq.NArith.BinPos.html#IsPos">IsPos</a> (<a href="Coq.NArith.BinPos.html#Pdouble_minus_one">Pdouble_minus_one</a> x')

258

| <a href="Coq.NArith.BinPos.html#xH">xH</a>, <a href="Coq.NArith.BinPos.html#xH">xH</a> => <a href="Coq.NArith.BinPos.html#IsNul">IsNul</a>

259

| <a href="Coq.NArith.BinPos.html#xH">xH</a>, _ => <a href="Coq.NArith.BinPos.html#IsNeg">IsNeg</a>

260

end

261

262

with <a name="Pminus_mask_carry"></a>Pminus_mask_carry (x y:<a href="Coq.NArith.BinPos.html#positive">positive</a>) {struct y} : <a href="Coq.NArith.BinPos.html#positive_mask">positive_mask</a> :=

263

match x, y with

264

| <a href="Coq.NArith.BinPos.html#xI">xI</a> x', <a href="Coq.NArith.BinPos.html#xI">xI</a> y' => <a href="Coq.NArith.BinPos.html#Pdouble_plus_one_mask">Pdouble_plus_one_mask</a> (Pminus_mask_carry x' y')

265

| <a href="Coq.NArith.BinPos.html#xI">xI</a> x', <a href="Coq.NArith.BinPos.html#xO">xO</a> y' => <a href="Coq.NArith.BinPos.html#Pdouble_mask">Pdouble_mask</a> (Pminus_mask x' y')

266

| <a href="Coq.NArith.BinPos.html#xI">xI</a> x', <a href="Coq.NArith.BinPos.html#xH">xH</a> => <a href="Coq.NArith.BinPos.html#IsPos">IsPos</a> (<a href="Coq.NArith.BinPos.html#Pdouble_minus_one">Pdouble_minus_one</a> x')

267

| <a href="Coq.NArith.BinPos.html#xO">xO</a> x', <a href="Coq.NArith.BinPos.html#xI">xI</a> y' => <a href="Coq.NArith.BinPos.html#Pdouble_mask">Pdouble_mask</a> (Pminus_mask_carry x' y')

268

| <a href="Coq.NArith.BinPos.html#xO">xO</a> x', <a href="Coq.NArith.BinPos.html#xO">xO</a> y' => <a href="Coq.NArith.BinPos.html#Pdouble_plus_one_mask">Pdouble_plus_one_mask</a> (Pminus_mask_carry x' y')

269

| <a href="Coq.NArith.BinPos.html#xO">xO</a> x', <a href="Coq.NArith.BinPos.html#xH">xH</a> => <a href="Coq.NArith.BinPos.html#Pdouble_minus_two">Pdouble_minus_two</a> x'

270

| <a href="Coq.NArith.BinPos.html#xH">xH</a>, _ => <a href="Coq.NArith.BinPos.html#IsNeg">IsNeg</a>

271

end.

272

273

274

</code>

275

276

277

Subtraction of binary positive numbers x and y, returns 1 if x<=y

278

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

279

<code>

280

281

282

<code class="keyword">Definition</code> <a name="Pminus"></a>Pminus (x y:<a href="Coq.NArith.BinPos.html#positive">positive</a>) :=

283

match <a href="Coq.NArith.BinPos.html#Pminus_mask">Pminus_mask</a> x y with

284

| <a href="Coq.NArith.BinPos.html#IsPos">IsPos</a> z => z

285

| _ => <a href="Coq.NArith.BinPos.html#xH">xH</a>

286

end.

287

288

289

<code class="keyword">Infix</code> "-" := <a href="Coq.NArith.BinPos.html#Pminus">Pminus</a> : positive_scope.

290

291

292

</code>

293

294

295

Multiplication on binary positive numbers

296

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

297

<code>

298

299

300

<code class="keyword">Fixpoint</code> <a name="Pmult"></a>Pmult (x y:<a href="Coq.NArith.BinPos.html#positive">positive</a>) {struct x} : <a href="Coq.NArith.BinPos.html#positive">positive</a> :=

301

match x with

302

| <a href="Coq.NArith.BinPos.html#xI">xI</a> x' => y + <a href="Coq.NArith.BinPos.html#xO">xO</a> (Pmult x' y)

303

| <a href="Coq.NArith.BinPos.html#xO">xO</a> x' => <a href="Coq.NArith.BinPos.html#xO">xO</a> (Pmult x' y)

304

| <a href="Coq.NArith.BinPos.html#xH">xH</a> => y

305

end.

306

307

308

<code class="keyword">Infix</code> "*" := <a href="Coq.NArith.BinPos.html#Pmult">Pmult</a> : positive_scope.

309

310

311

</code>

312

313

314

Division by 2 rounded below but for 1

315

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

316

<code>

317

318

319

<code class="keyword">Definition</code> <a name="Pdiv2"></a>Pdiv2 (z:<a href="Coq.NArith.BinPos.html#positive">positive</a>) :=

320

match z with

321

| <a href="Coq.NArith.BinPos.html#xH">xH</a> => <a href="Coq.NArith.BinPos.html#xH">xH</a>

322

| <a href="Coq.NArith.BinPos.html#xO">xO</a> p => p

323

| <a href="Coq.NArith.BinPos.html#xI">xI</a> p => p

324

end.

325

326

327

<code class="keyword">Infix</code> "/" := <a href="Coq.NArith.BinPos.html#Pdiv2">Pdiv2</a> : positive_scope.

328

329

330

</code>

331

332

333

Comparison on binary positive numbers

334

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

335

<code>

336

337

338

<code class="keyword">Fixpoint</code> <a name="Pcompare"></a>Pcompare (x y:<a href="Coq.NArith.BinPos.html#positive">positive</a>) (r:<a href="Coq.Init.Datatypes.html#comparison">comparison</a>) {struct y} : <a href="Coq.Init.Datatypes.html#comparison">comparison</a> :=

339

match x, y with

340

| <a href="Coq.NArith.BinPos.html#xI">xI</a> x', <a href="Coq.NArith.BinPos.html#xI">xI</a> y' => Pcompare x' y' r

341

| <a href="Coq.NArith.BinPos.html#xI">xI</a> x', <a href="Coq.NArith.BinPos.html#xO">xO</a> y' => Pcompare x' y' <a href="Coq.Init.Datatypes.html#Gt">Gt</a>

342

| <a href="Coq.NArith.BinPos.html#xI">xI</a> x', <a href="Coq.NArith.BinPos.html#xH">xH</a> => <a href="Coq.Init.Datatypes.html#Gt">Gt</a>

343

| <a href="Coq.NArith.BinPos.html#xO">xO</a> x', <a href="Coq.NArith.BinPos.html#xI">xI</a> y' => Pcompare x' y' <a href="Coq.Init.Datatypes.html#Lt">Lt</a>

344

| <a href="Coq.NArith.BinPos.html#xO">xO</a> x', <a href="Coq.NArith.BinPos.html#xO">xO</a> y' => Pcompare x' y' r

345

| <a href="Coq.NArith.BinPos.html#xO">xO</a> x', <a href="Coq.NArith.BinPos.html#xH">xH</a> => <a href="Coq.Init.Datatypes.html#Gt">Gt</a>

346

| <a href="Coq.NArith.BinPos.html#xH">xH</a>, <a href="Coq.NArith.BinPos.html#xI">xI</a> y' => <a href="Coq.Init.Datatypes.html#Lt">Lt</a>

347

| <a href="Coq.NArith.BinPos.html#xH">xH</a>, <a href="Coq.NArith.BinPos.html#xO">xO</a> y' => <a href="Coq.Init.Datatypes.html#Lt">Lt</a>

348

| <a href="Coq.NArith.BinPos.html#xH">xH</a>, <a href="Coq.NArith.BinPos.html#xH">xH</a> => r

349

end.

350

351

352

<code class="keyword">Infix</code> "?=" := <a href="Coq.NArith.BinPos.html#Pcompare">Pcompare</a> (at level 70, no associativity) : positive_scope.

353

354

355

</code>

356

357

358

Miscellaneous properties of binary positive numbers

359

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

360

<code>

361

362

363

<code class="keyword">Lemma</code> <a name="ZL11"></a>ZL11 : forall p:<a href="Coq.NArith.BinPos.html#positive">positive</a>, p = <a href="Coq.NArith.BinPos.html#xH">xH</a> \/ p <> <a href="Coq.NArith.BinPos.html#xH">xH</a>.

364

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

365

intros x; case x; intros; (left; reflexivity) || (right; discriminate).

366

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

367

368

369

</code>

370

371

372

Properties of successor on binary positive numbers

373

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

374

<code>

375

376

377

</code>

378

379

380

Specification of <code>xI</code> in term of <code>Psucc</code> and <code>xO</code>

381

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

382

<code>

383

384

385

<code class="keyword">Lemma</code> <a name="xI_succ_xO"></a>xI_succ_xO : forall p:<a href="Coq.NArith.BinPos.html#positive">positive</a>, <a href="Coq.NArith.BinPos.html#xI">xI</a> p = <a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> (<a href="Coq.NArith.BinPos.html#xO">xO</a> p).

386

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

387

reflexivity.

388

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

389

390

391

<code class="keyword">Lemma</code> <a name="Psucc_discr"></a>Psucc_discr : forall p:<a href="Coq.NArith.BinPos.html#positive">positive</a>, p <> <a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> p.

392

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

393

intro x; destruct x as [p| p| ]; discriminate.

394

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

395

396

397

</code>

398

399

400

Successor and double

401

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

402

<code>

403

404

405

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

406

forall p:<a href="Coq.NArith.BinPos.html#positive">positive</a>, <a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> (<a href="Coq.NArith.BinPos.html#Pdouble_minus_one">Pdouble_minus_one</a> p) = <a href="Coq.NArith.BinPos.html#xO">xO</a> p.

407

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

408

intro x; induction x as [x IHx| x| ]; simpl in |- *; try rewrite IHx;

409

reflexivity.

410

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

411

412

413

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

414

forall p:<a href="Coq.NArith.BinPos.html#positive">positive</a>, <a href="Coq.NArith.BinPos.html#Pdouble_minus_one">Pdouble_minus_one</a> (<a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> p) = <a href="Coq.NArith.BinPos.html#xI">xI</a> p.

415

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

416

intro x; induction x as [x IHx| x| ]; simpl in |- *; try rewrite IHx;

417

reflexivity.

418

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

419

420

421

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

422

forall p:<a href="Coq.NArith.BinPos.html#positive">positive</a>, <a href="Coq.NArith.BinPos.html#xO">xO</a> (<a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> p) = <a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> (<a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> (<a href="Coq.NArith.BinPos.html#xO">xO</a> p)).

423

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

424

intro y; induction y as [y Hrecy| y Hrecy| ]; simpl in |- *; auto.

425

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

426

427

428

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

429

forall p:<a href="Coq.NArith.BinPos.html#positive">positive</a>, <a href="Coq.NArith.BinPos.html#Pdouble_minus_one">Pdouble_minus_one</a> p <> <a href="Coq.NArith.BinPos.html#xO">xO</a> p.

430

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

431

intro x; destruct x as [p| p| ]; discriminate.

432

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

433

434

435

</code>

436

437

438

Successor and predecessor

439

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

440

<code>

441

442

443

<code class="keyword">Lemma</code> <a name="Psucc_not_one"></a>Psucc_not_one : forall p:<a href="Coq.NArith.BinPos.html#positive">positive</a>, <a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> p <> <a href="Coq.NArith.BinPos.html#xH">xH</a>.

444

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

445

intro x; destruct x as [x| x| ]; discriminate.

446

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

447

448

449

<code class="keyword">Lemma</code> <a name="Ppred_succ"></a>Ppred_succ : forall p:<a href="Coq.NArith.BinPos.html#positive">positive</a>, <a href="Coq.NArith.BinPos.html#Ppred">Ppred</a> (<a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> p) = p.

450

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

451

452

(induction p as [p IHp| | ]; [ idtac | reflexivity | reflexivity ]);

453

simpl in |- *; simpl in IHp; try rewrite <- IHp; reflexivity.

454

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

455

456

457

<code class="keyword">Lemma</code> <a name="Psucc_pred"></a>Psucc_pred : forall p:<a href="Coq.NArith.BinPos.html#positive">positive</a>, p = <a href="Coq.NArith.BinPos.html#xH">xH</a> \/ <a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> (<a href="Coq.NArith.BinPos.html#Ppred">Ppred</a> p) = p.

458

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

459

intro x; induction x as [x Hrecx| x Hrecx| ];

460

 [ simpl in |- *; auto

461

| simpl in |- *; intros; right; apply Psucc_o_double_minus_one_eq_xO

462

| auto ].

463

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

464

465

466

</code>

467

468

469

Injectivity of successor

470

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

471

<code>

472

473

474

<code class="keyword">Lemma</code> <a name="Psucc_inj"></a>Psucc_inj : forall p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>, <a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> p = <a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> q -> p = q.

475

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

476

intro x; induction x; intro y; destruct y as [y| y| ]; simpl in |- *; intro H;

477

discriminate H || (try (injection H; clear H; intro H)).

478

rewrite (IHx y H); reflexivity.

479

absurd (<a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> x = <a href="Coq.NArith.BinPos.html#xH">xH</a>); [ apply Psucc_not_one | assumption ].

480

apply <a href="Coq.Init.Logic.html#f_equal">f_equal</a> with (1 := H); assumption.

481

absurd (<a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> y = <a href="Coq.NArith.BinPos.html#xH">xH</a>);

482

[ apply Psucc_not_one | symmetry in |- *; assumption ].

483

reflexivity.

484

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

485

486

487

</code>

488

489

490

Properties of addition on binary positive numbers

491

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

492

<code>

493

494

495

</code>

496

497

498

Specification of <code>Psucc</code> in term of <code>Pplus</code>

499

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

500

<code>

501

502

503

<code class="keyword">Lemma</code> <a name="Pplus_one_succ_r"></a>Pplus_one_succ_r : forall p:<a href="Coq.NArith.BinPos.html#positive">positive</a>, <a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> p = p + <a href="Coq.NArith.BinPos.html#xH">xH</a>.

504

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

505

intro q; destruct q as [p| p| ]; reflexivity.

506

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

507

508

509

<code class="keyword">Lemma</code> <a name="Pplus_one_succ_l"></a>Pplus_one_succ_l : forall p:<a href="Coq.NArith.BinPos.html#positive">positive</a>, <a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> p = <a href="Coq.NArith.BinPos.html#xH">xH</a> + p.

510

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

511

intro q; destruct q as [p| p| ]; reflexivity.

512

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

513

514

515

</code>

516

517

518

Specification of <code>Pplus_carry</code>

519

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

520

<code>

521

522

523

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

524

forall p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>, <a href="Coq.NArith.BinPos.html#Pplus_carry">Pplus_carry</a> p q = <a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> (p + q).

525

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

526

intro x; induction x as [p IHp| p IHp| ]; intro y;

527

[ destruct y as [p0| p0| ]

528

| destruct y as [p0| p0| ]

529

| destruct y as [p| p| ] ]; simpl in |- *; auto; rewrite IHp;

530

auto.

531

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

532

533

534

</code>

535

536

537

Commutativity

538

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

539

<code>

540

541

542

<code class="keyword">Theorem</code> <a name="Pplus_comm"></a>Pplus_comm : forall p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>, p + q = q + p.

543

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

544

intro x; induction x as [p IHp| p IHp| ]; intro y;

545

[ destruct y as [p0| p0| ]

546

| destruct y as [p0| p0| ]

547

| destruct y as [p| p| ] ]; simpl in |- *; auto;

548

try do 2 rewrite <a href="Coq.NArith.BinPos.html#Pplus_carry_spec">Pplus_carry_spec</a>; rewrite IHp; auto.

549

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

550

551

552

</code>

553

554

555

Permutation of <code>Pplus</code> and <code>Psucc</code>

556

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

557

<code>

558

559

560

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

561

forall p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>, p + <a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> q = <a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> (p + q).

562

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

563

intro x; induction x as [p IHp| p IHp| ]; intro y;

564

[ destruct y as [p0| p0| ]

565

| destruct y as [p0| p0| ]

566

| destruct y as [p| p| ] ]; simpl in |- *; auto;

567

 [ rewrite Pplus_carry_spec; rewrite IHp; auto

568

| rewrite Pplus_carry_spec; auto

569

| destruct p; simpl in |- *; auto

570

| rewrite IHp; auto

571

| destruct p; simpl in |- *; auto ].

572

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

573

574

575

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

576

forall p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>, <a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> p + q = <a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> (p + q).

577

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

578

intros x y; rewrite <a href="Coq.NArith.BinPos.html#Pplus_comm">Pplus_comm</a>; rewrite <a href="Coq.NArith.BinPos.html#Pplus_comm">Pplus_comm</a> with (p:= x);

579

apply <a href="Coq.NArith.BinPos.html#Pplus_succ_permute_r">Pplus_succ_permute_r</a>.

580

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

581

582

583

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

584

forall p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>, q <> <a href="Coq.NArith.BinPos.html#xH">xH</a> -> <a href="Coq.NArith.BinPos.html#Pplus_carry">Pplus_carry</a> p (<a href="Coq.NArith.BinPos.html#Ppred">Ppred</a> q) = p + q.

585

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

586

intros q z H; elim (<a href="Coq.NArith.BinPos.html#Psucc_pred">Psucc_pred</a> z);

587

 [ intro; absurd (z = xH); auto

588

| intros E; pattern z at 2 in |- *; rewrite <- E;

589

rewrite Pplus_succ_permute_r; rewrite Pplus_carry_spec;

590

trivial ].

591

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

592

593

594

</code>

595

596

597

No neutral for addition on strictly positive numbers

598

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

599

<code>

600

601

602

<code class="keyword">Lemma</code> <a name="Pplus_no_neutral"></a>Pplus_no_neutral : forall p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>, q + p <> p.

603

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

604

intro x; induction x; intro y; destruct y as [y| y| ]; simpl in |- *; intro H;

605

discriminate H || injection H; clear H; intro H; apply (IHx y H).

606

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

607

608

609

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

610

forall p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>, <a href="Coq.NArith.BinPos.html#Pplus_carry">Pplus_carry</a> q p <> <a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> p.

611

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

612

intros x y H; absurd (y + x = x);

613

 [ apply Pplus_no_neutral

614

| apply Psucc_inj; rewrite <- Pplus_carry_spec; assumption ].

615

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

616

617

618

</code>

619

620

621

Simplification

622

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

623

<code>

624

625

626

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

627

forall p q r s:<a href="Coq.NArith.BinPos.html#positive">positive</a>, <a href="Coq.NArith.BinPos.html#Pplus_carry">Pplus_carry</a> p r = <a href="Coq.NArith.BinPos.html#Pplus_carry">Pplus_carry</a> q s -> p + r = q + s.

628

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

629

intros x y z t H; apply <a href="Coq.NArith.BinPos.html#Psucc_inj">Psucc_inj</a>; do 2 rewrite <- <a href="Coq.NArith.BinPos.html#Pplus_carry_spec">Pplus_carry_spec</a>;

630

assumption.

631

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

632

633

634

<code class="keyword">Lemma</code> <a name="Pplus_reg_r"></a>Pplus_reg_r : forall p q r:<a href="Coq.NArith.BinPos.html#positive">positive</a>, p + r = q + r -> p = q.

635

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

636

intros x y z; generalize x y; clear x y.

637

induction z as [z| z| ].

638

destruct x as [x| x| ]; intro y; destruct y as [y| y| ]; simpl in |- *;

639

intro H; discriminate H || (try (injection H; clear H; intro H)).

640

rewrite IHz with (1 := <a href="Coq.NArith.BinPos.html#Pplus_carry_plus">Pplus_carry_plus</a> _ _ _ _ H); reflexivity.

641

absurd (<a href="Coq.NArith.BinPos.html#Pplus_carry">Pplus_carry</a> x z = <a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> z);

642

[ apply Pplus_carry_no_neutral | assumption ].

643

rewrite IHz with (1 := H); reflexivity.

644

symmetry in H; absurd (<a href="Coq.NArith.BinPos.html#Pplus_carry">Pplus_carry</a> y z = <a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> z);

645

[ apply Pplus_carry_no_neutral | assumption ].

646

reflexivity.

647

destruct x as [x| x| ]; intro y; destruct y as [y| y| ]; simpl in |- *;

648

intro H; discriminate H || (try (injection H; clear H; intro H)).

649

rewrite IHz with (1 := H); reflexivity.

650

absurd (x + z = z); [ apply Pplus_no_neutral | assumption ].

651

rewrite IHz with (1 := H); reflexivity.

652

symmetry in H; absurd (y + z = z);

653

[ apply Pplus_no_neutral | assumption ].

654

reflexivity.

655

intros H x y; apply <a href="Coq.NArith.BinPos.html#Psucc_inj">Psucc_inj</a>; do 2 rewrite <a href="Coq.NArith.BinPos.html#Pplus_one_succ_r">Pplus_one_succ_r</a>; assumption.

656

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

657

658

659

<code class="keyword">Lemma</code> <a name="Pplus_reg_l"></a>Pplus_reg_l : forall p q r:<a href="Coq.NArith.BinPos.html#positive">positive</a>, p + q = p + r -> q = r.

660

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

661

intros x y z H; apply <a href="Coq.NArith.BinPos.html#Pplus_reg_r">Pplus_reg_r</a> with (r:= x);

662

rewrite <a href="Coq.NArith.BinPos.html#Pplus_comm">Pplus_comm</a> with (p:= z); rewrite <a href="Coq.NArith.BinPos.html#Pplus_comm">Pplus_comm</a> with (p:= y);

663

assumption.

664

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

665

666

667

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

668

forall p q r:<a href="Coq.NArith.BinPos.html#positive">positive</a>, <a href="Coq.NArith.BinPos.html#Pplus_carry">Pplus_carry</a> p r = <a href="Coq.NArith.BinPos.html#Pplus_carry">Pplus_carry</a> q r -> p = q.

669

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

670

intros x y z H; apply <a href="Coq.NArith.BinPos.html#Pplus_reg_r">Pplus_reg_r</a> with (r:= z); apply <a href="Coq.NArith.BinPos.html#Pplus_carry_plus">Pplus_carry_plus</a>;

671

assumption.

672

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

673

674

675

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

676

forall p q r:<a href="Coq.NArith.BinPos.html#positive">positive</a>, <a href="Coq.NArith.BinPos.html#Pplus_carry">Pplus_carry</a> p q = <a href="Coq.NArith.BinPos.html#Pplus_carry">Pplus_carry</a> p r -> q = r.

677

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

678

intros x y z H; apply <a href="Coq.NArith.BinPos.html#Pplus_reg_r">Pplus_reg_r</a> with (r:= x);

679

rewrite <a href="Coq.NArith.BinPos.html#Pplus_comm">Pplus_comm</a> with (p:= z); rewrite <a href="Coq.NArith.BinPos.html#Pplus_comm">Pplus_comm</a> with (p:= y);

680

apply <a href="Coq.NArith.BinPos.html#Pplus_carry_plus">Pplus_carry_plus</a>; assumption.

681

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

682

683

684

</code>

685

686

687

Addition on positive is associative

688

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

689

<code>

690

691

692

<code class="keyword">Theorem</code> <a name="Pplus_assoc"></a>Pplus_assoc : forall p q r:<a href="Coq.NArith.BinPos.html#positive">positive</a>, p + (q + r) = p + q + r.

693

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

694

intros x y; generalize x; clear x.

695

induction y as [y| y| ]; intro x.

696

destruct x as [x| x| ]; intro z; destruct z as [z| z| ]; simpl in |- *;

697

repeat rewrite <a href="Coq.NArith.BinPos.html#Pplus_carry_spec">Pplus_carry_spec</a>; repeat rewrite <a href="Coq.NArith.BinPos.html#Pplus_succ_permute_r">Pplus_succ_permute_r</a>;

698

repeat rewrite <a href="Coq.NArith.BinPos.html#Pplus_succ_permute_l">Pplus_succ_permute_l</a>;

699

reflexivity || (repeat apply <a href="Coq.Init.Logic.html#f_equal">f_equal</a> with (A:= <a href="Coq.NArith.BinPos.html#positive">positive</a>));

700

apply IHy.

701

destruct x as [x| x| ]; intro z; destruct z as [z| z| ]; simpl in |- *;

702

repeat rewrite <a href="Coq.NArith.BinPos.html#Pplus_carry_spec">Pplus_carry_spec</a>; repeat rewrite <a href="Coq.NArith.BinPos.html#Pplus_succ_permute_r">Pplus_succ_permute_r</a>;

703

repeat rewrite <a href="Coq.NArith.BinPos.html#Pplus_succ_permute_l">Pplus_succ_permute_l</a>;

704

reflexivity || (repeat apply <a href="Coq.Init.Logic.html#f_equal">f_equal</a> with (A:= <a href="Coq.NArith.BinPos.html#positive">positive</a>));

705

apply IHy.

706

intro z; rewrite <a href="Coq.NArith.BinPos.html#Pplus_comm">Pplus_comm</a> with (p:= <a href="Coq.NArith.BinPos.html#xH">xH</a>);

707

do 2 rewrite <- <a href="Coq.NArith.BinPos.html#Pplus_one_succ_r">Pplus_one_succ_r</a>; rewrite <a href="Coq.NArith.BinPos.html#Pplus_succ_permute_l">Pplus_succ_permute_l</a>;

708

rewrite <a href="Coq.NArith.BinPos.html#Pplus_succ_permute_r">Pplus_succ_permute_r</a>; reflexivity.

709

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

710

711

712

</code>

713

714

715

Commutation of addition with the double of a positive number

716

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

717

<code>

718

719

720

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

721

forall p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>, <a href="Coq.NArith.BinPos.html#xO">xO</a> (p + q) = <a href="Coq.NArith.BinPos.html#xI">xI</a> p + <a href="Coq.NArith.BinPos.html#Pdouble_minus_one">Pdouble_minus_one</a> q.

722

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

723

intros; change (<a href="Coq.NArith.BinPos.html#xI">xI</a> p) with (<a href="Coq.NArith.BinPos.html#xO">xO</a> p + <a href="Coq.NArith.BinPos.html#xH">xH</a>) in |- *.

724

rewrite <- <a href="Coq.NArith.BinPos.html#Pplus_assoc">Pplus_assoc</a>; rewrite <- <a href="Coq.NArith.BinPos.html#Pplus_one_succ_l">Pplus_one_succ_l</a>;

725

rewrite <a href="Coq.NArith.BinPos.html#Psucc_o_double_minus_one_eq_xO">Psucc_o_double_minus_one_eq_xO</a>.

726

reflexivity.

727

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

728

729

730

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

731

forall p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>, <a href="Coq.NArith.BinPos.html#Pdouble_minus_one">Pdouble_minus_one</a> (p + q) = <a href="Coq.NArith.BinPos.html#xO">xO</a> p + <a href="Coq.NArith.BinPos.html#Pdouble_minus_one">Pdouble_minus_one</a> q.

732

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

733

734

try rewrite <a href="Coq.NArith.BinPos.html#Pplus_carry_spec">Pplus_carry_spec</a>; try rewrite <a href="Coq.NArith.BinPos.html#Pdouble_minus_one_o_succ_eq_xI">Pdouble_minus_one_o_succ_eq_xI</a>;

735

try rewrite IHp; try rewrite <a href="Coq.NArith.BinPos.html#Pplus_xI_double_minus_one">Pplus_xI_double_minus_one</a>;

736

try reflexivity.

737

rewrite <- <a href="Coq.NArith.BinPos.html#Psucc_o_double_minus_one_eq_xO">Psucc_o_double_minus_one_eq_xO</a>; rewrite <a href="Coq.NArith.BinPos.html#Pplus_one_succ_l">Pplus_one_succ_l</a>;

738

reflexivity.

739

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

740

741

742

</code>

743

744

745

Misc

746

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

747

<code>

748

749

750

<code class="keyword">Lemma</code> <a name="Pplus_diag"></a>Pplus_diag : forall p:<a href="Coq.NArith.BinPos.html#positive">positive</a>, p + p = <a href="Coq.NArith.BinPos.html#xO">xO</a> p.

751

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

752

intro x; induction x; simpl in |- *; try rewrite <a href="Coq.NArith.BinPos.html#Pplus_carry_spec">Pplus_carry_spec</a>;

753

try rewrite IHx; reflexivity.

754

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

755

756

757

</code>

758

759

760

Peano induction on binary positive positive numbers

761

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

762

<code>

763

764

765

<code class="keyword">Fixpoint</code> <a name="plus_iter"></a>plus_iter (x y:<a href="Coq.NArith.BinPos.html#positive">positive</a>) {struct x} : <a href="Coq.NArith.BinPos.html#positive">positive</a> :=

766

match x with

767

| <a href="Coq.NArith.BinPos.html#xH">xH</a> => <a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> y

768

| <a href="Coq.NArith.BinPos.html#xO">xO</a> x => plus_iter x (plus_iter x y)

769

| <a href="Coq.NArith.BinPos.html#xI">xI</a> x => plus_iter x (plus_iter x (<a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> y))

770

end.

771

772

773

<code class="keyword">Lemma</code> <a name="plus_iter_eq_plus"></a>plus_iter_eq_plus : forall p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>, <a href="Coq.NArith.BinPos.html#plus_iter">plus_iter</a> p q = p + q.

774

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

775

intro x; induction x as [p IHp| p IHp| ]; intro y;

776

[ destruct y as [p0| p0| ]

777

| destruct y as [p0| p0| ]

778

| destruct y as [p| p| ] ]; simpl in |- *; reflexivity || (do 2 rewrite IHp);

779

rewrite <a href="Coq.NArith.BinPos.html#Pplus_assoc">Pplus_assoc</a>; rewrite <a href="Coq.NArith.BinPos.html#Pplus_diag">Pplus_diag</a>; try reflexivity.

780

rewrite <a href="Coq.NArith.BinPos.html#Pplus_carry_spec">Pplus_carry_spec</a>; rewrite <- <a href="Coq.NArith.BinPos.html#Pplus_succ_permute_r">Pplus_succ_permute_r</a>; reflexivity.

781

rewrite <a href="Coq.NArith.BinPos.html#Pplus_one_succ_r">Pplus_one_succ_r</a>; reflexivity.

782

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

783

784

785

<code class="keyword">Lemma</code> <a name="plus_iter_xO"></a>plus_iter_xO : forall p:<a href="Coq.NArith.BinPos.html#positive">positive</a>, <a href="Coq.NArith.BinPos.html#plus_iter">plus_iter</a> p p = <a href="Coq.NArith.BinPos.html#xO">xO</a> p.

786

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

787

intro; rewrite <- <a href="Coq.NArith.BinPos.html#Pplus_diag">Pplus_diag</a>; apply <a href="Coq.NArith.BinPos.html#plus_iter_eq_plus">plus_iter_eq_plus</a>.

788

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

789

790

791

<code class="keyword">Lemma</code> <a name="plus_iter_xI"></a>plus_iter_xI : forall p:<a href="Coq.NArith.BinPos.html#positive">positive</a>, <a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> (<a href="Coq.NArith.BinPos.html#plus_iter">plus_iter</a> p p) = <a href="Coq.NArith.BinPos.html#xI">xI</a> p.

792

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

793

intro; rewrite <a href="Coq.NArith.BinPos.html#xI_succ_xO">xI_succ_xO</a>; rewrite <- <a href="Coq.NArith.BinPos.html#Pplus_diag">Pplus_diag</a>;

794

apply (<a href="Coq.Init.Logic.html#f_equal">f_equal</a> (A:=<a href="Coq.NArith.BinPos.html#positive">positive</a>)); apply <a href="Coq.NArith.BinPos.html#plus_iter_eq_plus">plus_iter_eq_plus</a>.

795

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

796

797

798

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

799

forall P:<a href="Coq.NArith.BinPos.html#positive">positive</a> -> Type,

800

(forall n:<a href="Coq.NArith.BinPos.html#positive">positive</a>, P n -> P (<a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> n)) ->

801

forall p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>, P q -> P (<a href="Coq.NArith.BinPos.html#plus_iter">plus_iter</a> p q).

802

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

803

intros P H; induction p; simpl in |- *; intros.

804

apply IHp; apply IHp; apply H; assumption.

805

apply IHp; apply IHp; assumption.

806

apply H; assumption.

807

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

808

809

810

</code>

811

812

813

Peano induction

814

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

815

<code>

816

817

818

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

819

forall P:<a href="Coq.NArith.BinPos.html#positive">positive</a> -> Prop,

820

P <a href="Coq.NArith.BinPos.html#xH">xH</a> -> (forall n:<a href="Coq.NArith.BinPos.html#positive">positive</a>, P n -> P (<a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> n)) -> forall p:<a href="Coq.NArith.BinPos.html#positive">positive</a>, P p.

821

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

822

intros P H1 Hsucc n; induction n.

823

rewrite <- <a href="Coq.NArith.BinPos.html#plus_iter_xI">plus_iter_xI</a>; apply Hsucc; apply <a href="Coq.NArith.BinPos.html#iterate_add">iterate_add</a>; assumption.

824

rewrite <- <a href="Coq.NArith.BinPos.html#plus_iter_xO">plus_iter_xO</a>; apply <a href="Coq.NArith.BinPos.html#iterate_add">iterate_add</a>; assumption.

825

assumption.

826

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

827

828

829

</code>

830

831

832

Peano recursion

833

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

834

<code>

835

836

837

<code class="keyword">Definition</code> <a name="Prec"></a>Prec (A:Set) (a:A) (f:<a href="Coq.NArith.BinPos.html#positive">positive</a> -> A -> A) :

838

<a href="Coq.NArith.BinPos.html#positive">positive</a> -> A :=

839

(fix Prec (p:<a href="Coq.NArith.BinPos.html#positive">positive</a>) : A :=

840

match p with

841

| <a href="Coq.NArith.BinPos.html#xH">xH</a> => a

842

| <a href="Coq.NArith.BinPos.html#xO">xO</a> p => <a href="Coq.NArith.BinPos.html#iterate_add">iterate_add</a> (fun _ => A) f p p (Prec p)

843

| <a href="Coq.NArith.BinPos.html#xI">xI</a> p => f (<a href="Coq.NArith.BinPos.html#plus_iter">plus_iter</a> p p) (<a href="Coq.NArith.BinPos.html#iterate_add">iterate_add</a> (fun _ => A) f p p (Prec p))

844

end).

845

846

847

</code>

848

849

850

Peano case analysis

851

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

852

<code>

853

854

855

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

856

forall P:<a href="Coq.NArith.BinPos.html#positive">positive</a> -> Prop,

857

P <a href="Coq.NArith.BinPos.html#xH">xH</a> -> (forall n:<a href="Coq.NArith.BinPos.html#positive">positive</a>, P (<a href="Coq.NArith.BinPos.html#Psucc">Psucc</a> n)) -> forall p:<a href="Coq.NArith.BinPos.html#positive">positive</a>, P p.

858

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

859

intros; apply <a href="Coq.NArith.BinPos.html#Pind">Pind</a>; auto.

860

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

861

862

863

</code>

864

865

866

Properties of multiplication on binary positive numbers

867

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

868

<code>

869

870

871

</code>

872

873

874

One is right neutral for multiplication

875

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

876

<code>

877

878

879

<code class="keyword">Lemma</code> <a name="Pmult_1_r"></a>Pmult_1_r : forall p:<a href="Coq.NArith.BinPos.html#positive">positive</a>, p * <a href="Coq.NArith.BinPos.html#xH">xH</a> = p.

880

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

881

intro x; induction x; simpl in |- *.

882

rewrite IHx; reflexivity.

883

rewrite IHx; reflexivity.

884

reflexivity.

885

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

886

887

888

</code>

889

890

891

Right reduction properties for multiplication

892

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

893

<code>

894

895

896

<code class="keyword">Lemma</code> <a name="Pmult_xO_permute_r"></a>Pmult_xO_permute_r : forall p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>, p * <a href="Coq.NArith.BinPos.html#xO">xO</a> q = <a href="Coq.NArith.BinPos.html#xO">xO</a> (p * q).

897

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

898

intros x y; induction x; simpl in |- *.

899

rewrite IHx; reflexivity.

900

rewrite IHx; reflexivity.

901

reflexivity.

902

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

903

904

905

<code class="keyword">Lemma</code> <a name="Pmult_xI_permute_r"></a>Pmult_xI_permute_r : forall p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>, p * <a href="Coq.NArith.BinPos.html#xI">xI</a> q = p + <a href="Coq.NArith.BinPos.html#xO">xO</a> (p * q).

906

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

907

intros x y; induction x; simpl in |- *.

908

rewrite IHx; do 2 rewrite <a href="Coq.NArith.BinPos.html#Pplus_assoc">Pplus_assoc</a>; rewrite <a href="Coq.NArith.BinPos.html#Pplus_comm">Pplus_comm</a> with (p:= y);

909

reflexivity.

910

rewrite IHx; reflexivity.

911

reflexivity.

912

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

913

914

915

</code>

916

917

918

Commutativity of multiplication

919

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

920

<code>

921

922

923

<code class="keyword">Theorem</code> <a name="Pmult_comm"></a>Pmult_comm : forall p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>, p * q = q * p.

924

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

925

intros x y; induction y; simpl in |- *.

926

rewrite <- IHy; apply <a href="Coq.NArith.BinPos.html#Pmult_xI_permute_r">Pmult_xI_permute_r</a>.

927

rewrite <- IHy; apply <a href="Coq.NArith.BinPos.html#Pmult_xO_permute_r">Pmult_xO_permute_r</a>.

928

apply <a href="Coq.NArith.BinPos.html#Pmult_1_r">Pmult_1_r</a>.

929

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

930

931

932

</code>

933

934

935

Distributivity of multiplication over addition

936

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

937

<code>

938

939

940

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

941

forall p q r:<a href="Coq.NArith.BinPos.html#positive">positive</a>, p * (q + r) = p * q + p * r.

942

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

943

intros x y z; induction x; simpl in |- *.

944

rewrite IHx; rewrite <- <a href="Coq.NArith.BinPos.html#Pplus_assoc">Pplus_assoc</a> with (q:= <a href="Coq.NArith.BinPos.html#xO">xO</a> (x * y));

945

rewrite <a href="Coq.NArith.BinPos.html#Pplus_assoc">Pplus_assoc</a> with (p:= <a href="Coq.NArith.BinPos.html#xO">xO</a> (x * y));

946

rewrite <a href="Coq.NArith.BinPos.html#Pplus_comm">Pplus_comm</a> with (p:= <a href="Coq.NArith.BinPos.html#xO">xO</a> (x * y));

947

rewrite <- <a href="Coq.NArith.BinPos.html#Pplus_assoc">Pplus_assoc</a> with (q:= <a href="Coq.NArith.BinPos.html#xO">xO</a> (x * y));

948

rewrite <a href="Coq.NArith.BinPos.html#Pplus_assoc">Pplus_assoc</a> with (q:= z); reflexivity.

949

rewrite IHx; reflexivity.

950

reflexivity.

951

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

952

953

954

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

955

forall p q r:<a href="Coq.NArith.BinPos.html#positive">positive</a>, (p + q) * r = p * r + q * r.

956

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

957

intros x y z; do 3 rewrite <a href="Coq.NArith.BinPos.html#Pmult_comm">Pmult_comm</a> with (q:= z); apply <a href="Coq.NArith.BinPos.html#Pmult_plus_distr_l">Pmult_plus_distr_l</a>.

958

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

959

960

961

</code>

962

963

964

Associativity of multiplication

965

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

966

<code>

967

968

969

<code class="keyword">Theorem</code> <a name="Pmult_assoc"></a>Pmult_assoc : forall p q r:<a href="Coq.NArith.BinPos.html#positive">positive</a>, p * (q * r) = p * q * r.

970

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

971

intro x; induction x as [x| x| ]; simpl in |- *; intros y z.

972

rewrite IHx; rewrite <a href="Coq.NArith.BinPos.html#Pmult_plus_distr_r">Pmult_plus_distr_r</a>; reflexivity.

973

rewrite IHx; reflexivity.

974

reflexivity.

975

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

976

977

978

</code>

979

980

981

Parity properties of multiplication

982

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

983

<code>

984

985

986

<code class="keyword">Lemma</code> <a name="Pmult_xI_mult_xO_discr"></a>Pmult_xI_mult_xO_discr : forall p q r:<a href="Coq.NArith.BinPos.html#positive">positive</a>, <a href="Coq.NArith.BinPos.html#xI">xI</a> p * r <> <a href="Coq.NArith.BinPos.html#xO">xO</a> q * r.

987

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

988

intros x y z; induction z as [| z IHz| ]; try discriminate.

989

intro H; apply IHz; clear IHz.

990

do 2 rewrite <a href="Coq.NArith.BinPos.html#Pmult_xO_permute_r">Pmult_xO_permute_r</a> in H.

991

injection H; clear H; intro H; exact H.

992

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

993

994

995

<code class="keyword">Lemma</code> <a name="Pmult_xO_discr"></a>Pmult_xO_discr : forall p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>, <a href="Coq.NArith.BinPos.html#xO">xO</a> p * q <> q.

996

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

997

intros x y; induction y; try discriminate.

998

rewrite <a href="Coq.NArith.BinPos.html#Pmult_xO_permute_r">Pmult_xO_permute_r</a>; injection; assumption.

999

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

1000

1001

1002

</code>

1003

1004

1005

Simplification properties of multiplication

1006

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

1007

<code>

1008

1009

1010

<code class="keyword">Theorem</code> <a name="Pmult_reg_r"></a>Pmult_reg_r : forall p q r:<a href="Coq.NArith.BinPos.html#positive">positive</a>, p * r = q * r -> p = q.

1011

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

1012

intro x; induction x as [p IHp| p IHp| ]; intro y; destruct y as [q| q| ];

1013

intros z H; reflexivity || apply (<a href="Coq.Init.Logic.html#f_equal">f_equal</a> (A:=<a href="Coq.NArith.BinPos.html#positive">positive</a>)) || apply <a href="Coq.Init.Logic.html#False_ind">False_ind</a>.

1014

simpl in H; apply IHp with (<a href="Coq.NArith.BinPos.html#xO">xO</a> z); simpl in |- *;

1015

do 2 rewrite <a href="Coq.NArith.BinPos.html#Pmult_xO_permute_r">Pmult_xO_permute_r</a>; apply <a href="Coq.NArith.BinPos.html#Pplus_reg_l">Pplus_reg_l</a> with (1 := H).

1016

apply <a href="Coq.NArith.BinPos.html#Pmult_xI_mult_xO_discr">Pmult_xI_mult_xO_discr</a> with (1 := H).

1017

simpl in H; rewrite <a href="Coq.NArith.BinPos.html#Pplus_comm">Pplus_comm</a> in H; apply <a href="Coq.NArith.BinPos.html#Pplus_no_neutral">Pplus_no_neutral</a> with (1 := H).

1018

symmetry in H; apply <a href="Coq.NArith.BinPos.html#Pmult_xI_mult_xO_discr">Pmult_xI_mult_xO_discr</a> with (1 := H).

1019

apply IHp with (<a href="Coq.NArith.BinPos.html#xO">xO</a> z); simpl in |- *; do 2 rewrite <a href="Coq.NArith.BinPos.html#Pmult_xO_permute_r">Pmult_xO_permute_r</a>;

1020

assumption.

1021

apply <a href="Coq.NArith.BinPos.html#Pmult_xO_discr">Pmult_xO_discr</a> with (1 := H).

1022

simpl in H; symmetry in H; rewrite <a href="Coq.NArith.BinPos.html#Pplus_comm">Pplus_comm</a> in H;

1023

apply <a href="Coq.NArith.BinPos.html#Pplus_no_neutral">Pplus_no_neutral</a> with (1 := H).

1024

symmetry in H; apply <a href="Coq.NArith.BinPos.html#Pmult_xO_discr">Pmult_xO_discr</a> with (1 := H).

1025

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

1026

1027

1028

<code class="keyword">Theorem</code> <a name="Pmult_reg_l"></a>Pmult_reg_l : forall p q r:<a href="Coq.NArith.BinPos.html#positive">positive</a>, r * p = r * q -> p = q.

1029

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

1030

intros x y z H; apply <a href="Coq.NArith.BinPos.html#Pmult_reg_r">Pmult_reg_r</a> with (r:= z).

1031

rewrite <a href="Coq.NArith.BinPos.html#Pmult_comm">Pmult_comm</a> with (p:= x); rewrite <a href="Coq.NArith.BinPos.html#Pmult_comm">Pmult_comm</a> with (p:= y);

1032

assumption.

1033

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

1034

1035

1036

</code>

1037

1038

1039

Inversion of multiplication

1040

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

1041

<code>

1042

1043

1044

<code class="keyword">Lemma</code> <a name="Pmult_1_inversion_l"></a>Pmult_1_inversion_l : forall p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>, p * q = <a href="Coq.NArith.BinPos.html#xH">xH</a> -> p = <a href="Coq.NArith.BinPos.html#xH">xH</a>.

1045

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

1046

intros x y; destruct x as [p| p| ]; simpl in |- *.

1047

destruct y as [p0| p0| ]; intro; discriminate.

1048

intro; discriminate.

1049

reflexivity.

1050

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

1051

1052

1053

</code>

1054

1055

1056

Properties of comparison on binary positive numbers

1057

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

1058

<code>

1059

1060

1061

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

1062

forall p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>, (p ?= q) <a href="Coq.Init.Datatypes.html#Gt">Gt</a> <> <a href="Coq.Init.Datatypes.html#Eq">Eq</a> /\ (p ?= q) <a href="Coq.Init.Datatypes.html#Lt">Lt</a> <> <a href="Coq.Init.Datatypes.html#Eq">Eq</a>.

1063

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

1064

intro x; induction x as [p IHp| p IHp| ]; intro y; destruct y as [q| q| ];

1065

split; simpl in |- *; auto; discriminate || (elim (IHp q); auto).

1066

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

1067

1068

1069

<code class="keyword">Theorem</code> <a name="Pcompare_Eq_eq"></a>Pcompare_Eq_eq : forall p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>, (p ?= q) <a href="Coq.Init.Datatypes.html#Eq">Eq</a> = <a href="Coq.Init.Datatypes.html#Eq">Eq</a> -> p = q.

1070

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

1071

intro x; induction x as [p IHp| p IHp| ]; intro y; destruct y as [q| q| ];

1072

simpl in |- *; auto; intro H;

1073

[ rewrite (IHp q); trivial

1074

| absurd ((p ?= q) <a href="Coq.Init.Datatypes.html#Gt">Gt</a> = <a href="Coq.Init.Datatypes.html#Eq">Eq</a>);

1075

[ elim (Pcompare_not_Eq p q); auto | assumption ]

1076

| discriminate H

1077

| absurd ((p ?= q) <a href="Coq.Init.Datatypes.html#Lt">Lt</a> = <a href="Coq.Init.Datatypes.html#Eq">Eq</a>);

1078

[ elim (Pcompare_not_Eq p q); auto | assumption ]

1079

| rewrite (IHp q); auto

1080

| discriminate H

1081

| discriminate H

1082

| discriminate H ].

1083

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

1084

1085

1086

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

1087

forall p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>, (p ?= q) <a href="Coq.Init.Datatypes.html#Gt">Gt</a> = <a href="Coq.Init.Datatypes.html#Lt">Lt</a> -> (p ?= q) <a href="Coq.Init.Datatypes.html#Eq">Eq</a> = <a href="Coq.Init.Datatypes.html#Lt">Lt</a>.

1088

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

1089

intro x; induction x as [x Hrecx| x Hrecx| ]; intro y;

1090

[ induction y as [y Hrecy| y Hrecy| ]

1091

| induction y as [y Hrecy| y Hrecy| ]

1092

| induction y as [y Hrecy| y Hrecy| ] ]; simpl in |- *;

1093

auto; discriminate || intros H; discriminate H.

1094

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

1095

1096

1097

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

1098

forall p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>, (p ?= q) <a href="Coq.Init.Datatypes.html#Lt">Lt</a> = <a href="Coq.Init.Datatypes.html#Gt">Gt</a> -> (p ?= q) <a href="Coq.Init.Datatypes.html#Eq">Eq</a> = <a href="Coq.Init.Datatypes.html#Gt">Gt</a>.

1099

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

1100

intro x; induction x as [x Hrecx| x Hrecx| ]; intro y;

1101

[ induction y as [y Hrecy| y Hrecy| ]

1102

| induction y as [y Hrecy| y Hrecy| ]

1103

| induction y as [y Hrecy| y Hrecy| ] ]; simpl in |- *;

1104

auto; discriminate || intros H; discriminate H.

1105

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

1106

1107

1108

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

1109

forall p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>, (p ?= q) <a href="Coq.Init.Datatypes.html#Lt">Lt</a> = <a href="Coq.Init.Datatypes.html#Lt">Lt</a> -> (p ?= q) <a href="Coq.Init.Datatypes.html#Eq">Eq</a> = <a href="Coq.Init.Datatypes.html#Lt">Lt</a> \/ p = q.

1110

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

1111

intro x; induction x as [p IHp| p IHp| ]; intro y; destruct y as [q| q| ];

1112

simpl in |- *; auto; try discriminate; intro H2; elim (IHp q H2);

1113

auto; intros E; rewrite E; auto.

1114

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

1115

1116

1117

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

1118

forall p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>, (p ?= q) <a href="Coq.Init.Datatypes.html#Gt">Gt</a> = <a href="Coq.Init.Datatypes.html#Gt">Gt</a> -> (p ?= q) <a href="Coq.Init.Datatypes.html#Eq">Eq</a> = <a href="Coq.Init.Datatypes.html#Gt">Gt</a> \/ p = q.

1119

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

1120

intro x; induction x as [p IHp| p IHp| ]; intro y; destruct y as [q| q| ];

1121

simpl in |- *; auto; try discriminate; intro H2; elim (IHp q H2);

1122

auto; intros E; rewrite E; auto.

1123

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

1124

1125

1126

<code class="keyword">Lemma</code> <a name="Dcompare"></a>Dcompare : forall r:<a href="Coq.Init.Datatypes.html#comparison">comparison</a>, r = <a href="Coq.Init.Datatypes.html#Eq">Eq</a> \/ r = <a href="Coq.Init.Datatypes.html#Lt">Lt</a> \/ r = <a href="Coq.Init.Datatypes.html#Gt">Gt</a>.

1127

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

1128

simple induction r; auto.

1129

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

1130

1131

1132

<code class="keyword">Ltac</code> ElimPcompare c1 c2 :=

1133

elim (<a href="Coq.NArith.BinPos.html#Dcompare">Dcompare</a> ((c1 ?= c2) <a href="Coq.Init.Datatypes.html#Eq">Eq</a>));

1134

[ idtac | let x := fresh "H" in

1135

(intro x; case x; clear x) ].

1136

1137

1138

<code class="keyword">Theorem</code> <a name="Pcompare_refl"></a>Pcompare_refl : forall p:<a href="Coq.NArith.BinPos.html#positive">positive</a>, (p ?= p) <a href="Coq.Init.Datatypes.html#Eq">Eq</a> = <a href="Coq.Init.Datatypes.html#Eq">Eq</a>.

1139

intro x; induction x as [x Hrecx| x Hrecx| ]; auto.

1140

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

1141

1142

1143

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

1144

forall (p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>) (r:<a href="Coq.Init.Datatypes.html#comparison">comparison</a>),

1145

<a href="Coq.Init.Datatypes.html#CompOpp">CompOpp</a> ((p ?= q) r) = (q ?= p) (<a href="Coq.Init.Datatypes.html#CompOpp">CompOpp</a> r).

1146

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

1147

intro x; induction x as [p IHp| p IHp| ]; intro y;

1148

[ destruct y as [p0| p0| ]

1149

| destruct y as [p0| p0| ]

1150

| destruct y as [p| p| ] ]; intro r;

1151

reflexivity ||

1152

(symmetry in |- *; assumption) || discriminate H || simpl in |- *;

1153

apply IHp || (try rewrite IHp); try reflexivity.

1154

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

1155

1156

1157

<code class="keyword">Lemma</code> <a name="ZC1"></a>ZC1 : forall p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>, (p ?= q) <a href="Coq.Init.Datatypes.html#Eq">Eq</a> = <a href="Coq.Init.Datatypes.html#Gt">Gt</a> -> (q ?= p) <a href="Coq.Init.Datatypes.html#Eq">Eq</a> = <a href="Coq.Init.Datatypes.html#Lt">Lt</a>.

1158

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

1159

intros; change <a href="Coq.Init.Datatypes.html#Eq">Eq</a> with (<a href="Coq.Init.Datatypes.html#CompOpp">CompOpp</a> <a href="Coq.Init.Datatypes.html#Eq">Eq</a>) in |- *.

1160

rewrite <- <a href="Coq.NArith.BinPos.html#Pcompare_antisym">Pcompare_antisym</a>; rewrite H; reflexivity.

1161

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

1162

1163

1164

<code class="keyword">Lemma</code> <a name="ZC2"></a>ZC2 : forall p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>, (p ?= q) <a href="Coq.Init.Datatypes.html#Eq">Eq</a> = <a href="Coq.Init.Datatypes.html#Lt">Lt</a> -> (q ?= p) <a href="Coq.Init.Datatypes.html#Eq">Eq</a> = <a href="Coq.Init.Datatypes.html#Gt">Gt</a>.

1165

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

1166

intros; change <a href="Coq.Init.Datatypes.html#Eq">Eq</a> with (<a href="Coq.Init.Datatypes.html#CompOpp">CompOpp</a> <a href="Coq.Init.Datatypes.html#Eq">Eq</a>) in |- *.

1167

rewrite <- <a href="Coq.NArith.BinPos.html#Pcompare_antisym">Pcompare_antisym</a>; rewrite H; reflexivity.

1168

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

1169

1170

1171

<code class="keyword">Lemma</code> <a name="ZC3"></a>ZC3 : forall p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>, (p ?= q) <a href="Coq.Init.Datatypes.html#Eq">Eq</a> = <a href="Coq.Init.Datatypes.html#Eq">Eq</a> -> (q ?= p) <a href="Coq.Init.Datatypes.html#Eq">Eq</a> = <a href="Coq.Init.Datatypes.html#Eq">Eq</a>.

1172

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

1173

intros; change <a href="Coq.Init.Datatypes.html#Eq">Eq</a> with (<a href="Coq.Init.Datatypes.html#CompOpp">CompOpp</a> <a href="Coq.Init.Datatypes.html#Eq">Eq</a>) in |- *.

1174

rewrite <- <a href="Coq.NArith.BinPos.html#Pcompare_antisym">Pcompare_antisym</a>; rewrite H; reflexivity.

1175

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

1176

1177

1178

<code class="keyword">Lemma</code> <a name="ZC4"></a>ZC4 : forall p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>, (p ?= q) <a href="Coq.Init.Datatypes.html#Eq">Eq</a> = <a href="Coq.Init.Datatypes.html#CompOpp">CompOpp</a> ((q ?= p) <a href="Coq.Init.Datatypes.html#Eq">Eq</a>).

1179

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

1180

intros; change <a href="Coq.Init.Datatypes.html#Eq">Eq</a> at 1 with (<a href="Coq.Init.Datatypes.html#CompOpp">CompOpp</a> <a href="Coq.Init.Datatypes.html#Eq">Eq</a>) in |- *.

1181

symmetry in |- *; apply <a href="Coq.NArith.BinPos.html#Pcompare_antisym">Pcompare_antisym</a>.

1182

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

1183

1184

1185

</code>

1186

1187

1188

Properties of subtraction on binary positive numbers

1189

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

1190

<code>

1191

1192

1193

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

1194

forall p:<a href="Coq.NArith.BinPos.html#positive_mask">positive_mask</a>, <a href="Coq.NArith.BinPos.html#Pdouble_mask">Pdouble_mask</a> p = <a href="Coq.NArith.BinPos.html#IsNul">IsNul</a> -> p = <a href="Coq.NArith.BinPos.html#IsNul">IsNul</a>.

1195

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

1196

destruct p; simpl in |- *; [ trivial | discriminate 1 | discriminate 1 ].

1197

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

1198

1199

1200

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

1201

1202

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

1203

simple induction p; intros; discriminate.

1204

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

1205

1206

1207

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

1208

forall p:<a href="Coq.NArith.BinPos.html#positive_mask">positive_mask</a>, <a href="Coq.NArith.BinPos.html#Pdouble_plus_one_mask">Pdouble_plus_one_mask</a> p = <a href="Coq.NArith.BinPos.html#IsPos">IsPos</a> <a href="Coq.NArith.BinPos.html#xH">xH</a> -> p = <a href="Coq.NArith.BinPos.html#IsNul">IsNul</a>.

1209

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

1210

destruct p; simpl in |- *; [ trivial | discriminate 1 | discriminate 1 ].

1211

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

1212

1213

1214

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

1215

forall p:<a href="Coq.NArith.BinPos.html#positive_mask">positive_mask</a>, <a href="Coq.NArith.BinPos.html#Pdouble_mask">Pdouble_mask</a> p <> <a href="Coq.NArith.BinPos.html#IsPos">IsPos</a> <a href="Coq.NArith.BinPos.html#xH">xH</a>.

1216

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

1217

simple induction p; intros; discriminate.

1218

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

1219

1220

1221

<code class="keyword">Theorem</code> <a name="Pminus_mask_diag"></a>Pminus_mask_diag : forall p:<a href="Coq.NArith.BinPos.html#positive">positive</a>, <a href="Coq.NArith.BinPos.html#Pminus_mask">Pminus_mask</a> p p = <a href="Coq.NArith.BinPos.html#IsNul">IsNul</a>.

1222

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

1223

intro x; induction x as [p IHp| p IHp| ];

1224

 [ simpl in |- *; rewrite IHp; simpl in |- *; trivial

1225

| simpl in |- *; rewrite IHp; auto

1226

| auto ].

1227

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

1228

1229

1230

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

1231

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

1232

<a href="Coq.NArith.BinPos.html#Pminus_mask">Pminus_mask</a> p q = <a href="Coq.NArith.BinPos.html#IsPos">IsPos</a> <a href="Coq.NArith.BinPos.html#xH">xH</a> -> <a href="Coq.NArith.BinPos.html#Pminus_mask_carry">Pminus_mask_carry</a> p q = <a href="Coq.NArith.BinPos.html#IsNul">IsNul</a>.

1233

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

1234

intro x; induction x as [p| p| ]; intro y; destruct y as [q| q| ];

1235

simpl in |- *; intro H; try discriminate H;

1236

[ absurd (<a href="Coq.NArith.BinPos.html#Pdouble_mask">Pdouble_mask</a> (<a href="Coq.NArith.BinPos.html#Pminus_mask">Pminus_mask</a> p q) = <a href="Coq.NArith.BinPos.html#IsPos">IsPos</a> <a href="Coq.NArith.BinPos.html#xH">xH</a>);

1237

[ apply double_eq_one_discr | assumption ]

1238

| assert (Heq : <a href="Coq.NArith.BinPos.html#Pminus_mask">Pminus_mask</a> p q = <a href="Coq.NArith.BinPos.html#IsNul">IsNul</a>);

1239

    [ apply double_plus_one_eq_one_inversion; assumption

1240

| rewrite Heq; reflexivity ]

1241

| assert (Heq : <a href="Coq.NArith.BinPos.html#Pminus_mask_carry">Pminus_mask_carry</a> p q = <a href="Coq.NArith.BinPos.html#IsNul">IsNul</a>);

1242

    [ apply double_plus_one_eq_one_inversion; assumption

1243

| rewrite Heq; reflexivity ]

1244

| absurd (<a href="Coq.NArith.BinPos.html#Pdouble_mask">Pdouble_mask</a> (<a href="Coq.NArith.BinPos.html#Pminus_mask">Pminus_mask</a> p q) = <a href="Coq.NArith.BinPos.html#IsPos">IsPos</a> <a href="Coq.NArith.BinPos.html#xH">xH</a>);

1245

[ apply double_eq_one_discr | assumption ]

1246

| destruct p; simpl in |- *;

1247

[ discriminate H | discriminate H | reflexivity ] ].

1248

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

1249

1250

1251

</code>

1252

1253

1254

Properties of subtraction valid only for x>y

1255

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

1256

<code>

1257

1258

1259

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

1260

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

1261

(p ?= q) <a href="Coq.Init.Datatypes.html#Eq">Eq</a> = <a href="Coq.Init.Datatypes.html#Gt">Gt</a> ->

1262

exists h : <a href="Coq.NArith.BinPos.html#positive">positive</a>,

1263

<a href="Coq.NArith.BinPos.html#Pminus_mask">Pminus_mask</a> p q = <a href="Coq.NArith.BinPos.html#IsPos">IsPos</a> h /\

1264

q + h = p /\ (h = <a href="Coq.NArith.BinPos.html#xH">xH</a> \/ <a href="Coq.NArith.BinPos.html#Pminus_mask_carry">Pminus_mask_carry</a> p q = <a href="Coq.NArith.BinPos.html#IsPos">IsPos</a> (<a href="Coq.NArith.BinPos.html#Ppred">Ppred</a> h)).

1265

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

1266

intro x; induction x as [p| p| ]; intro y; destruct y as [q| q| ];

1267

simpl in |- *; intro H; try discriminate H.

1268

destruct (IHp q H) as [z [H4 [H6 H7]]]; exists (<a href="Coq.NArith.BinPos.html#xO">xO</a> z); split.

1269

rewrite H4; reflexivity.

1270

split.

1271

simpl in |- *; rewrite H6; reflexivity.

1272

right; clear H6; destruct (<a href="Coq.NArith.BinPos.html#ZL11">ZL11</a> z) as [H8| H8];

1273

[ rewrite H8; rewrite H8 in H4; rewrite <a href="Coq.NArith.BinPos.html#ZL10">ZL10</a>;

1274

[ reflexivity | assumption ]

1275

| clear H4; destruct H7 as [H9| H9];

1276

[ absurd (z = <a href="Coq.NArith.BinPos.html#xH">xH</a>); assumption

1277

| rewrite H9; clear H9; destruct z as [p0| p0| ];

1278

[ reflexivity | reflexivity | absurd (xH = xH); trivial ] ] ].

1279

case <a href="Coq.NArith.BinPos.html#Pcompare_Gt_Gt">Pcompare_Gt_Gt</a> with (1 := H);

1280

[ intros H3; elim (IHp q H3); intros z H4; exists (<a href="Coq.NArith.BinPos.html#xI">xI</a> z); elim H4;

1281

intros H5 H6; elim H6; intros H7 H8; split;

1282

[ simpl in |- *; rewrite H5; auto

1283

| split;

1284

         [ simpl in |- *; rewrite H7; trivial

1285

| right;

1286

change (Pdouble_mask (Pminus_mask p q) = IsPos (Ppred (xI z)))

1287

in |- *; rewrite H5; auto ] ]

1288

| intros H3; exists <a href="Coq.NArith.BinPos.html#xH">xH</a>; rewrite H3; split;

1289

[ simpl in |- *; rewrite Pminus_mask_diag; auto | split; auto ] ].

1290

exists (<a href="Coq.NArith.BinPos.html#xO">xO</a> p); auto.

1291

destruct (IHp q) as [z [H4 [H6 H7]]].

1292

apply <a href="Coq.NArith.BinPos.html#Pcompare_Lt_Gt">Pcompare_Lt_Gt</a>; assumption.

1293

destruct (<a href="Coq.NArith.BinPos.html#ZL11">ZL11</a> z) as [vZ| ];

1294

[ exists <a href="Coq.NArith.BinPos.html#xH">xH</a>; split;

1295

[ rewrite <a href="Coq.NArith.BinPos.html#ZL10">ZL10</a>; [ reflexivity | rewrite vZ in H4; assumption ]

1296

| split;

1297

[ simpl in |- *; rewrite Pplus_one_succ_r; rewrite <- vZ;

1298

rewrite H6; trivial

1299

| auto ] ]

1300

| exists (<a href="Coq.NArith.BinPos.html#xI">xI</a> (<a href="Coq.NArith.BinPos.html#Ppred">Ppred</a> z)); destruct H7 as [| H8];

1301

[ absurd (z = <a href="Coq.NArith.BinPos.html#xH">xH</a>); assumption

1302

| split;

1303

[ rewrite H8; trivial

1304

| split;

1305

[ simpl in |- *; rewrite <a href="Coq.NArith.BinPos.html#Pplus_carry_pred_eq_plus">Pplus_carry_pred_eq_plus</a>;

1306

[ rewrite H6; trivial | assumption ]

1307

| right; rewrite H8; reflexivity ] ] ] ].

1308

destruct (IHp q H) as [z [H4 [H6 H7]]].

1309

exists (<a href="Coq.NArith.BinPos.html#xO">xO</a> z); split;

1310

[ rewrite H4; auto

1311

| split;

1312

[ simpl in |- *; rewrite H6; reflexivity

1313

| right;

1314

change

1315

(<a href="Coq.NArith.BinPos.html#Pdouble_plus_one_mask">Pdouble_plus_one_mask</a> (<a href="Coq.NArith.BinPos.html#Pminus_mask_carry">Pminus_mask_carry</a> p q) =

1316

<a href="Coq.NArith.BinPos.html#IsPos">IsPos</a> (<a href="Coq.NArith.BinPos.html#Pdouble_minus_one">Pdouble_minus_one</a> z)) in |- *;

1317

destruct (<a href="Coq.NArith.BinPos.html#ZL11">ZL11</a> z) as [H8| H8];

1318

[ rewrite H8; simpl in |- *;

1319

assert (H9 : <a href="Coq.NArith.BinPos.html#Pminus_mask_carry">Pminus_mask_carry</a> p q = <a href="Coq.NArith.BinPos.html#IsNul">IsNul</a>);

1320

[ apply ZL10; rewrite <- H8; assumption

1321

| rewrite H9; reflexivity ]

1322

| destruct H7 as [H9| H9];

1323

[ absurd (z = <a href="Coq.NArith.BinPos.html#xH">xH</a>); auto

1324

| rewrite H9; destruct z as [p0| p0| ]; simpl in |- *;

1325

[ reflexivity

1326

| reflexivity

1327

| absurd (<a href="Coq.NArith.BinPos.html#xH">xH</a> = <a href="Coq.NArith.BinPos.html#xH">xH</a>); [ assumption | reflexivity ] ] ] ] ] ].

1328

exists (<a href="Coq.NArith.BinPos.html#Pdouble_minus_one">Pdouble_minus_one</a> p); split;

1329

[ reflexivity

1330

| clear IHp; split;

1331

[ destruct p; simpl in |- *;

1332

         [ reflexivity

1333

| rewrite Psucc_o_double_minus_one_eq_xO; reflexivity

1334

| reflexivity ]

1335

| destruct p; [ right | right | left ]; reflexivity ] ].

1336

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

1337

1338

1339

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

1340

forall p q:<a href="Coq.NArith.BinPos.html#positive">positive</a>, (p ?= q) <a href="Coq.Init.Datatypes.html#Eq">Eq</a> = <a href="Coq.Init.Datatypes.html#Gt">Gt</a> -> q + (p - q) = p.

1341

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

1342

intros x y H; elim <a href="Coq.NArith.BinPos.html#Pminus_mask_Gt">Pminus_mask_Gt</a> with (1 := H); intros z H1; elim H1;

1343

intros H2 H3; elim H3; intros H4 H5; unfold Pminus in |- *;

1344

rewrite H2; exact H4.

1345

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

1346

</code>

1347

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

1348

</body>

1349

</html>

b'\\ No newline at end of file'

Older »