meta.yml

---
fullname: Lemma Overloading
shortname: lemma-overloading
organization: coq-community
community: true
action: true
coqdoc: true
doi: 10.1017/S0956796813000051

synopsis: >-
  Libraries demonstrating design patterns for programming and proving
  with canonical structures in Coq

description: |-
  This project contains Hoare Type Theory libraries which
  demonstrate a series of design patterns for programming
  with canonical structures that enable one to carefully
  and predictably coax Coq's type inference engine into triggering
  the execution of user-supplied algorithms during unification, and
  illustrates these patterns through several realistic examples drawn
  from Hoare Type Theory. The project also contains typeclass-based
  re-implementations for comparison.

publications:
- pub_url: https://software.imdea.org/~aleks/papers/lessadhoc/journal.pdf
  pub_title: How to make ad hoc proof automation less ad hoc
  pub_doi: 10.1017/S0956796813000051
- pub_url: https://software.imdea.org/~aleks/papers/reflect/reflect.pdf
  pub_title: Structuring the verification of heap-manipulating programs
  pub_doi: 10.1145/1706299.1706331

authors:
- name: Georges Gonthier
  initial: true
- name: Beta Ziliani
  initial: true
- name: Aleksandar Nanevski
  initial: true
- name: Derek Dreyer
  initial: true

maintainers:
- name: Anton Trunov
  nickname: anton-trunov

opam-file-maintainer: palmskog@gmail.com

opam-file-version: dev

license:
  fullname: GNU General Public License v3.0 or later
  identifier: GPL-3.0-or-later
  file: LICENSE.md

supported_coq_versions:
  text: 8.16 or later (use releases for other Coq versions)
  opam: '{>= "8.16"}'

tested_coq_opam_versions:
- version: '2.0.0-coq-8.16'
  repo: 'mathcomp/mathcomp'
- version: '2.0.0-coq-8.17'
  repo: 'mathcomp/mathcomp'
- version: '2.0.0-coq-8.18'
  repo: 'mathcomp/mathcomp'
- version: '2.1.0-coq-8.16'
  repo: 'mathcomp/mathcomp'
- version: '2.1.0-coq-8.17'
  repo: 'mathcomp/mathcomp'
- version: '2.1.0-coq-8.18'
  repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.16'
  repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.17'
  repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.18'
  repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.19'
  repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.20'
  repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-dev'
  repo: 'mathcomp/mathcomp'
- version: 'coq-8.18'
  repo: 'mathcomp/mathcomp-dev'
- version: 'coq-8.19'
  repo: 'mathcomp/mathcomp-dev'
- version: 'coq-8.20'
  repo: 'mathcomp/mathcomp-dev'
- version: 'coq-dev'
  repo: 'mathcomp/mathcomp-dev'

dependencies:
- opam:
    name: coq-hierarchy-builder
    version: '{>= "1.5.0"}'
  description: |-
    [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) 1.5.0 or later
- opam:
    name: coq-mathcomp-ssreflect
    version: '{>= "2.0"}'
  nix: ssreflect
  description: |-
    [MathComp](https://math-comp.github.io) 2.0.0 or later (`ssreflect` suffices)

namespace: LemmaOverloading

keywords:
- name: canonical structures
- name: proof automation
- name: hoare type theory
- name: lemma overloading

categories:
- name: Computer Science/Data Types and Data Structures

documentation: |-
  ## Files described in the paper

  The Coq source files mentioned in the paper [How to make ad hoc proof automation less ad hoc][lessadhoc],
  Journal of Functional Programming 23(4), pp. 357-401, are described below. See also the
  [coqdoc presentation][coqdoc] of the files from the latest release.
  
  ### `indom.v`
  
  This file contains the indomR lemma from Section 3 "A simple overloaded lemma"
  
  ### `terms.v`, `xfind.v`, `cancel.v`, `cancelD.v`, `cancel2.v`
  
  These files prove the `cancelR` lemma from Section 4 "Reflection: Turning
  semantics into syntax". The first one contains the abstract syntax for heaps
  along with the lemma `cancel_sound`. `xfind.v` has the xfind structure
  to find an element in a list, return its index, and extend the list if the
  element is not found. The file `cancel.v` has the main overloaded lemma `cancelR`.
  Finally, `cancelD.v` contains the `simplify` lemma from section 4.3 and `cancel2.v`
  contains an alternative version of the cancellation function without using
  reflection.
   
  ### `stlogR.v`
  
  File containing a whole bunch of overloaded lemmas to automate the verification
  of imperative programs using Hoare Type Theory. The main technicalities in this
  file are covered in Section 5 "Solving for functional instances".
  
  ### `noalias.v`
  
  File containing all the automated lemmas described in Section 6 "Flexible
  composition and application of overloaded lemmas".
  
  
  ## Bonus track
  
  The files below didn't make it to the paper but deserve attention.
  
  ### `auto.v`
  
  This file contains an adapted example from VeriML (Stampoulist and Shao),
  to automatically prove propositions in a logic with binders.
  
  ### `llistR.v`
  
  Verification of a linked list datatype using the "step" overloaded lemma described in Section 5.2.
  
  ### `noaliasBT.v`
  
  There are several ways to attack a problem.
  Some of them lead to interesting but yet not entirely satisfactory results.
  Here are two versions of the `noalias` overloaded lemma with a different look.
  
  ### `indomCTC.v`, `xfindCTC.v`, `cancelCTC.v`, `noaliasCTC.v`, `stlogCTC.v` 
  
  These files contains the same automated lemmas as in the files `indom`, `cancel`,
  `noalias` and `stlogR`, but done with Coq Type Classes. 
  
  ## Other files
  
  The files not mentioned above are part of the HTT library,
  introduced in the paper [Structuring the Verification of Heap-Manipulating Programs][reflect],
  Proceedings of the Symposium on Principles of Programming Languages (POPL) 2010,
  pp. 261-274.

  [lessadhoc]: https://software.imdea.org/~aleks/papers/lessadhoc/journal.pdf
  [reflect]: https://software.imdea.org/~aleks/papers/reflect/reflect.pdf
  [coqdoc]: https://coq-community.github.io/lemma-overloading/docs/latest/coqdoc/toc.html
---