diff options
54 files changed, 472 insertions, 1594 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index bbd2d349c..384e46723 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -135,9 +135,6 @@ /plugins/firstorder/ @PierreCorbineau # Secondary maintainer @herbelin -/plugins/fourier/ @herbelin -# Secondary maintainer @gares - /plugins/funind/ @forestjulien # Secondary maintainer @Matafou @@ -306,7 +303,7 @@ /configure* @ejgallego -/META.coq @ejgallego +/META.coq.in @ejgallego /dev/build/windows @MSoegtropIMC # Secondary maintainer @maximedenes diff --git a/.gitignore b/.gitignore index 14ec71b93..0e41d6a77 100644 --- a/.gitignore +++ b/.gitignore @@ -179,3 +179,7 @@ test-suite/.nra.cache plugins/ssr/ssrparser.ml plugins/ssr/ssrvernac.ml + +# ocaml dev files +.merlin +META.coq @@ -39,6 +39,9 @@ Tactics still be used if you really want to ignore universe constraints. - Tactics and tactic notations now understand the `deprecated` attribute. +- The `fourier` tactic has been removed. Please now use `lra` instead. You + may need to add `Require Import Lra` to your developments. For compatibility, + we now define `fourier` as a deprecated alias of `lra`. Tools @@ -37,8 +37,6 @@ plugins/extraction developed by Pierre Letouzey (LRI, 2000-2004, PPS, 2005-now) plugins/firstorder developed by Pierre Corbineau (LRI, 2003-2008) -plugins/fourier - developed by Loïc Pottier (INRIA-Lemme, 2001) plugins/funind developed by Pierre Courtieu (INRIA-Lemme, 2003-2004, CNAM, 2006-now), Julien Forest (INRIA-Everest, 2006, CNAM, 2007-2008, ENSIIE, 2008-now) @@ -349,18 +349,6 @@ package "plugins" ( archive(native) = "newring_plugin.cmx" ) - package "fourier" ( - - description = "Coq fourier plugin" - version = "8.9" - - requires = "coq.plugins.ltac" - directory = "fourier" - - archive(byte) = "fourier_plugin.cmo" - archive(native) = "fourier_plugin.cmx" - ) - package "extraction" ( description = "Coq extraction plugin" @@ -80,7 +80,9 @@ export MLPACKFILES := $(call find, '*.mlpack') export ML4FILES := $(call find, '*.ml4') export MLGFILES := $(call find, '*.mlg') export CFILES := $(call findindir, 'kernel/byterun', '*.c') -export MERLINFILES := $(call find, '.merlin') + +export MERLININFILES := $(call find, '.merlin.in') +export MERLINFILES := $(MERLININFILES:.in=) # NB: The lists of currently existing .ml and .mli files will change # before and after a build or a make clean. Hence we do not export @@ -175,7 +177,7 @@ Makefile $(wildcard Makefile.*) config/Makefile : ; .PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean timingclean devdocclean alienclean -clean: objclean cruftclean depclean docclean devdocclean +clean: objclean cruftclean depclean docclean devdocclean camldevfilesclean cleankeepvo: indepclean clean-ide optclean cruftclean depclean docclean devdocclean @@ -185,6 +187,9 @@ cruftclean: ml4clean find . -name '*~' -o -name '*.annot' | xargs rm -f rm -f gmon.out core +camldevfilesclean: + rm -f $(MERLINFILES) META.coq + indepclean: rm -f $(GENFILES) rm -f $(COQTOPBYTE) $(CHICKENBYTE) $(TOPBYTE) diff --git a/Makefile.build b/Makefile.build index c100eda40..05633cecc 100644 --- a/Makefile.build +++ b/Makefile.build @@ -64,7 +64,7 @@ AFTER ?= # build the different subsystems: -world: coq coqide documentation revision +world: camldevfiles coq coqide documentation revision coq: coqlib coqbinaries tools diff --git a/Makefile.common b/Makefile.common index 727cb1e69..772561bd7 100644 --- a/Makefile.common +++ b/Makefile.common @@ -96,7 +96,7 @@ CORESRCDIRS:=\ PLUGINDIRS:=\ omega romega micromega quote \ - setoid_ring extraction fourier \ + setoid_ring extraction \ cc funind firstorder derive \ rtauto nsatz syntax btauto \ ssrmatching ltac ssr @@ -134,7 +134,6 @@ MICROMEGACMO:=plugins/micromega/micromega_plugin.cmo QUOTECMO:=plugins/quote/quote_plugin.cmo RINGCMO:=plugins/setoid_ring/newring_plugin.cmo NSATZCMO:=plugins/nsatz/nsatz_plugin.cmo -FOURIERCMO:=plugins/fourier/fourier_plugin.cmo EXTRACTIONCMO:=plugins/extraction/extraction_plugin.cmo FUNINDCMO:=plugins/funind/recdef_plugin.cmo FOCMO:=plugins/firstorder/ground_plugin.cmo @@ -155,7 +154,7 @@ SSRCMO:=plugins/ssr/ssreflect_plugin.cmo PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \ $(QUOTECMO) $(RINGCMO) \ - $(FOURIERCMO) $(EXTRACTIONCMO) \ + $(EXTRACTIONCMO) \ $(CCCMO) $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \ $(FUNINDCMO) $(NSATZCMO) $(NATSYNTAXCMO) $(OTHERSYNTAXCMO) \ $(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO) diff --git a/Makefile.dev b/Makefile.dev index 8f7d21694..ea1a3d40a 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -15,7 +15,7 @@ # Debug printers in dev/ ######################### -.PHONY: devel printers +.PHONY: devel printers camldevfiles DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/checker_printers.cmo @@ -85,13 +85,27 @@ endif # But these partial targets could be quite handy for quick builds # of specific components of Coq. +########################################################################### +# OCaml dev files +########################################################################### +camldevfiles: $(MERLINFILES) META.coq + +.merlin: .merlin.in + cp -a "$<" "$@" + +%/.merlin: %/.merlin.in + cp -a "$<" "$@" + +META.coq: META.coq.in + cp -a "$<" "$@" + ############################### ### 1) general-purpose targets ############################### coqlight: theories-light tools coqbinaries -states: theories/Init/Prelude.vo +states: camldevfiles theories/Init/Prelude.vo miniopt: $(COQTOPEXE) pluginsopt minibyte: $(COQTOPBYTE) pluginsbyte @@ -174,7 +188,6 @@ MICROMEGAVO:=$(filter plugins/micromega/%, $(PLUGINSVO)) QUOTEVO:=$(filter plugins/quote/%, $(PLUGINSVO)) RINGVO:=$(filter plugins/setoid_ring/%, $(PLUGINSVO)) NSATZVO:=$(filter plugins/nsatz/%, $(PLUGINSVO)) -FOURIERVO:=$(filter plugins/fourier/%, $(PLUGINSVO)) FUNINDVO:=$(filter plugins/funind/%, $(PLUGINSVO)) BTAUTOVO:=$(filter plugins/btauto/%, $(PLUGINSVO)) RTAUTOVO:=$(filter plugins/rtauto/%, $(PLUGINSVO)) @@ -188,7 +201,6 @@ micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT) setoid_ring: $(RINGVO) $(RINGCMO) nsatz: $(NSATZVO) $(NSATZCMO) extraction: $(EXTRACTIONCMO) $(EXTRACTIONVO) -fourier: $(FOURIERVO) $(FOURIERCMO) funind: $(FUNINDCMO) $(FUNINDVO) cc: $(CCVO) $(CCCMO) rtauto: $(RTAUTOVO) $(RTAUTOCMO) @@ -196,7 +208,7 @@ btauto: $(BTAUTOVO) $(BTAUTOCMO) ltac: $(LTACVO) $(LTACCMO) .PHONY: omega micromega setoid_ring nsatz extraction -.PHONY: fourier funind cc rtauto btauto ltac +.PHONY: funind cc rtauto btauto ltac # For emacs: # Local Variables: diff --git a/configure.ml b/configure.ml index c08e8dfcc..7fd900d99 100644 --- a/configure.ml +++ b/configure.ml @@ -475,6 +475,7 @@ let coq_bin_annot_flag = if !prefs.bin_annot then "-bin-annot" else "" (* This variable can be overriden only for debug purposes, use with care. *) let coq_safe_string = "-safe-string" +let coq_strict_sequence = "-strict-sequence" let cflags = "-Wall -Wno-unused -g -O2" @@ -661,7 +662,7 @@ let coq_warn_error = (* Flags used to compile Coq and plugins (via coq_makefile) *) let caml_flags = - Printf.sprintf "-thread -rectypes %s %s %s %s" coq_warnings coq_annot_flag coq_bin_annot_flag coq_safe_string + Printf.sprintf "-thread -rectypes %s %s %s %s %s" coq_warnings coq_annot_flag coq_bin_annot_flag coq_safe_string coq_strict_sequence (* Flags used to compile Coq but _not_ plugins (via coq_makefile) *) let coq_caml_flags = diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index 2bec09de2..bccd3fefb 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -33,7 +33,7 @@ if [ -z "$GUESS_CHECKER" ]; then -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \ -I $COQTOP/plugins/cc -I $COQTOP/plugins/dp \ -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \ - -I $COQTOP/plugins/firstorder -I $COQTOP/plugins/fourier \ + -I $COQTOP/plugins/firstorder \ -I $COQTOP/plugins/funind -I $COQTOP/plugins/groebner \ -I $COQTOP/plugins/interface -I $COQTOP/plugins/micromega \ -I $COQTOP/plugins/omega -I $COQTOP/plugins/quote \ diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el index 70a9756e5..ec72f9650 100644 --- a/dev/tools/coqdev.el +++ b/dev/tools/coqdev.el @@ -33,7 +33,7 @@ (defun coqdev-default-directory () "Return the Coq repository containing `default-directory'." - (let ((dir (locate-dominating-file default-directory "META.coq"))) + (let ((dir (locate-dominating-file default-directory "META.coq.in"))) (when dir (expand-file-name dir)))) (defun coqdev-setup-compile-command () diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 0e9c23b9b..2407a9051 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -96,15 +96,14 @@ and checked to be :math:`-1`. .. tacn:: lra :name: lra -This tactic is searching for *linear* refutations using Fourier -elimination [#]_. As a result, this tactic explores a subset of the *Cone* -defined as + This tactic is searching for *linear* refutations using Fourier + elimination [#]_. As a result, this tactic explores a subset of the *Cone* + defined as - :math:`\mathit{LinCone}(S) =\left\{ \left. \sum_{p \in S} \alpha_p \times p~\right|~\alpha_p \mbox{ are positive constants} \right\}` + :math:`\mathit{LinCone}(S) =\left\{ \left. \sum_{p \in S} \alpha_p \times p~\right|~\alpha_p \mbox{ are positive constants} \right\}` -The deductive power of `lra` is the combined deductive power of -`ring_simplify` and `fourier`. There is also an overlap with the field -tactic *e.g.*, :math:`x = 10 * x / 10` is solved by `lra`. + The deductive power of :tacn:`lra` overlaps with the one of :tacn:`field` + tactic *e.g.*, :math:`x = 10 * x / 10` is solved by :tacn:`lra`. `lia`: a tactic for linear integer arithmetic diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index afb49413d..f23e04c3a 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -889,7 +889,7 @@ Notation Interpretation Some tactics for real numbers +++++++++++++++++++++++++++++ -In addition to the powerful ``ring``, ``field`` and ``fourier`` +In addition to the powerful ``ring``, ``field`` and ``lra`` tactics (see Chapter :ref:`tactics`), there are also: .. tacn:: discrR diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index ec085a71e..562f8568d 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -4319,21 +4319,6 @@ printed with the Print Fields command. See also: file plugins/setoid_ring/RealField.v for an example of instantiation, theory theories/Reals for many examples of use of field. -.. tacn:: fourier - :name: fourier - -This tactic written by Loïc Pottier solves linear inequalities on real -numbers using Fourier’s method :cite:`Fourier`. This tactic must be loaded by -``Require Import Fourier``. - -.. example:: - .. coqtop:: reset all - - Require Import Reals. - Require Import Fourier. - Goal forall x y:R, (x < y)%R -> (y + 1 >= x - 1)%R. - intros; fourier. - Non-logical tactics ------------------------ diff --git a/ide/.merlin b/ide/.merlin.in index 953b5dce4..953b5dce4 100644 --- a/ide/.merlin +++ b/ide/.merlin.in diff --git a/ide/MacOS/default_accel_map b/ide/MacOS/default_accel_map index 47612cdf7..54a592a04 100644 --- a/ide/MacOS/default_accel_map +++ b/ide/MacOS/default_accel_map @@ -217,7 +217,6 @@ ; (gtk_accel_path "<Actions>/Tactics/Tactic casetype" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic cbv in" "") ; (gtk_accel_path "<Actions>/Templates/Template Load" "") -; (gtk_accel_path "<Actions>/Tactics/Tactic fourier" "") ; (gtk_accel_path "<Actions>/Templates/Template Goal" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic exists" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic decompose record" "") diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index f5dba2085..b0bafb793 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -311,7 +311,6 @@ let tactics = "fix __ with"; "fold"; "fold __ in"; - "fourier"; "functional induction"; ]; diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml index 9f5c99244..d554bebdd 100644 --- a/ide/gtk_parsing.ml +++ b/ide/gtk_parsing.ml @@ -35,8 +35,11 @@ let find_word_start (it:GText.iter) = (Minilib.log "find_word_start: cannot backward"; it) else if is_word_char it#char then step_to_start it - else (it#nocopy#forward_char; - Minilib.log ("Word start at: "^(string_of_int it#offset));it) + else begin + ignore(it#nocopy#forward_char); + Minilib.log ("Word start at: "^(string_of_int it#offset)); + it + end in step_to_start it#copy diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1f37d6367..cb50245d5 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -552,7 +552,7 @@ let find_fresh_name renaming (terms,termlists,binders,binderlists) avoid id = let is_var store pat = match DAst.get pat with - | PatVar na -> store na; true + | PatVar na -> ignore(store na); true | _ -> false let out_var pat = diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 39f7de942..ec6c5b297 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -278,7 +278,6 @@ type primitive = | Mk_rel of int | Mk_var of Id.t | Mk_proj - | Is_accu | Is_int | Cast_accu | Upd_cofix @@ -319,7 +318,6 @@ let eq_primitive p1 p2 = | Mk_cofix i1, Mk_cofix i2 -> Int.equal i1 i2 | Mk_rel i1, Mk_rel i2 -> Int.equal i1 i2 | Mk_var id1, Mk_var id2 -> Id.equal id1 id2 - | Is_accu, Is_accu -> true | Cast_accu, Cast_accu -> true | Upd_cofix, Upd_cofix -> true | Force_cofix, Force_cofix -> true @@ -345,7 +343,6 @@ let primitive_hash = function combinesmall 8 (Int.hash i) | Mk_var id -> combinesmall 9 (Id.hash id) - | Is_accu -> 10 | Is_int -> 11 | Cast_accu -> 12 | Upd_cofix -> 13 @@ -396,6 +393,7 @@ type mllambda = | MLsetref of string * mllambda | MLsequence of mllambda * mllambda | MLarray of mllambda array + | MLisaccu of string * inductive * mllambda and mllam_branches = ((constructor * lname option array) list * mllambda) array @@ -467,7 +465,12 @@ let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 = | MLarray arr1, MLarray arr2 -> Array.equal (eq_mllambda gn1 gn2 n env1 env2) arr1 arr2 - | _, _ -> false + | MLisaccu (s1, ind1, ml1), MLisaccu (s2, ind2, ml2) -> + String.equal s1 s2 && eq_ind ind1 ind2 && + eq_mllambda gn1 gn2 n env1 env2 ml1 ml2 + | (MLlocal _ | MLglobal _ | MLprimitive _ | MLlam _ | MLletrec _ | MLlet _ | + MLapp _ | MLif _ | MLmatch _ | MLconstruct _ | MLint _ | MLuint _ | + MLsetref _ | MLsequence _ | MLarray _ | MLisaccu _), _ -> false and eq_letrec gn1 gn2 n env1 env2 defs1 defs2 = let eq_def (_,args1,ml1) (_,args2,ml2) = @@ -542,6 +545,8 @@ let rec hash_mllambda gn n env t = combinesmall 14 (combine hml hml') | MLarray arr -> combinesmall 15 (hash_mllambda_array gn n env 1 arr) + | MLisaccu (s, ind, c) -> + combinesmall 16 (combine (String.hash s) (combine (ind_hash ind) (hash_mllambda gn n env c))) and hash_mllambda_letrec gn n env init defs = let hash_def (_,args,ml) = @@ -608,6 +613,7 @@ let fv_lam l = | MLsetref(_,l) -> aux l bind fv | MLsequence(l1,l2) -> aux l1 bind (aux l2 bind fv) | MLarray arr -> Array.fold_right (fun a fv -> aux a bind fv) arr fv + | MLisaccu (_, _, body) -> aux body bind fv in aux l LNset.empty LNset.empty @@ -1142,7 +1148,7 @@ let ml_of_instance instance u = mkMLapp (MLapp (MLglobal cn, fv_args env fvn fvr)) [|force|] | Lif(t,bt,bf) -> MLif(ml_of_lam env l t, ml_of_lam env l bt, ml_of_lam env l bf) - | Lfix ((rec_pos,start), (ids, tt, tb)) -> + | Lfix ((rec_pos, inds, start), (ids, tt, tb)) -> (* let type_f fvt = [| type fix |] let norm_f1 fv f1 .. fn params1 = body1 .. @@ -1211,8 +1217,9 @@ let ml_of_instance instance u = let paramsi = t_params.(i) in let reci = MLlocal (paramsi.(rec_pos.(i))) in let pargsi = Array.map (fun id -> MLlocal id) paramsi in + let (prefix, ind) = inds.(i) in let body = - MLif(MLapp(MLprimitive Is_accu,[|reci|]), + MLif(MLisaccu (prefix, ind, reci), mkMLapp (MLapp(MLprimitive (Mk_fix(rec_pos,i)), [|mk_type; mk_norm|])) @@ -1374,6 +1381,7 @@ let subst s l = | MLsetref(s,l1) -> MLsetref(s,aux l1) | MLsequence(l1,l2) -> MLsequence(aux l1, aux l2) | MLarray arr -> MLarray (Array.map aux arr) + | MLisaccu (s, ind, l) -> MLisaccu (s, ind, aux l) in aux l @@ -1471,7 +1479,7 @@ let optimize gdef l = let b1 = optimize s b1 in let b2 = optimize s b2 in begin match t, b2 with - | MLapp(MLprimitive Is_accu,[| l1 |]), MLmatch(annot, l2, _, bs) + | MLisaccu (_, _, l1), MLmatch(annot, l2, _, bs) when eq_mllambda l1 l2 -> MLmatch(annot, l1, b1, bs) | _, _ -> MLif(t, b1, b2) end @@ -1483,6 +1491,7 @@ let optimize gdef l = | MLsetref(r,l) -> MLsetref(r, optimize s l) | MLsequence(l1,l2) -> MLsequence(optimize s l1, optimize s l2) | MLarray arr -> MLarray (Array.map (optimize s) arr) + | MLisaccu (pf, ind, l) -> MLisaccu (pf, ind, optimize s l) in optimize LNmap.empty l @@ -1645,7 +1654,11 @@ let pp_mllam fmt l = pp_mllam fmt arr.(len-1) end; Format.fprintf fmt "|]@]" - + | MLisaccu (prefix, (mind, i), c) -> + let accu = Format.sprintf "%sAccu_%s_%i" prefix (string_of_mind mind) i in + Format.fprintf fmt + "@[begin match Obj.magic (%a) with@\n| %s _ ->@\n true@\n| _ ->@\n false@\nend@]" + pp_mllam c accu and pp_letrec fmt defs = let len = Array.length defs in @@ -1738,7 +1751,6 @@ let pp_mllam fmt l = | Mk_var id -> Format.fprintf fmt "mk_var_accu (Names.id_of_string \"%s\")" (string_of_id id) | Mk_proj -> Format.fprintf fmt "mk_proj_accu" - | Is_accu -> Format.fprintf fmt "is_accu" | Is_int -> Format.fprintf fmt "is_int" | Cast_accu -> Format.fprintf fmt "cast_accu" | Upd_cofix -> Format.fprintf fmt "upd_cofix" @@ -1884,7 +1896,7 @@ let compile_constant env sigma prefix ~interactive con cb = let t = Mod_subst.force_constr t in let code = lambda_of_constr env sigma t in if !Flags.debug then Feedback.msg_debug (Pp.str "Generated lambda code"); - let is_lazy = is_lazy prefix t in + let is_lazy = is_lazy env prefix t in let code = if is_lazy then mk_lazy code else code in let name = if interactive then LinkedInteractive prefix diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli index eaad8ee0c..5075bd3d1 100644 --- a/kernel/nativeinstr.mli +++ b/kernel/nativeinstr.mli @@ -36,7 +36,7 @@ and lambda = | Lcase of annot_sw * lambda * lambda * lam_branches (* annotations, term being matched, accu, branches *) | Lif of lambda * lambda * lambda - | Lfix of (int array * int) * fix_decl + | Lfix of (int array * (string * inductive) array * int) * fix_decl | Lcofix of int * fix_decl (* must be in eta-expanded form *) | Lmakeblock of prefix * pconstructor * int * lambda array (* prefix, constructor name, constructor tag, arguments *) diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 5843cd543..a5cdd0a19 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -333,54 +333,13 @@ let rec get_alias env (kn, u as p) = (*i Global environment *) -let global_env = ref empty_env - -let set_global_env env = global_env := env - let get_names decl = let decl = Array.of_list decl in Array.map fst decl -(* Rel Environment *) -module Vect = - struct - type 'a t = { - mutable elems : 'a array; - mutable size : int; - } - - let make n a = { - elems = Array.make n a; - size = 0; - } - - let extend v = - if Int.equal v.size (Array.length v.elems) then - let new_size = min (2*v.size) Sys.max_array_length in - if new_size <= v.size then invalid_arg "Vect.extend"; - let new_elems = Array.make new_size v.elems.(0) in - Array.blit v.elems 0 new_elems 0 (v.size); - v.elems <- new_elems - - let push v a = - extend v; - v.elems.(v.size) <- a; - v.size <- v.size + 1 - - let popn v n = - v.size <- max 0 (v.size - n) - - let pop v = popn v 1 - - let get_last v n = - if v.size <= n then invalid_arg "Vect.get:index out of bounds"; - v.elems.(v.size - n - 1) - - end - let empty_args = [||] -module Renv = +module Cache = struct module ConstrHash = @@ -394,45 +353,20 @@ module Renv = type constructor_info = tag * int * int (* nparam nrealargs *) - type t = { - name_rel : Name.t Vect.t; - construct_tbl : constructor_info ConstrTable.t; - - } - - - let make () = { - name_rel = Vect.make 16 Anonymous; - construct_tbl = ConstrTable.create 111 - } - - let push_rel env id = Vect.push env.name_rel id - - let push_rels env ids = - Array.iter (push_rel env) ids - - let pop env = Vect.pop env.name_rel - - let popn env n = - for _i = 1 to n do pop env done - - let get env n = - Lrel (Vect.get_last env.name_rel (n-1), n) - - let get_construct_info env c = - try ConstrTable.find env.construct_tbl c + let get_construct_info cache env c : constructor_info = + try ConstrTable.find cache c with Not_found -> let ((mind,j), i) = c in - let oib = lookup_mind mind !global_env in + let oib = lookup_mind mind env in let oip = oib.mind_packets.(j) in let tag,arity = oip.mind_reloc_tbl.(i-1) in let nparams = oib.mind_nparams in let r = (tag, nparams, arity) in - ConstrTable.add env.construct_tbl c r; + ConstrTable.add cache c r; r end -let is_lazy prefix t = +let is_lazy env prefix t = match kind t with | App (f,args) -> begin match kind f with @@ -440,7 +374,7 @@ let is_lazy prefix t = let entry = mkInd (fst c) in (try let _ = - Retroknowledge.get_native_before_match_info (!global_env).retroknowledge + Retroknowledge.get_native_before_match_info env.retroknowledge entry prefix c Llazy; in false @@ -463,73 +397,85 @@ let empty_evars = let empty_ids = [||] -let rec lambda_of_constr env sigma c = +(** Extract the inductive type over which a fixpoint is decreasing *) +let rec get_fix_struct env i t = match kind (Reduction.whd_all env t) with +| Prod (na, dom, t) -> + if Int.equal i 0 then + let dom = Reduction.whd_all env dom in + let (dom, _) = decompose_appvect dom in + match kind dom with + | Ind (ind, _) -> ind + | _ -> assert false + else + let env = Environ.push_rel (RelDecl.LocalAssum (na, dom)) env in + get_fix_struct env (i - 1) t +| _ -> assert false + +let rec lambda_of_constr cache env sigma c = match kind c with | Meta mv -> let ty = meta_type sigma mv in - Lmeta (mv, lambda_of_constr env sigma ty) + Lmeta (mv, lambda_of_constr cache env sigma ty) | Evar (evk,args as ev) -> (match evar_value sigma ev with | None -> let ty = evar_type sigma ev in - let args = Array.map (lambda_of_constr env sigma) args in - Levar(evk, lambda_of_constr env sigma ty, args) - | Some t -> lambda_of_constr env sigma t) + let args = Array.map (lambda_of_constr cache env sigma) args in + Levar(evk, lambda_of_constr cache env sigma ty, args) + | Some t -> lambda_of_constr cache env sigma t) - | Cast (c, _, _) -> lambda_of_constr env sigma c + | Cast (c, _, _) -> lambda_of_constr cache env sigma c - | Rel i -> Renv.get env i + | Rel i -> Lrel (RelDecl.get_name (Environ.lookup_rel i env), i) | Var id -> Lvar id | Sort s -> Lsort s | Ind (ind,u as pind) -> - let prefix = get_mind_prefix !global_env (fst ind) in + let prefix = get_mind_prefix env (fst ind) in Lind (prefix, pind) | Prod(id, dom, codom) -> - let ld = lambda_of_constr env sigma dom in - Renv.push_rel env id; - let lc = lambda_of_constr env sigma codom in - Renv.pop env; + let ld = lambda_of_constr cache env sigma dom in + let env = Environ.push_rel (RelDecl.LocalAssum (id, dom)) env in + let lc = lambda_of_constr cache env sigma codom in Lprod(ld, Llam([|id|], lc)) | Lambda _ -> let params, body = Term.decompose_lam c in + let fold (na, t) env = Environ.push_rel (RelDecl.LocalAssum (na, t)) env in + let env = List.fold_right fold params env in + let lb = lambda_of_constr cache env sigma body in let ids = get_names (List.rev params) in - Renv.push_rels env ids; - let lb = lambda_of_constr env sigma body in - Renv.popn env (Array.length ids); mkLlam ids lb - | LetIn(id, def, _, body) -> - let ld = lambda_of_constr env sigma def in - Renv.push_rel env id; - let lb = lambda_of_constr env sigma body in - Renv.pop env; + | LetIn(id, def, t, body) -> + let ld = lambda_of_constr cache env sigma def in + let env = Environ.push_rel (RelDecl.LocalDef (id, def, t)) env in + let lb = lambda_of_constr cache env sigma body in Llet(id, ld, lb) - | App(f, args) -> lambda_of_app env sigma f args + | App(f, args) -> lambda_of_app cache env sigma f args - | Const _ -> lambda_of_app env sigma c empty_args + | Const _ -> lambda_of_app cache env sigma c empty_args - | Construct _ -> lambda_of_app env sigma c empty_args + | Construct _ -> lambda_of_app cache env sigma c empty_args | Proj (p, c) -> - let pb = lookup_projection p !global_env in + let pb = lookup_projection p env in let ind = pb.proj_ind in - let prefix = get_mind_prefix !global_env (fst ind) in - mkLapp (Lproj (prefix, ind, pb.proj_arg)) [|lambda_of_constr env sigma c|] + let prefix = get_mind_prefix env (fst ind) in + mkLapp (Lproj (prefix, ind, pb.proj_arg)) [|lambda_of_constr cache env sigma c|] | Case(ci,t,a,branches) -> let (mind,i as ind) = ci.ci_ind in - let mib = lookup_mind mind !global_env in + let mib = lookup_mind mind env in let oib = mib.mind_packets.(i) in let tbl = oib.mind_reloc_tbl in (* Building info *) - let prefix = get_mind_prefix !global_env mind in + let prefix = get_mind_prefix env mind in let annot_sw = { asw_ind = ind; asw_ci = ci; @@ -538,21 +484,21 @@ let rec lambda_of_constr env sigma c = asw_prefix = prefix} in (* translation of the argument *) - let la = lambda_of_constr env sigma a in + let la = lambda_of_constr cache env sigma a in let entry = mkInd ind in let la = try - Retroknowledge.get_native_before_match_info (!global_env).retroknowledge + Retroknowledge.get_native_before_match_info (env).retroknowledge entry prefix (ind,1) la with Not_found -> la in (* translation of the type *) - let lt = lambda_of_constr env sigma t in + let lt = lambda_of_constr cache env sigma t in (* translation of branches *) let mk_branch i b = let cn = (ind,i+1) in let _, arity = tbl.(i) in - let b = lambda_of_constr env sigma b in + let b = lambda_of_constr cache env sigma b in if Int.equal arity 0 then (cn, empty_ids, b) else match b with @@ -565,86 +511,90 @@ let rec lambda_of_constr env sigma c = let bs = Array.mapi mk_branch branches in Lcase(annot_sw, lt, la, bs) - | Fix(rec_init,(names,type_bodies,rec_bodies)) -> - let ltypes = lambda_of_args env sigma 0 type_bodies in - Renv.push_rels env names; - let lbodies = lambda_of_args env sigma 0 rec_bodies in - Renv.popn env (Array.length names); - Lfix(rec_init, (names, ltypes, lbodies)) + | Fix((pos, i), (names,type_bodies,rec_bodies)) -> + let ltypes = lambda_of_args cache env sigma 0 type_bodies in + let map i t = + let ind = get_fix_struct env i t in + let prefix = get_mind_prefix env (fst ind) in + (prefix, ind) + in + let inds = Array.map2 map pos type_bodies in + let env = Environ.push_rec_types (names, type_bodies, rec_bodies) env in + let lbodies = lambda_of_args cache env sigma 0 rec_bodies in + Lfix((pos, inds, i), (names, ltypes, lbodies)) | CoFix(init,(names,type_bodies,rec_bodies)) -> - let rec_bodies = Array.map2 (Reduction.eta_expand !global_env) rec_bodies type_bodies in - let ltypes = lambda_of_args env sigma 0 type_bodies in - Renv.push_rels env names; - let lbodies = lambda_of_args env sigma 0 rec_bodies in - Renv.popn env (Array.length names); + let rec_bodies = Array.map2 (Reduction.eta_expand env) rec_bodies type_bodies in + let ltypes = lambda_of_args cache env sigma 0 type_bodies in + let env = Environ.push_rec_types (names, type_bodies, rec_bodies) env in + let lbodies = lambda_of_args cache env sigma 0 rec_bodies in Lcofix(init, (names, ltypes, lbodies)) -and lambda_of_app env sigma f args = +and lambda_of_app cache env sigma f args = match kind f with | Const (kn,u as c) -> - let kn,u = get_alias !global_env c in - let cb = lookup_constant kn !global_env in + let kn,u = get_alias env c in + let cb = lookup_constant kn env in (try - let prefix = get_const_prefix !global_env kn in + let prefix = get_const_prefix env kn in (* We delay the compilation of arguments to avoid an exponential behavior *) let f = Retroknowledge.get_native_compiling_info - (!global_env).retroknowledge (mkConst kn) prefix in - let args = lambda_of_args env sigma 0 args in + (env).retroknowledge (mkConst kn) prefix in + let args = lambda_of_args cache env sigma 0 args in f args with Not_found -> begin match cb.const_body with | Def csubst -> (* TODO optimize if f is a proj and argument is known *) if cb.const_inline_code then - lambda_of_app env sigma (Mod_subst.force_constr csubst) args + lambda_of_app cache env sigma (Mod_subst.force_constr csubst) args else - let prefix = get_const_prefix !global_env kn in + let prefix = get_const_prefix env kn in let t = - if is_lazy prefix (Mod_subst.force_constr csubst) then + if is_lazy env prefix (Mod_subst.force_constr csubst) then mkLapp Lforce [|Lconst (prefix, (kn,u))|] else Lconst (prefix, (kn,u)) in - mkLapp t (lambda_of_args env sigma 0 args) + mkLapp t (lambda_of_args cache env sigma 0 args) | OpaqueDef _ | Undef _ -> - let prefix = get_const_prefix !global_env kn in - mkLapp (Lconst (prefix, (kn,u))) (lambda_of_args env sigma 0 args) + let prefix = get_const_prefix env kn in + mkLapp (Lconst (prefix, (kn,u))) (lambda_of_args cache env sigma 0 args) end) | Construct (c,u) -> - let tag, nparams, arity = Renv.get_construct_info env c in + let tag, nparams, arity = Cache.get_construct_info cache env c in let expected = nparams + arity in let nargs = Array.length args in - let prefix = get_mind_prefix !global_env (fst (fst c)) in + let prefix = get_mind_prefix env (fst (fst c)) in if Int.equal nargs expected then try try Retroknowledge.get_native_constant_static_info - (!global_env).retroknowledge + (env).retroknowledge f args with NotClosed -> assert (Int.equal nparams 0); (* should be fine for int31 *) - let args = lambda_of_args env sigma nparams args in + let args = lambda_of_args cache env sigma nparams args in Retroknowledge.get_native_constant_dynamic_info - (!global_env).retroknowledge f prefix c args + (env).retroknowledge f prefix c args with Not_found -> - let args = lambda_of_args env sigma nparams args in - makeblock !global_env c u tag args + let args = lambda_of_args cache env sigma nparams args in + makeblock env c u tag args else - let args = lambda_of_args env sigma 0 args in + let args = lambda_of_args cache env sigma 0 args in (try Retroknowledge.get_native_constant_dynamic_info - (!global_env).retroknowledge f prefix c args + (env).retroknowledge f prefix c args with Not_found -> mkLapp (Lconstruct (prefix, (c,u))) args) | _ -> - let f = lambda_of_constr env sigma f in - let args = lambda_of_args env sigma 0 args in + let f = lambda_of_constr cache env sigma f in + let args = lambda_of_args cache env sigma 0 args in mkLapp f args -and lambda_of_args env sigma start args = +and lambda_of_args cache env sigma start args = let nargs = Array.length args in if start < nargs then Array.init (nargs - start) - (fun i -> lambda_of_constr env sigma args.(start + i)) + (fun i -> lambda_of_constr cache env sigma args.(start + i)) else empty_args let optimize lam = @@ -657,11 +607,8 @@ let optimize lam = lam let lambda_of_constr env sigma c = - set_global_env env; - let env = Renv.make () in - let ids = List.rev_map RelDecl.get_name (rel_context !global_env) in - Renv.push_rels env (Array.of_list ids); - let lam = lambda_of_constr env sigma c in + let cache = Cache.ConstrTable.create 91 in + let lam = lambda_of_constr cache env sigma c in (* if Flags.vm_draw_opt () then begin (msgerrnl (str "Constr = \n" ++ pr_constr c);flush_all()); (msgerrnl (str "Lambda = \n" ++ pp_lam lam);flush_all()); diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 26bfeb7e0..efe1700cd 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -23,7 +23,7 @@ val empty_evars : evars val decompose_Llam : lambda -> Name.t array * lambda val decompose_Llam_Llet : lambda -> (Name.t * lambda option) array * lambda -val is_lazy : prefix -> constr -> bool +val is_lazy : env -> prefix -> constr -> bool val mk_lazy : lambda -> lambda val get_mind_prefix : env -> MutInd.t -> string diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 649853f06..6bbf15160 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -110,9 +110,6 @@ type kind_of_value = val kind_of_value : t -> kind_of_value -(* *) -val is_accu : t -> bool - val str_encode : 'a -> string val str_decode : string -> 'a diff --git a/plugins/.merlin b/plugins/.merlin.in index 2ba616962..2ba616962 100644 --- a/plugins/.merlin +++ b/plugins/.merlin.in diff --git a/plugins/fourier/Fourier.v b/plugins/fourier/Fourier.v deleted file mode 100644 index 07f32be8e..000000000 --- a/plugins/fourier/Fourier.v +++ /dev/null @@ -1,20 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(* "Fourier's method to solve linear inequations/equations systems.".*) - -Require Export Field. -Require Export DiscrR. -Require Export Fourier_util. -Declare ML Module "fourier_plugin". - -Ltac fourier := abstract (compute [IZR IPR IPR_2] in *; fourierz; field; discrR). - -Ltac fourier_eq := apply Rge_antisym; fourier. diff --git a/plugins/fourier/Fourier_util.v b/plugins/fourier/Fourier_util.v deleted file mode 100644 index d3159698b..000000000 --- a/plugins/fourier/Fourier_util.v +++ /dev/null @@ -1,222 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -Require Export Rbase. -Comments "Lemmas used by the tactic Fourier". - -Open Scope R_scope. - -Lemma Rfourier_lt : forall x1 y1 a:R, x1 < y1 -> 0 < a -> a * x1 < a * y1. -intros; apply Rmult_lt_compat_l; assumption. -Qed. - -Lemma Rfourier_le : forall x1 y1 a:R, x1 <= y1 -> 0 < a -> a * x1 <= a * y1. -red. -intros. -case H; auto with real. -Qed. - -Lemma Rfourier_lt_lt : - forall x1 y1 x2 y2 a:R, - x1 < y1 -> x2 < y2 -> 0 < a -> x1 + a * x2 < y1 + a * y2. -intros x1 y1 x2 y2 a H H0 H1; try assumption. -apply Rplus_lt_compat. -try exact H. -apply Rfourier_lt. -try exact H0. -try exact H1. -Qed. - -Lemma Rfourier_lt_le : - forall x1 y1 x2 y2 a:R, - x1 < y1 -> x2 <= y2 -> 0 < a -> x1 + a * x2 < y1 + a * y2. -intros x1 y1 x2 y2 a H H0 H1; try assumption. -case H0; intros. -apply Rplus_lt_compat. -try exact H. -apply Rfourier_lt; auto with real. -rewrite H2. -rewrite (Rplus_comm y1 (a * y2)). -rewrite (Rplus_comm x1 (a * y2)). -apply Rplus_lt_compat_l. -try exact H. -Qed. - -Lemma Rfourier_le_lt : - forall x1 y1 x2 y2 a:R, - x1 <= y1 -> x2 < y2 -> 0 < a -> x1 + a * x2 < y1 + a * y2. -intros x1 y1 x2 y2 a H H0 H1; try assumption. -case H; intros. -apply Rfourier_lt_le; auto with real. -rewrite H2. -apply Rplus_lt_compat_l. -apply Rfourier_lt; auto with real. -Qed. - -Lemma Rfourier_le_le : - forall x1 y1 x2 y2 a:R, - x1 <= y1 -> x2 <= y2 -> 0 < a -> x1 + a * x2 <= y1 + a * y2. -intros x1 y1 x2 y2 a H H0 H1; try assumption. -case H0; intros. -red. -left; try assumption. -apply Rfourier_le_lt; auto with real. -rewrite H2. -case H; intros. -red. -left; try assumption. -rewrite (Rplus_comm x1 (a * y2)). -rewrite (Rplus_comm y1 (a * y2)). -apply Rplus_lt_compat_l. -try exact H3. -rewrite H3. -red. -right; try assumption. -auto with real. -Qed. - -Lemma Rlt_zero_pos_plus1 : forall x:R, 0 < x -> 0 < 1 + x. -intros x H; try assumption. -rewrite Rplus_comm. -apply Rle_lt_0_plus_1. -red; auto with real. -Qed. - -Lemma Rlt_mult_inv_pos : forall x y:R, 0 < x -> 0 < y -> 0 < x * / y. -intros x y H H0; try assumption. -replace 0 with (x * 0). -apply Rmult_lt_compat_l; auto with real. -ring. -Qed. - -Lemma Rlt_zero_1 : 0 < 1. -exact Rlt_0_1. -Qed. - -Lemma Rle_zero_pos_plus1 : forall x:R, 0 <= x -> 0 <= 1 + x. -intros x H; try assumption. -case H; intros. -red. -left; try assumption. -apply Rlt_zero_pos_plus1; auto with real. -rewrite <- H0. -replace (1 + 0) with 1. -red; left. -exact Rlt_zero_1. -ring. -Qed. - -Lemma Rle_mult_inv_pos : forall x y:R, 0 <= x -> 0 < y -> 0 <= x * / y. -intros x y H H0; try assumption. -case H; intros. -red; left. -apply Rlt_mult_inv_pos; auto with real. -rewrite <- H1. -red; right; ring. -Qed. - -Lemma Rle_zero_1 : 0 <= 1. -red; left. -exact Rlt_zero_1. -Qed. - -Lemma Rle_not_lt : forall n d:R, 0 <= n * / d -> ~ 0 < - n * / d. -intros n d H; red; intros H0; try exact H0. -generalize (Rgt_not_le 0 (n * / d)). -intros H1; elim H1; try assumption. -replace (n * / d) with (- - (n * / d)). -replace 0 with (- -0). -replace (- (n * / d)) with (- n * / d). -replace (-0) with 0. -red. -apply Ropp_gt_lt_contravar. -red. -exact H0. -ring. -ring. -ring. -ring. -Qed. - -Lemma Rnot_lt0 : forall x:R, ~ 0 < 0 * x. -intros x; try assumption. -replace (0 * x) with 0. -apply Rlt_irrefl. -ring. -Qed. - -Lemma Rlt_not_le_frac_opp : forall n d:R, 0 < n * / d -> ~ 0 <= - n * / d. -intros n d H; try assumption. -apply Rgt_not_le. -replace 0 with (-0). -replace (- n * / d) with (- (n * / d)). -apply Ropp_lt_gt_contravar. -try exact H. -ring. -ring. -Qed. - -Lemma Rnot_lt_lt : forall x y:R, ~ 0 < y - x -> ~ x < y. -unfold not; intros. -apply H. -apply Rplus_lt_reg_l with x. -replace (x + 0) with x. -replace (x + (y - x)) with y. -try exact H0. -ring. -ring. -Qed. - -Lemma Rnot_le_le : forall x y:R, ~ 0 <= y - x -> ~ x <= y. -unfold not; intros. -apply H. -case H0; intros. -left. -apply Rplus_lt_reg_l with x. -replace (x + 0) with x. -replace (x + (y - x)) with y. -try exact H1. -ring. -ring. -right. -rewrite H1; ring. -Qed. - -Lemma Rfourier_gt_to_lt : forall x y:R, y > x -> x < y. -unfold Rgt; intros; assumption. -Qed. - -Lemma Rfourier_ge_to_le : forall x y:R, y >= x -> x <= y. -intros x y; exact (Rge_le y x). -Qed. - -Lemma Rfourier_eqLR_to_le : forall x y:R, x = y -> x <= y. -exact Req_le. -Qed. - -Lemma Rfourier_eqRL_to_le : forall x y:R, y = x -> x <= y. -exact Req_le_sym. -Qed. - -Lemma Rfourier_not_ge_lt : forall x y:R, (x >= y -> False) -> x < y. -exact Rnot_ge_lt. -Qed. - -Lemma Rfourier_not_gt_le : forall x y:R, (x > y -> False) -> x <= y. -exact Rnot_gt_le. -Qed. - -Lemma Rfourier_not_le_gt : forall x y:R, (x <= y -> False) -> x > y. -exact Rnot_le_lt. -Qed. - -Lemma Rfourier_not_lt_ge : forall x y:R, (x < y -> False) -> x >= y. -exact Rnot_lt_ge. -Qed. diff --git a/plugins/fourier/fourier.ml b/plugins/fourier/fourier.ml deleted file mode 100644 index bee2b3b58..000000000 --- a/plugins/fourier/fourier.ml +++ /dev/null @@ -1,204 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(* Méthode d'élimination de Fourier *) -(* Référence: -Auteur(s) : Fourier, Jean-Baptiste-Joseph - -Titre(s) : Oeuvres de Fourier [Document électronique]. Tome second. Mémoires publiés dans divers recueils / publ. par les soins de M. Gaston Darboux,... - -Publication : Numérisation BnF de l'édition de Paris : Gauthier-Villars, 1890 - -Pages: 326-327 - -http://gallica.bnf.fr/ -*) - -(* Un peu de calcul sur les rationnels... -Les opérations rendent des rationnels normalisés, -i.e. le numérateur et le dénominateur sont premiers entre eux. -*) -type rational = {num:int; - den:int} -;; -let print_rational x = - print_int x.num; - print_string "/"; - print_int x.den -;; - -let rec pgcd x y = if y = 0 then x else pgcd y (x mod y);; - - -let r0 = {num=0;den=1};; -let r1 = {num=1;den=1};; - -let rnorm x = let x = (if x.den<0 then {num=(-x.num);den=(-x.den)} else x) in - if x.num=0 then r0 - else (let d=pgcd x.num x.den in - let d= (if d<0 then -d else d) in - {num=(x.num)/d;den=(x.den)/d});; - -let rop x = rnorm {num=(-x.num);den=x.den};; - -let rplus x y = rnorm {num=x.num*y.den + y.num*x.den;den=x.den*y.den};; - -let rminus x y = rnorm {num=x.num*y.den - y.num*x.den;den=x.den*y.den};; - -let rmult x y = rnorm {num=x.num*y.num;den=x.den*y.den};; - -let rinv x = rnorm {num=x.den;den=x.num};; - -let rdiv x y = rnorm {num=x.num*y.den;den=x.den*y.num};; - -let rinf x y = x.num*y.den < y.num*x.den;; -let rinfeq x y = x.num*y.den <= y.num*x.den;; - -(* {coef;hist;strict}, où coef=[c1; ...; cn; d], représente l'inéquation -c1x1+...+cnxn < d si strict=true, <= sinon, -hist donnant les coefficients (positifs) d'une combinaison linéaire qui permet d'obtenir l'inéquation à partir de celles du départ. -*) - -type ineq = {coef:rational list; - hist:rational list; - strict:bool};; - -let pop x l = l:=x::(!l);; - -(* sépare la liste d'inéquations s selon que leur premier coefficient est -négatif, nul ou positif. *) -let partitionne s = - let lpos=ref [] in - let lneg=ref [] in - let lnul=ref [] in - List.iter (fun ie -> match ie.coef with - [] -> raise (Failure "empty ineq") - |(c::r) -> if rinf c r0 - then pop ie lneg - else if rinf r0 c then pop ie lpos - else pop ie lnul) - s; - [!lneg;!lnul;!lpos] -;; -(* initialise les histoires d'une liste d'inéquations données par leurs listes de coefficients et leurs strictitudes (!): -(add_hist [(equation 1, s1);...;(équation n, sn)]) -= -[{équation 1, [1;0;...;0], s1}; - {équation 2, [0;1;...;0], s2}; - ... - {équation n, [0;0;...;1], sn}] -*) -let add_hist le = - let n = List.length le in - let i = ref 0 in - List.map (fun (ie,s) -> - let h = ref [] in - for _k = 1 to (n - (!i) - 1) do pop r0 h; done; - pop r1 h; - for _k = 1 to !i do pop r0 h; done; - i:=!i+1; - {coef=ie;hist=(!h);strict=s}) - le -;; -(* additionne deux inéquations *) -let ie_add ie1 ie2 = {coef=List.map2 rplus ie1.coef ie2.coef; - hist=List.map2 rplus ie1.hist ie2.hist; - strict=ie1.strict || ie2.strict} -;; -(* multiplication d'une inéquation par un rationnel (positif) *) -let ie_emult a ie = {coef=List.map (fun x -> rmult a x) ie.coef; - hist=List.map (fun x -> rmult a x) ie.hist; - strict= ie.strict} -;; -(* on enlève le premier coefficient *) -let ie_tl ie = {coef=List.tl ie.coef;hist=ie.hist;strict=ie.strict} -;; -(* le premier coefficient: "tête" de l'inéquation *) -let hd_coef ie = List.hd ie.coef -;; - -(* calcule toutes les combinaisons entre inéquations de tête négative et inéquations de tête positive qui annulent le premier coefficient. -*) -let deduce_add lneg lpos = - let res=ref [] in - List.iter (fun i1 -> - List.iter (fun i2 -> - let a = rop (hd_coef i1) in - let b = hd_coef i2 in - pop (ie_tl (ie_add (ie_emult b i1) - (ie_emult a i2))) res) - lpos) - lneg; - !res -;; -(* élimination de la première variable à partir d'une liste d'inéquations: -opération qu'on itère dans l'algorithme de Fourier. -*) -let deduce1 s = - match (partitionne s) with - [lneg;lnul;lpos] -> - let lnew = deduce_add lneg lpos in - (List.map ie_tl lnul)@lnew - |_->assert false -;; -(* algorithme de Fourier: on élimine successivement toutes les variables. -*) -let deduce lie = - let n = List.length (fst (List.hd lie)) in - let lie=ref (add_hist lie) in - for _i = 1 to n - 1 do - lie:= deduce1 !lie; - done; - !lie -;; - -(* donne [] si le système a des solutions, -sinon donne [c,s,lc] -où lc est la combinaison linéaire des inéquations de départ -qui donne 0 < c si s=true - ou 0 <= c sinon -cette inéquation étant absurde. -*) - -exception Contradiction of (rational * bool * rational list) list - -let unsolvable lie = - let lr = deduce lie in - let check = function - | {coef=[c];hist=lc;strict=s} -> - if (rinf c r0 && (not s)) || (rinfeq c r0 && s) - then raise (Contradiction [c,s,lc]) - |_->assert false - in - try List.iter check lr; [] - with Contradiction l -> l - -(* Exemples: - -let test1=[[r1;r1;r0],true;[rop r1;r1;r1],false;[r0;rop r1;rop r1],false];; -deduce test1;; -unsolvable test1;; - -let test2=[ -[r1;r1;r0;r0;r0],false; -[r0;r1;r1;r0;r0],false; -[r0;r0;r1;r1;r0],false; -[r0;r0;r0;r1;r1],false; -[r1;r0;r0;r0;r1],false; -[rop r1;rop r1;r0;r0;r0],false; -[r0;rop r1;rop r1;r0;r0],false; -[r0;r0;rop r1;rop r1;r0],false; -[r0;r0;r0;rop r1;rop r1],false; -[rop r1;r0;r0;r0;rop r1],false -];; -deduce test2;; -unsolvable test2;; - -*) diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml deleted file mode 100644 index 96be1d893..000000000 --- a/plugins/fourier/fourierR.ml +++ /dev/null @@ -1,644 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - - - -(* La tactique Fourier ne fonctionne de manière sûre que si les coefficients -des inéquations et équations sont entiers. En attendant la tactique Field. -*) - -open Constr -open Tactics -open Names -open Globnames -open Fourier -open Contradiction -open Proofview.Notations - -(****************************************************************************** -Opérations sur les combinaisons linéaires affines. -La partie homogène d'une combinaison linéaire est en fait une table de hash -qui donne le coefficient d'un terme du calcul des constructions, -qui est zéro si le terme n'y est pas. -*) - -module Constrhash = Hashtbl.Make(Constr) - -type flin = {fhom: rational Constrhash.t; - fcste:rational};; - -let flin_zero () = {fhom=Constrhash.create 50;fcste=r0};; - -let flin_coef f x = try Constrhash.find f.fhom x with Not_found -> r0;; - -let flin_add f x c = - let cx = flin_coef f x in - Constrhash.replace f.fhom x (rplus cx c); - f -;; -let flin_add_cste f c = - {fhom=f.fhom; - fcste=rplus f.fcste c} -;; - -let flin_one () = flin_add_cste (flin_zero()) r1;; - -let flin_plus f1 f2 = - let f3 = flin_zero() in - Constrhash.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom; - Constrhash.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom; - flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste; -;; - -let flin_minus f1 f2 = - let f3 = flin_zero() in - Constrhash.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom; - Constrhash.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom; - flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste); -;; -let flin_emult a f = - let f2 = flin_zero() in - Constrhash.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom; - flin_add_cste f2 (rmult a f.fcste); -;; - -(*****************************************************************************) - -type ineq = Rlt | Rle | Rgt | Rge - -let string_of_R_constant kn = - match Constant.repr3 kn with - | ModPath.MPfile dir, sec_dir, id when - sec_dir = DirPath.empty && - DirPath.to_string dir = "Coq.Reals.Rdefinitions" - -> Label.to_string id - | _ -> "constant_not_of_R" - -let rec string_of_R_constr c = - match Constr.kind c with - Cast (c,_,_) -> string_of_R_constr c - |Const (c,_) -> string_of_R_constant c - | _ -> "not_of_constant" - -exception NoRational - -let rec rational_of_constr c = - match Constr.kind c with - | Cast (c,_,_) -> (rational_of_constr c) - | App (c,args) -> - (match (string_of_R_constr c) with - | "Ropp" -> - rop (rational_of_constr args.(0)) - | "Rinv" -> - rinv (rational_of_constr args.(0)) - | "Rmult" -> - rmult (rational_of_constr args.(0)) - (rational_of_constr args.(1)) - | "Rdiv" -> - rdiv (rational_of_constr args.(0)) - (rational_of_constr args.(1)) - | "Rplus" -> - rplus (rational_of_constr args.(0)) - (rational_of_constr args.(1)) - | "Rminus" -> - rminus (rational_of_constr args.(0)) - (rational_of_constr args.(1)) - | _ -> raise NoRational) - | Const (kn,_) -> - (match (string_of_R_constant kn) with - "R1" -> r1 - |"R0" -> r0 - | _ -> raise NoRational) - | _ -> raise NoRational -;; - -exception NoLinear - -let rec flin_of_constr c = - try( - match Constr.kind c with - | Cast (c,_,_) -> (flin_of_constr c) - | App (c,args) -> - (match (string_of_R_constr c) with - "Ropp" -> - flin_emult (rop r1) (flin_of_constr args.(0)) - | "Rplus"-> - flin_plus (flin_of_constr args.(0)) - (flin_of_constr args.(1)) - | "Rminus"-> - flin_minus (flin_of_constr args.(0)) - (flin_of_constr args.(1)) - | "Rmult"-> - (try - let a = rational_of_constr args.(0) in - try - let b = rational_of_constr args.(1) in - flin_add_cste (flin_zero()) (rmult a b) - with NoRational -> - flin_add (flin_zero()) args.(1) a - with NoRational -> - flin_add (flin_zero()) args.(0) - (rational_of_constr args.(1))) - | "Rinv"-> - let a = rational_of_constr args.(0) in - flin_add_cste (flin_zero()) (rinv a) - | "Rdiv"-> - (let b = rational_of_constr args.(1) in - try - let a = rational_of_constr args.(0) in - flin_add_cste (flin_zero()) (rdiv a b) - with NoRational -> - flin_add (flin_zero()) args.(0) (rinv b)) - |_-> raise NoLinear) - | Const (c,_) -> - (match (string_of_R_constant c) with - "R1" -> flin_one () - |"R0" -> flin_zero () - |_-> raise NoLinear) - |_-> raise NoLinear) - with NoRational | NoLinear -> flin_add (flin_zero()) c r1 -;; - -let flin_to_alist f = - let res=ref [] in - Constrhash.iter (fun x c -> res:=(c,x)::(!res)) f; - !res -;; - -(* Représentation des hypothèses qui sont des inéquations ou des équations. -*) -type hineq={hname:constr; (* le nom de l'hypothèse *) - htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *) - hleft:constr; - hright:constr; - hflin:flin; - hstrict:bool} -;; - -(* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0 -*) - -exception NoIneq - -let ineq1_of_constr (h,t) = - let h = EConstr.Unsafe.to_constr h in - let t = EConstr.Unsafe.to_constr t in - match (Constr.kind t) with - | App (f,args) -> - (match Constr.kind f with - | Const (c,_) when Array.length args = 2 -> - let t1= args.(0) in - let t2= args.(1) in - (match (string_of_R_constant c) with - |"Rlt" -> [{hname=h; - htype="Rlt"; - hleft=t1; - hright=t2; - hflin= flin_minus (flin_of_constr t1) - (flin_of_constr t2); - hstrict=true}] - |"Rgt" -> [{hname=h; - htype="Rgt"; - hleft=t2; - hright=t1; - hflin= flin_minus (flin_of_constr t2) - (flin_of_constr t1); - hstrict=true}] - |"Rle" -> [{hname=h; - htype="Rle"; - hleft=t1; - hright=t2; - hflin= flin_minus (flin_of_constr t1) - (flin_of_constr t2); - hstrict=false}] - |"Rge" -> [{hname=h; - htype="Rge"; - hleft=t2; - hright=t1; - hflin= flin_minus (flin_of_constr t2) - (flin_of_constr t1); - hstrict=false}] - |_-> raise NoIneq) - | Ind ((kn,i),_) -> - if not (GlobRef.equal (IndRef(kn,i)) Coqlib.glob_eq) then raise NoIneq; - let t0= args.(0) in - let t1= args.(1) in - let t2= args.(2) in - (match (Constr.kind t0) with - | Const (c,_) -> - (match (string_of_R_constant c) with - | "R"-> - [{hname=h; - htype="eqTLR"; - hleft=t1; - hright=t2; - hflin= flin_minus (flin_of_constr t1) - (flin_of_constr t2); - hstrict=false}; - {hname=h; - htype="eqTRL"; - hleft=t2; - hright=t1; - hflin= flin_minus (flin_of_constr t2) - (flin_of_constr t1); - hstrict=false}] - |_-> raise NoIneq) - |_-> raise NoIneq) - |_-> raise NoIneq) - |_-> raise NoIneq -;; - -(* Applique la méthode de Fourier à une liste d'hypothèses (type hineq) -*) - -let fourier_lineq lineq1 = - let nvar=ref (-1) in - let hvar=Constrhash.create 50 in (* la table des variables des inéquations *) - List.iter (fun f -> - Constrhash.iter (fun x _ -> if not (Constrhash.mem hvar x) then begin - nvar:=(!nvar)+1; - Constrhash.add hvar x (!nvar) - end) - f.hflin.fhom) - lineq1; - let sys= List.map (fun h-> - let v=Array.make ((!nvar)+1) r0 in - Constrhash.iter (fun x c -> v.(Constrhash.find hvar x)<-c) - h.hflin.fhom; - ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict)) - lineq1 in - unsolvable sys -;; - -(*********************************************************************) -(* Defined constants *) - -let get = Lazy.force -let cget = get -let eget c = EConstr.of_constr (Lazy.force c) -let constant path s = UnivGen.constr_of_global @@ - Coqlib.coq_reference "Fourier" path s - -(* Standard library *) -open Coqlib -let coq_sym_eqT = lazy (build_coq_eq_sym ()) -let coq_False = lazy (UnivGen.constr_of_global @@ build_coq_False ()) -let coq_not = lazy (UnivGen.constr_of_global @@ build_coq_not ()) -let coq_eq = lazy (UnivGen.constr_of_global @@ build_coq_eq ()) - -(* Rdefinitions *) -let constant_real = constant ["Reals";"Rdefinitions"] - -let coq_Rlt = lazy (constant_real "Rlt") -let coq_Rgt = lazy (constant_real "Rgt") -let coq_Rle = lazy (constant_real "Rle") -let coq_Rge = lazy (constant_real "Rge") -let coq_R = lazy (constant_real "R") -let coq_Rminus = lazy (constant_real "Rminus") -let coq_Rmult = lazy (constant_real "Rmult") -let coq_Rplus = lazy (constant_real "Rplus") -let coq_Ropp = lazy (constant_real "Ropp") -let coq_Rinv = lazy (constant_real "Rinv") -let coq_R0 = lazy (constant_real "R0") -let coq_R1 = lazy (constant_real "R1") - -(* RIneq *) -let coq_Rinv_1 = lazy (constant ["Reals";"RIneq"] "Rinv_1") - -(* Fourier_util *) -let constant_fourier = constant ["fourier";"Fourier_util"] - -let coq_Rlt_zero_1 = lazy (constant_fourier "Rlt_zero_1") -let coq_Rlt_zero_pos_plus1 = lazy (constant_fourier "Rlt_zero_pos_plus1") -let coq_Rle_zero_pos_plus1 = lazy (constant_fourier "Rle_zero_pos_plus1") -let coq_Rlt_mult_inv_pos = lazy (constant_fourier "Rlt_mult_inv_pos") -let coq_Rle_zero_zero = lazy (constant_fourier "Rle_zero_zero") -let coq_Rle_zero_1 = lazy (constant_fourier "Rle_zero_1") -let coq_Rle_mult_inv_pos = lazy (constant_fourier "Rle_mult_inv_pos") -let coq_Rnot_lt0 = lazy (constant_fourier "Rnot_lt0") -let coq_Rle_not_lt = lazy (constant_fourier "Rle_not_lt") -let coq_Rfourier_gt_to_lt = lazy (constant_fourier "Rfourier_gt_to_lt") -let coq_Rfourier_ge_to_le = lazy (constant_fourier "Rfourier_ge_to_le") -let coq_Rfourier_eqLR_to_le = lazy (constant_fourier "Rfourier_eqLR_to_le") -let coq_Rfourier_eqRL_to_le = lazy (constant_fourier "Rfourier_eqRL_to_le") - -let coq_Rfourier_not_ge_lt = lazy (constant_fourier "Rfourier_not_ge_lt") -let coq_Rfourier_not_gt_le = lazy (constant_fourier "Rfourier_not_gt_le") -let coq_Rfourier_not_le_gt = lazy (constant_fourier "Rfourier_not_le_gt") -let coq_Rfourier_not_lt_ge = lazy (constant_fourier "Rfourier_not_lt_ge") -let coq_Rfourier_lt = lazy (constant_fourier "Rfourier_lt") -let coq_Rfourier_le = lazy (constant_fourier "Rfourier_le") -let coq_Rfourier_lt_lt = lazy (constant_fourier "Rfourier_lt_lt") -let coq_Rfourier_lt_le = lazy (constant_fourier "Rfourier_lt_le") -let coq_Rfourier_le_lt = lazy (constant_fourier "Rfourier_le_lt") -let coq_Rfourier_le_le = lazy (constant_fourier "Rfourier_le_le") -let coq_Rnot_lt_lt = lazy (constant_fourier "Rnot_lt_lt") -let coq_Rnot_le_le = lazy (constant_fourier "Rnot_le_le") -let coq_Rlt_not_le_frac_opp = lazy (constant_fourier "Rlt_not_le_frac_opp") - -(****************************************************************************** -Construction de la preuve en cas de succès de la méthode de Fourier, -i.e. on obtient une contradiction. -*) -let is_int x = (x.den)=1 -;; - -(* fraction = couple (num,den) *) -let rational_to_fraction x= (x.num,x.den) -;; - -(* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1))) -*) -let int_to_real n = - let nn=abs n in - if nn=0 - then get coq_R0 - else - (let s=ref (get coq_R1) in - for _i = 1 to (nn-1) do s:=mkApp (get coq_Rplus,[|get coq_R1;!s|]) done; - if n<0 then mkApp (get coq_Ropp, [|!s|]) else !s) -;; -(* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1))) -*) -let rational_to_real x = - let (n,d)=rational_to_fraction x in - mkApp (get coq_Rmult, - [|int_to_real n;mkApp(get coq_Rinv,[|int_to_real d|])|]) -;; - -(* preuve que 0<n*1/d -*) -let tac_zero_inf_pos gl (n,d) = - let get = eget in - let tacn=ref (apply (get coq_Rlt_zero_1)) in - let tacd=ref (apply (get coq_Rlt_zero_1)) in - for _i = 1 to n - 1 do - tacn:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacn); done; - for _i = 1 to d - 1 do - tacd:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done; - (Tacticals.New.tclTHENS (apply (get coq_Rlt_mult_inv_pos)) [!tacn;!tacd]) -;; - -(* preuve que 0<=n*1/d -*) -let tac_zero_infeq_pos gl (n,d)= - let get = eget in - let tacn=ref (if n=0 - then (apply (get coq_Rle_zero_zero)) - else (apply (get coq_Rle_zero_1))) in - let tacd=ref (apply (get coq_Rlt_zero_1)) in - for _i = 1 to n - 1 do - tacn:=(Tacticals.New.tclTHEN (apply (get coq_Rle_zero_pos_plus1)) !tacn); done; - for _i = 1 to d - 1 do - tacd:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done; - (Tacticals.New.tclTHENS (apply (get coq_Rle_mult_inv_pos)) [!tacn;!tacd]) -;; - -(* preuve que 0<(-n)*(1/d) => False -*) -let tac_zero_inf_false gl (n,d) = - let get = eget in -if n=0 then (apply (get coq_Rnot_lt0)) - else - (Tacticals.New.tclTHEN (apply (get coq_Rle_not_lt)) - (tac_zero_infeq_pos gl (-n,d))) -;; - -(* preuve que 0<=(-n)*(1/d) => False -*) -let tac_zero_infeq_false gl (n,d) = - let get = eget in - (Tacticals.New.tclTHEN (apply (get coq_Rlt_not_le_frac_opp)) - (tac_zero_inf_pos gl (-n,d))) -;; - -let exact = exact_check;; - -let tac_use h = - let get = eget in - let tac = exact (EConstr.of_constr h.hname) in - match h.htype with - "Rlt" -> tac - |"Rle" -> tac - |"Rgt" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_gt_to_lt)) tac) - |"Rge" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_ge_to_le)) tac) - |"eqTLR" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_eqLR_to_le)) tac) - |"eqTRL" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_eqRL_to_le)) tac) - |_->assert false -;; - -(* -let is_ineq (h,t) = - match (Constr.kind t) with - App (f,args) -> - (match (string_of_R_constr f) with - "Rlt" -> true - | "Rgt" -> true - | "Rle" -> true - | "Rge" -> true -(* Wrong:not in Rdefinitions: *) | "eqT" -> - (match (string_of_R_constr args.(0)) with - "R" -> true - | _ -> false) - | _ ->false) - |_->false -;; -*) - -let list_of_sign s = - let open Context.Named.Declaration in - List.map (function LocalAssum (name, typ) -> name, typ - | LocalDef (name, _, typ) -> name, typ) - s;; - -let mkAppL a = - let l = Array.to_list a in - mkApp(List.hd l, Array.of_list (List.tl l)) -;; - -exception GoalDone - -(* Résolution d'inéquations linéaires dans R *) -let rec fourier () = - Proofview.Goal.nf_enter begin fun gl -> - let concl = Proofview.Goal.concl gl in - let sigma = Tacmach.New.project gl in - Coqlib.check_required_library ["Coq";"fourier";"Fourier"]; - let goal = Termops.strip_outer_cast sigma concl in - let goal = EConstr.Unsafe.to_constr goal in - let fhyp=Id.of_string "new_hyp_for_fourier" in - (* si le but est une inéquation, on introduit son contraire, - et le but à prouver devient False *) - try - match (Constr.kind goal) with - App (f,args) -> - let get = eget in - (match (string_of_R_constr f) with - "Rlt" -> - (Tacticals.New.tclTHEN - (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_ge_lt)) - (intro_using fhyp)) - (fourier ())) - |"Rle" -> - (Tacticals.New.tclTHEN - (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_gt_le)) - (intro_using fhyp)) - (fourier ())) - |"Rgt" -> - (Tacticals.New.tclTHEN - (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_le_gt)) - (intro_using fhyp)) - (fourier ())) - |"Rge" -> - (Tacticals.New.tclTHEN - (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_lt_ge)) - (intro_using fhyp)) - (fourier ())) - |_-> raise GoalDone) - |_-> raise GoalDone - with GoalDone -> - (* les hypothèses *) - let hyps = List.map (fun (h,t)-> (EConstr.mkVar h,t)) - (list_of_sign (Proofview.Goal.hyps gl)) in - let lineq =ref [] in - List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq)) - with NoIneq -> ()) - hyps; - (* lineq = les inéquations découlant des hypothèses *) - if !lineq=[] then CErrors.user_err Pp.(str "No inequalities"); - let res=fourier_lineq (!lineq) in - let tac=ref (Proofview.tclUNIT ()) in - if res=[] - then CErrors.user_err Pp.(str "fourier failed") - (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *) - else (match res with - [(cres,sres,lc)]-> - (* lc=coefficients multiplicateurs des inéquations - qui donnent 0<cres ou 0<=cres selon sres *) - (*print_string "Fourier's method can prove the goal...";flush stdout;*) - let lutil=ref [] in - List.iter - (fun (h,c) -> - if c<>r0 - then (lutil:=(h,c)::(!lutil)(*; - print_rational(c);print_string " "*))) - (List.combine (!lineq) lc); - (* on construit la combinaison linéaire des inéquation *) - (match (!lutil) with - (h1,c1)::lutil -> - let s=ref (h1.hstrict) in - let t1=ref (mkAppL [|get coq_Rmult; - rational_to_real c1; - h1.hleft|]) in - let t2=ref (mkAppL [|get coq_Rmult; - rational_to_real c1; - h1.hright|]) in - List.iter (fun (h,c) -> - s:=(!s)||(h.hstrict); - t1:=(mkAppL [|get coq_Rplus; - !t1; - mkAppL [|get coq_Rmult; - rational_to_real c; - h.hleft|] |]); - t2:=(mkAppL [|get coq_Rplus; - !t2; - mkAppL [|get coq_Rmult; - rational_to_real c; - h.hright|] |])) - lutil; - let ineq=mkAppL [|if (!s) then get coq_Rlt else get coq_Rle; - !t1; - !t2 |] in - let tc=rational_to_real cres in - (* puis sa preuve *) - let get = eget in - let tac1=ref (if h1.hstrict - then (Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt)) - [tac_use h1; - tac_zero_inf_pos gl - (rational_to_fraction c1)]) - else (Tacticals.New.tclTHENS (apply (get coq_Rfourier_le)) - [tac_use h1; - tac_zero_inf_pos gl - (rational_to_fraction c1)])) in - s:=h1.hstrict; - List.iter (fun (h,c)-> - (if (!s) - then (if h.hstrict - then tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt_lt)) - [!tac1;tac_use h; - tac_zero_inf_pos gl - (rational_to_fraction c)]) - else tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt_le)) - [!tac1;tac_use h; - tac_zero_inf_pos gl - (rational_to_fraction c)])) - else (if h.hstrict - then tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_le_lt)) - [!tac1;tac_use h; - tac_zero_inf_pos gl - (rational_to_fraction c)]) - else tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_le_le)) - [!tac1;tac_use h; - tac_zero_inf_pos gl - (rational_to_fraction c)]))); - s:=(!s)||(h.hstrict)) - lutil; - let tac2= if sres - then tac_zero_inf_false gl (rational_to_fraction cres) - else tac_zero_infeq_false gl (rational_to_fraction cres) - in - tac:=(Tacticals.New.tclTHENS (cut (EConstr.of_constr ineq)) - [Tacticals.New.tclTHEN (change_concl - (EConstr.of_constr (mkAppL [| cget coq_not; ineq|] - ))) - (Tacticals.New.tclTHEN (apply (if sres then get coq_Rnot_lt_lt - else get coq_Rnot_le_le)) - (Tacticals.New.tclTHENS (Equality.replace - (EConstr.of_constr (mkAppL [|cget coq_Rminus;!t2;!t1|] - )) - (EConstr.of_constr tc)) - [tac2; - (Tacticals.New.tclTHENS - (Equality.replace - (EConstr.of_constr (mkApp (cget coq_Rinv, - [|cget coq_R1|]))) - (get coq_R1)) -(* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *) - - [Tacticals.New.tclORELSE - (* TODO : Ring.polynom []*) (Proofview.tclUNIT ()) - (Proofview.tclUNIT ()); - Tacticals.New.pf_constr_of_global (cget coq_sym_eqT) >>= fun symeq -> - (Tacticals.New.tclTHEN (apply symeq) - (apply (get coq_Rinv_1)))] - - ) - ])); - !tac1]); - tac:=(Tacticals.New.tclTHENS (cut (get coq_False)) - [Tacticals.New.tclTHEN intro (contradiction None); - !tac]) - |_-> assert false) |_-> assert false - ); -(* ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *))) gl) *) - !tac -(* ((tclABSTRACT None !tac) gl) *) - end -;; - -(* -let fourier_tac x gl = - fourier gl -;; - -let v_fourier = add_tactic "Fourier" fourier_tac -*) - diff --git a/plugins/fourier/fourier_plugin.mlpack b/plugins/fourier/fourier_plugin.mlpack deleted file mode 100644 index b6262f8ae..000000000 --- a/plugins/fourier/fourier_plugin.mlpack +++ /dev/null @@ -1,3 +0,0 @@ -Fourier -FourierR -G_fourier diff --git a/plugins/fourier/g_fourier.mlg b/plugins/fourier/g_fourier.mlg deleted file mode 100644 index 703e29f96..000000000 --- a/plugins/fourier/g_fourier.mlg +++ /dev/null @@ -1,22 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -{ - -open Ltac_plugin -open FourierR - -} - -DECLARE PLUGIN "fourier_plugin" - -TACTIC EXTEND fourier -| [ "fourierz" ] -> { fourier () } -END diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index b95d64ce9..549f1fc0e 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -14,6 +14,6 @@ bool -> int -> Constrexpr.constr_expr -> (pconstant -> Indfun_common.tcc_lemma_value ref -> pconstant -> - pconstant -> int -> EConstr.types -> int -> EConstr.constr -> 'a) -> Constrexpr.constr_expr list -> unit + pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> unit diff --git a/plugins/micromega/Fourier.v b/plugins/micromega/Fourier.v new file mode 100644 index 000000000..0153de1da --- /dev/null +++ b/plugins/micromega/Fourier.v @@ -0,0 +1,5 @@ +Require Import Lra. +Require Export Fourier_util. + +#[deprecated(since = "8.9.0", note = "Use lra instead.")] +Ltac fourier := lra. diff --git a/plugins/micromega/Fourier_util.v b/plugins/micromega/Fourier_util.v new file mode 100644 index 000000000..b62153dee --- /dev/null +++ b/plugins/micromega/Fourier_util.v @@ -0,0 +1,31 @@ +Require Export Rbase. +Require Import Lra. + +Open Scope R_scope. + +Lemma Rlt_mult_inv_pos : forall x y:R, 0 < x -> 0 < y -> 0 < x * / y. +intros x y H H0; try assumption. +replace 0 with (x * 0). +apply Rmult_lt_compat_l; auto with real. +ring. +Qed. + +Lemma Rlt_zero_pos_plus1 : forall x:R, 0 < x -> 0 < 1 + x. +intros x H; try assumption. +rewrite Rplus_comm. +apply Rle_lt_0_plus_1. +red; auto with real. +Qed. + +Lemma Rle_zero_pos_plus1 : forall x:R, 0 <= x -> 0 <= 1 + x. + intros; lra. +Qed. + +Lemma Rle_mult_inv_pos : forall x y:R, 0 <= x -> 0 < y -> 0 <= x * / y. +intros x y H H0; try assumption. +case H; intros. +red; left. +apply Rlt_mult_inv_pos; auto with real. +rewrite <- H1. +red; right; ring. +Qed. diff --git a/plugins/micromega/mutils.mli b/plugins/micromega/mutils.mli index 7b7a090de..094429ea1 100644 --- a/plugins/micromega/mutils.mli +++ b/plugins/micromega/mutils.mli @@ -30,7 +30,7 @@ end module TagSet : CSig.SetS with type elt = Tag.t -val pp_list : (out_channel -> 'a -> 'b) -> out_channel -> 'a list -> unit +val pp_list : (out_channel -> 'a -> unit) -> out_channel -> 'a list -> unit module CamlToCoq : sig diff --git a/test-suite/success/Fourier.v b/test-suite/success/LraTest.v index b63bead47..bf3a87da2 100644 --- a/test-suite/success/Fourier.v +++ b/test-suite/success/LraTest.v @@ -1,12 +1,14 @@ -Require Import Rfunctions. -Require Import Fourier. +Require Import Reals. +Require Import Lra. + +Open Scope R_scope. Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z). -intros; split_Rabs; fourier. +intros; split_Rabs; lra. Qed. Lemma l2 : forall x y : R, x < Rabs y -> y < 1 -> x >= 0 -> - y <= 1 -> Rabs x <= 1. intros. -split_Rabs; fourier. +split_Rabs; lra. Qed. diff --git a/test-suite/unit-tests/.merlin b/test-suite/unit-tests/.merlin.in index b2279de74..b2279de74 100644 --- a/test-suite/unit-tests/.merlin +++ b/test-suite/unit-tests/.merlin.in diff --git a/theories/Reals/Machin.v b/theories/Reals/Machin.v index cdf98cbde..8f7e07ac4 100644 --- a/theories/Reals/Machin.v +++ b/theories/Reals/Machin.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import Fourier. +Require Import Lra. Require Import Rbase. Require Import Rtrigo1. Require Import Ranalysis_reg. @@ -67,7 +67,7 @@ assert (atan x <= PI/4). assert (atan y < PI/4). rewrite <- atan_1; apply atan_increasing. assumption. -rewrite Ropp_div; split; fourier. +rewrite Ropp_div; split; lra. Qed. (* A simple formula, reasonably efficient. *) @@ -77,8 +77,8 @@ assert (utility : 0 < PI/2) by (apply PI2_RGT_0). rewrite <- atan_1. rewrite (atan_sub_correct 1 (/2)). apply f_equal, f_equal; unfold atan_sub; field. - apply Rgt_not_eq; fourier. - apply tech; try split; try fourier. + apply Rgt_not_eq; lra. + apply tech; try split; try lra. apply atan_bound. Qed. @@ -86,7 +86,7 @@ Lemma Machin_4_5_239 : PI/4 = 4 * atan (/5) - atan(/239). Proof. rewrite <- atan_1. rewrite (atan_sub_correct 1 (/5)); - [ | apply Rgt_not_eq; fourier | apply tech; try split; fourier | + [ | apply Rgt_not_eq; lra | apply tech; try split; lra | apply atan_bound ]. replace (4 * atan (/5) - atan (/239)) with (atan (/5) + (atan (/5) + (atan (/5) + (atan (/5) + - @@ -95,17 +95,17 @@ apply f_equal. replace (atan_sub 1 (/5)) with (2/3) by (unfold atan_sub; field). rewrite (atan_sub_correct (2/3) (/5)); - [apply f_equal | apply Rgt_not_eq; fourier | apply tech; try split; fourier | + [apply f_equal | apply Rgt_not_eq; lra | apply tech; try split; lra | apply atan_bound ]. replace (atan_sub (2/3) (/5)) with (7/17) by (unfold atan_sub; field). rewrite (atan_sub_correct (7/17) (/5)); - [apply f_equal | apply Rgt_not_eq; fourier | apply tech; try split; fourier | + [apply f_equal | apply Rgt_not_eq; lra | apply tech; try split; lra | apply atan_bound ]. replace (atan_sub (7/17) (/5)) with (9/46) by (unfold atan_sub; field). rewrite (atan_sub_correct (9/46) (/5)); - [apply f_equal | apply Rgt_not_eq; fourier | apply tech; try split; fourier | + [apply f_equal | apply Rgt_not_eq; lra | apply tech; try split; lra | apply atan_bound ]. rewrite <- atan_opp; apply f_equal. unfold atan_sub; field. @@ -115,7 +115,7 @@ Lemma Machin_2_3_7 : PI/4 = 2 * atan(/3) + (atan (/7)). Proof. rewrite <- atan_1. rewrite (atan_sub_correct 1 (/3)); - [ | apply Rgt_not_eq; fourier | apply tech; try split; fourier | + [ | apply Rgt_not_eq; lra | apply tech; try split; lra | apply atan_bound ]. replace (2 * atan (/3) + atan (/7)) with (atan (/3) + (atan (/3) + atan (/7))) by ring. @@ -123,7 +123,7 @@ apply f_equal. replace (atan_sub 1 (/3)) with (/2) by (unfold atan_sub; field). rewrite (atan_sub_correct (/2) (/3)); - [apply f_equal | apply Rgt_not_eq; fourier | apply tech; try split; fourier | + [apply f_equal | apply Rgt_not_eq; lra | apply tech; try split; lra | apply atan_bound ]. apply f_equal; unfold atan_sub; field. Qed. @@ -138,19 +138,19 @@ Lemma PI_2_3_7_ineq : sum_f_R0 (tg_alt PI_2_3_7_tg) (S (2 * N)) <= PI / 4 <= sum_f_R0 (tg_alt PI_2_3_7_tg) (2 * N). Proof. -assert (dec3 : 0 <= /3 <= 1) by (split; fourier). -assert (dec7 : 0 <= /7 <= 1) by (split; fourier). +assert (dec3 : 0 <= /3 <= 1) by (split; lra). +assert (dec7 : 0 <= /7 <= 1) by (split; lra). assert (decr : Un_decreasing PI_2_3_7_tg). apply Ratan_seq_decreasing in dec3. apply Ratan_seq_decreasing in dec7. intros n; apply Rplus_le_compat. - apply Rmult_le_compat_l; [ fourier | exact (dec3 n)]. + apply Rmult_le_compat_l; [ lra | exact (dec3 n)]. exact (dec7 n). assert (cv : Un_cv PI_2_3_7_tg 0). apply Ratan_seq_converging in dec3. apply Ratan_seq_converging in dec7. intros eps ep. - assert (ep' : 0 < eps /3) by fourier. + assert (ep' : 0 < eps /3) by lra. destruct (dec3 _ ep') as [N1 Pn1]; destruct (dec7 _ ep') as [N2 Pn2]. exists (N1 + N2)%nat; intros n Nn. unfold PI_2_3_7_tg. @@ -161,14 +161,14 @@ assert (cv : Un_cv PI_2_3_7_tg 0). apply Rplus_lt_compat. unfold R_dist, Rminus, Rdiv. rewrite <- (Rmult_0_r 2), <- Ropp_mult_distr_r_reverse. - rewrite <- Rmult_plus_distr_l, Rabs_mult, (Rabs_pos_eq 2);[|fourier]. - rewrite Rmult_assoc; apply Rmult_lt_compat_l;[fourier | ]. + rewrite <- Rmult_plus_distr_l, Rabs_mult, (Rabs_pos_eq 2);[|lra]. + rewrite Rmult_assoc; apply Rmult_lt_compat_l;[lra | ]. apply (Pn1 n); omega. apply (Pn2 n); omega. rewrite Machin_2_3_7. -rewrite !atan_eq_ps_atan; try (split; fourier). +rewrite !atan_eq_ps_atan; try (split; lra). unfold ps_atan; destruct (in_int (/3)); destruct (in_int (/7)); - try match goal with id : ~ _ |- _ => case id; split; fourier end. + try match goal with id : ~ _ |- _ => case id; split; lra end. destruct (ps_atan_exists_1 (/3)) as [v3 Pv3]. destruct (ps_atan_exists_1 (/7)) as [v7 Pv7]. assert (main : Un_cv (sum_f_R0 (tg_alt PI_2_3_7_tg)) (2 * v3 + v7)). diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v index 61d1b5afe..146d69101 100644 --- a/theories/Reals/PSeries_reg.v +++ b/theories/Reals/PSeries_reg.v @@ -15,7 +15,7 @@ Require Import Ranalysis1. Require Import MVT. Require Import Max. Require Import Even. -Require Import Fourier. +Require Import Lra. Local Open Scope R_scope. (* Boule is French for Ball *) @@ -431,7 +431,7 @@ assert (ctrho : forall n z, Boule c d z -> continuity_pt (rho_ n) z). intros y dyz; unfold rho_; destruct (Req_EM_T y x) as [xy | xny]. rewrite xy in dyz. destruct (Rle_dec delta (Rabs (z - x))). - rewrite Rmin_left, R_dist_sym in dyz; unfold R_dist in dyz; fourier. + rewrite Rmin_left, R_dist_sym in dyz; unfold R_dist in dyz; lra. rewrite Rmin_right, R_dist_sym in dyz; unfold R_dist in dyz; [case (Rlt_irrefl _ dyz) |apply Rlt_le, Rnot_le_gt; assumption]. reflexivity. @@ -449,7 +449,7 @@ assert (ctrho : forall n z, Boule c d z -> continuity_pt (rho_ n) z). assert (CVU rho_ rho c d ). intros eps ep. assert (ep8 : 0 < eps/8). - fourier. + lra. destruct (cvu _ ep8) as [N Pn1]. assert (cauchy1 : forall n p, (N <= n)%nat -> (N <= p)%nat -> forall z, Boule c d z -> Rabs (f' n z - f' p z) < eps/4). @@ -537,7 +537,7 @@ assert (CVU rho_ rho c d ). simpl; unfold R_dist. unfold Rminus; rewrite (Rplus_comm y), Rplus_assoc, Rplus_opp_r, Rplus_0_r. rewrite Rabs_pos_eq;[ |apply Rlt_le; assumption ]. - apply Rlt_le_trans with (Rmin (Rmin d' d2) delta);[fourier | ]. + apply Rlt_le_trans with (Rmin (Rmin d' d2) delta);[lra | ]. apply Rle_trans with (Rmin d' d2); apply Rmin_l. apply Rle_trans with (1 := R_dist_tri _ _ (rho_ p (y + Rmin (Rmin d' d2) delta/2))). apply Rplus_le_compat. @@ -548,33 +548,32 @@ assert (CVU rho_ rho c d ). replace (rho_ p (y + Rmin (Rmin d' d2) delta / 2)) with ((f p (y + Rmin (Rmin d' d2) delta / 2) - f p x)/ ((y + Rmin (Rmin d' d2) delta / 2) - x)). - apply step_2; auto; try fourier. + apply step_2; auto; try lra. assert (0 < pos delta) by (apply cond_pos). apply Boule_convex with y (y + delta/2). assumption. destruct (Pdelta (y + delta/2)); auto. - rewrite xy; unfold Boule; rewrite Rabs_pos_eq; try fourier; auto. - split; try fourier. + rewrite xy; unfold Boule; rewrite Rabs_pos_eq; try lra; auto. + split; try lra. apply Rplus_le_compat_l, Rmult_le_compat_r;[ | apply Rmin_r]. now apply Rlt_le, Rinv_0_lt_compat, Rlt_0_2. - apply Rminus_not_eq_right; rewrite xy; apply Rgt_not_eq; fourier. unfold rho_. destruct (Req_EM_T (y + Rmin (Rmin d' d2) delta/2) x) as [ymx | ymnx]. - case (RIneq.Rle_not_lt _ _ (Req_le _ _ ymx)); fourier. + case (RIneq.Rle_not_lt _ _ (Req_le _ _ ymx)); lra. reflexivity. unfold rho_. destruct (Req_EM_T (y + Rmin (Rmin d' d2) delta / 2) x) as [ymx | ymnx]. - case (RIneq.Rle_not_lt _ _ (Req_le _ _ ymx)); fourier. + case (RIneq.Rle_not_lt _ _ (Req_le _ _ ymx)); lra. reflexivity. - apply Rlt_le, Pd2; split;[split;[exact I | apply Rlt_not_eq; fourier] | ]. + apply Rlt_le, Pd2; split;[split;[exact I | apply Rlt_not_eq; lra] | ]. simpl; unfold R_dist. unfold Rminus; rewrite (Rplus_comm y), Rplus_assoc, Rplus_opp_r, Rplus_0_r. - rewrite Rabs_pos_eq;[ | fourier]. - apply Rlt_le_trans with (Rmin (Rmin d' d2) delta); [fourier |]. + rewrite Rabs_pos_eq;[ | lra]. + apply Rlt_le_trans with (Rmin (Rmin d' d2) delta); [lra |]. apply Rle_trans with (Rmin d' d2). solve[apply Rmin_l]. solve[apply Rmin_r]. - apply Rlt_le, Rlt_le_trans with (eps/4);[ | fourier]. + apply Rlt_le, Rlt_le_trans with (eps/4);[ | lra]. unfold rho_; destruct (Req_EM_T y x); solve[auto]. assert (unif_ac' : forall p, (N <= p)%nat -> forall y, Boule c d y -> Rabs (rho y - rho_ p y) < eps). @@ -589,7 +588,7 @@ assert (CVU rho_ rho c d ). intros eps' ep'; simpl; exists 0%nat; intros; rewrite R_dist_eq; assumption. intros p pN y b_y. replace eps with (eps/2 + eps/2) by field. - assert (ep2 : 0 < eps/2) by fourier. + assert (ep2 : 0 < eps/2) by lra. destruct (cvrho y b_y _ ep2) as [N2 Pn2]. apply Rle_lt_trans with (1 := R_dist_tri _ _ (rho_ (max N N2) y)). apply Rplus_lt_le_compat. diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v index d4035fad6..6991923b1 100644 --- a/theories/Reals/R_sqrt.v +++ b/theories/Reals/R_sqrt.v @@ -155,6 +155,22 @@ Proof. | apply (sqrt_positivity x (Rlt_le 0 x H1)) ]. Qed. +Lemma Rlt_mult_inv_pos : forall x y:R, 0 < x -> 0 < y -> 0 < x * / y. +intros x y H H0; try assumption. +replace 0 with (x * 0). +apply Rmult_lt_compat_l; auto with real. +ring. +Qed. + +Lemma Rle_mult_inv_pos : forall x y:R, 0 <= x -> 0 < y -> 0 <= x * / y. +intros x y H H0; try assumption. +case H; intros. +red; left. +apply Rlt_mult_inv_pos; auto with real. +rewrite <- H1. +red; right; ring. +Qed. + Lemma sqrt_div_alt : forall x y : R, 0 < y -> sqrt (x / y) = sqrt x / sqrt y. Proof. @@ -176,14 +192,14 @@ Proof. clearbody Hx'. clear Hx. apply Rsqr_inj. apply sqrt_pos. - apply Fourier_util.Rle_mult_inv_pos. + apply Rle_mult_inv_pos. apply Rsqrt_positivity. now apply sqrt_lt_R0. rewrite Rsqr_div, 2!Rsqr_sqrt. unfold Rsqr. now rewrite Rsqrt_Rsqrt. now apply Rlt_le. - now apply Fourier_util.Rle_mult_inv_pos. + now apply Rle_mult_inv_pos. apply Rgt_not_eq. now apply sqrt_lt_R0. Qed. diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v index afb78e1c8..e66130b34 100644 --- a/theories/Reals/Ranalysis5.v +++ b/theories/Reals/Ranalysis5.v @@ -12,7 +12,7 @@ Require Import Rbase. Require Import Ranalysis_reg. Require Import Rfunctions. Require Import Rseries. -Require Import Fourier. +Require Import Lra. Require Import RiemannInt. Require Import SeqProp. Require Import Max. @@ -56,7 +56,7 @@ Proof. } rewrite f_eq_g in Htemp by easy. unfold id in Htemp. - fourier. + lra. Qed. Lemma derivable_pt_id_interv : forall (lb ub x:R), @@ -99,7 +99,7 @@ assert (forall x l, lb < x < ub -> (derivable_pt_abs f x l <-> derivable_pt_abs apply Req_le ; apply Rabs_right ; apply Rgt_ge ; assumption. split. assert (Sublemma : forall x y z, -z < y - x -> x < y + z). - intros ; fourier. + intros ; lra. apply Sublemma. apply Sublemma2. rewrite Rabs_Ropp. apply Rlt_le_trans with (r2:=a-lb) ; [| apply RRle_abs] ; @@ -108,7 +108,7 @@ assert (forall x l, lb < x < ub -> (derivable_pt_abs f x l <-> derivable_pt_abs apply Rlt_le_trans with (r2:=Rmin (ub - a) (a - lb)) ; [| apply Rmin_r] ; apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))) ; [| apply Rmin_r] ; assumption. assert (Sublemma : forall x y z, y < z - x -> x + y < z). - intros ; fourier. + intros ; lra. apply Sublemma. apply Sublemma2. apply Rlt_le_trans with (r2:=ub-a) ; [| apply RRle_abs] ; @@ -137,7 +137,7 @@ assert (forall x l, lb < x < ub -> (derivable_pt_abs f x l <-> derivable_pt_abs apply Req_le ; apply Rabs_right ; apply Rgt_ge ; assumption. split. assert (Sublemma : forall x y z, -z < y - x -> x < y + z). - intros ; fourier. + intros ; lra. apply Sublemma. apply Sublemma2. rewrite Rabs_Ropp. apply Rlt_le_trans with (r2:=a-lb) ; [| apply RRle_abs] ; @@ -146,7 +146,7 @@ assert (forall x l, lb < x < ub -> (derivable_pt_abs f x l <-> derivable_pt_abs apply Rlt_le_trans with (r2:=Rmin (ub - a) (a - lb)) ; [| apply Rmin_r] ; apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))) ; [| apply Rmin_r] ; assumption. assert (Sublemma : forall x y z, y < z - x -> x + y < z). - intros ; fourier. + intros ; lra. apply Sublemma. apply Sublemma2. apply Rlt_le_trans with (r2:=ub-a) ; [| apply RRle_abs] ; @@ -415,7 +415,7 @@ Ltac case_le H := let h' := fresh in match t with ?x <= ?y => case (total_order_T x y); [intros h'; case h'; clear h' | - intros h'; clear -H h'; elimtype False; fourier ] end. + intros h'; clear -H h'; elimtype False; lra ] end. (* end hide *) @@ -539,37 +539,37 @@ intros f g lb ub lb_lt_ub f_incr_interv f_eq_g f_cont_interv b b_encad. assert (x1_encad : lb <= x1 <= ub). split. apply RmaxLess2. apply Rlt_le. rewrite Hx1. rewrite Sublemma. - split. apply Rlt_trans with (r2:=x) ; fourier. + split. apply Rlt_trans with (r2:=x) ; lra. assumption. assert (x2_encad : lb <= x2 <= ub). split. apply Rlt_le ; rewrite Hx2 ; apply Rgt_lt ; rewrite Sublemma2. - split. apply Rgt_trans with (r2:=x) ; fourier. + split. apply Rgt_trans with (r2:=x) ; lra. assumption. apply Rmin_r. assert (x_lt_x2 : x < x2). rewrite Hx2. apply Rgt_lt. rewrite Sublemma2. - split ; fourier. + split ; lra. assert (x1_lt_x : x1 < x). rewrite Hx1. rewrite Sublemma. - split ; fourier. + split ; lra. exists (Rmin (f x - f x1) (f x2 - f x)). - split. apply Rmin_pos ; apply Rgt_minus. apply f_incr_interv ; [apply RmaxLess2 | | ] ; fourier. + split. apply Rmin_pos ; apply Rgt_minus. apply f_incr_interv ; [apply RmaxLess2 | | ] ; lra. apply f_incr_interv ; intuition. intros y Temp. destruct Temp as (_,y_cond). rewrite <- f_x_b in y_cond. assert (Temp : forall x y d1 d2, d1 > 0 -> d2 > 0 -> Rabs (y - x) < Rmin d1 d2 -> x - d1 <= y <= x + d2). intros. - split. assert (H10 : forall x y z, x - y <= z -> x - z <= y). intuition. fourier. + split. assert (H10 : forall x y z, x - y <= z -> x - z <= y). intuition. lra. apply H10. apply Rle_trans with (r2:=Rabs (y0 - x0)). replace (Rabs (y0 - x0)) with (Rabs (x0 - y0)). apply RRle_abs. rewrite <- Rabs_Ropp. unfold Rminus ; rewrite Ropp_plus_distr. rewrite Ropp_involutive. intuition. apply Rle_trans with (r2:= Rmin d1 d2). apply Rlt_le ; assumption. apply Rmin_l. - assert (H10 : forall x y z, x - y <= z -> x <= y + z). intuition. fourier. + assert (H10 : forall x y z, x - y <= z -> x <= y + z). intuition. lra. apply H10. apply Rle_trans with (r2:=Rabs (y0 - x0)). apply RRle_abs. apply Rle_trans with (r2:= Rmin d1 d2). apply Rlt_le ; assumption. apply Rmin_r. @@ -602,12 +602,12 @@ intros f g lb ub lb_lt_ub f_incr_interv f_eq_g f_cont_interv b b_encad. assert (x1_neq_x' : x1 <> x'). intro Hfalse. rewrite Hfalse, f_x'_y in y_cond. assert (Hf : Rabs (y - f x) < f x - y). - apply Rlt_le_trans with (r2:=Rmin (f x - y) (f x2 - f x)). fourier. + apply Rlt_le_trans with (r2:=Rmin (f x - y) (f x2 - f x)). lra. apply Rmin_l. assert(Hfin : f x - y < f x - y). apply Rle_lt_trans with (r2:=Rabs (y - f x)). replace (Rabs (y - f x)) with (Rabs (f x - y)). apply RRle_abs. - rewrite <- Rabs_Ropp. replace (- (f x - y)) with (y - f x) by field ; reflexivity. fourier. + rewrite <- Rabs_Ropp. replace (- (f x - y)) with (y - f x) by field ; reflexivity. lra. apply (Rlt_irrefl (f x - y)) ; assumption. split ; intuition. assert (x'_lb : x - eps < x'). @@ -619,17 +619,17 @@ intros f g lb ub lb_lt_ub f_incr_interv f_eq_g f_cont_interv b b_encad. assert (x1_neq_x' : x' <> x2). intro Hfalse. rewrite <- Hfalse, f_x'_y in y_cond. assert (Hf : Rabs (y - f x) < y - f x). - apply Rlt_le_trans with (r2:=Rmin (f x - f x1) (y - f x)). fourier. + apply Rlt_le_trans with (r2:=Rmin (f x - f x1) (y - f x)). lra. apply Rmin_r. assert(Hfin : y - f x < y - f x). - apply Rle_lt_trans with (r2:=Rabs (y - f x)). apply RRle_abs. fourier. + apply Rle_lt_trans with (r2:=Rabs (y - f x)). apply RRle_abs. lra. apply (Rlt_irrefl (y - f x)) ; assumption. split ; intuition. assert (x'_ub : x' < x + eps). apply Sublemma3. split. intuition. apply Rlt_not_eq. apply Rlt_le_trans with (r2:=x2) ; [ |rewrite Hx2 ; apply Rmin_l] ; intuition. - apply Rabs_def1 ; fourier. + apply Rabs_def1 ; lra. assumption. split. apply Rle_trans with (r2:=x1) ; intuition. apply Rle_trans with (r2:=x2) ; intuition. @@ -742,7 +742,7 @@ intros f g lb ub x Prf g_cont_pur lb_lt_ub x_encad Prg_incr f_eq_g df_neq. assert (lb <= x + h <= ub). split. assert (Sublemma : forall x y z, -z <= y - x -> x <= y + z). - intros ; fourier. + intros ; lra. apply Sublemma. apply Rlt_le ; apply Sublemma2. rewrite Rabs_Ropp. apply Rlt_le_trans with (r2:=x-lb) ; [| apply RRle_abs] ; @@ -751,7 +751,7 @@ intros f g lb ub x Prf g_cont_pur lb_lt_ub x_encad Prg_incr f_eq_g df_neq. apply Rlt_le_trans with (r2:=delta''). assumption. intuition. apply Rmin_r. apply Rgt_minus. intuition. assert (Sublemma : forall x y z, y <= z - x -> x + y <= z). - intros ; fourier. + intros ; lra. apply Sublemma. apply Rlt_le ; apply Sublemma2. apply Rlt_le_trans with (r2:=ub-x) ; [| apply RRle_abs] ; @@ -767,7 +767,7 @@ intros f g lb ub x Prf g_cont_pur lb_lt_ub x_encad Prg_incr f_eq_g df_neq. assumption. split ; [|intuition]. assert (Sublemma : forall x y z, - z <= y - x -> x <= y + z). - intros ; fourier. + intros ; lra. apply Sublemma ; apply Rlt_le ; apply Sublemma2. rewrite Rabs_Ropp. apply Rlt_le_trans with (r2:=x-lb) ; [| apply RRle_abs] ; apply Rlt_le_trans with (r2:=Rmin (x - lb) (ub - x)) ; [| apply Rmin_l] ; @@ -1031,7 +1031,7 @@ Lemma derivable_pt_lim_CVU : forall (fn fn':nat -> R -> R) (f g:R->R) derivable_pt_lim f x (g x). Proof. intros fn fn' f g x c' r xinb Dfn_eq_fn' fn_CV_f fn'_CVU_g g_cont eps eps_pos. -assert (eps_8_pos : 0 < eps / 8) by fourier. +assert (eps_8_pos : 0 < eps / 8) by lra. elim (g_cont x xinb _ eps_8_pos) ; clear g_cont ; intros delta1 (delta1_pos, g_cont). destruct (Ball_in_inter _ _ _ _ _ xinb @@ -1041,11 +1041,11 @@ exists delta; intros h hpos hinbdelta. assert (eps'_pos : 0 < (Rabs h) * eps / 4). unfold Rdiv ; rewrite Rmult_assoc ; apply Rmult_lt_0_compat. apply Rabs_pos_lt ; assumption. -fourier. +lra. destruct (fn_CV_f x xinb ((Rabs h) * eps / 4) eps'_pos) as [N2 fnx_CV_fx]. assert (xhinbxdelta : Boule x delta (x + h)). clear -hinbdelta; apply Rabs_def2 in hinbdelta; unfold Boule; simpl. - destruct hinbdelta; apply Rabs_def1; fourier. + destruct hinbdelta; apply Rabs_def1; lra. assert (t : Boule c' r (x + h)). apply Pdelta in xhinbxdelta; tauto. destruct (fn_CV_f (x+h) t ((Rabs h) * eps / 4) eps'_pos) as [N1 fnxh_CV_fxh]. @@ -1064,17 +1064,17 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn exists (fn' N c) ; apply Dfn_eq_fn'. assert (t : Boule x delta c). apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta; destruct c_encad. - apply Rabs_def2 in xinb; apply Rabs_def1; fourier. + apply Rabs_def2 in xinb; apply Rabs_def1; lra. apply Pdelta in t; tauto. assert (pr2 : forall c : R, x + h < c < x -> derivable_pt id c). solve[intros; apply derivable_id]. - assert (xh_x : x+h < x) by fourier. + assert (xh_x : x+h < x) by lra. assert (pr3 : forall c : R, x + h <= c <= x -> continuity_pt (fn N) c). intros c c_encad ; apply derivable_continuous_pt. exists (fn' N c) ; apply Dfn_eq_fn' ; intuition. assert (t : Boule x delta c). apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta. - apply Rabs_def2 in xinb; apply Rabs_def1; fourier. + apply Rabs_def2 in xinb; apply Rabs_def1; lra. apply Pdelta in t; tauto. assert (pr4 : forall c : R, x + h <= c <= x -> continuity_pt id c). solve[intros; apply derivable_continuous ; apply derivable_id]. @@ -1117,7 +1117,7 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn assert (t : Boule x delta c). destruct P. apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta. - apply Rabs_def2 in xinb; apply Rabs_def1; fourier. + apply Rabs_def2 in xinb; apply Rabs_def1; lra. apply Pdelta in t; tauto. apply Rlt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * (eps / 8) + Rabs h * (eps / 8)). @@ -1131,27 +1131,27 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn apply Rlt_trans with (Rabs h). apply Rabs_def1. apply Rlt_trans with 0. - destruct P; fourier. + destruct P; lra. apply Rabs_pos_lt ; assumption. - rewrite <- Rabs_Ropp, Rabs_pos_eq, Ropp_involutive;[ | fourier]. - destruct P; fourier. + rewrite <- Rabs_Ropp, Rabs_pos_eq, Ropp_involutive;[ | lra]. + destruct P; lra. clear -Pdelta xhinbxdelta. apply Pdelta in xhinbxdelta; destruct xhinbxdelta as [_ P']. apply Rabs_def2 in P'; simpl in P'; destruct P'; - apply Rabs_def1; fourier. + apply Rabs_def1; lra. rewrite Rplus_assoc ; rewrite Rplus_assoc ; rewrite <- Rmult_plus_distr_l. replace (Rabs h * eps / 4 + (Rabs h * eps / 4 + Rabs h * (eps / 8 + eps / 8))) with (Rabs h * (eps / 4 + eps / 4 + eps / 8 + eps / 8)) by field. apply Rmult_lt_compat_l. apply Rabs_pos_lt ; assumption. - fourier. + lra. assert (H := pr1 c P) ; elim H ; clear H ; intros l Hl. assert (Temp : l = fn' N c). assert (bc'rc : Boule c' r c). assert (t : Boule x delta c). clear - xhinbxdelta P. destruct P; apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta. - apply Rabs_def1; fourier. + apply Rabs_def1; lra. apply Pdelta in t; tauto. assert (Hl' := Dfn_eq_fn' c N bc'rc). unfold derivable_pt_abs in Hl; clear -Hl Hl'. @@ -1175,17 +1175,17 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn exists (fn' N c) ; apply Dfn_eq_fn'. assert (t : Boule x delta c). apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta; destruct c_encad. - apply Rabs_def2 in xinb; apply Rabs_def1; fourier. + apply Rabs_def2 in xinb; apply Rabs_def1; lra. apply Pdelta in t; tauto. assert (pr2 : forall c : R, x < c < x + h -> derivable_pt id c). solve[intros; apply derivable_id]. - assert (xh_x : x < x + h) by fourier. + assert (xh_x : x < x + h) by lra. assert (pr3 : forall c : R, x <= c <= x + h -> continuity_pt (fn N) c). intros c c_encad ; apply derivable_continuous_pt. exists (fn' N c) ; apply Dfn_eq_fn' ; intuition. assert (t : Boule x delta c). apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta. - apply Rabs_def2 in xinb; apply Rabs_def1; fourier. + apply Rabs_def2 in xinb; apply Rabs_def1; lra. apply Pdelta in t; tauto. assert (pr4 : forall c : R, x <= c <= x + h -> continuity_pt id c). solve[intros; apply derivable_continuous ; apply derivable_id]. @@ -1223,7 +1223,7 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn assert (t : Boule x delta c). destruct P. apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta. - apply Rabs_def2 in xinb; apply Rabs_def1; fourier. + apply Rabs_def2 in xinb; apply Rabs_def1; lra. apply Pdelta in t; tauto. apply Rlt_trans with (Rabs h * eps / 4 + Rabs h * eps / 4 + Rabs h * (eps / 8) + Rabs h * (eps / 8)). @@ -1236,27 +1236,27 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn apply Rlt_not_eq ; exact (proj1 P). apply Rlt_trans with (Rabs h). apply Rabs_def1. - destruct P; rewrite Rabs_pos_eq;fourier. + destruct P; rewrite Rabs_pos_eq;lra. apply Rle_lt_trans with 0. - assert (t := Rabs_pos h); clear -t; fourier. - clear -P; destruct P; fourier. + assert (t := Rabs_pos h); clear -t; lra. + clear -P; destruct P; lra. clear -Pdelta xhinbxdelta. apply Pdelta in xhinbxdelta; destruct xhinbxdelta as [_ P']. apply Rabs_def2 in P'; simpl in P'; destruct P'; - apply Rabs_def1; fourier. + apply Rabs_def1; lra. rewrite Rplus_assoc ; rewrite Rplus_assoc ; rewrite <- Rmult_plus_distr_l. replace (Rabs h * eps / 4 + (Rabs h * eps / 4 + Rabs h * (eps / 8 + eps / 8))) with (Rabs h * (eps / 4 + eps / 4 + eps / 8 + eps / 8)) by field. apply Rmult_lt_compat_l. apply Rabs_pos_lt ; assumption. - fourier. + lra. assert (H := pr1 c P) ; elim H ; clear H ; intros l Hl. assert (Temp : l = fn' N c). assert (bc'rc : Boule c' r c). assert (t : Boule x delta c). clear - xhinbxdelta P. destruct P; apply Rabs_def2 in xhinbxdelta; destruct xhinbxdelta. - apply Rabs_def1; fourier. + apply Rabs_def1; lra. apply Pdelta in t; tauto. assert (Hl' := Dfn_eq_fn' c N bc'rc). unfold derivable_pt_abs in Hl; clear -Hl Hl'. diff --git a/theories/Reals/Ratan.v b/theories/Reals/Ratan.v index ce39d5ffe..03e6ff61a 100644 --- a/theories/Reals/Ratan.v +++ b/theories/Reals/Ratan.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import Fourier. +Require Import Lra. Require Import Rbase. Require Import PSeries_reg. Require Import Rtrigo1. @@ -32,7 +32,7 @@ intros x y; unfold Rdiv; rewrite <-Ropp_mult_distr_l_reverse; reflexivity. Qed. Definition pos_half_prf : 0 < /2. -Proof. fourier. Qed. +Proof. lra. Qed. Definition pos_half := mkposreal (/2) pos_half_prf. @@ -40,15 +40,15 @@ Lemma Boule_half_to_interval : forall x , Boule (/2) pos_half x -> 0 <= x <= 1. Proof. unfold Boule, pos_half; simpl. -intros x b; apply Rabs_def2 in b; destruct b; split; fourier. +intros x b; apply Rabs_def2 in b; destruct b; split; lra. Qed. Lemma Boule_lt : forall c r x, Boule c r x -> Rabs x < Rabs c + r. Proof. unfold Boule; intros c r x h. apply Rabs_def2 in h; destruct h; apply Rabs_def1; - (destruct (Rle_lt_dec 0 c);[rewrite Rabs_pos_eq; fourier | - rewrite <- Rabs_Ropp, Rabs_pos_eq; fourier]). + (destruct (Rle_lt_dec 0 c);[rewrite Rabs_pos_eq; lra | + rewrite <- Rabs_Ropp, Rabs_pos_eq; lra]). Qed. (* The following lemma does not belong here. *) @@ -117,53 +117,53 @@ intros [ | N] Npos n decr to0 cv nN. case (even_odd_cor n) as [p' [neven | nodd]]. rewrite neven. destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E]. - unfold R_dist; rewrite Rabs_pos_eq;[ | fourier]. + unfold R_dist; rewrite Rabs_pos_eq;[ | lra]. assert (dist : (p <= p')%nat) by omega. assert (t := decreasing_prop _ _ _ (CV_ALT_step1 f decr) dist). apply Rle_trans with (sum_f_R0 (tg_alt f) (2 * p) - l). unfold Rminus; apply Rplus_le_compat_r; exact t. match goal with _ : ?a <= l, _ : l <= ?b |- _ => replace (f (S (2 * p))) with (b - a) by - (rewrite tech5; unfold tg_alt; rewrite pow_1_odd; ring); fourier + (rewrite tech5; unfold tg_alt; rewrite pow_1_odd; ring); lra end. rewrite nodd; destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E]. unfold R_dist; rewrite <- Rabs_Ropp, Rabs_pos_eq, Ropp_minus_distr; - [ | fourier]. + [ | lra]. assert (dist : (p <= p')%nat) by omega. apply Rle_trans with (l - sum_f_R0 (tg_alt f) (S (2 * p))). unfold Rminus; apply Rplus_le_compat_l, Ropp_le_contravar. solve[apply Rge_le, (growing_prop _ _ _ (CV_ALT_step0 f decr) dist)]. unfold Rminus; rewrite tech5, Ropp_plus_distr, <- Rplus_assoc. - unfold tg_alt at 2; rewrite pow_1_odd; fourier. + unfold tg_alt at 2; rewrite pow_1_odd; lra. rewrite Nodd; destruct (alternated_series_ineq _ _ p decr to0 cv) as [B _]. destruct (alternated_series_ineq _ _ (S p) decr to0 cv) as [_ C]. assert (keep : (2 * S p = S (S ( 2 * p)))%nat) by ring. case (even_odd_cor n) as [p' [neven | nodd]]. rewrite neven; destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E]. - unfold R_dist; rewrite Rabs_pos_eq;[ | fourier]. + unfold R_dist; rewrite Rabs_pos_eq;[ | lra]. assert (dist : (S p < S p')%nat) by omega. apply Rle_trans with (sum_f_R0 (tg_alt f) (2 * S p) - l). unfold Rminus; apply Rplus_le_compat_r, (decreasing_prop _ _ _ (CV_ALT_step1 f decr)). omega. rewrite keep, tech5; unfold tg_alt at 2; rewrite <- keep, pow_1_even. - fourier. + lra. rewrite nodd; destruct (alternated_series_ineq _ _ p' decr to0 cv) as [D E]. - unfold R_dist; rewrite <- Rabs_Ropp, Rabs_pos_eq;[ | fourier]. + unfold R_dist; rewrite <- Rabs_Ropp, Rabs_pos_eq;[ | lra]. rewrite Ropp_minus_distr. apply Rle_trans with (l - sum_f_R0 (tg_alt f) (S (2 * p))). unfold Rminus; apply Rplus_le_compat_l, Ropp_le_contravar, Rge_le, (growing_prop _ _ _ (CV_ALT_step0 f decr)); omega. generalize C; rewrite keep, tech5; unfold tg_alt. rewrite <- keep, pow_1_even. - assert (t : forall a b c, a <= b + 1 * c -> a - b <= c) by (intros; fourier). + assert (t : forall a b c, a <= b + 1 * c -> a - b <= c) by (intros; lra). solve[apply t]. clear WLOG; intros Hyp [ | n] decr to0 cv _. generalize (alternated_series_ineq f l 0 decr to0 cv). unfold R_dist, tg_alt; simpl; rewrite !Rmult_1_l, !Rmult_1_r. assert (f 1%nat <= f 0%nat) by apply decr. - intros [A B]; rewrite Rabs_pos_eq; fourier. + intros [A B]; rewrite Rabs_pos_eq; lra. apply Rle_trans with (f 1%nat). apply (Hyp 1%nat (le_n 1) (S n) decr to0 cv). omega. @@ -180,7 +180,7 @@ Lemma Alt_CVU : forall (f : nat -> R -> R) g h c r, CVU (fun N x => sum_f_R0 (tg_alt (fun i => f i x)) N) g c r. Proof. intros f g h c r decr to0 to_g bound bound0 eps ep. -assert (ep' : 0 <eps/2) by fourier. +assert (ep' : 0 <eps/2) by lra. destruct (bound0 _ ep) as [N Pn]; exists N. intros n y nN dy. rewrite <- Rabs_Ropp, Ropp_minus_distr; apply Rle_lt_trans with (f n y). @@ -201,14 +201,14 @@ intros x; destruct (Rle_lt_dec 0 x). replace (x ^ 2) with (x * x) by field. apply Rmult_le_pos; assumption. replace (x ^ 2) with ((-x) * (-x)) by field. -apply Rmult_le_pos; fourier. +apply Rmult_le_pos; lra. Qed. Lemma pow2_abs : forall x, Rabs x ^ 2 = x ^ 2. Proof. intros x; destruct (Rle_lt_dec 0 x). rewrite Rabs_pos_eq;[field | assumption]. -rewrite <- Rabs_Ropp, Rabs_pos_eq;[field | fourier]. +rewrite <- Rabs_Ropp, Rabs_pos_eq;[field | lra]. Qed. (** * Properties of tangent *) @@ -307,18 +307,18 @@ destruct (MVT_cor1 cos (PI/2) x derivable_cos xgtpi2) as [c [Pc [cint1 cint2]]]. revert Pc; rewrite cos_PI2, Rminus_0_r. rewrite <- (pr_nu cos c (derivable_pt_cos c)), derive_pt_cos. -assert (0 < c < 2) by (split; assert (t := PI2_RGT_0); fourier). +assert (0 < c < 2) by (split; assert (t := PI2_RGT_0); lra). assert (0 < sin c) by now apply sin_pos_tech. intros Pc. case (Rlt_not_le _ _ cx). rewrite <- (Rplus_0_l (cos x)), Pc, Ropp_mult_distr_l_reverse. -apply Rle_minus, Rmult_le_pos;[apply Rlt_le; assumption | fourier ]. +apply Rle_minus, Rmult_le_pos;[apply Rlt_le; assumption | lra ]. Qed. Lemma PI2_3_2 : 3/2 < PI/2. Proof. -apply PI2_lower_bound;[split; fourier | ]. -destruct (pre_cos_bound (3/2) 1) as [t _]; [fourier | fourier | ]. +apply PI2_lower_bound;[split; lra | ]. +destruct (pre_cos_bound (3/2) 1) as [t _]; [lra | lra | ]. apply Rlt_le_trans with (2 := t); clear t. unfold cos_approx; simpl; unfold cos_term. rewrite !INR_IZR_INZ. @@ -330,7 +330,7 @@ apply Rdiv_lt_0_compat ; now apply IZR_lt. Qed. Lemma PI2_1 : 1 < PI/2. -Proof. assert (t := PI2_3_2); fourier. Qed. +Proof. assert (t := PI2_3_2); lra. Qed. Lemma tan_increasing : forall x y:R, @@ -347,7 +347,7 @@ intros x y Z_le_x x_lt_y y_le_1. derivable_pt tan x). intros ; apply derivable_pt_tan ; intuition. apply derive_increasing_interv with (a:=-PI/2) (b:=PI/2) (pr:=local_derivable_pt_tan) ; intuition. - fourier. + lra. assert (Temp := pr_nu tan t (derivable_pt_tan t t_encad) (local_derivable_pt_tan t t_encad)) ; rewrite <- Temp ; clear Temp. assert (Temp := derive_pt_tan t t_encad) ; rewrite Temp ; clear Temp. @@ -414,49 +414,49 @@ Qed. (** * Definition of arctangent as the reciprocal function of tangent and proof of this status *) Lemma tan_1_gt_1 : tan 1 > 1. Proof. -assert (0 < cos 1) by (apply cos_gt_0; assert (t:=PI2_1); fourier). +assert (0 < cos 1) by (apply cos_gt_0; assert (t:=PI2_1); lra). assert (t1 : cos 1 <= 1 - 1/2 + 1/24). - destruct (pre_cos_bound 1 0) as [_ t]; try fourier; revert t. + destruct (pre_cos_bound 1 0) as [_ t]; try lra; revert t. unfold cos_approx, cos_term; simpl; intros t; apply Rle_trans with (1:=t). clear t; apply Req_le; field. assert (t2 : 1 - 1/6 <= sin 1). - destruct (pre_sin_bound 1 0) as [t _]; try fourier; revert t. + destruct (pre_sin_bound 1 0) as [t _]; try lra; revert t. unfold sin_approx, sin_term; simpl; intros t; apply Rle_trans with (2:=t). clear t; apply Req_le; field. pattern 1 at 2; replace 1 with - (cos 1 / cos 1) by (field; apply Rgt_not_eq; fourier). + (cos 1 / cos 1) by (field; apply Rgt_not_eq; lra). apply Rlt_gt; apply (Rmult_lt_compat_r (/ cos 1) (cos 1) (sin 1)). apply Rinv_0_lt_compat; assumption. apply Rle_lt_trans with (1 := t1); apply Rlt_le_trans with (2 := t2). -fourier. +lra. Qed. Definition frame_tan y : {x | 0 < x < PI/2 /\ Rabs y < tan x}. Proof. destruct (total_order_T (Rabs y) 1) as [Hs|Hgt]. - assert (yle1 : Rabs y <= 1) by (destruct Hs; fourier). + assert (yle1 : Rabs y <= 1) by (destruct Hs; lra). clear Hs; exists 1; split;[split; [exact Rlt_0_1 | exact PI2_1] | ]. apply Rle_lt_trans with (1 := yle1); exact tan_1_gt_1. assert (0 < / (Rabs y + 1)). - apply Rinv_0_lt_compat; fourier. + apply Rinv_0_lt_compat; lra. set (u := /2 * / (Rabs y + 1)). assert (0 < u). - apply Rmult_lt_0_compat; [fourier | assumption]. + apply Rmult_lt_0_compat; [lra | assumption]. assert (vlt1 : / (Rabs y + 1) < 1). apply Rmult_lt_reg_r with (Rabs y + 1). - assert (t := Rabs_pos y); fourier. - rewrite Rinv_l; [rewrite Rmult_1_l | apply Rgt_not_eq]; fourier. + assert (t := Rabs_pos y); lra. + rewrite Rinv_l; [rewrite Rmult_1_l | apply Rgt_not_eq]; lra. assert (vlt2 : u < 1). apply Rlt_trans with (/ (Rabs y + 1)). rewrite double_var. - assert (t : forall x, 0 < x -> x < x + x) by (clear; intros; fourier). + assert (t : forall x, 0 < x -> x < x + x) by (clear; intros; lra). unfold u; rewrite Rmult_comm; apply t. unfold Rdiv; rewrite Rmult_comm; assumption. assumption. assert(int : 0 < PI / 2 - u < PI / 2). split. assert (t := PI2_1); apply Rlt_Rminus, Rlt_trans with (2 := t); assumption. - assert (dumb : forall x y, 0 < y -> x - y < x) by (clear; intros; fourier). + assert (dumb : forall x y, 0 < y -> x - y < x) by (clear; intros; lra). apply dumb; clear dumb; assumption. exists (PI/2 - u). assert (tmp : forall x y, 0 < x -> y < 1 -> x * y < x). @@ -473,7 +473,7 @@ split. assert (sin u < u). assert (t1 : 0 <= u) by (apply Rlt_le; assumption). assert (t2 : u <= 4) by - (apply Rle_trans with 1;[apply Rlt_le | fourier]; assumption). + (apply Rle_trans with 1;[apply Rlt_le | lra]; assumption). destruct (pre_sin_bound u 0 t1 t2) as [_ t]. apply Rle_lt_trans with (1 := t); clear t1 t2 t. unfold sin_approx; simpl; unfold sin_term; simpl ((-1) ^ 0); @@ -503,17 +503,17 @@ split. solve[apply Rinv_0_lt_compat, INR_fact_lt_0]. apply Rlt_trans with (2 := vlt2). simpl; unfold u; apply tmp; auto; rewrite Rmult_1_r; assumption. - apply Rlt_trans with (Rabs y + 1);[fourier | ]. + apply Rlt_trans with (Rabs y + 1);[lra | ]. pattern (Rabs y + 1) at 1; rewrite <- (Rinv_involutive (Rabs y + 1)); - [ | apply Rgt_not_eq; fourier]. + [ | apply Rgt_not_eq; lra]. rewrite <- Rinv_mult_distr. apply Rinv_lt_contravar. apply Rmult_lt_0_compat. - apply Rmult_lt_0_compat;[fourier | assumption]. + apply Rmult_lt_0_compat;[lra | assumption]. assumption. replace (/(Rabs y + 1)) with (2 * u). - fourier. - unfold u; field; apply Rgt_not_eq; clear -Hgt; fourier. + lra. + unfold u; field; apply Rgt_not_eq; clear -Hgt; lra. solve[discrR]. apply Rgt_not_eq; assumption. unfold tan. @@ -522,22 +522,22 @@ set (u' := PI / 2); unfold Rdiv; apply Rmult_lt_compat_r; unfold u'. rewrite cos_shift; assumption. assert (vlt3 : u < /4). replace (/4) with (/2 * /2) by field. - unfold u; apply Rmult_lt_compat_l;[fourier | ]. + unfold u; apply Rmult_lt_compat_l;[lra | ]. apply Rinv_lt_contravar. - apply Rmult_lt_0_compat; fourier. - fourier. -assert (1 < PI / 2 - u) by (assert (t := PI2_3_2); fourier). + apply Rmult_lt_0_compat; lra. + lra. +assert (1 < PI / 2 - u) by (assert (t := PI2_3_2); lra). apply Rlt_trans with (sin 1). - assert (t' : 1 <= 4) by fourier. + assert (t' : 1 <= 4) by lra. destruct (pre_sin_bound 1 0 (Rlt_le _ _ Rlt_0_1) t') as [t _]. apply Rlt_le_trans with (2 := t); clear t. - simpl plus; replace (sin_approx 1 1) with (5/6);[fourier | ]. + simpl plus; replace (sin_approx 1 1) with (5/6);[lra | ]. unfold sin_approx, sin_term; simpl; field. apply sin_increasing_1. - assert (t := PI2_1); fourier. + assert (t := PI2_1); lra. apply Rlt_le, PI2_1. - assert (t := PI2_1); fourier. - fourier. + assert (t := PI2_1); lra. + lra. assumption. Qed. @@ -547,7 +547,7 @@ intros x h; rewrite Ropp_div; apply Ropp_lt_contravar; assumption. Qed. Lemma pos_opp_lt : forall x, 0 < x -> -x < x. -Proof. intros; fourier. Qed. +Proof. intros; lra. Qed. Lemma tech_opp_tan : forall x y, -tan x < y -> tan (-x) < y. Proof. @@ -562,7 +562,7 @@ set (pr := (conj (tech_opp_tan _ _ (proj2 (Rabs_def2 _ _ Ptan_ub))) destruct (exists_atan_in_frame (-ub) ub y (pos_opp_lt _ ub0) (ub_opp _ ubpi2) ubpi2 pr) as [v [[vl vu] vq]]. exists v; clear pr. -split;[rewrite Ropp_div; split; fourier | assumption]. +split;[rewrite Ropp_div; split; lra | assumption]. Qed. Definition atan x := let (v, _) := pre_atan x in v. @@ -581,7 +581,7 @@ Lemma atan_opp : forall x, atan (- x) = - atan x. Proof. intros x; generalize (atan_bound (-x)); rewrite Ropp_div;intros [a b]. generalize (atan_bound x); rewrite Ropp_div; intros [c d]. -apply tan_is_inj; try rewrite Ropp_div; try split; try fourier. +apply tan_is_inj; try rewrite Ropp_div; try split; try lra. rewrite tan_neg, !atan_right_inv; reflexivity. Qed. @@ -604,23 +604,23 @@ assert (int_tan : forall y, tan (- ub) <= y -> y <= tan ub -> rewrite <- (atan_right_inv y); apply tan_increasing. destruct (atan_bound y); assumption. assumption. - fourier. - fourier. + lra. + lra. destruct (Rle_lt_dec (atan y) ub) as [h | abs]; auto. assert (tan ub < y). rewrite <- (atan_right_inv y); apply tan_increasing. - rewrite Ropp_div; fourier. + rewrite Ropp_div; lra. assumption. destruct (atan_bound y); assumption. - fourier. + lra. assert (incr : forall x y, -ub <= x -> x < y -> y <= ub -> tan x < tan y). intros y z l yz u; apply tan_increasing. - rewrite Ropp_div; fourier. + rewrite Ropp_div; lra. assumption. - fourier. + lra. assert (der : forall a, -ub <= a <= ub -> derivable_pt tan a). intros a [la ua]; apply derivable_pt_tan. - rewrite Ropp_div; split; fourier. + rewrite Ropp_div; split; lra. assert (df_neq : derive_pt tan (atan x) (derivable_pt_recip_interv_prelim1 tan atan (- ub) ub x lb_lt_ub xint inv_p int_tan incr der) <> 0). @@ -651,7 +651,7 @@ Qed. Lemma atan_0 : atan 0 = 0. Proof. apply tan_is_inj; try (apply atan_bound). - assert (t := PI_RGT_0); rewrite Ropp_div; split; fourier. + assert (t := PI_RGT_0); rewrite Ropp_div; split; lra. rewrite atan_right_inv, tan_0. reflexivity. Qed. @@ -659,7 +659,7 @@ Qed. Lemma atan_1 : atan 1 = PI/4. Proof. assert (ut := PI_RGT_0). -assert (-PI/2 < PI/4 < PI/2) by (rewrite Ropp_div; split; fourier). +assert (-PI/2 < PI/4 < PI/2) by (rewrite Ropp_div; split; lra). assert (t := atan_bound 1). apply tan_is_inj; auto. rewrite tan_PI4, atan_right_inv; reflexivity. @@ -688,23 +688,23 @@ assert (int_tan : forall y, tan (- ub) <= y -> y <= tan ub -> rewrite <- (atan_right_inv y); apply tan_increasing. destruct (atan_bound y); assumption. assumption. - fourier. - fourier. + lra. + lra. destruct (Rle_lt_dec (atan y) ub) as [h | abs]; auto. assert (tan ub < y). rewrite <- (atan_right_inv y); apply tan_increasing. - rewrite Ropp_div; fourier. + rewrite Ropp_div; lra. assumption. destruct (atan_bound y); assumption. - fourier. + lra. assert (incr : forall x y, -ub <= x -> x < y -> y <= ub -> tan x < tan y). intros y z l yz u; apply tan_increasing. - rewrite Ropp_div; fourier. + rewrite Ropp_div; lra. assumption. - fourier. + lra. assert (der : forall a, -ub <= a <= ub -> derivable_pt tan a). intros a [la ua]; apply derivable_pt_tan. - rewrite Ropp_div; split; fourier. + rewrite Ropp_div; split; lra. assert (df_neq : derive_pt tan (atan x) (derivable_pt_recip_interv_prelim1 tan atan (- ub) ub x lb_lt_ub xint inv_p int_tan incr der) <> 0). @@ -883,7 +883,7 @@ Proof. destruct (Rle_lt_dec 0 x). assert (pr : 0 <= x <= 1) by tauto. exact (ps_atan_exists_01 x pr). -assert (pr : 0 <= -x <= 1) by (destruct Hx; split; fourier). +assert (pr : 0 <= -x <= 1) by (destruct Hx; split; lra). destruct (ps_atan_exists_01 _ pr) as [v Pv]. exists (-v). apply (Un_cv_ext (fun n => (- 1) * sum_f_R0 (tg_alt (Ratan_seq (- x))) n)). @@ -898,8 +898,8 @@ Proof. destruct (Rle_lt_dec x 1). destruct (Rle_lt_dec (-1) x). left;split; auto. - right;intros [a1 a2]; fourier. -right;intros [a1 a2]; fourier. + right;intros [a1 a2]; lra. +right;intros [a1 a2]; lra. Qed. Definition ps_atan (x : R) : R := @@ -922,7 +922,7 @@ unfold ps_atan. unfold Rdiv; rewrite !Rmult_0_l, Rmult_0_r; reflexivity. intros eps ep; exists 0%nat; intros n _; unfold R_dist. rewrite Rminus_0_r, Rabs_pos_eq; auto with real. -case h2; split; fourier. +case h2; split; lra. Qed. Lemma ps_atan_exists_1_opp : @@ -948,9 +948,9 @@ destruct (in_int (- x)) as [inside | outside]. destruct (in_int x) as [ins' | outs']. generalize (ps_atan_exists_1_opp x inside ins'). intros h; exact h. - destruct inside; case outs'; split; fourier. + destruct inside; case outs'; split; lra. destruct (in_int x) as [ins' | outs']. - destruct outside; case ins'; split; fourier. + destruct outside; case ins'; split; lra. apply atan_opp. Qed. @@ -1057,7 +1057,7 @@ Proof. intros x n. assert (dif : - x ^ 2 <> 1). apply Rlt_not_eq; apply Rle_lt_trans with 0;[ | apply Rlt_0_1]. -assert (t := pow2_ge_0 x); fourier. +assert (t := pow2_ge_0 x); lra. replace (1 + x ^ 2) with (1 - - (x ^ 2)) by ring; rewrite <- (tech3 _ n dif). apply sum_eq; unfold tg_alt, Datan_seq; intros i _. rewrite pow_mult, <- Rpow_mult_distr. @@ -1073,7 +1073,7 @@ intros x y n n_lb x_encad ; assert (x_pos : x >= 0) by intuition. apply False_ind ; intuition. clear -x_encad x_pos y_pos ; induction n ; unfold Datan_seq. case x_pos ; clear x_pos ; intro x_pos. - simpl ; apply Rmult_gt_0_lt_compat ; intuition. fourier. + simpl ; apply Rmult_gt_0_lt_compat ; intuition. lra. rewrite x_pos ; rewrite pow_i. replace (y ^ (2*1)) with (y*y). apply Rmult_gt_0_compat ; assumption. simpl ; field. @@ -1084,7 +1084,7 @@ intros x y n n_lb x_encad ; assert (x_pos : x >= 0) by intuition. case x_pos ; clear x_pos ; intro x_pos. rewrite Hrew ; rewrite Hrew. apply Rmult_gt_0_lt_compat ; intuition. - apply Rmult_gt_0_lt_compat ; intuition ; fourier. + apply Rmult_gt_0_lt_compat ; intuition ; lra. rewrite x_pos. rewrite pow_i ; intuition. Qed. @@ -1141,7 +1141,7 @@ elim (pow_lt_1_zero _ x_ub2 _ eps'_pos) ; intros N HN ; exists N. intros n Hn. assert (H1 : - x^2 <> 1). apply Rlt_not_eq; apply Rle_lt_trans with (2 := Rlt_0_1). -assert (t := pow2_ge_0 x); fourier. +assert (t := pow2_ge_0 x); lra. rewrite Datan_sum_eq. unfold R_dist. assert (tool : forall a b, a / b - /b = (-1 + a) /b). @@ -1179,13 +1179,13 @@ apply (Alt_CVU (fun x n => Datan_seq n x) (Datan_seq (Rabs c + r)) c r). intros x inb; apply Datan_seq_decreasing; try (apply Boule_lt in inb; apply Rabs_def2 in inb; - destruct inb; fourier). + destruct inb; lra). intros x inb; apply Datan_seq_CV_0; try (apply Boule_lt in inb; apply Rabs_def2 in inb; - destruct inb; fourier). + destruct inb; lra). intros x inb; apply (Datan_lim x); try (apply Boule_lt in inb; apply Rabs_def2 in inb; - destruct inb; fourier). + destruct inb; lra). intros x [ | n] inb. solve[unfold Datan_seq; apply Rle_refl]. rewrite <- (Datan_seq_Rabs x); apply Rlt_le, Datan_seq_increasing. @@ -1193,7 +1193,7 @@ apply (Alt_CVU (fun x n => Datan_seq n x) apply Boule_lt in inb; intuition. solve[apply Rabs_pos]. apply Datan_seq_CV_0. - apply Rlt_trans with 0;[fourier | ]. + apply Rlt_trans with 0;[lra | ]. apply Rplus_le_lt_0_compat. solve[apply Rabs_pos]. destruct r; assumption. @@ -1226,7 +1226,7 @@ intros N x x_lb x_ub. apply Hdelta ; assumption. unfold id ; field ; assumption. intros eps eps_pos. - assert (eps_3_pos : (eps/3) > 0) by fourier. + assert (eps_3_pos : (eps/3) > 0) by lra. elim (IHN (eps/3) eps_3_pos) ; intros delta1 Hdelta1. assert (Main : derivable_pt_lim (fun x : R =>tg_alt (Ratan_seq x) (S N)) x ((tg_alt (Datan_seq x)) (S N))). clear -Tool ; intros eps' eps'_pos. @@ -1297,7 +1297,7 @@ intros N x x_lb x_ub. intuition ; apply Rlt_le_trans with (r2:=delta) ; intuition unfold delta, mydelta. apply Rmin_l. apply Rmin_r. - fourier. + lra. Qed. Lemma Ratan_CVU' : @@ -1310,7 +1310,7 @@ apply (Alt_CVU (fun i r => Ratan_seq r i) ps_atan PI_tg (/2) pos_half); now intros; apply Ratan_seq_converging, Boule_half_to_interval. intros x b; apply Boule_half_to_interval in b. unfold ps_atan; destruct (in_int x) as [inside | outside]; - [ | destruct b; case outside; split; fourier]. + [ | destruct b; case outside; split; lra]. destruct (ps_atan_exists_1 x inside) as [v Pv]. apply Un_cv_ext with (2 := Pv);[reflexivity]. intros x n b; apply Boule_half_to_interval in b. @@ -1330,7 +1330,7 @@ exists N; intros n x nN b_y. case (Rtotal_order 0 x) as [xgt0 | [x0 | x0]]. assert (Boule (/2) {| pos := / 2; cond_pos := pos_half_prf|} x). revert b_y; unfold Boule; simpl; intros b_y; apply Rabs_def2 in b_y. - destruct b_y; unfold Boule; simpl; apply Rabs_def1; fourier. + destruct b_y; unfold Boule; simpl; apply Rabs_def1; lra. apply Pn; assumption. rewrite <- x0, ps_atan0_0. rewrite <- (sum_eq (fun _ => 0)), sum_cte, Rmult_0_l, Rminus_0_r, Rabs_pos_eq. @@ -1343,7 +1343,7 @@ replace (ps_atan x - sum_f_R0 (tg_alt (Ratan_seq x)) n) with rewrite Rabs_Ropp. assert (Boule (/2) {| pos := / 2; cond_pos := pos_half_prf|} (-x)). revert b_y; unfold Boule; simpl; intros b_y; apply Rabs_def2 in b_y. - destruct b_y; unfold Boule; simpl; apply Rabs_def1; fourier. + destruct b_y; unfold Boule; simpl; apply Rabs_def1; lra. apply Pn; assumption. unfold Rminus; rewrite ps_atan_opp, Ropp_plus_distr, sum_Ratan_seq_opp. rewrite !Ropp_involutive; reflexivity. @@ -1372,7 +1372,7 @@ apply continuity_inv. apply continuity_plus. apply continuity_const ; unfold constant ; intuition. apply derivable_continuous ; apply derivable_pow. -intro x ; apply Rgt_not_eq ; apply Rge_gt_trans with (1+0) ; [|fourier] ; +intro x ; apply Rgt_not_eq ; apply Rge_gt_trans with (1+0) ; [|lra] ; apply Rplus_ge_compat_l. replace (x^2) with (x²). apply Rle_ge ; apply Rle_0_sqr. @@ -1393,11 +1393,11 @@ apply derivable_pt_lim_CVU with assumption. intros y N inb; apply Rabs_def2 in inb; destruct inb. apply Datan_is_datan. - fourier. - fourier. + lra. + lra. intros y inb; apply Rabs_def2 in inb; destruct inb. - assert (y_gt_0 : -1 < y) by fourier. - assert (y_lt_1 : y < 1) by fourier. + assert (y_gt_0 : -1 < y) by lra. + assert (y_lt_1 : y < 1) by lra. intros eps eps_pos ; elim (Ratan_is_ps_atan eps eps_pos). intros N HN ; exists N; intros n n_lb ; apply HN ; tauto. apply Datan_CVU_prelim. @@ -1406,8 +1406,8 @@ apply derivable_pt_lim_CVU with replace ((c + r - (c - r)) / 2) with (r :R) by field. assert (Rabs c < 1 - r). unfold Boule in Pcr1; destruct r; simpl in *; apply Rabs_def1; - apply Rabs_def2 in Pcr1; destruct Pcr1; fourier. - fourier. + apply Rabs_def2 in Pcr1; destruct Pcr1; lra. + lra. intros; apply Datan_continuity. Qed. @@ -1426,7 +1426,7 @@ Lemma ps_atan_continuity_pt_1 : forall eps : R, dist R_met (ps_atan x) (Alt_PI/4) < eps). Proof. intros eps eps_pos. -assert (eps_3_pos : eps / 3 > 0) by fourier. +assert (eps_3_pos : eps / 3 > 0) by lra. elim (Ratan_is_ps_atan (eps / 3) eps_3_pos) ; intros N1 HN1. unfold Alt_PI. destruct exist_PI as [v Pv]; replace ((4 * v)/4) with v by field. @@ -1461,10 +1461,10 @@ rewrite Rplus_assoc ; apply Rabs_triang. unfold D_x, no_cond ; split ; [ | apply Rgt_not_eq ] ; intuition. intuition. apply HN2; unfold N; omega. - fourier. + lra. rewrite <- Rabs_Ropp, Ropp_minus_distr; apply HN1. unfold N; omega. - fourier. + lra. assumption. field. ring. @@ -1486,11 +1486,11 @@ intros x x_encad Pratan Prmymeta. rewrite Hrew1. replace (Rsqr x) with (x ^ 2) by (unfold Rsqr; ring). unfold Rdiv; rewrite Rmult_1_l; reflexivity. - fourier. + lra. assumption. intros; reflexivity. - fourier. - assert (t := tan_1_gt_1); split;destruct x_encad; fourier. + lra. + assert (t := tan_1_gt_1); split;destruct x_encad; lra. intros; reflexivity. Qed. @@ -1503,46 +1503,46 @@ assert (pr1 : forall c : R, 0 < c < x -> derivable_pt (atan - ps_atan) c). apply derivable_pt_minus. exact (derivable_pt_atan c). apply derivable_pt_ps_atan. - destruct x_encad; destruct c_encad; split; fourier. + destruct x_encad; destruct c_encad; split; lra. assert (pr2 : forall c : R, 0 < c < x -> derivable_pt id c). - intros ; apply derivable_pt_id; fourier. + intros ; apply derivable_pt_id; lra. assert (delta_cont : forall c : R, 0 <= c <= x -> continuity_pt (atan - ps_atan) c). intros c [[c_encad1 | c_encad1 ] [c_encad2 | c_encad2]]; apply continuity_pt_minus. apply derivable_continuous_pt ; apply derivable_pt_atan. apply derivable_continuous_pt ; apply derivable_pt_ps_atan. - split; destruct x_encad; fourier. + split; destruct x_encad; lra. apply derivable_continuous_pt, derivable_pt_atan. apply derivable_continuous_pt, derivable_pt_ps_atan. - subst c; destruct x_encad; split; fourier. + subst c; destruct x_encad; split; lra. apply derivable_continuous_pt, derivable_pt_atan. apply derivable_continuous_pt, derivable_pt_ps_atan. - subst c; split; fourier. + subst c; split; lra. apply derivable_continuous_pt, derivable_pt_atan. apply derivable_continuous_pt, derivable_pt_ps_atan. - subst c; destruct x_encad; split; fourier. + subst c; destruct x_encad; split; lra. assert (id_cont : forall c : R, 0 <= c <= x -> continuity_pt id c). intros ; apply derivable_continuous ; apply derivable_id. -assert (x_lb : 0 < x) by (destruct x_encad; fourier). +assert (x_lb : 0 < x) by (destruct x_encad; lra). elim (MVT (atan - ps_atan)%F id 0 x pr1 pr2 x_lb delta_cont id_cont) ; intros d Temp ; elim Temp ; intros d_encad Main. clear - Main x_encad. assert (Temp : forall (pr: derivable_pt (atan - ps_atan) d), derive_pt (atan - ps_atan) d pr = 0). intro pr. assert (d_encad3 : -1 < d < 1). - destruct d_encad; destruct x_encad; split; fourier. + destruct d_encad; destruct x_encad; split; lra. pose (pr3 := derivable_pt_minus atan ps_atan d (derivable_pt_atan d) (derivable_pt_ps_atan d d_encad3)). rewrite <- pr_nu_var2_interv with (f:=(atan - ps_atan)%F) (g:=(atan - ps_atan)%F) (lb:=0) (ub:=x) (pr1:=pr3) (pr2:=pr). unfold pr3. rewrite derive_pt_minus. rewrite Datan_eq_DatanSeq_interv with (Prmymeta := derivable_pt_atan d). intuition. assumption. - destruct d_encad; fourier. + destruct d_encad; lra. assumption. reflexivity. assert (iatan0 : atan 0 = 0). apply tan_is_inj. apply atan_bound. - rewrite Ropp_div; assert (t := PI2_RGT_0); split; fourier. + rewrite Ropp_div; assert (t := PI2_RGT_0); split; lra. rewrite tan_0, atan_right_inv; reflexivity. generalize Main; rewrite Temp, Rmult_0_r. replace ((atan - ps_atan)%F x) with (atan x - ps_atan x) by intuition. @@ -1560,19 +1560,19 @@ Qed. Theorem Alt_PI_eq : Alt_PI = PI. Proof. apply Rmult_eq_reg_r with (/4); fold (Alt_PI/4); fold (PI/4); - [ | apply Rgt_not_eq; fourier]. + [ | apply Rgt_not_eq; lra]. assert (0 < PI/6) by (apply PI6_RGT_0). assert (t1:= PI2_1). assert (t2 := PI_4). assert (m := Alt_PI_RGT_0). -assert (-PI/2 < 1 < PI/2) by (rewrite Ropp_div; split; fourier). +assert (-PI/2 < 1 < PI/2) by (rewrite Ropp_div; split; lra). apply cond_eq; intros eps ep. change (R_dist (Alt_PI/4) (PI/4) < eps). assert (ca : continuity_pt atan 1). apply derivable_continuous_pt, derivable_pt_atan. assert (Xe : exists eps', exists eps'', eps' + eps'' <= eps /\ 0 < eps' /\ 0 < eps''). - exists (eps/2); exists (eps/2); repeat apply conj; fourier. + exists (eps/2); exists (eps/2); repeat apply conj; lra. destruct Xe as [eps' [eps'' [eps_ineq [ep' ep'']]]]. destruct (ps_atan_continuity_pt_1 _ ep') as [alpha [a0 Palpha]]. destruct (ca _ ep'') as [beta [b0 Pbeta]]. @@ -1585,14 +1585,14 @@ assert (Xa : exists a, 0 < a < 1 /\ R_dist a 1 < alpha /\ assert ((1 - alpha /2) <= Rmax (1 - alpha /2) (1 - beta /2)) by apply Rmax_l. assert ((1 - beta /2) <= Rmax (1 - alpha /2) (1 - beta /2)) by apply Rmax_r. assert (Rmax (1 - alpha /2) (1 - beta /2) < 1) - by (apply Rmax_lub_lt; fourier). - split;[split;[ | apply Rmax_lub_lt]; fourier | ]. + by (apply Rmax_lub_lt; lra). + split;[split;[ | apply Rmax_lub_lt]; lra | ]. assert (0 <= 1 - Rmax (/ 2) (Rmax (1 - alpha / 2) (1 - beta / 2))). assert (Rmax (/2) (Rmax (1 - alpha / 2) - (1 - beta /2)) <= 1) by (apply Rmax_lub; fourier). - fourier. + (1 - beta /2)) <= 1) by (apply Rmax_lub; lra). + lra. split; unfold R_dist; rewrite <-Rabs_Ropp, Ropp_minus_distr, - Rabs_pos_eq;fourier. + Rabs_pos_eq;lra. destruct Xa as [a [[Pa0 Pa1] [P1 P2]]]. apply Rle_lt_trans with (1 := R_dist_tri _ _ (ps_atan a)). apply Rlt_le_trans with (2 := eps_ineq). diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index aa886cee0..59e014862 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -15,7 +15,7 @@ Require Import Rbase. Require Import R_Ifp. -Require Import Fourier. +Require Import Lra. Local Open Scope R_scope. Implicit Type r : R. @@ -357,7 +357,7 @@ Qed. Lemma Rle_abs : forall x:R, x <= Rabs x. Proof. - intro; unfold Rabs; case (Rcase_abs x); intros; fourier. + intro; unfold Rabs; case (Rcase_abs x); intros; lra. Qed. Definition RRle_abs := Rle_abs. diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v index dfa5c7104..aaf691ed1 100644 --- a/theories/Reals/Rderiv.v +++ b/theories/Reals/Rderiv.v @@ -16,7 +16,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Rlimit. -Require Import Fourier. +Require Import Lra. Require Import Omega. Local Open Scope R_scope. @@ -77,7 +77,7 @@ Proof. elim (Rmin_Rgt (/ 2) x 0); intros a b; cut (0 < 2). intro; generalize (Rinv_0_lt_compat 2 H3); intro; fold (/ 2 > 0) in H4; apply (b (conj H4 H)). - fourier. + lra. intros; elim H3; clear H3; intros; generalize (let (H1, H2) := @@ -167,7 +167,7 @@ Proof. unfold Rabs; destruct (Rcase_abs 2) as [Hlt|Hge]; auto. cut (0 < 2). intro H7; elim (Rlt_asym 0 2 H7 Hlt). - fourier. + lra. apply Rabs_no_R0. discrR. Qed. diff --git a/theories/Reals/Reals.v b/theories/Reals/Reals.v index b249b519f..3ef368bb4 100644 --- a/theories/Reals/Reals.v +++ b/theories/Reals/Reals.v @@ -30,3 +30,4 @@ Require Export SeqSeries. Require Export Rtrigo. Require Export Ranalysis. Require Export Integration. +Require Import Fourier. diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index b14fcc4d3..e3e995d20 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -15,7 +15,7 @@ Require Import Rbase. Require Import Rfunctions. -Require Import Fourier. +Require Import Lra. Local Open Scope R_scope. (*******************************) @@ -24,7 +24,7 @@ Local Open Scope R_scope. (*********) Lemma eps2_Rgt_R0 : forall eps:R, eps > 0 -> eps * / 2 > 0. Proof. - intros; fourier. + intros; lra. Qed. (*********) @@ -45,14 +45,14 @@ Qed. Lemma Rlt_eps2_eps : forall eps:R, eps > 0 -> eps * / 2 < eps. Proof. intros. - fourier. + lra. Qed. (*********) Lemma Rlt_eps4_eps : forall eps:R, eps > 0 -> eps * / (2 + 2) < eps. Proof. intros. - fourier. + lra. Qed. (*********) diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index c6fac951b..d465523a7 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -25,7 +25,7 @@ Require Import R_sqrt. Require Import Sqrt_reg. Require Import MVT. Require Import Ranalysis4. -Require Import Fourier. +Require Import Lra. Local Open Scope R_scope. Lemma P_Rmin : forall (P:R -> Prop) (x y:R), P x -> P y -> P (Rmin x y). @@ -714,7 +714,7 @@ Qed. Lemma Rlt_Rpower_l a b c: 0 < c -> 0 < a < b -> a ^R c < b ^R c. Proof. intros c0 [a0 ab]; apply exp_increasing. -now apply Rmult_lt_compat_l; auto; apply ln_increasing; fourier. +now apply Rmult_lt_compat_l; auto; apply ln_increasing; lra. Qed. Lemma Rle_Rpower_l a b c: 0 <= c -> 0 < a <= b -> a ^R c <= b ^R c. @@ -722,7 +722,7 @@ Proof. intros [c0 | c0]; [ | intros; rewrite <- c0, !Rpower_O; [apply Rle_refl | |] ]. intros [a0 [ab|ab]]. - now apply Rlt_le, Rlt_Rpower_l;[ | split]; fourier. + now apply Rlt_le, Rlt_Rpower_l;[ | split]; lra. rewrite ab; apply Rle_refl. apply Rlt_le_trans with a; tauto. tauto. @@ -754,10 +754,10 @@ assert (cmp : 0 < x + sqrt (x ^ 2 + 1)). replace (x ^ 2) with ((-x) ^ 2) by ring. assert (sqrt ((- x) ^ 2) < sqrt ((-x)^2+1)). apply sqrt_lt_1_alt. - split;[apply pow_le | ]; fourier. + split;[apply pow_le | ]; lra. pattern x at 1; replace x with (- (sqrt ((- x) ^ 2))). - assert (t:= sqrt_pos ((-x)^2)); fourier. - simpl; rewrite Rmult_1_r, sqrt_square, Ropp_involutive;[reflexivity | fourier]. + assert (t:= sqrt_pos ((-x)^2)); lra. + simpl; rewrite Rmult_1_r, sqrt_square, Ropp_involutive;[reflexivity | lra]. apply Rplus_lt_le_0_compat;[apply Rnot_le_gt; assumption | apply sqrt_pos]. rewrite exp_ln;[ | assumption]. rewrite exp_Ropp, exp_ln;[ | assumption]. @@ -770,7 +770,7 @@ apply Rmult_eq_reg_l with (2 * (x + sqrt (x ^ 2 + 1)));[ | apply Rgt_not_eq, Rmult_lt_0_compat;[apply Rlt_0_2 | assumption]]. assert (pow2_sqrt : forall x, 0 <= x -> sqrt x ^ 2 = x) by (intros; simpl; rewrite Rmult_1_r, sqrt_sqrt; auto). -field_simplify;[rewrite pow2_sqrt;[field | ] | apply Rgt_not_eq; fourier]. +field_simplify;[rewrite pow2_sqrt;[field | ] | apply Rgt_not_eq; lra]. apply Rplus_le_le_0_compat;[simpl; rewrite Rmult_1_r; apply (Rle_0_sqr x)|apply Rlt_le, Rlt_0_1]. Qed. @@ -784,12 +784,12 @@ assert (0 < x + sqrt (x ^ 2 + 1)). replace (x ^ 2) with ((-x) ^ 2) by ring. assert (sqrt ((- x) ^ 2) < sqrt ((-x)^2+1)). apply sqrt_lt_1_alt. - split;[apply pow_le|]; fourier. + split;[apply pow_le|]; lra. pattern x at 1; replace x with (- (sqrt ((- x) ^ 2))). - assert (t:= sqrt_pos ((-x)^2)); fourier. - simpl; rewrite Rmult_1_r, sqrt_square, Ropp_involutive; auto; fourier. + assert (t:= sqrt_pos ((-x)^2)); lra. + simpl; rewrite Rmult_1_r, sqrt_square, Ropp_involutive; auto; lra. assert (0 < x ^ 2 + 1). - apply Rplus_le_lt_0_compat;[simpl; rewrite Rmult_1_r; apply Rle_0_sqr|fourier]. + apply Rplus_le_lt_0_compat;[simpl; rewrite Rmult_1_r; apply Rle_0_sqr|lra]. replace (/sqrt (x ^ 2 + 1)) with (/(x + sqrt (x ^ 2 + 1)) * (1 + (/(2 * sqrt (x ^ 2 + 1)) * (INR 2 * x ^ 1 + 0)))). @@ -817,7 +817,7 @@ intros x y xy. case (Rle_dec (arcsinh y) (arcsinh x));[ | apply Rnot_le_lt ]. intros abs; case (Rlt_not_le _ _ xy). rewrite <- (sinh_arcsinh y), <- (sinh_arcsinh x). -destruct abs as [lt | q];[| rewrite q; fourier]. +destruct abs as [lt | q];[| rewrite q; lra]. apply Rlt_le, sinh_lt; assumption. Qed. diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index ffc0adf50..ddd8722e1 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -18,7 +18,7 @@ Require Export Cos_rel. Require Export Cos_plus. Require Import ZArith_base. Require Import Zcomplements. -Require Import Fourier. +Require Import Lra. Require Import Ranalysis1. Require Import Rsqrt_def. Require Import PSeries_reg. diff --git a/theories/Reals/Rtrigo1.v b/theories/Reals/Rtrigo1.v index bf00f736f..a75fd2dde 100644 --- a/theories/Reals/Rtrigo1.v +++ b/theories/Reals/Rtrigo1.v @@ -18,7 +18,7 @@ Require Export Cos_rel. Require Export Cos_plus. Require Import ZArith_base. Require Import Zcomplements. -Require Import Fourier. +Require Import Lra. Require Import Ranalysis1. Require Import Rsqrt_def. Require Import PSeries_reg. @@ -175,10 +175,10 @@ Qed. Lemma sin_gt_cos_7_8 : sin (7 / 8) > cos (7 / 8). Proof. -assert (lo1 : 0 <= 7/8) by fourier. -assert (up1 : 7/8 <= 4) by fourier. -assert (lo : -2 <= 7/8) by fourier. -assert (up : 7/8 <= 2) by fourier. +assert (lo1 : 0 <= 7/8) by lra. +assert (up1 : 7/8 <= 4) by lra. +assert (lo : -2 <= 7/8) by lra. +assert (up : 7/8 <= 2) by lra. destruct (pre_sin_bound _ 0 lo1 up1) as [lower _ ]. destruct (pre_cos_bound _ 0 lo up) as [_ upper]. apply Rle_lt_trans with (1 := upper). @@ -205,12 +205,12 @@ Definition PI_2_aux : {z | 7/8 <= z <= 7/4 /\ -cos z = 0}. assert (cc : continuity (fun r =>- cos r)). apply continuity_opp, continuity_cos. assert (cvp : 0 < cos (7/8)). - assert (int78 : -2 <= 7/8 <= 2) by (split; fourier). + assert (int78 : -2 <= 7/8 <= 2) by (split; lra). destruct int78 as [lower upper]. case (pre_cos_bound _ 0 lower upper). unfold cos_approx; simpl sum_f_R0; unfold cos_term. intros cl _; apply Rlt_le_trans with (2 := cl); simpl. - fourier. + lra. assert (cun : cos (7/4) < 0). replace (7/4) with (7/8 + 7/8) by field. rewrite cos_plus. @@ -218,7 +218,7 @@ assert (cun : cos (7/4) < 0). exact sin_gt_cos_7_8. apply Rlt_le; assumption. apply Rlt_le; apply Rlt_trans with (1 := cvp); exact sin_gt_cos_7_8. -apply IVT; auto; fourier. +apply IVT; auto; lra. Qed. Definition PI2 := proj1_sig PI_2_aux. @@ -270,7 +270,7 @@ Qed. Lemma sin_pos_tech : forall x, 0 < x < 2 -> 0 < sin x. intros x [int1 int2]. assert (lo : 0 <= x) by (apply Rlt_le; assumption). -assert (up : x <= 4) by (apply Rlt_le, Rlt_trans with (1:=int2); fourier). +assert (up : x <= 4) by (apply Rlt_le, Rlt_trans with (1:=int2); lra). destruct (pre_sin_bound _ 0 lo up) as [t _]; clear lo up. apply Rlt_le_trans with (2:= t); clear t. unfold sin_approx; simpl sum_f_R0; unfold sin_term; simpl. @@ -280,13 +280,13 @@ end. assert (t' : x ^ 2 <= 4). replace 4 with (2 ^ 2) by field. apply (pow_incr x 2); split; apply Rlt_le; assumption. -apply Rmult_lt_0_compat;[assumption | fourier ]. +apply Rmult_lt_0_compat;[assumption | lra ]. Qed. Lemma sin_PI2 : sin (PI / 2) = 1. replace (PI / 2) with PI2 by (unfold PI; field). assert (int' : 0 < PI2 < 2). - destruct pi2_int; split; fourier. + destruct pi2_int; split; lra. assert (lo2 := sin_pos_tech PI2 int'). assert (t2 : Rabs (sin PI2) = 1). rewrite <- Rabs_R1; apply Rsqr_eq_abs_0. @@ -295,10 +295,10 @@ revert t2; rewrite Rabs_pos_eq;[| apply Rlt_le]; tauto. Qed. Lemma PI_RGT_0 : PI > 0. -Proof. unfold PI; destruct pi2_int; fourier. Qed. +Proof. unfold PI; destruct pi2_int; lra. Qed. Lemma PI_4 : PI <= 4. -Proof. unfold PI; destruct pi2_int; fourier. Qed. +Proof. unfold PI; destruct pi2_int; lra. Qed. (**********) Lemma PI_neq0 : PI <> 0. @@ -344,13 +344,13 @@ Lemma cos_bound : forall (a : R) (n : nat), - PI / 2 <= a -> a <= PI / 2 -> Proof. intros a n lower upper; apply pre_cos_bound. apply Rle_trans with (2 := lower). - apply Rmult_le_reg_r with 2; [fourier |]. + apply Rmult_le_reg_r with 2; [lra |]. replace ((-PI/2) * 2) with (-PI) by field. - assert (t := PI_4); fourier. + assert (t := PI_4); lra. apply Rle_trans with (1 := upper). -apply Rmult_le_reg_r with 2; [fourier | ]. +apply Rmult_le_reg_r with 2; [lra | ]. replace ((PI/2) * 2) with PI by field. -generalize PI_4; intros; fourier. +generalize PI_4; intros; lra. Qed. (**********) Lemma neg_cos : forall x:R, cos (x + PI) = - cos x. @@ -749,19 +749,19 @@ Qed. Lemma _PI2_RLT_0 : - (PI / 2) < 0. Proof. assert (H := PI_RGT_0). - fourier. + lra. Qed. Lemma PI4_RLT_PI2 : PI / 4 < PI / 2. Proof. assert (H := PI_RGT_0). - fourier. + lra. Qed. Lemma PI2_Rlt_PI : PI / 2 < PI. Proof. assert (H := PI_RGT_0). - fourier. + lra. Qed. (***************************************************) diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v index 7cbfc6303..78797c87c 100644 --- a/theories/Reals/Rtrigo_calc.v +++ b/theories/Reals/Rtrigo_calc.v @@ -205,7 +205,6 @@ Proof with trivial. rewrite cos2; unfold Rsqr; rewrite sin_PI6; rewrite sqrt_def... field. left ; prove_sup0. - discrR. Qed. Lemma tan_PI6 : tan (PI / 6) = 1 / sqrt 3. diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index c640167ac..05bc6aea9 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -76,7 +76,7 @@ let is_tactic = [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection"; "elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor"; "econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct"; - "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate"; "info_auto"; "info_eauto"; + "info"; "field"; "specialize"; "evar"; "solve"; "instanciate"; "info_auto"; "info_eauto"; "quote"; "eexact"; "autorewrite"; "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality"; "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega"; diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index 74e53bef1..3e2bd9872 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -18,14 +18,6 @@ module NamedDecl = Context.Named.Declaration let known_names = Summary.ref [] ~name:"proofusing-nameset" -let in_nameset = - let open Libobject in - declare_object { (default_object "proofusing-nameset") with - cache_function = (fun (_,x) -> known_names := x :: !known_names); - classify_function = (fun _ -> Dispose); - discharge_function = (fun _ -> None) - } - let rec close_fwd e s = let s' = List.fold_left (fun s decl -> @@ -73,7 +65,7 @@ let process_expr env e ty = let s = Id.Set.union v_ty (process_expr env e ty) in Id.Set.elements s -let name_set id expr = Lib.add_anonymous_leaf (in_nameset (id,expr)) +let name_set id expr = known_names := (id,expr) :: !known_names let minimize_hyps env ids = let rec aux ids = |