Merge 8.17 into main (allows for choosing blanks) #65
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Adapt to coq/coq#17836 (sort poly)
Revert "Adapt to coq/coq#17836 (sort poly)"
Adapt to coq/coq#18174 (Clenv.unify takes cv_pb)
* [build] Initial port to Dune This was done at the interest of Vincent WENDLING for jsCoq use. The setup is fairly standard, other than excluding the deprecated dir (which doesn't compile) * Update README.md * Update dune file in theories * Change importing Ltac2 modules and build only with dune * Update version numbers * Restore changes file and rename license file * Fix metadata in files * Add template tags * Add @install, minimal dune version, dev-repo to opam file * Added infrastructure for enforcing users to mention use of definitions. * Removed some unnecessary lemma's and corresponding tactics (that were apparently throwing errors anyway). * Restored old lemmas in 'SupAndInf' necessary for keeping limsup file working. To be rewritten in future. * Moved tests in SupAndInf.v file to separate test file. Small bug fix in rewrite rule sup and infimum. * 'We need to show'-tactic now also accepts equivalent goals. Added 'By ...' clause to allow for an additional lemma from which equivalence follows. * Replaced use of 'it suffices to show' by 'we need to show' for unfolding definitions. * Added testcases new behaviour tactic. * Improved feedback given new restricted proof automation. * Updated documentation. * Small change in error message. * Moved 'AutomationFailure' exception type to 'Wateprove' file. * Improved feedback 'ItHolds' for new restricted proof automation. * Replaced custom error shielded goal by standard error that can be caught using Ltac2. * Added 'Since ...' clause as alternative to 'By ...' that accepts statements instead of references. (No 'Since ... we need to show ...' because the 'By'-version is to be removed soon. ) * Removed acceptation equivalent goals from 'We need to show' tactic. * Improved feedback 'By ... we conclude ...' for new restricted automated proof finding. Added 'Since ... we conclude that ...' alternative. * Improved feedback, now it says which part of a chain of (in)equalities it failed to prove. Refactored checking whether additional lemma is actually used: now check is done in 'Waterprove.v', it throws errors with relevant information that other tactics use to display user-readable errors. * 'Contradiction' now tries to find a contradiction to the previous statement. * Moved 'Obtain' tactic to separate file. * Simplified old notation 'Obtain' tactic. Now it automatically tries to destruct previous statement and users no longer need to specify the corresponding property. * Simplified names for hypotheses not labeled by user. * Added 'change' to 'Expand definition', so putting in different dummy variables actually has effect. * Added StateGoal wrappers to subgoals of non-natural induction. * Added workaround for unexpected anomalies in restricted automation. * Strengthened workaround. Both to prevent more anomalies with hypotheses and to prevent endless searching for proof with hypothesis because it is used implicitly by the 'assumption' tactic. * Replaced axiomatic definitions with locked ones. Also strengthened shielded automation to depth 3 to be able to use definition supremum.. * Fixed dune build. * feat: add warnings * refactor: change the names of the warning functions * feat: add error function * Add files to _CoqProject.in * feat: use the warning in Conclusion.v * feat: deal with Rabs Rmax Rmin more easily by destructing them * Readded shortened 'Obtain accoriding to ...' tactic. * Reworked shielding to use Shorten database type. Includes new tactics for explicitly unfolding definitions, optimized for speed automation (i.e. they explicitly fail to prevent large growth search tree). * Improved expanding def for sup and inf. * Implemented user-level error throwing in tactics. * Fixed small error from merge. * Disabled debug mode automation. * Reverted back to old SupAndInf.v file. * Replaced wrapping after 'Expand the definition of ...' by throwing errors suggesting user to replace the line by a tactic with a similar effect as unfolding the definitions. (Also slightly simplified notation base case natural induction.) * Added tactic for unfolding that prints a message instead of throwing an errror. For internal use by Waterproof editor only. * chore: bump version number * fix: add internal unfold for general terms and tests for internal unfold * Hint fixes (#30) fix: change hint priorities * Automation debug (#31) * fix: change hint priorities * fix: change hint priorities * fix: fight line endings * feat: add switch for debugging of the automation * feat: Add description on how to enable debugging to readme * feat: use N1 instead of N in definition convergence * Improve either (#32) * fix: definition of divergence to infinity and min infinity * feat: add double_is_even to wp_integers rather than subsequences * feat: let either work with uninformative or if the goal is a prop * feat: also separate either code for prop for three statements. Refactor some decidability statements * refactor: use new either code in alternative characterization of continuity in R * feat: add alternative characterization continuity for natural numbers as subset of metric space of reals * feat: some adaptations for the continuity exercises * chore: update changelog and bump version number in opam file * Tactics for using strong induction to define index sequence (#33) * Added strong induction for defining index sequence. Warning: uses fixed letters 'n' and 'k' for index sequence and induction variable. * Removed 'Check' and 'Print's. * Removed old code. * Show version number (#34) * feat: Add tactic to show version number * fix: Add version file to _CoqProject.in * Allow testing against a folder with dune's runtest and set version number (#35) * feat: add exercises as dune test * feat: add python script for testing * feat: abstract the testing scripts and deal with errors better * fix: call the correct test script * Set Help to use default automation system. (#36) * Change required version number * Try to fix coq requirement * Fix for problems with strong induction for defining index sequence. (#38) * Fix for problems with strong induction for defining subsequence. * Updated formatting goal wrapper. * fix: some small fixes to be compatible with dev * fix: change order fold_right arguments in index sequence * fix: Small changes to the sequences and subsequences files because autorewrite no longer seems to work as before * chore: Change version number * try to allow for dev version * fix: try with version numbers * fix: try to fix version numbers * fix: Remove unnecessary import in Sequences.v * feat: add logging sentence for wp_autorewrite * feat: add logging sentence for wp_autorewrite (#43) * feat: create option to print rewrite hints (#44) * fix: Fix autorewrite (the env variable didn't come through properly) * fix: Compatibility with compilers >= 4.09.0 (#45) * fix: Exclude s390x architecture * refactor: put *.install and *.diags in gitignore --------- Co-authored-by: Emilio Jesus Gallego Arias Co-authored-by: Jelle
Update installation instructions
Implement a better way to do a case analyse on a type Co-authored-by: DikieDick
Note that both lines where loading the same plugin, but activating different syntax rules; that's not really allowed as it leaves the system in a partial state. If something like that is needed, true two plugins are necessary (Which is not hard to support nowadays).
* Merge 8.17 into main (#61) Main change according to (PR #58): we only declare one plugin now. * Renamed variables to prevent having actual exercise solution in repo (#64) * Specialize (#51) * feat: first version of waterproof specialize tactic * feat: Improve new specialize tactic, so it throws an error when a wrong variable is getting introduced. * Avoid doubling hypothesis, allow for multiple binders, prevent matching on functions, rename hypothesis to user-specified one --------- Co-authored-by: Jelle <jellewemmenhove@live.nl> * feat: Postponing choices in the Choose tactic * No longer rename variables in exists-statements --------- Co-authored-by: Jelle <jellewemmenhove@live.nl>
jim-portegies
changed the title
jellooo038
approved these changes
Aug 20, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Allows for
and
allowing the user to come back to these choices later.