diff options
Diffstat (limited to 'theories/ssr/ssreflect.v')
| -rw-r--r-- | theories/ssr/ssreflect.v | 56 |
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. |