Waterproof proof mode, first version.

Author: SkySkimmer

src/g_waterproof.mlg

@@ -21,8 +21,55 @@ DECLARE PLUGIN "coq-waterproof.plugin"
 {
 open Exceptions
 open Waterprove
+open Vernacextend
+open G_vernac
+open Ltac2_plugin
+open Ltac2_plugin.G_ltac2
 
 let waterproof_version : string = "3.1.1+dev"
+
+let wp_command_entry = Procq.Entry.make "waterproof_command"
+
+(* The actual custom entry is not yet created at plugin linking time
+   and may be re-created at summary unfreeze time, but we need a truly
+   global entry to use in VERNAC EXTEND.
+
+   To solve this we use indirection: the global entry calls a dynamic
+   parser which looks up the custom entry. *)
+let wp_entry_name = Names.Id.of_string "waterproof_tactic"
+
+let wp_entry_full_name =
+    (Libnames.add_path_suffix (Libnames.path_of_string "Waterproof.Waterproof") wp_entry_name)
+
+let parse_wp_tactic _kwstate strm =
+  let entry = Tac2entries.CustomTab.of_path wp_entry_full_name in
+  let entry = Tac2entries.find_custom_entry entry in
+  Procq.Entry.parse_token_stream entry strm
+
+let wp_tactic_entry = Procq.Entry.of_parser "waterproof_tactic" { parser_fun = parse_wp_tactic }
+let _wp_tactic_entry = wp_tactic_entry
+
+let _ : Pvernac.proof_mode = Pvernac.register_proof_mode "Waterproof"
+    (ProofMode {
+        command_entry = wp_command_entry;
+        wit_tactic_expr = Tac2env.wit_ltac2_tac;
+        tactic_expr_entry = wp_tactic_entry;
+      })
+
+(* Duplicated with g_ltac2 *)
+let pr_ltac2expr e = Tac2print.pr_rawexpr_gen E5 ~avoid:Names.Id.Set.empty e
+
+let () = "coq-waterproof.plugin" |> Mltop.declare_cache_obj @@ fun () ->
+  Tac2entries.register_custom_entry (CAst.make wp_entry_name)
+
+let waterproof_set_default_notation_target = function
+  | (Some _, _) as v -> v
+  | None, lev ->
+    let qid = Libnames.qualid_of_path wp_entry_full_name in
+    Some qid, Some (Option.default 5 lev)
+
+let raw_attributes = Attributes.raw_attributes
+
 }
 
 (* Add any words that occur right after mathematical expressions as keywords *)
@@ -35,6 +82,39 @@ let () = Mltop.add_init_function "coq-waterproof.plugin" @@ fun () ->
         (fun kw -> CLexer.add_keyword_tok kw (Tok.PKEYWORD s)))
       ["and"; "as"; "hold"; "holds"; "it"; "or"; "we"; "that"]
 }
