Stronger invariants on the use of the introduction pattern (pat1,...,patn).

The length of the pattern should now be exactly the number of
assumptions and definitions introduced by the destruction or induction,
including the induction hypotheses in case of an induction.

Like for pattern-matching, the local definitions in the argument of
the constructor can be skipped in which case a name is automatically
created for these.

7 files changed, 120 insertions, 64 deletions

diff --git a/tactics/inv.ml b/tactics/inv.ml
index 3574990f6c..01124e867c 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -296,17 +296,17 @@ let get_names (allow_conj,issimple) (loc, pat as x) = match pat with
       error "Discarding pattern not allowed for inversion equations."
   | IntroAction (IntroRewrite _) ->
       error "Rewriting pattern not allowed for inversion equations."
-  | IntroAction (IntroOrAndPattern [[]]) when allow_conj -> (None, [])
-  | IntroAction (IntroOrAndPattern [(_,IntroNaming (IntroIdentifier id)) :: _ as l])
+  | IntroAction (IntroOrAndPattern (IntroAndPattern [])) when allow_conj -> (None, [])
+  | IntroAction (IntroOrAndPattern (IntroAndPattern ((_,IntroNaming (IntroIdentifier id)) :: _ as l)))
       when allow_conj -> (Some id,l)
-  | IntroAction (IntroOrAndPattern [_]) ->
+  | IntroAction (IntroOrAndPattern (IntroAndPattern _)) ->
       if issimple then
         error"Conjunctive patterns not allowed for simple inversion equations."
       else
         error"Nested conjunctive patterns not allowed for inversion equations."
   | IntroAction (IntroInjection l) ->
       error "Injection patterns not allowed for inversion equations."
-  | IntroAction (IntroOrAndPattern l) ->
+  | IntroAction (IntroOrAndPattern (IntroOrPattern _)) ->
       error "Disjunctive patterns not allowed for inversion equations."
   | IntroAction (IntroApplyOn (c,pat)) ->
       error "Apply patterns not allowed for inversion equations."
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 14e0fed31d..f92213da81 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -258,8 +258,11 @@ and intern_intro_pattern_action lf ist = function
   | IntroApplyOn (c,pat) ->
       IntroApplyOn (intern_constr ist c, intern_intro_pattern lf ist pat)
 
-and intern_or_and_intro_pattern lf ist =
-  List.map (List.map (intern_intro_pattern lf ist))
+and intern_or_and_intro_pattern lf ist = function
+   | IntroAndPattern l ->
+      IntroAndPattern (List.map (intern_intro_pattern lf ist) l)
+  | IntroOrPattern ll ->
+      IntroOrPattern (List.map (List.map (intern_intro_pattern lf ist)) ll)
 
 let intern_or_and_intro_pattern_loc lf ist = function
   | ArgVar (_,id) as x ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 8db91c07f6..a6991691fb 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -511,7 +511,9 @@ let extract_ltac_constr_values ist env =
 (* Extract the identifier list from lfun: join all branches (what to do else?)*)
 let rec intropattern_ids (loc,pat) = match pat with
   | IntroNaming (IntroIdentifier id) -> [id]
-  | IntroAction (IntroOrAndPattern ll) ->
+  | IntroAction (IntroOrAndPattern (IntroAndPattern l)) ->
+      List.flatten (List.map intropattern_ids l)
+  | IntroAction (IntroOrAndPattern (IntroOrPattern ll)) ->
       List.flatten (List.map intropattern_ids (List.flatten ll))
   | IntroAction (IntroInjection l) ->
       List.flatten (List.map intropattern_ids l)
@@ -940,8 +942,13 @@ and interp_intro_pattern_action ist env sigma = function
       sigma, IntroApplyOn (c,ipat)
   | IntroWildcard | IntroRewrite _ as x -> sigma, x
 
