diff options
63 files changed, 1149 insertions, 1012 deletions
diff --git a/.gitignore b/.gitignore index 12a5c11e5e..b99d2a0d45 100644 --- a/.gitignore +++ b/.gitignore @@ -93,6 +93,7 @@ test-suite/coqdoc/Coqdoc.* test-suite/coqdoc/index.html test-suite/coqdoc/coqdoc.css test-suite/output/MExtraction.out +test-suite/output/*.out.real test-suite/oUnit-anon.cache test-suite/unit-tests/**/*.test diff --git a/Makefile.make b/Makefile.make index d8e229e4db..e19053462d 100644 --- a/Makefile.make +++ b/Makefile.make @@ -46,23 +46,20 @@ # !! Before using FIND_SKIP_DIRS, please read how you should in the !! # !! FIND_SKIP_DIRS section of dev/doc/build-system.dev.txt !! -FIND_SKIP_DIRS:='(' \ +# "-not -name ." to avoid skipping everything since we "find ." +# "-type d" to be able to find .merlin.in files +FIND_SKIP_DIRS:=-not -name . '(' \ -name '{arch}' -o \ - -name '.svn' -o \ + -name '.*' -type d -o \ -name '_darcs' -o \ - -name '.git' -o \ - -name '.bzr' -o \ -name 'debian' -o \ -name "$${GIT_DIR}" -o \ -name '_build' -o \ -name '_build_ci' -o \ - -name '_build_boot' -o \ -name '_install_ci' -o \ -name 'gramlib' -o \ -name 'user-contrib' -o \ -name 'test-suite' -o \ - -name '.opamcache' -o \ - -name '.coq-native' -o \ -name 'plugin_tutorial' \ ')' -prune -o diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index d20eea7874..06ee4fcc7a 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -61,7 +61,7 @@ let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = mind_entry_params = mb.mind_params_ctxt; mind_entry_inds; mind_entry_universes; - mind_entry_variance = mb.mind_variance; + mind_entry_cumulative= Option.has_some mb.mind_variance; mind_entry_private = mb.mind_private; } diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh index b58a794da2..871d033f5b 100755 --- a/dev/ci/ci-equations.sh +++ b/dev/ci/ci-equations.sh @@ -5,5 +5,4 @@ ci_dir="$(dirname "$0")" git_download equations -( cd "${CI_BUILD_DIR}/equations" && coq_makefile -f _CoqProject -o Makefile && \ - make && make test-suite && make examples && make install) +( cd "${CI_BUILD_DIR}/equations" && ./configure.sh coq && make ci) diff --git a/dev/ci/user-overlays/11027-SkySkimmer-expose-comind-univ.sh b/dev/ci/user-overlays/11027-SkySkimmer-expose-comind-univ.sh new file mode 100644 index 0000000000..bb65beb043 --- /dev/null +++ b/dev/ci/user-overlays/11027-SkySkimmer-expose-comind-univ.sh @@ -0,0 +1,19 @@ +if [ "$CI_PULL_REQUEST" = "11027" ] || [ "$CI_BRANCH" = "cleanup-comind-univ" ]; then + + elpi_CI_REF=expose-comind-univ + elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi + + equations_CI_REF=expose-comind-univ + equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations + + paramcoq_CI_REF=expose-comind-univ + paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq + + mtac2_CI_REF=expose-comind-univ + mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2 + + rewriter_CI_REF=cleanup-comind-univ + rewriter_CI_GITURL=https://github.com/SkySkimmer/rewriter + + +fi diff --git a/doc/changelog/04-tactics/11203-fix-time-printing.rst b/doc/changelog/04-tactics/11203-fix-time-printing.rst new file mode 100644 index 0000000000..cdfd2b228e --- /dev/null +++ b/doc/changelog/04-tactics/11203-fix-time-printing.rst @@ -0,0 +1,4 @@ +- The optional string argument to :tacn:`time` is now properly quoted + under :cmd:`Print Ltac` (`#11203 + <https://github.com/coq/coq/pull/11203>`_, fixes `#10971 + <https://github.com/coq/coq/issues/10971>`_, by Jason Gross) diff --git a/doc/changelog/04-tactics/11263-micromega-fix.rst b/doc/changelog/04-tactics/11263-micromega-fix.rst new file mode 100644 index 0000000000..ebfb6c19b1 --- /dev/null +++ b/doc/changelog/04-tactics/11263-micromega-fix.rst @@ -0,0 +1,6 @@ +- **Fixed** + Efficiency regression introduced by PR `#9725 <https://github.com/coq/coq/pull/9725>`_. + (`#11263 <https://github.com/coq/coq/pull/11263>`_, + fixes `#11063 <https://github.com/coq/coq/issues/11063>`_, + and `#11242 <https://github.com/coq/coq/issues/11242>`_, + and `#11270 <https://github.com/coq/coq/issues/11270>`_, by Frédéric Besson). diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index a2bc90ffc0..b816ef6210 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -24,6 +24,7 @@ plugins/extraction/Extraction.v plugins/funind/FunInd.v plugins/funind/Recdef.v plugins/ltac/Ltac.v +plugins/micromega/Ztac.v plugins/micromega/DeclConstant.v plugins/micromega/Env.v plugins/micromega/EnvRing.v diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 754b977f89..606cce0127 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -17,6 +17,8 @@ #include <signal.h> #include <stdint.h> #include <caml/memory.h> +#include <caml/signals.h> +#include <caml/version.h> #include <math.h> #include "coq_gc.h" #include "coq_instruct.h" @@ -203,11 +205,13 @@ if (sp - num_args < coq_stack_threshold) { \ *sp = swap_accu_sp_tmp__; \ }while(0) +#if OCAML_VERSION < 41000 /* For signal handling, we hijack some code from the caml runtime */ extern intnat volatile caml_signals_are_pending; extern intnat volatile caml_pending_signals[]; extern void caml_process_pending_signals(void); +#endif /* The interpreter itself */ @@ -506,11 +510,27 @@ value coq_interprete print_instr("check_stack"); CHECK_STACK(0); /* We also check for signals */ +#if OCAML_VERSION >= 41000 + { + value res = caml_process_pending_actions_exn(); + if (Is_exception_result(res)) { + /* If there is an asynchronous exception, we reset the vm */ + coq_sp = coq_stack_high; + caml_raise(Extract_exception(res)); + } + } +#else if (caml_signals_are_pending) { /* If there's a Ctrl-C, we reset the vm */ - if (caml_pending_signals[SIGINT]) { coq_sp = coq_stack_high; } + intnat sigint = caml_pending_signals[SIGINT]; + if (sigint) { coq_sp = coq_stack_high; } caml_process_pending_signals(); + if (sigint) { + caml_failwith("Coq VM: Fatal error: SIGINT signal detected " + "but no exception was raised"); + } } +#endif Next; Instruct(ENSURESTACKCAPACITY) { @@ -1743,7 +1763,7 @@ value coq_interprete #ifndef THREADED_CODE default: /*fprintf(stderr, "%d\n", *pc);*/ - failwith("Coq VM: Fatal error: bad opcode"); + caml_failwith("Coq VM: Fatal error: bad opcode"); } } #endif diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c index 3613bc07a6..bbe91da628 100644 --- a/kernel/byterun/coq_values.c +++ b/kernel/byterun/coq_values.c @@ -40,7 +40,7 @@ value coq_closure_arity(value clos) { c++; if (Is_instruction(c,GRAB)) return Val_int(3 + c[1] - Wosize_val(clos)); else { - if (Wosize_val(clos) != 2) failwith("Coq Values : coq_closure_arity"); + if (Wosize_val(clos) != 2) caml_failwith("Coq Values : coq_closure_arity"); return Val_int(1); } } diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 9d7387c7ad..261a3510d6 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -315,10 +315,6 @@ let refresh_polymorphic_type_of_inductive (_,mip) = let ctx = List.rev mip.mind_arity_ctxt in mkArity (List.rev ctx, Sorts.sort_of_univ ar.template_level), true -let dummy_variance = let open Entries in function - | Monomorphic_entry _ -> assert false - | Polymorphic_entry (_,uctx) -> Array.make (Univ.UContext.size uctx) Univ.Variance.Irrelevant - let cook_inductive { Opaqueproof.modlist; abstract } mib = let open Entries in let (section_decls, subst, abs_uctx) = abstract in @@ -333,10 +329,6 @@ let cook_inductive { Opaqueproof.modlist; abstract } mib = let auctx = Univ.AUContext.repr auctx in subst, Polymorphic_entry (nas, auctx) in - let variance = match mib.mind_variance with - | None -> None - | Some _ -> Some (dummy_variance ind_univs) - in let cache = RefTable.create 13 in let discharge c = Vars.subst_univs_level_constr subst (expmod_constr cache modlist c) in let inds = @@ -363,7 +355,7 @@ let cook_inductive { Opaqueproof.modlist; abstract } mib = mind_entry_params = params'; mind_entry_inds = inds'; mind_entry_private = mib.mind_private; - mind_entry_variance = variance; + mind_entry_cumulative = Option.has_some mib.mind_variance; mind_entry_universes = ind_univs } diff --git a/kernel/entries.ml b/kernel/entries.ml index b50c3ebbc3..8d930b521c 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -50,7 +50,7 @@ type mutual_inductive_entry = { mind_entry_params : Constr.rel_context; mind_entry_inds : one_inductive_entry list; mind_entry_universes : universes_entry; - mind_entry_variance : Univ.Variance.t array option; + mind_entry_cumulative : bool; (* universe constraints and the constraints for subtyping of inductive types in the block. *) mind_entry_private : bool option; diff --git a/kernel/environ.mli b/kernel/environ.mli index 257bd43083..bd5a000c2b 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -296,7 +296,13 @@ val add_constraints : Univ.Constraint.t -> env -> env (** Check constraints are satifiable in the environment. *) val check_constraints : Univ.Constraint.t -> env -> bool val push_context : ?strict:bool -> Univ.UContext.t -> env -> env +(* [push_context ?(strict=false) ctx env] pushes the universe context to the environment. + @raise UGraph.AlreadyDeclared if one of the universes is already declared. +*) val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env +(* [push_context_set ?(strict=false) ctx env] pushes the universe context set + to the environment. It does not fail if one of the universes is already declared. *) + val push_constraints_to_env : 'a Univ.constrained -> env -> env val push_subgraph : Univ.ContextSet.t -> env -> env diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index c91cb39fe2..d9ccf81619 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -61,64 +61,6 @@ let mind_check_names mie = (************************************************************************) -(************************** Cumulativity checking************************) -(************************************************************************) - -(* Check arities and constructors *) -let check_subtyping_arity_constructor env subst arcn numparams is_arity = - let numchecked = ref 0 in - let basic_check ev tp = - if !numchecked < numparams then () else Reduction.conv_leq ev tp (subst tp); - numchecked := !numchecked + 1 - in - let check_typ typ typ_env = - match typ with - | LocalAssum (_, typ') -> - begin - try - basic_check typ_env typ'; Environ.push_rel typ typ_env - with Reduction.NotConvertible -> - CErrors.anomaly ~label:"bad inductive subtyping relation" - Pp.(str "Invalid subtyping relation") - end - | _ -> CErrors.anomaly Pp.(str "") - in - let typs, codom = Reduction.dest_prod env arcn in - let last_env = Context.Rel.fold_outside check_typ typs ~init:env in - if not is_arity then basic_check last_env codom else () - -let check_cumulativity univs variances env_ar params data = - let uctx = match univs with - | Monomorphic_entry _ -> raise (InductiveError BadUnivs) - | Polymorphic_entry (_,uctx) -> uctx - in - let instance = UContext.instance uctx in - if Instance.length instance != Array.length variances then raise (InductiveError BadUnivs); - let numparams = Context.Rel.nhyps params in - let new_levels = Array.init (Instance.length instance) - (fun i -> Level.(make (UGlobal.make DirPath.empty i))) - in - let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap) - LMap.empty (Instance.to_array instance) new_levels - in - let dosubst = Vars.subst_univs_level_constr lmap in - let instance_other = Instance.of_array new_levels in - let constraints_other = Univ.subst_univs_level_constraints lmap (UContext.constraints uctx) in - let uctx_other = Univ.UContext.make (instance_other, constraints_other) in - let env = Environ.push_context uctx_other env_ar in - let subtyp_constraints = - Univ.enforce_leq_variance_instances variances - instance instance_other - Constraint.empty - in - let env = Environ.add_constraints subtyp_constraints env in - (* process individual inductive types: *) - List.iter (fun (arity,lc) -> - check_subtyping_arity_constructor env dosubst arity numparams true; - Array.iter (fun cnt -> check_subtyping_arity_constructor env dosubst cnt numparams false) lc) - data - -(************************************************************************) (************************** Type checking *******************************) (************************************************************************) @@ -351,8 +293,14 @@ let typecheck_inductive env (mie:mutual_inductive_entry) = let env_univs = match mie.mind_entry_universes with | Monomorphic_entry ctx -> - let env = if has_template_poly then set_universes_lbound env Univ.Level.prop else env in - push_context_set ctx env + if has_template_poly then + (* For that particular case, we typecheck the inductive in an environment + where the universes introduced by the definition are only [>= Prop] *) + let env = set_universes_lbound env Univ.Level.prop in + push_context_set ~strict:false ctx env + else + (* In the regular case, all universes are [> Set] *) + push_context_set ~strict:true ctx env | Polymorphic_entry (_, ctx) -> push_context ctx env in @@ -389,11 +337,8 @@ let typecheck_inductive env (mie:mutual_inductive_entry) = data, Some None in - let () = match mie.mind_entry_variance with - | None -> () - | Some variances -> - check_cumulativity mie.mind_entry_universes variances env_ar params (List.map pi1 data) - in + (* TODO pass only the needed bits *) + let variance = InferCumulativity.infer_inductive env mie in (* Abstract universes *) let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in @@ -408,4 +353,4 @@ let typecheck_inductive env (mie:mutual_inductive_entry) = Environ.push_rel_context ctx env in - env_ar_par, univs, mie.mind_entry_variance, record, params, Array.of_list data + env_ar_par, univs, variance, record, params, Array.of_list data diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml index 550c81ed82..77abe6b410 100644 --- a/kernel/inferCumulativity.ml +++ b/kernel/inferCumulativity.ml @@ -216,19 +216,11 @@ let infer_inductive env mie = let open Entries in let params = mie.mind_entry_params in let entries = mie.mind_entry_inds in - let variances = - match mie.mind_entry_variance with - | None -> None - | Some _ -> - let uctx = match mie.mind_entry_universes with - | Monomorphic_entry _ -> assert false - | Polymorphic_entry (_,uctx) -> uctx - in - try Some (infer_inductive_core env params entries uctx) - with TrivialVariance -> Some (Array.make (UContext.size uctx) Invariant) - in - { mie with mind_entry_variance = variances } - -let dummy_variance = let open Entries in function - | Monomorphic_entry _ -> assert false - | Polymorphic_entry (_,uctx) -> Array.make (UContext.size uctx) Irrelevant + if not mie.mind_entry_cumulative then None + else + let uctx = match mie.mind_entry_universes with + | Monomorphic_entry _ -> assert false + | Polymorphic_entry (_,uctx) -> uctx + in + try Some (infer_inductive_core env params entries uctx) + with TrivialVariance -> Some (Array.make (UContext.size uctx) Invariant) diff --git a/kernel/inferCumulativity.mli b/kernel/inferCumulativity.mli index a234e334d1..2bddfe21e2 100644 --- a/kernel/inferCumulativity.mli +++ b/kernel/inferCumulativity.mli @@ -9,6 +9,4 @@ (************************************************************************) val infer_inductive : Environ.env -> Entries.mutual_inductive_entry -> - Entries.mutual_inductive_entry - -val dummy_variance : Entries.universes_entry -> Univ.Variance.t array + Univ.Variance.t array option diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 2b83c2d868..f1e994b337 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -42,9 +42,9 @@ Type_errors Modops Inductive Typeops +InferCumulativity IndTyping Indtypes -InferCumulativity Cooking Term_typing Subtyping diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 759feda9ab..ee101400d6 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -331,13 +331,13 @@ type constraints_addition = | Now of Univ.ContextSet.t | Later of Univ.ContextSet.t Future.computation -let push_context_set poly cst senv = +let push_context_set ~strict cst senv = if Univ.ContextSet.is_empty cst then senv else let sections = Option.map (Section.push_constraints cst) senv.sections in { senv with - env = Environ.push_context_set ~strict:(not poly) cst senv.env; + env = Environ.push_context_set ~strict cst senv.env; univ = Univ.ContextSet.union cst senv.univ; sections } @@ -346,7 +346,7 @@ let add_constraints cst senv = | Later fc -> {senv with future_cst = fc :: senv.future_cst} | Now cst -> - push_context_set false cst senv + push_context_set ~strict:true cst senv let add_constraints_list cst senv = List.fold_left (fun acc c -> add_constraints c acc) senv cst @@ -547,7 +547,7 @@ let add_field ?(is_include=false) ((l,sfb) as field) gn senv = else (* Delayed constraints from opaque body are added by [add_constant_aux] *) let cst = constraints_of_sfb sfb in - List.fold_left (fun senv cst -> push_context_set false cst senv) senv cst + List.fold_left (fun senv cst -> push_context_set ~strict:true cst senv) senv cst in let env' = match sfb, gn with | SFBconst cb, C con -> Environ.add_constant con cb senv.env @@ -998,7 +998,7 @@ let close_section senv = let env = Environ.set_opaque_tables env (Environ.opaque_tables senv.env) in let senv = { senv with env; revstruct; sections; univ; objlabels; } in (* Second phase: replay the discharged section contents *) - let senv = push_context_set false cstrs senv in + let senv = push_context_set ~strict:true cstrs senv in let modlist = Section.replacement_context env0 sections0 in let cooking_info seg = let { abstr_ctx; abstr_subst; abstr_uctx } = seg in @@ -1015,7 +1015,6 @@ let close_section senv = | `Inductive (ind, mib) -> let info = cooking_info (Section.segment_of_inductive env0 ind sections0) in let mie = Cooking.cook_inductive info mib in - let mie = InferCumulativity.infer_inductive senv.env mie in let _, senv = add_mind (MutInd.label ind) mie senv in senv in diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 0b7ca26e09..92bbd264fa 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -113,7 +113,7 @@ val add_modtype : (** Adding universe constraints *) val push_context_set : - bool -> Univ.ContextSet.t -> safe_transformer0 + strict:bool -> Univ.ContextSet.t -> safe_transformer0 val add_constraints : Univ.Constraint.t -> safe_transformer0 diff --git a/library/global.ml b/library/global.ml index d4262683bb..fbbe09301b 100644 --- a/library/global.ml +++ b/library/global.ml @@ -90,7 +90,7 @@ let push_named_assum a = globalize0 (Safe_typing.push_named_assum a) let push_named_def d = globalize0 (Safe_typing.push_named_def d) let push_section_context c = globalize0 (Safe_typing.push_section_context c) let add_constraints c = globalize0 (Safe_typing.add_constraints c) -let push_context_set b c = globalize0 (Safe_typing.push_context_set b c) +let push_context_set ~strict c = globalize0 (Safe_typing.push_context_set ~strict c) let set_engagement c = globalize0 (Safe_typing.set_engagement c) let set_indices_matter b = globalize0 (Safe_typing.set_indices_matter b) @@ -206,7 +206,7 @@ let current_dirpath () = let with_global f = let (a, ctx) = f (env ()) (current_dirpath ()) in - push_context_set false ctx; a + push_context_set ~strict:true ctx; a let register_inline c = globalize0 (Safe_typing.register_inline c) let register_inductive c r = globalize0 (Safe_typing.register_inductive c r) diff --git a/library/global.mli b/library/global.mli index db0f87df7e..a38fde41a5 100644 --- a/library/global.mli +++ b/library/global.mli @@ -60,7 +60,7 @@ val add_mind : (** Extra universe constraints *) val add_constraints : Univ.Constraint.t -> unit -val push_context_set : bool -> Univ.ContextSet.t -> unit +val push_context_set : strict:bool -> Univ.ContextSet.t -> unit (** Non-interactive modules and module types *) diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 0e8c225a8f..7843faaef3 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -971,7 +971,7 @@ let pr_goal_selector ~toplevel s = | TacTime (s,t) -> hov 1 ( keyword "time" - ++ pr_opt str s ++ spc () + ++ pr_opt qstring s ++ spc () ++ pr_tac (ltactical,E) t), ltactical | TacRepeat t -> diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index ca5c8b30c2..98d14f3d33 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1930,7 +1930,7 @@ let build_morphism_signature env sigma m = let evd = solve_constraints env !evd in let evd = Evd.minimize_universes evd in let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in - Pretyping.check_evars env (Evd.from_env env) evd (EConstr.of_constr m); + Pretyping.check_evars env evd (EConstr.of_constr m); Evd.evar_universe_context evd, m let default_morphism sign m = diff --git a/plugins/micromega/Lia.v b/plugins/micromega/Lia.v index 55a93eade7..e53800d07d 100644 --- a/plugins/micromega/Lia.v +++ b/plugins/micromega/Lia.v @@ -23,28 +23,13 @@ Require Coq.micromega.Tauto. Declare ML Module "micromega_plugin". -Ltac zchange checker := +Ltac zchecker := intros __wit __varmap __ff ; - change (@Tauto.eval_bf _ (Zeval_formula (@find Z Z0 __varmap)) __ff) ; - apply (checker __ff __wit). - -Ltac zchecker_no_abstract checker := - zchange checker ; vm_compute ; reflexivity. - -Ltac zchecker_abstract checker := - abstract (zchange checker ; vm_cast_no_check (eq_refl true)). - -Ltac zchecker := zchecker_no_abstract ZTautoChecker_sound. - -(*Ltac zchecker_ext := zchecker_no_abstract ZTautoCheckerExt_sound.*) - -Ltac zchecker_ext := - intros __wit __varmap __ff ; - exact (ZTautoCheckerExt_sound __ff __wit - (@eq_refl bool true <: @eq bool (ZTautoCheckerExt __ff __wit) true) + exact (ZTautoChecker_sound __ff __wit + (@eq_refl bool true <: @eq bool (ZTautoChecker __ff __wit) true) (@find Z Z0 __varmap)). -Ltac lia := PreOmega.zify; xlia zchecker_ext. +Ltac lia := PreOmega.zify; xlia zchecker. Ltac nia := PreOmega.zify; xnlia zchecker. diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v index 80e0f3a536..0e8c09ef1b 100644 --- a/plugins/micromega/MExtraction.v +++ b/plugins/micromega/MExtraction.v @@ -56,7 +56,7 @@ Extract Constant Rinv => "fun x -> 1 / x". (*Extraction "micromega.ml" Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula Tauto.abst_form - ZMicromega.cnfZ ZMicromega.bound_problem_fr ZMicromega.Zeval_const QMicromega.cnfQ + ZMicromega.cnfZ ZMicromega.Zeval_const QMicromega.cnfQ List.map simpl_cone (*map_cone indexes*) denorm Qpower vm_add normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v index 6c1852acbf..0f7a02c2c9 100644 --- a/plugins/micromega/RMicromega.v +++ b/plugins/micromega/RMicromega.v @@ -17,12 +17,12 @@ Require Import OrderedRing. Require Import RingMicromega. Require Import Refl. -Require Import Raxioms Rfunctions RIneq Rpow_def DiscrR. +Require Import Raxioms Rfunctions RIneq Rpow_def. Require Import QArith. Require Import Qfield. Require Import Qreals. Require Import DeclConstant. -Require Import Lia. +Require Import Ztac. Require Setoid. (*Declare ML Module "micromega_plugin".*) @@ -334,15 +334,16 @@ Proof. apply Qeq_bool_eq in C2. rewrite C2. simpl. - rewrite Qpower0 by lia. + rewrite Qpower0. apply Q2R_0. + intro ; subst ; slia C1 C1. + rewrite Q2RpowerRZ. rewrite IHc. reflexivity. rewrite andb_false_iff in C. destruct C. simpl. apply Z.ltb_ge in H. - lia. + right ; normZ. slia H H0. left ; apply Qeq_bool_neq; auto. + simpl. rewrite <- IHc. diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index c1edf579cf..aa8876357a 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.v @@ -856,7 +856,7 @@ Proof. simpl. tauto. + - rewrite <- eval_cnf_cons_iff with (1:= fun env (term:Formula Z) => True) . + rewrite <- eval_cnf_cons_iff. simpl. unfold eval_tt. simpl. rewrite IHl. @@ -940,7 +940,7 @@ Proof. destruct (check_inconsistent f) eqn:U. - destruct f as [e op]. assert (US := check_inconsistent_sound _ _ U env). - rewrite eval_cnf_ff with (1:= eval_nformula). + rewrite eval_cnf_ff. tauto. - intros. rewrite cnf_of_list_correct. now apply xnormalise_correct. @@ -956,7 +956,7 @@ Proof. - destruct f as [e o]. assert (US := check_inconsistent_sound _ _ U env). - rewrite eval_cnf_tt with (1:= eval_nformula). + rewrite eval_cnf_tt. tauto. - rewrite cnf_of_list_correct. apply xnegate_correct. diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v index 02dd29ef14..a155207e2e 100644 --- a/plugins/micromega/Tauto.v +++ b/plugins/micromega/Tauto.v @@ -938,8 +938,6 @@ Section S. Qed. - Variable eval : Env -> Term -> Prop. - Variable eval' : Env -> Term' -> Prop. Variable no_middle_eval' : forall env d, (eval' env d) \/ ~ (eval' env d). @@ -1202,7 +1200,7 @@ Section S. Qed. - + Variable eval : Env -> Term -> Prop. Variable normalise_correct : forall env t tg, eval_cnf env (normalise t tg) -> eval env t. diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v index d709fdda14..9bedb47371 100644 --- a/plugins/micromega/ZMicromega.v +++ b/plugins/micromega/ZMicromega.v @@ -18,11 +18,11 @@ Require Import List. Require Import Bool. Require Import OrderedRing. Require Import RingMicromega. -Require FSetPositive FSetEqProperties. Require Import ZCoeff. Require Import Refl. Require Import ZArith_base. Require Import ZArithRing. +Require Import Ztac. Require PreOmega. (*Declare ML Module "micromega_plugin".*) Local Open Scope Z_scope. @@ -30,7 +30,7 @@ Local Open Scope Z_scope. Ltac flatten_bool := repeat match goal with [ id : (_ && _)%bool = true |- _ ] => destruct (andb_prop _ _ id); clear id - | [ id : (_ || _)%bool = true |- _ ] => destruct (orb_prop _ _ id); clear id + | [ id : (_ || _)%bool = true |- _ ] => destruct (orb_prop _ _ id); clear id end. Ltac inv H := inversion H ; try subst ; clear H. @@ -186,6 +186,7 @@ match o with | OpGt => Z.gt end. + Definition Zeval_formula (env : PolEnv Z) (f : Formula Z):= let (lhs, op, rhs) := f in (Zeval_op2 op) (Zeval_expr env lhs) (Zeval_expr env rhs). @@ -193,10 +194,13 @@ Definition Zeval_formula (env : PolEnv Z) (f : Formula Z):= Definition Zeval_formula' := eval_formula Z.add Z.mul Z.sub Z.opp (@eq Z) Z.le Z.lt (fun x => x) (fun x => x) (pow_N 1 Z.mul). -Lemma Zeval_formula_compat : forall env f, Zeval_formula env f <-> Zeval_formula' env f. +Lemma Zeval_formula_compat' : forall env f, Zeval_formula env f <-> Zeval_formula' env f. Proof. - destruct f ; simpl. - rewrite Zeval_expr_compat. rewrite Zeval_expr_compat. + intros. + unfold Zeval_formula. + destruct f. + repeat rewrite Zeval_expr_compat. + unfold Zeval_formula' ; simpl. unfold eval_expr. generalize (eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x) (fun x : N => x) (pow_N 1 Z.mul) env Flhs). @@ -308,10 +312,10 @@ Definition xnnormalise (t : Formula Z) : NFormula Z := Lemma xnnormalise_correct : forall env f, - eval_nformula env (xnnormalise f) <-> Zeval_formula env f. + eval_nformula env (xnnormalise f) <-> Zeval_formula env f. Proof. intros. - rewrite Zeval_formula_compat. + rewrite Zeval_formula_compat'. unfold xnnormalise. destruct f as [lhs o rhs]. destruct o eqn:O ; cbn ; rewrite ?eval_pol_sub; @@ -418,7 +422,7 @@ Proof. specialize (Zunsat_sound _ EQ env). tauto. + - rewrite <- eval_cnf_cons_iff with (1:= fun env (term:Formula Z) => True) . + rewrite <- eval_cnf_cons_iff. rewrite IHf. simpl. unfold E at 2. @@ -439,7 +443,7 @@ Proof. generalize (xnnormalise t) as f;intro. destruct (Zunsat f) eqn:U. - assert (US := Zunsat_sound _ U env). - rewrite eval_cnf_ff with (1:= eval_nformula). + rewrite eval_cnf_ff. tauto. - rewrite cnf_of_list_correct. apply xnormalise_correct. @@ -474,7 +478,7 @@ Proof. - tauto. Qed. -Lemma negate_correct : forall T env t (tg:T), eval_cnf eval_nformula env (negate t tg) <-> ~ Zeval_formula env t. +Lemma negate_correct : forall T env t (tg:T), eval_cnf eval_nformula env (negate t tg) <-> ~ Zeval_formula env t. Proof. intros. rewrite <- xnnormalise_correct. @@ -482,13 +486,13 @@ Proof. generalize (xnnormalise t) as f;intro. destruct (Zunsat f) eqn:U. - assert (US := Zunsat_sound _ U env). - rewrite eval_cnf_tt with (1:= eval_nformula). + rewrite eval_cnf_tt. tauto. - rewrite cnf_of_list_correct. apply xnegate_correct. Qed. -Definition cnfZ (Annot TX AF : Type) (f : TFormula (Formula Z) Annot TX AF) := +Definition cnfZ (Annot: Type) (TX : Type) (AF : Type) (f : TFormula (Formula Z) Annot TX AF) := rxcnf Zunsat Zdeduce normalise negate true f. Definition ZweakTautoChecker (w: list ZWitness) (f : BFormula (Formula Z)) : bool := @@ -555,7 +559,8 @@ Inductive ZArithProof := | RatProof : ZWitness -> ZArithProof -> ZArithProof | CutProof : ZWitness -> ZArithProof -> ZArithProof | EnumProof : ZWitness -> ZWitness -> list ZArithProof -> ZArithProof -(*| ExProof : positive -> positive -> positive -> ZArithProof ExProof z t x : exists z t, x = z - t /\ z >= 0 /\ t >= 0 *) +| ExProof : positive -> ZArithProof -> ZArithProof +(*ExProof x : exists z t, x = z - t /\ z >= 0 /\ t >= 0 *) . (*| SplitProof : PolC Z -> ZArithProof -> ZArithProof -> ZArithProof.*) @@ -826,187 +831,171 @@ Definition valid_cut_sign (op:Op1) := | _ => false end. -Module Vars. - Import FSetPositive. - Include PositiveSet. - Module Facts := FSetEqProperties.EqProperties(PositiveSet). +Definition bound_var (v : positive) : Formula Z := + Build_Formula (PEX v) OpGe (PEc 0). - Lemma mem_union_l : forall x s s', - mem x s = true -> - mem x (union s s') = true. - Proof. - intros. - rewrite Facts.union_mem. - rewrite H. reflexivity. - Qed. +Definition mk_eq_pos (x : positive) (y:positive) (t : positive) : Formula Z := + Build_Formula (PEX x) OpEq (PEsub (PEX y) (PEX t)). - Lemma mem_union_r : forall x s s', - mem x s' = true -> - mem x (union s s') = true. - Proof. - intros. - rewrite Facts.union_mem. - rewrite H. rewrite orb_comm. reflexivity. - Qed. - Lemma mem_singleton : forall p, - mem p (singleton p) = true. - Proof. - apply Facts.singleton_mem_1. - Qed. +Fixpoint vars (jmp : positive) (p : Pol Z) : list positive := + match p with + | Pc c => nil + | Pinj j p => vars (Pos.add j jmp) p + | PX p j q => jmp::(vars jmp p)++vars (Pos.succ jmp) q + end. - Lemma mem_elements : forall x v, - mem x v = true <-> List.In x (PositiveSet.elements v). - Proof. - intros. - rewrite Facts.MP.FM.elements_b. - rewrite existsb_exists. - unfold Facts.MP.FM.eqb. - split ; intros. - - destruct H as (x' & IN & EQ). - destruct (PositiveSet.E.eq_dec x x') ; try congruence. - subst ; auto. - - exists x. - split ; auto. - destruct (PositiveSet.E.eq_dec x x) ; congruence. - Qed. +Fixpoint max_var (jmp : positive) (p : Pol Z) : positive := + match p with + | Pc _ => jmp + | Pinj j p => max_var (Pos.add j jmp) p + | PX p j q => Pos.max (max_var jmp p) (max_var (Pos.succ jmp) q) + end. - Definition max_element (vars : t) := - fold Pos.max vars xH. +Lemma pos_le_add : forall y x, + (x <= y + x)%positive. +Proof. + intros. + assert ((Z.pos x) <= Z.pos (x + y))%Z. + rewrite <- (Z.add_0_r (Zpos x)). + rewrite <- Pos2Z.add_pos_pos. + apply Z.add_le_mono_l. + compute. congruence. + rewrite Pos.add_comm in H. + apply H. +Qed. - Lemma max_element_max : - forall x vars, mem x vars = true -> Pos.le x (max_element vars). - Proof. - unfold max_element. - intros. - rewrite mem_elements in H. - rewrite PositiveSet.fold_1. - set (F := (fun (a : positive) (e : PositiveSet.elt) => Pos.max e a)). - revert H. - assert (((x <= 1 -> x <= fold_left F (PositiveSet.elements vars) 1) - /\ - (List.In x (PositiveSet.elements vars) -> - x <= fold_left F (PositiveSet.elements vars) 1))%positive). - { - revert x. - generalize xH as acc. - induction (PositiveSet.elements vars). - - simpl. tauto. - - simpl. - intros. - destruct (IHl (F acc a) x). - split ; intros. - apply H. - unfold F. - rewrite Pos.max_le_iff. - tauto. - destruct H1 ; subst. - apply H. - unfold F. - rewrite Pos.max_le_iff. - simpl. - left. + +Lemma max_var_le : forall p v, + (v <= max_var v p)%positive. +Proof. + induction p; simpl. + - intros. + apply Pos.le_refl. + - intros. + specialize (IHp (p+v)%positive). + eapply Pos.le_trans ; eauto. + assert (xH + v <= p + v)%positive. + { apply Pos.add_le_mono. + apply Pos.le_1_l. apply Pos.le_refl. - tauto. } - tauto. - Qed. + eapply Pos.le_trans ; eauto. + apply pos_le_add. + - intros. + apply Pos.max_case_strong;intros ; auto. + specialize (IHp2 (Pos.succ v)%positive). + eapply Pos.le_trans ; eauto. +Qed. + +Lemma max_var_correct : forall p j v, + In v (vars j p) -> Pos.le v (max_var j p). +Proof. + induction p; simpl. + - tauto. + - auto. + - intros. + rewrite in_app_iff in H. + destruct H as [H |[ H | H]]. + + subst. + apply Pos.max_case_strong;intros ; auto. + apply max_var_le. + eapply Pos.le_trans ; eauto. + apply max_var_le. + + apply Pos.max_case_strong;intros ; auto. + eapply Pos.le_trans ; eauto. + + apply Pos.max_case_strong;intros ; auto. + eapply Pos.le_trans ; eauto. +Qed. + +Definition max_var_nformulae (l : list (NFormula Z)) := + List.fold_left (fun acc f => Pos.max acc (max_var xH (fst f))) l xH. - Definition is_subset (v1 v2 : t) := - forall x, mem x v1 = true -> mem x v2 = true. +Section MaxVar. - Lemma is_subset_union_l : forall v1 v2, - is_subset v1 (union v1 v2). + Definition F (acc : positive) (f : Pol Z * Op1) := Pos.max acc (max_var 1 (fst f)). + + Lemma max_var_nformulae_mono_aux : + forall l v acc, + (v <= acc -> + v <= fold_left F l acc)%positive. Proof. - unfold is_subset. + induction l ; simpl ; [easy|]. intros. - apply mem_union_l; auto. + apply IHl. + unfold F. + apply Pos.max_case_strong;intros ; auto. + eapply Pos.le_trans ; eauto. Qed. - Lemma is_subset_union_r : forall v1 v2, - is_subset v1 (union v2 v1). + Lemma max_var_nformulae_mono_aux' : + forall l acc acc', + (acc <= acc' -> + fold_left F l acc <= fold_left F l acc')%positive. Proof. - unfold is_subset. + induction l ; simpl ; [easy|]. intros. - apply mem_union_r; auto. + apply IHl. + unfold F. + apply Pos.max_le_compat_r; auto. Qed. - End Vars. - - -Fixpoint vars_of_pexpr (e : PExpr Z) : Vars.t := - match e with - | PEc _ => Vars.empty - | PEX x => Vars.singleton x - | PEadd e1 e2 | PEsub e1 e2 | PEmul e1 e2 => - let v1 := vars_of_pexpr e1 in - let v2 := vars_of_pexpr e2 in - Vars.union v1 v2 - | PEopp c => vars_of_pexpr c - | PEpow e n => vars_of_pexpr e - end. - -Definition vars_of_formula (f : Formula Z) := - match f with - | Build_Formula l o r => - let v1 := vars_of_pexpr l in - let v2 := vars_of_pexpr r in - Vars.union v1 v2 - end. - -Fixpoint vars_of_bformula {TX : Type} {TG : Type} {ID : Type} - (F : @GFormula (Formula Z) TX TG ID) : Vars.t := - match F with - | TT => Vars.empty - | FF => Vars.empty - | X p => Vars.empty - | A a t => vars_of_formula a - | Cj f1 f2 | D f1 f2 | I f1 _ f2 => - let v1 := vars_of_bformula f1 in - let v2 := vars_of_bformula f2 in - Vars.union v1 v2 - | Tauto.N f => vars_of_bformula f - end. - -Definition bound_var (v : positive) : Formula Z := - Build_Formula (PEX v) OpGe (PEc 0). - -Definition mk_eq_pos (x : positive) (y:positive) (t : positive) : Formula Z := - Build_Formula (PEX x) OpEq (PEsub (PEX y) (PEX t)). - -Section BOUND. - Context {TX TG ID : Type}. - Variable tag_of_var : positive -> positive -> option bool -> TG. - Definition bound_vars (fr : positive) - (v : Vars.t) : @GFormula (Formula Z) TX TG ID := - Vars.fold (fun k acc => - let y := (xO (fr + k)) in - let z := (xI (fr + k)) in - Cj - (Cj (A (mk_eq_pos k y z) (tag_of_var fr k None)) - (Cj (A (bound_var y) (tag_of_var fr k (Some false))) - (A (bound_var z) (tag_of_var fr k (Some true))))) - acc) v TT. + Lemma max_var_nformulae_correct_aux : forall l p o v, + In (p,o) l -> In v (vars xH p) -> Pos.le v (fold_left F l 1)%positive. + Proof. + intros. + generalize 1%positive as acc. + revert p o v H H0. + induction l. + - simpl. tauto. + - simpl. + intros. + destruct H ; subst. + + unfold F at 2. + simpl. + apply max_var_correct in H0. + apply max_var_nformulae_mono_aux. + apply Pos.max_case_strong;intros ; auto. + eapply Pos.le_trans ; eauto. + + eapply IHl ; eauto. + Qed. - Definition bound_problem (F : @GFormula (Formula Z) TX TG ID) : GFormula := - let v := vars_of_bformula F in - I (bound_vars (Pos.succ (Vars.max_element v)) v) None F. +End MaxVar. +Lemma max_var_nformalae_correct : forall l p o v, + In (p,o) l -> In v (vars xH p) -> Pos.le v (max_var_nformulae l)%positive. +Proof. + intros l p o v. + apply max_var_nformulae_correct_aux. +Qed. - Definition bound_problem_fr (fr : positive) (F : @GFormula (Formula Z) TX TG ID) : GFormula := - let v := vars_of_bformula F in - I (bound_vars fr v) None F. +Fixpoint max_var_psatz (w : Psatz Z) : positive := + match w with + | PsatzIn _ n => xH + | PsatzSquare p => max_var xH (Psquare 0 1 Z.add Z.mul Zeq_bool p) + | PsatzMulC p w => Pos.max (max_var xH p) (max_var_psatz w) + | PsatzMulE w1 w2 => Pos.max (max_var_psatz w1) (max_var_psatz w2) + | PsatzAdd w1 w2 => Pos.max (max_var_psatz w1) (max_var_psatz w2) + | _ => xH + end. -End BOUND. +Fixpoint max_var_prf (w : ZArithProof) : positive := + match w with + | DoneProof => xH + | RatProof w pf | CutProof w pf => Pos.max (max_var_psatz w) (max_var_prf pf) + | EnumProof w1 w2 l => List.fold_left (fun acc prf => Pos.max acc (max_var_prf prf)) l + (Pos.max (max_var_psatz w1) (max_var_psatz w2)) + | ExProof _ pf => max_var_prf pf + end. -Fixpoint ZChecker (l:list (NFormula Z)) (pf : ZArithProof) {struct pf} : bool := +Fixpoint ZChecker (l:list (NFormula Z)) (pf : ZArithProof) {struct pf} : bool := match pf with | DoneProof => false | RatProof w pf => @@ -1025,11 +1014,17 @@ Fixpoint ZChecker (l:list (NFormula Z)) (pf : ZArithProof) {struct pf} : bool : | Some cp => ZChecker (nformula_of_cutting_plane cp::l) pf end end -(* | SplitProof e pf1 pf2 => - match ZChecker ((e,NonStrict)::l) pf1 , ZChecker (( -*) - - | EnumProof w1 w2 pf => + | ExProof x prf => + let fr := max_var_nformulae l in + if Pos.leb x fr then + let z := Pos.succ fr in + let t := Pos.succ z in + let nfx := xnnormalise (mk_eq_pos x z t) in + let posz := xnnormalise (bound_var z) in + let post := xnnormalise (bound_var t) in + ZChecker (nfx::posz::post::l) prf + else false + | EnumProof w1 w2 pf => match eval_Psatz l w1 , eval_Psatz l w2 with | Some f1 , Some f2 => match genCuttingPlane f1 , genCuttingPlane f2 with @@ -1040,7 +1035,7 @@ Fixpoint ZChecker (l:list (NFormula Z)) (pf : ZArithProof) {struct pf} : bool : fun lb ub => match pfs with | nil => if Z.gtb lb ub then true else false - | pf::rsr => andb (ZChecker ((psub e1 (Pc lb), Equal) :: l) pf) (label rsr (Z.add lb 1%Z) ub) + | pf::rsr => andb (ZChecker ((psub e1 (Pc lb), Equal) :: l) pf) (label rsr (Z.add lb 1%Z) ub) end) pf (Z.opp z1) z2 else false | _ , _ => true @@ -1057,6 +1052,7 @@ Fixpoint bdepth (pf : ZArithProof) : nat := | RatProof _ p => S (bdepth p) | CutProof _ p => S (bdepth p) | EnumProof _ _ l => S (List.fold_right (fun pf x => Nat.max (bdepth pf) x) O l) + | ExProof _ p => S (bdepth p) end. Require Import Wf_nat. @@ -1246,16 +1242,190 @@ Proof. destruct (makeCuttingPlane p) ; discriminate. Qed. +Lemma eval_nformula_mk_eq_pos : forall env x z t, + env x = env z - env t -> + eval_nformula env (xnnormalise (mk_eq_pos x z t)). +Proof. + intros. + rewrite xnnormalise_correct. + simpl. auto. +Qed. + +Lemma eval_nformula_bound_var : forall env x, + env x >= 0 -> + eval_nformula env (xnnormalise (bound_var x)). +Proof. + intros. + rewrite xnnormalise_correct. + simpl. auto. +Qed. + + +Definition agree_env (fr : positive) (env env' : positive -> Z) : Prop := + forall x, Pos.le x fr -> env x = env' x. + +Lemma agree_env_subset : forall v1 v2 env env', + agree_env v1 env env' -> + Pos.le v2 v1 -> + agree_env v2 env env'. +Proof. + unfold agree_env. + intros. + apply H. + eapply Pos.le_trans ; eauto. +Qed. + + +Lemma agree_env_jump : forall fr j env env', + agree_env (fr + j) env env' -> + agree_env fr (Env.jump j env) (Env.jump j env'). +Proof. + intros. + unfold agree_env ; intro. + intros. + unfold Env.jump. + apply H. + apply Pos.add_le_mono_r; auto. +Qed. + + +Lemma agree_env_tail : forall fr env env', + agree_env (Pos.succ fr) env env' -> + agree_env fr (Env.tail env) (Env.tail env'). +Proof. + intros. + unfold Env.tail. + apply agree_env_jump. + rewrite <- Pos.add_1_r in H. + apply H. +Qed. + + +Lemma max_var_acc : forall p i j, + (max_var (i + j) p = max_var i p + j)%positive. +Proof. + induction p; simpl. + - reflexivity. + - intros. + rewrite ! IHp. + rewrite Pos.add_assoc. + reflexivity. + - intros. + rewrite !Pplus_one_succ_l. + rewrite ! IHp1. + rewrite ! IHp2. + rewrite ! Pos.add_assoc. + rewrite <- Pos.add_max_distr_r. + reflexivity. +Qed. + + + +Lemma agree_env_eval_nformula : + forall env env' e + (AGREE : agree_env (max_var xH (fst e)) env env'), + eval_nformula env e <-> eval_nformula env' e. +Proof. + destruct e. + simpl; intros. + assert ((RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x) env p) + = + (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x) env' p)). + { + revert env env' AGREE. + generalize xH. + induction p ; simpl. + - reflexivity. + - intros. + apply IHp with (p := p1%positive). + apply agree_env_jump. + eapply agree_env_subset; eauto. + rewrite (Pos.add_comm p). + rewrite max_var_acc. + apply Pos.le_refl. + - intros. + f_equal. + f_equal. + { apply IHp1 with (p:= p). + eapply agree_env_subset; eauto. + apply Pos.le_max_l. + } + f_equal. + { unfold Env.hd. + unfold Env.nth. + apply AGREE. + apply Pos.le_1_l. + } + { + apply IHp2 with (p := p). + apply agree_env_tail. + eapply agree_env_subset; eauto. + rewrite !Pplus_one_succ_r. + rewrite max_var_acc. + apply Pos.le_max_r. + } + } + rewrite H. tauto. +Qed. + +Lemma agree_env_eval_nformulae : + forall env env' l + (AGREE : agree_env (max_var_nformulae l) env env'), + make_conj (eval_nformula env) l <-> + make_conj (eval_nformula env') l. +Proof. + induction l. + - simpl. tauto. + - intros. + rewrite ! make_conj_cons. + assert (eval_nformula env a <-> eval_nformula env' a). + { + apply agree_env_eval_nformula. + eapply agree_env_subset ; eauto. + unfold max_var_nformulae. + simpl. + rewrite Pos.max_1_l. + apply max_var_nformulae_mono_aux. + apply Pos.le_refl. + } + rewrite H. + apply and_iff_compat_l. + apply IHl. + eapply agree_env_subset ; eauto. + unfold max_var_nformulae. + simpl. + apply max_var_nformulae_mono_aux'. + apply Pos.le_1_l. +Qed. -Lemma ZChecker_sound : forall w l, ZChecker l w = true -> forall env, make_impl (eval_nformula env) l False. + +Lemma eq_true_iff_eq : + forall b1 b2 : bool, (b1 = true <-> b2 = true) <-> b1 = b2. +Proof. + destruct b1,b2 ; intuition congruence. +Qed. + +Ltac pos_tac := + repeat + match goal with + | |- false = _ => symmetry + | |- Pos.eqb ?X ?Y = false => rewrite Pos.eqb_neq ; intro + | H : @eq positive ?X ?Y |- _ => apply Zpos_eq in H + | H : context[Z.pos (Pos.succ ?X)] |- _ => rewrite (Pos2Z.inj_succ X) in H + | H : Pos.leb ?X ?Y = true |- _ => rewrite Pos.leb_le in H ; + apply (Pos2Z.pos_le_pos X Y) in H + end. + +Lemma ZChecker_sound : forall w l, + ZChecker l w = true -> forall env, make_impl (eval_nformula env) l False. Proof. induction w using (well_founded_ind (well_founded_ltof _ bdepth)). - destruct w as [ | w pf | w pf | w1 w2 pf]. - (* DoneProof *) + destruct w as [ | w pf | w pf | w1 w2 pf | x pf]. + - (* DoneProof *) simpl. discriminate. - (* RatProof *) + - (* RatProof *) simpl. - intro l. case_eq (eval_Psatz l w) ; [| discriminate]. + intros l. case_eq (eval_Psatz l w) ; [| discriminate]. intros f Hf. case_eq (Zunsat f). intros. @@ -1276,15 +1446,15 @@ Proof. apply H2. split ; auto. apply eval_Psatz_sound with (2:= Hf) ; assumption. - (* CutProof *) + - (* CutProof *) simpl. - intro l. + intros l. case_eq (eval_Psatz l w) ; [ | discriminate]. intros f' Hlc. case_eq (genCuttingPlane f'). intros. assert (make_impl (eval_nformula env) (nformula_of_cutting_plane p::l) False). - eapply (H pf) ; auto. + eapply (H pf) ; auto. unfold ltof. simpl. auto with arith. @@ -1303,8 +1473,8 @@ Proof. intros. apply eval_Psatz_sound with (2:= Hlc) in H2. apply genCuttingPlaneNone with (2:= H2) ; auto. - (* EnumProof *) - intro. + - (* EnumProof *) + intros l. simpl. case_eq (eval_Psatz l w1) ; [ | discriminate]. case_eq (eval_Psatz l w2) ; [ | discriminate]. @@ -1359,7 +1529,7 @@ Proof. intros. assert (HH :forall x, -z1 <= x <= z2 -> exists pr, (In pr pf /\ - ZChecker ((PsubC Z.sub p1 x,Equal) :: l) pr = true)%Z). + ZChecker ((PsubC Z.sub p1 x,Equal) :: l) pr = true)%Z). clear HZ0 Hop1 Hop2 HCutL HCutR H0 H1. revert Hfix. generalize (-z1). clear z1. intro z1. @@ -1386,7 +1556,7 @@ Proof. (*/asser *) destruct (HH _ H1) as [pr [Hin Hcheker]]. assert (make_impl (eval_nformula env) ((PsubC Z.sub p1 (eval_pol env p1),Equal) :: l) False). - apply (H pr);auto. + eapply (H pr) ;auto. apply in_bdepth ; auto. rewrite <- make_conj_impl in H2. apply H2. @@ -1410,6 +1580,92 @@ Proof. intros. apply eval_Psatz_sound with (2:= Hf2) in H2. apply genCuttingPlaneNone with (2:= H2) ; auto. +- intros l. + unfold ZChecker. + fold ZChecker. + set (fr := (max_var_nformulae l)%positive). + set (z1 := (Pos.succ fr)) in *. + set (t1 := (Pos.succ z1)) in *. + destruct (x <=? fr)%positive eqn:LE ; [|congruence]. + intros. + set (env':= fun v => if Pos.eqb v z1 + then if Z.leb (env x) 0 then 0 else env x + else if Pos.eqb v t1 + then if Z.leb (env x) 0 then -(env x) else 0 + else env v). + apply H with (env:=env') in H0. + + rewrite <- make_conj_impl in *. + intro. + rewrite !make_conj_cons in H0. + apply H0 ; repeat split. + * + apply eval_nformula_mk_eq_pos. + unfold env'. + rewrite! Pos.eqb_refl. + replace (x=?z1)%positive with false. + replace (x=?t1)%positive with false. + replace (t1=?z1)%positive with false. + destruct (env x <=? 0); ring. + { unfold t1. + pos_tac; normZ. + lia (Hyp H2). + } + { + unfold t1, z1. + pos_tac; normZ. + lia (Add (Hyp LE) (Hyp H3)). + } + { + unfold z1. + pos_tac; normZ. + lia (Add (Hyp LE) (Hyp H3)). + } + * + apply eval_nformula_bound_var. + unfold env'. + rewrite! Pos.eqb_refl. + destruct (env x <=? 0) eqn:EQ. + compute. congruence. + rewrite Z.leb_gt in EQ. + normZ. + lia (Add (Hyp EQ) (Hyp H2)). + * + apply eval_nformula_bound_var. + unfold env'. + rewrite! Pos.eqb_refl. + replace (t1 =? z1)%positive with false. + destruct (env x <=? 0) eqn:EQ. + rewrite Z.leb_le in EQ. + normZ. + lia (Add (Hyp EQ) (Hyp H2)). + compute; congruence. + unfold t1. + clear. + pos_tac; normZ. + lia (Hyp H). + * + rewrite agree_env_eval_nformulae with (env':= env') in H1;auto. + unfold agree_env; intros. + unfold env'. + replace (x0 =? z1)%positive with false. + replace (x0 =? t1)%positive with false. + reflexivity. + { + unfold t1, z1. + unfold fr in *. + apply Pos2Z.pos_le_pos in H2. + pos_tac; normZ. + lia (Add (Hyp H2) (Hyp H4)). + } + { + unfold z1, fr in *. + apply Pos2Z.pos_le_pos in H2. + pos_tac; normZ. + lia (Add (Hyp H2) (Hyp H4)). + } + + unfold ltof. + simpl. + apply Nat.lt_succ_diag_r. Qed. @@ -1417,7 +1673,7 @@ Qed. Definition ZTautoChecker (f : BFormula (Formula Z)) (w: list ZArithProof): bool := @tauto_checker (Formula Z) (NFormula Z) unit Zunsat Zdeduce normalise negate ZArithProof (fun cl => ZChecker (List.map fst cl)) f w. -Lemma ZTautoChecker_sound : forall f w, ZTautoChecker f w = true -> forall env, eval_f (fun x => x) (Zeval_formula env) f. +Lemma ZTautoChecker_sound : forall f w, ZTautoChecker f w = true -> forall env, eval_bf (Zeval_formula env) f. Proof. intros f w. unfold ZTautoChecker. @@ -1430,11 +1686,12 @@ Proof. - unfold Zdeduce. intros. revert H. apply (nformula_plus_nformula_correct Zsor ZSORaddon); auto. - - intros env t tg. - rewrite normalise_correct ; auto. + intros. + rewrite normalise_correct in H. + auto. - - intros env t tg. - rewrite negate_correct ; auto. + intros. + rewrite negate_correct in H ; auto. - intros t w0. unfold eval_tt. intros. @@ -1443,270 +1700,6 @@ Proof. tauto. Qed. -Record is_diff_env_elt (fr : positive) (env env' : positive -> Z) (x:positive):= - { - eq_env : env x = env' x; - eq_diff : env x = env' (xO (fr+ x)) - env' (xI (fr + x)); - pos_xO : env' (xO (fr+x)) >= 0; - pos_xI : env' (xI (fr+x)) >= 0; - }. - - -Definition is_diff_env (s : Vars.t) (env env' : positive -> Z) := - let fr := Pos.succ (Vars.max_element s) in - forall x, Vars.mem x s = true -> - is_diff_env_elt fr env env' x. - -Definition mk_diff_env (s : Vars.t) (env : positive -> Z) := - let fr := Vars.max_element s in - fun x => - if Pos.leb x fr - then env x - else - let fr' := Pos.succ fr in - match x with - | xO x => if Z.leb (env (x - fr')%positive) 0 - then 0 else env (x -fr')%positive - | xI x => if Z.leb (env (x - fr')%positive) 0 - then - (env (x - fr')%positive) else 0 - | xH => 0 - end. - -Lemma le_xO : forall x, (x <= xO x)%positive. -Proof. - intros. - change x with (1 * x)%positive at 1. - change (xO x) with (2 * x)%positive. - apply Pos.mul_le_mono. - compute. congruence. - apply Pos.le_refl. -Qed. - -Lemma leb_xO_false : - (forall x y, x <=? y = false -> - xO x <=? y = false)%positive. -Proof. - intros. - rewrite Pos.leb_nle in *. - intro. apply H. - eapply Pos.le_trans ; eauto. - apply le_xO. -Qed. - -Lemma leb_xI_false : - (forall x y, x <=? y = false -> - xI x <=? y = false)%positive. -Proof. - intros. - rewrite Pos.leb_nle in *. - intro. apply H. - eapply Pos.le_trans ; eauto. - generalize (le_xO x). - intros. - eapply Pos.le_trans ; eauto. - change (xI x) with (Pos.succ (xO x))%positive. - apply Pos.lt_le_incl. - apply Pos.lt_succ_diag_r. -Qed. - -Lemma is_diff_env_ex : forall s env, - is_diff_env s env (mk_diff_env s env). -Proof. - intros. - unfold is_diff_env, mk_diff_env. - intros. - assert - ((Pos.succ (Vars.max_element s) + x <=? Vars.max_element s = false)%positive). - { - rewrite Pos.leb_nle. - intro. - eapply (Pos.lt_irrefl (Pos.succ (Vars.max_element s) + x)). - eapply Pos.le_lt_trans ; eauto. - generalize (Pos.lt_succ_diag_r (Vars.max_element s)). - intro. - eapply Pos.lt_trans ; eauto. - apply Pos.lt_add_r. - } - constructor. - - apply Vars.max_element_max in H. - rewrite <- Pos.leb_le in H. - rewrite H. auto. - - - rewrite leb_xO_false by auto. - rewrite leb_xI_false by auto. - rewrite Pos.add_comm. - rewrite Pos.add_sub. - destruct (env x <=? 0); ring. - - rewrite leb_xO_false by auto. - rewrite Pos.add_comm. - rewrite Pos.add_sub. - destruct (env x <=? 0) eqn:EQ. - apply Z.le_ge. - apply Z.le_refl. - rewrite Z.leb_gt in EQ. - apply Z.le_ge. - apply Z.lt_le_incl. - auto. - - rewrite leb_xI_false by auto. - rewrite Pos.add_comm. - rewrite Pos.add_sub. - destruct (env x <=? 0) eqn:EQ. - rewrite Z.leb_le in EQ. - apply Z.le_ge. - apply Z.opp_nonneg_nonpos; auto. - apply Z.le_ge. - apply Z.le_refl. -Qed. - -Lemma env_bounds : forall tg env s, - let fr := Pos.succ (Vars.max_element s) in - exists env', is_diff_env s env env' - /\ - eval_bf (Zeval_formula env') (bound_vars tg fr s). -Proof. - intros. - assert (DIFF:=is_diff_env_ex s env). - exists (mk_diff_env s env). split ; auto. - unfold bound_vars. - rewrite FSetPositive.PositiveSet.fold_1. - revert DIFF. - set (env' := mk_diff_env s env). - intro. - assert (ACC : eval_bf (Zeval_formula env') TT ). - { - simpl. auto. - } - revert ACC. - match goal with - | |- context[@TT ?A ?B ?C ?D] => generalize (@TT A B C D) as acc - end. - unfold is_diff_env in DIFF. - assert (DIFFL : forall x, In x (FSetPositive.PositiveSet.elements s) -> - (x < fr)%positive /\ - is_diff_env_elt fr env env' x). - { - intros. - rewrite <- Vars.mem_elements in H. - split. - apply Vars.max_element_max in H. - unfold fr in *. - eapply Pos.le_lt_trans ; eauto. - apply Pos.lt_succ_diag_r. - apply DIFF; auto. - } - clear DIFF. - match goal with - | |- context[fold_left ?F _ _] => - set (FUN := F) - end. - induction (FSetPositive.PositiveSet.elements s). - - simpl; auto. - - simpl. - intros. - eapply IHl ; eauto. - + intros. apply DIFFL. - simpl ; auto. - + unfold FUN. - simpl. - split ; auto. - assert (HYP : (a < fr /\ is_diff_env_elt fr env env' a)%positive). - { - apply DIFFL. - simpl. tauto. - } - destruct HYP as (LT & DIFF). - destruct DIFF. - rewrite <- eq_env0. - tauto. -Qed. - -Definition agree_env (v : Vars.t) (env env' : positive -> Z) : Prop := - forall x, Vars.mem x v = true -> env x = env' x. - -Lemma agree_env_subset : forall s1 s2 env env', - agree_env s1 env env' -> - Vars.is_subset s2 s1 -> - agree_env s2 env env'. -Proof. - unfold agree_env. - intros. - apply H. apply H0; auto. -Qed. - -Lemma agree_env_union : forall s1 s2 env env', - agree_env (Vars.union s1 s2) env env' -> - agree_env s1 env env' /\ agree_env s2 env env'. -Proof. - split; - eapply agree_env_subset; eauto. - apply Vars.is_subset_union_l. - apply Vars.is_subset_union_r. -Qed. - - - -Lemma agree_env_eval_expr : - forall env env' e - (AGREE : agree_env (vars_of_pexpr e) env env'), - Zeval_expr env e = Zeval_expr env' e. -Proof. - induction e; simpl;intros; - try (apply agree_env_union in AGREE; destruct AGREE); try f_equal ; auto. - - intros ; apply AGREE. - apply Vars.mem_singleton. -Qed. - -Lemma agree_env_eval_bf : - forall env env' f - (AGREE: agree_env (vars_of_bformula f) env env'), - eval_bf (Zeval_formula env') f <-> - eval_bf (Zeval_formula env) f. -Proof. - induction f; simpl; intros ; - try (apply agree_env_union in AGREE; destruct AGREE) ; try intuition fail. - - - unfold Zeval_formula. - destruct t. - simpl in * ; intros. - apply agree_env_union in AGREE ; destruct AGREE. - rewrite <- agree_env_eval_expr with (env:=env) by auto. - rewrite <- agree_env_eval_expr with (e:= Frhs) (env:=env) by auto. - tauto. -Qed. - -Lemma bound_problem_sound : forall tg f, - (forall env' : PolEnv Z, - eval_bf (Zeval_formula env') - (bound_problem tg f)) -> - forall env, - eval_bf (Zeval_formula env) f. -Proof. - intros. - unfold bound_problem in H. - destruct (env_bounds tg env (vars_of_bformula f)) - as (env' & DIFF & EVAL). - simpl in H. - apply H in EVAL. - eapply agree_env_eval_bf ; eauto. - unfold is_diff_env, agree_env in *. - intros. - apply DIFF in H0. - destruct H0. - intuition. -Qed. - - - -Definition ZTautoCheckerExt (f : BFormula (Formula Z)) (w : list ZArithProof) : bool := - ZTautoChecker (bound_problem (fun _ _ _ => tt) f) w. - -Lemma ZTautoCheckerExt_sound : forall f w, ZTautoCheckerExt f w = true -> forall env, eval_bf (Zeval_formula env) f. -Proof. - intros. - unfold ZTautoCheckerExt in H. - specialize (ZTautoChecker_sound _ _ H). - intros ; apply bound_problem_sound with (tg:= fun _ _ _ => tt); auto. -Qed. Fixpoint xhyps_of_pt (base:nat) (acc : list nat) (pt:ZArithProof) : list nat := match pt with @@ -1716,6 +1709,7 @@ Fixpoint xhyps_of_pt (base:nat) (acc : list nat) (pt:ZArithProof) : list nat := | EnumProof c1 c2 l => let acc := xhyps_of_psatz base (xhyps_of_psatz base acc c2) c1 in List.fold_left (xhyps_of_pt (S base)) l acc + | ExProof _ pt => xhyps_of_pt (S (S (S base ))) acc pt end. Definition hyps_of_pt (pt : ZArithProof) : list nat := xhyps_of_pt 0 nil pt. diff --git a/plugins/micromega/Ztac.v b/plugins/micromega/Ztac.v new file mode 100644 index 0000000000..091f58a0ef --- /dev/null +++ b/plugins/micromega/Ztac.v @@ -0,0 +1,140 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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) *) +(************************************************************************) + +(** Tactics for doing arithmetic proofs. + Useful to bootstrap lia. + *) + +Require Import ZArithRing. +Require Import ZArith_base. +Local Open Scope Z_scope. + +Lemma eq_incl : + forall (x y:Z), x = y -> x <= y /\ y <= x. +Proof. + intros; split; + apply Z.eq_le_incl; auto. +Qed. + +Lemma elim_concl_eq : + forall x y, (x < y \/ y < x -> False) -> x = y. +Proof. + intros. + destruct (Z_lt_le_dec x y). + exfalso. apply H ; auto. + destruct (Zle_lt_or_eq y x);auto. + exfalso. + apply H ; auto. +Qed. + +Lemma elim_concl_le : + forall x y, (y < x -> False) -> x <= y. +Proof. + intros. + destruct (Z_lt_le_dec y x). + exfalso ; auto. + auto. +Qed. + +Lemma elim_concl_lt : + forall x y, (y <= x -> False) -> x < y. +Proof. + intros. + destruct (Z_lt_le_dec x y). + auto. + exfalso ; auto. +Qed. + + + +Lemma Zlt_le_add_1 : forall n m : Z, n < m -> n + 1 <= m. +Proof. exact (Zlt_le_succ). Qed. + + +Ltac normZ := + repeat + match goal with + | H : _ < _ |- _ => apply Zlt_le_add_1 in H + | H : ?Y <= _ |- _ => + lazymatch Y with + | 0 => fail + | _ => apply Zle_minus_le_0 in H + end + | H : _ >= _ |- _ => apply Z.ge_le in H + | H : _ > _ |- _ => apply Z.gt_lt in H + | H : _ = _ |- _ => apply eq_incl in H ; destruct H + | |- @eq Z _ _ => apply elim_concl_eq ; let H := fresh "HZ" in intros [H|H] + | |- _ <= _ => apply elim_concl_le ; intros + | |- _ < _ => apply elim_concl_lt ; intros + | |- _ >= _ => apply Z.le_ge + end. + + +Inductive proof := +| Hyp (e : Z) (prf : 0 <= e) +| Add (p1 p2: proof) +| Mul (p1 p2: proof) +| Cst (c : Z) +. + +Lemma add_le : forall e1 e2, 0 <= e1 -> 0 <= e2 -> 0 <= e1+e2. +Proof. + intros. + change 0 with (0+ 0). + apply Z.add_le_mono; auto. +Qed. + +Lemma mul_le : forall e1 e2, 0 <= e1 -> 0 <= e2 -> 0 <= e1*e2. +Proof. + intros. + change 0 with (0* e2). + apply Zmult_le_compat_r; auto. +Qed. + +Fixpoint eval_proof (p : proof) : { e : Z | 0 <= e} := + match p with + | Hyp e prf => exist _ e prf + | Add p1 p2 => let (e1,p1) := eval_proof p1 in + let (e2,p2) := eval_proof p2 in + exist _ _ (add_le _ _ p1 p2) + | Mul p1 p2 => let (e1,p1) := eval_proof p1 in + let (e2,p2) := eval_proof p2 in + exist _ _ (mul_le _ _ p1 p2) + | Cst c => match Z_le_dec 0 c with + | left prf => exist _ _ prf + | _ => exist _ _ Z.le_0_1 + end + end. + +Ltac lia_step p := + let H := fresh in + let prf := (eval cbn - [Z.le Z.mul Z.opp Z.sub Z.add] in (eval_proof p)) in + match prf with + | @exist _ _ _ ?P => pose proof P as H + end ; ring_simplify in H. + +Ltac lia_contr := + match goal with + | H : 0 <= - (Zpos _) |- _ => + rewrite <- Z.leb_le in H; + compute in H ; discriminate + | H : 0 <= (Zneg _) |- _ => + rewrite <- Z.leb_le in H; + compute in H ; discriminate + end. + + +Ltac lia p := + lia_step p ; lia_contr. + +Ltac slia H1 H2 := + normZ ; lia (Add (Hyp _ H1) (Hyp _ H2)). + +Arguments Hyp {_} prf. diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index f14db40d45..92a2222cfa 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -285,6 +285,7 @@ module M = struct let coq_ratProof = lazy (constant "RatProof") let coq_cutProof = lazy (constant "CutProof") let coq_enumProof = lazy (constant "EnumProof") + let coq_ExProof = lazy (constant "ExProof") let coq_Zgt = lazy (z_constant "Z.gt") let coq_Zge = lazy (z_constant "Z.ge") let coq_Zle = lazy (z_constant "Z.le") @@ -1420,6 +1421,9 @@ let rec dump_proof_term = function , [| dump_psatz coq_Z dump_z c1 ; dump_psatz coq_Z dump_z c2 ; dump_list (Lazy.force coq_proofTerm) dump_proof_term prfs |] ) + | Micromega.ExProof (p, prf) -> + EConstr.mkApp + (Lazy.force coq_ExProof, [|dump_positive p; dump_proof_term prf|]) let rec size_of_psatz = function | Micromega.PsatzIn _ -> 1 @@ -1437,6 +1441,7 @@ let rec size_of_pf = function | Micromega.EnumProof (p1, p2, l) -> size_of_psatz p1 + size_of_psatz p2 + List.fold_left (fun acc p -> size_of_pf p + acc) 0 l + | Micromega.ExProof (_, a) -> size_of_pf a + 1 let dump_proof_term t = if debug then Printf.printf "dump_proof_term %i\n" (size_of_pf t); @@ -1455,6 +1460,8 @@ let rec pp_proof_term o = function Printf.fprintf o "EP[%a,%a,%a]" (pp_psatz pp_z) c1 (pp_psatz pp_z) c2 (pp_list "[" "]" pp_proof_term) rst + | Micromega.ExProof (p, prf) -> + Printf.fprintf o "Ex[%a,%a]" pp_positive p pp_proof_term prf let rec parse_hyps gl parse_arith env tg hyps = match hyps with @@ -1504,33 +1511,6 @@ let qq_domain_spec = let max_tag f = 1 + Tag.to_int (Mc.foldA (fun t1 (t2, _) -> Tag.max t1 t2) f (Tag.from 0)) -(** For completeness of the cutting-plane procedure, - each variable 'x' is replaced by 'y' - 'z' where - 'y' and 'z' are positive *) -let pre_processZ mt f = - let x0 i = 2 * i in - let x1 i = (2 * i) + 1 in - let tag_of_var fr p b = - let ip = CoqToCaml.positive fr + CoqToCaml.positive p in - match b with - | None -> - let y = Mc.XO (Mc.Coq_Pos.add fr p) in - let z = Mc.XI (Mc.Coq_Pos.add fr p) in - let tag = Tag.from (-x0 (x0 ip)) in - let constr = Mc.mk_eq_pos p y z in - (tag, dump_cstr (Lazy.force coq_Z) dump_z constr) - | Some false -> - let y = Mc.XO (Mc.Coq_Pos.add fr p) in - let tag = Tag.from (-x0 (x1 ip)) in - let constr = Mc.bound_var (Mc.XO y) in - (tag, dump_cstr (Lazy.force coq_Z) dump_z constr) - | Some true -> - let z = Mc.XI (Mc.Coq_Pos.add fr p) in - let tag = Tag.from (-x1 (x1 ip)) in - let constr = Mc.bound_var (Mc.XI z) in - (tag, dump_cstr (Lazy.force coq_Z) dump_z constr) - in - Mc.bound_problem_fr tag_of_var mt f (** Naive topological sort of constr according to the subterm-ordering *) (* An element is minimal x is minimal w.r.t y if @@ -2225,6 +2205,7 @@ let hyps_of_pt pt = | Mc.EnumProof (c1, c2, l) -> let s = xhyps_of_cone base (xhyps_of_cone base acc c2) c1 in List.fold_left (fun s x -> xhyps (base + 1) x s) s l + | Mc.ExProof (_, pt) -> xhyps (base + 3) pt acc in xhyps 0 pt ISet.empty @@ -2242,6 +2223,7 @@ let compact_pt pt f = ( compact_cone c1 (translate ofset) , compact_cone c2 (translate ofset) , Mc.map (fun x -> compact_pt (ofset + 1) x) l ) + | Mc.ExProof (x, pt) -> Mc.ExProof (x, compact_pt (ofset + 3) pt) in compact_pt 0 pt @@ -2418,8 +2400,9 @@ let sos_Q = let sos_R = micromega_genr (non_linear_prover_R "pure_sos" None) let xlia = - micromega_gen parse_zarith pre_processZ Mc.cnfZ zz_domain_spec dump_zexpr - linear_Z + micromega_gen parse_zarith + (fun _ x -> x) + Mc.cnfZ zz_domain_spec dump_zexpr linear_Z let xnlia = micromega_gen parse_zarith diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml index f508b3dc56..d17a0aabb7 100644 --- a/plugins/micromega/micromega.ml +++ b/plugins/micromega/micromega.ml @@ -281,6 +281,20 @@ module Coq_Pos = let compare = compare_cont Eq + (** val max : positive -> positive -> positive **) + + let max p p' = + match compare p p' with + | Gt -> p + | _ -> p' + + (** val leb : positive -> positive -> bool **) + + let leb x y = + match compare x y with + | Gt -> false + | _ -> true + (** val gcdn : nat -> positive -> positive -> positive **) let rec gcdn n0 a b = @@ -1760,13 +1774,6 @@ let simpl_cone cO cI ctimes ceqb e = match e with | _ -> PsatzAdd (t1, t2))) | _ -> e -module PositiveSet = - struct - type tree = - | Leaf - | Node of tree * bool * tree - end - type q = { qnum : z; qden : positive } (** val qeq_bool : q -> q -> bool **) @@ -1980,6 +1987,7 @@ type zArithProof = | RatProof of zWitness * zArithProof | CutProof of zWitness * zArithProof | EnumProof of zWitness * zWitness * zArithProof list +| ExProof of positive * zArithProof (** val zgcdM : z -> z -> z **) @@ -2051,116 +2059,6 @@ let valid_cut_sign = function | NonStrict -> true | _ -> false -module Vars = - struct - type elt = positive - - type tree = PositiveSet.tree = - | Leaf - | Node of tree * bool * tree - - type t = tree - - (** val empty : t **) - - let empty = - Leaf - - (** val add : elt -> t -> t **) - - let rec add i = function - | Leaf -> - (match i with - | XI i0 -> Node (Leaf, false, (add i0 Leaf)) - | XO i0 -> Node ((add i0 Leaf), false, Leaf) - | XH -> Node (Leaf, true, Leaf)) - | Node (l, o, r) -> - (match i with - | XI i0 -> Node (l, o, (add i0 r)) - | XO i0 -> Node ((add i0 l), o, r) - | XH -> Node (l, true, r)) - - (** val singleton : elt -> t **) - - let singleton i = - add i empty - - (** val union : t -> t -> t **) - - let rec union m m' = - match m with - | Leaf -> m' - | Node (l, o, r) -> - (match m' with - | Leaf -> m - | Node (l', o', r') -> - Node ((union l l'), (if o then true else o'), (union r r'))) - - (** val rev_append : elt -> elt -> elt **) - - let rec rev_append y x = - match y with - | XI y0 -> rev_append y0 (XI x) - | XO y0 -> rev_append y0 (XO x) - | XH -> x - - (** val rev : elt -> elt **) - - let rev x = - rev_append x XH - - (** val xfold : (elt -> 'a1 -> 'a1) -> t -> 'a1 -> elt -> 'a1 **) - - let rec xfold f m v i = - match m with - | Leaf -> v - | Node (l, b, r) -> - if b - then xfold f r (f (rev i) (xfold f l v (XO i))) (XI i) - else xfold f r (xfold f l v (XO i)) (XI i) - - (** val fold : (elt -> 'a1 -> 'a1) -> t -> 'a1 -> 'a1 **) - - let fold f m i = - xfold f m i XH - end - -(** val vars_of_pexpr : z pExpr -> Vars.t **) - -let rec vars_of_pexpr = function -| PEc _ -> Vars.empty -| PEX x -> Vars.singleton x -| PEadd (e1, e2) -> - let v1 = vars_of_pexpr e1 in let v2 = vars_of_pexpr e2 in Vars.union v1 v2 -| PEsub (e1, e2) -> - let v1 = vars_of_pexpr e1 in let v2 = vars_of_pexpr e2 in Vars.union v1 v2 -| PEmul (e1, e2) -> - let v1 = vars_of_pexpr e1 in let v2 = vars_of_pexpr e2 in Vars.union v1 v2 -| PEopp c -> vars_of_pexpr c -| PEpow (e0, _) -> vars_of_pexpr e0 - -(** val vars_of_formula : z formula -> Vars.t **) - -let vars_of_formula f = - let { flhs = l; fop = _; frhs = r } = f in - let v1 = vars_of_pexpr l in let v2 = vars_of_pexpr r in Vars.union v1 v2 - -(** val vars_of_bformula : (z formula, 'a1, 'a2, 'a3) gFormula -> Vars.t **) - -let rec vars_of_bformula = function -| A (a, _) -> vars_of_formula a -| Cj (f1, f2) -> - let v1 = vars_of_bformula f1 in - let v2 = vars_of_bformula f2 in Vars.union v1 v2 -| D (f1, f2) -> - let v1 = vars_of_bformula f1 in - let v2 = vars_of_bformula f2 in Vars.union v1 v2 -| N f0 -> vars_of_bformula f0 -| I (f1, _, f2) -> - let v1 = vars_of_bformula f1 in - let v2 = vars_of_bformula f2 in Vars.union v1 v2 -| _ -> Vars.empty - (** val bound_var : positive -> z formula **) let bound_var v = @@ -2171,24 +2069,18 @@ let bound_var v = let mk_eq_pos x y t0 = { flhs = (PEX x); fop = OpEq; frhs = (PEsub ((PEX y), (PEX t0))) } -(** val bound_vars : - (positive -> positive -> bool option -> 'a2) -> positive -> Vars.t -> (z - formula, 'a1, 'a2, 'a3) gFormula **) +(** val max_var : positive -> z pol -> positive **) -let bound_vars tag_of_var fr v = - Vars.fold (fun k acc -> - let y = XO (Coq_Pos.add fr k) in - let z0 = XI (Coq_Pos.add fr k) in - Cj ((Cj ((A ((mk_eq_pos k y z0), (tag_of_var fr k None))), (Cj ((A - ((bound_var y), (tag_of_var fr k (Some false)))), (A ((bound_var z0), - (tag_of_var fr k (Some true)))))))), acc)) v TT +let rec max_var jmp = function +| Pc _ -> jmp +| Pinj (j, p2) -> max_var (Coq_Pos.add j jmp) p2 +| PX (p2, _, q0) -> + Coq_Pos.max (max_var jmp p2) (max_var (Coq_Pos.succ jmp) q0) -(** val bound_problem_fr : - (positive -> positive -> bool option -> 'a2) -> positive -> (z formula, - 'a1, 'a2, 'a3) gFormula -> (z formula, 'a1, 'a2, 'a3) gFormula **) +(** val max_var_nformulae : z nFormula list -> positive **) -let bound_problem_fr tag_of_var fr f = - let v = vars_of_bformula f in I ((bound_vars tag_of_var fr v), None, f) +let max_var_nformulae l = + fold_left (fun acc f -> Coq_Pos.max acc (max_var XH (fst f))) l XH (** val zChecker : z nFormula list -> zArithProof -> bool **) @@ -2232,6 +2124,16 @@ let rec zChecker l = function | None -> true) | None -> false) | None -> false) +| ExProof (x, prf) -> + let fr = max_var_nformulae l in + if Coq_Pos.leb x fr + then let z0 = Coq_Pos.succ fr in + let t0 = Coq_Pos.succ z0 in + let nfx = xnnormalise (mk_eq_pos x z0 t0) in + let posz = xnnormalise (bound_var z0) in + let post = xnnormalise (bound_var t0) in + zChecker (nfx::(posz::(post::l))) prf + else false (** val zTautoChecker : z formula bFormula -> zArithProof list -> bool **) diff --git a/plugins/micromega/micromega.mli b/plugins/micromega/micromega.mli index 033f5d8732..4200c80574 100644 --- a/plugins/micromega/micromega.mli +++ b/plugins/micromega/micromega.mli @@ -47,6 +47,8 @@ module Coq_Pos : sig val size_nat : positive -> nat val compare_cont : comparison -> positive -> positive -> comparison val compare : positive -> positive -> comparison + val max : positive -> positive -> positive + val leb : positive -> positive -> bool val gcdn : nat -> positive -> positive -> positive val gcd : positive -> positive -> positive val of_succ_nat : nat -> positive @@ -624,10 +626,6 @@ val simpl_cone : -> 'a1 psatz -> 'a1 psatz -module PositiveSet : sig - type tree = Leaf | Node of tree * bool * tree -end - type q = {qnum : z; qden : positive} val qeq_bool : q -> q -> bool @@ -672,6 +670,7 @@ type zArithProof = | RatProof of zWitness * zArithProof | CutProof of zWitness * zArithProof | EnumProof of zWitness * zWitness * zArithProof list + | ExProof of positive * zArithProof val zgcdM : z -> z -> z val zgcd_pol : z polC -> z * z @@ -682,40 +681,10 @@ val nformula_of_cutting_plane : (z polC * z) * op1 -> z nFormula val is_pol_Z0 : z polC -> bool val eval_Psatz0 : z nFormula list -> zWitness -> z nFormula option val valid_cut_sign : op1 -> bool - -module Vars : sig - type elt = positive - type tree = PositiveSet.tree = Leaf | Node of tree * bool * tree - type t = tree - - val empty : t - val add : elt -> t -> t - val singleton : elt -> t - val union : t -> t -> t - val rev_append : elt -> elt -> elt - val rev : elt -> elt - val xfold : (elt -> 'a1 -> 'a1) -> t -> 'a1 -> elt -> 'a1 - val fold : (elt -> 'a1 -> 'a1) -> t -> 'a1 -> 'a1 -end - -val vars_of_pexpr : z pExpr -> Vars.t -val vars_of_formula : z formula -> Vars.t -val vars_of_bformula : (z formula, 'a1, 'a2, 'a3) gFormula -> Vars.t val bound_var : positive -> z formula val mk_eq_pos : positive -> positive -> positive -> z formula - -val bound_vars : - (positive -> positive -> bool option -> 'a2) - -> positive - -> Vars.t - -> (z formula, 'a1, 'a2, 'a3) gFormula - -val bound_problem_fr : - (positive -> positive -> bool option -> 'a2) - -> positive - -> (z formula, 'a1, 'a2, 'a3) gFormula - -> (z formula, 'a1, 'a2, 'a3) gFormula - +val max_var : positive -> z pol -> positive +val max_var_nformulae : z nFormula list -> positive val zChecker : z nFormula list -> zArithProof -> bool val zTautoChecker : z formula bFormula -> zArithProof list -> bool diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index d92b409ba1..03f042647c 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.ml @@ -294,7 +294,7 @@ end *) module type Tag = sig - type t + type t = int val from : int -> t val next : t -> t @@ -319,7 +319,9 @@ end * MODULE: Ordered sets of tags. *) -module TagSet = Set.Make (Tag) +module TagSet = struct + include Set.Make (Tag) +end (** As for Unix.close_process, our Unix.waipid will ignore all EINTR *) diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml index adf54713b9..a4f9b60b14 100644 --- a/plugins/micromega/polynomial.ml +++ b/plugins/micromega/polynomial.ml @@ -15,8 +15,7 @@ (************************************************************************) open Num -module Utils = Mutils -open Utils +open Mutils module Mc = Micromega let max_nb_cstr = ref max_int @@ -43,6 +42,7 @@ module Monomial : sig val fold : (var -> int -> 'a -> 'a) -> t -> 'a -> 'a val sqrt : t -> t option val variables : t -> ISet.t + val degree : t -> int end = struct (* A monomial is represented by a multiset of variables *) module Map = Map.Make (Int) @@ -50,6 +50,8 @@ end = struct type t = int Map.t + let degree m = Map.fold (fun _ i d -> i + d) m 0 + let is_singleton m = try let k, v = choose m in @@ -280,10 +282,11 @@ module LinPoly = struct let (monomial_of_index : Monomial.t IntMap.t ref) = ref IntMap.empty let fresh = ref 0 - let clear () = - index_of_monomial := MonoMap.empty; - monomial_of_index := IntMap.empty; - fresh := 0 + let reserve vr = + if !fresh > vr then failwith (Printf.sprintf "Cannot reserve %i" vr) + else fresh := vr + 1 + + let get_fresh () = !fresh let register m = try MonoMap.find m !index_of_monomial @@ -295,6 +298,13 @@ module LinPoly = struct res let retrieve i = IntMap.find i !monomial_of_index + + let clear () = + index_of_monomial := MonoMap.empty; + monomial_of_index := IntMap.empty; + fresh := 0; + ignore (register Monomial.const) + let _ = register Monomial.const end @@ -389,6 +399,11 @@ module LinPoly = struct (fun acc v _ -> ISet.union (Monomial.variables (MonT.retrieve v)) acc) ISet.empty p + let monomials p = Vect.fold (fun acc v _ -> ISet.add v acc) ISet.empty p + + let degree v = + Vect.fold (fun acc v vl -> max acc (Monomial.degree (MonT.retrieve v))) 0 v + let pp_goal typ o l = let vars = List.fold_left @@ -433,6 +448,9 @@ module ProofFormat = struct | Done | Step of int * prf_rule * proof | Enum of int * prf_rule * Vect.t * prf_rule * proof list + | ExProof of int * int * int * var * var * var * proof + + (* x = z - t, z >= 0, t >= 0 *) let rec output_prf_rule o = function | Annot (s, p) -> Printf.fprintf o "(%a)@%s" output_prf_rule p s @@ -459,6 +477,9 @@ module ProofFormat = struct | Enum (i, p1, v, p2, pl) -> Printf.fprintf o "%i{%a<=%a<=%a}%a" i output_prf_rule p1 Vect.pp v output_prf_rule p2 (pp_list ";" output_proof) pl + | ExProof (i, j, k, x, z, t, pr) -> + Printf.fprintf o "%i := %i = %i - %i ; %i := %i >= 0 ; %i := %i >= 0 ; %a" + i x z t j z k t output_proof pr let rec pr_size = function | Annot (_, p) -> pr_size p @@ -485,6 +506,8 @@ module ProofFormat = struct | Enum (i, p1, _, p2, l) -> let m = max (pr_rule_max_id p1) (pr_rule_max_id p2) in List.fold_left (fun i prf -> max i (proof_max_id prf)) (max i m) l + | ExProof (i, j, k, _, _, _, prf) -> + max (max (max i j) k) (proof_max_id prf) let rec pr_rule_def_cut id = function | Annot (_, p) -> pr_rule_def_cut id p @@ -544,6 +567,16 @@ module ProofFormat = struct (ISet.union (ISet.union (pr_rule_collect_hyps p1) (pr_rule_collect_hyps p2)) hyps) ) + | ExProof (i, j, k, x, z, t, prf) -> + let prf', hyps = simplify_proof prf in + if + (not (ISet.mem i hyps)) + && (not (ISet.mem j hyps)) + && not (ISet.mem k hyps) + then (prf', hyps) + else + ( ExProof (i, j, k, x, z, t, prf') + , ISet.add i (ISet.add j (ISet.add k hyps)) ) in fst (simplify_proof p) @@ -561,6 +594,9 @@ module ProofFormat = struct bds in (id, prf) + | ExProof (i, j, k, x, z, t, prf) -> + let id, prf = normalise_proof id prf in + (id, ExProof (i, j, k, x, z, t, prf)) | Enum (i, p1, v, p2, pl) -> (* Why do I have top-level cuts ? *) (* let p1 = implicit_cut p1 in @@ -608,9 +644,9 @@ module ProofFormat = struct let rec compare p1 p2 = match (p1, p2) with | Annot (s1, p1), Annot (s2, p2) -> - if s1 = s2 then compare p1 p2 else Util.pervasives_compare s1 s2 - | Hyp i, Hyp j -> Util.pervasives_compare i j - | Def i, Def j -> Util.pervasives_compare i j + if s1 = s2 then compare p1 p2 else String.compare s1 s2 + | Hyp i, Hyp j -> Int.compare i j + | Def i, Def j -> Int.compare i j | Cst n, Cst m -> Num.compare_num n m | Zero, Zero -> 0 | Square v1, Square v2 -> Vect.compare v1 v2 @@ -623,7 +659,7 @@ module ProofFormat = struct | AddPrf (p1, q1), MulPrf (p2, q2) -> cmp_pair compare compare (p1, q1) (p2, q2) | CutPrf p, CutPrf p' -> compare p p' - | _, _ -> Util.pervasives_compare (id_of_constr p1) (id_of_constr p2) + | _, _ -> Int.compare (id_of_constr p1) (id_of_constr p2) end let add_proof x y = @@ -759,6 +795,8 @@ module ProofFormat = struct ( cmpl_prf_rule_z env p1 , cmpl_prf_rule_z env p2 , List.map (cmpl_proof (i :: env)) l ) + | ExProof (i, j, k, x, _, _, prf) -> + Mc.ExProof (CamlToCoq.positive x, cmpl_proof (i :: j :: k :: env) prf) let compile_proof env prf = let id = 1 + proof_max_id prf in @@ -818,6 +856,7 @@ module ProofFormat = struct let _ = eval_prf_rule (fun i -> IMap.find i env) r2 in (* Should check bounds *) failwith "Not implemented" + | ExProof _ -> failwith "Not implemented" end module WithProof = struct @@ -852,7 +891,10 @@ module WithProof = struct let n, r = Vect.decomp_cst p in if Vect.is_null r && n >/ Int 0 then ((LinPoly.product p p1, o1), ProofFormat.mul_cst_proof n prf1) - else raise InvalidProof + else ( + Printf.printf "mult_error %a [*] %a\n" LinPoly.pp p output + ((p1, o1), prf1); + raise InvalidProof ) let cutting_plane ((p, o), prf) = let c, p' = Vect.decomp_cst p in diff --git a/plugins/micromega/polynomial.mli b/plugins/micromega/polynomial.mli index e7c619affc..7e905ac69b 100644 --- a/plugins/micromega/polynomial.mli +++ b/plugins/micromega/polynomial.mli @@ -23,6 +23,9 @@ module Monomial : sig (** [fold f m acc] folds over the variables with multiplicities *) + val degree : t -> int + (** [degree m] is the sum of the degrees of each variable *) + val const : t (** [const] @return the empty monomial i.e. without any variable *) @@ -33,6 +36,10 @@ module Monomial : sig (** [var x] @return the monomial x^1 *) + val prod : t -> t -> t + (** [prod n m] + @return the monomial n*m *) + val sqrt : t -> t option (** [sqrt m] @return [Some r] iff r^2 = m *) @@ -142,6 +149,12 @@ module LinPoly : sig val clear : unit -> unit (** [clear ()] clears the mapping. *) + val reserve : int -> unit + (** [reserve i] reserves the integer i *) + + val get_fresh : unit -> int + (** [get_fresh ()] return the first fresh variable *) + val retrieve : int -> Monomial.t (** [retrieve x] @return the monomial corresponding to the variable [x] *) @@ -225,6 +238,14 @@ module LinPoly : sig @return a mapping m such that m[s] = s^2 for every s^2 that is a monomial of [p] *) + val monomials : t -> ISet.t + (** [monomials p] + @return the set of monomials. *) + + val degree : t -> int + (** [degree p] + @return return the maximum degree *) + val pp_var : out_channel -> var -> unit (** [pp_var o v] pretty-prints a monomial indexed by v. *) @@ -260,6 +281,9 @@ module ProofFormat : sig | Done | Step of int * prf_rule * proof | Enum of int * prf_rule * Vect.t * prf_rule * proof list + | ExProof of int * int * int * var * var * var * proof + + (* x = z - t, z >= 0, t >= 0 *) val pr_size : prf_rule -> Num.num val pr_rule_max_id : prf_rule -> int diff --git a/plugins/micromega/simplex.ml b/plugins/micromega/simplex.ml index 5bda268035..ade8143f3c 100644 --- a/plugins/micromega/simplex.ml +++ b/plugins/micromega/simplex.ml @@ -9,8 +9,6 @@ (************************************************************************) open Polynomial -(** A naive simplex *) - open Num (*open Util*) @@ -61,6 +59,12 @@ let output_tableau o t = (fun k v -> Printf.fprintf o "%a = %a\n" LinPoly.pp_var k pp_row v) t +let output_env o t = + IMap.iter + (fun k v -> + Printf.fprintf o "%a : %a\n" LinPoly.pp_var k WithProof.output v) + t + let output_vars o m = IMap.iter (fun k _ -> Printf.fprintf o "%a " LinPoly.pp_var k) m @@ -329,16 +333,6 @@ open Mutils open Polynomial -let fresh_var l = - 1 - + - try - ISet.max_elt - (List.fold_left - (fun acc c -> ISet.union acc (Vect.variables c.coeffs)) - ISet.empty l) - with Not_found -> 0 - (*type varmap = (int * bool) IMap.t*) let make_certificate vm l = @@ -349,6 +343,12 @@ let make_certificate vm l = Vect.set x' (if b then n else Num.minus_num n) acc) Vect.null l) +(** [eliminate_equalities vr0 l] + represents an equality e = 0 of index idx in the list l + by 2 constraints (vr:e >= 0) and (vr+1:-e >= 0) + The mapping vm maps vr to idx + *) + let eliminate_equalities (vr0 : var) (l : Polynomial.cstr list) = let rec elim idx vr vm l acc = match l with @@ -374,6 +374,9 @@ let find_solution rst tbl = else Vect.set vr (Vect.get_cst v) res) tbl Vect.null +let find_full_solution rst tbl = + IMap.fold (fun vr v res -> Vect.set vr (Vect.get_cst v) res) tbl Vect.null + let choose_conflict (sol : Vect.t) (l : (var * Vect.t) list) = let esol = Vect.set 0 (Int 1) sol in let rec most_violating l e (x, v) rst = @@ -404,12 +407,22 @@ let rec solve opt l (rst : Restricted.t) (t : tableau) = | Unsat c -> Inr c ) let find_unsat_certificate (l : Polynomial.cstr list) = - let vr = fresh_var l in + let vr = LinPoly.MonT.get_fresh () in let _, vm, l' = eliminate_equalities vr l in match solve false l' (Restricted.make vr) IMap.empty with | Inr c -> Some (make_certificate vm c) | Inl _ -> None +let fresh_var l = + 1 + + + try + ISet.max_elt + (List.fold_left + (fun acc c -> ISet.union acc (Vect.variables c.coeffs)) + ISet.empty l) + with Not_found -> 0 + let find_point (l : Polynomial.cstr list) = let vr = fresh_var l in let _, vm, l' = eliminate_equalities vr l in @@ -418,7 +431,7 @@ let find_point (l : Polynomial.cstr list) = | _ -> None let optimise obj l = - let vr0 = fresh_var l in + let vr0 = LinPoly.MonT.get_fresh () in let _, vm, l' = eliminate_equalities (vr0 + 1) l in let bound pos res = match res with @@ -471,43 +484,17 @@ let make_farkas_proof (env : WithProof.t IMap.t) vm v = let frac_num n = n -/ Num.floor_num n -(* [resolv_var v rst tbl] returns (if it exists) a restricted variable vr such that v = vr *) -exception FoundVar of int - -let resolve_var v rst tbl = - let v = Vect.set v (Int 1) Vect.null in - try - IMap.iter - (fun k vect -> - if Restricted.is_restricted k rst then - if Vect.equal v vect then raise (FoundVar k) else ()) - tbl; - None - with FoundVar k -> Some k - -let prepare_cut env rst tbl x v = - (* extract the unrestricted part *) - let unrst, rstv = - Vect.partition - (fun x vl -> - (not (Restricted.is_restricted x rst)) && frac_num vl <>/ Int 0) - (Vect.set 0 (Int 0) v) - in - if Vect.is_null unrst then Some rstv - else - Some - (Vect.fold - (fun acc k i -> - match resolve_var k rst tbl with - | None -> acc (* Should not happen *) - | Some v' -> Vect.set v' i acc) - rstv unrst) +type ('a, 'b) hitkind = + | Forget + (* Not interesting *) + | Hit of 'a + (* Yes, we have a positive result *) + | Keep of 'b let cut env rmin sol vm (rst : Restricted.t) tbl (x, v) = - (* Printf.printf "Trying to cut %i\n" x;*) let n, r = Vect.decomp_cst v in let f = frac_num n in - if f =/ Int 0 then None (* The solution is integral *) + if f =/ Int 0 then Forget (* The solution is integral *) else (* This is potentially a cut *) let t = @@ -522,11 +509,11 @@ let cut env rmin sol vm (rst : Restricted.t) tbl (x, v) = in let cut_coeff2 v = frac_num (t */ v) in let cut_vector ccoeff = - match prepare_cut env rst tbl x v with - | None -> Vect.null - | Some r -> - (*Printf.printf "Potential cut %a\n" LinPoly.pp r;*) - Vect.fold (fun acc x n -> Vect.set x (ccoeff n) acc) Vect.null r + Vect.fold + (fun acc x n -> + if Restricted.is_restricted x rst then Vect.set x (ccoeff n) acc + else acc) + Vect.null r in let lcut = List.map @@ -538,52 +525,100 @@ let cut env rmin sol vm (rst : Restricted.t) tbl (x, v) = match WithProof.cutting_plane c with | None -> if debug then - Printf.printf "This is not cutting plane for %a\n%a:" LinPoly.pp_var x - WithProof.output c; + Printf.printf "This is not a cutting plane for %a\n%a:" LinPoly.pp_var + x WithProof.output c; None | Some (v, prf) -> - if debug then begin + if debug then ( Printf.printf "This is a cutting plane for %a:" LinPoly.pp_var x; - Printf.printf " %a\n" WithProof.output (v, prf) - end; + Printf.printf " %a\n" WithProof.output (v, prf) ); if snd v = Eq then (* Unsat *) Some (x, (v, prf)) else let vl = Vect.dotproduct (fst v) (Vect.set 0 (Int 1) sol) in - if eval_op Ge vl (Int 0) then begin - (* Can this happen? *) + if eval_op Ge vl (Int 0) then ( if debug then - Printf.printf "The cut is feasible %s >= 0 ??\n" + Printf.printf "The cut is feasible %s >= 0 \n" (Num.string_of_num vl); - None - end + None ) else Some (x, (v, prf)) in - find_some check_cutting_plane lcut + match find_some check_cutting_plane lcut with + | Some r -> Hit r + | None -> Keep (x, v) + +let merge_result_old oldr f x = + match oldr with + | Hit v -> Hit v + | Forget -> ( + match f x with Forget -> Forget | Hit v -> Hit v | Keep v -> Keep v ) + | Keep v -> ( + match f x with Forget -> Keep v | Keep v' -> Keep v | Hit v -> Hit v ) + +let merge_best lt oldr newr = + match (oldr, newr) with + | x, Forget -> x + | Hit v, Hit v' -> if lt v v' then Hit v else Hit v' + | _, Hit v | Hit v, _ -> Hit v + | Forget, Keep v -> Keep v + | Keep v, Keep v' -> Keep v' let find_cut nb env u sol vm rst tbl = if nb = 0 then IMap.fold - (fun x v acc -> - match acc with - | None -> cut env u sol vm rst tbl (x, v) - | Some c -> Some c) - tbl None + (fun x v acc -> merge_result_old acc (cut env u sol vm rst tbl) (x, v)) + tbl Forget else + let lt (_, (_, p1)) (_, (_, p2)) = + ProofFormat.pr_size p1 </ ProofFormat.pr_size p2 + in IMap.fold - (fun x v acc -> - match (cut env u sol vm rst tbl (x, v), acc) with - | None, Some r | Some r, None -> Some r - | None, None -> None - | Some (v, ((lp, o), p1)), Some (v', ((lp', o'), p2)) -> - Some - ( if ProofFormat.pr_size p1 </ ProofFormat.pr_size p2 then - (v, ((lp, o), p1)) - else (v', ((lp', o'), p2)) )) - tbl None + (fun x v acc -> merge_best lt acc (cut env u sol vm rst tbl (x, v))) + tbl Forget + +let var_of_vect v = fst (fst (Vect.decomp_fst v)) + +let eliminate_variable (bounded, vr, env, tbl) x = + if debug then + Printf.printf "Eliminating variable %a from tableau\n%a\n" LinPoly.pp_var x + output_tableau tbl; + (* We identify the new variables with the constraint. *) + LinPoly.MonT.reserve vr; + let z = LinPoly.var (vr + 1) in + let zv = var_of_vect z in + let t = LinPoly.var (vr + 2) in + let tv = var_of_vect t in + (* x = z - t *) + let xdef = Vect.add z (Vect.uminus t) in + let xp = ((Vect.set x (Int 1) (Vect.uminus xdef), Eq), Def vr) in + let zp = ((z, Ge), Def zv) in + let tp = ((t, Ge), Def tv) in + (* Pivot the current tableau using xdef *) + let tbl = IMap.map (fun v -> Vect.subst x xdef v) tbl in + (* Pivot the environment *) + let env = + IMap.map + (fun lp -> + let (v, o), p = lp in + let ai = Vect.get x v in + if ai =/ Int 0 then lp + else + WithProof.addition + (WithProof.mult (Vect.cst (Num.minus_num ai)) xp) + lp) + env + in + (* Add the variables to the environment *) + let env = IMap.add vr xp (IMap.add zv zp (IMap.add tv tp env)) in + (* Remember the mapping *) + let bounded = IMap.add x (vr, zv, tv) bounded in + if debug then ( + Printf.printf "Tableau without\n %a\n" output_tableau tbl; + Printf.printf "Environment\n %a\n" output_env env ); + (bounded, vr + 3, env, tbl) let integer_solver lp = let l, _ = List.split lp in - let vr0 = fresh_var l in + let vr0 = 3 * LinPoly.MonT.get_fresh () in let vr, vm, l' = eliminate_equalities vr0 l in let _, env = env_of_list (List.map WithProof.of_cstr lp) in let insert_row vr v rst tbl = @@ -601,24 +636,46 @@ let integer_solver lp = if debug then begin Printf.fprintf stdout "Looking for a cut\n"; Printf.fprintf stdout "Restricted %a ...\n" Restricted.pp rst; - Printf.fprintf stdout "Current Tableau\n%a\n" output_tableau tbl + Printf.fprintf stdout "Current Tableau\n%a\n" output_tableau tbl; + flush stdout (* Printf.fprintf stdout "Bounding box\n%a\n" output_box (bounding_box (vr+1) rst tbl l')*) end; - let sol = find_solution rst tbl in + let sol = find_full_solution rst tbl in match find_cut (!nb mod 2) env cr (*x*) sol vm rst tbl with - | None -> None - | Some (cr, ((v, op), cut)) -> ( + | Forget -> + None (* There is no hope, there should be an integer solution *) + | Hit (cr, ((v, op), cut)) -> if op = Eq then (* This is a contradiction *) Some (Step (vr, CutPrf cut, Done)) - else + else ( + LinPoly.MonT.reserve vr; let res = insert_row vr v (Restricted.set_exc vr rst) tbl in let prf = isolve (IMap.add vr ((v, op), Def vr) env) (Some cr) (vr + 1) res in match prf with | None -> None - | Some p -> Some (Step (vr, CutPrf cut, p)) ) ) + | Some p -> Some (Step (vr, CutPrf cut, p)) ) + | Keep (x, v) -> ( + if debug then + Printf.fprintf stdout "Remove %a from Tableau\n" LinPoly.pp_var x; + let bounded, vr, env, tbl = + Vect.fold + (fun acc x n -> + if x <> 0 && not (Restricted.is_restricted x rst) then + eliminate_variable acc x + else acc) + (IMap.empty, vr, env, tbl) v + in + let prf = isolve env cr vr (Inl (rst, tbl, None)) in + match prf with + | None -> None + | Some pf -> + Some + (IMap.fold + (fun x (vr, zv, tv) acc -> ExProof (vr, zv, tv, x, zv, tv, acc)) + bounded pf) ) ) in let res = solve true l' (Restricted.make vr0) IMap.empty in isolve env None vr res diff --git a/plugins/micromega/vect.ml b/plugins/micromega/vect.ml index 581dc79cef..f53a7b42c9 100644 --- a/plugins/micromega/vect.ml +++ b/plugins/micromega/vect.ml @@ -19,6 +19,7 @@ type var = int *) type t = (var * num) list +type vector = t (** [equal v1 v2 = true] if the vectors are syntactically equal. *) @@ -134,7 +135,7 @@ let rec add (ve1 : t) (ve2 : t) = match (ve1, ve2) with | [], v | v, [] -> v | (v1, c1) :: l1, (v2, c2) :: l2 -> - let cmp = Util.pervasives_compare v1 v2 in + let cmp = Int.compare v1 v2 in if cmp == 0 then let s = add_num c1 c2 in if eq_num (Int 0) s then add l1 l2 else (v1, s) :: add l1 l2 @@ -146,7 +147,7 @@ let rec xmul_add (n1 : num) (ve1 : t) (n2 : num) (ve2 : t) = | [], _ -> mul n2 ve2 | _, [] -> mul n1 ve1 | (v1, c1) :: l1, (v2, c2) :: l2 -> - let cmp = Util.pervasives_compare v1 v2 in + let cmp = Int.compare v1 v2 in if cmp == 0 then let s = (n1 */ c1) +/ (n2 */ c2) in if eq_num (Int 0) s then xmul_add n1 l1 n2 l2 @@ -195,6 +196,17 @@ let rec decomp_at i v = if i = vr then (vl, r) else if i < vr then (Int 0, v) else decomp_at i r let decomp_fst v = match v with [] -> ((0, Int 0), []) | x :: v -> (x, v) + +let rec subst (vr : int) (e : t) (v : t) = + match v with + | [] -> [] + | (x, n) :: v' -> ( + match Int.compare vr x with + | 0 -> mul_add n e (Int 1) v' + | -1 -> v + | 1 -> add [(x, n)] (subst vr e v') + | _ -> assert false ) + let fold f acc v = List.fold_left (fun acc (v, i) -> f acc v i) acc v let fold_error f acc v = @@ -269,3 +281,13 @@ let abs_min_elt v = let partition p = List.partition (fun (vr, vl) -> p vr vl) let mkvar x = set x (Int 1) null + +module Bound = struct + type t = {cst : num; var : var; coeff : num} + + let of_vect (v : vector) = + match v with + | [(x, v)] -> if x = 0 then None else Some {cst = Int 0; var = x; coeff = v} + | [(0, v); (x, v')] -> Some {cst = v; var = x; coeff = v'} + | _ -> None +end diff --git a/plugins/micromega/vect.mli b/plugins/micromega/vect.mli index 83d9ef32b0..4b814cbb82 100644 --- a/plugins/micromega/vect.mli +++ b/plugins/micromega/vect.mli @@ -25,6 +25,8 @@ type t are not represented. *) +type vector = t + (** {1 Generic functions} *) (** [hash] [equal] and [compare] so that Vect.t can be used as @@ -135,6 +137,9 @@ val mul : num -> t -> t val mul_add : num -> t -> num -> t -> t (** [mul_add c1 v1 c2 v2] returns the linear combination c1.v1+c2.v2 *) +val subst : int -> t -> t -> t +(** [subst x v v'] replaces x by v in vector v' *) + val div : num -> t -> t (** [div c1 v1] returns the mutiplication by the inverse of c1 i.e (1/c1).v1 *) @@ -170,3 +175,10 @@ val dotproduct : t -> t -> num val map : (var -> num -> 'a) -> t -> 'a list val abs_min_elt : t -> (var * num) option val partition : (var -> num -> bool) -> t -> t * t + +module Bound : sig + type t = {cst : num; var : var; coeff : num} + (** represents a0 + ai.xi *) + + val of_vect : vector -> t option +end diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 70b7d68670..43f9e55e14 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -288,16 +288,18 @@ let check_extra_evars_are_solved env current_sigma frozen = match frozen with (* [check_evars] fails if some unresolved evar remains *) -let check_evars env initial_sigma sigma c = +let check_evars env ?initial sigma c = let rec proc_rec c = match EConstr.kind sigma c with | Evar (evk, _) -> - if not (Evd.mem initial_sigma evk) then - let (loc,k) = evar_source evk sigma in - begin match k with - | Evar_kinds.ImplicitArg (gr, (i, id), false) -> () - | _ -> Pretype_errors.error_unsolvable_implicit ?loc env sigma evk None - end + (match initial with + | Some initial when Evd.mem initial evk -> () + | _ -> + let (loc,k) = evar_source evk sigma in + begin match k with + | Evar_kinds.ImplicitArg (gr, (i, id), false) -> () + | _ -> Pretype_errors.error_unsolvable_implicit ?loc env sigma evk None + end) | _ -> EConstr.iter sigma proc_rec c in proc_rec c diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 2628d88e17..18e416596e 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -115,9 +115,10 @@ val solve_remaining_evars : ?hook:inference_hook -> inference_flags -> val check_evars_are_solved : program_mode:bool -> env -> ?initial:evar_map -> (* current map: *) evar_map -> unit -(** [check_evars env initial_sigma extended_sigma c] fails if some - new unresolved evar remains in [c] *) -val check_evars : env -> evar_map -> evar_map -> constr -> unit +(** [check_evars env ?initial sigma c] fails if some unresolved evar + remains in [c] which isn't in [initial] (any unresolved evar if + [initial] not provided) *) +val check_evars : env -> ?initial:evar_map -> evar_map -> constr -> unit (**/**) (** Internal of Pretyping... *) diff --git a/tactics/declare.ml b/tactics/declare.ml index fb06bb8a4f..da4de3df77 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -56,7 +56,7 @@ let declare_universe_context ~poly ctx = let nas = name_instance (Univ.UContext.instance uctx) in Global.push_section_context (nas, uctx) else - Global.push_context_set false ctx + Global.push_context_set ~strict:true ctx (** Declaration of constants and parameters *) diff --git a/tactics/hints.ml b/tactics/hints.ml index eb50a2a67c..7b3797119a 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1289,8 +1289,7 @@ let prepare_hint check env init (sigma,c) = mkNamedLambda (make_annot id Sorts.Relevant) t (iter (replace_term sigma evar (mkVar id) c)) in let c' = iter c in let env = Global.env () in - let empty_sigma = Evd.from_env env in - if check then Pretyping.check_evars env empty_sigma sigma c'; + if check then Pretyping.check_evars env sigma c'; let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in (c', diff) diff --git a/test-suite/micromega/bug_11270.v b/test-suite/micromega/bug_11270.v new file mode 100644 index 0000000000..80abc6d0e9 --- /dev/null +++ b/test-suite/micromega/bug_11270.v @@ -0,0 +1,6 @@ +Require Import Psatz. +Theorem foo : forall a b, 1 <= S (a + a * S b). +Proof. +intros. +lia. +Qed. diff --git a/test-suite/output/MExtraction.v b/test-suite/output/MExtraction.v index 668be1fdbc..357afb51eb 100644 --- a/test-suite/output/MExtraction.v +++ b/test-suite/output/MExtraction.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -56,10 +56,11 @@ Extract Constant Rinv => "fun x -> 1 / x". Recursive Extraction Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula Tauto.abst_form - ZMicromega.cnfZ ZMicromega.bound_problem_fr ZMicromega.Zeval_const QMicromega.cnfQ + ZMicromega.cnfZ ZMicromega.Zeval_const QMicromega.cnfQ List.map simpl_cone (*map_cone indexes*) denorm Qpower vm_add normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. + (* Local Variables: *) (* coding: utf-8 *) (* End: *) diff --git a/test-suite/output/print_ltac.out b/test-suite/output/print_ltac.out new file mode 100644 index 0000000000..952761acca --- /dev/null +++ b/test-suite/output/print_ltac.out @@ -0,0 +1,8 @@ +Ltac t1 := time "my tactic" idtac +Ltac t2 := let x := string:("my tactic") in + idtac + x +Ltac t3 := idtacstr "my tactic" +Ltac t4 x := match x with + | ?A => (A, A) + end diff --git a/test-suite/output/print_ltac.v b/test-suite/output/print_ltac.v new file mode 100644 index 0000000000..a992846791 --- /dev/null +++ b/test-suite/output/print_ltac.v @@ -0,0 +1,12 @@ +(* Testing of various things about Print Ltac *) +(* https://github.com/coq/coq/issues/10971 *) +Ltac t1 := time "my tactic" idtac. +Print Ltac t1. +Ltac t2 := let x := string:("my tactic") in idtac x. +Print Ltac t2. +Tactic Notation "idtacstr" string(str) := idtac str. +Ltac t3 := idtacstr "my tactic". +Print Ltac t3. +(* https://github.com/coq/coq/issues/9716 *) +Ltac t4 x := match x with ?A => constr:((A, A)) end. +Print Ltac t4. diff --git a/theories/MSets/MSetEqProperties.v b/theories/MSets/MSetEqProperties.v index 303acf7ae2..e3ff4979a9 100644 --- a/theories/MSets/MSetEqProperties.v +++ b/theories/MSets/MSetEqProperties.v @@ -18,6 +18,8 @@ [equal s s'=true] instead of [Equal s s'], etc. *) Require Import MSetProperties Zerob Sumbool Lia DecidableTypeEx. +Require FSetEqProperties. + Module WEqPropertiesOn (Import E:DecidableType)(M:WSetsOn E). Module Import MP := WPropertiesOn E M. @@ -857,7 +859,7 @@ intros. rewrite <- (fold_equal _ _ _ _ fc ft 0 _ _ H). rewrite <- (fold_equal _ _ _ _ gc gt 0 _ _ H). rewrite <- (fold_equal _ _ _ _ fgc fgt 0 _ _ H); auto. -intros. do 3 (rewrite fold_add; auto with fset). lia. +intros. do 3 (rewrite fold_add by auto with fset). lia. do 3 rewrite fold_empty;auto. Qed. diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v index 5b3d6ea30e..b1f0d9bc39 100644 --- a/theories/QArith/Qreals.v +++ b/theories/QArith/Qreals.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Export Rbase. +Require Import Rdefinitions Raxioms RIneq. Require Export QArith_base. (** Injection of rational numbers into real numbers. *) @@ -48,7 +48,7 @@ set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2); set (Y2 := IZR (Zpos y2)) in *. assert ((X1 * Y2)%R = (Y1 * X2)%R). unfold X1, X2, Y1, Y2; do 2 rewrite <- mult_IZR. - apply IZR_eq; auto. +f_equal; auto. clear H. field_simplify_eq; auto. rewrite H0; ring. diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v index cbf90c5adb..0cad621692 100644 --- a/theories/Reals/ArithProp.v +++ b/theories/Reals/ArithProp.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import Rbase. +Require Import Rdefinitions Raxioms RIneq. Require Import Rbasic_fun. Require Import Even. Require Import Div2. @@ -85,7 +85,7 @@ Proof. assert (H1 := le_INR _ _ H). do 2 rewrite mult_INR in H1. apply Rmult_le_reg_l with (INR 2). - replace (INR 2) with 2; [ prove_sup0 | reflexivity ]. + apply lt_0_INR. apply Nat.lt_0_2. assumption. Qed. diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 229e6018ca..b0d7b26a86 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -19,7 +19,7 @@ Require Export Raxioms. Require Import Rpow_def. Require Import Zpower. Require Export ZArithRing. -Require Import Lia. +Require Import Ztac. Require Export RealField. Local Open Scope Z_scope. @@ -1875,7 +1875,7 @@ Lemma eq_IZR : forall n m:Z, IZR n = IZR m -> n = m. Proof. intros z1 z2 H; generalize (Rminus_diag_eq (IZR z1) (IZR z2) H); rewrite (Z_R_minus z1 z2); intro; generalize (eq_IZR_R0 (z1 - z2) H0); - intro; lia. + apply Zminus_eq. Qed. (**********) @@ -1913,21 +1913,24 @@ Qed. Lemma IZR_ge : forall n m:Z, (n >= m)%Z -> IZR n >= IZR m. Proof. intros m n H; apply Rnot_lt_ge; red; intro. - generalize (lt_IZR m n H0); intro; lia. + generalize (lt_IZR m n H0); intro. + slia H H1. Qed. Lemma IZR_le : forall n m:Z, (n <= m)%Z -> IZR n <= IZR m. Proof. intros m n H; apply Rnot_gt_le; red; intro. - unfold Rgt in H0; generalize (lt_IZR n m H0); intro; lia. + unfold Rgt in H0; generalize (lt_IZR n m H0); intro. + slia H H1. Qed. Lemma IZR_lt : forall n m:Z, (n < m)%Z -> IZR n < IZR m. Proof. intros m n H; cut (m <= n)%Z. intro H0; elim (IZR_le m n H0); intro; auto. - generalize (eq_IZR m n H1); intro; exfalso; lia. - lia. + generalize (eq_IZR m n H1); intro; exfalso. + slia H H3. + normZ. slia H H0. Qed. Lemma IZR_neq : forall z1 z2:Z, z1 <> z2 -> IZR z1 <> IZR z2. @@ -1954,7 +1957,7 @@ Lemma one_IZR_r_R1 : forall r (n m:Z), r < IZR n <= r + 1 -> r < IZR m <= r + 1 -> n = m. Proof. intros r z x [H1 H2] [H3 H4]. - cut ((z - x)%Z = 0%Z). lia. + apply Zminus_eq. apply one_IZR_lt1. rewrite <- Z_R_minus; split. replace (-1) with (r - (r + 1)). diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v index 5f0747d869..d9820f9444 100644 --- a/theories/Reals/R_Ifp.v +++ b/theories/Reals/R_Ifp.v @@ -13,8 +13,8 @@ (* *) (**********************************************************) -Require Import Rbase. -Require Import Lia. +Require Import Rdefinitions Raxioms RIneq. +Require Import Ztac. Local Open Scope R_scope. (*********************************************************) @@ -60,7 +60,7 @@ Proof. apply lt_IZR in H1. rewrite <- minus_IZR in H2. apply le_IZR in H2. - lia. + normZ. slia H2 HZ. slia H1 HZ. Qed. (**********) @@ -229,8 +229,8 @@ Proof. rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H. rewrite <- (plus_IZR (Int_part r1 - Int_part r2) 1) in H; generalize (up_tech (r1 - r2) (Int_part r1 - Int_part r2) H0 H); - intros; clear H H0; unfold Int_part at 1; - lia. + intros; clear H H0; unfold Int_part at 1. + normZ. slia H HZ. slia H0 HZ. Qed. (**********) @@ -322,8 +322,8 @@ Proof. generalize (Rlt_le (IZR (Int_part r1 - Int_part r2 - 1)) (r1 - r2) H); intro; clear H; generalize (up_tech (r1 - r2) (Int_part r1 - Int_part r2 - 1) H1 H0); - intros; clear H0 H1; unfold Int_part at 1; - lia. + intros; clear H0 H1; unfold Int_part at 1. + normZ. slia H HZ. slia H0 HZ. Qed. (**********) @@ -437,7 +437,8 @@ Proof. rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H0; rewrite <- (plus_IZR (Int_part r1 + Int_part r2 + 1) 1) in H0; generalize (up_tech (r1 + r2) (Int_part r1 + Int_part r2 + 1) H H0); - intro; clear H H0; unfold Int_part at 1; lia. + intro; clear H H0; unfold Int_part at 1. + normZ. slia H HZ. slia H0 HZ. Qed. (**********) @@ -498,8 +499,8 @@ Proof. rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H1; rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H1; generalize (up_tech (r1 + r2) (Int_part r1 + Int_part r2) H0 H1); - intro; clear H0 H1; unfold Int_part at 1; - lia. + intro; clear H0 H1; unfold Int_part at 1. + normZ. slia H HZ. slia H0 HZ. Qed. (**********) diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v index 1a74582b71..e6c6e8bf48 100644 --- a/theories/Reals/R_sqr.v +++ b/theories/Reals/R_sqr.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import Rbase. +Require Import Rdefinitions Raxioms RIneq. Require Import Rbasic_fun. Local Open Scope R_scope. diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index efca826077..7e59639dd4 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -13,7 +13,7 @@ (* *) (*********************************************************) -Require Import Rbase. +Require Import Rdefinitions Raxioms RIneq. Require Import R_Ifp. Local Open Scope R_scope. diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index 7f9e019c5b..a63df38808 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -17,7 +17,7 @@ (********************************************************) Require Export ArithRing. -Require Import Rbase. +Require Import Rdefinitions Raxioms RIneq. Require Export Rpow_def. Require Export R_Ifp. Require Export Rbasic_fun. @@ -25,8 +25,8 @@ Require Export R_sqr. Require Export SplitAbsolu. Require Export SplitRmult. Require Export ArithProp. -Require Import Lia. Require Import Zpower. +Require Import Ztac. Local Open Scope nat_scope. Local Open Scope R_scope. @@ -122,7 +122,7 @@ Hint Resolve pow_lt: real. Lemma Rlt_pow_R1 : forall (x:R) (n:nat), 1 < x -> (0 < n)%nat -> 1 < x ^ n. Proof. intros x n; elim n; simpl; auto with real. - intros H' H'0; exfalso; lia. + intros H' H'0; exfalso. apply (Nat.lt_irrefl 0); assumption. intros n0; case n0. simpl; rewrite Rmult_1_r; auto. intros n1 H' H'0 H'1. @@ -262,14 +262,14 @@ Proof. elim (IZN (up (b * / (Rabs x - 1))) H2); intros; exists x0; apply (Rge_trans (INR x0) (IZR (up (b * / (Rabs x - 1)))) (b * / (Rabs x - 1))). - rewrite INR_IZR_INZ; apply IZR_ge; lia. + rewrite INR_IZR_INZ; apply IZR_ge. normZ. slia H3 H5. unfold Rge; left; assumption. exists 0%nat; apply (Rge_trans (INR 0) (IZR (up (b * / (Rabs x - 1)))) (b * / (Rabs x - 1))). - rewrite INR_IZR_INZ; apply IZR_ge; simpl; lia. + rewrite INR_IZR_INZ; apply IZR_ge; simpl. normZ. slia H2 H3. unfold Rge; left; assumption. - lia. + apply Z.le_ge_cases. Qed. Lemma pow_ne_zero : forall n:nat, n <> 0%nat -> 0 ^ n = 0. @@ -745,7 +745,8 @@ Proof. - now simpl; rewrite Rmult_1_l. - now rewrite <- !pow_powerRZ, Rpow_mult_distr. - destruct Hmxy as [H|H]. - + assert(m = 0) as -> by now lia. + + assert(m = 0) as -> by + (destruct n; [assumption| subst; simpl in H; lia_contr]). now rewrite <- Hm, Rmult_1_l. + assert(x0 <> 0)%R by now intros ->; apply H; rewrite Rmult_0_l. assert(y0 <> 0)%R by now intros ->; apply H; rewrite Rmult_0_r. @@ -808,7 +809,7 @@ Proof. ring. rewrite Rmult_plus_distr_r; rewrite Hrecn; cut ((n + 1)%nat = S n). intro H; rewrite H; simpl; ring. - lia. + apply Nat.add_1_r. Qed. Lemma sum_f_R0_triangle : diff --git a/theories/Reals/SplitRmult.v b/theories/Reals/SplitRmult.v index be2b5a73f3..cad1525580 100644 --- a/theories/Reals/SplitRmult.v +++ b/theories/Reals/SplitRmult.v @@ -11,7 +11,7 @@ (*i Lemma mult_non_zero :(r1,r2:R)``r1<>0`` /\ ``r2<>0`` -> ``r1*r2<>0``. i*) -Require Import Rbase. +Require Import Rdefinitions Raxioms RIneq. Ltac split_Rmult := match goal with diff --git a/vernac/classes.ml b/vernac/classes.ml index 0333b73ffe..c9b5144299 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -410,7 +410,7 @@ let do_instance_resolve_TC termtype sigma env = (* Beware of this step, it is required as to minimize universes. *) let sigma = Evd.minimize_universes sigma in (* Check that the type is free of evars now. *) - Pretyping.check_evars env (Evd.from_env env) sigma termtype; + Pretyping.check_evars env sigma termtype; termtype, sigma let do_instance_type_ctx_instance props k env' ctx' sigma ~program_mode subst = diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index a001420f74..8a403e5a03 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -255,7 +255,7 @@ let context ~poly l = let sigma, (_, ((_env, ctx), impls)) = interp_context_evars ~program_mode:false env sigma l in (* Note, we must use the normalized evar from now on! *) let sigma = Evd.minimize_universes sigma in - let ce t = Pretyping.check_evars env (Evd.from_env env) sigma t in + let ce t = Pretyping.check_evars env sigma t in let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) ctx in (* reorder, evar-normalize and add implicit status *) let ctx = List.rev_map (fun d -> diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 2aee9bd47f..b603c54026 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -255,7 +255,7 @@ let inductive_levels env evd arities inds = in let cstrs_levels, min_levels, sizes = CList.split3 - (List.map2 (fun (_,tys,_) (arity,(ctx,du)) -> + (List.map2 (fun (_,tys) (arity,(ctx,du)) -> let len = List.length tys in let minlev = Sorts.univ_of_sort du in let minlev = @@ -323,18 +323,18 @@ let check_named {CAst.loc;v=na} = match na with let msg = str "Parameters must be named." in user_err ?loc msg -let template_polymorphism_candidate env ~ctor_levels uctx params concl = +let template_polymorphism_candidate ~template_check ~ctor_levels uctx params concl = match uctx with | Entries.Monomorphic_entry uctx -> let concltemplate = Option.cata (fun s -> not (Sorts.is_small s)) false concl in if not concltemplate then false + else if not template_check then true else - let template_check = Environ.check_template env in let conclu = Option.cata Sorts.univ_of_sort Univ.type0m_univ concl in let params, conclunivs = IndTyping.template_polymorphic_univs ~template_check ~ctor_levels uctx params conclu in - not (template_check && Univ.LSet.is_empty conclunivs) + not (Univ.LSet.is_empty conclunivs) | Entries.Polymorphic_entry _ -> false let check_param = function @@ -350,33 +350,28 @@ let restrict_inductive_universes sigma ctx_params arities constructors = let uvars = Univ.LSet.empty in let uvars = Context.Rel.(fold_outside (Declaration.fold_constr merge_universes_of_constr) ctx_params ~init:uvars) in let uvars = List.fold_right merge_universes_of_constr arities uvars in - let uvars = List.fold_right (fun (_,ctypes,_) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in + let uvars = List.fold_right (fun (_,ctypes) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in Evd.restrict_universe_context sigma uvars -let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_params ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite = +let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite = (* Compute renewed arities *) let sigma = Evd.minimize_universes sigma in let nf = Evarutil.nf_evars_universes sigma in - let constructors = List.map (on_pi2 (List.map nf)) constructors in + let constructors = List.map (on_snd (List.map nf)) constructors in let arities = List.map EConstr.(to_constr sigma) arities in let sigma = List.fold_left make_anonymous_conclusion_flexible sigma arityconcl in let sigma, arities = inductive_levels env_ar_params sigma arities constructors in let sigma = Evd.minimize_universes sigma in let nf = Evarutil.nf_evars_universes sigma in let arities = List.map (on_snd nf) arities in - let constructors = List.map (on_pi2 (List.map nf)) constructors in + let constructors = List.map (on_snd (List.map nf)) constructors in let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in let arityconcl = List.map (Option.map (fun (_anon, s) -> EConstr.ESorts.kind sigma s)) arityconcl in let sigma = restrict_inductive_universes sigma ctx_params (List.map snd arities) constructors in let uctx = Evd.check_univ_decl ~poly sigma udecl in - List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr (snd c))) arities; - Context.Rel.iter (fun c -> check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr c)) ctx_params; - List.iter (fun (_,ctyps,_) -> - List.iter (fun c -> check_evars env_ar_params (Evd.from_env env_ar_params) sigma (EConstr.of_constr c)) ctyps) - constructors; (* Build the inductive entries *) - let entries = List.map4 (fun indname (templatearity, arity) concl (cnames,ctypes,cimpls) -> + let entries = List.map4 (fun indname (templatearity, arity) concl (cnames,ctypes) -> let template_candidate () = templatearity || let ctor_levels = @@ -390,7 +385,7 @@ let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_pa List.fold_left (fun levels c -> add_levels c levels) param_levels ctypes in - template_polymorphism_candidate env0 ~ctor_levels uctx ctx_params concl + template_polymorphism_candidate ~template_check:(Environ.check_template env_ar_params) ~ctor_levels uctx ctx_params concl in let template = match template with | Some template -> @@ -408,7 +403,6 @@ let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_pa }) indnames arities arityconcl constructors in - let variance = if poly && cumulative then Some (InferCumulativity.dummy_variance uctx) else None in (* Build the mutual inductive entry *) let mind_ent = { mind_entry_params = ctx_params; @@ -417,12 +411,10 @@ let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_pa mind_entry_inds = entries; mind_entry_private = if private_ind then Some false else None; mind_entry_universes = uctx; - mind_entry_variance = variance; + mind_entry_cumulative = poly && cumulative; } in - (if poly && cumulative then - InferCumulativity.infer_inductive env_ar mind_ent - else mind_ent), Evd.universe_binders sigma + mind_ent, Evd.universe_binders sigma let interp_params env udecl uparamsl paramsl = let sigma, udecl = interp_univ_decl_opt env udecl in @@ -492,9 +484,10 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not List.init (List.length indl) EConstr.(fun i -> mkApp (mkRel (i + 1 + nuparams), uargs)) @ List.init nuparams EConstr.(fun i -> mkRel (i + 1)) in let generalize_constructor c = EConstr.Unsafe.to_constr (EConstr.Vars.substnl uparam_subst nparams c) in + let cimpls = List.map pi3 constructors in let constructors = List.map (fun (cnames,ctypes,cimpls) -> - (cnames,List.map generalize_constructor ctypes,cimpls)) - constructors + (cnames,List.map generalize_constructor ctypes)) + constructors in let ctx_params = ctx_params @ ctx_uparams in let userimpls = useruimpls @ userimpls in @@ -505,11 +498,12 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not (* Try further to solve evars, and instantiate them *) let sigma = solve_remaining_evars all_and_fail_flags env_params sigma in let impls = - List.map2 (fun indimpls (_,_,cimpls) -> + List.map2 (fun indimpls cimpls -> indimpls, List.map (fun impls -> - userimpls @ impls) cimpls) indimpls constructors + userimpls @ impls) cimpls) + indimpls cimpls in - let mie, pl = interp_mutual_inductive_constr ~env0 ~template ~sigma ~env_params ~env_ar ~ctx_params ~udecl ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in + let mie, pl = interp_mutual_inductive_constr ~template ~sigma ~ctx_params ~udecl ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in (mie, pl, impls) diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index ef05b213d8..cc104b3762 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -49,24 +49,22 @@ val declare_mutual_inductive_with_eliminations -> Names.MutInd.t [@@ocaml.deprecated "Please use DeclareInd.declare_mutual_inductive_with_eliminations"] -val interp_mutual_inductive_constr : - env0:Environ.env -> - sigma:Evd.evar_map -> - template:bool option -> - udecl:UState.universe_decl -> - env_ar:Environ.env -> - env_params:Environ.env -> - ctx_params:(EConstr.t, EConstr.t) Context.Rel.Declaration.pt list -> - indnames:Names.Id.t list -> - arities:EConstr.t list -> - arityconcl:(bool * EConstr.ESorts.t) option list -> - constructors:(Names.Id.t list * Constr.constr list * 'a list list) list -> - env_ar_params:Environ.env -> - cumulative:bool -> - poly:bool -> - private_ind:bool -> - finite:Declarations.recursivity_kind -> - Entries.mutual_inductive_entry * UnivNames.universe_binders +val interp_mutual_inductive_constr + : sigma:Evd.evar_map + -> template:bool option + -> udecl:UState.universe_decl + -> ctx_params:(EConstr.t, EConstr.t) Context.Rel.Declaration.pt list + -> indnames:Names.Id.t list + -> arities:EConstr.t list + -> arityconcl:(bool * EConstr.ESorts.t) option list + -> constructors:(Names.Id.t list * Constr.constr list) list + -> env_ar_params:Environ.env + (** Environment with the inductives and parameters in the rel_context *) + -> cumulative:bool + -> poly:bool + -> private_ind:bool + -> finite:Declarations.recursivity_kind + -> Entries.mutual_inductive_entry * UnivNames.universe_binders (************************************************************************) (** Internal API, exported for Record *) @@ -78,17 +76,17 @@ val should_auto_template : Id.t -> bool -> bool inductive under consideration. *) val template_polymorphism_candidate - : Environ.env + : template_check:bool -> ctor_levels:Univ.LSet.t -> Entries.universes_entry -> Constr.rel_context -> Sorts.t option -> bool -(** [template_polymorphism_candidate env ~ctor_levels uctx params +(** [template_polymorphism_candidate ~template_check ~ctor_levels uctx params conclsort] is [true] iff an inductive with params [params], conclusion [conclsort] and universe levels appearing in the constructor arguments [ctor_levels] would be definable as template polymorphic. It should have at least one universe in its monomorphic universe context that can be made parametric in its - conclusion sort, if one is given. If the [Template Check] flag is + conclusion sort, if one is given. If the [template_check] flag is false we just check that the conclusion sort is not small. *) diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml index 54dda09e83..c816a4eb4f 100644 --- a/vernac/declaremods.ml +++ b/vernac/declaremods.ml @@ -550,7 +550,7 @@ let intern_arg (acc, cst) (idl,(typ,ann)) = let lib_dir = Lib.library_dp() in let env = Global.env() in let (mty, _, cst') = Modintern.interp_module_ast env Modintern.ModType typ in - let () = Global.push_context_set true cst' in + let () = Global.push_context_set ~strict:true cst' in let env = Global.env () in let sobjs = get_module_sobjs false env inl mty in let mp0 = get_module_path mty in @@ -674,7 +674,7 @@ module RawModOps = struct let start_module export id args res fs = let mp = Global.start_module id in let arg_entries_r, cst = intern_args args in - let () = Global.push_context_set true cst in + let () = Global.push_context_set ~strict:true cst in let env = Global.env () in let res_entry_o, subtyps, cst = match res with | Enforce (res,ann) -> @@ -689,7 +689,7 @@ let start_module export id args res fs = let typs, cst = build_subtypes env mp arg_entries_r resl in None, typs, cst in - let () = Global.push_context_set true cst in + let () = Global.push_context_set ~strict:true cst in openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps }; let prefix = Lib.start_module export id mp fs in Nametab.(push_dir (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModule prefix)); @@ -782,7 +782,7 @@ let declare_module id args res mexpr_o fs = | None -> None | _ -> inl_res in - let () = Global.push_context_set true cst in + let () = Global.push_context_set ~strict:true cst in let mp_env,resolver = Global.add_module id entry inl in (* Name consistency check : kernel vs. library *) @@ -804,10 +804,10 @@ module RawModTypeOps = struct let start_modtype id args mtys fs = let mp = Global.start_modtype id in let arg_entries_r, cst = intern_args args in - let () = Global.push_context_set true cst in + let () = Global.push_context_set ~strict:true cst in let env = Global.env () in let sub_mty_l, cst = build_subtypes env mp arg_entries_r mtys in - let () = Global.push_context_set true cst in + let () = Global.push_context_set ~strict:true cst in openmodtype_info := sub_mty_l; let prefix = Lib.start_modtype id mp fs in Nametab.(push_dir (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModtype prefix)); @@ -835,19 +835,19 @@ let declare_modtype id args mtys (mty,ann) fs = then we adds the module parameters to the global env. *) let mp = Global.start_modtype id in let arg_entries_r, cst = intern_args args in - let () = Global.push_context_set true cst in + let () = Global.push_context_set ~strict:true cst in let params = mk_params_entry arg_entries_r in let env = Global.env () in let mte, _, cst = Modintern.interp_module_ast env Modintern.ModType mty in - let () = Global.push_context_set true cst in + let () = Global.push_context_set ~strict:true cst in let env = Global.env () in (* We check immediately that mte is well-formed *) let _, _, _, cst = Mod_typing.translate_mse env None inl mte in - let () = Global.push_context_set true cst in + let () = Global.push_context_set ~strict:true cst in let env = Global.env () in let entry = params, mte in let sub_mty_l, cst = build_subtypes env mp arg_entries_r mtys in - let () = Global.push_context_set true cst in + let () = Global.push_context_set ~strict:true cst in let env = Global.env () in let sobjs = get_functor_sobjs false env inl entry in let subst = map_mp (get_module_path (snd entry)) mp empty_delta_resolver in @@ -903,7 +903,7 @@ let type_of_incl env is_mod = function let declare_one_include (me_ast,annot) = let env = Global.env() in let me, kind, cst = Modintern.interp_module_ast env Modintern.ModAny me_ast in - let () = Global.push_context_set true cst in + let () = Global.push_context_set ~strict:true cst in let env = Global.env () in let is_mod = (kind == Modintern.Module) in let cur_mp = Lib.current_mp () in diff --git a/vernac/record.ml b/vernac/record.ml index d85b71df44..ea10e06d02 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -202,7 +202,7 @@ let typecheck_params_and_fields finite def poly pl ps records = in let univs = Evd.check_univ_decl ~poly sigma decl in let ubinders = Evd.universe_binders sigma in - let ce t = Pretyping.check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr t) in + let ce t = Pretyping.check_evars env0 sigma (EConstr.of_constr t) in let () = List.iter (iter_constr ce) (List.rev newps) in ubinders, univs, template, newps, imps, ans @@ -411,7 +411,6 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa | Polymorphic_entry (nas, ctx) -> true, Polymorphic_entry (nas, ctx) in - let variance = if poly && cumulative then Some (InferCumulativity.dummy_variance ctx) else None in let binder_name = match name with | None -> @@ -447,7 +446,8 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa univs) param_levels fields in - ComInductive.template_polymorphism_candidate (Global.env ()) ~ctor_levels univs params + let template_check = Environ.check_template (Global.env ()) in + ComInductive.template_polymorphism_candidate ~template_check ~ctor_levels univs params (Some (Sorts.sort_of_univ min_univ)) in match template with @@ -477,10 +477,9 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa mind_entry_inds = blocks; mind_entry_private = None; mind_entry_universes = univs; - mind_entry_variance = variance; + mind_entry_cumulative = poly && cumulative; } in - let mie = InferCumulativity.infer_inductive (Global.env ()) mie in let impls = List.map (fun _ -> paramimpls, []) record_data in let kn = DeclareInd.declare_mutual_inductive_with_eliminations mie ubinders impls ~primitive_expected:!primitive_flag diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e4965614d8..439ec61d38 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1621,7 +1621,7 @@ let vernac_global_check c = let c,uctx = interp_constr env sigma c in let senv = Global.safe_env() in let uctx = UState.context_set uctx in - let senv = Safe_typing.push_context_set false uctx senv in + let senv = Safe_typing.push_context_set ~strict:false uctx senv in let c = EConstr.to_constr sigma c in let j = Safe_typing.typing senv c in let env = Safe_typing.env_of_safe_env senv in |