[ssr] new test by Arthur Charguéraud

2 files changed, 113 insertions, 0 deletions

diff --git a/test-suite/ssr/misc_extended.v b/test-suite/ssr/misc_extended.v
new file mode 100644
index 0000000000..81c86f1af4
--- /dev/null
+++ b/test-suite/ssr/misc_extended.v
@@ -0,0 +1,83 @@
+Require Import ssreflect.
+
+Require Import List.
+
+Lemma test_elim_pattern_1 : forall A (l:list A), l ++ nil = l.
+Proof.
+intros A.
+elim/list_ind => [^~ 1 ].
+  by [].
+match goal with |- (a1 :: l1) ++ nil = a1 :: l1 => idtac end.
+Abort.
+
+Lemma test_elim_pattern_2 : forall A (l:list A), l ++ nil = l.
+Proof.
+intros. elim: l => [^~ 1 ].
+  by [].
+match goal with |- (a1 :: l1) ++ nil = a1 :: l1 => idtac end.
+Abort.
+
+Lemma test_elim_pattern_3 : forall A (l:list A), l ++ nil = l.
+Proof.
+intros. elim: l => [ | x l' IH ].
+  by [].
+match goal with |- (x :: l') ++ nil = x :: l' => idtac end.
+Abort.
+
+
+Generalizable Variables A.
+
+Class Inhab (A:Type) : Type :=
+  { arbitrary : A }.
+
+Lemma test_intro_typeclass_1 : forall A `{Inhab A} (l1 l2:list A), l2 = nil -> l1 ++ l2 = l1.
+Proof.
+move =>> H.
+  match goal with |- _ = _ => idtac end.
+Abort.
+
+Lemma test_intro_typeclass_2 : forall A `{Inhab A} (x:A), x = arbitrary -> x = arbitrary.
+Proof.
+move =>> H.
+  match goal with |- _ = _ => idtac end.
+Abort.
+
+Lemma test_intro_temporary_1 : forall A (l1 l2:list A), l2 = nil -> l1 ++ l2 = l1.
+Proof.
+move => A + l2.
+  match goal with |- forall l1, l2 = nil -> l1 ++ l2 = l1 => idtac end.
+Abort.
+
+Lemma test_intro_temporary_2 : forall A `{Inhab A} (l1 l2:list A), l2 = nil -> l1 ++ l2 = l1.
+Proof.
+move => > E.
+  match goal with |- _ = _ => idtac end.
+Abort.
+
+Lemma test_dispatch : (forall x:nat, x= x )/\ (forall y:nat, y = y).
+Proof.
+intros. split => [ a | b ].
+  match goal with |- a = a => by [] end.
+match goal with |- b = b => by [] end.
+Abort.
+
+Lemma test_tactics_as_view_1 : forall A (l1:list A), nil ++ l1 = l1.
+Proof.
+move => /ltac:(simpl).
+Abort.
+
+Lemma test_tactics_as_view_2 : forall A, (forall (l1:list A), nil ++ l1 = l1) /\ (nil ++ nil = @nil A).
+Proof.
+move => A.
+(* TODO: I want to do  [split =>.] as a temporary step in setting up my script,
+    but this syntax does not seem to be supported. Can't we have an empty ipat?
+   Note that I can do [split => [ | ]]*)
+split => [| /ltac:(simpl)].
+Abort.
+
+Notation "%%" := (ltac:(simpl)) : ssripat_scope.
+
+Lemma test_tactics_as_view_3 : forall A, (forall (l1:list A), nil ++ l1 = l1) /\ (nil ++ nil = @nil A).
+Proof.
+move => /ltac:(split) [ | /%% ].
+Abort.
diff --git a/test-suite/ssr/misc_tc.v b/test-suite/ssr/misc_tc.v
new file mode 100644
index 0000000000..4db45b743a
--- /dev/null
+++ b/test-suite/ssr/misc_tc.v
@@ -0,0 +1,30 @@
+Require Import ssreflect List.
+
+Generalizable Variables A B.
+
+Class Inhab (A:Type) : Type :=
+  { arbitrary : A }.
+
+Lemma test_intro_typeclass_1 : forall A `{Inhab A} (x:A), x = arbitrary -> x = arbitrary.
+Proof.
+move =>> H. (* introduces [H:x=arbitrary] because first non dependent hypothesis *)
+Abort.
+
+Lemma test_intro_typeclass_2 : forall A `{Inhab A} (l1 l2:list A), l2 = nil -> l1 ++ l2 = l1.
+Proof.
+move =>> H. (* introduces [Inhab A] automatically because it is a typeclass instance *)
+Abort.
+
+Lemma test_intro_typeclass_3 : forall `{Inhab A, Inhab B} (x:A) (y:B), True -> x = x.
+Proof. (* Above types [A] and [B] are implicitly quantified *)
+move =>> y H. (* introduces the two typeclass instances automatically *)
+Abort.
+
+Class Foo `{Inhab A} : Type :=
+  { foo : A }.
+
+Lemma test_intro_typeclass_4 : forall `{Foo A}, True -> True.
+Proof. (* Above, [A] and [{Inhab A}] are implicitly quantified *)
+move =>> H. (* introduces [A] and [Inhab A] because they are dependently used,
+               and introduce [Foo A] automatically because it is an instance. *)
+Abort.