diff options
68 files changed, 1759 insertions, 1543 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 73b979c6a3..b39e74ffee 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -632,13 +632,11 @@ library:ci-fiat-crypto: stage: stage-4 needs: - build:edge+flambda - - library:ci-bedrock2 - library:ci-coqprime - plugin:ci-bignums - plugin:ci-rewriter dependencies: - build:edge+flambda - - library:ci-bedrock2 - library:ci-coqprime - plugin:ci-rewriter diff --git a/Makefile.build b/Makefile.build index a8ae040f8e..3c32e5bcc2 100644 --- a/Makefile.build +++ b/Makefile.build @@ -417,7 +417,7 @@ $(COQTOPBYTE): $(COQTOP_BYTE) $(LINKCMO) $(LIBCOQRUN) ########################################################################### .PHONY: tools -tools: $(TOOLS) $(OCAMLLIBDEP) $(COQDEPBOOT) +tools: $(TOOLS) $(OCAMLLIBDEP) $(COQDEPBOOT) $(DOC_GRAM) # coqdep_boot : a basic version of coqdep, with almost no dependencies. # We state these dependencies here explicitly, since some .ml.d files @@ -865,9 +865,11 @@ endif # Dependencies of .v files +PLUGININCLUDES=$(addprefix -I plugins/, $(PLUGINDIRS)) + $(VDFILE).d: $(D_DEPEND_BEFORE_SRC) $(VFILES) $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(SHOW)'COQDEP VFILES' - $(HIDE)$(COQDEPBOOT) -vos -boot $(DYNDEP) -Q user-contrib "" $(USERCONTRIBINCLUDES) $(VFILES) $(TOTARGET) + $(HIDE)$(COQDEPBOOT) -vos -boot $(DYNDEP) -R theories Coq -R plugins Coq -Q user-contrib "" $(PLUGININCLUDES) $(USERCONTRIBINCLUDES) $(VFILES) $(TOTARGET) ########################################################################### diff --git a/Makefile.ci b/Makefile.ci index 4fc0e69748..10c3b027c3 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -65,7 +65,7 @@ ci-math-classes: ci-bignums ci-corn: ci-math-classes -ci-fiat-crypto: ci-bedrock2 ci-coqprime ci-rewriter +ci-fiat-crypto: ci-coqprime ci-rewriter ci-simple-io: ci-ext-lib ci-quickchick: ci-ext-lib ci-simple-io diff --git a/Makefile.common b/Makefile.common index e392e51153..32bf19e99c 100644 --- a/Makefile.common +++ b/Makefile.common @@ -43,8 +43,9 @@ COQMAKE_BOTH_TIME_FILES:=tools/make-both-time-files.py COQMAKE_BOTH_SINGLE_TIMING_FILES:=tools/make-both-single-timing-files.py VOTOUR:=bin/votour +# these get installed! TOOLS:=$(COQDEP) $(COQMAKEFILE) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\ - $(COQWORKMGR) $(COQPP) $(DOC_GRAM) $(VOTOUR) + $(COQWORKMGR) $(COQPP) $(VOTOUR) TOOLS_HELPERS:=tools/CoqMakefile.in $(COQMAKE_ONE_TIME_FILE) $(COQTIME_FILE_MAKER)\ $(COQMAKE_BOTH_TIME_FILES) $(COQMAKE_BOTH_SINGLE_TIMING_FILES) @@ -55,7 +56,8 @@ OCAMLLIBDEPBYTE:=bin/ocamllibdep.byte$(EXE) FAKEIDE:=bin/fake_ide$(EXE) FAKEIDEBYTE:=bin/fake_ide.byte$(EXE) -PRIVATEBINARIES:=$(FAKEIDE) $(OCAMLLIBDEP) $(COQDEPBOOT) +# These don't get signed on OSX, and don't need to be separately listed for cleaning +PRIVATEBINARIES:=$(FAKEIDE) $(OCAMLLIBDEP) $(COQDEPBOOT) $(DOC_GRAM) CSDPCERT:=plugins/micromega/csdpcert$(EXE) CSDPCERTBYTE:=plugins/micromega/csdpcert.byte$(EXE) diff --git a/Makefile.make b/Makefile.make index e19053462d..e63a578e37 100644 --- a/Makefile.make +++ b/Makefile.make @@ -56,6 +56,7 @@ FIND_SKIP_DIRS:=-not -name . '(' \ -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 \ @@ -251,7 +252,7 @@ docclean: rm -rf doc/sphinx/_build archclean: clean-ide optclean voclean plugin-tutorialclean - rm -rf _build + rm -rf _build _build_boot rm -f $(ALLSTDLIB).* optclean: diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index a2cf44389e..051f51bbb3 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -20,7 +20,7 @@ exception InductiveMismatch of MutInd.t * string let check mind field b = if not b then raise (InductiveMismatch (mind,field)) -let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = +let to_entry mind (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = let open Entries in let nparams = List.length mb.mind_params_ctxt in (* include letins *) let mind_entry_record = match mb.mind_record with @@ -28,7 +28,27 @@ let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = | PrimRecord data -> Some (Some (Array.map (fun (x,_,_,_) -> x) data)) in let mind_entry_universes = match mb.mind_universes with - | Monomorphic univs -> Monomorphic_entry univs + | Monomorphic _ -> + (* We only need to rebuild the set of constraints for template polymorphic + inductive types. The set of monomorphic constraints is already part of + the graph at that point, but we need to emulate a broken bound variable + mechanism for template inductive types. *) + let fold accu ind = match ind.mind_arity with + | RegularArity _ -> accu + | TemplateArity ar -> + match accu with + | None -> Some ar.template_context + | Some ctx -> + (* Ensure that all template contexts agree. This is enforced by the + kernel. *) + let () = check mind "mind_arity" (ContextSet.equal ctx ar.template_context) in + Some ctx + in + let univs = match Array.fold_left fold None mb.mind_packets with + | None -> ContextSet.empty + | Some ctx -> ctx + in + Monomorphic_entry univs | Polymorphic auctx -> Polymorphic_entry (AUContext.names auctx, AUContext.repr auctx) in let mind_entry_inds = Array.map_to_list (fun ind -> @@ -69,8 +89,9 @@ let check_arity env ar1 ar2 = match ar1, ar2 with | RegularArity ar, RegularArity {mind_user_arity;mind_sort} -> Constr.equal ar.mind_user_arity mind_user_arity && Sorts.equal ar.mind_sort mind_sort - | TemplateArity ar, TemplateArity {template_param_levels;template_level} -> + | TemplateArity ar, TemplateArity {template_param_levels;template_level;template_context} -> List.equal (Option.equal Univ.Level.equal) ar.template_param_levels template_param_levels && + ContextSet.equal template_context ar.template_context && UGraph.check_leq (universes env) template_level ar.template_level (* template_level is inferred by indtypes, so functor application can produce a smaller one *) | (RegularArity _ | TemplateArity _), _ -> assert false @@ -136,7 +157,7 @@ let check_same_record r1 r2 = match r1, r2 with | (NotRecord | FakeRecord | PrimRecord _), _ -> false let check_inductive env mind mb = - let entry = to_entry mb in + let entry = to_entry mind mb in let { mind_packets; mind_record; mind_finite; mind_ntypes; mind_hyps; mind_nparams; mind_nparams_rec; mind_params_ctxt; mind_universes; mind_variance; mind_sec_variance; diff --git a/checker/values.ml b/checker/values.ml index fff166f27b..c8bbc092b4 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -228,7 +228,7 @@ let v_oracle = |] let v_pol_arity = - v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|] + v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ;v_context_set|] let v_primitive = v_enum "primitive" 44 (* Number of "Primitive" in Int63.v and PrimFloat.v *) @@ -28,7 +28,7 @@ depends: [ ] build: [ - [ "./configure" "-prefix" prefix "-native-compiler" "no" ] + [ "./configure" "-prefix" prefix ] [ "make" "-f" "Makefile.dune" "voboot" ] [ "dune" "build" "-p" name "-j" jobs ] ] diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 7342bc72e7..608cc127a0 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -97,11 +97,8 @@ ######################################################################## # Coquelicot ######################################################################## -# Modified until https://gitlab.inria.fr/coquelicot/coquelicot/merge_requests/2 is merged -: "${coquelicot_CI_REF:=fix-rlist-import}" -: "${coquelicot_CI_GITURL:=https://gitlab.inria.fr/pedrot/coquelicot}" -# : "${coquelicot_CI_REF:=master}" -# : "${coquelicot_CI_GITURL:=https://gitlab.inria.fr/coquelicot/coquelicot}" +: "${coquelicot_CI_REF:=master}" +: "${coquelicot_CI_GITURL:=https://gitlab.inria.fr/coquelicot/coquelicot}" : "${coquelicot_CI_ARCHIVEURL:=${coquelicot_CI_GITURL}/-/archive}" ######################################################################## diff --git a/dev/ci/ci-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh index 2af4b58201..9ce5da9f50 100755 --- a/dev/ci/ci-fiat-crypto-legacy.sh +++ b/dev/ci/ci-fiat-crypto-legacy.sh @@ -6,8 +6,8 @@ ci_dir="$(dirname "$0")" FORCE_GIT=1 git_download fiat_crypto_legacy -fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite old-pipeline-lite lite-display" -fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem old-pipeline-nobigmem nonautogenerated-specific nonautogenerated-specific-display" +fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite-hardcoded old-pipeline-lite-hardcoded lite-display-hardcoded" +fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem-hardcoded old-pipeline-nobigmem-hardcoded nonautogenerated-specific nonautogenerated-specific-display" ( cd "${CI_BUILD_DIR}/fiat_crypto_legacy" && git submodule update --init --recursive && \ ./etc/ci/remove_autogenerated.sh && \ diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index 000c418137..811fefda35 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -9,11 +9,15 @@ git_download fiat_crypto # We need a larger stack size to not overflow ocamlopt+flambda when # building the executables. # c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241 +fiat_crypto_CI_STACKSIZE=32768 -fiat_crypto_CI_MAKE_ARGS="EXTERNAL_DEPENDENCIES=1" +# fiat-crypto is not guaranteed to build with the latest version of +# bedrock2, so we use the pinned version of bedrock2, but the external +# version of other developments +fiat_crypto_CI_MAKE_ARGS="EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1" fiat_crypto_CI_TARGETS1="${fiat_crypto_CI_MAKE_ARGS} standalone-ocaml c-files rust-files printlite lite" fiat_crypto_CI_TARGETS2="${fiat_crypto_CI_MAKE_ARGS} all" ( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \ - ulimit -s 32768 && \ + ulimit -s ${fiat_crypto_CI_STACKSIZE} && \ make ${fiat_crypto_CI_TARGETS1} && make -j 1 ${fiat_crypto_CI_TARGETS2} ) diff --git a/doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst b/doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst new file mode 100644 index 0000000000..2a341261e5 --- /dev/null +++ b/doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst @@ -0,0 +1,9 @@ +- **Added:** + :cmd:`Show Lia Profile` prints some statistics about :tacn:`lia` calls. + (`#11474 <https://github.com/coq/coq/pull/11474>`_, by Frédéric Besson). + +- **Fixed:** + Efficiency regression of ``lia`` + (`#11474 <https://github.com/coq/coq/pull/11474>`_, + fixes `#11436 <https://github.com/coq/coq/issues/11436>`_, + by Frédéric Besson). diff --git a/doc/changelog/08-tools/11523-coqdep+refactor2.rst b/doc/changelog/08-tools/11523-coqdep+refactor2.rst new file mode 100644 index 0000000000..90c23d8b76 --- /dev/null +++ b/doc/changelog/08-tools/11523-coqdep+refactor2.rst @@ -0,0 +1,7 @@ +- **Changed:** + Internal options and behavior of ``coqdep`` have changed, in particular + options ``-w``, ``-D``, ``-mldep``, and ``-dumpbox`` have been removed, + and ``-boot`` will not load any path by default, ``-R/-Q`` should be + used instead + (`#11523 <https://github.com/coq/coq/pull/11523>`_, + by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/09-coqide/11414-remove-ide-tactic-menu.rst b/doc/changelog/09-coqide/11414-remove-ide-tactic-menu.rst new file mode 100644 index 0000000000..6294cdb24a --- /dev/null +++ b/doc/changelog/09-coqide/11414-remove-ide-tactic-menu.rst @@ -0,0 +1,4 @@ +- **Removed:** + Removed the "Tactic" menu from CoqIDE which had been unmaintained for a number of years + (`#11414 <https://github.com/coq/coq/pull/11414>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/10-standard-library/11404-removeRList.rst b/doc/changelog/10-standard-library/11404-removeRList.rst new file mode 100644 index 0000000000..88e22d128c --- /dev/null +++ b/doc/changelog/10-standard-library/11404-removeRList.rst @@ -0,0 +1,15 @@ +- **Removed:** + Type `RList` has been removed. All uses have been replaced by `list R`. + Functions from `RList` named `In`, `Rlength`, `cons_Rlist`, `app_Rlist` + have also been removed as they are essentially the same as `In`, `length`, + `app`, and `map` from `List`, modulo the following changes: + + - `RList.In x (RList.cons a l)` used to be convertible to + `(x = a) \\/ RList.In x l`, + but `List.In x (a :: l)` is convertible to + `(a = x) \\/ List.In l`. + The equality is reversed. + - `app_Rlist` and `List.map` take arguments in different order. + + (`#11404 <https://github.com/coq/coq/pull/11404>`_, + by Yves Bertot). diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index cc19c8b6a9..b0197c500c 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -35,6 +35,12 @@ tactics for solving arithmetic goals over :math:`\mathbb{Q}`, use the Simplex method for solving linear goals. If it is not set, the decision procedures are using Fourier elimination. +.. cmd:: Show Lia Profile + + This command prints some statistics about the amount of pivoting + operations needed by :tacn:`lia` and may be useful to detect + inefficiencies (only meaningful if flag :flag:`Simplex` is set). + .. flag:: Lia Cache This flag (set by default) instructs :tacn:`lia` to cache its results in the file `.lia.cache` diff --git a/doc/tools/coqrst/checkdeps.py b/doc/tools/coqrst/checkdeps.py index 91f0a7cb1b..feafcba026 100644 --- a/doc/tools/coqrst/checkdeps.py +++ b/doc/tools/coqrst/checkdeps.py @@ -10,13 +10,20 @@ from __future__ import print_function import sys +missing_deps = [] + def eprint(*args, **kwargs): print(*args, file=sys.stderr, **kwargs) def missing_dep(dep): - eprint('Cannot find %s (needed to build documentation)' % dep) - eprint('You can run `pip3 install %s` to install it.' % dep) - sys.exit(1) + missing_deps.append(dep) + +def report_missing_deps(): + if len(missing_deps) > 0: + deps = " ".join(missing_deps) + eprint('Cannot find package(s) `%s` (needed to build documentation)' % deps) + eprint('You can run `pip3 install %s` to install it/them.' % deps) + sys.exit(1) try: import sphinx_rtd_theme @@ -37,3 +44,10 @@ try: import bs4 except: missing_dep('beautifulsoup4') + +try: + import sphinxcontrib.bibtex +except: + missing_dep('sphinxcontrib-bibtex') + +report_missing_deps() @@ -25,7 +25,11 @@ (source_tree theories) (source_tree plugins) (source_tree user-contrib)) - (action (with-stdout-to .vfiles.d (bash "%{bin:coqdep} -dyndep both -noglob -boot `find theories plugins user-contrib -type f -name *.v`")))) + (action + (with-stdout-to .vfiles.d + (bash "%{bin:coqdep} -dyndep both -noglob -boot -R theories Coq -R plugins Coq -Q user-contrib/Ltac2 Ltac2 -I user-contrib/Ltac2 \ + `find plugins/ -maxdepth 1 -mindepth 1 -type d -printf '-I %p '` \ + `find theories plugins user-contrib -type f -name *.v`")))) (alias (name vodeps) diff --git a/engine/proofview.ml b/engine/proofview.ml index 16be96454e..b0ea75ac60 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -302,7 +302,8 @@ let tclONCE = Proof.once exception MoreThanOneSuccess let _ = CErrors.register_handler begin function - | MoreThanOneSuccess -> CErrors.user_err Pp.(str "This tactic has more than one success.") + | MoreThanOneSuccess -> + Pp.str "This tactic has more than one success." | _ -> raise CErrors.Unhandled end @@ -347,8 +348,7 @@ exception NoSuchGoals of int let _ = CErrors.register_handler begin function | NoSuchGoals n -> - CErrors.user_err - (str "No such " ++ str (String.plural n "goal") ++ str ".") + str "No such " ++ str (String.plural n "goal") ++ str "." | _ -> raise CErrors.Unhandled end @@ -420,12 +420,9 @@ let tclFOCUSID ?(nosuchgoal=tclZERO (NoSuchGoals 1)) id t = exception SizeMismatch of int*int let _ = CErrors.register_handler begin function | SizeMismatch (i,j) -> - let open Pp in - let errmsg = - str"Incorrect number of goals" ++ spc() ++ - str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str")." - in - CErrors.user_err errmsg + let open Pp in + str"Incorrect number of goals" ++ spc() ++ + str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str")." | _ -> raise CErrors.Unhandled end @@ -910,7 +907,8 @@ let tclPROGRESS t = tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS", Pp.str "Failed to progress.")) let _ = CErrors.register_handler begin function - | Logic_monad.Tac_Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") + | Logic_monad.Tac_Timeout -> + Pp.str "[Proofview.tclTIMEOUT] Tactic timeout!" | _ -> raise CErrors.Unhandled end diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index bfd99e7ce3..5b9ea17ba7 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -228,198 +228,3 @@ let state_preserving = [ "Test Printing Wildcard"; ] - - -let tactics = - [ - [ - "abstract"; - "absurd"; - "apply"; - "apply __ with"; - "assert"; - "assert (__:__)"; - "assert (__:=__)"; - "assumption"; - "auto"; - "auto with"; - "autorewrite"; - ]; - - [ - "case"; - "case __ with"; - "casetype"; - "cbv"; - "cbv in"; - "change"; - "change __ in"; - "clear"; - "clearbody"; - "cofix"; - "compare"; - "compute"; - "compute in"; - "congruence"; - "constructor"; - "constructor __ with"; - "contradiction"; - "cut"; - "cutrewrite"; - ]; - - [ - "decide equality"; - "decompose"; - "decompose record"; - "decompose sum"; - "dependent inversion"; - "dependent inversion __ with"; - "dependent inversion__clear"; - "dependent inversion__clear __ with"; - "dependent rewrite ->"; - "dependent rewrite <-"; - "destruct"; - "discriminate"; - "do"; - "double induction"; - ]; - - [ - "eapply"; - "eauto"; - "eauto with"; - "eexact"; - "elim"; - "elim __ using"; - "elim __ with"; - "elimtype"; - "exact"; - "exists"; - ]; - - [ - "fail"; - "field"; - "first"; - "firstorder"; - "firstorder using"; - "firstorder with"; - "fix"; - "fix __ with"; - "fold"; - "fold __ in"; - "functional induction"; - ]; - - [ - "generalize"; - "generalize dependent"; - ]; - - [ - "hnf"; - ]; - - [ - "idtac"; - "induction"; - "info"; - "injection"; - "instantiate (__:=__)"; - "intro"; - "intro after"; - "intro __ after"; - "intros"; - "intros until"; - "intuition"; - "inversion"; - "inversion __ in"; - "inversion __ using"; - "inversion __ using __ in"; - "inversion__clear"; - "inversion__clear __ in"; - ]; - - [ - "jp <n>"; - "jp"; - ]; - - [ - "lapply"; - "lazy"; - "lazy in"; - "left"; - ]; - - [ - "move __ after"; - ]; - - [ - "omega"; - ]; - - [ - "pattern"; - "pose"; - "pose __:=__)"; - "progress"; - ]; - - [ - "quote"; - ]; - - [ - "red"; - "red in"; - "refine"; - "reflexivity"; - "rename __ into"; - "repeat"; - "replace __ with"; - "rewrite"; - "rewrite __ in"; - "rewrite <-"; - "rewrite <- __ in"; - "right"; - "ring"; - ]; - - [ - "set"; - "set (__:=__)"; - "setoid__replace"; - "setoid__rewrite"; - "simpl"; - "simpl __ in"; - "simple destruct"; - "simple induction"; - "simple inversion"; - "simplify__eq"; - "solve"; - "split"; -(* "split__Rabs"; - "split__Rmult"; -*) - "subst"; - "symmetry"; - "symmetry in"; - ]; - - [ - "tauto"; - "transitivity"; - "trivial"; - "try"; - ]; - - [ - "unfold"; - "unfold __ in"; - ]; -] - - diff --git a/ide/coq_commands.mli b/ide/coq_commands.mli index 5f8ce30901..c8c11f77af 100644 --- a/ide/coq_commands.mli +++ b/ide/coq_commands.mli @@ -8,6 +8,5 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -val tactics : string list list val commands : string list list val state_preserving : string list diff --git a/ide/coqide.ml b/ide/coqide.ml index e0347d3c5f..ccf6d40b2b 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -977,7 +977,6 @@ let build_ui () = let view_menu = GAction.action_group ~name:"View" () in let export_menu = GAction.action_group ~name:"Export" () in let navigation_menu = GAction.action_group ~name:"Navigation" () in - let tactics_menu = GAction.action_group ~name:"Tactics" () in let templates_menu = GAction.action_group ~name:"Templates" () in let tools_menu = GAction.action_group ~name:"Tools" () in let queries_menu = GAction.action_group ~name:"Queries" () in @@ -985,7 +984,7 @@ let build_ui () = let windows_menu = GAction.action_group ~name:"Windows" () in let help_menu = GAction.action_group ~name:"Help" () in let all_menus = [ - file_menu; edit_menu; view_menu; export_menu; navigation_menu; tactics_menu; + file_menu; edit_menu; view_menu; export_menu; navigation_menu; templates_menu; tools_menu; queries_menu; compile_menu; windows_menu; help_menu; ] in @@ -1119,11 +1118,6 @@ let build_ui () = ("Force", "_Force", `EXECUTE, Nav.join_document, "Fully check the document", "f"); ] end; - menu tactics_menu [ - item "Tactics" ~label:"_Tactics"; - ]; - alpha_items tactics_menu "Tactic" Coq_commands.tactics; - menu templates_menu [ item "Templates" ~label:"Te_mplates"; template_item ("Lemma new_lemma : .\nProof.\n\nQed.\n", 6,9, "J"); @@ -1207,7 +1201,6 @@ let build_ui () = Coqide_ui.ui_m#insert_action_group edit_menu 0; Coqide_ui.ui_m#insert_action_group view_menu 0; Coqide_ui.ui_m#insert_action_group navigation_menu 0; - Coqide_ui.ui_m#insert_action_group tactics_menu 0; Coqide_ui.ui_m#insert_action_group templates_menu 0; Coqide_ui.ui_m#insert_action_group tools_menu 0; Coqide_ui.ui_m#insert_action_group queries_menu 0; diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index 59dd9c0e4c..f22821c6ea 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -99,9 +99,6 @@ let init () = \n <menuitem action='Previous' />\ \n <menuitem action='Next' />\ \n </menu>\ -\n <menu action='Tactics'>\ -\n %s\ -\n </menu>\ \n <menu action='Templates'>\ \n <menuitem action='Lemma' />\ \n <menuitem action='Theorem' />\ @@ -164,7 +161,6 @@ let init () = \n</toolbar>\ \n</ui>" (if Coq_config.gtk_platform <> `QUARTZ then "<menuitem action='Quit' />" else "") - (Buffer.contents (list_items "Tactic" Coq_commands.tactics)) (Buffer.contents (list_items "Template" Coq_commands.commands)) (Buffer.contents (list_queries "User-Query" Preferences.user_queries#get)) in diff --git a/ide/preferences.ml b/ide/preferences.ml index d3cf08e90e..af1759b0bb 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -331,10 +331,6 @@ let modifier_for_navigation = let modifier_for_templates = new preference ~name:["modifier_for_templates"] ~init:"<Control><Shift>" ~repr:Repr.(string) -let modifier_for_tactics = - new preference ~name:["modifier_for_tactics"] - ~init:(select_arch "<Control><Alt>" "<Control><Primary>") ~repr:Repr.(string) - let modifier_for_display = new preference ~name:["modifier_for_display"] ~init:(select_arch "<Alt><Shift>" "<Primary><Shift>")~repr:Repr.(string) @@ -347,7 +343,6 @@ let attach_modifiers_callback () = (* To be done after the preferences are loaded *) let _ = attach_modifiers modifier_for_navigation "<Actions>/Navigation/" in let _ = attach_modifiers modifier_for_templates "<Actions>/Templates/" in - let _ = attach_modifiers modifier_for_tactics "<Actions>/Tactics/" in let _ = attach_modifiers modifier_for_display "<Actions>/View/" in let _ = attach_modifiers modifier_for_queries "<Actions>/Queries/" in () @@ -951,9 +946,6 @@ let configure ?(apply=(fun () -> ())) parent = (string_of_project_behavior read_project#get) in let project_file_name = pstring "Default name for project file" project_file_name in - let modifier_for_tactics = - pmodifiers "Global change of modifiers for Tactics Menu" modifier_for_tactics - in let modifier_for_templates = pmodifiers "Global change of modifiers for Templates Menu" modifier_for_templates in @@ -1056,7 +1048,7 @@ let configure ?(apply=(fun () -> ())) parent = [cmd_coqtop;cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc; cmd_print;cmd_editor;cmd_browse]); Section("Shortcuts", Some `PREFERENCES, - [modifiers_valid; modifier_for_tactics; + [modifiers_valid; modifier_for_templates; modifier_for_display; modifier_for_navigation; modifier_for_queries (*; user_queries *)]); Section("Misc", Some `ADD, diff --git a/ide/preferences.mli b/ide/preferences.mli index 7b43079b4f..754f15c575 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -71,7 +71,6 @@ val automatic_tactics : string list preference val cmd_print : string preference val modifier_for_navigation : string preference val modifier_for_templates : string preference -val modifier_for_tactics : string preference val modifier_for_display : string preference val modifier_for_queries : string preference val modifiers_valid : string preference diff --git a/interp/constrextern.ml b/interp/constrextern.ml index cc0c1e4602..c55e17e7a3 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -281,6 +281,17 @@ let get_extern_reference () = !my_extern_reference let extern_reference ?loc vars l = !my_extern_reference vars l (**********************************************************************) +(* utilities *) + +let rec fill_arg_scopes args subscopes (entry,(_,scopes) as all) = + match args, subscopes with + | [], _ -> [] + | a :: args, scopt :: subscopes -> + (a, (entry, (scopt, scopes))) :: fill_arg_scopes args subscopes all + | a :: args, [] -> + (a, (entry, (None, scopes))) :: fill_arg_scopes args [] all + +(**********************************************************************) (* mapping patterns to cases_pattern_expr *) let add_patt_for_params ind l = @@ -550,14 +561,14 @@ let is_gvar id c = match DAst.get c with | GVar id' -> Id.equal id id' | _ -> false -let is_projection nargs = function - | Some r when not !Flags.in_debugger && not !Flags.raw_print && !print_projections -> - (try - let n = Recordops.find_projection_nparams r + 1 in - if n <= nargs then Some n - else None - with Not_found -> None) - | _ -> None +let is_projection nargs r = + if not !Flags.in_debugger && not !Flags.raw_print && !print_projections then + try + let n = Recordops.find_projection_nparams r + 1 in + if n <= nargs then Some n + else None + with Not_found -> None + else None let is_hole = function CHole _ | CEvar _ -> true | _ -> false @@ -569,11 +580,12 @@ let is_needed_for_correct_partial_application tail imp = exception Expl -(* Implicit args indexes are in ascending order *) -(* inctx is useful only if there is a last argument to be deduced from ctxt *) -let explicitize inctx impl (cf,f) args = - let impl = if !Constrintern.parsing_explicit then [] else impl in - let n = List.length args in +(* Take a list of arguments starting at position [q] and their implicit status *) +(* Decide for each implicit argument if it skipped or made explicit *) +(* If the removal of implicit arguments is not possible, raise [Expl] *) +(* [inctx] tells if the term is in a context which will enforce the external type *) +(* [n] is the total number of arguments block to which the [args] belong *) +let adjust_implicit_arguments inctx n q args impl = let rec exprec q = function | a::args, imp::impl when is_status_implicit imp -> let tail = exprec (q+1) (args,impl) in @@ -595,10 +607,11 @@ let explicitize inctx impl (cf,f) args = (* The non-explicit application cannot be parsed back with the same type *) raise Expl | [], _ -> [] - in + in exprec q (args,impl) + +let extern_projection (cf,f) args impl = let ip = is_projection (List.length args) cf in - let expl () = - match ip with + match ip with | Some i -> (* Careful: It is possible to have declared implicits ending before the principal argument *) @@ -607,33 +620,61 @@ let explicitize inctx impl (cf,f) args = with Failure _ -> false in if is_impl - then raise Expl + then None else let (args1,args2) = List.chop i args in let (impl1,impl2) = try List.chop i impl with Failure _ -> impl, [] in - let args1 = exprec 1 (args1,impl1) in - let args2 = exprec (i+1) (args2,impl2) in - let ip = Some (List.length args1) in - CApp ((ip,f),args1@args2) - | None -> - let args = exprec 1 (args,impl) in - if List.is_empty args then f.CAst.v else - match f.CAst.v with - | CApp (g,args') -> - (* may happen with notations for a prefix of an n-ary - application *) - CApp (g,args'@args) - | _ -> CApp ((None, f), args) in - try expl () - with Expl -> - let f',us = match f with { CAst.v = CRef (f,us) } -> f,us | _ -> assert false in - let ip = if !print_projections then ip else None in - CAppExpl ((ip, f', us), List.map Lazy.force args) + Some (i,(args1,impl1),(args2,impl2)) + | None -> None let is_start_implicit = function | imp :: _ -> is_status_implicit imp && maximal_insertion_of imp | [] -> false +let extern_record ref args = + try + if !Flags.raw_print then raise Exit; + let cstrsp = match ref with GlobRef.ConstructRef c -> c | _ -> raise Not_found in + let struc = Recordops.lookup_structure (fst cstrsp) in + if PrintingRecord.active (fst cstrsp) then + () + else if PrintingConstructor.active (fst cstrsp) then + raise Exit + else if not (get_record_print ()) then + raise Exit; + let projs = struc.Recordops.s_PROJ in + let locals = struc.Recordops.s_PROJKIND in + let rec cut args n = + if Int.equal n 0 then args + else + match args with + | [] -> raise No_match + | _ :: t -> cut t (n - 1) in + let args = cut args struc.Recordops.s_EXPECTEDPARAM in + let rec ip projs locs args acc = + match projs with + | [] -> acc + | None :: q -> raise No_match + | Some c :: q -> + match locs with + | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern].") + | { Recordops.pk_true_proj = false } :: locs' -> + (* we don't want to print locals *) + ip q locs' args acc + | { Recordops.pk_true_proj = true } :: locs' -> + match args with + | [] -> raise No_match + (* we give up since the constructor is not complete *) + | arg :: tail -> + let arg = Lazy.force arg in + let loc = arg.CAst.loc in + let ref = extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c) in + ip q locs' tail ((ref, arg) :: acc) + in + Some (List.rev (ip projs locals args [])) + with + | Not_found | No_match | Exit -> None + let extern_global impl f us = if not !Constrintern.parsing_explicit && is_start_implicit impl then @@ -641,26 +682,63 @@ let extern_global impl f us = else CRef (f,us) -let extern_app inctx impl (cf,f) us args = - if List.is_empty args then - (* If coming from a notation "Notation a := @b" *) - CAppExpl ((None, f, us), []) - else if not !Constrintern.parsing_explicit && - ((!Flags.raw_print || - (!print_implicits && not !print_implicits_explicit_args)) && - List.exists is_status_implicit impl) - then +(* Implicit args indexes are in ascending order *) +(* inctx is useful only if there is a last argument to be deduced from ctxt *) +let extern_applied_ref inctx impl (cf,f) us args = + let isproj = is_projection (List.length args) cf in + try + if not !Constrintern.parsing_explicit && + ((!Flags.raw_print || + (!print_implicits && not !print_implicits_explicit_args)) && + List.exists is_status_implicit impl) + then raise Expl; + let impl = if !Constrintern.parsing_explicit then [] else impl in + let n = List.length args in + let ref = CRef (f,us) in + let f = CAst.make ref in + match extern_projection (cf,f) args impl with + (* Try a [t.(f args1) args2] projection-style notation *) + | Some (i,(args1,impl1),(args2,impl2)) -> + let args1 = adjust_implicit_arguments inctx n 1 args1 impl1 in + let args2 = adjust_implicit_arguments inctx n (i+1) args2 impl2 in + let ip = Some (List.length args1) in + CApp ((ip,f),args1@args2) + (* A normal application node with each individual implicit + arguments either dropped or made explicit *) + | None -> + let args = adjust_implicit_arguments inctx n 1 args impl in + if args = [] then ref else CApp ((None, f), args) + with Expl -> + (* A [@f args] node *) let args = List.map Lazy.force args in - CAppExpl ((is_projection (List.length args) cf,f,us), args) - else - explicitize inctx impl (cf, CAst.make @@ CRef (f,us)) args + let isproj = if !print_projections then isproj else None in + CAppExpl ((isproj,f,us), args) -let rec fill_arg_scopes args subscopes (entry,(_,scopes) as all) = match args, subscopes with -| [], _ -> [] -| a :: args, scopt :: subscopes -> - (a, (entry, (scopt, scopes))) :: fill_arg_scopes args subscopes all -| a :: args, [] -> - (a, (entry, (None, scopes))) :: fill_arg_scopes args [] all +let extern_applied_syntactic_definition n extraimpl (cf,f) syndefargs extraargs = + try + let syndefargs = List.map (fun a -> (a,None)) syndefargs in + let extraargs = adjust_implicit_arguments false (List.length extraargs) 1 extraargs extraimpl in + let args = syndefargs @ extraargs in + if args = [] then cf else CApp ((None, CAst.make cf), args) + with Expl -> + let args = syndefargs @ List.map Lazy.force extraargs in + CAppExpl ((None,f,None), args) + +let mkFlattenedCApp (head,args) = + match head.CAst.v with + | CApp (g,args') -> + (* may happen with notations for a prefix of an n-ary application *) + (* or after removal of a coercion to funclass *) + CApp (g,args'@args) + | _ -> + CApp ((None, head), args) + +let extern_applied_notation n impl f args = + if List.is_empty args then + f.CAst.v + else + let args = adjust_implicit_arguments false (List.length args) 1 args impl in + mkFlattenedCApp (f,args) let extern_args extern env args = let map (arg, argscopes) = lazy (extern argscopes env arg) in @@ -838,56 +916,19 @@ let rec extern inctx scopes vars r = | GRef (ref,us) -> let subscopes = find_arguments_scope ref in let args = fill_arg_scopes args subscopes scopes in - begin - try - if !Flags.raw_print then raise Exit; - let cstrsp = match ref with GlobRef.ConstructRef c -> c | _ -> raise Not_found in - let struc = Recordops.lookup_structure (fst cstrsp) in - if PrintingRecord.active (fst cstrsp) then - () - else if PrintingConstructor.active (fst cstrsp) then - raise Exit - else if not (get_record_print ()) then - raise Exit; - let projs = struc.Recordops.s_PROJ in - let locals = struc.Recordops.s_PROJKIND in - let rec cut args n = - if Int.equal n 0 then args - else - match args with - | [] -> raise No_match - | _ :: t -> cut t (n - 1) in - let args = cut args struc.Recordops.s_EXPECTEDPARAM in - let rec ip projs locs args acc = - match projs with - | [] -> acc - | None :: q -> raise No_match - | Some c :: q -> - match locs with - | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern].") - | { Recordops.pk_true_proj = false } :: locs' -> - (* we don't want to print locals *) - ip q locs' args acc - | { Recordops.pk_true_proj = true } :: locs' -> - match args with - | [] -> raise No_match - (* we give up since the constructor is not complete *) - | (arg, scopes) :: tail -> - let head = extern true scopes vars arg in - ip q locs' tail ((extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), head) :: acc) - in - CRecord (List.rev (ip projs locals args [])) - with - | Not_found | No_match | Exit -> - let args = extern_args (extern true) vars args in - extern_app inctx - (select_stronger_impargs (implicits_of_global ref)) - (Some ref,extern_reference ?loc vars ref) (extern_universes us) args - end - - | _ -> - explicitize inctx [] (None,sub_extern false scopes vars f) - (List.map (fun c -> lazy (sub_extern true scopes vars c)) args)) + let args = extern_args (extern true) vars args in + (* Try a "{|...|}" record notation *) + (match extern_record ref args with + | Some l -> CRecord l + | None -> + (* Otherwise... *) + extern_applied_ref inctx + (select_stronger_impargs (implicits_of_global ref)) + (ref,extern_reference ?loc vars ref) (extern_universes us) args) + | _ -> + let args = List.map (fun c -> (sub_extern true scopes vars c,None)) args in + let head = sub_extern false scopes vars f in + mkFlattenedCApp (head,args)) | GLetIn (na,b,t,c) -> CLetIn (make ?loc na,sub_extern false scopes vars b, @@ -1104,46 +1145,45 @@ and extern_notation (custom,scopes as allscopes) vars t rules = let loc = Glob_ops.loc_of_glob_constr t in try if is_inactive_rule keyrule then raise No_match; - (* Adjusts to the number of arguments expected by the notation *) - let (t,args,argsscopes,argsimpls) = match DAst.get t ,n with - | GApp (f,args), Some n - when List.length args >= n -> + let f,args = + match DAst.get t with + | GApp (f,args) -> f,args + | _ -> t,[] in + let nallargs = List.length args in + let argsscopes,argsimpls = + match DAst.get f with + | GRef (ref,_) -> + let subscopes = find_arguments_scope ref in + let impls = select_impargs_size nallargs (implicits_of_global ref) in + subscopes, impls + | _ -> + [], [] in + (* Adjust to the number of arguments expected by the notation *) + let (t,args,argsscopes,argsimpls) = match n with + | Some n when nallargs >= n && nallargs > 0 -> let args1, args2 = List.chop n args in - let subscopes, impls = - match DAst.get f with - | GRef (ref,us) -> - let subscopes = - try List.skipn n (find_arguments_scope ref) - with Failure _ -> [] in - let impls = - let impls = - select_impargs_size - (List.length args) (implicits_of_global ref) in - try List.skipn n impls with Failure _ -> [] in - subscopes,impls - | _ -> - [], [] in + let args2scopes = try List.skipn n argsscopes with Failure _ -> [] in + let args2impls = try List.skipn n argsimpls with Failure _ -> [] in + (* Note: NApp(NRef f,[]), hence n=0, encodes @f *) (if Int.equal n 0 then f else DAst.make @@ GApp (f,args1)), - args2, subscopes, impls - | GApp (f, args), None -> + args2, args2scopes, args2impls + | None when nallargs > 0 -> begin match DAst.get f with - | GRef (ref,us) -> - let subscopes = find_arguments_scope ref in - let impls = - select_impargs_size - (List.length args) (implicits_of_global ref) in - f, args, subscopes, impls + | GRef (ref,us) -> f, args, argsscopes, argsimpls | _ -> t, [], [], [] end - | GRef (ref,us), Some 0 -> DAst.make @@ GApp (t,[]), [], [], [] - | _, None -> t, [], [], [] + | Some 0 when nallargs = 0 -> + begin match DAst.get f with + | GRef (ref,us) -> DAst.make @@ GApp (t,[]), [], [], [] + | _ -> t, [], [], [] + end + | None -> t, [], [], [] | _ -> raise No_match in (* Try matching ... *) let terms,termlists,binders,binderlists = match_notation_constr !print_universes t pat in (* Try availability of interpretation ... *) - let e = - match keyrule with + match keyrule with | NotationRule (sc,ntn) -> (match availability_of_entry_coercion custom (fst ntn) with | None -> raise No_match @@ -1171,22 +1211,25 @@ and extern_notation (custom,scopes as allscopes) vars t rules = List.map (fun (bl,(subentry,(scopt,scl))) -> pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) vars bl)) binderlists in - insert_coercion coercion (insert_delimiters (make_notation loc ntn (l,ll,bl,bll)) key)) + let c = make_notation loc ntn (l,ll,bl,bll) in + let c = insert_coercion coercion (insert_delimiters c key) in + let args = fill_arg_scopes args argsscopes allscopes in + let args = extern_args (extern true) vars args in + CAst.make ?loc @@ extern_applied_notation nallargs argsimpls c args) | SynDefRule kn -> match availability_of_entry_coercion custom InConstrEntrySomeLevel with | None -> raise No_match | Some coercion -> let l = List.map (fun (c,(subentry,(scopt,scl))) -> - extern true (subentry,(scopt,scl@snd scopes)) vars c, None) + extern true (subentry,(scopt,scl@snd scopes)) vars c) terms in - let a = CRef (Nametab.shortest_qualid_of_syndef ?loc vars kn,None) in - insert_coercion coercion (CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l)) in - if List.is_empty args then e - else - let args = fill_arg_scopes args argsscopes allscopes in - let args = extern_args (extern true) vars args in - CAst.make ?loc @@ explicitize false argsimpls (None,e) args + let cf = Nametab.shortest_qualid_of_syndef ?loc vars kn in + let a = CRef (cf,None) in + let args = fill_arg_scopes args argsscopes allscopes in + let args = extern_args (extern true) vars args in + let c = CAst.make ?loc @@ extern_applied_syntactic_definition nallargs argsimpls (a,cf) l args in + insert_coercion coercion c with No_match -> extern_notation allscopes vars t rules diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c699f79351..f4ae5bf676 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1643,7 +1643,7 @@ let drop_notations_pattern looked_for genv = | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c) | None -> raise (InternalizationError (loc,NotAConstructor head)) end - | CPatCstr (qid, Some expl_pl, pl) -> + | CPatCstr (qid, Some expl_pl, pl) -> let g = try Nametab.locate qid with Not_found -> raise (InternalizationError (loc,NotAConstructor qid)) in diff --git a/kernel/cooking.ml b/kernel/cooking.ml index cebbfe4986..f1eb000c88 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -312,14 +312,14 @@ let cook_one_ind ~template_check ~ntypes let arity = abstract_as_type (expmod arity) hyps in let sort = destSort (expmod (mkSort sort)) in RegularArity {mind_user_arity=arity; mind_sort=sort} - | TemplateArity {template_param_levels=levels;template_level} -> + | TemplateArity {template_param_levels=levels;template_level;template_context} -> let sec_levels = CList.map_filter (fun d -> if RelDecl.is_local_assum d then Some (template_level_of_var ~template_check d) else None) section_decls in let levels = List.rev_append sec_levels levels in - TemplateArity {template_param_levels=levels;template_level} + TemplateArity {template_param_levels=levels;template_level;template_context} in let mind_arity_ctxt = let ctx = Context.Rel.map expmod mip.mind_arity_ctxt in diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 0b6e59bd5e..c550b0d432 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -32,6 +32,7 @@ type engagement = set_predicativity type template_arity = { template_param_levels : Univ.Level.t option list; template_level : Univ.Universe.t; + template_context : Univ.ContextSet.t; } type ('a, 'b) declaration_arity = diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 27e3f84464..047027984d 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -49,7 +49,8 @@ let map_decl_arity f g = function let hcons_template_arity ar = { template_param_levels = ar.template_param_levels; (* List.Smart.map (Option.Smart.map Univ.hcons_univ_level) ar.template_param_levels; *) - template_level = Univ.hcons_univ ar.template_level } + template_level = Univ.hcons_univ ar.template_level; + template_context = Univ.hcons_universe_context_set ar.template_context } let universes_context = function | Monomorphic _ -> Univ.AUContext.empty diff --git a/kernel/float64.ml b/kernel/float64.ml index 3e36373b77..cc661aeba3 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -12,7 +12,10 @@ format *) type t = float -let is_nan f = f <> f +(* The [f : float] type annotation enable the compiler to compile f <> f + as comparison on floats rather than the polymorphic OCaml comparison + which is much slower. *) +let is_nan (f : float) = f <> f let is_infinity f = f = infinity let is_neg_infinity f = f = neg_infinity @@ -42,19 +45,20 @@ let abs = abs_float type float_comparison = FEq | FLt | FGt | FNotComparable -let eq x y = x = y +(* See above comment on [is_nan] for the [float] type annotations. *) +let eq (x : float) (y : float) = x = y [@@ocaml.inline always] -let lt x y = x < y +let lt (x : float) (y : float) = x < y [@@ocaml.inline always] -let le x y = x <= y +let le (x : float) (y : float) = x <= y [@@ocaml.inline always] (* inspired by lib/util.ml; see also #10471 *) -let pervasives_compare = compare +let pervasives_compare (x : float) (y : float) = compare x y -let compare x y = +let compare (x : float) (y : float) = if x < y then FLt else ( diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index 591cd050a5..113ee787f2 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -66,7 +66,9 @@ let mind_check_names mie = type univ_info = { ind_squashed : bool; ind_has_relevant_arg : bool; ind_min_univ : Universe.t option; (* Some for template *) - ind_univ : Universe.t } + ind_univ : Universe.t; + missing : Universe.Set.t; (* missing u <= ind_univ constraints *) + } let check_univ_leq ?(is_real_arg=false) env u info = let ind_univ = info.ind_univ in @@ -78,9 +80,8 @@ let check_univ_leq ?(is_real_arg=false) env u info = if type_in_type env || Univ.Universe.is_sprop u || UGraph.check_leq (universes env) u ind_univ then { info with ind_min_univ = Option.map (Universe.sup u) info.ind_min_univ } else if is_impredicative_univ env ind_univ - then if Option.is_empty info.ind_min_univ then { info with ind_squashed = true } - else raise (InductiveError BadUnivs) - else raise (InductiveError BadUnivs) + && Option.is_empty info.ind_min_univ then { info with ind_squashed = true } + else {info with missing = Universe.Set.add u info.missing} let check_context_univs ~ctor env info ctx = let check_one d (info,env) = @@ -109,6 +110,7 @@ let check_arity env_params env_ar ind = ind_has_relevant_arg=false; ind_min_univ; ind_univ=Sorts.univ_of_sort ind_sort; + missing=Universe.Set.empty; } in let univ_info = check_indices_matter env_params univ_info indices in @@ -174,7 +176,7 @@ let check_record data = (* - all_sorts in case of small, unitary Prop (not smashed) *) (* - logical_sorts in case of large, unitary Prop (smashed) *) -let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_;ind_has_relevant_arg=_} = +let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_;ind_has_relevant_arg=_;missing=_} = if not ind_squashed then InType else Sorts.family (Sorts.sort_of_univ ind_univ) @@ -224,6 +226,8 @@ let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt conc params, univs let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) = + if not (Universe.Set.is_empty univ_info.missing) + then raise (InductiveError (MissingConstraints (univ_info.missing,univ_info.ind_univ))); let arity = Vars.subst_univs_level_constr usubst arity in let lc = Array.map (Vars.subst_univs_level_constr usubst) lc in let indices = Vars.subst_univs_level_context usubst indices in @@ -270,7 +274,7 @@ let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,sp CErrors.user_err Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.") else - TemplateArity {template_param_levels = param_levels; template_level = min_univ} + TemplateArity {template_param_levels = param_levels; template_level = min_univ; template_context = ctx } in let kelim = allowed_sorts univ_info in diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index f6f2058c13..8db8a044a8 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -321,6 +321,8 @@ let universes_of_private eff = let env_of_safe_env senv = senv.env let env_of_senv = env_of_safe_env +let structure_body_of_safe_env env = env.revstruct + let sections_of_safe_env senv = senv.sections let get_section = function @@ -757,7 +759,7 @@ let translate_direct_opaque env kn ce = let () = assert (is_empty_private u) in { cb with const_body = OpaqueDef c } -let export_side_effects mb env (b_ctx, eff) = +let export_side_effects mb env eff = let not_exists e = not (Environ.mem_constant e.seff_constant env) in let aux (acc,sl) e = if not (not_exists e) then acc, sl @@ -774,7 +776,7 @@ let export_side_effects mb env (b_ctx, eff) = in let rec translate_seff sl seff acc env = match seff with - | [] -> List.rev acc, b_ctx + | [] -> List.rev acc | eff :: rest -> if Int.equal sl 0 then let env, cb = @@ -803,8 +805,8 @@ let push_opaque_proof pf senv = let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in senv, o -let export_private_constants ce senv = - let exported, ce = export_side_effects senv.revstruct senv.env ce in +let export_private_constants eff senv = + let exported = export_side_effects senv.revstruct senv.env eff in let map senv (kn, c) = match c.const_body with | OpaqueDef p -> let local = empty_private c.const_universes in @@ -817,7 +819,7 @@ let export_private_constants ce senv = let exported = List.map (fun (kn, _) -> kn) exported in (* No delayed constants to declare *) let senv = List.fold_left add_constant_aux senv bodies in - (ce, exported), senv + exported, senv let add_constant l decl senv = let kn = Constant.make2 senv.modpath l in diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 92bbd264fa..e472dfd5e5 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -37,6 +37,8 @@ val env_of_safe_env : safe_environment -> Environ.env val sections_of_safe_env : safe_environment -> section_data Section.t option +val structure_body_of_safe_env : safe_environment -> Declarations.structure_body + (** The safe_environment state monad *) type safe_transformer0 = safe_environment -> safe_environment @@ -84,8 +86,8 @@ type side_effect_declaration = type exported_private_constant = Constant.t val export_private_constants : - private_constants Entries.proof_output -> - (Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer + private_constants -> + exported_private_constant list safe_transformer (** returns the main constant *) val add_constant : diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index f221ac7a4f..c2cdf98ee8 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -12,6 +12,7 @@ open Names open Constr open Environ open Reduction +open Univ (* Type errors. *) @@ -63,8 +64,8 @@ type ('constr, 'types) ptype_error = | IllFormedRecBody of 'constr pguard_error * Name.t Context.binder_annot array * int * env * ('constr, 'types) punsafe_judgment array | IllTypedRecBody of int * Name.t Context.binder_annot array * ('constr, 'types) punsafe_judgment array * 'types array - | UnsatisfiedConstraints of Univ.Constraint.t - | UndeclaredUniverse of Univ.Level.t + | UnsatisfiedConstraints of Constraint.t + | UndeclaredUniverse of Level.t | DisallowedSProp | BadRelevance @@ -83,7 +84,7 @@ type inductive_error = | NotAnArity of env * constr | BadEntry | LargeNonPropInductiveNotInType - | BadUnivs + | MissingConstraints of (Universe.Set.t * Universe.t) exception InductiveError of inductive_error diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index ae6fd31762..0f29717f12 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -11,6 +11,7 @@ open Names open Constr open Environ +open Univ (** Type errors. {% \label{typeerrors} %} *) @@ -64,8 +65,8 @@ type ('constr, 'types) ptype_error = | IllFormedRecBody of 'constr pguard_error * Name.t Context.binder_annot array * int * env * ('constr, 'types) punsafe_judgment array | IllTypedRecBody of int * Name.t Context.binder_annot array * ('constr, 'types) punsafe_judgment array * 'types array - | UnsatisfiedConstraints of Univ.Constraint.t - | UndeclaredUniverse of Univ.Level.t + | UnsatisfiedConstraints of Constraint.t + | UndeclaredUniverse of Level.t | DisallowedSProp | BadRelevance @@ -86,7 +87,8 @@ type inductive_error = | NotAnArity of env * constr | BadEntry | LargeNonPropInductiveNotInType - | BadUnivs + | MissingConstraints of (Universe.Set.t * Universe.t) + (* each universe in the set should have been <= the other one *) exception InductiveError of inductive_error @@ -133,9 +135,9 @@ val error_ill_typed_rec_body : val error_elim_explain : Sorts.family -> Sorts.family -> arity_error -val error_unsatisfied_constraints : env -> Univ.Constraint.t -> 'a +val error_unsatisfied_constraints : env -> Constraint.t -> 'a -val error_undeclared_universe : env -> Univ.Level.t -> 'a +val error_undeclared_universe : env -> Level.t -> 'a val error_disallowed_sprop : env -> 'a diff --git a/library/global.mli b/library/global.mli index a38fde41a5..b6bd69c17c 100644 --- a/library/global.mli +++ b/library/global.mli @@ -47,8 +47,8 @@ val push_named_def : (Id.t * Entries.section_def_entry) -> unit val push_section_context : (Name.t array * Univ.UContext.t) -> unit val export_private_constants : - Safe_typing.private_constants Entries.proof_output -> - Constr.constr Univ.in_universe_context_set * Safe_typing.exported_private_constant list + Safe_typing.private_constants -> + Safe_typing.exported_private_constant list val add_constant : Id.t -> Safe_typing.global_declaration -> Constant.t diff --git a/man/coqdep.1 b/man/coqdep.1 index 02c9d4390c..4223482c99 100644 --- a/man/coqdep.1 +++ b/man/coqdep.1 @@ -6,9 +6,6 @@ coqdep \- Compute inter-module dependencies for Coq and Caml programs .SH SYNOPSIS .B coqdep [ -.BI \-w -] -[ .BI \-I \ directory ] [ @@ -21,9 +18,6 @@ coqdep \- Compute inter-module dependencies for Coq and Caml programs .BI \-i ] [ -.BI \-D -] -[ .BI \-slash ] .I filename ... @@ -61,25 +55,6 @@ directives and the dot notation .BI \-c Prints the dependencies of Caml modules. (On Caml modules, the behaviour is exactly the same as ocamldep). -\" THESE OPTIONS ARE BROKEN CURRENTLY -\" .TP -\" .BI \-w -\" Prints a warning if a Coq command -\" .IR Declare \& -\" .IR ML \& -\" .IR Module \& -\" is incorrect. (For instance, you wrote `Declare ML Module "A".', -\" but the module A contains #open "B"). The correct command is printed -\" (see option \-D). The warning is printed on standard error. -\" .TP -\" .BI \-D -\" This commands looks for every command -\" .IR Declare \& -\" .IR ML \& -\" .IR Module \& -\" of each Coq file given as argument and complete (if needed) -\" the list of Caml modules. The new command is printed on -\" the standard output. No dependency is computed with this option. .TP .BI \-f \ file Read filenames and options -I, -R and -Q from a _CoqProject FILE. @@ -93,10 +68,6 @@ Indicates where is the Coq library. The default value has been determined at installation time, and therefore this option should not be used under normal circumstances. .TP -.BI \-dumpgraph[box] \ file -Dumps a dot dependency graph in file -.IR file \&. -.TP .BI \-exclude-dir \ dir Skips subdirectory .IR dir \ during @@ -169,7 +140,7 @@ example% coqdep \-I . *.v With a warning: .IP .B -example% coqdep \-w \-I . *.v +example% coqdep \-I . *.v .RS .sp .5 .nf diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 2dc3e8a934..853be82eb8 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -26,43 +26,8 @@ open Common (*S Part I: computing Coq environment. *) (***************************************) -(* FIXME: this is a Libobject hack that should be removed. *) -module DynHandle = Libobject.Dyn.Map(struct type 'a t = 'a -> (Label.t * structure_field_body) option end) - -let handle h (Libobject.Dyn.Dyn (tag, o)) = match DynHandle.find tag h with -| f -> f o -| exception Not_found -> None - let toplevel_env () = - let get_reference = function - | (_,kn), Lib.Leaf Libobject.AtomicObject o -> - let mp,l = KerName.repr kn in - let handler = - DynHandle.add Declare.Internal.objConstant begin fun _ -> - let constant = Global.lookup_constant (Constant.make1 kn) in - Some (l, SFBconst constant) - end @@ - DynHandle.add DeclareInd.Internal.objInductive begin fun _ -> - let inductive = Global.lookup_mind (MutInd.make1 kn) in - Some (l, SFBmind inductive) - end @@ - DynHandle.empty - in - handle handler o - | (_,kn), Lib.Leaf Libobject.ModuleObject _ -> - let mp,l = KerName.repr kn in - let modl = Global.lookup_module (MPdot (mp, l)) in - Some (l, SFBmodule modl) - | (_,kn), Lib.Leaf Libobject.ModuleTypeObject _ -> - let mp,l = KerName.repr kn in - let modtype = Global.lookup_modtype (MPdot (mp, l)) in - Some (l, SFBmodtype modtype) - | (_,kn), Lib.Leaf Libobject.IncludeObject _ -> - user_err Pp.(str "No extraction of toplevel Include yet.") - | _ -> None - in - List.rev (List.map_filter get_reference (Lib.contents ())) - + List.rev (Safe_typing.structure_body_of_safe_env (Global.safe_env ())) let environment_until dir_opt = let rec parse = function diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 92a2222cfa..cdadde8621 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -2416,6 +2416,36 @@ let nqa = (fun _ x -> x) Mc.cnfQ qq_domain_spec dump_qexpr nlinear_prover_R +let print_lia_profile () = + Simplex.( + let { number_of_successes + ; number_of_failures + ; success_pivots + ; failure_pivots + ; average_pivots + ; maximum_pivots } = + Simplex.get_profile_info () + in + Feedback.msg_notice + Pp.( + (* successes *) + str "number of successes: " + ++ int number_of_successes ++ fnl () + (* success pivots *) + ++ str "number of success pivots: " + ++ int success_pivots ++ fnl () + (* failure *) + ++ str "number of failures: " + ++ int number_of_failures ++ fnl () + (* failure pivots *) + ++ str "number of failure pivots: " + ++ int failure_pivots ++ fnl () + (* Other *) + ++ str "average number of pivots: " + ++ int average_pivots ++ fnl () + ++ str "maximum number of pivots: " + ++ int maximum_pivots ++ fnl ())) + (* Local Variables: *) (* coding: utf-8 *) (* End: *) diff --git a/plugins/micromega/coq_micromega.mli b/plugins/micromega/coq_micromega.mli index 37ea560241..bcfc47357f 100644 --- a/plugins/micromega/coq_micromega.mli +++ b/plugins/micromega/coq_micromega.mli @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(*val is_ground_tac : EConstr.constr -> unit Proofview.tactic*) val psatz_Z : int -> unit Proofview.tactic -> unit Proofview.tactic val psatz_Q : int -> unit Proofview.tactic -> unit Proofview.tactic val psatz_R : int -> unit Proofview.tactic -> unit Proofview.tactic @@ -21,6 +20,7 @@ val sos_Q : unit Proofview.tactic -> unit Proofview.tactic val sos_R : unit Proofview.tactic -> unit Proofview.tactic val lra_Q : unit Proofview.tactic -> unit Proofview.tactic val lra_R : unit Proofview.tactic -> unit Proofview.tactic +val print_lia_profile : unit -> unit (** {5 Use Micromega independently from tactics. } *) diff --git a/plugins/micromega/g_micromega.mlg b/plugins/micromega/g_micromega.mlg index edf8106f30..d0f70bceac 100644 --- a/plugins/micromega/g_micromega.mlg +++ b/plugins/micromega/g_micromega.mlg @@ -28,10 +28,6 @@ open Tacarg DECLARE PLUGIN "micromega_plugin" -TACTIC EXTEND RED -| [ "myred" ] -> { Tactics.red_in_concl } -END - TACTIC EXTEND PsatzZ | [ "psatz_Z" int_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_Z i (Tacinterp.tactic_of_value ist t)) @@ -87,3 +83,6 @@ TACTIC EXTEND PsatzQ | [ "psatz_Q" tactic(t) ] -> { (Coq_micromega.psatz_Q (-1) (Tacinterp.tactic_of_value ist t)) } END +VERNAC COMMAND EXTEND ShowLiaProfile CLASSIFIED AS QUERY +| [ "Show" "Lia" "Profile" ] -> { Coq_micromega.print_lia_profile () } +END diff --git a/plugins/micromega/simplex.ml b/plugins/micromega/simplex.ml index ade8143f3c..54976221bc 100644 --- a/plugins/micromega/simplex.ml +++ b/plugins/micromega/simplex.ml @@ -18,6 +18,49 @@ type ('a, 'b) sum = Inl of 'a | Inr of 'b let debug = false +(** Exploiting profiling information *) + +let profile_info = ref [] +let nb_pivot = ref 0 + +type profile_info = + { number_of_successes : int + ; number_of_failures : int + ; success_pivots : int + ; failure_pivots : int + ; average_pivots : int + ; maximum_pivots : int } + +let init_profile = + { number_of_successes = 0 + ; number_of_failures = 0 + ; success_pivots = 0 + ; failure_pivots = 0 + ; average_pivots = 0 + ; maximum_pivots = 0 } + +let get_profile_info () = + let update_profile + { number_of_successes + ; number_of_failures + ; success_pivots + ; failure_pivots + ; average_pivots + ; maximum_pivots } (b, i) = + { number_of_successes = (number_of_successes + if b then 1 else 0) + ; number_of_failures = (number_of_failures + if b then 0 else 1) + ; success_pivots = (success_pivots + if b then i else 0) + ; failure_pivots = (failure_pivots + if b then 0 else i) + ; average_pivots = average_pivots + 1 (* number of proofs *) + ; maximum_pivots = max maximum_pivots i } + in + let p = List.fold_left update_profile init_profile !profile_info in + profile_info := []; + { p with + average_pivots = + ( try (p.success_pivots + p.failure_pivots) / p.average_pivots + with Division_by_zero -> 0 ) } + type iset = unit IMap.t type tableau = Vect.t IMap.t @@ -60,10 +103,7 @@ let output_tableau o t = 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 + IMap.iter (fun k v -> Printf.fprintf o "%i : %a\n" k WithProof.output v) t let output_vars o m = IMap.iter (fun k _ -> Printf.fprintf o "%a " LinPoly.pp_var k) m @@ -224,6 +264,7 @@ let pivot_with (m : tableau) (v : var) (p : Vect.t) = IMap.map (fun (r : Vect.t) -> pivot_row r v p) m let pivot (m : tableau) (r : var) (c : var) = + incr nb_pivot; let row = safe_find "pivot" r m in let piv = solve_column c r row in IMap.add c piv (pivot_with (IMap.remove r m) c piv) @@ -477,8 +518,11 @@ let make_farkas_proof (env : WithProof.t IMap.t) vm v = try let x', b = IMap.find x vm in let n = if b then n else Num.minus_num n in - WithProof.mult (Vect.cst n) (IMap.find x' env) - with Not_found -> WithProof.mult (Vect.cst n) (IMap.find x env) + let prf = IMap.find x' env in + WithProof.mult (Vect.cst n) prf + with Not_found -> + let prf = IMap.find x env in + WithProof.mult (Vect.cst n) prf end) WithProof.zero v @@ -493,21 +537,43 @@ type ('a, 'b) hitkind = let cut env rmin sol vm (rst : Restricted.t) tbl (x, v) = let n, r = Vect.decomp_cst v in - let f = frac_num n in - if f =/ Int 0 then Forget (* The solution is integral *) + let fn = frac_num n in + if fn =/ Int 0 then Forget (* The solution is integral *) else - (* This is potentially a cut *) - let t = - if f </ Int 1 // Int 2 then - let t' = Int 1 // f in - if Num.is_integer_num t' then t' -/ Int 1 else Num.floor_num t' - else Int 1 - in - let cut_coeff1 v = + (* The cut construction is from: + Letchford and Lodi. Strengthening Chvatal-Gomory cuts and Gomory fractional cuts. + + We implement the classic Proposition 2 from the "known results" + *) + + (* Proposition 3 requires all the variables to be restricted and is + therefore not always applicable. *) + (* let ccoeff_prop1 v = frac_num v in + let ccoeff_prop3 v = + (* mixed integer cut *) let fv = frac_num v in - if fv <=/ Int 1 -/ f then fv // (Int 1 -/ f) else (Int 1 -/ fv) // f + Num.min_num fv (fn */ (Int 1 -/ fv) // (Int 1 -/ fn)) in - let cut_coeff2 v = frac_num (t */ v) in + let ccoeff_prop3 = + if Restricted.is_restricted x rst then ("Prop3", ccoeff_prop3) + else ("Prop1", ccoeff_prop1) + in *) + let n0_5 = Int 1 // Int 2 in + (* If the fractional part [fn] is small, we construct the t-cut. + If the fractional part [fn] is big, we construct the t-cut of the negated row. + (This is only a cut if all the fractional variables are restricted.) + *) + let ccoeff_prop2 = + let tmin = + if fn </ n0_5 then (* t-cut *) + Num.ceiling_num (n0_5 // fn) + else + (* multiply by -1 & t-cut *) + minus_num (Num.ceiling_num (n0_5 // (Int 1 -/ fn))) + in + ("Prop2", fun v -> frac_num (v */ tmin)) + in + let ccoeff = ccoeff_prop2 in let cut_vector ccoeff = Vect.fold (fun acc x n -> @@ -516,35 +582,31 @@ let cut env rmin sol vm (rst : Restricted.t) tbl (x, v) = Vect.null r in let lcut = - List.map - (fun cv -> Vect.normalise (cut_vector cv)) - [cut_coeff1; cut_coeff2] + ( fst ccoeff + , make_farkas_proof env vm (Vect.normalise (cut_vector (snd ccoeff))) ) in - let lcut = List.map (make_farkas_proof env vm) lcut in - let check_cutting_plane c = + let check_cutting_plane (p, c) = match WithProof.cutting_plane c with | None -> if debug then - Printf.printf "This is not a cutting plane for %a\n%a:" LinPoly.pp_var - x WithProof.output c; + Printf.printf "%s: This is not a cutting plane for %a\n%a:" p + LinPoly.pp_var x WithProof.output c; None | Some (v, prf) -> if debug then ( - Printf.printf "This is a cutting plane for %a:" LinPoly.pp_var x; + Printf.printf "%s: This is a cutting plane for %a:" p LinPoly.pp_var x; 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 ( - if debug then - Printf.printf "The cut is feasible %s >= 0 \n" - (Num.string_of_num vl); - None ) - else Some (x, (v, prf)) + Some (x, (v, prf)) in - match find_some check_cutting_plane lcut with + match check_cutting_plane lcut with | Some r -> Hit r - | None -> Keep (x, v) + | None -> + let has_unrestricted = + Vect.fold + (fun acc v vl -> acc || not (Restricted.is_restricted v rst)) + false r + in + if has_unrestricted then Keep (x, v) else Forget let merge_result_old oldr f x = match oldr with @@ -681,12 +743,16 @@ let integer_solver lp = isolve env None vr res let integer_solver lp = + nb_pivot := 0; if debug then Printf.printf "Input integer solver\n%a\n" WithProof.output_sys (List.map WithProof.of_cstr lp); match integer_solver lp with - | None -> None + | None -> + profile_info := (false, !nb_pivot) :: !profile_info; + None | Some prf -> + profile_info := (true, !nb_pivot) :: !profile_info; if debug then Printf.fprintf stdout "Proof %a\n" ProofFormat.output_proof prf; Some prf diff --git a/plugins/micromega/simplex.mli b/plugins/micromega/simplex.mli index 19bcce3590..ff672edafd 100644 --- a/plugins/micromega/simplex.mli +++ b/plugins/micromega/simplex.mli @@ -9,6 +9,20 @@ (************************************************************************) open Polynomial +(** Profiling *) + +type profile_info = + { number_of_successes : int + ; number_of_failures : int + ; success_pivots : int + ; failure_pivots : int + ; average_pivots : int + ; maximum_pivots : int } + +val get_profile_info : unit -> profile_info + +(** Simplex interface *) + val optimise : Vect.t -> cstr list -> (Num.num option * Num.num option) option val find_point : cstr list -> Vect.t option val find_unsat_certificate : cstr list -> Vect.t option diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index b54a713a16..aafd662f7d 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -311,21 +311,47 @@ let eq_alias a b = match a, b with | VarAlias id1, VarAlias id2 -> Id.equal id1 id2 | _ -> false -type aliasing = EConstr.t option * alias list +type 'a aliasing = 'a option * alias list let empty_aliasing = None, [] let make_aliasing c = Some c, [] let push_alias (alias, l) a = (alias, a :: l) + +module Alias = +struct +type t = { mutable lift : int; mutable data : EConstr.t } + +let make c = { lift = 0; data = c } + +let lift n { lift; data } = { lift = lift + n; data } + +let eval alias = + let c = EConstr.Vars.lift alias.lift alias.data in + let () = alias.lift <- 0 in + let () = alias.data <- c in + c + +let repr sigma alias = match EConstr.kind sigma alias.data with +| Rel n -> Some (RelAlias (n + alias.lift)) +| Var id -> Some (VarAlias id) +| _ -> None + +end + let lift_aliasing n (alias, l) = let map a = match a with | VarAlias _ -> a | RelAlias m -> RelAlias (m + n) in - (Option.map (fun c -> lift n c) alias, List.map map l) + (Option.map (fun c -> Alias.lift n c) alias, List.map map l) + +let cast_aliasing (alias, l) = match alias with +| None -> (None, l) +| Some c -> (Some (Alias.make c), l) type aliases = { - rel_aliases : aliasing Int.Map.t; - var_aliases : aliasing Id.Map.t; + rel_aliases : Alias.t aliasing Int.Map.t; + var_aliases : EConstr.t aliasing Id.Map.t; (** Only contains [VarAlias] *) } @@ -359,13 +385,14 @@ let compute_rel_aliases var_aliases rels sigma = | Var id' -> let aliases_of_n = try Id.Map.find id' var_aliases with Not_found -> empty_aliasing in - Int.Map.add n (push_alias aliases_of_n (VarAlias id')) aliases + Int.Map.add n (push_alias (cast_aliasing aliases_of_n) (VarAlias id')) aliases | Rel p -> let aliases_of_n = try Int.Map.find (p+n) aliases with Not_found -> empty_aliasing in Int.Map.add n (push_alias aliases_of_n (RelAlias (p+n))) aliases | _ -> - Int.Map.add n (make_aliasing (lift n (mkCast(t,DEFAULTcast,u)))) aliases) + let alias = Alias.lift n (Alias.make @@ mkCast(t,DEFAULTcast, u)) in + Int.Map.add n (make_aliasing alias) aliases) | LocalAssum _ -> aliases) ) rels @@ -387,7 +414,7 @@ let lift_aliases n aliases = let get_alias_chain_of sigma aliases x = match x with | RelAlias n -> (try Int.Map.find n aliases.rel_aliases with Not_found -> empty_aliasing) - | VarAlias id -> (try Id.Map.find id aliases.var_aliases with Not_found -> empty_aliasing) + | VarAlias id -> (try cast_aliasing (Id.Map.find id aliases.var_aliases) with Not_found -> empty_aliasing) let normalize_alias_opt_alias sigma aliases x = match get_alias_chain_of sigma aliases x with @@ -420,13 +447,14 @@ let extend_alias sigma decl { var_aliases; rel_aliases } = | Var id' -> let aliases_of_binder = try Id.Map.find id' var_aliases with Not_found -> empty_aliasing in - Int.Map.add 1 (push_alias aliases_of_binder (VarAlias id')) rel_aliases + Int.Map.add 1 (push_alias (cast_aliasing aliases_of_binder) (VarAlias id')) rel_aliases | Rel p -> let aliases_of_binder = try Int.Map.find (p+1) rel_aliases with Not_found -> empty_aliasing in Int.Map.add 1 (push_alias aliases_of_binder (RelAlias (p+1))) rel_aliases | _ -> - Int.Map.add 1 (make_aliasing (lift 1 t)) rel_aliases) + let alias = Alias.lift 1 (Alias.make t) in + Int.Map.add 1 (make_aliasing alias) rel_aliases) | LocalAssum _ -> rel_aliases in { var_aliases; rel_aliases } @@ -434,7 +462,7 @@ let expand_alias_once sigma aliases x = match get_alias_chain_of sigma aliases x with | None, [] -> None | Some a, [] -> Some a - | _, l -> Some (of_alias (List.last l)) + | _, l -> Some (Alias.make (of_alias (List.last l))) let expansions_of_var sigma aliases x = let (_, l) = get_alias_chain_of sigma aliases x in @@ -442,9 +470,9 @@ let expansions_of_var sigma aliases x = let expansion_of_var sigma aliases x = match get_alias_chain_of sigma aliases x with - | None, [] -> (false, of_alias x) - | Some a, _ -> (true, a) - | None, a :: _ -> (true, of_alias a) + | None, [] -> (false, Some x) + | Some a, _ -> (true, Alias.repr sigma a) + | None, a :: _ -> (true, Some a) let rec expand_vars_in_term_using sigma aliases t = match EConstr.kind sigma t with | Rel n -> of_alias (normalize_alias sigma aliases (RelAlias n)) @@ -482,10 +510,10 @@ let free_vars_and_rels_up_alias_expansion env sigma aliases c = match ck with | VarAlias id -> acc4 := Id.Set.add id !acc4 | RelAlias n -> if n >= depth+1 then acc3 := Int.Set.add (n-depth) !acc3); - match EConstr.kind sigma c' with - | Var id -> acc2 := Id.Set.add id !acc2 - | Rel n -> if n >= depth+1 then acc1 := Int.Set.add (n-depth) !acc1 - | _ -> frec (aliases,depth) c end + match c' with + | Some (VarAlias id) -> acc2 := Id.Set.add id !acc2 + | Some (RelAlias n) -> if n >= depth+1 then acc1 := Int.Set.add (n-depth) !acc1 + | None -> frec (aliases,depth) c end | Const _ | Ind _ | Construct _ -> acc2 := Id.Set.union (vars_of_global env (fst @@ EConstr.destRef sigma c)) !acc2 | _ -> @@ -971,7 +999,7 @@ let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_ with Not_found -> match expand_alias_once evd aliases t with | None -> raise Not_found - | Some c -> aux k (lift k c) in + | Some c -> aux k (Alias.eval (Alias.lift k c)) in try let c = aux 0 c_in_env_extended_with_k_binders in Invertible (UniqueProjection (c,!effects)) @@ -1223,7 +1251,7 @@ let rec is_constrainable_in top env evd k (ev,(fv_rels,fv_ids) as g) t = let has_constrainable_free_vars env evd aliases force k ev (fv_rels,fv_ids,let_rels,let_ids) t = match to_alias evd t with | Some t -> - let expanded, t' = expansion_of_var evd aliases t in + let expanded, _ = expansion_of_var evd aliases t in if expanded then (* t is a local definition, we keep it only if appears in the list *) (* of let-in variables effectively occurring on the right-hand side, *) diff --git a/proofs/proof.ml b/proofs/proof.ml index 5ab4409f8b..e2ee5426b5 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -69,18 +69,15 @@ exception FullyUnfocused let _ = CErrors.register_handler begin function | CannotUnfocusThisWay -> - CErrors.user_err Pp.(str "This proof is focused, but cannot be unfocused this way") + Pp.str "This proof is focused, but cannot be unfocused this way" | NoSuchGoals (i,j) when Int.equal i j -> - CErrors.user_err ~hdr:"Focus" Pp.(str"No such goal (" ++ int i ++ str").") + Pp.(str "[Focus] No such goal (" ++ int i ++ str").") | NoSuchGoals (i,j) -> - CErrors.user_err ~hdr:"Focus" Pp.( - str"Not every goal in range ["++ int i ++ str","++int j++str"] exist." - ) + Pp.(str "[Focus] Not every goal in range ["++ int i ++ str","++int j++str"] exist.") | NoSuchGoal id -> - CErrors.user_err - ~hdr:"Focus" - Pp.(str "No such goal: " ++ str (Names.Id.to_string id) ++ str ".") - | FullyUnfocused -> CErrors.user_err Pp.(str "The proof is not focused") + Pp.(str "[Focus] No such goal: " ++ str (Names.Id.to_string id) ++ str ".") + | FullyUnfocused -> + Pp.str "The proof is not focused" | _ -> raise CErrors.Unhandled end diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index 66e2ae5c29..61e8741973 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -79,7 +79,7 @@ module Strict = struct (function | FailedBullet (b,sugg) -> let prefix = Pp.(str"Wrong bullet " ++ pr_bullet b ++ str": ") in - CErrors.user_err ~hdr:"Focus" Pp.(prefix ++ suggest_on_error sugg) + Pp.(str "[Focus]" ++ spc () ++ prefix ++ suggest_on_error sugg) | _ -> raise CErrors.Unhandled) @@ -204,8 +204,7 @@ exception SuggestNoSuchGoals of int * Proof.t let _ = CErrors.register_handler begin function | SuggestNoSuchGoals(n,proof) -> let suffix = suggest proof in - CErrors.user_err - Pp.(str "No such " ++ str (CString.plural n "goal") ++ str "." ++ - pr_non_empty_arg (fun x -> x) suffix) + Pp.(str "No such " ++ str (CString.plural n "goal") ++ str "." ++ + pr_non_empty_arg (fun x -> x) suffix) | _ -> raise CErrors.Unhandled end diff --git a/tactics/declare.ml b/tactics/declare.ml index c7581fb0e0..ce2f3ec2c5 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -160,6 +160,18 @@ let register_side_effect (c, role) = | None -> () | Some (Evd.Schema (ind, kind)) -> DeclareScheme.declare_scheme kind [|ind,c|] +let get_roles export eff = + let map c = + let role = try Some (Cmap.find c eff.Evd.seff_roles) with Not_found -> None in + (c, role) + in + List.map map export + +let export_side_effects eff = + let export = Global.export_private_constants eff.Evd.seff_private in + let export = get_roles export eff in + List.iter register_side_effect export + let record_aux env s_ty s_bo = let open Environ in let in_ty = keep_hyps env s_ty in @@ -278,13 +290,6 @@ let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a proo opaque_entry_universes = univs; } -let get_roles export eff = - let map c = - let role = try Some (Cmap.find c eff.Evd.seff_roles) with Not_found -> None in - (c, role) - in - List.map map export - let feedback_axiom () = Feedback.(feedback AddedAxiom) let is_unsafe_typing_flags () = @@ -293,37 +298,36 @@ let is_unsafe_typing_flags () = let define_constant ~name cd = (* Logically define the constant and its subproofs, no libobject tampering *) - let export, decl, unsafe = match cd with - | DefinitionEntry de -> - (* We deal with side effects *) - if not de.proof_entry_opaque then - (* This globally defines the side-effects in the environment. *) - let body, eff = Future.force de.proof_entry_body in - let body, export = Global.export_private_constants (body, eff.Evd.seff_private) in - let export = get_roles export eff in - let de = { de with proof_entry_body = Future.from_val (body, ()) } in - let cd = Entries.DefinitionEntry (cast_proof_entry de) in - export, ConstantEntry cd, false - else - let map (body, eff) = body, eff.Evd.seff_private in - let body = Future.chain de.proof_entry_body map in - let de = { de with proof_entry_body = body } in - let de = cast_opaque_proof_entry EffectEntry de in - [], OpaqueEntry de, false - | ParameterEntry e -> - [], ConstantEntry (Entries.ParameterEntry e), not (Lib.is_modtype_strict()) - | PrimitiveEntry e -> - [], ConstantEntry (Entries.PrimitiveEntry e), false + let decl, unsafe = match cd with + | DefinitionEntry de -> + (* We deal with side effects *) + if not de.proof_entry_opaque then + let body, eff = Future.force de.proof_entry_body in + (* This globally defines the side-effects in the environment + and registers their libobjects. *) + let () = export_side_effects eff in + let de = { de with proof_entry_body = Future.from_val (body, ()) } in + let cd = Entries.DefinitionEntry (cast_proof_entry de) in + ConstantEntry cd, false + else + let map (body, eff) = body, eff.Evd.seff_private in + let body = Future.chain de.proof_entry_body map in + let de = { de with proof_entry_body = body } in + let de = cast_opaque_proof_entry EffectEntry de in + OpaqueEntry de, false + | ParameterEntry e -> + ConstantEntry (Entries.ParameterEntry e), not (Lib.is_modtype_strict()) + | PrimitiveEntry e -> + ConstantEntry (Entries.PrimitiveEntry e), false in let kn = Global.add_constant name decl in if unsafe || is_unsafe_typing_flags() then feedback_axiom(); - kn, export + kn let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd = let () = check_exists name in - let kn, export = define_constant ~name cd in - (* Register the libobjects attached to the constants and its subproofs *) - let () = List.iter register_side_effect export in + let kn = define_constant ~name cd in + (* Register the libobjects attached to the constants *) let () = register_constant kn kind local in kn @@ -377,10 +381,8 @@ let declare_variable ~name ~kind d = | SectionLocalDef (de) -> (* The body should already have been forced upstream because it is a section-local definition, but it's not enforced by typing *) - let (body, eff) = Future.force de.proof_entry_body in - let ((body, uctx), export) = Global.export_private_constants (body, eff.Evd.seff_private) in - let eff = get_roles export eff in - let () = List.iter register_side_effect eff in + let ((body, uctx), eff) = Future.force de.proof_entry_body in + let () = export_side_effects eff in let poly, univs = match de.proof_entry_universes with | Monomorphic_entry uctx -> false, uctx | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml index 3c9803432a..a4a06873b8 100644 --- a/tactics/pfedit.ml +++ b/tactics/pfedit.ml @@ -27,7 +27,7 @@ let use_unification_heuristics () = !use_unification_heuristics_ref exception NoSuchGoal let () = CErrors.register_handler begin function - | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.") + | NoSuchGoal -> Pp.(str "No such goal.") | _ -> raise CErrors.Unhandled end diff --git a/test-suite/bugs/closed/bug_5617.v b/test-suite/bugs/closed/bug_5617.v new file mode 100644 index 0000000000..c18e79295c --- /dev/null +++ b/test-suite/bugs/closed/bug_5617.v @@ -0,0 +1,8 @@ +Set Primitive Projections. +Record T X := { F : X }. + +Fixpoint f (n : nat) : nat := +match n with +| 0 => 0 +| S m => F _ {| F := f |} m +end. diff --git a/test-suite/micromega/bug_11436.v b/test-suite/micromega/bug_11436.v new file mode 100644 index 0000000000..fc6ccbb233 --- /dev/null +++ b/test-suite/micromega/bug_11436.v @@ -0,0 +1,19 @@ +Require Import ZArith Lia. +Local Open Scope Z_scope. + +Unset Lia Cache. + +Goal forall a q q0 q1 r r0 r1: Z, + 0 <= a < 2 ^ 64 -> + r1 = 4 * q + r -> + 0 <= r < 4 -> + a = 4 * q0 + r0 -> + 0 <= r0 < 4 -> + a + 4 = 2 ^ 64 * q1 + r1 -> + 0 <= r1 < 2 ^ 64 -> + r = r0. +Proof. + intros. + (* subst. *) + Time lia. +Qed. diff --git a/test-suite/micromega/evars_loops_in_8_10_fixed_8_11.v b/test-suite/micromega/evars_loops_in_8_10_fixed_8_11.v new file mode 100644 index 0000000000..a53c160e45 --- /dev/null +++ b/test-suite/micromega/evars_loops_in_8_10_fixed_8_11.v @@ -0,0 +1,4 @@ +Require Import Lia. +Goal forall n (B: n >= 0), exists Goal1 Goal2 Goal3, + (0 * (Goal1 * Goal2 + Goal1) <> Goal3 * 0 * (Goal1 * S Goal2)). +Proof. eexists _, _, _. Fail lia. Abort. diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v index 9efb81a901..36b4243ef8 100644 --- a/test-suite/micromega/square.v +++ b/test-suite/micromega/square.v @@ -11,15 +11,14 @@ Open Scope Z_scope. Lemma Zabs_square : forall x, (Z.abs x)^2 = x^2. Proof. - intros ; case (Zabs_dec x) ; intros ; nia. + intros ; nia. Qed. -Hint Resolve Z.abs_nonneg Zabs_square. Lemma integer_statement : ~exists n, exists p, n^2 = 2*p^2 /\ n <> 0. Proof. intros [n [p [Heq Hnz]]]; pose (n' := Z.abs n); pose (p':=Z.abs p). assert (facts : 0 <= Z.abs n /\ 0 <= Z.abs p /\ Z.abs n^2=n^2 - /\ Z.abs p^2 = p^2) by auto. + /\ Z.abs p^2 = p^2) by auto using Z.abs_nonneg, Zabs_square. assert (H : (0 < n' /\ 0 <= p' /\ n' ^2 = 2* p' ^2)) by (destruct facts as [Hf1 [Hf2 [Hf3 Hf4]]]; unfold n', p' ; nia). generalize p' H; elim n' using (well_founded_ind (Zwf_well_founded 0)); clear. @@ -45,10 +44,7 @@ Proof. intros. destruct x. simpl. - unfold Z.pow_pos. - simpl. - rewrite Pos.mul_1_r. - reflexivity. + lia. Qed. Theorem sqrt2_not_rational : ~exists x:Q, x^2==2#1. diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 799d310fa7..43f88f42a5 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -63,3 +63,11 @@ fun '{| |} => true : R -> bool b = a : Prop +The command has indeed failed with message: +The format is not the same on the right- and left-hand sides of the special token "..". +The command has indeed failed with message: +The format is not the same on the right- and left-hand sides of the special token "..". +The command has indeed failed with message: +The format is not the same on the right- and left-hand sides of the special token "..". +The command has indeed failed with message: +The format is not the same on the right- and left-hand sides of the special token "..". diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 26c7840a16..4de6ce19b4 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -158,3 +158,29 @@ Check b = a. End Test. End L. + +Module M. + +(* Accept boxes around the end variables of a recursive notation (if equal boxes) *) + +Notation " {@ T1 ; T2 ; .. ; Tn } " := + (and T1 (and T2 .. (and Tn True)..)) + (format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[' Tn ']' } ']'"). + +Fail Notation " {@ T1 ; T2 ; .. ; Tn } " := + (and T1 (and T2 .. (and Tn True)..)) + (format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[' Tn ']' } ']'"). + +Fail Notation " {@ T1 ; T2 ; .. ; Tn } " := + (and T1 (and T2 .. (and Tn True)..)) + (format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[v' Tn ']' } ']'"). + +Fail Notation " {@ T1 ; T2 ; .. ; Tn } " := + (and T1 (and T2 .. (and Tn True)..)) + (format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[' Tn ']' } ']'"). + +Fail Notation " {@ T1 ; T2 ; .. ; Tn } " := + (and T1 (and T2 .. (and Tn True)..)) + (format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[' Tn ']' } ']'"). + +End M. diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out new file mode 100644 index 0000000000..83dd2f40fb --- /dev/null +++ b/test-suite/output/Notations5.out @@ -0,0 +1,248 @@ +p 0 0 true + : 0 = 0 /\ true = true +p 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +p 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +p 0 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +p 0 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +p (A:=nat) + : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b +p (A:=nat) + : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b +@p nat 0 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +@p + : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b +p 0 0 + : forall b : bool, 0 = 0 /\ b = b +p + : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b +p 0 0 true + : 0 = 0 /\ true = true +p 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +p 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +p 0 0 + : forall b : bool, 0 = 0 /\ b = b +p 0 0 + : forall b : bool, 0 = 0 /\ b = b +p + : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b +p + : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b +@p nat 0 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +@p + : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b +f x true + : 0 = 0 /\ true = true +f x (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +f x (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +@f nat + : forall a1 a2 : nat, + T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b +f (a1:=0) (a2:=0) + : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b +f (a1:=0) (a2:=0) + : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b +@f + : forall (A : Type) (a1 a2 : A), + T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b +f + : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b +x.(f) true + : 0 = 0 /\ true = true +x.(f) (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +x.(f) (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +@f nat + : forall a1 a2 : nat, + T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b +f (a1:=0) (a2:=0) + : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b +f (a1:=0) (a2:=0) + : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b +@f + : forall (A : Type) (a1 a2 : A), + T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b +f + : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b +p + : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b +where +?A : [ |- Type] +p + : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b +where +?A : [ |- Type] +u + : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b +u + : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b +p 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +p 0 0 + : forall b : bool, 0 = 0 /\ b = b +@p nat 0 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +@p nat 0 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +u + : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b +where +?A : [ |- Type] +u + : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b +u + : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b +u + : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b +where +?A : [ |- Type] +u 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +u 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +@u nat 0 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +@u nat 0 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +u 0 0 true + : 0 = 0 /\ true = true +u 0 0 true + : 0 = 0 /\ true = true +v + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +v 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +v 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +v 0 (B:=bool) true + : 0 = 0 /\ true = true +v + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +@v 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +@v 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +v 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +v + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +v 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +v 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +v 0 (B:=bool) true + : 0 = 0 /\ true = true +v + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +@v 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +@v 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +v 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +## + : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b +where +?A : [ |- Type] +## + : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b +where +?A : [ |- Type] +## 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +## 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +## 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +## 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +## 0 0 (B:=bool) true + : 0 = 0 /\ true = true +## 0 0 (B:=bool) true + : 0 = 0 /\ true = true +## 0 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +## 0 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +p + : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b +where +?A : [ |- Type] +## + : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b +## + : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b +p 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +p 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +@p nat 0 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b +p 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +p 0 0 + : forall b : ?B, 0 = 0 /\ b = b +where +?B : [ |- Type] +p 0 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +p 0 0 true + : 0 = 0 /\ true = true +## 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +## 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +## 0 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +## 0 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +## 0 0 (B:=bool) true + : 0 = 0 /\ true = true +## 0 0 (B:=bool) true + : 0 = 0 /\ true = true +## 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +## 0 + : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +## 0 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +## 0 0 (B:=bool) + : forall b : bool, 0 = 0 /\ b = b +## 0 0 (B:=bool) true + : 0 = 0 /\ true = true +## 0 0 (B:=bool) true + : 0 = 0 /\ true = true diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v new file mode 100644 index 0000000000..b3bea929ba --- /dev/null +++ b/test-suite/output/Notations5.v @@ -0,0 +1,340 @@ +Module AppliedTermsPrinting. + +(* Test different printing paths for applied terms *) + + Module InferredGivenImplicit. + Set Implicit Arguments. + Set Maximal Implicit Insertion. + + Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b. + + Check p 0 0 true. + (* p 0 0 true *) + Check p 0 0. + (* p 0 0 *) + Check p 0. + (* p 0 *) + Check @p _ 0 0 bool. + (* p 0 0 (B:=bool) *) + Check p 0 0 (B:=bool). + (* p 0 0 (B:=bool) *) + Check @p nat. + (* p (A:=nat) *) + Check p (A:=nat). + (* p (A:=nat) *) + Check @p _ 0 0. + (* @p nat 0 0 *) + Check @p. + (* @p *) + + Unset Printing Implicit Defensive. + Check @p _ 0 0 bool. + (* p 0 0 *) + Check @p nat. + (* p *) + Set Printing Implicit Defensive. + End InferredGivenImplicit. + + Module ManuallyGivenImplicit. + Axiom p : forall {A} (a1 a2:A) {B} (b:B), a1 = a2 /\ b = b. + + Check p 0 0 true. + (* p 0 0 true *) + Check p 0 0. + (* p 0 0 *) + Check p 0. + (* p 0 *) + Check @p _ 0 0 bool. + (* p 0 0 *) + Check p 0 0 (B:=bool). + (* p 0 0 *) + Check @p nat. + (* p *) + Check p (A:=nat). + (* p *) + Check @p _ 0 0. + (* @p nat 0 0 *) + Check @p. + (* @p *) + + End ManuallyGivenImplicit. + + Module ProjectionWithImplicits. + Set Implicit Arguments. + Set Maximal Implicit Insertion. + + Record T {A} (a1 a2:A) := { f : forall B (b:B), a1 = a2 /\ b = b }. + Parameter x : T 0 0. + Check f x true. + (* f x true *) + Check @f _ _ _ x bool. + (* f x (B:=bool) *) + Check f x (B:=bool). + (* f x (B:=bool) *) + Check @f nat. + (* @f nat *) + Check @f _ 0 0. + (* f (a1:=0) (a2:=0) *) + Check f (a1:=0) (a2:=0). + (* f (a1:=0) (a2:=0) *) + Check @f. + (* @f *) + + Unset Printing Implicit Defensive. + Check f (a1:=0) (a2:=0). + (* f *) + Set Printing Implicit Defensive. + + Set Printing Projections. + + Check x.(f) true. + (* x.(f) true *) + Check x.(@f _ _ _) bool. + (* x.(f) (B:=bool) *) + Check x.(f) (B:=bool). + (* x.(f) (B:=bool) *) + Check @f nat. + (* @f nat *) + Check @f _ 0 0. + (* f (a1:=0) (a2:=0) *) + Check f (a1:=0) (a2:=0). + (* f (a1:=0) (a2:=0) *) + Check @f. + (* @f *) + + Unset Printing Implicit Defensive. + Check f (a1:=0) (a2:=0). + (* f *) + + End ProjectionWithImplicits. + + Module AtAbbreviationForApplicationHead. + + Axiom p : forall {A} (a1 a2:A) {B} (b:B), a1 = a2 /\ b = b. + + Notation u := @p. + + Check u _. + (* p *) + Check p. + (* p *) + Check @p. + (* u *) + Check u. + (* u *) + Check p 0 0. + (* p 0 0 *) + Check u nat 0 0 bool. + (* p 0 0 -- WEAKNESS should ideally be (B:=bool) *) + Check u nat 0 0. + (* @p nat 0 0 *) + Check @p nat 0 0. + (* @p nat 0 0 *) + + End AtAbbreviationForApplicationHead. + + Module AbbreviationForApplicationHead. + + Set Implicit Arguments. + Set Maximal Implicit Insertion. + + Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b. + + Notation u := p. + + Check p. + (* u *) + Check @p. + (* u -- BUG *) + Check @u. + (* u -- BUG *) + Check u. + (* u *) + Check p 0 0. + (* u 0 0 *) + Check u 0 0. + (* u 0 0 *) + Check @p nat 0 0. + (* @u nat 0 0 *) + Check @u nat 0 0. + (* @u nat 0 0 *) + Check p 0 0 true. + (* u 0 0 true *) + Check u 0 0 true. + (* u 0 0 true *) + + End AbbreviationForApplicationHead. + + Module AtAbbreviationForPartialApplication. + + Set Implicit Arguments. + Set Maximal Implicit Insertion. + + Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b. + + Notation v := (@p _ 0). + + Check v. + (* v *) + Check p 0 0. + (* v 0 *) + Check v 0. + (* v 0 *) + Check v 0 true. + (* v 0 (B:=bool) true -- BUG *) + Check @p nat 0. + (* v *) + Check @p nat 0 0. + (* @v 0 *) + Check @v 0. + (* @v 0 *) + Check @p nat 0 0 bool. + (* v 0 (B:=bool) *) + + End AtAbbreviationForPartialApplication. + + Module AbbreviationForPartialApplication. + + Set Implicit Arguments. + Set Maximal Implicit Insertion. + + Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b. + + Notation v := (p 0). + + Check v. + (* v *) + Check p 0 0. + (* v 0 *) + Check v 0. + (* v 0 *) + Check v 0 true. + (* v 0 (B:=bool) true -- BUG *) + Check @p nat 0. + (* v *) + Check @p nat 0 0. + (* @v 0 *) + Check @v 0. + (* @v 0 *) + Check @p nat 0 0 bool. + (* v 0 (B:=bool) *) + + End AbbreviationForPartialApplication. + + Module NotationForHeadApplication. + + Set Implicit Arguments. + Set Maximal Implicit Insertion. + + Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b. + + Notation "##" := p (at level 0). + + Check p. + (* ## *) + Check ##. + (* ## *) + Check p 0. + (* ## 0 *) + Check ## 0. + (* ## 0 *) + Check p 0 0. + (* ## 0 0 *) + Check ## 0 0. + (* ## 0 0 *) + Check p 0 0 true. + (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *) + Check ## 0 0 true. + (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *) + Check p 0 0 (B:=bool). + (* ## 0 0 (B:=bool) *) + Check ## 0 0 (B:=bool). + (* ## 0 0 (B:=bool) *) + + End NotationForHeadApplication. + + Module AtNotationForHeadApplication. + + Set Implicit Arguments. + Set Maximal Implicit Insertion. + + Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b. + + Notation "##" := @p (at level 0). + + Check p. + (* p *) + Check @p. + (* ## *) + Check ##. + (* ## *) + Check p 0. + (* p 0 -- why not "## nat 0" *) + Check ## nat 0. + (* p 0 *) + Check ## nat 0 0. + (* @p nat 0 0 *) + Check p 0 0. + (* p 0 0 *) + Check ## nat 0 0 _. + (* p 0 0 *) + Check ## nat 0 0 bool. + (* p 0 0 (B:=bool) *) + Check ## nat 0 0 bool true. + (* p 0 0 true *) + + End AtNotationForHeadApplication. + + Module NotationForPartialApplication. + + Set Implicit Arguments. + Set Maximal Implicit Insertion. + + Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b. + + Notation "## q" := (p q) (at level 0, q at level 0). + + Check p 0. + (* ## 0 *) + Check ## 0. + (* ## 0 *) + (* Check ## 0 0. *) + (* Anomaly *) + Check p 0 0 (B:=bool). + (* ## 0 0 (B:=bool) *) + Check ## 0 0 bool. + (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *) + Check p 0 0 true. + (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *) + Check ## 0 0 bool true. + (* ## 0 0 (B:=bool) true -- INCONSISTENT parsing/printing + BUG B should not be displayed *) + + End NotationForPartialApplication. + + Module AtNotationForPartialApplication. + + Set Implicit Arguments. + Set Maximal Implicit Insertion. + + Axiom p : forall A (a1 a2:A) B (b:B), a1 = a2 /\ b = b. + + Notation "## q" := (@p _ q) (at level 0, q at level 0). + + Check p 0. + (* ## 0 *) + Check ## 0. + (* ## 0 *) + (* Check ## 0 0. *) + (* Anomaly *) + Check p 0 0 (B:=bool). + (* ## 0 0 (B:=bool) *) + Check ## 0 0 bool. + (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *) + Check p 0 0 true. + (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *) + Check ## 0 0 bool true. + (* ## 0 0 (B:=bool) true -- INCONSISTENCY parsing/printing + BUG B should not be displayed *) + + End AtNotationForPartialApplication. + +End AppliedTermsPrinting. diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v index 128543d8ab..18cc3aa034 100644 --- a/theories/Reals/RList.v +++ b/theories/Reals/RList.v @@ -8,98 +8,90 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +Require Import List. Require Import Rbase. Require Import Rfunctions. Local Open Scope R_scope. -Inductive Rlist : Type := -| nil : Rlist -| cons : R -> Rlist -> Rlist. -Fixpoint In (x:R) (l:Rlist) : Prop := - match l with - | nil => False - | cons a l' => x = a \/ In x l' - end. +#[deprecated(since="8.12",note="use (list R) instead")] +Notation Rlist := (list R). -Fixpoint Rlength (l:Rlist) : nat := - match l with - | nil => 0%nat - | cons a l' => S (Rlength l') - end. +#[deprecated(since="8.12",note="use List.length instead")] +Notation Rlength := List.length. -Fixpoint MaxRlist (l:Rlist) : R := +Fixpoint MaxRlist (l:list R) : R := match l with | nil => 0 - | cons a l1 => + | a :: l1 => match l1 with | nil => a - | cons a' l2 => Rmax a (MaxRlist l1) + | a' :: l2 => Rmax a (MaxRlist l1) end end. -Fixpoint MinRlist (l:Rlist) : R := +Fixpoint MinRlist (l:list R) : R := match l with | nil => 1 - | cons a l1 => + | a :: l1 => match l1 with | nil => a - | cons a' l2 => Rmin a (MinRlist l1) + | a' :: l2 => Rmin a (MinRlist l1) end end. -Lemma MaxRlist_P1 : forall (l:Rlist) (x:R), In x l -> x <= MaxRlist l. +Lemma MaxRlist_P1 : forall (l:list R) (x:R), In x l -> x <= MaxRlist l. Proof. intros; induction l as [| r l Hrecl]. simpl in H; elim H. induction l as [| r0 l Hrecl0]. simpl in H; elim H; intro. - simpl; right; assumption. + simpl; right; symmetry; assumption. elim H0. - replace (MaxRlist (cons r (cons r0 l))) with (Rmax r (MaxRlist (cons r0 l))). + replace (MaxRlist (r :: r0 :: l)) with (Rmax r (MaxRlist (r0 :: l))). simpl in H; decompose [or] H. rewrite H0; apply RmaxLess1. - unfold Rmax; case (Rle_dec r (MaxRlist (cons r0 l))); intro. + unfold Rmax; case (Rle_dec r (MaxRlist (r0 :: l))); intro. apply Hrecl; simpl; tauto. - apply Rle_trans with (MaxRlist (cons r0 l)); + apply Rle_trans with (MaxRlist (r0 :: l)); [ apply Hrecl; simpl; tauto | left; auto with real ]. - unfold Rmax; case (Rle_dec r (MaxRlist (cons r0 l))); intro. + unfold Rmax; case (Rle_dec r (MaxRlist (r0 :: l))); intro. apply Hrecl; simpl; tauto. - apply Rle_trans with (MaxRlist (cons r0 l)); + apply Rle_trans with (MaxRlist (r0 :: l)); [ apply Hrecl; simpl; tauto | left; auto with real ]. reflexivity. Qed. -Fixpoint AbsList (l:Rlist) (x:R) : Rlist := +Fixpoint AbsList (l:list R) (x:R) : list R := match l with | nil => nil - | cons a l' => cons (Rabs (a - x) / 2) (AbsList l' x) + | a :: l' => (Rabs (a - x) / 2) :: (AbsList l' x) end. -Lemma MinRlist_P1 : forall (l:Rlist) (x:R), In x l -> MinRlist l <= x. +Lemma MinRlist_P1 : forall (l:list R) (x:R), In x l -> MinRlist l <= x. Proof. intros; induction l as [| r l Hrecl]. simpl in H; elim H. induction l as [| r0 l Hrecl0]. simpl in H; elim H; intro. - simpl; right; symmetry ; assumption. + simpl; right; assumption. elim H0. - replace (MinRlist (cons r (cons r0 l))) with (Rmin r (MinRlist (cons r0 l))). + replace (MinRlist (r :: r0 :: l)) with (Rmin r (MinRlist (r0 :: l))). simpl in H; decompose [or] H. rewrite H0; apply Rmin_l. - unfold Rmin; case (Rle_dec r (MinRlist (cons r0 l))); intro. - apply Rle_trans with (MinRlist (cons r0 l)). + unfold Rmin; case (Rle_dec r (MinRlist (r0 :: l))); intro. + apply Rle_trans with (MinRlist (r0 :: l)). assumption. apply Hrecl; simpl; tauto. apply Hrecl; simpl; tauto. - apply Rle_trans with (MinRlist (cons r0 l)). + apply Rle_trans with (MinRlist (r0 :: l)). apply Rmin_r. apply Hrecl; simpl; tauto. reflexivity. Qed. Lemma AbsList_P1 : - forall (l:Rlist) (x y:R), In y l -> In (Rabs (y - x) / 2) (AbsList l x). + forall (l:list R) (x y:R), In y l -> In (Rabs (y - x) / 2) (AbsList l x). Proof. intros; induction l as [| r l Hrecl]. elim H. @@ -109,21 +101,21 @@ Proof. Qed. Lemma MinRlist_P2 : - forall l:Rlist, (forall y:R, In y l -> 0 < y) -> 0 < MinRlist l. + forall l:list R, (forall y:R, In y l -> 0 < y) -> 0 < MinRlist l. Proof. intros; induction l as [| r l Hrecl]. apply Rlt_0_1. induction l as [| r0 l Hrecl0]. simpl; apply H; simpl; tauto. - replace (MinRlist (cons r (cons r0 l))) with (Rmin r (MinRlist (cons r0 l))). - unfold Rmin; case (Rle_dec r (MinRlist (cons r0 l))); intro. + replace (MinRlist (r :: r0 :: l)) with (Rmin r (MinRlist (r0 :: l))). + unfold Rmin; case (Rle_dec r (MinRlist (r0 :: l))); intro. apply H; simpl; tauto. apply Hrecl; intros; apply H; simpl; simpl in H0; tauto. reflexivity. Qed. Lemma AbsList_P2 : - forall (l:Rlist) (x y:R), + forall (l:list R) (x y:R), In y (AbsList l x) -> exists z : R, In z l /\ y = Rabs (z - x) / 2. Proof. intros; induction l as [| r l Hrecl]. @@ -131,47 +123,48 @@ Proof. elim H; intro. exists r; split. simpl; tauto. + symmetry. assumption. assert (H1 := Hrecl H0); elim H1; intros; elim H2; clear H2; intros; exists x0; simpl; simpl in H2; tauto. Qed. Lemma MaxRlist_P2 : - forall l:Rlist, (exists y : R, In y l) -> In (MaxRlist l) l. + forall l:list R, (exists y : R, In y l) -> In (MaxRlist l) l. Proof. intros; induction l as [| r l Hrecl]. simpl in H; elim H; trivial. induction l as [| r0 l Hrecl0]. simpl; left; reflexivity. - change (In (Rmax r (MaxRlist (cons r0 l))) (cons r (cons r0 l))); - unfold Rmax; case (Rle_dec r (MaxRlist (cons r0 l))); + change (In (Rmax r (MaxRlist (r0 :: l))) (r :: r0 :: l)); + unfold Rmax; case (Rle_dec r (MaxRlist (r0 :: l))); intro. right; apply Hrecl; exists r0; left; reflexivity. left; reflexivity. Qed. -Fixpoint pos_Rl (l:Rlist) (i:nat) : R := +Fixpoint pos_Rl (l:list R) (i:nat) : R := match l with | nil => 0 - | cons a l' => match i with + | a :: l' => match i with | O => a | S i' => pos_Rl l' i' end end. Lemma pos_Rl_P1 : - forall (l:Rlist) (a:R), - (0 < Rlength l)%nat -> - pos_Rl (cons a l) (Rlength l) = pos_Rl l (pred (Rlength l)). + forall (l:list R) (a:R), + (0 < length l)%nat -> + pos_Rl (a :: l) (length l) = pos_Rl l (pred (length l)). Proof. intros; induction l as [| r l Hrecl]; [ elim (lt_n_O _ H) - | simpl; case (Rlength l); [ reflexivity | intro; reflexivity ] ]. + | simpl; case (length l); [ reflexivity | intro; reflexivity ] ]. Qed. Lemma pos_Rl_P2 : - forall (l:Rlist) (x:R), - In x l <-> (exists i : nat, (i < Rlength l)%nat /\ x = pos_Rl l i). + forall (l:list R) (x:R), + In x l <-> (exists i : nat, (i < length l)%nat /\ x = pos_Rl l i). Proof. intros; induction l as [| r l Hrecl]. split; intro; @@ -179,12 +172,12 @@ Proof. split; intro. elim H; intro. exists 0%nat; split; - [ simpl; apply lt_O_Sn | simpl; apply H0 ]. + [ simpl; apply lt_O_Sn | simpl; symmetry; apply H0 ]. elim Hrecl; intros; assert (H3 := H1 H0); elim H3; intros; elim H4; intros; exists (S x0); split; [ simpl; apply lt_n_S; assumption | simpl; assumption ]. elim H; intros; elim H0; intros; destruct (zerop x0) as [->|]. - simpl in H2; left; assumption. + simpl in H2; left; symmetry; assumption. right; elim Hrecl; intros H4 H5; apply H5; assert (H6 : S (pred x0) = x0). symmetry ; apply S_pred with 0%nat; assumption. exists (pred x0); split; @@ -193,21 +186,21 @@ Proof. Qed. Lemma Rlist_P1 : - forall (l:Rlist) (P:R -> R -> Prop), + forall (l:list R) (P:R -> R -> Prop), (forall x:R, In x l -> exists y : R, P x y) -> - exists l' : Rlist, - Rlength l = Rlength l' /\ - (forall i:nat, (i < Rlength l)%nat -> P (pos_Rl l i) (pos_Rl l' i)). + exists l' : list R, + length l = length l' /\ + (forall i:nat, (i < length l)%nat -> P (pos_Rl l i) (pos_Rl l' i)). Proof. intros; induction l as [| r l Hrecl]. exists nil; intros; split; [ reflexivity | intros; simpl in H0; elim (lt_n_O _ H0) ]. - assert (H0 : In r (cons r l)). + assert (H0 : In r (r :: l)). simpl; left; reflexivity. assert (H1 := H _ H0); assert (H2 : forall x:R, In x l -> exists y : R, P x y). intros; apply H; simpl; right; assumption. - assert (H3 := Hrecl H2); elim H1; intros; elim H3; intros; exists (cons x x0); + assert (H3 := Hrecl H2); elim H1; intros; elim H3; intros; exists (x :: x0); intros; elim H5; clear H5; intros; split. simpl; rewrite H5; reflexivity. intros; destruct (zerop i) as [->|]. @@ -218,57 +211,45 @@ Proof. assumption. Qed. -Definition ordered_Rlist (l:Rlist) : Prop := - forall i:nat, (i < pred (Rlength l))%nat -> pos_Rl l i <= pos_Rl l (S i). +Definition ordered_Rlist (l:list R) : Prop := + forall i:nat, (i < pred (length l))%nat -> pos_Rl l i <= pos_Rl l (S i). -Fixpoint insert (l:Rlist) (x:R) : Rlist := +Fixpoint insert (l:list R) (x:R) : list R := match l with - | nil => cons x nil - | cons a l' => + | nil => x :: nil + | a :: l' => match Rle_dec a x with - | left _ => cons a (insert l' x) - | right _ => cons x l + | left _ => a :: (insert l' x) + | right _ => x :: l end end. -Fixpoint cons_Rlist (l k:Rlist) : Rlist := - match l with - | nil => k - | cons a l' => cons a (cons_Rlist l' k) - end. - -Fixpoint cons_ORlist (k l:Rlist) : Rlist := +Fixpoint cons_ORlist (k l:list R) : list R := match k with | nil => l - | cons a k' => cons_ORlist k' (insert l a) + | a :: k' => cons_ORlist k' (insert l a) end. -Fixpoint app_Rlist (l:Rlist) (f:R -> R) : Rlist := +Fixpoint mid_Rlist (l:list R) (x:R) : list R := match l with | nil => nil - | cons a l' => cons (f a) (app_Rlist l' f) + | a :: l' => ((x + a) / 2) :: (mid_Rlist l' a) end. -Fixpoint mid_Rlist (l:Rlist) (x:R) : Rlist := +Definition Rtail (l:list R) : list R := match l with | nil => nil - | cons a l' => cons ((x + a) / 2) (mid_Rlist l' a) + | a :: l' => l' end. -Definition Rtail (l:Rlist) : Rlist := +Definition FF (l:list R) (f:R -> R) : list R := match l with | nil => nil - | cons a l' => l' - end. - -Definition FF (l:Rlist) (f:R -> R) : Rlist := - match l with - | nil => nil - | cons a l' => app_Rlist (mid_Rlist l' a) f + | a :: l' => map f (mid_Rlist l' a) end. Lemma RList_P0 : - forall (l:Rlist) (a:R), + forall (l:list R) (a:R), pos_Rl (insert l a) 0 = a \/ pos_Rl (insert l a) 0 = pos_Rl l 0. Proof. intros; induction l as [| r l Hrecl]; @@ -278,7 +259,7 @@ Proof. Qed. Lemma RList_P1 : - forall (l:Rlist) (a:R), ordered_Rlist l -> ordered_Rlist (insert l a). + forall (l:list R) (a:R), ordered_Rlist l -> ordered_Rlist (insert l a). Proof. intros; induction l as [| r l Hrecl]. simpl; unfold ordered_Rlist; intros; simpl in H0; @@ -286,8 +267,8 @@ Proof. simpl; case (Rle_dec r a); intro. assert (H1 : ordered_Rlist l). unfold ordered_Rlist; unfold ordered_Rlist in H; intros; - assert (H1 : (S i < pred (Rlength (cons r l)))%nat); - [ simpl; replace (Rlength l) with (S (pred (Rlength l))); + assert (H1 : (S i < pred (length (r :: l)))%nat); + [ simpl; replace (length l) with (S (pred (length l))); [ apply lt_n_S; assumption | symmetry ; apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H1 in H0; simpl in H0; elim (lt_n_O _ H0) ] @@ -300,18 +281,18 @@ Proof. [ simpl; assumption | rewrite H4; apply (H 0%nat); simpl; apply lt_O_Sn ]. simpl; apply H2; simpl in H0; apply lt_S_n; - replace (S (pred (Rlength (insert l a)))) with (Rlength (insert l a)); + replace (S (pred (length (insert l a)))) with (length (insert l a)); [ assumption | apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H3 in H0; elim (lt_n_O _ H0) ]. unfold ordered_Rlist; intros; induction i as [| i Hreci]; [ simpl; auto with real - | change (pos_Rl (cons r l) i <= pos_Rl (cons r l) (S i)); apply H; + | change (pos_Rl (r :: l) i <= pos_Rl (r :: l) (S i)); apply H; simpl in H0; simpl; apply (lt_S_n _ _ H0) ]. Qed. Lemma RList_P2 : - forall l1 l2:Rlist, ordered_Rlist l2 -> ordered_Rlist (cons_ORlist l1 l2). + forall l1 l2:list R, ordered_Rlist l2 -> ordered_Rlist (cons_ORlist l1 l2). Proof. simple induction l1; [ intros; simpl; apply H @@ -319,36 +300,36 @@ Proof. Qed. Lemma RList_P3 : - forall (l:Rlist) (x:R), - In x l <-> (exists i : nat, x = pos_Rl l i /\ (i < Rlength l)%nat). + forall (l:list R) (x:R), + In x l <-> (exists i : nat, x = pos_Rl l i /\ (i < length l)%nat). Proof. intros; split; intro; [ induction l as [| r l Hrecl] | induction l as [| r l Hrecl] ]. elim H. elim H; intro; - [ exists 0%nat; split; [ apply H0 | simpl; apply lt_O_Sn ] + [ exists 0%nat; split; [ symmetry; apply H0 | simpl; apply lt_O_Sn ] | elim (Hrecl H0); intros; elim H1; clear H1; intros; exists (S x0); split; [ apply H1 | simpl; apply lt_n_S; assumption ] ]. elim H; intros; elim H0; intros; elim (lt_n_O _ H2). simpl; elim H; intros; elim H0; clear H0; intros; induction x0 as [| x0 Hrecx0]; - [ left; apply H0 + [ left; symmetry; apply H0 | right; apply Hrecl; exists x0; split; [ apply H0 | simpl in H1; apply lt_S_n; assumption ] ]. Qed. Lemma RList_P4 : - forall (l1:Rlist) (a:R), ordered_Rlist (cons a l1) -> ordered_Rlist l1. + forall (l1:list R) (a:R), ordered_Rlist (a :: l1) -> ordered_Rlist l1. Proof. intros; unfold ordered_Rlist; intros; apply (H (S i)); simpl; - replace (Rlength l1) with (S (pred (Rlength l1))); + replace (length l1) with (S (pred (length l1))); [ apply lt_n_S; assumption | symmetry ; apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H1 in H0; elim (lt_n_O _ H0) ]. Qed. Lemma RList_P5 : - forall (l:Rlist) (x:R), ordered_Rlist l -> In x l -> pos_Rl l 0 <= x. + forall (l:list R) (x:R), ordered_Rlist l -> In x l -> pos_Rl l 0 <= x. Proof. intros; induction l as [| r l Hrecl]; [ elim H0 @@ -361,14 +342,14 @@ Proof. Qed. Lemma RList_P6 : - forall l:Rlist, + forall l:list R, ordered_Rlist l <-> (forall i j:nat, - (i <= j)%nat -> (j < Rlength l)%nat -> pos_Rl l i <= pos_Rl l j). + (i <= j)%nat -> (j < length l)%nat -> pos_Rl l i <= pos_Rl l j). Proof. - simple induction l; split; intro. + induction l as [ | r r0 H]; split; intro. intros; right; reflexivity. - unfold ordered_Rlist; intros; simpl in H0; elim (lt_n_O _ H0). + unfold ordered_Rlist;intros; simpl in H0; elim (lt_n_O _ H0). intros; induction i as [| i Hreci]; [ induction j as [| j Hrecj]; [ right; reflexivity @@ -391,14 +372,14 @@ Proof. Qed. Lemma RList_P7 : - forall (l:Rlist) (x:R), - ordered_Rlist l -> In x l -> x <= pos_Rl l (pred (Rlength l)). + forall (l:list R) (x:R), + ordered_Rlist l -> In x l -> x <= pos_Rl l (pred (length l)). Proof. intros; assert (H1 := RList_P6 l); elim H1; intros H2 _; assert (H3 := H2 H); clear H1 H2; assert (H1 := RList_P3 l x); elim H1; clear H1; intros; assert (H4 := H1 H0); elim H4; clear H4; intros; elim H4; clear H4; intros; rewrite H4; - assert (H6 : Rlength l = S (pred (Rlength l))). + assert (H6 : length l = S (pred (length l))). apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H6 in H5; elim (lt_n_O _ H5). apply H3; @@ -408,52 +389,55 @@ Proof. Qed. Lemma RList_P8 : - forall (l:Rlist) (a x:R), In x (insert l a) <-> x = a \/ In x l. -Proof. - simple induction l. - intros; split; intro; simpl in H; apply H. - intros; split; intro; - [ simpl in H0; generalize H0; case (Rle_dec r a); intros; - [ simpl in H1; elim H1; intro; - [ right; left; assumption - | elim (H a x); intros; elim (H3 H2); intro; - [ left; assumption | right; right; assumption ] ] - | simpl in H1; decompose [or] H1; - [ left; assumption - | right; left; assumption - | right; right; assumption ] ] - | simpl; case (Rle_dec r a); intro; - [ simpl in H0; decompose [or] H0; - [ right; elim (H a x); intros; apply H3; left - | left - | right; elim (H a x); intros; apply H3; right ] - | simpl in H0; decompose [or] H0; [ left | right; left | right; right ] ]; - assumption ]. + forall (l:list R) (a x:R), In x (insert l a) <-> x = a \/ In x l. +Proof. + induction l as [ | r r0 H]. + intros; split; intro; destruct H as [ax | []]; left; symmetry; exact ax. + intros; split; intro. + simpl in H0; generalize H0; case (Rle_dec r a); intros. + simpl in H1; elim H1; intro. + right; left; assumption. + elim (H a x); intros; elim (H3 H2); intro. + left; assumption. + right; right; assumption. + simpl in H1; decompose [or] H1. + left; symmetry; assumption. + right; left; assumption. + right; right; assumption. + simpl; case (Rle_dec r a); intro. + simpl in H0; decompose [or] H0. + right; elim (H a x); intros; apply H3; left. assumption. + left. assumption. + right; elim (H a x); intros; apply H3; right; assumption. + simpl in H0; decompose [or] H0; [ left | right; left | right; right]; + trivial; symmetry; assumption. Qed. Lemma RList_P9 : - forall (l1 l2:Rlist) (x:R), In x (cons_ORlist l1 l2) <-> In x l1 \/ In x l2. + forall (l1 l2:list R) (x:R), In x (cons_ORlist l1 l2) <-> In x l1 \/ In x l2. Proof. - simple induction l1. + induction l1 as [ | r r0 H]. intros; split; intro; [ simpl in H; right; assumption | simpl; elim H; intro; [ elim H0 | assumption ] ]. intros; split. simpl; intros; elim (H (insert l2 r) x); intros; assert (H3 := H1 H0); - elim H3; intro; - [ left; right; assumption - | elim (RList_P8 l2 r x); intros H5 _; assert (H6 := H5 H4); elim H6; intro; - [ left; left; assumption | right; assumption ] ]. + elim H3; intro. + left; right; assumption. + elim (RList_P8 l2 r x); intros H5 _; assert (H6 := H5 H4); elim H6; intro. + left; left; symmetry; assumption. + right; assumption. intro; simpl; elim (H (insert l2 r) x); intros _ H1; apply H1; - elim H0; intro; - [ elim H2; intro; - [ right; elim (RList_P8 l2 r x); intros _ H4; apply H4; left; assumption - | left; assumption ] - | right; elim (RList_P8 l2 r x); intros _ H3; apply H3; right; assumption ]. + elim H0; intro. + elim H2; intro. + right; elim (RList_P8 l2 r x); intros _ H4; apply H4; left. + symmetry; assumption. + left; assumption. + right; elim (RList_P8 l2 r x); intros _ H3; apply H3; right; assumption. Qed. Lemma RList_P10 : - forall (l:Rlist) (a:R), Rlength (insert l a) = S (Rlength l). + forall (l:list R) (a:R), length (insert l a) = S (length l). Proof. intros; induction l as [| r l Hrecl]; [ reflexivity @@ -462,10 +446,10 @@ Proof. Qed. Lemma RList_P11 : - forall l1 l2:Rlist, - Rlength (cons_ORlist l1 l2) = (Rlength l1 + Rlength l2)%nat. + forall l1 l2:list R, + length (cons_ORlist l1 l2) = (length l1 + length l2)%nat. Proof. - simple induction l1; + induction l1 as [ | r r0 H]; [ intro; reflexivity | intros; simpl; rewrite (H (insert l2 r)); rewrite RList_P10; apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR; @@ -473,8 +457,8 @@ Proof. Qed. Lemma RList_P12 : - forall (l:Rlist) (i:nat) (f:R -> R), - (i < Rlength l)%nat -> pos_Rl (app_Rlist l f) i = f (pos_Rl l i). + forall (l:list R) (i:nat) (f:R -> R), + (i < length l)%nat -> pos_Rl (map f l) i = f (pos_Rl l i). Proof. simple induction l; [ intros; elim (lt_n_O _ H) @@ -483,30 +467,30 @@ Proof. Qed. Lemma RList_P13 : - forall (l:Rlist) (i:nat) (a:R), - (i < pred (Rlength l))%nat -> + forall (l:list R) (i:nat) (a:R), + (i < pred (length l))%nat -> pos_Rl (mid_Rlist l a) (S i) = (pos_Rl l i + pos_Rl l (S i)) / 2. Proof. - simple induction l. + induction l as [ | r r0 H]. intros; simpl in H; elim (lt_n_O _ H). - simple induction r0. + induction r0 as [ | r1 r2 H0]. intros; simpl in H0; elim (lt_n_O _ H0). intros; simpl in H1; induction i as [| i Hreci]. reflexivity. change - (pos_Rl (mid_Rlist (cons r1 r2) r) (S i) = - (pos_Rl (cons r1 r2) i + pos_Rl (cons r1 r2) (S i)) / 2) - ; apply H0; simpl; apply lt_S_n; assumption. + (pos_Rl (mid_Rlist (r1 :: r2) r) (S i) = + (pos_Rl (r1 :: r2) i + pos_Rl (r1 :: r2) (S i)) / 2). + apply H; simpl; apply lt_S_n; assumption. Qed. -Lemma RList_P14 : forall (l:Rlist) (a:R), Rlength (mid_Rlist l a) = Rlength l. +Lemma RList_P14 : forall (l:list R) (a:R), length (mid_Rlist l a) = length l. Proof. - simple induction l; intros; + induction l as [ | r r0 H]; intros; [ reflexivity | simpl; rewrite (H r); reflexivity ]. Qed. Lemma RList_P15 : - forall l1 l2:Rlist, + forall l1 l2:list R, ordered_Rlist l1 -> ordered_Rlist l2 -> pos_Rl l1 0 = pos_Rl l2 0 -> pos_Rl (cons_ORlist l1 l2) 0 = pos_Rl l1 0. @@ -514,10 +498,10 @@ Proof. intros; apply Rle_antisym. induction l1 as [| r l1 Hrecl1]; [ simpl; simpl in H1; right; symmetry ; assumption - | elim (RList_P9 (cons r l1) l2 (pos_Rl (cons r l1) 0)); intros; + | elim (RList_P9 (r :: l1) l2 (pos_Rl (r :: l1) 0)); intros; assert (H4 : - In (pos_Rl (cons r l1) 0) (cons r l1) \/ In (pos_Rl (cons r l1) 0) l2); + In (pos_Rl (r :: l1) 0) (r :: l1) \/ In (pos_Rl (r :: l1) 0) l2); [ left; left; reflexivity | assert (H5 := H3 H4); apply RList_P5; [ apply RList_P2; assumption | assumption ] ] ]. @@ -525,25 +509,25 @@ Proof. [ simpl; simpl in H1; right; assumption | assert (H2 : - In (pos_Rl (cons_ORlist (cons r l1) l2) 0) (cons_ORlist (cons r l1) l2)); + In (pos_Rl (cons_ORlist (r :: l1) l2) 0) (cons_ORlist (r :: l1) l2)); [ elim - (RList_P3 (cons_ORlist (cons r l1) l2) - (pos_Rl (cons_ORlist (cons r l1) l2) 0)); + (RList_P3 (cons_ORlist (r :: l1) l2) + (pos_Rl (cons_ORlist (r :: l1) l2) 0)); intros; apply H3; exists 0%nat; split; [ reflexivity | rewrite RList_P11; simpl; apply lt_O_Sn ] - | elim (RList_P9 (cons r l1) l2 (pos_Rl (cons_ORlist (cons r l1) l2) 0)); + | elim (RList_P9 (r :: l1) l2 (pos_Rl (cons_ORlist (r :: l1) l2) 0)); intros; assert (H5 := H3 H2); elim H5; intro; [ apply RList_P5; assumption | rewrite H1; apply RList_P5; assumption ] ] ]. Qed. Lemma RList_P16 : - forall l1 l2:Rlist, + forall l1 l2:list R, ordered_Rlist l1 -> ordered_Rlist l2 -> - pos_Rl l1 (pred (Rlength l1)) = pos_Rl l2 (pred (Rlength l2)) -> - pos_Rl (cons_ORlist l1 l2) (pred (Rlength (cons_ORlist l1 l2))) = - pos_Rl l1 (pred (Rlength l1)). + pos_Rl l1 (pred (length l1)) = pos_Rl l2 (pred (length l2)) -> + pos_Rl (cons_ORlist l1 l2) (pred (length (cons_ORlist l1 l2))) = + pos_Rl l1 (pred (length l1)). Proof. intros; apply Rle_antisym. induction l1 as [| r l1 Hrecl1]. @@ -551,99 +535,99 @@ Proof. assert (H2 : In - (pos_Rl (cons_ORlist (cons r l1) l2) - (pred (Rlength (cons_ORlist (cons r l1) l2)))) - (cons_ORlist (cons r l1) l2)); + (pos_Rl (cons_ORlist (r :: l1) l2) + (pred (length (cons_ORlist (r :: l1) l2)))) + (cons_ORlist (r :: l1) l2)); [ elim - (RList_P3 (cons_ORlist (cons r l1) l2) - (pos_Rl (cons_ORlist (cons r l1) l2) - (pred (Rlength (cons_ORlist (cons r l1) l2))))); - intros; apply H3; exists (pred (Rlength (cons_ORlist (cons r l1) l2))); + (RList_P3 (cons_ORlist (r :: l1) l2) + (pos_Rl (cons_ORlist (r :: l1) l2) + (pred (length (cons_ORlist (r :: l1) l2))))); + intros; apply H3; exists (pred (length (cons_ORlist (r :: l1) l2))); split; [ reflexivity | rewrite RList_P11; simpl; apply lt_n_Sn ] | elim - (RList_P9 (cons r l1) l2 - (pos_Rl (cons_ORlist (cons r l1) l2) - (pred (Rlength (cons_ORlist (cons r l1) l2))))); + (RList_P9 (r :: l1) l2 + (pos_Rl (cons_ORlist (r :: l1) l2) + (pred (length (cons_ORlist (r :: l1) l2))))); intros; assert (H5 := H3 H2); elim H5; intro; [ apply RList_P7; assumption | rewrite H1; apply RList_P7; assumption ] ]. induction l1 as [| r l1 Hrecl1]. simpl; simpl in H1; right; assumption. elim - (RList_P9 (cons r l1) l2 (pos_Rl (cons r l1) (pred (Rlength (cons r l1))))); + (RList_P9 (r :: l1) l2 (pos_Rl (r :: l1) (pred (length (r :: l1))))). intros; assert (H4 : - In (pos_Rl (cons r l1) (pred (Rlength (cons r l1)))) (cons r l1) \/ - In (pos_Rl (cons r l1) (pred (Rlength (cons r l1)))) l2); - [ left; change (In (pos_Rl (cons r l1) (Rlength l1)) (cons r l1)); - elim (RList_P3 (cons r l1) (pos_Rl (cons r l1) (Rlength l1))); - intros; apply H5; exists (Rlength l1); split; + In (pos_Rl (r :: l1) (pred (length (r :: l1)))) (r :: l1) \/ + In (pos_Rl (r :: l1) (pred (length (r :: l1)))) l2); + [ left; change (In (pos_Rl (r :: l1) (length l1)) (r :: l1)); + elim (RList_P3 (r :: l1) (pos_Rl (r :: l1) (length l1))); + intros; apply H5; exists (length l1); split; [ reflexivity | simpl; apply lt_n_Sn ] | assert (H5 := H3 H4); apply RList_P7; [ apply RList_P2; assumption | elim - (RList_P9 (cons r l1) l2 - (pos_Rl (cons r l1) (pred (Rlength (cons r l1))))); + (RList_P9 (r :: l1) l2 + (pos_Rl (r :: l1) (pred (length (r :: l1))))); intros; apply H7; left; elim - (RList_P3 (cons r l1) - (pos_Rl (cons r l1) (pred (Rlength (cons r l1))))); - intros; apply H9; exists (pred (Rlength (cons r l1))); + (RList_P3 (r :: l1) + (pos_Rl (r :: l1) (pred (length (r :: l1))))); + intros; apply H9; exists (pred (length (r :: l1))); split; [ reflexivity | simpl; apply lt_n_Sn ] ] ]. Qed. Lemma RList_P17 : - forall (l1:Rlist) (x:R) (i:nat), + forall (l1:list R) (x:R) (i:nat), ordered_Rlist l1 -> In x l1 -> - pos_Rl l1 i < x -> (i < pred (Rlength l1))%nat -> pos_Rl l1 (S i) <= x. + pos_Rl l1 i < x -> (i < pred (length l1))%nat -> pos_Rl l1 (S i) <= x. Proof. - simple induction l1. + induction l1 as [ | r r0 H]. intros; elim H0. intros; induction i as [| i Hreci]. simpl; elim H1; intro; [ simpl in H2; rewrite H4 in H2; elim (Rlt_irrefl _ H2) | apply RList_P5; [ apply RList_P4 with r; assumption | assumption ] ]. simpl; simpl in H2; elim H1; intro. - rewrite H4 in H2; assert (H5 : r <= pos_Rl r0 i); + rewrite <- H4 in H2; assert (H5 : r <= pos_Rl r0 i); [ apply Rle_trans with (pos_Rl r0 0); [ apply (H0 0%nat); simpl; simpl in H3; apply neq_O_lt; red; intro; rewrite <- H5 in H3; elim (lt_n_O _ H3) | elim (RList_P6 r0); intros; apply H5; [ apply RList_P4 with r; assumption | apply le_O_n - | simpl in H3; apply lt_S_n; apply lt_trans with (Rlength r0); + | simpl in H3; apply lt_S_n; apply lt_trans with (length r0); [ apply H3 | apply lt_n_Sn ] ] ] | elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H5 H2)) ]. apply H; try assumption; [ apply RList_P4 with r; assumption | simpl in H3; apply lt_S_n; - replace (S (pred (Rlength r0))) with (Rlength r0); + replace (S (pred (length r0))) with (length r0); [ apply H3 | apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H5 in H3; elim (lt_n_O _ H3) ] ]. Qed. Lemma RList_P18 : - forall (l:Rlist) (f:R -> R), Rlength (app_Rlist l f) = Rlength l. + forall (l:list R) (f:R -> R), length (map f l) = length l. Proof. simple induction l; intros; [ reflexivity | simpl; rewrite H; reflexivity ]. Qed. Lemma RList_P19 : - forall l:Rlist, - l <> nil -> exists r : R, (exists r0 : Rlist, l = cons r r0). + forall l:list R, + l <> nil -> exists r : R, (exists r0 : list R, l = r :: r0). Proof. intros; induction l as [| r l Hrecl]; [ elim H; reflexivity | exists r; exists l; reflexivity ]. Qed. Lemma RList_P20 : - forall l:Rlist, - (2 <= Rlength l)%nat -> + forall l:list R, + (2 <= length l)%nat -> exists r : R, - (exists r1 : R, (exists l' : Rlist, l = cons r (cons r1 l'))). + (exists r1 : R, (exists l' : list R, l = r :: r1 :: l')). Proof. intros; induction l as [| r l Hrecl]; [ simpl in H; elim (le_Sn_O _ H) @@ -652,40 +636,32 @@ Proof. | exists r; exists r0; exists l; reflexivity ] ]. Qed. -Lemma RList_P21 : forall l l':Rlist, l = l' -> Rtail l = Rtail l'. +Lemma RList_P21 : forall l l':list R, l = l' -> Rtail l = Rtail l'. Proof. intros; rewrite H; reflexivity. Qed. Lemma RList_P22 : - forall l1 l2:Rlist, l1 <> nil -> pos_Rl (cons_Rlist l1 l2) 0 = pos_Rl l1 0. + forall l1 l2:list R, l1 <> nil -> pos_Rl (app l1 l2) 0 = pos_Rl l1 0. Proof. simple induction l1; [ intros; elim H; reflexivity | intros; reflexivity ]. Qed. -Lemma RList_P23 : - forall l1 l2:Rlist, - Rlength (cons_Rlist l1 l2) = (Rlength l1 + Rlength l2)%nat. -Proof. - simple induction l1; - [ intro; reflexivity | intros; simpl; rewrite H; reflexivity ]. -Qed. - Lemma RList_P24 : - forall l1 l2:Rlist, + forall l1 l2:list R, l2 <> nil -> - pos_Rl (cons_Rlist l1 l2) (pred (Rlength (cons_Rlist l1 l2))) = - pos_Rl l2 (pred (Rlength l2)). + pos_Rl (app l1 l2) (pred (length (app l1 l2))) = + pos_Rl l2 (pred (length l2)). Proof. - simple induction l1. + induction l1 as [ | r r0 H]. intros; reflexivity. intros; rewrite <- (H l2 H0); induction l2 as [| r1 l2 Hrecl2]. elim H0; reflexivity. - do 2 rewrite RList_P23; - replace (Rlength (cons r r0) + Rlength (cons r1 l2))%nat with - (S (S (Rlength r0 + Rlength l2))); - [ replace (Rlength r0 + Rlength (cons r1 l2))%nat with - (S (Rlength r0 + Rlength l2)); + do 2 rewrite app_length; + replace (length (r :: r0) + length (r1 :: l2))%nat with + (S (S (length r0 + length l2))); + [ replace (length r0 + length (r1 :: l2))%nat with + (S (length r0 + length l2)); [ reflexivity | simpl; apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR; rewrite S_INR; ring ] @@ -694,39 +670,39 @@ Proof. Qed. Lemma RList_P25 : - forall l1 l2:Rlist, + forall l1 l2:list R, ordered_Rlist l1 -> ordered_Rlist l2 -> - pos_Rl l1 (pred (Rlength l1)) <= pos_Rl l2 0 -> - ordered_Rlist (cons_Rlist l1 l2). + pos_Rl l1 (pred (length l1)) <= pos_Rl l2 0 -> + ordered_Rlist (app l1 l2). Proof. - simple induction l1. + induction l1 as [ | r r0 H]. intros; simpl; assumption. - simple induction r0. + induction r0 as [ | r1 r2 H0]. intros; simpl; simpl in H2; unfold ordered_Rlist; intros; simpl in H3. induction i as [| i Hreci]. simpl; assumption. change (pos_Rl l2 i <= pos_Rl l2 (S i)); apply (H1 i); apply lt_S_n; - replace (S (pred (Rlength l2))) with (Rlength l2); + replace (S (pred (length l2))) with (length l2); [ assumption | apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H4 in H3; elim (lt_n_O _ H3) ]. - intros; clear H; assert (H : ordered_Rlist (cons_Rlist (cons r1 r2) l2)). - apply H0; try assumption. + intros; assert (H4 : ordered_Rlist (app (r1 :: r2) l2)). + apply H; try assumption. apply RList_P4 with r; assumption. - unfold ordered_Rlist; intros; simpl in H4; + unfold ordered_Rlist; intros i H5; simpl in H5. induction i as [| i Hreci]. simpl; apply (H1 0%nat); simpl; apply lt_O_Sn. change - (pos_Rl (cons_Rlist (cons r1 r2) l2) i <= - pos_Rl (cons_Rlist (cons r1 r2) l2) (S i)); - apply (H i); simpl; apply lt_S_n; assumption. + (pos_Rl (app (r1 :: r2) l2) i <= + pos_Rl (app (r1 :: r2) l2) (S i)); + apply (H4 i); simpl; apply lt_S_n; assumption. Qed. Lemma RList_P26 : - forall (l1 l2:Rlist) (i:nat), - (i < Rlength l1)%nat -> pos_Rl (cons_Rlist l1 l2) i = pos_Rl l1 i. + forall (l1 l2:list R) (i:nat), + (i < length l1)%nat -> pos_Rl (app l1 l2) i = pos_Rl l1 i. Proof. simple induction l1. intros; elim (lt_n_O _ H). @@ -735,49 +711,41 @@ Proof. apply (H l2 i); simpl in H0; apply lt_S_n; assumption. Qed. -Lemma RList_P27 : - forall l1 l2 l3:Rlist, - cons_Rlist l1 (cons_Rlist l2 l3) = cons_Rlist (cons_Rlist l1 l2) l3. -Proof. - simple induction l1; intros; - [ reflexivity | simpl; rewrite (H l2 l3); reflexivity ]. -Qed. - -Lemma RList_P28 : forall l:Rlist, cons_Rlist l nil = l. -Proof. - simple induction l; - [ reflexivity | intros; simpl; rewrite H; reflexivity ]. -Qed. - Lemma RList_P29 : - forall (l2 l1:Rlist) (i:nat), - (Rlength l1 <= i)%nat -> - (i < Rlength (cons_Rlist l1 l2))%nat -> - pos_Rl (cons_Rlist l1 l2) i = pos_Rl l2 (i - Rlength l1). + forall (l2 l1:list R) (i:nat), + (length l1 <= i)%nat -> + (i < length (app l1 l2))%nat -> + pos_Rl (app l1 l2) i = pos_Rl l2 (i - length l1). Proof. - simple induction l2. - intros; rewrite RList_P28 in H0; elim (lt_irrefl _ (le_lt_trans _ _ _ H H0)). + induction l2 as [ | r r0 H]. + intros; rewrite app_nil_r in H0; elim (lt_irrefl _ (le_lt_trans _ _ _ H H0)). intros; - replace (cons_Rlist l1 (cons r r0)) with - (cons_Rlist (cons_Rlist l1 (cons r nil)) r0). + replace (app l1 (r :: r0)) with + (app (app l1 (r :: nil)) r0). inversion H0. rewrite <- minus_n_n; simpl; rewrite RList_P26. - clear l2 r0 H i H0 H1 H2; induction l1 as [| r0 l1 Hrecl1]. + clear r0 H i H0 H1 H2; induction l1 as [| r0 l1 Hrecl1]. reflexivity. simpl; assumption. - rewrite RList_P23; rewrite plus_comm; simpl; apply lt_n_Sn. - replace (S m - Rlength l1)%nat with (S (S m - S (Rlength l1))). + rewrite app_length; rewrite plus_comm; simpl; apply lt_n_Sn. + replace (S m - length l1)%nat with (S (S m - S (length l1))). rewrite H3; simpl; - replace (S (Rlength l1)) with (Rlength (cons_Rlist l1 (cons r nil))). - apply (H (cons_Rlist l1 (cons r nil)) i). - rewrite RList_P23; rewrite plus_comm; simpl; rewrite <- H3; + replace (S (length l1)) with (length (app l1 (r :: nil))). + apply (H (app l1 (r :: nil)) i). + rewrite app_length; rewrite plus_comm; simpl; rewrite <- H3; apply le_n_S; assumption. - repeat rewrite RList_P23; simpl; rewrite RList_P23 in H1; - rewrite plus_comm in H1; simpl in H1; rewrite (plus_comm (Rlength l1)); + repeat rewrite app_length; simpl; rewrite app_length in H1; + rewrite plus_comm in H1; simpl in H1; rewrite (plus_comm (length l1)); simpl; rewrite plus_comm; apply H1. - rewrite RList_P23; rewrite plus_comm; reflexivity. - change (S (m - Rlength l1) = (S m - Rlength l1)%nat); + rewrite app_length; rewrite plus_comm; reflexivity. + change (S (m - length l1) = (S m - length l1)%nat); apply minus_Sn_m; assumption. - replace (cons r r0) with (cons_Rlist (cons r nil) r0); - [ symmetry ; apply RList_P27 | reflexivity ]. + replace (r :: r0) with (app (r :: nil) r0); + [ symmetry ; apply app_assoc | reflexivity ]. Qed. + +#[deprecated(since="8.12",note="use List.cons instead")] +Notation cons := List.cons. + +#[deprecated(since="8.12",note="use List.nil instead")] +Notation nil := List.nil. diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index 0337b12cad..23094c6b93 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -464,7 +464,7 @@ Proof. elim (Rlt_irrefl _ H7) ] ]. Qed. -Fixpoint SubEquiN (N:nat) (x y:R) (del:posreal) : Rlist := +Fixpoint SubEquiN (N:nat) (x y:R) (del:posreal) : list R := match N with | O => cons y nil | S p => cons x (SubEquiN p (x + del) y del) @@ -473,7 +473,7 @@ Fixpoint SubEquiN (N:nat) (x y:R) (del:posreal) : Rlist := Definition max_N (a b:R) (del:posreal) (h:a < b) : nat := let (N,_) := maxN del h in N. -Definition SubEqui (a b:R) (del:posreal) (h:a < b) : Rlist := +Definition SubEqui (a b:R) (del:posreal) (h:a < b) : list R := SubEquiN (S (max_N del h)) a b del. Lemma Heine_cor1 : @@ -566,25 +566,25 @@ Qed. Lemma SubEqui_P2 : forall (a b:R) (del:posreal) (h:a < b), - pos_Rl (SubEqui del h) (pred (Rlength (SubEqui del h))) = b. + pos_Rl (SubEqui del h) (pred (length (SubEqui del h))) = b. Proof. intros; unfold SubEqui; destruct (maxN del h)as (x,_). cut (forall (x:nat) (a:R) (del:posreal), pos_Rl (SubEquiN (S x) a b del) - (pred (Rlength (SubEquiN (S x) a b del))) = b); + (pred (length (SubEquiN (S x) a b del))) = b); [ intro; apply H | simple induction x0; [ intros; reflexivity | intros; change (pos_Rl (SubEquiN (S n) (a0 + del0) b del0) - (pred (Rlength (SubEquiN (S n) (a0 + del0) b del0))) = b) + (pred (length (SubEquiN (S n) (a0 + del0) b del0))) = b) ; apply H ] ]. Qed. Lemma SubEqui_P3 : - forall (N:nat) (a b:R) (del:posreal), Rlength (SubEquiN N a b del) = S N. + forall (N:nat) (a b:R) (del:posreal), length (SubEquiN N a b del) = S N. Proof. simple induction N; intros; [ reflexivity | simpl; rewrite H; reflexivity ]. @@ -605,7 +605,7 @@ Qed. Lemma SubEqui_P5 : forall (a b:R) (del:posreal) (h:a < b), - Rlength (SubEqui del h) = S (S (max_N del h)). + length (SubEqui del h) = S (S (max_N del h)). Proof. intros; unfold SubEqui; apply SubEqui_P3. Qed. @@ -623,7 +623,7 @@ Proof. intros; unfold ordered_Rlist; intros; rewrite SubEqui_P5 in H; simpl in H; inversion H. rewrite (SubEqui_P6 del h (i:=(max_N del h))). - replace (S (max_N del h)) with (pred (Rlength (SubEqui del h))). + replace (S (max_N del h)) with (pred (length (SubEqui del h))). rewrite SubEqui_P2; unfold max_N; case (maxN del h) as (?&?&?); left; assumption. rewrite SubEqui_P5; reflexivity. @@ -639,7 +639,7 @@ Qed. Lemma SubEqui_P8 : forall (a b:R) (del:posreal) (h:a < b) (i:nat), - (i < Rlength (SubEqui del h))%nat -> a <= pos_Rl (SubEqui del h) i <= b. + (i < length (SubEqui del h))%nat -> a <= pos_Rl (SubEqui del h) i <= b. Proof. intros; split. pattern a at 1; rewrite <- (SubEqui_P1 del h); apply RList_P5. @@ -657,7 +657,7 @@ Lemma SubEqui_P9 : { g:StepFun a b | g b = f b /\ (forall i:nat, - (i < pred (Rlength (SubEqui del h)))%nat -> + (i < pred (length (SubEqui del h)))%nat -> constant_D_eq g (co_interval (pos_Rl (SubEqui del h) i) (pos_Rl (SubEqui del h) (S i))) @@ -713,7 +713,7 @@ Proof. a <= t <= b -> t = b \/ (exists i : nat, - (i < pred (Rlength (SubEqui del H)))%nat /\ + (i < pred (length (SubEqui del H)))%nat /\ co_interval (pos_Rl (SubEqui del H) i) (pos_Rl (SubEqui del H) (S i)) t)). intro; elim (H8 _ H7); intro. @@ -722,7 +722,7 @@ Proof. elim H9; clear H9; intros I [H9 H10]; assert (H11 := H6 I H9 t H10); rewrite H11; left; apply H4. assumption. - apply SubEqui_P8; apply lt_trans with (pred (Rlength (SubEqui del H))). + apply SubEqui_P8; apply lt_trans with (pred (length (SubEqui del H))). assumption. apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H12 in H9; elim (lt_n_O _ H9). @@ -734,7 +734,7 @@ Proof. (t - pos_Rl (SubEqui del H) (max_N del H))) with t; [ idtac | ring ]; apply Rlt_le_trans with b. rewrite H14 in H12; - assert (H13 : S (max_N del H) = pred (Rlength (SubEqui del H))). + assert (H13 : S (max_N del H) = pred (length (SubEqui del H))). rewrite SubEqui_P5; reflexivity. rewrite H13 in H12; rewrite SubEqui_P2 in H12; apply H12. rewrite SubEqui_P6. @@ -785,7 +785,7 @@ Proof. apply H5. assumption. inversion H7. - replace (S (max_N del H)) with (pred (Rlength (SubEqui del H))). + replace (S (max_N del H)) with (pred (length (SubEqui del H))). rewrite (SubEqui_P2 del H); elim H8; intros. elim H11; intro. assumption. @@ -1753,7 +1753,7 @@ Proof. rewrite <- H5; elim (RList_P6 l); intros; apply H10. assumption. apply le_O_n. - apply lt_trans with (pred (Rlength l)); [ assumption | apply lt_pred_n_n ]. + apply lt_trans with (pred (length l)); [ assumption | apply lt_pred_n_n ]. apply neq_O_lt; intro; rewrite <- H12 in H6; discriminate. unfold Rmin; decide (Rle_dec a b) with H; reflexivity. assert (H11 : pos_Rl l (S i) <= b). @@ -1960,7 +1960,7 @@ Proof. replace b with (Rmin b c). rewrite <- H5; elim (RList_P6 l1); intros; apply H10; try assumption. apply le_O_n. - apply lt_trans with (pred (Rlength l1)); try assumption; apply lt_pred_n_n; + apply lt_trans with (pred (length l1)); try assumption; apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H12 in H6; discriminate. unfold Rmin; decide (Rle_dec b c) with Hyp2; @@ -1991,7 +1991,7 @@ Proof. replace a with (Rmin a b). rewrite <- H5; elim (RList_P6 l1); intros; apply H11; try assumption. apply le_O_n. - apply lt_trans with (pred (Rlength l1)); try assumption; apply lt_pred_n_n; + apply lt_trans with (pred (length l1)); try assumption; apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H13 in H6; discriminate. unfold Rmin; decide (Rle_dec a b) with Hyp1; reflexivity. @@ -2018,7 +2018,7 @@ Proof. replace a with (Rmin a b). rewrite <- H5; elim (RList_P6 l1); intros; apply H11; try assumption. apply le_O_n. - apply lt_trans with (pred (Rlength l1)); try assumption; apply lt_pred_n_n; + apply lt_trans with (pred (length l1)); try assumption; apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H13 in H6; discriminate. unfold Rmin; decide (Rle_dec a b) with Hyp1; reflexivity. @@ -2037,7 +2037,7 @@ Proof. replace b with (Rmin b c). rewrite <- H5; elim (RList_P6 l1); intros; apply H10; try assumption. apply le_O_n. - apply lt_trans with (pred (Rlength l1)); try assumption; apply lt_pred_n_n; + apply lt_trans with (pred (length l1)); try assumption; apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H12 in H6; discriminate. unfold Rmin; decide (Rle_dec b c) with Hyp2; reflexivity. diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index c8ec4782d9..65221c67d2 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -12,6 +12,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis_reg. Require Import Classical_Prop. +Require Import List. Require Import RList. Local Open Scope R_scope. @@ -114,41 +115,41 @@ Qed. Definition open_interval (a b x:R) : Prop := a < x < b. Definition co_interval (a b x:R) : Prop := a <= x < b. -Definition adapted_couple (f:R -> R) (a b:R) (l lf:Rlist) : Prop := +Definition adapted_couple (f:R -> R) (a b:R) (l lf:list R) : Prop := ordered_Rlist l /\ pos_Rl l 0 = Rmin a b /\ - pos_Rl l (pred (Rlength l)) = Rmax a b /\ - Rlength l = S (Rlength lf) /\ + pos_Rl l (pred (length l)) = Rmax a b /\ + length l = S (length lf) /\ (forall i:nat, - (i < pred (Rlength l))%nat -> + (i < pred (length l))%nat -> constant_D_eq f (open_interval (pos_Rl l i) (pos_Rl l (S i))) (pos_Rl lf i)). -Definition adapted_couple_opt (f:R -> R) (a b:R) (l lf:Rlist) := +Definition adapted_couple_opt (f:R -> R) (a b:R) (l lf:list R) := adapted_couple f a b l lf /\ (forall i:nat, - (i < pred (Rlength lf))%nat -> + (i < pred (length lf))%nat -> pos_Rl lf i <> pos_Rl lf (S i) \/ f (pos_Rl l (S i)) <> pos_Rl lf i) /\ - (forall i:nat, (i < pred (Rlength l))%nat -> pos_Rl l i <> pos_Rl l (S i)). + (forall i:nat, (i < pred (length l))%nat -> pos_Rl l i <> pos_Rl l (S i)). -Definition is_subdivision (f:R -> R) (a b:R) (l:Rlist) : Type := - { l0:Rlist & adapted_couple f a b l l0 }. +Definition is_subdivision (f:R -> R) (a b:R) (l:list R) : Type := + { l0:list R & adapted_couple f a b l l0 }. Definition IsStepFun (f:R -> R) (a b:R) : Type := - { l:Rlist & is_subdivision f a b l }. + { l:list R & is_subdivision f a b l }. (** ** Class of step functions *) Record StepFun (a b:R) : Type := mkStepFun {fe :> R -> R; pre : IsStepFun fe a b}. -Definition subdivision (a b:R) (f:StepFun a b) : Rlist := projT1 (pre f). +Definition subdivision (a b:R) (f:StepFun a b) : list R := projT1 (pre f). -Definition subdivision_val (a b:R) (f:StepFun a b) : Rlist := +Definition subdivision_val (a b:R) (f:StepFun a b) : list R := match projT2 (pre f) with | existT _ a b => a end. -Fixpoint Int_SF (l k:Rlist) : R := +Fixpoint Int_SF (l k:list R) : R := match l with | nil => 0 | cons a l' => @@ -179,7 +180,7 @@ Proof. Qed. Lemma StepFun_P2 : - forall (a b:R) (f:R -> R) (l lf:Rlist), + forall (a b:R) (f:R -> R) (l lf:list R), adapted_couple f a b l lf -> adapted_couple f b a l lf. Proof. unfold adapted_couple; intros; decompose [and] H; clear H; @@ -219,7 +220,7 @@ Proof. Qed. Lemma StepFun_P5 : - forall (a b:R) (f:R -> R) (l:Rlist), + forall (a b:R) (f:R -> R) (l:list R), is_subdivision f a b l -> is_subdivision f b a l. Proof. destruct 1 as (x,(H0,(H1,(H2,(H3,H4))))); exists x; @@ -236,7 +237,7 @@ Proof. Qed. Lemma StepFun_P7 : - forall (a b r1 r2 r3:R) (f:R -> R) (l lf:Rlist), + forall (a b r1 r2 r3:R) (f:R -> R) (l lf:list R), a <= b -> adapted_couple f a b (cons r1 (cons r2 l)) (cons r3 lf) -> adapted_couple f r2 b (cons r2 l) lf. @@ -257,31 +258,36 @@ Proof. rewrite H4; reflexivity. intros; unfold constant_D_eq, open_interval; intros; unfold constant_D_eq, open_interval in H6; - assert (H9 : (S i < pred (Rlength (cons r1 (cons r2 l))))%nat). + assert (H9 : (S i < pred (length (cons r1 (cons r2 l))))%nat). simpl; simpl in H0; apply lt_n_S; assumption. assert (H10 := H6 _ H9); apply H10; assumption. Qed. Lemma StepFun_P8 : - forall (f:R -> R) (l1 lf1:Rlist) (a b:R), + forall (f:R -> R) (l1 lf1:list R) (a b:R), adapted_couple f a b l1 lf1 -> a = b -> Int_SF lf1 l1 = 0. Proof. simple induction l1. intros; induction lf1 as [| r lf1 Hreclf1]; reflexivity. - simple induction r0. + intros r r0. + induction r0 as [ | r1 r2 H0]. intros; induction lf1 as [| r1 lf1 Hreclf1]. reflexivity. unfold adapted_couple in H0; decompose [and] H0; clear H0; simpl in H5; discriminate. - intros; induction lf1 as [| r3 lf1 Hreclf1]. + intros H. + induction lf1 as [| r3 lf1 Hreclf1]; intros a b H1 H2. reflexivity. simpl; cut (r = r1). - intro; rewrite H3; rewrite (H0 lf1 r b). + intros H3. + rewrite H3; rewrite (H lf1 r b). ring. rewrite H3; apply StepFun_P7 with a r r3; [ right; assumption | assumption ]. - clear H H0 Hreclf1 r0; unfold adapted_couple in H1; decompose [and] H1; + clear H H0 Hreclf1; unfold adapted_couple in H1. + decompose [and] H1. intros; simpl in H4; rewrite H4; unfold Rmin; case (Rle_dec a b); intro; [ assumption | reflexivity ]. + unfold adapted_couple in H1; decompose [and] H1; intros; apply Rle_antisym. apply (H3 0%nat); simpl; apply lt_O_Sn. simpl in H5; rewrite H2 in H5; rewrite H5; replace (Rmin b b) with (Rmax a b); @@ -292,8 +298,8 @@ Proof. Qed. Lemma StepFun_P9 : - forall (a b:R) (f:R -> R) (l lf:Rlist), - adapted_couple f a b l lf -> a <> b -> (2 <= Rlength l)%nat. + forall (a b:R) (f:R -> R) (l lf:list R), + adapted_couple f a b l lf -> a <> b -> (2 <= length l)%nat. Proof. intros; unfold adapted_couple in H; decompose [and] H; clear H; induction l as [| r l Hrecl]; @@ -307,13 +313,13 @@ Proof. Qed. Lemma StepFun_P10 : - forall (f:R -> R) (l lf:Rlist) (a b:R), + forall (f:R -> R) (l lf:list R) (a b:R), a <= b -> adapted_couple f a b l lf -> - exists l' : Rlist, - (exists lf' : Rlist, adapted_couple_opt f a b l' lf'). + exists l' : list R, + (exists lf' : list R, adapted_couple_opt f a b l' lf'). Proof. - simple induction l. + induction l as [ | r r0 H]. intros; unfold adapted_couple in H0; decompose [and] H0; simpl in H4; discriminate. intros; case (Req_dec a b); intro. @@ -503,7 +509,7 @@ Proof. Qed. Lemma StepFun_P11 : - forall (a b r r1 r3 s1 s2 r4:R) (r2 lf1 s3 lf2:Rlist) + forall (a b r r1 r3 s1 s2 r4:R) (r2 lf1 s3 lf2:list R) (f:R -> R), a < b -> adapted_couple f a b (cons r (cons r1 r2)) (cons r3 lf1) -> @@ -627,7 +633,7 @@ Proof. Qed. Lemma StepFun_P12 : - forall (a b:R) (f:R -> R) (l lf:Rlist), + forall (a b:R) (f:R -> R) (l lf:list R), adapted_couple_opt f a b l lf -> adapted_couple_opt f b a l lf. Proof. unfold adapted_couple_opt; unfold adapted_couple; intros; @@ -643,7 +649,7 @@ Proof. Qed. Lemma StepFun_P13 : - forall (a b r r1 r3 s1 s2 r4:R) (r2 lf1 s3 lf2:Rlist) + forall (a b r r1 r3 s1 s2 r4:R) (r2 lf1 s3 lf2:list R) (f:R -> R), a <> b -> adapted_couple f a b (cons r (cons r1 r2)) (cons r3 lf1) -> @@ -657,15 +663,15 @@ Proof. Qed. Lemma StepFun_P14 : - forall (f:R -> R) (l1 l2 lf1 lf2:Rlist) (a b:R), + forall (f:R -> R) (l1 l2 lf1 lf2:list R) (a b:R), a <= b -> adapted_couple f a b l1 lf1 -> adapted_couple_opt f a b l2 lf2 -> Int_SF lf1 l1 = Int_SF lf2 l2. Proof. - simple induction l1. + induction l1 as [ | r r0 H0]. intros l2 lf1 lf2 a b Hyp H H0; unfold adapted_couple in H; decompose [and] H; clear H H0 H2 H3 H1 H6; simpl in H4; discriminate. - simple induction r0. + induction r0 as [|r1 r2 H]. intros; case (Req_dec a b); intro. unfold adapted_couple_opt in H2; elim H2; intros; rewrite (StepFun_P8 H4 H3); rewrite (StepFun_P8 H1 H3); reflexivity. @@ -798,7 +804,7 @@ Proof. rewrite H9; change (forall i:nat, - (i < pred (Rlength (cons r4 lf2)))%nat -> + (i < pred (length (cons r4 lf2)))%nat -> pos_Rl (cons r4 lf2) i <> pos_Rl (cons r4 lf2) (S i) \/ f (pos_Rl (cons s1 (cons s2 s3)) (S i)) <> pos_Rl (cons r4 lf2) i) ; rewrite <- H5; apply H3. @@ -840,7 +846,7 @@ Proof. rewrite <- H10; unfold open_interval; apply H2. elim H3; clear H3; intros; split. rewrite H5 in H3; intros; apply (H3 (S i)). - simpl; replace (Rlength lf2) with (S (pred (Rlength lf2))). + simpl; replace (length lf2) with (S (pred (length lf2))). apply lt_n_S; apply H12. symmetry ; apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H13 in H12; elim (lt_n_O _ H12). @@ -863,7 +869,7 @@ Proof. Qed. Lemma StepFun_P15 : - forall (f:R -> R) (l1 l2 lf1 lf2:Rlist) (a b:R), + forall (f:R -> R) (l1 l2 lf1 lf2:list R) (a b:R), adapted_couple f a b l1 lf1 -> adapted_couple_opt f a b l2 lf2 -> Int_SF lf1 l1 = Int_SF lf2 l2. Proof. @@ -876,10 +882,10 @@ Proof. Qed. Lemma StepFun_P16 : - forall (f:R -> R) (l lf:Rlist) (a b:R), + forall (f:R -> R) (l lf:list R) (a b:R), adapted_couple f a b l lf -> - exists l' : Rlist, - (exists lf' : Rlist, adapted_couple_opt f a b l' lf'). + exists l' : list R, + (exists lf' : list R, adapted_couple_opt f a b l' lf'). Proof. intros; destruct (Rle_dec a b) as [Hle|Hnle]; [ apply (StepFun_P10 Hle H) @@ -891,7 +897,7 @@ Proof. Qed. Lemma StepFun_P17 : - forall (f:R -> R) (l1 l2 lf1 lf2:Rlist) (a b:R), + forall (f:R -> R) (l1 l2 lf1 lf2:list R) (a b:R), adapted_couple f a b l1 lf1 -> adapted_couple f a b l2 lf2 -> Int_SF lf1 l1 = Int_SF lf2 l2. Proof. @@ -922,7 +928,7 @@ Proof. Qed. Lemma StepFun_P19 : - forall (l1:Rlist) (f g:R -> R) (l:R), + forall (l1:list R) (f g:R -> R) (l:R), Int_SF (FF l1 (fun x:R => f x + l * g x)) l1 = Int_SF (FF l1 f) l1 + l * Int_SF (FF l1 g) l1. Proof. @@ -933,8 +939,8 @@ Proof. Qed. Lemma StepFun_P20 : - forall (l:Rlist) (f:R -> R), - (0 < Rlength l)%nat -> Rlength l = S (Rlength (FF l f)). + forall (l:list R) (f:R -> R), + (0 < length l)%nat -> length l = S (length (FF l f)). Proof. intros l f H; induction l; [ elim (lt_irrefl _ H) @@ -942,7 +948,7 @@ Proof. Qed. Lemma StepFun_P21 : - forall (a b:R) (f:R -> R) (l:Rlist), + forall (a b:R) (f:R -> R) (l:list R), is_subdivision f a b l -> adapted_couple f a b l (FF l f). Proof. intros * (x & H & H1 & H0 & H2 & H4). @@ -979,7 +985,7 @@ Proof. Qed. Lemma StepFun_P22 : - forall (a b:R) (f g:R -> R) (lf lg:Rlist), + forall (a b:R) (f g:R -> R) (lf lg:list R), a <= b -> is_subdivision f a b lf -> is_subdivision g a b lg -> is_subdivision f a b (cons_ORlist lf lg). @@ -1032,25 +1038,25 @@ Proof. (H8 : In (pos_Rl (cons_ORlist (cons r lf) lg) - (pred (Rlength (cons_ORlist (cons r lf) lg)))) + (pred (length (cons_ORlist (cons r lf) lg)))) (cons_ORlist (cons r lf) lg)). elim (RList_P3 (cons_ORlist (cons r lf) lg) (pos_Rl (cons_ORlist (cons r lf) lg) - (pred (Rlength (cons_ORlist (cons r lf) lg))))); + (pred (length (cons_ORlist (cons r lf) lg))))); intros _ H10; apply H10; - exists (pred (Rlength (cons_ORlist (cons r lf) lg))); + exists (pred (length (cons_ORlist (cons r lf) lg))); split; [ reflexivity | rewrite RList_P11; simpl; apply lt_n_Sn ]. elim (RList_P9 (cons r lf) lg (pos_Rl (cons_ORlist (cons r lf) lg) - (pred (Rlength (cons_ORlist (cons r lf) lg))))); + (pred (length (cons_ORlist (cons r lf) lg))))); intros H10 _. assert (H11 := H10 H8); elim H11; intro. elim (RList_P3 (cons r lf) (pos_Rl (cons_ORlist (cons r lf) lg) - (pred (Rlength (cons_ORlist (cons r lf) lg))))); + (pred (length (cons_ORlist (cons r lf) lg))))); intros H13 _; assert (H14 := H13 H12); elim H14; intros; elim H15; clear H15; intros; rewrite H15; rewrite <- H5; elim (RList_P6 (cons r lf)); intros; apply H17; @@ -1060,10 +1066,10 @@ Proof. elim (RList_P3 lg (pos_Rl (cons_ORlist (cons r lf) lg) - (pred (Rlength (cons_ORlist (cons r lf) lg))))); + (pred (length (cons_ORlist (cons r lf) lg))))); intros H13 _; assert (H14 := H13 H12); elim H14; intros; elim H15; clear H15; intros. - rewrite H15; assert (H17 : Rlength lg = S (pred (Rlength lg))). + rewrite H15; assert (H17 : length lg = S (pred (length lg))). apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H17 in H16; elim (lt_n_O _ H16). rewrite <- H0; elim (RList_P6 lg); intros; apply H18; @@ -1075,7 +1081,7 @@ Proof. assert (H8 : In b (cons_ORlist (cons r lf) lg)). elim (RList_P9 (cons r lf) lg b); intros; apply H10; left; elim (RList_P3 (cons r lf) b); intros; apply H12; - exists (pred (Rlength (cons r lf))); split; + exists (pred (length (cons r lf))); split; [ symmetry ; assumption | simpl; apply lt_n_Sn ]. apply RList_P7; [ apply RList_P2; assumption | assumption ]. apply StepFun_P20; rewrite RList_P11; rewrite H2; rewrite H7; simpl; @@ -1089,7 +1095,7 @@ Proof. intros; elim H11; clear H11; intros; assert (H12 := H11); assert (Hyp_cons : - exists r : R, (exists r0 : Rlist, cons_ORlist lf lg = cons r r0)). + exists r : R, (exists r0 : list R, cons_ORlist lf lg = cons r r0)). apply RList_P19; red; intro; rewrite H13 in H8; elim (lt_n_O _ H8). elim Hyp_cons; clear Hyp_cons; intros r [r0 Hyp_cons]; rewrite Hyp_cons; unfold FF; rewrite RList_P12. @@ -1128,7 +1134,7 @@ Proof. elim (RList_P6 (cons_ORlist lf lg)); intros; apply H11. apply RList_P2; assumption. apply le_O_n. - apply lt_trans with (pred (Rlength (cons_ORlist lf lg))); + apply lt_trans with (pred (length (cons_ORlist lf lg))); [ assumption | apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H13 in H8; elim (lt_n_O _ H8) ]. @@ -1147,9 +1153,9 @@ Proof. set (I := fun j:nat => - pos_Rl lf j <= pos_Rl (cons_ORlist lf lg) i /\ (j < Rlength lf)%nat); + pos_Rl lf j <= pos_Rl (cons_ORlist lf lg) i /\ (j < length lf)%nat); assert (H12 : Nbound I). - unfold Nbound; exists (Rlength lf); intros; unfold I in H12; elim H12; + unfold Nbound; exists (length lf); intros; unfold I in H12; elim H12; intros; apply lt_le_weak; assumption. assert (H13 : exists n : nat, I n). exists 0%nat; unfold I; split. @@ -1159,7 +1165,7 @@ Proof. elim (RList_P6 (cons_ORlist lf lg)); intros; apply H13. apply RList_P2; assumption. apply le_O_n. - apply lt_trans with (pred (Rlength (cons_ORlist lf lg))). + apply lt_trans with (pred (length (cons_ORlist lf lg))). assumption. apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H15 in H8; elim (lt_n_O _ H8). @@ -1167,12 +1173,12 @@ Proof. rewrite <- H6 in H11; rewrite <- H5 in H11; elim (Rlt_irrefl _ H11). assert (H14 := Nzorn H13 H12); elim H14; clear H14; intros x0 H14; exists (pos_Rl lf0 x0); unfold constant_D_eq, open_interval; - intros; assert (H16 := H9 x0); assert (H17 : (x0 < pred (Rlength lf))%nat). + intros; assert (H16 := H9 x0); assert (H17 : (x0 < pred (length lf))%nat). elim H14; clear H14; intros; unfold I in H14; elim H14; clear H14; intros; - apply lt_S_n; replace (S (pred (Rlength lf))) with (Rlength lf). + apply lt_S_n; replace (S (pred (length lf))) with (length lf). inversion H18. 2: apply lt_n_S; assumption. - cut (x0 = pred (Rlength lf)). + cut (x0 = pred (length lf)). intro; rewrite H19 in H14; rewrite H5 in H14; cut (pos_Rl (cons_ORlist lf lg) i < b). intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H14 H21)). @@ -1180,7 +1186,7 @@ Proof. elim H10; intros; apply Rlt_trans with x; assumption. rewrite <- H5; apply Rle_trans with - (pos_Rl (cons_ORlist lf lg) (pred (Rlength (cons_ORlist lf lg)))). + (pos_Rl (cons_ORlist lf lg) (pred (length (cons_ORlist lf lg)))). elim (RList_P6 (cons_ORlist lf lg)); intros; apply H21. apply RList_P2; assumption. apply lt_n_Sm_le; apply lt_n_S; assumption. @@ -1197,8 +1203,8 @@ Proof. elim H14; clear H14; intros; split. apply Rle_lt_trans with (pos_Rl (cons_ORlist lf lg) i); assumption. apply Rlt_le_trans with (pos_Rl (cons_ORlist lf lg) (S i)); try assumption. - assert (H22 : (S x0 < Rlength lf)%nat). - replace (Rlength lf) with (S (pred (Rlength lf))); + assert (H22 : (S x0 < length lf)%nat). + replace (length lf) with (S (pred (length lf))); [ apply lt_n_S; assumption | symmetry ; apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H22 in H21; elim (lt_n_O _ H21) ]. @@ -1216,7 +1222,7 @@ Proof. Qed. Lemma StepFun_P23 : - forall (a b:R) (f g:R -> R) (lf lg:Rlist), + forall (a b:R) (f g:R -> R) (lf lg:list R), is_subdivision f a b lf -> is_subdivision g a b lg -> is_subdivision f a b (cons_ORlist lf lg). Proof. @@ -1229,7 +1235,7 @@ Proof. Qed. Lemma StepFun_P24 : - forall (a b:R) (f g:R -> R) (lf lg:Rlist), + forall (a b:R) (f g:R -> R) (lf lg:list R), a <= b -> is_subdivision f a b lf -> is_subdivision g a b lg -> is_subdivision g a b (cons_ORlist lf lg). @@ -1282,24 +1288,24 @@ Proof. (H8 : In (pos_Rl (cons_ORlist (cons r lf) lg) - (pred (Rlength (cons_ORlist (cons r lf) lg)))) + (pred (length (cons_ORlist (cons r lf) lg)))) (cons_ORlist (cons r lf) lg)). elim (RList_P3 (cons_ORlist (cons r lf) lg) (pos_Rl (cons_ORlist (cons r lf) lg) - (pred (Rlength (cons_ORlist (cons r lf) lg))))); + (pred (length (cons_ORlist (cons r lf) lg))))); intros _ H10; apply H10; - exists (pred (Rlength (cons_ORlist (cons r lf) lg))); + exists (pred (length (cons_ORlist (cons r lf) lg))); split; [ reflexivity | rewrite RList_P11; simpl; apply lt_n_Sn ]. elim (RList_P9 (cons r lf) lg (pos_Rl (cons_ORlist (cons r lf) lg) - (pred (Rlength (cons_ORlist (cons r lf) lg))))); + (pred (length (cons_ORlist (cons r lf) lg))))); intros H10 _; assert (H11 := H10 H8); elim H11; intro. elim (RList_P3 (cons r lf) (pos_Rl (cons_ORlist (cons r lf) lg) - (pred (Rlength (cons_ORlist (cons r lf) lg))))); + (pred (length (cons_ORlist (cons r lf) lg))))); intros H13 _; assert (H14 := H13 H12); elim H14; intros; elim H15; clear H15; intros; rewrite H15; rewrite <- H5; elim (RList_P6 (cons r lf)); intros; apply H17; @@ -1309,10 +1315,10 @@ Proof. elim (RList_P3 lg (pos_Rl (cons_ORlist (cons r lf) lg) - (pred (Rlength (cons_ORlist (cons r lf) lg))))); + (pred (length (cons_ORlist (cons r lf) lg))))); intros H13 _; assert (H14 := H13 H12); elim H14; intros; elim H15; clear H15; intros; rewrite H15; - assert (H17 : Rlength lg = S (pred (Rlength lg))). + assert (H17 : length lg = S (pred (length lg))). apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H17 in H16; elim (lt_n_O _ H16). rewrite <- H0; elim (RList_P6 lg); intros; apply H18; @@ -1324,7 +1330,7 @@ Proof. assert (H8 : In b (cons_ORlist (cons r lf) lg)). elim (RList_P9 (cons r lf) lg b); intros; apply H10; left; elim (RList_P3 (cons r lf) b); intros; apply H12; - exists (pred (Rlength (cons r lf))); split; + exists (pred (length (cons r lf))); split; [ symmetry ; assumption | simpl; apply lt_n_Sn ]. apply RList_P7; [ apply RList_P2; assumption | assumption ]. apply StepFun_P20; rewrite RList_P11; rewrite H7; rewrite H2; simpl; @@ -1338,7 +1344,7 @@ Proof. intros; elim H11; clear H11; intros; assert (H12 := H11); assert (Hyp_cons : - exists r : R, (exists r0 : Rlist, cons_ORlist lf lg = cons r r0)). + exists r : R, (exists r0 : list R, cons_ORlist lf lg = cons r r0)). apply RList_P19; red; intro; rewrite H13 in H8; elim (lt_n_O _ H8). elim Hyp_cons; clear Hyp_cons; intros r [r0 Hyp_cons]; rewrite Hyp_cons; unfold FF; rewrite RList_P12. @@ -1377,7 +1383,7 @@ Proof. elim (RList_P6 (cons_ORlist lf lg)); intros; apply H11. apply RList_P2; assumption. apply le_O_n. - apply lt_trans with (pred (Rlength (cons_ORlist lf lg))); + apply lt_trans with (pred (length (cons_ORlist lf lg))); [ assumption | apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H13 in H8; elim (lt_n_O _ H8) ]. @@ -1394,9 +1400,9 @@ Proof. set (I := fun j:nat => - pos_Rl lg j <= pos_Rl (cons_ORlist lf lg) i /\ (j < Rlength lg)%nat); + pos_Rl lg j <= pos_Rl (cons_ORlist lf lg) i /\ (j < length lg)%nat); assert (H12 : Nbound I). - unfold Nbound; exists (Rlength lg); intros; unfold I in H12; elim H12; + unfold Nbound; exists (length lg); intros; unfold I in H12; elim H12; intros; apply lt_le_weak; assumption. assert (H13 : exists n : nat, I n). exists 0%nat; unfold I; split. @@ -1406,7 +1412,7 @@ Proof. elim (RList_P6 (cons_ORlist lf lg)); intros; apply H13; [ apply RList_P2; assumption | apply le_O_n - | apply lt_trans with (pred (Rlength (cons_ORlist lf lg))); + | apply lt_trans with (pred (length (cons_ORlist lf lg))); [ assumption | apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H15 in H8; elim (lt_n_O _ H8) ] ]. @@ -1414,12 +1420,12 @@ Proof. rewrite <- H1 in H11; rewrite <- H0 in H11; elim (Rlt_irrefl _ H11). assert (H14 := Nzorn H13 H12); elim H14; clear H14; intros x0 H14; exists (pos_Rl lg0 x0); unfold constant_D_eq, open_interval; - intros; assert (H16 := H4 x0); assert (H17 : (x0 < pred (Rlength lg))%nat). + intros; assert (H16 := H4 x0); assert (H17 : (x0 < pred (length lg))%nat). elim H14; clear H14; intros; unfold I in H14; elim H14; clear H14; intros; - apply lt_S_n; replace (S (pred (Rlength lg))) with (Rlength lg). + apply lt_S_n; replace (S (pred (length lg))) with (length lg). inversion H18. 2: apply lt_n_S; assumption. - cut (x0 = pred (Rlength lg)). + cut (x0 = pred (length lg)). intro; rewrite H19 in H14; rewrite H0 in H14; cut (pos_Rl (cons_ORlist lf lg) i < b). intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H14 H21)). @@ -1427,7 +1433,7 @@ Proof. elim H10; intros; apply Rlt_trans with x; assumption. rewrite <- H0; apply Rle_trans with - (pos_Rl (cons_ORlist lf lg) (pred (Rlength (cons_ORlist lf lg)))). + (pos_Rl (cons_ORlist lf lg) (pred (length (cons_ORlist lf lg)))). elim (RList_P6 (cons_ORlist lf lg)); intros; apply H21. apply RList_P2; assumption. apply lt_n_Sm_le; apply lt_n_S; assumption. @@ -1445,8 +1451,8 @@ Proof. elim H14; clear H14; intros; split. apply Rle_lt_trans with (pos_Rl (cons_ORlist lf lg) i); assumption. apply Rlt_le_trans with (pos_Rl (cons_ORlist lf lg) (S i)); try assumption. - assert (H22 : (S x0 < Rlength lg)%nat). - replace (Rlength lg) with (S (pred (Rlength lg))). + assert (H22 : (S x0 < length lg)%nat). + replace (length lg) with (S (pred (length lg))). apply lt_n_S; assumption. symmetry ; apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H22 in H21; elim (lt_n_O _ H21). @@ -1463,7 +1469,7 @@ Proof. Qed. Lemma StepFun_P25 : - forall (a b:R) (f g:R -> R) (lf lg:Rlist), + forall (a b:R) (f g:R -> R) (lf lg:list R), is_subdivision f a b lf -> is_subdivision g a b lg -> is_subdivision g a b (cons_ORlist lf lg). Proof. @@ -1476,7 +1482,7 @@ Proof. Qed. Lemma StepFun_P26 : - forall (a b l:R) (f g:R -> R) (l1:Rlist), + forall (a b l:R) (f g:R -> R) (l1:list R), is_subdivision f a b l1 -> is_subdivision g a b l1 -> is_subdivision (fun x:R => f x + l * g x) a b l1. @@ -1494,7 +1500,7 @@ Proof. change (pos_Rl x0 i + l * pos_Rl x i = pos_Rl - (app_Rlist (mid_Rlist (cons r r0) r) (fun x2:R => f x2 + l * g x2)) + (map (fun x2:R => f x2 + l * g x2) (mid_Rlist (cons r r0) r)) (S i)); rewrite RList_P12. rewrite RList_P13. rewrite <- H12; rewrite (H9 _ H8); try rewrite (H4 _ H8); @@ -1521,7 +1527,7 @@ Proof. Qed. Lemma StepFun_P27 : - forall (a b l:R) (f g:R -> R) (lf lg:Rlist), + forall (a b l:R) (f g:R -> R) (lf lg:list R), is_subdivision f a b lf -> is_subdivision g a b lg -> is_subdivision (fun x:R => f x + l * g x) a b (cons_ORlist lf lg). @@ -1586,9 +1592,9 @@ Proof. Qed. Lemma StepFun_P31 : - forall (a b:R) (f:R -> R) (l lf:Rlist), + forall (a b:R) (f:R -> R) (l lf:list R), adapted_couple f a b l lf -> - adapted_couple (fun x:R => Rabs (f x)) a b l (app_Rlist lf Rabs). + adapted_couple (fun x:R => Rabs (f x)) a b l (map Rabs lf). Proof. unfold adapted_couple; intros; decompose [and] H; clear H; repeat split; try assumption. @@ -1604,15 +1610,15 @@ Lemma StepFun_P32 : Proof. intros a b f; unfold IsStepFun; apply existT with (subdivision f); unfold is_subdivision; - apply existT with (app_Rlist (subdivision_val f) Rabs); + apply existT with (map Rabs (subdivision_val f)); apply StepFun_P31; apply StepFun_P1. Qed. Lemma StepFun_P33 : - forall l2 l1:Rlist, - ordered_Rlist l1 -> Rabs (Int_SF l2 l1) <= Int_SF (app_Rlist l2 Rabs) l1. + forall l2 l1:list R, + ordered_Rlist l1 -> Rabs (Int_SF l2 l1) <= Int_SF (map Rabs l2) l1. Proof. - simple induction l2; intros. + induction l2 as [ | r r0 H]; intros. simpl; rewrite Rabs_R0; right; reflexivity. simpl; induction l1 as [| r1 l1 Hrecl1]. rewrite Rabs_R0; right; reflexivity. @@ -1635,7 +1641,7 @@ Proof. replace (Int_SF (subdivision_val (mkStepFun (StepFun_P32 f))) (subdivision (mkStepFun (StepFun_P32 f)))) with - (Int_SF (app_Rlist (subdivision_val f) Rabs) (subdivision f)). + (Int_SF (map Rabs (subdivision_val f)) (subdivision f)). apply StepFun_P33; assert (H0 := StepFun_P29 f); unfold is_subdivision in H0; elim H0; intros; unfold adapted_couple in p; decompose [and] p; assumption. @@ -1645,14 +1651,14 @@ Proof. Qed. Lemma StepFun_P35 : - forall (l:Rlist) (a b:R) (f g:R -> R), + forall (l:list R) (a b:R) (f g:R -> R), ordered_Rlist l -> pos_Rl l 0 = a -> - pos_Rl l (pred (Rlength l)) = b -> + pos_Rl l (pred (length l)) = b -> (forall x:R, a < x < b -> f x <= g x) -> Int_SF (FF l f) l <= Int_SF (FF l g) l. Proof. - simple induction l; intros. + induction l as [ | r r0 H]; intros. right; reflexivity. simpl; induction r0 as [| r0 r1 Hrecr0]. right; reflexivity. @@ -1682,7 +1688,7 @@ Proof. rewrite <- Rinv_r_sym. rewrite Rmult_1_l; rewrite double; assert (H5 : r0 <= b). replace b with - (pos_Rl (cons r (cons r0 r1)) (pred (Rlength (cons r (cons r0 r1))))). + (pos_Rl (cons r (cons r0 r1)) (pred (length (cons r (cons r0 r1))))). replace r0 with (pos_Rl (cons r (cons r0 r1)) 1). elim (RList_P6 (cons r (cons r0 r1))); intros; apply H5. assumption. @@ -1712,7 +1718,7 @@ Proof. Qed. Lemma StepFun_P36 : - forall (a b:R) (f g:StepFun a b) (l:Rlist), + forall (a b:R) (f g:StepFun a b) (l:list R), a <= b -> is_subdivision f a b l -> is_subdivision g a b l -> @@ -1748,18 +1754,18 @@ Proof. Qed. Lemma StepFun_P38 : - forall (l:Rlist) (a b:R) (f:R -> R), + forall (l:list R) (a b:R) (f:R -> R), ordered_Rlist l -> pos_Rl l 0 = a -> - pos_Rl l (pred (Rlength l)) = b -> + pos_Rl l (pred (length l)) = b -> { g:StepFun a b | g b = f b /\ (forall i:nat, - (i < pred (Rlength l))%nat -> + (i < pred (length l))%nat -> constant_D_eq g (co_interval (pos_Rl l i) (pos_Rl l (S i))) (f (pos_Rl l i))) }. Proof. - intros l a b f; generalize a; clear a; induction l. + intros l a b f; generalize a; clear a; induction l as [|r l IHl]. intros a H H0 H1; simpl in H0; simpl in H1; exists (mkStepFun (StepFun_P4 a b (f b))); split. reflexivity. @@ -1772,7 +1778,7 @@ Proof. apply RList_P4 with r; assumption. assert (H3 : pos_Rl (cons r1 l) 0 = r1). reflexivity. - assert (H4 : pos_Rl (cons r1 l) (pred (Rlength (cons r1 l))) = b). + assert (H4 : pos_Rl (cons r1 l) (pred (length (cons r1 l))) = b). rewrite <- H1; reflexivity. elim (IHl r1 H2 H3 H4); intros g [H5 H6]. set @@ -1796,7 +1802,7 @@ Proof. simpl in H0; rewrite <- H0; apply (H 0%nat); simpl; apply lt_O_Sn. unfold Rmin; decide (Rle_dec r1 b) with H7; reflexivity. apply (H10 i); apply lt_S_n. - replace (S (pred (Rlength lg))) with (Rlength lg). + replace (S (pred (length lg))) with (length lg). apply H9. apply S_pred with 0%nat; apply neq_O_lt; intro; rewrite <- H14 in H9; elim (lt_n_O _ H9). @@ -1825,9 +1831,9 @@ Proof. change (constant_D_eq g' (open_interval (pos_Rl lg i) (pos_Rl lg (S i))) (pos_Rl lg2 i)); clear Hreci; assert (H16 := H15 i); - assert (H17 : (i < pred (Rlength lg))%nat). + assert (H17 : (i < pred (length lg))%nat). apply lt_S_n. - replace (S (pred (Rlength lg))) with (Rlength lg). + replace (S (pred (length lg))) with (length lg). assumption. apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H14 in H9; elim (lt_n_O _ H9). @@ -1843,7 +1849,7 @@ Proof. assumption. elim (RList_P3 lg (pos_Rl lg i)); intros; apply H21; exists i; split. reflexivity. - apply lt_trans with (pred (Rlength lg)); try assumption. + apply lt_trans with (pred (length lg)); try assumption. apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H22 in H17; elim (lt_n_O _ H17). unfold Rmin; decide (Rle_dec r1 b) with H7; reflexivity. @@ -1860,7 +1866,7 @@ Proof. (constant_D_eq (mkStepFun H8) (co_interval (pos_Rl (cons r1 l) i) (pos_Rl (cons r1 l) (S i))) (f (pos_Rl (cons r1 l) i))); assert (H10 := H6 i); - assert (H11 : (i < pred (Rlength (cons r1 l)))%nat). + assert (H11 : (i < pred (length (cons r1 l)))%nat). simpl; apply lt_S_n; assumption. assert (H12 := H10 H11); unfold constant_D_eq, co_interval in H12; unfold constant_D_eq, co_interval; intros; @@ -1873,7 +1879,7 @@ Proof. elim (RList_P6 (cons r1 l)); intros; apply H15; [ assumption | apply le_O_n - | simpl; apply lt_trans with (Rlength l); + | simpl; apply lt_trans with (length l); [ apply lt_S_n; assumption | apply lt_n_Sn ] ]. Qed. @@ -1912,12 +1918,12 @@ Proof. Qed. Lemma StepFun_P40 : - forall (f:R -> R) (a b c:R) (l1 l2 lf1 lf2:Rlist), + forall (f:R -> R) (a b c:R) (l1 l2 lf1 lf2:list R), a < b -> b < c -> adapted_couple f a b l1 lf1 -> adapted_couple f b c l2 lf2 -> - adapted_couple f a c (cons_Rlist l1 l2) (FF (cons_Rlist l1 l2) f). + adapted_couple f a c (app l1 l2) (FF (app l1 l2) f). Proof. intros f a b c l1 l2 lf1 lf2 H H0 H1 H2; unfold adapted_couple in H1, H2; unfold adapted_couple; decompose [and] H1; @@ -1941,28 +1947,28 @@ Proof. | left; assumption ]. red; intro; rewrite H1 in H11; discriminate. apply StepFun_P20. - rewrite RList_P23; apply neq_O_lt; red; intro. - assert (H2 : (Rlength l1 + Rlength l2)%nat = 0%nat). + rewrite app_length; apply neq_O_lt; red; intro. + assert (H2 : (length l1 + length l2)%nat = 0%nat). symmetry ; apply H1. elim (plus_is_O _ _ H2); intros; rewrite H12 in H6; discriminate. unfold constant_D_eq, open_interval; intros; - elim (le_or_lt (S (S i)) (Rlength l1)); intro. - assert (H14 : pos_Rl (cons_Rlist l1 l2) i = pos_Rl l1 i). + elim (le_or_lt (S (S i)) (length l1)); intro. + assert (H14 : pos_Rl (app l1 l2) i = pos_Rl l1 i). apply RList_P26; apply lt_S_n; apply le_lt_n_Sm; apply le_S_n; - apply le_trans with (Rlength l1); [ assumption | apply le_n_Sn ]. - assert (H15 : pos_Rl (cons_Rlist l1 l2) (S i) = pos_Rl l1 (S i)). + apply le_trans with (length l1); [ assumption | apply le_n_Sn ]. + assert (H15 : pos_Rl (app l1 l2) (S i) = pos_Rl l1 (S i)). apply RList_P26; apply lt_S_n; apply le_lt_n_Sm; assumption. - rewrite H14 in H2; rewrite H15 in H2; assert (H16 : (2 <= Rlength l1)%nat). + rewrite H14 in H2; rewrite H15 in H2; assert (H16 : (2 <= length l1)%nat). apply le_trans with (S (S i)); [ repeat apply le_n_S; apply le_O_n | assumption ]. elim (RList_P20 _ H16); intros r1 [r2 [r3 H17]]; rewrite H17; change - (f x = pos_Rl (app_Rlist (mid_Rlist (cons_Rlist (cons r2 r3) l2) r1) f) i) + (f x = pos_Rl (map f (mid_Rlist (app (cons r2 r3) l2) r1)) i) ; rewrite RList_P12. induction i as [| i Hreci]. simpl; assert (H18 := H8 0%nat); unfold constant_D_eq, open_interval in H18; - assert (H19 : (0 < pred (Rlength l1))%nat). + assert (H19 : (0 < pred (length l1))%nat). rewrite H17; simpl; apply lt_O_Sn. assert (H20 := H18 H19); repeat rewrite H20. reflexivity. @@ -1991,14 +1997,14 @@ Proof. clear Hreci; rewrite RList_P13. rewrite H17 in H14; rewrite H17 in H15; change - (pos_Rl (cons_Rlist (cons r2 r3) l2) i = + (pos_Rl (app (cons r2 r3) l2) i = pos_Rl (cons r1 (cons r2 r3)) (S i)) in H14; rewrite H14; change - (pos_Rl (cons_Rlist (cons r2 r3) l2) (S i) = + (pos_Rl (app (cons r2 r3) l2) (S i) = pos_Rl (cons r1 (cons r2 r3)) (S (S i))) in H15; rewrite H15; assert (H18 := H8 (S i)); unfold constant_D_eq, open_interval in H18; - assert (H19 : (S i < pred (Rlength l1))%nat). + assert (H19 : (S i < pred (length l1))%nat). apply lt_pred; apply lt_S_n; apply le_lt_n_Sm; assumption. assert (H20 := H18 H19); repeat rewrite H20. reflexivity. @@ -2025,7 +2031,7 @@ Proof. simpl; rewrite H17 in H1; simpl in H1; apply lt_S_n; assumption. rewrite RList_P14; rewrite H17 in H1; simpl in H1; apply H1. inversion H12. - assert (H16 : pos_Rl (cons_Rlist l1 l2) (S i) = b). + assert (H16 : pos_Rl (app l1 l2) (S i) = b). rewrite RList_P29. rewrite H15; rewrite <- minus_n_n; rewrite H10; unfold Rmin; case (Rle_dec b c) as [|[]]; [ reflexivity | left; assumption ]. @@ -2033,30 +2039,30 @@ Proof. induction l1 as [| r l1 Hrecl1]. simpl in H15; discriminate. clear Hrecl1; simpl in H1; simpl; apply lt_n_S; assumption. - assert (H17 : pos_Rl (cons_Rlist l1 l2) i = b). + assert (H17 : pos_Rl (app l1 l2) i = b). rewrite RList_P26. - replace i with (pred (Rlength l1)); + replace i with (pred (length l1)); [ rewrite H4; unfold Rmax; case (Rle_dec a b) as [|[]]; [ reflexivity | left; assumption ] | rewrite H15; reflexivity ]. rewrite H15; apply lt_n_Sn. rewrite H16 in H2; rewrite H17 in H2; elim H2; intros; elim (Rlt_irrefl _ (Rlt_trans _ _ _ H14 H18)). - assert (H16 : pos_Rl (cons_Rlist l1 l2) i = pos_Rl l2 (i - Rlength l1)). + assert (H16 : pos_Rl (app l1 l2) i = pos_Rl l2 (i - length l1)). apply RList_P29. apply le_S_n; assumption. - apply lt_le_trans with (pred (Rlength (cons_Rlist l1 l2))); + apply lt_le_trans with (pred (length (app l1 l2))); [ assumption | apply le_pred_n ]. assert - (H17 : pos_Rl (cons_Rlist l1 l2) (S i) = pos_Rl l2 (S (i - Rlength l1))). - replace (S (i - Rlength l1)) with (S i - Rlength l1)%nat. + (H17 : pos_Rl (app l1 l2) (S i) = pos_Rl l2 (S (i - length l1))). + replace (S (i - length l1)) with (S i - length l1)%nat. apply RList_P29. apply le_S_n; apply le_trans with (S i); [ assumption | apply le_n_Sn ]. induction l1 as [| r l1 Hrecl1]. simpl in H6; discriminate. clear Hrecl1; simpl in H1; simpl; apply lt_n_S; assumption. symmetry ; apply minus_Sn_m; apply le_S_n; assumption. - assert (H18 : (2 <= Rlength l1)%nat). + assert (H18 : (2 <= length l1)%nat). clear f c l2 lf2 H0 H3 H8 H7 H10 H9 H11 H13 i H1 x H2 H12 m H14 H15 H16 H17; induction l1 as [| r l1 Hrecl1]. discriminate. @@ -2068,7 +2074,7 @@ Proof. clear Hrecl1; simpl; repeat apply le_n_S; apply le_O_n. elim (RList_P20 _ H18); intros r1 [r2 [r3 H19]]; rewrite H19; change - (f x = pos_Rl (app_Rlist (mid_Rlist (cons_Rlist (cons r2 r3) l2) r1) f) i) + (f x = pos_Rl (map f (mid_Rlist (app (cons r2 r3) l2) r1)) i) ; rewrite RList_P12. induction i as [| i Hreci]. assert (H20 := le_S_n _ _ H15); assert (H21 := le_trans _ _ _ H18 H20); @@ -2076,31 +2082,31 @@ Proof. clear Hreci; rewrite RList_P13. rewrite H19 in H16; rewrite H19 in H17; change - (pos_Rl (cons_Rlist (cons r2 r3) l2) i = - pos_Rl l2 (S i - Rlength (cons r1 (cons r2 r3)))) + (pos_Rl (app (cons r2 r3) l2) i = + pos_Rl l2 (S i - length (cons r1 (cons r2 r3)))) in H16; rewrite H16; change - (pos_Rl (cons_Rlist (cons r2 r3) l2) (S i) = - pos_Rl l2 (S (S i - Rlength (cons r1 (cons r2 r3))))) - in H17; rewrite H17; assert (H20 := H13 (S i - Rlength l1)%nat); + (pos_Rl (app (cons r2 r3) l2) (S i) = + pos_Rl l2 (S (S i - length (cons r1 (cons r2 r3))))) + in H17; rewrite H17; assert (H20 := H13 (S i - length l1)%nat); unfold constant_D_eq, open_interval in H20; - assert (H21 : (S i - Rlength l1 < pred (Rlength l2))%nat). + assert (H21 : (S i - length l1 < pred (length l2))%nat). apply lt_pred; rewrite minus_Sn_m. - apply plus_lt_reg_l with (Rlength l1); rewrite <- le_plus_minus. + apply plus_lt_reg_l with (length l1); rewrite <- le_plus_minus. rewrite H19 in H1; simpl in H1; rewrite H19; simpl; - rewrite RList_P23 in H1; apply lt_n_S; assumption. + rewrite app_length in H1; apply lt_n_S; assumption. apply le_trans with (S i); [ apply le_S_n; assumption | apply le_n_Sn ]. apply le_S_n; assumption. assert (H22 := H20 H21); repeat rewrite H22. reflexivity. rewrite <- H19; assert - (H23 : pos_Rl l2 (S i - Rlength l1) <= pos_Rl l2 (S (S i - Rlength l1))). + (H23 : pos_Rl l2 (S i - length l1) <= pos_Rl l2 (S (S i - length l1))). apply H7; apply lt_pred. rewrite minus_Sn_m. - apply plus_lt_reg_l with (Rlength l1); rewrite <- le_plus_minus. + apply plus_lt_reg_l with (length l1); rewrite <- le_plus_minus. rewrite H19 in H1; simpl in H1; rewrite H19; simpl; - rewrite RList_P23 in H1; apply lt_n_S; assumption. + rewrite app_length in H1; apply lt_n_S; assumption. apply le_trans with (S i); [ apply le_S_n; assumption | apply le_n_Sn ]. apply le_S_n; assumption. elim H23; intro. @@ -2115,7 +2121,7 @@ Proof. [ prove_sup0 | unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; - [ rewrite Rmult_1_l; rewrite (Rplus_comm (pos_Rl l2 (S i - Rlength l1))); + [ rewrite Rmult_1_l; rewrite (Rplus_comm (pos_Rl l2 (S i - length l1))); rewrite double; apply Rplus_lt_compat_l; assumption | discrR ] ]. rewrite <- H19 in H16; rewrite <- H19 in H17; elim H2; intros; @@ -2123,11 +2129,11 @@ Proof. simpl in H16; rewrite H16 in H25; simpl in H26; simpl in H17; rewrite H17 in H26; simpl in H24; rewrite H24 in H25; elim (Rlt_irrefl _ (Rlt_trans _ _ _ H25 H26)). - assert (H23 : pos_Rl (cons_Rlist l1 l2) (S i) = pos_Rl l2 (S i - Rlength l1)). + assert (H23 : pos_Rl (app l1 l2) (S i) = pos_Rl l2 (S i - length l1)). rewrite H19; simpl; simpl in H16; apply H16. assert (H24 : - pos_Rl (cons_Rlist l1 l2) (S (S i)) = pos_Rl l2 (S (S i - Rlength l1))). + pos_Rl (app l1 l2) (S (S i)) = pos_Rl l2 (S (S i - length l1))). rewrite H19; simpl; simpl in H17; apply H17. rewrite <- H23; rewrite <- H24; assumption. simpl; rewrite H19 in H1; simpl in H1; apply lt_S_n; assumption. @@ -2141,7 +2147,7 @@ Proof. intros f a b c H H0 (l1,(lf1,H1)) (l2,(lf2,H2)); destruct (total_order_T a b) as [[Hltab|Hab]|Hgtab]. destruct (total_order_T b c) as [[Hltbc|Hbc]|Hgtbc]. - exists (cons_Rlist l1 l2); exists (FF (cons_Rlist l1 l2) f); + exists (app l1 l2); exists (FF (app l1 l2) f); apply StepFun_P40 with b lf1 lf2; assumption. exists l1; exists lf1; rewrite Hbc in H1; assumption. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 Hgtbc)). @@ -2150,9 +2156,9 @@ Proof. Qed. Lemma StepFun_P42 : - forall (l1 l2:Rlist) (f:R -> R), - pos_Rl l1 (pred (Rlength l1)) = pos_Rl l2 0 -> - Int_SF (FF (cons_Rlist l1 l2) f) (cons_Rlist l1 l2) = + forall (l1 l2:list R) (f:R -> R), + pos_Rl l1 (pred (length l1)) = pos_Rl l2 0 -> + Int_SF (FF (app l1 l2) f) (app l1 l2) = Int_SF (FF l1 f) l1 + Int_SF (FF l2 f) l2. Proof. intros l1 l2 f; induction l1 as [| r l1 IHl1]; intros H; @@ -2193,7 +2199,7 @@ Proof. elim Hle; intro. elim Hle'; intro. replace (Int_SF lf3 l3) with - (Int_SF (FF (cons_Rlist l1 l2) f) (cons_Rlist l1 l2)). + (Int_SF (FF (app l1 l2) f) (app l1 l2)). replace (Int_SF lf1 l1) with (Int_SF (FF l1 f) l1). replace (Int_SF lf2 l2) with (Int_SF (FF l2 f) l2). symmetry ; apply StepFun_P42. @@ -2225,7 +2231,7 @@ Proof. elim Hle''; intro. rewrite Rplus_comm; replace (Int_SF lf1 l1) with - (Int_SF (FF (cons_Rlist l3 l2) f) (cons_Rlist l3 l2)). + (Int_SF (FF (app l3 l2) f) (app l3 l2)). replace (Int_SF lf3 l3) with (Int_SF (FF l3 f) l3). replace (Int_SF lf2 l2) with (Int_SF (FF l2 f) l2). apply StepFun_P42. @@ -2249,7 +2255,7 @@ Proof. ring. elim Hle; intro. replace (Int_SF lf2 l2) with - (Int_SF (FF (cons_Rlist l3 l1) f) (cons_Rlist l3 l1)). + (Int_SF (FF (app l3 l1) f) (app l3 l1)). replace (Int_SF lf3 l3) with (Int_SF (FF l3 f) l3). replace (Int_SF lf1 l1) with (Int_SF (FF l1 f) l1). symmetry ; apply StepFun_P42. @@ -2277,7 +2283,7 @@ Proof. ring. rewrite Rplus_comm; elim Hle''; intro. replace (Int_SF lf2 l2) with - (Int_SF (FF (cons_Rlist l1 l3) f) (cons_Rlist l1 l3)). + (Int_SF (FF (app l1 l3) f) (app l1 l3)). replace (Int_SF lf3 l3) with (Int_SF (FF l3 f) l3). replace (Int_SF lf1 l1) with (Int_SF (FF l1 f) l1). symmetry ; apply StepFun_P42. @@ -2304,7 +2310,7 @@ Proof. ring. elim Hle'; intro. replace (Int_SF lf1 l1) with - (Int_SF (FF (cons_Rlist l2 l3) f) (cons_Rlist l2 l3)). + (Int_SF (FF (app l2 l3) f) (app l2 l3)). replace (Int_SF lf3 l3) with (Int_SF (FF l3 f) l3). replace (Int_SF lf2 l2) with (Int_SF (FF l2 f) l2). symmetry ; apply StepFun_P42. @@ -2334,7 +2340,7 @@ Proof. replace (Int_SF lf3 l3) with (Int_SF lf2 l2 + Int_SF lf1 l1). ring. replace (Int_SF lf3 l3) with - (Int_SF (FF (cons_Rlist l2 l1) f) (cons_Rlist l2 l1)). + (Int_SF (FF (app l2 l1) f) (app l2 l1)). replace (Int_SF lf1 l1) with (Int_SF (FF l1 f) l1). replace (Int_SF lf2 l2) with (Int_SF (FF l2 f) l2). symmetry ; apply StepFun_P42. @@ -2395,17 +2401,17 @@ Proof. elim H; clear H; intros; unfold IsStepFun in X; unfold is_subdivision in X; elim X; clear X; intros l1 [lf1 H2]; cut - (forall (l1 lf1:Rlist) (a b c:R) (f:R -> R), + (forall (l1 lf1:list R) (a b c:R) (f:R -> R), adapted_couple f a b l1 lf1 -> a <= c <= b -> - { l:Rlist & { l0:Rlist & adapted_couple f a c l l0 } }). + { l:list R & { l0:list R & adapted_couple f a c l l0 } }). intro X; unfold IsStepFun; unfold is_subdivision; eapply X. apply H2. split; assumption. clear f a b c H0 H H1 H2 l1 lf1; simple induction l1. intros; unfold adapted_couple in H; decompose [and] H; clear H; simpl in H4; discriminate. - simple induction r0. + intros r r0; elim r0. intros X lf1 a b c f H H0; assert (H1 : a = b). unfold adapted_couple in H; decompose [and] H; clear H; simpl in H3; simpl in H2; assert (H7 : a <= b). @@ -2438,7 +2444,7 @@ Proof. unfold constant_D_eq, open_interval; intros; simpl in H8; inversion H8. simpl; assert (H10 := H7 0%nat); - assert (H12 : (0 < pred (Rlength (cons r (cons r1 r2))))%nat). + assert (H12 : (0 < pred (length (cons r (cons r1 r2))))%nat). simpl; apply lt_O_Sn. apply (H10 H12); unfold open_interval; simpl; rewrite H11 in H9; simpl in H9; elim H9; clear H9; @@ -2479,7 +2485,7 @@ Proof. intros; simpl in H; unfold constant_D_eq, open_interval; intros; induction i as [| i Hreci]. simpl; assert (H17 := H10 0%nat); - assert (H18 : (0 < pred (Rlength (cons r (cons r1 r2))))%nat). + assert (H18 : (0 < pred (length (cons r (cons r1 r2))))%nat). simpl; apply lt_O_Sn. apply (H17 H18); unfold open_interval; simpl; simpl in H4; elim H4; clear H4; intros; split; try assumption; @@ -2507,16 +2513,16 @@ Proof. elim H; clear H; intros; unfold IsStepFun in X; unfold is_subdivision in X; elim X; clear X; intros l1 [lf1 H2]; cut - (forall (l1 lf1:Rlist) (a b c:R) (f:R -> R), + (forall (l1 lf1:list R) (a b c:R) (f:R -> R), adapted_couple f a b l1 lf1 -> a <= c <= b -> - { l:Rlist & { l0:Rlist & adapted_couple f c b l l0 } }). + { l:list R & { l0:list R & adapted_couple f c b l l0 } }). intro X; unfold IsStepFun; unfold is_subdivision; eapply X; [ apply H2 | split; assumption ]. clear f a b c H0 H H1 H2 l1 lf1; simple induction l1. intros; unfold adapted_couple in H; decompose [and] H; clear H; simpl in H4; discriminate. - simple induction r0. + intros r r0; elim r0. intros X lf1 a b c f H H0; assert (H1 : a = b). unfold adapted_couple in H; decompose [and] H; clear H; simpl in H3; simpl in H2; assert (H7 : a <= b). diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v index d21042884e..fa5442e86f 100644 --- a/theories/Reals/Rtopology.v +++ b/theories/Reals/Rtopology.v @@ -12,6 +12,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis1. Require Import RList. +Require Import List. Require Import Classical_Prop. Require Import Classical_Pred_Type. Local Open Scope R_scope. @@ -388,7 +389,7 @@ Record family : Type := mkfamily Definition family_open_set (f:family) : Prop := forall x:R, open_set (f x). Definition domain_finite (D:R -> Prop) : Prop := - exists l : Rlist, (forall x:R, D x <-> In x l). + exists l : list R, (forall x:R, D x <-> In x l). Definition family_finite (f:family) : Prop := domain_finite (ind f). @@ -669,7 +670,7 @@ Proof. intro H14; simpl in H14; unfold intersection_domain in H14; specialize H13 with x0; destruct H13 as (H13,H15); destruct (Req_dec x0 y0) as [H16|H16]. - simpl; left; apply H16. + simpl; left. symmetry; apply H16. simpl; right; apply H13. simpl; unfold intersection_domain; unfold Db in H14; decompose [and or] H14. @@ -678,8 +679,8 @@ Proof. intro H14; simpl in H14; destruct H14 as [H15|H15]; simpl; unfold intersection_domain. split. - apply (cond_fam f0); rewrite H15; exists b; apply H6. - unfold Db; right; assumption. + apply (cond_fam f0); rewrite <- H15; exists b; apply H6. + unfold Db; right; symmetry; assumption. simpl; unfold intersection_domain; elim (H13 x0). intros _ H16; assert (H17 := H16 H15); simpl in H17; unfold intersection_domain in H17; split. @@ -750,15 +751,15 @@ Proof. intro H14; simpl in H14; unfold intersection_domain in H14; specialize (H13 x0); destruct H13 as (H13,H15); destruct (Req_dec x0 y0) as [Heq|Hneq]. - simpl; left; apply Heq. + simpl; left; symmetry; apply Heq. simpl; right; apply H13; simpl; unfold intersection_domain; unfold Db in H14; decompose [and or] H14. split; assumption. elim Hneq; assumption. intros [H15|H15]. split. - apply (cond_fam f0); rewrite H15; exists m; apply H6. - unfold Db; right; assumption. + apply (cond_fam f0); rewrite <- H15; exists m; apply H6. + unfold Db; right; symmetry; assumption. elim (H13 x0); intros _ H16. assert (H17 := H16 H15). simpl in H17. @@ -810,9 +811,10 @@ Proof. unfold family_finite; unfold domain_finite; exists (cons y0 nil); intro; split. simpl; unfold intersection_domain; intros (H3,H4). - unfold D' in H4; left; apply H4. + unfold D' in H4; left; symmetry; apply H4. simpl; unfold intersection_domain; intros [H4|[]]. - split; [ rewrite H4; apply (cond_fam f0); exists a; apply H2 | apply H4 ]. + split; [ rewrite <- H4; apply (cond_fam f0); exists a; apply H2 | + symmetry; apply H4 ]. split; [ right; reflexivity | apply Hle ]. apply compact_eqDom with (fun c:R => False). apply compact_EMP. diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 2140014c58..745cf950b5 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -20,7 +20,6 @@ open Minisys As of today, this module depends on the following Coq modules: - - Flags - Envars - CoqProject_file @@ -28,10 +27,7 @@ open Minisys coqlib handling up so this can be bootstrapped earlier. *) -let option_D = ref false -let option_w = ref false let option_sort = ref false -let option_dump = ref None let warning_mult suf iter = let tab = Hashtbl.create 151 in @@ -74,378 +70,10 @@ let sort () = in List.iter (fun (name,_) -> loop name) !vAccu -let (dep_tab : (string,string list) Hashtbl.t) = Hashtbl.create 151 - -let mL_dep_list b f = - try - Hashtbl.find dep_tab f - with Not_found -> - let deja_vu = ref ([] : string list) in - try - let chan = open_in f in - let buf = Lexing.from_channel chan in - try - while true do - let (Use_module str) = caml_action buf in - if str = b then begin - coqdep_warning "in file %s the notation %s. is useless !\n" f b - end else - if not (List.mem str !deja_vu) then addQueue deja_vu str - done; [] - with Fin_fichier -> begin - close_in chan; - let rl = List.rev !deja_vu in - Hashtbl.add dep_tab f rl; - rl - end - with Sys_error _ -> [] - -let affiche_Declare f dcl = - printf "\n*** In file %s: \n" f; - printf "Declare ML Module"; - List.iter (fun str -> printf " \"%s\"" str) dcl; - printf ".\n%!" - -let warning_Declare f dcl = - eprintf "*** Warning : in file %s, the ML modules declaration should be\n" f; - eprintf "*** Declare ML Module"; - List.iter (fun str -> eprintf " \"%s\"" str) dcl; - eprintf ".\n%!" - -let traite_Declare f = - let decl_list = ref ([] : string list) in - let rec treat = function - | s :: ll -> - let s' = basename_noext s in - (match search_ml_known s with - | Some mldir when not (List.mem s' !decl_list) -> - let fullname = file_name s' mldir in - let depl = mL_dep_list s (fullname ^ ".ml") in - treat depl; - decl_list := s :: !decl_list - | _ -> ()); - treat ll - | [] -> () - in - try - let chan = open_in f in - let buf = Lexing.from_channel chan in - begin try - while true do - let tok = coq_action buf in - (match tok with - | Declare sl -> - decl_list := []; - treat sl; - decl_list := List.rev !decl_list; - if !option_D then - affiche_Declare f !decl_list - else if !decl_list <> sl then - warning_Declare f !decl_list - | _ -> ()) - done - with Fin_fichier -> () end; - close_in chan - with Sys_error _ -> () - -let declare_dependencies () = - List.iter - (fun (name,_) -> - traite_Declare (name^".v"); - pp_print_flush std_formatter ()) - (List.rev !vAccu) - -(** DAGs guaranteed to be transitive reductions *) -module DAG (Node : Set.OrderedType) : -sig - type node = Node.t - type t - val empty : t - val add_transitive_edge : node -> node -> t -> t - val iter : (node -> node -> unit) -> t -> unit -end = -struct - type node = Node.t - module NSet = Set.Make(Node) - module NMap = Map.Make(Node) - - (** Associate to a node the set of its neighbours *) - type _t = NSet.t NMap.t - - (** Optimisation: construct the reverse graph at the same time *) - type t = { dir : _t; rev : _t; } - - - let node_equal x y = Node.compare x y = 0 - - let add_edge x y graph = - let set = try NMap.find x graph with Not_found -> NSet.empty in - NMap.add x (NSet.add y set) graph - - let remove_edge x y graph = - let set = try NMap.find x graph with Not_found -> NSet.empty in - let set = NSet.remove y set in - if NSet.is_empty set then NMap.remove x graph - else NMap.add x set graph - - let has_edge x y graph = - let set = try NMap.find x graph with Not_found -> NSet.empty in - NSet.mem y set - - let connected x y graph = - let rec aux rem seen = - if NSet.is_empty rem then false - else - let x = NSet.choose rem in - if node_equal x y then true - else - let rem = NSet.remove x rem in - if NSet.mem x seen then - aux rem seen - else - let seen = NSet.add x seen in - let next = try NMap.find x graph with Not_found -> NSet.empty in - let rem = NSet.union next rem in - aux rem seen - in - aux (NSet.singleton x) NSet.empty - - (** Check whether there is a path from a to b going through the edge - x -> y. *) - let connected_through a b x y graph = - let rec aux rem seen = - if NMap.is_empty rem then false - else - let (n, through) = NMap.choose rem in - if node_equal n b && through then true - else - let rem = NMap.remove n rem in - let is_seen = try Some (NMap.find n seen) with Not_found -> None in - match is_seen with - | None -> - let seen = NMap.add n through seen in - let next = try NMap.find n graph with Not_found -> NSet.empty in - let is_x = node_equal n x in - let push m accu = - let through = through || (is_x && node_equal m y) in - NMap.add m through accu - in - let rem = NSet.fold push next rem in - aux rem seen - | Some false -> - (* The path we took encountered x -> y but not the one in seen *) - if through then aux (NMap.add n true rem) (NMap.add n true seen) - else aux rem seen - | Some true -> aux rem seen - in - aux (NMap.singleton a false) NMap.empty - - let closure x graph = - let rec aux rem seen = - if NSet.is_empty rem then seen - else - let x = NSet.choose rem in - let rem = NSet.remove x rem in - if NSet.mem x seen then - aux rem seen - else - let seen = NSet.add x seen in - let next = try NMap.find x graph with Not_found -> NSet.empty in - let rem = NSet.union next rem in - aux rem seen - in - aux (NSet.singleton x) NSet.empty - - let empty = { dir = NMap.empty; rev = NMap.empty; } - - (** Online transitive reduction algorithm *) - let add_transitive_edge x y graph = - if connected x y graph.dir then graph - else - let dir = add_edge x y graph.dir in - let rev = add_edge y x graph.rev in - let graph = { dir; rev; } in - let ancestors = closure x rev in - let descendents = closure y dir in - let fold_ancestor a graph = - let fold_descendent b graph = - let to_remove = has_edge a b graph.dir in - let to_remove = to_remove && not (node_equal x a && node_equal y b) in - let to_remove = to_remove && connected_through a b x y graph.dir in - if to_remove then - let dir = remove_edge a b graph.dir in - let rev = remove_edge b a graph.rev in - { dir; rev; } - else graph - in - NSet.fold fold_descendent descendents graph - in - NSet.fold fold_ancestor ancestors graph - - let iter f graph = - let iter x set = NSet.iter (fun y -> f x y) set in - NMap.iter iter graph.dir - -end - -module Graph = -struct -(** Dumping a dependency graph **) - -module DAG = DAG(struct type t = string let compare = compare end) - -(** TODO: we should share this code with Coqdep_common *) -module VData = struct - type t = string list option * string list - let compare = Util.pervasives_compare -end - -module VCache = Set.Make(VData) - -let treat_coq_file chan = - let buf = Lexing.from_channel chan in - let deja_vu_v = ref VCache.empty in - let deja_vu_ml = ref StrSet.empty in - let mark_v_done from acc str = - let seen = VCache.mem (from, str) !deja_vu_v in - if not seen then - let () = deja_vu_v := VCache.add (from, str) !deja_vu_v in - match search_v_known ?from str with - | None -> acc - | Some file_str -> (canonize file_str, !suffixe) :: acc - else acc - in - let rec loop acc = - let token = try Some (coq_action buf) with Fin_fichier -> None in - match token with - | None -> acc - | Some action -> - let acc = match action with - | Require (from, strl) -> - List.fold_left (fun accu v -> mark_v_done from accu v) acc strl - | Declare sl -> - let declare suff dir s = - let base = escape (file_name s dir) in - match !option_dynlink with - | No -> [] - | Byte -> [base,suff] - | Opt -> [base,".cmxs"] - | Both -> [base,suff; base,".cmxs"] - | Variable -> - if suff=".cmo" then [base,"$(DYNOBJ)"] - else [base,"$(DYNLIB)"] - in - let decl acc str = - let s = basename_noext str in - if not (StrSet.mem s !deja_vu_ml) then - let () = deja_vu_ml := StrSet.add s !deja_vu_ml in - match search_mllib_known s with - | Some mldir -> (declare ".cma" mldir s) @ acc - | None -> - match search_ml_known s with - | Some mldir -> (declare ".cmo" mldir s) @ acc - | None -> acc - else acc - in - List.fold_left decl acc sl - | Load str -> - let str = Filename.basename str in - let seen = VCache.mem (None, [str]) !deja_vu_v in - if not seen then - let () = deja_vu_v := VCache.add (None, [str]) !deja_vu_v in - match search_v_known [str] with - | None -> acc - | Some file_str -> (canonize file_str, ".v") :: acc - else acc - | AddLoadPath _ | AddRecLoadPath _ -> acc (* TODO *) - in - loop acc - in - loop [] - -let treat_coq_file f = - let chan = try Some (open_in f) with Sys_error _ -> None in - match chan with - | None -> [] - | Some chan -> - try - let ans = treat_coq_file chan in - let () = close_in chan in - ans - with Syntax_error (i, j) -> close_in chan; error_cannot_parse f (i, j) - -type graph = - | Element of string - | Subgraph of string * graph list - -let rec insert_graph name path graphs = match path, graphs with - | [] , graphs -> (Element name) :: graphs - | (box :: boxes), (Subgraph (hd, names)) :: tl when hd = box -> - Subgraph (hd, insert_graph name boxes names) :: tl - | _, hd :: tl -> hd :: (insert_graph name path tl) - | (box :: boxes), [] -> [ Subgraph (box, insert_graph name boxes []) ] - -let print_graphs chan graph = - let rec print_aux name = function - | [] -> name - | (Element str) :: tl -> fprintf chan "\"%s\";\n" str; print_aux name tl - | Subgraph (box, names) :: tl -> - fprintf chan "subgraph cluster%n {\nlabel=\"%s\";\n" name box; - let name = print_aux (name + 1) names in - fprintf chan "}\n"; print_aux name tl - in - ignore (print_aux 0 graph) - -let rec pop_common_prefix = function - | [Subgraph (_, graphs)] -> pop_common_prefix graphs - | graphs -> graphs - -let split_path = Str.split (Str.regexp "/") - -let rec pop_last = function - | [] -> [] - | [ x ] -> [] - | x :: xs -> x :: pop_last xs - -let get_boxes path = pop_last (split_path path) - -let insert_raw_graph file = - insert_graph file (get_boxes file) - -let rec get_dependencies name args = - let vdep = treat_coq_file (name ^ ".v") in - let fold (deps, graphs, alseen) (dep, _) = - let dag = DAG.add_transitive_edge name dep deps in - if not (List.mem dep alseen) then - get_dependencies dep (dag, insert_raw_graph dep graphs, dep :: alseen) - else - (dag, graphs, alseen) - in - List.fold_left fold args vdep - -let coq_dependencies_dump chan dumpboxes = - let (deps, graphs, _) = - List.fold_left (fun ih (name, _) -> get_dependencies name ih) - (DAG.empty, List.fold_left (fun ih (file, _) -> insert_raw_graph file ih) [] !vAccu, - List.map fst !vAccu) !vAccu - in - fprintf chan "digraph dependencies {\n"; - if dumpboxes then print_graphs chan (pop_common_prefix graphs) - else List.iter (fun (name, _) -> fprintf chan "\"%s\"[label=\"%s\"]\n" name (basename_noext name)) !vAccu; - DAG.iter (fun name dep -> fprintf chan "\"%s\" -> \"%s\"\n" dep name) deps; - fprintf chan "}\n%!" - -end - let usage () = eprintf " usage: coqdep [options] <filename>+\n"; eprintf " options:\n"; eprintf " -c : Also print the dependencies of caml modules (=ocamldep).\n"; - (* Does not work anymore *) - (* eprintf " -w : Print informations on missing or wrong \"Declare - ML Module\" commands in coq files.\n"; *) - (* Does not work anymore: *) - (* eprintf " -D : Prints the missing ocmal module names. No dependency computed.\n"; *) eprintf " -boot : For coq developers, prints dependencies over coq library files (omitted by default).\n"; eprintf " -sort : output the given file name ordered by dependencies\n"; eprintf " -noglob | -no-glob : \n"; @@ -456,8 +84,6 @@ let usage () = eprintf " -R dir logname : add and import dir recursively to coq load path under logical name logname\n"; eprintf " -Q dir logname : add (recursively) and open (non recursively) dir to coq load path under logical name logname\n"; eprintf " -vos : also output dependencies about .vos files\n"; - eprintf " -dumpgraph f : print a dot dependency graph in file 'f'\n"; - eprintf " -dumpgraphbox f : print a dot dependency graph box in file 'f'\n"; eprintf " -exclude-dir dir : skip subdirectories named 'dir' during -R/-Q search\n"; eprintf " -coqlib dir : set the coq standard library directory\n"; eprintf " -suffix s : \n"; @@ -468,7 +94,6 @@ let usage () = let split_period = Str.split (Str.regexp (Str.quote ".")) let add_q_include path l = add_rec_dir_no_import add_known path (split_period l) - let add_r_include path l = add_rec_dir_import add_known path (split_period l) let treat_coqproject f = @@ -482,9 +107,8 @@ let treat_coqproject f = iter_sourced (fun f -> treat_file None f) (all_files project) let rec parse = function + (* TODO, deprecate option -c *) | "-c" :: ll -> option_c := true; parse ll - | "-D" :: ll -> option_D := true; parse ll - | "-w" :: ll -> option_w := true; parse ll | "-boot" :: ll -> option_boot := true; parse ll | "-sort" :: ll -> option_sort := true; parse ll | "-vos" :: ll -> write_vos := true; parse ll @@ -495,17 +119,12 @@ let rec parse = function | "-R" :: r :: ln :: ll -> add_r_include r ln; parse ll | "-Q" :: r :: ln :: ll -> add_q_include r ln; parse ll | "-R" :: ([] | [_]) -> usage () - | "-dumpgraph" :: f :: ll -> option_dump := Some (false, f); parse ll - | "-dumpgraphbox" :: f :: ll -> option_dump := Some (true, f); parse ll | "-exclude-dir" :: r :: ll -> System.exclude_directory r; parse ll | "-exclude-dir" :: [] -> usage () | "-coqlib" :: r :: ll -> Envars.set_user_coqlib r; parse ll | "-coqlib" :: [] -> usage () | "-suffix" :: s :: ll -> suffixe := s ; parse ll | "-suffix" :: [] -> usage () - | "-slash" :: ll -> - coqdep_warning "warning: option -slash has no effect and is deprecated."; - parse ll | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll @@ -525,19 +144,8 @@ let coqdep () = (* Add current dir with empty logical path if not set by options above. *) (try ignore (Coqdep_common.find_dir_logpath (Sys.getcwd())) with Not_found -> add_norec_dir_import add_known "." []); - (* NOTE: These directories are searched from last to first *) - if !option_boot then begin - add_rec_dir_import add_known "theories" ["Coq"]; - add_rec_dir_import add_known "plugins" ["Coq"]; - add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"]; - add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"]; - let user = "user-contrib" in - if Sys.file_exists user then begin - add_rec_dir_no_import add_known user []; - add_rec_dir_no_import (fun _ -> add_caml_known) user []; - end; - end else begin - (* option_boot is actually always false in this branch *) + (* We don't setup any loadpath if the -boot is passed *) + if not !option_boot then begin Envars.set_coqlib ~fail:(fun msg -> raise (CoqlibError msg)); let coqlib = Envars.coqlib () in add_rec_dir_import add_coqlib_known (coqlib//"theories") ["Coq"]; @@ -554,17 +162,9 @@ let coqdep () = warning_mult ".mli" iter_mli_known; warning_mult ".ml" iter_ml_known; if !option_sort then begin sort (); exit 0 end; - if !option_c && not !option_D then mL_dependencies (); - if not !option_D then coq_dependencies (); - if !option_w || !option_D then declare_dependencies (); - begin match !option_dump with - | None -> () - | Some (box, file) -> - let chan = open_out file in - let chan_fmt = formatter_of_out_channel chan in - try Graph.coq_dependencies_dump chan_fmt box; close_out chan - with e -> close_out chan; raise e - end + if !option_c then mL_dependencies (); + coq_dependencies (); + () let _ = try diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml index 1730dd3d68..1cebb3638e 100644 --- a/tools/coqdep_boot.ml +++ b/tools/coqdep_boot.ml @@ -19,6 +19,7 @@ open Coqdep_common let split_period = Str.split (Str.regexp (Str.quote ".")) let add_q_include path l = add_rec_dir_no_import add_known path (split_period l) +let add_r_include path l = add_rec_dir_import add_known path (split_period l) let rec parse = function | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll @@ -26,16 +27,14 @@ let rec parse = function | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll | "-dyndep" :: "both" :: ll -> option_dynlink := Both; parse ll | "-dyndep" :: "var" :: ll -> option_dynlink := Variable; parse ll - | "-c" :: ll -> option_c := true; parse ll | "-boot" :: ll -> parse ll (* We're already in boot mode by default *) - | "-mldep" :: ocamldep :: ll -> - option_mldep := Some ocamldep; option_c := true; parse ll | "-I" :: r :: ll -> (* To solve conflict (e.g. same filename in kernel and checker) we allow to state an explicit order *) add_caml_dir r; norec_dirs := StrSet.add r !norec_dirs; parse ll + | "-R" :: r :: ln :: ll -> add_r_include r ln; parse ll | "-Q" :: r :: ln :: ll -> add_q_include r ln; parse ll | f :: ll -> treat_file None f; parse ll | [] -> () @@ -44,16 +43,4 @@ let _ = let () = option_boot := true in if Array.length Sys.argv < 2 then exit 1; parse (List.tl (Array.to_list Sys.argv)); - if !option_c then begin - add_rec_dir_import add_known "." []; - add_rec_dir_import (fun _ -> add_caml_known) "." ["Coq"]; - end - else begin - add_rec_dir_import add_known "theories" ["Coq"]; - add_rec_dir_import add_known "plugins" ["Coq"]; - add_caml_dir "tactics"; - add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"]; - add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"]; - end; - if !option_c then mL_dependencies (); coq_dependencies () diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 775c528176..bd72a52adf 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -35,7 +35,6 @@ let option_c = ref false let option_noglob = ref false let option_dynlink = ref Both let option_boot = ref false -let option_mldep = ref None let norec_dirs = ref StrSet.empty @@ -246,26 +245,7 @@ let depend_ML str = (" "^mlifile^".cmi"," "^mlifile^".cmi") | None, None -> "", "" -let soustraite_fichier_ML dep md ext = - try - let chan = open_process_in (dep^" -modules "^md^ext) in - let list = ocamldep_parse (Lexing.from_channel chan) in - let a_faire = ref "" in - let a_faire_opt = ref "" in - List.iter - (fun str -> - let byte,opt = depend_ML str in - a_faire := !a_faire ^ byte; - a_faire_opt := !a_faire_opt ^ opt) - (List.rev list); - (!a_faire, !a_faire_opt) - with - | Sys_error _ -> ("","") - | _ -> - Printf.eprintf "Coqdep: subprocess %s failed on file %s%s\n" dep md ext; - exit 1 - -let autotraite_fichier_ML md ext = +let traite_fichier_ML md ext = try let chan = open_in (md ^ ext) in let buf = Lexing.from_channel chan in @@ -290,11 +270,6 @@ let autotraite_fichier_ML md ext = (!a_faire, !a_faire_opt) with Sys_error _ -> ("","") -let traite_fichier_ML md ext = - match !option_mldep with - | Some dep -> soustraite_fichier_ML dep md ext - | None -> autotraite_fichier_ML md ext - let traite_fichier_modules md ext = try let chan = open_in (md ^ ext) in diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 6d49f7e06c..96266b8e36 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -30,7 +30,6 @@ val write_vos : bool ref type dynlink = Opt | Byte | Both | No | Variable val option_dynlink : dynlink ref -val option_mldep : string option ref val norec_dirs : StrSet.t ref val suffixe : string ref type dir = string option diff --git a/vernac/himsg.ml b/vernac/himsg.ml index eb39564fed..17c3e0395a 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1216,8 +1216,12 @@ let error_bad_entry () = let error_large_non_prop_inductive_not_in_type () = str "Large non-propositional inductive types must be in Type." -let error_inductive_bad_univs () = - str "Incorrect universe constraints declared for inductive type." +let error_inductive_missing_constraints (us,ind_univ) = + let pr_u = Univ.Universe.pr_with UnivNames.pr_with_global_universes in + str "Missing universe constraint declared for inductive type:" ++ spc() + ++ v 0 (prlist_with_sep spc (fun u -> + hov 0 (pr_u u ++ str " <= " ++ pr_u ind_univ)) + (Univ.Universe.Set.elements us)) (* Recursion schemes errors *) @@ -1256,7 +1260,7 @@ let explain_inductive_error = function | BadEntry -> error_bad_entry () | LargeNonPropInductiveNotInType -> error_large_non_prop_inductive_not_in_type () - | BadUnivs -> error_inductive_bad_univs () + | MissingConstraints csts -> error_inductive_missing_constraints csts (* Recursion schemes errors *) diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 05e23164b1..0c39aba70a 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -126,7 +126,7 @@ let parse_format ({CAst.loc;v=str} : lstring) = let rec parse_non_format i = let n = nonspaces false 0 i in push_token (make_loc i (i+n-1)) (UnpTerminal (String.sub str i n)) (parse_token 1 (i+n)) - and parse_quoted n i = + and parse_quoted n k i = if i < len then match str.[i] with (* Parse " // " *) | '/' when i+1 < len && str.[i+1] == '/' -> @@ -140,7 +140,7 @@ let parse_format ({CAst.loc;v=str} : lstring) = (parse_token 1 (close_quotation i (i+p+1))) | c -> (* The spaces are real spaces *) - push_white i n (match c with + push_white (i-n-1-k) n (match c with | '[' -> if i+1 < len then match str.[i+1] with (* Parse " [h .. ", *) @@ -177,7 +177,7 @@ let parse_format ({CAst.loc;v=str} : lstring) = push_white (i-n) (n-k) (push_token (make_loc i (i+1)) (UnpTerminal "'") (parse_token 1 (i+1))) (* Parse the beginning of a quoted expression *) | '\'' -> - parse_quoted (n-k) (i+1) + parse_quoted (n-k) k (i+1) (* Otherwise *) | _ -> push_white (i-n) (n-k) (parse_non_format i) @@ -477,6 +477,9 @@ let warn_format_break = (fun () -> strbrk "Discarding format implicitly indicated by multiple spaces in notation because an explicit format modifier is given.") +let has_ldots l = + List.exists (function (_,UnpTerminal s) -> String.equal s (Id.to_string Notation_ops.ldots_var) | _ -> false) l + let rec split_format_at_ldots hd = function | (loc,UnpTerminal s) :: fmt when String.equal s (Id.to_string Notation_ops.ldots_var) -> loc, List.rev hd, fmt | u :: fmt -> @@ -504,11 +507,32 @@ let find_prod_list_loc sfmt fmt = (* A separator; we highlight the separating sequence *) Loc.merge_opt (fst (List.hd sfmt)) (fst (List.last sfmt)) +let is_blank s = + let n = String.length s in + let rec aux i s = i >= n || s.[i] = ' ' && aux (i+1) s in + aux 0 s + +let is_formatting = function + | (_,UnpCut _) -> true + | (_,UnpTerminal s) -> is_blank s + | _ -> false + +let rec is_var_in_recursive_format = function + | (_,UnpTerminal s) when not (is_blank s) -> true + | (loc,UnpBox (b,l)) -> + (match List.filter (fun a -> not (is_formatting a)) l with + | [a] -> is_var_in_recursive_format a + | _ -> error_not_same ?loc ()) + | _ -> false + +let rec check_eq_var_upto_name = function + | (_,UnpTerminal s1), (_,UnpTerminal s2) when not (is_blank s1 && is_blank s2) || s1 = s2 -> () + | (_,UnpBox (b1,l1)), (_,UnpBox (b2,l2)) when b1 = b2 -> List.iter check_eq_var_upto_name (List.combine l1 l2) + | (_,UnpCut b1), (_,UnpCut b2) when b1 = b2 -> () + | _, (loc,_) -> error_not_same ?loc () + let skip_var_in_recursive_format = function - | (_,UnpTerminal s) :: sl (* skip first var *) when not (List.for_all (fun c -> c = " ") (String.explode s)) -> - (* To do, though not so important: check that the names match - the names in the notation *) - sl + | a :: sl when is_var_in_recursive_format a -> a, sl | (loc,_) :: _ -> error_not_same ?loc () | [] -> assert false @@ -516,15 +540,20 @@ let read_recursive_format sl fmt = (* Turn [[UnpTerminal s :: some-list @ UnpTerminal ".." :: same-some-list @ UnpTerminal s' :: rest] *) (* into [(some-list,rest)] *) let get_head fmt = - let sl = skip_var_in_recursive_format fmt in - try split_format_at_ldots [] sl with Exit -> error_not_same ?loc:(fst (List.last (if sl = [] then fmt else sl))) () in + let var,sl = skip_var_in_recursive_format fmt in + try var, split_format_at_ldots [] sl + with Exit -> error_not_same ?loc:(fst (List.last (if sl = [] then fmt else sl))) () in let rec get_tail = function | (loc,a) :: sepfmt, (_,b) :: fmt when (=) a b -> get_tail (sepfmt, fmt) (* FIXME *) | [], tail -> skip_var_in_recursive_format tail | (loc,_) :: _, ([] | (_,UnpTerminal _) :: _)-> error_not_same ?loc () | _, (loc,_)::_ -> error_not_same ?loc () in - let loc, slfmt, fmt = get_head fmt in - slfmt, get_tail (slfmt, fmt) + let var1, (loc, slfmt, fmt) = get_head fmt in + let var2, res = get_tail (slfmt, fmt) in + check_eq_var_upto_name (var1,var2); + (* To do, though not so important: check that the names match + the names in the notation *) + slfmt, res let hunks_of_format (from,(vars,typs)) symfmt = let rec aux = function @@ -537,13 +566,9 @@ let hunks_of_format (from,(vars,typs)) symfmt = | NonTerminal s :: symbs, (_,UnpTerminal s') :: fmt when Id.equal s (Id.of_string s') -> let i = index_id s vars in let symbs, l = aux (symbs,fmt) in symbs, unparsing_metavar i from typs :: l - | symbs, (_,UnpBox (a,b)) :: fmt -> - let symbs', b' = aux (symbs,b) in - let symbs', l = aux (symbs',fmt) in - symbs', UnpBox (a,List.map (fun x -> (None,x)) b') :: l | symbs, (_,(UnpCut _ as u)) :: fmt -> let symbs, l = aux (symbs,fmt) in symbs, u :: l - | SProdList (m,sl) :: symbs, fmt -> + | SProdList (m,sl) :: symbs, fmt when has_ldots fmt -> let i = index_id m vars in let typ = List.nth typs (i-1) in let _,prec = precedence_of_entry_type from typ in @@ -558,6 +583,10 @@ let hunks_of_format (from,(vars,typs)) symfmt = UnpBinderListMetaVar (i,isopen,slfmt) | _ -> assert false in symbs, hunk :: l + | symbs, (_,UnpBox (a,b)) :: fmt -> + let symbs', b' = aux (symbs,b) in + let symbs', l = aux (symbs',fmt) in + symbs', UnpBox (a,List.map (fun x -> (None,x)) b') :: l | symbs, [] -> symbs, [] | Break _ :: symbs, fmt -> warn_format_break (); aux (symbs,fmt) | _, fmt -> error_format ?loc:(fst (List.hd fmt)) () diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index c81a4abc1b..80b72225f0 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -124,7 +124,7 @@ module Proof_global = struct let () = CErrors.register_handler begin function | NoCurrentProof -> - CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).") + Pp.(str "No focused proof (No proof-editing in progress).") | _ -> raise CErrors.Unhandled end |