package coq-waterproof
Coq proofs in a style that resembles non-mechanized mathematical proofs
Install
Dune Dependency
Authors
Maintainers
Sources
2.1.1+8.17.tar.gz
md5=246900c584d34deb5a4ed74e74c3aeab
sha512=f5242890a140c6966bd76e1d487a8ca139c14874eb0c1a589f28b72773be24f11f07bb1b163153c5811330a28a91a94d508233dc19849baa671fada857f05a3b
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