Fixes #10812: tactic subst failure with section variables indirectly dependent in goal

doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst

@@ -0,0 +1,9 @@
+- **Changed:**
+  Tactic :tacn:`subst` :n:`@ident` now fails over a section variable which is
+  indirectly dependent in the goal; the incompatibility can generally
+  be fixed by first clearing the hypotheses causing an indirect
+  dependency, as reported by the error message, or by using :tacn:`rewrite` :n:`in *`
+  instead; similarly, :tacn:`subst` has no more effect on such variables
+  (`#12146 <https://github.com/coq/coq/pull/12146>`_,
+  by Hugo Herbelin; fixes `#10812 <https://github.com/coq/coq/pull/10812>`_;
+  fixes `#12139 <https://github.com/coq/coq/pull/12139>`_).

doc/sphinx/proof-engine/tactics.rst

@@ -2832,6 +2832,11 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
    If :n:`@ident` is a local definition of the form :n:`@ident := t`, it is also
    unfolded and cleared.
 
+   If :n:`@ident` is a section variable it is expected to have no
+   indirect occurrences in the goal, i.e. that no global declarations
+   implicitly depending on the section variable must be present in the
+   goal.
+
    .. note::
       + When several hypotheses have the form :n:`@ident = t` or :n:`t = @ident`, the
         first one is used.
@@ -2845,9 +2850,11 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
 
    .. tacv:: subst
 
-      This applies subst repeatedly from top to bottom to all identifiers of the
+      This applies :tacn:`subst` repeatedly from top to bottom to all hypotheses of the
       context for which an equality of the form :n:`@ident = t` or :n:`t = @ident`
-      or :n:`@ident := t` exists, with :n:`@ident` not occurring in ``t``.
+      or :n:`@ident := t` exists, with :n:`@ident` not occurring in
+      ``t`` and :n:`@ident` not a section variable with indirect
+      dependencies in the goal.
 
    .. flag:: Regular Subst Tactic
 
@@ -2873,6 +2880,15 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
       hypotheses, which without the flag it may break.
       default.
 
+   .. exn:: Cannot find any non-recursive equality over :n:`@ident`.
+      :undocumented:
+
+   .. exn:: Section variable :n:`@ident` occurs implicitly in global declaration :n:`@qualid` present in hypothesis :n:`@ident`.
+            Section variable :n:`@ident` occurs implicitly in global declaration :n:`@qualid` present in the conclusion.
+
+      Raised when the variable is a section variable with indirect
+      dependencies in the goal.
+
 
 .. tacn:: stepl @term
    :name: stepl

engine/termops.ml

@@ -803,23 +803,29 @@ let occur_evar sigma n c =
 
 let occur_in_global env id constr =
   let vars = vars_of_global env constr in
-  if Id.Set.mem id vars then raise Occur
+  Id.Set.mem id vars
 
 let occur_var env sigma id c =
   let rec occur_rec c =
     match EConstr.destRef sigma c with
-    | gr, _ -> occur_in_global env id gr
+    | gr, _ -> if occur_in_global env id gr then raise Occur
     | exception DestKO -> EConstr.iter sigma occur_rec c
   in
   try occur_rec c; false with Occur -> true
 
+exception OccurInGlobal of GlobRef.t
+
+let occur_var_indirectly env sigma id c =
+  let var = GlobRef.VarRef id in
+  let rec occur_rec c =
+    match EConstr.destRef sigma c with
+    | gr, _ -> if not (GlobRef.equal gr var) && occur_in_global env id gr then raise (OccurInGlobal gr)
+    | exception DestKO -> EConstr.iter sigma occur_rec c
+  in
+  try occur_rec c; None with OccurInGlobal gr -> Some gr
+
 let occur_var_in_decl env sigma hyp decl =
-  let open NamedDecl in
-  match decl with
-    | LocalAssum (_,typ) -> occur_var env sigma hyp typ
-    | LocalDef (_, body, typ) ->
-        occur_var env sigma hyp typ ||
-        occur_var env sigma hyp body
+  NamedDecl.exists (occur_var env sigma hyp) decl
 
 let local_occur_var sigma id c =
   let rec occur c = match EConstr.kind sigma c with
@@ -828,6 +834,9 @@ let local_occur_var sigma id c =
   in
   try occur c; false with Occur -> true
 
