Merge PR #13317: [ssr] intro pattern extensions for dup, swap and apply

Reviewed-by: gares
Ack-by: Zimmi48

6 files changed, 103 insertions, 1 deletions

diff --git a/doc/changelog/06-ssreflect/13317-ssr_dup_swap_apply_ipat.rst b/doc/changelog/06-ssreflect/13317-ssr_dup_swap_apply_ipat.rst
new file mode 100644
index 0000000000..8d1564533d
--- /dev/null
+++ b/doc/changelog/06-ssreflect/13317-ssr_dup_swap_apply_ipat.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  SSReflect intro pattern ltac views ``/[dup]``, ``/[swap]`` and ``/[apply]``
+  (`#13317 <https://github.com/coq/coq/pull/13317>`_,
+  by Cyril Cohen).
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 22544b2018..07c2d268c6 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -1647,7 +1647,10 @@ Notations can be used to name tactics,  for example
    Notation "'myop'" := (ltac:(my ltac code)) : ssripat_scope.
 
 lets one write just ``/myop`` in the intro pattern. Note the scope
-annotation: views are interpreted opening the ``ssripat`` scope.
+annotation: views are interpreted opening the ``ssripat`` scope.  We
+provide the following ltac views: ``/[dup]`` to duplicate the top of
+the stack, ``/[swap]`` to swap the two first elements and ``/[apply]``
+to apply the top of the stack to the next.
 
 Intro patterns
 ``````````````
diff --git a/test-suite/ssr/ipat_apply.v b/test-suite/ssr/ipat_apply.v
new file mode 100644
index 0000000000..2f7986aea6
--- /dev/null
+++ b/test-suite/ssr/ipat_apply.v
@@ -0,0 +1,13 @@
+Require Import ssreflect.
+
+Section Apply.
+
+Variable P : nat -> Prop.
+Lemma test_apply A B : forall (f : A -> B) (a : A), B.
+
+Proof.
+move=> /[apply] b.
+exact.
+Qed.
+
+End Apply.
diff --git a/test-suite/ssr/ipat_dup.v b/test-suite/ssr/ipat_dup.v
new file mode 100644
index 0000000000..b1936df31d
--- /dev/null
+++ b/test-suite/ssr/ipat_dup.v
@@ -0,0 +1,13 @@
+Require Import ssreflect.
+
+Section Dup.
+
+Variable P : nat -> Prop.
+
+Lemma test_dup1 : forall n : nat, P n.
+Proof. move=> /[dup] m n; suff: P n by []. Abort.
+
+Lemma test_dup2 : let n := 1 in False.
+Proof. move=> /[dup] m n; have : m = n := eq_refl. Abort.
+
+End Dup.
diff --git a/test-suite/ssr/ipat_swap.v b/test-suite/ssr/ipat_swap.v
new file mode 100644
index 0000000000..1d78a2a009
--- /dev/null
+++ b/test-suite/ssr/ipat_swap.v
@@ -0,0 +1,13 @@
+Require Import ssreflect.
+
+Section Swap.
+
+Definition P n := match n with 1 => true | _ => false end.
+
+Lemma test_swap1 : forall (n : nat) (b : bool), P n = b.
+Proof. move=> /[swap] b n; suff: P n = b by []. Abort.
+
+Lemma test_swap1 : let n := 1 in let b := true in False.
+Proof. move=> /[swap] b n; have : P n = b := eq_refl. Abort.
+
+End Swap.
diff --git a/theories/ssr/ssreflect.v b/theories/ssr/ssreflect.v
index 97a283b875..175cae8415 100644
--- a/theories/ssr/ssreflect.v
+++ b/theories/ssr/ssreflect.v
@@ -59,6 +59,15 @@ Declare ML Module "ssreflect_plugin".
        Canonical foo_unlockable := #[#unlockable fun foo#]#.
      This minimizes the comparison overhead for foo, while still allowing
      rewrite unlock to expose big_foo_expression.
+
+  Additionally we provide default intro pattern ltac views:
+  - top of the stack actions:
+    => /[apply]     := => hyp {}/hyp
+    => /[swap]      := => x y; move: y x
+                      (also swap and perserves let bindings)
+    => /[dup]       := => x; have copy := x; move: copy x
+                      (also copies and preserves let bindings)
+
  More information about these definitions and their use can be found in the
  ssreflect manual, and in specific comments below.                           **)
 
@@ -654,3 +663,50 @@ End Exports.
 
 End NonPropType.
 Export NonPropType.Exports.
+
+Module Export ipat.
+
+Notation "'[' 'apply' ']'" := (ltac:(let f := fresh "_top_" in move=> f {}/f))
+  (at level 0, only parsing) : ssripat_scope.
+
+(** We try to preserve the naming by matching the names from the goal.
+    We do 'move' to perform a hnf before trying to match.               **)
+Notation "'[' 'swap' ']'" := (ltac:(move;
+  lazymatch goal with
+  | |- forall (x : _), _ => let x := fresh x in move=> x; move;
+    lazymatch goal with
+    | |- forall (y : _), _ => let y := fresh y in move=> y; move: y x
+    | |- let y := _ in _ => let y := fresh y in move=> y; move: @y x
+    | _ => let y := fresh "_top_" in move=> y; move: y x
+    end
+  | |- let x := _ in _ => let x := fresh x in move => x; move;
+    lazymatch goal with
+    | |- forall (y : _), _ => let y := fresh y in move=> y; move: y @x
+    | |- let y := _ in _ => let y := fresh y in move=> y; move: @y @x
+    | _ => let y := fresh "_top_" in move=> y; move: y x
+    end
+  | _ => let x := fresh "_top_" in let x := fresh x in move=> x; move;
+    lazymatch goal with
+    | |- forall (y : _), _ => let y := fresh y in move=> y; move: y @x
+    | |- let y := _ in _ => let y := fresh y in move=> y; move: @y @x
+    | _ => let y := fresh "_top_" in move=> y; move: y x
+    end
+  end))
+  (at level 0, only parsing) : ssripat_scope.
+
+Notation "'[' 'dup' ']'" := (ltac:(move;
+  lazymatch goal with
+  | |- forall (x : _), _ =>
+    let x := fresh x in move=> x;
+    let copy := fresh x in have copy := x; move: copy x
+  | |- let x := _ in _ =>
+    let x := fresh x in move=> x;
+    let copy := fresh x in pose copy := x;
+    do [unfold x in (value of copy)]; move: @copy @x
+  | |- _ =>
+    let x := fresh "_top_" in move=> x;
+    let copy := fresh "_top" in have copy := x; move: copy x
+  end))
+  (at level 0, only parsing) : ssripat_scope.
+
+End ipat.