diff options
46 files changed, 715 insertions, 599 deletions
diff --git a/Makefile.doc b/Makefile.doc index a5ff8e0123..e9bc03565d 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -101,7 +101,7 @@ full-stdlib: \ doc/stdlib/html/index.html doc/stdlib/FullLibrary.ps doc/stdlib/FullLibrary.pdf sphinx-clean: - rm -rf $(SPHINXBUILDDIR) + rm -rf $(SPHINXBUILDDIR) doc/sphinx/index.rst doc/sphinx/zebibliography.rst .PHONY: plugin-tutorial plugin-tutorial: states tools diff --git a/Makefile.ide b/Makefile.ide index 9964a474f8..54bf0b6a4e 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -298,7 +298,7 @@ $(COQIDEAPP):$(COQIDEAPP)/Contents/Resources ########################################################################### # This is either x86_64-w64-mingw32 or i686-w64-mingw32 -TARGET_ARCH=$(shell $CC -dumpmachine) +TARGET_ARCH=$(shell $(CC) -dumpmachine) %.o: %.rc $(SHOW)'WINDRES $<' diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index ebbf10f548..beed8bc443 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -949,7 +949,7 @@ function make_arch_pkg_config { ##### OCAML ##### function make_ocaml { - if build_prep https://github.com/ocaml/ocaml/archive 4.08.1 tar.gz 1 ocaml-4.08.1 ; then + if build_prep https://github.com/ocaml/ocaml/archive 4.10.2 tar.gz 1 ocaml-4.10.2 ; then # see https://github.com/ocaml/ocaml/blob/4.08/README.win32.adoc # get flexdll sources into folder ./flexdll @@ -1047,8 +1047,7 @@ function make_ocamlbuild { function make_findlib { make_ocaml make_ocamlbuild - # Note: latest is 1.8.1 but http://projects.camlcity.org/projects/dl/findlib-1.8.1/doc/README says this is for OCaml 4.09 - if build_prep https://opam.ocaml.org/1.2.2/archives ocamlfind.1.8.0+opam tar.gz 1 ; then + if build_prep http://download.camlcity.org/download/ findlib-1.8.1 tar.gz 1; then logn configure ./configure -bindir "$PREFIXOCAML\\bin" -sitelib "$PREFIXOCAML\\libocaml\\site-lib" -config "$PREFIXOCAML\\etc\\findlib.conf" # Note: findlib doesn't support -j 8, so don't pass MAKE_OPT log2 make all @@ -1153,7 +1152,7 @@ function make_lablgtk { make_gtk_sourceview3 make_ocaml_cairo2 - if build_prep https://github.com/garrigue/lablgtk/archive 3.0.beta5 tar.gz 1 lablgtk-3.0.beta5 ; then + if build_prep https://github.com/garrigue/lablgtk/archive 3.1.1 tar.gz 1 lablgtk-3.1.1 ; then make_arch_pkg_config # lablgtk3 includes more packages that are not relevant for Coq, @@ -1436,12 +1435,12 @@ function make_coq { # make clean # Copy these files somewhere the plugin builds can find them - logn copy-basic-overlays cp dev/ci/ci-basic-overlay.sh /build/ + #logn copy-basic-overlays cp dev/ci/ci-basic-overlay.sh /build/ build_post fi - load_overlay_data + #load_overlay_data } ##### GNU Make for MinGW ##### diff --git a/doc/sphinx/proofs/writing-proofs/index.rst b/doc/sphinx/proofs/writing-proofs/index.rst index 7724d7433c..63ddbd0a3a 100644 --- a/doc/sphinx/proofs/writing-proofs/index.rst +++ b/doc/sphinx/proofs/writing-proofs/index.rst @@ -10,19 +10,16 @@ the user and the assistant. The building blocks for this dialog are tactics which the user will use to represent steps in the proof of a theorem. -Incomplete proofs have one or more open (unproven) sub-goals. Each -goal has its own context (a set of assumptions that can be used to -prove the goal). Tactics can transform goals and contexts. -Internally, the incomplete proof is represented as a partial proof -term, with holes for the unproven sub-goals. +The first section presents the proof mode (the core mechanism of the +dialog between the user and the proof assistant). Then, several +sections describe the available tactics. One section covers the +SSReflect proof language, which provides a consistent alternative set +of tactics to the standard basic tactics. The last section documents +the ``Scheme`` family of commands, which can be used to extend the +power of the :tacn:`induction` and :tacn:`inversion` tactics. -When a proof is complete, the user leaves the proof mode and defers -the verification of the resulting proof term to the :ref:`kernel -<core-language>`. - -This chapter is divided in several parts, describing the basic ideas -of the proof mode (during which tactics can be used), and several -flavors of tactics, including the SSReflect proof language. +Additional tactics are documented in the next chapter +:ref:`automatic-tactics`. .. toctree:: :maxdepth: 1 diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index a482e044d8..cc9e1bb31d 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -175,7 +175,21 @@ let rec remove_grammars n = camlp5_entries := EntryDataMap.add tag (EntryData.Ex entries) !camlp5_entries; remove_grammars (n - 1) -(* Parse a string, does NOT check if the entire string was read *) +let make_rule r = [None, None, r] + +(** An entry that checks we reached the end of the input. *) + +(* used by the Tactician plugin *) +let eoi_entry en = + let e = Entry.make ((Entry.name en) ^ "_eoi") in + let symbs = Rule.next (Rule.next Rule.stop (Symbol.nterm en)) (Symbol.token Tok.PEOI) in + let act = fun _ x loc -> x in + let ext = { pos = None; data = make_rule [Production.make symbs act] } in + safe_extend e ext; + e + +(* Parse a string, does NOT check if the entire string was read + (use eoi_entry) *) let parse_string f ?loc x = let strm = Stream.of_string x in @@ -289,6 +303,7 @@ module Constr = let constr = Entry.create "constr" let term = Entry.create "term" let operconstr = term + let constr_eoi = eoi_entry constr let lconstr = Entry.create "lconstr" let binder_constr = Entry.create "binder_constr" let ident = Entry.create "ident" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 8bff5cfd94..06d05a4797 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -120,6 +120,7 @@ end (** Parse a string *) val parse_string : 'a Entry.t -> ?loc:Loc.t -> string -> 'a +val eoi_entry : 'a Entry.t -> 'a Entry.t type gram_universe [@@deprecated "Deprecated in 8.13"] [@@@ocaml.warning "-3"] @@ -180,6 +181,7 @@ module Prim : module Constr : sig val constr : constr_expr Entry.t + val constr_eoi : constr_expr Entry.t val lconstr : constr_expr Entry.t val binder_constr : constr_expr Entry.t val term : constr_expr Entry.t diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml index 80c13a3698..196a68e67c 100644 --- a/plugins/ltac/pltac.ml +++ b/plugins/ltac/pltac.ml @@ -47,6 +47,8 @@ let binder_tactic = Entry.create "binder_tactic" let tactic = Entry.create "tactic" (* Main entry for quotations *) +let tactic_eoi = eoi_entry tactic + let () = let open Stdarg in let open Tacarg in diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index 73bce84d18..c0bf6b9f76 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -40,3 +40,4 @@ val tactic_expr : raw_tactic_expr Entry.t [@@deprecated "Deprecated in 8.13; use 'ltac_expr' instead"] val binder_tactic : raw_tactic_expr Entry.t val tactic : raw_tactic_expr Entry.t +val tactic_eoi : raw_tactic_expr Entry.t diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index f6a741f468..5fbabd7ca1 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -46,7 +46,11 @@ type ssrclear = ssrhyps type ssrdocc = ssrclear option * ssrocc (* OLD ssr terms *) -type ssrtermkind = char (* FIXME, make algebraic *) +(* terms are pre constr, the kind is a parsing/printing flag to distinguish + * between x, @x and (x). It affects automatic clear and let-in preservation. *) +(* FIXME *) +(* Cpattern is a temporary flag that becomes InParens ASAP. *) +type ssrtermkind = Ssrmatching_plugin.Ssrmatching.ssrtermkind type ssrterm = ssrtermkind * Genintern.glob_constr_and_expr (* NEW ssr term *) diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml index 61643c2aa3..37eba7d399 100644 --- a/plugins/ssr/ssrbwd.ml +++ b/plugins/ssr/ssrbwd.ml @@ -19,30 +19,21 @@ open Ssrmatching_plugin open Ssrmatching open Ssrast -open Ssrprinters open Ssrcommon -let char_to_kind = function - | '(' -> xInParens - | '@' -> xWithAt - | ' ' -> xNoFlag - | 'x' -> xCpattern - | _ -> assert false - (** Backward chaining tactics: apply, exact, congr. *) (** The "apply" tactic *) let interp_agen ist gl ((goclr, _), (k, gc as c)) (clr, rcs) = (* ppdebug(lazy(str"sigma@interp_agen=" ++ pr_evar_map None (project gl))); *) - let k = char_to_kind k in let rc = pf_intern_term ist gl c in let rcs' = rc :: rcs in match goclr with | None -> clr, rcs' | Some ghyps -> let clr' = snd (interp_hyps ist gl ghyps) @ clr in - if k <> xNoFlag then clr', rcs' else + if k <> NoFlag then clr', rcs' else let loc = rc.CAst.loc in match DAst.get rc with | GVar id when not_section_id id -> SsrHyp (Loc.tag ?loc id) :: clr', rcs' @@ -132,7 +123,7 @@ let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic ~nf_evars: let vtac gv i gl' = refine_interp_apply_view i ist gl' gv in let ggenl, tclGENTAC = if gviews <> [] && ggenl <> [] then - let ggenl= List.map (fun (x,g) -> x, cpattern_of_term g ist) (List.hd ggenl) in + let ggenl= List.map (fun (x,(k,p)) -> x, {kind=k; pattern=p; interpretation= Some ist}) (List.hd ggenl) in [], Tacticals.tclTHEN (Proofview.V82.of_tactic (genstac (ggenl,[]))) else ggenl, Tacticals.tclTHEN Tacticals.tclIDTAC in tclGENTAC (fun gl -> diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index cd219838d5..4d57abb465 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -290,7 +290,7 @@ let interp_hyps ist gl ghyps = (* Old terms *) let mk_term k c = k, (mkRHole, Some c) -let mk_lterm c = mk_term xNoFlag c +let mk_lterm c = mk_term NoFlag c (* New terms *) @@ -318,9 +318,9 @@ let interp_ast_closure_term (ist : Geninterp.interp_sign) (gl : 'goal Evd.sigma) let ssrterm_of_ast_closure_term { body; annotation } = let c = match annotation with - | `Parens -> xInParens - | `At -> xWithAt - | _ -> xNoFlag in + | `Parens -> InParens + | `At -> WithAt + | _ -> NoFlag in mk_term c body let ssrdgens_of_parsed_dgens = function @@ -926,7 +926,7 @@ let pf_interp_ty ?(resolve_typeclasses=false) env sigma0 ist ty = CProdN (abs, force_type t) | CLetIn (n, v, oty, t) -> incr n_binders; CLetIn (n, v, oty, force_type t) | _ -> (mkCCast ty (mkCType None)).v)) ty in - mk_term ' ' (force_type ty) in + mk_term NoFlag (force_type ty) in let strip_cast (sigma, t) = let open EConstr in let rec aux t = match kind_of_type sigma t with @@ -1099,7 +1099,7 @@ let hyp_of_var sigma v = SsrHyp (Loc.tag @@ EConstr.destVar sigma v) let interp_clr sigma = function | Some clr, (k, c) - when (k = xNoFlag || k = xWithAt) && is_pf_var sigma c -> + when (k = NoFlag || k = WithAt) && is_pf_var sigma c -> hyp_of_var sigma c :: clr | Some clr, _ -> clr | None, _ -> [] @@ -1167,7 +1167,7 @@ let pf_interp_gen_aux gl to_ind ((oclr, occ), t) = let cl = EConstr.of_constr cl in let clr = interp_clr sigma (oclr, (tag_of_cpattern t, c)) in if not(occur_existential sigma c) then - if tag_of_cpattern t = xWithAt then + if tag_of_cpattern t = WithAt then if not (EConstr.isVar sigma c) then errorstrm (str "@ can be used with variables only") else match Tacmach.pf_get_hyp gl (EConstr.destVar sigma c) with diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index fdfba48024..aeb6b3cf85 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -232,7 +232,7 @@ let rec get_evalref env sigma c = match EConstr.kind sigma c with (* Strip a pattern generated by a prenex implicit to its constant. *) let strip_unfold_term _ ((sigma, t) as p) kt = match EConstr.kind sigma t with - | App (f, a) when kt = xNoFlag && Array.for_all (EConstr.isEvar sigma) a && EConstr.isConst sigma f -> + | App (f, a) when kt = NoFlag && Array.for_all (EConstr.isEvar sigma) a && EConstr.isConst sigma f -> (sigma, f), true | Const _ | Var _ -> p, true | Proj _ -> p, true @@ -736,7 +736,7 @@ let unlocktac ist args = Ssrcommon.tacMK_SSR_CONST "locked" >>= fun locked -> Ssrcommon.tacMK_SSR_CONST "master_key" >>= fun key -> let ktacs = [ - (Proofview.tclEVARMAP >>= fun sigma -> unfoldtac None None (sigma, locked) xInParens); + (Proofview.tclEVARMAP >>= fun sigma -> unfoldtac None None (sigma, locked) InParens); Ssrelim.casetac key (fun ?seed:_ k -> k) ] in Tacticals.New.tclTHENLIST (List.map utac args @ ktacs) diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 4961138190..f2c7f495b3 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -143,8 +143,8 @@ let havetac ist let gl, _ = pf_e_type_of gl idty in pf_unify_HO gl args_id.(2) abstract_key in Tacticals.tclTHENFIRST (Proofview.V82.of_tactic itac_mkabs) (fun gl -> - let mkt t = mk_term xNoFlag t in - let mkl t = (xNoFlag, (t, None)) in + let mkt t = mk_term NoFlag t in + let mkl t = (NoFlag, (t, None)) in let interp gl rtc t = pf_abs_ssrterm ~resolve_typeclasses:rtc ist gl t in let interp_ty gl rtc t = let a,b,_,u = pf_interp_ty ~resolve_typeclasses:rtc (pf_env gl) (project gl) ist t in a,b,u in diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 46f90a7ee1..1e940b5ad3 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -741,7 +741,7 @@ let tclLAST_GEN ~to_ind ((oclr, occ), t) conclusion = tclINDEPENDENTL begin [A.. -> Ind] and opens new goals for [A..] as well as for the branches of [Ind], see the [~to_ind] argument *) if not(Termops.occur_existential sigma c) then - if Ssrmatching.tag_of_cpattern t = Ssrprinters.xWithAt then + if Ssrmatching.tag_of_cpattern t = Ssrmatching.WithAt then if not (EConstr.isVar sigma c) then Ssrcommon.errorstrm Pp.(str "@ can be used with variables only") else match Context.Named.lookup (EConstr.destVar sigma c) hyps with diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index f06b460ee9..935cef58b9 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -38,6 +38,8 @@ open Constrexpr_ops open Proofview open Proofview.Notations +open Ssrmatching_plugin.Ssrmatching + open Ssrprinters open Ssrcommon open Ssrtacticals @@ -455,9 +457,9 @@ END (* Old kinds of terms *) let input_ssrtermkind _ strm = match Util.stream_nth 0 strm with - | Tok.KEYWORD "(" -> xInParens - | Tok.KEYWORD "@" -> xWithAt - | _ -> xNoFlag + | Tok.KEYWORD "(" -> InParens + | Tok.KEYWORD "@" -> WithAt + | _ -> NoFlag let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind @@ -554,9 +556,9 @@ END GRAMMAR EXTEND Gram GLOBAL: ssrbwdview; ssrbwdview: [ - [ test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr -> { [mk_term xNoFlag c] } + [ test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr -> { [mk_term NoFlag c] } | test_not_ssrslashnum; "/"; c = Pcoq.Constr.constr; w = ssrbwdview -> { - (mk_term xNoFlag c) :: w } ]]; + (mk_term NoFlag c) :: w } ]]; END (* New Views *) @@ -2201,10 +2203,10 @@ let pr_ssrcongrarg _ _ _ ((n, f), dgens) = ARGUMENT EXTEND ssrcongrarg TYPED AS ((int * ssrterm) * ssrdgens) PRINTED BY { pr_ssrcongrarg } -| [ natural(n) constr(c) ssrdgens(dgens) ] -> { (n, mk_term xNoFlag c), dgens } -| [ natural(n) constr(c) ] -> { (n, mk_term xNoFlag c),([[]],[]) } -| [ constr(c) ssrdgens(dgens) ] -> { (0, mk_term xNoFlag c), dgens } -| [ constr(c) ] -> { (0, mk_term xNoFlag c), ([[]],[]) } +| [ natural(n) constr(c) ssrdgens(dgens) ] -> { (n, mk_term NoFlag c), dgens } +| [ natural(n) constr(c) ] -> { (n, mk_term NoFlag c),([[]],[]) } +| [ constr(c) ssrdgens(dgens) ] -> { (0, mk_term NoFlag c), dgens } +| [ constr(c) ] -> { (0, mk_term NoFlag c), ([[]],[]) } END @@ -2260,7 +2262,7 @@ let pr_rule = function let pr_ssrrule _ _ _ = pr_rule -let noruleterm loc = mk_term xNoFlag (mkCProp loc) +let noruleterm loc = mk_term NoFlag (mkCProp loc) } diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index 95c8024e89..6ed68094dc 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -28,16 +28,6 @@ let pp_concat hd ?(sep=str", ") = function [] -> hd | x :: xs -> let pp_term gl t = let t = Reductionops.nf_evar (project gl) t in pr_econstr_env (pf_env gl) (project gl) t -(* FIXME *) -(* terms are pre constr, the kind is parsing/printing flag to distinguish - * between x, @x and (x). It affects automatic clear and let-in preservation. - * Cpattern is a temporary flag that becomes InParens ASAP. *) -(* type ssrtermkind = InParens | WithAt | NoFlag | Cpattern *) -let xInParens = '(' -let xWithAt = '@' -let xNoFlag = ' ' -let xCpattern = 'x' - (* Term printing utilities functions for deciding bracketing. *) let pr_paren prx x = hov 1 (str "(" ++ prx x ++ str ")") (* String lexing utilities *) @@ -45,10 +35,10 @@ let skip_wschars s = let rec loop i = match s.[i] with '\n'..' ' -> loop (i + 1) | _ -> i in loop (* We also guard characters that might interfere with the ssreflect *) (* tactic syntax. *) -let guard_term ch1 s i = match s.[i] with +let guard_term kind s i = match s.[i] with | '(' -> false | '{' | '/' | '=' -> true - | _ -> ch1 = xInParens + | _ -> kind = Ssrmatching_plugin.Ssrmatching.InParens (* We also guard characters that might interfere with the ssreflect *) (* tactic syntax. *) diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli index 87eb05b667..21fb28038a 100644 --- a/plugins/ssr/ssrprinters.mli +++ b/plugins/ssr/ssrprinters.mli @@ -24,11 +24,6 @@ val pp_concat : Pp.t -> ?sep:Pp.t -> Pp.t list -> Pp.t -val xInParens : ssrtermkind -val xWithAt : ssrtermkind -val xNoFlag : ssrtermkind -val xCpattern : ssrtermkind - val pr_clear : (unit -> Pp.t) -> ssrclear -> Pp.t val pr_clear_ne : ssrclear -> Pp.t val pr_dir : ssrdir -> Pp.t diff --git a/plugins/ssrmatching/g_ssrmatching.mlg b/plugins/ssrmatching/g_ssrmatching.mlg index 2252435658..7022949ab6 100644 --- a/plugins/ssrmatching/g_ssrmatching.mlg +++ b/plugins/ssrmatching/g_ssrmatching.mlg @@ -67,9 +67,9 @@ END { let input_ssrtermkind _ strm = match Util.stream_nth 0 strm with - | Tok.KEYWORD "(" -> '(' - | Tok.KEYWORD "@" -> '@' - | _ -> ' ' + | Tok.KEYWORD "(" -> InParens + | Tok.KEYWORD "@" -> WithAt + | _ -> NoFlag let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind } @@ -78,8 +78,8 @@ GRAMMAR EXTEND Gram GLOBAL: cpattern; cpattern: [[ k = ssrtermkind; c = constr -> { let pattern = mk_term k c None in - if loc_of_cpattern pattern <> Some loc && k = '(' - then mk_term 'x' c None + if loc_of_cpattern pattern <> Some loc && k = InParens + then mk_term Cpattern c None else pattern } ]]; END @@ -97,8 +97,8 @@ GRAMMAR EXTEND Gram GLOBAL: lcpattern; lcpattern: [[ k = ssrtermkind; c = lconstr -> { let pattern = mk_term k c None in - if loc_of_cpattern pattern <> Some loc && k = '(' - then mk_term 'x' c None + if loc_of_cpattern pattern <> Some loc && k = InParens + then mk_term Cpattern c None else pattern } ]]; END diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index ea014250ca..2a21049c6e 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -37,6 +37,8 @@ open Evar_kinds open Constrexpr open Constrexpr_ops +type ssrtermkind = | InParens | WithAt | NoFlag | Cpattern + let errorstrm = CErrors.user_err ~hdr:"ssrmatching" let loc_error loc msg = CErrors.user_err ?loc ~hdr:msg (str msg) let ppnl = Feedback.msg_info @@ -78,10 +80,10 @@ let skip_wschars s = let rec loop i = match s.[i] with '\n'..' ' -> loop (i + 1) | _ -> i in loop (* We also guard characters that might interfere with the ssreflect *) (* tactic syntax. *) -let guard_term ch1 s i = match s.[i] with +let guard_term kind s i = match s.[i] with | '(' -> false | '{' | '/' | '=' -> true - | _ -> ch1 = '(' + | _ -> kind = InParens (* The call 'guard s i' should return true if the contents of s *) (* starting at i need bracketing to avoid ambiguities. *) let pr_guarded guard prc c = @@ -102,14 +104,6 @@ let prl_glob_constr_and_expr env sigma = function let pr_glob_constr_and_expr env sigma = function | _, Some c -> pr_constr_expr env sigma c | c, None -> pr_glob_constr c -let pr_term (k, c, _) = - let env = Global.env () in - let sigma = Evd.from_env env in - pr_guarded (guard_term k) (pr_glob_constr_and_expr env sigma) c -let prl_term (k, c, _) = - let env = Global.env () in - let sigma = Evd.from_env env in - pr_guarded (guard_term k) (prl_glob_constr_and_expr env sigma) c (** Adding a new uninterpreted generic argument type *) let add_genarg tag pr = @@ -153,28 +147,6 @@ let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args) let mkRCast rc rt = DAst.make @@ GCast (rc, dC rt) let mkRLambda n s t = DAst.make @@ GLambda (n, Explicit, s, t) -(* ssrterm conbinators *) -let combineCG t1 t2 f g = - let mk_ist i1 i2 = match i1, i2 with - | None, Some i -> Some i - | Some i, None -> Some i - | None, None -> None - | Some i, Some j when i == j -> Some i - | _ -> CErrors.anomaly (Pp.str "combineCG: different ist") in - match t1, t2 with - | (x, (t1, None), i1), (_, (t2, None), i2) -> - x, (g t1 t2, None), mk_ist i1 i2 - | (x, (_, Some t1), i1), (_, (_, Some t2), i2) -> - x, (mkRHole, Some (f t1 t2)), mk_ist i1 i2 - | _, (_, (_, None), _) -> CErrors.anomaly (str"have: mixed C-G constr.") - | _ -> CErrors.anomaly (str"have: mixed G-C constr.") -let loc_ofCG = function - | (_, (s, None), _) -> Glob_ops.loc_of_glob_constr s - | (_, (_, Some s), _) -> Constrexpr_ops.constr_loc s - -let mk_term k c ist = k, (mkRHole, Some c), ist -let mk_lterm = mk_term ' ' - let nf_evar sigma c = EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr c)) @@ -803,25 +775,15 @@ type ('ident, 'term) ssrpattern = | E_In_X_In_T of 'term * 'ident * 'term | E_As_X_In_T of 'term * 'ident * 'term -let pr_pattern = function - | T t -> prl_term t - | In_T t -> str "in " ++ prl_term t - | X_In_T (x,t) -> prl_term x ++ str " in " ++ prl_term t - | In_X_In_T (x,t) -> str "in " ++ prl_term x ++ str " in " ++ prl_term t +let pr_pattern pr_ident pr_term = function + | T t -> pr_term t + | In_T t -> str "in " ++ pr_term t + | X_In_T (x,t) -> pr_ident x ++ str " in " ++ pr_term t + | In_X_In_T (x,t) -> str "in " ++ pr_ident x ++ str " in " ++ pr_term t | E_In_X_In_T (e,x,t) -> - prl_term e ++ str " in " ++ prl_term x ++ str " in " ++ prl_term t + pr_term e ++ str " in " ++ pr_ident x ++ str " in " ++ pr_term t | E_As_X_In_T (e,x,t) -> - prl_term e ++ str " as " ++ prl_term x ++ str " in " ++ prl_term t - -let pr_pattern_w_ids = function - | T t -> prl_term t - | In_T t -> str "in " ++ prl_term t - | X_In_T (x,t) -> pr_id x ++ str " in " ++ prl_term t - | In_X_In_T (x,t) -> str "in " ++ pr_id x ++ str " in " ++ prl_term t - | E_In_X_In_T (e,x,t) -> - prl_term e ++ str " in " ++ pr_id x ++ str " in " ++ prl_term t - | E_As_X_In_T (e,x,t) -> - prl_term e ++ str " as " ++ pr_id x ++ str " in " ++ prl_term t + pr_term e ++ str " as " ++ pr_ident x ++ str " in " ++ pr_term t let pr_pattern_aux pr_constr = function | T t -> pr_constr t @@ -834,16 +796,53 @@ let pr_pattern_aux pr_constr = function pr_constr e ++ str " as " ++ pr_constr x ++ str " in " ++ pr_constr t let pp_pattern env (sigma, p) = pr_pattern_aux (fun t -> pr_econstr_pat env sigma (pi3 (nf_open_term sigma sigma (EConstr.of_constr t)))) p + +type cpattern = + { kind : ssrtermkind + ; pattern : Genintern.glob_constr_and_expr + ; interpretation : Geninterp.interp_sign option } + +let pr_term {kind; pattern; _} = + let env = Global.env () in + let sigma = Evd.from_env env in + pr_guarded (guard_term kind) (pr_glob_constr_and_expr env sigma) pattern +let prl_term {kind; pattern; _} = + let env = Global.env () in + let sigma = Evd.from_env env in + pr_guarded (guard_term kind) (prl_glob_constr_and_expr env sigma) pattern + let pr_cpattern = pr_term -let wit_rpatternty = add_genarg "rpatternty" (fun env sigma -> pr_pattern) +let pr_pattern_w_ids = pr_pattern pr_id prl_term + +let mk_term k c ist = {kind=k; pattern=(mkRHole, Some c); interpretation=ist} +let mk_lterm = mk_term NoFlag let glob_ssrterm gs = function - | k, (_, Some c), None -> - let x = Tacintern.intern_constr gs c in - k, (fst x, Some c), None + | {kind; pattern=(_, Some c); interpretation=None} -> + let x = Tacintern.intern_constr gs c in + {kind; pattern=(fst x, Some c); interpretation=None} | ct -> ct +(* ssrterm conbinators *) +let combineCG t1 t2 f g = + let mk_ist i1 i2 = match i1, i2 with + | None, Some i -> Some i + | Some i, None -> Some i + | None, None -> None + | Some i, Some j when i == j -> Some i + | _ -> CErrors.anomaly (Pp.str "combineCG: different ist") in + match t1, t2 with + | {kind=x; pattern=(t1, None); interpretation=i1}, {pattern=(t2, None); interpretation=i2} -> + {kind=x; pattern=(g t1 t2, None); interpretation = mk_ist i1 i2} + | {kind=x; pattern=(_, Some t1); interpretation=i1}, {pattern=(_, Some t2); interpretation=i2} -> + {kind=x; pattern=(mkRHole, Some (f t1 t2)); interpretation = mk_ist i1 i2} + | _, {pattern=(_, None); _} -> CErrors.anomaly (str"have: mixed C-G constr.") + | _ -> CErrors.anomaly (str"have: mixed G-C constr.") +let loc_ofCG = function + | {pattern = (s, None); _} -> Glob_ops.loc_of_glob_constr s + | {pattern = (_, Some s); _} -> Constrexpr_ops.constr_loc s + (* This piece of code asserts the following notations are reserved *) (* Reserved Notation "( a 'in' b )" (at level 0). *) (* Reserved Notation "( a 'as' b )" (at level 0). *) @@ -851,19 +850,19 @@ let glob_ssrterm gs = function (* Reserved Notation "( a 'as' b 'in' c )" (at level 0). *) let glob_cpattern gs p = pp(lazy(str"globbing pattern: " ++ pr_term p)); - let glob x = pi2 (glob_ssrterm gs (mk_lterm x None)) in + let glob x = (glob_ssrterm gs (mk_lterm x None)).pattern in let encode k s l = let name = Name (Id.of_string ("_ssrpat_" ^ s)) in - k, (mkRCast mkRHole (mkRLambda name mkRHole (mkRApp mkRHole l)), None), None in + {kind=k; pattern=(mkRCast mkRHole (mkRLambda name mkRHole (mkRApp mkRHole l)), None); interpretation=None} in let bind_in t1 t2 = let mkCHole = mkCHole ~loc:None in let n = Name (destCVar t1) in fst (glob (mkCCast mkCHole (mkCLambda n mkCHole t2))) in let check_var t2 = if not (isCVar t2) then loc_error (constr_loc t2) "Only identifiers are allowed here" in match p with - | _, (_, None), _ as x -> x - | k, (v, Some t), _ as orig -> - if k = 'x' then glob_ssrterm gs ('(', (v, Some t), None) else + | {pattern = (_, None); _} as x -> x + | {kind=k; pattern=(v, Some t); _} as orig -> + if k = Cpattern then glob_ssrterm gs {kind=InParens; pattern=(v, Some t); interpretation=None} else match t.CAst.v with | CNotation(_,(InConstrEntry,"( _ in _ )"), ([t1; t2], [], [], [])) -> (try match glob t1, glob t2 with @@ -891,8 +890,8 @@ let glob_rpattern s p = | E_In_X_In_T(e,x,t) -> E_In_X_In_T (glob_ssrterm s e,x,glob_ssrterm s t) | E_As_X_In_T(e,x,t) -> E_As_X_In_T (glob_ssrterm s e,x,glob_ssrterm s t) -let subst_ssrterm s (k, c, ist) = - k, Tacsubst.subst_glob_constr_and_expr s c, ist +let subst_ssrterm s {kind; pattern; interpretation} = + {kind; pattern=Tacsubst.subst_glob_constr_and_expr s pattern; interpretation} let subst_rpattern s = function | T t -> T (subst_ssrterm s t) @@ -902,7 +901,7 @@ let subst_rpattern s = function | E_In_X_In_T(e,x,t) -> E_In_X_In_T (subst_ssrterm s e,x,subst_ssrterm s t) | E_As_X_In_T(e,x,t) -> E_As_X_In_T (subst_ssrterm s e,x,subst_ssrterm s t) -let interp_ssrterm ist (k,t,_) = k, t, Some ist +let interp_ssrterm ist {kind; pattern; _} = {kind; pattern; interpretation = Some ist} let interp_rpattern s = function | T t -> T (interp_ssrterm s t) @@ -910,23 +909,24 @@ let interp_rpattern s = function | X_In_T(x,t) -> X_In_T (interp_ssrterm s x,interp_ssrterm s t) | In_X_In_T(x,t) -> In_X_In_T (interp_ssrterm s x,interp_ssrterm s t) | E_In_X_In_T(e,x,t) -> - E_In_X_In_T (interp_ssrterm s e,interp_ssrterm s x,interp_ssrterm s t) + E_In_X_In_T (interp_ssrterm s e,interp_ssrterm s x,interp_ssrterm s t) | E_As_X_In_T(e,x,t) -> - E_As_X_In_T (interp_ssrterm s e,interp_ssrterm s x,interp_ssrterm s t) + E_As_X_In_T (interp_ssrterm s e,interp_ssrterm s x,interp_ssrterm s t) let interp_rpattern0 ist gl t = Tacmach.project gl, interp_rpattern ist t -type cpattern = char * Genintern.glob_constr_and_expr * Geninterp.interp_sign option -let tag_of_cpattern = pi1 +let tag_of_cpattern p = p.kind let loc_of_cpattern = loc_ofCG -let cpattern_of_term (c, t) ist = c, t, Some ist type occ = (bool * int list) option type rpattern = (cpattern, cpattern) ssrpattern +let pr_rpattern = pr_pattern pr_cpattern pr_cpattern + +let wit_rpatternty = add_genarg "rpatternty" (fun env sigma -> pr_pattern pr_cpattern pr_cpattern) type pattern = Evd.evar_map * (constr, constr) ssrpattern -let id_of_cpattern (_, (c1, c2), _) = +let id_of_cpattern {pattern = (c1, c2); _} = let open CAst in match DAst.get c1, c2 with | _, Some { v = CRef (qid, _) } when qualid_is_ident qid -> @@ -941,12 +941,12 @@ let id_of_Cterm t = match id_of_cpattern t with let interp_open_constr ist env sigma gc = Tacinterp.interp_open_constr ist env sigma gc -let pf_intern_term env sigma (_, c, ist) = glob_constr ist env sigma c +let pf_intern_term env sigma {pattern = c; interpretation = ist; _} = glob_constr ist env sigma c let interp_ssrterm ist gl t = Tacmach.project gl, interp_ssrterm ist t let interp_term env sigma = function - | (_, c, Some ist) -> + | {pattern = c; interpretation = Some ist; _} -> on_snd EConstr.Unsafe.to_constr (interp_open_constr ist env sigma c) | _ -> errorstrm (str"interpreting a term with no ist") @@ -974,17 +974,17 @@ let pr_ist { lfun= lfun } = *) let interp_pattern ?wit_ssrpatternarg env sigma0 red redty = - pp(lazy(str"interpreting: " ++ pr_pattern red)); + pp(lazy(str"interpreting: " ++ pr_rpattern red)); let xInT x y = X_In_T(x,y) and inXInT x y = In_X_In_T(x,y) in let inT x = In_T x and eInXInT e x t = E_In_X_In_T(e,x,t) in let eAsXInT e x t = E_As_X_In_T(e,x,t) in - let mkG ?(k=' ') x ist = k,(x,None), ist in - let ist_of (_,_,ist) = ist in - let decode (_,_,ist as t) ?reccall f g = + let mkG ?(k=NoFlag) x ist = {kind = k; pattern = (x,None); interpretation = ist } in + let ist_of x = x.interpretation in + let decode ({interpretation=ist; _} as t) ?reccall f g = try match DAst.get (pf_intern_term env sigma0 t) with | GCast(t,CastConv c) when isGHole t && isGLambda c-> let (x, c) = destGLambda c in - f x (' ',(c,None),ist) + f x {kind = NoFlag; pattern = (c,None); interpretation = ist} | GVar id when Option.has_some ist && let ist = Option.get ist in Id.Map.mem id ist.lfun && @@ -1027,7 +1027,7 @@ let interp_pattern ?wit_ssrpatternarg env sigma0 red redty = sigma new_evars in sigma in let red = let rec decode_red = function - | T(k,(t,None),ist) -> + | T {kind=k; pattern=(t,None); interpretation=ist} -> begin match DAst.get t with | GCast (c,CastConv t) when isGHole c && @@ -1058,7 +1058,7 @@ let interp_pattern ?wit_ssrpatternarg env sigma0 red redty = let red = match redty with | None -> red - | Some (ty, ist) -> let ty = ' ', ty, Some ist in + | Some (ty, ist) -> let ty = {kind=NoFlag; pattern=ty; interpretation = Some ist} in match red with | T t -> T (combineCG t ty (mkCCast ?loc:(loc_ofCG t)) mkRCast) | X_In_T (x,t) -> @@ -1072,9 +1072,12 @@ let interp_pattern ?wit_ssrpatternarg env sigma0 red redty = E_As_X_In_T (combineCG e ty (mkCCast ?loc:(loc_ofCG t)) mkRCast, x, t) | red -> red in pp(lazy(str"typed as: " ++ pr_pattern_w_ids red)); - let mkXLetIn ?loc x (a,(g,c),ist) = match c with - | Some b -> a,(g,Some (mkCLetIn ?loc x (mkCHole ~loc) b)), ist - | None -> a,(DAst.make ?loc @@ GLetIn (x, DAst.make ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None), ist in + let mkXLetIn ?loc x {kind; pattern=(g,c); interpretation} = match c with + | Some b -> {kind; pattern=(g,Some (mkCLetIn ?loc x (mkCHole ~loc) b)); interpretation} + | None -> { kind + ; pattern = DAst.make ?loc @@ GLetIn + (x, DAst.make ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None + ; interpretation} in match red with | T t -> let sigma, t = interp_term env sigma0 t in sigma, T t | In_T t -> let sigma, t = interp_term env sigma0 t in sigma, In_T t @@ -1255,16 +1258,16 @@ let pf_fill_occ_term gl occ t = cl, t let cpattern_of_id id = - ' ', (DAst.make @@ GRef (GlobRef.VarRef id, None), None), Some Geninterp.({ lfun = Id.Map.empty; poly = false; extra = Tacinterp.TacStore.empty }) + { kind= NoFlag + ; pattern = DAst.make @@ GRef (GlobRef.VarRef id, None), None + ; interpretation = Some Geninterp.({ lfun = Id.Map.empty; poly = false; extra = Tacinterp.TacStore.empty })} -let is_wildcard ((_, (l, r), _) : cpattern) : bool = match DAst.get l, r with +let is_wildcard ({pattern = (l, r); _} : cpattern) : bool = match DAst.get l, r with | _, Some { CAst.v = CHole _ } | GHole _, None -> true | _ -> false (* "ssrpattern" *) -let pr_rpattern = pr_pattern - let pf_merge_uc uc gl = re_sig (sig_it gl) (Evd.merge_universe_context (project gl) uc) diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 17b47227cb..2b90cef039 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -20,17 +20,16 @@ open Genintern (** Pattern parsing *) +type ssrtermkind = | InParens | WithAt | NoFlag | Cpattern + (** The type of context patterns, the patterns of the [set] tactic and [:] tactical. These are patterns that identify a precise subterm. *) -type cpattern +type cpattern = + { kind : ssrtermkind + ; pattern : Genintern.glob_constr_and_expr + ; interpretation : Geninterp.interp_sign option } val pr_cpattern : cpattern -> Pp.t -(** The type of rewrite patterns, the patterns of the [rewrite] tactic. - These patterns also include patterns that identify all the subterms - of a context (i.e. "in" prefix) *) -type rpattern -val pr_rpattern : rpattern -> Pp.t - (** Pattern interpretation and matching *) exception NoMatch @@ -48,6 +47,12 @@ type ('ident, 'term) ssrpattern = type pattern = evar_map * (constr, constr) ssrpattern val pp_pattern : env -> pattern -> Pp.t +(** The type of rewrite patterns, the patterns of the [rewrite] tactic. + These patterns also include patterns that identify all the subterms + of a context (i.e. "in" prefix) *) +type rpattern = (cpattern, cpattern) ssrpattern +val pr_rpattern : rpattern -> Pp.t + (** Extracts the redex and applies to it the substitution part of the pattern. @raise Anomaly if called on [In_T] or [In_X_In_T] *) val redex_of_pattern : @@ -193,9 +198,6 @@ val pf_fill_occ_term : goal sigma -> occ -> evar_map * EConstr.t -> EConstr.t * val fill_occ_term : Environ.env -> Evd.evar_map -> EConstr.t -> occ -> evar_map * EConstr.t -> EConstr.t * EConstr.t -(* It may be handy to inject a simple term into the first form of cpattern *) -val cpattern_of_term : char * glob_constr_and_expr -> Geninterp.interp_sign -> cpattern - (** Helpers to make stateful closures. Example: a [find_P] function may be called many times, but the pattern instantiation phase is performed only the first time. The corresponding [conclude] has to return the instantiated @@ -219,7 +221,7 @@ val pf_unify_HO : goal sigma -> EConstr.constr -> EConstr.constr -> goal sigma (** Some more low level functions needed to implement the full SSR language on top of the former APIs *) -val tag_of_cpattern : cpattern -> char +val tag_of_cpattern : cpattern -> ssrtermkind val loc_of_cpattern : cpattern -> Loc.t option val id_of_pattern : pattern -> Names.Id.t option val is_wildcard : cpattern -> bool @@ -245,7 +247,7 @@ sig val pr_rpattern : rpattern -> Pp.t val mk_rpattern : (cpattern, cpattern) ssrpattern -> rpattern val mk_lterm : Constrexpr.constr_expr -> Geninterp.interp_sign option -> cpattern - val mk_term : char -> Constrexpr.constr_expr -> Geninterp.interp_sign option -> cpattern + val mk_term : ssrtermkind -> Constrexpr.constr_expr -> Geninterp.interp_sign option -> cpattern val glob_cpattern : Genintern.glob_sign -> cpattern -> cpattern val subst_ssrterm : Mod_subst.substitution -> cpattern -> cpattern diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index d0b724b755..4b0974ae03 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -127,9 +127,10 @@ let flex_kind_of_term flags env evd c sk = else Rigid | Evar ev -> if is_evar_allowed flags (fst ev) then Flexible ev else Rigid - | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ | Int _ | Float _ | Array _ -> Rigid + | Lambda _ | Prod _ | Sort _ | Ind _ | Int _ | Float _ | Array _ -> Rigid + | Construct _ | CoFix _ (* Incorrect: should check only app in sk *) -> Rigid | Meta _ -> Rigid - | Fix _ -> Rigid (* happens when the fixpoint is partially applied *) + | Fix _ -> Rigid (* happens when the fixpoint is partially applied (should check it?) *) | Cast _ | App _ | Case _ -> assert false let apprec_nohdbeta flags env evd c = @@ -328,12 +329,6 @@ let ise_and evd l = | UnifFailure _ as x -> x in ise_and evd l -let ise_exact ise x1 x2 = - match ise x1 x2 with - | None, out -> out - | _, (UnifFailure _ as out) -> out - | Some _, Success i -> UnifFailure (i,NotSameArgSize) - let ise_array2 evd f v1 v2 = let rec allrec i = function | -1 -> Success i @@ -355,37 +350,49 @@ let rec ise_inst2 evd f l1 l2 = match l1, l2 with (* Applicative node of stack are read from the outermost to the innermost but are unified the other way. *) -let rec ise_app_stack2 env f evd sk1 sk2 = - match sk1,sk2 with - | Stack.App node1 :: q1, Stack.App node2 :: q2 -> - let (t1,l1) = Stack.decomp_node_last node1 q1 in - let (t2,l2) = Stack.decomp_node_last node2 q2 in - begin match ise_app_stack2 env f evd l1 l2 with - |(_,UnifFailure _) as x -> x - |x,Success i' -> x,f env i' CONV t1 t2 +let rec ise_app_rev_stack2 env f evd revsk1 revsk2 = + match Stack.decomp_rev revsk1, Stack.decomp_rev revsk2 with + | Some (t1,revsk1), Some (t2,revsk2) -> + begin + match ise_app_rev_stack2 env f evd revsk1 revsk2 with + | (_, UnifFailure _) as x -> x + | x, Success i' -> x, f env i' CONV t1 t2 end - | _, _ -> (sk1,sk2), Success evd + | _, _ -> (revsk1,revsk2), Success evd (* This function tries to unify 2 stacks element by element. It works from the end to the beginning. If it unifies a non empty suffix of stacks but not the entire stacks, the first part of the answer is - Some(the remaining prefixes to tackle)) *) -let ise_stack2 no_app env evd f sk1 sk2 = - let rec ise_stack2 deep i sk1 sk2 = - let fail x = if deep then Some (List.rev sk1, List.rev sk2), Success i + Some(the remaining prefixes to tackle) + If [no_app] is set, situations like [match head u1 u2 with ... end] + will not try to match [u1] and [u2] (why?); but situations like + [match head u1 u2 with ... end v] will try to match [v] (??) *) +(* Input: E1[] =? E2[] where the E1, E2 are concatenations of + n-ary-app/case/fix/proj elimination rules + Output: + - either None if E1 = E2 is solved, + - or Some (E1'',E2'') such that there is a decomposition of + E1[] = E1'[E1''[]] and E2[] = E2'[E2''[]] s.t. E1' = E2' and + E1'' cannot be unified with E2'' + - UnifFailure if no such non-empty E1' = E2' exists *) +let rec ise_stack2 no_app env evd f sk1 sk2 = + let rec ise_rev_stack2 deep i revsk1 revsk2 = + let fail x = if deep then Some (List.rev revsk1, List.rev revsk2), Success i else None, x in - match sk1, sk2 with + match revsk1, revsk2 with | [], [] -> None, Success i | Stack.Case (_,t1,_,c1)::q1, Stack.Case (_,t2,_,c2)::q2 -> - (match f env i CONV t1 t2 with - | Success i' -> - (match ise_array2 i' (fun ii -> f env ii CONV) c1 c2 with - | Success i'' -> ise_stack2 true i'' q1 q2 - | UnifFailure _ as x -> fail x) - | UnifFailure _ as x -> fail x) + begin + match ise_and i [ + (fun i -> f env i CONV t1 t2); + (fun i -> ise_array2 i (fun ii -> f env ii CONV) c1 c2)] + with + | Success i' -> ise_rev_stack2 true i' q1 q2 + | UnifFailure _ as x -> fail x + end | Stack.Proj (p1)::q1, Stack.Proj (p2)::q2 -> if QProjection.Repr.equal env (Projection.repr p1) (Projection.repr p2) - then ise_stack2 true i q1 q2 + then ise_rev_stack2 true i q1 q2 else fail (UnifFailure (i, NotSameHead)) | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1)::q1, Stack.Fix (((li2, i2),(_,tys2,bds2)),a2)::q2 -> @@ -393,51 +400,51 @@ let ise_stack2 no_app env evd f sk1 sk2 = match ise_and i [ (fun i -> ise_array2 i (fun ii -> f env ii CONV) tys1 tys2); (fun i -> ise_array2 i (fun ii -> f (push_rec_types recdef1 env) ii CONV) bds1 bds2); - (fun i -> ise_exact (ise_stack2 false i) a1 a2)] with - | Success i' -> ise_stack2 true i' q1 q2 + (fun i -> snd (ise_stack2 no_app env i f a1 a2))] with + | Success i' -> ise_rev_stack2 true i' q1 q2 | UnifFailure _ as x -> fail x else fail (UnifFailure (i,NotSameHead)) | Stack.App _ :: _, Stack.App _ :: _ -> if no_app && deep then fail ((*dummy*)UnifFailure(i,NotSameHead)) else - begin match ise_app_stack2 env f i sk1 sk2 with + begin match ise_app_rev_stack2 env f i revsk1 revsk2 with |_,(UnifFailure _ as x) -> fail x - |(l1, l2), Success i' -> ise_stack2 true i' l1 l2 + |(l1, l2), Success i' -> ise_rev_stack2 true i' l1 l2 end |_, _ -> fail (UnifFailure (i,(* Maybe improve: *) NotSameHead)) - in ise_stack2 false evd (List.rev sk1) (List.rev sk2) + in ise_rev_stack2 false evd (List.rev sk1) (List.rev sk2) (* Make sure that the matching suffix is the all stack *) -let exact_ise_stack2 env evd f sk1 sk2 = - let rec ise_stack2 i sk1 sk2 = - match sk1, sk2 with +let rec exact_ise_stack2 env evd f sk1 sk2 = + let rec ise_rev_stack2 i revsk1 revsk2 = + match revsk1, revsk2 with | [], [] -> Success i | Stack.Case (_,t1,_,c1)::q1, Stack.Case (_,t2,_,c2)::q2 -> ise_and i [ - (fun i -> ise_stack2 i q1 q2); + (fun i -> ise_rev_stack2 i q1 q2); (fun i -> ise_array2 i (fun ii -> f env ii CONV) c1 c2); (fun i -> f env i CONV t1 t2)] | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1)::q1, Stack.Fix (((li2, i2),(_,tys2,bds2)),a2)::q2 -> if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then ise_and i [ - (fun i -> ise_stack2 i q1 q2); + (fun i -> ise_rev_stack2 i q1 q2); (fun i -> ise_array2 i (fun ii -> f env ii CONV) tys1 tys2); (fun i -> ise_array2 i (fun ii -> f (push_rec_types recdef1 env) ii CONV) bds1 bds2); - (fun i -> ise_stack2 i a1 a2)] + (fun i -> exact_ise_stack2 env i f a1 a2)] else UnifFailure (i,NotSameHead) | Stack.Proj (p1)::q1, Stack.Proj (p2)::q2 -> if QProjection.Repr.equal env (Projection.repr p1) (Projection.repr p2) - then ise_stack2 i q1 q2 + then ise_rev_stack2 i q1 q2 else (UnifFailure (i, NotSameHead)) | Stack.App _ :: _, Stack.App _ :: _ -> - begin match ise_app_stack2 env f i sk1 sk2 with + begin match ise_app_rev_stack2 env f i revsk1 revsk2 with |_,(UnifFailure _ as x) -> x - |(l1, l2), Success i' -> ise_stack2 i' l1 l2 + |(l1, l2), Success i' -> ise_rev_stack2 i' l1 l2 end |_, _ -> UnifFailure (i,(* Maybe improve: *) NotSameHead) in if Reductionops.Stack.compare_shape sk1 sk2 then - ise_stack2 evd (List.rev sk1) (List.rev sk2) + ise_rev_stack2 evd (List.rev sk1) (List.rev sk2) else UnifFailure (evd, (* Dummy *) NotSameHead) (* Add equality constraints for covariant/invariant positions. For @@ -575,31 +582,35 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty let quick_fail i = (* not costly, loses info *) UnifFailure (i, NotSameHead) in - let miller_pfenning on_left fallback ev lF tM evd = + let miller_pfenning l2r fallback ev lF tM evd = match is_unification_pattern_evar env evd ev lF tM with | None -> fallback () | Some l1' -> (* Miller-Pfenning's patterns unification *) let t2 = tM in let t2 = solve_pattern_eqn env evd l1' t2 in solve_simple_eqn (conv_fun evar_conv_x) flags env evd - (position_problem on_left pbty,ev,t2) + (position_problem l2r pbty,ev,t2) in - let consume_stack on_left (termF,skF) (termO,skO) evd = - let switch f a b = if on_left then f a b else f b a in + let consume_stack l2r (termF,skF) (termO,skO) evd = + let switch f a b = if l2r then f a b else f b a in let not_only_app = Stack.not_purely_applicative skO in match switch (ise_stack2 not_only_app env evd (evar_conv_x flags)) skF skO with - |Some (l,r), Success i' when on_left && (not_only_app || List.is_empty l) -> + | Some (l,r), Success i' when l2r && (not_only_app || List.is_empty l) -> + (* E[?n]=E'[redex] reduces to either l[?n]=r[redex] with + case/fix/proj in E' (why?) or ?n=r[redex] *) switch (evar_conv_x flags env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r)) - |Some (r,l), Success i' when not on_left && (not_only_app || List.is_empty l) -> + | Some (r,l), Success i' when not l2r && (not_only_app || List.is_empty l) -> + (* E'[redex]=E[?n] reduces to either r[redex]=l[?n] with + case/fix/proj in E' (why?) or r[redex]=?n *) switch (evar_conv_x flags env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r)) - |None, Success i' -> switch (evar_conv_x flags env i' pbty) termF termO - |_, (UnifFailure _ as x) -> x - |Some _, _ -> UnifFailure (evd,NotSameArgSize) in - let eta env evd onleft sk term sk' term' = - assert (match sk with [] -> true | _ -> false); + | None, Success i' -> switch (evar_conv_x flags env i' pbty) termF termO + | _, (UnifFailure _ as x) -> x + | Some _, _ -> UnifFailure (evd,NotSameArgSize) in + let eta_lambda env evd onleft term (term',sk') = + (* Reduces an equation [env |- <(fun na:c1 => c'1)|empty> = <term'|sk'>] to + [env, na:c1 |- c'1 = sk'[term'] (with some additional reduction) *) let (na,c1,c'1) = destLambda evd term in - let c = nf_evar evd c1 in - let env' = push_rel (RelDecl.LocalAssum (na,c)) env in + let env' = push_rel (RelDecl.LocalAssum (na,c1)) env in let out1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env' evd (c'1, Stack.empty) in let out2 = whd_nored_state env' evd @@ -617,32 +628,39 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk sk')] in - let consume on_left (_, skF as apprF) (_,skM as apprM) i = + let consume l2r (_, skF as apprF) (_,skM as apprM) i = if not (Stack.is_empty skF && Stack.is_empty skM) then - consume_stack on_left apprF apprM i + consume_stack l2r apprF apprM i else quick_fail i in - let miller on_left ev (termF,skF as apprF) (termM, skM as apprM) i = - let switch f a b = if on_left then f a b else f b a in + let miller l2r ev (termF,skF as apprF) (termM, skM as apprM) i = + let switch f a b = if l2r then f a b else f b a in let not_only_app = Stack.not_purely_applicative skM in match Stack.list_of_app_stack skF with | None -> quick_fail evd | Some lF -> let tM = Stack.zip evd apprM in - miller_pfenning on_left + miller_pfenning l2r (fun () -> if not_only_app then (* Postpone the use of an heuristic *) switch (fun x y -> Success (Evarutil.add_unification_pb (pbty,env,x,y) i)) (Stack.zip evd apprF) tM else quick_fail i) ev lF tM i in - let flex_maybeflex on_left ev (termF,skF as apprF) (termM, skM as apprM) vM = - let switch f a b = if on_left then f a b else f b a in + let flex_maybeflex l2r ev (termF,skF as apprF) (termM, skM as apprM) vM = + (* Problem: E[?n[inst]] = E'[redex] + Strategy, as far as I understand: + 1. if E[]=[]u1..un and ?n[inst] u1..un = E'[redex] is a Miller pattern: solve it now + 2a. if E'=E'1[E'2] and E=E'1 unifiable, recursively solve ?n[inst] = E'2[redex] + 2b. if E'=E'1[E'2] and E=E1[E2] and E=E'1 unifiable and E' contient app/fix/proj, + recursively solve E2[?n[inst]] = E'2[redex] + 3. reduce the redex into M and recursively solve E[?n[inst]] =? E'[M] *) + let switch f a b = if l2r then f a b else f b a in let delta i = switch (evar_eqappr_x flags env i pbty) apprF (whd_betaiota_deltazeta_for_iota_state flags.open_ts env i (vM,skM)) in - let default i = ise_try i [miller on_left ev apprF apprM; - consume on_left apprF apprM; + let default i = ise_try i [miller l2r ev apprF apprM; + consume l2r apprF apprM; delta] in match EConstr.kind evd termM with @@ -663,8 +681,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty let delta' i = switch (evar_eqappr_x flags env i pbty) apprF apprM' in - fun i -> ise_try i [miller on_left ev apprF apprM'; - consume on_left apprF apprM'; delta'] + fun i -> ise_try i [miller l2r ev apprF apprM'; + consume l2r apprF apprM'; delta'] with Retyping.RetypeError _ -> (* Happens thanks to w_unify building ill-typed terms *) default @@ -672,21 +690,32 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty end | _ -> default evd in - let flex_rigid on_left ev (termF, skF as apprF) (termR, skR as apprR) = - let switch f a b = if on_left then f a b else f b a in + let flex_rigid l2r ev (termF, skF as apprF) (termR, skR as apprR) = + (* Problem: E[?n[inst]] = E'[M] with M blocking computation (in theory) + Strategy, as far as I understand: + 1. if E[]=[]u1..un and ?n[inst] u1..un = E'[M] is a Miller pattern: solve it now + 2a. if E'=E'1[E'2] and E=E'1 unifiable and E' contient app/fix/proj, + recursively solve ?n[inst] = E'2[M] + 2b. if E'=E'1[E'2] and E=E1[E2] and E=E'1 unifiable and E' contient app/fix/proj, + recursively solve E2[?n[inst]] = E'2[M] + 3a. if M a lambda or a constructor: eta-expand and recursively solve + 3b. if M a constructor C ..ui..: eta-expand and recursively solve proji[E[?n[inst]]]=ui + 4. fail if E purely applicative and ?n occurs rigidly in E'[M] + 5. absorb arguments if purely applicative and postpone *) + let switch f a b = if l2r then f a b else f b a in let eta evd = match EConstr.kind evd termR with | Lambda _ when (* if ever problem is ill-typed: *) List.is_empty skR -> - eta env evd false skR termR skF termF - | Construct u -> eta_constructor flags env evd skR u skF termF + eta_lambda env evd false termR apprF + | Construct u -> eta_constructor flags env evd u skR apprF | _ -> UnifFailure (evd,NotSameHead) in match Stack.list_of_app_stack skF with | None -> - ise_try evd [consume_stack on_left apprF apprR; eta] + ise_try evd [consume_stack l2r apprF apprR; eta] | Some lF -> let tR = Stack.zip evd apprR in - miller_pfenning on_left + miller_pfenning l2r (fun () -> ise_try evd [eta;(* Postpone the use of an heuristic *) @@ -716,6 +745,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty solve_simple_eqn (conv_fun evar_conv_x) flags env i' (position_problem true pbty,destEvar i' ev1',term2) else + (* HH: Why not to drop sk1 and sk2 since they unified *) evar_eqappr_x flags env evd pbty (ev1', sk1) (term2, sk2) | Some (r,[]), Success i' -> @@ -736,7 +766,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty if isEvar i' ev1' then solve_simple_eqn (conv_fun evar_conv_x) flags env i' (position_problem true pbty,destEvar i' ev1',Stack.zip i' (term2,r)) - else evar_eqappr_x flags env evd pbty + else + (* HH: Why not to drop sk1 and sk2 since they unified *) + evar_eqappr_x flags env evd pbty (ev1', sk1) (term2, sk2) | None, (UnifFailure _ as x) -> (* sk1 and sk2 have no common outer part *) @@ -764,7 +796,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty else (* We could instead try Miller unification, then postpone to see if other equations help, as in: - [Check fun a b c : unit => (eqᵣefl : _ a b = _ c a b)] *) + [Check fun a b c : unit => (eq_refl : _ a b = _ c a b)] *) UnifFailure (i,NotSameArgSize) | _, _ -> anomaly (Pp.str "Unexpected result from ise_stack2.") in @@ -776,7 +808,17 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty match (flex_kind_of_term flags env evd term1 sk1, flex_kind_of_term flags env evd term2 sk2) with | Flexible (sp1,al1), Flexible (sp2,al2) -> - (* sk1[?ev1] =? sk2[?ev2] *) + (* Notations: + - "sk" is a stack (or, more abstractly, an evaluation context, written E) + - "ev" is an evar "?ev", more precisely an evar ?n with an instance inst + - "al" is an evar instance + Problem: E₁[?n₁[inst₁]] = E₂[?n₂[inst₂]] (i.e. sk1[?ev1] =? sk2[?ev2] + Strategy is first-order unification + 1a. if E₁=E₂ unifiable, solve ?n₁[inst₁] = ?n₂[inst₂] + 1b. if E₂=E₂'[E₂''] and E₁=E₂' unifiable, recursively solve ?n₁[inst₁] = E₂''[?n₂[inst₂]] + 1b'. if E₁=E₁'[E₁''] and E₁'=E₂ unifiable, recursively solve E₁''[?n₁[inst₁]] = ?n₂[inst₂] + recursively solve E2[?n[inst]] = E'2[redex] + 2. fails if neither E₁ nor E₂ is a prefix of the other *) let f1 i = first_order env i term1 term2 sk1 sk2 and f2 i = if Evar.equal sp1 sp2 then @@ -976,10 +1018,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty (* Eta-expansion *) | Rigid, _ when isLambda evd term1 && (* if ever ill-typed: *) List.is_empty sk1 -> - eta env evd true sk1 term1 sk2 term2 + eta_lambda env evd true term1 (term2,sk2) | _, Rigid when isLambda evd term2 && (* if ever ill-typed: *) List.is_empty sk2 -> - eta env evd false sk2 term2 sk1 term1 + eta_lambda env evd false term2 (term1,sk1) | Rigid, Rigid -> begin match EConstr.kind evd term1, EConstr.kind evd term2 with @@ -1033,10 +1075,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty else UnifFailure (evd,NotSameHead) | Construct u, _ -> - eta_constructor flags env evd sk1 u sk2 term2 + eta_constructor flags env evd u sk1 (term2,sk2) | _, Construct u -> - eta_constructor flags env evd sk2 u sk1 term1 + eta_constructor flags env evd u sk2 (term1,sk1) | Fix ((li1, i1),(_,tys1,bds1 as recdef1)), Fix ((li2, i2),(_,tys2,bds2)) -> (* Partially applied fixs *) if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then @@ -1131,7 +1173,9 @@ and conv_record flags env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk (fst (decompose_app_vect i (substl ks h))))] else UnifFailure(evd,(*dummy*)NotSameHead) -and eta_constructor flags env evd sk1 ((ind, i), u) sk2 term2 = +and eta_constructor flags env evd ((ind, i), u) sk1 (term2,sk2) = + (* reduces an equation <Construct(ind,i)|sk1> == <term2|sk2> to the + equations [arg_i = Proj_i (sk2[term2])] where [sk1] is [params args] *) let open Declarations in let mib = lookup_mind (fst ind) env in match get_projections env ind with diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 44414aa6a0..f9f6f74a66 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1585,7 +1585,16 @@ let rec invert_definition unify flags choose imitate_defs imitate envk (subst1 b c) | Evar (evk',args' as ev') -> if Evar.equal evk evk' then raise (OccurCheckIn (evd,rhs)); - (* Evar/Evar problem (but left evar is virtual) *) + (* At this point, we imitated a context say, C[ ], and virtually + instantiated ?evk@{x₁..xn} with C[?evk''@{x₁..xn,y₁..yk}] + for y₁..yk the spine of variables of C[ ], now facing the + equation env, y₁...yk |- ?evk'@{args'} =?= ?evk''@{args,y1:=y1..yk:=yk} *) + (* Assume evk' is defined in context x₁'..xk'. + As a first step, we try to find a restriction ?evk'''@{xᵢ₁'..xᵢⱼ} of + ?evk' and an instance args''' in the environment of ?evk such that + env, y₁..yk |- args'''[args] = args' and thus such that + env, y₁..yk |- ?evk'''@{args'''[args]} = ?evk''@{args,y1:=y1..yk:=yk} *) + (* Note that we don't need to declare ?evk'' yet: it may remain virtual *) let aliases = lift_aliases k aliases in (try let ev = (evk,List.map (lift k) argsv) in @@ -1597,14 +1606,14 @@ let rec invert_definition unify flags choose imitate_defs | CannotProject (evd,ev') -> if not !progress then raise (NotEnoughInformationEvarEvar t); - (* Make the virtual left evar real *) + (* We could not invert args' in terms of args, so we now make ?evk'' real *) let ty = get_type_of env' evd t in let (evd,evar'',ev'') = materialize_evar (evar_define unify flags ~choose) env' evd k ev ty in (* materialize_evar may instantiate ev' by another evar; adjust it *) let (evk',args' as ev') = normalize_evar evd ev' in let evd = - (* Try to project (a restriction of) the left evar ... *) + (* Try now to invert args in terms of args' *) try let evd,body = project_evar_on_evar false unify flags env' evd aliases 0 None ev'' ev' in let evd = Evd.define evk' body evd in diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 094dae4828..d347f46637 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -136,6 +136,24 @@ val solve_evar_evar : ?force:bool -> (** The two evars are expected to be in inferably convertible types; if not, an exception IllTypedInstance is raised *) +(* [solve_simple_eqn unifier flags env evd (direction,?ev[inst],t)] + makes progresses on problems of the form [?ev[inst] := t] (or + [?ev[inst] :<= t], or [?ev[inst] :>= t]). It uses imitation and a + limited form of projection. At the time of writing this comment, + only rels/vars (possibly indirectly via a chain of evars) and + constructors are used for projection. For instance + [?e[x,S 0] := x + S 0] will be solved by imitating [+] and + projecting [x] and [S 0] (so that [?e[a,b]:=a+b]) but in + [?e[0+0] := 0+0], the possible imitation will not be seen. + + [choose] tells to make an irreversible choice when two valid + projections are competing. It is to be used when no more reversible + progress can be done. It is [false] by default. + + [imitate_defs] tells to expand local definitions if they cannot be + projected. It is [true] by default. +*) + val solve_simple_eqn : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool -> env -> evar_map -> bool option * existential * constr -> unification_result diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 9580825010..52f60fbc5e 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -194,6 +194,7 @@ sig val append_app : 'a array -> 'a t -> 'a t val decomp : 'a t -> ('a * 'a t) option val decomp_node_last : 'a app_node -> 'a t -> ('a * 'a t) + val decomp_rev : 'a t -> ('a * 'a t) option val compare_shape : 'a t -> 'a t -> bool val map : ('a -> 'a) -> 'a t -> 'a t val fold2 : ('a -> constr -> constr -> 'a) -> 'a -> @@ -214,13 +215,13 @@ end = struct open EConstr type 'a app_node = int * 'a array * int - (* first releavnt position, arguments, last relevant position *) + (* first relevant position, arguments, last relevant position *) (* - Invariant that this module must ensure : - (behare of direct access to app_node by the rest of Reductionops) + Invariant that this module must ensure: + (beware of direct access to app_node by the rest of Reductionops) - in app_node (i,_,j) i <= j - - There is no array realocation (outside of debug printing) + - There is no array reallocation (outside of debug printing) *) let pr_app_node pr (i,a,j) = @@ -267,12 +268,10 @@ struct let le = Array.length v in if Int.equal le 0 then s else App (0,v,pred le) :: s - let decomp_node (i,l,j) sk = - if i < j then (l.(i), App (succ i,l,j) :: sk) - else (l.(i), sk) - - let decomp = function - | App node::s -> Some (decomp_node node s) + let decomp_rev = function + | App (i,l,j) :: sk -> + if i < j then Some (l.(j), App (i,l,pred j) :: sk) + else Some (l.(j), sk) | _ -> None let decomp_node_last (i,l,j) sk = @@ -293,7 +292,7 @@ struct Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 | (Primitive(_,_,a1,_)::s1, Primitive(_,_,a2,_)::s2) -> Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 - | ((Case _|Proj _|Fix _|Primitive _) :: _ | []) ,_ -> false in + | ((Case _ | Proj _ | Fix _ | Primitive _) :: _ | []) ,_ -> false in compare_rec 0 stk1 stk2 exception IncompatibleFold2 @@ -334,29 +333,35 @@ struct append_app a s let rec args_size = function - | App (i,_,j)::s -> j + 1 - i + args_size s - | (Case _|Fix _|Proj _|Primitive _)::_ | [] -> 0 + | App (i,_,j) :: s -> j + 1 - i + args_size s + | (Case _ | Fix _ | Proj _ | Primitive _) :: _ | [] -> 0 let strip_app s = let rec aux out = function | ( App _ as e) :: s -> aux (e :: out) s | s -> List.rev out,s in aux [] s + let strip_n_app n s = let rec aux n out = function | App (i,a,j) as e :: s -> - let nb = j - i + 1 in + let nb = j - i + 1 in if n >= nb then - aux (n - nb) (e::out) s + aux (n - nb) (e :: out) s else - let p = i+n in + let p = i + n in Some (CList.rev (if Int.equal n 0 then out else App (i,a,p-1) :: out), a.(p), - if j > p then App(succ p,a,j)::s else s) + if j > p then App (succ p,a,j) :: s else s) | s -> None in aux n [] s + let decomp s = + match strip_n_app 0 s with + | Some (_,a,s) -> Some (a,s) + | None -> None + let not_purely_applicative args = List.exists (function (Fix _ | Case _ | Proj _ ) -> true | App _ | Primitive _ -> false) args @@ -369,12 +374,11 @@ struct (Array.fold_right (fun x y -> x::y) a' args', s') | s -> ([],s) in let (out,s') = aux s in - let init = match s' with [] -> true | _ -> false in - Option.init init out + match s' with [] -> Some out | _ -> None let assign s p c = match strip_n_app p s with - | Some (pre,_,sk) -> pre @ (App (0,[|c|],0)::sk) + | Some (pre,_,sk) -> pre @ (App (0,[|c|],0) :: sk) | None -> assert false let tail n0 s0 = @@ -382,12 +386,12 @@ struct if Int.equal n 0 then s else match s with | App (i,a,j) :: s -> - let nb = j - i + 1 in + let nb = j - i + 1 in if n >= nb then aux (n - nb) s else let p = i+n in - if j >= p then App(p,a,j)::s else s + if j >= p then App (p,a,j) :: s else s | _ -> raise (Invalid_argument "Reductionops.Stack.tail") in aux n0 s0 diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 0b7f43f469..ae93eb48b4 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -69,10 +69,9 @@ module Stack : sig val empty : 'a t val is_empty : 'a t -> bool - val append_app : 'a array -> 'a t -> 'a t - val decomp : 'a t -> ('a * 'a t) option val decomp_node_last : 'a app_node -> 'a t -> ('a * 'a t) + [@@ocaml.deprecated "Use decomp_rev"] val compare_shape : 'a t -> 'a t -> bool @@ -84,23 +83,51 @@ module Stack : sig val fold2 : ('a -> constr -> constr -> 'a) -> 'a -> constr t -> constr t -> 'a val map : ('a -> 'a) -> 'a t -> 'a t + + (** [append_app args sk] pushes array of arguments [args] on [sk] *) + val append_app : 'a array -> 'a t -> 'a t + + (** [append_app_list args sk] pushes list of arguments [args] on [sk] *) val append_app_list : 'a list -> 'a t -> 'a t - (** if [strip_app s] = [(a,b)], then [s = a @ b] and [b] does not - start by App *) + (** if [strip_app sk] = [(sk1,sk2)], then [sk = sk1 @ sk2] with + [sk1] purely applicative and [sk2] does not start with an argument *) val strip_app : 'a t -> 'a t * 'a t - (** @return (the nth first elements, the (n+1)th element, the remaining stack) *) + (** @return (the nth first elements, the (n+1)th element, the remaining stack) + if there enough of those *) val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option + (** [decomp sk] extracts the first argument of [sk] is there is some *) + val decomp : 'a t -> ('a * 'a t) option + + (** [decomp sk] extracts the first argument of reversed stack [sk] is there is some *) + val decomp_rev : 'a t -> ('a * 'a t) option + + (** [not_purely_applicative sk] *) val not_purely_applicative : 'a t -> bool + + (** [list_of_app_stack sk] either returns [Some sk] turned into a list of + arguments if [sk] is purely applicative and [None] otherwise *) val list_of_app_stack : constr t -> constr list option + (** [assign sk n a] changes the [n]th argument of [sk] with [a], counting from 0 + @raise an anomaly if there is less that [n] arguments available *) val assign : 'a t -> int -> 'a -> 'a t + + (** [args_size sk] returns the number of arguments available at the + head of [sk] *) val args_size : 'a t -> int + + (** [tail n sk] drops the [n] first arguments of [sk] + @raise [Invalid_argument] if there are not enough arguments *) val tail : int -> 'a t -> 'a t + + (** [nth sk n] returns the [n]-th argument of [sk], counting from 0 + @raise [Not_found] if there is no [n]th argument *) val nth : 'a t -> int -> 'a + (** [zip sigma t sk] *) val zip : evar_map -> constr * constr t -> constr end diff --git a/theories/Bool/BoolEq.v b/theories/Bool/BoolEq.v index f002ee427c..dd10c758a5 100644 --- a/theories/Bool/BoolEq.v +++ b/theories/Bool/BoolEq.v @@ -46,7 +46,7 @@ Section Bool_eq_dec. Definition exists_beq_eq : forall x y:A, {b : bool | b = beq x y}. Proof. - intros. + intros x y. exists (beq x y). constructor. Defined. diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v index ef78121d63..5eb2a99739 100644 --- a/theories/Bool/DecBool.v +++ b/theories/Bool/DecBool.v @@ -18,7 +18,7 @@ Theorem ifdec_left : forall (A B:Prop) (C:Set) (H:{A} + {B}), ~ B -> forall x y:C, ifdec H x y = x. Proof. - intros; case H; auto. + intros A B C H **; case H; auto. intro; absurd B; trivial. Qed. @@ -26,7 +26,7 @@ Theorem ifdec_right : forall (A B:Prop) (C:Set) (H:{A} + {B}), ~ A -> forall x y:C, ifdec H x y = y. Proof. - intros; case H; auto. + intros A B C H **; case H; auto. intro; absurd A; trivial. Qed. diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v index 7e9087c377..8366e8257e 100644 --- a/theories/Bool/IfProp.v +++ b/theories/Bool/IfProp.v @@ -29,13 +29,13 @@ case diff_true_false; trivial with bool. Qed. Lemma IfProp_true : forall A B:Prop, IfProp A B true -> A. -intros. +intros A B H. inversion H. assumption. Qed. Lemma IfProp_false : forall A B:Prop, IfProp A B false -> B. -intros. +intros A B H. inversion H. assumption. Qed. @@ -45,7 +45,7 @@ destruct 1; auto with bool. Qed. Lemma IfProp_sum : forall (A B:Prop) (b:bool), IfProp A B b -> {A} + {B}. -destruct b; intro H. +intros A B b; destruct b; intro H. - left; inversion H; auto with bool. - right; inversion H; auto with bool. Qed. diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v index aff5008410..418fc88489 100644 --- a/theories/Bool/Zerob.v +++ b/theories/Bool/Zerob.v @@ -19,26 +19,26 @@ Definition zerob (n:nat) : bool := | S _ => false end. -Lemma zerob_true_intro : forall n:nat, n = 0 -> zerob n = true. +Lemma zerob_true_intro (n : nat) : n = 0 -> zerob n = true. Proof. destruct n; [ trivial with bool | inversion 1 ]. Qed. #[global] Hint Resolve zerob_true_intro: bool. -Lemma zerob_true_elim : forall n:nat, zerob n = true -> n = 0. +Lemma zerob_true_elim (n : nat) : zerob n = true -> n = 0. Proof. destruct n; [ trivial with bool | inversion 1 ]. Qed. -Lemma zerob_false_intro : forall n:nat, n <> 0 -> zerob n = false. +Lemma zerob_false_intro (n : nat) : n <> 0 -> zerob n = false. Proof. destruct n; [ destruct 1; auto with bool | trivial with bool ]. Qed. #[global] Hint Resolve zerob_false_intro: bool. -Lemma zerob_false_elim : forall n:nat, zerob n = false -> n <> 0. +Lemma zerob_false_elim (n : nat) : zerob n = false -> n <> 0. Proof. destruct n; [ inversion 1 | auto with bool ]. Qed. diff --git a/theories/Classes/CEquivalence.v b/theories/Classes/CEquivalence.v index f23cf158ac..82a76e8afd 100644 --- a/theories/Classes/CEquivalence.v +++ b/theories/Classes/CEquivalence.v @@ -64,8 +64,8 @@ Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv. now transitivity y. Qed. -Arguments equiv_symmetric {A R} sa x y. -Arguments equiv_transitive {A R} sa x y z. +Arguments equiv_symmetric {A R} sa x y : rename. +Arguments equiv_transitive {A R} sa x y z : rename. (** Use the [substitute] command which substitutes an equivalence in every hypothesis. *) diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v index 9ff18ebe2c..d6a0ae5411 100644 --- a/theories/Classes/CMorphisms.v +++ b/theories/Classes/CMorphisms.v @@ -567,9 +567,7 @@ Section Normalize. Lemma proper_normalizes_proper `(Normalizes R0 R1, Proper A R1 m) : Proper R0 m. Proof. - red in H, H0. red in H. - apply (snd (H _ _)). - assumption. + apply (_ : Normalizes R0 R1). assumption. Qed. Lemma flip_atom R : Normalizes R (flip (flip R)). diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v index c489d82d0b..561822ef0c 100644 --- a/theories/Classes/CRelationClasses.v +++ b/theories/Classes/CRelationClasses.v @@ -352,14 +352,12 @@ Section Binary. Global Instance partial_order_antisym `(PartialOrder eqA R) : Antisymmetric eqA R. Proof with auto. reduce_goal. - apply H. firstorder. + firstorder. Qed. Lemma PartialOrder_inverse `(PartialOrder eqA R) : PartialOrder eqA (flip R). Proof. - unfold flip; constructor; unfold flip. - - intros X. apply H. apply symmetry. apply X. - - unfold relation_conjunction. intros [H1 H2]. apply H. constructor; assumption. + firstorder. Qed. End Binary. diff --git a/theories/Classes/DecidableClass.v b/theories/Classes/DecidableClass.v index 7169aa673d..cd6765bab9 100644 --- a/theories/Classes/DecidableClass.v +++ b/theories/Classes/DecidableClass.v @@ -46,7 +46,7 @@ Qed. (** The generic function that should be used to program, together with some useful tactics. *) -Definition decide P {H : Decidable P} := Decidable_witness (Decidable:=H). +Definition decide P {H : Decidable P} := @Decidable_witness _ H. Ltac _decide_ P H := let b := fresh "b" in diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index d96bd72561..4d9069b4d0 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -64,8 +64,8 @@ Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv | 1. now transitivity y. Qed. -Arguments equiv_symmetric {A R} sa x y. -Arguments equiv_transitive {A R} sa x y z. +Arguments equiv_symmetric {A R} sa x y : rename. +Arguments equiv_transitive {A R} sa x y z : rename. (** Use the [substitute] command which substitutes an equivalence in every hypothesis. *) diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v index e9d434b488..ae1d978bfb 100644 --- a/theories/Logic/FunctionalExtensionality.v +++ b/theories/Logic/FunctionalExtensionality.v @@ -16,7 +16,7 @@ Lemma equal_f : forall {A B : Type} {f g : A -> B}, f = g -> forall x, f x = g x. Proof. - intros. + intros A B f g H x. rewrite H. auto. Qed. @@ -118,7 +118,7 @@ Definition f_equal__functional_extensionality_dep_good {A B f g} H a : f_equal (fun h => h a) (@functional_extensionality_dep_good A B f g H) = H a. Proof. - apply forall_eq_rect with (H := H); clear H g. + apply (fun P k => forall_eq_rect _ P k _ H); clear H g. change (eq_refl (f a)) with (f_equal (fun h => h a) (eq_refl f)). apply f_equal, functional_extensionality_dep_good_refl. Defined. diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index 7ee3a99d60..21eed3a696 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -39,8 +39,8 @@ Definition JMeq_hom {A : Type} (x y : A) := JMeq x y. Register JMeq_hom as core.JMeq.hom. Lemma JMeq_sym : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x. -Proof. -intros; destruct H; trivial. +Proof. +intros A B x y H; destruct H; trivial. Qed. #[global] @@ -150,7 +150,7 @@ Lemma JMeq_eq_dep : forall U (P:U->Type) p q (x:P p) (y:P q), p = q -> JMeq x y -> eq_dep U P p x q y. Proof. -intros. +intros U P p q x y H H0. destruct H. apply JMeq_eq in H0 as ->. reflexivity. diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index c469a49903..f324bbf52b 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -226,7 +226,7 @@ Proof. apply Z.lt_le_trans with (1:= H5); auto with zarith. apply Zpower_le_monotone; auto with zarith. rewrite Zplus_mod; auto with zarith. - rewrite -> Zmod_small with (a := t); auto with zarith. + rewrite -> (Zmod_small t); auto with zarith. apply Zmod_small; auto with zarith. split; auto with zarith. assert (0 <= 2 ^a * r); auto with zarith. @@ -489,15 +489,15 @@ Definition cast i j := Lemma cast_refl : forall i, cast i i = Some (fun P H => H). Proof. - unfold cast;intros. + unfold cast;intros i. generalize (eqb_correct i i). - rewrite eqb_refl;intros. + rewrite eqb_refl;intros e. rewrite (Eqdep_dec.eq_proofs_unicity eq_dec (e (eq_refl true)) (eq_refl i));trivial. Qed. Lemma cast_diff : forall i j, i =? j = false -> cast i j = None. Proof. - intros;unfold cast;intros; generalize (eqb_correct i j). + intros i j H;unfold cast;intros; generalize (eqb_correct i j). rewrite H;trivial. Qed. @@ -509,15 +509,15 @@ Definition eqo i j := Lemma eqo_refl : forall i, eqo i i = Some (eq_refl i). Proof. - unfold eqo;intros. + unfold eqo;intros i. generalize (eqb_correct i i). - rewrite eqb_refl;intros. + rewrite eqb_refl;intros e. rewrite (Eqdep_dec.eq_proofs_unicity eq_dec (e (eq_refl true)) (eq_refl i));trivial. Qed. Lemma eqo_diff : forall i j, i =? j = false -> eqo i j = None. Proof. - unfold eqo;intros; generalize (eqb_correct i j). + unfold eqo;intros i j H; generalize (eqb_correct i j). rewrite H;trivial. Qed. @@ -651,7 +651,7 @@ Proof. apply Zgcdn_is_gcd. unfold Zgcd_bound. generalize (to_Z_bounded b). - destruct φ b. + destruct φ b as [|p|p]. unfold size; auto with zarith. intros (_,H). cut (Psize p <= size)%nat; [ lia | rewrite <- Zpower2_Psize; auto]. @@ -727,7 +727,7 @@ Proof. replace ((φ m + φ n) mod wB)%Z with ((((φ m + φ n) - wB) + wB) mod wB)%Z. rewrite -> Zplus_mod, Z_mod_same_full, Zplus_0_r, !Zmod_small; auto with zarith. rewrite !Zmod_small; auto with zarith. - apply f_equal2 with (f := Zmod); auto with zarith. + apply (f_equal2 Zmod); auto with zarith. case_eq (n <=? m + n)%int63; auto. rewrite leb_spec, H1; auto with zarith. assert (H1: (φ (m + n) = φ m + φ n)%Z). @@ -805,7 +805,7 @@ Lemma lsl_add_distr x y n: (x + y) << n = ((x << n) + (y << n))%int63. Proof. apply to_Z_inj; rewrite -> !lsl_spec, !add_spec, Zmult_mod_idemp_l. rewrite -> !lsl_spec, <-Zplus_mod. - apply f_equal2 with (f := Zmod); auto with zarith. + apply (f_equal2 Zmod); auto with zarith. Qed. Lemma lsr_M_r x i (H: (digits <=? i = true)%int63) : x >> i = 0%int63. @@ -973,14 +973,14 @@ Proof. case H2; intros _ H3; case (Zle_or_lt φ i φ j); intros F2. 2: generalize (H3 F2); discriminate. clear H2 H3. - apply f_equal with (f := negb). - apply f_equal with (f := is_zero). + apply (f_equal negb). + apply (f_equal is_zero). apply to_Z_inj. rewrite -> !lsl_spec, !lsr_spec, !lsl_spec. pattern wB at 2 3; replace wB with (2^(1+ φ (digits - 1))); auto. rewrite -> Zpower_exp, Z.pow_1_r; auto with zarith. rewrite !Zmult_mod_distr_r. - apply f_equal2 with (f := Zmult); auto. + apply (f_equal2 Zmult); auto. replace wB with (2^ d); auto with zarith. replace d with ((d - φ i) + φ i)%Z by ring. case (to_Z_bounded i); intros H1i H2i. @@ -1078,8 +1078,8 @@ Proof. 2: generalize (Hn 0%int63); do 2 case bit; auto; intros [ ]; auto. rewrite lsl_add_distr. rewrite (bit_split x) at 1; rewrite (bit_split y) at 1. - rewrite <-!add_assoc; apply f_equal2 with (f := add); auto. - rewrite add_comm, <-!add_assoc; apply f_equal2 with (f := add); auto. + rewrite <-!add_assoc; apply (f_equal2 add); auto. + rewrite add_comm, <-!add_assoc; apply (f_equal2 add); auto. rewrite add_comm; auto. intros Heq. generalize (add_le_r x y); rewrite Heq, lor_le; intro Hb. @@ -1360,7 +1360,7 @@ Lemma sqrt2_step_def rec ih il j: else j else j. Proof. - unfold sqrt2_step; case diveucl_21; intros;simpl. + unfold sqrt2_step; case diveucl_21; intros i j';simpl. case (j +c i);trivial. Qed. @@ -1390,7 +1390,7 @@ Proof. assert (W1:= to_Z_bounded a1). assert (W2:= to_Z_bounded a2). assert (Wb:= to_Z_bounded b). - assert (φ b>0) by (auto with zarith). + assert (φ b>0) as H by (auto with zarith). generalize (Z_div_mod (φ a1*wB+φ a2) φ b H). revert W. destruct (diveucl_21 a1 a2 b); destruct (Z.div_eucl (φ a1*wB+φ a2) φ b). diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index d1be8812e9..69873d0321 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -43,7 +43,7 @@ Section Well_founded. forall (x:A) (r:Acc R x), F_sub x (fun y:{y:A | R y x} => Fix_F_sub (`y) (Acc_inv r (proj2_sig y))) = Fix_F_sub x r. Proof. - destruct r using Acc_inv_dep; auto. + intros x r; destruct r using Acc_inv_dep; auto. Qed. Lemma Fix_F_inv : forall (x:A) (r s:Acc R x), Fix_F_sub x r = Fix_F_sub x s. @@ -95,12 +95,12 @@ Section Measure_well_founded. Proof with auto. unfold well_founded. cut (forall (a: M) (a0: T), m a0 = a -> Acc MR a0). - + intros. + + intros H a. apply (H (m a))... + apply (@well_founded_ind M R wf (fun mm => forall a, m a = mm -> Acc MR a)). - intros. + intros ? H ? H0. apply Acc_intro. - intros. + intros y H1. unfold MR in H1. rewrite H0 in H1. apply (H (m y))... @@ -174,7 +174,7 @@ Section Fix_rects. revert a'. pattern x, (Fix_F_sub A R P f x a). apply Fix_F_sub_rect. - intros. + intros ? H **. rewrite F_unfold. apply equiv_lowers. intros. @@ -197,11 +197,11 @@ Section Fix_rects. : forall x, Q _ (Fix_sub A R Rwf P f x). Proof with auto. unfold Fix_sub. - intros. + intros x. apply Fix_F_sub_rect. - intros. - assert (forall y: A, R y x0 -> Q y (Fix_F_sub A R P f y (Rwf y)))... - set (inv x0 X0 a). clearbody q. + intros x0 H a. + assert (forall y: A, R y x0 -> Q y (Fix_F_sub A R P f y (Rwf y))) as X0... + set (q := inv x0 X0 a). clearbody q. rewrite <- (equiv_lowers (fun y: {y: A | R y x0} => Fix_F_sub A R P f (proj1_sig y) (Rwf (proj1_sig y))) (fun y: {y: A | R y x0} => Fix_F_sub A R P f (proj1_sig y) (Acc_inv a (proj2_sig y))))... @@ -242,9 +242,9 @@ Module WfExtensionality. Fix_sub A R Rwf P F_sub x = F_sub x (fun y:{y : A | R y x} => Fix_sub A R Rwf P F_sub (` y)). Proof. - intros ; apply Fix_eq ; auto. - intros. - assert(f = g). + intros A R Rwf P F_sub x; apply Fix_eq ; auto. + intros ? f g H. + assert(f = g) as H0. - extensionality y ; apply H. - rewrite H0 ; auto. Qed. diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index b008c6c2aa..4e596a165c 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -637,13 +637,13 @@ Qed. Lemma Qmult_1_l : forall n, 1*n == n. Proof. - intro; red; simpl; destruct (Qnum n); auto. + intro n; red; simpl; destruct (Qnum n); auto. Qed. Theorem Qmult_1_r : forall n, n*1==n. Proof. - intro; red; simpl. - rewrite Z.mul_1_r with (n := Qnum n). + intro n; red; simpl. + rewrite (Z.mul_1_r (Qnum n)). rewrite Pos.mul_comm; simpl; trivial. Qed. @@ -709,7 +709,7 @@ Qed. Theorem Qmult_inv_r : forall x, ~ x == 0 -> x*(/x) == 1. Proof. intros (x1, x2); unfold Qeq, Qdiv, Qmult; case x1; simpl; - intros; simpl_mult; try ring. + intros H **; simpl_mult; try ring. elim H; auto. Qed. @@ -722,7 +722,7 @@ Qed. Theorem Qdiv_mult_l : forall x y, ~ y == 0 -> (x*y)/y == x. Proof. - intros; unfold Qdiv. + intros x y H; unfold Qdiv. rewrite <- (Qmult_assoc x y (Qinv y)). rewrite (Qmult_inv_r y H). apply Qmult_1_r. @@ -730,7 +730,7 @@ Qed. Theorem Qmult_div_r : forall x y, ~ y == 0 -> y*(x/y) == x. Proof. - intros; unfold Qdiv. + intros x y ?; unfold Qdiv. rewrite (Qmult_assoc y x (Qinv y)). rewrite (Qmult_comm y x). fold (Qdiv (Qmult x y) y). @@ -845,7 +845,7 @@ Qed. Lemma Qlt_trans : forall x y z, x<y -> y<z -> x<z. Proof. - intros. + intros x y z ? ?. apply Qle_lt_trans with y; auto. apply Qlt_le_weak; auto. Qed. @@ -877,19 +877,19 @@ Hint Resolve Qle_not_lt Qlt_not_le Qnot_le_lt Qnot_lt_le Lemma Q_dec : forall x y, {x<y} + {y<x} + {x==y}. Proof. - unfold Qlt, Qle, Qeq; intros. + unfold Qlt, Qle, Qeq; intros x y. exact (Z_dec' (Qnum x * QDen y) (Qnum y * QDen x)). Defined. Lemma Qlt_le_dec : forall x y, {x<y} + {y<=x}. Proof. - unfold Qlt, Qle; intros. + unfold Qlt, Qle; intros x y. exact (Z_lt_le_dec (Qnum x * QDen y) (Qnum y * QDen x)). Defined. Lemma Qarchimedean : forall q : Q, { p : positive | q < Z.pos p # 1 }. Proof. - intros. destruct q as [a b]. destruct a. + intros q. destruct q as [a b]. destruct a as [|p|p]. - exists xH. reflexivity. - exists (p+1)%positive. apply (Z.lt_le_trans _ (Z.pos (p+1))). simpl. rewrite Pos.mul_1_r. @@ -1169,12 +1169,12 @@ Qed. Lemma Qinv_lt_contravar : forall a b : Q, 0 < a -> 0 < b -> (a < b <-> /b < /a). Proof. - intros. split. - - intro. rewrite <- Qmult_1_l. apply Qlt_shift_div_r. apply H0. + intros a b H H0. split. + - intro H1. rewrite <- Qmult_1_l. apply Qlt_shift_div_r. apply H0. rewrite <- (Qmult_inv_r a). rewrite Qmult_comm. apply Qmult_lt_l. apply Qinv_lt_0_compat. apply H. apply H1. intro abs. rewrite abs in H. apply (Qlt_irrefl 0 H). - - intro. rewrite <- (Qinv_involutive b). rewrite <- (Qmult_1_l (// b)). + - intro H1. rewrite <- (Qinv_involutive b). rewrite <- (Qmult_1_l (// b)). apply Qlt_shift_div_l. apply Qinv_lt_0_compat. apply H0. rewrite <- (Qmult_inv_r a). apply Qmult_lt_l. apply H. apply H1. intro abs. rewrite abs in H. apply (Qlt_irrefl 0 H). @@ -1190,7 +1190,7 @@ Instance Qpower_positive_comp : Proper (Qeq==>eq==>Qeq) Qpower_positive. Proof. intros x x' Hx y y' Hy. rewrite <-Hy; clear y' Hy. unfold Qpower_positive. -induction y; simpl; +induction y as [y IHy|y IHy|]; simpl; try rewrite IHy; try rewrite Hx; reflexivity. diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index 533c675415..e94ae1e789 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -129,19 +129,19 @@ Qed. Add Morphism Qplus' with signature (Qeq ==> Qeq ==> Qeq) as Qplus'_comp. Proof. - intros; unfold Qplus'. + intros ? ? H ? ? H0; unfold Qplus'. rewrite H, H0; auto with qarith. Qed. Add Morphism Qmult' with signature (Qeq ==> Qeq ==> Qeq) as Qmult'_comp. Proof. - intros; unfold Qmult'. + intros ? ? H ? ? H0; unfold Qmult'. rewrite H, H0; auto with qarith. Qed. Add Morphism Qminus' with signature (Qeq ==> Qeq ==> Qeq) as Qminus'_comp. Proof. - intros; unfold Qminus'. + intros ? ? H ? ? H0; unfold Qminus'. rewrite H, H0; auto with qarith. Qed. diff --git a/theories/ZArith/Zgcd_alt.v b/theories/ZArith/Zgcd_alt.v index 9a1bbca99f..c11077607e 100644 --- a/theories/ZArith/Zgcd_alt.v +++ b/theories/ZArith/Zgcd_alt.v @@ -58,9 +58,9 @@ Open Scope Z_scope. Lemma Zgcdn_pos : forall n a b, 0 <= Zgcdn n a b. Proof. - induction n. + intros n; induction n. simpl; auto with zarith. - destruct a; simpl; intros; auto with zarith; auto. + intros a; destruct a; simpl; intros; auto with zarith; auto. Qed. Lemma Zgcd_alt_pos : forall a b, 0 <= Zgcd_alt a b. @@ -75,9 +75,9 @@ Open Scope Z_scope. Lemma Zgcdn_linear_bound : forall n a b, Z.abs a < Z.of_nat n -> Zis_gcd a b (Zgcdn n a b). Proof. - induction n. + intros n; induction n as [|n IHn]. intros; lia. - destruct a; intros; simpl; + intros a; destruct a as [|p|p]; intros b H; simpl; [ generalize (Zis_gcd_0_abs b); intuition | | ]; unfold Z.modulo; generalize (Z_div_mod b (Zpos p) (eq_refl Gt)); @@ -106,7 +106,7 @@ Open Scope Z_scope. Lemma fibonacci_pos : forall n, 0 <= fibonacci n. Proof. enough (forall N n, (n<N)%nat -> 0<=fibonacci n) by eauto. - induction N. intros; lia. + intros N; induction N as [|N IHN]. intros; lia. intros [ | [ | n ] ]. 1-2: simpl; lia. intros. change (0 <= fibonacci (S n) + fibonacci n). @@ -116,11 +116,11 @@ Open Scope Z_scope. Lemma fibonacci_incr : forall n m, (n<=m)%nat -> fibonacci n <= fibonacci m. Proof. - induction 1. + induction 1 as [|m H IH]. auto with zarith. apply Z.le_trans with (fibonacci m); auto. clear. - destruct m. + destruct m as [|m]. simpl; auto with zarith. change (fibonacci (S m) <= fibonacci (S m)+fibonacci m). generalize (fibonacci_pos m); lia. @@ -137,10 +137,10 @@ Open Scope Z_scope. fibonacci (S n) <= a /\ fibonacci (S (S n)) <= b. Proof. - induction n. + intros n; induction n as [|n IHn]. intros [|a|a]; intros; simpl; lia. intros [|a|a] b (Ha,Ha'); [simpl; lia | | easy ]. - remember (S n) as m. + remember (S n) as m eqn:Heqm. rewrite Heqm at 2. simpl Zgcdn. unfold Z.modulo; generalize (Z_div_mod b (Zpos a) eq_refl). destruct (Z.div_eucl b (Zpos a)) as (q,r). @@ -171,19 +171,19 @@ Open Scope Z_scope. 0 < a < b -> a < fibonacci (S n) -> Zis_gcd a b (Zgcdn n a b). Proof. - destruct a. 1,3 : intros; lia. + intros n a; destruct a as [|p|p]. 1,3 : intros; lia. cut (forall k n b, k = (S (Pos.to_nat p) - n)%nat -> 0 < Zpos p < b -> Zpos p < fibonacci (S n) -> Zis_gcd (Zpos p) b (Zgcdn n (Zpos p) b)). destruct 2; eauto. - clear n; induction k. + clear n; intros k; induction k as [|k IHk]. intros. apply Zgcdn_linear_bound. lia. - intros. - generalize (Zgcdn_worst_is_fibonacci n (Zpos p) b H0); intros. - assert (Zis_gcd (Zpos p) b (Zgcdn (S n) (Zpos p) b)). + intros n b H H0 H1. + generalize (Zgcdn_worst_is_fibonacci n (Zpos p) b H0); intros H2. + assert (Zis_gcd (Zpos p) b (Zgcdn (S n) (Zpos p) b)) as H3. apply IHk; auto. lia. replace (fibonacci (S (S n))) with (fibonacci (S n)+fibonacci n) by auto. @@ -197,13 +197,13 @@ Open Scope Z_scope. Lemma Zgcd_bound_fibonacci : forall a, 0 < a -> a < fibonacci (Zgcd_bound a). Proof. - destruct a; [lia| | intro H; discriminate]. + intros a; destruct a as [|p|p]; [lia| | intro H; discriminate]. intros _. - induction p; [ | | compute; auto ]; + induction p as [p IHp|p IHp|]; [ | | compute; auto ]; simpl Zgcd_bound in *; rewrite plus_comm; simpl plus; set (n:= (Pos.size_nat p+Pos.size_nat p)%nat) in *; simpl; - assert (n <> O) by (unfold n; destruct p; simpl; auto). + assert (n <> O) as H by (unfold n; destruct p; simpl; auto). destruct n as [ |m]; [elim H; auto| ]. generalize (fibonacci_pos m); rewrite Pos2Z.inj_xI; lia. @@ -229,11 +229,11 @@ Open Scope Z_scope. Lemma Zgcdn_is_gcd_pos n a b : (Zgcd_bound (Zpos a) <= n)%nat -> Zis_gcd (Zpos a) b (Zgcdn n (Zpos a) b). Proof. - intros. + intros H. generalize (Zgcd_bound_fibonacci (Zpos a)). simpl Zgcd_bound in *. - remember (Pos.size_nat a+Pos.size_nat a)%nat as m. - assert (1 < m)%nat. + remember (Pos.size_nat a+Pos.size_nat a)%nat as m eqn:Heqm. + assert (1 < m)%nat as H0. { rewrite Heqm; destruct a; simpl; rewrite 1?plus_comm; auto with arith. } destruct m as [ |m]; [inversion H0; auto| ]. diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v index b69af424b1..bc3f5706c9 100644 --- a/theories/ZArith/Zpow_facts.v +++ b/theories/ZArith/Zpow_facts.v @@ -83,10 +83,10 @@ Proof. intros. apply Z.lt_le_incl. now apply Z.pow_gt_lin_r. Qed. Lemma Zpower2_Psize n p : Zpos p < 2^(Z.of_nat n) <-> (Pos.size_nat p <= n)%nat. Proof. - revert p; induction n. - destruct p; now split. + revert p; induction n as [|n IHn]. + intros p; destruct p; now split. assert (Hn := Nat2Z.is_nonneg n). - destruct p; simpl Pos.size_nat. + intros p; destruct p as [p|p|]; simpl Pos.size_nat. - specialize IHn with p. rewrite Nat2Z.inj_succ, Z.pow_succ_r; lia. - specialize IHn with p. @@ -138,7 +138,7 @@ Definition Zpow_mod a m n := Theorem Zpow_mod_pos_correct a m n : n <> 0 -> Zpow_mod_pos a m n = (Z.pow_pos a m) mod n. Proof. - intros Hn. induction m. + intros Hn. induction m as [m IHm|m IHm|]. - rewrite Pos.xI_succ_xO at 2. rewrite <- Pos.add_1_r, <- Pos.add_diag. rewrite 2 Zpower_pos_is_exp, Zpower_pos_1_r. rewrite Z.mul_mod, (Z.mul_mod (Z.pow_pos a m)) by trivial. @@ -193,7 +193,7 @@ Proof. assert (p<=1) by (apply Z.divide_pos_le; auto with zarith). lia. - intros n Hn Rec. - rewrite Z.pow_succ_r by trivial. intros. + rewrite Z.pow_succ_r by trivial. intros H. assert (2<=p) by (apply prime_ge_2; auto). assert (2<=q) by (apply prime_ge_2; auto). destruct prime_mult with (2 := H); auto. @@ -229,7 +229,7 @@ Proof. (* x = 1 *) exists 0; rewrite Z.pow_0_r; auto. (* x = 0 *) - exists n; destruct H; rewrite Z.mul_0_r in H; auto. + exists n; destruct H as [? H]; rewrite Z.mul_0_r in H; auto. Qed. (** * Z.square: a direct definition of [z^2] *) diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v index 6f464d89bb..6b01d798e4 100644 --- a/theories/ZArith/Zpower.v +++ b/theories/ZArith/Zpower.v @@ -42,7 +42,7 @@ Lemma Zpower_nat_is_exp : forall (n m:nat) (z:Z), Zpower_nat z (n + m) = Zpower_nat z n * Zpower_nat z m. Proof. - induction n. + intros n; induction n as [|n IHn]. - intros. now rewrite Zpower_nat_0_r, Z.mul_1_l. - intros. simpl. now rewrite IHn, Z.mul_assoc. Qed. @@ -135,7 +135,7 @@ Section Powers_of_2. Lemma two_power_nat_equiv n : two_power_nat n = 2 ^ (Z.of_nat n). Proof. - induction n. + induction n as [|n IHn]. - trivial. - now rewrite Nat2Z.inj_succ, Z.pow_succ_r, <- IHn by apply Nat2Z.is_nonneg. Qed. @@ -164,7 +164,7 @@ Section Powers_of_2. Theorem shift_nat_correct n x : Zpos (shift_nat n x) = Zpower_nat 2 n * Zpos x. Proof. - induction n. + induction n as [|n IHn]. - trivial. - now rewrite Zpower_nat_succ_r, <- Z.mul_assoc, <- IHn. Qed. @@ -295,7 +295,7 @@ Section power_div_with_rest. rewrite Z.mul_sub_distr_r, Z.mul_shuffle3, Z.mul_assoc. repeat split; auto. rewrite !Z.mul_1_l, H, Z.add_assoc. - apply f_equal2 with (f := Z.add); auto. + apply (f_equal2 Z.add); auto. rewrite <- Z.sub_sub_distr, <- !Z.add_diag, Z.add_simpl_r. now rewrite Z.mul_1_l. - rewrite Pos2Z.neg_xO in H. @@ -303,7 +303,7 @@ Section power_div_with_rest. repeat split; auto. - repeat split; auto. rewrite H, (Z.mul_opp_l 1), Z.mul_1_l, Z.add_assoc. - apply f_equal2 with (f := Z.add); auto. + apply (f_equal2 Z.add); auto. rewrite Z.add_comm, <- Z.add_diag. rewrite Z.mul_add_distr_l. replace (-1 * d) with (-d). diff --git a/theories/micromega/Tauto.v b/theories/micromega/Tauto.v index 515372466a..e4129f8382 100644 --- a/theories/micromega/Tauto.v +++ b/theories/micromega/Tauto.v @@ -1371,13 +1371,13 @@ Section S. destruct pol;auto. generalize (is_cnf_tt_inv (xcnf (negb true) f1)). destruct (is_cnf_tt (xcnf (negb true) f1)). - + intros. + + intros H. rewrite H by auto. reflexivity. + generalize (is_cnf_ff_inv (xcnf (negb true) f1)). destruct (is_cnf_ff (xcnf (negb true) f1)). - * intros. + * intros H. rewrite H by auto. unfold or_cnf_opt. simpl. diff --git a/theories/micromega/ZMicromega.v b/theories/micromega/ZMicromega.v index 1616b5a2a4..a4b631fc13 100644 --- a/theories/micromega/ZMicromega.v +++ b/theories/micromega/ZMicromega.v @@ -38,7 +38,7 @@ Ltac inv H := inversion H ; try subst ; clear H. Lemma eq_le_iff : forall x, 0 = x <-> (0 <= x /\ x <= 0). Proof. intros. - split ; intros. + split ; intros H. - subst. compute. intuition congruence. - destruct H. @@ -48,7 +48,7 @@ Qed. Lemma lt_le_iff : forall x, 0 < x <-> 0 <= x - 1. Proof. - split ; intros. + split ; intros H. - apply Zlt_succ_le. ring_simplify. auto. @@ -70,12 +70,13 @@ Lemma le_neg : forall x, Proof. intro. rewrite lt_le_iff. - split ; intros. + split ; intros H. - apply Znot_le_gt in H. apply Zgt_le_succ in H. rewrite le_0_iff in H. ring_simplify in H; auto. - - assert (C := (Z.add_le_mono _ _ _ _ H H0)). + - intro H0. + assert (C := (Z.add_le_mono _ _ _ _ H H0)). ring_simplify in C. compute in C. apply C ; reflexivity. @@ -84,7 +85,7 @@ Qed. Lemma eq_cnf : forall x, (0 <= x - 1 -> False) /\ (0 <= -1 - x -> False) <-> x = 0. Proof. - intros. + intros x. rewrite Z.eq_sym_iff. rewrite eq_le_iff. rewrite (le_0_iff x 0). @@ -108,7 +109,7 @@ Proof. auto using Z.le_antisymm. eauto using Z.le_trans. apply Z.le_neq. - destruct (Z.lt_trichotomy n m) ; intuition. + apply Z.lt_trichotomy. apply Z.add_le_mono_l; assumption. apply Z.mul_pos_pos ; auto. discriminate. @@ -160,18 +161,18 @@ Fixpoint Zeval_const (e: PExpr Z) : option Z := Lemma ZNpower : forall r n, r ^ Z.of_N n = pow_N 1 Z.mul r n. Proof. - destruct n. + intros r n; destruct n as [|p]. reflexivity. simpl. unfold Z.pow_pos. replace (pow_pos Z.mul r p) with (1 * (pow_pos Z.mul r p)) by ring. generalize 1. - induction p; simpl ; intros ; repeat rewrite IHp ; ring. + induction p as [p IHp|p IHp|]; simpl ; intros ; repeat rewrite IHp ; ring. Qed. Lemma Zeval_expr_compat : forall env e, Zeval_expr env e = eval_expr env e. Proof. - induction e ; simpl ; try congruence. + intros env e; induction e ; simpl ; try congruence. reflexivity. rewrite ZNpower. congruence. Qed. @@ -201,7 +202,7 @@ Lemma pop2_bop2 : forall (op : Op2) (q1 q2 : Z), is_true (Zeval_bop2 op q1 q2) <-> Zeval_pop2 op q1 q2. Proof. unfold is_true. - destruct op ; simpl; intros. + intro op; destruct op ; simpl; intros q1 q2. - apply Z.eqb_eq. - rewrite <- Z.eqb_eq. rewrite negb_true_iff. @@ -220,7 +221,7 @@ Definition Zeval_op2 (k: Tauto.kind) : Op2 -> Z -> Z -> Tauto.rtyp k:= Lemma Zeval_op2_hold : forall k op q1 q2, Tauto.hold k (Zeval_op2 k op q1 q2) <-> Zeval_pop2 op q1 q2. Proof. - destruct k. + intro k; destruct k. simpl ; tauto. simpl. apply pop2_bop2. Qed. @@ -235,18 +236,18 @@ Definition Zeval_formula' := Lemma Zeval_formula_compat : forall env k f, Tauto.hold k (Zeval_formula env k f) <-> Zeval_formula env Tauto.isProp f. Proof. - destruct k ; simpl. + intros env k; destruct k ; simpl. - tauto. - - destruct f ; simpl. - rewrite <- Zeval_op2_hold with (k:=Tauto.isBool). + - intros f; destruct f ; simpl. + rewrite <- (Zeval_op2_hold Tauto.isBool). simpl. tauto. Qed. Lemma Zeval_formula_compat' : forall env f, Zeval_formula env Tauto.isProp f <-> Zeval_formula' env f. Proof. - intros. + intros env f. unfold Zeval_formula. - destruct f. + destruct f as [Flhs Fop Frhs]. repeat rewrite Zeval_expr_compat. unfold Zeval_formula' ; simpl. unfold eval_expr. @@ -343,7 +344,7 @@ Lemma Zunsat_sound : forall f, Zunsat f = true -> forall env, eval_nformula env f -> False. Proof. unfold Zunsat. - intros. + intros f H env ?. destruct f. eapply check_inconsistent_sound with (1 := Zsor) (2 := ZSORaddon) in H; eauto. Qed. @@ -365,7 +366,7 @@ Lemma xnnormalise_correct : forall env f, eval_nformula env (xnnormalise f) <-> Zeval_formula env Tauto.isProp f. Proof. - intros. + intros env f. rewrite Zeval_formula_compat'. unfold xnnormalise. destruct f as [lhs o rhs]. @@ -375,18 +376,18 @@ Proof. generalize ( eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x) (fun x : N => x) (pow_N 1 Z.mul) env lhs); generalize (eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x) - (fun x : N => x) (pow_N 1 Z.mul) env rhs); intros. + (fun x : N => x) (pow_N 1 Z.mul) env rhs); intros z z0. - split ; intros. - + assert (z0 + (z - z0) = z0 + 0) by congruence. + + assert (z0 + (z - z0) = z0 + 0) as H0 by congruence. rewrite Z.add_0_r in H0. rewrite <- H0. ring. + subst. ring. - - split ; repeat intro. + - split ; intros H H0. subst. apply H. ring. apply H. - assert (z0 + (z - z0) = z0 + 0) by congruence. + assert (z0 + (z - z0) = z0 + 0) as H1 by congruence. rewrite Z.add_0_r in H1. rewrite <- H1. ring. @@ -396,11 +397,11 @@ Proof. - split ; intros. + apply Zle_0_minus_le; auto. + apply Zle_minus_le_0; auto. - - split ; intros. + - split ; intros H. + apply Zlt_0_minus_lt; auto. + apply Zlt_left_lt in H. apply H. - - split ; intros. + - split ; intros H. + apply Zlt_0_minus_lt ; auto. + apply Zlt_left_lt in H. apply H. @@ -430,7 +431,7 @@ Ltac iff_ring := Lemma xnormalise_correct : forall env f, (make_conj (fun x => eval_nformula env x -> False) (xnormalise f)) <-> eval_nformula env f. Proof. - intros. + intros env f. destruct f as [e o]; destruct o eqn:Op; cbn - [psub]; repeat rewrite eval_pol_sub; fold eval_pol; repeat rewrite eval_pol_Pc; generalize (eval_pol env e) as x; intro. @@ -458,11 +459,11 @@ Lemma cnf_of_list_correct : make_conj (fun x : NFormula Z => eval_nformula env x -> False) f. Proof. unfold cnf_of_list. - intros. + intros T tg f env. set (F := (fun (x : NFormula Z) (acc : list (list (NFormula Z * T))) => if Zunsat x then acc else ((x, tg) :: nil) :: acc)). set (E := ((fun x : NFormula Z => eval_nformula env x -> False))). - induction f. + induction f as [|a f IHf]. - compute. tauto. - rewrite make_conj_cons. @@ -489,10 +490,10 @@ Definition normalise {T : Type} (t:Formula Z) (tg:T) : cnf (NFormula Z) T := Lemma normalise_correct : forall (T: Type) env t (tg:T), eval_cnf eval_nformula env (normalise t tg) <-> Zeval_formula env Tauto.isProp t. Proof. - intros. + intros T env t tg. rewrite <- xnnormalise_correct. unfold normalise. - generalize (xnnormalise t) as f;intro. + generalize (xnnormalise t) as f;intro f. destruct (Zunsat f) eqn:U. - assert (US := Zunsat_sound _ U env). rewrite eval_cnf_ff. @@ -519,10 +520,10 @@ Definition negate {T : Type} (t:Formula Z) (tg:T) : cnf (NFormula Z) T := Lemma xnegate_correct : forall env f, (make_conj (fun x => eval_nformula env x -> False) (xnegate f)) <-> ~ eval_nformula env f. Proof. - intros. + intros env f. destruct f as [e o]; destruct o eqn:Op; cbn - [psub]; repeat rewrite eval_pol_sub; fold eval_pol; repeat rewrite eval_pol_Pc; - generalize (eval_pol env e) as x; intro. + generalize (eval_pol env e) as x; intro x. - tauto. - rewrite eq_cnf. destruct (Z.eq_decidable x 0);tauto. @@ -533,10 +534,10 @@ Qed. Lemma negate_correct : forall T env t (tg:T), eval_cnf eval_nformula env (negate t tg) <-> ~ Zeval_formula env Tauto.isProp t. Proof. - intros. + intros T env t tg. rewrite <- xnnormalise_correct. unfold negate. - generalize (xnnormalise t) as f;intro. + generalize (xnnormalise t) as f;intro f. destruct (Zunsat f) eqn:U. - assert (US := Zunsat_sound _ U env). rewrite eval_cnf_tt. @@ -569,10 +570,10 @@ Require Import Znumtheory. Lemma Zdivide_ceiling : forall a b, (b | a) -> ceiling a b = Z.div a b. Proof. unfold ceiling. - intros. + intros a b H. apply Zdivide_mod in H. case_eq (Z.div_eucl a b). - intros. + intros z z0 H0. change z with (fst (z,z0)). rewrite <- H0. change (fst (Z.div_eucl a b)) with (Z.div a b). @@ -642,12 +643,12 @@ Definition isZ0 (x:Z) := Lemma isZ0_0 : forall x, isZ0 x = true <-> x = 0. Proof. - destruct x ; simpl ; intuition congruence. + intros x; destruct x ; simpl ; intuition congruence. Qed. Lemma isZ0_n0 : forall x, isZ0 x = false <-> x <> 0. Proof. - destruct x ; simpl ; intuition congruence. + intros x; destruct x ; simpl ; intuition congruence. Qed. Definition ZgcdM (x y : Z) := Z.max (Z.gcd x y) 1. @@ -682,8 +683,8 @@ Inductive Zdivide_pol (x:Z): PolC Z -> Prop := Lemma Zdiv_pol_correct : forall a p, 0 < a -> Zdivide_pol a p -> forall env, eval_pol env p = a * eval_pol env (Zdiv_pol p a). Proof. - intros until 2. - induction H0. + intros a p H H0. + induction H0 as [? ?|? ? IHZdivide_pol j|? ? ? IHZdivide_pol1 ? IHZdivide_pol2 j]. (* Pc *) simpl. intros. @@ -702,7 +703,7 @@ Qed. Lemma Zgcd_pol_ge : forall p, fst (Zgcd_pol p) >= 0. Proof. - induction p. 1-2: easy. + intros p; induction p as [c|p p1 IHp1|p1 IHp1 ? p3 IHp3]. 1-2: easy. simpl. case_eq (Zgcd_pol p1). case_eq (Zgcd_pol p3). @@ -715,7 +716,7 @@ Qed. Lemma Zdivide_pol_Zdivide : forall p x y, Zdivide_pol x p -> (y | x) -> Zdivide_pol y p. Proof. - intros. + intros p x y H H0. induction H. constructor. apply Z.divide_trans with (1:= H0) ; assumption. @@ -725,7 +726,7 @@ Qed. Lemma Zdivide_pol_one : forall p, Zdivide_pol 1 p. Proof. - induction p ; constructor ; auto. + intros p; induction p as [c| |]; constructor ; auto. exists c. ring. Qed. @@ -744,19 +745,19 @@ Lemma Zdivide_pol_sub : forall p a b, Zdivide_pol a (PsubC Z.sub p b) -> Zdivide_pol (Z.gcd a b) p. Proof. - induction p. + intros p; induction p as [c|? p IHp|p ? ? ? IHp2]. simpl. - intros. inversion H0. + intros a b H H0. inversion H0. constructor. apply Zgcd_minus ; auto. - intros. + intros ? ? H H0. constructor. simpl in H0. inversion H0 ; subst; clear H0. apply IHp ; auto. - simpl. intros. + simpl. intros a b H H0. inv H0. constructor. - apply Zdivide_pol_Zdivide with (1:= H3). + apply Zdivide_pol_Zdivide with (1:= (ltac:(assumption) : Zdivide_pol a p)). destruct (Zgcd_is_gcd a b) ; assumption. apply IHp2 ; assumption. Qed. @@ -765,15 +766,15 @@ Lemma Zdivide_pol_sub_0 : forall p a, Zdivide_pol a (PsubC Z.sub p 0) -> Zdivide_pol a p. Proof. - induction p. + intros p; induction p as [c|? p IHp|? IHp1 ? ? IHp2]. simpl. - intros. inversion H. + intros ? H. inversion H. constructor. rewrite Z.sub_0_r in *. assumption. - intros. + intros ? H. constructor. simpl in H. inversion H ; subst; clear H. apply IHp ; auto. - simpl. intros. + simpl. intros ? H. inv H. constructor. auto. apply IHp2 ; assumption. @@ -783,9 +784,9 @@ Qed. Lemma Zgcd_pol_div : forall p g c, Zgcd_pol p = (g, c) -> Zdivide_pol g (PsubC Z.sub p c). Proof. - induction p ; simpl. + intros p; induction p as [c|? ? IHp|p1 IHp1 ? p3 IHp2]; simpl. (* Pc *) - intros. inv H. + intros ? ? H. inv H. constructor. exists 0. now ring. (* Pinj *) @@ -793,28 +794,28 @@ Proof. constructor. apply IHp ; auto. (* PX *) intros g c. - case_eq (Zgcd_pol p1) ; case_eq (Zgcd_pol p3) ; intros. + case_eq (Zgcd_pol p1) ; case_eq (Zgcd_pol p3) ; intros z z0 H z1 z2 H0 H1. inv H1. unfold ZgcdM at 1. destruct (Zmax_spec (Z.gcd (ZgcdM z1 z2) z) 1) as [HH1 | HH1]; destruct HH1 as [HH1 HH1'] ; rewrite HH1'. constructor. - apply Zdivide_pol_Zdivide with (x:= ZgcdM z1 z2). + apply (Zdivide_pol_Zdivide _ (ZgcdM z1 z2)). unfold ZgcdM. destruct (Zmax_spec (Z.gcd z1 z2) 1) as [HH2 | HH2]. - destruct HH2. + destruct HH2 as [H1 H2]. rewrite H2. apply Zdivide_pol_sub ; auto. apply Z.lt_le_trans with 1. reflexivity. now apply Z.ge_le. - destruct HH2. rewrite H2. + destruct HH2 as [H1 H2]. rewrite H2. apply Zdivide_pol_one. unfold ZgcdM in HH1. unfold ZgcdM. destruct (Zmax_spec (Z.gcd z1 z2) 1) as [HH2 | HH2]. - destruct HH2. rewrite H2 in *. + destruct HH2 as [H1 H2]. rewrite H2 in *. destruct (Zgcd_is_gcd (Z.gcd z1 z2) z); auto. - destruct HH2. rewrite H2. + destruct HH2 as [H1 H2]. rewrite H2. destruct (Zgcd_is_gcd 1 z); auto. - apply Zdivide_pol_Zdivide with (x:= z). + apply (Zdivide_pol_Zdivide _ z). apply (IHp2 _ _ H); auto. destruct (Zgcd_is_gcd (ZgcdM z1 z2) z); auto. constructor. apply Zdivide_pol_one. @@ -873,7 +874,7 @@ Definition is_pol_Z0 (p : PolC Z) : bool := Lemma is_pol_Z0_eval_pol : forall p, is_pol_Z0 p = true -> forall env, eval_pol env p = 0. Proof. unfold is_pol_Z0. - destruct p ; try discriminate. + intros p; destruct p as [z| |]; try discriminate. destruct z ; try discriminate. reflexivity. Qed. @@ -915,8 +916,8 @@ Fixpoint max_var (jmp : positive) (p : Pol Z) : positive := Lemma pos_le_add : forall y x, (x <= y + x)%positive. Proof. - intros. - assert ((Z.pos x) <= Z.pos (x + y))%Z. + intros y x. + assert ((Z.pos x) <= Z.pos (x + y))%Z as H. rewrite <- (Z.add_0_r (Zpos x)). rewrite <- Pos2Z.add_pos_pos. apply Z.add_le_mono_l. @@ -929,10 +930,10 @@ Qed. Lemma max_var_le : forall p v, (v <= max_var v p)%positive. Proof. - induction p; simpl. + intros p; induction p as [?|p ? IHp|? IHp1 ? ? IHp2]; simpl. - intros. apply Pos.le_refl. - - intros. + - intros v. specialize (IHp (p+v)%positive). eapply Pos.le_trans ; eauto. assert (xH + v <= p + v)%positive. @@ -942,7 +943,7 @@ Proof. } eapply Pos.le_trans ; eauto. apply pos_le_add. - - intros. + - intros v. apply Pos.max_case_strong;intros ; auto. specialize (IHp2 (Pos.succ v)%positive). eapply Pos.le_trans ; eauto. @@ -951,10 +952,10 @@ Qed. Lemma max_var_correct : forall p j v, In v (vars j p) -> Pos.le v (max_var j p). Proof. - induction p; simpl. + intros p; induction p; simpl. - tauto. - auto. - - intros. + - intros j v H. rewrite in_app_iff in H. destruct H as [H |[ H | H]]. + subst. @@ -980,7 +981,7 @@ Section MaxVar. (v <= acc -> v <= fold_left F l acc)%positive. Proof. - induction l ; simpl ; [easy|]. + intros l; induction l as [|a l IHl] ; simpl ; [easy|]. intros. apply IHl. unfold F. @@ -993,7 +994,7 @@ Section MaxVar. (acc <= acc' -> fold_left F l acc <= fold_left F l acc')%positive. Proof. - induction l ; simpl ; [easy|]. + intros l; induction l as [|a l IHl]; simpl ; [easy|]. intros. apply IHl. unfold F. @@ -1006,13 +1007,13 @@ Section MaxVar. Lemma max_var_nformulae_correct_aux : forall l p o v, In (p,o) l -> In v (vars xH p) -> Pos.le v (fold_left F l 1)%positive. Proof. - intros. + intros l p o v H H0. generalize 1%positive as acc. revert p o v H H0. - induction l. + induction l as [|a l IHl]. - simpl. tauto. - simpl. - intros. + intros p o v H H0 ?. destruct H ; subst. + unfold F at 2. simpl. @@ -1128,14 +1129,14 @@ Require Import Wf_nat. Lemma in_bdepth : forall l a b y, In y l -> ltof ZArithProof bdepth y (EnumProof a b l). Proof. - induction l. + intros l; induction l as [|a l IHl]. (* nil *) simpl. tauto. (* cons *) simpl. - intros. - destruct H. + intros a0 b y H. + destruct H as [H|H]. subst. unfold ltof. simpl. @@ -1180,8 +1181,8 @@ Lemma eval_Psatz_sound : forall env w l f', make_conj (eval_nformula env) l -> eval_Psatz l w = Some f' -> eval_nformula env f'. Proof. - intros. - apply (eval_Psatz_Sound Zsor ZSORaddon) with (l:=l) (e:= w) ; auto. + intros env w l f' H H0. + apply (fun H => eval_Psatz_Sound Zsor ZSORaddon l _ H w) ; auto. apply make_conj_in ; auto. Qed. @@ -1193,7 +1194,7 @@ Proof. unfold nformula_of_cutting_plane. unfold eval_nformula. unfold RingMicromega.eval_nformula. unfold eval_op1. - intros. + intros env e e' c H H0. rewrite (RingMicromega.eval_pol_add Zsor ZSORaddon). simpl. (**) @@ -1201,10 +1202,10 @@ Proof. revert H0. case_eq (Zgcd_pol e) ; intros g c0. generalize (Zgt_cases g 0) ; destruct (Z.gtb g 0). - intros. + intros H0 H1 H2. inv H2. change (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x)) with eval_pol in *. - apply Zgcd_pol_correct_lt with (env:=env) in H1. 2: auto using Z.gt_lt. + apply (Zgcd_pol_correct_lt _ env) in H1. 2: auto using Z.gt_lt. apply Z.le_add_le_sub_l, Z.ge_le; rewrite Z.add_0_r. apply (narrow_interval_lower_bound g (- c0) (eval_pol env (Zdiv_pol (PsubC Z.sub e c0) g)) H0). apply Z.le_ge. @@ -1213,7 +1214,7 @@ Proof. rewrite <- H1. assumption. (* g <= 0 *) - intros. inv H2. auto with zarith. + intros H0 H1 H2. inv H2. auto with zarith. Qed. Lemma cutting_plane_sound : forall env f p, @@ -1222,34 +1223,34 @@ Lemma cutting_plane_sound : forall env f p, eval_nformula env (nformula_of_cutting_plane p). Proof. unfold genCuttingPlane. - destruct f as [e op]. + intros env f; destruct f as [e op]. destruct op. (* Equal *) - destruct p as [[e' z] op]. + intros p; destruct p as [[e' z] op]. case_eq (Zgcd_pol e) ; intros g c. case_eq (Z.gtb g 0 && (negb (Zeq_bool c 0) && negb (Zeq_bool (Z.gcd g c) g))) ; [discriminate|]. case_eq (makeCuttingPlane e). - intros. + intros ? ? H H0 H1 H2 H3. inv H3. unfold makeCuttingPlane in H. rewrite H1 in H. revert H. change (eval_pol env e = 0) in H2. case_eq (Z.gtb g 0). - intros. - rewrite <- Zgt_is_gt_bool in H. + intros H H3. + rewrite <- Zgt_is_gt_bool in H. rewrite Zgcd_pol_correct_lt with (1:= H1) in H2. 2: auto using Z.gt_lt. - unfold nformula_of_cutting_plane. + unfold nformula_of_cutting_plane. change (eval_pol env (padd e' (Pc z)) = 0). inv H3. rewrite eval_pol_add. set (x:=eval_pol env (Zdiv_pol (PsubC Z.sub e c) g)) in *; clearbody x. simpl. rewrite andb_false_iff in H0. - destruct H0. + destruct H0 as [H0|H0]. rewrite Zgt_is_gt_bool in H ; congruence. rewrite andb_false_iff in H0. - destruct H0. + destruct H0 as [H0|H0]. rewrite negb_false_iff in H0. apply Zeq_bool_eq in H0. subst. simpl. @@ -1259,13 +1260,13 @@ Proof. apply Zeq_bool_eq in H0. assert (HH := Zgcd_is_gcd g c). rewrite H0 in HH. - inv HH. + destruct HH as [H3 H4 ?]. apply Zdivide_opp_r in H4. rewrite Zdivide_ceiling ; auto. apply Z.sub_move_0_r. apply Z.div_unique_exact. now intros ->. now rewrite Z.add_move_0_r in H2. - intros. + intros H H3. unfold nformula_of_cutting_plane. inv H3. change (eval_pol env (padd e' (Pc 0)) = 0). @@ -1273,7 +1274,7 @@ Proof. simpl. now rewrite Z.add_0_r. (* NonEqual *) - intros. + intros ? H H0. inv H0. unfold eval_nformula in *. unfold RingMicromega.eval_nformula in *. @@ -1282,20 +1283,20 @@ Proof. rewrite (RingMicromega.eval_pol_add Zsor ZSORaddon). simpl. now rewrite Z.add_0_r. (* Strict *) - destruct p as [[e' z] op]. + intros p; destruct p as [[e' z] op]. case_eq (makeCuttingPlane (PsubC Z.sub e 1)). - intros. + intros ? ? H H0 H1. inv H1. - apply makeCuttingPlane_ns_sound with (env:=env) (2:= H). + apply (makeCuttingPlane_ns_sound env) with (2:= H). simpl in *. rewrite (RingMicromega.PsubC_ok Zsor ZSORaddon). now apply Z.lt_le_pred. (* NonStrict *) - destruct p as [[e' z] op]. + intros p; destruct p as [[e' z] op]. case_eq (makeCuttingPlane e). - intros. + intros ? ? H H0 H1. inv H1. - apply makeCuttingPlane_ns_sound with (env:=env) (2:= H). + apply (makeCuttingPlane_ns_sound env) with (2:= H). assumption. Qed. @@ -1304,12 +1305,15 @@ Lemma genCuttingPlaneNone : forall env f, eval_nformula env f -> False. Proof. unfold genCuttingPlane. - destruct f. + intros env f; destruct f as [p o]. destruct o. case_eq (Zgcd_pol p) ; intros g c. case_eq (Z.gtb g 0 && (negb (Zeq_bool c 0) && negb (Zeq_bool (Z.gcd g c) g))). - intros. + intros H H0 H1 H2. flatten_bool. + match goal with [ H' : (g >? 0) = true |- ?G ] => rename H' into H3 end. + match goal with [ H' : negb (Zeq_bool c 0) = true |- ?G ] => rename H' into H end. + match goal with [ H' : negb (Zeq_bool (Z.gcd g c) g) = true |- ?G ] => rename H' into H5 end. rewrite negb_true_iff in H5. apply Zeq_bool_neq in H5. rewrite <- Zgt_is_gt_bool in H3. @@ -1359,7 +1363,7 @@ Lemma agree_env_subset : forall v1 v2 env env', agree_env v2 env env'. Proof. unfold agree_env. - intros. + intros v1 v2 env env' H ? ? ?. apply H. eapply Pos.le_trans ; eauto. Qed. @@ -1369,7 +1373,7 @@ Lemma agree_env_jump : forall fr j env env', agree_env (fr + j) env env' -> agree_env fr (Env.jump j env) (Env.jump j env'). Proof. - intros. + intros fr j env env' H. unfold agree_env ; intro. intros. unfold Env.jump. @@ -1382,7 +1386,7 @@ Lemma agree_env_tail : forall fr env env', agree_env (Pos.succ fr) env env' -> agree_env fr (Env.tail env) (Env.tail env'). Proof. - intros. + intros fr env env' H. unfold Env.tail. apply agree_env_jump. rewrite <- Pos.add_1_r in H. @@ -1393,7 +1397,7 @@ Qed. Lemma max_var_acc : forall p i j, (max_var (i + j) p = max_var i p + j)%positive. Proof. - induction p; simpl. + intros p; induction p as [|? ? IHp|? IHp1 ? ? IHp2]; simpl. - reflexivity. - intros. rewrite ! IHp. @@ -1415,27 +1419,27 @@ Lemma agree_env_eval_nformula : (AGREE : agree_env (max_var xH (fst e)) env env'), eval_nformula env e <-> eval_nformula env' e. Proof. - destruct e. - simpl; intros. + intros env env' e; destruct e as [p o]. + simpl; intros AGREE. assert ((RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x) env p) = - (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x) env' p)). + (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x) env' p)) as H. { revert env env' AGREE. generalize xH. - induction p ; simpl. + induction p as [?|p ? IHp|? IHp1 ? ? IHp2]; simpl. - reflexivity. - - intros. - apply IHp with (p := p1%positive). + - intros p1 **. + apply (IHp p1). apply agree_env_jump. eapply agree_env_subset; eauto. rewrite (Pos.add_comm p). rewrite max_var_acc. apply Pos.le_refl. - - intros. + - intros p ? ? AGREE. f_equal. f_equal. - { apply IHp1 with (p:= p). + { apply (IHp1 p). eapply agree_env_subset; eauto. apply Pos.le_max_l. } @@ -1446,7 +1450,7 @@ Proof. apply Pos.le_1_l. } { - apply IHp2 with (p := p). + apply (IHp2 p). apply agree_env_tail. eapply agree_env_subset; eauto. rewrite !Pplus_one_succ_r. @@ -1463,11 +1467,11 @@ Lemma agree_env_eval_nformulae : make_conj (eval_nformula env) l <-> make_conj (eval_nformula env') l. Proof. - induction l. + intros env env' l; induction l as [|a l IHl]. - simpl. tauto. - intros. rewrite ! make_conj_cons. - assert (eval_nformula env a <-> eval_nformula env' a). + assert (eval_nformula env a <-> eval_nformula env' a) as H. { apply agree_env_eval_nformula. eapply agree_env_subset ; eauto. @@ -1491,7 +1495,7 @@ Qed. Lemma eq_true_iff_eq : forall b1 b2 : bool, (b1 = true <-> b2 = true) <-> b1 = b2. Proof. - destruct b1,b2 ; intuition congruence. + intros b1 b2; destruct b1,b2 ; intuition congruence. Qed. Ltac pos_tac := @@ -1520,7 +1524,7 @@ Qed. Lemma ZChecker_sound : forall w l, ZChecker l w = true -> forall env, make_impl (eval_nformula env) l False. Proof. - induction w using (well_founded_ind (well_founded_ltof _ bdepth)). + intros w; induction w as [w H] using (well_founded_ind (well_founded_ltof _ bdepth)). destruct w as [ | w pf | w pf | p pf1 pf2 | w1 w2 pf | x pf]. - (* DoneProof *) simpl. discriminate. @@ -1529,12 +1533,12 @@ Proof. intros l. case_eq (eval_Psatz l w) ; [| discriminate]. intros f Hf. case_eq (Zunsat f). - intros. + intros H0 ? ?. apply (checker_nf_sound Zsor ZSORaddon l w). unfold check_normalised_formulas. unfold eval_Psatz in Hf. rewrite Hf. unfold Zunsat in H0. assumption. - intros. - assert (make_impl (eval_nformula env) (f::l) False). + intros H0 H1 env. + assert (make_impl (eval_nformula env) (f::l) False) as H2. apply H with (2:= H1). unfold ltof. simpl. @@ -1553,8 +1557,8 @@ Proof. case_eq (eval_Psatz l w) ; [ | discriminate]. intros f' Hlc. case_eq (genCuttingPlane f'). - intros. - assert (make_impl (eval_nformula env) (nformula_of_cutting_plane p::l) False). + intros p H0 H1 env. + assert (make_impl (eval_nformula env) (nformula_of_cutting_plane p::l) False) as H2. eapply (H pf) ; auto. unfold ltof. simpl. @@ -1565,13 +1569,13 @@ Proof. intro. apply H2. split ; auto. - apply eval_Psatz_sound with (env:=env) in Hlc. + apply (eval_Psatz_sound env) in Hlc. apply cutting_plane_sound with (1:= Hlc) (2:= H0). auto. (* genCuttingPlane = None *) - intros. + intros H0 H1 env. rewrite <- make_conj_impl. - intros. + intros H2. apply eval_Psatz_sound with (2:= Hlc) in H2. apply genCuttingPlaneNone with (2:= H2) ; auto. - (* SplitProof *) @@ -1581,18 +1585,20 @@ Proof. case_eq (genCuttingPlane (popp p, NonStrict)) ; [| discriminate]. intros cp1 GCP1 cp2 GCP2 ZC1 env. flatten_bool. + match goal with [ H' : ZChecker _ pf1 = true |- _ ] => rename H' into H0 end. + match goal with [ H' : ZChecker _ pf2 = true |- _ ] => rename H' into H1 end. destruct (eval_nformula_split env p). - + apply H with (env:=env) in H0. + + apply (fun H' ck => H _ H' _ ck env) in H0. rewrite <- make_conj_impl in *. intro ; apply H0. rewrite make_conj_cons. split; auto. - apply cutting_plane_sound with (f:= (p,NonStrict)) ; auto. + apply (cutting_plane_sound _ (p,NonStrict)) ; auto. apply ltof_bdepth_split_l. - + apply H with (env:=env) in H1. + + apply (fun H' ck => H _ H' _ ck env) in H1. rewrite <- make_conj_impl in *. intro ; apply H1. rewrite make_conj_cons. split; auto. - apply cutting_plane_sound with (f:= (popp p,NonStrict)) ; auto. + apply (cutting_plane_sound _ (popp p,NonStrict)) ; auto. apply ltof_bdepth_split_r. - (* EnumProof *) intros l. @@ -1601,22 +1607,22 @@ Proof. case_eq (eval_Psatz l w2) ; [ | discriminate]. intros f1 Hf1 f2 Hf2. case_eq (genCuttingPlane f2). - destruct p as [ [p1 z1] op1]. + intros p; destruct p as [ [p1 z1] op1]. case_eq (genCuttingPlane f1). - destruct p as [ [p2 z2] op2]. + intros p; destruct p as [ [p2 z2] op2]. case_eq (valid_cut_sign op1 && valid_cut_sign op2 && is_pol_Z0 (padd p1 p2)). intros Hcond. flatten_bool. - rename H1 into HZ0. - rename H2 into Hop1. - rename H3 into Hop2. + match goal with [ H1 : is_pol_Z0 (padd p1 p2) = true |- _ ] => rename H1 into HZ0 end. + match goal with [ H2 : valid_cut_sign op1 = true |- _ ] => rename H2 into Hop1 end. + match goal with [ H3 : valid_cut_sign op2 = true |- _ ] => rename H3 into Hop2 end. intros HCutL HCutR Hfix env. (* get the bounds of the enum *) rewrite <- make_conj_impl. - intro. - assert (-z1 <= eval_pol env p1 <= z2). + intro H0. + assert (-z1 <= eval_pol env p1 <= z2) as H1. split. - apply eval_Psatz_sound with (env:=env) in Hf2 ; auto. + apply (eval_Psatz_sound env) in Hf2 ; auto. apply cutting_plane_sound with (1:= Hf2) in HCutR. unfold nformula_of_cutting_plane in HCutR. unfold eval_nformula in HCutR. @@ -1628,10 +1634,10 @@ Proof. rewrite Z.add_move_0_l in HCutR; rewrite HCutR, Z.opp_involutive; reflexivity. now apply Z.le_sub_le_add_r in HCutR. (**) - apply is_pol_Z0_eval_pol with (env := env) in HZ0. + apply (fun H => is_pol_Z0_eval_pol _ H env) in HZ0. rewrite eval_pol_add, Z.add_move_r, Z.sub_0_l in HZ0. rewrite HZ0. - apply eval_Psatz_sound with (env:=env) in Hf1 ; auto. + apply (eval_Psatz_sound env) in Hf1 ; auto. apply cutting_plane_sound with (1:= Hf1) in HCutL. unfold nformula_of_cutting_plane in HCutL. unfold eval_nformula in HCutL. @@ -1647,7 +1653,7 @@ Proof. match goal with | |- context[?F pf (-z1) z2 = true] => set (FF := F) end. - intros. + intros Hfix. assert (HH :forall x, -z1 <= x <= z2 -> exists pr, (In pr pf /\ ZChecker ((PsubC Z.sub p1 x,Equal) :: l) pr = true)%Z). @@ -1655,16 +1661,18 @@ Proof. revert Hfix. generalize (-z1). clear z1. intro z1. revert z1 z2. - induction pf;simpl ;intros. + induction pf as [|a pf IHpf];simpl ;intros z1 z2 Hfix x **. revert Hfix. now case (Z.gtb_spec); [ | easy ]; intros LT; elim (Zlt_not_le _ _ LT); transitivity x. flatten_bool. + match goal with [ H' : _ <= x <= _ |- _ ] => rename H' into H0 end. + match goal with [ H' : FF pf (z1 + 1) z2 = true |- _ ] => rename H' into H2 end. destruct (Z_le_lt_eq_dec _ _ (proj1 H0)) as [ LT | -> ]. 2: exists a; auto. rewrite <- Z.le_succ_l in LT. assert (LE: (Z.succ z1 <= x <= z2)%Z) by intuition. elim IHpf with (2:=H2) (3:= LE). - intros. + intros x0 ?. exists x0 ; split;tauto. intros until 1. apply H ; auto. @@ -1676,7 +1684,7 @@ Proof. apply Z.add_le_mono_r. assumption. (*/asser *) destruct (HH _ H1) as [pr [Hin Hcheker]]. - assert (make_impl (eval_nformula env) ((PsubC Z.sub p1 (eval_pol env p1),Equal) :: l) False). + assert (make_impl (eval_nformula env) ((PsubC Z.sub p1 (eval_pol env p1),Equal) :: l) False) as H2. eapply (H pr) ;auto. apply in_bdepth ; auto. rewrite <- make_conj_impl in H2. @@ -1690,15 +1698,15 @@ Proof. unfold eval_pol. ring. discriminate. (* No cutting plane *) - intros. + intros H0 H1 H2 env. rewrite <- make_conj_impl. - intros. + intros H3. apply eval_Psatz_sound with (2:= Hf1) in H3. apply genCuttingPlaneNone with (2:= H3) ; auto. (* No Cutting plane (bis) *) - intros. + intros H0 H1 env. rewrite <- make_conj_impl. - intros. + intros H2. apply eval_Psatz_sound with (2:= Hf2) in H2. apply genCuttingPlaneNone with (2:= H2) ; auto. - intros l. @@ -1708,15 +1716,15 @@ Proof. set (z1 := (Pos.succ fr)) in *. set (t1 := (Pos.succ z1)) in *. destruct (x <=? fr)%positive eqn:LE ; [|congruence]. - intros. + intros H0 env. set (env':= fun v => if Pos.eqb v z1 then if Z.leb (env x) 0 then 0 else env x else if Pos.eqb v t1 then if Z.leb (env x) 0 then -(env x) else 0 else env v). - apply H with (env:=env') in H0. + apply (fun H' ck => H _ H' _ ck env') in H0. + rewrite <- make_conj_impl in *. - intro. + intro H1. rewrite !make_conj_cons in H0. apply H0 ; repeat split. * @@ -1729,17 +1737,17 @@ Proof. destruct (env x <=? 0); ring. { unfold t1. pos_tac; normZ. - lia (Hyp H2). + lia (Hyp (e := Z.pos z1 - Z.succ (Z.pos z1)) ltac:(assumption)). } { unfold t1, z1. pos_tac; normZ. - lia (Add (Hyp LE) (Hyp H3)). + lia (Add (Hyp LE) (Hyp (e := Z.pos x - Z.succ (Z.succ (Z.pos fr))) ltac:(assumption))). } { unfold z1. pos_tac; normZ. - lia (Add (Hyp LE) (Hyp H3)). + lia (Add (Hyp LE) (Hyp (e := Z.pos x - Z.succ (Z.pos fr)) ltac:(assumption))). } * apply eval_nformula_bound_var. @@ -1749,7 +1757,7 @@ Proof. compute. congruence. rewrite Z.leb_gt in EQ. normZ. - lia (Add (Hyp EQ) (Hyp H2)). + lia (Add (Hyp EQ) (Hyp (e := 0 - (env x + 1)) ltac:(assumption))). * apply eval_nformula_bound_var. unfold env'. @@ -1758,15 +1766,15 @@ Proof. destruct (env x <=? 0) eqn:EQ. rewrite Z.leb_le in EQ. normZ. - lia (Add (Hyp EQ) (Hyp H2)). + lia (Add (Hyp EQ) (Hyp (e := 0 - (- env x + 1)) ltac:(assumption))). compute; congruence. unfold t1. clear. pos_tac; normZ. - lia (Hyp H). + lia (Hyp (e := Z.pos z1 - Z.succ (Z.pos z1)) ltac:(assumption)). * - rewrite agree_env_eval_nformulae with (env':= env') in H1;auto. - unfold agree_env; intros. + rewrite (agree_env_eval_nformulae _ env') in H1;auto. + unfold agree_env; intros x0 H2. unfold env'. replace (x0 =? z1)%positive with false. replace (x0 =? t1)%positive with false. @@ -1776,13 +1784,13 @@ Proof. unfold fr in *. apply Pos2Z.pos_le_pos in H2. pos_tac; normZ. - lia (Add (Hyp H2) (Hyp H4)). + lia (Add (Hyp H2) (Hyp (e := Z.pos x0 - Z.succ (Z.succ (Z.pos (max_var_nformulae l)))) ltac:(assumption))). } { unfold z1, fr in *. apply Pos2Z.pos_le_pos in H2. pos_tac; normZ. - lia (Add (Hyp H2) (Hyp H4)). + lia (Add (Hyp H2) (Hyp (e := Z.pos x0 - Z.succ (Z.pos (max_var_nformulae l))) ltac:(assumption))). } + unfold ltof. simpl. @@ -1796,27 +1804,27 @@ Lemma ZTautoChecker_sound : forall f w, ZTautoChecker f w = true -> forall env, Proof. intros f w. unfold ZTautoChecker. - apply tauto_checker_sound with (eval' := eval_nformula). + apply (tauto_checker_sound _ _ _ _ eval_nformula). - apply Zeval_nformula_dec. - - intros until env. + - intros t ? env. unfold eval_nformula. unfold RingMicromega.eval_nformula. destruct t. apply (check_inconsistent_sound Zsor ZSORaddon) ; auto. - - unfold Zdeduce. intros. revert H. + - unfold Zdeduce. intros ? ? ? H **. revert H. apply (nformula_plus_nformula_correct Zsor ZSORaddon); auto. - - intros. + intros ? ? ? ? H. rewrite normalise_correct in H. rewrite Zeval_formula_compat; auto. - - intros. + intros ? ? ? ? H. rewrite negate_correct in H ; auto. rewrite Tauto.hold_eNOT. rewrite Zeval_formula_compat; auto. - intros t w0. unfold eval_tt. - intros. - rewrite make_impl_map with (eval := eval_nformula env). + intros H env. + rewrite (make_impl_map (eval_nformula env)). eapply ZChecker_sound; eauto. tauto. Qed. diff --git a/theories/setoid_ring/Field_theory.v b/theories/setoid_ring/Field_theory.v index c12f46bed6..4b3bba9843 100644 --- a/theories/setoid_ring/Field_theory.v +++ b/theories/setoid_ring/Field_theory.v @@ -397,7 +397,7 @@ Qed. Theorem cross_product_eq a b c d : ~ b == 0 -> ~ d == 0 -> a * d == c * b -> a / b == c / d. Proof. -intros. +intros H H0 H1. transitivity (a / b * (d / d)). - now rewrite rdiv_r_r, rmul_1_r. - now rewrite rdiv4, H1, (rmul_comm b d), <- rdiv4, rdiv_r_r. @@ -418,23 +418,23 @@ Qed. Lemma pow_pos_0 p : pow_pos rmul 0 p == 0. Proof. -induction p;simpl;trivial; now rewrite !IHp. +induction p as [p IHp|p IHp|];simpl;trivial; now rewrite !IHp. Qed. Lemma pow_pos_1 p : pow_pos rmul 1 p == 1. Proof. -induction p;simpl;trivial; ring [IHp]. +induction p as [p IHp|p IHp|];simpl;trivial; ring [IHp]. Qed. Lemma pow_pos_cst c p : pow_pos rmul [c] p == [pow_pos cmul c p]. Proof. -induction p;simpl;trivial; now rewrite !(morph_mul CRmorph), !IHp. +induction p as [p IHp|p IHp|];simpl;trivial; now rewrite !(morph_mul CRmorph), !IHp. Qed. Lemma pow_pos_mul_l x y p : pow_pos rmul (x * y) p == pow_pos rmul x p * pow_pos rmul y p. Proof. -induction p;simpl;trivial; ring [IHp]. +induction p as [p IHp|p IHp|];simpl;trivial; ring [IHp]. Qed. Lemma pow_pos_add_r x p1 p2 : @@ -446,7 +446,7 @@ Qed. Lemma pow_pos_mul_r x p1 p2 : pow_pos rmul x (p1*p2) == pow_pos rmul (pow_pos rmul x p1) p2. Proof. -induction p1;simpl;intros; rewrite ?pow_pos_mul_l, ?pow_pos_add_r; +induction p1 as [p1 IHp1|p1 IHp1|];simpl;intros; rewrite ?pow_pos_mul_l, ?pow_pos_add_r; simpl; trivial; ring [IHp1]. Qed. @@ -459,8 +459,8 @@ Qed. Lemma pow_pos_div a b p : ~ b == 0 -> pow_pos rmul (a / b) p == pow_pos rmul a p / pow_pos rmul b p. Proof. - intros. - induction p; simpl; trivial. + intros H. + induction p as [p IHp|p IHp|]; simpl; trivial. - rewrite IHp. assert (nz := pow_pos_nz p H). rewrite !rdiv4; trivial. @@ -578,14 +578,15 @@ Qed. Theorem PExpr_eq_semi_ok e e' : PExpr_eq e e' = true -> (e === e')%poly. Proof. -revert e'; induction e; destruct e'; simpl; try discriminate. +revert e'; induction e as [| |?|?|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe|? IHe ?]; + intro e'; destruct e'; simpl; try discriminate. - intros H l. now apply (morph_eq CRmorph). - case Pos.eqb_spec; intros; now subst. - intros H; destruct (if_true _ _ H). now rewrite IHe1, IHe2. - intros H; destruct (if_true _ _ H). now rewrite IHe1, IHe2. - intros H; destruct (if_true _ _ H). now rewrite IHe1, IHe2. - intros H. now rewrite IHe. -- intros H. destruct (if_true _ _ H). +- intros H. destruct (if_true _ _ H) as [H0 H1]. apply N.eqb_eq in H0. now rewrite IHe, H0. Qed. @@ -667,7 +668,7 @@ Proof. - case Pos.eqb_spec; [intro; subst | intros _]. + simpl. now rewrite rpow_pow. + destruct e;simpl;trivial. - repeat case ceqb_spec; intros; rewrite ?rpow_pow, ?H; simpl. + repeat case ceqb_spec; intros H **; rewrite ?rpow_pow, ?H; simpl. * now rewrite phi_1, pow_pos_1. * now rewrite phi_0, pow_pos_0. * now rewrite pow_pos_cst. @@ -686,7 +687,8 @@ Infix "**" := NPEmul (at level 40, left associativity). Theorem NPEmul_ok e1 e2 : (e1 ** e2 === e1 * e2)%poly. Proof. intros l. -revert e2; induction e1;destruct e2; simpl;try reflexivity; +revert e2; induction e1 as [| |?|?|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe1|? IHe1 n]; + intro e2; destruct e2; simpl;try reflexivity; repeat (case ceqb_spec; intro H; try rewrite H; clear H); simpl; try reflexivity; try ring [phi_0 phi_1]. apply (morph_mul CRmorph). @@ -801,7 +803,7 @@ Qed. Theorem PCond_app l l1 l2 : PCond l (l1 ++ l2) <-> PCond l l1 /\ PCond l l2. Proof. -induction l1. +induction l1 as [|a l1 IHl1]. - simpl. split; [split|destruct 1]; trivial. - simpl app. rewrite !PCond_cons, IHl1. symmetry; apply and_assoc. Qed. @@ -813,7 +815,7 @@ Definition absurd_PCond := cons 0%poly nil. Lemma absurd_PCond_bottom : forall l, ~ PCond l absurd_PCond. Proof. unfold absurd_PCond; simpl. -red; intros. +red; intros ? H. apply H. apply phi_0. Qed. @@ -901,7 +903,7 @@ Theorem isIn_ok e1 p1 e2 p2 : Proof. Opaque NPEpow. revert p1 p2. -induction e2; intros p1 p2; +induction e2 as [| |?|?|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe2_1 ? IHe2_2|? IHe|? IHe2 n]; intros p1 p2; try refine (default_isIn_ok e1 _ p1 p2); simpl isIn. - specialize (IHe2_1 p1 p2). destruct isIn as [([|p],e)|]. @@ -936,7 +938,7 @@ induction e2; intros p1 p2; destruct IHe2_2 as (IH,GT). split; trivial. set (d := ZtoN (Z.pos p1 - NtoZ n)) in *; clearbody d. npe_simpl. rewrite IH. npe_ring. -- destruct n; trivial. +- destruct n as [|p]; trivial. specialize (IHe2 p1 (p * p2)%positive). destruct isIn as [(n,e)|]; trivial. destruct IHe2 as (IH,GT). split; trivial. @@ -983,7 +985,7 @@ Lemma split_aux_ok1 e1 p e2 : /\ e2 === right res * common res)%poly. Proof. Opaque NPEpow NPEmul. - intros. unfold res;clear res; generalize (isIn_ok e1 p e2 xH). + intros res. unfold res;clear res; generalize (isIn_ok e1 p e2 xH). destruct (isIn e1 p e2 1) as [([|p'],e')|]; simpl. - intros (H1,H2); split; npe_simpl. + now rewrite PE_1_l. @@ -1000,7 +1002,8 @@ Theorem split_aux_ok: forall e1 p e2, (e1 ^ Npos p === left (split_aux e1 p e2) * common (split_aux e1 p e2) /\ e2 === right (split_aux e1 p e2) * common (split_aux e1 p e2))%poly. Proof. -induction e1;intros k e2; try refine (split_aux_ok1 _ k e2);simpl. +intro e1;induction e1 as [| |?|?|? IHe1_1 ? IHe1_2|? IHe1_1 ? IHe1_2|e1_1 IHe1_1 ? IHe1_2|? IHe1|? IHe1 n]; + intros k e2; try refine (split_aux_ok1 _ k e2);simpl. destruct (IHe1_1 k e2) as (H1,H2). destruct (IHe1_2 k (right (split_aux e1_1 k e2))) as (H3,H4). clear IHe1_1 IHe1_2. @@ -1101,7 +1104,8 @@ Eval compute Theorem Pcond_Fnorm l e : PCond l (condition (Fnorm e)) -> ~ (denum (Fnorm e))@l == 0. Proof. -induction e; simpl condition; rewrite ?PCond_cons, ?PCond_app; +induction e as [| |?|?|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe|? IHe|? IHe1 ? IHe2|? IHe n]; + simpl condition; rewrite ?PCond_cons, ?PCond_app; simpl denum; intros (Hc1,Hc2) || intros Hc; rewrite ?NPEmul_ok. - simpl. rewrite phi_1; exact rI_neq_rO. - simpl. rewrite phi_1; exact rI_neq_rO. @@ -1141,7 +1145,8 @@ Theorem Fnorm_FEeval_PEeval l fe: PCond l (condition (Fnorm fe)) -> FEeval l fe == (num (Fnorm fe)) @ l / (denum (Fnorm fe)) @ l. Proof. -induction fe; simpl condition; rewrite ?PCond_cons, ?PCond_app; simpl; +induction fe as [| |?|?|fe1 IHfe1 fe2 IHfe2|fe1 IHfe1 fe2 IHfe2|fe1 IHfe1 fe2 IHfe2|fe IHfe|fe IHfe|fe1 IHfe1 fe2 IHfe2|fe IHfe n]; + simpl condition; rewrite ?PCond_cons, ?PCond_app; simpl; intros (Hc1,Hc2) || intros Hc; try (specialize (IHfe1 Hc1);apply Pcond_Fnorm in Hc1); try (specialize (IHfe2 Hc2);apply Pcond_Fnorm in Hc2); @@ -1260,7 +1265,7 @@ Proof. destruct (Nnorm _ _ _) as [c | | ] eqn: HN; try ( apply rdiv_ext; eapply ring_rw_correct; eauto). - destruct (ceqb_spec c cI). + destruct (ceqb_spec c cI) as [H0|]. set (nnum := NPphi_dev _ _). apply eq_trans with (nnum / NPphi_dev l (Pc c)). apply rdiv_ext; @@ -1285,7 +1290,7 @@ Proof. destruct (Nnorm _ _ _) as [c | | ] eqn: HN; try ( apply rdiv_ext; eapply ring_rw_pow_correct; eauto). - destruct (ceqb_spec c cI). + destruct (ceqb_spec c cI) as [H0|]. set (nnum := NPphi_pow _ _). apply eq_trans with (nnum / NPphi_pow l (Pc c)). apply rdiv_ext; @@ -1415,7 +1420,8 @@ Theorem Field_simplify_eq_pow_in_correct : NPphi_pow l np1 == NPphi_pow l np2. Proof. - intros. subst nfe1 nfe2 lmp np1 np2. + intros n l lpe fe1 fe2 ? lmp ? nfe1 ? nfe2 ? den ? np1 ? np2 ? ? ?. + subst nfe1 nfe2 lmp np1 np2. rewrite !(Pphi_pow_ok Rsth Reqe ARth CRmorph pow_th get_sign_spec). repeat (rewrite <- (norm_subst_ok Rsth Reqe ARth CRmorph pow_th);trivial). simpl. apply Field_simplify_aux_ok; trivial. @@ -1434,7 +1440,8 @@ forall n l lpe fe1 fe2, PCond l (condition nfe1 ++ condition nfe2) -> NPphi_dev l np1 == NPphi_dev l np2. Proof. - intros. subst nfe1 nfe2 lmp np1 np2. + intros n l lpe fe1 fe2 ? lmp ? nfe1 ? nfe2 ? den ? np1 ? np2 ? ? ?. + subst nfe1 nfe2 lmp np1 np2. rewrite !(Pphi_dev_ok Rsth Reqe ARth CRmorph get_sign_spec). repeat (rewrite <- (norm_subst_ok Rsth Reqe ARth CRmorph pow_th);trivial). apply Field_simplify_aux_ok; trivial. @@ -1458,7 +1465,7 @@ Lemma fcons_ok : forall l l1, (forall lock, lock = PCond l -> lock (Fapp l1 nil)) -> PCond l l1. Proof. intros l l1 h1; assert (H := h1 (PCond l) (refl_equal _));clear h1. -induction l1; simpl; intros. +induction l1 as [|a l1 IHl1]; simpl; intros. trivial. elim PCond_fcons_inv with (1 := H); intros. destruct l1; trivial. split; trivial. apply IHl1; trivial. @@ -1480,7 +1487,7 @@ Fixpoint Fcons (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) := Theorem PFcons_fcons_inv: forall l a l1, PCond l (Fcons a l1) -> ~ a @ l == 0 /\ PCond l l1. Proof. -induction l1 as [|e l1]; simpl Fcons. +intros l a l1; induction l1 as [|e l1 IHl1]; simpl Fcons. - simpl; now split. - case PExpr_eq_spec; intros H; rewrite !PCond_cons; intros (H1,H2); repeat split; trivial. @@ -1501,7 +1508,7 @@ Fixpoint Fcons0 (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) := Theorem PFcons0_fcons_inv: forall l a l1, PCond l (Fcons0 a l1) -> ~ a @ l == 0 /\ PCond l l1. Proof. -induction l1 as [|e l1]; simpl Fcons0. +intros l a l1; induction l1 as [|e l1 IHl1]; simpl Fcons0. - simpl; now split. - generalize (ring_correct O l nil a e). lazy zeta; simpl Peq. case Peq; intros H; rewrite !PCond_cons; intros (H1,H2); @@ -1529,7 +1536,7 @@ intros l a; elim a; try (intros; apply PFcons0_fcons_inv; trivial; fail). destruct (H0 _ H3) as (H4,H5). split; trivial. simpl. apply field_is_integral_domain; trivial. -- intros. destruct (H _ H0). split; trivial. +- intros ? H ? ? H0. destruct (H _ H0). split; trivial. apply PEpow_nz; trivial. Qed. @@ -1580,7 +1587,7 @@ intros l a; elim a; try (intros; apply PFcons0_fcons_inv; trivial; fail). split; trivial. apply ropp_neq_0; trivial. rewrite (morph_opp CRmorph), phi_0, phi_1 in H0. trivial. -- intros. destruct (H _ H0);split;trivial. apply PEpow_nz; trivial. +- intros ? H ? ? H0. destruct (H _ H0);split;trivial. apply PEpow_nz; trivial. Qed. Definition Fcons2 e l := Fcons1 (PEsimp e) l. @@ -1674,7 +1681,7 @@ Hypothesis gen_phiPOS_not_0 : forall p, ~ gen_phiPOS1 rI radd rmul p == 0. Lemma add_inj_r p x y : gen_phiPOS1 rI radd rmul p + x == gen_phiPOS1 rI radd rmul p + y -> x==y. Proof. -elim p using Pos.peano_ind; simpl; intros. +elim p using Pos.peano_ind; simpl; [intros H|intros ? H ?]. apply S_inj; trivial. apply H. apply S_inj. @@ -1710,8 +1717,8 @@ Lemma gen_phiN_inj x y : gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y -> x = y. Proof. -destruct x; destruct y; simpl; intros; trivial. - elim gen_phiPOS_not_0 with p. +destruct x as [|p]; destruct y as [|p']; simpl; intros H; trivial. + elim gen_phiPOS_not_0 with p'. symmetry . rewrite (same_gen Rsth Reqe ARth); trivial. elim gen_phiPOS_not_0 with p. @@ -1770,14 +1777,14 @@ Lemma gen_phiZ_inj x y : gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y -> x = y. Proof. -destruct x; destruct y; simpl; intros. +destruct x as [|p|p]; destruct y as [|p'|p']; simpl; intros H. trivial. - elim gen_phiPOS_not_0 with p. + elim gen_phiPOS_not_0 with p'. rewrite (same_gen Rsth Reqe ARth). symmetry ; trivial. - elim gen_phiPOS_not_0 with p. + elim gen_phiPOS_not_0 with p'. rewrite (same_gen Rsth Reqe ARth). - rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)). + rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p')). rewrite <- H. apply (ARopp_zero Rsth Reqe ARth). elim gen_phiPOS_not_0 with p. @@ -1790,12 +1797,12 @@ destruct x; destruct y; simpl; intros. rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)). rewrite H. apply (ARopp_zero Rsth Reqe ARth). - elim gen_phiPOS_discr_sgn with p0 p. + elim gen_phiPOS_discr_sgn with p' p. symmetry ; trivial. - replace p0 with p; trivial. + replace p' with p; trivial. apply gen_phiPOS_inject. rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)). - rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p0)). + rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p')). rewrite H; trivial. reflexivity. Qed. |