Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided in

a Coq meeting some time ago. NB: this syntax is an alias for (x,(y,(z,t)))



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11033 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 39 insertions, 33 deletions

diff --git a/CHANGES b/CHANGES
index c51cbd9dc..ee4f01044 100644
--- a/CHANGES
+++ b/CHANGES
@@ -164,7 +164,8 @@ Tactics
   Some intro patterns don't need space between them. In particular
   intros ?a?b used to be legal and equivalent to intros ? a ? b. Now it
   is still legal but equivalent to intros ?a ?b.
-- New intro pattern "{A,B,C}" synonym to "(A,(B,C))"
+- New intro pattern "(A & ... & Y & Z)" synonym to "(A,....,(Y,Z)))))"
+  for right-associative constructs like /\ or exists.
 - rewrite now supports "by" to solve side-conditions and "at" to select
   occurrences. (DOC TODO)
 - New syntax "rewrite A,B" for "rewrite A; rewrite B"
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index ed1ee75cc..3a8f6ca52 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1675,6 +1675,8 @@ either:
 \item a disjunction of lists of patterns:
   {\tt [$p_{11}$ {\ldots} $p_{1m_1}$ | {\ldots} | $p_{11}$ {\ldots} $p_{nm_n}$]}
 \item a conjunction of patterns: {\tt (} $p_1$ {\tt ,} {\ldots} {\tt ,} $p_n$ {\tt )}
+\item a list of patterns {\tt (} $p_1$\ {\tt \&}\ {\ldots}\ {\tt \&}\ $p_n$ {\tt )}
+ for sequence of right-associative binary constructs
 \item the rewriting orientations: {\tt ->} or {\tt <-}
 \end{itemize}
 
@@ -1702,7 +1704,7 @@ introduction pattern $p$:
   number of constructors is $n$ (or over a statement of conclusion a
   similar inductive type ): it destructs the introduced hypothesis as
   {\tt destruct} (see Section~\ref{destruct}) would and applies on
-  each generated subgoal the corresponding tactic
+  each generated subgoal the corresponding tactic;
   \texttt{intros}~$p_{i1}$ {\ldots} $p_{im_i}$; if the disjunctive
   pattern is part of a sequence of patterns and is not the last
   pattern of the sequence, then {\Coq} completes the pattern so as all
