Merge 8.17 into main (allows for choosing blanks) (impermeable#65)

* Changes for compatibility with 8.19

* Adapt files for the build process

* Update README.md

* Don't use opam to build and install for now

* Adapt dune files to make build with dune possible

* Change name field in dune file to Waterproof

* Revert to dune language 3.6

* Remove line on theory Ltac2

* 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)

* Adapt to coq/coq#17836 (sort poly) (impermeable#28)

* Adapt to coq/coq#18280 (case relevance outside case info) (impermeable#37)

* Merge features of version 2.1.1 into coq-master (impermeable#46)

* [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 (impermeable#30)

fix: change hint priorities

* Automation debug (impermeable#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 (impermeable#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 (impermeable#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 (impermeable#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 (impermeable#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. (impermeable#36)

* Change required version number

* Try to fix coq requirement

* Fix for problems with strong induction for defining index sequence. (impermeable#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 (impermeable#43)

* feat: create option to print rewrite hints (impermeable#44)

* fix: Fix autorewrite (the env variable didn't come through properly)

* fix: Compatibility with compilers >= 4.09.0 (impermeable#45)

* fix: Exclude s390x architecture

* refactor: put *.install and *.diags in gitignore

---------

Co-authored-by: Emilio Jesus Gallego Arias
Co-authored-by: Jelle

* Adapt to coq/coq#18327 (projection opacity) (impermeable#41)

* Adapt to coq/coq#18529 (no Dyn.anonymous) (impermeable#47)

* Adapt to coq/coq#18624 (Tac2ffi / Tac2val split) (impermeable#49)

* Adapt to coq/coq#18546. (impermeable#48)

* Adapt to coq/coq#18880 (impermeable#52)

* Adapt to coq/coq#18938 (EConstr.ERelevance) (impermeable#53)

* Update README.md

Update installation instructions

* Testmaster (impermeable#54)

Implement a better way to do a case analyse on a type

Co-authored-by: DikieDick

* fix: Change 'Variable' to 'local Parameter'

* feat: add a test for awp_autorewrite from coq-master

* Refactor: incorporate some changes from 8.17 and update version numbers (impermeable#57)

* [build] Fix use of plugin aliases in findlib loading. (impermeable#58)

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).

* feat: Postponing choices in the Choose tactic (impermeable#59)

* Merge 8.17 into main (impermeable#61)

Main change according to (PR impermeable#58): we only declare one plugin now.

* Renamed variables to prevent having  actual exercise solution in repo (impermeable#64)

* Specialize (impermeable#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 <[email protected]>

* feat: Postponing choices in the Choose tactic

* No longer rename variables in exists-statements

---------

Co-authored-by: Jelle <[email protected]>

---------

Co-authored-by: Gaëtan Gilbert <[email protected]>
Co-authored-by: Rodolphe Lepigre <[email protected]>
Co-authored-by: Pierre Roux <[email protected]>
Co-authored-by: Emilio Jesús Gallego Arias <[email protected]>
Co-authored-by: Jelle <[email protected]>

tests/tactics/Choose.v

@@ -59,3 +59,13 @@ Goal forall n : nat, ( ( (n = n) \/ (n + 1 = n + 1) ) -> (n + 1 = n + 1)).
     intro n.
     Fail Choose m := n.
 Abort.
+
+(** Test 5: Choose a blank *)
+Goal exists n : nat, n + 1 = n + 1.
+    Choose n := (_).
+Abort.
+
+(** Test 6: Choose a named evar *)
+Goal exists n : nat, n + 1 = n + 1.
+    Choose n := (?[m]).
+Abort.

theories/Tactics/Choose.v

@@ -22,6 +22,9 @@ Require Import Ltac2.Message.
 Require Import Util.Goals.
 Require Import Util.MessagesToUser.
 
+Local Ltac2 concat_list (ls : message list) : message :=
+  List.fold_right concat (of_string "") ls.
+
 (* Ltac2 Type exn ::= [ ChooseError(string) ]. *)
 
 
@@ -44,9 +47,13 @@ Require Import Util.MessagesToUser.
 Ltac2 choose_variable_in_exists_goal_with_renaming (s:ident) (t:constr) :=
   lazy_match! goal with
     | [ |- exists _ : _, _] =>
-      pose ($s := $t);
+      set ($s := $t);
       let v := Control.hyp s in
       let w := Fresh.fresh (Fresh.Free.of_goal ()) @_defeq in
+      match Constr.has_evar t with
+      |  true => warn (concat_list [of_string "Please come back to this line later to make a definite choice for "; of_ident s; of_string "."])
+      | _ => ()
+      end;
       exists $v;
       assert ($w : $v = $t) by reflexivity
     | [ |- _ ] => throw (of_string "`Choose` can only be applied to 'exists' goals.")
@@ -68,14 +75,17 @@ Ltac2 choose_variable_in_exists_goal_with_renaming (s:ident) (t:constr) :=
 *)
 Ltac2 choose_variable_in_exists_no_renaming (t:constr) :=
     lazy_match! goal with
-        | [ |- exists _ : _, _] => exists $t
+        | [ |- exists _ : _, _] =>
+          match Constr.has_evar t with
+          |  true => warn (concat_list [of_string "Please come back to this line later to make a definite choice."]); eexists $t
+          |  false => exists $t
+          end
         | [ |- _ ] => throw (of_string "`Choose` can only be applied to 'exists' goals.")
     end.
 
-Ltac2 Notation "Choose" s(opt(seq(ident, ":="))) t(constr) :=
+Ltac2 Notation "Choose" s(opt(seq(ident, ":="))) t(open_constr) :=
   panic_if_goal_wrapped ();
   match s with 
     | None => choose_variable_in_exists_no_renaming t
     | Some s => choose_variable_in_exists_goal_with_renaming s t
   end.
-