Merge PR #6705: [ssr] extended intro patterns

8 files changed, 274 insertions, 1 deletions

diff --git a/test-suite/ssr/elim.v b/test-suite/ssr/elim.v
index 908249a369..720f4f6607 100644
--- a/test-suite/ssr/elim.v
+++ b/test-suite/ssr/elim.v
@@ -33,7 +33,7 @@ Qed.
 (* The same but without names for variables involved in the generated eq *)
 Lemma testL3 : forall A (s : seq A), s = s.
 Proof.
-move=> A s; elim branch: s; move: (s) => _.
+move=> A s; elim branch: s.
 match goal with _ : _ = [::] |- [::] = [::] => move: branch => // | _ => fail end.
 move=> _; match goal with _ : _ =  _ :: _ |- _ :: _ = _ :: _ => move: branch => // | _ => fail end.
 Qed.
diff --git a/test-suite/ssr/ipat_clear_if_id.v b/test-suite/ssr/ipat_clear_if_id.v
index 7a44db2ea0..cc087a62ad 100644
--- a/test-suite/ssr/ipat_clear_if_id.v
+++ b/test-suite/ssr/ipat_clear_if_id.v
@@ -8,6 +8,7 @@ Variable v2 : nat -> bool.
 
 Lemma test (v3 : nat -> bool) (v4 : bool -> bool) (v5 : bool -> bool) : nat -> nat -> nat -> nat -> True.
 Proof.
+Set Debug Ssreflect.
 move=> {}/v1 b1 {}/v2 b2 {}/v3 b3 {}/v2/v4/v5 b4.
 Check b1 : bool.
 Check b2 : bool.
@@ -20,4 +21,12 @@ Check v2 : nat -> bool.
 by [].
 Qed.
 
+Lemma test2 (v : True <-> False) : True -> False.
+Proof.
+move=> {}/v.
+Fail Check v.
+by [].
+Qed.
+
+
 End Foo.
