package coq-waterproof
Coq proofs in a style that resembles non-mechanized mathematical proofs
Install
Dune Dependency
Authors
Maintainers
Sources
2.2.0+8.17.tar.gz
md5=cd4867e94e20eba727bd6deea06130cd
sha512=1205227101bb30f3e8c4ec05217920dcda1e3631ecd0428f2ac820c9a2811f91526d68623aaf01dd9aa1e81e8adfc083af01152d7f7a6e48894caa829bc3f440
doc/coq-waterproof.plugin/Waterproof/Waterprove/index.html
Module Waterproof.WaterproveSource
Source
val waterprove :
int ->
?shield:bool ->
Tactypes.delayed_open_constr list ->
Hint_dataset_declarations.database_type ->
unit Proofview.tacticWaterprove
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 searchshield(bool): if set totrue, will stop the proof search if a forbidden pattern is foundlems(Tactypes.delayed_open_constr list): additional lemmas that are given to solve the proofdatabase_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.tacticRestricted 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.
Arguments:
depth(int): max depth of the proof searchshield(bool): if set totrue, will stop the proof search if a forbidden pattern is foundlems(Tactypes.delayed_open_constr list): additional lemmas that are given to solve the proofdatabase_type(Hint_dataset_declarations): type of databases that will be use as hint databasesmust_use(string list): list of hints that have to be used during the automatic solvingforbidden(string list): list of hints that must not be used during the automatic solving