From e04377e2c5eca2b47bd5f8db320069aa47040488 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 18 Apr 2020 22:58:40 -0400
Subject: [declare] [tactics] Move declare to `vernac`

This PR moves `Declare` to `vernac` which will hopefully allow to
unify it with `DeclareDef` and avoid exposing entry internals.

There are many tradeoffs to be made as interface and placement of
tactics is far from clear; I've tried to reach a minimally invasive
compromise:

- moved leminv to `ltac_plugin`; this is unused in the core codebase
  and IMO for now it is the best place
- hook added for abstract; this should be cleaned up later
- hook added for scheme declaration; this should be cleaned up later
- separation of hints vernacular and "tactic" part should be also done
  later, for now I've introduced a `declareUctx` module to avoid being
  invasive there.

In particular this last point strongly suggest that for now, the best
place for `Class_tactics` would be also in `ltac`, but I've avoided
that for now too.

This partially supersedes #10951 for now and helps with #11492 .
---
 plugins/ltac/extratactics.mlg   |   2 +-
 plugins/ltac/leminv.ml          | 297 ++++++++++++++++++++++++++++++++++++++++
 plugins/ltac/leminv.mli         |  21 +++
 plugins/ltac/ltac_plugin.mlpack |   1 +
 plugins/setoid_ring/newring.ml  |   2 +-
 5 files changed, 321 insertions(+), 2 deletions(-)
 create mode 100644 plugins/ltac/leminv.ml
 create mode 100644 plugins/ltac/leminv.mli

(limited to 'plugins')

diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 7754fe401e..0bad3cbe5b 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -312,7 +312,7 @@ let add_rewrite_hint ~poly bases ort t lcsr =
         if poly then ctx
         else (* This is a global universe context that shouldn't be
                 refreshed at every use of the hint, declare it globally. *)