diff --git a/test-suite/ssr/ipat_fastid.v b/test-suite/ssr/ipat_fastid.v
new file mode 100644
index 0000000000..8dc0c6cf0b
--- /dev/null
+++ b/test-suite/ssr/ipat_fastid.v
@@ -0,0 +1,31 @@
+Require Import ssreflect.
+
+Axiom odd : nat -> Prop.
+
+Lemma simple :
+  forall x, 3 <= x -> forall y, odd (y+x) -> x = y -> True.
+Proof.
+move=> >x_ge_3 >xy_odd.
+lazymatch goal with
+| |- ?x = ?y -> True => done
+end.
+Qed.
+
+
+Definition stuff x := 3 <= x -> forall y, odd (y+x) -> x = y -> True.
+
+Lemma harder : forall x, stuff x.
+Proof.
+move=> >x_ge_3 >xy_odd.
+lazymatch goal with
+| |- ?x = ?y -> True => done
+end.
+Qed.
+
+Lemma homotop : forall x : nat, forall e : x = x, e = e -> True.
+Proof.
+move=> >eq_ee.
+lazymatch goal with
+| |- True => done
+end.
+Qed.
diff --git a/test-suite/ssr/ipat_seed.v b/test-suite/ssr/ipat_seed.v
new file mode 100644
index 0000000000..e418d66917
--- /dev/null
+++ b/test-suite/ssr/ipat_seed.v
@@ -0,0 +1,60 @@
+Require Import ssreflect.
+
+Section foo.
+
+Variable A : Type.
+
+Record bar (X : Type) := mk_bar {
+  a : X * A;
+  b : A;
+  c := (a,7);
+  _ : X;
+  _ : X
+}.
+
+Inductive baz (X : Type) (Y : Type) : nat -> Type :=
+| K1 x (e : 0=1) (f := 3) of x=x:>X : baz X Y O
+| K2 n of n=n & baz X nat 0 : baz X Y (n+1).
+
+Axiom Q : nat -> Prop.
+Axiom Qx : forall x, Q x.
+Axiom my_ind :
+  forall P : nat -> Prop, P O -> (forall n m (w : P n /\ P m), P (n+m)) ->
+     forall w, P w.
+
+Lemma test x : bar nat -> baz nat nat x -> forall n : nat, Q n.
+Proof.
+
+(* record *)
+move => [^~ _ccc ].
+Check (refl_equal _ : c_ccc = (a_ccc, 7)).
+
+(* inductive *)
+move=> [^ xxx_ ].
+Check (refl_equal _ : xxx_f = 3).
+  by [].
+Check (refl_equal _ : xxx_n = xxx_n).
+
+(* eliminator *)
+elim/my_ind => [^ wow_ ].
+  exact: Qx 0.
+Check (wow_w : Q wow_n /\ Q wow_m).
+exact: Qx (wow_n + wow_m).
+
+Qed.
+
+Arguments mk_bar A x y z w : rename.
+Arguments K1 A B a b c : rename.
+
+
+Lemma test2 x : bar nat -> baz nat nat x -> forall n : nat, Q n.
+Proof.
+move=> [^~ _ccc ].
+Check (refl_equal _ :  c_ccc = (x_ccc, 7)).
+move=> [^ xxx_ ].
+Check (refl_equal _ : xxx_f = 3).
+  by [].
+Check (refl_equal _ : xxx_n = xxx_n).
+Abort.
+
+End foo.
diff --git a/test-suite/ssr/ipat_tac.v b/test-suite/ssr/ipat_tac.v
new file mode 100644
index 0000000000..cfef2e37be
--- /dev/null
+++ b/test-suite/ssr/ipat_tac.v
@@ -0,0 +1,38 @@
+Require Import ssreflect.
+
+Ltac fancy := case; last first.
+
+Notation fancy := (ltac:( fancy )).
+
+Ltac replicate n :=
+  let what := fresh "_replicate_" in
+  move=> what; do n! [ have := what ]; clear what.
+
+Notation replicate n := (ltac:( replicate n )).
+
+Lemma foo x (w : nat) (J : bool -> nat -> nat) : exists y, x=0+y.
+Proof.
+move: (w) => /ltac:(idtac) _.
+move: w => /(replicate 6) w1 w2 w3 w4 w5 w6.
+move: w1 => /J/fancy [w'||];last exact: false.
+  move: w' => /J/fancy[w''||]; last exact: false.
+    by exists x.
+  by exists x.
+by exists x.
+Qed.
+
+Ltac unfld what := rewrite /what.
+
+Notation "% n" := (ltac:( unfld n )) (at level 0) : ssripat_scope.
+Notation "% n" := n : nat_scope.
+
+Open Scope nat_scope.
+
+
+Definition def := 4.
+
+Lemma test : True -> def = 4.
+Proof.
+move=> _ /(% def).
+match goal with |- 4 = 4 => reflexivity end.
+Qed.
diff --git a/test-suite/ssr/ipat_tmp.v b/test-suite/ssr/ipat_tmp.v
new file mode 100644
index 0000000000..5f5421ac74
--- /dev/null
+++ b/test-suite/ssr/ipat_tmp.v
@@ -0,0 +1,22 @@
+Require Import ssreflect ssrbool.
+
+ Axiom eqn : nat -> nat -> bool.
+ Infix "==" := eqn (at level 40).
+ Axiom eqP : forall x y : nat, reflect (x = y) (x == y).
+
+ Lemma test1 :
+   forall x y : nat, x = y -> forall z : nat, y == z -> x = z.
+ Proof.
+ by move=> x y + z /eqP <-; apply.
+ Qed.
+
+ Lemma test2 : forall (x y : nat) (e : x = y), e = e -> x = y.
+ Proof.
+ move=> + y + _ => x def_x; exact: (def_x : x = y).
+ Qed.
+
+ Lemma test3 :
+   forall x y : nat, x = y -> forall z : nat, y == z -> x = z.
+ Proof.
+ move=> ++++ /eqP <- => x y e z; exact: e.
+ Qed.
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.