+let local_occur_var_in_decl sigma hyp decl =
+  NamedDecl.exists (local_occur_var sigma hyp) decl
+
   (* returns the list of free debruijn indices in a term *)
 
 let free_rels sigma m =

engine/termops.mli

@@ -92,12 +92,14 @@ val occur_meta_or_existential : Evd.evar_map -> constr -> bool
 val occur_metavariable : Evd.evar_map -> metavariable -> constr -> bool
 val occur_evar : Evd.evar_map -> Evar.t -> constr -> bool
 val occur_var : env -> Evd.evar_map -> Id.t -> constr -> bool
+val occur_var_indirectly : env -> Evd.evar_map -> Id.t -> constr -> GlobRef.t option
 val occur_var_in_decl :
   env -> Evd.evar_map ->
   Id.t -> named_declaration -> bool
 
 (** As {!occur_var} but assume the identifier not to be a section variable *)
 val local_occur_var : Evd.evar_map -> Id.t -> constr -> bool
+val local_occur_var_in_decl : Evd.evar_map -> Id.t -> named_declaration -> bool
 
 val free_rels : Evd.evar_map -> constr -> Int.Set.t
 

tactics/equality.ml

@@ -1707,12 +1707,42 @@ let is_eq_x gl x d =
   with Constr_matching.PatternMatchingFailure ->
     ()
 
+exception FoundDepInGlobal of Id.t option * GlobRef.t
+
+let test_non_indirectly_dependent_section_variable gl x =
+  let env = Proofview.Goal.env gl in
+  let sigma = Tacmach.New.project gl in
+  let hyps = Proofview.Goal.hyps gl in
+  let concl = Proofview.Goal.concl gl in
+  List.iter (fun decl ->
+    NamedDecl.iter_constr (fun c ->
+      match occur_var_indirectly env sigma x c with
+      | Some gr -> raise (FoundDepInGlobal (Some (NamedDecl.get_id decl), gr))
+      | None -> ()) decl) hyps;
+  match occur_var_indirectly env sigma x concl with
+    | Some gr -> raise (FoundDepInGlobal (None, gr))
+    | None -> ()
+
+let check_non_indirectly_dependent_section_variable gl x =
+  try test_non_indirectly_dependent_section_variable gl x
+  with FoundDepInGlobal (pos,gr) ->
+    let where = match pos with
+      | Some id -> str "hypothesis " ++ Id.print id
+      | None -> str "the conclusion of the goal" in
+    user_err ~hdr:"Subst"
+      (strbrk "Section variable " ++ Id.print x ++
+       strbrk " occurs implicitly in global declaration " ++ Printer.pr_global gr ++
+       strbrk " present in " ++ where ++ strbrk ".")
+
+let is_non_indirectly_dependent_section_variable gl z =
+  try test_non_indirectly_dependent_section_variable gl z; true
+  with FoundDepInGlobal (pos,gr) -> false
+
 (* Rewrite "hyp:x=rhs" or "hyp:rhs=x" (if dir=false) everywhere and
    erase hyp and x; proceed by generalizing all dep hyps *)
 
 let subst_one dep_proof_ok x (hyp,rhs,dir) =
   Proofview.Goal.enter begin fun gl ->
-  let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
   let hyps = Proofview.Goal.hyps gl in
   let concl = Proofview.Goal.concl gl in
