diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/decl_mode/decl_interp.ml | 7 | ||||
| -rw-r--r-- | plugins/fourier/Fourier.v | 2 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 3 | ||||
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 75 | ||||
| -rw-r--r-- | plugins/funind/glob_term_to_relation.mli | 2 | ||||
| -rw-r--r-- | plugins/funind/glob_termops.ml | 60 | ||||
| -rw-r--r-- | plugins/funind/glob_termops.mli | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 46 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.mli | 2 | ||||
| -rw-r--r-- | plugins/funind/merge.ml | 18 | ||||
| -rw-r--r-- | plugins/ltac/g_ltac.ml4 | 2 | ||||
| -rw-r--r-- | plugins/ltac/g_obligations.ml4 | 2 | ||||
| -rw-r--r-- | plugins/ltac/g_rewrite.ml4 | 2 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.mli | 6 | ||||
| -rw-r--r-- | plugins/micromega/RMicromega.v | 315 | ||||
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 3 | ||||
| -rw-r--r-- | plugins/setoid_ring/RealField.v | 21 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 21 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 4 | ||||
| -rw-r--r-- | plugins/syntax/r_syntax.ml | 159 |
21 files changed, 265 insertions, 491 deletions
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 2b63ed6d6e..3b233d6ef4 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -264,7 +264,7 @@ let prod_one_id (loc,id) glob = GHole (loc,Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), glob) let let_in_one_alias (id,pat) glob = - GLetIn (Loc.ghost,Name id, glob_of_pat pat, glob) + GLetIn (Loc.ghost,Name id, glob_of_pat pat, None, glob) let rec bind_primary_aliases map pat = match pat with @@ -359,10 +359,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps = let rids=ref ([],pat_vars) in let npatt= deanonymize rids patt in List.rev (fst !rids),npatt in - let term2 = - GLetIn(Loc.ghost,Anonymous, - GCast(Loc.ghost,glob_of_pat npatt, - CastConv app_ind),term1) in + let term2=GLetIn(Loc.ghost,Anonymous,glob_of_pat npatt,Some app_ind,term1) in let term3=List.fold_right let_in_one_alias aliases term2 in let term4=List.fold_right prod_one_id loc_ids term3 in let term5=List.fold_right prod_one_hyp params term4 in diff --git a/plugins/fourier/Fourier.v b/plugins/fourier/Fourier.v index 1d7ee93ea3..a962547131 100644 --- a/plugins/fourier/Fourier.v +++ b/plugins/fourier/Fourier.v @@ -13,6 +13,6 @@ Require Export DiscrR. Require Export Fourier_util. Declare ML Module "fourier_plugin". -Ltac fourier := abstract (fourierz; field; discrR). +Ltac fourier := abstract (compute [IZR IPR IPR_2] in *; fourierz; field; discrR). Ltac fourier_eq := apply Rge_antisym; fourier. diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 527f4f0b12..3199474dde 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1217,7 +1217,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let mk_fixes : tactic = let pre_info,infos = list_chop fun_num infos in match pre_info,infos with - | [],[] -> tclIDTAC + | _,[] -> tclIDTAC | _, this_fix_info::others_infos -> let other_fix_infos = List.map @@ -1233,7 +1233,6 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam else Proofview.V82.of_tactic (Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1) other_fix_infos 0) - | _ -> anomaly (Pp.str "Not a valid information") in let first_tac : tactic = (* every operations until fix creations *) tclTHENSEQ diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index de2e5ea4e2..084de31c09 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -42,7 +42,7 @@ let compose_glob_context = match bt with | Lambda n -> mkGLambda(n,t,acc) | Prod n -> mkGProd(n,t,acc) - | LetIn n -> mkGLetIn(n,t,acc) + | LetIn n -> mkGLetIn(n,t,None,acc) in List.fold_right compose_binder @@ -489,7 +489,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = | u::l -> match t with | GLambda(loc,na,_,nat,b) -> - GLetIn(Loc.ghost,na,u,aux b l) + GLetIn(Loc.ghost,na,u,None,aux b l) | _ -> GApp(Loc.ghost,t,l) in @@ -535,7 +535,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = args_res.result } | GApp _ -> assert false (* we have collected all the app in [glob_decompose_app] *) - | GLetIn(_,n,t,b) -> + | GLetIn(_,n,v,t,b) -> (* if we have [(let x := v in b) t1 ... tn] , we discard our work and compute the list of constructor for [let x = v in (b t1 ... tn)] up to alpha conversion @@ -559,7 +559,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = env funnames avoid - (mkGLetIn(new_n,t,mkGApp(new_b,args))) + (mkGLetIn(new_n,v,t,mkGApp(new_b,args))) | GCases _ | GIf _ | GLetTuple _ -> (* we have [(match e1, ...., en with ..... end) t1 tn] we first compute the result from the case and @@ -603,12 +603,13 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let new_env = raw_push_named (n,None,t) env in let b_res = build_entry_lc new_env funnames avoid b in combine_results (combine_prod n) t_res b_res - | GLetIn(_,n,v,b) -> + | GLetIn(loc,n,v,typ,b) -> (* we first compute the list of constructor corresponding to the body of the function, then the one corresponding to the value [t] and combine the two result *) + let v = match typ with None -> v | Some t -> GCast (loc,v,CastConv t) in let v_res = build_entry_lc env funnames avoid v in let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in @@ -1115,8 +1116,9 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (* We have renamed all the anonymous functions during alpha_renaming phase *) end - | GLetIn(_,n,t,b) -> + | GLetIn(loc,n,v,t,b) -> begin + let t = match t with None -> v | Some t -> GCast (loc,v,CastConv t) in let not_free_in_t id = not (is_free_in id t) in let evd = (Evd.from_env env) in let t',ctx = Pretyping.understand env evd t in @@ -1131,7 +1133,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = match n with | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args -> new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) - | _ -> GLetIn(Loc.ghost,n,t,new_b), + | _ -> GLetIn(Loc.ghost,n,t,None,new_b), (* HOPING IT WOULD WORK *) Id.Set.filter not_free_in_t id_to_exclude end | GLetTuple(_,nal,(na,rto),t,b) -> @@ -1189,9 +1191,13 @@ let rec compute_cst_params relnames params = function compute_cst_params_from_app [] (params,rtl) | GApp(_,f,args) -> List.fold_left (compute_cst_params relnames) params (f::args) - | GLambda(_,_,_,t,b) | GProd(_,_,_,t,b) | GLetIn(_,_,t,b) | GLetTuple(_,_,_,t,b) -> + | GLambda(_,_,_,t,b) | GProd(_,_,_,t,b) | GLetTuple(_,_,_,t,b) -> let t_params = compute_cst_params relnames params t in compute_cst_params relnames t_params b + | GLetIn(_,_,v,t,b) -> + let v_params = compute_cst_params relnames params v in + let t_params = Option.fold_left (compute_cst_params relnames) v_params t in + compute_cst_params relnames t_params b | GCases _ -> params (* If there is still cases at this point they can only be discrimination ones *) @@ -1202,12 +1208,12 @@ let rec compute_cst_params relnames params = function and compute_cst_params_from_app acc (params,rtl) = match params,rtl with | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *) - | ((Name id,_,is_defined) as param)::params',(GVar(_,id'))::rtl' - when Id.compare id id' == 0 && not is_defined -> + | ((Name id,_,None) as param)::params',(GVar(_,id'))::rtl' + when Id.compare id id' == 0 -> compute_cst_params_from_app (param::acc) (params',rtl') | _ -> List.rev acc -let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool) list array) csts = +let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * glob_constr option) list array) csts = let rels_params = Array.mapi (fun i args -> @@ -1222,11 +1228,11 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool) let _ = try List.iteri - (fun i ((n,nt,is_defined) as param) -> + (fun i ((n,nt,typ) as param) -> if Array.for_all (fun l -> - let (n',nt',is_defined') = List.nth l i in - Name.equal n n' && glob_constr_eq nt nt' && (is_defined : bool) == is_defined') + let (n',nt',typ') = List.nth l i in + Name.equal n n' && glob_constr_eq nt nt' && Option.equal glob_constr_eq typ typ') rels_params then l := param::!l @@ -1241,15 +1247,15 @@ let rec rebuild_return_type rt = match rt with | Constrexpr.CProdN(loc,n,t') -> Constrexpr.CProdN(loc,n,rebuild_return_type t') - | Constrexpr.CLetIn(loc,na,t,t') -> - Constrexpr.CLetIn(loc,na,t,rebuild_return_type t') + | Constrexpr.CLetIn(loc,na,v,t,t') -> + Constrexpr.CLetIn(loc,na,v,t,rebuild_return_type t') | _ -> Constrexpr.CProdN(Loc.ghost,[[Loc.ghost,Anonymous], Constrexpr.Default Decl_kinds.Explicit,rt], Constrexpr.CSort(Loc.ghost,GType [])) let do_build_inductive - evd (funconstants: Term.pconstant list) (funsargs: (Name.t * glob_constr * bool) list list) + evd (funconstants: Term.pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list) returned_types (rtl:glob_constr list) = let _time1 = System.get_time () in @@ -1288,16 +1294,17 @@ let do_build_inductive let resa = Array.map (build_entry_lc env funnames_as_set []) rta in let env_with_graphs = let rel_arity i funargs = (* Rebuilding arities (with parameters) *) - let rel_first_args :(Name.t * Glob_term.glob_constr * bool ) list = + let rel_first_args :(Name.t * Glob_term.glob_constr * Glob_term.glob_constr option ) list = funargs in List.fold_right - (fun (n,t,is_defined) acc -> - if is_defined - then + (fun (n,t,typ) acc -> + match typ with + | Some typ -> Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, + Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ), acc) - else + | None -> Constrexpr.CProdN (Loc.ghost, [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], @@ -1355,16 +1362,17 @@ let do_build_inductive rel_constructors in let rel_arity i funargs = (* Reduilding arities (with parameters) *) - let rel_first_args :(Name.t * Glob_term.glob_constr * bool ) list = + let rel_first_args :(Name.t * Glob_term.glob_constr * Glob_term.glob_constr option ) list = (snd (List.chop nrel_params funargs)) in List.fold_right - (fun (n,t,is_defined) acc -> - if is_defined - then + (fun (n,t,typ) acc -> + match typ with + | Some typ -> Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, + Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ), acc) - else + | None -> Constrexpr.CProdN (Loc.ghost, [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], @@ -1391,12 +1399,13 @@ let do_build_inductive in let rel_params = List.map - (fun (n,t,is_defined) -> - if is_defined - then - Constrexpr.LocalRawDef((Loc.ghost,n), Constrextern.extern_glob_constr Id.Set.empty t) - else - Constrexpr.LocalRawAssum + (fun (n,t,typ) -> + match typ with + | Some typ -> + Constrexpr.CLocalDef((Loc.ghost,n), Constrextern.extern_glob_constr Id.Set.empty t, + Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ)) + | None -> + Constrexpr.CLocalAssum ([(Loc.ghost,n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t) ) rels_params diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli index 5bb1376e26..0cab5a6d35 100644 --- a/plugins/funind/glob_term_to_relation.mli +++ b/plugins/funind/glob_term_to_relation.mli @@ -12,7 +12,7 @@ val build_inductive : *) Evd.evar_map -> Term.pconstant list -> - (Name.t*Glob_term.glob_constr*bool) list list -> (* The list of function args *) + (Name.t*Glob_term.glob_constr*Glob_term.glob_constr option) list list -> (* The list of function args *) Constrexpr.constr_expr list -> (* The list of function returned type *) Glob_term.glob_constr list -> (* the list of body *) unit diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 4e561fc7e5..99f50437b9 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -15,7 +15,7 @@ let mkGVar id = GVar(Loc.ghost,id) let mkGApp(rt,rtl) = GApp(Loc.ghost,rt,rtl) let mkGLambda(n,t,b) = GLambda(Loc.ghost,n,Explicit,t,b) let mkGProd(n,t,b) = GProd(Loc.ghost,n,Explicit,t,b) -let mkGLetIn(n,t,b) = GLetIn(Loc.ghost,n,t,b) +let mkGLetIn(n,b,t,c) = GLetIn(Loc.ghost,n,b,t,c) let mkGCases(rto,l,brl) = GCases(Loc.ghost,Term.RegularStyle,rto,l,brl) let mkGSort s = GSort(Loc.ghost,s) let mkGHole () = GHole(Loc.ghost,Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None) @@ -37,8 +37,8 @@ let glob_decompose_prod_or_letin = let rec glob_decompose_prod args = function | GProd(_,n,k,t,b) -> glob_decompose_prod ((n,None,Some t)::args) b - | GLetIn(_,n,t,b) -> - glob_decompose_prod ((n,Some t,None)::args) b + | GLetIn(_,n,b,t,c) -> + glob_decompose_prod ((n,Some b,t)::args) c | rt -> args,rt in glob_decompose_prod [] @@ -51,7 +51,7 @@ let glob_compose_prod_or_letin = fun concl decl -> match decl with | (n,None,Some t) -> mkGProd(n,t,concl) - | (n,Some bdy,None) -> mkGLetIn(n,bdy,concl) + | (n,Some bdy,t) -> mkGLetIn(n,bdy,t,concl) | _ -> assert false) let glob_decompose_prod_n n = @@ -73,8 +73,8 @@ let glob_decompose_prod_or_letin_n n = match c with | GProd(_,n,_,t,b) -> glob_decompose_prod (i-1) ((n,None,Some t)::args) b - | GLetIn(_,n,t,b) -> - glob_decompose_prod (i-1) ((n,Some t,None)::args) b + | GLetIn(_,n,b,t,c) -> + glob_decompose_prod (i-1) ((n,Some b,t)::args) c | rt -> args,rt in glob_decompose_prod n [] @@ -150,10 +150,11 @@ let change_vars = change_vars mapping t, change_vars (remove_name_from_mapping mapping name) b ) - | GLetIn(loc,name,def,b) -> + | GLetIn(loc,name,def,typ,b) -> GLetIn(loc, name, change_vars mapping def, + Option.map (change_vars mapping) typ, change_vars (remove_name_from_mapping mapping name) b ) | GLetTuple(loc,nal,(na,rto),b,e) -> @@ -272,10 +273,11 @@ let rec alpha_rt excluded rt = let new_t = alpha_rt excluded t in let new_b = alpha_rt excluded b in GProd(loc,Anonymous,k,new_t,new_b) - | GLetIn(loc,Anonymous,t,b) -> - let new_t = alpha_rt excluded t in + | GLetIn(loc,Anonymous,b,t,c) -> let new_b = alpha_rt excluded b in - GLetIn(loc,Anonymous,new_t,new_b) + let new_t = Option.map (alpha_rt excluded) t in + let new_c = alpha_rt excluded c in + GLetIn(loc,Anonymous,new_b,new_t,new_c) | GLambda(loc,Name id,k,t,b) -> let new_id = Namegen.next_ident_away id excluded in let t,b = @@ -302,19 +304,17 @@ let rec alpha_rt excluded rt = let new_t = alpha_rt new_excluded t in let new_b = alpha_rt new_excluded b in GProd(loc,Name new_id,k,new_t,new_b) - | GLetIn(loc,Name id,t,b) -> + | GLetIn(loc,Name id,b,t,c) -> let new_id = Namegen.next_ident_away id excluded in - let t,b = - if Id.equal new_id id - then t,b - else - let replace = change_vars (Id.Map.add id new_id Id.Map.empty) in - (t,replace b) + let c = + if Id.equal new_id id then c + else change_vars (Id.Map.add id new_id Id.Map.empty) c in let new_excluded = new_id::excluded in - let new_t = alpha_rt new_excluded t in let new_b = alpha_rt new_excluded b in - GLetIn(loc,Name new_id,new_t,new_b) + let new_t = Option.map (alpha_rt new_excluded) t in + let new_c = alpha_rt new_excluded c in + GLetIn(loc,Name new_id,new_b,new_t,new_c) | GLetTuple(loc,nal,(na,rto),t,b) -> @@ -388,13 +388,20 @@ let is_free_in id = | GEvar _ -> false | GPatVar _ -> false | GApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl) - | GLambda(_,n,_,t,b) | GProd(_,n,_,t,b) | GLetIn(_,n,t,b) -> + | GLambda(_,n,_,t,b) | GProd(_,n,_,t,b) -> let check_in_b = match n with | Name id' -> not (Id.equal id' id) | _ -> true in is_free_in t || (check_in_b && is_free_in b) + | GLetIn(_,n,b,t,c) -> + let check_in_c = + match n with + | Name id' -> not (Id.equal id' id) + | _ -> true + in + is_free_in b || Option.cata is_free_in true t || (check_in_c && is_free_in c) | GCases(_,_,_,el,brl) -> (List.exists (fun (e,_) -> is_free_in e) el) || List.exists is_free_in_br brl @@ -473,11 +480,12 @@ let replace_var_by_term x_id term = replace_var_by_pattern t, replace_var_by_pattern b ) - | GLetIn(_,Name id,_,_) when Id.compare id x_id == 0 -> rt - | GLetIn(loc,name,def,b) -> + | GLetIn(_,Name id,_,_,_) when Id.compare id x_id == 0 -> rt + | GLetIn(loc,name,def,typ,b) -> GLetIn(loc, name, replace_var_by_pattern def, + Option.map (replace_var_by_pattern) typ, replace_var_by_pattern b ) | GLetTuple(_,nal,_,_,_) @@ -589,7 +597,7 @@ let ids_of_glob_constr c = ids_of_glob_constr [] g @ List.flatten (List.map (ids_of_glob_constr []) args) @ acc | GLambda (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc | GProd (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc - | GLetIn (loc,na,b,c) -> idof na :: ids_of_glob_constr [] b @ ids_of_glob_constr [] c @ acc + | GLetIn (loc,na,b,t,c) -> idof na :: ids_of_glob_constr [] b @ Option.cata (ids_of_glob_constr []) [] t @ ids_of_glob_constr [] c @ acc | GCast (loc,c,(CastConv t|CastVM t|CastNative t)) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] t @ acc | GCast (loc,c,CastCoerce) -> ids_of_glob_constr [] c @ acc | GIf (loc,c,(na,po),b1,b2) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] b1 @ ids_of_glob_constr [] b2 @ acc @@ -633,9 +641,9 @@ let zeta_normalize = zeta_normalize_term t, zeta_normalize_term b ) - | GLetIn(_,Name id,def,b) -> + | GLetIn(_,Name id,def,typ,b) -> zeta_normalize_term (replace_var_by_term id def b) - | GLetIn(loc,Anonymous,def,b) -> zeta_normalize_term b + | GLetIn(loc,Anonymous,def,typ,b) -> zeta_normalize_term b | GLetTuple(loc,nal,(na,rto),def,b) -> GLetTuple(loc, nal, @@ -690,7 +698,7 @@ let expand_as = | GApp(loc,f,args) -> GApp(loc,expand_as map f,List.map (expand_as map) args) | GLambda(loc,na,k,t,b) -> GLambda(loc,na,k,expand_as map t, expand_as map b) | GProd(loc,na,k,t,b) -> GProd(loc,na,k,expand_as map t, expand_as map b) - | GLetIn(loc,na,v,b) -> GLetIn(loc,na, expand_as map v,expand_as map b) + | GLetIn(loc,na,v,typ,b) -> GLetIn(loc,na, expand_as map v,Option.map (expand_as map) typ,expand_as map b) | GLetTuple(loc,nal,(na,po),v,b) -> GLetTuple(loc,nal,(na,Option.map (expand_as map) po), expand_as map v, expand_as map b) diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 179e8fe8d9..84359a36b7 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -19,7 +19,7 @@ val mkGVar : Id.t -> glob_constr val mkGApp : glob_constr*(glob_constr list) -> glob_constr val mkGLambda : Name.t * glob_constr * glob_constr -> glob_constr val mkGProd : Name.t * glob_constr * glob_constr -> glob_constr -val mkGLetIn : Name.t * glob_constr * glob_constr -> glob_constr +val mkGLetIn : Name.t * glob_constr * glob_constr option * glob_constr -> glob_constr val mkGCases : glob_constr option * tomatch_tuples * cases_clauses -> glob_constr val mkGSort : glob_sort -> glob_constr val mkGHole : unit -> glob_constr (* we only build Evd.BinderType Anonymous holes *) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 99b04898ba..d394fe313e 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -129,11 +129,11 @@ let functional_induction with_clean c princl pat = let rec abstract_glob_constr c = function | [] -> c - | Constrexpr.LocalRawDef (x,b)::bl -> Constrexpr_ops.mkLetInC(x,b,abstract_glob_constr c bl) - | Constrexpr.LocalRawAssum (idl,k,t)::bl -> + | Constrexpr.CLocalDef (x,b,t)::bl -> Constrexpr_ops.mkLetInC(x,b,t,abstract_glob_constr c bl) + | Constrexpr.CLocalAssum (idl,k,t)::bl -> List.fold_right (fun x b -> Constrexpr_ops.mkLambdaC([x],k,t,b)) idl (abstract_glob_constr c bl) - | Constrexpr.LocalPattern _::bl -> assert false + | Constrexpr.CLocalPattern _::bl -> assert false let interp_casted_constr_with_implicits env sigma impls c = Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls @@ -192,8 +192,10 @@ let is_rec names = | GRec _ -> error "GRec not handled" | GIf(_,b,_,lhs,rhs) -> (lookup names b) || (lookup names lhs) || (lookup names rhs) - | GLetIn(_,na,t,b) | GLambda(_,na,_,t,b) | GProd(_,na,_,t,b) -> + | GProd(_,na,_,t,b) | GLambda(_,na,_,t,b) -> lookup names t || lookup (Nameops.name_fold Id.Set.remove na names) b + | GLetIn(_,na,b,t,c) -> + lookup names b || Option.cata (lookup names) true t || lookup (Nameops.name_fold Id.Set.remove na names) c | GLetTuple(_,nal,_,t,b) -> lookup names t || lookup (List.fold_left @@ -215,9 +217,9 @@ let is_rec names = let rec local_binders_length = function (* Assume that no `{ ... } contexts occur *) | [] -> 0 - | Constrexpr.LocalRawDef _::bl -> 1 + local_binders_length bl - | Constrexpr.LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl - | Constrexpr.LocalPattern _::bl -> assert false + | Constrexpr.CLocalDef _::bl -> 1 + local_binders_length bl + | Constrexpr.CLocalAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl + | Constrexpr.CLocalPattern _::bl -> assert false let prepare_body ((name,_,args,types,_),_) rt = let n = local_binders_length args in @@ -496,7 +498,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas | None -> begin match args with - | [Constrexpr.LocalRawAssum ([(_,Name x)],k,t)] -> t,x + | [Constrexpr.CLocalAssum ([(_,Name x)],k,t)] -> t,x | _ -> error "Recursive argument must be specified" end | Some wf_args -> @@ -504,7 +506,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas match List.find (function - | Constrexpr.LocalRawAssum(l,k,t) -> + | Constrexpr.CLocalAssum(l,k,t) -> List.exists (function (_,Name id) -> Id.equal id wf_args | _ -> false) l @@ -512,7 +514,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas ) args with - | Constrexpr.LocalRawAssum(_,k,t) -> t,wf_args + | Constrexpr.CLocalAssum(_,k,t) -> t,wf_args | _ -> assert false with Not_found -> assert false in @@ -570,10 +572,10 @@ let make_assoc assoc l1 l2 = let rec rebuild_bl (aux,assoc) bl typ = match bl,typ with | [], _ -> (List.rev aux,replace_vars_constr_expr assoc typ,assoc) - | (Constrexpr.LocalRawAssum(nal,bk,_))::bl',typ -> + | (Constrexpr.CLocalAssum(nal,bk,_))::bl',typ -> rebuild_nal (aux,assoc) bk bl' nal (List.length nal) typ - | (Constrexpr.LocalRawDef(na,_))::bl',Constrexpr.CLetIn(_,_,nat,typ') -> - rebuild_bl ((Constrexpr.LocalRawDef(na,replace_vars_constr_expr assoc nat)::aux),assoc) + | (Constrexpr.CLocalDef(na,_,_))::bl',Constrexpr.CLetIn(_,_,nat,ty,typ') -> + rebuild_bl ((Constrexpr.CLocalDef(na,replace_vars_constr_expr assoc nat,Option.map (replace_vars_constr_expr assoc) ty (* ??? *))::aux),assoc) bl' typ' | _ -> assert false and rebuild_nal (aux,assoc) bk bl' nal lnal typ = @@ -586,7 +588,7 @@ let rec rebuild_bl (aux,assoc) bl typ = then let old_nal',new_nal' = List.chop lnal nal' in let nassoc = make_assoc assoc old_nal' nal in - let assum = LocalRawAssum(nal,bk,replace_vars_constr_expr assoc nal't) in + let assum = CLocalAssum(nal,bk,replace_vars_constr_expr assoc nal't) in rebuild_bl ((assum :: aux), nassoc) bl' (if List.is_empty new_nal' && List.is_empty rest then typ' @@ -596,7 +598,7 @@ let rec rebuild_bl (aux,assoc) bl typ = else let captured_nal,non_captured_nal = List.chop lnal' nal in let nassoc = make_assoc assoc nal' captured_nal in - let assum = LocalRawAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't) in + let assum = CLocalAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't) in rebuild_nal ((assum :: aux), nassoc) bk bl' non_captured_nal (lnal - lnal') (CProdN(Loc.ghost,rest,typ')) | _ -> assert false @@ -726,8 +728,8 @@ let rec add_args id new_args b = CLambdaN(loc, List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, add_args id new_args b1) - | CLetIn(loc,na,b1,b2) -> - CLetIn(loc,na,add_args id new_args b1,add_args id new_args b2) + | CLetIn(loc,na,b1,t,b2) -> + CLetIn(loc,na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2) | CAppExpl(loc,(pf,r,us),exprl) -> begin match r with @@ -813,7 +815,7 @@ let rec chop_n_arrow n t = | _ -> anomaly (Pp.str "Not enough products") -let rec get_args b t : Constrexpr.local_binder list * +let rec get_args b t : Constrexpr.local_binder_expr list * Constrexpr.constr_expr * Constrexpr.constr_expr = match b with | Constrexpr.CLambdaN (loc, (nal_ta), b') -> @@ -824,7 +826,7 @@ let rec get_args b t : Constrexpr.local_binder list * in let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in (List.map (fun (nal,k,ta) -> - (Constrexpr.LocalRawAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t'' + (Constrexpr.CLocalAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t'' end | _ -> [],b,t @@ -865,13 +867,13 @@ let make_graph (f_ref:global_reference) = List.flatten (List.map (function - | Constrexpr.LocalRawDef (na,_)-> [] - | Constrexpr.LocalRawAssum (nal,_,_) -> + | Constrexpr.CLocalDef (na,_,_)-> [] + | Constrexpr.CLocalAssum (nal,_,_) -> List.map (fun (loc,n) -> CRef(Libnames.Ident(loc, Nameops.out_name n),None)) nal - | Constrexpr.LocalPattern _ -> assert false + | Constrexpr.CLocalPattern _ -> assert false ) nal_tas ) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index a45effb167..aed0fa331c 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -70,8 +70,8 @@ let chop_rlambda_n = then List.rev acc,rt else match rt with - | Glob_term.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b - | Glob_term.GLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b + | Glob_term.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b + | Glob_term.GLetIn(_,name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b | _ -> raise (CErrors.UserError(Some "chop_rlambda_n", str "chop_rlambda_n: Not enough Lambdas")) diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index e5c756f564..2aabfa003e 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -34,7 +34,7 @@ val list_add_set_eq : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list val chop_rlambda_n : int -> Glob_term.glob_constr -> - (Name.t*Glob_term.glob_constr*bool) list * Glob_term.glob_constr + (Name.t*Glob_term.glob_constr*Glob_term.glob_constr option) list * Glob_term.glob_constr val chop_rprod_n : int -> Glob_term.glob_constr -> (Name.t*Glob_term.glob_constr) list * Glob_term.glob_constr diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 19c2ed4178..9c23be68ae 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -510,14 +510,14 @@ let rec merge_app c1 c2 id1 id2 shift filter_shift_stable = let args = filter_shift_stable lnk (arr1 @ arr2) in GApp (Loc.ghost,GVar (Loc.ghost,shift.ident) , args) | GApp(_,f1, arr1), GApp(_,f2,arr2) -> raise NoMerge - | GLetIn(_,nme,bdy,trm) , _ -> + | GLetIn(_,nme,bdy,typ,trm) , _ -> let _ = prstr "\nICI2!\n" in let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in - GLetIn(Loc.ghost,nme,bdy,newtrm) - | _, GLetIn(_,nme,bdy,trm) -> + GLetIn(Loc.ghost,nme,bdy,typ,newtrm) + | _, GLetIn(_,nme,bdy,typ,trm) -> let _ = prstr "\nICI3!\n" in let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in - GLetIn(Loc.ghost,nme,bdy,newtrm) + GLetIn(Loc.ghost,nme,bdy,typ,newtrm) | _ -> let _ = prstr "\nICI4!\n" in raise NoMerge @@ -528,14 +528,14 @@ let rec merge_app_unsafe c1 c2 shift filter_shift_stable = let args = filter_shift_stable lnk (arr1 @ arr2) in GApp (Loc.ghost,GVar(Loc.ghost,shift.ident) , args) (* FIXME: what if the function appears in the body of the let? *) - | GLetIn(_,nme,bdy,trm) , _ -> + | GLetIn(_,nme,bdy,typ,trm) , _ -> let _ = prstr "\nICI2 '!\n" in let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in - GLetIn(Loc.ghost,nme,bdy,newtrm) - | _, GLetIn(_,nme,bdy,trm) -> + GLetIn(Loc.ghost,nme,bdy,typ,newtrm) + | _, GLetIn(_,nme,bdy,typ,trm) -> let _ = prstr "\nICI3 '!\n" in let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in - GLetIn(Loc.ghost,nme,bdy,newtrm) + GLetIn(Loc.ghost,nme,bdy,typ,newtrm) | _ -> let _ = prstr "\nICI4 '!\n" in raise NoMerge @@ -822,7 +822,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = let _ = prNamedRConstr (string_of_name nme) tp in let _ = prstr " ; " in let typ = glob_constr_to_constr_expr tp in - LocalRawAssum ([(Loc.ghost,nme)], Constrexpr_ops.default_binder_kind, typ) :: acc) + CLocalAssum ([(Loc.ghost,nme)], Constrexpr_ops.default_binder_kind, typ) :: acc) [] params in let concl = Constrextern.extern_constr false (Global.env()) Evd.empty concl in let arity,_ = diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index aab5687465..fd33a779dc 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +DECLARE PLUGIN "ltac_plugin" + open Util open Pp open Compat diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index d286a58708..3e6e2db605 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -70,7 +70,7 @@ GEXTEND Gram Constr.closed_binder: [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in - [LocalRawAssum ([id], default_binder_kind, typ)] + [CLocalAssum ([id], default_binder_kind, typ)] ] ]; END diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index b1c4f58eb8..c50100bf55 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -183,7 +183,7 @@ VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF [ declare_relation a aeq n None None (Some lemma3) ] END -type binders_argtype = local_binder list +type binders_argtype = local_binder_expr list let wit_binders = (Genarg.create_arg "binders" : binders_argtype Genarg.uniform_genarg_type) diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 35c4483513..4fdce0c84f 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -77,17 +77,17 @@ val is_applied_rewrite_relation : env -> evar_map -> Context.Rel.t -> constr -> types option val declare_relation : - ?binders:local_binder list -> constr_expr -> constr_expr -> Id.t -> + ?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> constr_expr option -> constr_expr option -> constr_expr option -> unit val add_setoid : - bool -> local_binder list -> constr_expr -> constr_expr -> constr_expr -> + bool -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr -> Id.t -> unit val add_morphism_infer : bool -> constr_expr -> Id.t -> unit val add_morphism : - bool -> local_binder list -> constr_expr -> constr_expr -> Id.t -> unit + bool -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> unit val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v index 2352d78d63..30e475b710 100644 --- a/plugins/micromega/RMicromega.v +++ b/plugins/micromega/RMicromega.v @@ -18,7 +18,7 @@ Require Import Refl. Require Import Raxioms RIneq Rpow_def DiscrR. Require Import QArith. Require Import Qfield. - +Require Import Qreals. Require Setoid. (*Declare ML Module "micromega_plugin".*) @@ -38,15 +38,8 @@ Proof. exact Rplus_opp_r. Qed. -Add Ring Rring : Rsrt. Open Scope R_scope. -Lemma Rmult_neutral : forall x:R , 0 * x = 0. -Proof. - intro ; ring. -Qed. - - Lemma Rsor : SOR R0 R1 Rplus Rmult Rminus Ropp (@eq R) Rle Rlt. Proof. constructor; intros ; subst ; try (intuition (subst; try ring ; auto with real)). @@ -59,142 +52,41 @@ Proof. apply (Rlt_irrefl m) ; auto. apply Rnot_le_lt. auto with real. destruct (total_order_T n m) as [ [H1 | H1] | H1] ; auto. - intros. - rewrite <- (Rmult_neutral m). - apply (Rmult_lt_compat_r) ; auto. -Qed. - -Definition IQR := fun x : Q => (IZR (Qnum x) * / IZR (' Qden x))%R. - - -Lemma Rinv_elim : forall x y z, - y <> 0 -> (z * y = x <-> x * / y = z). -Proof. - intros. - split ; intros. - subst. - rewrite Rmult_assoc. - rewrite Rinv_r; auto. - ring. - subst. - rewrite Rmult_assoc. - rewrite (Rmult_comm (/ y)). - rewrite Rinv_r ; auto. - ring. -Qed. - -Ltac INR_nat_of_P := - match goal with - | H : context[INR (Pos.to_nat ?X)] |- _ => - revert H ; - let HH := fresh in - assert (HH := pos_INR_nat_of_P X) ; revert HH ; generalize (INR (Pos.to_nat X)) - | |- context[INR (Pos.to_nat ?X)] => - let HH := fresh in - assert (HH := pos_INR_nat_of_P X) ; revert HH ; generalize (INR (Pos.to_nat X)) - end. - -Ltac add_eq expr val := set (temp := expr) ; - generalize (eq_refl temp) ; - unfold temp at 1 ; generalize temp ; intro val ; clear temp. - -Ltac Rinv_elim := - match goal with - | |- context[?x * / ?y] => - let z := fresh "v" in - add_eq (x * / y) z ; - let H := fresh in intro H ; rewrite <- Rinv_elim in H - end. - -Lemma Rlt_neq : forall r , 0 < r -> r <> 0. -Proof. - red. intros. - subst. - apply (Rlt_irrefl 0 H). + now apply Rmult_lt_0_compat. Qed. +Notation IQR := Q2R (only parsing). Lemma Rinv_1 : forall x, x * / 1 = x. Proof. intro. - Rinv_elim. - subst ; ring. - apply R1_neq_R0. + rewrite Rinv_1. + apply Rmult_1_r. Qed. -Lemma Qeq_true : forall x y, - Qeq_bool x y = true -> - IQR x = IQR y. +Lemma Qeq_true : forall x y, Qeq_bool x y = true -> IQR x = IQR y. Proof. - unfold IQR. - simpl. - intros. - apply Qeq_bool_eq in H. - unfold Qeq in H. - assert (IZR (Qnum x * ' Qden y) = IZR (Qnum y * ' Qden x))%Z. - rewrite H. reflexivity. - repeat rewrite mult_IZR in H0. - simpl in H0. - revert H0. - repeat INR_nat_of_P. intros. - apply Rinv_elim in H2 ; [| apply Rlt_neq ; auto]. - rewrite <- H2. - field. - split ; apply Rlt_neq ; auto. + now apply Qeq_eqR, Qeq_bool_eq. Qed. Lemma Qeq_false : forall x y, Qeq_bool x y = false -> IQR x <> IQR y. Proof. intros. - apply Qeq_bool_neq in H. - intro. apply H. clear H. - unfold Qeq,IQR in *. - simpl in *. - revert H0. - repeat Rinv_elim. - intros. - subst. - assert (IZR (Qnum x * ' Qden y)%Z = IZR (Qnum y * ' Qden x)%Z). - repeat rewrite mult_IZR. - simpl. - rewrite <- H0. rewrite <- H. - ring. - apply eq_IZR ; auto. - INR_nat_of_P; intros; apply Rlt_neq ; auto. - INR_nat_of_P; intros ; apply Rlt_neq ; auto. + apply Qeq_bool_neq in H. + contradict H. + now apply eqR_Qeq. Qed. - - Lemma Qle_true : forall x y : Q, Qle_bool x y = true -> IQR x <= IQR y. Proof. intros. - apply Qle_bool_imp_le in H. - unfold Qle in H. - unfold IQR. - simpl in *. - apply IZR_le in H. - repeat rewrite mult_IZR in H. - simpl in H. - repeat INR_nat_of_P; intros. - assert (Hr := Rlt_neq r H). - assert (Hr0 := Rlt_neq r0 H0). - replace (IZR (Qnum x) * / r) with ((IZR (Qnum x) * r0) * (/r * /r0)). - replace (IZR (Qnum y) * / r0) with ((IZR (Qnum y) * r) * (/r * /r0)). - apply Rmult_le_compat_r ; auto. - apply Rmult_le_pos. - unfold Rle. left. apply Rinv_0_lt_compat ; auto. - unfold Rle. left. apply Rinv_0_lt_compat ; auto. - field ; intuition. - field ; intuition. + now apply Qle_Rle, Qle_bool_imp_le. Qed. - - Lemma IQR_0 : IQR 0 = 0. Proof. - compute. apply Rinv_1. + apply Rmult_0_l. Qed. Lemma IQR_1 : IQR 1 = 1. @@ -202,160 +94,6 @@ Proof. compute. apply Rinv_1. Qed. -Lemma IQR_plus : forall x y, IQR (x + y) = IQR x + IQR y. -Proof. - intros. - unfold IQR. - simpl in *. - rewrite plus_IZR in *. - rewrite mult_IZR in *. - simpl. - rewrite Pos2Nat.inj_mul. - rewrite mult_INR. - rewrite mult_IZR. - simpl. - repeat INR_nat_of_P. - intros. field. - split ; apply Rlt_neq ; auto. -Qed. - -Lemma IQR_opp : forall x, IQR (- x) = - IQR x. -Proof. - intros. - unfold IQR. - simpl. - rewrite opp_IZR. - ring. -Qed. - -Lemma IQR_minus : forall x y, IQR (x - y) = IQR x - IQR y. -Proof. - intros. - unfold Qminus. - rewrite IQR_plus. - rewrite IQR_opp. - ring. -Qed. - - -Lemma IQR_mult : forall x y, IQR (x * y) = IQR x * IQR y. -Proof. - unfold IQR ; intros. - simpl. - repeat rewrite mult_IZR. - rewrite Pos2Nat.inj_mul. - rewrite mult_INR. - repeat INR_nat_of_P. - intros. field ; split ; apply Rlt_neq ; auto. -Qed. - -Lemma IQR_inv_lt : forall x, (0 < x)%Q -> - IQR (/ x) = / IQR x. -Proof. - unfold IQR ; simpl. - intros. - unfold Qlt in H. - revert H. - simpl. - intros. - unfold Qinv. - destruct x. - destruct Qnum ; simpl in *. - exfalso. auto with zarith. - clear H. - repeat INR_nat_of_P. - intros. - assert (HH := Rlt_neq _ H). - assert (HH0 := Rlt_neq _ H0). - rewrite Rinv_mult_distr ; auto. - rewrite Rinv_involutive ; auto. - ring. - apply Rinv_0_lt_compat in H0. - apply Rlt_neq ; auto. - simpl in H. - exfalso. - rewrite Pos.mul_comm in H. - compute in H. - discriminate. -Qed. - -Lemma Qinv_opp : forall x, (- (/ x) = / ( -x))%Q. -Proof. - destruct x ; destruct Qnum ; reflexivity. -Qed. - -Lemma Qopp_involutive_strong : forall x, (- - x = x)%Q. -Proof. - intros. - destruct x. - unfold Qopp. - simpl. - rewrite Z.opp_involutive. - reflexivity. -Qed. - -Lemma Ropp_0 : forall r , - r = 0 -> r = 0. -Proof. - intros. - rewrite <- (Ropp_involutive r). - apply Ropp_eq_0_compat ; auto. -Qed. - -Lemma IQR_x_0 : forall x, IQR x = 0 -> x == 0%Q. -Proof. - destruct x ; simpl. - unfold IQR. - simpl. - INR_nat_of_P. - intros. - apply Rmult_integral in H0. - destruct H0. - apply eq_IZR_R0 in H0. - subst. - reflexivity. - exfalso. - apply Rinv_0_lt_compat in H. - rewrite <- H0 in H. - apply Rlt_irrefl in H. auto. -Qed. - - -Lemma IQR_inv_gt : forall x, (0 > x)%Q -> - IQR (/ x) = / IQR x. -Proof. - intros. - rewrite <- (Qopp_involutive_strong x). - rewrite <- Qinv_opp. - rewrite IQR_opp. - rewrite IQR_inv_lt. - repeat rewrite IQR_opp. - rewrite Ropp_inv_permute. - auto. - intro. - apply Ropp_0 in H0. - apply IQR_x_0 in H0. - rewrite H0 in H. - compute in H. discriminate. - unfold Qlt in *. - destruct x ; simpl in *. - auto with zarith. -Qed. - -Lemma IQR_inv : forall x, ~ x == 0 -> - IQR (/ x) = / IQR x. -Proof. - intros. - assert ( 0 > x \/ 0 < x)%Q. - destruct x ; unfold Qlt, Qeq in * ; simpl in *. - rewrite Z.mul_1_r in *. - destruct Qnum ; simpl in * ; intuition auto. - right. reflexivity. - left ; reflexivity. - destruct H0. - apply IQR_inv_gt ; auto. - apply IQR_inv_lt ; auto. -Qed. - Lemma IQR_inv_ext : forall x, IQR (/ x) = (if Qeq_bool x 0 then 0 else / IQR x). Proof. @@ -366,18 +104,13 @@ Proof. destruct x ; simpl. unfold Qeq in H. simpl in H. - replace Qnum with 0%Z. - compute. rewrite Rinv_1. - reflexivity. - rewrite <- H. ring. + rewrite Zmult_1_r in H. + rewrite H. + apply Rmult_0_l. intros. - apply IQR_inv. - intro. - rewrite <- Qeq_bool_iff in H0. - congruence. + now apply Q2R_inv, Qeq_bool_neq. Qed. - Notation to_nat := N.to_nat. Lemma QSORaddon : @@ -391,10 +124,10 @@ Proof. constructor ; intros ; try reflexivity. apply IQR_0. apply IQR_1. - apply IQR_plus. - apply IQR_minus. - apply IQR_mult. - apply IQR_opp. + apply Q2R_plus. + apply Q2R_minus. + apply Q2R_mult. + apply Q2R_opp. apply Qeq_true ; auto. apply R_power_theory. apply Qeq_false. @@ -453,13 +186,13 @@ Proof. apply IQR_1. reflexivity. unfold IQR. simpl. rewrite Rinv_1. reflexivity. - apply IQR_plus. - apply IQR_minus. - apply IQR_mult. + apply Q2R_plus. + apply Q2R_minus. + apply Q2R_mult. rewrite <- IHc. apply IQR_inv_ext. rewrite <- IHc. - apply IQR_opp. + apply Q2R_opp. Qed. Require Import EnvRing. diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 97f29df823..6051cb3d3c 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -364,6 +364,7 @@ struct [["Coq";"Reals" ; "Rdefinitions"]; ["Coq";"Reals" ; "Rpow_def"] ; ["Coq";"Reals" ; "Raxioms"] ; + ["Coq";"QArith"; "Qreals"] ; ] let z_modules = [["Coq";"ZArith";"BinInt"]] @@ -479,7 +480,7 @@ struct let coq_Rinv = lazy (r_constant "Rinv") let coq_Rpower = lazy (r_constant "pow") let coq_IZR = lazy (r_constant "IZR") - let coq_IQR = lazy (constant "IQR") + let coq_IQR = lazy (r_constant "Q2R") let coq_PEX = lazy (constant "PEX" ) diff --git a/plugins/setoid_ring/RealField.v b/plugins/setoid_ring/RealField.v index 293722125b..facd2e0625 100644 --- a/plugins/setoid_ring/RealField.v +++ b/plugins/setoid_ring/RealField.v @@ -59,11 +59,12 @@ Notation Rset := (Eqsth R). Notation Rext := (Eq_ext Rplus Rmult Ropp). Lemma Rlt_0_2 : 0 < 2. +Proof. apply Rlt_trans with (0 + 1). apply Rlt_n_Sn. rewrite Rplus_comm. apply Rplus_lt_compat_l. - replace 1 with (0 + 1). + replace R1 with (0 + 1). apply Rlt_n_Sn. apply Rplus_0_l. Qed. @@ -126,9 +127,17 @@ Ltac Rpow_tac t := | _ => constr:(N.of_nat t) end. -Add Field RField : Rfield - (completeness Zeq_bool_complete, power_tac R_power_theory [Rpow_tac]). - - - +Ltac IZR_tac t := + match t with + | R0 => constr:(0%Z) + | R1 => constr:(1%Z) + | IZR ?u => + match isZcst u with + | true => u + | _ => constr:(InitialRing.NotConstant) + end + | _ => constr:(InitialRing.NotConstant) + end. +Add Field RField : Rfield + (completeness Zeq_bool_complete, constants [IZR_tac], power_tac R_power_theory [Rpow_tac]). diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index eb35d3f806..87ee666605 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -323,14 +323,16 @@ let _ = add_map "ring" (map_with_eq [coq_cons,(function -1->Eval|2->Rec|_->Prot); coq_nil, (function -1->Eval|_ -> Prot); + my_reference "IDphi", (function _->Eval); + my_reference "gen_phiZ", (function _->Eval); (* Pphi_dev: evaluate polynomial and coef operations, protect ring operations and make recursive call on the var map *) pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot); pol_cst "Pphi_pow", - (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot); + (function -1|8|9|10|13|15|17->Eval|11|16->Rec|_->Prot); (* PEeval: evaluate morphism and polynomial, protect ring operations and make recursive call on the var map *) - pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot)]) + pol_cst "PEeval", (function -1|8|10|13->Eval|12->Rec|_->Prot)]) (****************************************************************************) (* Ring database *) @@ -756,12 +758,14 @@ let _ = add_map "field" (map_with_eq [coq_cons,(function -1->Eval|2->Rec|_->Prot); coq_nil, (function -1->Eval|_ -> Prot); + my_reference "IDphi", (function _->Eval); + my_reference "gen_phiZ", (function _->Eval); (* display_linear: evaluate polynomials and coef operations, protect field operations and make recursive call on the var map *) my_reference "display_linear", (function -1|9|10|11|12|13|15|16->Eval|14->Rec|_->Prot); my_reference "display_pow_linear", - (function -1|9|10|11|12|13|14|16|18|19->Eval|17->Rec|_->Prot); + (function -1|9|10|11|14|16|18|19->Eval|12|17->Rec|_->Prot); (* Pphi_dev: evaluate polynomial and coef operations, protect ring operations and make recursive call on the var map *) pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot); @@ -769,19 +773,20 @@ let _ = add_map "field" (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot); (* PEeval: evaluate morphism and polynomial, protect ring operations and make recursive call on the var map *) - pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot); + pol_cst "PEeval", (function -1|8|10|13->Eval|12->Rec|_->Prot); (* FEeval: evaluate morphism, protect field operations and make recursive call on the var map *) - my_reference "FEeval", (function -1|8|9|10|11|14->Eval|13->Rec|_->Prot)]);; + my_reference "FEeval", (function -1|10|12|15->Eval|14->Rec|_->Prot)]);; let _ = add_map "field_cond" (map_without_eq [coq_cons,(function -1->Eval|2->Rec|_->Prot); coq_nil, (function -1->Eval|_ -> Prot); - (* PCond: evaluate morphism and denum list, protect ring + my_reference "IDphi", (function _->Eval); + my_reference "gen_phiZ", (function _->Eval); + (* PCond: evaluate denum list, protect ring operations and make recursive call on the var map *) - my_reference "PCond", (function -1|9|11|14->Eval|13->Rec|_->Prot)]);; -(* (function -1|9|11->Eval|10->Rec|_->Prot)]);;*) + my_reference "PCond", (function -1|11|14->Eval|9|13->Rec|_->Prot)]);; let _ = Redexpr.declare_reduction "simpl_field_expr" diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 03c4ae47dd..4d55946336 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -156,7 +156,7 @@ let mkCHole loc = CHole (loc, None, IntroAnonymous, None) let mkCLambda loc name ty t = CLambdaN (loc, [[loc, name], Default Explicit, ty], t) let mkCLetIn loc name bo t = - CLetIn (loc, (loc, name), bo, t) + CLetIn (loc, (loc, name), bo, None, t) let mkCCast loc t ty = CCast (loc,t, dC ty) (** Constructors for rawconstr *) let mkRHole = GHole (dummy_loc, InternalHole, IntroAnonymous, None) @@ -1193,7 +1193,7 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = pp(lazy(str"typed as: " ++ pr_pattern_w_ids red)); let mkXLetIn loc x (a,(g,c)) = match c with | Some b -> a,(g,Some (mkCLetIn loc x (mkCHole loc) b)) - | None -> a,(GLetIn (loc,x,(GHole (loc, BinderType x, IntroAnonymous, None)), g), None) in + | None -> a,(GLetIn (loc,x,(GHole (loc, BinderType x, IntroAnonymous, None)), None, g), None) in match red with | T t -> let sigma, t = interp_term ist gl t in sigma, T t | In_T t -> let sigma, t = interp_term ist gl t in sigma, In_T t diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 3ae2d45f32..8f065f5282 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -9,6 +9,8 @@ open Util open Names open Globnames +open Glob_term +open Bigint (* Poor's man DECLARE PLUGIN *) let __coq_plugin_name = "r_syntax_plugin" @@ -17,95 +19,105 @@ let () = Mltop.add_known_module __coq_plugin_name exception Non_closed_number (**********************************************************************) -(* Parsing R via scopes *) +(* Parsing positive via scopes *) (**********************************************************************) -open Glob_term -open Bigint +let binnums = ["Coq";"Numbers";"BinNums"] let make_dir l = DirPath.make (List.rev_map Id.of_string l) -let rdefinitions = make_dir ["Coq";"Reals";"Rdefinitions"] -let make_path dir id = Libnames.make_path dir (Id.of_string id) +let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) + +let positive_path = make_path binnums "positive" + +(* TODO: temporary hack *) +let make_kn dir id = Globnames.encode_mind dir id + +let positive_kn = make_kn (make_dir binnums) (Id.of_string "positive") +let glob_positive = IndRef (positive_kn,0) +let path_of_xI = ((positive_kn,0),1) +let path_of_xO = ((positive_kn,0),2) +let path_of_xH = ((positive_kn,0),3) +let glob_xI = ConstructRef path_of_xI +let glob_xO = ConstructRef path_of_xO +let glob_xH = ConstructRef path_of_xH + +let pos_of_bignat dloc x = + let ref_xI = GRef (dloc, glob_xI, None) in + let ref_xH = GRef (dloc, glob_xH, None) in + let ref_xO = GRef (dloc, glob_xO, None) in + let rec pos_of x = + match div2_with_rest x with + | (q,false) -> GApp (dloc, ref_xO,[pos_of q]) + | (q,true) when not (Bigint.equal q zero) -> GApp (dloc,ref_xI,[pos_of q]) + | (q,true) -> ref_xH + in + pos_of x + +(**********************************************************************) +(* Printing positive via scopes *) +(**********************************************************************) + +let rec bignat_of_pos = function + | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a) + | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a)) + | GRef (_, a, _) when Globnames.eq_gr a glob_xH -> Bigint.one + | _ -> raise Non_closed_number + +(**********************************************************************) +(* Parsing Z via scopes *) +(**********************************************************************) +let z_path = make_path binnums "Z" +let z_kn = make_kn (make_dir binnums) (Id.of_string "Z") +let glob_z = IndRef (z_kn,0) +let path_of_ZERO = ((z_kn,0),1) +let path_of_POS = ((z_kn,0),2) +let path_of_NEG = ((z_kn,0),3) +let glob_ZERO = ConstructRef path_of_ZERO +let glob_POS = ConstructRef path_of_POS +let glob_NEG = ConstructRef path_of_NEG + +let z_of_int dloc n = + if not (Bigint.equal n zero) then + let sgn, n = + if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in + GApp(dloc, GRef (dloc,sgn,None), [pos_of_bignat dloc n]) + else + GRef (dloc, glob_ZERO, None) + +(**********************************************************************) +(* Printing Z via scopes *) +(**********************************************************************) + +let bigint_of_z = function + | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a + | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a) + | GRef (_, a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero + | _ -> raise Non_closed_number + +(**********************************************************************) +(* Parsing R via scopes *) +(**********************************************************************) + +let rdefinitions = ["Coq";"Reals";"Rdefinitions"] let r_path = make_path rdefinitions "R" (* TODO: temporary hack *) let make_path dir id = Globnames.encode_con dir (Id.of_string id) -let r_kn = make_path rdefinitions "R" -let glob_R = ConstRef r_kn -let glob_R1 = ConstRef (make_path rdefinitions "R1") -let glob_R0 = ConstRef (make_path rdefinitions "R0") -let glob_Ropp = ConstRef (make_path rdefinitions "Ropp") -let glob_Rplus = ConstRef (make_path rdefinitions "Rplus") -let glob_Rmult = ConstRef (make_path rdefinitions "Rmult") - -let two = mult_2 one -let three = add_1 two -let four = mult_2 two - -(* Unary representation of strictly positive numbers *) -let rec small_r dloc n = - if equal one n then GRef (dloc, glob_R1, None) - else GApp(dloc,GRef (dloc,glob_Rplus, None), - [GRef (dloc, glob_R1, None);small_r dloc (sub_1 n)]) - -let r_of_posint dloc n = - let r1 = GRef (dloc, glob_R1, None) in - let r2 = small_r dloc two in - let rec r_of_pos n = - if less_than n four then small_r dloc n - else - let (q,r) = div2_with_rest n in - let b = GApp(dloc,GRef(dloc,glob_Rmult,None),[r2;r_of_pos q]) in - if r then GApp(dloc,GRef(dloc,glob_Rplus,None),[r1;b]) else b in - if not (Bigint.equal n zero) then r_of_pos n else GRef(dloc,glob_R0,None) +let glob_IZR = ConstRef (make_path (make_dir rdefinitions) "IZR") let r_of_int dloc z = - if is_strictly_neg z then - GApp (dloc, GRef(dloc,glob_Ropp,None), [r_of_posint dloc (neg z)]) - else - r_of_posint dloc z + GApp (dloc, GRef(dloc,glob_IZR,None), [z_of_int dloc z]) (**********************************************************************) (* Printing R via scopes *) (**********************************************************************) -let bignat_of_r = -(* for numbers > 1 *) -let rec bignat_of_pos = function - (* 1+1 *) - | GApp (_,GRef (_,p,_), [GRef (_,o1,_); GRef (_,o2,_)]) - when Globnames.eq_gr p glob_Rplus && Globnames.eq_gr o1 glob_R1 && Globnames.eq_gr o2 glob_R1 -> two - (* 1+(1+1) *) - | GApp (_,GRef (_,p1,_), [GRef (_,o1,_); - GApp(_,GRef (_,p2,_),[GRef(_,o2,_);GRef(_,o3,_)])]) - when Globnames.eq_gr p1 glob_Rplus && Globnames.eq_gr p2 glob_Rplus && - Globnames.eq_gr o1 glob_R1 && Globnames.eq_gr o2 glob_R1 && Globnames.eq_gr o3 glob_R1 -> three - (* (1+1)*b *) - | GApp (_,GRef (_,p,_), [a; b]) when Globnames.eq_gr p glob_Rmult -> - if not (Bigint.equal (bignat_of_pos a) two) then raise Non_closed_number; - mult_2 (bignat_of_pos b) - (* 1+(1+1)*b *) - | GApp (_,GRef (_,p1,_), [GRef (_,o,_); GApp (_,GRef (_,p2,_),[a;b])]) - when Globnames.eq_gr p1 glob_Rplus && Globnames.eq_gr p2 glob_Rmult && Globnames.eq_gr o glob_R1 -> - if not (Bigint.equal (bignat_of_pos a) two) then raise Non_closed_number; - add_1 (mult_2 (bignat_of_pos b)) - | _ -> raise Non_closed_number -in -let bignat_of_r = function - | GRef (_,a,_) when Globnames.eq_gr a glob_R0 -> zero - | GRef (_,a,_) when Globnames.eq_gr a glob_R1 -> one - | r -> bignat_of_pos r -in -bignat_of_r - let bigint_of_r = function - | GApp (_,GRef (_,o,_), [a]) when Globnames.eq_gr o glob_Ropp -> - let n = bignat_of_r a in - if Bigint.equal n zero then raise Non_closed_number; - neg n - | a -> bignat_of_r a + | GApp (_,GRef (_,o,_), [a]) when Globnames.eq_gr o glob_IZR -> + bigint_of_z a + | _ -> raise Non_closed_number let uninterp_r p = try @@ -113,12 +125,9 @@ let uninterp_r p = with Non_closed_number -> None -let mkGRef gr = GRef (Loc.ghost,gr,None) - let _ = Notation.declare_numeral_interpreter "R_scope" (r_path,["Coq";"Reals";"Rdefinitions"]) r_of_int - (List.map mkGRef - [glob_Ropp;glob_R0;glob_Rplus;glob_Rmult;glob_R1], + ([GRef (Loc.ghost,glob_IZR,None)], uninterp_r, false) |