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