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

Reviewed-by: gares
Ack-by: Zimmi48

3 files changed, 39 insertions, 0 deletions

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.