package coq-waterproof
Coq proofs in a style that resembles non-mechanized mathematical proofs
Install
Dune Dependency
Authors
Maintainers
Sources
2.2.0+8.20.tar.gz
md5=18c6dafc6fb018f167f89fb236ff494b
sha512=096ebe52912ebe3fb063a5ce88bee1dfc8f63226f7f1284a4304a079751b98c617a4fcafa9781c3e54e024e631c87248885b56efc20086c98ae0e525cfe08efb
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