diff options
| -rw-r--r-- | doc/changelog/01-kernel/12537-master+module-starting-extends-delta-resolver.rst | 8 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 4 | ||||
| -rw-r--r-- | pretyping/nativenorm.ml | 11 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 14 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 26 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 282 | ||||
| -rw-r--r-- | pretyping/vnorm.ml | 11 | ||||
| -rw-r--r-- | test-suite/output/Search.out | 3 | ||||
| -rw-r--r-- | test-suite/output/Search.v | 23 | ||||
| -rw-r--r-- | test-suite/success/bug_10890.v | 8 | ||||
| -rw-r--r-- | test-suite/success/sprop_uip.v | 26 | ||||
| -rw-r--r-- | theories/Reals/Rpower.v | 109 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 2 |
13 files changed, 329 insertions, 198 deletions
diff --git a/doc/changelog/01-kernel/12537-master+module-starting-extends-delta-resolver.rst b/doc/changelog/01-kernel/12537-master+module-starting-extends-delta-resolver.rst new file mode 100644 index 0000000000..bec121836c --- /dev/null +++ b/doc/changelog/01-kernel/12537-master+module-starting-extends-delta-resolver.rst @@ -0,0 +1,8 @@ +- **Fixed:** + A loss of definitional equality for declarations obtained through + :cmd:`Include` when entering the scope of a :cmd:`Module` or + :cmd:`Module Type` was causing :cmd:`Search` not to see the included + declarations + (`#12537 <https://github.com/coq/coq/pull/12537>`_, fixes `#12525 + <https://github.com/coq/coq/pull/12525>`_ and `#12647 + <https://github.com/coq/coq/pull/12647>`_, by Hugo Herbelin). diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 93337fca5d..8b85072d6d 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1023,6 +1023,8 @@ let start_module l senv = mp, { empty_environment with env = senv.env; + modresolver = senv.modresolver; + paramresolver = senv.paramresolver; modpath = mp; modvariant = STRUCT ([],senv); required = senv.required } @@ -1034,6 +1036,8 @@ let start_modtype l senv = mp, { empty_environment with env = senv.env; + modresolver = senv.modresolver; + paramresolver = senv.paramresolver; modpath = mp; modvariant = SIG ([], senv); required = senv.required } diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 30e1dc0611..3f68e3c78f 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -318,13 +318,12 @@ and nf_atom_type env sigma atom = | Avar id -> mkVar id, Typeops.type_of_variable env id | Acase(ans,accu,p,bs) -> - let () = if Typeops.should_invert_case env ans.asw_ci then - (* TODO implement case inversion readback (properly reducing - it is a problem for the kernel) *) - CErrors.user_err Pp.(str "Native compute readback of case inversion not implemented.") - in let a,ta = nf_accu_type env sigma accu in let ((mind,_),u as ind),allargs = find_rectype_a env ta in + let iv = if Typeops.should_invert_case env ans.asw_ci then + CaseInvert {univs=u; args=allargs} + else NoInvert + in let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in let nparams = mib.mind_nparams in let params,realargs = Array.chop nparams allargs in @@ -344,7 +343,7 @@ and nf_atom_type env sigma atom = in let branchs = Array.mapi mkbranch bsw in let tcase = build_case_type p realargs a in - mkCase(ans.asw_ci, p, NoInvert, a, branchs), tcase + mkCase(ans.asw_ci, p, iv, a, branchs), tcase | Afix(tt,ft,rp,s) -> let tt = Array.map (fun t -> nf_type_sort env sigma t) tt in let tt = Array.map fst tt and rt = Array.map snd tt in diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 6f02d76f3a..594b8ab54c 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -436,15 +436,11 @@ type state = constr * constr Stack.t type reduction_function = env -> evar_map -> constr -> constr type e_reduction_function = env -> evar_map -> constr -> evar_map * constr -type contextual_stack_reduction_function = +type stack_reduction_function = env -> evar_map -> constr -> constr * constr list -type stack_reduction_function = contextual_stack_reduction_function -type local_stack_reduction_function = - evar_map -> constr -> constr * constr list type state_reduction_function = env -> evar_map -> state -> state -type local_state_reduction_function = evar_map -> state -> state let pr_state env sigma (tm,sk) = let open Pp in @@ -572,14 +568,6 @@ let reduce_and_refold_fix recfun env sigma fix sk = (fun _ (t,sk') -> recfun (t,sk')) [] sigma raw_answer sk -let fix_recarg ((recindices,bodynum),_) stack = - assert (0 <= bodynum && bodynum < Array.length recindices); - let recargnum = Array.get recindices bodynum in - try - Some (recargnum, Stack.nth stack recargnum) - with Not_found -> - None - open Primred module CNativeEntries = diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index b316b3c213..218936edfb 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -112,15 +112,11 @@ type reduction_function = env -> evar_map -> constr -> constr type e_reduction_function = env -> evar_map -> constr -> evar_map * constr -type contextual_stack_reduction_function = +type stack_reduction_function = env -> evar_map -> constr -> constr * constr list -type stack_reduction_function = contextual_stack_reduction_function -type local_stack_reduction_function = - evar_map -> constr -> constr * constr list type state_reduction_function = env -> evar_map -> state -> state -type local_state_reduction_function = evar_map -> state -> state val pr_state : env -> evar_map -> state -> Pp.t @@ -130,11 +126,6 @@ val strong_with_flags : (CClosure.RedFlags.reds -> reduction_function) -> (CClosure.RedFlags.reds -> reduction_function) val strong : reduction_function -> reduction_function -(*i -val stack_reduction_of_reduction : - 'a reduction_function -> 'a state_reduction_function -i*) -val stacklam : (state -> 'a) -> constr list -> evar_map -> constr -> constr Stack.t -> 'a val whd_state_gen : CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state @@ -167,13 +158,13 @@ val whd_allnolet : reduction_function val whd_betalet : reduction_function (** Removes cast and put into applicative form *) -val whd_nored_stack : contextual_stack_reduction_function -val whd_beta_stack : contextual_stack_reduction_function -val whd_betaiota_stack : contextual_stack_reduction_function -val whd_betaiotazeta_stack : contextual_stack_reduction_function -val whd_all_stack : contextual_stack_reduction_function -val whd_allnolet_stack : contextual_stack_reduction_function -val whd_betalet_stack : contextual_stack_reduction_function +val whd_nored_stack : stack_reduction_function +val whd_beta_stack : stack_reduction_function +val whd_betaiota_stack : stack_reduction_function +val whd_betaiotazeta_stack : stack_reduction_function +val whd_all_stack : stack_reduction_function +val whd_allnolet_stack : stack_reduction_function +val whd_betalet_stack : stack_reduction_function val whd_nored_state : state_reduction_function val whd_beta_state : state_reduction_function @@ -242,7 +233,6 @@ val is_arity : env -> evar_map -> constr -> bool val is_sort : env -> evar_map -> types -> bool val contract_fix : evar_map -> fixpoint -> constr -val fix_recarg : ('a, 'a) pfixpoint -> 'b Stack.t -> (int * 'b) option (** {6 Querying the kernel conversion oracle: opaque/transparent constants } *) val is_transparent : Environ.env -> Constant.t tableKey -> bool diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index baa32565f6..e4b5dc1edf 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -358,30 +358,6 @@ let reference_eval env sigma = function let x = Name default_dependent_ident -let make_elim_fun (names,(nbfix,lv,n)) u largs = - let lu = List.firstn n largs in - let p = List.length lv in - let lyi = List.map fst lv in - let la = - List.map_i (fun q aq -> - (* k from the comment is q+1 *) - try mkRel (p+1-(List.index Int.equal (n-q) lyi)) - with Not_found -> aq) - 0 (List.map (Vars.lift p) lu) - in - fun i -> - match names.(i) with - | None -> None - | Some (minargs,ref) -> - let body = applist (mkEvalRef ref u, la) in - let g = - List.fold_left_i (fun q (* j = n+1-q *) c (ij,tij) -> - let subst = List.map (Vars.lift (-q)) (List.firstn (n-ij) la) in - let tij' = Vars.substl (List.rev subst) tij in - let x = make_annot x Sorts.Relevant in (* TODO relevance *) - mkLambda (x,tij',c)) 1 body (List.rev lv) - in Some (minargs,g) - (* [f] is convertible to [Fix(recindices,bodynum),bodyvect)]: do so that the reduction uses this extra information *) @@ -467,16 +443,6 @@ let substl_checking_arity env subst sigma c = type fix_reduction_result = NotReducible | Reduced of (constr * constr list) -let reduce_fix whdfun sigma fix stack = - match fix_recarg fix (Stack.append_app_list stack Stack.empty) with - | None -> NotReducible - | Some (recargnum,recarg) -> - let (recarg'hd,_ as recarg') = whdfun sigma recarg in - let stack' = List.assign stack recargnum (applist recarg') in - (match EConstr.kind sigma recarg'hd with - | Construct _ -> Reduced (contract_fix sigma fix, stack') - | _ -> NotReducible) - let contract_fix_use_function env sigma f ((recindices,bodynum),(_names,_types,bodies as typedbodies)) = let nbodies = Array.length recindices in @@ -484,22 +450,6 @@ let contract_fix_use_function env sigma f let lbodies = List.init nbodies make_Fi in substl_checking_arity env (List.rev lbodies) sigma (nf_beta env sigma bodies.(bodynum)) -let reduce_fix_use_function env sigma f whfun fix stack = - match fix_recarg fix (Stack.append_app_list stack Stack.empty) with - | None -> NotReducible - | Some (recargnum,recarg) -> - let (recarg'hd,_ as recarg') = - if EConstr.isRel sigma recarg then - (* The recarg cannot be a local def, no worry about the right env *) - (recarg, []) - else - whfun recarg in - let stack' = List.assign stack recargnum (applist recarg') in - (match EConstr.kind sigma recarg'hd with - | Construct _ -> - Reduced (contract_fix_use_function env sigma f fix,stack') - | _ -> NotReducible) - let contract_cofix_use_function env sigma f (bodynum,(_names,_,bodies as typedbodies)) = let nbodies = Array.length bodies in @@ -574,34 +524,23 @@ let match_eval_ref_value env sigma constr stack = env |> lookup_rel n |> RelDecl.get_value |> Option.map (lift n) | _ -> None -let special_red_case env sigma whfun (ci, p, iv, c, lf) = - let rec redrec s = - let (constr, cargs) = whfun s in - match match_eval_ref env sigma constr cargs with - | Some (ref, u) -> - (match reference_opt_value env sigma ref u with - | None -> raise Redelimination - | Some gvalue -> - if reducible_mind_case sigma gvalue then - reduce_mind_case_use_function constr env sigma - {mP=p; mconstr=gvalue; mcargs=cargs; - mci=ci; mlf=lf} - else - redrec (applist(gvalue, cargs))) - | None -> - if reducible_mind_case sigma constr then - reduce_mind_case sigma - {mP=p; mconstr=constr; mcargs=cargs; - mci=ci; mlf=lf} - else - raise Redelimination - in - redrec c +let push_app sigma (hd, stk as p) = match EConstr.kind sigma hd with +| App (hd, args) -> + (hd, Array.fold_right (fun x accu -> x :: accu) args stk) +| _ -> p let recargs = function | EvalVar _ | EvalRel _ | EvalEvar _ -> None | EvalConst c -> ReductionBehaviour.get (GlobRef.ConstRef c) +let fix_recarg ((recindices,bodynum),_) stack = + assert (0 <= bodynum && bodynum < Array.length recindices); + let recargnum = Array.get recindices bodynum in + try + Some (recargnum, List.nth stack recargnum) + with Failure _ -> + None + let reduce_projection env sigma p ~npars (recarg'hd,stack') stack = (match EConstr.kind sigma recarg'hd with | Construct _ -> @@ -609,24 +548,9 @@ let reduce_projection env sigma p ~npars (recarg'hd,stack') stack = Reduced (List.nth stack' proj_narg, stack) | _ -> NotReducible) -let reduce_proj env sigma whfun whfun' c = - let rec redrec s = - match EConstr.kind sigma s with - | Proj (proj, c) -> - let c' = try redrec c with Redelimination -> c in - let constr, cargs = whfun c' in - (match EConstr.kind sigma constr with - | Construct _ -> - let proj_narg = Projection.npars proj + Projection.arg proj in - List.nth cargs proj_narg - | _ -> raise Redelimination) - | Case (n,p,iv,c,brs) -> - let c' = redrec c in - let p = (n,p,iv,c',brs) in - (try special_red_case env sigma whfun' p - with Redelimination -> mkCase p) - | _ -> raise Redelimination - in redrec c +let rec beta_applist sigma accu c stk = match EConstr.kind sigma c, stk with +| Lambda (_, _, c), arg :: stk -> beta_applist sigma (arg :: accu) c stk +| _ -> substl accu c, stk let whd_nothing_for_iota env sigma s = let rec whrec (x, stack as s) = @@ -650,17 +574,17 @@ let whd_nothing_for_iota env sigma s = (match constant_opt_value_in env (const, u) with | Some body -> whrec (EConstr.of_constr body, stack) | None -> s) - | LetIn (_,b,_,c) -> stacklam whrec [b] sigma c stack + | LetIn (_,b,_,c) -> whrec (beta_applist sigma [b] c stack) | Cast (c,_,_) -> whrec (c, stack) - | App (f,cl) -> whrec (f, Stack.append_app cl stack) + | App (f,cl) -> whrec (f, Array.fold_right (fun c accu -> c :: accu) cl stack) | Lambda (na,t,c) -> - (match Stack.decomp stack with - | Some (a,m) -> stacklam whrec [a] sigma c m + (match stack with + | a :: stack -> whrec (beta_applist sigma [a] c stack) | _ -> s) | x -> s in - EConstr.decompose_app sigma (Stack.zip sigma (whrec (s,Stack.empty))) + whrec s (* [red_elim_const] contracts iota/fix/cofix redexes hidden behind constants by keeping the name of the constants in the recursive calls; @@ -703,21 +627,17 @@ let rec red_elim_const env sigma ref u largs = try match reference_eval env sigma ref with | EliminationCases n when nargs >= n -> let c = reference_value env sigma ref u in - let c', lrest = whd_nothing_for_iota env sigma (applist(c,largs)) in - let whfun = whd_simpl_stack env sigma in - (special_red_case env sigma whfun (EConstr.destCase sigma c'), lrest), nocase + let c', lrest = whd_nothing_for_iota env sigma (c, largs) in + (special_red_case env sigma (EConstr.destCase sigma c'), lrest), nocase | EliminationProj n when nargs >= n -> let c = reference_value env sigma ref u in - let c', lrest = whd_nothing_for_iota env sigma (applist(c,largs)) in - let whfun = whd_construct_stack env sigma in - let whfun' = whd_simpl_stack env sigma in - (reduce_proj env sigma whfun whfun' c', lrest), nocase + let c', lrest = whd_nothing_for_iota env sigma (c, largs) in + (reduce_proj env sigma c', lrest), nocase | EliminationFix (min,minfxargs,infos) when nargs >= min -> let c = reference_value env sigma ref u in - let d, lrest = whd_nothing_for_iota env sigma (applist(c,largs)) in - let f = make_elim_fun ([|Some (minfxargs,ref)|],infos) u largs in - let whfun = whd_construct_stack env sigma in - (match reduce_fix_use_function env sigma f whfun (destFix sigma d) lrest with + let d, lrest = whd_nothing_for_iota env sigma (c, largs) in + let f = ([|Some (minfxargs,ref)|],infos), u, largs in + (match reduce_fix_use_function env sigma f (destFix sigma d) lrest with | NotReducible -> raise Redelimination | Reduced (c,rest) -> (nf_beta env sigma c, rest), nocase) | EliminationMutualFix (min,refgoal,refinfos) when nargs >= min -> @@ -729,10 +649,9 @@ let rec red_elim_const env sigma ref u largs = let c', lrest = whd_betalet_stack env sigma (applist(c,args)) in descend (destEvalRefU sigma c') lrest in let (_, midargs as s) = descend (ref,u) largs in - let d, lrest = whd_nothing_for_iota env sigma (applist s) in - let f = make_elim_fun refinfos u midargs in - let whfun = whd_construct_stack env sigma in - (match reduce_fix_use_function env sigma f whfun (destFix sigma d) lrest with + let d, lrest = whd_nothing_for_iota env sigma s in + let f = refinfos, u, midargs in + (match reduce_fix_use_function env sigma f (destFix sigma d) lrest with | NotReducible -> raise Redelimination | Reduced (c,rest) -> (nf_beta env sigma c, rest), nocase) | NotAnElimination when unfold_nonelim -> @@ -755,32 +674,30 @@ and reduce_params env sigma stack l = | _ -> raise Redelimination) stack l - (* reduce to whd normal form or to an applied constant that does not hide a reducible iota/fix/cofix redex (the "simpl" tactic) *) and whd_simpl_stack env sigma = let open ReductionBehaviour in let rec redrec s = - let (x, stack) = decompose_app_vect sigma s in - let stack = Array.to_list stack in - let s' = (x, stack) in + let s' = push_app sigma s in + let (x, stack) = s' in match EConstr.kind sigma x with | Lambda (na,t,c) -> (match stack with | [] -> s' - | a :: rest -> redrec (beta_applist sigma (x, stack))) - | LetIn (n,b,t,c) -> redrec (applist (Vars.substl [b] c, stack)) - | App (f,cl) -> redrec (applist(f, (Array.to_list cl)@stack)) - | Cast (c,_,_) -> redrec (applist(c, stack)) + | a :: rest -> redrec (beta_applist sigma [a] c rest)) + | LetIn (n,b,t,c) -> redrec (Vars.substl [b] c, stack) + | App (f,cl) -> assert false (* see push_app above *) + | Cast (c,_,_) -> redrec (c, stack) | Case (ci,p,iv,c,lf) -> (try - redrec (applist(special_red_case env sigma redrec (ci,p,iv,c,lf), stack)) + redrec (special_red_case env sigma (ci,p,iv,c,lf), stack) with Redelimination -> s') | Fix fix -> - (try match reduce_fix (whd_construct_stack env) sigma fix stack with - | Reduced s' -> redrec (applist s') + (try match reduce_fix env sigma fix stack with + | Reduced s' -> redrec s' | NotReducible -> s' with Redelimination -> s') @@ -800,11 +717,11 @@ and whd_simpl_stack env sigma = (match reduce_projection env sigma p ~npars (whd_construct_stack env sigma c) stack with - | Reduced s' -> redrec (applist s') + | Reduced s' -> redrec s' | NotReducible -> s') | _ -> match reduce_projection env sigma p ~npars (whd_construct_stack env sigma c) stack with - | Reduced s' -> redrec (applist s') + | Reduced s' -> redrec s' | NotReducible -> s') else s' with Redelimination -> s') @@ -814,7 +731,7 @@ and whd_simpl_stack env sigma = | Some (ref, u) -> (try let sapp, nocase = red_elim_const env sigma ref u stack in - let hd, _ as s'' = redrec (applist(sapp)) in + let hd, _ as s'' = redrec sapp in let rec is_case x = match EConstr.kind sigma x with | Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x | App (hd, _) -> is_case hd @@ -827,10 +744,102 @@ and whd_simpl_stack env sigma = in redrec +and reduce_fix env sigma fix stack = + match fix_recarg fix stack with + | None -> NotReducible + | Some (recargnum,recarg) -> + let (recarg'hd,_ as recarg') = whd_construct_stack env sigma recarg in + let stack' = List.assign stack recargnum (applist recarg') in + (match EConstr.kind sigma recarg'hd with + | Construct _ -> Reduced (contract_fix sigma fix, stack') + | _ -> NotReducible) + +and reduce_fix_use_function env sigma f fix stack = + match fix_recarg fix stack with + | None -> NotReducible + | Some (recargnum,recarg) -> + let (recarg'hd,_ as recarg') = + if EConstr.isRel sigma recarg then + (* The recarg cannot be a local def, no worry about the right env *) + (recarg, []) + else + whd_construct_stack env sigma recarg in + let stack' = List.assign stack recargnum (applist recarg') in + (match EConstr.kind sigma recarg'hd with + | Construct _ -> + let (names, (nbfix, lv, n)), u, largs = f in + let lu = List.firstn n largs in + let p = List.length lv in + let lyi = List.map fst lv in + let la = + List.map_i (fun q aq -> + (* k from the comment is q+1 *) + try mkRel (p+1-(List.index Int.equal (n-q) lyi)) + with Not_found -> Vars.lift p aq) + 0 lu + in + let f i = match names.(i) with + | None -> None + | Some (minargs,ref) -> + let body = applist (mkEvalRef ref u, la) in + let g = + List.fold_left_i (fun q (* j = n+1-q *) c (ij,tij) -> + let subst = List.map (Vars.lift (-q)) (List.firstn (n-ij) la) in + let tij' = Vars.substl (List.rev subst) tij in + let x = make_annot x Sorts.Relevant in (* TODO relevance *) + mkLambda (x,tij',c)) 1 body (List.rev lv) + in Some (minargs,g) + in + Reduced (contract_fix_use_function env sigma f fix,stack') + | _ -> NotReducible) + +and reduce_proj env sigma c = + let rec redrec s = + match EConstr.kind sigma s with + | Proj (proj, c) -> + let c' = try redrec c with Redelimination -> c in + let constr, cargs = whd_construct_stack env sigma c' in + (match EConstr.kind sigma constr with + | Construct _ -> + let proj_narg = Projection.npars proj + Projection.arg proj in + List.nth cargs proj_narg + | _ -> raise Redelimination) + | Case (n,p,iv,c,brs) -> + let c' = redrec c in + let p = (n,p,iv,c',brs) in + (try special_red_case env sigma p + with Redelimination -> mkCase p) + | _ -> raise Redelimination + in redrec c + +and special_red_case env sigma (ci, p, iv, c, lf) = + let rec redrec s = + let (constr, cargs) = whd_simpl_stack env sigma s in + match match_eval_ref env sigma constr cargs with + | Some (ref, u) -> + (match reference_opt_value env sigma ref u with + | None -> raise Redelimination + | Some gvalue -> + if reducible_mind_case sigma gvalue then + reduce_mind_case_use_function constr env sigma + {mP=p; mconstr=gvalue; mcargs=cargs; + mci=ci; mlf=lf} + else + redrec (gvalue, cargs)) + | None -> + if reducible_mind_case sigma constr then + reduce_mind_case sigma + {mP=p; mconstr=constr; mcargs=cargs; + mci=ci; mlf=lf} + else + raise Redelimination + in + redrec (push_app sigma (c, [])) + (* reduce until finding an applied constructor or fail *) and whd_construct_stack env sigma s = - let (constr, cargs as s') = whd_simpl_stack env sigma s in + let (constr, cargs as s') = whd_simpl_stack env sigma (s, []) in if reducible_mind_case sigma constr then s' else match match_eval_ref env sigma constr cargs with | Some (ref, u) -> @@ -855,13 +864,13 @@ let try_red_product env sigma c = | App (f,l) -> (match EConstr.kind sigma f with | Fix fix -> - let stack = Stack.append_app l Stack.empty in - (match fix_recarg fix stack with + (match fix_recarg fix (Array.to_list l) with | None -> raise Redelimination | Some (recargnum,recarg) -> let recarg' = redrec env recarg in - let stack' = Stack.assign stack recargnum recarg' in - simpfun (Stack.zip sigma (f,stack'))) + let l = Array.copy l in + let () = Array.set l recargnum recarg' in + simpfun (mkApp (f, l))) | _ -> simpfun (mkApp (redrec env f, l))) | Cast (c,_,_) -> redrec env c | Prod (x,a,b) -> @@ -973,19 +982,19 @@ let whd_simpl_orelse_delta_but_fix env sigma c = if List.length stack <= npars then (* Do not show the eta-expanded form *) s' - else redrec (applist (c, stack)) - | _ -> redrec (applist(c, stack))) + else redrec (c, stack) + | _ -> redrec (c, stack)) | None -> s' in let simpfun = clos_norm_flags betaiota env sigma in simpfun (applist (redrec c)) -let hnf_constr = whd_simpl_orelse_delta_but_fix +let hnf_constr env sigma c = whd_simpl_orelse_delta_but_fix env sigma (c, []) (* The "simpl" reduction tactic *) let whd_simpl env sigma c = - applist (whd_simpl_stack env sigma c) + applist (whd_simpl_stack env sigma (c, [])) let simpl env sigma c = strong whd_simpl env sigma c @@ -1267,11 +1276,10 @@ let one_step_reduce env sigma c = | Cast (c,_,_) -> redrec (c,stack) | Case (ci,p,iv,c,lf) -> (try - (special_red_case env sigma (whd_simpl_stack env sigma) - (ci,p,iv,c,lf), stack) + (special_red_case env sigma (ci,p,iv,c,lf), stack) with Redelimination -> raise NotStepReducible) | Fix fix -> - (try match reduce_fix (whd_construct_stack env) sigma fix stack with + (try match reduce_fix env sigma fix stack with | Reduced s' -> s' | NotReducible -> raise NotStepReducible with Redelimination -> raise NotStepReducible) diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index b3f577b684..854a5ff63d 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -263,12 +263,11 @@ and nf_stk ?from:(from=0) env sigma c t stk = | Zswitch sw :: stk -> assert (from = 0) ; let ci = sw.sw_annot.Vmvalues.ci in - let () = if Typeops.should_invert_case env ci then - (* TODO implement case inversion readback (properly reducing - it is a problem for the kernel) *) - CErrors.user_err Pp.(str "VM compute readback of case inversion not implemented.") - in let ((mind,_ as ind), u), allargs = find_rectype_a env t in + let iv = if Typeops.should_invert_case env ci then + CaseInvert {univs=u; args=allargs} + else NoInvert + in let (mib,mip) = Inductive.lookup_mind_specif env ind in let nparams = mib.mind_nparams in let params,realargs = Util.Array.chop nparams allargs in @@ -287,7 +286,7 @@ and nf_stk ?from:(from=0) env sigma c t stk = in let branchs = Array.mapi mkbranch bsw in let tcase = build_case_type p realargs c in - nf_stk env sigma (mkCase(ci, p, NoInvert, c, branchs)) tcase stk + nf_stk env sigma (mkCase(ci, p, iv, c, branchs)) tcase stk | Zproj p :: stk -> assert (from = 0) ; let p' = Projection.make p true in diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index 317e9c3757..09feca71e7 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -455,3 +455,6 @@ PreOrder_Reflexive: reflexive_eq_dom_reflexive: forall {A B : Type} {R' : Relation_Definitions.relation B}, Reflexive R' -> Reflexive (eq ==> R')%signature +B.b: B.a +A.b: A.a +F.L: F.P 0 diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v index 4ec7a760b9..a5ac2cb511 100644 --- a/test-suite/output/Search.v +++ b/test-suite/output/Search.v @@ -66,3 +66,26 @@ Reset Initial. Require Import Morphisms. Search is:Instance [ Reflexive | Symmetric ]. + +Module Bug12525. + (* This was revealing a kernel bug with delta-resolution *) + Module A. Axiom a:Prop. Axiom b:a. End A. + Module B. Include A. End B. + Module M. + Search B.a. + End M. +End Bug12525. + +From Coq Require Lia. + +Module Bug12647. + (* Similar to #12525 *) + Module Type Foo. + Axiom P : nat -> Prop. + Axiom L : P 0. + End Foo. + + Module Bar (F : Foo). + Search F.P. + End Bar. +End Bug12647. diff --git a/test-suite/success/bug_10890.v b/test-suite/success/bug_10890.v new file mode 100644 index 0000000000..37b6c816cc --- /dev/null +++ b/test-suite/success/bug_10890.v @@ -0,0 +1,8 @@ +Require Import Derive. + +Derive foo SuchThat (foo = foo :> nat) As bar. +Proof. + Unshelve. + 2:abstract exact 0. + exact eq_refl. +Defined. (* or Qed: anomaly kernel doesn't support existential variables *) diff --git a/test-suite/success/sprop_uip.v b/test-suite/success/sprop_uip.v index 508cc2be7d..eae1b75689 100644 --- a/test-suite/success/sprop_uip.v +++ b/test-suite/success/sprop_uip.v @@ -95,6 +95,32 @@ Section funext. := eq_refl. End funext. +(* test reductions on inverted cases *) + +(* first check production of correct blocked cases *) +Definition lazy_seq_rect := Eval lazy in seq_rect. +Definition vseq_rect := Eval vm_compute in seq_rect. +Definition native_seq_rect := Eval native_compute in seq_rect. +Definition cbv_seq_rect := Eval cbv in seq_rect. + +(* check it reduces according to indices *) +Ltac reset := match goal with H : _ |- _ => change (match H with srefl _ => False end) end. +Ltac check := match goal with |- False => idtac end. +Lemma foo (H:seq 0 0) : False. +Proof. + reset. + Fail check. (* check that "reset" and "check" actually do something *) + + lazy; check; reset. + + (* TODO *) + vm_compute. Fail check. + native_compute. Fail check. + cbv. Fail check. + cbn. Fail check. + simpl. Fail check. +Abort. + (* check that extraction doesn't fall apart on matches with special reduction *) Require Extraction. diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index 047c9d0804..ef09188c33 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -97,6 +97,12 @@ Qed. (** * Properties of Exp *) (******************************************************************) +Lemma exp_neq_0 : forall x:R, exp x <> 0. +Proof. + intro x. + exact (not_eq_sym (Rlt_not_eq 0 (exp x) (exp_pos x))). +Qed. + Theorem exp_increasing : forall x y:R, x < y -> exp x < exp y. Proof. intros x y H. @@ -198,6 +204,8 @@ Definition ln (x:R) : R := | right a => 0 end. +Definition Rlog x y := (ln y)/(ln x). + Lemma exp_ln : forall x:R, 0 < x -> exp (ln x) = x. Proof. intros; unfold ln; decide (Rlt_dec 0 x) with H. @@ -268,6 +276,16 @@ Proof. elim (Rlt_irrefl _ H2). Qed. +Lemma ln_neq_0 : forall x:R, x <> 1 -> 0 < x -> ln x <> 0. +Proof. + intros x Hneq_x_1 Hlt_0_x. + rewrite <- ln_1. + intro H. + assert (x = 1) as H0. + + exact (ln_inv x 1 Hlt_0_x (ltac:(lra) : 0 < 1) H). + + contradiction. +Qed. + Theorem ln_mult : forall x y:R, 0 < x -> 0 < y -> ln (x * y) = ln x + ln y. Proof. intros x y H H0; apply exp_inv. @@ -279,6 +297,25 @@ Proof. apply Rmult_lt_0_compat; assumption. Qed. +Lemma ln_pow : forall (x : R), 0 < x -> forall (n : nat), ln (x^n) = (INR n)*(ln x). +Proof. + intros x Hx. + induction n as [|m Hm]. + + simpl. + rewrite ln_1. + exact (eq_sym (Rmult_0_l (ln x))). + + unfold pow. + fold pow. + rewrite (ln_mult x (x^m) Hx (pow_lt x m Hx)). + rewrite Hm. + rewrite <- (Rmult_1_l (ln x)) at 1. + rewrite <- (Rmult_plus_distr_r 1 (INR m) (ln x)). + rewrite (Rplus_comm 1 (INR m)). + destruct m as [|m]; simpl. + - lra. + - reflexivity. +Qed. + Theorem ln_Rinv : forall x:R, 0 < x -> ln (/ x) = - ln x. Proof. intros x H; apply exp_inv; repeat rewrite exp_ln || rewrite exp_Ropp. @@ -379,8 +416,6 @@ Qed. Definition Rpower (x y:R) := exp (y * ln x). -Local Infix "^R" := Rpower (at level 30, right associativity) : R_scope. - (******************************************************************) (** * Properties of Rpower *) (******************************************************************) @@ -395,13 +430,13 @@ Local Infix "^R" := Rpower (at level 30, right associativity) : R_scope. default value of [Rpower] on the negative side, as it is the case for [Rpower_O]). *) -Theorem Rpower_plus : forall x y z:R, z ^R (x + y) = z ^R x * z ^R y. +Theorem Rpower_plus : forall x y z:R, Rpower z (x + y) = Rpower z x * Rpower z y. Proof. intros x y z; unfold Rpower. rewrite Rmult_plus_distr_r; rewrite exp_plus; auto. Qed. -Theorem Rpower_mult : forall x y z:R, (x ^R y) ^R z = x ^R (y * z). +Theorem Rpower_mult : forall x y z:R, Rpower (Rpower x y) z = Rpower x (y * z). Proof. intros x y z; unfold Rpower. rewrite ln_exp. @@ -410,19 +445,19 @@ Proof. ring. Qed. -Theorem Rpower_O : forall x:R, 0 < x -> x ^R 0 = 1. +Theorem Rpower_O : forall x:R, 0 < x -> Rpower x 0 = 1. Proof. intros x _; unfold Rpower. rewrite Rmult_0_l; apply exp_0. Qed. -Theorem Rpower_1 : forall x:R, 0 < x -> x ^R 1 = x. +Theorem Rpower_1 : forall x:R, 0 < x -> Rpower x 1 = x. Proof. intros x H; unfold Rpower. rewrite Rmult_1_l; apply exp_ln; apply H. Qed. -Theorem Rpower_pow : forall (n:nat) (x:R), 0 < x -> x ^R INR n = x ^ n. +Theorem Rpower_pow : forall (n:nat) (x:R), 0 < x -> Rpower x (INR n) = x ^ n. Proof. intros n; elim n; simpl; auto; fold INR. intros x H; apply Rpower_O; auto. @@ -432,8 +467,15 @@ Proof. try apply Rmult_comm || assumption. Qed. +Lemma Rpower_nonzero : forall (x : R) (n : nat), 0 < x -> Rpower x (INR n) <> 0. +Proof. + intros x n H. + rewrite (Rpower_pow n x H). + exact (pow_nonzero x n (not_eq_sym (Rlt_not_eq 0 x H))). +Qed. + Theorem Rpower_lt : - forall x y z:R, 1 < x -> y < z -> x ^R y < x ^R z. + forall x y z:R, 1 < x -> y < z -> Rpower x y < Rpower x z. Proof. intros x y z H H1. unfold Rpower. @@ -445,7 +487,19 @@ Proof. apply H1. Qed. -Theorem Rpower_sqrt : forall x:R, 0 < x -> x ^R (/ 2) = sqrt x. +Lemma Rpower_Rlog : forall x y:R, x <> 1 -> 0 < x -> 0 < y -> Rpower x (Rlog x y) = y. +Proof. + intros x y H_neq_x_1 H_lt_0_x H_lt_0_y. + unfold Rpower. + unfold Rlog. + unfold Rdiv. + rewrite (Rmult_assoc (ln y) (/ln x) (ln x)). + rewrite (Rinv_l (ln x) (ln_neq_0 x H_neq_x_1 H_lt_0_x)). + rewrite (Rmult_1_r (ln y)). + exact (exp_ln y H_lt_0_y). +Qed. + +Theorem Rpower_sqrt : forall x:R, 0 < x -> Rpower x (/ 2) = sqrt x. Proof. intros x H. apply ln_inv. @@ -454,7 +508,7 @@ Proof. apply Rmult_eq_reg_l with (INR 2). apply exp_inv. fold Rpower. - cut ((x ^R (/ INR 2)) ^R INR 2 = sqrt x ^R INR 2). + cut (Rpower (Rpower x (/ INR 2)) (INR 2) = Rpower (sqrt x) (INR 2)). unfold Rpower; auto. rewrite Rpower_mult. rewrite Rinv_l. @@ -468,7 +522,7 @@ Proof. apply not_O_INR; discriminate. Qed. -Theorem Rpower_Ropp : forall x y:R, x ^R (- y) = / x ^R y. +Theorem Rpower_Ropp : forall x y:R, Rpower x (- y) = / (Rpower x y). Proof. unfold Rpower. intros x y; rewrite Ropp_mult_distr_l_reverse. @@ -490,7 +544,7 @@ Proof. Qed. Theorem Rle_Rpower : - forall e n m:R, 1 <= e -> n <= m -> e ^R n <= e ^R m. + forall e n m:R, 1 <= e -> n <= m -> Rpower e n <= Rpower e m. Proof. intros e n m [H | H]; intros H1. case H1. @@ -499,6 +553,27 @@ Proof. now rewrite <- H; unfold Rpower; rewrite ln_1, !Rmult_0_r; apply Rle_refl. Qed. +Lemma ln_Rpower : forall x y:R, ln (Rpower x y) = y * ln x. +Proof. + intros x y. + unfold Rpower. + rewrite (ln_exp (y * ln x)). + reflexivity. +Qed. + +Lemma Rlog_pow : forall (x : R) (n : nat), x <> 1 -> 0 < x -> Rlog x (x^n) = INR n. +Proof. + intros x n H_neq_x_1 H_lt_0_x. + rewrite <- (Rpower_pow n x H_lt_0_x). + unfold Rpower. + unfold Rlog. + rewrite (ln_exp (INR n * ln x)). + unfold Rdiv. + rewrite (Rmult_assoc (INR n) (ln x) (/ln x)). + rewrite (Rinv_r (ln x) (ln_neq_0 x H_neq_x_1 H_lt_0_x)). + exact (Rmult_1_r (INR n)). +Qed. + Theorem ln_lt_2 : / 2 < ln 2. Proof. apply Rmult_lt_reg_l with (r := 2). @@ -506,7 +581,7 @@ Proof. rewrite Rinv_r. apply exp_lt_inv. apply Rle_lt_trans with (1 := exp_le_3). - change (3 < 2 ^R (1 + 1)). + change (3 < Rpower 2 (1 + 1)). repeat rewrite Rpower_plus; repeat rewrite Rpower_1. now apply (IZR_lt 3 4). prove_sup0. @@ -651,7 +726,7 @@ Qed. Theorem Dpower : forall y z:R, 0 < y -> - D_in (fun x:R => x ^R z) (fun x:R => z * x ^R (z - 1)) ( + D_in (fun x:R => Rpower x z) (fun x:R => z * Rpower x (z - 1)) ( fun x:R => 0 < x) y. Proof. intros y z H; @@ -682,7 +757,7 @@ Qed. Theorem derivable_pt_lim_power : forall x y:R, - 0 < x -> derivable_pt_lim (fun x => x ^R y) x (y * x ^R (y - 1)). + 0 < x -> derivable_pt_lim (fun x => Rpower x y) x (y * Rpower x (y - 1)). Proof. intros x y H. unfold Rminus; rewrite Rpower_plus. @@ -711,13 +786,13 @@ intros x y z x0 y0; unfold Rpower. rewrite <- exp_plus, ln_mult, Rmult_plus_distr_l; auto. Qed. -Lemma Rlt_Rpower_l a b c: 0 < c -> 0 < a < b -> a ^R c < b ^R c. +Lemma Rlt_Rpower_l a b c: 0 < c -> 0 < a < b -> Rpower a c < Rpower b c. Proof. intros c0 [a0 ab]; apply exp_increasing. now apply Rmult_lt_compat_l; auto; apply ln_increasing; lra. Qed. -Lemma Rle_Rpower_l a b c: 0 <= c -> 0 < a <= b -> a ^R c <= b ^R c. +Lemma Rle_Rpower_l a b c: 0 <= c -> 0 < a <= b -> Rpower a c <= Rpower b c. Proof. intros [c0 | c0]; [ | intros; rewrite <- c0, !Rpower_O; [apply Rle_refl | |] ]. diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 4231915be1..bbcfcc4826 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -161,7 +161,7 @@ let init_gc () = * In this case, we put in place our preferred configuration. *) Gc.set { (Gc.get ()) with - Gc.minor_heap_size = 33554432; (* 4M *) + Gc.minor_heap_size = 32*1024*1024; (* 32Mwords x 8 bytes/word = 256Mb *) Gc.space_overhead = 120} let init_process () = |