research-article

How to make ad hoc proof automation less ad hoc

Authors:

Georges Gonthier,

Aleksandar Nanevski,

Derek DreyerAuthors Info & Claims

ACM SIGPLAN Notices, Volume 46, Issue 9

Pages 163 - 175

https://doi.org/10.1145/2034574.2034798

Published: 19 September 2011 Publication History

Abstract

Most interactive theorem provers provide support for some form of user-customizable proof automation. In a number of popular systems, such as Coq and Isabelle, this automation is achieved primarily through tactics, which are programmed in a separate language from that of the prover's base logic. While tactics are clearly useful in practice, they can be difficult to maintain and compose because, unlike lemmas, their behavior cannot be specified within the expressive type system of the prover itself.

We propose a novel approach to proof automation in Coq that allows the user to specify the behavior of custom automated routines in terms of Coq's own type system. Our approach involves a sophisticated application of Coq's canonical structures, which generalize Haskell type classes and facilitate a flexible style of dependently-typed logic programming. Specifically, just as Haskell type classes are used to infer the canonical implementation of an overloaded term at a given type, canonical structures can be used to infer the canonical proof of an overloaded lemma for a given instantiation of its parameters. We present a series of design patterns for canonical structure programming that enable one to carefully and predictably coax Coq's type inference engine into triggering the execution of user-supplied algorithms during unification, and we illustrate these patterns through several realistic examples drawn from Hoare Type Theory. We assume no prior knowledge of Coq and describe the relevant aspects of Coq type inference from first principles.

Supplementary Material

MP4 File (_talk3.mp4)

Download
51.75 MB

References

[1]

Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi. Hints in unification. In TPHOLs, volume 5674 of LNCS, pages 84--98, 2009.

Digital Library

[2]

Bruno Barras, Jean-Pierre Jouannaud, Pierre-Yves Strub, and Qian Wang. CoqMTU: a higher-order type theory with a predicative hierarchy of universes parametrized by a decidable first-order theory. In LICS, pages 143--151, 2011.

Digital Library

[3]

Yves Bertot, Georges Gonthier, Sidi Ould Biha, and Ioana Pasca. Canonical big operators. In TPHOLs, volume 5170 of LNCS, pages 86--101, 2008.

Digital Library

[4]

Thomas Braibant and Damien Pous. Rewriting modulo associativity and commutativity in Coq. In Second Coq workshop, 2010.

[5]

Manuel M. T. Chakravarty, Gabriele Keller, and Simon Peyton Jones. Associated type synonyms. In ICFP, pages 241--253, 2005.

Digital Library

[6]

Adam Chlipala. Certified programming with dependent types. URL: http://adam.chlipala.net/cpdt, 2008.

[7]

Adam Chlipala. Mostly-automated verification of low-level programs in computational separation logic. In PLDI, 2011.

Digital Library

[8]

Georges Gonthier. Formal proof - the four-color theorem. Notices of the AMS, 55(11):1382--93, 2008.

[9]

Georges Gonthier. Point-free, set-free concrete linear algebra. In ITP, 2011.

Digital Library

[10]

Georges Gonthier and Assia Mahboubi. An introduction to small scale reflection in Coq. Journal of Formalized Reasoning, 3(2):95--152, 2010.

[11]

Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, and Derek Dreyer. How to make ad hoc proof automation less ad hoc, 2011. Code + appendix: http://www.mpi-sws.org/~beta/lessadhoc.

Digital Library

[12]

Benjamin Grégoire and Assia Mahboubi. Proving equalities in a commutative ring done right in Coq. In TPHOLs, pages 98--113, 2005.

Digital Library

[13]

Cordelia Hall, Kevin Hammond, Simon Peyton Jones, and Philip Wadler. Type classes in Haskell. TOPLAS, 18:241--256, 1996.

Digital Library

[14]

Limin Jia, Jianzhou Zhao, Vilhelm Sjöberg, and Stephanie Weirich. Dependent types and program equivalence. In POPL, pages 275--286, 2010.

Digital Library

[15]

Mark P. Jones. Type classes with functional dependencies. In ESOP, pages 230--244, 2000.