@@ -1717,7 +1719,14 @@ introduction pattern $p$:
   would, and applies the patterns $p_1$~\ldots~$p_n$ to the arguments
   of the constructor of $I$ (observe that {\tt ($p_1$, {\ldots},
   $p_n$)} is an alternative notation for {\tt [$p_1$ {\ldots}
-  $p_n$]}).
+  $p_n$]});
+\item introduction via {\tt ( $p_1$ \& \ldots \& $p_n$ )}
+  is a shortcut for introduction via
+  {\tt ($p_1$,(\ldots,(\dots,$p_n$)\ldots))}; it expects the
+  hypothesis to be a sequence of right-associative binary inductive 
+  constructors such as {\tt conj} or {\tt ex\_intro}; for instance, an
+  hypothesis with type {\tt A\verb|/\|exists x, B\verb|/\|C\verb|/\|D} can be
+  introduced via pattern {\tt (a \& x \& b \& c \& d)};
 \item introduction over {\tt ->} (respectively {\tt <-}) expects the
   hypothesis to be an equality and the right-hand-side (respectively
   the left-hand-side) is replaced by the left-hand-side (respectively
@@ -1749,14 +1758,6 @@ Show 2.
 
 \end{itemize}
 
-\Rem An additional abbreviation is allowed for sequences of rightmost
-binary conjunctions: pattern 
-{\tt \{} $p_1$ {\tt ,} {\ldots} {\tt ,} $p_n$ {\tt \}} 
-is a synonym for pattern 
-{\tt (} $p_1$ {\tt , (} $p_2$ {\tt ,} {\ldots} {\tt (}$p_{n-1}${\tt ,}$p_n${\tt )} {\ldots}  {\tt ))}.
-In particular it can be used to introduce existential hypotheses
-and/or n-ary conjunctions. 
-
 \begin{coq_example}
 Lemma intros_test : forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C.
 intros A B C [a| [_ c]] f.
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 672c4eaba..ebf28e8eb 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -220,14 +220,18 @@ GEXTEND Gram
   ;
   simple_intropattern:
     [ [ "["; tc = LIST1 intropatterns SEP "|" ; "]" -> IntroOrAndPattern tc
-      | "("; tc = LIST0 simple_intropattern SEP "," ; ")" -> IntroOrAndPattern [tc]
       | "()" -> IntroOrAndPattern [[]]
-      | "{"; tc = LIST0 simple_intropattern SEP "," ; "}" -> 
-	  (* {A,B,C} is translated into (A,(B,C)) *)
+      | "("; si = simple_intropattern; ")" -> IntroOrAndPattern [[si]]
+      | "("; si = simple_intropattern; ","; 
+             tc = LIST1 simple_intropattern SEP "," ; ")" -> 
+	       IntroOrAndPattern [si::tc]
+      | "("; si = simple_intropattern; "&"; 
+	     tc = LIST1 simple_intropattern SEP "&" ; ")" -> 
+	  (* (A & B & C) is translated into (A,(B,C)) *)
 	  let rec pairify = function 
 	    | ([]|[_]|[_;_]) as l -> IntroOrAndPattern [l]
 	    | t::q -> IntroOrAndPattern [[t;pairify q]]
-	  in pairify tc
+	  in pairify (si::tc)
       | "_" -> IntroWildcard
       | prefix = pattern_ident -> IntroFresh prefix
       | "?" -> IntroAnonymous
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 2a2960f19..437f52ab0 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -1592,11 +1592,11 @@ intros m; functional induction (map_option f m); simpl; auto; intros.
 inversion H.
 rewrite join_in in H; destruct H as [H|[H|H]].
 exists d; split; auto; rewrite (f_compat d H), e0; discriminate.
-destruct (IHt _ H) as {d0,?,?}; exists d0; auto.
-destruct (IHt0 _ H) as {d0,?,?}; exists d0; auto.
+destruct (IHt _ H) as (d0 & ? & ?); exists d0; auto.
+destruct (IHt0 _ H) as (d0 & ? & ?); exists d0; auto.
 rewrite concat_in in H; destruct H as [H|H].
-destruct (IHt _ H) as {d0,?,?}; exists d0; auto.
-destruct (IHt0 _ H) as {d0,?,?}; exists d0; auto.
+destruct (IHt _ H) as (d0 & ? & ?); exists d0; auto.
+destruct (IHt0 _ H) as (d0 & ? & ?); exists d0; auto.
 Qed.
 
 Lemma map_option_bst : forall m, bst m -> bst (map_option f m).
@@ -1604,10 +1604,10 @@ Proof.
 intros m; functional induction (map_option f m); simpl; auto; intros; 
  inv bst.
 apply join_bst; auto; intros y H; 
- destruct (map_option_2 H) as {d0,?,?}; eauto using MapsTo_In.
+ destruct (map_option_2 H) as (d0 & ? & ?); eauto using MapsTo_In.
 apply concat_bst; auto; intros y y' H H'.
-destruct (map_option_2 H) as {d0,?,?}.
-destruct (map_option_2 H') as {d0',?,?}.
+destruct (map_option_2 H) as (d0 & ? & ?).
+destruct (map_option_2 H') as (d0' & ? & ?).
 eapply X.lt_trans with x; eauto using MapsTo_In.
 Qed.
 Hint Resolve map_option_bst.
@@ -1626,9 +1626,9 @@ intros m; functional induction (map_option f m); simpl; auto; intros;
  try destruct X.compare; simpl; auto.
 rewrite (f_compat d e); auto.
 intros y H;
- destruct (map_option_2 H) as {?,?,?}; eauto using MapsTo_In.
+ destruct (map_option_2 H) as (? & ? & ?); eauto using MapsTo_In.
 intros y H; 
- destruct (map_option_2 H) as {?,?,?}; eauto using MapsTo_In.
+ destruct (map_option_2 H) as (? & ? & ?); eauto using MapsTo_In.
 
 rewrite <- IHt, IHt0; auto; nonify (find x0 r); auto.
 rewrite IHt, IHt0; auto; nonify (find x0 r); nonify (find x0 l); auto.
@@ -1637,8 +1637,8 @@ rewrite <- IHt0, IHt; auto; nonify (find x0 l); auto.
  destruct (find x0 (map_option f r)); auto.
 
 intros y y' H H'.
-destruct (map_option_2 H) as {?,?,?}.
-destruct (map_option_2 H') as {?,?,?}.
+destruct (map_option_2 H) as (? & ? & ?).
+destruct (map_option_2 H') as (? & ? & ?).
 eapply X.lt_trans with x; eauto using MapsTo_In.
 Qed.
 
diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v
index 671917595..209eb5497 100644
--- a/theories/NArith/BinPos.v
+++ b/theories/NArith/BinPos.v
@@ -1022,24 +1022,24 @@ Proof.
   induction p as [p IHp| p IHp| ]; intros [q| q| ] H; simpl in *; 
    try discriminate H.
   (* p~1, q~1 *) 
-  destruct (IHp q H) as {r,U,V,W}; exists (r~0); rewrite ?U, ?V; auto.
+  destruct (IHp q H) as (r & U & V & W); exists (r~0); rewrite ?U, ?V; auto.
   repeat split; auto; right.
   destruct (ZL11 r) as [EQ|NE]; [|destruct W as [|W]; [elim NE; auto|]].
   rewrite ZL10; subst; auto.
   rewrite W; simpl; destruct r; auto; elim NE; auto.
   (* p~1, q~0 *)
   destruct (Pcompare_Gt_Gt _ _ H) as [H'|H']; clear H; rename H' into H.
-  destruct (IHp q H) as {r,U,V,W}; exists (r~1); rewrite ?U, ?V; auto.
+  destruct (IHp q H) as (r & U & V & W); exists (r~1); rewrite ?U, ?V; auto.
   exists 1; subst; rewrite Pminus_mask_diag; auto.
   (* p~1, 1 *)
   exists (p~0); auto.
   (* p~0, q~1 *)
-  destruct (IHp q (Pcompare_Lt_Gt _ _ H)) as {r,U,V,W}.
+  destruct (IHp q (Pcompare_Lt_Gt _ _ H)) as (r & U & V & W).
   destruct (ZL11 r) as [EQ|NE]; [|destruct W as [|W]; [elim NE; auto|]].
   exists 1; subst; rewrite ZL10, Pplus_one_succ_r; auto.
   exists ((Ppred r)~1); rewrite W, Pplus_carry_pred_eq_plus, V; auto.
   (* p~0, q~0 *)
-  destruct (IHp q H) as {r,U,V,W}; exists (r~0); rewrite ?U, ?V; auto.
+  destruct (IHp q H) as (r & U & V & W); exists (r~0); rewrite ?U, ?V; auto.
   repeat split; auto; right.
   destruct (ZL11 r) as [EQ|NE]; [|destruct W as [|W]; [elim NE; auto|]].
   rewrite ZL10; subst; auto.
@@ -1052,7 +1052,7 @@ Qed.
 Theorem Pplus_minus :
   forall p q:positive, (p ?= q) Eq = Gt -> q + (p - q) = p.
 Proof.
-  intros p q H; destruct (Pminus_mask_Gt p q H) as {r,U,V,_}.
+  intros p q H; destruct (Pminus_mask_Gt p q H) as (r & U & V & _).
   unfold Pminus; rewrite U; simpl; auto.
 Qed.
 
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index 591968a86..2996a5c91 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -1876,7 +1876,7 @@ Section Int31_Spec.
  simpl tail031_alt.
  case_eq (firstr x); intros.
  rewrite (inj_S (tail031_alt n (shiftr x))), Zpower_Zsucc; auto with zarith.
- destruct (IHn (shiftr x)) as {y,Hy1,Hy2}.
+ destruct (IHn (shiftr x)) as (y & Hy1 & Hy2).
  
  rewrite phi_nz; rewrite phi_nz in H; contradict H.
  rewrite (sneakl_shiftr x), H1, H; auto.
diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
index de7e4c6e8..b439462db 100644
--- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v
+++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
@@ -806,7 +806,7 @@ Section ZModulo.
 
  clear; induction p.
  exists (Zpos p); simpl; rewrite Pmult_1_r; auto with zarith.
- destruct IHp as {y,Yp,Ye}.
+ destruct IHp as (y & Yp & Ye).
  exists y.
  split; auto.
  change (Zpos p~0) with (2*Zpos p).