package coq-waterproof

  1. Overview
  2. Docs
Coq proofs in a style that resembles non-mechanized mathematical proofs

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (3)

Authors

  1. J
    Jelle Wemmenhove
  2. P
    Pim Otte
  3. B
    Balthazar Pathiachvili
  4. D
    Dick Arends
  5. C
    Cosmin Manea
  6. L
    Lulof Pirée
  7. A
    Adrian Vrămuleţ
  8. T
    Tudor Voicu
  9. J
    Jim Portegies <j.w.portegies@tue.nl>

Maintainers

  1. J
    Jim Portegies <j.w.portegies@tue.nl>

Sources

3.1.0+9.1.tar.gz
md5=83359b33c0c6e1fb87f938280cd4e0a2
sha512=d0b0d674e9b5c731b54779d9b77b61f6142d561b05e8c06f2afd0a62e507afedd7696754d29c31522fee996a1f6c6a5d158b250ab04fd9dd5bd812bb99d3a97f

doc/coq-waterproof.plugin/Waterproof/Wp_eauto/index.html

Module Waterproof.Wp_eautoSource

Sourceval esearch : bool -> int -> Tactypes.delayed_open_constr list -> Hints.hint_db list -> Pp.t list -> Pp.t list -> Backtracking.trace Proofview.tactic

Searches a sequence of at most n tactics within db_list and lems that solves the goal

The goal can contain evars

Sourceval wp_eauto : bool -> int -> Tactypes.delayed_open_constr list -> string list -> Backtracking.trace Proofview.tactic

Waterproof eauto

This function is a rewrite around Eauto.eauto with the same arguments to be able to retrieve which hints have been used in case of success.

The code structure has been rearranged to match the one of wp_auto.wp_auto.

Sourceval rwp_eauto : bool -> int -> Tactypes.delayed_open_constr list -> Hints.hint_db_name list -> Pp.t list -> Pp.t list -> Backtracking.trace Proofview.tactic

Restricted Waterproof eauto

This function acts the same as wp_auto but will fail if all proof found contain at least one must-use lemma that is unused or one hint that is in the forbidden list.