diff options
42 files changed, 569 insertions, 309 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index a8bca2bffe..ce6be777f3 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -706,7 +706,11 @@ library:ci-engine_bench: extends: .ci-template library:ci-fcsl_pcm: - extends: .ci-template + extends: .ci-template-flambda + stage: stage-3 + needs: + - build:edge+flambda + - library:ci-mathcomp library:ci-fiat_crypto: extends: .ci-template-flambda @@ -781,6 +785,10 @@ plugin:ci-gappa: library:ci-geocoq: extends: .ci-template-flambda + stage: stage-3 + needs: + - build:edge+flambda + - library:ci-mathcomp library:ci-hott: extends: .ci-template @@ -878,6 +886,10 @@ plugin:plugin-tutorial: plugin:ci-quickchick: extends: .ci-template-flambda + stage: stage-3 + needs: + - build:edge+flambda + - library:ci-mathcomp plugin:ci-reduction_effects: extends: .ci-template diff --git a/Makefile.ci b/Makefile.ci index c589c95258..f7c2943cc2 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -88,9 +88,12 @@ ci-fiat_crypto_ocaml: ci-fiat_crypto ci-interval: ci-mathcomp ci-flocq ci-coquelicot ci-bignums ci-fourcolor: ci-mathcomp ci-oddorder: ci-mathcomp +ci-fcsl_pcm: ci-mathcomp + +ci-geocoq: ci-mathcomp ci-simple_io: ci-ext_lib -ci-quickchick: ci-ext_lib ci-simple_io +ci-quickchick: ci-ext_lib ci-simple_io ci-mathcomp ci-metacoq: ci-equations diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 8d8f78e10c..006565df5c 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -143,33 +143,3 @@ make() command make --output-sync "$@" fi } - -# this installs just the ssreflect library of math-comp -install_ssreflect() -{ - echo 'Installing ssreflect' - - git_download mathcomp - - ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp/ssreflect" && \ - make && \ - make install ) - -} - -# this installs just the ssreflect + algebra library of math-comp -install_ssralg() -{ - echo 'Installing ssralg' - - git_download mathcomp - - ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && \ - make -C ssreflect && \ - make -C ssreflect install && \ - make -C fingroup && \ - make -C fingroup install && \ - make -C algebra && \ - make -C algebra install ) - -} diff --git a/dev/ci/ci-deriving.sh b/dev/ci/ci-deriving.sh index ec3625c177..c34fc44f69 100755 --- a/dev/ci/ci-deriving.sh +++ b/dev/ci/ci-deriving.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -install_ssreflect - git_download deriving ( cd "${CI_BUILD_DIR}/deriving" && make && make tests && make install ) diff --git a/dev/ci/ci-fcsl_pcm.sh b/dev/ci/ci-fcsl_pcm.sh index cb951630c8..e1248c6627 100755 --- a/dev/ci/ci-fcsl_pcm.sh +++ b/dev/ci/ci-fcsl_pcm.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -install_ssreflect - git_download fcsl_pcm ( cd "${CI_BUILD_DIR}/fcsl_pcm" && make ) diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh index e4fc983e68..0ad9ac0cbb 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -install_ssralg - git_download geocoq ( cd "${CI_BUILD_DIR}/geocoq" && ./configure.sh && make ) diff --git a/dev/ci/ci-quickchick.sh b/dev/ci/ci-quickchick.sh index 08686d7ced..2bc2a18849 100755 --- a/dev/ci/ci-quickchick.sh +++ b/dev/ci/ci-quickchick.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -install_ssreflect - git_download quickchick ( cd "${CI_BUILD_DIR}/quickchick" && make && make install) diff --git a/doc/changelog/05-tactic-language/13920-ltac2-ind-api.rst b/doc/changelog/05-tactic-language/13920-ltac2-ind-api.rst new file mode 100644 index 0000000000..32499957be --- /dev/null +++ b/doc/changelog/05-tactic-language/13920-ltac2-ind-api.rst @@ -0,0 +1,5 @@ +- **Added:** + Added the Ltac2 API `Ltac2.Ind` for manipulating inductive types + (`#13920 <https://github.com/coq/coq/pull/13920>`_, + fixes `#10095 <https://github.com/coq/coq/issues/10095>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/10-standard-library/13804-count_occ.rst b/doc/changelog/10-standard-library/13804-count_occ.rst new file mode 100644 index 0000000000..9354b219d8 --- /dev/null +++ b/doc/changelog/10-standard-library/13804-count_occ.rst @@ -0,0 +1,4 @@ +- **Added:** + Lemmas about ``count_occ``: ``count_occ_app``, ``count_occ_elt_eq``, ``count_occ_elt_neq``, ``count_occ_bound``, ``count_occ_repeat_eq``, ``count_occ_repeat_neq``, ``count_occ_unique``, ``count_occ_repeat_excl``, ``count_occ_sgt``, ``Permutation_count_occ`` + (`#13804 <https://github.com/coq/coq/pull/13804>`_, + by Olivier Laurent with help of Jean-Christophe Léchenet). diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index b0f4e883be..d67906c4a8 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -685,6 +685,7 @@ through the <tt>Require Import</tt> command.</p> user-contrib/Ltac2/Fresh.v user-contrib/Ltac2/Ident.v user-contrib/Ltac2/Init.v + user-contrib/Ltac2/Ind.v user-contrib/Ltac2/Int.v user-contrib/Ltac2/List.v user-contrib/Ltac2/Ltac1.v diff --git a/interp/reserve.ml b/interp/reserve.ml index 07160dcf6f..cdc95285fe 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -15,8 +15,6 @@ open Util open Pp open Names open Nameops -open Libobject -open Lib open Notation_term open Notation_ops open Globnames @@ -77,15 +75,11 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) | NRef (ref,_) -> RefKey(canonical_gr ref), None | _ -> Oth, None -let cache_reserved_type (_,(id,t)) = +let add_reserved_type (id,t) = let key = fst (notation_constr_key t) in reserve_table := Id.Map.add id t !reserve_table; reserve_revtable := keymap_add key (id, t) !reserve_revtable -let in_reserved : Id.t * notation_constr -> obj = - declare_object {(default_object "RESERVED-TYPE") with - cache_function = cache_reserved_type } - let declare_reserved_type_binding {CAst.loc;v=id} t = if not (Id.equal id (root_of_id id)) then user_err ?loc ~hdr:"declare_reserved_type" @@ -96,7 +90,7 @@ let declare_reserved_type_binding {CAst.loc;v=id} t = user_err ?loc ~hdr:"declare_reserved_type" ((Id.print id++str" is already bound to a type")) with Not_found -> () end; - add_anonymous_leaf (in_reserved (id,t)) + add_reserved_type (id,t) let declare_reserved_type idl t = List.iter (fun id -> declare_reserved_type_binding id t) (List.rev idl) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index d517d215ed..9ce388929c 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -2130,7 +2130,7 @@ let compile_deps env sigma prefix init t = in aux env 0 init t -let compile_constant_field env _prefix con acc cb = +let compile_constant_field env con acc cb = let gl = compile_constant env empty_evars con cb in gl@acc diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index 90525a19b2..17312ec8ea 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -65,7 +65,7 @@ val register_native_file : string -> unit val is_loaded_native_file : string -> bool -val compile_constant_field : env -> string -> Constant.t -> +val compile_constant_field : env -> Constant.t -> global list -> 'a constant_body -> global list val compile_mind_field : ModPath.t -> Label.t -> diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml index 2e27fe071e..6dd7f315e0 100644 --- a/kernel/nativelibrary.ml +++ b/kernel/nativelibrary.ml @@ -17,21 +17,21 @@ open Nativecode (** This file implements separate compilation for libraries in the native compiler *) -let rec translate_mod prefix mp env mod_expr acc = +let rec translate_mod mp env mod_expr acc = match mod_expr with | NoFunctor struc -> let env' = add_structure mp struc empty_delta_resolver env in - List.fold_left (translate_field prefix mp env') acc struc + List.fold_left (translate_field mp env') acc struc | MoreFunctor _ -> acc -and translate_field prefix mp env acc (l,x) = +and translate_field mp env acc (l,x) = match x with | SFBconst cb -> let con = Constant.make2 mp l in (debug_native_compiler (fun () -> let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in Pp.str msg)); - compile_constant_field env prefix con acc cb + compile_constant_field env con acc cb | SFBmind mb -> (debug_native_compiler (fun () -> let id = mb.mind_packets.(0).mind_typename in @@ -45,7 +45,7 @@ and translate_field prefix mp env acc (l,x) = Printf.sprintf "Compiling module %s..." (ModPath.to_string mp) in Pp.str msg)); - translate_mod prefix mp env md.mod_type acc + translate_mod mp env md.mod_type acc | SFBmodtype mdtyp -> let mp = mdtyp.mod_mp in (debug_native_compiler (fun () -> @@ -53,19 +53,18 @@ and translate_field prefix mp env acc (l,x) = Printf.sprintf "Compiling module type %s..." (ModPath.to_string mp) in Pp.str msg)); - translate_mod prefix mp env mdtyp.mod_type acc + translate_mod mp env mdtyp.mod_type acc -let dump_library mp dp env mod_expr = +let dump_library mp env mod_expr = debug_native_compiler (fun () -> Pp.str "Compiling library..."); match mod_expr with | NoFunctor struc -> let env = add_structure mp struc empty_delta_resolver env in - let prefix = mod_uid_of_dirpath dp ^ "." in let t0 = Sys.time () in clear_global_tbl (); clear_symbols (); let mlcode = - List.fold_left (translate_field prefix mp env) [] struc + List.fold_left (translate_field mp env) [] struc in let t1 = Sys.time () in let time_info = Format.sprintf "Time spent generating this code: %.5fs" (t1-.t0) in diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli index 8f58dfa8d3..1d0d56703d 100644 --- a/kernel/nativelibrary.mli +++ b/kernel/nativelibrary.mli @@ -15,5 +15,5 @@ open Nativecode (** This file implements separate compilation for libraries in the native compiler *) -val dump_library : ModPath.t -> DirPath.t -> env -> module_signature -> +val dump_library : ModPath.t -> env -> module_signature -> global list * Nativevalues.symbols diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index a35f94e3ce..5f83e78eb0 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1273,7 +1273,7 @@ let export ?except ~output_native_objects senv dir = in let ast, symbols = if output_native_objects then - Nativelibrary.dump_library mp dir senv.env str + Nativelibrary.dump_library mp senv.env str else [], Nativevalues.empty_symbols in let lib = { diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 24aa4ed771..013892ad74 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -269,16 +269,14 @@ let build_constant_declaration env result = in Environ.really_needed env (Id.Set.union ids_typ ids_def), def | Some declared -> - let needed = Environ.really_needed env declared in - (* Transitive closure ensured by the upper layers *) - let () = assert (Id.Set.equal needed declared) in - (* We use the declared set and chain a check of correctness *) - declared, - match def with - | Undef _ | Primitive _ | OpaqueDef _ as x -> x (* nothing to check *) - | Def cs as x -> - let () = check_section_variables env declared typ (Mod_subst.force_constr cs) in - x + let declared = Environ.really_needed env declared in + (* We use the declared set and chain a check of correctness *) + declared, + match def with + | Undef _ | Primitive _ | OpaqueDef _ as x -> x (* nothing to check *) + | Def cs as x -> + let () = check_section_variables env declared typ (Mod_subst.force_constr cs) in + x in let univs = result.cook_universes in let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index f2241e78d2..54d7c310aa 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -2148,7 +2148,8 @@ let interp_redexp env sigma r = (* Backwarding recursive needs of tactic glob/interp/eval functions *) let _ = - let eval lfun poly env sigma ty tac = + let eval ?loc ~poly env sigma tycon tac = + let lfun = GlobEnv.lfun env in let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in let ist = { lfun; poly; extra; } in let tac = eval_tactic_ist ist tac in @@ -2156,8 +2157,13 @@ let _ = poly seems like enough to get reasonable behavior in practice *) let name = Id.of_string "ltac_gen" in - let (c, sigma) = Proof.refine_by_tactic ~name ~poly env sigma ty tac in - (EConstr.of_constr c, sigma) + let sigma, ty = match tycon with + | Some ty -> sigma, ty + | None -> GlobEnv.new_type_evar env sigma ~src:(loc,Evar_kinds.InternalHole) + in + let (c, sigma) = Proof.refine_by_tactic ~name ~poly (GlobEnv.renamed_env env) sigma ty tac in + let j = { Environ.uj_val = EConstr.of_constr c; uj_type = ty } in + (j, sigma) in GlobEnv.register_constr_interp0 wit_tactic eval diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml index 34fae613bf..ad28b54900 100644 --- a/pretyping/globEnv.ml +++ b/pretyping/globEnv.ml @@ -51,6 +51,8 @@ let make ~hypnaming env sigma lvar = } let env env = env.static_env +let renamed_env env = env.renamed_env +let lfun env = env.lvar.ltac_genargs let vars_of_env env = Id.Set.union (Id.Map.domain env.lvar.ltac_genargs) (vars_of_env env.static_env) @@ -183,10 +185,13 @@ let interp_ltac_variable ?loc typing_fun env sigma id : Evd.evar_map * unsafe_ju let interp_ltac_id env id = ltac_interp_id env.lvar id +type 'a obj_interp_fun = + ?loc:Loc.t -> poly:bool -> t -> Evd.evar_map -> Evardefine.type_constraint -> + 'a -> unsafe_judgment * Evd.evar_map + module ConstrInterpObj = struct - type ('r, 'g, 't) obj = - unbound_ltac_var_map -> bool -> env -> Evd.evar_map -> types -> 'g -> constr * Evd.evar_map + type ('r, 'g, 't) obj = 'g obj_interp_fun let name = "constr_interp" let default _ = None end @@ -195,8 +200,8 @@ module ConstrInterp = Genarg.Register(ConstrInterpObj) let register_constr_interp0 = ConstrInterp.register0 -let interp_glob_genarg env poly sigma ty arg = +let interp_glob_genarg ?loc ~poly env sigma ty arg = let open Genarg in let GenArg (Glbwit tag, arg) = arg in let interp = ConstrInterp.obj tag in - interp env.lvar.ltac_genargs poly env.renamed_env sigma ty arg + interp ?loc ~poly env sigma ty arg diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli index 023e24e6d8..40feb8206b 100644 --- a/pretyping/globEnv.mli +++ b/pretyping/globEnv.mli @@ -15,11 +15,18 @@ open EConstr open Ltac_pretype open Evarutil +(** Type of environment extended with naming and ltac interpretation data *) + +type t + (** To embed constr in glob_constr *) +type 'a obj_interp_fun = + ?loc:Loc.t -> poly:bool -> t -> Evd.evar_map -> Evardefine.type_constraint -> + 'a -> unsafe_judgment * Evd.evar_map + val register_constr_interp0 : - ('r, 'g, 't) Genarg.genarg_type -> - (unbound_ltac_var_map -> bool -> env -> evar_map -> types -> 'g -> constr * evar_map) -> unit + ('r, 'g, 't) Genarg.genarg_type -> 'g obj_interp_fun -> unit (** {6 Pretyping name management} *) @@ -32,10 +39,6 @@ val register_constr_interp0 : variables used to build purely-named evar contexts *) -(** Type of environment extended with naming and ltac interpretation data *) - -type t - (** Build a pretyping environment from an ltac environment *) val make : hypnaming:naming_mode -> env -> evar_map -> ltac_var_map -> t @@ -43,6 +46,8 @@ val make : hypnaming:naming_mode -> env -> evar_map -> ltac_var_map -> t (** Export the underlying environment *) val env : t -> env +val renamed_env : t -> env +val lfun : t -> unbound_ltac_var_map val vars_of_env : t -> Id.Set.t @@ -85,5 +90,5 @@ val interp_ltac_id : t -> Id.t -> Id.t (** Interpreting a generic argument, typically a "ltac:(...)", taking into account the possible renaming *) -val interp_glob_genarg : t -> bool -> evar_map -> constr -> - Genarg.glob_generic_argument -> constr * evar_map +val interp_glob_genarg : ?loc:Loc.t -> poly:bool -> t -> evar_map -> Evardefine.type_constraint -> + Genarg.glob_generic_argument -> unsafe_judgment * evar_map diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 3ccc6ea125..800096f2b3 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -653,12 +653,8 @@ struct sigma, { uj_val; uj_type } | Some arg -> - let sigma, ty = - match tycon with - | Some ty -> sigma, ty - | None -> new_type_evar env sigma ~src:(loc,Evar_kinds.InternalHole) in - let c, sigma = GlobEnv.interp_glob_genarg env poly sigma ty arg in - sigma, { uj_val = c; uj_type = ty } + let j, sigma = GlobEnv.interp_glob_genarg ?loc ~poly env sigma tycon arg in + sigma, j let pretype_rec self (fixkind, names, bl, lar, vdef) = fun ?loc ~program_mode ~poly resolve_tc tycon env sigma -> diff --git a/tactics/cbn.ml b/tactics/cbn.ml index 167f7d4026..99d579f5c6 100644 --- a/tactics/cbn.ml +++ b/tactics/cbn.ml @@ -402,11 +402,11 @@ let safe_meta_value sigma ev = (* Beta Reduction tools *) -let apply_subst recfun env sigma refold cst_l t stack = +let apply_subst recfun env sigma cst_l t stack = let rec aux env cst_l t stack = match (Stack.decomp stack, EConstr.kind sigma t) with | Some (h,stacktl), Lambda (_,_,c) -> - let cst_l' = if refold then Cst_stack.add_param h cst_l else cst_l in + let cst_l' = Cst_stack.add_param h cst_l in aux (h::env) cst_l' c stacktl | _ -> recfun sigma cst_l (substl env t, stack) in aux env cst_l t stack @@ -453,50 +453,42 @@ let magically_constant_of_fixbody env sigma reference bd = function | None -> bd end -let contract_cofix ?env sigma ?reference (bodynum,(names,types,bodies as typedbodies)) = +let contract_cofix ~env sigma ?reference (bodynum,(names,types,bodies as typedbodies)) = let nbodies = Array.length bodies in let make_Fi j = let ind = nbodies-j-1 in if Int.equal bodynum ind then mkCoFix (ind,typedbodies) else let bd = mkCoFix (ind,typedbodies) in - match env with + match reference with | None -> bd - | Some e -> - match reference with - | None -> bd - | Some r -> magically_constant_of_fixbody e sigma r bd names.(ind).binder_name in + | Some r -> magically_constant_of_fixbody env sigma r bd names.(ind).binder_name in let closure = List.init nbodies make_Fi in substl closure bodies.(bodynum) (** Similar to the "fix" case below *) -let reduce_and_refold_cofix recfun env sigma refold cst_l cofix sk = +let reduce_and_refold_cofix recfun env sigma cst_l cofix sk = let raw_answer = - let env = if refold then Some env else None in - contract_cofix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) cofix in + contract_cofix ~env sigma ?reference:(Cst_stack.reference sigma cst_l) cofix in apply_subst (fun sigma x (t,sk') -> - let t' = - if refold then Cst_stack.best_replace sigma (mkCoFix cofix) cst_l t else t in + let t' = Cst_stack.best_replace sigma (mkCoFix cofix) cst_l t in recfun x (t',sk')) - [] sigma refold Cst_stack.empty raw_answer sk + [] sigma Cst_stack.empty raw_answer sk (* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce Bi[Fj --> FIX[nl;j](A1...Ak;[F1...Fk]{B1...Bk})] *) -let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies as typedbodies)) = +let contract_fix ~env sigma ?reference ((recindices,bodynum),(names,types,bodies as typedbodies)) = let nbodies = Array.length recindices in let make_Fi j = let ind = nbodies-j-1 in if Int.equal bodynum ind then mkFix ((recindices,ind),typedbodies) else let bd = mkFix ((recindices,ind),typedbodies) in - match env with + match reference with | None -> bd - | Some e -> - match reference with - | None -> bd - | Some r -> magically_constant_of_fixbody e sigma r bd names.(ind).binder_name in + | Some r -> magically_constant_of_fixbody env sigma r bd names.(ind).binder_name in let closure = List.init nbodies make_Fi in substl closure bodies.(bodynum) @@ -504,18 +496,14 @@ let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies replace the fixpoint by the best constant from [cst_l] Other rels are directly substituted by constants "magically found from the context" in contract_fix *) -let reduce_and_refold_fix recfun env sigma refold cst_l fix sk = +let reduce_and_refold_fix recfun env sigma cst_l fix sk = let raw_answer = - let env = if refold then Some env else None in - contract_fix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) fix in + contract_fix ~env sigma ?reference:(Cst_stack.reference sigma cst_l) fix in apply_subst (fun sigma x (t,sk') -> - let t' = - if refold then - Cst_stack.best_replace sigma (mkFix fix) cst_l t - else t - in recfun x (t',sk')) - [] sigma refold Cst_stack.empty raw_answer sk + let t' = Cst_stack.best_replace sigma (mkFix fix) cst_l t in + recfun x (t',sk')) + [] sigma Cst_stack.empty raw_answer sk module CredNative = Reductionops.CredNative @@ -524,7 +512,7 @@ module CredNative = Reductionops.CredNative Here is where unfolded constant are stored in order to be eventually refolded. - If tactic_mode is true, it uses ReductionBehaviour, prefers + It uses ReductionBehaviour, prefers refold constant instead of value and tries to infer constants fix and cofix came from. @@ -558,7 +546,7 @@ let apply_branch env sigma (ind, i) args (ci, u, pms, iv, r, lf) = in Vars.substl subst (snd br) -let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = +let rec whd_state_gen ?csts flags env sigma = let open Context.Named.Declaration in let open ReductionBehaviour in let rec whrec cst_l (x, stack) = @@ -584,7 +572,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = | Var id when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fVAR id) -> (match lookup_named id env with | LocalDef (_,body,_) -> - whrec (if refold then Cst_stack.add_cst (mkVar id) cst_l else cst_l) (body, stack) + whrec (Cst_stack.add_cst (mkVar id) cst_l) (body, stack) | _ -> fold ()) | Evar ev -> fold () | Meta ev -> @@ -600,10 +588,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = | body -> begin let body = EConstr.of_constr body in - if not tactic_mode - then whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l) - (body, stack) - else (* Looks for ReductionBehaviour *) + (* Looks for ReductionBehaviour *) match ReductionBehaviour.get (GlobRef.ConstRef c) with | None -> whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, stack) | Some behavior -> @@ -652,10 +637,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = else fold () | Proj (p, c) when CClosure.RedFlags.red_projection flags p -> (let npars = Projection.npars p in - if not tactic_mode then - let stack' = (c, Stack.Proj (p, Cst_stack.empty (*cst_l*)) :: stack) in - whrec Cst_stack.empty stack' - else match ReductionBehaviour.get (GlobRef.ConstRef (Projection.constant p)) with + match ReductionBehaviour.get (GlobRef.ConstRef (Projection.constant p)) with | None -> let stack' = (c, Stack.Proj (p, cst_l) :: stack) in let stack'', csts = whrec Cst_stack.empty stack' in @@ -693,24 +675,24 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = end) | LetIn (_,b,_,c) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fZETA -> - apply_subst (fun _ -> whrec) [b] sigma refold cst_l c stack + apply_subst (fun _ -> whrec) [b] sigma cst_l c stack | Cast (c,_,_) -> whrec cst_l (c, stack) | App (f,cl) -> whrec - (if refold then Cst_stack.add_args cl cst_l else cst_l) + (Cst_stack.add_args cl cst_l) (f, Stack.append_app cl stack) | Lambda (na,t,c) -> (match Stack.decomp stack with | Some _ when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA -> - apply_subst (fun _ -> whrec) [] sigma refold cst_l x stack + apply_subst (fun _ -> whrec) [] sigma cst_l x stack | None when CClosure.RedFlags.red_set flags CClosure.RedFlags.fETA -> let env' = push_rel (LocalAssum (na, t)) env in - let whrec' = whd_state_gen ~refold ~tactic_mode flags env' sigma in - (match EConstr.kind sigma (Stack.zip ~refold sigma (fst (whrec' (c, Stack.empty)))) with + let whrec' = whd_state_gen flags env' sigma in + (match EConstr.kind sigma (Stack.zip ~refold:true sigma (whrec' (c, Stack.empty))) with | App (f,cl) -> let napp = Array.length cl in if napp > 0 then - let (x', l'),_ = whrec' (Array.last cl, Stack.empty) in + let (x', l') = whrec' (Array.last cl, Stack.empty) in match EConstr.kind sigma x', l' with | Rel 1, [] -> let lc = Array.sub cl 0 (napp-1) in @@ -743,7 +725,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = |args, (Stack.Fix (f,s',cst_l)::s'') when use_fix -> let x' = Stack.zip sigma (x, args) in let out_sk = s' @ (Stack.append_app [|x'|] s'') in - reduce_and_refold_fix whrec env sigma refold cst_l f out_sk + reduce_and_refold_fix whrec env sigma cst_l f out_sk |args, (Stack.Cst (const,curr,remains,s',cst_l) :: s'') -> let x' = Stack.zip sigma (x, args) in begin match remains with @@ -755,7 +737,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = | Some body -> let const = (fst const, EInstance.make (snd const)) in let body = EConstr.of_constr body in - whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l) + whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, s' @ (Stack.append_app [|x'|] s''))) | Stack.Cst_proj p -> let stack = s' @ (Stack.append_app [|x'|] s'') in @@ -778,7 +760,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = if CClosure.RedFlags.red_set flags CClosure.RedFlags.fCOFIX then match Stack.strip_app stack with |args, ((Stack.Case _ |Stack.Proj _)::s') -> - reduce_and_refold_cofix whrec env sigma refold cst_l cofix stack + reduce_and_refold_cofix whrec env sigma cst_l cofix stack |_ -> fold () else fold () @@ -812,12 +794,10 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = in fun xs -> let (s,cst_l as res) = whrec (Option.default Cst_stack.empty csts) xs in - if tactic_mode then (Stack.best_state sigma s cst_l,Cst_stack.empty) else res + (Stack.best_state sigma s cst_l) let whd_cbn flags env sigma t = - let (state,_) = - (whd_state_gen ~refold:true ~tactic_mode:true flags env sigma (t, Stack.empty)) - in + let state = whd_state_gen flags env sigma (t, Stack.empty) in Stack.zip ~refold:true sigma state let norm_cbn flags env sigma t = diff --git a/test-suite/bugs/closed/bug_13903.v b/test-suite/bugs/closed/bug_13903.v new file mode 100644 index 0000000000..7c1820b85c --- /dev/null +++ b/test-suite/bugs/closed/bug_13903.v @@ -0,0 +1,5 @@ +Section test. +Variables (T : Type) (x : T). +#[using="x"] Definition test : unit := tt. +End test. +Check test : forall T, T -> unit. diff --git a/test-suite/bugs/closed/bug_13960.v b/test-suite/bugs/closed/bug_13960.v new file mode 100644 index 0000000000..947db9586f --- /dev/null +++ b/test-suite/bugs/closed/bug_13960.v @@ -0,0 +1,10 @@ +Require Ltac2.Ltac2. + +Set Default Goal Selector "!". + +Ltac2 t () := let _ := Message.print (Message.of_string "hi") in 42. + +Goal False. +Proof. +Ltac2 Eval t (). +Abort. diff --git a/test-suite/ltac2/ind.v b/test-suite/ltac2/ind.v new file mode 100644 index 0000000000..6f7352d224 --- /dev/null +++ b/test-suite/ltac2/ind.v @@ -0,0 +1,25 @@ +Require Import Ltac2.Ltac2. +Require Import Ltac2.Option. + +Ltac2 Eval + let nat := Option.get (Env.get [@Coq; @Init; @Datatypes; @nat]) in + let nat := match nat with + | Std.IndRef nat => nat + | _ => Control.throw Not_found + end in + let data := Ind.data nat in + (* Check that there is only one inductive in the block *) + let ntypes := Ind.nblocks data in + let () := if Int.equal ntypes 1 then () else Control.throw Not_found in + let nat' := Ind.repr (Ind.get_block data 0) in + (* Check it corresponds *) + let () := if Ind.equal nat nat' then () else Control.throw Not_found in + let () := if Int.equal (Ind.index nat) 0 then () else Control.throw Not_found in + (* Check the number of constructors *) + let nconstr := Ind.nconstructors data in + let () := if Int.equal nconstr 2 then () else Control.throw Not_found in + (* Create a fresh instance *) + let s := Ind.get_constructor data 1 in + let s := Env.instantiate (Std.ConstructRef s) in + constr:($s 0) +. diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index 6978fa1ddf..a1a4da6f37 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -87,7 +87,7 @@ Program Instance unit_eqdec : EqDec unit eq := fun x y => in_left. Next Obligation. Proof. - destruct x ; destruct y. + do 2 match goal with [ x : () |- _ ] => destruct x end. reflexivity. Qed. @@ -142,7 +142,10 @@ Program Instance list_eqdec `(eqa : EqDec A eq) : EqDec (list A) eq := | _, _ => in_right end }. - Next Obligation. destruct y ; unfold not in *; eauto. Defined. + Next Obligation. + match goal with y : list _ |- _ => destruct y end ; + unfold not in *; eauto. + Defined. Solve Obligations with unfold equiv, complement in * ; program_simpl ; intuition (discriminate || eauto). diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index 6a98af39aa..3e71a60fa6 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -87,7 +87,7 @@ Tactic Notation "clsubst" "*" := clsubst_nofail. Lemma nequiv_equiv_trans : forall `{Setoid A} (x y z : A), x =/= y -> y == z -> x =/= z. Proof with auto. - intros; intro. + intros A ? x y z H H0 H1. assert(z == y) by (symmetry ; auto). assert(x == y) by (transitivity z ; eauto). contradiction. @@ -95,7 +95,7 @@ Qed. Lemma equiv_nequiv_trans : forall `{Setoid A} (x y z : A), x == y -> y =/= z -> x =/= z. Proof. - intros; intro. + intros A ? x y z **; intro. assert(y == x) by (symmetry ; auto). assert(y == z) by (transitivity x ; eauto). contradiction. diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index 2947c4831f..f4220e3aa1 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -96,7 +96,7 @@ Program Instance unit_eqdec : EqDec (eq_setoid unit) := Next Obligation. Proof. - destruct x ; destruct y. + do 2 match goal with x : () |- _ => destruct x end. reflexivity. Qed. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index d6277b3bb5..5298f3160a 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -877,6 +877,36 @@ Section Elts. intros H. simpl. now destruct (eq_dec x y). Qed. + Lemma count_occ_app l1 l2 x : + count_occ (l1 ++ l2) x = count_occ l1 x + count_occ l2 x. + Proof. + induction l1 as [ | h l1 IHl1]; cbn; auto. + now destruct (eq_dec h x); [ rewrite IHl1 | ]. + Qed. + + Lemma count_occ_elt_eq l1 l2 x y : x = y -> + count_occ (l1 ++ x :: l2) y = S (count_occ (l1 ++ l2) y). + Proof. + intros ->. + rewrite ? count_occ_app; cbn. + destruct (eq_dec y y) as [Heq | Hneq]; + [ apply Nat.add_succ_r | now contradiction Hneq ]. + Qed. + + Lemma count_occ_elt_neq l1 l2 x y : x <> y -> + count_occ (l1 ++ x :: l2) y = count_occ (l1 ++ l2) y. + Proof. + intros Hxy. + rewrite ? count_occ_app; cbn. + now destruct (eq_dec x y) as [Heq | Hneq]; [ contradiction Hxy | ]. + Qed. + + Lemma count_occ_bound x l : count_occ l x <= length l. + Proof. + induction l as [|h l]; cbn; auto. + destruct (eq_dec h x); [ apply (proj1 (Nat.succ_le_mono _ _)) | ]; intuition. + Qed. + End Elts. (*******************************) @@ -3242,6 +3272,54 @@ Section Repeat. now rewrite (IHl HF') at 1. Qed. + Hypothesis decA : forall x y : A, {x = y}+{x <> y}. + + Lemma count_occ_repeat_eq x y n : x = y -> count_occ decA (repeat y n) x = n. + Proof. + intros ->. + induction n; cbn; auto. + destruct (decA y y); auto. + exfalso; intuition. + Qed. + + Lemma count_occ_repeat_neq x y n : x <> y -> count_occ decA (repeat y n) x = 0. + Proof. + intros Hneq. + induction n; cbn; auto. + destruct (decA y x); auto. + exfalso; intuition. + Qed. + + Lemma count_occ_unique x l : count_occ decA l x = length l -> l = repeat x (length l). + Proof. + induction l as [|h l]; cbn; intros Hocc; auto. + destruct (decA h x). + - f_equal; intuition. + - assert (Hb := count_occ_bound decA x l). + rewrite Hocc in Hb. + exfalso; apply (Nat.nle_succ_diag_l _ Hb). + Qed. + + Lemma count_occ_repeat_excl x l : + (forall y, y <> x -> count_occ decA l y = 0) -> l = repeat x (length l). + Proof. + intros Hocc. + apply Forall_eq_repeat, Forall_forall; intros z Hin. + destruct (decA z x) as [Heq|Hneq]; auto. + apply Hocc, count_occ_not_In in Hneq; intuition. + Qed. + + Lemma count_occ_sgt l x : l = x :: nil <-> + count_occ decA l x = 1 /\ forall y, y <> x -> count_occ decA l y = 0. + Proof. + split. + - intros ->; cbn; split; intros; destruct decA; subst; intuition. + - intros [Heq Hneq]. + apply count_occ_repeat_excl in Hneq. + rewrite Hneq, count_occ_repeat_eq in Heq; trivial. + now rewrite Heq in Hneq. + Qed. + End Repeat. Lemma repeat_to_concat A n (a:A) : diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index 826815410a..69b158a87e 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -71,7 +71,7 @@ Hint Constructors NoDupA : core. Lemma NoDupA_altdef : forall l, NoDupA l <-> ForallOrdPairs (complement eqA) l. Proof. - split; induction 1; constructor; auto. + split; induction 1 as [|a l H rest]; constructor; auto. rewrite Forall_forall. intros b Hb. intro Eq; elim H. rewrite InA_alt. exists b; auto. rewrite InA_alt; intros (a' & Haa' & Ha'). @@ -85,7 +85,7 @@ Definition inclA l l' := forall x, InA x l -> InA x l'. Definition equivlistA l l' := forall x, InA x l <-> InA x l'. Lemma incl_nil l : inclA nil l. -Proof. intro. intros. inversion H. Qed. +Proof. intros a H. inversion H. Qed. #[local] Hint Resolve incl_nil : list. @@ -128,7 +128,7 @@ Qed. Global Instance eqlistA_equiv : Equivalence eqlistA. Proof. constructor; red. - induction x; auto. + intros x; induction x; auto. induction 1; auto. intros x y z H; revert z; induction H; auto. inversion 1; subst; auto. invlist eqlistA; eauto with *. @@ -138,9 +138,9 @@ Qed. Global Instance eqlistA_equivlistA : subrelation eqlistA equivlistA. Proof. - intros x x' H. induction H. + intros x x' H. induction H as [|? ? ? ? H ? IHeqlistA]. intuition. - red; intros. + red; intros x0. rewrite 2 InA_cons. rewrite (IHeqlistA x0), H; intuition. Qed. @@ -165,7 +165,7 @@ Hint Immediate InA_eqA : core. Lemma In_InA : forall l x, In x l -> InA x l. Proof. - simple induction l; simpl; intuition. + intros l; induction l; simpl; intuition. subst; auto. Qed. #[local] @@ -174,8 +174,9 @@ Hint Resolve In_InA : core. Lemma InA_split : forall l x, InA x l -> exists l1 y l2, eqA x y /\ l = l1++y::l2. Proof. -induction l; intros; inv. +intros l; induction l as [|a l IHl]; intros x H; inv. exists (@nil A); exists a; exists l; auto. +match goal with H' : InA x l |- _ => rename H' into H0 end. destruct (IHl x H0) as (l1,(y,(l2,(H1,H2)))). exists (a::l1); exists y; exists l2; auto. split; simpl; f_equal; auto. @@ -184,9 +185,10 @@ Qed. Lemma InA_app : forall l1 l2 x, InA x (l1 ++ l2) -> InA x l1 \/ InA x l2. Proof. - induction l1; simpl in *; intuition. + intros l1; induction l1 as [|a l1 IHl1]; simpl in *; intuition. inv; auto. - elim (IHl1 l2 x H0); auto. + match goal with H0' : InA _ (l1 ++ _) |- _ => rename H0' into H0 end. + elim (IHl1 _ _ H0); auto. Qed. Lemma InA_app_iff : forall l1 l2 x, @@ -194,7 +196,7 @@ Lemma InA_app_iff : forall l1 l2 x, Proof. split. apply InA_app. - destruct 1; generalize H; do 2 rewrite InA_alt. + destruct 1 as [H|H]; generalize H; do 2 rewrite InA_alt. destruct 1 as (y,(H1,H2)); exists y; split; auto. apply in_or_app; auto. destruct 1 as (y,(H1,H2)); exists y; split; auto. @@ -240,11 +242,12 @@ Lemma NoDupA_app : forall l l', NoDupA l -> NoDupA l' -> (forall x, InA x l -> InA x l' -> False) -> NoDupA (l++l'). Proof. -induction l; simpl; auto; intros. +intros l; induction l as [|a l IHl]; simpl; auto; intros l' H H0 H1. inv. constructor. rewrite InA_alt; intros (y,(H4,H5)). destruct (in_app_or _ _ _ H5). +match goal with H2' : ~ InA a l |- _ => rename H2' into H2 end. elim H2. rewrite InA_alt. exists y; auto. @@ -253,13 +256,13 @@ auto. rewrite InA_alt. exists y; auto. apply IHl; auto. -intros. +intros x ? ?. apply (H1 x); auto. Qed. Lemma NoDupA_rev : forall l, NoDupA l -> NoDupA (rev l). Proof. -induction l. +intros l; induction l. simpl; auto. simpl; intros. inv. @@ -270,17 +273,17 @@ intros x. rewrite InA_alt. intros (x1,(H2,H3)). intro; inv. -destruct H0. -rewrite <- H4, H2. +match goal with H0 : ~ InA _ _ |- _ => destruct H0 end. +match goal with H4 : eqA x ?x' |- InA ?x' _ => rewrite <- H4, H2 end. apply In_InA. rewrite In_rev; auto. Qed. Lemma NoDupA_split : forall l l' x, NoDupA (l++x::l') -> NoDupA (l++l'). Proof. - induction l; simpl in *; intros; inv; auto. + intros l; induction l; simpl in *; intros; inv; auto. constructor; eauto. - contradict H0. + match goal with H0 : ~ InA _ _ |- _ => contradict H0 end. rewrite InA_app_iff in *. rewrite InA_cons. intuition. @@ -288,17 +291,17 @@ Qed. Lemma NoDupA_swap : forall l l' x, NoDupA (l++x::l') -> NoDupA (x::l++l'). Proof. - induction l; simpl in *; intros; inv; auto. + intros l; induction l as [|a l IHl]; simpl in *; intros l' x H; inv; auto. constructor; eauto. - assert (H2:=IHl _ _ H1). + match goal with H1 : NoDupA (l ++ x :: l') |- _ => assert (H2:=IHl _ _ H1) end. inv. rewrite InA_cons. red; destruct 1. - apply H0. + match goal with H0 : ~ InA a (l ++ x :: l') |- _ => apply H0 end. rewrite InA_app_iff in *; rewrite InA_cons; auto. - apply H; auto. + auto. constructor. - contradict H0. + match goal with H0 : ~ InA a (l ++ x :: l') |- _ => contradict H0 end. rewrite InA_app_iff in *; rewrite InA_cons; intuition. eapply NoDupA_split; eauto. Qed. @@ -356,19 +359,21 @@ Lemma equivlistA_NoDupA_split l l1 l2 x y : eqA x y -> NoDupA (x::l) -> NoDupA (l1++y::l2) -> equivlistA (x::l) (l1++y::l2) -> equivlistA l (l1++l2). Proof. - intros; intro a. + intros H H0 H1 H2; intro a. generalize (H2 a). rewrite !InA_app_iff, !InA_cons. inv. assert (SW:=NoDupA_swap H1). inv. - rewrite InA_app_iff in H0. + rewrite InA_app_iff in *. split; intros. - assert (~eqA a x) by (contradict H3; rewrite <- H3; auto). + match goal with H3 : ~ InA x l |- _ => + assert (~eqA a x) by (contradict H3; rewrite <- H3; auto) + end. assert (~eqA a y) by (rewrite <- H; auto). tauto. - assert (OR : eqA a x \/ InA a l) by intuition. clear H6. + assert (OR : eqA a x \/ InA a l) by intuition. destruct OR as [EQN|INA]; auto. - elim H0. + match goal with H0 : ~ (InA y l1 \/ InA y l2) |- _ => elim H0 end. rewrite <-H,<-EQN; auto. Qed. @@ -448,7 +453,7 @@ Qed. Lemma ForallOrdPairs_inclA : forall l l', NoDupA l' -> inclA l' l -> ForallOrdPairs R l -> ForallOrdPairs R l'. Proof. -induction l' as [|x l' IH]. +intros l l'. induction l' as [|x l' IH]. constructor. intros ND Incl FOP. apply FOP_cons; inv; unfold inclA in *; auto. rewrite Forall_forall; intros y Hy. @@ -476,7 +481,7 @@ Lemma fold_right_commutes_restr : forall s1 s2 x, ForallOrdPairs R (s1++x::s2) -> eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))). Proof. -induction s1; simpl; auto; intros. +intros s1; induction s1 as [|a s1 IHs1]; simpl; auto; intros s2 x H. reflexivity. transitivity (f a (f x (fold_right f i (s1++s2)))). apply Comp; auto. @@ -484,7 +489,9 @@ apply IHs1. invlist ForallOrdPairs; auto. apply TraR. invlist ForallOrdPairs; auto. -rewrite Forall_forall in H0; apply H0. +match goal with H0 : Forall (R a) (s1 ++ x :: s2) |- R a x => + rewrite Forall_forall in H0; apply H0 +end. apply in_or_app; simpl; auto. Qed. @@ -492,14 +499,14 @@ Lemma fold_right_equivlistA_restr : forall s s', NoDupA s -> NoDupA s' -> ForallOrdPairs R s -> equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s'). Proof. - simple induction s. - destruct s'; simpl. + intros s; induction s as [|x l Hrec]. + intros s'; destruct s' as [|a s']; simpl. intros; reflexivity. - unfold equivlistA; intros. + unfold equivlistA; intros H H0 H1 H2. destruct (H2 a). assert (InA a nil) by auto; inv. - intros x l Hrec s' N N' F E; simpl in *. - assert (InA x s') by (rewrite <- (E x); auto). + intros s' N N' F E; simpl in *. + assert (InA x s') as H by (rewrite <- (E x); auto). destruct (InA_split H) as (s1,(y,(s2,(H1,H2)))). subst s'. transitivity (f x (fold_right f i (s1++s2))). @@ -520,7 +527,7 @@ Lemma fold_right_add_restr : forall s' s x, NoDupA s -> NoDupA s' -> ForallOrdPairs R s' -> ~ InA x s -> equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f i s)). Proof. - intros; apply (@fold_right_equivlistA_restr s' (x::s)); auto. + intros s' s x **; apply (@fold_right_equivlistA_restr s' (x::s)); auto. Qed. End Fold_With_Restriction. @@ -532,7 +539,7 @@ Variable Tra :transpose f. Lemma fold_right_commutes : forall s1 s2 x, eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))). Proof. -induction s1; simpl; auto; intros. +intros s1; induction s1 as [|a s1 IHs1]; simpl; auto; intros s2 x. reflexivity. transitivity (f a (f x (fold_right f i (s1++s2)))); auto. apply Comp; auto. @@ -542,7 +549,7 @@ Lemma fold_right_equivlistA : forall s s', NoDupA s -> NoDupA s' -> equivlistA s s' -> eqB (fold_right f i s) (fold_right f i s'). Proof. -intros; apply fold_right_equivlistA_restr with (R:=fun _ _ => True); +intros; apply (fold_right_equivlistA_restr (R:=fun _ _ => True)); repeat red; auto. apply ForallPairs_ForallOrdPairs; try red; auto. Qed. @@ -551,7 +558,7 @@ Lemma fold_right_add : forall s' s x, NoDupA s -> NoDupA s' -> ~ InA x s -> equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f i s)). Proof. - intros; apply (@fold_right_equivlistA s' (x::s)); auto. + intros s' s x **; apply (@fold_right_equivlistA s' (x::s)); auto. Qed. End Fold. @@ -571,7 +578,7 @@ Lemma fold_right_eqlistA2 : eqB (fold_right f i s) (fold_right f j s'). Proof. intros s. - induction s;intros. + induction s as [|a s IHs];intros s' i j heqij heqss'. - inversion heqss'. subst. simpl. @@ -604,7 +611,7 @@ Lemma fold_right_commutes_restr2 : forall s1 s2 x (i j:B) (heqij: eqB i j), ForallOrdPairs R (s1++x::s2) -> eqB (fold_right f i (s1++x::s2)) (f x (fold_right f j (s1++s2))). Proof. -induction s1; simpl; auto; intros. +intros s1; induction s1 as [|a s1 IHs1]; simpl; auto; intros s2 x i j heqij ?. - apply Comp. + destruct eqA_equiv. apply Equivalence_Reflexive. + eapply fold_right_eqlistA2. @@ -617,7 +624,9 @@ induction s1; simpl; auto; intros. invlist ForallOrdPairs; auto. apply TraR. invlist ForallOrdPairs; auto. - rewrite Forall_forall in H0; apply H0. + match goal with H0 : Forall (R a) (s1 ++ x :: s2) |- _ => + rewrite Forall_forall in H0; apply H0 + end. apply in_or_app; simpl; auto. reflexivity. Qed. @@ -628,14 +637,14 @@ Lemma fold_right_equivlistA_restr2 : equivlistA s s' -> eqB i j -> eqB (fold_right f i s) (fold_right f j s'). Proof. - simple induction s. - destruct s'; simpl. + intros s; induction s as [|x l Hrec]. + intros s'; destruct s' as [|a s']; simpl. intros. assumption. - unfold equivlistA; intros. + unfold equivlistA; intros ? ? H H0 H1 H2 **. destruct (H2 a). assert (InA a nil) by auto; inv. - intros x l Hrec s' i j N N' F E eqij; simpl in *. - assert (InA x s') by (rewrite <- (E x); auto). + intros s' i j N N' F E eqij; simpl in *. + assert (InA x s') as H by (rewrite <- (E x); auto). destruct (InA_split H) as (s1,(y,(s2,(H1,H2)))). subst s'. transitivity (f x (fold_right f j (s1++s2))). @@ -663,7 +672,7 @@ Lemma fold_right_add_restr2 : forall s' s i j x, NoDupA s -> NoDupA s' -> eqB i j -> ForallOrdPairs R s' -> ~ InA x s -> equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f j s)). Proof. - intros; apply (@fold_right_equivlistA_restr2 s' (x::s) i j); auto. + intros s' s i j x **; apply (@fold_right_equivlistA_restr2 s' (x::s) i j); auto. Qed. End Fold2_With_Restriction. @@ -674,7 +683,7 @@ Lemma fold_right_commutes2 : forall s1 s2 i x x', eqA x x' -> eqB (fold_right f i (s1++x::s2)) (f x' (fold_right f i (s1++s2))). Proof. - induction s1;simpl;intros. + intros s1; induction s1 as [|a s1 IHs1];simpl;intros s2 i x x' H. - apply Comp;auto. reflexivity. - transitivity (f a (f x' (fold_right f i (s1++s2)))); auto. @@ -688,7 +697,7 @@ Lemma fold_right_equivlistA2 : equivlistA s s' -> eqB (fold_right f i s) (fold_right f j s'). Proof. red in Tra. -intros; apply fold_right_equivlistA_restr2 with (R:=fun _ _ => True); +intros; apply (fold_right_equivlistA_restr2 (R:=fun _ _ => True)); repeat red; auto. apply ForallPairs_ForallOrdPairs; try red; auto. Qed. @@ -697,9 +706,9 @@ Lemma fold_right_add2 : forall s' s i j x, NoDupA s -> NoDupA s' -> eqB i j -> ~ InA x s -> equivlistA s' (x::s) -> eqB (fold_right f i s') (f x (fold_right f j s)). Proof. - intros. + intros s' s i j x **. replace (f x (fold_right f j s)) with (fold_right f j (x::s)) by auto. - eapply fold_right_equivlistA2;auto. + eapply fold_right_equivlistA2;auto. Qed. End Fold2. @@ -710,7 +719,7 @@ Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}. Lemma InA_dec : forall x l, { InA x l } + { ~ InA x l }. Proof. -induction l. +intros x l; induction l as [|a l IHl]. right; auto. intro; inv. destruct (eqA_dec x a). @@ -729,28 +738,30 @@ Fixpoint removeA (x : A) (l : list A) : list A := Lemma removeA_filter : forall x l, removeA x l = filter (fun y => if eqA_dec x y then false else true) l. Proof. -induction l; simpl; auto. +intros x l; induction l as [|a l IHl]; simpl; auto. destruct (eqA_dec x a); auto. rewrite IHl; auto. Qed. Lemma removeA_InA : forall l x y, InA y (removeA x l) <-> InA y l /\ ~eqA x y. Proof. -induction l; simpl; auto. -split. +intros l; induction l as [|a l IHl]; simpl; auto. +intros x y; split. intro; inv. destruct 1; inv. -intros. +intros x y. destruct (eqA_dec x a) as [Heq|Hnot]; simpl; auto. rewrite IHl; split; destruct 1; split; auto. inv; auto. -destruct H0; transitivity a; auto. +match goal with H0 : ~ eqA x y |- _ => destruct H0 end; transitivity a; auto. split. intro; inv. split; auto. contradict Hnot. transitivity y; auto. -rewrite (IHl x y) in H0; destruct H0; auto. +match goal with H0 : InA y (removeA x l) |- _ => + rewrite (IHl x y) in H0; destruct H0; auto +end. destruct 1; inv; auto. right; rewrite IHl; auto. Qed. @@ -758,7 +769,7 @@ Qed. Lemma removeA_NoDupA : forall s x, NoDupA s -> NoDupA (removeA x s). Proof. -simple induction s; simpl; intros. +intros s; induction s as [|a s IHs]; simpl; intros x ?. auto. inv. destruct (eqA_dec x a); simpl; auto. @@ -770,16 +781,16 @@ Qed. Lemma removeA_equivlistA : forall l l' x, ~InA x l -> equivlistA (x :: l) l' -> equivlistA l (removeA x l'). Proof. -unfold equivlistA; intros. +unfold equivlistA; intros l l' x H H0 x0. rewrite removeA_InA. -split; intros. +split; intros H1. rewrite <- H0; split; auto. contradict H. apply InA_eqA with x0; auto. rewrite <- (H0 x0) in H1. destruct H1. inv; auto. -elim H2; auto. +match goal with H2 : ~ eqA x x0 |- _ => elim H2; auto end. Qed. End Remove. @@ -806,7 +817,7 @@ Hint Constructors lelistA sort : core. Lemma InfA_ltA : forall l x y, ltA x y -> InfA y l -> InfA x l. Proof. - destruct l; constructor. inv; eauto. + intros l; destruct l; constructor. inv; eauto. Qed. Global Instance InfA_compat : Proper (eqA==>eqlistA==>iff) InfA. @@ -815,8 +826,8 @@ Proof using eqA_equiv ltA_compat. (* and not ltA_strorder *) inversion_clear Hll'. intuition. split; intro; inv; constructor. - rewrite <- Hxx', <- H; auto. - rewrite Hxx', H; auto. + match goal with H : eqA _ _ |- _ => rewrite <- Hxx', <- H; auto end. + match goal with H : eqA _ _ |- _ => rewrite Hxx', H; auto end. Qed. (** For compatibility, can be deduced from [InfA_compat] *) @@ -830,9 +841,9 @@ Hint Immediate InfA_ltA InfA_eqA : core. Lemma SortA_InfA_InA : forall l x a, SortA l -> InfA a l -> InA x l -> ltA a x. Proof. - simple induction l. - intros. inv. - intros. inv. + intros l; induction l as [|a l IHl]. + intros x a **. inv. + intros x a0 **. inv. setoid_replace x with a; auto. eauto. Qed. @@ -840,13 +851,13 @@ Qed. Lemma In_InfA : forall l x, (forall y, In y l -> ltA x y) -> InfA x l. Proof. - simple induction l; simpl; intros; constructor; auto. + intros l; induction l; simpl; intros; constructor; auto. Qed. Lemma InA_InfA : forall l x, (forall y, InA y l -> ltA x y) -> InfA x l. Proof. - simple induction l; simpl; intros; constructor; auto. + intros l; induction l; simpl; intros; constructor; auto. Qed. (* In fact, this may be used as an alternative definition for InfA: *) @@ -861,7 +872,7 @@ Qed. Lemma InfA_app : forall l1 l2 a, InfA a l1 -> InfA a l2 -> InfA a (l1++l2). Proof. - induction l1; simpl; auto. + intros l1; induction l1; simpl; auto. intros; inv; auto. Qed. @@ -870,7 +881,7 @@ Lemma SortA_app : (forall x y, InA x l1 -> InA y l2 -> ltA x y) -> SortA (l1 ++ l2). Proof. - induction l1; simpl in *; intuition. + intros l1; induction l1; intros l2; simpl in *; intuition. inv. constructor; auto. apply InfA_app; auto. @@ -879,8 +890,8 @@ Qed. Lemma SortA_NoDupA : forall l, SortA l -> NoDupA l. Proof. - simple induction l; auto. - intros x l' H H0. + intros l; induction l as [|x l' H]; auto. + intros H0. inv. constructor; auto. intro. @@ -922,7 +933,7 @@ Qed. Global Instance rev_eqlistA_compat : Proper (eqlistA==>eqlistA) (@rev A). Proof. -repeat red. intros. +repeat red. intros x y ?. rewrite <- (app_nil_r (rev x)), <- (app_nil_r (rev y)). apply eqlistA_rev_app; auto. Qed. @@ -936,15 +947,15 @@ Qed. Lemma SortA_equivlistA_eqlistA : forall l l', SortA l -> SortA l' -> equivlistA l l' -> eqlistA l l'. Proof. -induction l; destruct l'; simpl; intros; auto. -destruct (H1 a); assert (InA a nil) by auto; inv. +intros l; induction l as [|a l IHl]; intros l'; destruct l' as [|a0 l']; simpl; intros H H0 H1; auto. +destruct (H1 a0); assert (InA a0 nil) by auto; inv. destruct (H1 a); assert (InA a nil) by auto; inv. inv. assert (forall y, InA y l -> ltA a y). -intros; eapply SortA_InfA_InA with (l:=l); eauto. +intros; eapply (SortA_InfA_InA (l:=l)); eauto. assert (forall y, InA y l' -> ltA a0 y). -intros; eapply SortA_InfA_InA with (l:=l'); eauto. -clear H3 H4. +intros; eapply (SortA_InfA_InA (l:=l')); eauto. +do 2 match goal with H : InfA _ _ |- _ => clear H end. assert (eqA a a0). destruct (H1 a). destruct (H1 a0). @@ -953,13 +964,19 @@ assert (eqA a a0). elim (StrictOrder_Irreflexive a); eauto. constructor; auto. apply IHl; auto. -split; intros. +intros x; split; intros. destruct (H1 x). assert (InA x (a0::l')) by auto. inv; auto. -rewrite H9,<-H3 in H4. elim (StrictOrder_Irreflexive a); eauto. +match goal with H3 : eqA a a0, H4 : InA x l, H9 : eqA x a0 |- InA x l' => + rewrite H9,<-H3 in H4 +end. +elim (StrictOrder_Irreflexive a); eauto. destruct (H1 x). assert (InA x (a::l)) by auto. inv; auto. -rewrite H9,H3 in H4. elim (StrictOrder_Irreflexive a0); eauto. +match goal with H3 : eqA a a0, H4 : InA x l', H9 : eqA x a |- InA x l => + rewrite H9,H3 in H4 +end. +elim (StrictOrder_Irreflexive a0); eauto. Qed. End EqlistA. @@ -970,12 +987,12 @@ Section Filter. Lemma filter_sort : forall f l, SortA l -> SortA (List.filter f l). Proof. -induction l; simpl; auto. +intros f l; induction l as [|a l IHl]; simpl; auto. intros; inv; auto. destruct (f a); auto. constructor; auto. apply In_InfA; auto. -intros. +intros y H. rewrite filter_In in H; destruct H. eapply SortA_InfA_InA; eauto. Qed. @@ -984,12 +1001,14 @@ Arguments eq {A} x _. Lemma filter_InA : forall f, Proper (eqA==>eq) f -> forall l x, InA x (List.filter f l) <-> InA x l /\ f x = true. Proof. +(* Unset Mangle Names. *) clear sotrans ltA ltA_strorder ltA_compat. -intros; do 2 rewrite InA_alt; intuition. -destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; exists y; intuition. -destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; intuition. +intros f H l x; do 2 rewrite InA_alt; intuition; + match goal with Hex' : exists _, _ |- _ => rename Hex' into Hex end. +destruct Hex as (y,(H0,H1)); rewrite filter_In in H1; exists y; intuition. +destruct Hex as (y,(H0,H1)); rewrite filter_In in H1; intuition. rewrite (H _ _ H0); auto. -destruct H1 as (y,(H0,H1)); exists y; rewrite filter_In; intuition. +destruct Hex as (y,(H0,H1)); exists y; rewrite filter_In; intuition. rewrite <- (H _ _ H0); auto. Qed. @@ -997,19 +1016,20 @@ Lemma filter_split : forall f, (forall x y, f x = true -> f y = false -> ltA x y) -> forall l, SortA l -> l = filter f l ++ filter (fun x=>negb (f x)) l. Proof. -induction l; simpl; intros; auto. +intros f H l; induction l as [|a l IHl]; simpl; intros H0; auto. inv. +match goal with H1' : SortA l, H2' : InfA a l |- _ => rename H1' into H1, H2' into H2 end. rewrite IHl at 1; auto. case_eq (f a); simpl; intros; auto. -assert (forall e, In e l -> f e = false). - intros. +assert (forall e, In e l -> f e = false) as H3. + intros e H3. assert (H4:=SortA_InfA_InA H1 H2 (In_InA H3)). case_eq (f e); simpl; intros; auto. elim (StrictOrder_Irreflexive e). transitivity a; auto. replace (List.filter f l) with (@nil A); auto. -generalize H3; clear; induction l; simpl; auto. -case_eq (f a); auto; intros. +generalize H3; clear; induction l as [|a l IHl]; simpl; auto. +case_eq (f a); auto; intros H H3. rewrite H3 in H; auto; try discriminate. Qed. @@ -1043,23 +1063,24 @@ Lemma findA_NoDupA : Proof. set (eqk := fun p p' : A*B => eqA (fst p) (fst p')). set (eqke := fun p p' : A*B => eqA (fst p) (fst p') /\ snd p = snd p'). -induction l; intros; simpl. -split; intros; try discriminate. +intros l; induction l as [|a l IHl]; intros a0 b H; simpl. +split; intros H0; try discriminate. invlist InA. destruct a as (a',b'); rename a0 into a. invlist NoDupA. split; intros. invlist InA. -compute in H2; destruct H2. subst b'. +match goal with H2 : eqke (a, b) (a', b') |- _ => compute in H2; destruct H2 end. +subst b'. destruct (eqA_dec a a'); intuition. destruct (eqA_dec a a') as [HeqA|]; simpl. -contradict H0. -revert HeqA H2; clear - eqA_equiv. +match goal with H0 : ~ InA eqk (a', b') l |- _ => contradict H0 end. +match goal with H2 : InA eqke (a, b) l |- _ => revert HeqA H2; clear - eqA_equiv end. induction l. intros; invlist InA. intros; invlist InA; auto. -destruct a0. -compute in H; destruct H. +match goal with |- InA eqk _ (?p :: _) => destruct p as [a0 b0] end. +match goal with H : eqke (a, b) (a0, b0) |- _ => compute in H; destruct H end. subst b. left; auto. compute. diff --git a/theories/Logic/ProofIrrelevanceFacts.v b/theories/Logic/ProofIrrelevanceFacts.v index 131668154e..7560ea96b5 100644 --- a/theories/Logic/ProofIrrelevanceFacts.v +++ b/theories/Logic/ProofIrrelevanceFacts.v @@ -27,7 +27,7 @@ Module ProofIrrelevanceTheory (M:ProofIrrelevance). forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h. Proof. - intros; rewrite M.proof_irrelevance with (p1:=h) (p2:=eq_refl p). + intros U p Q x h; rewrite (M.proof_irrelevance _ h (eq_refl p)). reflexivity. Qed. End Eq_rect_eq. @@ -45,8 +45,8 @@ Module ProofIrrelevanceTheory (M:ProofIrrelevance). forall (U:Type) (P:U->Prop) (x y:U) (p:P x) (q:P y), x = y -> exist P x p = exist P y q. Proof. - intros. - rewrite M.proof_irrelevance with (p1:=q) (p2:=eq_rect x P p y H). + intros U P x y p q H. + rewrite (M.proof_irrelevance _ q (eq_rect x P p y H)). elim H using eq_indd. reflexivity. Qed. @@ -55,8 +55,8 @@ Module ProofIrrelevanceTheory (M:ProofIrrelevance). forall (U:Type) (P:U->Prop) (x y:U) (p:P x) (q:P y), x = y -> existT P x p = existT P y q. Proof. - intros. - rewrite M.proof_irrelevance with (p1:=q) (p2:=eq_rect x P p y H). + intros U P x y p q H. + rewrite (M.proof_irrelevance _ q (eq_rect x P p y H)). elim H using eq_indd. reflexivity. Qed. diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index 9788ad50dc..9540bc1075 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -68,10 +68,11 @@ Ltac pi := repeat f_equal ; apply proof_irrelevance. Lemma subset_eq : forall A (P : A -> Prop) (n m : sig P), n = m <-> `n = `m. Proof. + intros A P n m. destruct n as (x,p). destruct m as (x',p'). simpl. - split ; intros ; subst. + split ; intros H ; subst. - inversion H. reflexivity. @@ -92,7 +93,7 @@ Lemma match_eq_rewrite : forall (A B : Type) (x : A) (fn : {y : A | y = x} -> B) (y : {y:A | y = x}), match_eq A B x fn = fn y. Proof. - intros. + intros A B x fn y. unfold match_eq. f_equal. destruct y. diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index 45fb48ad5d..2bf54baef3 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -535,6 +535,32 @@ Proof. now apply Permutation_cons_inv with x. Qed. +Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}. + +Lemma Permutation_count_occ l1 l2 : + Permutation l1 l2 <-> forall x, count_occ eq_dec l1 x = count_occ eq_dec l2 x. +Proof. + split. + - induction 1 as [ | y l1 l2 HP IHP | y z l | l1 l2 l3 HP1 IHP1 HP2 IHP2 ]; + cbn; intros a; auto. + + now rewrite IHP. + + destruct (eq_dec y a); destruct (eq_dec z a); auto. + + now rewrite IHP1, IHP2. + - revert l2; induction l1 as [|y l1 IHl1]; cbn; intros l2 Hocc. + + replace l2 with (@nil A); auto. + symmetry; apply (count_occ_inv_nil eq_dec); intuition. + + assert (exists l2' l2'', l2 = l2' ++ y :: l2'') as [l2' [l2'' ->]]. + { specialize (Hocc y). + destruct (eq_dec y y); intuition. + apply in_split, (count_occ_In eq_dec). + rewrite <- Hocc; apply Nat.lt_0_succ. } + apply Permutation_cons_app, IHl1. + intros z; specialize (Hocc z); destruct (eq_dec y z) as [Heq | Hneq]. + * rewrite (count_occ_elt_eq _ _ _ Heq) in Hocc. + now injection Hocc. + * now rewrite (count_occ_elt_neq _ _ _ Hneq) in Hocc. + Qed. + End Permutation_properties. Section Permutation_map. diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v index 206eb606d2..422316d879 100644 --- a/theories/Sorting/Sorted.v +++ b/theories/Sorting/Sorted.v @@ -71,6 +71,7 @@ Section defs. (forall a l, Sorted l -> P l -> HdRel a l -> P (a :: l)) -> forall l:list A, Sorted l -> P l. Proof. + intros P ? ? l. induction l. firstorder using Sorted_inv. firstorder using Sorted_inv. Qed. @@ -78,7 +79,8 @@ Section defs. Proof. split; [induction 1 as [|a l [|]]| induction 1]; auto using Sorted, LocallySorted, HdRel. - inversion H1; subst; auto using LocallySorted. + match goal with H1 : HdRel a (_ :: _) |- _ => inversion H1 end. + subst; auto using LocallySorted. Qed. (** Strongly sorted: elements of the list are pairwise ordered *) @@ -90,7 +92,7 @@ Section defs. Lemma StronglySorted_inv : forall a l, StronglySorted (a :: l) -> StronglySorted l /\ Forall (R a) l. Proof. - intros; inversion H; auto. + intros a l H; inversion H; auto. Defined. Lemma StronglySorted_rect : @@ -99,7 +101,7 @@ Section defs. (forall a l, StronglySorted l -> P l -> Forall (R a) l -> P (a :: l)) -> forall l, StronglySorted l -> P l. Proof. - induction l; firstorder using StronglySorted_inv. + intros P ? ? l; induction l; firstorder using StronglySorted_inv. Defined. Lemma StronglySorted_rec : @@ -120,7 +122,8 @@ Section defs. Lemma Sorted_extends : Transitive R -> forall a l, Sorted (a::l) -> Forall (R a) l. Proof. - intros. change match a :: l with [] => True | a :: l => Forall (R a) l end. + intros H a l H0. + change match a :: l with [] => True | a :: l => Forall (R a) l end. induction H0 as [|? ? ? ? H1]; [trivial|]. destruct H1; constructor; trivial. eapply Forall_impl; [|eassumption]. diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v index c923b503a7..a49e21fa92 100644 --- a/theories/Structures/DecidableType.v +++ b/theories/Structures/DecidableType.v @@ -93,7 +93,7 @@ Module KeyDecidableType(D:DecidableType). Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m. Proof. - intros; apply InA_eqA with p; auto using eqk_equiv. + intros p q m **; apply InA_eqA with p; auto using eqk_equiv. Qed. Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). @@ -106,18 +106,18 @@ Module KeyDecidableType(D:DecidableType). Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l. Proof. - firstorder. - exists x; auto. - induction H. - destruct y. - exists e; auto. - destruct IHInA as [e H0]. + intros k l; split; intros [y H]. + exists y; auto. + induction H as [a l eq|a l H IH]. + destruct a as [k' y']. + exists y'; auto. + destruct IH as [e H0]. exists e; auto. Qed. Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. Proof. - intros; unfold MapsTo in *; apply InA_eqA with (x,e); auto using eqke_equiv. + intros l x y e **; unfold MapsTo in *; apply InA_eqA with (x,e); auto using eqke_equiv. Qed. Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. @@ -127,21 +127,21 @@ Module KeyDecidableType(D:DecidableType). Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l. Proof. - inversion 1. - inversion_clear H0; eauto. + inversion 1 as [? H0]. + inversion_clear H0 as [? ? H1|]; eauto. destruct H1; simpl in *; intuition. Qed. Lemma In_inv_2 : forall k k' e e' l, InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l. Proof. - inversion_clear 1; compute in H0; intuition. + inversion_clear 1 as [? ? H0|? ? H0]; compute in H0; intuition. Qed. Lemma In_inv_3 : forall x x' l, InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l. Proof. - inversion_clear 1; compute in H0; intuition. + inversion_clear 1 as [? ? H0|? ? H0]; compute in H0; intuition. Qed. End Elt. diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index dc7a48cd6b..7bc9f97e2b 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -65,7 +65,7 @@ Module MOT_to_OT (Import O : MiniOrderedType) <: OrderedType. Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y}. Proof with auto with ordered_type. - intros; elim (compare x y); intro H; [ right | left | right ]... + intros x y; elim (compare x y); intro H; [ right | left | right ]... assert (~ eq y x)... Defined. @@ -83,7 +83,7 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma lt_antirefl : forall x, ~ lt x x. Proof. - intros; intro; absurd (eq x x); auto with ordered_type. + intros x; intro; absurd (eq x x); auto with ordered_type. Qed. Instance lt_strorder : StrictOrder lt. @@ -91,14 +91,14 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z. Proof with auto with ordered_type. - intros; destruct (compare x z) as [Hlt|Heq|Hlt]; auto. + intros x y z H ?; destruct (compare x z) as [Hlt|Heq|Hlt]; auto. elim (lt_not_eq H); apply eq_trans with z... elim (lt_not_eq (lt_trans Hlt H))... Qed. Lemma eq_lt : forall x y z, eq x y -> lt y z -> lt x z. Proof with auto with ordered_type. - intros; destruct (compare x z) as [Hlt|Heq|Hlt]; auto. + intros x y z H H0; destruct (compare x z) as [Hlt|Heq|Hlt]; auto. elim (lt_not_eq H0); apply eq_trans with x... elim (lt_not_eq (lt_trans H0 Hlt))... Qed. @@ -111,7 +111,7 @@ Module OrderedTypeFacts (Import O: OrderedType). Qed. Lemma lt_total : forall x y, lt x y \/ eq x y \/ lt y x. - Proof. intros; destruct (compare x y); auto. Qed. + Proof. intros x y; destruct (compare x y); auto. Qed. Module TO. Definition t := t. @@ -157,7 +157,7 @@ Module OrderedTypeFacts (Import O: OrderedType). forall x y : t, eq x y -> exists H : eq x y, compare x y = EQ H. Proof. - intros; case (compare x y); intros H'; try (exfalso; order). + intros x y H; case (compare x y); intros H'; try (exfalso; order). exists H'; auto. Qed. @@ -165,7 +165,7 @@ Module OrderedTypeFacts (Import O: OrderedType). forall x y : t, lt x y -> exists H : lt x y, compare x y = LT H. Proof. - intros; case (compare x y); intros H'; try (exfalso; order). + intros x y H; case (compare x y); intros H'; try (exfalso; order). exists H'; auto. Qed. @@ -173,7 +173,7 @@ Module OrderedTypeFacts (Import O: OrderedType). forall x y : t, lt y x -> exists H : lt y x, compare x y = GT H. Proof. - intros; case (compare x y); intros H'; try (exfalso; order). + intros x y H; case (compare x y); intros H'; try (exfalso; order). exists H'; auto. Qed. @@ -203,7 +203,7 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma lt_dec : forall x y : t, {lt x y} + {~ lt x y}. Proof. - intros; elim (compare x y); [ left | right | right ]; auto with ordered_type. + intros x y; elim (compare x y); [ left | right | right ]; auto with ordered_type. Defined. Definition eqb x y : bool := if eq_dec x y then true else false. @@ -211,7 +211,7 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma eqb_alt : forall x y, eqb x y = match compare x y with EQ _ => true | _ => false end. Proof. - unfold eqb; intros; destruct (eq_dec x y); elim_comp; auto. + unfold eqb; intros x y; destruct (eq_dec x y); elim_comp; auto. Qed. (* Specialization of results about lists modulo. *) @@ -327,7 +327,7 @@ Module KeyOrderedType(O:OrderedType). Lemma ltk_not_eqke : forall e e', ltk e e' -> ~eqke e e'. Proof. unfold eqke, ltk; intuition; simpl in *; subst. - exact (lt_not_eq H H1). + match goal with H : lt _ _, H1 : eq _ _ |- _ => exact (lt_not_eq H H1) end. Qed. #[local] @@ -398,18 +398,18 @@ Module KeyOrderedType(O:OrderedType). Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l. Proof with auto with ordered_type. - firstorder. - exists x... - induction H. - destruct y. - exists e... - destruct IHInA as [e H0]. + intros k l; split; intros [y H]. + exists y... + induction H as [a l eq|a l H IH]. + destruct a as [k' y']. + exists y'... + destruct IH as [e H0]. exists e... Qed. Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l. Proof. - intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto with *. + intros l x y e **; unfold MapsTo in *; apply InA_eqA with (x,e); eauto with *. Qed. Lemma In_eq : forall l x y, eq x y -> In x l -> In y l. @@ -437,7 +437,7 @@ Module KeyOrderedType(O:OrderedType). Lemma Sort_Inf_NotIn : forall l k e, Sort l -> Inf (k,e) l -> ~In k l. Proof. - intros; red; intros. + intros l k e H H0; red; intros H1. destruct H1 as [e' H2]. elim (@ltk_not_eqk (k,e) (k,e')). eapply Sort_Inf_In; eauto with ordered_type. @@ -457,34 +457,34 @@ Module KeyOrderedType(O:OrderedType). Lemma Sort_In_cons_2 : forall l e e', Sort (e::l) -> InA eqk e' (e::l) -> ltk e e' \/ eqk e e'. Proof. - inversion_clear 2; auto with ordered_type. + intros l; inversion_clear 2; auto with ordered_type. left; apply Sort_In_cons_1 with l; auto. Qed. Lemma Sort_In_cons_3 : forall x l k e, Sort ((k,e)::l) -> In x l -> ~eq x k. Proof. - inversion_clear 1; red; intros. + inversion_clear 1 as [|? ? H0 H1]; red; intros H H2. destruct (Sort_Inf_NotIn H0 H1 (In_eq H2 H)). Qed. Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l. Proof. - inversion 1. - inversion_clear H0; eauto with ordered_type. + inversion 1 as [? H0]. + inversion_clear H0 as [? ? H1|]; eauto with ordered_type. destruct H1; simpl in *; intuition. Qed. Lemma In_inv_2 : forall k k' e e' l, InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l. Proof. - inversion_clear 1; compute in H0; intuition. + inversion_clear 1 as [? ? H0|? ? H0]; compute in H0; intuition. Qed. Lemma In_inv_3 : forall x x' l, InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l. Proof. - inversion_clear 1; compute in H0; intuition. + inversion_clear 1 as [? ? H0|? ? H0]; compute in H0; intuition. Qed. End Elt. diff --git a/user-contrib/Ltac2/Ind.v b/user-contrib/Ltac2/Ind.v new file mode 100644 index 0000000000..f397a0e2c8 --- /dev/null +++ b/user-contrib/Ltac2/Ind.v @@ -0,0 +1,45 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +From Ltac2 Require Import Init. + +Ltac2 Type t := inductive. + +Ltac2 @ external equal : t -> t -> bool := "ltac2" "ind_equal". +(** Equality test. *) + +Ltac2 Type data. +(** Type of data representing inductive blocks. *) + +Ltac2 @ external data : t -> data := "ltac2" "ind_data". +(** Get the mutual blocks corresponding to an inductive type in the current + environment. Panics if there is no such inductive. *) + +Ltac2 @ external repr : data -> t := "ltac2" "ind_repr". +(** Returns the inductive corresponding to the block. Inverse of [data]. *) + +Ltac2 @ external index : t -> int := "ltac2" "ind_index". +(** Returns the index of the inductive type inside its mutual block. Guaranteed + to range between [0] and [nblocks data - 1] where [data] was retrieved + using the above function. *) + +Ltac2 @ external nblocks : data -> int := "ltac2" "ind_nblocks". +(** Returns the number of inductive types appearing in a mutual block. *) + +Ltac2 @ external nconstructors : data -> int := "ltac2" "ind_nconstructors". +(** Returns the number of constructors appearing in the current block. *) + +Ltac2 @ external get_block : data -> int -> data := "ltac2" "ind_get_block". +(** Returns the block corresponding to the nth inductive type. Index must range + between [0] and [nblocks data - 1], otherwise the function panics. *) + +Ltac2 @ external get_constructor : data -> int -> constructor := "ltac2" "ind_get_constructor". +(** Returns the nth constructor of the inductive type. Index must range between + [0] and [nconstructors data - 1], otherwise the function panics. *) diff --git a/user-contrib/Ltac2/Ltac2.v b/user-contrib/Ltac2/Ltac2.v index ccfc7e4a70..e55c6c13d3 100644 --- a/user-contrib/Ltac2/Ltac2.v +++ b/user-contrib/Ltac2/Ltac2.v @@ -22,6 +22,7 @@ Require Ltac2.Fresh. Require Ltac2.Pattern. Require Ltac2.Std. Require Ltac2.Env. +Require Ltac2.Ind. Require Ltac2.Printf. Require Ltac2.Ltac1. Require Export Ltac2.Notations. diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index 948a359124..bcf9ece7c8 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -1075,6 +1075,54 @@ let () = define1 "env_instantiate" reference begin fun r -> return (Value.of_constr c) end +(** Ind *) + +let () = define2 "ind_equal" (repr_ext val_inductive) (repr_ext val_inductive) begin fun ind1 ind2 -> + return (Value.of_bool (Ind.UserOrd.equal ind1 ind2)) +end + +let () = define1 "ind_data" (repr_ext val_inductive) begin fun ind -> + Proofview.tclENV >>= fun env -> + if Environ.mem_mind (fst ind) env then + let mib = Environ.lookup_mind (fst ind) env in + return (Value.of_ext val_ind_data (ind, mib)) + else + throw err_notfound +end + +let () = define1 "ind_repr" (repr_ext val_ind_data) begin fun (ind, _) -> + return (Value.of_ext val_inductive ind) +end + +let () = define1 "ind_index" (repr_ext val_inductive) begin fun (ind, n) -> + return (Value.of_int n) +end + +let () = define1 "ind_nblocks" (repr_ext val_ind_data) begin fun (ind, mib) -> + return (Value.of_int (Array.length mib.Declarations.mind_packets)) +end + +let () = define1 "ind_nconstructors" (repr_ext val_ind_data) begin fun ((_, n), mib) -> + let open Declarations in + return (Value.of_int (Array.length mib.mind_packets.(n).mind_consnames)) +end + +let () = define2 "ind_get_block" (repr_ext val_ind_data) int begin fun (ind, mib) n -> + if 0 <= n && n < Array.length mib.Declarations.mind_packets then + return (Value.of_ext val_ind_data ((fst ind, n), mib)) + else throw err_notfound +end + +let () = define2 "ind_get_constructor" (repr_ext val_ind_data) int begin fun ((mind, n), mib) i -> + let open Declarations in + let ncons = Array.length mib.mind_packets.(n).mind_consnames in + if 0 <= i && i < ncons then + (* WARNING: In the ML API constructors are indexed from 1 for historical + reasons, but Ltac2 uses 0-indexing instead. *) + return (Value.of_ext val_constructor ((mind, n), i + 1)) + else throw err_notfound +end + (** Ltac1 in Ltac2 *) let ltac1 = Tac2ffi.repr_ext Value.val_ltac1 @@ -1388,24 +1436,35 @@ let () = (** Ltac2 in terms *) let () = - let interp ist poly env sigma concl (ids, tac) = + let interp ?loc ~poly env sigma tycon (ids, tac) = (* Syntax prevents bound notation variables in constr quotations *) let () = assert (Id.Set.is_empty ids) in - let ist = Tac2interp.get_env ist in + let ist = Tac2interp.get_env @@ GlobEnv.lfun env in let tac = Proofview.tclIGNORE (Tac2interp.interp ist tac) in let name, poly = Id.of_string "ltac2", poly in - let c, sigma = Proof.refine_by_tactic ~name ~poly env sigma concl tac in - (EConstr.of_constr c, sigma) + let sigma, concl = match tycon with + | Some ty -> sigma, ty + | None -> GlobEnv.new_type_evar env sigma ~src:(loc,Evar_kinds.InternalHole) + in + let c, sigma = Proof.refine_by_tactic ~name ~poly (GlobEnv.renamed_env env) sigma concl tac in + let j = { Environ.uj_val = EConstr.of_constr c; Environ.uj_type = concl } in + (j, sigma) in GlobEnv.register_constr_interp0 wit_ltac2_constr interp let () = - let interp ist poly env sigma concl id = - let ist = Tac2interp.get_env ist in + let interp ?loc ~poly env sigma tycon id = + let ist = Tac2interp.get_env @@ GlobEnv.lfun env in let c = Id.Map.find id ist.env_ist in let c = Value.to_constr c in - let sigma = Typing.check env sigma c concl in - (c, sigma) + let t = Retyping.get_type_of (GlobEnv.renamed_env env) sigma c in + match tycon with + | None -> + { Environ.uj_val = c; Environ.uj_type = t }, sigma + | Some ty -> + let sigma = Evarconv.unify_leq_delay (GlobEnv.renamed_env env) sigma t ty in + let j = { Environ.uj_val = c; Environ.uj_type = ty } in + j, sigma in GlobEnv.register_constr_interp0 wit_ltac2_quotation interp diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index d0655890a7..faa1e74728 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -816,7 +816,18 @@ let perform_eval ~pstate e = | Goal_select.SelectList l -> Proofview.tclFOCUSLIST l v | Goal_select.SelectId id -> Proofview.tclFOCUSID id v | Goal_select.SelectAll -> v - | Goal_select.SelectAlreadyFocused -> assert false (* TODO **) + | Goal_select.SelectAlreadyFocused -> + let open Proofview.Notations in + Proofview.numgoals >>= fun n -> + if Int.equal n 1 then v + else + let e = CErrors.UserError + (None, + Pp.(str "Expected a single focused goal but " ++ + int n ++ str " goals are focused.")) + in + let info = Exninfo.reify () in + Proofview.tclZERO ~info e in let (proof, _, ans) = Proof.run_tactic (Global.env ()) v proof in let { Proof.sigma } = Proof.data proof in diff --git a/user-contrib/Ltac2/tac2ffi.ml b/user-contrib/Ltac2/tac2ffi.ml index a09438c6bf..5f9fbc4e41 100644 --- a/user-contrib/Ltac2/tac2ffi.ml +++ b/user-contrib/Ltac2/tac2ffi.ml @@ -104,6 +104,7 @@ let val_binder = Val.create "binder" let val_univ = Val.create "universe" let val_free : Names.Id.Set.t Val.tag = Val.create "free" let val_ltac1 : Geninterp.Val.t Val.tag = Val.create "ltac1" +let val_ind_data : (Names.Ind.t * Declarations.mutual_inductive_body) Val.tag = Val.create "ind_data" let extract_val (type a) (type b) (tag : a Val.tag) (tag' : b Val.tag) (v : b) : a = match Val.eq tag tag' with diff --git a/user-contrib/Ltac2/tac2ffi.mli b/user-contrib/Ltac2/tac2ffi.mli index c9aa50389e..e87ad7139c 100644 --- a/user-contrib/Ltac2/tac2ffi.mli +++ b/user-contrib/Ltac2/tac2ffi.mli @@ -184,6 +184,7 @@ val val_binder : (Name.t Context.binder_annot * types) Val.tag val val_univ : Univ.Level.t Val.tag val val_free : Id.Set.t Val.tag val val_ltac1 : Geninterp.Val.t Val.tag +val val_ind_data : (Names.Ind.t * Declarations.mutual_inductive_body) Val.tag val val_exn : Exninfo.iexn Tac2dyn.Val.tag (** Toplevel representation of OCaml exceptions. Invariant: no [LtacError] |