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

<LI><A HREF="#htoc65">55  My goal contains some existential hypotheses, how can I use it and decompose my knowledge about this new thing into different hypotheses?</A>

130

<LI><A HREF="#htoc66">56  My goal is an equality, how can I swap the left and right hand terms?</A>

131

<LI><A HREF="#htoc67">57  My hypothesis is an equality, how can I swap the left and right hand terms?</A>

132

<LI><A HREF="#htoc68">58  My goal is an equality, how can I prove it by transitivity?</A>

133

<LI><A HREF="#htoc69">59  My goal would be solvable using <TT>apply;assumption</TT> if it would not create meta-variables, how can I prove it?</A>

134

<LI><A HREF="#htoc70">60  My goal is solvable by some lemma within a set of lemmas and I don't want to remember which one, how can I prove it?</A>

135

<LI><A HREF="#htoc71">61  My goal is one of the hypotheses, how can I prove it?</A>

136

<LI><A HREF="#htoc72">62  My goal appears twice in the hypotheses and I want to choose which one is used, how can I do it?</A>

137

<LI><A HREF="#htoc73">63  What can be the difference between applying one hypothesis or another in the context of the last question?</A>

138

<LI><A HREF="#htoc74">64  My goal is a propositional tautology, how can I prove it?</A>

139

<LI><A HREF="#htoc75">65  My goal is a first order formula, how can I prove it?</A>

140

<LI><A HREF="#htoc76">66  My goal is solvable by a sequence of rewrites, how can I prove it?</A>

141

<LI><A HREF="#htoc77">67  My goal is a disequality solvable by a sequence of rewrites, how can I prove it?</A>

142

<LI><A HREF="#htoc78">68  My goal is an equality on some ring (e.g. natural numbers), how can I prove it?</A>

143

<LI><A HREF="#htoc79">69  My goal is an equality on some field (e.g. real numbers), how can I prove it?</A>

144

<LI><A HREF="#htoc80">70  My goal is an inequality on integers in Presburger's arithmetic (an expression build from +,-,constants and variables), how can I prove it?</A>

145

<LI><A HREF="#htoc81">71  My goal is an equation solvable using equational hypothesis on some ring (e.g. natural numbers), how can I prove it?</A>

146

</UL>

147

<LI><A HREF="#htoc82">6.2  Tactics usage</A>

148

149

<A HREF="#htoc83">72  I want to state a fact that I will use later as an hypothesis, how can I do it?</A>

150

<LI><A HREF="#htoc84">73  I want to state a fact that I will use later as an hypothesis and prove it later, how can I do it?</A>

151

<LI><A HREF="#htoc85">74  What is the difference between <TT>Qed</TT> and <TT>Defined</TT>?</A>

152

<LI><A HREF="#htoc86">75  How can I know what a tactic does?</A>

153

154

<LI><A HREF="#htoc88">77  What is <TT>eauto</TT>?</A>

155

<LI><A HREF="#htoc89">78  How can I speed up <TT>auto</TT>?</A>

156

<LI><A HREF="#htoc90">79  What is the equivalent of <TT>tauto</TT> for classical logic?</A>

157

<LI><A HREF="#htoc91">80  I want to replace some term with another in the goal, how can I do it?</A>

158

<LI><A HREF="#htoc92">81  I want to replace some term with another in an hypothesis, how can I do it?</A>

159

<LI><A HREF="#htoc93">82  I want to replace some symbol with its definition, how can I do it?</A>

160

<LI><A HREF="#htoc94">83  How can I reduce some term?</A>

161

<LI><A HREF="#htoc95">84  How can I declare a shortcut for some term?</A>

162

<LI><A HREF="#htoc96">85  How can I perform case analysis?</A>

163

<LI><A HREF="#htoc97">86  Why should I name my intros?</A>

164

<LI><A HREF="#htoc98">87  How can I automatize the naming?</A>

165

<LI><A HREF="#htoc99">88  I want to automatize the use of some tactic, how can I do it?</A>

166

<LI><A HREF="#htoc100">89  I want to execute the <TT>p</TT>roof with tactic only if it solves the goal, how can I do it?</A>

167

<LI><A HREF="#htoc101">90  How can I do the opposite of the <TT>intro</TT> tactic?</A>

168

<LI><A HREF="#htoc102">91  One of the hypothesis is an equality between a variable and some term, I want to get rid of this variable, how can I do it?</A>

169

<LI><A HREF="#htoc103">92  What can I do if I get ``<TT>generated subgoal term has metavariables in it </TT>''?</A>

170

<LI><A HREF="#htoc104">93  How can I instantiate some metavariable?</A>

171

<LI><A HREF="#htoc105">94  What is the use of the <TT>pattern</TT> tactic?</A>

172

<LI><A HREF="#htoc106">95  What is the difference between assert, cut and generalize?</A>

173

<LI><A HREF="#htoc107">96  What can I do if Coqcan not infer some implicit argument ?</A>

174

<LI><A HREF="#htoc108">97  How can I explicit some implicit argument ?</A>

175

</UL>

176

<LI><A HREF="#htoc109">6.3  Proof management</A>

177

178

<A HREF="#htoc110">98  How can I change the order of the subgoals?</A>

179

<LI><A HREF="#htoc111">99  How can I change the order of the hypothesis?</A>

180

<LI><A HREF="#htoc112">100  How can I change the name of an hypothesis?</A>

181

<LI><A HREF="#htoc113">101  How can I delete some hypothesis?</A>

182

<LI><A HREF="#htoc114">102  How can use a proof which is not finished?</A>

183

<LI><A HREF="#htoc115">103  How can I state a conjecture?</A>

184

<LI><A HREF="#htoc116">104  What is the difference between a lemma, a fact and a theorem?</A>

185

<LI><A HREF="#htoc117">105  How can I organize my proofs?</A>

186

</UL>

187

</UL>

188

<LI><A HREF="#htoc118">7  Inductive and Co-inductive types</A>

189

190

<A HREF="#htoc119">7.1  General</A>

191

192

<A HREF="#htoc120">106  How can I prove that two constructors are different?</A>

193

<LI><A HREF="#htoc121">107  During an inductive proof, how to get rid of impossible cases of an inductive definition?</A>

194

<LI><A HREF="#htoc122">108  How can I prove that 2 terms in an inductive set are equal? Or different?</A>

195

<LI><A HREF="#htoc123">109  Why is the proof of <TT>0+n=n</TT> on natural numbers

196

trivial but the proof of <TT>n+0=n</TT> is not?</A>

197

<LI><A HREF="#htoc124">110  Why is dependent elimination in Prop not

198

available by default?</A>

199

</UL>

200

<LI><A HREF="#htoc125">7.2  Recursion</A>

201

202

<A HREF="#htoc126">111  Why can't I define a non terminating program?</A>

203

<LI><A HREF="#htoc127">112  Why only structurally well-founded loops are allowed?</A>

204

<LI><A HREF="#htoc128">113  How to define loops based on non structurally smaller

205

recursive calls?</A>

206

<LI><A HREF="#htoc129">114  What is behind the accessibility and well-foundedness proofs?</A>

207

<LI><A HREF="#htoc130">115  How to perform double induction?</A>

208

<LI><A HREF="#htoc131">116  How to define a function by double recursion?</A>

209

<LI><A HREF="#htoc132">117  How to perform nested induction?</A>

210

<LI><A HREF="#htoc133">118  How to define a function by nested recursion?</A>

211

</UL>

212

<LI><A HREF="#htoc134">7.3  Co-inductive types</A>

213

214

<A HREF="#htoc135">119  I have a cofixpoint t:=F(t) and I want to prove t=F(t). How to do it?</A>

215

</UL>

216

</UL>

217

<LI><A HREF="#htoc136">8  Syntax and notations</A>

218

<UL>

219

220

<A HREF="#htoc137">120  I do not want to type ``forall'' because it is too long, what can I do?</A>

221

<LI><A HREF="#htoc138">121  How can I define a notation for square?</A>

222

<LI><A HREF="#htoc139">122  Why ``no associativity'' and ``left associativity'' at the same level does not work?</A>

223

<LI><A HREF="#htoc140">123  How can I know the associativity associated with a level?</A>

224

</UL>

225

</UL>

226

<LI><A HREF="#htoc141">9  Modules</A>

227

228

<UL>

229

230

231

<LI><A HREF="#htoc144">125  Why do I always get the same error message?</A>

232

<LI><A HREF="#htoc145">126  Is there any printing command in Ltac?</A>

233

<LI><A HREF="#htoc146">127  What is the syntax for let in Ltac?</A>

234

<LI><A HREF="#htoc147">128  What is the syntax for pattern matching in Ltac?</A>

235

<LI><A HREF="#htoc148">129  What is the semantics for match goal?</A>

236

<LI><A HREF="#htoc149">130  How can I generate a new name?</A>

237

<LI><A HREF="#htoc150">131  How can I define static and dynamic code?</A>

238

</UL>

239

</UL>

240

<LI><A HREF="#htoc151">11  Tactics written in Ocaml</A>

241

<UL>

242

243

<A HREF="#htoc152">132  Can you show me an example of a tactic written in OCaml?</A>

244

</UL>

245

</UL>

246

<LI><A HREF="#htoc153">12  Case studies</A>

247

<UL>

248

249

<A HREF="#htoc154">133  How can I define vectors or lists of size n?</A>

250

<LI><A HREF="#htoc155">134  How to prove that 2 sets are different?</A>

251

<LI><A HREF="#htoc156">135  Is there an axiom-free proof of Streicher's axiom K for

252

the equality on <TT>nat</TT>?</A>

253

<LI><A HREF="#htoc157">136  How to prove that two proofs of <TT>n<=m</TT> on <TT>nat</TT> are equal?</A>

254

<LI><A HREF="#htoc158">137  How to exploit equalities on sets</A>

255

<LI><A HREF="#htoc159">138  I have a problem of dependent elimination on

256

proofs, how to solve it?</A>

257

<LI><A HREF="#htoc160">139  And what if I want to prove the following?</A>

258

</UL>

259

</UL>

260

<LI><A HREF="#htoc161">13  Publishing tools</A>

261

<UL>

262

263

<A HREF="#htoc162">140  How can I generate some latex from my development?</A>

264

<LI><A HREF="#htoc163">141  How can I generate some HTML from my development?</A>

265

<LI><A HREF="#htoc164">142  How can I generate some dependency graph from my development?</A>

266

<LI><A HREF="#htoc165">143  How can I cite some Coq in my latex document?</A>

267

<LI><A HREF="#htoc166">144  How can I cite the Coq reference manual?</A>

268

<LI><A HREF="#htoc167">145  Where can I publish my developments in Coq?</A>

269

<LI><A HREF="#htoc168">146  How can I read my proof in natural language?</A>

270

</UL>

271

</UL>

272

<LI><A HREF="#htoc169">14  CoqIde</A>

273

<UL>

274

275

<A HREF="#htoc170">147  What is CoqIde?</A>

276

<LI><A HREF="#htoc171">148  How to enable Emacs keybindings?</A>

277

<LI><A HREF="#htoc172">149  How to enable antialiased fonts?</A>

278

<LI><A HREF="#htoc173">150  How to use those Forall and Exists pretty symbols?</A>

279

<LI><A HREF="#htoc174">151  How to define an input method for non ASCII symbols?</A>

280

<LI><A HREF="#htoc175">152  How to build a custom CoqIde with user ml code?</A>

281

<LI><A HREF="#htoc176">153  How to customize the shortcuts for menus?</A>

282

<LI><A HREF="#htoc177">154  What encoding should I use? What is this \x{iiii} in my file?</A>

283

</UL>

284

</UL>

285

<LI><A HREF="#htoc178">15  Extraction</A>

286

<UL>

287

288

<A HREF="#htoc179">155  What is program extraction?</A>

289

<LI><A HREF="#htoc180">156  Which language can I extract to?</A>

290

<LI><A HREF="#htoc181">157  How can I extract an incomplete proof?</A>

291

</UL>

292

</UL>

293

<LI><A HREF="#htoc182">16  Glossary</A>

294

<UL>

295

296

<A HREF="#htoc183">158  Can you explain me what an evaluable constant is?</A>

297

298

<LI><A HREF="#htoc185">160  What is a meta variable?</A>

299

<LI><A HREF="#htoc186">161  What is Gallina?</A>

300

<LI><A HREF="#htoc187">162  What is The Vernacular?</A>

301

<LI><A HREF="#htoc188">163  What is a dependent type?</A>

302

<LI><A HREF="#htoc189">164  What is a proof by reflection?</A>

303

<LI><A HREF="#htoc190">165  What is intuitionistic logic?</A>

304

<LI><A HREF="#htoc191">166  What is proof-irrelevance?</A>

305

<LI><A HREF="#htoc192">167  What is the difference between opaque and transparent?</A>

306

</UL>

307

</UL>

308

<LI><A HREF="#htoc193">17  Troubleshooting</A>

309

<UL>

310

311

312

<LI><A HREF="#htoc195">169  Why <TT>Reset Initial.</TT> does not work when using <TT>coqc</TT>?</A>

313

<LI><A HREF="#htoc196">170  What can I do if I get ``No more subgoals but non-instantiated existential variables''?</A>

314

<LI><A HREF="#htoc197">171  What can I do if I get ``Cannot solve a second-order unification problem''?</A>

315

<LI><A HREF="#htoc198">172  Why does Coq tell me that <TT>{x:A|(P x)}</TT> is not convertible with <TT>(sig A P)</TT>?</A>

316

<LI><A HREF="#htoc199">173  I copy-paste a term and Coq says it is not convertible

317

to the original term. Sometimes it even says the copied term is not

318

well-typed.</A>

319

</UL>

320

</UL>

321

<LI><A HREF="#htoc200">18  Conclusion and Farewell.</A>

322

<UL>

323

324

<A HREF="#htoc201">174  What if my question isn't answered here?</A>

325

</UL>

326

</UL>

327

</UL>

328

329

330

331

<H2><A NAME="htoc1">1</A>  Introduction</H2>

332

333

This FAQ is the sum of the questions that came to mind as we developed

334

proofs in Coq. Since we are singularly short-minded, we wrote the

335

answers we found on bits of papers to have them at hand whenever the

336

situation occurs again. This is pretty much the result of that: a

337

collection of tips one can refer to when proofs become intricate. Yes,

338

this means we won't take the blame for the shortcomings of this

339

FAQ. But if you want to contribute and send in your own question and

340

answers, feel free to write to us...

341

342

343

344

<H2><A NAME="htoc2">2</A>  Presentation</H2>

345

346

347

348

349

350

The Coq tool is a formal proof management system: a proof done with Coq is mechanically checked by the machine.

351

In particular, Coq allows:

352

353

the definition of functions or predicates,

354

<LI>to state mathematical theorems and software specifications,

355

<LI>to develop interactively formal proofs of these theorems,

356

<LI>to check these proofs by a small certification "kernel".

357

</UL>

358

Coq is based on a logical framework called "Calculus of Inductive Constructions" extended by a modular development system for theories.

359

360

361

362

<H4><A NAME="htoc4">2</A>  Did you really need to name it like that?</H4>

363

364

Some French computer scientists have a tradition of naming their

365

software as animal species: Caml, Elan, Foc or Phox are examples

366

