Skip to content
Snippets Groups Projects
Select Git revision
  • fix-export
  • instance-nobody-open-proof
  • ralf/notation
  • master default protected
  • robbert/set_rename
  • robbert/map_seq
  • ci/debug
  • ci/opam2
  • ci/perf
  • ci/buildcache
  • ci/ralf/mangled
  • ralf/exact_vm_cast
  • ci/coqdoc
  • ci/artifacts
  • coq-stdpp-1.0
  • options
  • coq-stdpp-1.1.0
  • coq-stdpp-1.0.0
18 results
Compare
Forked from Iris / stdpp
2279 commits behind the upstream repository.
user avatar
Set Hint Mode for all classes in `base.v`.
Robbert Krebbers authored 
This provides significant robustness against looping type class search.

As a consequence, at many places throughout the library we had to add
additional typing information to lemmas. This was to be expected, since
most of the old lemmas were ambiguous. For example:

  Section fin_collection.
    Context `{FinCollection A C}.

    size_singleton (x : A) : size {[ x ]} = 1.

In this case, the lemma does not tell us which `FinCollection` with
elements `A` we are talking about. So, `{[ x ]}` could not only refer to
the singleton operation of the `FinCollection A C` in the section, but
also to any other `FinCollection` in the development. To make this lemma
unambigious, it should be written as:

  Lemma size_singleton (x : A) : size ({[ x ]} : C) = 1.

In similar spirit, lemmas like the one below were also ambiguous:

  Lemma lookup_alter_None {A} (f : A → A) m i j :
    alter f i m !! j = None :left_right_arrow: m !! j = None.

It is not clear which finite map implementation we are talking about.
To make this lemma unambigious, it should be written as:

  Lemma lookup_alter_None {A} (f : A → A) (m : M A) i j :
    alter f i m !! j = None :left_right_arrow: m !! j = None.

That is, we have to specify the type of `m`.
7d7c9871
History
user avatar 7d7c9871
History
Name Last commit Last update
build
theories
.gitignore
.gitlab-ci.yml
CONTRIBUTING.md
LICENSE
Makefile
README.md
_CoqProject
awk.Makefile
opam
opam.pins
README.md

Coq-std++

This project contains an extended "Standard Library" for Coq called coq-std++. The key features of this library are as follows:

  • It provides a great number of definitions and lemmas for common data structures such as lists, finite maps, finite sets, and finite multisets.
  • It uses type classes for common notations (like ∅, ∪, and Haskell-style monad notations) so that these can be overloaded for different data structures.
  • It uses type classes to keep track of common properties of types, like it having decidable equality or being countable or finite.
  • Most data structures are represented in canonical ways so that Leibniz equality can be used as much as possible (for example, for maps we have m1 = m2 iff ∀ i, m1 !! i = m2 !! i). On top of that, the library provides setoid instances for most types and operations.
  • It provides various tactics for common tasks, like an ssreflect inspired done tactic for finishing trivial goals, a simple breadth-first solver naive_solver, an equality simplifier simplify_eq, a solver solve_proper for proving compatibility of functions with respect to relations, and a solver set_solver for goals involving set operations.
  • It is entirely dependency- and axiom-free.

History

Coq-std++ has originally been developed by Robbert Krebbers as part of his formalization of the C programming language in his PhD thesis, called CH2O. After that, Coq-std++ has been part of the Iris project, and has continued to be developed by Robbert Krebbers, Ralf Jung, and Jacques Henri-Jourdan.

Prerequisites

This version is known to compile with:

  • Coq 8.5pl3 / 8.6

Building Instructions

Run make to build the full development. Run make install to install the library.