diff options
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | README.md | 8 | ||||
| -rw-r--r-- | TODO | 53 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 13 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_proofs.mli | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 5 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.mli | 5 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 14 | ||||
| -rw-r--r-- | plugins/funind/recdef.mli | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4306.v | 32 | ||||
| -rw-r--r-- | theories/Reals/DiscrR.v | 5 | ||||
| -rw-r--r-- | theories/Reals/RIneq.v | 11 | ||||
| -rw-r--r-- | theories/Reals/Ranalysis5.v | 16 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 12 | ||||
| -rw-r--r-- | vernac/topfmt.ml | 4 |
16 files changed, 91 insertions, 94 deletions
@@ -17,6 +17,7 @@ Tactics Most notably, the new implementation recognizes Miller patterns that were missed before because of a missing normalization step. Hopefully this should be fairly uncommon. +- "auto with real" can now discharge comparisons of literals Standard Library @@ -7,15 +7,17 @@ mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. ## Installation -See the file `INSTALL` for installation procedure. +Go to the [download page](https://coq.inria.fr/download) for Windows and MacOS packages; +read the [help page](https://coq.inria.fr/opam/www/using.html) on how to install Coq with OPAM; +or refer to the [`INSTALL` file](/INSTALL) for the procedure to install from source. ## Documentation The documentation is part of the archive in directory doc. The documentation of the last released version is available on the Coq -web site at [coq.inria.fr/doc](http://coq.inria.fr/doc). +web site at [coq.inria.fr/documentation](http://coq.inria.fr/documentation). ## Changes -There is a file named `CHANGES` that explains the differences and the +There is a file named [`CHANGES`](/CHANGES) that explains the differences and the incompatibilities since last versions. If you upgrade Coq, please read it carefully. @@ -1,53 +0,0 @@ -Langage: - -Distribution: - -Environnement: - -- Porter SearchIsos - -Noyau: - -Tactic: - -- Que contradiction raisonne a isomorphisme pres de False - -Vernac: - -- Print / Print Proof en fait identiques ; Print ne devrait pas afficher - les constantes opaques (devrait afficher qqchose comme <opaque>) - -Theories: - -- Rendre transparent tous les theoremes prouvant {A}+{B} -- Faire demarrer PolyList.nth a` l'indice 0 - Renommer l'actuel nth en nth1 ?? - -Doc: - -- Mettre à jour les messages d'erreurs de Discriminate/Simplify_eq/Injection -- Documenter le filtrage sur les types inductifs avec let-ins (dont la - compatibilite V6) - -- Ajouter let dans les règles du CIC - -> FAIT, mais reste a documenter le let dans les inductifs - et les champs manifestes dans les Record -- revoir le chapitre sur les tactiques utilisateur -- faut-il mieux spécifier la sémantique de Simpl (??) - -- Préciser la clarification syntaxique de IntroPattern -- preciser que Goal vient en dernier dans une clause pattern list et - qu'il doit apparaitre si il y a un "in" - -- Omega Time debranche mais Omega System et Omega Action remarchent ? -- Ajout "Replace in" (mais TODO) -- Syntaxe Conditional tac Rewrite marche, à documenter -- Documenter Dependent Rewrite et CutRewrite ? -- Ajouter les motifs sous-termes de ltac - -- ajouter doc de GenFixpoint (mais avant: changer syntaxe) (J. Forest ou Pierre C.) -- mettre à jour la doc de induction (arguments multiples) (Pierre C.) -- mettre à jour la doc de functional induction/scheme (J. Forest ou Pierre C.) ---> mettre à jour le CHANGES (vers la ligne 72) - - diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 48c0f5f04c..8dae17d69e 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -299,7 +299,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = Can be safely replaced by the next comment for Ocaml >= 3.08.4 *) let sub = Int.Map.bindings sub in - List.fold_left (fun end_of_type (i,t) -> lift 1 (substnl [t] (i-1) end_of_type)) + List.fold_left (fun end_of_type (i,t) -> liftn 1 i (substnl [t] (i-1) end_of_type)) end_of_type_with_pop sub in @@ -1401,8 +1401,8 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let prove_with_tcc tcc_lemma_constr eqs : tactic = match !tcc_lemma_constr with - | None -> anomaly (Pp.str "No tcc proof !!") - | Some lemma -> + | Undefined -> anomaly (Pp.str "No tcc proof !!") + | Value lemma -> fun gls -> (* let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in *) (* let ids = hid::pf_ids_of_hyps gls in *) @@ -1420,7 +1420,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic = Proofview.V82.of_tactic (Eauto.gen_eauto (false,5) [] (Some [])) ] gls - + | Not_needed -> tclIDTAC let backtrack_eqs_until_hrec hrec eqs : tactic = fun gls -> @@ -1599,8 +1599,9 @@ let prove_principle_for_gen let args_ids = List.map (get_name %> Nameops.out_name) princ_info.args in let lemma = match !tcc_lemma_ref with - | None -> error "No tcc proof !!" - | Some lemma -> EConstr.of_constr lemma + | Undefined -> error "No tcc proof !!" + | Value lemma -> EConstr.of_constr lemma + | Not_needed -> EConstr.of_constr (Coqlib.build_coq_I ()) in (* let rec list_diff del_list check_list = *) (* match del_list with *) diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli index 769d726d70..7ddc84d015 100644 --- a/plugins/funind/functional_principles_proofs.mli +++ b/plugins/funind/functional_principles_proofs.mli @@ -9,7 +9,7 @@ val prove_princ_for_struct : val prove_principle_for_gen : constant*constant*constant -> (* name of the function, the functional and the fixpoint equation *) - constr option ref -> (* a pointer to the obligation proofs lemma *) + Indfun_common.tcc_lemma_value ref -> (* a pointer to the obligation proofs lemma *) bool -> (* is that function uses measure *) int -> (* the number of recursive argument *) EConstr.types -> (* the type of the recursive argument *) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 20da12f395..7b0d7d27d7 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -543,3 +543,8 @@ let prodn n env b = (* compose_prod [xn:Tn;..;x1:T1] b = (x1:T1)..(xn:Tn)b *) let compose_prod l b = prodn (List.length l) l b + +type tcc_lemma_value = + | Undefined + | Value of Constr.constr + | Not_needed diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 5c3e73e9d7..5ef8f05bb7 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -119,3 +119,8 @@ val decompose_lam_n : Evd.evar_map -> int -> EConstr.t -> (Names.Name.t * EConstr.t) list * EConstr.t val compose_lam : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t val compose_prod : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t + +type tcc_lemma_value = + | Undefined + | Value of Constr.constr + | Not_needed diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 5460d6fb73..26ba5ef40e 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -45,12 +45,6 @@ open Indfun_common open Sigma.Notations open Context.Rel.Declaration -let local_assum (na, t) = - LocalAssum (na, EConstr.Unsafe.to_constr t) - -let local_def (na, b, t) = - LocalDef (na, EConstr.Unsafe.to_constr b, EConstr.Unsafe.to_constr t) - (* Ugly things which should not be here *) let coq_constant m s = @@ -1323,7 +1317,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp | _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant") in let lemma = mkConst (Names.Constant.make1 (Lib.make_kn na)) in - ref_ := Some (EConstr.Unsafe.to_constr lemma); + ref_ := Value (EConstr.Unsafe.to_constr lemma); let lid = ref [] in let h_num = ref (-1) in let env = Global.env () in @@ -1411,7 +1405,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp let com_terminate tcc_lemma_name - (tcc_lemma_ref : Constr.t option ref) + tcc_lemma_ref is_mes fonctional_ref input_type @@ -1440,6 +1434,7 @@ let com_terminate (new_goal_type); with Failure "empty list of subgoals!" -> (* a non recursive function declared with measure ! *) + tcc_lemma_ref := Not_needed; defined () @@ -1515,7 +1510,6 @@ let (com_eqn : int -> Id.t -> (* Pp.msgnl (str "eqn finished"); *) );; - let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq generate_induction_principle using_lemmas : unit = let open Term in @@ -1561,7 +1555,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num in let evm = Evd.from_ctx evuctx in let tcc_lemma_name = add_suffix function_name "_tcc" in - let tcc_lemma_constr = ref None in + let tcc_lemma_constr = ref Undefined in (* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) let hook _ _ = let term_ref = Nametab.locate (qualid_of_ident term_id) in diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index 9c1081b9d2..80f02e01c4 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -13,7 +13,7 @@ bool -> Constrexpr.constr_expr -> Constrexpr.constr_expr -> int -> Constrexpr.constr_expr -> (Term.pconstant -> - Term.constr option ref -> + Indfun_common.tcc_lemma_value ref -> Term.pconstant -> Term.pconstant -> int -> EConstr.types -> int -> EConstr.constr -> 'a) -> Constrexpr.constr_expr list -> unit diff --git a/test-suite/bugs/closed/4306.v b/test-suite/bugs/closed/4306.v new file mode 100644 index 0000000000..4aef5bb95e --- /dev/null +++ b/test-suite/bugs/closed/4306.v @@ -0,0 +1,32 @@ +Require Import List. +Require Import Arith. +Require Import Recdef. +Require Import Omega. + +Function foo (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat := + match xys with + | (nil, _) => snd xys + | (_, nil) => fst xys + | (x :: xs', y :: ys') => match Compare_dec.nat_compare x y with + | Lt => x :: foo (xs', y :: ys') + | Eq => x :: foo (xs', ys') + | Gt => y :: foo (x :: xs', ys') + end + end. +Proof. + intros; simpl; omega. + intros; simpl; omega. + intros; simpl; omega. +Qed. + +Function bar (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat := + let (xs, ys) := xys in + match (xs, ys) with + | (nil, _) => ys + | (_, nil) => xs + | (x :: xs', y :: ys') => match Compare_dec.nat_compare x y with + | Lt => x :: foo (xs', ys) + | Eq => x :: foo (xs', ys') + | Gt => y :: foo (xs, ys') + end + end.
\ No newline at end of file diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v index 05911cd539..7f26c1b86f 100644 --- a/theories/Reals/DiscrR.v +++ b/theories/Reals/DiscrR.v @@ -22,11 +22,6 @@ Proof. intros; rewrite H; reflexivity. Qed. -Lemma IZR_neq : forall z1 z2:Z, z1 <> z2 -> IZR z1 <> IZR z2. -Proof. -intros; red; intro; elim H; apply eq_IZR; assumption. -Qed. - Ltac discrR := try match goal with diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 7e1cc3e036..711703ad70 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -1926,6 +1926,17 @@ Proof. omega. Qed. +Lemma IZR_neq : forall z1 z2:Z, z1 <> z2 -> IZR z1 <> IZR z2. +Proof. +intros; red; intro; elim H; apply eq_IZR; assumption. +Qed. + +Hint Extern 0 (IZR _ <= IZR _) => apply IZR_le, Zle_bool_imp_le, eq_refl : real. +Hint Extern 0 (IZR _ >= IZR _) => apply Rle_ge, IZR_le, Zle_bool_imp_le, eq_refl : real. +Hint Extern 0 (IZR _ < IZR _) => apply IZR_lt, eq_refl : real. +Hint Extern 0 (IZR _ > IZR _) => apply IZR_lt, eq_refl : real. +Hint Extern 0 (IZR _ <> IZR _) => apply IZR_neq, Zeq_bool_neq, eq_refl : real. + Lemma one_IZR_lt1 : forall n:Z, -1 < IZR n < 1 -> n = 0%Z. Proof. intros z [H1 H2]. diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v index f9da88aad4..ccb4207ba0 100644 --- a/theories/Reals/Ranalysis5.v +++ b/theories/Reals/Ranalysis5.v @@ -15,6 +15,7 @@ Require Import RiemannInt. Require Import SeqProp. Require Import Max. Require Import Omega. +Require Import Lra. Local Open Scope R_scope. (** * Preliminaries lemmas *) @@ -245,14 +246,8 @@ Lemma IVT_interv_prelim0 : forall (x y:R) (P:R->bool) (N:nat), x <= Dichotomy_ub x y P N <= y /\ x <= Dichotomy_lb x y P N <= y. Proof. assert (Sublemma : forall x y lb ub, lb <= x <= ub /\ lb <= y <= ub -> lb <= (x+y) / 2 <= ub). - intros x y lb ub Hyp. - split. - replace lb with ((lb + lb) * /2) by field. - unfold Rdiv ; apply Rmult_le_compat_r ; intuition. - now apply Rlt_le, Rinv_0_lt_compat, IZR_lt. - replace ub with ((ub + ub) * /2) by field. - unfold Rdiv ; apply Rmult_le_compat_r ; intuition. - now apply Rlt_le, Rinv_0_lt_compat, IZR_lt. + intros x y lb ub Hyp. + lra. intros x y P N x_lt_y. induction N. simpl ; intuition. @@ -1029,10 +1024,7 @@ Qed. Lemma ub_lt_2_pos : forall x ub lb, lb < x -> x < ub -> 0 < (ub-lb)/2. Proof. intros x ub lb lb_lt_x x_lt_ub. - assert (T : 0 < ub - lb). - fourier. - unfold Rdiv ; apply Rlt_mult_inv_pos ; intuition. -now apply IZR_lt. +lra. Qed. Definition mkposreal_lb_ub (x lb ub:R) (lb_lt_x:lb<x) (x_lt_ub:x<ub) : posreal. diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c259beb17b..a4dcefcbde 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -649,7 +649,7 @@ let init_toplevel arglist = let any = CErrors.push any in flush_all(); let msg = - if !batch_mode then mt () + if !batch_mode && not Stateid.(equal (Stm.get_current_state ()) dummy) then mt () else str "Error during initialization: " ++ CErrors.iprint any ++ fnl () in let is_anomaly e = CErrors.is_anomaly e || not (CErrors.handled e) in diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 18f93197c1..84330b88ac 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -162,7 +162,17 @@ and load_vernac verbosely sid file = (* we go out of the following infinite loop when a End_of_input is * raised, which means that we raised the end of the file being loaded *) while true do - let loc, ast = Stm.parse_sentence !rsid in_pa in + let loc, ast = + try Stm.parse_sentence !rsid in_pa + with + | Stm.End_of_input -> raise Stm.End_of_input + | any -> + let (e, info) = CErrors.push any in + let loc = Loc.get_loc info in + let msg = CErrors.iprint (e, info) in + Feedback.msg_error ?loc msg; + iraise (e, info) + in (* Printing of vernacs *) if !beautify then pr_new_syntax in_pa chan_beautify loc (Some ast); diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index ee55366927..a4acd3f24e 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -141,11 +141,13 @@ let ann_hdr = tag Tag.error (str "Anomaly:") ++ spc () let make_body quoter info ?pre_hdr s = pr_opt_no_spc (fun x -> x ++ fnl ()) pre_hdr ++ quoter (hov 0 (info ++ s)) +(* The empty quoter *) +let noq x = x (* Generic logger *) let gen_logger dbg err ?pre_hdr level msg = match level with | Debug -> msgnl_with !std_ft (make_body dbg dbg_hdr ?pre_hdr msg) | Info -> msgnl_with !std_ft (make_body dbg info_hdr ?pre_hdr msg) - | Notice -> msgnl_with !std_ft (make_body dbg info_hdr ?pre_hdr msg) + | Notice -> msgnl_with !std_ft (make_body noq info_hdr ?pre_hdr msg) | Warning -> Flags.if_warn (fun () -> msgnl_with !err_ft (make_body err warn_hdr ?pre_hdr msg)) () | Error -> msgnl_with !err_ft (make_body err err_hdr ?pre_hdr msg) |