of this tacit convention. In French, ``coq'' means rooster, and it

367

sounds like the initials of the Calculus of Constructions CoC on which

368

it is based.

369

370

371

372

<H4><A NAME="htoc5">3</A>  Is Coq a theorem prover?</H4>

373

374

Coq comes with a few decision procedures (on propositional

375

calculus, Presburger's arithmetic, ring and field simplification,

376

resolution, ...) but the main style for proving theorems is

377

interactively by using LCF-style tactics.

378

379

380

381

<H4><A NAME="htoc6">4</A>  What are the other theorem provers?</H4>

382

383

Many other theorem provers are available for use nowadays.

384

Isabelle, HOL, HOL Light, Lego, Nuprl, PVS are examples of provers that are fairly similar

385

to Coq by the way they interact with the user. Other relatives of

386

Coq are ACL2, Alfa, Elf, Kiv, Mizar, NqThm,

387

Omega...

388

389

390

391

392

<H4><A NAME="htoc7">5</A>  Who do I have to trust when I see a proof checked by Coq?</H4>

393

394

You have to trust:

395

396

The theory behind Coq<DD> The theory of Coq version 8.0 is

397

generally admitted to be consistent wrt Zermelo-Fraenkel set theory +

398

inaccessibles cardinals. Proofs of consistency of subsystems of the

399

theory of Coq can be found in the literature.

400

<DT>The Coq kernel implementation<DD> You have to trust that the

401

implementation of the Coq kernel mirrors the theory behind Coq. The

402

kernel is intentionally small to limit the risk of conceptual or

403

accidental implementation bugs.

404

<DT>The Objective Caml compiler<DD> The Coq kernel is written using the

405

Objective Caml language but it uses only the most standard features

406

(no object, no label ...), so that it is highly unprobable that an

407

Objective Caml bug breaks the consistency of Coq without breaking all

408

other kinds of features of Coq or of other software compiled with

409

Objective Caml.

410

<DT>Your hardware<DD> In theory, if your hardware does not work

411

properly, it can accidentally be the case that False becomes

412

provable. But it is more likely the case that the whole Coq system

413

will be unusable. You can check your proof using different computers

414

if you feel the need to.

415

<DT>Your axioms<DD> Your axioms must be consistent with the theory

416

behind Coq.

417

</DL>

418

419

420

<H4><A NAME="htoc8">6</A>  Where can I find information about the theory behind Coq?</H4>

421

422

423

The Calculus of Inductive Constructions<DD> The

424

<A HREF="http://coq.inria.fr/doc/Reference-Manual006.html">corresponding</A>

425

chapter and the chapter on

426

<A HREF="http://coq.inria.fr/doc/Reference-Manual007.html">modules</A> in

427

the Coq Reference Manual.

428

<DT>Type theory<DD> A book [<A HREF="#ProofsTypes"><CITE>10</CITE></A>] or some lecture

429

notes [<A HREF="#Types:Dowek"><CITE>7</CITE></A>].

430

<DT>Inductive types<DD>

431

Christine Paulin-Mohring's habilitation thesis [<A HREF="#Pau96b"><CITE>17</CITE></A>].

432

<DT>Co-Inductive types<DD>

433

Eduardo Gim�nez' thesis [<A HREF="#EGThese"><CITE>8</CITE></A>].

434

<DT>Miscellaneous<DD> A

435

<A HREF="http://coq.inria.fr/doc/biblio.html">bibliography</A> about Coq

436

</DL>

437

438

439

<H4><A NAME="htoc9">7</A>  How can I use Coq to prove programs?</H4>

440

441

You can either extract a program from a proof by using the extraction

442

mechanism or use dedicated tools, such as

443

<A HREF="http://why.lri.fr">Why</A>,

444

<A HREF="http://krakatoa.lri.fr">Krakatoa</A>,

445

<A HREF="http://why.lri.fr/caduceus/index.en.html">Caduceus</A>, to prove

446

annotated programs written in other languages.

447

448

449

450

<H4><A NAME="htoc10">8</A>  How many Coq users are there?</H4>

451

452

An estimation is about 100 regular users.

453

454

455

456

457

458

The first implementation is from 1985 (it was named CoC which is

459

the acronym of the name of the logic it implemented: the Calculus of

460

Constructions). The first official release of Coq (version 4.10)

461

was distributed in 1989.

462

463

464

465

<H4><A NAME="htoc12">10</A>  What are the Coq-related tools?</H4>

466

467

468

Coqide<DD> A GTK based GUI for Coq.

469

<DT>Pcoq<DD> A GUI for Coq with proof by pointing and pretty printing.

470

<DT>Helm/Mowgli<DD> A rendering, searching and publishing tool.

471

<DT>Why<DD> A back-end generator of verification conditions.

472

<DT>Krakatoa<DD> A Java code certification tool that uses both Coq and Why to verify the soundness of implementations with regards to the specifications.

473

<DT>Caduceus<DD> A C code certification tool that uses both Coq and Why.

474

<DT>coqwc<DD> A tool similar to <TT>wc</TT> to count lines in Coq files.

475

<DT>coq-tex<DD> A tool to insert Coq examples within .tex files.

476

<DT>coqdoc<DD> A documentation tool for Coq.

477

<DT>Proof General<DD> A emacs mode for Coq and many other proof assistants.

478

<DT>Foc<DD> The <A HREF="http://www-spi.lip6.fr/foc/index-en.html">Foc</A> project aims at building an environment to develop certified computer algebra libraries.

479

</DL>

480

481

482

<H4><A NAME="htoc13">11</A>  What are the high-level tactics of Coq</H4>

483

484

485

Decision of quantifier-free Presburger's Arithmetic

486

<LI>Simplification of expressions on rings and fields

487

<LI>Decision of closed systems of equations

488

<LI>Semi-decision of first-order logic

489

<LI>Prolog-style proof search, possibly involving equalities

490

</UL>

491

492

493

<H4><A NAME="htoc14">12</A>  What are the main libraries available for Coq</H4>

494

495

496

Basic Peano's arithmetic, binary integer numbers, rational numbers,

497

<LI>Real analysis,

498

<LI>Libraries for lists, boolean, maps, floating-point numbers,

499

<LI>Libraries for relations, sets and constructive algebra,

500

<LI>Geometry

501

</UL>

502

503

504

<H4><A NAME="htoc15">13</A>  What are the academic applications for Coq?</H4>

505

506

Coq is used for formalizing mathematical theories, for teaching,

507

and for proving properties of algorithms or programs libraries.

508

509

The largest mathematical formalization has been done at the University

510

of Nijmegen (see the

511

<A HREF="http://vacuumcleaner.cs.kun.nl/c-corn">Constructive Coq

512

Repository at Nijmegen</A>).

513

514

515

516

<H4><A NAME="htoc16">14</A>  What are the industrial applications for Coq?</H4>

517

518

Coq is used e.g. to prove properties of the JavaCard system

519

(especially by the companies Schlumberger and Trusted Logic). It has

520

also been used to formalize the semantics of the Lucid-Synchrone

521

data-flow synchronous calculus used by Esterel-Technologies.

522

523

524

525

<H2><A NAME="htoc17">3</A>  Documentation</H2>

526

527

528

529

<H4><A NAME="htoc18">15</A>  Where can I find documentation about Coq?</H4>

530

531

All the documentation about Coq, from the reference manual [<A HREF="#Coq:manual"><CITE>15</CITE></A>] to

532

friendly tutorials [<A HREF="#Coq:Tutorial"><CITE>14</CITE></A>] and documentation of the standard library, is available

533

<A HREF="http://coq.inria.fr/doc-eng.html">online</A>.

534

All these documents are viewable either in browsable HTML, or as

535

downloadable postscripts.

536

537

538

539

<H4><A NAME="htoc19">16</A>  Where can I find this FAQ on the web?</H4>

540

541

This FAQ is available online at <A HREF="http://coq.inria.fr/doc/faq.html"><TT>http://coq.inria.fr/doc/faq.html</TT></A>.

542

543

544

545

<H4><A NAME="htoc20">17</A>  How can I submit suggestions / improvements / additions for this FAQ?</H4>

546

547

This FAQ is unfinished (in the sense that there are some obvious

548

sections that are missing). Please send contributions to <TT>Florent.Kirchner at lix.polytechnique.fr</TT> and <TT>Julien.Narboux at inria.fr</TT>.

549

550

551

552

<H4><A NAME="htoc21">18</A>  Is there any mailing list about Coq?</H4>

553

554

The main Coq mailing list is <TT>coq-club@coq.inria.fr</TT>, which

555

broadcasts questions and suggestions about the implementation, the

556

logical formalism or proof developments. See

557

<A HREF="http://coq.inria.fr/mailman/listinfo/coq-club"><TT>http://coq.inria.fr/mailman/listinfo/coq-club</TT></A> for

558

subscription. For bugs reports see question <A HREF="#coqbug">23</A>.

559

560

561

562

<H4><A NAME="htoc22">19</A>  Where can I find an archive of the list?</H4>

563

564

The archives of the Coq mailing list are available at

565

<A HREF="http://coq.inria.fr/pipermail/coq-club"><TT>http://coq.inria.fr/pipermail/coq-club</TT></A>.

566

567

568

569

<H4><A NAME="htoc23">20</A>  How can I be kept informed of new releases of Coq?</H4>

570

571

New versions of Coq are announced on the coq-club mailing list. If you only want to receive information about new releases, you can subscribe to Coq on <A HREF="http://freshmeat.net/projects/coq/"><TT>http://freshmeat.net/projects/coq/</TT></A>.

572

573

574

575

<H4><A NAME="htoc24">21</A>  Is there any book about Coq?</H4>

576

577

The first book on Coq, Yves Bertot and Pierre Cast�ran's Coq'Art has been published by Springer-Verlag in 2004:

578

579

``This book provides a pragmatic introduction to the development of

580

proofs and certified programs using Coq. With its large collection of

581

examples and exercises it is an invaluable tool for researchers,

582

students, and engineers interested in formal methods and the

583

development of zero-default software.''

584

</BLOCKQUOTE>

585

586

587

<H4><A NAME="htoc25">22</A>  Where can I find some Coq examples?</H4>

588

589

There are examples in the manual [<A HREF="#Coq:manual"><CITE>15</CITE></A>] and in the

590

Coq'Art [<A HREF="#Coq:coqart"><CITE>1</CITE></A>] exercises <A HREF="http://www.labri.fr/Perso/ casteran/CoqArt/index.html"><TT>http://www.labri.fr/Perso/~casteran/CoqArt/index.html</TT></A>.

591

You can also find large developments using

592

Coq in the Coq user contributions:

593

<A HREF="http://coq.inria.fr/contrib-eng.html"><TT>http://coq.inria.fr/contrib-eng.html</TT></A>.

594

595

596

597

<H4><A NAME="htoc26">23</A>  How can I report a bug?</H4>

598

599

You can use the web interface at <A HREF="http://coq.inria.fr/bin/coq-bugs"><TT>http://coq.inria.fr/bin/coq-bugs</TT></A>.

600

601

602

603

<H2><A NAME="htoc27">4</A>  Installation</H2>

604

605

606

607

<H4><A NAME="htoc28">24</A>  What is the license of Coq?</H4>

608

609

The main files are distributed under the GNU Lesser General License

610

(LGPL). A few contributions are GPL.

611

612

613

614

<H4><A NAME="htoc29">25</A>  Where can I find the sources of Coq?</H4>

615

616

The sources of Coq can be found online in the tar.gz'ed packages

617

