Merge branch 'main' into feat/expand-definition-2

Author: jim-portegies

src/g_waterproof.mlg

@@ -72,21 +72,10 @@ let () = add_scope "open_lconstr" (fun arg ->
 (* Doing this enables parsing the mathematical expressions without parentheses *)
 (* The cost of this is that these words are no longer allowed to be variables *)
 {
-let () = Procq.set_keyword_state (
-    (CLexer.add_keyword (
-    (CLexer.add_keyword (
-    (CLexer.add_keyword (
-    (CLexer.add_keyword (
-    (CLexer.add_keyword (
-    (CLexer.add_keyword (
-    CLexer.add_keyword (Procq.get_keyword_state()) "and"
-    ) "as")
-    ) "hold")
-    ) "holds")
-    ) "it")
-    ) "or")
-    ) "we")
-    )
+let () = Mltop.add_init_function "coq-waterproof.plugin" @@ fun () ->
+    Procq.set_keyword_state
+      (List.fold_left CLexer.add_keyword (Procq.get_keyword_state())
+      ["and"; "as"; "hold"; "holds"; "it"; "or"; "we"; "that"])
 }
 VERNAC COMMAND EXTEND AutomationShieldEnableSideEff CLASSIFIED AS SIDEFF
   | [ "Waterproof" "Enable" "Automation" "Shield" ] ->

src/waterprove.ml

@@ -27,12 +27,12 @@ open Wp_eauto
 open Wp_rewrite
 
 (**
-  Is automation shield enabled ? 
+  Is automation shield enabled ?
 *)
 let automation_shield: bool ref = Summary.ref ~name:"automation_shield" true
 
 (**
-  Do we want to debug the automation ?   
+  Do we want to debug the automation ?
 *)
 let automation_debug : bool ref = Summary.ref ~name:"automation_debug" false
 
@@ -76,15 +76,17 @@ let restricted_automation_routine (depth: int) (lems: Tactypes.delayed_open_cons
     - [depth] ([int]): max depth of the proof search
     - [shield] ([bool]): if set to [true], will stop the proof search if a forbidden pattern is found
     - [lems] ([Tactypes.delayed_open_constr list]): additional lemmas that are given to solve the proof
+    - [dbs] ([hint_db_name list]): list of additional hint databases to use
     - [database_type] ([Hint_dataset_declarations]): type of databases that will be use as hint databases
 *)
-let waterprove (depth: int) ?(shield: bool = false) (lems: Tactypes.delayed_open_constr list) (database_type: database_type): unit tactic =
+let waterprove (depth: int) ?(shield: bool = false) (lems: Tactypes.delayed_open_constr list)
+  (dbs: hint_db_name list) (database_type: database_type): unit tactic =
   Proofview.Goal.enter @@ fun goal ->
     begin
-      if shield && !automation_shield then 
-        automation_routine 3 lems (get_current_databases Shorten)
+      if shield && !automation_shield then
+        automation_routine 3 lems (dbs @ (get_current_databases Shorten))
       else
-        automation_routine depth lems (get_current_databases database_type)
+        automation_routine depth lems (dbs @ get_current_databases database_type)
     end
 
 (**
@@ -96,19 +98,21 @@ let waterprove (depth: int) ?(shield: bool = false) (lems: Tactypes.delayed_open
     - [depth] ([int]): max depth of the proof search
     - [shield] ([bool]): if set to [true], will stop the proof search if a forbidden pattern is found
     - [lems] ([Tactypes.delayed_open_constr list]): additional lemmas that are given to solve the proof
+    - [dbs] ([hint_db_name list]): list of additional hint databases to use
     - [database_type] ([Hint_dataset_declarations]): type of databases that will be use as hint databases
     - [must_use] ([string list]): list of hints that have to be used during the automatic solving
     - [forbidden] ([string list]): list of hints that must not be used during the automatic solving
 *)
-let rwaterprove (depth: int) ?(shield: bool = false) (lems: Tactypes.delayed_open_constr list) (database_type: database_type) (must_use: constr list) (forbidden: constr list): unit tactic =
+let rwaterprove (depth: int) ?(shield: bool = false) (lems: Tactypes.delayed_open_constr list)
+  (dbs : hint_db_name list) (database_type: database_type) (must_use: constr list) (forbidden: constr list): unit tactic =
   Proofview.Goal.enter @@ fun goal ->
     begin
       let env = Proofview.Goal.env goal in
       let sigma = Proofview.Goal.sigma goal in
       let must_use_tactics = List.map (Printer.pr_econstr_env env sigma) must_use in
       let forbidden_tactics = List.map (Printer.pr_econstr_env env sigma) forbidden in
       if shield && !automation_shield then
-        restricted_automation_routine 3 lems (get_current_databases Shorten) must_use_tactics forbidden_tactics
+        restricted_automation_routine 3 lems (dbs @ (get_current_databases Shorten)) must_use_tactics forbidden_tactics
       else
-        restricted_automation_routine depth lems (get_current_databases database_type) must_use_tactics forbidden_tactics
+        restricted_automation_routine depth lems (dbs @ (get_current_databases database_type)) must_use_tactics forbidden_tactics
       end

src/waterprove.mli

@@ -17,12 +17,12 @@
 (******************************************************************************)
 
 (**
-  Is automation shield enabled ? 
+  Is automation shield enabled ?
 *)
 val automation_shield : bool ref
 
 (**
-  Do we want to debug the automation ?   
+  Do we want to debug the automation ?
 *)
 val automation_debug : bool ref
 
@@ -44,12 +44,14 @@ val print_rewrite_hints: bool ref
     - [depth] ([int]): max depth of the proof search
     - [shield] ([bool]): if set to [true], will stop the proof search if a forbidden pattern is found
     - [lems] ([Tactypes.delayed_open_constr list]): additional lemmas that are given to solve the proof
+    - [dbs] ([hint_db_name list]): list of additional hint databases to use
     - [database_type] ([Hint_dataset_declarations]): type of databases that will be use as hint databases
 *)
 val waterprove :
   int ->
   ?shield:bool ->
   Tactypes.delayed_open_constr list ->
+  Hints.hint_db_name list ->
   Hint_dataset_declarations.database_type ->
   unit Proofview.tactic
 
@@ -62,6 +64,7 @@ val waterprove :
     - [depth] ([int]): max depth of the proof search
     - [shield] ([bool]): if set to [true], will stop the proof search if a forbidden pattern is found
     - [lems] ([Tactypes.delayed_open_constr list]): additional lemmas that are given to solve the proof
+    - [dbs] ([hint_db_name list]): list of additional hint databases to use
     - [database_type] ([Hint_dataset_declarations]): type of databases that will be use as hint databases
     - [must_use] ([string list]): list of hints that have to be used during the automatic solving
     - [forbidden] ([string list]): list of hints that must not be used during the automatic solving
@@ -70,6 +73,7 @@ val rwaterprove :
   int ->
   ?shield:bool ->
   Tactypes.delayed_open_constr list ->
+  Hints.hint_db_name list ->
   Hint_dataset_declarations.database_type ->
   Evd.econstr list ->
   Evd.econstr list ->

src/wp_ffi.ml

@@ -121,26 +121,28 @@ let feedback_level = make_repr of_feedback_level to_feedback_level
 
 (* Exports {! Waterprove.waterprove} to Ltac2 *)
 let () =
-  define "waterprove" (int @-> bool @-> (list (thunk constr)) @-> database_type @-> tac unit) @@
-    fun depth shield lems database_type ->
+  define "waterprove" (int @-> bool @-> (list (thunk constr)) @-> list string @-> database_type @-> tac unit) @@
+    fun depth shield lems dbs database_type ->
       begin
         waterprove
           depth
           ~shield
           (List.map (fun lem -> delayed_of_thunk constr lem) lems)
+          dbs
           database_type
       end
 
 (* Exports {! Waterprove.rwaterprove} to Ltac2 *)
 let () =
-  define "rwaterprove" (int @-> bool @-> (list (thunk constr))
+  define "rwaterprove" (int @-> bool @-> (list (thunk constr)) @-> list string
       @-> database_type @-> list constr @-> list constr @-> tac unit) @@
-    fun depth shield lems database_type must_use forbidden ->
+    fun depth shield lems dbs database_type must_use forbidden ->
       begin
         rwaterprove
           depth
           ~shield
           (List.map (fun lem -> delayed_of_thunk constr lem) lems)
+          dbs
           database_type
           must_use
           forbidden

tests/automation/Chains.v

@@ -57,26 +57,26 @@ Abort.
 Goal P -> (& a = b = b = b = b = b).
 Proof.
   intro H.
-  rwaterprove 5 true Main constr:(h).
+  rwaterprove 5 true Main [constr:(h)] [].
 Abort.
 
 (* Test 5: extra lemma has to be used in last equality. *)
 Goal P -> (& b = b = b = b = b = a).
 Proof.
   intro H.
-  rwaterprove 5 true Main constr:(h).
+  rwaterprove 5 true Main [constr:(h)] [].
 Abort.
 
 (* Test 6: extra lemma has to be used in 2nd and 2nd-to-last equality. *)
 Goal P -> (& b = b = a = b = b = a = a).
 Proof.
   intro H.
-  rwaterprove 5 true Main constr:(h).
+  rwaterprove 5 true Main [constr:(h)] [].
 Abort.
 
 (* Test 7: Fails if extra lemma is never used. *)
 Goal P -> (P -> b = c) -> (& b = b = c = b = b = c = c).
 Proof.
   intros H1 H2.
-  Fail rwaterprove 5 true Main constr:(h).
+  Fail rwaterprove 5 true Main [constr:(h)] [].
 Abort.

tests/tactics/Conclusion.v

@@ -141,7 +141,7 @@ Proof.
     reflexivity.
     assert_fails_with_string
     (fun () => By test_by_we_conclude_1 we conclude that (1 < 2))
-"Could not verify this follows from test_by_we_conclude_1.".
+"Could not verify this follows from the provided reasons.".
 Abort.
 
 (** Additional tests 'By ...' clause.  *)
@@ -307,3 +307,73 @@ Proof.
   It holds that (true).
   Since true we conclude that true.
 Qed.
+
+(** Test 11: Test concluding from multiple reasons.
+*)
+
+Local Parameter P Q R T : Prop.
+Local Parameter HP : P.
+Local Parameter HPQ : P -> Q.
+Local Parameter HQR : Q -> R.
+Local Parameter HRT : R -> T.
+
+Local Parameter U V : Prop.
+Local Parameter HUV : U -> V.
+Local Parameter HVP : V -> P.
+
+Local Create HintDb my_reason.
+From Stdlib Require Import String.
+
+Goal T.
+By HP, HPQ, HQR and HRT we conclude that T.
+Qed.
+
+(** Test 12: Conclude from multiple reasons, one of them is also a local hypothesis. *)
+
+Goal P -> T.
+intro H.
+By HP, HPQ, HQR and HRT we conclude that T.
+Qed.
+
+(** Test 13: Conclude from multiple reasons, one of
+  them is a local hypothesis, using the local hypothesis. *)
+Goal P -> T.
+intro H.
+By H, HPQ, HQR and HRT we conclude that T.
+Qed.
+
+(** Test 14: Conclude using an extra database. *)
+Notation "'my' 'reason'" := "my_reason"%string.
+Hint Resolve HUV : my_reason.
+
+Notation "'my' 'other' 'reason'" := "my_other_reason"%string.
+Hint Resolve HVP : my_other_reason.
+
+Goal U -> V.
+intro H.
+By my reason we conclude that V.
+Qed.
+
+(** Test 15: Use two extra databases.*)
+
+Goal U -> P.
+intro H.
+By my reason and my other reason we conclude that P.
+Qed.
+
+(** Test 16: Use two extra databases and extra lemmas. *)
+
+Goal U -> R.
+intro H.
+By my reason, my other reason, HPQ and HQR we conclude that R.
+Qed.
+
+(** Test 17: Fail when a reason is given that is not
+  used. *)
+
+Goal U -> R.
+intro H.
+assert_fails_with_string
+  (fun () => By my reason, my other reason, HPQ, HQR and HRT we conclude that R)
+  "Could not verify this follows from the provided reasons.".
+Abort.

tests/tactics/Help.v

@@ -24,6 +24,7 @@ Require Import Waterproof.Tactics.Help.
 Require Import Waterproof.Util.MessagesToUser.
 Require Import Waterproof.Util.Assertions.
 Require Import Waterproof.Notations.Sets.
+Require Import Waterproof.Tactics.By.
 Open Scope subset_scope.
 
 Waterproof Enable Hypothesis Help.

tests/tactics/ItHolds.v

@@ -401,3 +401,69 @@ Proof.
   Use x := 6 in (H1).
   Fail It holds that (6 >= 5 -> True) as (H1).
 Abort.
+
+(** Test 29: Use multiple hypotheses,
+  hypothesis of same type already in local context *)
+
+Local Parameter a b c : Prop.
+Local Parameter Ha : a.
+Local Parameter Hab : a -> b.
+Local Parameter Hbc : b -> c.
+
+Goal a -> b.
+Proof.
+intro H.
+By Ha, Hab and Hbc it holds that c.
+Abort.
+
+(** Test 30: Use multiple hypothesis,
+  use one hypothesis from context *)
+
+Goal a -> b.
+Proof.
+intro H.
+By H, Hab and Hbc it holds that c.
+Abort.
+
+Waterproof Enable Redirect Errors.
+Waterproof Enable Logging.
+
+(** Test 31: Multiple hypotheses, mention hypothesis that is not useful *)
+
+Goal a -> b.
+Proof.
+assert_fails_with_string (fun () => By Ha, Hab and Hbc it holds that b)
+"Could not verify this follows from the provided reasons.".
+Abort.
+
+Local Parameter d : Prop.
+Local Parameter Hd : d.
+
+Local Create HintDb my_reason.
+From Stdlib Require Import String.
+
+Notation "'my' 'reason'" := "my_reason"%string.
+Hint Resolve Hd : my_reason.
+
+(** Test 32: Use extra database *)
+
+Goal a -> b.
+Proof.
+assert_fails_with_string
+  (fun () =>It holds that d)
+  "Could not verify that d.".
+By my reason it holds that d.
+Abort.
+
+Local Create HintDb my_second_reason.
+Notation "'my' 'second' 'reason'" := "my_second_reason"%string.
+Local Parameter Hda : d -> a.
+Hint Resolve Hda : my_second_reason.
+
+(** Test 33: Use extra databases and additional lemmas *)
+
+Goal b.
+By my reason, my second reason and Hab it holds that b as (i).
+clear i.
+By my reason, my second reason, Hab and Hbc it holds that c.
+Abort.