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

_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

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/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/ItHolds.v

@@ -106,6 +106,25 @@ Local Ltac2 wp_assert_by (claim : constr) (label : ident option) (xtr_lemma : co
 Local Ltac2 wp_assert_since (claim : constr) (label : ident option) (xtr_claim : constr) :=
   since_framework (core_wp_assert_by claim label) xtr_claim.
 
+(**
+  Removes a [StateHyp.Wrapper] wrapper from the goal.
+    
+  Arguments: The statement in the specified hypothesis
+    
+  Does: 
+    - Removes the wrapper [StateHyp.Wrapper A G].
+
+  Raises exception:
+    - (fatal) if the wrong hypothesis is specified.
+*)
+Local Ltac2 unwrap_state_hyp (statement : constr) :=
+  lazy_match! goal with
+    | [|- StateHyp.Wrapper ?s _] => 
+         if check_constr_equal s statement
+           then apply (StateHyp.wrap $s)
+           else throw (of_string "Wrong statement specified.")
+    | [|- _] => ()
+  end.
 
 (**
   Attempts to assert a claim and proves it automatically using a specified lemma, 
@@ -141,6 +160,32 @@ Ltac2 Notation "Since" xtr_claim(constr) "it" "holds" "that" claim(constr) label
     - (fatal) if [rwaterprove] fails to prove the claim using the specified lemma.
     - [[label] is already used], if there is already another hypothesis with identifier [label].
 *)
+
+Local Ltac2 wp_assert_with_unwrap (claim : constr) (label : ident option) :=
+  (* Try out label first. 
+    Code results in wrong error if done inside repeated match.. *)
+  match label with | None => () | Some label => try_out_label label end;
+
+  match! goal with
+  | [h : ?s |- StateHyp.Wrapper ?s ?h_spec _] => 
+    let h_constr := Control.hyp h in
+    (* sanity check "h = h_spec" *)
+    if check_constr_equal h_constr h_spec
+      then ()
+      else fail;
+
+    if check_constr_equal s claim
+      then apply (StateHyp.wrap $s)
+      else throw (of_string "Wrong statement specified.");
+    (* rename ident generated in specialize with user-specified label*)
+    match label with
+    | None => ()
+    | Some label => Std.rename [(h, label)]
+    end
+  | [|- _] => 
+    panic_if_goal_wrapped ();
+    wp_assert claim label
+  end.
+
 Ltac2 Notation "It" "holds" "that" claim(constr) label(opt(seq("(", ident, ")")))  :=
-  panic_if_goal_wrapped ();
-  wp_assert claim label.
+  wp_assert_with_unwrap claim label.

theories/Tactics/Specialize.v

@@ -0,0 +1,74 @@
+(******************************************************************************)
+(*                  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 Util.Init.
+Require Import Util.Goals.
+Require Import Util.MessagesToUser.
+
+
+(**
+  Specializes a hypothesis that starts with a for-all statement.
+    
+  Arguments:
+    - [s : ident], name of the variable to choose
+    - [choice : constr], choice for the variable
+    - [in_hyp : ident], name of the hypothesis to specialize.
+
+  Raises fatal exceptions:
+    - If the hypothesis [in_hyp] does not start with a for-all statement.
+*)
+
+Local Ltac2 _ident_to_hyp_list (ls : (ident * constr) list) : (Std.hypothesis * constr) list 
+:= List.map (fun (i, x) => (Std.NamedHyp i, x)) ls.
+
+Local Ltac2 wp_specialize (var_choice_list : (ident * constr) list) (h:constr) :=
+  (* let h := Control.hyp in_hyp in *)
+  (* let named_hyp := Std.NamedHyp s in *)
+  let statement := eval unfold type_of in (type_of $h) in
+  (* let specialized_statement := eval unfold type_of in (type_of ($h $choice)) in *)
+  lazy_match! statement with
+    | _ -> ?x => (* Exclude matching on functions (naming codomain necessary) *)
+      throw (of_string "`Pick ... in (*)` only works if (*) starts with a for-all quantifier.")
+    | forall _ : _, _ =>
+      let w := Fresh.fresh (Fresh.Free.of_goal ()) @_H in
+      Std.specialize (h, Std.ExplicitBindings (_ident_to_hyp_list var_choice_list)) 
+        (Some (Std.IntroNaming (Std.IntroIdentifier w))) ;
+      (* specialize $h with ($named_hyp := $choice) as $w; *)
+      (* Wrap the goal *)
+      let constr_w := Control.hyp w in
+      let type_w := Constr.type constr_w in
+      apply (StateHyp.unwrap $type_w $constr_w)
+    | _ => throw (of_string "`Pick ... in (*)` only works if (*) starts with a for-all quantifier.")
+  end.
+
+(**
+  Specializes a hypothesis that starts with a for-all statement.
+    
+  Arguments:
+    - [s : ident], name of the variable to choose
+    - [choice : constr], choice for the variable
+    - [in_hyp : ident], name of the hypothesis to specialize.
+
+  Raises fatal exceptions:
+    - If the hypothesis [in_hyp] does not start with a for-all statement.
+*)
+Ltac2 Notation "Use" s(list1(seq(ident, ":=", constr), ",")) "in" "(" in_hyp(constr) ")" :=
+  wp_specialize s in_hyp.

theories/Util/Goals.v

@@ -96,6 +96,23 @@ Notation "'Add' 'the' 'following' 'line' 'to' 'the' 'proof:' 'We' 'need' 'to' 's
     format "'[ ' Add  the  following  line  to  the  proof: ']' '//'   We  need  to  show  that  ( G ). '//' or  write: '//'   We  conclude  that  ( G ). '//' if  no  intermediary  proof  steps  are  required."
   ).
 
+Module StateHyp.
+
+  Private Inductive Wrapper (A : Type) (h : A) (G : Type) : Type :=
+    | wrap : G -> Wrapper A h G.
+
+  Definition unwrap (A : Type) (h : A) (G : Type) : Wrapper A h G -> G :=
+    fun x => match x with wrap _ _ _ y => y end.
+
+End StateHyp.
+
+Notation "'Add' 'the' 'following' 'line' 'to' 'the' 'proof:' 'It' 'holds' 'that' '(' A ').'" :=
+  (StateHyp.Wrapper A _ _) (
+    at level 99,
+    only printing,
+    format "'[ ' Add  the  following  line  to  the  proof: ']' '//'   It  holds  that  ( A )."
+  ).
+
 Module ByContradiction.
 
   Private Inductive Wrapper (A G : Type) : Type :=
@@ -147,6 +164,7 @@ Ltac2 panic_if_goal_wrapped () :=
     | [|- NaturalInduction.Base.Wrapper _] => raise_goal_wrapped_error ()
     | [|- NaturalInduction.Step.Wrapper _] => raise_goal_wrapped_error ()
     | [|- StateGoal.Wrapper _]             => raise_goal_wrapped_error ()
+    | [|- StateHyp.Wrapper _ _ _]              => raise_goal_wrapped_error ()
     | [|- ByContradiction.Wrapper _ _]     => raise_goal_wrapped_error ()
     | [|- _] => ()
   end.