diff options
42 files changed, 319 insertions, 536 deletions
diff --git a/.travis.yml b/.travis.yml index 7138d5c61e..81f50af0a0 100644 --- a/.travis.yml +++ b/.travis.yml @@ -40,6 +40,7 @@ env: - TEST_TARGET="ci-math-comp" - TEST_TARGET="ci-sf" - TEST_TARGET="ci-unimath" + - TEST_TARGET="ci-vst" # Not ready yet for 8.7 # - TEST_TARGET="ci-cpdt" # - TEST_TARGET="ci-metacoq" @@ -49,6 +50,7 @@ matrix: allow_failures: - env: TEST_TARGET="ci-geocoq" + - env: TEST_TARGET="ci-vst" # Full Coq test-suite with two compilers # [TODO: use yaml refs and avoid duplication for packages list] diff --git a/Makefile.ci b/Makefile.ci index 897318c4dd..b055ada8e5 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -1,7 +1,7 @@ CI_TARGETS=ci-all ci-hott ci-math-comp ci-compcert ci-sf ci-cpdt \ ci-color ci-math-classes ci-tlc ci-fiat-crypto ci-fiat-parsers \ ci-coquelicot ci-flocq ci-iris-coq ci-metacoq ci-geocoq \ - ci-unimath + ci-unimath ci-vst .PHONY: $(CI_TARGETS) diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 241ec35861..336ce9d8f1 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -46,8 +46,11 @@ ######################################################################## # HoTT ######################################################################## +# Temporal overlay : ${HoTT_CI_BRANCH:=mz-8.7} : ${HoTT_CI_GITURL:=https://github.com/ejgallego/HoTT.git} +# : ${HoTT_CI_BRANCH:=master} +# : ${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT.git} ######################################################################## # GeoCoq @@ -74,6 +77,12 @@ : ${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git} ######################################################################## +# VST +######################################################################## +: ${VST_CI_BRANCH:=master} +: ${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git} + +######################################################################## # fiat_parsers ######################################################################## : ${fiat_parsers_CI_BRANCH:=master} diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh new file mode 100755 index 0000000000..c111951852 --- /dev/null +++ b/dev/ci/ci-vst.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +VST_CI_DIR=${CI_BUILD_DIR}/VST + +# opam install -j ${NJOBS} -y menhir +git_checkout ${VST_CI_BRANCH} ${VST_CI_GITURL} ${VST_CI_DIR} + +# Targets are: msl veric floyd +# Patch to avoid the upper version limit +( cd ${VST_CI_DIR} && sed -i.bak 's/8.6$/8.6 or-else trunk/' Makefile && make -j ${NJOBS} ) diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 4a1d688f51..45b5a1007a 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -358,7 +358,7 @@ object(self) | Good evs -> proof#set_goals goals; proof#set_evars evs; - proof#refresh (); + proof#refresh ~force:true; Coq.return () ) ) diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index b5405570c9..3cbe583881 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -14,7 +14,7 @@ class type proof_view = object inherit GObj.widget method buffer : GText.buffer - method refresh : unit -> unit + method refresh : force:bool -> unit method clear : unit -> unit method set_goals : Interface.goals option -> unit method set_evars : Interface.evar list option -> unit @@ -197,6 +197,7 @@ let proof_view () = inherit GObj.widget view#as_widget val mutable goals = None val mutable evars = None + val mutable last_width = -1 method buffer = text_buffer @@ -206,13 +207,24 @@ let proof_view () = method set_evars evs = evars <- evs - method refresh () = - let dummy _ () = () in - display (mode_tactic dummy) view goals None evars + method refresh ~force = + (* We need to block updates here due to the following race: + insertion of messages may create a vertical scrollbar, this + will trigger a width change, calling refresh again and + going into an infinite loop. *) + let width = Ideutils.textview_width view in + (* Could still this method race if the scrollbar changes the + textview_width ?? *) + let needed = force || last_width <> width in + if needed then begin + last_width <- width; + let dummy _ () = () in + display (mode_tactic dummy) view goals None evars + end end in (* Is there a better way to connect the signal ? *) (* Can this be done in the object constructor? *) - let w_cb _ = pf#refresh () in + let w_cb _ = pf#refresh ~force:false in ignore (view#misc#connect#size_allocate w_cb); pf diff --git a/ide/wg_ProofView.mli b/ide/wg_ProofView.mli index aa01d955d0..a90d429d04 100644 --- a/ide/wg_ProofView.mli +++ b/ide/wg_ProofView.mli @@ -10,7 +10,7 @@ class type proof_view = object inherit GObj.widget method buffer : GText.buffer - method refresh : unit -> unit + method refresh : force:bool -> unit method clear : unit -> unit method set_goals : Interface.goals option -> unit method set_evars : Interface.evar list option -> unit diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 5f80d68974..d7950e5fd5 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -111,7 +111,7 @@ let to_box = let open Pp in ) let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match Pp.repr pp with - | Ppcmd_empty -> constructor "ppdoc" "emtpy" [] + | Ppcmd_empty -> constructor "ppdoc" "empty" [] | Ppcmd_string s -> constructor "ppdoc" "string" [of_string s] | Ppcmd_glue sl -> constructor "ppdoc" "glue" [of_list of_pp sl] | Ppcmd_box (bt,s) -> constructor "ppdoc" "box" [of_pair of_box of_pp (bt,s)] diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index a9f7106395..25d3c705f4 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -283,14 +283,9 @@ type bullet = | Plus of int (** {6 Types concerning Stm} *) -type 'a stm_vernac = +type stm_vernac = | JoinDocument - | Finish | Wait - | PrintDag - | Observe of Stateid.t - | Command of 'a (* An out of flow command not to be recorded by Stm *) - | PGLast of 'a (* To ease the life of PG *) (** {6 Types concerning the module layer} *) @@ -450,8 +445,9 @@ type vernac_expr = | VernacRegister of lident * register_kind | VernacComments of comment list - (* Stm backdoor *) - | VernacStm of vernac_expr stm_vernac + (* Stm backdoor: used in fake_id, will be removed when fake_ide + becomes aware of feedback about completed jobs. *) + | VernacStm of stm_vernac (* Proof management *) | VernacGoal of constr_expr @@ -509,16 +505,11 @@ and report_with = Stateid.t * Feedback.route_id (* feedback on id/route *) and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) and vernac_start = string * opacity_guarantee * Id.t list and vernac_sideff_type = Id.t list -and vernac_is_alias = bool and vernac_part_of_script = bool and vernac_control = - | VtFinish | VtWait | VtJoinDocument - | VtPrintDag - | VtObserve of Stateid.t | VtBack of Stateid.t - | VtPG and opacity_guarantee = | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) diff --git a/library/summary.ml b/library/summary.ml index 2ec4760d64..d9f6441003 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -108,7 +108,7 @@ let unfreeze_summaries fs = with e when CErrors.noncritical e -> let e = CErrors.push e in Feedback.msg_error - Pp.(seq [str "Error unfrezing summay %s\n%s\n%!"; + Pp.(seq [str "Error unfreezing summary %s\n%s\n%!"; str (name_of_summary id); CErrors.iprint e]); iraise e diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 5544508968..ded7a557cf 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -66,13 +66,7 @@ GEXTEND Gram (* Stm backdoor *) | IDENT "Stm"; IDENT "JoinDocument"; "." -> VernacStm JoinDocument - | IDENT "Stm"; IDENT "Finish"; "." -> VernacStm Finish | IDENT "Stm"; IDENT "Wait"; "." -> VernacStm Wait - | IDENT "Stm"; IDENT "PrintDag"; "." -> VernacStm PrintDag - | IDENT "Stm"; IDENT "Observe"; id = INT; "." -> - VernacStm (Observe (Stateid.of_int (int_of_string id))) - | IDENT "Stm"; IDENT "Command"; v = vernac_aux -> VernacStm (Command v) - | IDENT "Stm"; IDENT "PGLast"; v = vernac_aux -> VernacStm (PGLast v) | v = vernac_poly -> v ] ] diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index aab5687465..fd33a779dc 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +DECLARE PLUGIN "ltac_plugin" + open Util open Pp open Compat diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index f36c8c1530..38eeda9b96 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -702,7 +702,7 @@ let tag_var = tag Tag.variable | CEvar (_,n,l) -> return (pr_evar (pr mt) n l, latom) | CPatVar (_,p) -> - return (str "?" ++ pr_patvar p, latom) + return (str "@?" ++ pr_patvar p, latom) | CSort (_,s) -> return (pr_glob_sort s, latom) | CCast (_,a,b) -> diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 78ef4d4bad..cfc2e48d11 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -534,18 +534,8 @@ open Decl_kinds (* Stm *) | VernacStm JoinDocument -> return (keyword "Stm JoinDocument") - | VernacStm PrintDag -> - return (keyword "Stm PrintDag") - | VernacStm Finish -> - return (keyword "Stm Finish") | VernacStm Wait -> return (keyword "Stm Wait") - | VernacStm (Observe id) -> - return (keyword "Stm Observe " ++ str(Stateid.to_string id)) - | VernacStm (Command v) -> - return (keyword "Stm Command " ++ pr_vernac_body v) - | VernacStm (PGLast v) -> - return (keyword "Stm PGLast " ++ pr_vernac_body v) (* Proof management *) | VernacAbortAll -> diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 8fabb70536..5963d45ef9 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -204,6 +204,11 @@ let print_opacity ref = str "transparent (with minimal expansion weight)"] (*******************) + +let print_if_is_coercion ref = + if Classops.coercion_exists ref then [pr_global ref ++ str " is a coercion"] else [] + +(*******************) (* *) let print_polymorphism ref = @@ -257,7 +262,8 @@ let print_name_infos ref = type_info_for_implicit @ print_renames_list (mt()) renames @ print_impargs_list (mt()) impls @ - print_argument_scopes (mt()) scopes + print_argument_scopes (mt()) scopes @ + print_if_is_coercion ref let print_id_args_data test pr id l = if List.exists test l then diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml index f51586c739..2c489d6ded 100644 --- a/proofs/proof_using.ml +++ b/proofs/proof_using.ml @@ -108,7 +108,7 @@ let remove_ids_and_lets env s ids = let suggest_Proof_using name env vars ids_typ context_ids = let module S = Id.Set in let open Pp in - let print x = Feedback.msg_error x in + let print x = Feedback.msg_debug x in let pr_set parens s = let wrap ppcmds = if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")" diff --git a/stm/stm.ml b/stm/stm.ml index b9dbb78917..b0ad3f8790 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2232,10 +2232,13 @@ let known_state ?(redefine_qed=false) ~cache id = if eff then update_global_env () ), (if eff then `Yes else cache), true | `Cmd { cast = x; ceff = eff } -> (fun () -> - resilient_command reach view.next; - stm_vernac_interp id x; - if eff then update_global_env () - ), (if eff then `Yes else cache), true + (match !Flags.async_proofs_mode with + | Flags.APon | Flags.APonLazy -> + resilient_command reach view.next + | Flags.APoff -> reach view.next); + stm_vernac_interp id x; + if eff then update_global_env () + ), (if eff then `Yes else cache), true | `Fork ((x,_,_,_), None) -> (fun () -> resilient_command reach view.next; stm_vernac_interp id x; @@ -2525,20 +2528,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty stm_prerr_endline (fun () -> " classified as: " ^ string_of_vernac_classification c); match c with - (* PG stuff *) - | VtStm(VtPG,false), VtNow -> stm_vernac_interp Stateid.dummy x; `Ok - | VtStm(VtPG,_), _ -> anomaly(str "PG command in script or VtLater") (* Joining various parts of the document *) | VtStm (VtJoinDocument, b), VtNow -> join (); `Ok - | VtStm (VtFinish, b), VtNow -> finish (); `Ok - | VtStm (VtWait, b), VtNow -> finish (); wait (); `Ok - | VtStm (VtPrintDag, b), VtNow -> - VCS.print ~now:true (); `Ok - | VtStm (VtObserve id, b), VtNow -> observe id; `Ok - | VtStm ((VtObserve _ | VtFinish | VtJoinDocument - |VtPrintDag |VtWait),_), VtLater -> + | VtStm (VtWait, b), VtNow -> finish (); wait (); `Ok + | VtStm ((VtJoinDocument|VtWait),_), VtLater -> anomaly(str"classifier: join actions cannot be classified as VtLater") - + (* Back *) | VtStm (VtBack oid, true), w -> let id = VCS.new_node ~id:newtip () in @@ -2701,15 +2696,6 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty | VtUnknown, VtLater -> anomaly(str"classifier: VtUnknown must imply VtNow") end in - (* Proof General *) - begin match expr with - | VernacStm (PGLast _) -> - if not (VCS.Branch.equal head VCS.Branch.master) then - stm_vernac_interp Stateid.dummy - { verbose = true; loc = Loc.ghost; indentation = 0; strlen = 0; - expr = VernacShow (ShowGoal OpenSubgoals) } - | _ -> () - end; stm_prerr_endline (fun () -> "processed }}}"); VCS.print (); rc diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index dc5be08a37..5908c09d08 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -33,9 +33,7 @@ let string_of_vernac_type = function | VtQuery (b,(id,route)) -> "Query " ^ string_of_in_script b ^ " report " ^ Stateid.to_string id ^ " route " ^ string_of_int route - | VtStm ((VtFinish|VtJoinDocument|VtObserve _|VtPrintDag|VtWait), b) -> - "Stm " ^ string_of_in_script b - | VtStm (VtPG, b) -> "Stm PG " ^ string_of_in_script b + | VtStm ((VtJoinDocument|VtWait), b) -> "Stm " ^ string_of_in_script b | VtStm (VtBack _, b) -> "Stm Back " ^ string_of_in_script b let string_of_vernac_when = function @@ -52,12 +50,6 @@ let declare_vernac_classifier = classifiers := !classifiers @ [s,f] -let elide_part_of_script_and_now (a, _) = - match a with - | VtQuery (_,id) -> VtQuery (false,id), VtNow - | VtStm (x, _) -> VtStm (x, false), VtNow - | x -> x, VtNow - let make_polymorphic (a, b as x) = match a with | VtStartProof (x, _, ids) -> @@ -69,23 +61,14 @@ let set_undo_classifier f = undo_classifier := f let rec classify_vernac e = let static_classifier e = match e with - (* PG compatibility *) - | VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"]) - | VernacSetOption ((["Silent"]|["Undo"]|["Printing";"Depth"]),_) - when !Flags.print_emacs -> VtStm(VtPG,false), VtNow (* Univ poly compatibility: we run it now, so that we can just * look at Flags in stm.ml. Would be nicer to have the stm * look at the entire dag to detect this option. *) | VernacSetOption (["Universe"; "Polymorphism"],_) | VernacUnsetOption (["Universe"; "Polymorphism"]) -> VtSideff [], VtNow (* Stm *) - | VernacStm Finish -> VtStm (VtFinish, true), VtNow - | VernacStm Wait -> VtStm (VtWait, true), VtNow + | VernacStm Wait -> VtStm (VtWait, true), VtNow | VernacStm JoinDocument -> VtStm (VtJoinDocument, true), VtNow - | VernacStm PrintDag -> VtStm (VtPrintDag, true), VtNow - | VernacStm (Observe id) -> VtStm (VtObserve id, true), VtNow - | VernacStm (Command x) -> elide_part_of_script_and_now (classify_vernac x) - | VernacStm (PGLast x) -> fst (classify_vernac x), VtNow (* Nested vernac exprs *) | VernacProgram e -> classify_vernac e | VernacLocal (_,e) -> classify_vernac e diff --git a/test-suite/output/ErrorInModule.out b/test-suite/output/ErrorInModule.out new file mode 100644 index 0000000000..851ecd9306 --- /dev/null +++ b/test-suite/output/ErrorInModule.out @@ -0,0 +1,2 @@ +File "stdin", line 3, characters 20-31: +Error: The reference nonexistent was not found in the current environment. diff --git a/test-suite/output/ErrorInModule.v b/test-suite/output/ErrorInModule.v new file mode 100644 index 0000000000..e69e23276b --- /dev/null +++ b/test-suite/output/ErrorInModule.v @@ -0,0 +1,4 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-quick") -*- *) +Module M. + Definition foo := nonexistent. +End M. diff --git a/test-suite/output/ErrorInSection.out b/test-suite/output/ErrorInSection.out new file mode 100644 index 0000000000..851ecd9306 --- /dev/null +++ b/test-suite/output/ErrorInSection.out @@ -0,0 +1,2 @@ +File "stdin", line 3, characters 20-31: +Error: The reference nonexistent was not found in the current environment. diff --git a/test-suite/output/ErrorInSection.v b/test-suite/output/ErrorInSection.v new file mode 100644 index 0000000000..3036f8f05b --- /dev/null +++ b/test-suite/output/ErrorInSection.v @@ -0,0 +1,4 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-quick") -*- *) +Section S. + Definition foo := nonexistent. +End S. diff --git a/theories/Logic/vo.itarget b/theories/Logic/vo.itarget index 8b0aa6691e..5eba0b6235 100644 --- a/theories/Logic/vo.itarget +++ b/theories/Logic/vo.itarget @@ -27,6 +27,7 @@ IndefiniteDescription.vo JMeq.vo ProofIrrelevanceFacts.vo ProofIrrelevance.vo +PropFacts.vo PropExtensionality.vo RelationalChoice.vo SetIsType.vo diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v index 048e409cde..5f04cf242e 100644 --- a/theories/QArith/Qreals.v +++ b/theories/QArith/Qreals.v @@ -15,7 +15,8 @@ Definition Q2R (x : Q) : R := (IZR (Qnum x) * / IZR (QDen x))%R. Lemma IZR_nz : forall p : positive, IZR (Zpos p) <> 0%R. Proof. -intros; apply not_O_IZR; auto with qarith. +intros. +now apply not_O_IZR. Qed. Hint Resolve IZR_nz Rmult_integral_contrapositive. @@ -48,8 +49,7 @@ assert ((X1 * Y2)%R = (Y1 * X2)%R). apply IZR_eq; auto. clear H. field_simplify_eq; auto. -ring_simplify X1 Y2 (Y2 * X1)%R. -rewrite H0; ring. +rewrite H0; ring. Qed. Lemma Rle_Qle : forall x y : Q, (Q2R x <= Q2R y)%R -> x<=y. @@ -66,10 +66,8 @@ replace (X1 * Y2)%R with (X1 * / X2 * (X2 * Y2))%R; try (field; auto). replace (Y1 * X2)%R with (Y1 * / Y2 * (X2 * Y2))%R; try (field; auto). apply Rmult_le_compat_r; auto. apply Rmult_le_pos. -unfold X2; replace 0%R with (IZR 0); auto; apply IZR_le; - auto with zarith. -unfold Y2; replace 0%R with (IZR 0); auto; apply IZR_le; - auto with zarith. +now apply IZR_le. +now apply IZR_le. Qed. Lemma Qle_Rle : forall x y : Q, x<=y -> (Q2R x <= Q2R y)%R. @@ -88,10 +86,8 @@ replace (X1 * / X2)%R with (X1 * Y2 * (/ X2 * / Y2))%R; try (field; auto). replace (Y1 * / Y2)%R with (Y1 * X2 * (/ X2 * / Y2))%R; try (field; auto). apply Rmult_le_compat_r; auto. apply Rmult_le_pos; apply Rlt_le; apply Rinv_0_lt_compat. -unfold X2; replace 0%R with (IZR 0); auto; apply IZR_lt; red; - auto with zarith. -unfold Y2; replace 0%R with (IZR 0); auto; apply IZR_lt; red; - auto with zarith. +now apply IZR_lt. +now apply IZR_lt. Qed. Lemma Rlt_Qlt : forall x y : Q, (Q2R x < Q2R y)%R -> x<y. @@ -108,10 +104,8 @@ replace (X1 * Y2)%R with (X1 * / X2 * (X2 * Y2))%R; try (field; auto). replace (Y1 * X2)%R with (Y1 * / Y2 * (X2 * Y2))%R; try (field; auto). apply Rmult_lt_compat_r; auto. apply Rmult_lt_0_compat. -unfold X2; replace 0%R with (IZR 0); auto; apply IZR_lt; red; - auto with zarith. -unfold Y2; replace 0%R with (IZR 0); auto; apply IZR_lt; red; - auto with zarith. +now apply IZR_lt. +now apply IZR_lt. Qed. Lemma Qlt_Rlt : forall x y : Q, x<y -> (Q2R x < Q2R y)%R. @@ -130,10 +124,8 @@ replace (X1 * / X2)%R with (X1 * Y2 * (/ X2 * / Y2))%R; try (field; auto). replace (Y1 * / Y2)%R with (Y1 * X2 * (/ X2 * / Y2))%R; try (field; auto). apply Rmult_lt_compat_r; auto. apply Rmult_lt_0_compat; apply Rinv_0_lt_compat. -unfold X2; replace 0%R with (IZR 0); auto; apply IZR_lt; red; - auto with zarith. -unfold Y2; replace 0%R with (IZR 0); auto; apply IZR_lt; red; - auto with zarith. +now apply IZR_lt. +now apply IZR_lt. Qed. Lemma Q2R_plus : forall x y : Q, Q2R (x+y) = (Q2R x + Q2R y)%R. diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v index c3ab8edc5e..17ffc0fe32 100644 --- a/theories/Reals/AltSeries.v +++ b/theories/Reals/AltSeries.v @@ -339,51 +339,24 @@ Proof. symmetry ; apply S_pred with 0%nat. assumption. apply Rle_lt_trans with (/ INR (2 * N)). - apply Rmult_le_reg_l with (INR (2 * N)). + apply Rinv_le_contravar. rewrite mult_INR; apply Rmult_lt_0_compat; [ simpl; prove_sup0 | apply lt_INR_0; assumption ]. - rewrite <- Rinv_r_sym. - apply Rmult_le_reg_l with (INR (2 * n)). - rewrite mult_INR; apply Rmult_lt_0_compat; - [ simpl; prove_sup0 | apply lt_INR_0; assumption ]. - rewrite (Rmult_comm (INR (2 * n))); rewrite Rmult_assoc; - rewrite <- Rinv_l_sym. - do 2 rewrite Rmult_1_r; apply le_INR. - apply (fun m n p:nat => mult_le_compat_l p n m); assumption. - replace n with (S (pred n)). - apply not_O_INR; discriminate. - symmetry ; apply S_pred with 0%nat. - assumption. - replace N with (S (pred N)). - apply not_O_INR; discriminate. - symmetry ; apply S_pred with 0%nat. - assumption. + apply le_INR. + now apply mult_le_compat_l. rewrite mult_INR. - rewrite Rinv_mult_distr. - replace (INR 2) with 2; [ idtac | reflexivity ]. - apply Rmult_lt_reg_l with 2. - prove_sup0. - rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ idtac | discrR ]. - rewrite Rmult_1_l; apply Rmult_lt_reg_l with (INR N). - apply lt_INR_0; assumption. - rewrite <- Rinv_r_sym. - apply Rmult_lt_reg_l with (/ (2 * eps)). - apply Rinv_0_lt_compat; assumption. - rewrite Rmult_1_r; - replace (/ (2 * eps) * (INR N * (2 * eps))) with - (INR N * (2 * eps * / (2 * eps))); [ idtac | ring ]. - rewrite <- Rinv_r_sym. - rewrite Rmult_1_r; replace (INR N) with (IZR (Z.of_nat N)). - rewrite <- H4. - elim H1; intros; assumption. - symmetry ; apply INR_IZR_INZ. - apply prod_neq_R0; - [ discrR | red; intro; rewrite H8 in H; elim (Rlt_irrefl _ H) ]. - apply not_O_INR. - red; intro; rewrite H8 in H5; elim (lt_irrefl _ H5). - replace (INR 2) with 2; [ discrR | reflexivity ]. - apply not_O_INR. - red; intro; rewrite H8 in H5; elim (lt_irrefl _ H5). + apply Rmult_lt_reg_l with (INR N / eps). + apply Rdiv_lt_0_compat with (2 := H). + now apply (lt_INR 0). + replace (_ */ _) with (/(2 * eps)). + replace (_ / _ * _) with (INR N). + rewrite INR_IZR_INZ. + now rewrite <- H4. + field. + now apply Rgt_not_eq. + simpl (INR 2); field; split. + now apply Rgt_not_eq, (lt_INR 0). + now apply Rgt_not_eq. apply Rle_ge; apply PI_tg_pos. apply lt_le_trans with N; assumption. elim H1; intros H5 _. @@ -395,7 +368,6 @@ Proof. elim (Rlt_irrefl _ (Rlt_trans _ _ _ H6 H5)). elim (lt_n_O _ H6). apply le_IZR. - simpl. left; apply Rlt_trans with (/ (2 * eps)). apply Rinv_0_lt_compat; assumption. elim H1; intros; assumption. diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v index b14d807d2e..eb4a3b8047 100644 --- a/theories/Reals/Cos_plus.v +++ b/theories/Reals/Cos_plus.v @@ -289,11 +289,9 @@ Proof. apply INR_fact_lt_0. rewrite <- Rinv_r_sym. rewrite Rmult_1_r. - replace 1 with (INR 1). - apply le_INR. + apply (le_INR 1). apply lt_le_S. apply INR_lt; apply INR_fact_lt_0. - reflexivity. apply INR_fact_neq_0. apply Rmult_le_reg_l with (INR (fact (S (N + n)))). apply INR_fact_lt_0. @@ -576,11 +574,9 @@ Proof. apply INR_fact_lt_0. rewrite <- Rinv_r_sym. rewrite Rmult_1_r. - replace 1 with (INR 1). - apply le_INR. + apply (le_INR 1). apply lt_le_S. apply INR_lt; apply INR_fact_lt_0. - reflexivity. apply INR_fact_neq_0. apply Rmult_le_reg_l with (INR (fact (S (S (N + n))))). apply INR_fact_lt_0. diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v index e9de24898e..76f4e14495 100644 --- a/theories/Reals/Exp_prop.v +++ b/theories/Reals/Exp_prop.v @@ -532,7 +532,7 @@ Proof. apply Rmult_le_reg_l with (INR (fact (div2 (pred n)))). apply INR_fact_lt_0. rewrite Rmult_1_r; rewrite <- Rinv_r_sym. - replace 1 with (INR 1); [ apply le_INR | reflexivity ]. + apply (le_INR 1). apply lt_le_S. apply INR_lt. apply INR_fact_lt_0. diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index dd2108159f..7e1cc3e036 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -1629,7 +1629,7 @@ Hint Resolve lt_INR: real. Lemma lt_1_INR : forall n:nat, (1 < n)%nat -> 1 < INR n. Proof. - intros; replace 1 with (INR 1); auto with real. + apply lt_INR. Qed. Hint Resolve lt_1_INR: real. @@ -1653,17 +1653,16 @@ Hint Resolve pos_INR: real. Lemma INR_lt : forall n m:nat, INR n < INR m -> (n < m)%nat. Proof. - double induction n m; intros. - simpl; exfalso; apply (Rlt_irrefl 0); auto. - auto with arith. - generalize (pos_INR (S n0)); intro; cut (INR 0 = 0); - [ intro H2; rewrite H2 in H0; idtac | simpl; trivial ]. - generalize (Rle_lt_trans 0 (INR (S n0)) 0 H1 H0); intro; exfalso; - apply (Rlt_irrefl 0); auto. - do 2 rewrite S_INR in H1; cut (INR n1 < INR n0). - intro H2; generalize (H0 n0 H2); intro; auto with arith. - apply (Rplus_lt_reg_l 1 (INR n1) (INR n0)). - rewrite Rplus_comm; rewrite (Rplus_comm 1 (INR n0)); trivial. + intros n m. revert n. + induction m ; intros n H. + - elim (Rlt_irrefl 0). + apply Rle_lt_trans with (2 := H). + apply pos_INR. + - destruct n as [|n]. + apply Nat.lt_0_succ. + apply lt_n_S, IHm. + rewrite 2!S_INR in H. + apply Rplus_lt_reg_r with (1 := H). Qed. Hint Resolve INR_lt: real. @@ -1707,14 +1706,10 @@ Hint Resolve not_INR: real. Lemma INR_eq : forall n m:nat, INR n = INR m -> n = m. Proof. - intros; case (le_or_lt n m); intros H1. - case (le_lt_or_eq _ _ H1); intros H2; auto. - cut (n <> m). - intro H3; generalize (not_INR n m H3); intro H4; exfalso; auto. - omega. - symmetry ; cut (m <> n). - intro H3; generalize (not_INR m n H3); intro H4; exfalso; auto. - omega. + intros n m HR. + destruct (dec_eq_nat n m) as [H|H]. + exact H. + now apply not_INR in H. Qed. Hint Resolve INR_eq: real. @@ -1728,7 +1723,8 @@ Hint Resolve INR_le: real. Lemma not_1_INR : forall n:nat, n <> 1%nat -> INR n <> 1. Proof. - replace 1 with (INR 1); auto with real. + intros n. + apply not_INR. Qed. Hint Resolve not_1_INR: real. @@ -1905,8 +1901,8 @@ Qed. (**********) Lemma le_IZR_R1 : forall n:Z, IZR n <= 1 -> (n <= 1)%Z. Proof. - pattern 1 at 1; replace 1 with (IZR 1); intros; auto. - apply le_IZR; trivial. + intros n. + apply le_IZR. Qed. (**********) @@ -1935,7 +1931,7 @@ Proof. intros z [H1 H2]. apply Z.le_antisymm. apply Z.lt_succ_r; apply lt_IZR; trivial. - replace 0%Z with (Z.succ (-1)); trivial. + change 0%Z with (Z.succ (-1)). apply Z.le_succ_l; apply lt_IZR; trivial. Qed. @@ -2012,12 +2008,11 @@ Lemma double_var : forall r1, r1 = r1 / 2 + r1 / 2. Proof. intro; rewrite <- double; unfold Rdiv; rewrite <- Rmult_assoc; symmetry ; apply Rinv_r_simpl_m. - replace 2 with (INR 2); - [ apply not_0_INR; discriminate | unfold INR; ring ]. + now apply not_0_IZR. Qed. Lemma R_rm : ring_morph - R0 R1 Rplus Rmult Rminus Ropp eq + 0%R 1%R Rplus Rmult Rminus Ropp eq 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool IZR. Proof. constructor ; try easy. diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v index e9b1762af8..46583d374e 100644 --- a/theories/Reals/R_Ifp.v +++ b/theories/Reals/R_Ifp.v @@ -42,28 +42,23 @@ Qed. Lemma up_tech : forall (r:R) (z:Z), IZR z <= r -> r < IZR (z + 1) -> (z + 1)%Z = up r. Proof. - intros; generalize (Rplus_le_compat_l 1 (IZR z) r H); intro; clear H; - rewrite (Rplus_comm 1 (IZR z)) in H1; rewrite (Rplus_comm 1 r) in H1; - cut (1 = IZR 1); auto with zarith real. - intro; generalize H1; pattern 1 at 1; rewrite H; intro; clear H H1; - rewrite <- (plus_IZR z 1) in H2; apply (tech_up r (z + 1)); - auto with zarith real. + intros. + apply tech_up with (1 := H0). + rewrite plus_IZR. + now apply Rplus_le_compat_r. Qed. (**********) Lemma fp_R0 : frac_part 0 = 0. Proof. - unfold frac_part; unfold Int_part; elim (archimed 0); intros; - unfold Rminus; elim (Rplus_ne (- IZR (up 0 - 1))); - intros a b; rewrite b; clear a b; rewrite <- Z_R_minus; - cut (up 0 = 1%Z). - intro; rewrite H1; - rewrite (Rminus_diag_eq (IZR 1) (IZR 1) (eq_refl (IZR 1))); - apply Ropp_0. - elim (archimed 0); intros; clear H2; unfold Rgt in H1; - rewrite (Rminus_0_r (IZR (up 0))) in H0; generalize (lt_O_IZR (up 0) H1); - intro; clear H1; generalize (le_IZR_R1 (up 0) H0); - intro; clear H H0; omega. + unfold frac_part, Int_part. + replace (up 0) with 1%Z. + now rewrite <- minus_IZR. + destruct (archimed 0) as [H1 H2]. + apply lt_IZR in H1. + rewrite <- minus_IZR in H2. + apply le_IZR in H2. + omega. Qed. (**********) @@ -229,8 +224,7 @@ Proof. rewrite (Rplus_opp_r (IZR (Int_part r1) - IZR (Int_part r2))) in H; elim (Rplus_ne (r1 - r2)); intros a b; rewrite b in H; clear a b; rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H0; - rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H; - cut (1 = IZR 1); auto with zarith real. + rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H. rewrite <- (plus_IZR (Int_part r1 - Int_part r2) 1) in H; generalize (up_tech (r1 - r2) (Int_part r1 - Int_part r2) H0 H); intros; clear H H0; unfold Int_part at 1; @@ -497,8 +491,7 @@ Proof. in H0; rewrite (Rplus_opp_r (IZR (Int_part r1) + IZR (Int_part r2))) in H0; elim (Rplus_ne (IZR (Int_part r1) + IZR (Int_part r2))); intros a b; rewrite a in H0; clear a b; elim (Rplus_ne (r1 + r2)); - intros a b; rewrite b in H0; clear a b; cut (1 = IZR 1); - auto with zarith real. + intros a b; rewrite b in H0; clear a b. rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H0; rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H1; rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H1; diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v index 27cb356a09..b749da0d2a 100644 --- a/theories/Reals/Ranalysis2.v +++ b/theories/Reals/Ranalysis2.v @@ -423,10 +423,7 @@ Proof. intro; rewrite H11 in H10; assert (H12 := Rmult_lt_compat_l 2 _ _ Hyp H10); rewrite Rmult_1_r in H12; rewrite <- Rinv_r_sym in H12; [ idtac | discrR ]. - cut (IZR 1 < IZR 2). - unfold IZR; unfold INR, Pos.to_nat; simpl; intro; - elim (Rlt_irrefl 1 (Rlt_trans _ _ _ H13 H12)). - apply IZR_lt; omega. + now apply lt_IZR in H12. unfold Rabs; case (Rcase_abs (/ 2)) as [Hlt|Hge]. assert (Hyp : 0 < 2). prove_sup0. diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index 7885d697f1..af7cbb940d 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -83,11 +83,10 @@ Proof. cut (x = INR (pred x0)). intro H19; rewrite H19; apply le_INR; apply lt_le_S; apply INR_lt; rewrite H18; rewrite <- H19; assumption. - rewrite H10; rewrite H8; rewrite <- INR_IZR_INZ; replace 1 with (INR 1); - [ idtac | reflexivity ]; rewrite <- minus_INR. - replace (x0 - 1)%nat with (pred x0); - [ reflexivity - | case x0; [ reflexivity | intro; simpl; apply minus_n_O ] ]. + rewrite H10; rewrite H8; rewrite <- INR_IZR_INZ; + rewrite <- (minus_INR _ 1). + apply f_equal; + case x0; [ reflexivity | intro; apply sym_eq, minus_n_O ]. induction x0 as [|x0 Hrecx0]. rewrite H8 in H3. rewrite <- INR_IZR_INZ in H3; simpl in H3. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H6 H3)). diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index f071407521..843aa27521 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -29,59 +29,28 @@ Qed. Lemma eps2 : forall eps:R, eps * / 2 + eps * / 2 = eps. Proof. intro esp. - assert (H := double_var esp). - unfold Rdiv in H. - symmetry ; exact H. + apply eq_sym, double_var. Qed. (*********) Lemma eps4 : forall eps:R, eps * / (2 + 2) + eps * / (2 + 2) = eps * / 2. Proof. intro eps. - replace (2 + 2) with 4. - pattern eps at 3; rewrite double_var. - rewrite (Rmult_plus_distr_r (eps / 2) (eps / 2) (/ 2)). - unfold Rdiv. - repeat rewrite Rmult_assoc. - rewrite <- Rinv_mult_distr. - reflexivity. - discrR. - discrR. - ring. + field. Qed. (*********) Lemma Rlt_eps2_eps : forall eps:R, eps > 0 -> eps * / 2 < eps. Proof. intros. - pattern eps at 2; rewrite <- Rmult_1_r. - repeat rewrite (Rmult_comm eps). - apply Rmult_lt_compat_r. - exact H. - apply Rmult_lt_reg_l with 2. fourier. - rewrite Rmult_1_r; rewrite <- Rinv_r_sym. - fourier. - discrR. Qed. (*********) Lemma Rlt_eps4_eps : forall eps:R, eps > 0 -> eps * / (2 + 2) < eps. Proof. intros. - replace (2 + 2) with 4. - pattern eps at 2; rewrite <- Rmult_1_r. - repeat rewrite (Rmult_comm eps). - apply Rmult_lt_compat_r. - exact H. - apply Rmult_lt_reg_l with 4. - replace 4 with 4. - apply Rmult_lt_0_compat; fourier. - ring. - rewrite Rmult_1_r; rewrite <- Rinv_r_sym. fourier. - discrR. - ring. Qed. (*********) diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index f62ed2a6c1..b8040bb4f5 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -456,7 +456,7 @@ Proof. unfold Rpower; auto. rewrite Rpower_mult. rewrite Rinv_l. - replace 1 with (INR 1); auto. + change 1 with (INR 1). repeat rewrite Rpower_pow; simpl. pattern x at 1; rewrite <- (sqrt_sqrt x (Rlt_le _ _ H)). ring. diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v index b3c9c7449a..6c2b0a1a77 100644 --- a/theories/Reals/Rsqrt_def.v +++ b/theories/Reals/Rsqrt_def.v @@ -648,7 +648,7 @@ Proof. Qed. (** We can now define the square root function as the reciprocal - transformation of the square root function *) + transformation of the square function *) Lemma Rsqrt_exists : forall y:R, 0 <= y -> { z:R | 0 <= z /\ y = Rsqr z }. Proof. diff --git a/theories/Reals/Rtrigo1.v b/theories/Reals/Rtrigo1.v index 17b9677eff..5a999eebe6 100644 --- a/theories/Reals/Rtrigo1.v +++ b/theories/Reals/Rtrigo1.v @@ -694,16 +694,15 @@ Proof. rewrite <- Rinv_l_sym. do 2 rewrite Rmult_1_r; apply Rle_lt_trans with (INR (fact (2 * n + 1)) * 4). apply Rmult_le_compat_l. - replace 0 with (INR 0); [ idtac | reflexivity ]; apply le_INR; apply le_O_n. - simpl in |- *; rewrite Rmult_1_r; replace 4 with (Rsqr 2); - [ idtac | ring_Rsqr ]; replace (a * a) with (Rsqr a); - [ idtac | reflexivity ]; apply Rsqr_incr_1. + apply pos_INR. + simpl in |- *; rewrite Rmult_1_r; change 4 with (Rsqr 2); + apply Rsqr_incr_1. apply Rle_trans with (PI / 2); [ assumption | unfold Rdiv in |- *; apply Rmult_le_reg_l with 2; [ prove_sup0 | rewrite <- Rmult_assoc; rewrite Rinv_r_simpl_m; - [ replace 4 with 4; [ apply PI_4 | ring ] | discrR ] ] ]. + [ apply PI_4 | discrR ] ] ]. left; assumption. left; prove_sup0. rewrite H1; replace (2 * n + 1 + 2)%nat with (S (S (2 * n + 1))). @@ -725,9 +724,8 @@ Proof. cut (0 <= x). intro; apply Rplus_le_le_0_compat; repeat apply Rmult_le_pos; assumption || left; prove_sup. - unfold x in |- *; replace 0 with (INR 0); - [ apply le_INR; apply le_O_n | reflexivity ]. - prove_sup0. + apply pos_INR. + now apply IZR_lt. ring. apply INR_fact_neq_0. apply INR_fact_neq_0. @@ -735,39 +733,33 @@ Proof. Qed. Lemma SIN : forall a:R, 0 <= a -> a <= PI -> sin_lb a <= sin a <= sin_ub a. +Proof. intros; unfold sin_lb, sin_ub in |- *; apply (sin_bound a 1 H H0). Qed. Lemma COS : forall a:R, - PI / 2 <= a -> a <= PI / 2 -> cos_lb a <= cos a <= cos_ub a. +Proof. intros; unfold cos_lb, cos_ub in |- *; apply (cos_bound a 1 H H0). Qed. (**********) Lemma _PI2_RLT_0 : - (PI / 2) < 0. Proof. - rewrite <- Ropp_0; apply Ropp_lt_contravar; apply PI2_RGT_0. + assert (H := PI_RGT_0). + fourier. Qed. Lemma PI4_RLT_PI2 : PI / 4 < PI / 2. Proof. - unfold Rdiv in |- *; apply Rmult_lt_compat_l. - apply PI_RGT_0. - apply Rinv_lt_contravar. - apply Rmult_lt_0_compat; prove_sup0. - pattern 2 at 1 in |- *; rewrite <- Rplus_0_r. - replace 4 with (2 + 2); [ apply Rplus_lt_compat_l; prove_sup0 | ring ]. + assert (H := PI_RGT_0). + fourier. Qed. Lemma PI2_Rlt_PI : PI / 2 < PI. Proof. - unfold Rdiv in |- *; pattern PI at 2 in |- *; rewrite <- Rmult_1_r. - apply Rmult_lt_compat_l. - apply PI_RGT_0. - rewrite <- Rinv_1; apply Rinv_lt_contravar. - rewrite Rmult_1_l; prove_sup0. - pattern 1 at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; - apply Rlt_0_1. + assert (H := PI_RGT_0). + fourier. Qed. (***************************************************) @@ -784,12 +776,10 @@ Proof. rewrite H3; rewrite sin_PI2; apply Rlt_0_1. rewrite <- sin_PI_x; generalize (Ropp_gt_lt_contravar x (PI / 2) H3); intro H4; generalize (Rplus_lt_compat_l PI (- x) (- (PI / 2)) H4). - replace (PI + - x) with (PI - x). replace (PI + - (PI / 2)) with (PI / 2). intro H5; generalize (Ropp_lt_gt_contravar x PI H0); intro H6; change (- PI < - x) in H6; generalize (Rplus_lt_compat_l PI (- PI) (- x) H6). rewrite Rplus_opp_r. - replace (PI + - x) with (PI - x). intro H7; elim (SIN (PI - x) (Rlt_le 0 (PI - x) H7) @@ -797,9 +787,7 @@ Proof. intros H8 _; generalize (sin_lb_gt_0 (PI - x) H7 (Rlt_le (PI - x) (PI / 2) H5)); intro H9; apply (Rlt_le_trans 0 (sin_lb (PI - x)) (sin (PI - x)) H9 H8). - reflexivity. - pattern PI at 2 in |- *; rewrite double_var; ring. - reflexivity. + field. Qed. Theorem cos_gt_0 : forall x:R, - (PI / 2) < x -> x < PI / 2 -> 0 < cos x. @@ -852,16 +840,12 @@ Proof. rewrite <- (Ropp_involutive (cos x)); apply Ropp_le_ge_contravar; rewrite <- neg_cos; replace (x + PI) with (x - PI + 2 * INR 1 * PI). rewrite cos_period; apply cos_ge_0. - replace (- (PI / 2)) with (- PI + PI / 2). + replace (- (PI / 2)) with (- PI + PI / 2) by field. unfold Rminus in |- *; rewrite (Rplus_comm x); apply Rplus_le_compat_l; assumption. - pattern PI at 1 in |- *; rewrite (double_var PI); rewrite Ropp_plus_distr; - ring. unfold Rminus in |- *; rewrite Rplus_comm; - replace (PI / 2) with (- PI + 3 * (PI / 2)). + replace (PI / 2) with (- PI + 3 * (PI / 2)) by field. apply Rplus_le_compat_l; assumption. - pattern PI at 1 in |- *; rewrite (double_var PI); rewrite Ropp_plus_distr; - ring. unfold INR in |- *; ring. Qed. @@ -902,16 +886,12 @@ Proof. apply Ropp_lt_gt_contravar; rewrite <- neg_cos; replace (x + PI) with (x - PI + 2 * INR 1 * PI). rewrite cos_period; apply cos_gt_0. - replace (- (PI / 2)) with (- PI + PI / 2). + replace (- (PI / 2)) with (- PI + PI / 2) by field. unfold Rminus in |- *; rewrite (Rplus_comm x); apply Rplus_lt_compat_l; assumption. - pattern PI at 1 in |- *; rewrite (double_var PI); rewrite Ropp_plus_distr; - ring. unfold Rminus in |- *; rewrite Rplus_comm; - replace (PI / 2) with (- PI + 3 * (PI / 2)). + replace (PI / 2) with (- PI + 3 * (PI / 2)) by field. apply Rplus_lt_compat_l; assumption. - pattern PI at 1 in |- *; rewrite (double_var PI); rewrite Ropp_plus_distr; - ring. unfold INR in |- *; ring. Qed. @@ -948,7 +928,7 @@ Lemma cos_ge_0_3PI2 : forall x:R, 3 * (PI / 2) <= x -> x <= 2 * PI -> 0 <= cos x. Proof. intros; rewrite <- cos_neg; rewrite <- (cos_period (- x) 1); - unfold INR in |- *; replace (- x + 2 * 1 * PI) with (2 * PI - x). + unfold INR in |- *; replace (- x + 2 * 1 * PI) with (2 * PI - x) by ring. generalize (Ropp_le_ge_contravar x (2 * PI) H0); intro H1; generalize (Rge_le (- x) (- (2 * PI)) H1); clear H1; intro H1; generalize (Rplus_le_compat_l (2 * PI) (- (2 * PI)) (- x) H1). @@ -957,36 +937,30 @@ Proof. generalize (Rge_le (- (3 * (PI / 2))) (- x) H3); clear H3; intro H3; generalize (Rplus_le_compat_l (2 * PI) (- x) (- (3 * (PI / 2))) H3). - replace (2 * PI + - (3 * (PI / 2))) with (PI / 2). + replace (2 * PI + - (3 * (PI / 2))) with (PI / 2) by field. intro H4; apply (cos_ge_0 (2 * PI - x) (Rlt_le (- (PI / 2)) (2 * PI - x) (Rlt_le_trans (- (PI / 2)) 0 (2 * PI - x) _PI2_RLT_0 H2)) H4). - rewrite double; pattern PI at 2 3 in |- *; rewrite double_var; ring. - ring. Qed. Lemma form1 : forall p q:R, cos p + cos q = 2 * cos ((p - q) / 2) * cos ((p + q) / 2). Proof. intros p q; pattern p at 1 in |- *; - replace p with ((p - q) / 2 + (p + q) / 2). - rewrite <- (cos_neg q); replace (- q) with ((p - q) / 2 - (p + q) / 2). + replace p with ((p - q) / 2 + (p + q) / 2) by field. + rewrite <- (cos_neg q); replace (- q) with ((p - q) / 2 - (p + q) / 2) by field. rewrite cos_plus; rewrite cos_minus; ring. - pattern q at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring. - pattern p at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring. Qed. Lemma form2 : forall p q:R, cos p - cos q = -2 * sin ((p - q) / 2) * sin ((p + q) / 2). Proof. intros p q; pattern p at 1 in |- *; - replace p with ((p - q) / 2 + (p + q) / 2). - rewrite <- (cos_neg q); replace (- q) with ((p - q) / 2 - (p + q) / 2). + replace p with ((p - q) / 2 + (p + q) / 2) by field. + rewrite <- (cos_neg q); replace (- q) with ((p - q) / 2 - (p + q) / 2) by field. rewrite cos_plus; rewrite cos_minus; ring. - pattern q at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring. - pattern p at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring. Qed. Lemma form3 : @@ -1004,11 +978,9 @@ Lemma form4 : forall p q:R, sin p - sin q = 2 * cos ((p + q) / 2) * sin ((p - q) / 2). Proof. intros p q; pattern p at 1 in |- *; - replace p with ((p - q) / 2 + (p + q) / 2). - pattern q at 3 in |- *; replace q with ((p + q) / 2 - (p - q) / 2). + replace p with ((p - q) / 2 + (p + q) / 2) by field. + pattern q at 3 in |- *; replace q with ((p + q) / 2 - (p - q) / 2) by field. rewrite sin_plus; rewrite sin_minus; ring. - pattern q at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring. - pattern p at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring. Qed. @@ -1064,13 +1036,13 @@ Proof. repeat rewrite (Rmult_comm (/ 2)). clear H4; intro H4; generalize (Rplus_le_compat (- (PI / 2)) x (- (PI / 2)) y H H1); - replace (- (PI / 2) + - (PI / 2)) with (- PI). + replace (- (PI / 2) + - (PI / 2)) with (- PI) by field. intro H5; generalize (Rmult_le_compat_l (/ 2) (- PI) (x + y) (Rlt_le 0 (/ 2) (Rinv_0_lt_compat 2 Hyp)) H5). - replace (/ 2 * (x + y)) with ((x + y) / 2). - replace (/ 2 * - PI) with (- (PI / 2)). + replace (/ 2 * (x + y)) with ((x + y) / 2) by apply Rmult_comm. + replace (/ 2 * - PI) with (- (PI / 2)) by field. clear H5; intro H5; elim H4; intro H40. elim H5; intro H50. generalize (cos_gt_0 ((x + y) / 2) H50 H40); intro H6; @@ -1092,13 +1064,6 @@ Proof. rewrite H40 in H3; assert (H50 := cos_PI2); unfold Rdiv in H50; rewrite H50 in H3; rewrite Rmult_0_r in H3; rewrite Rmult_0_l in H3; elim (Rlt_irrefl 0 H3). - unfold Rdiv in |- *. - rewrite <- Ropp_mult_distr_l_reverse. - apply Rmult_comm. - unfold Rdiv in |- *; apply Rmult_comm. - pattern PI at 1 in |- *; rewrite double_var. - rewrite Ropp_plus_distr. - reflexivity. Qed. Lemma sin_increasing_1 : @@ -1108,43 +1073,42 @@ Lemma sin_increasing_1 : Proof. intros; generalize (Rplus_lt_compat_l x x y H3); intro H4; generalize (Rplus_le_compat (- (PI / 2)) x (- (PI / 2)) x H H); - replace (- (PI / 2) + - (PI / 2)) with (- PI). + replace (- (PI / 2) + - (PI / 2)) with (- PI) by field. assert (Hyp : 0 < 2). prove_sup0. intro H5; generalize (Rle_lt_trans (- PI) (x + x) (x + y) H5 H4); intro H6; generalize (Rmult_lt_compat_l (/ 2) (- PI) (x + y) (Rinv_0_lt_compat 2 Hyp) H6); - replace (/ 2 * - PI) with (- (PI / 2)). - replace (/ 2 * (x + y)) with ((x + y) / 2). + replace (/ 2 * - PI) with (- (PI / 2)) by field. + replace (/ 2 * (x + y)) with ((x + y) / 2) by apply Rmult_comm. clear H4 H5 H6; intro H4; generalize (Rplus_lt_compat_l y x y H3); intro H5; rewrite Rplus_comm in H5; generalize (Rplus_le_compat y (PI / 2) y (PI / 2) H2 H2). rewrite <- double_var. intro H6; generalize (Rlt_le_trans (x + y) (y + y) PI H5 H6); intro H7; generalize (Rmult_lt_compat_l (/ 2) (x + y) PI (Rinv_0_lt_compat 2 Hyp) H7); - replace (/ 2 * PI) with (PI / 2). - replace (/ 2 * (x + y)) with ((x + y) / 2). + replace (/ 2 * PI) with (PI / 2) by apply Rmult_comm. + replace (/ 2 * (x + y)) with ((x + y) / 2) by apply Rmult_comm. clear H5 H6 H7; intro H5; generalize (Ropp_le_ge_contravar (- (PI / 2)) y H1); rewrite Ropp_involutive; clear H1; intro H1; generalize (Rge_le (PI / 2) (- y) H1); clear H1; intro H1; generalize (Ropp_le_ge_contravar y (PI / 2) H2); clear H2; intro H2; generalize (Rge_le (- y) (- (PI / 2)) H2); clear H2; intro H2; generalize (Rplus_lt_compat_l (- y) x y H3); - replace (- y + x) with (x - y). + replace (- y + x) with (x - y) by apply Rplus_comm. rewrite Rplus_opp_l. intro H6; generalize (Rmult_lt_compat_l (/ 2) (x - y) 0 (Rinv_0_lt_compat 2 Hyp) H6); - rewrite Rmult_0_r; replace (/ 2 * (x - y)) with ((x - y) / 2). + rewrite Rmult_0_r; replace (/ 2 * (x - y)) with ((x - y) / 2) by apply Rmult_comm. clear H6; intro H6; generalize (Rplus_le_compat (- (PI / 2)) x (- (PI / 2)) (- y) H H2); - replace (- (PI / 2) + - (PI / 2)) with (- PI). - replace (x + - y) with (x - y). + replace (- (PI / 2) + - (PI / 2)) with (- PI) by field. intro H7; generalize (Rmult_le_compat_l (/ 2) (- PI) (x - y) (Rlt_le 0 (/ 2) (Rinv_0_lt_compat 2 Hyp)) H7); - replace (/ 2 * - PI) with (- (PI / 2)). - replace (/ 2 * (x - y)) with ((x - y) / 2). + replace (/ 2 * - PI) with (- (PI / 2)) by field. + replace (/ 2 * (x - y)) with ((x - y) / 2) by apply Rmult_comm. clear H7; intro H7; clear H H0 H1 H2; apply Rminus_lt; rewrite form4; generalize (cos_gt_0 ((x + y) / 2) H4 H5); intro H8; generalize (Rmult_lt_0_compat 2 (cos ((x + y) / 2)) Hyp H8); @@ -1159,23 +1123,6 @@ Proof. 2 * cos ((x + y) / 2)) H10 H8); intro H11; rewrite Rmult_0_r in H11; rewrite Rmult_comm; assumption. apply Ropp_lt_gt_contravar; apply PI2_Rlt_PI. - unfold Rdiv in |- *; apply Rmult_comm. - unfold Rdiv in |- *; rewrite <- Ropp_mult_distr_l_reverse; apply Rmult_comm. - reflexivity. - pattern PI at 1 in |- *; rewrite double_var. - rewrite Ropp_plus_distr. - reflexivity. - unfold Rdiv in |- *; apply Rmult_comm. - unfold Rminus in |- *; apply Rplus_comm. - unfold Rdiv in |- *; apply Rmult_comm. - unfold Rdiv in |- *; apply Rmult_comm. - unfold Rdiv in |- *; apply Rmult_comm. - unfold Rdiv in |- *. - rewrite <- Ropp_mult_distr_l_reverse. - apply Rmult_comm. - pattern PI at 1 in |- *; rewrite double_var. - rewrite Ropp_plus_distr. - reflexivity. Qed. Lemma sin_decreasing_0 : @@ -1190,33 +1137,16 @@ Proof. generalize (Rplus_le_compat_l (- PI) (PI / 2) x H0); generalize (Rplus_le_compat_l (- PI) y (3 * (PI / 2)) H1); generalize (Rplus_le_compat_l (- PI) (PI / 2) y H2); - replace (- PI + x) with (x - PI). - replace (- PI + PI / 2) with (- (PI / 2)). - replace (- PI + y) with (y - PI). - replace (- PI + 3 * (PI / 2)) with (PI / 2). - replace (- (PI - x)) with (x - PI). - replace (- (PI - y)) with (y - PI). + replace (- PI + x) with (x - PI) by apply Rplus_comm. + replace (- PI + PI / 2) with (- (PI / 2)) by field. + replace (- PI + y) with (y - PI) by apply Rplus_comm. + replace (- PI + 3 * (PI / 2)) with (PI / 2) by field. + replace (- (PI - x)) with (x - PI) by ring. + replace (- (PI - y)) with (y - PI) by ring. intros; change (sin (y - PI) < sin (x - PI)) in H8; - apply Rplus_lt_reg_l with (- PI); rewrite Rplus_comm; - replace (y + - PI) with (y - PI). - rewrite Rplus_comm; replace (x + - PI) with (x - PI). + apply Rplus_lt_reg_l with (- PI); rewrite Rplus_comm. + rewrite (Rplus_comm _ x). apply (sin_increasing_0 (y - PI) (x - PI) H4 H5 H6 H7 H8). - reflexivity. - reflexivity. - unfold Rminus in |- *; rewrite Ropp_plus_distr. - rewrite Ropp_involutive. - apply Rplus_comm. - unfold Rminus in |- *; rewrite Ropp_plus_distr. - rewrite Ropp_involutive. - apply Rplus_comm. - pattern PI at 2 in |- *; rewrite double_var. - rewrite Ropp_plus_distr. - ring. - unfold Rminus in |- *; apply Rplus_comm. - pattern PI at 2 in |- *; rewrite double_var. - rewrite Ropp_plus_distr. - ring. - unfold Rminus in |- *; apply Rplus_comm. Qed. Lemma sin_decreasing_1 : @@ -1230,24 +1160,14 @@ Proof. generalize (Rplus_le_compat_l (- PI) y (3 * (PI / 2)) H1); generalize (Rplus_le_compat_l (- PI) (PI / 2) y H2); generalize (Rplus_lt_compat_l (- PI) x y H3); - replace (- PI + PI / 2) with (- (PI / 2)). - replace (- PI + y) with (y - PI). - replace (- PI + 3 * (PI / 2)) with (PI / 2). - replace (- PI + x) with (x - PI). + replace (- PI + PI / 2) with (- (PI / 2)) by field. + replace (- PI + y) with (y - PI) by apply Rplus_comm. + replace (- PI + 3 * (PI / 2)) with (PI / 2) by field. + replace (- PI + x) with (x - PI) by apply Rplus_comm. intros; apply Ropp_lt_cancel; repeat rewrite <- sin_neg; - replace (- (PI - x)) with (x - PI). - replace (- (PI - y)) with (y - PI). + replace (- (PI - x)) with (x - PI) by ring. + replace (- (PI - y)) with (y - PI) by ring. apply (sin_increasing_1 (x - PI) (y - PI) H7 H8 H5 H6 H4). - unfold Rminus in |- *; rewrite Ropp_plus_distr. - rewrite Ropp_involutive. - apply Rplus_comm. - unfold Rminus in |- *; rewrite Ropp_plus_distr. - rewrite Ropp_involutive. - apply Rplus_comm. - unfold Rminus in |- *; apply Rplus_comm. - pattern PI at 2 in |- *; rewrite double_var; ring. - unfold Rminus in |- *; apply Rplus_comm. - pattern PI at 2 in |- *; rewrite double_var; ring. Qed. Lemma cos_increasing_0 : @@ -1287,31 +1207,16 @@ Proof. generalize (Rplus_lt_compat_l (-3 * (PI / 2)) x y H5); rewrite <- (cos_neg x); rewrite <- (cos_neg y); rewrite <- (cos_period (- x) 1); rewrite <- (cos_period (- y) 1); - unfold INR in |- *; replace (-3 * (PI / 2) + x) with (x - 3 * (PI / 2)). - replace (-3 * (PI / 2) + y) with (y - 3 * (PI / 2)). - replace (-3 * (PI / 2) + PI) with (- (PI / 2)). - replace (-3 * (PI / 2) + 2 * PI) with (PI / 2). + unfold INR in |- *; replace (-3 * (PI / 2) + x) with (x - 3 * (PI / 2)) by ring. + replace (-3 * (PI / 2) + y) with (y - 3 * (PI / 2)) by ring. + replace (-3 * (PI / 2) + PI) with (- (PI / 2)) by field. + replace (-3 * (PI / 2) + 2 * PI) with (PI / 2) by field. clear H1 H2 H3 H4 H5; intros H1 H2 H3 H4 H5; - replace (- x + 2 * 1 * PI) with (PI / 2 - (x - 3 * (PI / 2))). - replace (- y + 2 * 1 * PI) with (PI / 2 - (y - 3 * (PI / 2))). + replace (- x + 2 * 1 * PI) with (PI / 2 - (x - 3 * (PI / 2))) by field. + replace (- y + 2 * 1 * PI) with (PI / 2 - (y - 3 * (PI / 2))) by field. repeat rewrite cos_shift; apply (sin_increasing_1 (x - 3 * (PI / 2)) (y - 3 * (PI / 2)) H5 H4 H3 H2 H1). - rewrite Rmult_1_r. - rewrite (double PI); pattern PI at 3 4 in |- *; rewrite double_var. - ring. - rewrite Rmult_1_r. - rewrite (double PI); pattern PI at 3 4 in |- *; rewrite double_var. - ring. - rewrite (double PI); pattern PI at 3 4 in |- *; rewrite double_var. - ring. - pattern PI at 3 in |- *; rewrite double_var; ring. - unfold Rminus in |- *. - rewrite <- Ropp_mult_distr_l_reverse. - apply Rplus_comm. - unfold Rminus in |- *. - rewrite <- Ropp_mult_distr_l_reverse. - apply Rplus_comm. Qed. Lemma cos_decreasing_0 : @@ -1350,31 +1255,8 @@ Lemma tan_diff : cos x <> 0 -> cos y <> 0 -> tan x - tan y = sin (x - y) / (cos x * cos y). Proof. intros; unfold tan in |- *; rewrite sin_minus. - unfold Rdiv in |- *. - unfold Rminus in |- *. - rewrite Rmult_plus_distr_r. - rewrite Rinv_mult_distr. - repeat rewrite (Rmult_comm (sin x)). - repeat rewrite Rmult_assoc. - rewrite (Rmult_comm (cos y)). - repeat rewrite Rmult_assoc. - rewrite <- Rinv_l_sym. - rewrite Rmult_1_r. - rewrite (Rmult_comm (sin x)). - apply Rplus_eq_compat_l. - rewrite <- Ropp_mult_distr_l_reverse. - rewrite <- Ropp_mult_distr_r_reverse. - rewrite (Rmult_comm (/ cos x)). - repeat rewrite Rmult_assoc. - rewrite (Rmult_comm (cos x)). - repeat rewrite Rmult_assoc. - rewrite <- Rinv_l_sym. - rewrite Rmult_1_r. - reflexivity. - assumption. - assumption. - assumption. - assumption. + field. + now split. Qed. Lemma tan_increasing_0 : @@ -1411,10 +1293,9 @@ Proof. intro H11; generalize (Rge_le (- y) (- (PI / 4)) H11); clear H11; intro H11; generalize (Rplus_le_compat (- (PI / 4)) x (- (PI / 4)) (- y) H H11); - generalize (Rplus_le_compat x (PI / 4) (- y) (PI / 4) H0 H10); - replace (x + - y) with (x - y). - replace (PI / 4 + PI / 4) with (PI / 2). - replace (- (PI / 4) + - (PI / 4)) with (- (PI / 2)). + generalize (Rplus_le_compat x (PI / 4) (- y) (PI / 4) H0 H10). + replace (PI / 4 + PI / 4) with (PI / 2) by field. + replace (- (PI / 4) + - (PI / 4)) with (- (PI / 2)) by field. intros; case (Rtotal_order 0 (x - y)); intro H14. generalize (sin_gt_0 (x - y) H14 (Rle_lt_trans (x - y) (PI / 2) PI H12 PI2_Rlt_PI)); @@ -1422,28 +1303,6 @@ Proof. elim H14; intro H15. rewrite <- H15 in H9; rewrite sin_0 in H9; elim (Rlt_irrefl 0 H9). apply Rminus_lt; assumption. - pattern PI at 1 in |- *; rewrite double_var. - unfold Rdiv in |- *. - rewrite Rmult_plus_distr_r. - repeat rewrite Rmult_assoc. - rewrite <- Rinv_mult_distr. - rewrite Ropp_plus_distr. - replace 4 with 4. - reflexivity. - ring. - discrR. - discrR. - pattern PI at 1 in |- *; rewrite double_var. - unfold Rdiv in |- *. - rewrite Rmult_plus_distr_r. - repeat rewrite Rmult_assoc. - rewrite <- Rinv_mult_distr. - replace 4 with 4. - reflexivity. - ring. - discrR. - discrR. - reflexivity. case (Rcase_abs (sin (x - y))); intro H9. assumption. generalize (Rge_le (sin (x - y)) 0 H9); clear H9; intro H9; @@ -1457,8 +1316,7 @@ Proof. (Rlt_le 0 (/ (cos x * cos y)) H12)); intro H13; elim (Rlt_irrefl 0 (Rle_lt_trans 0 (sin (x - y) * / (cos x * cos y)) 0 H13 H3)). - rewrite Rinv_mult_distr. - reflexivity. + apply Rinv_mult_distr. assumption. assumption. Qed. @@ -1496,9 +1354,8 @@ Proof. clear H10 H11; intro H8; generalize (Ropp_le_ge_contravar y (PI / 4) H2); intro H11; generalize (Rge_le (- y) (- (PI / 4)) H11); clear H11; intro H11; - generalize (Rplus_le_compat (- (PI / 4)) x (- (PI / 4)) (- y) H H11); - replace (x + - y) with (x - y). - replace (- (PI / 4) + - (PI / 4)) with (- (PI / 2)). + generalize (Rplus_le_compat (- (PI / 4)) x (- (PI / 4)) (- y) H H11). + replace (- (PI / 4) + - (PI / 4)) with (- (PI / 2)) by field. clear H11; intro H9; generalize (Rlt_minus x y H3); clear H3; intro H3; clear H H0 H1 H2 H4 H5 HP1 HP2; generalize PI2_Rlt_PI; intro H1; generalize (Ropp_lt_gt_contravar (PI / 2) PI H1); @@ -1509,18 +1366,6 @@ Proof. generalize (Rmult_lt_gt_compat_neg_l (sin (x - y)) 0 (/ (cos x * cos y)) H2 H8); rewrite Rmult_0_r; intro H4; assumption. - pattern PI at 1 in |- *; rewrite double_var. - unfold Rdiv in |- *. - rewrite Rmult_plus_distr_r. - repeat rewrite Rmult_assoc. - rewrite <- Rinv_mult_distr. - replace 4 with 4. - rewrite Ropp_plus_distr. - reflexivity. - ring. - discrR. - discrR. - reflexivity. apply Rinv_mult_distr; assumption. Qed. @@ -1762,8 +1607,7 @@ Proof. rewrite Rplus_0_r. rewrite Ropp_Ropp_IZR. rewrite Rplus_opp_r. - left; replace 0 with (IZR 0); [ apply IZR_lt | reflexivity ]. - assumption. + now apply Rlt_le, IZR_lt. rewrite <- sin_neg. rewrite Ropp_mult_distr_l_reverse. rewrite Ropp_involutive. diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v index 092bc30d07..55cb74e35d 100644 --- a/theories/Reals/Rtrigo_alt.v +++ b/theories/Reals/Rtrigo_alt.v @@ -99,24 +99,22 @@ Proof. apply Rle_trans with 20. apply Rle_trans with 16. replace 16 with (Rsqr 4); [ idtac | ring_Rsqr ]. - replace (a * a) with (Rsqr a); [ idtac | reflexivity ]. apply Rsqr_incr_1. assumption. assumption. - left; prove_sup0. - rewrite <- (Rplus_0_r 16); replace 20 with (16 + 4); - [ apply Rplus_le_compat_l; left; prove_sup0 | ring ]. - rewrite <- (Rplus_comm 20); pattern 20 at 1; rewrite <- Rplus_0_r; - apply Rplus_le_compat_l. + now apply IZR_le. + now apply IZR_le. + rewrite <- (Rplus_0_l 20) at 1; + apply Rplus_le_compat_r. apply Rplus_le_le_0_compat. - repeat apply Rmult_le_pos. - left; prove_sup0. - left; prove_sup0. - replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ]. - replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ]. apply Rmult_le_pos. - left; prove_sup0. - replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ]. + apply Rmult_le_pos. + now apply IZR_le. + apply pos_INR. + apply pos_INR. + apply Rmult_le_pos. + now apply IZR_le. + apply pos_INR. apply INR_fact_neq_0. apply INR_fact_neq_0. simpl; ring. @@ -182,16 +180,14 @@ Proof. replace (- sum_f_R0 (tg_alt Un) (S (2 * n))) with (-1 * sum_f_R0 (tg_alt Un) (S (2 * n))); [ rewrite scal_sum | ring ]. apply sum_eq; intros; unfold sin_term, Un, tg_alt; - replace ((-1) ^ S i) with (-1 * (-1) ^ i). + change ((-1) ^ S i) with (-1 * (-1) ^ i). unfold Rdiv; ring. - reflexivity. replace (- sum_f_R0 (tg_alt Un) (2 * n)) with (-1 * sum_f_R0 (tg_alt Un) (2 * n)); [ rewrite scal_sum | ring ]. apply sum_eq; intros. unfold sin_term, Un, tg_alt; - replace ((-1) ^ S i) with (-1 * (-1) ^ i). + change ((-1) ^ S i) with (-1 * (-1) ^ i). unfold Rdiv; ring. - reflexivity. replace (2 * (n + 1))%nat with (S (S (2 * n))). reflexivity. ring. @@ -279,26 +275,23 @@ Proof. with (4 * INR n1 * INR n1 + 14 * INR n1 + 12); [ idtac | ring ]. apply Rle_trans with 12. apply Rle_trans with 4. - replace 4 with (Rsqr 2); [ idtac | ring_Rsqr ]. - replace (a0 * a0) with (Rsqr a0); [ idtac | reflexivity ]. + change 4 with (Rsqr 2). apply Rsqr_incr_1. assumption. - discrR. assumption. - left; prove_sup0. - pattern 4 at 1; rewrite <- Rplus_0_r; replace 12 with (4 + 8); - [ apply Rplus_le_compat_l; left; prove_sup0 | ring ]. - rewrite <- (Rplus_comm 12); pattern 12 at 1; rewrite <- Rplus_0_r; - apply Rplus_le_compat_l. + now apply IZR_le. + now apply IZR_le. + rewrite <- (Rplus_0_l 12) at 1; + apply Rplus_le_compat_r. apply Rplus_le_le_0_compat. - repeat apply Rmult_le_pos. - left; prove_sup0. - left; prove_sup0. - replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ]. - replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ]. apply Rmult_le_pos. - left; prove_sup0. - replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ]. + apply Rmult_le_pos. + now apply IZR_le. + apply pos_INR. + apply pos_INR. + apply Rmult_le_pos. + now apply IZR_le. + apply pos_INR. apply INR_fact_neq_0. apply INR_fact_neq_0. simpl; ring. @@ -351,15 +344,13 @@ Proof. replace (- sum_f_R0 (tg_alt Un) (S (2 * n0))) with (-1 * sum_f_R0 (tg_alt Un) (S (2 * n0))); [ rewrite scal_sum | ring ]. apply sum_eq; intros; unfold cos_term, Un, tg_alt; - replace ((-1) ^ S i) with (-1 * (-1) ^ i). + change ((-1) ^ S i) with (-1 * (-1) ^ i). unfold Rdiv; ring. - reflexivity. replace (- sum_f_R0 (tg_alt Un) (2 * n0)) with (-1 * sum_f_R0 (tg_alt Un) (2 * n0)); [ rewrite scal_sum | ring ]; apply sum_eq; intros; unfold cos_term, Un, tg_alt; - replace ((-1) ^ S i) with (-1 * (-1) ^ i). + change ((-1) ^ S i) with (-1 * (-1) ^ i). unfold Rdiv; ring. - reflexivity. replace (2 * (n0 + 1))%nat with (S (S (2 * n0))). reflexivity. ring. diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index 0d2a9a8bac..b46df202e2 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -157,7 +157,7 @@ Proof. apply Rinv_0_lt_compat; assumption. rewrite H3 in H0; assumption. apply lt_le_trans with 1%nat; [ apply lt_O_Sn | apply le_max_r ]. - apply le_IZR; replace (IZR 0) with 0; [ idtac | reflexivity ]; left; + apply le_IZR; left; apply Rlt_trans with (/ eps); [ apply Rinv_0_lt_compat; assumption | assumption ]. assert (H0 := archimed (/ eps)). @@ -194,30 +194,27 @@ Proof. elim H1; intros; assumption. apply lt_le_trans with (S n). unfold ge in H2; apply le_lt_n_Sm; assumption. - replace (2 * n + 1)%nat with (S (2 * n)); [ idtac | ring ]. + replace (2 * n + 1)%nat with (S (2 * n)) by ring. apply le_n_S; apply le_n_2n. apply Rmult_lt_reg_l with (INR (2 * S n)). apply lt_INR_0; replace (2 * S n)%nat with (S (S (2 * n))). apply lt_O_Sn. - replace (S n) with (n + 1)%nat; [ idtac | ring ]. + replace (S n) with (n + 1)%nat by ring. ring. rewrite <- Rinv_r_sym. - rewrite Rmult_1_r; replace 1 with (INR 1); [ apply lt_INR | reflexivity ]. + rewrite Rmult_1_r. + apply (lt_INR 1). replace (2 * S n)%nat with (S (S (2 * n))). apply lt_n_S; apply lt_O_Sn. - replace (S n) with (n + 1)%nat; [ ring | ring ]. + ring. apply not_O_INR; discriminate. apply not_O_INR; discriminate. replace (2 * n + 1)%nat with (S (2 * n)); [ apply not_O_INR; discriminate | ring ]. apply Rle_ge; left; apply Rinv_0_lt_compat. apply lt_INR_0. - replace (2 * S n * (2 * n + 1))%nat with (S (S (4 * (n * n) + 6 * n))). + replace (2 * S n * (2 * n + 1))%nat with (2 + (4 * (n * n) + 6 * n))%nat by ring. apply lt_O_Sn. - apply INR_eq. - repeat rewrite S_INR; rewrite plus_INR; repeat rewrite mult_INR; - rewrite plus_INR; rewrite mult_INR; repeat rewrite S_INR; - replace (INR 0) with 0; [ ring | reflexivity ]. Qed. Lemma cosn_no_R0 : forall n:nat, cos_n n <> 0. @@ -318,28 +315,25 @@ Proof. elim H1; intros; assumption. apply lt_le_trans with (S n). unfold ge in H2; apply le_lt_n_Sm; assumption. - replace (2 * S n + 1)%nat with (S (2 * S n)); [ idtac | ring ]. + replace (2 * S n + 1)%nat with (S (2 * S n)) by ring. apply le_S; apply le_n_2n. apply Rmult_lt_reg_l with (INR (2 * S n)). apply lt_INR_0; replace (2 * S n)%nat with (S (S (2 * n))); - [ apply lt_O_Sn | replace (S n) with (n + 1)%nat; [ idtac | ring ]; ring ]. + [ apply lt_O_Sn | ring ]. rewrite <- Rinv_r_sym. - rewrite Rmult_1_r; replace 1 with (INR 1); [ apply lt_INR | reflexivity ]. + rewrite Rmult_1_r. + apply (lt_INR 1). replace (2 * S n)%nat with (S (S (2 * n))). apply lt_n_S; apply lt_O_Sn. - replace (S n) with (n + 1)%nat; [ ring | ring ]. + ring. apply not_O_INR; discriminate. apply not_O_INR; discriminate. apply not_O_INR; discriminate. - left; change (0 < / INR ((2 * S n + 1) * (2 * S n))); - apply Rinv_0_lt_compat. + left; apply Rinv_0_lt_compat. apply lt_INR_0. replace ((2 * S n + 1) * (2 * S n))%nat with - (S (S (S (S (S (S (4 * (n * n) + 10 * n))))))). + (6 + (4 * (n * n) + 10 * n))%nat by ring. apply lt_O_Sn. - apply INR_eq; repeat rewrite S_INR; rewrite plus_INR; repeat rewrite mult_INR; - rewrite plus_INR; rewrite mult_INR; repeat rewrite S_INR; - replace (INR 0) with 0; [ ring | reflexivity ]. Qed. Lemma sin_no_R0 : forall n:nat, sin_n n <> 0. diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v index 5a2a07c42d..3697999f70 100644 --- a/theories/Reals/SeqProp.v +++ b/theories/Reals/SeqProp.v @@ -1167,7 +1167,7 @@ Proof. assert (H6 := archimed (Rabs x)); fold M in H6; elim H6; intros. rewrite H4 in H7; rewrite <- INR_IZR_INZ in H7. simpl in H7; elim (Rlt_irrefl _ (Rlt_trans _ _ _ H2 H7)). - replace 1 with (INR 1); [ apply le_INR | reflexivity ]; apply le_n_S; + apply (le_INR 1); apply le_n_S; apply le_O_n. apply le_IZR; simpl; left; apply Rlt_trans with (Rabs x). assumption. diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index 1f8b76cb62..c494517766 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -147,6 +147,16 @@ Definition shiftrepeat {A} := @rectS _ (fun n _ => t A (S (S n))) (fun h => h :: h :: []) (fun h _ _ H => h :: H). Global Arguments shiftrepeat {A} {n} v. +(** Take first [p] elements of a vector *) +Fixpoint take {A} {n} (p:nat) (le:p <= n) (v:t A n) : t A p := + match p as p return p <= n -> t A p with + | 0 => fun _ => [] + | S p' => match v in t _ n return S p' <= n -> t A (S p') with + | []=> fun le => False_rect _ (Nat.nle_succ_0 p' le) + | x::xs => fun le => x::take p' (le_S_n p' _ le) xs + end + end le. + (** Remove [p] last elements of a vector *) Lemma trunc : forall {A} {n} (p:nat), n > p -> t A n -> t A (n - p). diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v index c5278b918f..869d0fb5af 100644 --- a/theories/Vectors/VectorSpec.v +++ b/theories/Vectors/VectorSpec.v @@ -122,3 +122,32 @@ induction l. - reflexivity. - unfold to_list; simpl. now f_equal. Qed. + +Lemma take_O : forall {A} {n} le (v:t A n), take 0 le v = []. +Proof. + reflexivity. +Qed. + +Lemma take_idem : forall {A} p n (v:t A n) le le', + take p le' (take p le v) = take p le v. +Proof. + induction p; intros n v le le'. + - auto. + - destruct v. inversion le. simpl. apply f_equal. apply IHp. +Qed. + +Lemma take_app : forall {A} {n} (v:t A n) {m} (w:t A m) le, take n le (append v w) = v. +Proof. + induction v; intros m w le. + - reflexivity. + - simpl. apply f_equal. apply IHv. +Qed. + +(* Proof is irrelevant for [take] *) +Lemma take_prf_irr : forall {A} p {n} (v:t A n) le le', take p le v = take p le' v. +Proof. + induction p; intros n v le le'. + - reflexivity. + - destruct v. inversion le. simpl. apply f_equal. apply IHp. +Qed. + diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 06908abb6e..9917a49b42 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -266,9 +266,9 @@ let ensure_bname src tgt = let src, tgt = Filename.basename src, Filename.basename tgt in let src, tgt = chop_extension src, chop_extension tgt in if src <> tgt then begin - Feedback.msg_error (str "Source and target file names must coincide, directories can differ"); - Feedback.msg_error (str "Source: " ++ str src); - Feedback.msg_error (str "Target: " ++ str tgt); + Feedback.msg_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++ + str "Source: " ++ str src ++ fnl () ++ + str "Target: " ++ str tgt); flush_all (); exit 1 end diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 32e18a0149..ca03ba3f3a 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -67,8 +67,7 @@ let show_node () = could, possibly, be cleaned away. (Feb. 2010) *) () -let show_thesis () = - Feedback.msg_error (anomaly (Pp.str "TODO") ) +let show_thesis () = CErrors.anomaly (Pp.str "Show Thesis: TODO") let show_top_evars () = (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *) @@ -2210,6 +2209,11 @@ let with_fail b f = let interp ?(verbosely=true) ?proof (loc,c) = let orig_program_mode = Flags.is_program_mode () in let rec aux ?locality ?polymorphism isprogcmd = function + + (* This assert case will be removed when fake_ide can understand + completion feedback *) + | VernacStm _ -> assert false (* Done by Stm *) + | VernacProgram c when not isprogcmd -> aux ?locality ?polymorphism true c | VernacProgram _ -> CErrors.error "Program mode specified twice" | VernacLocal (b, c) when Option.is_empty locality -> @@ -2218,9 +2222,6 @@ let interp ?(verbosely=true) ?proof (loc,c) = aux ?locality ~polymorphism:b isprogcmd c | VernacPolymorphic (b, c) -> CErrors.error "Polymorphism specified twice" | VernacLocal _ -> CErrors.error "Locality specified twice" - | VernacStm (Command c) -> aux ?locality ?polymorphism isprogcmd c - | VernacStm (PGLast c) -> aux ?locality ?polymorphism isprogcmd c - | VernacStm _ -> assert false (* Done by Stm *) | VernacFail v -> with_fail true (fun () -> aux ?locality ?polymorphism isprogcmd v) | VernacTimeout (n,v) -> |