Intro pattern extensions for dup, swap and apply

1 files changed, 57 insertions, 0 deletions

diff --git a/mathcomp/ssreflect/ssreflect.v b/mathcomp/ssreflect/ssreflect.v
index 2925496..888f98d 100644
--- a/mathcomp/ssreflect/ssreflect.v
+++ b/mathcomp/ssreflect/ssreflect.v
@@ -28,6 +28,14 @@ Global Set Bullet Behavior "None".
 (*        triggered by such evars under binders.                              *)
 (*  Import Deprecation.Silent :: turn off deprecation warning messages.       *)
 (*  Import Deprecation.Reject :: raise an error instead of only warning.      *)
+(*                                                                            *)
+(*   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)             *)
 (******************************************************************************)
 
 Module NonPropType.
@@ -94,3 +102,52 @@ End Exports.
 
 End Deprecation.
 Export Deprecation.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.
+
+(* 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 "'[' '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.