Intro pattern extensions for dup, swap and apply

1 files changed, 56 insertions, 0 deletions

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.