[ssr] extended intro patterns: + > [^] /ltac:

This commit implements the following intro patterns:

Temporary "=> +"
 "move=> + stuff" ==== "move=> tmp stuff; move: tmp"
 It preserves the original name.
 "=>" can be chained to force generalization as in
 "move=> + y + => x z"

Tactics as views "=> /ltac:(tactic)"
 Supports notations, eg "Notation foo := ltac:(bla bla bla). .. => /foo".
 Limited to views on the right of "=>", views that decorate a tactic
 as move or case are not supported to be tactics.

Dependent "=> >H"
 move=> >H  ===== move=> ???? H, with enough ? to
 name H the first non-dependent assumption (LHS of the first arrow).
 TC isntances are skipped.

Block intro "=> [^ H] [^~ H]"
 after "case" or "elim" or "elim/v" it introduces in one go
 all new assumptions coming from the eliminations. The names are
 picked from the inductive type declaration or the elimination principle
 "v" in "elim/v" and are appended/prepended the seed "H"

The implementation makes crucial use of the goal_with_state feature of
the tactic monad. For example + schedules a generalization to be performed
at the end of the intro pattern and [^ .. ] reads the name seeds from
the state (that is filled in by case and elim).

6 files changed, 161 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.