-          (Declare.declare_universe_context ~poly:false ctx;
+          (DeclareUctx.declare_universe_context ~poly:false ctx;
            Univ.ContextSet.empty)
     in
       CAst.make ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in
diff --git a/plugins/ltac/leminv.ml b/plugins/ltac/leminv.ml
new file mode 100644
index 0000000000..5a8ec404ee
--- /dev/null
+++ b/plugins/ltac/leminv.ml
@@ -0,0 +1,297 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Pp
+open CErrors
+open Util
+open Names
+open Termops
+open Environ
+open Constr
+open Context
+open EConstr
+open Vars
+open Namegen
+open Evd
+open Printer
+open Reductionops
+open Inductiveops
+open Tacmach.New
+open Clenv
+open Tacticals.New
+open Tactics
+open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
+
+let no_inductive_inconstr env sigma constr =
+  (str "Cannot recognize an inductive predicate in " ++
+     pr_leconstr_env env sigma constr ++
+     str "." ++ spc () ++ str "If there is one, may be the structure of the arity" ++
+     spc () ++ str "or of the type of constructors" ++ spc () ++
+     str "is hidden by constant definitions.")
+
+(* Inversion stored in lemmas *)
+
+(* ALGORITHM:
+
+   An inversion stored in a lemma is computed from a term-pattern, in
+   a signature, as follows:
+
+   Suppose we have an inductive relation, (I abar), in a signature Gamma:
+
+       Gamma |- (I abar)
+
+   Then we compute the free-variables of abar.  Suppose that Gamma is
+   thinned out to only include these.
+
+   [We need technically to require that all free-variables of the
+    types of the free variables of abar are themselves free-variables
+    of abar.  This needs to be checked, but it should not pose a
+    problem - it is hard to imagine cases where it would not hold.]
+
+   Now, we pose the goal:
+
+       (P:(Gamma)Prop)(Gamma)(I abar)->(P vars[Gamma]).
+
+   We execute the tactic:
+
+   REPEAT Intro THEN (OnLastHyp (Inv NONE false o outSOME))
+
+   This leaves us with some subgoals.  All the assumptions after "P"
+   in these subgoals are new assumptions.  I.e. if we have a subgoal,
+
+       P:(Gamma)Prop, Gamma, Hbar:Tbar |- (P ybar)
+
+   then the assumption we needed to have was
+
+      (Hbar:Tbar)(P ybar)
+
+   So we construct all the assumptions we need, and rebuild the goal
+   with these assumptions.  Then, we can re-apply the same tactic as
+   above, but instead of stopping after the inversion, we just apply
+   the respective assumption in each subgoal.
+
+ *)
+
+(* returns the sub_signature of sign corresponding to those identifiers that
+ * are not global. *)
+(*
+let get_local_sign sign =
+  let lid = ids_of_sign sign in
+  let globsign = Global.named_context() in
+  let add_local id res_sign =
+    if not (mem_sign globsign id) then
+      add_sign (lookup_sign id sign) res_sign
+    else
+      res_sign
+  in
+  List.fold_right add_local lid nil_sign
+*)
+(* returns the identifier of lid that was the latest declared in sign.
+ * (i.e. is the identifier id of lid such that
+ * sign_length (sign_prefix id sign) > sign_length (sign_prefix id' sign) >
+ * for any id'<>id in lid).
+ * it returns both the pair (id,(sign_prefix id sign)) *)
+(*
+let max_prefix_sign lid sign =
+  let rec max_rec (resid,prefix) = function
+    | [] -> (resid,prefix)
+    | (id::l) ->
+        let pre = sign_prefix id sign in
+        if sign_length pre > sign_length prefix then
+          max_rec (id,pre) l
+        else
+          max_rec (resid,prefix) l
+  in
+  match lid with
+    | [] -> nil_sign
+    | id::l -> snd (max_rec (id, sign_prefix id sign) l)
+*)
+let rec add_prods_sign env sigma t =
+  match EConstr.kind sigma (whd_all env sigma t) with
+    | Prod (na,c1,b) ->
+        let id = id_of_name_using_hdchar env sigma t na.binder_name in
+        let b'= subst1 (mkVar id) b in
+        add_prods_sign (push_named (LocalAssum ({na with binder_name=id},c1)) env) sigma b'
+    | LetIn (na,c1,t1,b) ->
+        let id = id_of_name_using_hdchar env sigma t na.binder_name in
+        let b'= subst1 (mkVar id) b in
+        add_prods_sign (push_named (LocalDef ({na with binder_name=id},c1,t1)) env) sigma b'
+    | _ -> (env,t)
+
+(* [dep_option] indicates whether the inversion lemma is dependent or not.
+   If it is dependent and I is of the form (x_bar:T_bar)(I t_bar) then
+   the stated goal will be (x_bar:T_bar)(H:(I t_bar))(P t_bar H)
+   where P:(x_bar:T_bar)(H:(I x_bar))[sort].
+   The generalisation of such a goal at the moment of the dependent case should
+   be easy.
+
+   If it is non dependent, then if [I]=(I t_bar) and (x_bar:T_bar) are the
+   variables occurring in [I], then the stated goal will be:
+    (x_bar:T_bar)(I t_bar)->(P x_bar)
+   where P: P:(x_bar:T_bar)[sort].
+*)
+
+let compute_first_inversion_scheme env sigma ind sort dep_option =
+  let indf,realargs = dest_ind_type ind in
+  let allvars = vars_of_env env in
+  let p = next_ident_away (Id.of_string "P") allvars in
+  let pty,goal =
+    if dep_option  then
+      let pty = make_arity env sigma true indf sort in
+      let r = relevance_of_inductive_type env ind in
+      let goal =
+        mkProd
+          (make_annot Anonymous r, mkAppliedInd ind, applist(mkVar p,realargs@[mkRel 1]))
+      in
+      pty,goal
+    else
+      let i = mkAppliedInd ind in
+      let ivars = global_vars env sigma i in
+      let revargs,ownsign =
+        fold_named_context
+          (fun env d (revargs,hyps) ->
+            let d = map_named_decl EConstr.of_constr d in
+             let id = NamedDecl.get_id d in
+             if Id.List.mem id ivars then
+               ((mkVar id)::revargs, Context.Named.add d hyps)
+             else
+               (revargs,hyps))
+          env ~init:([],[])
+      in
+      let pty = it_mkNamedProd_or_LetIn (mkSort sort) ownsign in
+      let goal = mkArrow i Sorts.Relevant (applist(mkVar p, List.rev revargs)) in
+      (pty,goal)
+  in
+  let npty = nf_all env sigma pty in
+  let extenv = push_named (LocalAssum (make_annot p Sorts.Relevant,npty)) env in
+  extenv, goal
+
+(* [inversion_scheme sign I]
+
+   Given a local signature, [sign], and an instance of an inductive
+   relation, [I], inversion_scheme will prove the associated inversion
+   scheme on sort [sort]. Depending on the value of [dep_option] it will
+   build a dependent lemma or a non-dependent one *)
+
+let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op =
+  let (env,i) = add_prods_sign env sigma t in
+  let ind =
+    try find_rectype env sigma i
+    with Not_found ->
+      user_err ~hdr:"inversion_scheme" (no_inductive_inconstr env sigma i)
+  in
+  let (invEnv,invGoal) =
+    compute_first_inversion_scheme env sigma ind sort dep_option
+  in
+  assert
+    (List.subset
+       (global_vars env sigma invGoal)
+       (ids_of_named_context (named_context invEnv)));
+  (*
+    user_err ~hdr:"lemma_inversion"
+    (str"Computed inversion goal was not closed in initial signature.");
+  *)
+  let pf = Proof.start ~name ~poly (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in
+  let pf, _, () = Proof.run_tactic env (tclTHEN intro (onLastHypId inv_op)) pf in
+  let pfterm = List.hd (Proof.partial_proof pf) in
+  let global_named_context = Global.named_context_val () in
+  let ownSign = ref begin
+    fold_named_context
+      (fun env d sign ->
+        let d = map_named_decl EConstr.of_constr d in
+         if mem_named_context_val (NamedDecl.get_id d) global_named_context then sign
+         else Context.Named.add d sign)
+      invEnv ~init:Context.Named.empty
+  end in
+  let avoid = ref Id.Set.empty in
+  let Proof.{sigma} = Proof.data pf in
+  let sigma = Evd.minimize_universes sigma in
+  let rec fill_holes c =
+    match EConstr.kind sigma c with
+    | Evar (e,args) ->
+        let h = next_ident_away (Id.of_string "H") !avoid in
+        let ty,inst = Evarutil.generalize_evar_over_rels sigma (e,args) in
+        avoid := Id.Set.add h !avoid;
+        ownSign := Context.Named.add (LocalAssum (make_annot h Sorts.Relevant,ty)) !ownSign;
+        applist (mkVar h, inst)
+    | _ -> EConstr.map sigma fill_holes c
+  in
+  let c = fill_holes pfterm in
+  (* warning: side-effect on ownSign *)
+  let invProof = it_mkNamedLambda_or_LetIn c !ownSign in
+  let p = EConstr.to_constr sigma invProof in
+  p, sigma
+
+let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
+  let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in
+  let univs = Evd.univ_entry ~poly sigma in
+  let entry = Declare.definition_entry ~univs invProof in
+  let _ : Names.Constant.t = Declare.declare_constant ~name ~kind:Decls.(IsProof Lemma) (Declare.DefinitionEntry entry) in
+  ()
+
+(* inv_op = Inv (derives de complete inv. lemma)
+ * inv_op = InvNoThining (derives de semi inversion lemma) *)
+
+let add_inversion_lemma_exn ~poly na com comsort bool tac =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let sigma, c = Constrintern.interp_type_evars ~program_mode:false env sigma com in
+  let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid sigma comsort in
+  try
+    add_inversion_lemma ~poly na env sigma c sort bool tac
+  with
+    |   UserError (Some "Case analysis",s) -> (* Reference to Indrec *)
+          user_err ~hdr:"Inv needs Nodep Prop Set" s
+
+(* ================================= *)
+(* Applying a given inversion lemma  *)
+(* ================================= *)
+
+let lemInv id c =
+  Proofview.Goal.enter begin fun gls ->
+  try
+    let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_get_type_of gls c) in
+    let clause = clenv_constrain_last_binding (EConstr.mkVar id) clause in
+    Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false
+  with
+    | NoSuchBinding ->
+        user_err
+          (hov 0 (pr_econstr_env (pf_env gls) (project gls) c ++ spc () ++ str "does not refer to an inversion lemma."))
+    | UserError (a,b) ->
+         user_err ~hdr:"LemInv"
+           (str "Cannot refine current goal with the lemma " ++
+              pr_leconstr_env (pf_env gls) (project gls) c)
+  end
+
+let lemInv_gen id c = try_intros_until (fun id -> lemInv id c) id
+
+let lemInvIn id c ids =
+  Proofview.Goal.enter begin fun gl ->
+    let hyps = List.map (fun id -> pf_get_hyp id gl) ids in
+    let intros_replace_ids =
+      let concl = Proofview.Goal.concl gl in
+      let sigma = project gl in
+      let nb_of_new_hyp = nb_prod sigma concl - List.length ids in
+      if nb_of_new_hyp < 1  then
+        intros_replacing ids
+      else
+        (tclTHEN (tclDO nb_of_new_hyp intro) (intros_replacing ids))
+    in
+    ((tclTHEN (tclTHEN (bring_hyps hyps) (lemInv id c))
+        (intros_replace_ids)))
+  end
+
+let lemInvIn_gen id c l = try_intros_until (fun id -> lemInvIn id c l) id
+
+let lemInv_clause id c = function
+  | [] -> lemInv_gen id c
+  | l -> lemInvIn_gen id c l
diff --git a/plugins/ltac/leminv.mli b/plugins/ltac/leminv.mli
new file mode 100644
index 0000000000..5a5de7b58f
--- /dev/null
+++ b/plugins/ltac/leminv.mli
@@ -0,0 +1,21 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+open EConstr
+open Constrexpr
+open Tactypes
+
+val lemInv_clause :
+  quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic
+
+val add_inversion_lemma_exn : poly:bool ->
+  Id.t -> constr_expr -> Sorts.family -> bool -> (Id.t -> unit Proofview.tactic) ->
+    unit
diff --git a/plugins/ltac/ltac_plugin.mlpack b/plugins/ltac/ltac_plugin.mlpack
index e83eab20dc..f31361279c 100644
--- a/plugins/ltac/ltac_plugin.mlpack
+++ b/plugins/ltac/ltac_plugin.mlpack
@@ -9,6 +9,7 @@ Tactic_debug
 Tacintern
 Profile_ltac
 Tactic_matching
+Leminv
 Tacinterp
 Tacentries
 Evar_tactics
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 0646af3552..633cdbd735 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -150,7 +150,7 @@ let decl_constant na univs c =
   let open Constr in
   let vars = CVars.universes_of_constr c in
   let univs = UState.restrict_universe_context ~lbound:(Global.universes_lbound ()) univs vars in
-  let () = Declare.declare_universe_context ~poly:false univs in
+  let () = DeclareUctx.declare_universe_context ~poly:false univs in
   let types = (Typeops.infer (Global.env ()) c).uj_type in
   let univs = Monomorphic_entry Univ.ContextSet.empty in
   mkConst(declare_constant ~name:(Id.of_string na)
-- 
cgit v1.2.3