(<A HREF="http://coq.inria.fr/distrib-eng.html"><TT>http://coq.inria.fr/distrib-eng.html</TT></A>). Development sources can

618

be accessed via anonymous CVS: <A HREF="http://coqcvs.inria.fr/"><TT>http://coqcvs.inria.fr/</TT></A>

619

620

621

622

<H4><A NAME="htoc30">26</A>  On which platform is Coq available?</H4>

623

624

Compiled binaries are available for Linux, MacOS X, Solaris, and

625

Windows. The sources can be easily compiled on all platforms supporting Objective Caml.

626

627

628

629

<H2><A NAME="htoc31">5</A>  The logic of Coq</H2>

630

631

632

633

<H3><A NAME="htoc32">5.1</A>  General</H3>

634

635

636

637

<H4><A NAME="htoc33">27</A>  What is the logic of Coq?</H4>

638

639

Coq is based on an axiom-free type theory called

640

the Calculus of Inductive Constructions (see Coquand [<A HREF="#CoHu86"><CITE>5</CITE></A>]

641

and Coquand--Paulin-Mohring [<A HREF="#CoPa89"><CITE>6</CITE></A>]). It includes higher-order

642

functions and predicates, inductive and co-inductive datatypes and

643

predicates, and a stratified hierarchy of sets.

644

645

646

647

<H4><A NAME="htoc34">28</A>  Is Coq's logic intuitionistic or classical?</H4>

648

649

Coq theory is basically intuitionistic

650

(i.e. excluded-middle A\/� A is not granted by default) with

651

the possibility to reason classically on demand by requiring an

652

optional axiom stating A\/� A.

653

654

655

656

<H4><A NAME="htoc35">29</A>  Can I define non-terminating programs in Coq?</H4>

657

658

No, all programs in Coq are terminating. Especially, loops

659

must come with an evidence of their termination.

660

661

662

663

<H4><A NAME="htoc36">30</A>  How is equational reasoning working in Coq?</H4>

664

665

Coq comes with an internal notion of computation called

666

conversion (e.g. (x+1)+y is internally equivalent to

667

(x+y)+1; similarly applying argument a to a function mapping x

668

to some expression t converts to the expression t where x is

669

replaced by a). This notion of conversion (which is decidable

670

because Coq programs are terminating) covers a certain part of

671

equational reasoning but is limited to sequential evaluation of

672

expressions of (not necessarily closed) programs. Besides conversion,

673

equations have to be treated by hand or using specialised tactics.

674

675

676

677

<H3><A NAME="htoc37">5.2</A>  Axioms</H3>

678

679

680

681

<H4><A NAME="htoc38">31</A>  What axioms can be safely added to Coq?</H4>

682

683

There are a few typical useful axioms that are independent from the

684

Calculus of Inductive Constructions and that can be safely added to

685

Coq. These axioms are stated in the directory <TT>Logic</TT> of the

686

standard library of Coq. The most interesting ones are

687

688

Excluded-middle: for all A:Prop, A \/ � A

689

<LI>Proof-irrelevance: for all A:Prop, for all p1 p2:A, p1=p2

690

<LI>Unicity of equality proofs (or equivalently Streicher's axiom K)

691

<LI>The principle of description: for all x, there exists! y, R(x,y) -> there exists f, for all x, R(x,f(x))

692

<LI>The functional axiom of choice: for all x, there exists y, R(x,y) -> there exists f, for all x, R(x,f(x))

693

<LI>Extensionality of predicates: for all P Q:A-> Prop, (for all x, P(x) <-> Q(x)) -> P=Q

694

<LI>Extensionality of functions: for all f g:A-> B, (for all x, f(x)=g(x)) -> f=g

695

</UL>

696

Here is a summary of the relative strength of these axioms, most

697

proofs can be found in directory <TT>Logic</TT> of the standard library.

698

699

700

701

702

703

<H4><A NAME="htoc39">32</A>  What standard axioms are inconsistent with Coq?</H4>

704

705

The axiom of description together with classical logic

706

(e.g. excluded-middle) are inconsistent in the variant of the Calculus

707

of Inductive Constructions where <TT>Set</TT> is impredicative.

708

709

As a consequence, the functional form of the axiom of choice and

710

excluded-middle, or any form of the axiom of choice together with

711

predicate extensionality are inconsistent in the <TT>Set</TT>-impredicative

712

version of the Calculus of Inductive Constructions.

713

714

The main purpose of the <TT>Set</TT>-predicative restriction of the Calculus

715

of Inductive Constructions is precisely to accommodate these axioms

716

which are quite standard in mathematical usage.

717

718

The <TT>Set</TT>-predicative system is commonly considered consistent by

719

interpreting it in a standard set-theoretic boolean model, even with

720

classical logic, axiom of choice and predicate extensionality added.

721

722

723

724

<H4><A NAME="htoc40">33</A>  What is Streicher's axiom K</H4>

725

726

727

Streicher's axiom K [<A HREF="#HofStr98"><CITE>12</CITE></A>] asserts dependent

728

elimination of reflexive equality proofs.

729

730

731

732

733

734

<TT>Coq <     P (refl_equal x) -> forall p: x=x, P p.</TT>

735

</DIV>

736

737

In the general case, axiom K is an independent statement of the

738

Calculus of Inductive Constructions. However, it is true on decidable

739

domains (see file <A HREF="http://coq.inria.fr/library/Coq.Logic.Eqdep_dec.html

740

"><TT>Eqdep_dec.v</TT></A>). It is also

741

trivially a consequence of proof-irrelevance (see

742

<A HREF="#proof-irrelevance">34</A>) hence of classical logic.

743

744

Axiom K is equivalent to Uniqueness of Identity Proofs [<A HREF="#HofStr98"><CITE>12</CITE></A>]

745

746

747

748

749

</DIV>

750

751

Axiom K is also equivalent to Uniqueness of Reflexive Identity Proofs [<A HREF="#HofStr98"><CITE>12</CITE></A>]

752

753

754

755

756

</DIV>

757

758

Axiom K is also equivalent to

759

760

761

762

763

764

765

766

</DIV>

767

768

It is also equivalent to the injectivity of dependent equality (dependent equality is itself equivalent to equality of dependent pairs).

769

770

771

772

773

774

775

776

777

778

779

780

</DIV>

781

782

783

784

<H4><A NAME="htoc41">34</A>  What is proof-irrelevance</H4>

785

786

787

A specificity of the Calculus of Inductive Constructions is to permit

788

statements about proofs. This leads to the question of comparing two

789

proofs of the same proposition. Identifying all proofs of the same

790

proposition is called proof-irrelevance:

791

<DIV ALIGN=center>for all A:<TT>Prop</TT>, for all p q:A, p=q

792

</DIV>

793

Proof-irrelevance (in <TT>Prop</TT>) can be assumed without contradiction in

794

Coq. It corresponds to a model where provability, whatever the

795

proof is, is more important than the computational content of the

796

proof. This is in harmony with the common purely logical

797

interpretation of <TT>Prop</TT>. Contrastingly, proof-irrelevance is

798

inconsistent in <TT>Set</TT> in harmony with the computational meaning of

799

the sort <TT>Set</TT>.

800

801

Proof-irrelevance (in <TT>Prop</TT>) is a consequence of classical logic

802

(see proofs in file <A HREF="http://coq.inria.fr/library/Coq.Logic.Classical.html

803

"><TT>Classical.v</TT></A> and

804

<A HREF="http://coq.inria.fr/library/Coq.Logic.Berardi.html

805

"><TT>Berardi.v</TT></A>). Proof-irrelevance is also a

806

consequence of propositional extensionality (i.e. <TT>(A <-> B)

807

-> A=B</TT>, see the proof in file

808

<A HREF="http://coq.inria.fr/library/Coq.Logic.ClassicalFacts.html

809

"><TT>ClassicalFacts.v</TT></A>).

810

811

Conversely, proof-irrelevance directly implies Streicher's axiom K.

812

813

814

815

<H4><A NAME="htoc42">35</A>  What about functional extensionality?</H4>

816

817

Extensionality of functions is an axiom in, say set theory, but from a

818

programing point of view, extensionality cannot be a priori

819

accepted since it would identify, say programs such as mergesort and

820

quicksort.

821

822

Let <TT>A</TT>, <TT>B</TT> be types. To deal with extensionality on

823

<CODE>A->B</CODE>, the recommended approach is to define one's

824

own extensional equality on <CODE>A->B</CODE>.

825

826

827

828

<TT>Coq < Definition ext_eq (f g: A->B) := forall x:A, f x = g x.</TT>

829

</DIV>

830

831

and to reason on <CODE>A->B</CODE> as a setoid (see the Chapter on

832

Setoids in the Reference Manual).

833

834

835

836

<H4><A NAME="htoc43">36</A>  Is <TT>Prop</TT> impredicative?</H4>

837

838

Yes, the sort <TT>Prop</TT> of propositions is impredicative. Otherwise said, a statement of the form for all

839

A:Prop, P(A) can be instantiated by itself: if for all A:<TT>Prop</TT>, P(A)

840

is provable, then P(for all A:<TT>Prop</TT>, P(A)) is.

841

842

843

844

<H4><A NAME="htoc44">37</A>  Is <TT>Set</TT> impredicative?</H4>

845

846

No, the sort <TT>Set</TT> lying at the bottom of the hierarchy of

847

computational types is predicative in the basic Coq system.

848

This means that a family of types in <TT>Set</TT>, e.g. for all A:<TT>Set</TT>, A

849

-> A, is not a type in <TT>Set</TT> and it cannot be applied on

850

itself.

851

852

However, the sort <TT>Set</TT> was impredicative in the original versions of

853

Coq. For backward compatibility, or for experiments by

854

knowledgeable users, the logic of Coq can be set impredicative for

855

<TT>Set</TT> by calling Coq with the option <TT>-impredicative-set</TT>.

856

857

<TT>Set</TT> has been made predicative from version 8.0 of Coq. The main

858

reason is to interact smoothly with a classical mathematical world

859

where both excluded-middle and the axiom of description are valid (see

860

file <A HREF="http://coq.inria.fr/library/Coq.Logic.ClassicalDescription.html

861

"><TT>ClassicalDescription.v</TT></A> for a

862

proof that excluded-middle and description implies the double negation

863

of excluded-middle in <TT>Set</TT> and file <TT>Hurkens_Set.v</TT> from the

864

user contribution <TT>Rocq/PARADOXES</TT> for a proof that

865

impredicativity of <TT>Set</TT> implies the simple negation of

866

excluded-middle in <TT>Set</TT>).

867

868

869

870

<H4><A NAME="htoc45">38</A>  Is <TT>Type</TT> impredicative?</H4>

871

872

No, <TT>Type</TT> is stratified. This is hidden for the

873

user, but Coq internally maintains a set of constraints ensuring

874

stratification.

875

876

If <TT>Type</TT> were impredicative then it would be possible to encode

877

Girard's systems U- and U in Coq and it is known from Girard,

878

Coquand, Hurkens and Miquel that systems U- and U are inconsistent

879

[Girard 1972, Coquand 1991, Hurkens 1993, Miquel 2001]. This encoding

880

can be found in file <TT>Logic/Hurkens.v</TT> of Coq standard library.

881

882

For instance, when the user see <TT>for all X:Type, X->X : Type</TT>, each

883

occurrence of <TT>Type</TT> is implicitly bound to a different level, say

884

alpha and beta and the actual statement is <TT>forall X:Type(alpha), X->X : Type(beta)</TT> with the constraint

885

alpha<beta.

886

887

When a statement violates a constraint, the message <TT>Universe

888

inconsistency</TT> appears. Example: <TT>fun (x:Type) (y:for all X:Type, X

889

-> X) => y x x</TT>.

890

891

892

893

<H4><A NAME="htoc46">39</A>  I have two proofs of the same proposition. Can I prove they are equal?</H4>

894

895

In the base Coq system, the answer is generally no. However, if

896

classical logic is set, the answer is yes for propositions in <TT>Prop</TT>.

897

The answer is also yes if proof irrelevance holds (see question

898

<A HREF="#proof-irrelevance">34</A>).

899

900

There are also ``simple enough'' propositions for which you can prove

901

the equality without requiring any extra axioms. This is typically

902

the case for propositions defined deterministically as a first-order

903

inductive predicate on decidable sets. See for instance in question

904

<A HREF="#le-uniqueness">136</A> an axiom-free proof of the unicity of the proofs of

905

the proposition <TT>le m n</TT> (less or equal on <TT>nat</TT>).

906

907

<!--TOC subsubsection I have two proofs of an equality statement. Can I prove they are

908

equal?-->

909

910

<H4><A NAME="htoc47">40</A>  I have two proofs of an equality statement. Can I prove they are

911

equal?</H4>

912

913

Yes, if equality is decidable on the domain considered (which

914

is the case for <TT>nat</TT>, <TT>bool</TT>, etc): see Coq file

915

<CODE>Eqdep_dec.v</CODE>). No otherwise, unless

916

assuming Streicher's axiom K (see [<A HREF="#HofStr98"><CITE>12</CITE></A>]) or a more general

917

assumption such as proof-irrelevance (see <A HREF="#proof-irrelevance">34</A>) or

918

classical logic.

919

920

All of these statements can be found in file <A HREF="http://coq.inria.fr/library/Coq.Logic.Eqdep.html

921

"><TT>Eqdep.v</TT></A>.

922

923

<!--TOC subsubsection Can I prove that the second components of equal dependent

924

pairs are equal?-->

925

926

<H4><A NAME="htoc48">41</A>  Can I prove that the second components of equal dependent

927

pairs are equal?</H4>

928

929

The answer is the same as for proofs of equality

930

statements. It is provable if equality on the domain of the first

931

component is decidable (look at <CODE>inj_right_pair</CODE> from file

932

<A HREF="http://coq.inria.fr/library/Coq.Logic.Eqdep_dec.html

933

"><TT>Eqdep_dec.v</TT></A>), but not provable in the general

934

case. However, it is consistent (with the Calculus of Constructions)

935

to assume it is true. The file <A HREF="http://coq.inria.fr/library/Coq.Logic.Eqdep.html

936

"><TT>Eqdep.v</TT></A> actually

937

provides an axiom (equivalent to Streicher's axiom K) which entails

938

the result (look at <CODE>inj_pair2</CODE> in <A HREF="http://coq.inria.fr/library/Coq.Logic.Eqdep.html

939

"><TT>Eqdep.v</TT></A>).

940

941

942

943

<H3><A NAME="htoc49">5.3</A>  Impredicativity</H3>

944

945

946

947

<H4><A NAME="htoc50">42</A>  Why <TT>injection</TT> does not work on impredicative <TT>Set</TT>?</H4>

948

949

E.g. in this case (this occurs only in the <TT>Set</TT>-impredicative

950

variant of Coq):

951

952

953

954

955

956

957

958

959

960

961

962

963

</DIV>

964

965

Injectivity of constructors is restricted to predicative types. If

966

injectivity on large inductive types were not restricted, we would be

967

allowed to derive an inconsistency (e.g. following the lines of

968

Burali-Forti paradox). The question remains open whether injectivity

969

is consistent on some large inductive types not expressive enough to

970

encode known paradoxes (such as type I above).

971

972

973

974

<H4><A NAME="htoc51">43</A>  What is a "large inductive definition"?</H4>

975

976

An inductive definition in <TT>Prop</TT> pr <TT>Set</TT> is called large

977

if its constructors embed sets or propositions. As an example, here is

978

a large inductive type:

979

980

981

982

983

<TT>Coq <   existST : forall X:Set, P X -> sigST P.</TT>

984

</DIV>

985

986

In the <TT>Set</TT> impredicative variant of Coq, large inductive

987

definitions in <TT>Set</TT> have restricted elimination schemes to

988

prevent inconsistencies. Especially, projecting the set or the

989

proposition content of a large inductive definition is forbidden. If

990

it were allowed, it would be possible to encode e.g. Burali-Forti

991

paradox [<A HREF="#Gir70"><CITE>9</CITE></A><CITE>, </CITE><A HREF="#Coq85"><CITE>4</CITE></A>].

992

993

994

995

<H2><A NAME="htoc52">6</A>  Talkin' with the Rooster</H2>

996

997

998

999

<H3><A NAME="htoc53">6.1</A>  My goal is ..., how can I prove it?</H3>

1000

1001

1002

1003

<H4><A NAME="htoc54">44</A>  My goal is a conjunction, how can I prove it?</H4>

1004

1005

Use some theorem or assumption or use the <TT>split</TT> tactic.

1006

1007

1008

1009

<TT>1 subgoal</TT>

1010

1011

1012

<TT>   forall A B : Prop, A -> B -> A /\ B</TT>

1013

1014

1015

<TT>1 subgoal</TT>

1016

1017

1018

1019

1020

1021

1022

1023

1024

1025

<TT>2 subgoals</TT>

1026

1027

1028

1029

1030

1031

1032

1033

<TT>subgoal 2 is:</TT>

1034

1035

1036

1037

<TT>1 subgoal</TT>

1038

1039

1040

1041

1042

1043

1044

1045

1046

1047

<TT>Proof completed.</TT>

1048

1049

1050

<TT>intros.</TT>

1051

<TT>split.</TT>

1052

<TT> assumption.</TT>

1053

<TT> assumption.</TT>

1054

<TT>Unnamed_thm is defined</TT>

1055

</DIV>

1056

1057

1058

1059

<H4><A NAME="htoc55">45</A>  My goal contains a conjunction as an hypothesis, how can I use it?</H4>

1060

1061

If you want to decompose your hypothesis into other hypothesis you can use the <TT>decompose</TT> tactic:

1062

1063

1064

1065

1066

<TT>1 subgoal</TT>

1067

1068

1069

<TT>   forall A B : Prop, A /\ B -> B</TT>

1070

1071

1072

<TT>1 subgoal</TT>

1073

1074

1075

1076

1077

1078

1079

1080

1081

<TT>1 subgoal</TT>

1082

1083

1084

1085

1086

1087

1088

1089

1090

1091

1092

<TT>Proof completed.</TT>

1093

1094

1095

<TT>intros.</TT>

1096

<TT>decompose [and] H.</TT>

1097

<TT>assumption.</TT>

1098

<TT>Unnamed_thm0 is defined</TT>

1099

</DIV>

1100

1101

1102

1103

<H4><A NAME="htoc56">46</A>  My goal is a disjunction, how can I prove it?</H4>

1104

1105

You can prove the left part or the right part of the disjunction using

1106

<TT>left</TT> or <TT>right</TT> tactics. If you want to do a classical

1107

reasoning step, use the <TT>classic</TT> axiom to prove the right part with the assumption

1108

that the left part of the disjunction is false.

1109

1110

1111

1112

1113

<TT>1 subgoal</TT>

1114

1115

1116

<TT>   forall A B : Prop, A -> A \/ B</TT>

1117

1118

1119

<TT>1 subgoal</TT>

1120

1121

1122

1123

1124

1125

1126

1127

1128

<TT>1 subgoal</TT>

1129

1130

1131

1132

1133

1134

1135

1136

1137

<TT>Proof completed.</TT>

1138

1139

1140

<TT>intros.</TT>

1141

1142

<TT>assumption.</TT>

1143

<TT>Unnamed_thm1 is defined</TT>

1144

</DIV>

1145

1146

An example using classical reasoning:

1147

1148

1149

1150

1151

1152

1153

1154

1155

<TT>Coq < | _:_ |-?X1 \/ _ => (elim (classic X1);intro;[left;trivial|right])</TT>

1156

1157

<TT>classical_right is defined</TT>

1158

1159

1160

1161

1162

<TT>Coq < | _:_ |- _ \/?X1 => (elim (classic X1);intro;[right;trivial|left])</TT>

1163

1164

<TT>classical_left is defined</TT>

1165

1166

1167

1168

1169

<TT>1 subgoal</TT>

1170

1171

1172

<TT>   forall A B : Prop, (~ A -> B) -> A \/ B</TT>

1173

1174

1175

<TT>1 subgoal</TT>

1176

1177

1178

1179

1180

1181

1182

1183

1184

<TT>1 subgoal</TT>

1185

1186

1187

1188

1189

1190

1191

1192

1193

1194

<TT>Proof completed.</TT>

1195

1196

1197

<TT>intros.</TT>

1198

<TT>classical_right.</TT>

1199

1200

<TT>Unnamed_thm2 is defined</TT>

1201

</DIV>

1202

1203

1204

1205

<H4><A NAME="htoc57">47</A>  My goal is an universally quantified statement, how can I prove it?</H4>

1206

1207

Use some theorem or assumption or introduce the quantified variable in

1208

the context using the <TT>intro</TT> tactic. If there are several

1209

variables you can use the <TT>intros</TT> tactic. A good habit is to

1210

provide names for these variables: Coq will do it anyway, but such

1211

automatic naming decreases legibility and robustness.

1212

1213

1214

1215

<H4><A NAME="htoc58">48</A>  My goal is an existential, how can I prove it?</H4>

1216

1217

Use some theorem or assumption or exhibit the witness using the <TT>exists</TT> tactic.

1218

1219

1220

1221

<TT>1 subgoal</TT>

1222

1223

1224

<TT>   exists x : nat, (forall y : nat, x + y = y)</TT>

1225

1226

1227

<TT>1 subgoal</TT>

1228

1229

1230

<TT>   forall y : nat, 0 + y = y</TT>

1231

1232

1233

<TT>1 subgoal</TT>

1234

1235

1236

1237

1238

1239

1240

<TT>Proof completed.</TT>

1241

1242

1243

<TT>exists 0.</TT>

1244

<TT>intros.</TT>

1245

1246

<TT>Unnamed_thm3 is defined</TT>

1247

</DIV>

1248

1249

1250

1251

<H4><A NAME="htoc59">49</A>  My goal is solvable by some lemma, how can I prove it?</H4>

1252

1253

Just use the <TT>apply</TT> tactic.

1254

1255

1256

1257

1258

<TT>1 subgoal</TT>

1259

1260

1261

<TT>   forall x : nat, x + 0 = x</TT>

1262

1263

1264

<TT>Proof completed.</TT>

1265

1266

1267

1268

<TT>mylemma is defined</TT>

1269

1270

1271

1272

<TT>1 subgoal</TT>

1273

1274

1275

1276

1277

1278

<TT>Proof completed.</TT>

1279

1280

1281

<TT>apply mylemma.</TT>

1282

<TT>Unnamed_thm is defined</TT>

1283

</DIV>

1284

1285

1286

1287

<H4><A NAME="htoc60">50</A>  My goal contains False as an hypotheses, how can I prove it?</H4>

1288

1289

You can use the <TT>contradiction</TT> or <TT>intuition</TT> tactics.

1290

1291

1292

1293

<H4><A NAME="htoc61">51</A>  My goal is an equality of two convertible terms, how can I prove it?</H4>

1294

1295

Just use the <TT>reflexivity</TT> tactic.

1296

1297

1298

1299

1300

<TT>1 subgoal</TT>

1301

1302

1303

<TT>   forall x : nat, 0 + x = x</TT>

1304

1305

1306

<TT>1 subgoal</TT>

1307

1308

1309

1310

1311

1312

1313

<TT>Proof completed.</TT>

1314

1315

1316

<TT>intros.</TT>

1317

<TT>reflexivity.</TT>

1318

<TT>Unnamed_thm0 is defined</TT>

1319

</DIV>

1320

1321

1322

1323

<H4><A NAME="htoc62">52</A>  My goal is a <TT>let x := a in ...</TT>, how can I prove it?</H4>

1324

1325

Just use the <TT>intro</TT> tactic.

1326

1327

1328

1329

<H4><A NAME="htoc63">53</A>  My goal is a <TT>let (a, ..., b) := c in</TT>, how can I prove it?</H4>

1330

1331

Just use the <TT>destruct</TT> c as (a,...,b) tactic.

1332

1333

1334

1335

<H4><A NAME="htoc64">54</A>  My goal contains some existential hypotheses, how can I use it?</H4>

1336

1337

You can use the tactic <TT>elim</TT> with you hypotheses as an argument.

1338

1339

1340

1341

<H4><A NAME="htoc65">55</A>  My goal contains some existential hypotheses, how can I use it and decompose my knowledge about this new thing into different hypotheses?</H4>

1342

1343

<PRE>

1344

Ltac DecompEx H P := elim H;intro P;intro TO;decompose [and] TO;clear TO;clear H.

1345

</PRE>

1346

1347

1348

<H4><A NAME="htoc66">56</A>  My goal is an equality, how can I swap the left and right hand terms?</H4>

1349

1350

Just use the <TT>symmetry</TT> tactic.

1351

1352

1353

1354

<TT>1 subgoal</TT>

1355

1356

1357

<TT>   forall x y : nat, x = y -> y = x</TT>

1358

1359

1360

<TT>1 subgoal</TT>

1361

1362

1363

1364

1365

1366

1367

1368

1369

<TT>1 subgoal</TT>

1370

1371

1372

1373

1374

1375

1376

1377

1378

<TT>Proof completed.</TT>

1379

1380

1381

<TT>intros.</TT>

1382

<TT>symmetry  in |- *.</TT>

1383

<TT>assumption.</TT>

1384

<TT>Unnamed_thm1 is defined</TT>

1385

</DIV>

1386

1387

1388

1389

<H4><A NAME="htoc67">57</A>  My hypothesis is an equality, how can I swap the left and right hand terms?</H4>

1390

1391

Just use the <TT>symmetryin</TT> tactic.

1392

1393

1394

1395

1396

<TT>1 subgoal</TT>

1397

1398

1399

<TT>   forall x y : nat, x = y -> y = x</TT>

1400

1401

1402

<TT>1 subgoal</TT>

1403

1404

1405

1406

1407

1408

1409

1410

1411

<TT>1 subgoal</TT>

1412

1413

1414

1415

1416

1417

1418

1419

1420

<TT>Proof completed.</TT>

1421

1422

1423

<TT>intros.</TT>

1424

<TT>symmetry  in H.</TT>

1425

<TT>assumption.</TT>

1426

<TT>Unnamed_thm2 is defined</TT>

1427

</DIV>

1428

1429

1430

1431

<H4><A NAME="htoc68">58</A>  My goal is an equality, how can I prove it by transitivity?</H4>

1432

1433

Just use the <TT>transitivity</TT> tactic.

1434

1435

1436

1437

<TT>1 subgoal</TT>

1438

1439

1440

<TT>   forall x y z : nat, x = y -> y = z -> x = z</TT>

1441

1442

1443

<TT>1 subgoal</TT>

1444

1445

1446

1447

1448

1449

1450

1451

1452

1453

1454

<TT>2 subgoals</TT>

1455

1456

1457

1458

1459

1460

1461

1462

1463

<TT>subgoal 2 is:</TT>

1464

1465

1466

1467

<TT>1 subgoal</TT>

1468

1469

1470

1471

1472

1473

1474

1475

1476

1477

1478

<TT>Proof completed.</TT>

1479

1480

1481

<TT>intros.</TT>

1482

<TT>transitivity y.</TT>

1483

<TT> assumption.</TT>

1484

<TT> assumption.</TT>

1485

<TT>Unnamed_thm3 is defined</TT>

1486

</DIV>

1487

1488

1489

1490

<H4><A NAME="htoc69">59</A>  My goal would be solvable using <TT>apply;assumption</TT> if it would not create meta-variables, how can I prove it?</H4>

1491

1492

You can use <TT>eapply yourtheorem;eauto</TT> but it won't work in all cases ! (for example if more than one hypothesis match one of the subgoals generated by <TT>eapply</TT>) so you should rather use <TT>try solve [eapply yourtheorem;eauto]</TT>, otherwise some metavariables may be incorrectly instantiated.

1493

1494

1495

1496

1497

<TT>1 subgoal</TT>

1498

1499

1500

<TT>   forall x y z : nat, x = y -> y = z -> x = z</TT>

1501

1502

1503

<TT>1 subgoal</TT>

1504

1505

1506

1507

1508

1509

1510

1511

1512

1513

1514

<TT>Proof completed.</TT>

1515

1516

1517

<TT>intros.</TT>

1518

<TT>transitivity y; assumption.</TT>

1519

<TT>trans is defined</TT>

1520

1521

1522

1523

<TT>1 subgoal</TT>

1524

1525

1526

<TT>   forall x y z : nat, x = y -> y = z -> x = z</TT>

1527

1528

1529

<TT>1 subgoal</TT>

1530

1531

1532

1533

1534

1535

1536

1537

1538

1539

1540

<TT>Proof completed.</TT>

1541

1542

1543

<TT>intros.</TT>

1544

<TT>eapply trans; eauto.</TT>

1545

<TT>Unnamed_thm4 is defined</TT>

1546

1547

1548

1549

<TT>1 subgoal</TT>

1550

1551

1552

<TT>   forall x y z t : nat, x = y -> x = t -> y = z -> x = z</TT>

1553

1554

1555

<TT>1 subgoal</TT>

1556

1557

1558

1559

1560

1561

1562

1563

1564

1565

1566

1567

1568

<TT>1 subgoal</TT>

1569

1570

1571

1572

1573

1574

1575

1576

1577

1578

1579

1580

1581

<TT>1 subgoal</TT>

1582

1583

1584

1585

1586

1587

1588

1589

1590

1591

1592

1593

1594

<TT>2 subgoals</TT>

1595

1596

1597

1598

1599

1600

1601

1602

1603

1604

1605

<TT>subgoal 2 is:</TT>

1606

1607

1608

1609

<TT>1 subgoal</TT>

1610

1611

1612

1613

1614

1615

1616

1617

1618

1619

1620

1621

1622

<TT>Proof completed.</TT>

1623

1624

1625

<TT>intros.</TT>

1626

<TT>eapply trans.</TT>

1627

<TT> apply H.</TT>

1628

1629

1630

<TT>Unnamed_thm5 is defined</TT>

1631

1632

1633

1634

<TT>1 subgoal</TT>

1635

1636

1637

<TT>   forall x y z t : nat, x = y -> x = t -> y = z -> x = z</TT>

1638

1639

1640

<TT>1 subgoal</TT>

1641

1642

1643

1644

1645

1646

1647

1648

1649

1650

1651

1652

1653

<TT>1 subgoal</TT>

1654

1655

1656

1657

1658

1659

1660

1661

1662

1663

1664

1665

1666

<TT>1 subgoal</TT>

1667

1668

1669

1670

1671

1672

1673

1674

1675

1676

1677

1678

1679

<TT>1 subgoal</TT>

1680

1681

1682

1683

1684

1685

1686

1687

1688

1689

1690

1691

1692

<TT>2 subgoals</TT>

1693

1694

1695

1696

1697

1698

1699

1700

1701

1702

1703

<TT>subgoal 2 is:</TT>

1704

1705

1706

1707

<TT>1 subgoal</TT>

1708

1709

1710

1711

1712

1713

1714

1715

1716

1717

1718

1719

1720

<TT>Proof completed.</TT>

1721

1722

1723

<TT>intros.</TT>

1724

<TT>try solve [ eapply trans; eauto ].</TT>

1725

<TT>eapply trans.</TT>

1726

<TT> apply H.</TT>

1727

1728

1729

<TT>Unnamed_thm6 is defined</TT>

1730

1731

1732

</DIV>

1733

1734

1735

1736

<H4><A NAME="htoc70">60</A>  My goal is solvable by some lemma within a set of lemmas and I don't want to remember which one, how can I prove it?</H4>

1737

1738

You can use a what is called a hints' base.

1739

1740

1741

1742

1743

1744

1745

1746

1747

1748

1749

1750

<TT>1 subgoal</TT>

1751

1752

1753

1754

1755

1756

<TT>Proof completed.</TT>

1757

1758

1759

1760

<TT>toto1 is defined</TT>

1761

1762

1763

<TT>1 subgoal</TT>

1764

1765

1766

1767

1768

1769

<TT>Proof completed.</TT>

1770

1771

1772

1773

<TT>toto2 is defined</TT>

1774

1775

1776

<TT>1 subgoal</TT>

1777

1778

1779

1780

1781

1782

<TT>Proof completed.</TT>

1783

1784

1785

1786

<TT>toto3 is defined</TT>

1787

1788

1789

1790

1791

1792

1793

<TT>1 subgoal</TT>

1794

1795

1796

1797

1798

1799

<TT>Proof completed.</TT>

1800

1801

1802

<TT>auto with mybase.</TT>

1803

<TT>Unnamed_thm7 is defined</TT>

1804

</DIV>

1805

1806

1807

1808

<H4><A NAME="htoc71">61</A>  My goal is one of the hypotheses, how can I prove it?</H4>

1809

1810

Use the <TT>assumption</TT> tactic.

1811

1812

1813

1814

1815

<TT>1 subgoal</TT>

1816

1817

1818

1819

1820

1821

<TT>1 subgoal</TT>

1822

1823

1824

1825

1826

1827

1828

<TT>Proof completed.</TT>

1829

1830

1831

<TT>intro.</TT>

1832

<TT>assumption.</TT>

1833

<TT>Unnamed_thm8 is defined</TT>

1834

</DIV>

1835

1836

1837

1838

<H4><A NAME="htoc72">62</A>  My goal appears twice in the hypotheses and I want to choose which one is used, how can I do it?</H4>

1839

1840

Use the <TT>exact</TT> tactic.

1841

1842

1843

1844

<TT>1 subgoal</TT>

1845

1846

1847

1848

1849

1850

<TT>1 subgoal</TT>

1851

1852

1853

1854

1855

1856

1857

1858

<TT>Proof completed.</TT>

1859

1860

1861

<TT>intros.</TT>

1862

<TT>exact H0.</TT>

1863

<TT>Unnamed_thm9 is defined</TT>

1864

</DIV>

1865

1866

1867

1868

<H4><A NAME="htoc73">63</A>  What can be the difference between applying one hypothesis or another in the context of the last question?</H4>

1869

1870

From a proof point of view it is equivalent but if you want to extract

1871

a program from your proof, the two hypotheses can lead to different

1872

programs.

1873

1874

1875

1876

<H4><A NAME="htoc74">64</A>  My goal is a propositional tautology, how can I prove it?</H4>

1877

1878

Just use the <TT>tauto</TT> tactic.

1879

1880

1881

1882

<TT>1 subgoal</TT>

1883

1884

1885

<TT>   forall A B : Prop, A -> (A \/ B) /\ A</TT>

1886

1887

1888

<TT>1 subgoal</TT>

1889

1890

1891

1892

1893

1894

1895

1896

1897

<TT>Proof completed.</TT>

1898

1899

1900

<TT>intros.</TT>

1901

<TT>tauto.</TT>

1902

<TT>Unnamed_thm10 is defined</TT>

1903

</DIV>

1904

1905

1906

1907

<H4><A NAME="htoc75">65</A>  My goal is a first order formula, how can I prove it?</H4>

1908

1909

Just use the semi-decision tactic: <TT>firstorder</TT>.

1910

1911

1912

1913

<H4><A NAME="htoc76">66</A>  My goal is solvable by a sequence of rewrites, how can I prove it?</H4>

1914

1915

Just use the <TT>congruence</TT> tactic.

1916

1917

1918

1919

<TT>1 subgoal</TT>

1920

1921

1922

<TT>   forall a b c d e : Z, a = d -> b = e -> c + b = d -> c + e = a</TT>

1923

1924

1925

<TT>1 subgoal</TT>

1926

1927

1928

1929

1930

1931

1932

1933

1934

1935

1936

1937

1938

1939

<TT>Proof completed.</TT>

1940

1941

1942

<TT>intros.</TT>

1943

<TT>congruence.</TT>

1944

<TT>Unnamed_thm11 is defined</TT>

1945

</DIV>

1946

1947

1948

1949

<H4><A NAME="htoc77">67</A>  My goal is a disequality solvable by a sequence of rewrites, how can I prove it?</H4>

1950

1951

Just use the <TT>congruence</TT> tactic.

1952

1953

1954

1955

1956

<TT>1 subgoal</TT>

1957

1958

1959

<TT>   forall a b c d : Z, a <> d -> b = a -> d = c + b -> b <> c + b</TT>

1960

1961

1962

<TT>1 subgoal</TT>

1963

1964

1965

1966

1967

1968

1969

1970

1971

1972

1973

1974

1975

<TT>Proof completed.</TT>

1976

1977

1978

<TT>intros.</TT>

1979

<TT>congruence.</TT>

1980

<TT>Unnamed_thm12 is defined</TT>

1981

</DIV>

1982

1983

1984

1985

<H4><A NAME="htoc78">68</A>  My goal is an equality on some ring (e.g. natural numbers), how can I prove it?</H4>

1986

1987

Just use the <TT>ring</TT> tactic.

1988

1989

1990

1991

1992

1993

1994

1995

1996

1997

1998

<TT>1 subgoal</TT>

1999

2000

2001

<TT>   forall a b : Z, (a + b) * (a + b) = a * a + 2 * a * b + b * b</TT>

2002

2003

2004

<TT>1 subgoal</TT>

2005

2006

2007

2008

2009

2010

2011

2012

<TT>Proof completed.</TT>

2013

2014

2015

<TT>intros.</TT>

2016

2017

<TT>Unnamed_thm13 is defined</TT>

2018

</DIV>

2019

2020

2021

2022

<H4><A NAME="htoc79">69</A>  My goal is an equality on some field (e.g. real numbers), how can I prove it?</H4>

2023

2024

Just use the <TT>field</TT> tactic.

2025

2026

2027

2028

2029

2030

2031

2032

2033

2034

2035

<TT>1 subgoal</TT>

2036

2037

2038

<TT>   forall a b : R, b * a <> 0 -> a / b * (b / a) = 1</TT>

2039

2040

2041

<TT>1 subgoal</TT>

2042

2043

2044

2045

2046

2047

2048

2049

2050

<TT>1 subgoal</TT>

2051

2052

2053

2054

2055

2056

2057

2058

2059

<TT>Proof completed.</TT>

2060

2061

2062

<TT>intros.</TT>

2063

<TT>field.</TT>

2064

<TT>assumption.</TT>

2065

<TT>Unnamed_thm14 is defined</TT>

2066

</DIV>

2067

2068

2069

2070

<H4><A NAME="htoc80">70</A>  My goal is an inequality on integers in Presburger's arithmetic (an expression build from +,-,constants and variables), how can I prove it?</H4>

2071

2072

2073

2074

2075

2076

2077

2078

2079

2080

2081

<TT>1 subgoal</TT>

2082

2083

2084

<TT>   forall a : Z, a > 0 -> a + a > a</TT>

2085

2086

2087

<TT>1 subgoal</TT>

2088

2089

2090

2091

2092

2093

2094

2095

<TT>Proof completed.</TT>

2096

2097

2098

<TT>intros.</TT>

2099

<TT>omega.</TT>

2100

<TT>Unnamed_thm15 is defined</TT>

2101

</DIV>

2102

2103

2104

2105

<H4><A NAME="htoc81">71</A>  My goal is an equation solvable using equational hypothesis on some ring (e.g. natural numbers), how can I prove it?</H4>

2106

2107

You need the <TT>gb</TT> tactic (see Lo�c Pottier's homepage).

2108

2109

2110

2111

<H3><A NAME="htoc82">6.2</A>  Tactics usage</H3>

2112

2113

2114

2115

<H4><A NAME="htoc83">72</A>  I want to state a fact that I will use later as an hypothesis, how can I do it?</H4>

2116

2117

If you want to use forward reasoning (first proving the fact and then

2118

using it) you just need to use the <TT>assert</TT> tactic. If you want to use

2119

backward reasoning (proving your goal using an assumption and then

2120

proving the assumption) use the <TT>cut</TT> tactic.

2121

2122

2123

2124

2125

<TT>1 subgoal</TT>

2126

2127

2128

<TT>   forall A B C : Prop, Prop -> (A -> B) -> (B -> C) -> A -> C</TT>

2129

2130

2131

<TT>1 subgoal</TT>

2132

2133

2134

2135

2136

2137

2138

2139

2140

2141

2142

2143

2144

<TT>2 subgoals</TT>

2145

2146

2147

2148

2149

2150

2151

2152

2153

2154

2155

<TT>subgoal 2 is:</TT>

2156

2157

2158

2159

<TT>1 subgoal</TT>

2160

2161

2162

2163

2164

2165

2166

2167

2168

2169

2170

2171

2172

2173

<TT>1 subgoal</TT>

2174

2175

2176

2177

2178

2179

2180

2181

2182

2183

2184

2185

2186

2187

<TT>Proof completed.</TT>

2188

2189

2190

<TT>intros.</TT>

2191

<TT>assert (A -> C).</TT>

2192

<TT> intro; apply H0; apply H; assumption.</TT>

2193

<TT> apply H2.</TT>

2194

<TT>   assumption.</TT>

2195

<TT>Unnamed_thm16 is defined</TT>

2196

2197

2198

2199

<TT>1 subgoal</TT>

2200

2201

2202

<TT>   forall A B C : Prop, Prop -> (A -> B) -> (B -> C) -> A -> C</TT>

2203

2204

2205

<TT>1 subgoal</TT>

2206

2207

2208

2209

2210

2211

2212

2213

2214

2215

2216

2217

2218

<TT>2 subgoals</TT>

2219

2220

2221

2222

2223

2224

2225

2226

2227

2228

2229

<TT>subgoal 2 is:</TT>

2230

2231

2232

2233

<TT>2 subgoals</TT>

2234

2235

2236

2237

2238

2239

2240

2241

2242

2243

2244

2245

<TT>subgoal 2 is:</TT>

2246

2247

2248

2249

<TT>1 subgoal</TT>

2250

2251

2252

2253

2254

2255

2256

2257

2258

2259

2260

2261

2262

<TT>Proof completed.</TT>

2263

2264

2265

<TT>intros.</TT>

2266

2267

<TT> intro.</TT>

2268

<TT>   apply H2; assumption.</TT>

2269

<TT> intro; apply H0; apply H; assumption.</TT>

2270

<TT>Unnamed_thm17 is defined</TT>

2271

</DIV>

2272

2273

2274

2275

<H4><A NAME="htoc84">73</A>  I want to state a fact that I will use later as an hypothesis and prove it later, how can I do it?</H4>

2276

2277

You can use <TT>cut</TT> followed by <TT>intro</TT> or you can use the following Ltac command:

2278

<PRE>

2279

Ltac assert_later t := cut t;[intro|idtac].

2280

</PRE>

2281

2282

2283

<H4><A NAME="htoc85">74</A>  What is the difference between <TT>Qed</TT> and <TT>Defined</TT>?</H4>

2284

2285

These two commands perform type checking, but when <TT>Defined</TT> is used the new definition is set as transparent, otherwise it is defined as opaque (see <A HREF="#opaque">167</A>).

2286

2287

2288

2289

<H4><A NAME="htoc86">75</A>  How can I know what a tactic does?</H4>

2290

2291

You can use the <TT>info</TT> command.

2292

2293

2294

2295

2296

2297

You can increase the depth of the proof search or add some lemmas in the base of hints.

2298

Perhaps you may need to use <TT>eauto</TT>.

2299

2300

2301

2302

<H4><A NAME="htoc88">77</A>  What is <TT>eauto</TT>?</H4>

2303

2304

This is the same tactic as <TT>auto</TT>, but it relies on <TT>eapply</TT> instead of <TT>apply</TT>.

2305

2306

2307

2308

<H4><A NAME="htoc89">78</A>  How can I speed up <TT>auto</TT>?</H4>

2309

2310

You can use <TT>info </TT><TT>auto</TT>to replace <TT>auto</TT> by the tactics it generates.

2311

You can split your hint bases into smaller ones.

2312

2313

2314

2315

<H4><A NAME="htoc90">79</A>  What is the equivalent of <TT>tauto</TT> for classical logic?</H4>

2316

2317

Currently there are no equivalent tactic for classical logic. You can use G�del's ``not not'' translation.

2318

2319

2320

2321

<H4><A NAME="htoc91">80</A>  I want to replace some term with another in the goal, how can I do it?</H4>

2322

2323

If one of your hypothesis (say <TT>H</TT>) states that the terms are equal you can use the <TT>rewrite</TT> tactic. Otherwise you can use the <TT>replace</TT> <TT>with</TT> tactic.

2324

2325

2326

2327

<H4><A NAME="htoc92">81</A>  I want to replace some term with another in an hypothesis, how can I do it?</H4>

2328

2329

You can use the <TT>rewrite</TT> <TT>in</TT> tactic.

2330

2331

2332

2333

<H4><A NAME="htoc93">82</A>  I want to replace some symbol with its definition, how can I do it?</H4>

2334

2335

You can use the <TT>unfold</TT> tactic.

2336

2337

2338

2339

<H4><A NAME="htoc94">83</A>  How can I reduce some term?</H4>

2340

2341

You can use the <TT>simpl</TT> tactic.

2342

2343

2344

2345

<H4><A NAME="htoc95">84</A>  How can I declare a shortcut for some term?</H4>

2346

2347

You can use the <TT>set</TT> or <TT>pose</TT> tactics.

2348

2349

2350

2351

<H4><A NAME="htoc96">85</A>  How can I perform case analysis?</H4>

2352

2353

You can use the <TT>case</TT> or <TT>destruct</TT> tactics.

2354

2355

2356

2357

<H4><A NAME="htoc97">86</A>  Why should I name my intros?</H4>

2358

2359

When you use the <TT>intro</TT> tactic you don't have to give a name to your

2360

hypothesis. If you do so the name will be generated by Coq but your

2361

scripts may be less robust. If you add some hypothesis to your theorem

2362

(or change their order), you will have to change your proof to adapt

2363

to the new names.

2364

2365

2366

2367

<H4><A NAME="htoc98">87</A>  How can I automatize the naming?</H4>

2368

2369

You can use the <TT>Show Intro.</TT> or <TT>Show Intros.</TT> commands to generate the names and use your editor to generate a fully named <TT>intro</TT> tactic.

2370

This can be automatized within <TT>xemacs</TT>.

2371

2372

2373

2374

2375

<TT>1 subgoal</TT>

2376

2377

2378

<TT>   forall A B C : Prop, A -> B -> C -> A /\ B /\ C</TT>

2379

2380

2381

2382

2383

2384

2385

2386

2387

2388

2389

<TT>1 subgoal</TT>

2390

2391

2392

2393

2394

2395

2396

2397

2398

2399

2400

2401

<TT>Proof completed.</TT>

2402

2403

2404

<TT>intros A B C H H0 H1.</TT>

2405

<TT>repeat split; assumption.</TT>

2406

<TT>Unnamed_thm18 is defined</TT>

2407

</DIV>

2408

2409

2410

2411

<H4><A NAME="htoc99">88</A>  I want to automatize the use of some tactic, how can I do it?</H4>

2412

2413

You need to use the <TT>proof with T</TT> command and add ... at the

2414

end of your sentences.

2415

2416

For instance:

2417

2418

2419

2420

<TT>1 subgoal</TT>

2421

2422

2423

<TT>   forall A B C : Prop, A -> B /\ C -> A /\ B /\ C</TT>

2424

2425

2426

2427

2428

<TT>1 subgoal</TT>

2429

2430

2431

2432

2433

2434

2435

2436

2437

2438

2439

<TT>Proof completed.</TT>

2440

2441

2442

<TT>intros.</TT>

2443

<TT>split.</TT>

2444

<TT>Unnamed_thm19 is defined</TT>

2445

</DIV>

2446

2447

2448

2449

<H4><A NAME="htoc100">89</A>  I want to execute the <TT>p</TT>roof with tactic only if it solves the goal, how can I do it?</H4>

2450

2451

You need to use the <TT>try</TT> and <TT>solve</TT> tactics. For instance:

2452

2453

2454

2455

2456

2457

2458

2459

2460

2461

<TT>1 subgoal</TT>

2462

2463

2464

<TT>   forall a b : Z, Z -> a + b = b + a</TT>

2465

2466

2467

2468

2469

<TT>Proof completed.</TT>

2470

2471

2472

<TT>intros.</TT>

2473

<TT>Unnamed_thm20 is defined</TT>

2474

</DIV>

2475

2476

2477

2478

<H4><A NAME="htoc101">90</A>  How can I do the opposite of the <TT>intro</TT> tactic?</H4>

2479

2480

You can use the <TT>generalize</TT> tactic.

2481

2482

2483

2484

2485

<TT>1 subgoal</TT>

2486

2487

2488

<TT>   forall A B : Prop, A -> B -> A /\ B</TT>

2489

2490

2491

<TT>1 subgoal</TT>

2492

2493

2494

2495

2496

2497

2498

2499

2500

2501

<TT>1 subgoal</TT>

2502

2503

2504

2505

2506

2507

2508

2509

2510

2511

<TT>1 subgoal</TT>

2512

2513

2514

2515

2516

2517

2518

2519

2520

2521

2522

<TT>Proof completed.</TT>

2523

2524

2525

<TT>intros.</TT>

2526

<TT>generalize H.</TT>

2527

<TT>intro.</TT>

2528

2529

<TT>Unnamed_thm21 is defined</TT>

2530

</DIV>

2531

2532

2533

2534

<H4><A NAME="htoc102">91</A>  One of the hypothesis is an equality between a variable and some term, I want to get rid of this variable, how can I do it?</H4>

2535

2536

You can use the <TT>subst</TT> tactic. This will rewrite the equality everywhere and clear the assumption.

2537

2538

2539

2540

<H4><A NAME="htoc103">92</A>  What can I do if I get ``<TT>generated subgoal term has metavariables in it </TT>''?</H4>

2541

2542

You should use the <TT>eapply</TT> tactic, this will generate some goals containing metavariables.

2543

2544

2545

2546

<H4><A NAME="htoc104">93</A>  How can I instantiate some metavariable?</H4>

2547

2548

Just use the <TT>instantiate</TT> tactic.

2549

2550

2551

2552

<H4><A NAME="htoc105">94</A>  What is the use of the <TT>pattern</TT> tactic?</H4>

2553

2554

The <TT>pattern</TT> tactic transforms the current goal, performing

2555

beta-expansion on all the applications featuring this tactic's

2556

argument. For instance, if the current goal includes a subterm <TT>phi(t)</TT>, then <TT>pattern t</TT> transforms the subterm into <TT>(fun

2557

x:A => phi(x)) t</TT>. This can be useful when <TT>apply</TT> fails on matching,

2558

to abstract the appropriate terms.

2559

2560

2561

2562

<H4><A NAME="htoc106">95</A>  What is the difference between assert, cut and generalize?</H4>

2563

2564

PS: Notice for people that are interested in proof rendering that <TT>assert</TT>and <TT>pose</TT> (and <TT>cut</TT>) are not rendered the same as <TT>generalize</TT> (see the

2565

HELM experimental rendering tool at <A HREF="http://helm.cs.unibo.it/library.html"><TT>http://helm.cs.unibo.it</TT></A>, link

2566

HELM, link COQ Online). Indeed <TT>generalize</TT> builds a beta-expanded term

2567

while <TT>assert</TT>, <TT>pose</TT> and <TT>cut</TT> uses a let-in.

2568

<PRE>

2569

(* Goal is T *)

2570

generalize (H1 H2).

2571

(* Goal is A->T *)

2572

... a proof of A->T ...

2573

</PRE>

2574

is rendered into something like

2575

<PRE>

2576

(h) ... the proof of A->T ...

2577

we proved A->T

2578

(h0) by (H1 H2) we proved A

2579

by (h h0) we proved T

2580

</PRE>while

2581

<PRE>

2582

(* Goal is T *)

2583

assert q := (H1 H2).

2584

(* Goal is A *)

2585

... a proof of A ...

2586

(* Goal is A |- T *)

2587

... a proof of T ...

2588

</PRE>is rendered into something like

2589

<PRE>

2590

(q) ... the proof of A ...

2591

we proved A

2592

... the proof of T ...

2593

we proved T

2594

</PRE>Otherwise said, <TT>generalize</TT> is not rendered in a forward-reasoning way,

2595

while <TT>assert</TT> is.

2596

2597

2598

2599

<H4><A NAME="htoc107">96</A>  What can I do if Coqcan not infer some implicit argument ?</H4>

2600

2601

You can state explicitely what this implicit argument is. See <A HREF="#implicit">97</A>.

2602

2603

2604

2605

<H4><A NAME="htoc108">97</A>  How can I explicit some implicit argument ?</H4>

2606

2607

Just use <TT>A:=term</TT> where <TT>A</TT> is the argument.

2608

2609

For instance if you want to use the existence of ``nil'' on nat*nat lists:

2610

<PRE>

2611

exists (nil (A:=(nat*nat))).

2612

</PRE>

2613

2614

2615

<H3><A NAME="htoc109">6.3</A>  Proof management</H3>

2616

2617

2618

2619

<H4><A NAME="htoc110">98</A>  How can I change the order of the subgoals?</H4>

2620

2621

You can use the <TT>Focus</TT> command to concentrate on some goal. When the goal is proved you will see the remaining goals.

2622

2623

2624

2625

<H4><A NAME="htoc111">99</A>  How can I change the order of the hypothesis?</H4>

2626

2627

You can use the <TT>Move ... after</TT> command.

2628

2629

2630

2631

<H4><A NAME="htoc112">100</A>  How can I change the name of an hypothesis?</H4>

2632

2633

You can use the <TT>Rename ... into</TT> command.

2634

2635

2636

2637

<H4><A NAME="htoc113">101</A>  How can I delete some hypothesis?</H4>

2638

2639

You can use the <TT>Clear</TT> command.

2640

2641

2642

2643

<H4><A NAME="htoc114">102</A>  How can use a proof which is not finished?</H4>

2644

2645

You can use the <TT>Admitted</TT> command to state your current proof as an axiom.

2646

2647

2648

2649

<H4><A NAME="htoc115">103</A>  How can I state a conjecture?</H4>

2650

2651

You can use the <TT>Admitted</TT> command to state your current proof as an axiom.

2652

2653

2654

2655

<H4><A NAME="htoc116">104</A>  What is the difference between a lemma, a fact and a theorem?</H4>

2656

2657

From Coq point of view there are no difference. But some tools can

2658

have a different behavior when you use a lemma rather than a

2659

theorem. For instance <TT>coqdoc</TT> will not generate documentation for

2660

the lemmas within your development.

2661

2662

2663

2664

<H4><A NAME="htoc117">105</A>  How can I organize my proofs?</H4>

2665

2666

You can organize your proofs using the section mechanism of Coq. Have

2667

a look at the manual for further information.

2668

2669

2670

2671

<H2><A NAME="htoc118">7</A>  Inductive and Co-inductive types</H2>

2672

2673

2674

2675

<H3><A NAME="htoc119">7.1</A>  General</H3>

2676

2677

2678

2679

<H4><A NAME="htoc120">106</A>  How can I prove that two constructors are different?</H4>

2680

2681

You can use the <TT>discriminate</TT> tactic.

2682

2683

2684

2685

2686

<TT>toto is defined</TT>

2687

<TT>toto_rect is defined</TT>

2688

<TT>toto_ind is defined</TT>

2689

<TT>toto_rec is defined</TT>

2690

2691

2692

<TT>1 subgoal</TT>

2693

2694

2695

2696

2697

2698

<TT>Proof completed.</TT>

2699

2700

2701

<TT>discriminate.</TT>

2702

<TT>Unnamed_thm22 is defined</TT>

2703

</DIV>

2704

2705

2706

2707

<H4><A NAME="htoc121">107</A>  During an inductive proof, how to get rid of impossible cases of an inductive definition?</H4>

2708

2709

Use the <TT>inversion</TT> tactic.

2710

2711

2712

2713

<H4><A NAME="htoc122">108</A>  How can I prove that 2 terms in an inductive set are equal? Or different?</H4>

2714

2715

Have a look at "decide equality" and "discriminate" in the <A HREF="http://coq.inria.fr/doc/main.html">Reference Manual</A>.

2716

2717

<!--TOC subsubsection Why is the proof of <TT>0+n=n</TT> on natural numbers

2718

trivial but the proof of <TT>n+0=n</TT> is not?-->

2719

2720

<H4><A NAME="htoc123">109</A>  Why is the proof of <TT>0+n=n</TT> on natural numbers

2721

trivial but the proof of <TT>n+0=n</TT> is not?</H4>

2722

2723

Since <TT>+</TT> (<TT>plus</TT>) on natural numbers is defined by analysis on its first argument

2724

2725

2726

2727

2728

2729

<TT>(fix plus (n m : nat) {struct n} : nat :=</TT>

2730

<TT>   match n with</TT>

2731

2732

2733

2734

2735

<TT>Argument scopes are [nat_scope nat_scope]</TT>

2736

</DIV>

2737

2738

The expression <TT>0+n</TT> evaluates to <TT>n</TT>. As Coq reasons

2739

modulo evaluation of expressions, <TT>0+n</TT> and <TT>n</TT> are

2740

considered equal and the theorem <TT>0+n=n</TT> is an instance of the

2741

reflexivity of equality. On the other side, <TT>n+0</TT> does not

2742

evaluate to <TT>n</TT> and a proof by induction on <TT>n</TT> is

2743

necessary to trigger the evaluation of <TT>+</TT>.

2744

2745

<!--TOC subsubsection Why is dependent elimination in Prop not

2746

available by default?-->

2747

2748

<H4><A NAME="htoc124">110</A>  Why is dependent elimination in Prop not

2749

available by default?</H4>

2750

2751

This is just because most of the time it is not needed. To derive a

2752

dependent elimination principle in <TT>Prop</TT>, use the command <TT>Scheme</TT> and

2753

apply the elimination scheme using the <CODE>using</CODE> option of

2754

<CODE>elim</CODE>, <CODE>destruct</CODE> or <CODE>induction</CODE>.

2755

2756

2757

2758

<H3><A NAME="htoc125">7.2</A>  Recursion</H3>

2759

2760

2761

2762

<H4><A NAME="htoc126">111</A>  Why can't I define a non terminating program?</H4>

2763

2764

Because otherwise the decidability of the type-checking

2765

algorithm (which involves evaluation of programs) is not ensured. On

2766

another side, if non terminating proofs were allowed, we could get a

2767

proof of <TT>False</TT>:

2768

2769

2770

2771

2772

2773

2774

2775

2776

2777

</DIV>

2778

2779

2780

2781

<H4><A NAME="htoc127">112</A>  Why only structurally well-founded loops are allowed?</H4>

2782

2783

The structural order on inductive types is a simple and

2784

powerful notion of termination. The consistency of the Calculus of

2785

Inductive Constructions relies on it and another consistency proof

2786

would have to be made for stronger termination arguments (such

2787

as the termination of the evaluation of CIC programs themselves!).

2788

2789

In spite of this, all non-pathological termination orders can be mapped

2790

to a structural order. Tools to do this are provided in the file

2791

<A HREF="http://coq.inria.fr/library/Coq.Init.Wf.html

2792

"><TT>Wf.v</TT></A> of the standard library of Coq.

2793

2794

<!--TOC subsubsection How to define loops based on non structurally smaller

2795

recursive calls?-->

2796

2797

<H4><A NAME="htoc128">113</A>  How to define loops based on non structurally smaller

2798

recursive calls?</H4>

2799

2800

The procedure is as follows (we consider the definition of <TT>mergesort</TT> as an example).

2801

<UL><LI>Define the termination order, say <TT>R</TT> on the type <TT>A</TT> of

2802

the arguments of the loop.

2803

2804

2805

2806

2807

</DIV>

2808

2809

2810

<LI>Prove that this order is well-founded (in fact that all elements in <TT>A</TT> are accessible along <TT>R</TT>).

2811

2812

2813

2814

2815

</DIV>

2816

2817

2818

<LI>Define the step function (which needs proofs that recursive

2819

calls are on smaller arguments).

2820

2821

2822

2823

2824

2825

2826

2827

2828

2829

2830

2831

2832

2833

2834

</DIV>

2835

2836

2837

<LI>Define the recursive function by fixpoint on the step function.

2838

2839

2840

2841

<TT>Coq < Definition merge := Fix Rwf (fun _ => list nat) merge_step.</TT>

2842

</DIV>

2843

</UL>

2844

2845

2846

<H4><A NAME="htoc129">114</A>  What is behind the accessibility and well-foundedness proofs?</H4>

2847

2848

Well-foundedness of some relation <TT>R</TT> on some type <TT>A</TT>

2849

is defined as the accessibility of all elements of <TT>A</TT> along <TT>R</TT>.

2850

2851

2852

2853

2854

<TT>well_founded = </TT>

2855

<TT>fun (A : Set) (R : A -> A -> Prop) => forall a : A, Acc R a</TT>

2856

<TT>     : forall A : Set, (A -> A -> Prop) -> Prop</TT>

2857

<TT>Argument A is implicit</TT>

2858

<TT>Argument scopes are [type_scope _]</TT>

2859

2860

2861

<TT>Inductive Acc (A : Set) (R : A -> A -> Prop) : A -> Prop :=</TT>

2862

<TT>    Acc_intro : forall x : A, (forall y : A, R y x -> Acc R y) -> Acc R x</TT>

2863

<TT>For Acc: Argument A is implicit</TT>

2864

<TT>For Acc_intro: Arguments A, R are implicit</TT>

2865

<TT>For Acc: Argument scopes are [type_scope _ _]</TT>

2866

<TT>For Acc_intro: Argument scopes are [type_scope _ _ _]</TT>

2867

</DIV>

2868

2869

The structure of the accessibility predicate is a well-founded tree

2870

branching at each node <TT>x</TT> in <TT>A</TT> along all the nodes <TT>x'</TT>

2871

less than <TT>x</TT> along <TT>R</TT>. Any sequence of elements of <TT>A</TT>

2872

decreasing along the order <TT>R</TT> are branches in the accessibility

2873

tree. Hence any decreasing along <TT>R</TT> is mapped into a structural

2874

decreasing in the accessibility tree of <TT>R</TT>. This is emphasised in

2875

the definition of <TT>fix</TT> which recurs not on its argument <TT>x:A</TT>

2876

but on the accessibility of this argument along <TT>R</TT>.

2877

2878

See file <A HREF="http://coq.inria.fr/library/Coq.Init.Wf.html

2879

"><TT>Wf.v</TT></A>.

2880

2881

2882

2883

<H4><A NAME="htoc130">115</A>  How to perform double induction?</H4>

2884

2885

In general a double induction is simply solved by an induction on the

2886

first hypothesis followed by an inversion over the second

2887

hypothesis. Here is an example

2888

2889

2890

2891

2892

2893

2894

<TT>even is defined</TT>

2895

<TT>even_ind is defined</TT>

2896

2897

2898

2899

2900

2901

<TT>odd is defined</TT>

2902

<TT>odd_ind is defined</TT>

2903

2904

2905

<TT>Coq < Goal forall n:nat, even n -> odd n -> False.</TT>

2906

<TT>1 subgoal</TT>

2907

2908

2909

<TT>   forall n : nat, even n -> odd n -> False</TT>

2910

2911

2912

<TT>2 subgoals</TT>

2913

2914

2915

<TT>   odd 0 -> False</TT>

2916

<TT>subgoal 2 is:</TT>

2917

<TT> odd (S (S n)) -> False</TT>

2918

2919

2920

<TT>1 subgoal</TT>

2921

2922

2923

2924

<TT>  IHeven : odd n -> False</TT>

2925

2926

<TT>   odd (S (S n)) -> False</TT>

2927

2928

2929

<TT>1 subgoal</TT>

2930

2931

2932

2933

<TT>  IHeven : odd n -> False</TT>

2934

2935

2936

2937

2938

2939

<TT>   False</TT>

2940

<TT>Proof completed.</TT>

2941

2942

2943

<TT>induction 1.</TT>

2944

<TT> inversion 1.</TT>

2945

<TT> inversion 1.</TT>

2946

<TT>   apply IHeven; trivial.</TT>

2947

<TT>Unnamed_thm is defined</TT>

2948

</DIV>

2949

2950

In case the type of the second induction hypothesis is not

2951

dependent, <TT>inversion</TT> can just be replaced by <TT>destruct</TT>.

2952

2953

2954

2955

<H4><A NAME="htoc131">116</A>  How to define a function by double recursion?</H4>

2956

2957

The same trick applies, you can even use the pattern-matching

2958

compilation algorithm to do the work for you. Here is an example:

2959

2960

2961

2962

2963

2964

2965

2966

<TT>Coq <   | S k, S l => minus k l</TT>

2967

2968

<TT>minus is recursively defined</TT>

2969

2970

2971

<TT>minus = </TT>

2972

<TT>(fix minus (n m : nat) {struct n} : nat :=</TT>

2973

<TT>   match n with</TT>

2974

2975

<TT>   | S k => match m with</TT>

2976

2977

<TT>            | S l => minus k l</TT>

2978

2979

2980

2981

<TT>Argument scopes are [nat_scope nat_scope]</TT>

2982

</DIV>

2983

2984

In case of dependencies in the type of the induction objects

2985

t1 and t2, an extra argument stating t1=t2 must be given to

2986

the fixpoint definition

2987

2988

2989

2990

<H4><A NAME="htoc132">117</A>  How to perform nested induction?</H4>

2991

2992

To reason by nested induction, just reason by induction on the

2993

successive components.

2994

2995

2996

2997

2998

2999

3000

3001

3002

<TT>1 subgoal</TT>

3003

3004

3005

<TT>   forall n n0 : nat, n0 < n \/ n <= n0</TT>

3006

3007

3008

<TT>1 subgoal</TT>

3009

3010

3011

<TT>  IHn : forall n0 : nat, n0 < n \/ n <= n0</TT>

3012

3013

3014

3015

3016

3017

<TT>Proof completed.</TT>

3018

</DIV>

3019

3020

3021

3022

<H4><A NAME="htoc133">118</A>  How to define a function by nested recursion?</H4>

3023

3024

The same trick applies. Here is the example of Ackermann

3025

function.

3026

3027

3028

3029

3030

3031

3032

3033

3034

3035

3036

3037

3038

3039

<TT>ack is recursively defined</TT>

3040

</DIV>

3041

3042

3043

3044

<H3><A NAME="htoc134">7.3</A>  Co-inductive types</H3>

3045

3046

3047

3048

<H4><A NAME="htoc135">119</A>  I have a cofixpoint t:=F(t) and I want to prove t=F(t). How to do it?</H4>

3049

3050

Just case-expand F(<TT>t</TT>) then complete by a trivial case analysis.

3051

Here is what it gives on e.g. the type of streams on naturals

3052

3053

3054

3055

3056

<TT>Coq <   Cons : A -> Stream A -> Stream A.</TT>

3057

<TT>Stream is defined</TT>

3058

3059

3060

<TT>nats is corecursively defined</TT>

3061

3062

3063

3064

<TT>1 subgoal</TT>

3065

3066

3067

<TT>   forall n : nat, nats n = Cons n (nats (S n))</TT>

3068

3069

3070

3071

3072

3073

3074

3075

<TT>1 subgoal</TT>

3076

3077

3078

3079

<TT>   nats n = match nats n with</TT>

3080

3081

3082

3083

3084

<TT>Proof completed.</TT>

3085

3086

3087

<TT>intro; change (nats n = match nats n with</TT>

3088

3089

3090

<TT>case (nats n); reflexivity.</TT>

3091

<TT>Stream_unfold is defined</TT>

3092

</DIV>

3093

3094

3095

3096

<H2><A NAME="htoc136">8</A>  Syntax and notations</H2>

3097

3098

3099

3100

<H4><A NAME="htoc137">120</A>  I do not want to type ``forall'' because it is too long, what can I do?</H4>

3101

3102

You can define your own notation for forall:

3103

<PRE>

3104

Notation "fa x : t, P" := (forall x:t, P) (at level 200, x ident).

3105

</PRE>or if your are using CoqIde you can define a pretty symbol for for all and an input method (see <A HREF="#forallcoqide">150</A>).

3106

3107

3108

3109

<H4><A NAME="htoc138">121</A>  How can I define a notation for square?</H4>

3110

3111

You can use for instance:

3112

<PRE>

3113

Notation "x ^2" := (Rmult x x) (at level 20).

3114

</PRE>Note that you can not use:

3115

<TT>N</TT>otation "x �" := (Rmult x x) (at level 20).

3116

3117

because ``2'' is an iso-latin character. If you really want this kind of notation you should use UTF-8.

3118

3119

3120

3121

<H4><A NAME="htoc139">122</A>  Why ``no associativity'' and ``left associativity'' at the same level does not work?</H4>

3122

3123

Because we relie on camlp4 for syntactical analysis and camlp4 does not really implement no associativity. By default, non associative operators are defined as right associative.

3124

3125

3126

3127

<H4><A NAME="htoc140">123</A>  How can I know the associativity associated with a level?</H4>

3128

3129

You can do ``Print Grammar constr'', and decode the output from camlp4, good luck !

3130

3131

3132

3133

<H2><A NAME="htoc141">9</A>  Modules</H2>

3134

3135

3136

3137

3138

3139

3140

3141

3142

3143

Ltac is the tactic language for Coq. It provides the user with a

3144

high-level ``toolbox'' for tactic creation.

3145

3146

3147

3148

<H4><A NAME="htoc144">125</A>  Why do I always get the same error message?</H4>

3149

3150

3151

3152

<H4><A NAME="htoc145">126</A>  Is there any printing command in Ltac?</H4>

3153

3154

You can use the <TT>idtac</TT> tactic with a string argument. This string

3155

will be printed out. The same applies to the <TT>fail</TT> tactic

3156

3157

3158

3159

<H4><A NAME="htoc146">127</A>  What is the syntax for let in Ltac?</H4>

3160

3161

If xi are identifiers and ei and expr are tactic expressions, then let reads:

3162

3163

<TT>let x</TT><TT>1</TT><TT>:=e</TT><TT>1</TT><TT> with x</TT><TT>2</TT><TT>:=e</TT><TT>2</TT><TT>...with x</TT><TT>n</TT><TT>:=e</TT><TT>n</TT><TT> in

3164

expr</TT>.

3165

</DIV>

3166

Beware that if expr is complex (i.e. features at least a sequence) parenthesis

3167

should be added around it. For example:

3168

3169

3170

3171

<TT>twoIntro is defined</TT>

3172

</DIV>

3173

3174

3175

3176

<H4><A NAME="htoc147">128</A>  What is the syntax for pattern matching in Ltac?</H4>

3177

3178

Pattern matching on a term expr (non-linear first order unification)

3179

with patterns pi and tactic expressions ei reads:

3180

3181

3182

<TT>match expr with

3183

p</TT><TT>1</TT><TT> => e</TT><TT>1</TT><TT>

3184

|p</TT><TT>2</TT><TT> => e</TT><TT>2</TT><TT>

3185

... |p</TT><TT>n</TT><TT> => e</TT><TT>n</TT><TT>

3186

| _ => e</TT><TT>n+1</TT><TT>

3187

end.

3188

</TT>

3189

</DIV>

3190

Underscore matches all terms.

3191

3192

3193

3194

<H4><A NAME="htoc148">129</A>  What is the semantics for match goal?</H4>

3195

3196

<TT>match goal</TT> matches the current goal against a series of

3197

patterns: hyp1 ... hypn |- ccl. It uses a

3198

first-order unification algorithm, and tries all the possible

3199

combinations of hypi before dropping the branch and moving to the

3200

next one. Underscore matches all terms.

3201

3202

3203

3204

<H4><A NAME="htoc149">130</A>  How can I generate a new name?</H4>

3205

3206

You can use the following syntax:

3207

<TT>let id:=fresh in ...</TT>

3208

For example:

3209

3210

3211

3212

<TT>introIdGen is defined</TT>

3213

</DIV>

3214

3215

3216

3217

<H4><A NAME="htoc150">131</A>  How can I define static and dynamic code?</H4>

3218

3219

3220

3221

<H2><A NAME="htoc151">11</A>  Tactics written in Ocaml</H2>

3222

3223

3224

3225

<H4><A NAME="htoc152">132</A>  Can you show me an example of a tactic written in OCaml?</H4>

3226

3227

You have some examples of tactics written in Ocaml in the ``contrib'' directory of Coq sources.

3228

3229

3230

3231

<H2><A NAME="htoc153">12</A>  Case studies</H2>

3232

3233

3234

3235

<H4><A NAME="htoc154">133</A>  How can I define vectors or lists of size n?</H4>

3236

3237

3238

3239

<H4><A NAME="htoc155">134</A>  How to prove that 2 sets are different?</H4>

3240

3241

You need to find a property true on one set and false on the

3242

other one. As an example we show how to prove that <TT>bool</TT> and <TT>nat</TT> are discriminable. As discrimination property we take the

3243

property to have no more than 2 elements.

3244

3245

3246

3247

3248

3249

3250

3251

3252

3253

<TT>Coq <       ~ (forall a b:X, ~ (forall x:X, x <> a -> x <> b -> False))).</TT>

3254

3255

3256

3257

3258

3259

3260

3261

3262

3263

3264

3265

3266

</DIV>

3267

3268

<!--TOC subsubsection Is there an axiom-free proof of Streicher's axiom K for

3269

the equality on <TT>nat</TT>?-->

3270

3271

<H4><A NAME="htoc156">135</A>  Is there an axiom-free proof of Streicher's axiom K for

3272

the equality on <TT>nat</TT>?</H4>

3273

3274

3275

Yes, because equality is decidable on <TT>nat</TT>. Here is the proof.

3276

3277

3278

3279

3280

3281

3282

3283

3284

<TT>Coq <   forall (x:nat) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.</TT>

3285

3286

3287

3288

3289

3290

3291

3292

3293

3294

3295

</DIV>

3296

3297

Similarly, we have

3298

3299

3300

3301

3302

3303

3304

3305

3306

3307

3308

3309

</DIV>

3310

3311

3312

3313

<H4><A NAME="htoc157">136</A>  How to prove that two proofs of <TT>n<=m</TT> on <TT>nat</TT> are equal?</H4>

3314

3315

3316

This is provable without requiring any axiom because axiom K

3317

directly holds on <TT>nat</TT>. Here is a proof using question <A HREF="#K-nat">135</A>.

3318

3319

3320

3321

3322

3323

3324

3325

3326

3327

3328

3329

3330

3331

3332

3333

3334

3335

3336

3337

3338

3339

3340

3341

3342

3343

3344

3345

3346

3347

3348

3349

3350

3351

3352

3353

3354

3355

3356

3357

3358

3359

3360

</DIV>

3361

3362

3363

3364

<H4><A NAME="htoc158">137</A>  How to exploit equalities on sets</H4>

3365

3366

To extract information from an equality on sets, you need to

3367

find a predicate of sets satisfied by the elements of the sets. As an

3368

example, let's consider the following theorem.

3369

3370

3371

3372

3373

3374

3375

</DIV>

3376

3377

We have a proof requiring the axiom of proof-irrelevance. We

3378

conjecture that proof-irrelevance can be circumvented by introducing a

3379

primitive definition of discrimination of the proofs of

3380

<CODE>{x : nat | x <= m}</CODE>.

3381

3382

<A HREF="./interval_discr.v">Here</A> is the proof.

3383

3384

3385

<!--TOC subsubsection I have a problem of dependent elimination on

3386

proofs, how to solve it?-->

3387

3388

<H4><A NAME="htoc159">138</A>  I have a problem of dependent elimination on

3389

proofs, how to solve it?</H4>

3390

3391

3392

3393

3394

3395

3396

3397

3398

3399

3400

3401

3402

3403

3404

</DIV>

3405

3406

You need to derive the dependent elimination

3407

scheme for DefProp by hand using <TT>S</TT>cheme.

3408

3409

3410

3411

3412

3413

3414

3415

3416

3417

3418

3419

3420

3421

3422

3423

3424

3425

3426

3427

3428

3429

</DIV>

3430

3431

3432

3433

<H4><A NAME="htoc160">139</A>  And what if I want to prove the following?</H4>

3434

3435

3436

3437

3438

3439

<TT>Coq <   | pS : forall n:nat, natProp n -> natProp (S n).</TT>

3440

3441

3442

<TT>Coq <   pack : forall n:nat, natProp n -> package.</TT>

3443

3444

3445

3446

3447

3448

</DIV>

3449

3450

3451

3452

3453

3454

<TT>Coq < Definition pack_S : package -> package.</TT>

3455

3456

3457

3458

3459

3460

3461

3462

3463

3464

3465

3466

3467

3468

3469

3470

3471

3472

3473

3474

3475

3476

3477

3478

3479

3480

3481

3482

3483

3484

3485

3486

3487

3488

3489

3490

3491

3492

</DIV>

3493

3494

3495

3496

<H2><A NAME="htoc161">13</A>  Publishing tools</H2>

3497

3498

3499

3500

<H4><A NAME="htoc162">140</A>  How can I generate some latex from my development?</H4>

3501

3502

You can use <TT>coqdoc</TT>.

3503

3504

3505

3506

<H4><A NAME="htoc163">141</A>  How can I generate some HTML from my development?</H4>

3507

3508

You can use <TT>coqdoc</TT>.

3509

3510

3511

3512

<H4><A NAME="htoc164">142</A>  How can I generate some dependency graph from my development?</H4>

3513

3514

3515

3516

<H4><A NAME="htoc165">143</A>  How can I cite some Coq in my latex document?</H4>

3517

3518

You can use <TT>coq_tex</TT>.

3519

3520

3521

3522

<H4><A NAME="htoc166">144</A>  How can I cite the Coq reference manual?</H4>

3523

3524

You can use this bibtex entry:

3525

<PRE>

3526

@Manual{Coq:manual,

3527

title = {The Coq proof assistant reference manual},

3528

author = {\mbox{The Coq development team}},

3529

organization = {LogiCal Project},

3530

note = {Version 8.0},

3531

year = {2004},

3532

url = "http://coq.inria.fr"

3533

}

3534

</PRE>

3535

3536

3537

<H4><A NAME="htoc167">145</A>  Where can I publish my developments in Coq?</H4>

3538

3539

You can submit your developments as a user contribution to the Coq

3540

development team. This ensures its liveness along the evolution and

3541

possible changes of Coq.

3542

3543

You can also submit your developments to the HELM/MoWGLI repository at

3544

the University of Bologna (see

3545

<A HREF="http://mowgli.cs.unibo.it"><TT>http://mowgli.cs.unibo.it</TT></A>). For

3546

developments submitted in this database, it is possible to visualize

3547

the developments in natural language and execute various retrieving

3548

requests.

3549

3550

3551

3552

<H4><A NAME="htoc168">146</A>  How can I read my proof in natural language?</H4>

3553

3554

You can submit your proof to the HELM/MoWGLI repository and use the

3555

rendering tool provided by the server (see

3556

<A HREF="http://mowgli.cs.unibo.it"><TT>http://mowgli.cs.unibo.it</TT></A>).

3557

3558

3559

3560

<H2><A NAME="htoc169">14</A>  CoqIde</H2>

3561

3562

3563

3564

<H4><A NAME="htoc170">147</A>  What is CoqIde?</H4>

3565

3566

CoqIde is a gtk based GUI for Coq.

3567

3568

3569

3570

<H4><A NAME="htoc171">148</A>  How to enable Emacs keybindings?</H4>

3571

3572

Insert <TT>gtk-key-theme-name = "Emacs"</TT>

3573

in your <TT>.coqide-gtk2rc</TT> file. It may be in the current dir

3574

or in <CODE>$HOME</CODE> dir. This is done by default.

3575

3576

3577

3578

<H4><A NAME="htoc172">149</A>  How to enable antialiased fonts?</H4>

3579

3580

Set the <CODE>GDK_USE_XFT</CODE> variable to <CODE>1</CODE>. This is by default with <CODE>Gtk >= 2.2</CODE>.

3581

If some of your fonts are not available, set <CODE>GDK_USE_XFT</CODE> to <CODE>0</CODE>.

3582

3583

3584

3585

<H4><A NAME="htoc173">150</A>  How to use those Forall and Exists pretty symbols?</H4>

3586

3587

Thanks to the notation features in Coq, you just need to insert these

3588

lines in your Coq buffer:

3589

<TT>N</TT>otation "for all x : t, P" := (forall x:t, P) (at level 200, x ident).

3590

3591

<TT>N</TT>otation "there exists x : t, P" := (exists x:t, P) (at level 200, x ident).

3592

3593

3594

Copy/Paste of these lines from this file will not work outside of CoqIde.

3595

You need to load a file containing these lines or to enter the for all

3596

using an input method (see <A HREF="#inputmeth">151</A>). To try it just use <CODE>Require Import utf8</CODE> from inside

3597

CoqIde.

3598

To enable these notations automatically start coqide with

3599

<PRE>

3600

coqide -l utf8

3601

</PRE>In the ide subdir of Coq library, you will find a sample utf8.v with some

3602

pretty simple notations.

3603

3604

3605

3606

<H4><A NAME="htoc174">151</A>  How to define an input method for non ASCII symbols?</H4>

3607

3608

3609

First solution: type <CODE><CONTROL><SHIFT>2200</CODE> to enter a forall in the script widow.

3610

2200 is the hexadecimal code for forall in unicode charts and is encoded as

3611

in UTF-8.

3612

2203 is for exists. See <A HREF="http://www.unicode.org"><TT>http://www.unicode.org</TT></A> for more codes.

3613

<LI>Second solution: rebind <CODE><AltGr>a</CODE> to forall and <CODE><AltGr>e</CODE> to exists.

3614

Under X11, you need to use something like

3615

<PRE>

3616

xmodmap -e "keycode 24 = a A F13 F13"

3617

xmodmap -e "keycode 26 = e E F14 F14"

3618

</PRE> and then to add

3619

<PRE>

3620

bind "F13" {"insert-at-cursor" ("")}

3621

bind "F14" {"insert-at-cursor" ("")}

3622

</PRE> to your "binding "text"" section in <CODE>.coqiderc-gtk2rc.</CODE>

3623

The strange ("") argument is the UTF-8 encoding for

3624

0x2200.

3625

You can compute these encodings using the lablgtk2 toplevel with

3626

<PRE>

3627

Glib.Utf8.from_unichar 0x2200;;

3628

</PRE> Further symbols can be bound on higher Fxx keys or on even on other keys you

3629

do not need .

3630

</UL>

3631

3632

3633

<H4><A NAME="htoc175">152</A>  How to build a custom CoqIde with user ml code?</H4>

3634

3635

Use

3636

coqmktop -ide -byte m1.cmo...mi.cmo

3637

3638

coqmktop -ide -opt m1.cmx...mi.cmx

3639

3640

3641

3642

<H4><A NAME="htoc176">153</A>  How to customize the shortcuts for menus?</H4>

3643

3644

Two solutions are offered:

3645

3646

Edit $HOME/.coqide.keys by hand or

3647

<LI>Add "gtk-can-change-accels = 1" in your .coqide-gtk2rc file. Then

3648

from CoqIde, you may select a menu entry and press the desired

3649

shortcut.

3650

</UL>

3651

3652

3653

<H4><A NAME="htoc177">154</A>  What encoding should I use? What is this \x{iiii} in my file?</H4>

3654

3655

The encoding option is related to the way files are saved.

3656

Keep it as UTF-8 until it becomes important for you to exchange files

3657

with non UTF-8 aware applications.

3658

If you choose something else than UTF-8, then missing characters will

3659

be encoded by \x{....} or \x{........}

3660

where each dot is an hex. digit.

3661

The number between braces is the hexadecimal UNICODE index for the

3662

missing character.

3663

3664

3665

3666

<H2><A NAME="htoc178">15</A>  Extraction</H2>

3667

3668

3669

3670

<H4><A NAME="htoc179">155</A>  What is program extraction?</H4>

3671

3672

Program extraction consist in generating a program from a constructive proof.

3673

3674

3675

3676

<H4><A NAME="htoc180">156</A>  Which language can I extract to?</H4>

3677

3678

You can extract your programs to Objective Caml and Haskell.

3679

3680

3681

3682

<H4><A NAME="htoc181">157</A>  How can I extract an incomplete proof?</H4>

3683

3684

You can provide programs for your axioms.

3685

3686

3687

3688

<H2><A NAME="htoc182">16</A>  Glossary</H2>

3689

3690

3691

3692

<H4><A NAME="htoc183">158</A>  Can you explain me what an evaluable constant is?</H4>

3693

3694

An evaluable constant is a constant which is unfoldable.

3695

3696

3697

3698

3699

3700

The goal is the statement to be proved.

3701

3702

3703

3704

<H4><A NAME="htoc185">160</A>  What is a meta variable?</H4>

3705

3706

A meta variable in Coq represents a ``hole'', i.e. a part of a proof

3707

that is still unknown.

3708

3709

3710

3711

<H4><A NAME="htoc186">161</A>  What is Gallina?</H4>

3712

3713

Gallina is the specification language of Coq. Complete documentation

3714

of this language can be found in the Reference Manual.

3715

3716

3717

3718

<H4><A NAME="htoc187">162</A>  What is The Vernacular?</H4>

3719

3720

It is the language of commands of Gallina i.e. definitions, lemmas, ...

3721

3722

3723

3724

<H4><A NAME="htoc188">163</A>  What is a dependent type?</H4>

3725

3726

A dependant type is a type which depends on some term. For instance

3727

``vector of size n'' is a dependant type representing all the vectors

3728

of size n. Its type depends on n

3729

3730

3731

3732

<H4><A NAME="htoc189">164</A>  What is a proof by reflection?</H4>

3733

3734

This is a proof generated by some computation which is done using the

3735

internal reduction of Coq (not using the tactic language of Coq

3736

(Ltac) nor the implementation language for Coq). An example of

3737

tactic using the reflection mechanism is the <TT>ring</TT> tactic. The

3738

reflection method consist in reflecting a subset of Coq language (for

3739

example the arithmetical expressions) into an object of the Coqlanguage itself (in this case an inductive type denoting arithmetical

3740

expressions). For more information see [<A HREF="#howe"><CITE>13</CITE></A><CITE>, </CITE><A HREF="#harrison"><CITE>11</CITE></A><CITE>, </CITE><A HREF="#boutin"><CITE>2</CITE></A>]

3741

and the last chapter of the Coq'Art.

3742

3743

3744

3745

<H4><A NAME="htoc190">165</A>  What is intuitionistic logic?</H4>

3746

3747

This is any logic which does not assume that ``A or not A''.

3748

3749

3750

3751

<H4><A NAME="htoc191">166</A>  What is proof-irrelevance?</H4>

3752

3753

See question <A HREF="#proof-irrelevance">34</A>

3754

3755

3756

3757

<H4><A NAME="htoc192">167</A>  What is the difference between opaque and transparent?</H4>

3758

3759

3760

Opaque definitions can not be unfolded but transparent ones can.

3761

3762

3763

3764

<H2><A NAME="htoc193">17</A>  Troubleshooting</H2>

3765

3766

3767

3768

3769

3770

Sometime you can use the <TT>abstract</TT> tactic, which makes as if you had

3771

stated some local lemma, this speeds up the typing process.

3772

3773

3774

3775

<H4><A NAME="htoc195">169</A>  Why <TT>Reset Initial.</TT> does not work when using <TT>coqc</TT>?</H4>

3776

3777

The initial state corresponds to the state of coqtop when the interactive

3778

session began. It does not make sense in files to compile.

3779

3780

3781

3782

<H4><A NAME="htoc196">170</A>  What can I do if I get ``No more subgoals but non-instantiated existential variables''?</H4>

3783

3784

This means that <TT>eauto</TT> or <TT>eapply</TT> didn't instantiate an

3785

existential variable which eventually got erased by some computation.

3786

You have to backtrack to the faulty occurrence of <TT>eauto</TT> or

3787

<TT>eapply</TT> and give the missing argument an explicit value.

3788

3789

3790

3791

<H4><A NAME="htoc197">171</A>  What can I do if I get ``Cannot solve a second-order unification problem''?</H4>

3792

3793

You can help Coq using the <TT>pattern</TT> tactic.

3794

3795

3796

3797

<H4><A NAME="htoc198">172</A>  Why does Coq tell me that <TT>{x:A|(P x)}</TT> is not convertible with <TT>(sig A P)</TT>?</H4>

3798

3799

This is because <TT>{x:A|P x}</TT> is a notation for

3800

<TT>sig (fun x:A => P x)</TT>. Since Coq does not reason up to

3801

eta-conversion, this is different from <TT>sig P</TT>.

3802

3803

<!--TOC subsubsection I copy-paste a term and Coq says it is not convertible

3804

to the original term. Sometimes it even says the copied term is not

3805

well-typed.-->

3806

3807

<H4><A NAME="htoc199">173</A>  I copy-paste a term and Coq says it is not convertible

3808

to the original term. Sometimes it even says the copied term is not

3809

well-typed.</H4>

3810

3811

This is probably due to invisible implicit information (implicit

3812

arguments, coercions and Cases annotations) in the printed term, which

3813

is not re-synthesised from the copied-pasted term in the same way as

3814

it is in the original term.

3815

3816

Consider for instance <TT>(@eq Type True True)</TT>. This term is

3817

printed as <TT>True=True</TT> and re-parsed as <TT>(@eq Prop True

3818

True)</TT>. The two terms are not convertible (hence they fool tactics

3819

like <TT>pattern</TT>).

3820

3821

There is currently no satisfactory answer to the problem. However,

3822

the command <TT>Set Printing All</TT> is useful for diagnosing the

3823

problem.

3824

3825

Due to coercions, one may even face type-checking errors. In some

3826

rare cases, the criterion to hide coercions is a bit too loose, which

3827

may result in a typing error message if the parser is not able to find

3828

again the missing coercion.

3829

3830

3831

3832

<H2><A NAME="htoc200">18</A>  Conclusion and Farewell.</H2>

3833

3834

3835

3836

3837

<H4><A NAME="htoc201">174</A>  What if my question isn't answered here?</H4>

3838

3839

3840

Don't panic <CODE>:-)</CODE>. You can try the Coq manual [<A HREF="#Coq:manual"><CITE>15</CITE></A>] for a technical

3841

description of the prover. The Coq'Art [<A HREF="#Coq:coqart"><CITE>1</CITE></A>] is the first

3842

book written on Coq and provides a comprehensive review of the

3843

theorem prover as well as a number of example and exercises. Finally,

3844

the tutorial [<A HREF="#Coq:Tutorial"><CITE>14</CITE></A>] provides a smooth introduction to

3845

theorem proving in Coq.

3846

3847

3848

3849

3850

3851

<H2>References</H2>

3852

3853

Yves Bertot and Pierre Cast�ran.

3854

Interactive Theorem Proving and Program Development, Coq'Art:

3855

The Calculus of Inductive Constructions.

3856

Texts in Theoretical Computer Science. An EATCS series. Springer

3857

Verlag, 2004.

3858

3859

3860

Samuel Boutin.

3861

Using reflection to build efficient and certified decision pro

3862

cedures.

3863

In M. Abadi and T. Ito, editors, Proceedings of TACS'97, volume

3864

1281 of LNCS. Springer-Verlag, 1997.

3865

3866

3867

David Carlisle, Scott Pakin, and Alexander Holt.

3868

The Great, Big List of LATEX Symbols, February 2001.

3869

3870

3871

Thierry Coquand.

3872

Une Th�orie des Constructions.

3873

PhD thesis, Universit� Paris 7, January 1985.

3874

3875

3876

Thierry Coquand and G�rard Huet.

3877

The Calculus of Constructions.

3878

Information and Computation, 76(2/3), 1988.

3879

3880

3881

Thierry Coquand and Christine Paulin-Mohring.

3882

Inductively defined types.

3883

In P. Martin-L�f and G. Mints, editors, Proceedings of

3884

Colog'88, volume 417 of Lecture Notes in Computer Science.

3885

Springer-Verlag, 1990.

3886

3887

3888

Gilles Dowek.

3889

Th�orie des types.

3890

Lecture notes, 2002.

3891

3892

3893

Eduardo Gim�nez.

3894

Un Calcul de Constructions Infinies et son application a la

3895

v�rification de syst�mes communicants.

3896

th�se d'universit�, Ecole Normale Sup�rieure de Lyon, December 1996.

3897

3898

3899

Jean-Yves Girard.

3900

Une extension de l'interpr�tation de G�del � l'analyse, et

3901

son application � l'�limination des coupures dans l'analyse et la

3902

th�orie des types.

3903

In Proceedings of the 2nd Scandinavian Logic Symposium.

3904

North-Holland, 1970.

3905

3906

3907

Jean-Yves Girard, Yves Lafont, and Paul Taylor.

3908

Proofs and Types.

3909

Cambrige Tracts in Theoretical Computer Science, Cambridge University

3910

Press, 1989.

3911

3912

3913

John Harrison.

3914

Meta theory and reflection in theorem proving:a survey and cri tique.

3915

Technical Report CRC-053, SRI International Cambridge Computer

3916

Science Research Center, 1995.

3917

3918

3919

Martin Hofmann and Thomas Streicher.

3920

The groupoid interpretation of type theory.

3921

In Proceedings of the meeting Twenty-five years of constructive

3922

type theory. Oxford University Press, 1998.

3923

3924

3925

Doug Howe.

3926

Computation meta theory in nuprl.

3927

In E. Lusk and R. Overbeek, editors, The Proceedings of the

3928

Ninth International Conference of Autom ated Deduction, volume 310, pages

3929

238--257. Springer-Verlag, 1988.

3930

3931

3932

G�rard Huet, Gilles Kahn, and Christine Paulin-Mohring.

3933

The Coq Proof Assistant A Tutorial, 2004.

3934

3935

3936

The Coq development team.

3937

The Coq proof assistant reference manual.

3938

LogiCal Project, 2004.

3939

Version 8.0.

3940

3941

3942

Tobias Oetiker.

3943

The Not So Short Introduction to LATEX2e, January 1999.

3944

3945

3946

Christine Paulin-Mohring.

3947

D�finitions Inductives en Th�orie des Types d'Ordre Sup�rieur.

3948

Habilitation � diriger les recherches, Universit� Claude Bernard Lyon

3949

I, December 1996.</DL>

3950

3951

3952

3953

3954

3955

3956

3957

3958

3959

<BLOCKQUOTE>This document was translated from LATEX by

3960

<A HREF="http://pauillac.inria.fr/~maranget/hevea/index.html">HEVEA</A>.

3961

</BLOCKQUOTE>

3962

</BODY>

3963

</HTML>

Older »