Merge 8.17 into main (allows for choosing blanks)

_CoqProject.in

@@ -67,6 +67,7 @@ theories/Tactics/Help.v
 theories/Tactics/Induction.v
 theories/Tactics/ItHolds.v
 theories/Tactics/ItSuffices.v
+theories/Tactics/Specialize.v
 theories/Tactics/Take.v
 theories/Tactics/ToShow.v
 theories/Tactics/Unfold.v
@@ -137,6 +138,7 @@ tests/tactics/Either.v
 tests/tactics/Induction.v
 tests/tactics/ItHolds.v
 tests/tactics/ItSuffices.v
+tests/tactics/Specialize.v
 tests/tactics/Take.v
 tests/tactics/ToShow.v
 tests/tactics/Unfold.v

src/databases.mlg

@@ -16,7 +16,7 @@
 (*                                                                            *)
 (******************************************************************************)
 
-DECLARE PLUGIN "coq-waterproof.databases"
+DECLARE PLUGIN "coq-waterproof.plugin"
 
 {
 
@@ -73,4 +73,4 @@ VERNAC COMMAND EXTEND DatabaseQuery CLASSIFIED AS QUERY
       Feedback.msg_notice ((str "Decidability databases :") ++ List.fold_left (fun acc database_name -> acc ++ str " " ++ str database_name) (str "") (get_current_databases Decidability));
       Feedback.msg_notice ((str "Shorten databases :") ++ List.fold_left (fun acc database_name -> acc ++ str " " ++ str database_name) (str "") (get_current_databases Shorten))
     }
-END
+END

tests/libs/Analysis/StrongInductionIndexSequence.v

@@ -57,38 +57,40 @@ Abort.
 
 
 
-(* Test 3:  more complicated example from actual exercises,
-    i.e. with function notation 'n(k)' and 'P(n(k)) = blue' as property. *)
+(* Test 3:  more complicated example inspired by actual exercises,
+    i.e. with function notation 'n(k)' and 'candy_seq(n(k)) = sweet' as property. *)
 Require Import Waterproof.Notations.
 Require Import Waterproof.Automation.
 
 Waterproof Enable Automation RealsAndIntegers.
 Waterproof Enable Automation Intuition.
 
-Inductive Color : Set :=
-| blue : Color
-| orange : Color.
+Inductive Flavor : Set :=
+| sweet : Flavor
+| sour  : Flavor
+| salty : Flavor.
 
-#[local] Parameter P : ℕ → Color.
-Parameter infinitely_many_blues : ∀ k : ℕ, ∃ m : ℕ, (m ≥ k)%nat ∧ P(m) = blue.
 
-Lemma exercise_10_7_6 : 
-  ∃ n : ℕ → ℕ, (is_index_seq n) ∧ (∀ k : ℕ, P (n k) = blue).
+#[local] Parameter candy_seq : ℕ → Flavor.
+Parameter infinitely_many_sweet : ∀ k : ℕ, ∃ m : ℕ, (m ≥ k)%nat ∧ candy_seq(m) = sweet.
+
+Goal
+  ∃ n : ℕ → ℕ, (is_index_seq n) ∧ (∀ k : ℕ, candy_seq (n k) = sweet).
 Proof.
 Define the index sequence n inductively.
-- By (infinitely_many_blues) it holds that
-    (∃ m : ℕ, (m ≥ 0)%nat ∧ P(m) = blue).
+- By (infinitely_many_sweet) it holds that
+    (∃ m : ℕ, (m ≥ 0)%nat ∧ candy_seq(m) = sweet).
   Obtain such an m.
   Choose n_0 := m.
-  We conclude that (P(n_0) = blue).
+  We conclude that (candy_seq(n_0) = sweet).
 - Take k : ℕ and assume n(0),...,n(k) are defined.
-  Assume that (∀ l : ℕ, (l ≤ k)%nat ⇒ P(n(l)) = blue).
+  Assume that (∀ l : ℕ, (l ≤ k)%nat ⇒ candy_seq(n(l)) = sweet).
   Assume that (∀ l : ℕ, (l < k)%nat ⇒ (n(l) < n(l+1))%nat).