-and interp_or_and_intro_pattern ist env sigma =
-  List.fold_map (interp_intro_pattern_list_as_list ist env) sigma
+and interp_or_and_intro_pattern ist env sigma = function
+  | IntroAndPattern l ->
+      let sigma, l = List.fold_map (interp_intro_pattern ist env) sigma l in
+      sigma, IntroAndPattern l
+  | IntroOrPattern ll ->
+      let sigma, ll = List.fold_map (interp_intro_pattern_list_as_list ist env) sigma ll in
+      sigma, IntroOrPattern ll
 
 and interp_intro_pattern_list_as_list ist env sigma = function
   | [loc,IntroNaming (IntroIdentifier id)] as l ->
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index c74f6093a2..e09360a6a6 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -54,10 +54,16 @@ and subst_intro_pattern_action subst = function
   | IntroApplyOn (t,pat) ->
       IntroApplyOn (subst_glob_constr subst t,subst_intro_pattern subst pat)
   | IntroOrAndPattern l ->
-      IntroOrAndPattern (List.map (List.map (subst_intro_pattern subst)) l)
+      IntroOrAndPattern (subst_intro_or_and_pattern subst l)
   | IntroInjection l -> IntroInjection (List.map (subst_intro_pattern subst) l)
   | IntroWildcard | IntroRewrite _ as x -> x
 
+and subst_intro_or_and_pattern subst = function
+  | IntroAndPattern l ->
+      IntroAndPattern (List.map (subst_intro_pattern subst) l)
+  | IntroOrPattern ll ->
+      IntroOrPattern (List.map (List.map (subst_intro_pattern subst)) ll)
+
 let subst_induction_arg subst = function
   | clear,ElimOnConstr c -> clear,ElimOnConstr (subst_glob_with_bindings subst c)
   | clear,ElimOnAnonHyp n as x -> x
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 061c05b9b2..4029d1fcca 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -147,51 +147,85 @@ type branch_args = {
   largs      : constr list; (* its arguments *)
   branchnum  : int;         (* the branch number *)
   pred       : constr;      (* the predicate we used *)
-  nassums    : int;         (* the number of assumptions to be introduced *)
+  nassums    : int;         (* number of assumptions/letin to be introduced *)
   branchsign : bool list;   (* the signature of the branch.
-                               true=recursive argument, false=constant *)
+                               true=assumption, false=let-in *)
   branchnames : Tacexpr.intro_patterns}
 
 type branch_assumptions = {
   ba        : branch_args;       (* the branch args *)
   assums    : Context.Named.t}   (* the list of assumptions introduced *)
 
+open Misctypes
+
 let fix_empty_or_and_pattern nv l =
   (* 1- The syntax does not distinguish between "[ ]" for one clause with no
      names and "[ ]" for no clause at all *)
   (* 2- More generally, we admit "[ ]" for any disjunctive pattern of
      arbitrary length *)
   match l with
-  | [[]] -> List.make nv []
+  | IntroOrPattern [[]] -> IntroOrPattern (List.make nv [])
   | _ -> l
 
-let check_or_and_pattern_size loc names n =
-  if not (Int.equal (List.length names) n) then
-    if Int.equal n 1 then
-      user_err_loc (loc,"",str "Expects a conjunctive pattern.")
-    else
-      user_err_loc (loc,"",str "Expects a disjunctive pattern with " ++ int n
-	++ str " branches.")
-
-let compute_induction_names n = function
+let check_or_and_pattern_size loc names branchsigns =
+  let n = Array.length branchsigns in
+  let msg p1 p2 = strbrk "a conjunctive pattern made of " ++ int p1 ++ (if p1 == p2 then mt () else str " or " ++ int p2) ++ str " patterns" in
+  let err1 p1 p2 =
+    user_err_loc (loc,"",str "Expects " ++ msg p1 p2 ++ str ".") in
+  let errn n =
+    user_err_loc (loc,"",str "Expects a disjunctive pattern with " ++ int n
+	++ str " branches.") in
+  let err1' p1 p2 =
+    user_err_loc (loc,"",strbrk "Expects a disjunctive pattern with 1 branch or " ++ msg p1 p2 ++ str ".") in
+  match names with
+  | IntroAndPattern l ->
+      if not (Int.equal n 1) then errn n;
+      let p1 = List.count (fun x -> x) branchsigns.(0) in
+      let p2 = List.length branchsigns.(0) in
+      let p = List.length l in
+      if not (Int.equal p p1 || Int.equal p p2) ||
+         not (List.for_all (function _,IntroNaming _ | _,IntroAction _ -> true | _,IntroForthcoming _ -> false) l) then err1 p1 p2;
+      if Int.equal p p1 then
+        IntroAndPattern
+          (List.extend branchsigns.(0) (Loc.ghost,IntroNaming IntroAnonymous) l)
+      else
+        names
+  | IntroOrPattern ll ->
+      if not (Int.equal n (List.length ll)) then
+        if Int.equal n 1 then
+          let p1 = List.count (fun x -> x) branchsigns.(0) in
+          let p2 = List.length branchsigns.(0) in
+          err1' p1 p2 else errn n;
+      names
+
+let get_and_check_or_and_pattern loc names branchsigns =
+  let names = check_or_and_pattern_size loc names branchsigns in
+  match names with
+  | IntroAndPattern l -> [|l|]
+  | IntroOrPattern l -> Array.of_list l
+
+let compute_induction_names branchletsigns = function
   | None ->
-      Array.make n []
+      Array.make (Array.length branchletsigns) []
   | Some (loc,names) ->
-      let names = fix_empty_or_and_pattern n names in
-      check_or_and_pattern_size loc names n;
-      Array.of_list names
+      let names = fix_empty_or_and_pattern (Array.length branchletsigns) names in
+      get_and_check_or_and_pattern loc names branchletsigns
 
-let compute_construtor_signatures isrec ((_,k as ity),u) =
+(* Compute the let-in signature of case analysis or standard induction scheme *)
+let compute_constructor_signatures isrec ((_,k as ity),u) =
   let rec analrec c recargs =
     match kind_of_term c, recargs with
     | Prod (_,_,c), recarg::rest ->
-	let b = match Declareops.dest_recarg recarg with
-	  | Norec | Imbr _  -> false
-	  | Mrec (_,j)  -> isrec && Int.equal j k
-	in b :: (analrec c rest)
-    | LetIn (_,_,_,c), rest -> false :: (analrec c rest)
+        let rest = analrec c rest in
+        begin match Declareops.dest_recarg recarg with
+        | Norec | Imbr _  -> true :: rest
+        | Mrec (_,j)  ->
+            if isrec && Int.equal j k then true :: true :: rest
+            else true :: rest
+        end
+    | LetIn (_,_,_,c), rest -> false :: analrec c rest
     | _, [] -> []
-    | _ -> anomaly (Pp.str "compute_construtor_signatures")
+    | _ -> anomaly (Pp.str "compute_constructor_signatures")
   in
   let (mib,mip) = Global.lookup_inductive ity in
   let n = mib.mind_nparams in
@@ -596,8 +630,8 @@ module New = struct
             (str "The elimination combinator " ++ str name_elim ++ str " is unknown.")
     in
     let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in
-    let branchsigns = compute_construtor_signatures isrec ind in
-    let brnames = compute_induction_names (Array.length branchsigns) allnames in
+    let branchsigns = compute_constructor_signatures isrec ind in
+    let brnames = compute_induction_names branchsigns allnames in
     let flags = Unification.elim_flags () in
     let elimclause' =
       match predicate with
@@ -609,10 +643,7 @@ module New = struct
       let (hd,largs) = decompose_app clenv'.templtyp.Evd.rebus in
       let ba = { branchsign = branchsigns.(i);
                  branchnames = brnames.(i);
-                 nassums =
-          List.fold_left
-            (fun acc b -> if b then acc+2 else acc+1)
-            0 branchsigns.(i);
+                 nassums = List.length branchsigns.(i);
                  branchnum = i+1;
                  ity = ind;
                  largs = List.map (clenv_nf_meta clenv') largs;
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 147f1f0f20..4f6f87f698 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -102,28 +102,32 @@ type branch_args = {
   largs      : constr list; (** its arguments *)
   branchnum  : int;         (** the branch number *)
   pred       : constr;      (** the predicate we used *)
-  nassums    : int;         (** the number of assumptions to be introduced *)
+  nassums    : int;         (** number of assumptions/letin to be introduced *)
   branchsign : bool list;   (** the signature of the branch.
-                                true=recursive argument, false=constant *)
+                                true=assumption, false=let-in *)
   branchnames : intro_patterns}
 
 type branch_assumptions = {
   ba        : branch_args;       (** the branch args *)
   assums    : Context.Named.t}   (** the list of assumptions introduced *)
 
-(** [check_disjunctive_pattern_size loc pats n] returns an appropriate 
-   error message if |pats| <> n *)
-val check_or_and_pattern_size :
-  Loc.t -> delayed_open_constr or_and_intro_pattern_expr -> int -> unit
+(** [check_disjunctive_pattern_size loc pats n] returns an appropriate
+   error message if |pats| <> n; extends them if no pattern is given
+   for let-ins in the case of a conjunctive pattern *)
+val get_and_check_or_and_pattern : 
+  Loc.t -> delayed_open_constr or_and_intro_pattern_expr ->
+  bool list array -> intro_patterns array
 
 (** Tolerate "[]" to mean a disjunctive pattern of any length *)
 val fix_empty_or_and_pattern : int -> 
   delayed_open_constr or_and_intro_pattern_expr ->
   delayed_open_constr or_and_intro_pattern_expr
 
+val compute_constructor_signatures : rec_flag -> pinductive -> bool list array
+
 (** Useful for [as intro_pattern] modifier *)
 val compute_induction_names :
-  int -> or_and_intro_pattern option -> intro_patterns array
+  bool list array -> or_and_intro_pattern option -> intro_patterns array
 
 val elimination_sort_of_goal : goal sigma -> sorts_family
 val elimination_sort_of_hyp  : Id.t -> goal sigma -> sorts_family
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f0f46c14db..796cea98f8 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2089,14 +2089,15 @@ let intro_or_and_pattern loc bracketed ll thin tac id =
   Proofview.Goal.enter { enter = begin fun gl ->
   let c = mkVar id in
   let t = Tacmach.New.pf_unsafe_type_of gl c in
-  let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in
-  let nv = constructors_nrealdecls ind in
-  let ll = fix_empty_or_and_pattern (Array.length nv) ll in
-  check_or_and_pattern_size loc ll (Array.length nv);
+  let (ind,t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in
+  let branchsigns = compute_constructor_signatures false ind in
+  let nv_with_let = Array.map List.length branchsigns in
+  let ll = fix_empty_or_and_pattern (Array.length branchsigns) ll in
+  let ll = get_and_check_or_and_pattern loc ll branchsigns in
   Tacticals.New.tclTHENLASTn
     (Tacticals.New.tclTHEN (simplest_case c) (Proofview.V82.tactic (clear [id])))
     (Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l)
-       nv (Array.of_list ll))
+       nv_with_let ll)
   end }
 
 let rewrite_hyp assert_style l2r id =
@@ -2137,7 +2138,8 @@ let prepare_naming loc = function
 let rec explicit_intro_names = function
 | (_, IntroForthcoming _) :: l -> explicit_intro_names l
 | (_, IntroNaming (IntroIdentifier id)) :: l -> id :: explicit_intro_names l
-| (_, IntroAction (IntroOrAndPattern ll)) :: l' ->
+| (_, IntroAction (IntroOrAndPattern l)) :: l' ->
+    let ll = match l with IntroAndPattern l -> [l] | IntroOrPattern ll -> ll in
     List.flatten (List.map (fun l -> explicit_intro_names (l@l')) ll)
 | (_, IntroAction (IntroInjection l)) :: l' ->
     explicit_intro_names (l@l')
@@ -2842,8 +2844,8 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
   let avoid = avoid @ avoid' in
   let rec peel_tac ra dests names thin =
     match ra with
-    | (RecArg,deprec,recvarname) ::
-        (IndArg,depind,hyprecname) :: ra' ->
+    | (RecArg,_,deprec,recvarname) ::
+        (IndArg,_,depind,hyprecname) :: ra' ->
         Proofview.Goal.enter { enter = begin fun gl ->
         let (recpat,names) = match names with
           | [loc,IntroNaming (IntroIdentifier id) as pat] ->
@@ -2860,7 +2862,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
 	    peel_tac ra' (update_dest dests ids') names thin)
         end })
         end }
-    | (IndArg,dep,hyprecname) :: ra' ->
+    | (IndArg,_,dep,hyprecname) :: ra' ->
         Proofview.Goal.enter { enter = begin fun gl ->
 	(* Rem: does not happen in Coq schemes, only in user-defined schemes *)
         let pat,names =
@@ -2868,7 +2870,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
 	dest_intro_patterns avoid thin MoveLast [pat] (fun ids thin ->
         peel_tac ra' (update_dest dests ids) names thin)
         end }
-    | (RecArg,dep,recvarname) :: ra' ->
+    | (RecArg,_,dep,recvarname) :: ra' ->
         Proofview.Goal.enter { enter = begin fun gl ->
         let (pat,names) =
           consume_pattern avoid (Name recvarname) dep gl names in
@@ -2876,7 +2878,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
 	dest_intro_patterns avoid thin dest [pat] (fun ids thin ->
         peel_tac ra' dests names thin)
         end }
-    | (OtherArg,dep,_) :: ra' ->
+    | (OtherArg,_,dep,_) :: ra' ->
         Proofview.Goal.enter { enter = begin fun gl ->
         let (pat,names) = consume_pattern avoid Anonymous dep gl names in
         let dest = get_recarg_dest dests in
@@ -3682,9 +3684,9 @@ let compute_scheme_signature scheme names_info ind_type_guess =
   let rec check_branch p c =
     match kind_of_term c with
       | Prod (_,t,c) ->
-	(is_pred p t, dependent (mkRel 1) c) :: check_branch (p+1) c
+	(is_pred p t, true, dependent (mkRel 1) c) :: check_branch (p+1) c
       | LetIn (_,_,_,c) ->
-	(OtherArg, dependent (mkRel 1) c) :: check_branch (p+1) c
+	(OtherArg, false, dependent (mkRel 1) c) :: check_branch (p+1) c
       | _ when is_pred p c == IndArg -> []
       | _ -> raise Exit
   in
@@ -3694,12 +3696,12 @@ let compute_scheme_signature scheme names_info ind_type_guess =
 	(try
 	   let lchck_brch = check_branch p t in
 	   let n = List.fold_left
-	     (fun n (b,_) -> if b == RecArg then n+1 else n) 0 lchck_brch in
+	     (fun n (b,_,_) -> if b == RecArg then n+1 else n) 0 lchck_brch in
 	   let recvarname, hyprecname, avoid =
 	     make_up_names n scheme.indref names_info in
 	   let namesign =
-	     List.map (fun (b,dep) ->
-	       (b, dep, if b == IndArg then hyprecname else recvarname))
+	     List.map (fun (b,is_assum,dep) ->
+	       (b,is_assum,dep,if b == IndArg then hyprecname else recvarname))
 	       lchck_brch in
 	   (avoid,namesign) :: find_branches (p+1) brs
 	 with Exit-> error_ind_scheme "the branches of")
@@ -3744,7 +3746,7 @@ let given_elim hyp0 (elimc,lbind as e) gl =
   Tacmach.New.project gl, (e, Tacmach.New.pf_unsafe_type_of gl elimc), ind_type_guess
 
 type scheme_signature =
-    (Id.t list * (elim_arg_kind * bool * Id.t) list) array
+    (Id.t list * (elim_arg_kind * bool * bool * Id.t) list) array
 
 type eliminator_source =
   | ElimUsing of (eliminator * types) * scheme_signature
@@ -3865,7 +3867,10 @@ let apply_induction_in_context hyp0 inhyps elim indvars names induct_tac =
       List.fold_left
         (fun a (id,b,_) -> if Option.is_empty b then (mkVar id)::a else a) [] deps in
     let (sigma, isrec, elim, indsign) = get_eliminator elim dep s (Proofview.Goal.assume gl) in
-    let names = compute_induction_names (Array.length indsign) names in
+    let branchletsigns =
+      let f (_,is_not_let,_,_) = is_not_let in
+      Array.map (fun (_,l) -> List.map f l) indsign in
+    let names = compute_induction_names branchletsigns names in
     let tac =
     (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn)
       (Tacticals.New.tclTHENLIST [