@@ -1721,7 +1751,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
     List.rev (pi3 (List.fold_right (fun dcl (dest,deps,allhyps) ->
       let id = NamedDecl.get_id dcl in
       if not (Id.equal id hyp)
-         && List.exists (fun y -> occur_var_in_decl env sigma y dcl) deps
+         && List.exists (fun y -> local_occur_var_in_decl sigma y dcl) deps
       then
         let id_dest = if !regular_subst_tactic then dest else MoveLast in
         (dest,id::deps,(id_dest,id)::allhyps)
@@ -1730,7 +1760,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
       hyps
       (MoveBefore x,[x],[]))) in (* In practice, no dep hyps before x, so MoveBefore x is good enough *)
   (* Decides if x appears in conclusion *)
-  let depconcl = occur_var env sigma x concl in
+  let depconcl = local_occur_var sigma x concl in
   let need_rewrite = not (List.is_empty dephyps) || depconcl in
   tclTHENLIST
     ((if need_rewrite then
@@ -1761,6 +1791,8 @@ let subst_one_var dep_proof_ok x =
             (str "Cannot find any non-recursive equality over " ++ Id.print x ++
                str".")
         with FoundHyp res -> res in
+      if is_section_variable x then
+        check_non_indirectly_dependent_section_variable gl x;
       subst_one dep_proof_ok x res
   end
 
@@ -1794,53 +1826,37 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
 
   if !regular_subst_tactic then
 
-  (* First step: find hypotheses to treat in linear time *)
-  let find_equations gl =
-    let env = Proofview.Goal.env gl in
-    let sigma = project gl in
-    let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in
-    let select_equation_name decl =
+    (* Find hypotheses to treat in linear time *)
+    let process hyp =
+      Proofview.Goal.enter begin fun gl ->
+      let env = Proofview.Goal.env gl in
+      let sigma = project gl in
+      let c = pf_get_hyp hyp gl |> NamedDecl.get_type in
       try
-        let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in
+        let lbeq,u,(_,x,y) = pf_apply find_eq_data_decompose gl c in
         let u = EInstance.kind sigma u in
         let eq = Constr.mkRef (lbeq.eq,u) in
         if flags.only_leibniz then restrict_to_eq_and_identity eq;
         match EConstr.kind sigma x, EConstr.kind sigma y with
-        | Var z, _  when not (is_evaluable env (EvalVarRef z)) ->
-            Some (NamedDecl.get_id decl)
-        | _, Var z when not (is_evaluable env (EvalVarRef z)) ->
-            Some (NamedDecl.get_id decl)
+        | Var x, Var y when Id.equal x y ->
+            Proofview.tclUNIT ()
+        | Var x', _ when not (Termops.local_occur_var sigma x' y) &&
+                        not (is_evaluable env (EvalVarRef x')) &&
+                        is_non_indirectly_dependent_section_variable gl x' ->
+            subst_one flags.rewrite_dependent_proof x' (hyp,y,true)
+        | _, Var y' when not (Termops.local_occur_var sigma y' x) &&
+                        not (is_evaluable env (EvalVarRef y')) &&
+                        is_non_indirectly_dependent_section_variable gl y' ->
+            subst_one flags.rewrite_dependent_proof y' (hyp,x,false)
         | _ ->
-            None
-      with Constr_matching.PatternMatchingFailure -> None
+            Proofview.tclUNIT ()
+      with Constr_matching.PatternMatchingFailure ->
+         Proofview.tclUNIT ()
+        end
     in
-    let hyps = Proofview.Goal.hyps gl in
-    List.rev (List.map_filter select_equation_name hyps)
-  in
-
-  (* Second step: treat equations *)
-  let process hyp =
     Proofview.Goal.enter begin fun gl ->
-    let sigma = project gl in
-    let env = Proofview.Goal.env gl in
-    let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in
-    let c = pf_get_hyp hyp gl |> NamedDecl.get_type in
-    let _,_,(_,x,y) = find_eq_data_decompose c in
-    (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
-    if EConstr.eq_constr sigma x y then Proofview.tclUNIT () else
-      match EConstr.kind sigma x, EConstr.kind sigma y with
-      | Var x', _ when not (Termops.local_occur_var sigma x' y) && not (is_evaluable env (EvalVarRef x')) ->
-          subst_one flags.rewrite_dependent_proof x' (hyp,y,true)
-      | _, Var y' when not (Termops.local_occur_var sigma y' x) && not (is_evaluable env (EvalVarRef y')) ->
-          subst_one flags.rewrite_dependent_proof y' (hyp,x,false)
-      | _ ->
-          Proofview.tclUNIT ()
+      tclMAP process (List.rev (List.map NamedDecl.get_id (Proofview.Goal.hyps gl)))
     end
-  in
-  Proofview.Goal.enter begin fun gl ->
-    let ids = find_equations gl in
-    tclMAP process ids
-  end
 
   else
 

test-suite/bugs/closed/bug_10812.v

@@ -0,0 +1,28 @@
+(* subst with indirectly dependent section variables *)
+
+Section A.
+
+Variable a:nat.
+Definition b := a.
+
+Goal a=1 -> a+a=1 -> b=1.
+intros.
+Fail subst a. (* was working; we make it failing *)
+rewrite H in H0.
+discriminate.
+Qed.
+
+Goal a=1 -> a+a=1 -> b=1.
+intros.
+subst. (* should not apply to a *)
+rewrite H in H0.
+discriminate.
+Qed.
+
+Goal forall t, a=t -> b=t.
+intros.
+subst.
+reflexivity.
+Qed.
+
+End A.