Digital Library

[16]

Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: formal verification of an operating-system kernel. CACM, 53(6):107--115, 2010.

Digital Library

[17]

Xavier Leroy. Formal verification of a realistic compiler. CACM, 52:107--115, July 2009.

Digital Library

[18]

J. Garrett Morris and Mark P. Jones. Instance chains: Type class programming without overlapping instances. In ICFP, pages 375--386, 2010.

Digital Library

[19]

Aleksandar Nanevski, Viktor Vafeiadis, and Josh Berdine. Structuring the verification of heap-manipulating programs. In POPL, pages 261--274, 2010.

Digital Library

[20]

Brigitte Pientka and Joshua Dunfield. Programming with proofs and explicit contexts. In PPDP, pages 163--173, 2008.

Digital Library

[21]

Adam Poswolsky and Carsten Schürmann. System description: Delphin - a functional programming language for deductive systems. ENTCS, 228:113--120, 2009.

Digital Library

[22]

John C. Reynolds. Separation logic: a logic for shared mutable data structures. In LICS, 2002.

Digital Library

[23]

Amokrane Saïbi. Typing algorithm in type theory with inheritance. In POPL, pages 292--301, 1997.

Digital Library

[24]

Matthieu Sozeau and Nicolas Oury. First-class type classes. In TPHOLs, volume 5170 of LNCS, pages 278--293, 2008.

Digital Library

[25]

Bas Spitters and Eelis van der Weegen. Type classes for mathematics in type theory. MSCS, Special issue on 'Interactive theorem proving and the formalization of mathematics', 21:1--31, 2011.

[26]

Antonis Stampoulis and Zhong Shao. VeriML: Typed computation of logical terms inside a language with effects. In ICFP, pages 333--344, 2010.

Digital Library

[27]

Pierre-Yves Strub. Coq modulo theory. In CSL, pages 529--543, 2010.

Digital Library

[28]

Philip Wadler and Stephen Blott. How to make ad-hoc polymorphism less ad hoc. In POPL, pages 60--76, 1989.

Digital Library

Cited By

Farka FKomendantskaya EHammond K(2017)Coinductive Soundness of Corecursive Type Class ResolutionLogic-Based Program Synthesis and Transformation10.1007/978-3-319-63139-4_18(311-327)Online publication date: 25-Jul-2017
https://doi.org/10.1007/978-3-319-63139-4_18
Malecha GBengtson J(2016)Extensible and Efficient Automation Through Reflective TacticsProgramming Languages and Systems10.1007/978-3-662-49498-1_21(532-559)Online publication date: 2016
https://doi.org/10.1007/978-3-662-49498-1_21
Fu PKomendantskaya E(2015)A Type-Theoretic Approach to ResolutionRevised Selected Papers of the 25th International Symposium on Logic-Based Program Synthesis and Transformation - Volume 952710.1007/978-3-319-27436-2_6(91-106)Online publication date: 13-Jul-2015
https://dl.acm.org/doi/10.1007/978-3-319-27436-2_6
Show More Cited By

Index Terms

How to make ad hoc proof automation less ad hoc
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Data types and structures
2. Theory of computation
  1. Logic
    1. Constraint and logic programming
  2. Semantics and reasoning
    1. Program reasoning
      1. Program verification

Recommendations

How to make ad hoc proof automation less ad hoc
ICFP '11: Proceedings of the 16th ACM SIGPLAN international conference on Functional programming

Most interactive theorem provers provide support for some form of user-customizable proof automation. In a number of popular systems, such as Coq and Isabelle, this automation is achieved primarily through tactics, which are programmed in a separate ...
Mtac: a monad for typed tactic programming in Coq
ICFP '13: Proceedings of the 18th ACM SIGPLAN international conference on Functional programming

Effective support for custom proof automation is essential for large scale interactive proof development. However, existing languages for automation via *tactics* either (a) provide no way to specify the behavior of tactics within the base logic of the ...
Mtac: a monad for typed tactic programming in Coq
ICFP '13