+
+VERNAC ARGUMENT EXTEND wp_tactic_entry
+PRINTED BY { pr_ltac2expr }
+| [ _wp_tactic_entry(e) ] -> { e }
+END
+
+VERNAC { wp_command_entry } EXTEND VernacLtac2Alt
+| ![proof] [ wp_tactic_entry(t) "." ] =>
+  { classify_as_proofstep } -> { fun ~pstate ->
+    Tac2entries.call ~pstate None ~with_end_tac:(CAst.make false) t
+  }
+END
+
+VERNAC COMMAND EXTEND WaterproofNotation
+| #[ raw_attributes ] [ "Waterproof" "Notation" ltac2def_syn(e) ] => { Vernacextend.(VtSideff ([], VtNow)) } SYNTERP AS synterpv {
+    let (toks, n, body) = e in
+    let n = waterproof_set_default_notation_target n in
+    Tac2entries.register_notation raw_attributes toks n body
+  } ->
+  {
+    Tac2entries.register_notation_interpretation synterpv
+  }
+END
+
+GRAMMAR EXTEND Gram
+  GLOBAL: wp_command_entry;
+  wp_command_entry: TOP
+    [ [ p = subprf -> { Vernacexpr.VernacSynPure p }
+      | g = OPT toplevel_selector; p = subprf_with_selector -> { Vernacexpr.VernacSynPure (p g) }
+      ] ];
+END
+
+(* Rest of waterproof *)
 VERNAC COMMAND EXTEND AutomationShieldEnableSideEff CLASSIFIED AS SIDEFF
   | [ "Waterproof" "Enable" "Automation" "Shield" ] ->
     {

tests/automation/Chains.v

@@ -34,6 +34,8 @@ Waterproof Enable Redirect Feedback.
 Local Parameter X : Type.
 Local Parameter a b c : X.
 
+Set Default Proof Mode "Ltac2".
+
 (* Test 1: first equality does not hold. *)
 Goal (& a = b = c).
 Proof.

tests/automation/Shield.v

@@ -128,14 +128,14 @@ Abort.
 (** Testing de Morgan laws. *)
 
 Require Import Waterproof.Libs.Negation.
-#[export] Hint Extern 1 => solve_by_manipulating_negation (fun () => ()) : wp_negation_logic.
+#[export] Hint Extern 1 => ltac2: solve_by_manipulating_negation (fun () => ()) : wp_negation_logic.
 
 (** Level 1 *)
 Local Parameter P1 : R -> Prop.
 (* Test 15 *)
 Goal ~ (forall x : R, P1 x) -> (exists x : R, ~ (P1 x)).
 Proof.
-  intro H.
+  ltac2: intro H.
   We conclude that (there exists x : ℝ, ¬ P1 x).
 Qed.
 
@@ -150,14 +150,14 @@ Local Parameter P2 : R -> R -> Prop.
 (* Test 17 *)
 Goal ~ (forall x : R, exists y : R, P2 x y) -> (exists x : R, ~ (exists y : R, P2 x y)).
 Proof.
-  intro H.
+  ltac2: intro H.
   We conclude that (there exists x : ℝ, ~ (exists y : R, P2 x y)).
 Qed.
 
 (* Test 17 *)
 Goal (exists x : R, ~ (exists y : R, P2 x y)) -> (exists x : R, forall y : R, ~ P2 x y).
 Proof.
-  intro H.
+  ltac2: intro H.
   We conclude that (exists x : R, forall y : R, ~ P2 x y).
 Qed.
 
@@ -166,7 +166,7 @@ Qed.
 Local Parameter P3 : R -> R -> R -> Prop.
 Goal ~ (forall x : R, exists y : R, P2 x y) -> (exists x : R, ~ (exists y : R, P2 x y)).
 Proof.
-  intro H.
+  ltac2: intro H.
   We conclude that (there exists x : ℝ, ~ (exists y : R, P2 x y)).
 Qed.
 
@@ -180,7 +180,7 @@ Goal ~ (forall eps : R, eps > 0 -> exists delta : R, delta > 0 -> forall x : R,
      (exists eps : R, eps > 0 /\ ~(exists delta : R, delta > 0 -> forall x : R,
           0 < Rdist x a < delta -> Rdist (f x) L < eps)).
 Proof.
-  intro H.
+  ltac2: intro H.
   We conclude that (there exists eps : ℝ , eps > 0
     ∧ ¬ (there exists delta : ℝ, delta > 0 ⇨ for all x : ℝ,
                        0 < Rdist x a < delta ⇨ Rdist (f x) L < eps)).
@@ -233,13 +233,13 @@ Abort.
 (** Testing de Morgan laws. *)
 
 Require Import Waterproof.Libs.Negation.
-#[export] Hint Extern 1 => (solve_by_manipulating_negation (fun () => ())) : wp_negation_logic.
+#[export] Hint Extern 1 => ltac2: (solve_by_manipulating_negation (fun () => ())) : wp_negation_logic.
 
 (** Level 1 *)
 (* Test 25 *)
 Goal ~ (∀ x ∈ R, P1 x) -> (∃ x ∈ R, ~ (P1 x)).
 Proof.
-  intro H.
+  ltac2: intro H.
   We conclude that (∃ x ∈ ℝ, ¬ P1 x).
 Qed.
 
@@ -253,22 +253,22 @@ Abort.
 (* Test 27 *)
 Goal ~ (∀ x ∈ R, ∃ y ∈ R, P2 x y) -> (∃ x ∈ R, ~ (∃ y ∈ R, P2 x y)).
 Proof.
-  intro H.
+  ltac2: intro H.
   We conclude that (∃ x ∈ ℝ, ~ (∃ y ∈ R, P2 x y)).
 Qed.
 
 (* Test 28 *)
 Goal (∃ x < 5, ~ (∃ y ≥ 7, P2 x y)) -> (∃ x < 5, ∀ y ≥ 7, ~ P2 x y).
 Proof.
-  intro H.
+  ltac2: intro H.
   We conclude that (∃ x < 5, ∀ y ≥ 7, ~ P2 x y).
 Qed.
 
 (** Level 3 *)
 (* Test 29 *)
 Goal ~ (∀ x ≤ 30, ∃ y ∈ R, P2 x y) -> (∃ x ≤ 30, ~ (∃ y ∈ R, P2 x y)).
 Proof.
-  intro H.
+  ltac2: intro H.
   We conclude that (∃ x ≤ 30, ~ (∃ y ∈ R, P2 x y)).
 Qed.
 
@@ -280,7 +280,7 @@ Goal ~ (∀ eps ∈ R, eps > 0 -> ∃ delta ∈ R, delta > 0 -> ∀ x ∈ R,
      (∃ eps ∈ R, eps > 0 /\ ~(∃ delta ∈ R, delta > 0 -> ∀ x ∈ R,
           0 < Rdist x a < delta -> Rdist (f x) L < eps)).
 Proof.
-  intro H.
+  ltac2: intro H.
   We conclude that (∃ eps ∈ R, eps > 0 /\ ~(∃ delta ∈ R, delta > 0 -> ∀ x ∈ R,
           0 < Rdist x a < delta -> Rdist (f x) L < eps)).
 Qed.

tests/automation/databases/Decidability.v

@@ -21,61 +21,61 @@ Require Import Waterproof.Automation.
 
 Goal forall P : Prop, {P} + {~P}.
 Proof.
-  auto with wp_decidability_epsilon.
+  ltac2: auto with wp_decidability_epsilon.
 Qed.
 
 Goal forall P Q : Prop, P \/ Q -> {P} + {Q}.
 Proof.
-  auto with wp_decidability_epsilon.
+  ltac2: auto with wp_decidability_epsilon.
 Qed.
 
 Goal forall P : Prop, P \/ ~P.
 Proof.
-  auto with wp_decidability_classical.
+  ltac2: auto with wp_decidability_classical.
 Qed.
 
 Goal forall P Q : Prop, {P} + {Q} -> P \/ Q.
-  auto with wp_decidability_constructive.
+  ltac2: auto with wp_decidability_constructive.
 Qed.
 
 Goal forall P Q : Prop, {Q} + {P} -> Q \/ P.
-  auto with wp_decidability_constructive.
+  ltac2: auto with wp_decidability_constructive.
 Qed.
 
 Goal forall P Q R: Prop, {P} + {Q} + {R} -> P \/ Q \/ R.
-  auto with wp_decidability_constructive.
+  ltac2: auto with wp_decidability_constructive.
 Qed.
 
 Goal forall P Q R: Prop, {P} + {R} + {Q} -> P \/ Q \/ R.
-  auto with wp_decidability_constructive.
+  ltac2: auto with wp_decidability_constructive.
 Qed.
 
 Goal forall P Q R: Prop, {Q} + {P} + {R} -> P \/ Q \/ R.
-  auto with wp_decidability_constructive.
+  ltac2: auto with wp_decidability_constructive.
 Qed.
 
 Goal forall P Q R: Prop, {Q} + {R} + {P} -> P \/ Q \/ R.
-  auto with wp_decidability_constructive.
+  ltac2: auto with wp_decidability_constructive.
 Qed.
 
 Goal forall P Q R: Prop, {R} + {P} + {Q} -> P \/ Q \/ R.
-  auto with wp_decidability_constructive.
+  ltac2: auto with wp_decidability_constructive.
 Qed.
 
 Goal forall P Q R: Prop, {R} + {P} + {Q} -> P \/ Q \/ R.
-  auto with wp_decidability_constructive.
+  ltac2: auto with wp_decidability_constructive.
 Qed.
 
 Goal forall n : nat, n < 5 \/ n > 4.
 Proof.
-  intro n.
-  auto with wp_decidability_nat.
+  ltac2: intro n.
+  ltac2: auto with wp_decidability_nat.
 Qed.
 
 From Stdlib Require Import Reals.Reals.
 Open Scope R_scope.
 Goal forall x : R, x < 5 \/ x > 4.
 Proof.
-  intro x.
-  auto with wp_decidability_reals.
+  ltac2: intro x.
+  ltac2: auto with wp_decidability_reals.
 Qed.

tests/automation/databases/Integers.v

@@ -30,28 +30,28 @@ From Stdlib Require Import Lia.
 
 Goal  ∀ n : ℕ -> ℕ, (∀ k : ℕ, (n (k + 1) > n k)%nat) ⇒
     ∀ k : ℕ, (n k ≥ k)%nat.
-  intro n.
-  intro H.
-  induction k as [| k IHk].
-  - solve [auto with wp_integers zarith].
-  - assert (H1 : S k = k + 1) by (auto with wp_integers zarith).
-    rewrite H1.
-    assert (H2 : n (k + 1) > n k) by (auto with wp_integers zarith).
-    auto with wp_integers zarith.
+  ltac2: intro n.
+  ltac2: intro H.
+  ltac2: induction k as [| k IHk].
+  - ltac2: solve [auto with wp_integers zarith].
+  - ltac2: assert (H1 : S k = k + 1) by (auto with wp_integers zarith).
+    ltac2: rewrite H1.
+    ltac2: assert (H2 : n (k + 1) > n k) by (auto with wp_integers zarith).
+    ltac2: auto with wp_integers zarith.
 Qed.
 
 Goal (& 3 < 4 <= 5).
-  cbn; repeat split; solve [ltac1:(auto with wp_core wp_integers)].
+  ltac2: (cbn; repeat split; solve [ltac1:(auto with wp_core wp_integers)]).
 Qed.
 
 Goal (& 3 = 3 = 3).
-  cbn; repeat split; solve [auto with wp_core wp_integers].
+  ltac2: (cbn; repeat split; solve [auto with wp_core wp_integers]).
 Qed.
 
 (* Test 1: check if terms of a subset can be coerced to terms of the underlying set (here: [R]). *)
 Goal forall x : nat, (& x < 5 = 2 + 3) -> (x < 5).
-  intro x.
-  intro H.
-  simpl_ineq_chains ().
-  solve [auto with wp_integers zarith].
+  ltac2: intro x.
+  ltac2: intro H.
+  ltac2: simpl_ineq_chains ().
+  ltac2: solve [auto with wp_integers zarith].
 Qed.

tests/automation/databases/RealsAndIntegers.v

@@ -30,47 +30,47 @@ Open Scope R_scope.
 
 Goal forall x y: R, forall f: R -> R, x = y -> f (x + 1) = f (y + 1).
 Proof.
-  waterprove 5 false Main.
+  ltac2: waterprove 5 false Main.
 Qed.
 
 Goal forall x y: R, forall f: R -> R, x = y -> f x = f y /\ x = y.
 Proof.
-  waterprove 5 false Main.
+  ltac2: waterprove 5 false Main.
 Qed.
 
 Goal (& 3 < 4 <= 5).
-  cbn; repeat split; auto with wp_core wp_reals.
+  ltac2: (cbn; repeat split; auto with wp_core wp_reals).
 Qed.
 
 Goal (& 3 = 3 = 3).
-  cbn; repeat split; auto with wp_core wp_reals.
+  ltac2: (cbn; repeat split; auto with wp_core wp_reals).
 Qed.
 
 Goal forall x : R, (& x < 5 = 2 + 3) -> (x < 5).
-  intro x.
-  intro H.
-  auto with wp_core wp_reals.
+  ltac2: intro x.
+  ltac2: intro H.
+  ltac2: auto with wp_core wp_reals.
 Qed.
 
 (** ** Testcases to deal with Rabs Rmin Rmax *)
 
 Goal forall b: R, b > 0 -> - Rmax( 0, 1 - b/2) >= - 1.
-  auto with wp_reals.
+  ltac2: auto with wp_reals.
 Qed.
 
 Goal forall b: R, b > 0 -> Rmin( 0, -1 + b/2) <= 1.
-  auto with wp_reals.
+  ltac2: auto with wp_reals.
 Qed.
 
 Goal forall r : R, r > 0 ->
   | Rmax 0 (1 - r/2) - 1 | = 1 - (Rmax 0 (1 - r/2)).
-  auto with wp_reals.
+  ltac2: auto with wp_reals.
 Qed.
 
 Goal forall x r : R, r > 0 ->
   x = Rmax 0 (1 - r/2) -> Rabs (x - 1) < r.
-  intros x r r_gt_0 x_eq_Rmax.
-  auto with wp_reals.
+  ltac2: intros x r r_gt_0 x_eq_Rmax.
+  ltac2: auto with wp_reals.
 Qed.
 
 Close Scope R_scope.