package coq-waterproof

You can search for identifiers within the package.

in-package search v0.2.0

Coq proofs in a style that resembles non-mechanized mathematical proofs

Install

dune-project

Dependency

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

Authors

Maintainers

J

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

Sources

2.0.1+8.17.tar.gz

md5=a891f29ee1723d8031d4cb50903da735

sha512=cfc7a8010b71ab45264f396b144f0cf887baf9ddae9df1e92d977252801197017225af0d4bbabaf7a0b57454aa2ce68989c58ce6c1707b4bc40674488bf0a622

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

Module `Waterproof.Waterprove`Source

Sourceval automation_shield : bool ref

Is automation shield enabled ?

Source

val waterprove : 
  int ->
  ?shield:bool ->
  Tactypes.delayed_open_constr list ->
  Hint_dataset_declarations.database_type ->
  unit Proofview.tactic

Waterprove

This function is the main automatic solver of coq-waterproof.

The databases used for the proof search are the one declared in the current imported dataset (see Hint_dataset.loaded_hint_dataset).

The forbidden patterns are defined in is_forbidden.

Arguments:

depth (int): max depth of the proof search
shield (bool): if set to true, will stop the proof search if a forbidden pattern is found
lems (Tactypes.delayed_open_constr list): additional lemmas that are given to solve the proof
database_type (Hint_dataset_declarations): type of databases that will be use as hint databases

Source

val rwaterprove : 
  int ->
  ?shield:bool ->
  Tactypes.delayed_open_constr list ->
  Hint_dataset_declarations.database_type ->
  Evd.econstr list ->
  Evd.econstr list ->
  unit Proofview.tactic

Restricted Waterprove

This function is similar to waterprove but use wp_auto.rwp_auto and wp_eauto.rwp_eauto instead of wp_auto.wp_auto and wp_eauto.wp_eauto.