-  By (infinitely_many_blues) it holds that 
-    (∃ m : ℕ, (m ≥ (n k) + 1)%nat ∧ P(m) = blue).
+  By (infinitely_many_sweet) it holds that 
+    (∃ m : ℕ, (m ≥ (n k) + 1)%nat ∧ candy_seq(m) = sweet).
   Obtain such an m.
   Choose n_kplus1 := m.
   We show both statements.
-  * We conclude that (P(n_kplus1) = blue).
+  * We conclude that (candy_seq(n_kplus1) = sweet).
   * We conclude that (n(k) < n_kplus1)%nat.
 Qed.

tests/tactics/Choose.v

@@ -59,3 +59,13 @@
     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.

tests/tactics/ItHolds.v

@@ -23,9 +23,9 @@ Require Import Lra.
 
 (* Set Default Timeout 1. *)
 
+Require Import Waterproof.Tactics.
 Require Import Waterproof.Automation.
 Require Import Waterproof.Notations.
-Require Import Waterproof.Tactics.
 Require Import Waterproof.Util.Assertions.
 
 Waterproof Enable Automation RealsAndIntegers.
@@ -306,6 +306,8 @@ Proof.
   By Ha it holds that B.
 Abort.
 
+(* -------------------------------------------------------------------------- *)
+
 (* Test 21: we can use "It holds that" using boolean statements *)
 Goal 1 < 2.
 Proof.
@@ -319,3 +321,63 @@ Proof.
   Since (orb true false) it holds that (1 < 2).
   assumption.
 Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(** Test 23: Test whether wrapper for specialize works *)
+Goal (forall x : nat, x >= 5 -> True) -> True.
+Proof.
+  intro H1.
+  Use x := 6 in (H1).
+  It holds that (6 >= 5 -> True) (i).
+Abort.
+
+(** Test 24: Test wrapper specialize blocks other tactics  *)
+Goal (forall x : nat, x >= 5 -> True) -> True.
+Proof.
+  intro H1.
+  Use x := 6 in (H1).
+  Fail We claim that (False).
+Abort.
+
+(** Test 25: Test wrapper specialize fails with wrong statement *)
+Goal (forall x : nat, x >= 5 -> True) -> True.
+Proof.
+  intro H1.
+  It holds that (3 >= 5 -> True). (* test whether automation could show this*)
+  Use x := 6 in (H1).
+  Fail It holds that (3 >= 5 -> True).
+Abort.
+
+(** Test 26: Test succesful renaming hypothesis from specialize 
+  even if another instance is added inbetween. *)
+Goal (forall x : nat, x >= 5 -> True) -> True.
+Proof.
+  intro H1.
+  Use x := 6 in (H1).
+  assert (6 >= 5 -> True) as decoy by exact (H1 6).
+  It holds that (6 >= 5 -> True) (i).
+  ltac1:(rename i into ii). (* test for hypohtesis without producing output *)
+  Fail Check _H. (* '_H' is auto-generated by 'specialize' tactic *)
+Abort.
+
+(** Test 27: Test fail renaming hypothesis from specialize 
+  if user-specified name is already used. *)
+Goal (forall x : nat, x >= 5 -> True) -> True.
+Proof.
+  intro H1.
+  Use x := 6 in (H1).
+  Fail It holds that (6 >= 5 -> True) (H1).
+Abort.
+
+
+(* TODO (cf. test below): wrong statement error should have priority over wrong label. *)
+
+(** Test 28: Test fail renaming hypothesis from specialize 
+  if wrong statement user-specified name is already used. *)
+Goal (forall x : nat, x >= 5 -> True) -> True.
+Proof.
+  intro H1.
+  Use x := 6 in (H1).
+  Fail It holds that (6 >= 5 -> True) (H1).
+Abort.

tests/tactics/Specialize.v