Effective support for custom proof automation is essential for large scale interactive proof development. However, existing languages for automation via *tactics* either (a) provide no way to specify the behavior of tactics within the base logic of the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 46, Issue 9

ICFP '11

September 2011

456 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2034574

Issue’s Table of Contents

ICFP '11: Proceedings of the 16th ACM SIGPLAN international conference on Functional programming
September 2011
470 pages
ISBN:9781450308656
DOI:10.1145/2034773
General Chairs:
Manuel Chakravarty
University of New South Wales, Australia
,
Zhenjiang Hu
National Institute of Informatics, Japan
,
Program Chair:
Olivier Danvy
Aarhus University, Denmark

Copyright © 2011 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 19 September 2011

Published in SIGPLAN Volume 46, Issue 9

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

50
Total Citations
View Citations
439
Total Downloads

Downloads (Last 12 months)22
Downloads (Last 6 weeks)2

Reflects downloads up to 16 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Farka FKomendantskaya EHammond K(2017)Coinductive Soundness of Corecursive Type Class ResolutionLogic-Based Program Synthesis and Transformation10.1007/978-3-319-63139-4_18(311-327)Online publication date: 25-Jul-2017
https://doi.org/10.1007/978-3-319-63139-4_18
Malecha GBengtson J(2016)Extensible and Efficient Automation Through Reflective TacticsProgramming Languages and Systems10.1007/978-3-662-49498-1_21(532-559)Online publication date: 2016
https://doi.org/10.1007/978-3-662-49498-1_21
Fu PKomendantskaya E(2015)A Type-Theoretic Approach to ResolutionRevised Selected Papers of the 25th International Symposium on Logic-Based Program Synthesis and Transformation - Volume 952710.1007/978-3-319-27436-2_6(91-106)Online publication date: 13-Jul-2015
https://dl.acm.org/doi/10.1007/978-3-319-27436-2_6
Delaware Bd. S. Oliveira BSchrijvers T(2013)Meta-theory à la carteACM SIGPLAN Notices10.1145/2480359.242909448:1(207-218)Online publication date: 23-Jan-2013
https://dl.acm.org/doi/10.1145/2480359.2429094
Delaware Bd. S. Oliveira BSchrijvers TGiacobazzi RCousot R(2013)Meta-theory à la carteProceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/2429069.2429094(207-218)Online publication date: 23-Jan-2013
https://dl.acm.org/doi/10.1145/2429069.2429094
Mahboubi ATassi E(2013)Canonical structures for the working coq userProceedings of the 4th international conference on Interactive Theorem Proving10.1007/978-3-642-39634-2_5(19-34)Online publication date: 22-Jul-2013
https://dl.acm.org/doi/10.1007/978-3-642-39634-2_5
Makarov ESpitters B(2013)The picard algorithm for ordinary differential equations in coqProceedings of the 4th international conference on Interactive Theorem Proving10.1007/978-3-642-39634-2_34(463-468)Online publication date: 22-Jul-2013
https://dl.acm.org/doi/10.1007/978-3-642-39634-2_34
Gonthier GAsperti AAvigad JBertot YCohen CGarillot FLe Roux SMahboubi AO'Connor RBiha SPasca IRideau LSolovyev ATassi EThéry L(2013)A machine-checked proof of the odd order theoremProceedings of the 4th international conference on Interactive Theorem Proving10.1007/978-3-642-39634-2_14(163-179)Online publication date: 22-Jul-2013
https://dl.acm.org/doi/10.1007/978-3-642-39634-2_14
Hobor AGherghina C(2012)Barriers in Concurrent Separation Logic: Now With Tool Support!Logical Methods in Computer Science10.2168/LMCS-8(2:2)20128:2Online publication date: 20-Apr-2012
https://doi.org/10.2168/LMCS-8(2:2)2012
Armstrong AFoster SStruth G(2012)Dependently typed programming based on automated theorem provingProceedings of the 11th international conference on Mathematics of Program Construction10.1007/978-3-642-31113-0_12(220-240)Online publication date: 25-Jun-2012
https://dl.acm.org/doi/10.1007/978-3-642-31113-0_12
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents