Fixing destruct/induction with a using clause on a non-inductive type,

that was broken by commit bf01856940 + use types from induction scheme
to restrict selection of pattern + accept matching from partially
applied term when using "using".

4 files changed, 89 insertions, 24 deletions

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 65d08609f..8b14feca0 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1410,7 +1410,7 @@ let default_matching_flags (sigma,_) =
 
 exception PatternNotFound
 
-let make_pattern_test from_prefix_of_ind env sigma (pending,c) =
+let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
   let flags = default_matching_flags pending in
   let n = List.length (snd (decompose_app c)) in
   let matching_fun _ t =
@@ -1427,12 +1427,8 @@ let make_pattern_test from_prefix_of_ind env sigma (pending,c) =
             applist (t,l1)
         else t in
       let sigma = w_typed_unify env sigma Reduction.CONV flags c t' in
-      let _ =
-        if from_prefix_of_ind then
-          (* We check that the subterm we found from prefix is applied *)
-          (* enough to be of inductive type *)
-          try ignore (Inductiveops.find_mrectype env sigma (Retyping.get_type_of env sigma t))
-          with UserError _ -> raise (NotUnifiable None) in
+      let ty = Retyping.get_type_of env sigma t in
+      if not (is_correct_type ty) then raise (NotUnifiable None);
       Some(sigma, t)
     with
     | PretypeError (_,_,CannotUnify (c1,c2,Some e)) ->
@@ -1526,7 +1522,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
 type prefix_of_inductive_support_flag = bool
 
 type abstraction_request =
-| AbstractPattern of prefix_of_inductive_support_flag * Name.t * pending_constr * clause or_like_first * bool
+| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Name.t * pending_constr * clause or_like_first * bool
 | AbstractExact of Name.t * constr * types option * clause * bool
 
 type abstraction_result =
@@ -1536,9 +1532,9 @@ type abstraction_result =
 
 let make_abstraction env evd ccl abs =
   match abs with
-  | AbstractPattern (from_prefix,name,c,occs,check_occs) ->
+  | AbstractPattern (from_prefix,check,name,c,occs,check_occs) ->
       make_abstraction_core name
-        (make_pattern_test from_prefix env evd c)
+        (make_pattern_test from_prefix check env evd c)
         env evd (snd c) None occs check_occs ccl
   | AbstractExact (name,c,ty,occs,check_occs) ->
       make_abstraction_core name
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 3b4998129..7f5cac2d2 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -65,8 +65,10 @@ val w_coerce_to_type : env -> evar_map -> constr -> types -> types ->
 
 exception PatternNotFound
 
+type prefix_of_inductive_support_flag = bool
+
 type abstraction_request =
-| AbstractPattern of bool * Names.Name.t * pending_constr * Locus.clause Locus.or_like_first * bool
+| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Names.Name.t * pending_constr * Locus.clause Locus.or_like_first * bool
 | AbstractExact of Names.Name.t * constr * types option * Locus.clause * bool
 
 val finish_evar_resolution : ?flags:Pretyping.inference_flags ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2f64fd351..009a1d2ac 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2254,7 +2254,8 @@ let letin_pat_tac with_eq id c occs =
     let env = Proofview.Goal.env gl in
     let sigma = Proofview.Goal.sigma gl in
     let ccl = Proofview.Goal.concl gl in
-    let abs = AbstractPattern (false,id,c,AtOccs occs,false) in
+    let check t = true in
+    let abs = AbstractPattern (false,check,id,c,AtOccs occs,false) in
     let (id,_,depdecls,lastlhyp,ccl,res) = make_abstraction env sigma ccl abs in
     let sigma,c = match res with
     | None -> finish_evar_resolution ~flags:(tactic_infer_flags false) env sigma c
@@ -3789,8 +3790,9 @@ let clear_induction_arg_if_hyp is_arg_pure_hyp c env =
   else
     env
 
-let make_body env sigma is_arg_pure_hyp c lbind t =
-  let mind,typ = reduce_to_quantified_ind env sigma t in
+let make_body env sigma (is_arg_pure_hyp,_) c lbind t =
+  let decls,t = splay_prod env sigma t in
+  let typ = it_mkProd t decls in
   let indclause = make_clenv_binding env sigma (c,typ) lbind in
   let env = clear_induction_arg_if_hyp is_arg_pure_hyp c env in
   let evdref = ref indclause.evd in
@@ -3811,7 +3813,37 @@ let make_body env sigma is_arg_pure_hyp c lbind t =
   (* side-effect *)
   (!evdref, c)
 
-let pose_induction_arg clear_flag isrec with_evars is_arg_pure_hyp elim
+let check_expected_type env sigma (elimc,bl) t =
+  (* Compute the expected template type of the term in case a using
+     clause is given *)
+  let elimt = typ_of env sigma elimc in
+  let sign,_ = splay_prod env sigma elimt in
+  let n = List.length sign in
+  if n == 0 then error "Scheme cannot be applied.";
+  let sigma,cl = make_evar_clause env sigma (Some (n-1)) elimt in
+  let sigma = solve_evar_clause env sigma true cl bl in
+  let (_,u,_) = destProd cl.cl_concl in
+  Evarconv.e_cumul env (ref sigma) t u
+
+let check_enough_applied env sigma elim =
+  (* A heuristic to decide whether the induction arg is enough applied *)
+  match elim with
+  | None ->
+      (* No eliminator given *)
+      fun u ->
+      let t,_ = decompose_app (whd_betadeltaiota env sigma u) in isInd t
+  | Some elimc ->
+      let elimt = typ_of env sigma (fst elimc) in
+      let scheme = compute_elim_sig ~elimc elimt in
+      fun u -> match scheme.indref with
+      | None ->
+         (* in the absence of information, do not assume it may be
+            partially applied *)
+          true
+      | Some gr ->
+          check_expected_type env sigma elimc u
+
+let pose_induction_arg clear_flag isrec with_evars info_arg elim
      id ((pending,(c0,lbind)),(eqname,names)) t inhyps cls =
   Proofview.Goal.nf_enter begin fun gl ->
   let env = Proofview.Goal.env gl in
@@ -3819,16 +3851,17 @@ let pose_induction_arg clear_flag isrec with_evars is_arg_pure_hyp elim
   Proofview.Refine.refine ~unsafe:true begin fun sigma ->
   let (sigma',c') = use_bindings env sigma (c0,lbind) t in
   let occs = match cls with None -> LikeFirst | Some occs -> AtOccs occs in
-  let abs = AbstractPattern (true,Name id,(pending,c'),occs,false) in
+  let check = check_enough_applied env sigma elim in
+  let abs = AbstractPattern (snd info_arg,check,Name id,(pending,c'),occs,false) in
   let (id,sign,_,lastlhyp,ccl,res) = make_abstraction env sigma' ccl abs in
   match res with
   | None ->
       (* pattern not found *)
       let (sigma,c0) = finish_evar_resolution ~flags:(tactic_infer_flags with_evars) env sigma (pending,c0) in
-      let (sigma,c) = make_body env sigma is_arg_pure_hyp c0 lbind t in
+      let (sigma,c) = make_body env sigma info_arg c0 lbind t in
       let t = Retyping.get_type_of env sigma c in
       let with_eq = Option.map (fun eq -> (false,eq)) eqname in
-      let env = clear_induction_arg_if_hyp is_arg_pure_hyp c0 env in
+      let env = clear_induction_arg_if_hyp (fst info_arg) c0 env in
       mkletin_goal env sigma with_eq false (id,lastlhyp,ccl,c) (Some t)
 
   | Some (sigma',c) ->
@@ -3840,9 +3873,6 @@ let pose_induction_arg clear_flag isrec with_evars is_arg_pure_hyp elim
   end
 end
 
-let isIndType env sigma t =
-  try let _ = find_mrectype env sigma t in true with Not_found -> false
-
 let induction_gen clear_flag isrec with_evars elim
     ((_pending,(c,lbind)),(eqname,names) as arg) cls =
   let inhyps = match cls with
@@ -3856,7 +3886,8 @@ let induction_gen clear_flag isrec with_evars elim
     isVar c && not (mem_named_context (destVar c) (Global.named_context()))
     && lbind == NoBindings && not with_evars && Option.is_empty eqname
     && not (has_selected_occurrences cls) in
-  if is_arg_pure_hyp && isIndType env sigma t then
+  let enough_applied = check_enough_applied env sigma elim t in
+  if is_arg_pure_hyp && enough_applied then
     (* First case: induction on a variable already in an inductive type and
        with maximal abstraction over the variable.
        This is a situation where the induction argument is a
@@ -3874,11 +3905,12 @@ let induction_gen clear_flag isrec with_evars elim
     (* Type not the right one if partially applied but anyway for internal use*)
       let x = id_of_name_using_hdchar (Global.env()) t Anonymous in
       new_fresh_id [] x gl in
+    let info_arg = (is_arg_pure_hyp, not enough_applied) in
     if isrec then
       (* Historically, induction has side conditions last *)
       Tacticals.New.tclTHENFIRST
         (Tacticals.New.tclTHENLIST [
-          pose_induction_arg clear_flag isrec with_evars is_arg_pure_hyp elim id arg t inhyps cls;
+          pose_induction_arg clear_flag isrec with_evars info_arg elim id arg t inhyps cls;
           if with_evars
              (* do not give a success semantics to edestruct on an
                 open term yet *)
@@ -3893,7 +3925,7 @@ let induction_gen clear_flag isrec with_evars elim
       (* Historically, destruct has side conditions first *)
       Tacticals.New.tclTHENLAST
         (Tacticals.New.tclTHENLIST [
-          pose_induction_arg clear_flag isrec with_evars is_arg_pure_hyp elim id arg t inhyps cls;
+          pose_induction_arg clear_flag isrec with_evars info_arg elim id arg t inhyps cls;
           if with_evars
              (* do not give a success semantics to edestruct on an
                 open term yet *)
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 314b612e1..a3b4b192e 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -200,3 +200,38 @@ edestruct (H _ _).
 - apply (eq_refl x).
 Qed.
 *)
+Abort.
+
+(* Test selection when not in an inductive type *)
+Parameter A:Type.
+Axiom elim: forall P, A -> P.
+Goal forall a:A, a = a.
+induction a using elim.
+Qed.
+
+Goal forall a:nat -> A, a 0 = a 1.
+intro a.
+induction (a 0) using elim.
+Qed.
+
+(* From Oct 2014, a subterm is found, as if without "using"; in 8.4,
+   it did not find a subterm *)
+
+Goal forall a:nat -> A, a 0 = a 1.
+intro a.
+induction a using elim.
+Qed.
+
+Goal forall a:nat -> A, forall b, a 0 = b.
+intros a b.
+induction a using elim.
+Qed.
+
+(* From Oct 2014, first subterm is found; in 8.4, it failed because it
+   found "a 0" and wanted to clear a *)
+
+Goal forall a:nat -> nat, a 0 = a 1.
+intro a.
+destruct a.
+change (0 = a 1).
+Abort.