@@ -0,0 +1,98 @@
+(******************************************************************************)
+(*                  This file is part of Waterproof-lib.                      *)
+(*                                                                            *)
+(*   Waterproof-lib is free software: you can redistribute it and/or modify   *)
+(*    it under the terms of the GNU General Public License as published by    *)
+(*     the Free Software Foundation, either version 3 of the License, or      *)
+(*                    (at your option) any later version.                     *)
+(*                                                                            *)
+(*     Waterproof-lib is distributed in the hope that it will be useful,      *)
+(*      but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*       MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the         *)
+(*               GNU General Public License for more details.                 *)
+(*                                                                            *)
+(*     You should have received a copy of the GNU General Public License      *)
+(*   along with Waterproof-lib. If not, see <https://www.gnu.org/licenses/>.  *)
+(*                                                                            *)
+(******************************************************************************)
+
+Require Import Ltac2.Ltac2.
+Require Import Ltac2.Message.
+
+Require Import Waterproof.Tactics.
+Require Import Waterproof.Automation.
+
+(** Test 0: This should be the expected behavior. *)
+Goal (forall n : nat, n = n) -> True.
+Proof.
+intro H.
+Use n := 3 in (H).
+It holds that (3 = 3).
+Abort.
+
+(** Test 1: This should fail as the wrong variable name is chosen. *)
+Goal (forall n : nat, n = n) -> True.
+Proof.
+intro H.
+Fail Use m := (3) in (H).
+Abort.
+
+(** Test 2: This should fail because the wrong goal is specified. *)
+Goal (forall n : nat, n = n) -> True.
+Proof.
+intro H.
+Use n := (3) in (H).
+Fail It holds that (True).
+Abort.
+
+(** Test 3: This should fail because first the wrapper needs to be resolved. *)
+Goal (forall n : nat, n = n) -> True.
+Proof.
+intro H.
+Use n := (3) in (H).
+Fail exact I.
+Abort.
+
+(** It should be possible to use an outside lemma *)
+Local Parameter F : nat -> nat.
+Local Parameter F_identity : forall n : nat, F n = n.
+
+Goal True.
+Proof.
+Fail It holds that (F 3 = 3).
+Use n := (5) in (F_identity).
+It holds that (F 5 = 5).
+Abort.
+
+(** Test 4: cannot use specialize tactic for function, 
+  throw readable error message stating as much.  *)
+Definition f : nat -> nat := fun (n : nat) => n.
+Goal False.
+Proof.
+  Fail Use n := 5 in (f).
+Abort.
+
+(** Test 5: original universal quantifier hypohtesis left unchanged. *)
+Goal (forall n : nat, n = n) -> True.
+Proof.
+intro H.
+Use n := 3 in (H).
+ltac1:(rename H into HH).   (* test for hypohtesis without producing output *)
+Abort.
+
+(** Test 6: multiple variable specifications  *)
+Goal (forall n m : nat, n = m) -> False.
+Proof.
+intro H.
+Use n := 3, m := 4 in (H).
+It holds that (3 = 4).
+Abort.
+
+(** Test 7: multiple variable specifications, different order  *)
+Goal (forall n m : nat, n = m) -> False.
+Proof.
+intro H.
+Use m := 4, n := 3 in (H).
+Fail It holds that (4 = 3). (* as expected :) *)
+It holds that (3 = 4).
+Abort.

theories/Automation/Framework.v

@@ -17,4 +17,4 @@
 (******************************************************************************)
 
 From Ltac2 Require Import Init.
-Declare ML Module "waterproof:coq-waterproof.databases".
+Declare ML Module "waterproof:coq-waterproof.plugin".

theories/Tactics.v

@@ -33,6 +33,7 @@ Require Export Tactics.Help.
 Require Export Tactics.Induction.
 Require Export Tactics.ItHolds.
 Require Export Tactics.ItSuffices.
+Require Export Tactics.Specialize.
 Require Export Tactics.Take.
 Require Export Tactics.ToShow.
 Require Export Tactics.Unfold.

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