diff options
Diffstat (limited to 'contrib')
43 files changed, 819 insertions, 814 deletions
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml index 48444509..0c906712 100644 --- a/contrib/extraction/modutil.ml +++ b/contrib/extraction/modutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: modutil.ml 10665 2008-03-14 12:10:09Z soubiran $ i*) +(*i $Id: modutil.ml 11262 2008-07-24 20:59:29Z letouzey $ i*) open Names open Declarations @@ -347,6 +347,73 @@ and optim_me to_appear s = function MEapply (optim_me to_appear s me, optim_me to_appear s me') | MEfunctor (mbid,mt,me) -> MEfunctor (mbid,mt, optim_me to_appear s me) -let optimize_struct to_appear struc = - let subst = ref (Refmap.empty : ml_ast Refmap.t) in - List.map (fun (mp,lse) -> (mp, optim_se true to_appear subst lse)) struc +(* After these optimisations, some dependencies may not be needed anymore. + For monolithic extraction, we recompute a minimal set of dependencies. *) + +exception NoDepCheck + +let base_r = function + | ConstRef c as r -> r + | IndRef (kn,_) -> IndRef (kn,0) + | ConstructRef ((kn,_),_) -> IndRef (kn,0) + | _ -> assert false + +let reset_needed, add_needed, found_needed, is_needed = + let needed = ref Refset.empty in + ((fun l -> needed := Refset.empty), + (fun r -> needed := Refset.add (base_r r) !needed), + (fun r -> needed := Refset.remove (base_r r) !needed), + (fun r -> Refset.mem (base_r r) !needed)) + +let declared_refs = function + | Dind (kn,_) -> [|IndRef (kn,0)|] + | Dtype (r,_,_) -> [|r|] + | Dterm (r,_,_) -> [|r|] + | Dfix (rv,_,_) -> rv + +(* Computes the dependencies of a declaration, except in case + of custom extraction. *) + +let compute_deps_decl = function + | Dind (kn,ind) -> + (* Todo Later : avoid dependencies when Extract Inductive *) + ind_iter_references add_needed add_needed add_needed kn ind + | Dtype (r,ids,t) -> + if not (is_custom r) then type_iter_references add_needed t + | Dterm (r,u,t) -> + type_iter_references add_needed t; + if not (is_custom r) then + ast_iter_references add_needed add_needed add_needed u + | Dfix _ as d -> + (* Todo Later : avoid dependencies when Extract Constant *) + decl_iter_references add_needed add_needed add_needed d + +let rec depcheck_se = function + | [] -> [] + | ((l,SEdecl d) as t)::se -> + let se' = depcheck_se se in + let rv = declared_refs d in + if not (array_exists is_needed rv) then + (Array.iter remove_info_axiom rv; se') + else + (Array.iter found_needed rv; compute_deps_decl d; t::se') + | _ -> raise NoDepCheck + +let rec depcheck_struct = function + | [] -> [] + | (mp,lse)::struc -> + let struc' = depcheck_struct struc in + let lse' = depcheck_se lse in + (mp,lse')::struc' + +let optimize_struct to_appear struc = + let subst = ref (Refmap.empty : ml_ast Refmap.t) in + let opt_struc = + List.map (fun (mp,lse) -> (mp, optim_se true to_appear subst lse)) struc + in + try + if modular () then raise NoDepCheck; + reset_needed (); + List.iter add_needed to_appear; + depcheck_struct opt_struc + with NoDepCheck -> opt_struc diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml index abf461c1..10f669e1 100644 --- a/contrib/extraction/table.ml +++ b/contrib/extraction/table.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: table.ml 10348 2007-12-06 17:36:14Z aspiwack $ i*) +(*i $Id: table.ml 11262 2008-07-24 20:59:29Z letouzey $ i*) open Names open Term @@ -175,6 +175,7 @@ let info_axioms = ref Refset.empty let log_axioms = ref Refset.empty let init_axioms () = info_axioms := Refset.empty; log_axioms := Refset.empty let add_info_axiom r = info_axioms := Refset.add r !info_axioms +let remove_info_axiom r = info_axioms := Refset.remove r !info_axioms let add_log_axiom r = log_axioms := Refset.add r !log_axioms (*s Extraction mode: modular or monolithic *) diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli index ca02cb4d..4dbccd08 100644 --- a/contrib/extraction/table.mli +++ b/contrib/extraction/table.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: table.mli 10245 2007-10-21 13:41:53Z letouzey $ i*) +(*i $Id: table.mli 11262 2008-07-24 20:59:29Z letouzey $ i*) open Names open Libnames @@ -77,6 +77,7 @@ val is_projection : global_reference -> bool val projection_arity : global_reference -> int val add_info_axiom : global_reference -> unit +val remove_info_axiom : global_reference -> unit val add_log_axiom : global_reference -> unit val reset_tables : unit -> unit diff --git a/contrib/firstorder/sequent.ml b/contrib/firstorder/sequent.ml index c832d30f..e931f8fd 100644 --- a/contrib/firstorder/sequent.ml +++ b/contrib/firstorder/sequent.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: sequent.ml 10824 2008-04-21 13:57:03Z msozeau $ *) +(* $Id: sequent.ml 11282 2008-07-28 11:51:53Z msozeau $ *) open Term open Util @@ -281,7 +281,7 @@ let create_with_auto_hints l depth gl= searchtable_map dbname with Not_found-> error ("Firstorder: "^dbname^" : No such Hint database") in - Hint_db.iter g (snd hdb) in + Hint_db.iter g hdb in List.iter h l; !seqref diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index 3d80bd00..bd335d30 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -136,7 +136,7 @@ let change_hyp_with_using msg hyp_id t tac : tactic = fun g -> let prov_id = pf_get_new_id hyp_id g in tclTHENS - ((* observe_tac msg *) (forward (Some (tclCOMPLETE tac)) (Genarg.IntroIdentifier prov_id) t)) + ((* observe_tac msg *) (forward (Some (tclCOMPLETE tac)) (dummy_loc,Genarg.IntroIdentifier prov_id) t)) [tclTHENLIST [ (* observe_tac "change_hyp_with_using thin" *) (thin [hyp_id]); @@ -388,7 +388,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = in (* observe_tac "rec hyp " *) (tclTHENS - (assert_as true (Genarg.IntroIdentifier rec_pte_id) t_x) + (assert_as true (dummy_loc, Genarg.IntroIdentifier rec_pte_id) t_x) [ (* observe_tac "prove rec hyp" *) (prove_rec_hyp eq_hyps); (* observe_tac "prove rec hyp" *) @@ -571,7 +571,7 @@ let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id fun g -> let prov_hid = pf_get_new_id hid g in tclTHENLIST[ - forward None (Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args)); + forward None (dummy_loc,Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args)); thin [hid]; h_rename [prov_hid,hid] ] g @@ -1399,7 +1399,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = false (true,5) [Lazy.force refl_equal] - [empty_transparent_state, Auto.Hint_db.empty] + [Auto.Hint_db.empty false] ) ) ) @@ -1497,7 +1497,7 @@ let prove_principle_for_gen (tclTHEN (forward (Some ((fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g))) - (Genarg.IntroIdentifier wf_thm_id) + (dummy_loc,Genarg.IntroIdentifier wf_thm_id) (mkApp (delayed_force well_founded,[|input_type;relation|]))) ( (* observe_tac *) @@ -1561,7 +1561,7 @@ let prove_principle_for_gen ); (* observe_tac "" *) (forward (Some (prove_rec_arg_acc)) - (Genarg.IntroIdentifier acc_rec_arg_id) + (dummy_loc,Genarg.IntroIdentifier acc_rec_arg_id) (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|])) ); (* observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids))); diff --git a/contrib/funind/g_indfun.ml4 b/contrib/funind/g_indfun.ml4 index dae76f2d..d435f513 100644 --- a/contrib/funind/g_indfun.ml4 +++ b/contrib/funind/g_indfun.ml4 @@ -90,11 +90,6 @@ END TACTIC EXTEND newfunind ["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> [ - let pat = - match pat with - | None -> IntroAnonymous - | Some pat -> pat - in let c = match cl with | [] -> assert false | [c] -> c @@ -106,11 +101,6 @@ END TACTIC EXTEND snewfunind ["soft" "functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> [ - let pat = - match pat with - | None -> IntroAnonymous - | Some pat -> pat - in let c = match cl with | [] -> assert false | [c] -> c @@ -319,7 +309,7 @@ let poseq_unsafe idunsafe cstr gl = tclTHEN (Tactics.letin_tac None (Name idunsafe) cstr allClauses) (tclTHENFIRST - (Tactics.assert_as true IntroAnonymous (mkEq typ (mkVar idunsafe) cstr)) + (Tactics.assert_as true (Util.dummy_loc,IntroAnonymous) (mkEq typ (mkVar idunsafe) cstr)) Tactics.reflexivity) gl @@ -396,7 +386,7 @@ let finduction (oid:identifier option) (heuristic: fapp_info list -> fapp_info l fun gl -> (functional_induction true (applist (info.fname, List.rev !list_constr_largs)) - None IntroAnonymous) gl)) + None None) gl)) nexttac)) ordered_info_list in (* we try each (f t u v) until one does not fail *) (* TODO: try also to mix functional schemes *) diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index a6cbb321..79ef0097 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -120,7 +120,7 @@ let functional_induction with_clean c princl pat = princ_infos args_as_induction_constr princ' - pat + (None,pat) None) subst_and_reduce g diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml index 63d44916..f62d70ab 100644 --- a/contrib/funind/invfun.ml +++ b/contrib/funind/invfun.ml @@ -280,13 +280,13 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.map (fun (_,_,br_type) -> List.map - (fun id -> Genarg.IntroIdentifier id) + (fun id -> dummy_loc, Genarg.IntroIdentifier id) (generate_fresh_id (id_of_string "y") ids (List.length (fst (decompose_prod_assum br_type)))) ) branches in (* before building the full intro pattern for the principle *) - let pat = Genarg.IntroOrAndPattern intro_pats in + let pat = Some (dummy_loc,Genarg.IntroOrAndPattern intro_pats) in let eq_ind = Coqlib.build_coq_eq () in let eq_construct = mkConstruct((destInd eq_ind),1) in (* The next to referencies will be used to find out which constructor to apply in each branch *) @@ -297,7 +297,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem (* We get the identifiers of this branch *) let this_branche_ids = List.fold_right - (fun pat acc -> + (fun (_,pat) acc -> match pat with | Genarg.IntroIdentifier id -> Idset.add id acc | _ -> anomaly "Not an identifier" @@ -447,7 +447,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem [ observe_tac "intro args_names" (tclMAP h_intro args_names); observe_tac "principle" (forward (Some (h_exact f_principle)) - (Genarg.IntroIdentifier principle_id) + (dummy_loc,Genarg.IntroIdentifier principle_id) princ_type); tclTHEN_i (observe_tac "functional_induction" ( @@ -948,7 +948,7 @@ let functional_inversion kn hid fconst f_correct : tactic = h_generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]; thin [hid]; h_intro hid; - Inv.inv FullInversion Genarg.IntroAnonymous (Rawterm.NamedHyp hid); + Inv.inv FullInversion None (Rawterm.NamedHyp hid); (fun g -> let new_ids = List.filter (fun id -> not (Idset.mem id old_ids)) (pf_ids_of_hyps g) in tclMAP (revert_graph kn pre_tac) (hid::new_ids) g diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml index c9bf2f1f..5bd7a6b2 100644 --- a/contrib/funind/recdef.ml +++ b/contrib/funind/recdef.ml @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: recdef.ml 11094 2008-06-10 19:35:23Z herbelin $ *) +(* $Id: recdef.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Term open Termops @@ -1157,7 +1157,7 @@ let rec introduce_all_values_eq cont_tac functional termine [] -> let heq2 = next_global_ident_away true heq_id ids in tclTHENLIST - [forward None (IntroIdentifier heq2) + [forward None (dummy_loc,IntroIdentifier heq2) (mkApp(mkVar heq1, [|f_S(f_S(mkVar pmax))|])); simpl_iter (onHyp heq2); unfold_in_hyp [((true,[1]), evaluable_of_global_reference diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index 6ec0fac4..767a7dd6 100644 --- a/contrib/interface/blast.ml +++ b/contrib/interface/blast.ml @@ -161,21 +161,22 @@ let rec e_trivial_fail_db db_list local_db goal = let d = pf_last_hyp g' in let hintl = make_resolve_hyp (pf_env g') (project g') d in (e_trivial_fail_db db_list - (add_hint_list hintl local_db) g'))) :: + (Hint_db.add_list hintl local_db) g'))) :: (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) ) in tclFIRST (List.map tclCOMPLETE tacl) goal and e_my_find_search db_list local_db hdc concl = let hdc = head_of_constr_reference hdc in - let flags = Auto.auto_unif_flags in let hintl = if occur_existential concl then - list_map_append (fun (st, db) -> List.map (fun x -> ({flags with Unification.modulo_delta = st}, x)) - (Hint_db.map_all hdc db)) (local_db::db_list) + list_map_append (fun db -> + let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in + List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list) else - list_map_append (fun (st, db) -> List.map (fun x -> ({flags with Unification.modulo_delta = st}, x)) - (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list) + list_map_append (fun db -> + let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in + List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list) in let tac_of_hint = fun (st, ({pri=b; pat = p; code=t} as _patac)) -> @@ -279,7 +280,7 @@ module MySearchProblem = struct let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') in - let ldb = add_hint_list hintl (List.hd s.localdb) in + let ldb = Hint_db.add_list hintl (List.hd s.localdb) in { depth = s.depth; tacres = res; last_tactic = pp; dblist = s.dblist; localdb = ldb :: List.tl s.localdb }) @@ -375,7 +376,7 @@ let rec trivial_fail_db db_list local_db gl = tclTHEN intro (fun g'-> let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') - in trivial_fail_db db_list (add_hint_list hintl local_db) g') + in trivial_fail_db db_list (Hint_db.add_list hintl local_db) g') in tclFIRST (assumption::intro_tac:: @@ -383,14 +384,15 @@ let rec trivial_fail_db db_list local_db gl = (trivial_resolve db_list local_db (pf_concl gl)))) gl and my_find_search db_list local_db hdc concl = - let flags = Auto.auto_unif_flags in let tacl = if occur_existential concl then - list_map_append (fun (st, db) -> List.map (fun x -> {flags with Unification.modulo_delta = st}, x) - (Hint_db.map_all hdc db)) (local_db::db_list) + list_map_append (fun db -> + let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in + List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list) else - list_map_append (fun (st, db) -> List.map (fun x -> {flags with Unification.modulo_delta = st}, x) - (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list) + list_map_append (fun db -> + let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in + List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list) in List.map (fun (st, {pri=b; pat=p; code=t} as _patac) -> @@ -477,7 +479,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal = with Failure _ -> [] in (free_try - (search_gen decomp n db_list (add_hint_list hintl local_db) [d]) + (search_gen decomp n db_list (Hint_db.add_list hintl local_db) [d]) g')) in let rec_tacs = diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml index dd40c5cc..203bc9e3 100644 --- a/contrib/interface/depends.ml +++ b/contrib/interface/depends.ml @@ -57,8 +57,7 @@ let explore_tree pfs = and explain_prim = function | Refine c -> "Refine " ^ (string_of_ppcmds (Printer.prterm c)) | Intro identifier -> "Intro" - | Intro_replacing identifier -> "Intro_replacing" - | Cut (bool, identifier, types) -> "Cut" + | Cut (bool, _, identifier, types) -> "Cut" | FixRule (identifier, int, l) -> "FixRule" | Cofix (identifier, l) -> "Cofix" | Convert_concl (types, cast_kind) -> "Convert_concl" @@ -269,7 +268,7 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of igtal acc) | TacMatch (_, tac, tacexpr_mrl) -> failwith "depends_of_tacexpr of a Match not implemented yet" - | TacMatchContext (_, _, tacexpr_mrl) -> failwith "depends_of_tacexpr of a Match Context not implemented yet" + | TacMatchGoal (_, _, tacexpr_mrl) -> failwith "depends_of_tacexpr of a Match Context not implemented yet" | TacFun tacfa -> depends_of_tac_fun_ast tacfa acc | TacArg tacarg -> depends_of_tac_arg tacarg acc and depends_of_atomic_tacexpr atexpr acc = let depends_of_'constr_with_bindings = depends_of_'a_with_bindings depends_of_'constr in match atexpr with @@ -281,7 +280,8 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of | TacExact c | TacExactNoCheck c | TacVmCastNoCheck c -> depends_of_'constr c acc - | TacApply (_, _, cb) -> depends_of_'constr_with_bindings cb acc + | TacApply (_, _, [cb]) -> depends_of_'constr_with_bindings cb acc + | TacApply (_, _, _) -> failwith "TODO" | TacElim (_, cwb, cwbo) -> depends_of_'constr_with_bindings cwb (Option.fold_right depends_of_'constr_with_bindings cwbo acc) @@ -302,14 +302,13 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of | TacLetTac (_,c,_,_) -> depends_of_'constr c acc (* Derived basic tactics *) - | TacSimpleInduction _ - | TacSimpleDestruct _ + | TacSimpleInductionDestruct _ | TacDoubleInduction _ -> acc - | TacNewInduction (_, cwbial, cwbo, _, _) - | TacNewDestruct (_, cwbial, cwbo, _, _) -> + | TacInductionDestruct (_, _, [cwbial, cwbo, _, _]) -> list_union_map (depends_of_'a_induction_arg depends_of_'constr_with_bindings) cwbial (Option.fold_right depends_of_'constr_with_bindings cwbo acc) + | TacInductionDestruct (_, _, _) -> failwith "TODO" | TacDecomposeAnd c | TacDecomposeOr c -> depends_of_'constr c acc | TacDecompose (il, c) -> depends_of_'constr c (list_union_map depends_of_'ind il acc) @@ -410,8 +409,7 @@ let depends_of_compound_rule cr acc = match cr with and depends_of_prim_rule pr acc = match pr with | Refine c -> depends_of_constr c acc | Intro id -> acc - | Intro_replacing id -> acc - | Cut (_, _, t) -> depends_of_constr t acc (* TODO: check what 2nd argument contains *) + | Cut (_, _, _, t) -> depends_of_constr t acc (* TODO: check what 3nd argument contains *) | FixRule (_, _, l) -> list_union_map (o depends_of_constr trd_of_3) l acc (* TODO: check what the arguments contain *) | Cofix (_, l) -> list_union_map (o depends_of_constr snd) l acc (* TODO: check what the arguments contain *) | Convert_concl (t, _) -> depends_of_constr t acc diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml index 06b957d9..65eadf13 100644 --- a/contrib/interface/pbp.ml +++ b/contrib/interface/pbp.ml @@ -48,7 +48,7 @@ type pbp_atom = | PbpTryClear of identifier list | PbpGeneralize of identifier * identifier list | PbpLApply of identifier (* = CutAndApply *) - | PbpIntros of intro_pattern_expr list + | PbpIntros of intro_pattern_expr located list | PbpSplit (* Existential *) | PbpExists of identifier @@ -93,7 +93,7 @@ type pbp_rule = (identifier list * pbp_sequence option;; -let make_named_intro id = PbpIntros [IntroIdentifier id];; +let make_named_intro id = PbpIntros [zz,IntroIdentifier id];; let make_clears str_list = PbpThen [PbpTryClear str_list] @@ -171,7 +171,7 @@ let make_pbp_atomic_tactic = function | PbpRight -> TacAtom (zz, TacRight (false,NoBindings)) | PbpIntros l -> TacAtom (zz, TacIntroPattern l) | PbpLApply h -> TacAtom (zz, TacLApply (make_var h)) - | PbpApply h -> TacAtom (zz, TacApply (true,false,(make_var h,NoBindings))) + | PbpApply h -> TacAtom (zz, TacApply (true,false,[make_var h,NoBindings])) | PbpElim (hyp_name, names) -> let bind = List.map (fun s ->(zz,NamedHyp s,make_pbp_pattern s)) names in TacAtom @@ -255,9 +255,9 @@ fun avoid c path -> match kind_of_term c, path with or_and_tree_to_intro_pattern (id2::avoid) cont_expr path in let patt_list = if a = 1 then - [cont_patt; IntroIdentifier id2] + [zz,cont_patt; zz,IntroIdentifier id2] else - [IntroIdentifier id2; cont_patt] in + [zz,IntroIdentifier id2; zz,cont_patt] in (IntroOrAndPattern[patt_list], avoid_names, id, c, path, rank, total_branches) | (App(oper, [|c1; c2|]), 2::3::path) @@ -268,7 +268,7 @@ fun avoid c path -> match kind_of_term c, path with let id1 = next_global_ident x avoid in let cont_patt, avoid_names, id, c, path, rank, total_branches = or_and_tree_to_intro_pattern (id1::avoid) body path in - (IntroOrAndPattern[[IntroIdentifier id1; cont_patt]], + (IntroOrAndPattern[[zz,IntroIdentifier id1; zz,cont_patt]], avoid_names, id, c, path, rank, total_branches) | _ -> assert false) | (App(oper, [|c1; c2|]), 2::a::path) @@ -282,9 +282,9 @@ fun avoid c path -> match kind_of_term c, path with let new_rank = if a = 1 then rank else rank+1 in let patt_list = if a = 1 then - [[cont_patt];[IntroIdentifier id2]] + [[zz,cont_patt];[zz,IntroIdentifier id2]] else - [[IntroIdentifier id2];[cont_patt]] in + [[zz,IntroIdentifier id2];[zz,cont_patt]] in (IntroOrAndPattern patt_list, avoid_names, id, c, path, new_rank, total_branches+1) | (_, path) -> let id = next_global_ident hyp_radix avoid in @@ -305,13 +305,13 @@ let (imply_intro3: pbp_rule) = function let intro_patt, avoid_names, id, c, p, rank, total_branches = or_and_tree_to_intro_pattern avoid prem path in if total_branches = 1 then - Some(chain_tactics [PbpIntros [intro_patt]] + Some(chain_tactics [PbpIntros [zz,intro_patt]] (f avoid_names clear_names clear_flag (Some id) (kind_of_term c) path)) else Some (PbpThens - ([PbpIntros [intro_patt]], + ([PbpIntros [zz,intro_patt]], auxiliary_goals clear_names clear_flag id (rank - 1) ((f avoid_names clear_names clear_flag (Some id) @@ -667,7 +667,7 @@ let rec cleanup_clears str_list = function let rec optim3_aux str_list = function (PbpGeneralize (h,l1)):: - (PbpIntros [IntroIdentifier s])::(PbpGeneralize (h',l2))::others + (PbpIntros [zz,IntroIdentifier s])::(PbpGeneralize (h',l2))::others when s=h' -> optim3_aux (s::str_list) (PbpGeneralize (h,l1@l2)::others) | (PbpTryClear names)::other -> diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml index 953fb5e7..4b9c1332 100644 --- a/contrib/interface/showproof.ml +++ b/contrib/interface/showproof.ml @@ -1197,12 +1197,12 @@ let rec natural_ntree ig ntree = | TacAssumption -> natural_trivial ig lh g gs ltree | TacClear _ -> natural_clear ig lh g gs ltree (* Besoin de l'argument de la tactique *) - | TacSimpleInduction (NamedHyp id) -> + | TacSimpleInductionDestruct (true,NamedHyp id) -> natural_induction ig lh g gs ge id ltree false | TacExtend (_,"InductionIntro",[a]) -> let id=(out_gen wit_ident a) in natural_induction ig lh g gs ge id ltree true - | TacApply (_,false,(c,_)) -> natural_apply ig lh g gs (snd c) ltree + | TacApply (_,false,[c,_]) -> natural_apply ig lh g gs (snd c) ltree | TacExact c -> natural_exact ig lh g gs (snd c) ltree | TacCut c -> natural_cut ig lh g gs (snd c) ltree | TacExtend (_,"CutIntro",[a]) -> diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 7d1f57fe..da4908e5 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -615,8 +615,7 @@ let get_flag r = (* Rem: EVAR flag obsolčte *) conv_flags, red_ids -let rec xlate_intro_pattern = - function +let rec xlate_intro_pattern (loc,pat) = match pat with | IntroOrAndPattern [] -> assert false | IntroOrAndPattern (fp::ll) -> CT_disj_pattern @@ -684,8 +683,8 @@ let xlate_one_unfold_block = function ;; let xlate_with_names = function - IntroAnonymous -> CT_coerce_ID_OPT_to_INTRO_PATT_OPT ctv_ID_OPT_NONE - | fp -> CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT (xlate_intro_pattern fp) + None -> CT_coerce_ID_OPT_to_INTRO_PATT_OPT ctv_ID_OPT_NONE + | Some fp -> CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT (xlate_intro_pattern fp) let rawwit_main_tactic = Pcoq.rawwit_tactic Pcoq.tactic_main_level @@ -829,11 +828,11 @@ and xlate_tactic = | [] -> assert false | fst::others -> CT_match_tac_rules(fst, others)) - | TacMatchContext (_,_,[]) | TacMatchContext (true,_,_) -> failwith "" - | TacMatchContext (false,false,rule1::rules) -> + | TacMatchGoal (_,_,[]) | TacMatchGoal (true,_,_) -> failwith "" + | TacMatchGoal (false,false,rule1::rules) -> CT_match_context(xlate_context_rule rule1, List.map xlate_context_rule rules) - | TacMatchContext (false,true,rule1::rules) -> + | TacMatchGoal (false,true,rule1::rules) -> CT_match_context_reverse(xlate_context_rule rule1, List.map xlate_context_rule rules) | TacLetIn (false, l, t) -> @@ -926,23 +925,26 @@ and xlate_tac = | TacExtend (_,"contradiction",[]) -> CT_contradiction | TacDoubleInduction (n1, n2) -> CT_tac_double (xlate_quantified_hypothesis n1, xlate_quantified_hypothesis n2) - | TacExtend (_,"discriminate", [idopt]) -> + | TacExtend (_,"discriminate", []) -> + CT_discriminate_eq (CT_coerce_ID_OPT_to_ID_OR_INT_OPT ctv_ID_OPT_NONE) + | TacExtend (_,"discriminate", [id]) -> CT_discriminate_eq (xlate_quantified_hypothesis_opt - (out_gen (wit_opt rawwit_quant_hyp) idopt)) - | TacExtend (_,"simplify_eq", [idopt]) -> - let idopt1 = out_gen (wit_opt rawwit_quant_hyp) idopt in - let idopt2 = match idopt1 with - None -> CT_coerce_ID_OPT_to_ID_OR_INT_OPT - (CT_coerce_NONE_to_ID_OPT CT_none) - | Some v -> - CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT - (xlate_quantified_hypothesis v) in - CT_simplify_eq idopt2 - | TacExtend (_,"injection", [idopt]) -> + (Some (out_gen rawwit_quant_hyp id))) + | TacExtend (_,"simplify_eq", []) -> + CT_simplify_eq (CT_coerce_ID_OPT_to_ID_OR_INT_OPT + (CT_coerce_NONE_to_ID_OPT CT_none)) + | TacExtend (_,"simplify_eq", [id]) -> + let id1 = out_gen rawwit_quant_hyp id in + let id2 = CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT + (xlate_quantified_hypothesis id1) in + CT_simplify_eq id2 + | TacExtend (_,"injection", []) -> + CT_injection_eq (CT_coerce_ID_OPT_to_ID_OR_INT_OPT ctv_ID_OPT_NONE) + | TacExtend (_,"injection", [id]) -> CT_injection_eq (xlate_quantified_hypothesis_opt - (out_gen (wit_opt rawwit_quant_hyp) idopt)) + (Some (out_gen rawwit_quant_hyp id))) | TacExtend (_,"injection_as", [idopt;ipat]) -> xlate_error "TODO: injection as" | TacFix (idopt, n) -> @@ -967,19 +969,22 @@ and xlate_tac = CT_intros_until (CT_coerce_ID_to_ID_OR_INT (xlate_ident id)) | TacIntrosUntil (AnonHyp n) -> CT_intros_until (CT_coerce_INT_to_ID_OR_INT (CT_int n)) - | TacIntroMove (Some id1, Some (_,id2)) -> - CT_intro_after(CT_coerce_ID_to_ID_OPT (xlate_ident id1),xlate_ident id2) - | TacIntroMove (None, Some (_,id2)) -> - CT_intro_after(CT_coerce_NONE_to_ID_OPT CT_none, xlate_ident id2) - | TacMove (true, id1, id2) -> + | TacIntroMove (Some id1, MoveAfter id2) -> + CT_intro_after(CT_coerce_ID_to_ID_OPT (xlate_ident id1),xlate_hyp id2) + | TacIntroMove (None, MoveAfter id2) -> + CT_intro_after(CT_coerce_NONE_to_ID_OPT CT_none, xlate_hyp id2) + | TacMove (true, id1, MoveAfter id2) -> CT_move_after(xlate_hyp id1, xlate_hyp id2) | TacMove (false, id1, id2) -> xlate_error "Non dep Move is only internal" + | TacMove _ -> xlate_error "TODO: move before, at top, at bottom" | TacIntroPattern patt_list -> CT_intros (CT_intro_patt_list (List.map xlate_intro_pattern patt_list)) - | TacIntroMove (Some id, None) -> + | TacIntroMove (Some id, MoveToEnd true) -> CT_intros (CT_intro_patt_list[CT_coerce_ID_to_INTRO_PATT(xlate_ident id)]) - | TacIntroMove (None, None) -> CT_intro (CT_coerce_NONE_to_ID_OPT CT_none) + | TacIntroMove (None, MoveToEnd true) -> + CT_intro (CT_coerce_NONE_to_ID_OPT CT_none) + | TacIntroMove _ -> xlate_error "TODO" | TacLeft (false,bindl) -> CT_left (xlate_bindings bindl) | TacRight (false,bindl) -> CT_right (xlate_bindings bindl) | TacSplit (false,false,bindl) -> CT_split (xlate_bindings bindl) @@ -1150,11 +1155,12 @@ and xlate_tac = xlate_error "TODO: trivial using" | TacReduce (red, l) -> CT_reduce (xlate_red_tactic red, xlate_clause l) - | TacApply (true,false,(c,bindl)) -> + | TacApply (true,false,[c,bindl]) -> CT_apply (xlate_formula c, xlate_bindings bindl) - | TacApply (true,true,(c,bindl)) -> + | TacApply (true,true,[c,bindl]) -> CT_eapply (xlate_formula c, xlate_bindings bindl) - | TacApply (false,_,_) -> xlate_error "TODO: simple (e)apply" + | TacApply (_,_,_) -> + xlate_error "TODO: simple (e)apply and iterated apply" | TacConstructor (false,n_or_meta, bindl) -> let n = match n_or_meta with AI n -> n | MetaId _ -> xlate_error "" in CT_constructor (CT_int n, xlate_bindings bindl) @@ -1178,10 +1184,12 @@ and xlate_tac = | TacCase (false,(c1,sl)) -> CT_casetac (xlate_formula c1, xlate_bindings sl) | TacElim (true,_,_) | TacCase (true,_) - | TacNewDestruct (true,_,_,_,_) | TacNewInduction (true,_,_,_,_) -> + | TacInductionDestruct (_,true,_) -> xlate_error "TODO: eelim, ecase, edestruct, einduction" - | TacSimpleInduction h -> CT_induction (xlate_quantified_hypothesis h) - | TacSimpleDestruct h -> CT_destruct (xlate_quantified_hypothesis h) + | TacSimpleInductionDestruct (true,h) -> + CT_induction (xlate_quantified_hypothesis h) + | TacSimpleInductionDestruct (false,h) -> + CT_destruct (xlate_quantified_hypothesis h) | TacCut c -> CT_cut (xlate_formula c) | TacLApply c -> CT_use (xlate_formula c) | TacDecompose ([],c) -> @@ -1222,19 +1230,16 @@ and xlate_tac = CT_dauto(xlate_int_or_var_opt_to_int_opt a, xlate_int_opt b) | TacDAuto (a, b, _) -> xlate_error "TODO: dauto using" - | TacNewDestruct(false,a,b,c,None) -> + | TacInductionDestruct(true,false,[a,b,(None,c),None]) -> CT_new_destruct (List.map xlate_int_or_constr a, xlate_using b, xlate_with_names c) - | TacNewInduction(false,a,b,c,None) -> + | TacInductionDestruct(false,false,[a,b,(None,c),None]) -> CT_new_induction (List.map xlate_int_or_constr a, xlate_using b, xlate_with_names c) - | TacNewDestruct(false,a,b,c,_) -> xlate_error "TODO: destruct in" - | TacNewInduction(false,a,b,c,_) ->xlate_error "TODO: induction in" - (*| TacInstantiate (a, b, cl) -> - CT_instantiate(CT_int a, xlate_formula b, - assert false) *) + | TacInductionDestruct(_,false,_) -> + xlate_error "TODO: clause 'in' and full 'as' of destruct/induction" | TacLetTac (na, c, cl, true) when cl = nowhere -> CT_pose(xlate_id_opt_aux na, xlate_formula c) | TacLetTac (na, c, cl, true) -> @@ -1243,13 +1248,13 @@ and xlate_tac = but the structures are different *) xlate_clause cl) | TacLetTac (na, c, cl, false) -> xlate_error "TODO: remember" - | TacAssert (None, IntroIdentifier id, c) -> + | TacAssert (None, (_,IntroIdentifier id), c) -> CT_assert(xlate_id_opt ((0,0),Name id), xlate_formula c) - | TacAssert (None, IntroAnonymous, c) -> + | TacAssert (None, (_,IntroAnonymous), c) -> CT_assert(xlate_id_opt ((0,0),Anonymous), xlate_formula c) - | TacAssert (Some (TacId []), IntroIdentifier id, c) -> + | TacAssert (Some (TacId []), (_,IntroIdentifier id), c) -> CT_truecut(xlate_id_opt ((0,0),Name id), xlate_formula c) - | TacAssert (Some (TacId []), IntroAnonymous, c) -> + | TacAssert (Some (TacId []), (_,IntroAnonymous), c) -> CT_truecut(xlate_id_opt ((0,0),Anonymous), xlate_formula c) | TacAssert _ -> xlate_error "TODO: assert with 'as' and 'by' and pose proof with 'as'" diff --git a/contrib/micromega/Micromegatac.v b/contrib/micromega/Psatz.v index 13c7eace..b2dd9910 100644 --- a/contrib/micromega/Micromegatac.v +++ b/contrib/micromega/Psatz.v @@ -23,57 +23,53 @@ Require Export RingMicromega. Require Import VarMap. Require Tauto. -Ltac micromegac dom d := +Ltac xpsatz dom d := let tac := lazymatch dom with | Z => - micromegap d ; + (sos_Z || psatz_Z d) ; intros __wit __varmap __ff ; change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity | R => - rmicromegap d ; + (sos_R || psatz_R d) ; intros __wit __varmap __ff ; change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity + | Q => + (sos_Q || psatz_Q d) ; + intros __wit __varmap __ff ; + change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; + apply (QTautoChecker_sound __ff __wit); vm_compute ; reflexivity | _ => fail "Unsupported domain" end in tac. -Tactic Notation "micromega" constr(dom) int_or_var(n) := micromegac dom n. -Tactic Notation "micromega" constr(dom) := micromegac dom ltac:-1. +Tactic Notation "psatz" constr(dom) int_or_var(n) := xpsatz dom n. +Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:-1. -Ltac zfarkas := omicronp ; - intros __wit __varmap __ff ; - change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; - apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity. - -Ltac omicron dom := +Ltac psatzl dom := let tac := lazymatch dom with | Z => - zomicronp ; + psatzl_Z ; intros __wit __varmap __ff ; change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity | Q => - qomicronp ; + psatzl_Q ; intros __wit __varmap __ff ; change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; apply (QTautoChecker_sound __ff __wit); vm_compute ; reflexivity | R => - romicronp ; + psatzl_R ; intros __wit __varmap __ff ; change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity | _ => fail "Unsupported domain" end in tac. -Ltac sos dom := - let tac := lazymatch dom with - | Z => - sosp ; - intros __wit __varmap __ff ; - change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; - apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity - | _ => fail "Unsupported domain" - end in tac. +Ltac lia := + xlia ; + intros __wit __varmap __ff ; + change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; + apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity. diff --git a/contrib/micromega/QMicromega.v b/contrib/micromega/QMicromega.v index 9e95f6c4..c054f218 100644 --- a/contrib/micromega/QMicromega.v +++ b/contrib/micromega/QMicromega.v @@ -16,38 +16,11 @@ Require Import OrderedRing. Require Import RingMicromega. Require Import Refl. Require Import QArith. -Require Import Qring. - -(* Qsrt has been removed from the library ? *) -Definition Qsrt : ring_theory 0 1 Qplus Qmult Qminus Qopp Qeq. -Proof. - constructor. - exact Qplus_0_l. - exact Qplus_comm. - exact Qplus_assoc. - exact Qmult_1_l. - exact Qmult_comm. - exact Qmult_assoc. - exact Qmult_plus_distr_l. - reflexivity. - exact Qplus_opp_r. -Qed. - - -Add Ring Qring : Qsrt. - -Lemma Qmult_neutral : forall x , 0 * x == 0. -Proof. - intros. - compute. - reflexivity. -Qed. - -(* Is there any qarith database ? *) +Require Import Qfield. Lemma Qsor : SOR 0 1 Qplus Qmult Qminus Qopp Qeq Qle Qlt. Proof. - constructor; intros ; subst ; try (intuition (subst; auto with qarith)). + constructor; intros ; subst ; try (intuition (subst; auto with qarith)). apply Q_Setoid. rewrite H ; rewrite H0 ; reflexivity. rewrite H ; rewrite H0 ; reflexivity. @@ -67,45 +40,12 @@ Proof. destruct(Q_dec n m) as [[H1 |H1] | H1 ] ; tauto. apply (Qplus_le_compat p p n m (Qle_refl p) H). generalize (Qmult_lt_compat_r 0 n m H0 H). - rewrite Qmult_neutral. + rewrite Qmult_0_l. auto. compute in H. discriminate. Qed. -Definition Qeq_bool (p q : Q) : bool := Zeq_bool (Qnum p * ' Qden q)%Z (Qnum q * ' Qden p)%Z. - -Definition Qle_bool (x y : Q) : bool := Zle_bool (Qnum x * ' Qden y)%Z (Qnum y * ' Qden x)%Z. - -Require ZMicromega. - -Lemma Qeq_bool_ok : forall x y, Qeq_bool x y = true -> x == y. -Proof. - intros. - unfold Qeq_bool in H. - unfold Qeq. - apply (Zeqb_ok _ _ H). -Qed. - - -Lemma Qeq_bool_neq : forall x y, Qeq_bool x y = false -> ~ x == y. -Proof. - unfold Qeq_bool,Qeq. - red ; intros ; subst. - rewrite H0 in H. - apply (ZMicromega.Zeq_bool_neq _ _ H). - reflexivity. -Qed. - -Lemma Qle_bool_imp_le : forall x y : Q, Qle_bool x y = true -> x <= y. -Proof. - unfold Qle_bool, Qle. - intros. - apply Zle_bool_imp_le ; auto. -Qed. - - - Lemma QSORaddon : SORaddon 0 1 Qplus Qmult Qminus Qopp Qeq Qle (* ring elements *) @@ -115,7 +55,7 @@ Lemma QSORaddon : Proof. constructor. constructor ; intros ; try reflexivity. - apply Qeq_bool_ok ; auto. + apply Qeq_bool_eq; auto. constructor. reflexivity. intros x y. @@ -173,9 +113,9 @@ match o with | OpEq => Qeq | OpNEq => fun x y => ~ x == y | OpLe => Qle -| OpGe => Qge +| OpGe => fun x y => Qle y x | OpLt => Qlt -| OpGt => Qgt +| OpGt => fun x y => Qlt y x end. Definition Qeval_formula (e:PolEnv Q) (ff : Formula Q) := diff --git a/contrib/micromega/RMicromega.v b/contrib/micromega/RMicromega.v index ef28db32..7c6969c2 100644 --- a/contrib/micromega/RMicromega.v +++ b/contrib/micromega/RMicromega.v @@ -76,12 +76,12 @@ Proof. apply mult_IZR. apply Ropp_Ropp_IZR. apply IZR_eq. - apply Zeqb_ok ; auto. + apply Zeq_bool_eq ; auto. apply R_power_theory. intros x y. intro. apply IZR_neq. - apply ZMicromega.Zeq_bool_neq ; auto. + apply Zeq_bool_neq ; auto. intros. apply IZR_le. apply Zle_bool_imp_le. auto. Qed. @@ -97,9 +97,34 @@ Definition INZ (n:N) : R := Definition Reval_expr := eval_pexpr Rplus Rmult Rminus Ropp IZR Nnat.nat_of_N pow. -Definition Reval_formula := +Definition Reval_op2 (o:Op2) : R -> R -> Prop := + match o with + | OpEq => @eq R + | OpNEq => fun x y => ~ x = y + | OpLe => Rle + | OpGe => Rge + | OpLt => Rlt + | OpGt => Rgt + end. + + +Definition Reval_formula (e: PolEnv R) (ff : Formula Z) := + let (lhs,o,rhs) := ff in Reval_op2 o (Reval_expr e lhs) (Reval_expr e rhs). + +Definition Reval_formula' := eval_formula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt IZR Nnat.nat_of_N pow. +Lemma Reval_formula_compat : forall env f, Reval_formula env f <-> Reval_formula' env f. +Proof. + intros. + unfold Reval_formula. + destruct f. + unfold Reval_formula'. + unfold Reval_expr. + split ; destruct Fop ; simpl ; auto. + apply Rge_le. + apply Rle_ge. +Qed. Definition Reval_nformula := eval_nformula 0 Rplus Rmult Rminus Ropp (@eq R) Rle Rlt IZR Nnat.nat_of_N pow. @@ -139,8 +164,9 @@ Proof. unfold RTautoChecker. apply (tauto_checker_sound Reval_formula Reval_nformula). apply Reval_nformula_dec. - intros. unfold Reval_formula. now apply (cnf_normalise_correct Rsor). - intros. unfold Reval_formula. now apply (cnf_negate_correct Rsor). + intros. rewrite Reval_formula_compat. + unfold Reval_formula'. now apply (cnf_normalise_correct Rsor). + intros. rewrite Reval_formula_compat. unfold Reval_formula. now apply (cnf_negate_correct Rsor). intros t w0. apply RWeakChecker_sound. Qed. diff --git a/contrib/micromega/ZMicromega.v b/contrib/micromega/ZMicromega.v index 94c83f73..0855925a 100644 --- a/contrib/micromega/ZMicromega.v +++ b/contrib/micromega/ZMicromega.v @@ -39,15 +39,6 @@ Proof. apply Zmult_lt_0_compat ; auto. Qed. -Lemma Zeq_bool_neq : forall x y, Zeq_bool x y = false -> x <> y. -Proof. - red ; intros. - subst. - unfold Zeq_bool in H. - rewrite Zcompare_refl in H. - discriminate. -Qed. - Lemma ZSORaddon : SORaddon 0 1 Zplus Zmult Zminus Zopp (@eq Z) Zle (* ring elements *) 0%Z 1%Z Zplus Zmult Zminus Zopp (* coefficients *) @@ -56,7 +47,7 @@ Lemma ZSORaddon : Proof. constructor. constructor ; intros ; try reflexivity. - apply Zeqb_ok ; auto. + apply Zeq_bool_eq ; auto. constructor. reflexivity. intros x y. diff --git a/contrib/micromega/certificate.ml b/contrib/micromega/certificate.ml index 88e882e6..f4efcd08 100644 --- a/contrib/micromega/certificate.ml +++ b/contrib/micromega/certificate.ml @@ -108,7 +108,7 @@ struct if compare_num v (Int 0) <> 0 then if Monomial.compare Monomial.const k = 0 - then Printf.fprintf o "%s " (string_of_num v) + then Printf.fprintf o "%s " (string_of_num v) else Printf.fprintf o "%s*%a " (string_of_num v) Monomial.pp k) p (* Get the coefficient of monomial mn *) @@ -304,8 +304,8 @@ let factorise_linear_cone c = (match pending with | None -> rebuild_cone l (Some e) | Some p -> (match factorise p e with - | None -> Mc.S_Add(p, rebuild_cone l (Some e)) - | Some f -> rebuild_cone l (Some f) ) + | None -> Mc.S_Add(p, rebuild_cone l (Some e)) + | Some f -> rebuild_cone l (Some f) ) ) in (rebuild_cone (List.sort Pervasives.compare (cone_list c [])) None) @@ -387,10 +387,10 @@ let build_linear_system l = (* I need at least something strictly positive *) let strict = { coeffs = Vect.from_list ((Big_int unit_big_int):: - (List.map (fun (x,y) -> - match y with Mc.Strict -> - Big_int unit_big_int - | _ -> Big_int zero_big_int) l)); + (List.map (fun (x,y) -> + match y with Mc.Strict -> + Big_int unit_big_int + | _ -> Big_int zero_big_int) l)); op = Ge ; cst = Big_int unit_big_int } in (* Add the positivity constraint *) {coeffs = Vect.from_list ([Big_int unit_big_int]) ; @@ -414,22 +414,22 @@ let make_certificate n_spec cert li = in let rec scalar_product cert l = match cert with - | [] -> Mc.S_Z - | c::cert -> match l with - | [] -> failwith "make_certificate(1)" - | i::l -> - let r = scalar_product cert l in - match compare_big_int c zero_big_int with - | -1 -> Mc.S_Add ( - Mc.S_Ideal (Mc.PEc ( bint_to_cst c), Mc.S_In (Ml2C.nat i)), - r) - | 0 -> r - | _ -> Mc.S_Add ( - Mc.S_Mult (Mc.S_Pos (bint_to_cst c), Mc.S_In (Ml2C.nat i)), - r) in + | [] -> Mc.S_Z + | c::cert -> match l with + | [] -> failwith "make_certificate(1)" + | i::l -> + let r = scalar_product cert l in + match compare_big_int c zero_big_int with + | -1 -> Mc.S_Add ( + Mc.S_Ideal (Mc.PEc ( bint_to_cst c), Mc.S_In (Ml2C.nat i)), + r) + | 0 -> r + | _ -> Mc.S_Add ( + Mc.S_Mult (Mc.S_Pos (bint_to_cst c), Mc.S_In (Ml2C.nat i)), + r) in Some ((factorise_linear_cone - (simplify_cone n_spec (Mc.S_Add (cst, scalar_product cert' li))))) + (simplify_cone n_spec (Mc.S_Add (cst, scalar_product cert' li))))) exception Found of Monomial.t @@ -444,7 +444,7 @@ let raw_certificate l = with x -> if debug then (Printf.printf "raw certificate %s" (Printexc.to_string x); - flush stdout) ; + flush stdout) ; None @@ -462,9 +462,9 @@ let linear_prover n_spec l = (fun (x,_) -> if snd' x = Mc.NonEqual then true else false) li in let l' = List.map (fun (c,i) -> let (Mc.Pair(x,y)) = c in - match y with - Mc.NonEqual -> failwith "cannot happen" - | y -> ((dev_form n_spec x, y),i)) l' in + match y with + Mc.NonEqual -> failwith "cannot happen" + | y -> ((dev_form n_spec x, y),i)) l' in simple_linear_prover n_spec l' @@ -513,106 +513,228 @@ let rec remove_assoc p x l = let eq x y = Vect.compare x y = 0 -(* Beurk... this code is a shame *) +let remove e l = List.fold_left (fun l x -> if eq x e then l else x::l) [] l -let rec zlinear_prover sys = xzlinear_prover [] sys -and xzlinear_prover enum l : (Mc.proofTerm option) = - match linear_prover z_spec l with - | Some prf -> Some (Mc.RatProof prf) - | None -> +(* The prover is (probably) incomplete -- + only searching for naive cutting planes *) + +let candidates sys = + let ll = List.fold_right ( + fun (Mc.Pair(e,k)) r -> + match k with + | Mc.NonStrict -> (dev_form z_spec e , Ge)::r + | Mc.Equal -> (dev_form z_spec e , Eq)::r + (* we already know the bound -- don't compute it again *) + | _ -> failwith "Cannot happen candidates") sys [] in + + let (sys,var_mn) = make_linear_system ll in + let vars = mapi (fun _ i -> Vect.set i (Int 1) Vect.null) var_mn in + (List.fold_left (fun l cstr -> + let gcd = Big_int (Vect.gcd cstr.coeffs) in + if gcd =/ (Int 1) && cstr.op = Eq + then l + else (Vect.mul (Int 1 // gcd) cstr.coeffs)::l) [] sys) @ vars + + +let rec xzlinear_prover planes sys = + match linear_prover z_spec sys with + | Some prf -> Some (Mc.RatProof prf) + | None -> (* find the candidate with the smallest range *) + (* Grrr - linear_prover is also calling 'make_linear_system' *) let ll = List.fold_right (fun (Mc.Pair(e,k)) r -> match k with Mc.NonEqual -> r | k -> (dev_form z_spec e , - match k with - | Mc.Strict | Mc.NonStrict -> Ge - (* Loss of precision -- weakness of fourier*) - | Mc.Equal -> Eq - | Mc.NonEqual -> failwith "Cannot happen") :: r) l [] in - - let (sys,var) = make_linear_system ll in - let res = - match Fourier.find_Q_interval sys with - | Some(i,x,j) -> if i =/ j - then Some(i,Vect.set x (Int 1) Vect.null,i) else None - | None -> None in - let res = match res with - | None -> - begin - let candidates = List.fold_right - (fun cstr acc -> - let gcd = Big_int (Vect.gcd cstr.coeffs) in - let vect = Vect.mul (Int 1 // gcd) cstr.coeffs in - if mem eq vect enum then acc - else ((vect,Fourier.optimise vect sys)::acc)) sys [] in - let candidates = List.fold_left (fun l (x,i) -> - match i with - None -> (x,Empty)::l - | Some i -> (x,i)::l) [] (candidates) in - match List.fold_left (fun (x1,i1) (x2,i2) -> - if smaller_itv i1 i2 - then (x1,i1) else (x2,i2)) (Vect.null,Itv(None,None)) candidates - with - | (i,Empty) -> None - | (x,Itv(Some i, Some j)) -> Some(i,x,j) - | (x,Point n) -> Some(n,x,n) - | x -> match Fourier.find_Q_interval sys with - | None -> None - | Some(i,x,j) -> - if i =/ j - then Some(i,Vect.set x (Int 1) Vect.null,i) - else None - end - | _ -> res in - - match res with + match k with + Mc.NonStrict -> Ge + | Mc.Equal -> Eq + | Mc.Strict | Mc.NonEqual -> failwith "Cannot happen") :: r) sys [] in + let (ll,var) = make_linear_system ll in + let candidates = List.fold_left (fun acc vect -> + match Fourier.optimise vect ll with + | None -> acc + | Some i -> +(* Printf.printf "%s in %s\n" (Vect.string vect) (string_of_intrvl i) ; *) + flush stdout ; + (vect,i) ::acc) [] planes in + + let smallest_interval = + match List.fold_left (fun (x1,i1) (x2,i2) -> + if smaller_itv i1 i2 + then (x1,i1) else (x2,i2)) (Vect.null,Itv(None,None)) candidates + with + | (x,Itv(Some i, Some j)) -> Some(i,x,j) + | (x,Point n) -> Some(n,x,n) + | x -> None (* This might be a cutting plane *) + in + match smallest_interval with | Some (lb,e,ub) -> - let (lbn,lbd) = - (Ml2C.bigint (sub_big_int (numerator lb) unit_big_int), - Ml2C.bigint (denominator lb)) in - let (ubn,ubd) = - (Ml2C.bigint (add_big_int unit_big_int (numerator ub)) , - Ml2C.bigint (denominator ub)) in - let expr = list_to_polynomial var (Vect.to_list e) in - (match - (*x <= ub -> x > ub *) - linear_prover z_spec - (Mc.Pair(pplus (pmult (pconst ubd) expr) (popp (pconst ubn)), - Mc.NonStrict) :: l), - (* lb <= x -> lb > x *) - linear_prover z_spec - (Mc.Pair( pplus (popp (pmult (pconst lbd) expr)) (pconst lbn) , - Mc.NonStrict)::l) - with - | Some cub , Some clb -> - (match zlinear_enum (e::enum) expr - (ceiling_num lb) (floor_num ub) l - with - | None -> None - | Some prf -> - Some (Mc.EnumProof(Ml2C.q lb,expr,Ml2C.q ub,clb,cub,prf))) - | _ -> None - ) + let (lbn,lbd) = + (Ml2C.bigint (sub_big_int (numerator lb) unit_big_int), + Ml2C.bigint (denominator lb)) in + let (ubn,ubd) = + (Ml2C.bigint (add_big_int unit_big_int (numerator ub)) , + Ml2C.bigint (denominator ub)) in + let expr = list_to_polynomial var (Vect.to_list e) in + (match + (*x <= ub -> x > ub *) + linear_prover z_spec + (Mc.Pair(pplus (pmult (pconst ubd) expr) (popp (pconst ubn)), + Mc.NonStrict) :: sys), + (* lb <= x -> lb > x *) + linear_prover z_spec + (Mc.Pair( pplus (popp (pmult (pconst lbd) expr)) (pconst lbn) , + Mc.NonStrict)::sys) + with + | Some cub , Some clb -> + (match zlinear_enum (remove e planes) expr + (ceiling_num lb) (floor_num ub) sys + with + | None -> None + | Some prf -> + Some (Mc.EnumProof(Ml2C.q lb,expr,Ml2C.q ub,clb,cub,prf))) + | _ -> None + ) | _ -> None -and xzlinear_enum enum expr clb cub l = +and zlinear_enum planes expr clb cub l = if clb >/ cub then Some Mc.Nil else let pexpr = pplus (popp (pconst (Ml2C.bigint (numerator clb)))) expr in let sys' = (Mc.Pair(pexpr, Mc.Equal))::l in - match xzlinear_prover enum sys' with + (*let enum = *) + match xzlinear_prover planes sys' with | None -> if debug then print_string "zlp?"; None | Some prf -> if debug then print_string "zlp!"; - match zlinear_enum enum expr (clb +/ (Int 1)) cub l with + match zlinear_enum planes expr (clb +/ (Int 1)) cub l with | None -> None | Some prfl -> Some (Mc.Cons(prf,prfl)) -and zlinear_enum enum expr clb cub l = - let res = xzlinear_enum enum expr clb cub l in - if debug then Printf.printf "zlinear_enum %s %s -> %s\n" - (string_of_num clb) - (string_of_num cub) - (match res with - | None -> "None" - | Some r -> "Some") ; res +let zlinear_prover sys = + let candidates = candidates sys in + (* Printf.printf "candidates %d" (List.length candidates) ; *) + xzlinear_prover candidates sys + +open Sos + +let rec scale_term t = + match t with + | Zero -> unit_big_int , Zero + | Const n -> (denominator n) , Const (Big_int (numerator n)) + | Var n -> unit_big_int , Var n + | Inv _ -> failwith "scale_term : not implemented" + | Opp t -> let s, t = scale_term t in s, Opp t + | Add(t1,t2) -> let s1,y1 = scale_term t1 and s2,y2 = scale_term t2 in + let g = gcd_big_int s1 s2 in + let s1' = div_big_int s1 g in + let s2' = div_big_int s2 g in + let e = mult_big_int g (mult_big_int s1' s2') in + if (compare_big_int e unit_big_int) = 0 + then (unit_big_int, Add (y1,y2)) + else e, Add (Mul(Const (Big_int s2'), y1), + Mul (Const (Big_int s1'), y2)) + | Sub _ -> failwith "scale term: not implemented" + | Mul(y,z) -> let s1,y1 = scale_term y and s2,y2 = scale_term z in + mult_big_int s1 s2 , Mul (y1, y2) + | Pow(t,n) -> let s,t = scale_term t in + power_big_int_positive_int s n , Pow(t,n) + | _ -> failwith "scale_term : not implemented" + +let scale_term t = + let (s,t') = scale_term t in + s,t' + + +let get_index_of_ith_match f i l = + let rec get j res l = + match l with + | [] -> failwith "bad index" + | e::l -> if f e + then + (if j = i then res else get (j+1) (res+1) l ) + else get j (res+1) l in + get 0 0 l + + +let rec scale_certificate pos = match pos with + | Axiom_eq i -> unit_big_int , Axiom_eq i + | Axiom_le i -> unit_big_int , Axiom_le i + | Axiom_lt i -> unit_big_int , Axiom_lt i + | Monoid l -> unit_big_int , Monoid l + | Rational_eq n -> (denominator n) , Rational_eq (Big_int (numerator n)) + | Rational_le n -> (denominator n) , Rational_le (Big_int (numerator n)) + | Rational_lt n -> (denominator n) , Rational_lt (Big_int (numerator n)) + | Square t -> let s,t' = scale_term t in + mult_big_int s s , Square t' + | Eqmul (t, y) -> let s1,y1 = scale_term t and s2,y2 = scale_certificate y in + mult_big_int s1 s2 , Eqmul (y1,y2) + | Sum (y, z) -> let s1,y1 = scale_certificate y + and s2,y2 = scale_certificate z in + let g = gcd_big_int s1 s2 in + let s1' = div_big_int s1 g in + let s2' = div_big_int s2 g in + mult_big_int g (mult_big_int s1' s2'), + Sum (Product(Rational_le (Big_int s2'), y1), + Product (Rational_le (Big_int s1'), y2)) + | Product (y, z) -> + let s1,y1 = scale_certificate y and s2,y2 = scale_certificate z in + mult_big_int s1 s2 , Product (y1,y2) + + +open Micromega + let rec term_to_q_expr = function + | Const n -> PEc (Ml2C.q n) + | Zero -> PEc ( Ml2C.q (Int 0)) + | Var s -> PEX (Ml2C.index + (int_of_string (String.sub s 1 (String.length s - 1)))) + | Mul(p1,p2) -> PEmul(term_to_q_expr p1, term_to_q_expr p2) + | Add(p1,p2) -> PEadd(term_to_q_expr p1, term_to_q_expr p2) + | Opp p -> PEopp (term_to_q_expr p) + | Pow(t,n) -> PEpow (term_to_q_expr t,Ml2C.n n) + | Sub(t1,t2) -> PEsub (term_to_q_expr t1, term_to_q_expr t2) + | _ -> failwith "term_to_q_expr: not implemented" + +let q_cert_of_pos pos = + let rec _cert_of_pos = function + Axiom_eq i -> Mc.S_In (Ml2C.nat i) + | Axiom_le i -> Mc.S_In (Ml2C.nat i) + | Axiom_lt i -> Mc.S_In (Ml2C.nat i) + | Monoid l -> Mc.S_Monoid (Ml2C.list Ml2C.nat l) + | Rational_eq n | Rational_le n | Rational_lt n -> + if compare_num n (Int 0) = 0 then Mc.S_Z else + Mc.S_Pos (Ml2C.q n) + | Square t -> Mc.S_Square (term_to_q_expr t) + | Eqmul (t, y) -> Mc.S_Ideal(term_to_q_expr t, _cert_of_pos y) + | Sum (y, z) -> Mc.S_Add (_cert_of_pos y, _cert_of_pos z) + | Product (y, z) -> Mc.S_Mult (_cert_of_pos y, _cert_of_pos z) in + simplify_cone q_spec (_cert_of_pos pos) + + + let rec term_to_z_expr = function + | Const n -> PEc (Ml2C.bigint (big_int_of_num n)) + | Zero -> PEc ( Z0) + | Var s -> PEX (Ml2C.index + (int_of_string (String.sub s 1 (String.length s - 1)))) + | Mul(p1,p2) -> PEmul(term_to_z_expr p1, term_to_z_expr p2) + | Add(p1,p2) -> PEadd(term_to_z_expr p1, term_to_z_expr p2) + | Opp p -> PEopp (term_to_z_expr p) + | Pow(t,n) -> PEpow (term_to_z_expr t,Ml2C.n n) + | Sub(t1,t2) -> PEsub (term_to_z_expr t1, term_to_z_expr t2) + | _ -> failwith "term_to_z_expr: not implemented" + +let z_cert_of_pos pos = + let s,pos = (scale_certificate pos) in + let rec _cert_of_pos = function + Axiom_eq i -> Mc.S_In (Ml2C.nat i) + | Axiom_le i -> Mc.S_In (Ml2C.nat i) + | Axiom_lt i -> Mc.S_In (Ml2C.nat i) + | Monoid l -> Mc.S_Monoid (Ml2C.list Ml2C.nat l) + | Rational_eq n | Rational_le n | Rational_lt n -> + if compare_num n (Int 0) = 0 then Mc.S_Z else + Mc.S_Pos (Ml2C.bigint (big_int_of_num n)) + | Square t -> Mc.S_Square (term_to_z_expr t) + | Eqmul (t, y) -> Mc.S_Ideal(term_to_z_expr t, _cert_of_pos y) + | Sum (y, z) -> Mc.S_Add (_cert_of_pos y, _cert_of_pos z) + | Product (y, z) -> Mc.S_Mult (_cert_of_pos y, _cert_of_pos z) in + simplify_cone z_spec (_cert_of_pos pos) diff --git a/contrib/micromega/coq_micromega.ml b/contrib/micromega/coq_micromega.ml index 29e2a183..02ff61a1 100644 --- a/contrib/micromega/coq_micromega.ml +++ b/contrib/micromega/coq_micromega.ml @@ -106,6 +106,7 @@ struct ["Coq" ; "micromega" ; "EnvRing"]; ["Coq";"QArith"; "QArith_base"]; ["Coq";"Reals" ; "Rdefinitions"]; + ["Coq";"Reals" ; "Rpow_def"]; ["LRing_normalise"]] let constant = gen_constant_in_modules "ZMicromega" coq_modules @@ -163,6 +164,9 @@ struct let coq_Qmake = lazy (constant "Qmake") + let coq_R0 = lazy (constant "R0") + let coq_R1 = lazy (constant "R1") + let coq_proofTerm = lazy (constant "ProofTerm") let coq_ratProof = lazy (constant "RatProof") @@ -179,10 +183,36 @@ struct let coq_Zminus = lazy (constant "Zminus") let coq_Zopp = lazy (constant "Zopp") let coq_Zmult = lazy (constant "Zmult") + let coq_Zpower = lazy (constant "Zpower") let coq_N_of_Z = lazy (gen_constant_in_modules "ZArithRing" [["Coq";"setoid_ring";"ZArithRing"]] "N_of_Z") + let coq_Qgt = lazy (constant "Qgt") + let coq_Qge = lazy (constant "Qge") + let coq_Qle = lazy (constant "Qle") + let coq_Qlt = lazy (constant "Qlt") + let coq_Qeq = lazy (constant "Qeq") + + + let coq_Qplus = lazy (constant "Qplus") + let coq_Qminus = lazy (constant "Qminus") + let coq_Qopp = lazy (constant "Qopp") + let coq_Qmult = lazy (constant "Qmult") + let coq_Qpower = lazy (constant "Qpower") + + + let coq_Rgt = lazy (constant "Rgt") + let coq_Rge = lazy (constant "Rge") + let coq_Rle = lazy (constant "Rle") + let coq_Rlt = lazy (constant "Rlt") + + let coq_Rplus = lazy (constant "Rplus") + let coq_Rminus = lazy (constant "Rminus") + let coq_Ropp = lazy (constant "Ropp") + let coq_Rmult = lazy (constant "Rmult") + let coq_Rpower = lazy (constant "pow") + let coq_PEX = lazy (constant "PEX" ) let coq_PEc = lazy (constant"PEc") @@ -225,6 +255,7 @@ struct (gen_constant_in_modules "RingMicromega" [["Coq" ; "micromega" ; "RingMicromega"] ; ["RingMicromega"] ] "Formula") + type parse_error = | Ukn | BadStr of string @@ -347,16 +378,11 @@ let dump_q q = let parse_q term = match Term.kind_of_term term with - | Term.App(c, args) -> - ( - match Term.kind_of_term c with - Term.Construct((n,j),i) -> - if Names.string_of_kn n = "Coq.QArith.QArith_base#<>#Q" - then {Mc.qnum = parse_z args.(0) ; Mc.qden = parse_positive args.(1) } + | Term.App(c, args) -> if c = Lazy.force coq_Qmake then + {Mc.qnum = parse_z args.(0) ; Mc.qden = parse_positive args.(1) } else raise ParseError - | _ -> raise ParseError - ) - | _ -> raise ParseError + | _ -> raise ParseError + let rec parse_list parse_elt term = let (i,c) = get_left_construct term in @@ -466,19 +492,6 @@ let parse_q term = pp_cone o e - - - let rec parse_op term = - let (i,c) = get_left_construct term in - match i with - | 1 -> Mc.OpEq - | 2 -> Mc.OpLe - | 3 -> Mc.OpGe - | 4 -> Mc.OpGt - | 5 -> Mc.OpLt - | i -> raise ParseError - - let rec dump_op = function | Mc.OpEq-> Lazy.force coq_OpEq | Mc.OpNEq-> Lazy.force coq_OpNEq @@ -510,68 +523,52 @@ let parse_q term = dump_op o ; dump_expr typ dump_constant e2|]) + let assoc_const x l = + try + snd (List.find (fun (x',y) -> x = Lazy.force x') l) + with + Not_found -> raise ParseError + + let zop_table = [ + coq_Zgt, Mc.OpGt ; + coq_Zge, Mc.OpGe ; + coq_Zlt, Mc.OpLt ; + coq_Zle, Mc.OpLe ] + + let rop_table = [ + coq_Rgt, Mc.OpGt ; + coq_Rge, Mc.OpGe ; + coq_Rlt, Mc.OpLt ; + coq_Rle, Mc.OpLe ] + + let qop_table = [ + coq_Qlt, Mc.OpLt ; + coq_Qle, Mc.OpLe ; + coq_Qeq, Mc.OpEq + ] let parse_zop (op,args) = match kind_of_term op with - | Const x -> - (match Names.string_of_con x with - | "Coq.ZArith.BinInt#<>#Zgt" -> (Mc.OpGt, args.(0), args.(1)) - | "Coq.ZArith.BinInt#<>#Zge" -> (Mc.OpGe, args.(0), args.(1)) - | "Coq.ZArith.BinInt#<>#Zlt" -> (Mc.OpLt, args.(0), args.(1)) - | "Coq.ZArith.BinInt#<>#Zle" -> (Mc.OpLe, args.(0), args.(1)) - (*| "Coq.Init.Logic#<>#not" -> Mc.OpNEq (* for backward compat *)*) - | s -> raise ParseError - ) + | Const x -> (assoc_const op zop_table, args.(0) , args.(1)) | Ind(n,0) -> - (match Names.string_of_kn n with - | "Coq.Init.Logic#<>#eq" -> - if args.(0) <> Lazy.force coq_Z - then raise ParseError - else (Mc.OpEq, args.(1), args.(2)) - | _ -> raise ParseError) + if op = Lazy.force coq_Eq && args.(0) = Lazy.force coq_Z + then (Mc.OpEq, args.(1), args.(2)) + else raise ParseError | _ -> failwith "parse_zop" let parse_rop (op,args) = - try match kind_of_term op with - | Const x -> - (match Names.string_of_con x with - | "Coq.Reals.Rdefinitions#<>#Rgt" -> (Mc.OpGt, args.(0), args.(1)) - | "Coq.Reals.Rdefinitions#<>#Rge" -> (Mc.OpGe, args.(0), args.(1)) - | "Coq.Reals.Rdefinitions#<>#Rlt" -> (Mc.OpLt, args.(0), args.(1)) - | "Coq.Reals.Rdefinitions#<>#Rle" -> (Mc.OpLe, args.(0), args.(1)) - (*| "Coq.Init.Logic#<>#not"-> Mc.OpNEq (* for backward compat *)*) - | s -> raise ParseError - ) + | Const x -> (assoc_const op rop_table, args.(0) , args.(1)) | Ind(n,0) -> - (match Names.string_of_kn n with - | "Coq.Init.Logic#<>#eq" -> - (* if args.(0) <> Lazy.force coq_R - then raise ParseError - else*) (Mc.OpEq, args.(1), args.(2)) - | _ -> raise ParseError) - | _ -> failwith "parse_rop" - with x -> - (Pp.pp (Pp.str "parse_rop failure ") ; - Pp.pp (Printer.prterm op) ; Pp.pp_flush ()) - ; raise x - + if op = Lazy.force coq_Eq && args.(0) = Lazy.force coq_R + then (Mc.OpEq, args.(1), args.(2)) + else raise ParseError + | _ -> failwith "parse_zop" let parse_qop (op,args) = - ( - (match kind_of_term op with - | Const x -> - (match Names.string_of_con x with - | "Coq.QArith.QArith_base#<>#Qgt" -> Mc.OpGt - | "Coq.QArith.QArith_base#<>#Qge" -> Mc.OpGe - | "Coq.QArith.QArith_base#<>#Qlt" -> Mc.OpLt - | "Coq.QArith.QArith_base#<>#Qle" -> Mc.OpLe - | "Coq.QArith.QArith_base#<>#Qeq" -> Mc.OpEq - | s -> raise ParseError - ) - | _ -> failwith "parse_zop") , args.(0) , args.(1)) + (assoc_const op qop_table, args.(0) , args.(1)) module Env = @@ -612,6 +609,14 @@ let parse_q term = | Ukn of string + let assoc_ops x l = + try + snd (List.find (fun (x',y) -> x = Lazy.force x') l) + with + Not_found -> Ukn "Oups" + + + let parse_expr parse_constant parse_exp ops_spec env term = if debug then (Pp.pp (Pp.str "parse_expr: "); @@ -634,7 +639,7 @@ let parse_q term = ( match kind_of_term t with | Const c -> - ( match ops_spec (Names.string_of_con c) with + ( match assoc_ops t ops_spec with | Binop f -> combine env f (args.(0),args.(1)) | Opp -> let (expr,env) = parse_expr env args.(0) in (Mc.PEopp expr, env) @@ -653,29 +658,29 @@ let parse_q term = parse_expr env term -let zop_spec = function - | "Coq.ZArith.BinInt#<>#Zplus" -> Binop (fun x y -> Mc.PEadd(x,y)) - | "Coq.ZArith.BinInt#<>#Zminus" -> Binop (fun x y -> Mc.PEsub(x,y)) - | "Coq.ZArith.BinInt#<>#Zmult" -> Binop (fun x y -> Mc.PEmul (x,y)) - | "Coq.ZArith.BinInt#<>#Zopp" -> Opp - | "Coq.ZArith.Zpow_def#<>#Zpower" -> Power - | s -> Ukn s + let zop_spec = + [ + coq_Zplus , Binop (fun x y -> Mc.PEadd(x,y)) ; + coq_Zminus , Binop (fun x y -> Mc.PEsub(x,y)) ; + coq_Zmult , Binop (fun x y -> Mc.PEmul (x,y)) ; + coq_Zopp , Opp ; + coq_Zpower , Power] -let qop_spec = function - | "Coq.QArith.QArith_base#<>#Qplus" -> Binop (fun x y -> Mc.PEadd(x,y)) - | "Coq.QArith.QArith_base#<>#Qminus" -> Binop (fun x y -> Mc.PEsub(x,y)) - | "Coq.QArith.QArith_base#<>#Qmult" -> Binop (fun x y -> Mc.PEmul (x,y)) - | "Coq.QArith.QArith_base#<>#Qopp" -> Opp - | "Coq.QArith.QArith_base#<>#Qpower" -> Power - | s -> Ukn s +let qop_spec = + [ + coq_Qplus , Binop (fun x y -> Mc.PEadd(x,y)) ; + coq_Qminus , Binop (fun x y -> Mc.PEsub(x,y)) ; + coq_Qmult , Binop (fun x y -> Mc.PEmul (x,y)) ; + coq_Qopp , Opp ; + coq_Qpower , Power] -let rop_spec = function - | "Coq.Reals.Rdefinitions#<>#Rplus" -> Binop (fun x y -> Mc.PEadd(x,y)) - | "Coq.Reals.Rdefinitions#<>#Rminus" -> Binop (fun x y -> Mc.PEsub(x,y)) - | "Coq.Reals.Rdefinitions#<>#Rmult" -> Binop (fun x y -> Mc.PEmul (x,y)) - | "Coq.Reals.Rdefinitions#<>#Ropp" -> Opp - | "Coq.Reals.Rpow_def#<>#pow" -> Power - | s -> Ukn s +let rop_spec = + [ + coq_Rplus , Binop (fun x y -> Mc.PEadd(x,y)) ; + coq_Rminus , Binop (fun x y -> Mc.PEsub(x,y)) ; + coq_Rmult , Binop (fun x y -> Mc.PEmul (x,y)) ; + coq_Ropp , Opp ; + coq_Rpower , Power] @@ -691,12 +696,12 @@ let rconstant term = Pp.pp (Pp.str "rconstant: "); Pp.pp (Printer.prterm term); Pp.pp_flush ()); match Term.kind_of_term term with - | Const x -> - (match Names.string_of_con x with - | "Coq.Reals.Rdefinitions#<>#R0" -> Mc.Z0 - | "Coq.Reals.Rdefinitions#<>#R1" -> Mc.Zpos Mc.XH - | _ -> raise ParseError - ) + | Const x -> + if term = Lazy.force coq_R0 + then Mc.Z0 + else if term = Lazy.force coq_R1 + then Mc.Zpos Mc.XH + else raise ParseError | _ -> raise ParseError @@ -731,23 +736,6 @@ let parse_rexpr = (* generic parsing of arithmetic expressions *) - let rec parse_conj parse_arith env term = - match kind_of_term term with - | App(l,rst) -> - (match kind_of_term l with - | Ind (n,_) -> - ( match Names.string_of_kn n with - | "Coq.Init.Logic#<>#and" -> - let (e1,env) = parse_arith env rst.(0) in - let (e2,env) = parse_conj parse_arith env rst.(1) in - (Mc.Cons(e1,e2),env) - | _ -> (* This might be an equality *) - let (e,env) = parse_arith env term in - (Mc.Cons(e,Mc.Nil),env)) - | _ -> (* This is an arithmetic expression *) - let (e,env) = parse_arith env term in - (Mc.Cons(e,Mc.Nil),env)) - | _ -> failwith "parse_conj(2)" @@ -850,46 +838,6 @@ let parse_rexpr = xdump f - (* Backward compat *) - - let rec parse_concl parse_arith env term = - match kind_of_term term with - | Prod(_,expr,rst) -> (* a -> b *) - let (lhs,rhs,env) = parse_concl parse_arith env rst in - let (e,env) = parse_arith env expr in - (Mc.Cons(e,lhs),rhs,env) - | App(_,_) -> - let (conj, env) = parse_conj parse_arith env term in - (Mc.Nil,conj,env) - | Ind(n,_) -> - (match (Names.string_of_kn n) with - | "Coq.Init.Logic#<>#False" -> (Mc.Nil,Mc.Nil,env) - | s -> - print_string s ; flush stdout; - failwith "parse_concl") - | _ -> failwith "parse_concl" - - - let rec parse_hyps parse_arith env goal_hyps hyps = - match hyps with - | [] -> ([],goal_hyps,env) - | (i,t)::l -> - let (li,lt,env) = parse_hyps parse_arith env goal_hyps l in - try - let (c,env) = parse_arith env t in - (i::li, Mc.Cons(c,lt), env) - with x -> - (*(if debug then Printf.printf "parse_arith : %s\n" x);*) - (li,lt,env) - - - let parse_goal parse_arith env hyps term = - try - let (lhs,rhs,env) = parse_concl parse_arith env term in - let (li,lt,env) = parse_hyps parse_arith env lhs hyps in - (li,lt,rhs,env) - with Failure x -> raise ParseError - (* backward compat *) (* ! reverse the list of bindings *) @@ -1235,8 +1183,8 @@ let lift_ratproof prover l = | Some c -> Some (Mc.RatProof c) -type csdpcert = Certificate.Mc.z Certificate.Mc.coneMember option -type micromega_polys = (Micromega.z Mc.pExpr, Mc.op1) Micromega.prod list +type csdpcert = Sos.positivstellensatz option +type micromega_polys = (Micromega.q Mc.pExpr, Mc.op1) Micromega.prod list type provername = string * int option let call_csdpcert provername poly = @@ -1255,36 +1203,84 @@ let call_csdpcert provername poly = close_in ch_from; Sys.remove tmp_from; cert -let omicron gl = +let rec z_to_q_expr e = + match e with + | Mc.PEc z -> Mc.PEc {Mc.qnum = z ; Mc.qden = Mc.XH} + | Mc.PEX x -> Mc.PEX x + | Mc.PEadd(e1,e2) -> Mc.PEadd(z_to_q_expr e1, z_to_q_expr e2) + | Mc.PEsub(e1,e2) -> Mc.PEsub(z_to_q_expr e1, z_to_q_expr e2) + | Mc.PEmul(e1,e2) -> Mc.PEmul(z_to_q_expr e1, z_to_q_expr e2) + | Mc.PEopp(e) -> Mc.PEopp(z_to_q_expr e) + | Mc.PEpow(e,n) -> Mc.PEpow(z_to_q_expr e,n) + + +let call_csdpcert_q provername poly = + match call_csdpcert provername poly with + | None -> None + | Some cert -> + let cert = Certificate.q_cert_of_pos cert in + match Mc.qWeakChecker (CamlToCoq.list (fun x -> x) poly) cert with + | Mc.True -> Some cert + | Mc.False -> (print_string "buggy certificate" ; flush stdout) ;None + + +let call_csdpcert_z provername poly = + let l = List.map (fun (Mc.Pair(e,o)) -> (Mc.Pair(z_to_q_expr e,o))) poly in + match call_csdpcert provername l with + | None -> None + | Some cert -> + let cert = Certificate.z_cert_of_pos cert in + match Mc.zWeakChecker (CamlToCoq.list (fun x -> x) poly) cert with + | Mc.True -> Some cert + | Mc.False -> (print_string "buggy certificate" ; flush stdout) ;None + + + + +let psatzl_Z gl = micromega_gen parse_zarith Mc.negate Mc.normalise zz_domain_spec [lift_ratproof (Certificate.linear_prover Certificate.z_spec), "fourier refutation" ] gl -let qomicron gl = +let psatzl_Q gl = micromega_gen parse_qarith Mc.cnf_negate Mc.cnf_normalise qq_domain_spec [ Certificate.linear_prover Certificate.q_spec, "fourier refutation" ] gl -let romicron gl = +let psatz_Q i gl = + micromega_gen parse_qarith Mc.cnf_negate Mc.cnf_normalise qq_domain_spec + [ call_csdpcert_q ("real_nonlinear_prover", Some i), "fourier refutation" ] gl + +let psatzl_R gl = micromega_gen parse_rarith Mc.cnf_negate Mc.cnf_normalise rz_domain_spec [ Certificate.linear_prover Certificate.z_spec, "fourier refutation" ] gl -let rmicromega i gl = - micromega_gen parse_rarith Mc.negate Mc.normalise rz_domain_spec - [ call_csdpcert ("real_nonlinear_prover", Some i), "fourier refutation" ] gl +let psatz_R i gl = + micromega_gen parse_rarith Mc.cnf_negate Mc.cnf_normalise rz_domain_spec + [ call_csdpcert_z ("real_nonlinear_prover", Some i), "fourier refutation" ] gl -let micromega i gl = +let psatz_Z i gl = micromega_gen parse_zarith Mc.negate Mc.normalise zz_domain_spec - [lift_ratproof (call_csdpcert ("real_nonlinear_prover",Some i)), + [lift_ratproof (call_csdpcert_z ("real_nonlinear_prover",Some i)), "fourier refutation" ] gl -let sos gl = +let sos_Z gl = micromega_gen parse_zarith Mc.negate Mc.normalise zz_domain_spec - [lift_ratproof (call_csdpcert ("pure_sos", None)), "pure sos refutation"] gl + [lift_ratproof (call_csdpcert_z ("pure_sos", None)), "pure sos refutation"] gl + +let sos_Q gl = + micromega_gen parse_qarith Mc.cnf_negate Mc.cnf_normalise qq_domain_spec + [call_csdpcert_q ("pure_sos", None), "pure sos refutation"] gl + +let sos_R gl = + micromega_gen parse_rarith Mc.cnf_negate Mc.cnf_normalise rz_domain_spec + [call_csdpcert_z ("pure_sos", None), "pure sos refutation"] gl + + -let zomicron gl = +let xlia gl = micromega_gen parse_zarith Mc.negate Mc.normalise zz_domain_spec [Certificate.zlinear_prover, "zprover"] gl diff --git a/contrib/micromega/csdpcert.ml b/contrib/micromega/csdpcert.ml index cfaf6ae1..e451a38f 100644 --- a/contrib/micromega/csdpcert.ml +++ b/contrib/micromega/csdpcert.ml @@ -27,7 +27,7 @@ struct open Mc let rec expr_to_term = function - | PEc z -> Const (Big_int (C2Ml.z_big_int z)) + | PEc z -> Const (C2Ml.q_to_num z) | PEX v -> Var ("x"^(string_of_int (C2Ml.index v))) | PEmul(p1,p2) -> let p1 = expr_to_term p1 in @@ -40,25 +40,15 @@ struct | PEopp p -> Opp (expr_to_term p) - let rec term_to_expr = function - | Const n -> PEc (Ml2C.bigint (big_int_of_num n)) - | Zero -> PEc ( Z0) - | Var s -> PEX (Ml2C.index - (int_of_string (String.sub s 1 (String.length s - 1)))) - | Mul(p1,p2) -> PEmul(term_to_expr p1, term_to_expr p2) - | Add(p1,p2) -> PEadd(term_to_expr p1, term_to_expr p2) - | Opp p -> PEopp (term_to_expr p) - | Pow(t,n) -> PEpow (term_to_expr t,Ml2C.n n) - | Sub(t1,t2) -> PEsub (term_to_expr t1, term_to_expr t2) - | _ -> failwith "term_to_expr: not implemented" - - let term_to_expr e = + + +(* let term_to_expr e = let e' = term_to_expr e in if debug then Printf.printf "term_to_expr : %s - %s\n" (string_of_poly (poly_of_term e)) (string_of_poly (poly_of_term (expr_to_term e'))); - e' + e' *) end open M @@ -66,110 +56,8 @@ open M open List open Mutils -let rec scale_term t = - match t with - | Zero -> unit_big_int , Zero - | Const n -> (denominator n) , Const (Big_int (numerator n)) - | Var n -> unit_big_int , Var n - | Inv _ -> failwith "scale_term : not implemented" - | Opp t -> let s, t = scale_term t in s, Opp t - | Add(t1,t2) -> let s1,y1 = scale_term t1 and s2,y2 = scale_term t2 in - let g = gcd_big_int s1 s2 in - let s1' = div_big_int s1 g in - let s2' = div_big_int s2 g in - let e = mult_big_int g (mult_big_int s1' s2') in - if (compare_big_int e unit_big_int) = 0 - then (unit_big_int, Add (y1,y2)) - else e, Add (Mul(Const (Big_int s2'), y1), - Mul (Const (Big_int s1'), y2)) - | Sub _ -> failwith "scale term: not implemented" - | Mul(y,z) -> let s1,y1 = scale_term y and s2,y2 = scale_term z in - mult_big_int s1 s2 , Mul (y1, y2) - | Pow(t,n) -> let s,t = scale_term t in - power_big_int_positive_int s n , Pow(t,n) - | _ -> failwith "scale_term : not implemented" - -let scale_term t = - let (s,t') = scale_term t in - s,t' - - -let rec scale_certificate pos = match pos with - | Axiom_eq i -> unit_big_int , Axiom_eq i - | Axiom_le i -> unit_big_int , Axiom_le i - | Axiom_lt i -> unit_big_int , Axiom_lt i - | Monoid l -> unit_big_int , Monoid l - | Rational_eq n -> (denominator n) , Rational_eq (Big_int (numerator n)) - | Rational_le n -> (denominator n) , Rational_le (Big_int (numerator n)) - | Rational_lt n -> (denominator n) , Rational_lt (Big_int (numerator n)) - | Square t -> let s,t' = scale_term t in - mult_big_int s s , Square t' - | Eqmul (t, y) -> let s1,y1 = scale_term t and s2,y2 = scale_certificate y in - mult_big_int s1 s2 , Eqmul (y1,y2) - | Sum (y, z) -> let s1,y1 = scale_certificate y - and s2,y2 = scale_certificate z in - let g = gcd_big_int s1 s2 in - let s1' = div_big_int s1 g in - let s2' = div_big_int s2 g in - mult_big_int g (mult_big_int s1' s2'), - Sum (Product(Rational_le (Big_int s2'), y1), - Product (Rational_le (Big_int s1'), y2)) - | Product (y, z) -> - let s1,y1 = scale_certificate y and s2,y2 = scale_certificate z in - mult_big_int s1 s2 , Product (y1,y2) - - -let is_eq = function Mc.Equal -> true | _ -> false -let is_le = function Mc.NonStrict -> true | _ -> false -let is_lt = function Mc.Strict -> true | _ -> false - -let get_index_of_ith_match f i l = - let rec get j res l = - match l with - | [] -> failwith "bad index" - | e::l -> if f e - then - (if j = i then res else get (j+1) (res+1) l ) - else get j (res+1) l in - get 0 0 l - - -let cert_of_pos eq le lt ll l pos = - let s,pos = (scale_certificate pos) in - let rec _cert_of_pos = function - Axiom_eq i -> let idx = get_index_of_ith_match is_eq i l in - Mc.S_In (Ml2C.nat idx) - | Axiom_le i -> let idx = get_index_of_ith_match is_le i l in - Mc.S_In (Ml2C.nat idx) - | Axiom_lt i -> let idx = get_index_of_ith_match is_lt i l in - Mc.S_In (Ml2C.nat idx) - | Monoid l -> Mc.S_Monoid (Ml2C.list Ml2C.nat l) - | Rational_eq n | Rational_le n | Rational_lt n -> - if compare_num n (Int 0) = 0 then Mc.S_Z else - Mc.S_Pos (Ml2C.bigint (big_int_of_num n)) - | Square t -> Mc.S_Square (term_to_expr t) - | Eqmul (t, y) -> Mc.S_Ideal(term_to_expr t, _cert_of_pos y) - | Sum (y, z) -> Mc.S_Add (_cert_of_pos y, _cert_of_pos z) - | Product (y, z) -> Mc.S_Mult (_cert_of_pos y, _cert_of_pos z) in - s, Certificate.simplify_cone Certificate.z_spec (_cert_of_pos pos) - - -let term_of_cert l pos = - let l = List.map fst' l in - let rec _cert_of_pos = function - | Mc.S_In i -> expr_to_term (List.nth l (C2Ml.nat i)) - | Mc.S_Pos p -> Const (C2Ml.num p) - | Mc.S_Z -> Const (Int 0) - | Mc.S_Square t -> Mul(expr_to_term t, expr_to_term t) - | Mc.S_Monoid m -> List.fold_right - (fun x m -> Mul (expr_to_term (List.nth l (C2Ml.nat x)),m)) - (C2Ml.list (fun x -> x) m) (Const (Int 1)) - | Mc.S_Ideal (t, y) -> Mul(expr_to_term t, _cert_of_pos y) - | Mc.S_Add (y, z) -> Add (_cert_of_pos y, _cert_of_pos z) - | Mc.S_Mult (y, z) -> Mul (_cert_of_pos y, _cert_of_pos z) in - (_cert_of_pos pos) let rec canonical_sum_to_string = function s -> failwith "not implemented" @@ -208,22 +96,6 @@ let rec sets_of_list l = | e::l -> let s = sets_of_list l in s@(List.map (fun s0 -> e::s0) s) -let cert_of_pos pos = - let s,pos = (scale_certificate pos) in - let rec _cert_of_pos = function - Axiom_eq i -> Mc.S_In (Ml2C.nat i) - | Axiom_le i -> Mc.S_In (Ml2C.nat i) - | Axiom_lt i -> Mc.S_In (Ml2C.nat i) - | Monoid l -> Mc.S_Monoid (Ml2C.list Ml2C.nat l) - | Rational_eq n | Rational_le n | Rational_lt n -> - if compare_num n (Int 0) = 0 then Mc.S_Z else - Mc.S_Pos (Ml2C.bigint (big_int_of_num n)) - | Square t -> Mc.S_Square (term_to_expr t) - | Eqmul (t, y) -> Mc.S_Ideal(term_to_expr t, _cert_of_pos y) - | Sum (y, z) -> Mc.S_Add (_cert_of_pos y, _cert_of_pos z) - | Product (y, z) -> Mc.S_Mult (_cert_of_pos y, _cert_of_pos z) in - s, Certificate.simplify_cone Certificate.z_spec (_cert_of_pos pos) - (* The exploration is probably not complete - for simple cases, it works... *) let real_nonlinear_prover d l = try @@ -272,15 +144,7 @@ let real_nonlinear_prover d l = let proof = list_fold_right_elements (fun s t -> Sum(s,t)) (proof_ne :: proofs_ideal @ proofs_cone) in - - let s,proof' = scale_certificate proof in - let cert = snd (cert_of_pos proof') in - if debug - then Printf.printf "cert poly : %s\n" - (string_of_poly (poly_of_term (term_of_cert l cert))); - match Mc.zWeakChecker (Ml2C.list (fun x -> x) l) cert with - | Mc.True -> Some cert - | Mc.False -> (print_string "buggy certificate" ; flush stdout) ;None + Some proof with | Sos.TooDeep -> None @@ -300,16 +164,16 @@ let pure_sos l = (term_of_poly p)), rst)) polys (Rational_lt (Int 0))) in let proof = Sum(Axiom_lt i, pos) in - let s,proof' = scale_certificate proof in - let cert = snd (cert_of_pos proof') in - Some cert +(* let s,proof' = scale_certificate proof in + let cert = snd (cert_of_pos proof') in *) + Some proof with | Not_found -> (* This is no strict inequality *) None | x -> None -type micromega_polys = (Micromega.z Mc.pExpr, Mc.op1) Micromega.prod list -type csdp_certificate = Certificate.Mc.z Certificate.Mc.coneMember option +type micromega_polys = (Micromega.q Mc.pExpr, Mc.op1) Micromega.prod list +type csdp_certificate = Sos.positivstellensatz option type provername = string * int option let main () = diff --git a/contrib/micromega/g_micromega.ml4 b/contrib/micromega/g_micromega.ml4 index 259b5d4b..50024e78 100644 --- a/contrib/micromega/g_micromega.ml4 +++ b/contrib/micromega/g_micromega.ml4 @@ -14,7 +14,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: g_micromega.ml4 10947 2008-05-19 19:10:40Z herbelin $ *) +(* $Id: g_micromega.ml4 11306 2008-08-05 16:51:08Z notin $ *) open Quote open Ring @@ -26,34 +26,49 @@ let out_arg = function | ArgVar _ -> anomaly "Unevaluated or_var variable" | ArgArg x -> x -TACTIC EXTEND Micromega -| [ "micromegap" int_or_var(i) ] -> [ Coq_micromega.micromega (out_arg i) ] -| [ "micromegap" ] -> [ Coq_micromega.micromega (-1) ] +TACTIC EXTEND PsatzZ +| [ "psatz_Z" int_or_var(i) ] -> [ Coq_micromega.psatz_Z (out_arg i) ] +| [ "psatz_Z" ] -> [ Coq_micromega.psatz_Z (-1) ] END -TACTIC EXTEND Sos -[ "sosp" ] -> [ Coq_micromega.sos] +TACTIC EXTEND Sos_Z +| [ "sos_Z" ] -> [ Coq_micromega.sos_Z] + END + +TACTIC EXTEND Sos_Q +| [ "sos_Q" ] -> [ Coq_micromega.sos_Q] + END + +TACTIC EXTEND Sos_R +| [ "sos_R" ] -> [ Coq_micromega.sos_R] END TACTIC EXTEND Omicron -[ "omicronp" ] -> [ Coq_micromega.omicron] +[ "psatzl_Z" ] -> [ Coq_micromega.psatzl_Z] END TACTIC EXTEND QOmicron -[ "qomicronp" ] -> [ Coq_micromega.qomicron] +[ "psatzl_Q" ] -> [ Coq_micromega.psatzl_Q] END TACTIC EXTEND ZOmicron -[ "zomicronp" ] -> [ Coq_micromega.zomicron] +[ "xlia" ] -> [ Coq_micromega.xlia] END TACTIC EXTEND ROmicron -[ "romicronp" ] -> [ Coq_micromega.romicron] +[ "psatzl_R" ] -> [ Coq_micromega.psatzl_R] END TACTIC EXTEND RMicromega -| [ "rmicromegap" int_or_var(i) ] -> [ Coq_micromega.rmicromega (out_arg i) ] -| [ "rmicromegap" ] -> [ Coq_micromega.rmicromega (-1) ] +| [ "psatz_R" int_or_var(i) ] -> [ Coq_micromega.psatz_R (out_arg i) ] +| [ "psatz_R" ] -> [ Coq_micromega.psatz_R (-1) ] +END + + +TACTIC EXTEND QMicromega +| [ "psatz_Q" int_or_var(i) ] -> [ Coq_micromega.psatz_Q (out_arg i) ] +| [ "psatz_Q" ] -> [ Coq_micromega.psatz_Q (-1) ] END + diff --git a/contrib/romega/ROmega.v b/contrib/romega/ROmega.v index 68bc43bb..4281cc57 100644 --- a/contrib/romega/ROmega.v +++ b/contrib/romega/ROmega.v @@ -9,3 +9,4 @@ Require Import ReflOmegaCore. Require Export Setoid. Require Export PreOmega. +Require Export ZArith_base. diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v index 9d379548..12176d66 100644 --- a/contrib/romega/ReflOmegaCore.v +++ b/contrib/romega/ReflOmegaCore.v @@ -7,7 +7,7 @@ *************************************************************************) -Require Import List Bool Sumbool EqNat Setoid Ring_theory Decidable. +Require Import List Bool Sumbool EqNat Setoid Ring_theory Decidable ZArith_base. Delimit Scope Int_scope with I. (* Abstract Integers. *) @@ -81,7 +81,6 @@ End Int. Module Z_as_Int <: Int. - Require Import ZArith_base. Open Scope Z_scope. Definition int := Z. diff --git a/contrib/setoid_ring/Field_theory.v b/contrib/setoid_ring/Field_theory.v index 65a397ac..b2e5cc4b 100644 --- a/contrib/setoid_ring/Field_theory.v +++ b/contrib/setoid_ring/Field_theory.v @@ -1619,6 +1619,7 @@ split. generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto. apply H0. generalize (PCond_cons_inv_r _ _ _ H1); simpl; auto. +clear get_sign get_sign_spec. generalize Hp; case l0; simpl; intuition. Qed. diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v index c1fa963f..e664b3b7 100644 --- a/contrib/setoid_ring/InitialRing.v +++ b/contrib/setoid_ring/InitialRing.v @@ -38,14 +38,6 @@ Proof. exact Zmult_plus_distr_l. trivial. exact Zminus_diag. Qed. - Lemma Zeqb_ok : forall x y, Zeq_bool x y = true -> x = y. - Proof. - intros x y. - assert (H := Zcompare_Eq_eq x y);unfold Zeq_bool; - destruct (Zcompare x y);intros H1;auto;discriminate H1. - Qed. - - (** Two generic morphisms from Z to (abrbitrary) rings, *) (**second one is more convenient for proofs but they are ext. equal*) Section ZMORPHISM. @@ -174,7 +166,7 @@ Section ZMORPHISM. Zeq_bool x y = true -> [x] == [y]. Proof. intros x y H. - assert (H1 := Zeqb_ok x y H);unfold IDphi in H1. + assert (H1 := Zeq_bool_eq x y H);unfold IDphi in H1. rewrite H1;rrefl. Qed. diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v index 29feab5c..531ab3ca 100644 --- a/contrib/setoid_ring/Ring_theory.v +++ b/contrib/setoid_ring/Ring_theory.v @@ -494,7 +494,7 @@ Qed. Proof. intros;mrewrite. Qed. Lemma ARdistr_r : forall x y z, z * (x + y) == z*x + z*y. - Proof. + Proof. intros;mrewrite. repeat rewrite (ARth.(ARmul_comm) z);sreflexivity. Qed. diff --git a/contrib/setoid_ring/ZArithRing.v b/contrib/setoid_ring/ZArithRing.v index 4a5b623b..942915ab 100644 --- a/contrib/setoid_ring/ZArithRing.v +++ b/contrib/setoid_ring/ZArithRing.v @@ -50,7 +50,7 @@ Ltac Zpower_neg := end. Add Ring Zr : Zth - (decidable Zeqb_ok, constants [Zcst], preprocess [Zpower_neg;unfold Zsucc], + (decidable Zeq_bool_eq, constants [Zcst], preprocess [Zpower_neg;unfold Zsucc], power_tac Zpower_theory [Zpow_tac], (* The two following option are not needed, it is the default chose when the set of coefficiant is usual ring Z *) diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index dd79801d..3d022add 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(*i $Id: newring.ml4 11094 2008-06-10 19:35:23Z herbelin $ i*) +(*i $Id: newring.ml4 11282 2008-07-28 11:51:53Z msozeau $ i*) open Pp open Util @@ -452,11 +452,14 @@ let (theory_to_obj, obj_to_theory) = let setoid_of_relation env a r = - lapp coq_mk_Setoid - [|a ; r ; - Class_tactics.reflexive_proof env a r ; - Class_tactics.symmetric_proof env a r ; - Class_tactics.transitive_proof env a r |] + try + lapp coq_mk_Setoid + [|a ; r ; + Class_tactics.reflexive_proof env a r ; + Class_tactics.symmetric_proof env a r ; + Class_tactics.transitive_proof env a r |] + with Not_found -> + error "cannot find setoid relation" let op_morph r add mul opp req m1 m2 m3 = lapp coq_mk_reqe [| r; add; mul; opp; req; m1; m2; m3 |] diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4 index 88243b60..4cf5336d 100644 --- a/contrib/subtac/g_subtac.ml4 +++ b/contrib/subtac/g_subtac.ml4 @@ -14,7 +14,7 @@ Syntax for the subtac terms and types. Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliātre *) -(* $Id: g_subtac.ml4 10919 2008-05-11 22:04:26Z msozeau $ *) +(* $Id: g_subtac.ml4 11282 2008-07-28 11:51:53Z msozeau $ *) open Flags @@ -139,10 +139,10 @@ VERNAC COMMAND EXTEND Subtac_Admit_Obligations END VERNAC COMMAND EXTEND Subtac_Set_Solver -| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ +| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ Coqlib.check_required_library ["Coq";"Program";"Tactics"]; Tacinterp.add_tacdef false - [(Qualid (dummy_loc, qualid_of_string "Coq.Program.Tactics.obligations_tactic"), true, t)] ] + [(Qualid (dummy_loc, qualid_of_string "Coq.Program.Tactics.obligation_tactic"), true, t)] ] END VERNAC COMMAND EXTEND Subtac_Show_Obligations diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index a59ad6f5..7bfa107b 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac.ml 11150 2008-06-19 11:38:27Z msozeau $ *) +(* $Id: subtac.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Global open Pp @@ -229,7 +229,8 @@ let subtac (loc, command) = debug 2 (Himsg.explain_pretype_error env exn); raise e - | (Stdpp.Exc_located (loc, e')) as e -> + | (Stdpp.Exc_located (loc, Proof_type.LtacLocated (_,e')) | + Stdpp.Exc_located (loc, e') as e) -> debug 2 (str "Parsing exception: "); (match e' with | Type_errors.TypeError (env, exn) -> diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml index c7182bd2..04bf54d3 100644 --- a/contrib/subtac/subtac_cases.ml +++ b/contrib/subtac/subtac_cases.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_cases.ml 11154 2008-06-19 18:42:19Z msozeau $ *) +(* $Id: subtac_cases.ml 11282 2008-07-28 11:51:53Z msozeau $ *) open Cases open Util @@ -2056,8 +2056,10 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra t, prepare_predicate_from_arsign_tycon loc env (Evd.evars_of !isevars) tomatchs sign (lift tomatchs_len t) in - let arity = - it_mkProd_or_LetIn (lift neqs arity) (context_of_arsign eqs) + let neqs, arity = + let ctx = context_of_arsign eqs in + let neqs = List.length ctx in + neqs, it_mkProd_or_LetIn (lift neqs arity) ctx in let lets, matx = (* Type the rhs under the assumption of equations *) diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml index 15addb44..9a5539e2 100644 --- a/contrib/subtac/subtac_classes.ml +++ b/contrib/subtac/subtac_classes.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: subtac_classes.ml 11047 2008-06-03 23:08:00Z msozeau $ i*) +(*i $Id: subtac_classes.ml 11282 2008-07-28 11:51:53Z msozeau $ i*) open Pretyping open Evd @@ -73,26 +73,18 @@ let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ = let type_ctx_instance isevars env ctx inst subst = List.fold_left2 (fun (subst, instctx) (na, _, t) ce -> - let t' = replace_vars subst t in + let t' = substl subst t in let c = interp_casted_constr_evars isevars env ce t' in + isevars := resolve_typeclasses ~onlyargs:true ~fail:true env !isevars; let d = na, Some c, t' in - (na, c) :: subst, d :: instctx) + c :: subst, d :: instctx) (subst, []) (List.rev ctx) inst -(*let superclass_ce = CRef (Ident (dummy_loc, id_of_string ".superclass"))*) - let type_class_instance_params isevars env id n ctx inst subst = List.fold_left2 (fun (subst, instctx) (na, _, t) ce -> let t' = replace_vars subst t in - let c = -(* if ce = superclass_ce then *) - (* (\* Control over the evars which are direct superclasses to avoid partial instanciations *) - (* in instance search. *\) *) - (* Evarutil.e_new_evar isevars env ~src:(dummy_loc, ImplicitArg (VarRef id, (n, Some na))) t' *) - (* else *) - interp_casted_constr_evars isevars env ce t' - in + let c = interp_casted_constr_evars isevars env ce t' in let d = na, Some c, t' in (na, c) :: subst, d :: instctx) (subst, []) (List.rev ctx) inst @@ -140,9 +132,9 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class let k, ctx', imps, subst = let c = Command.generalize_constr_expr tclass ctx in let c', imps = interp_type_evars_impls ~evdref:isevars env c in - let ctx, c = Classes.decompose_named_assum c' in + let ctx, c = Sign.decompose_prod_assum c' in let cl, args = Typeclasses.dest_class_app c in - cl, ctx, imps, substitution_of_constrs (List.map snd cl.cl_context) (List.rev (Array.to_list args)) + cl, ctx, imps, (List.rev (Array.to_list args)) in let id = match snd instid with @@ -155,11 +147,11 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class let i = Nameops.add_suffix (Classes.id_of_class k) "_instance_0" in Termops.next_global_ident_away false i (Termops.ids_of_context env) in - let env' = Classes.push_named_context ctx' env in + let env' = push_rel_context ctx' env in isevars := Evarutil.nf_evar_defs !isevars; isevars := resolve_typeclasses ~onlyargs:false ~fail:true env' !isevars; let sigma = Evd.evars_of !isevars in - let substctx = Typeclasses.nf_substitution sigma subst in + let substctx = List.map (Evarutil.nf_evar sigma) subst in let subst, _propsctx = let props = List.map (fun (x, l, d) -> @@ -172,8 +164,8 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class List.fold_left (fun (props, rest) (id,_,_) -> try - let ((loc, mid), c) = List.find (fun ((_,id'), c) -> id' = id) rest in - let rest' = List.filter (fun ((_,id'), c) -> id' <> id) rest in + let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in + let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in Constrintern.add_glob loc (ConstRef (List.assoc mid k.cl_projs)); c :: props, rest' with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest) @@ -184,20 +176,13 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class else type_ctx_instance isevars env' k.cl_props props substctx in - let inst_constr, ty_constr = instance_constructor k (List.rev_map snd subst) in + let inst_constr, ty_constr = instance_constructor k (List.rev subst) in isevars := Evarutil.nf_evar_defs !isevars; - let term = Evarutil.nf_isevar !isevars (it_mkNamedLambda_or_LetIn inst_constr ctx') - and termtype = Evarutil.nf_isevar !isevars (it_mkNamedProd_or_LetIn ty_constr ctx') + let term = Evarutil.nf_isevar !isevars (it_mkLambda_or_LetIn inst_constr ctx') + and termtype = Evarutil.nf_isevar !isevars (it_mkProd_or_LetIn ty_constr ctx') in isevars := undefined_evars !isevars; Evarutil.check_evars env Evd.empty !isevars termtype; -(* let imps = *) -(* Util.list_map_i *) -(* (fun i binder -> *) -(* match binder with *) -(* ExplByPos (i, Some na), (true, true)) *) -(* 1 ctx *) -(* in *) let hook gr = let cst = match gr with ConstRef kn -> kn | _ -> assert false in let inst = Typeclasses.new_instance k pri global cst in diff --git a/contrib/subtac/subtac_classes.mli b/contrib/subtac/subtac_classes.mli index 43f00107..afb0d38d 100644 --- a/contrib/subtac/subtac_classes.mli +++ b/contrib/subtac/subtac_classes.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: subtac_classes.mli 10797 2008-04-15 13:19:33Z msozeau $ i*) +(*i $Id: subtac_classes.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) (*i*) open Names @@ -26,11 +26,11 @@ open Classes val type_ctx_instance : Evd.evar_defs ref -> Environ.env -> - (Names.identifier * 'a * Term.constr) list -> + ('a * Term.constr option * Term.constr) list -> Topconstr.constr_expr list -> - (Names.identifier * Term.constr) list -> - (Names.identifier * Term.constr) list * - (Names.identifier * Term.constr option * Term.constr) list + Term.constr list -> + Term.constr list * + ('a * Term.constr option * Term.constr) list val new_instance : ?global:bool -> diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml index b45e23d0..b046f0b3 100644 --- a/contrib/subtac/subtac_coercion.ml +++ b/contrib/subtac/subtac_coercion.ml @@ -6,7 +6,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_coercion.ml 11143 2008-06-18 15:52:42Z msozeau $ *) +(* $Id: subtac_coercion.ml 11282 2008-07-28 11:51:53Z msozeau $ *) open Util open Names @@ -111,41 +111,31 @@ module Coercion = struct : (Term.constr -> Term.constr) option = let x = nf_evar (evars_of !isevars) x and y = nf_evar (evars_of !isevars) y in -(* (try debug 1 (str "Coerce called for " ++ (my_print_constr env x) ++ *) -(* str " and "++ my_print_constr env y ++ *) -(* str " with evars: " ++ spc () ++ *) -(* my_print_evardefs !isevars); *) -(* with _ -> ()); *) let rec coerce_unify env x y = -(* (try debug 1 (str "coerce_unify from " ++ (my_print_constr env x) ++ *) -(* str " to "++ my_print_constr env y) *) -(* with _ -> ()); *) let x = hnf env isevars x and y = hnf env isevars y in try isevars := the_conv_x_leq env x y !isevars; - (* (try debug 1 (str "Unified " ++ (my_print_constr env x) ++ *) - (* str " and "++ my_print_constr env y); *) - (* with _ -> ()); *) None with Reduction.NotConvertible -> coerce' env x y and coerce' env x y : (Term.constr -> Term.constr) option = let subco () = subset_coerce env isevars x y in + let dest_prod c = + match Reductionops.decomp_n_prod env (evars_of !isevars) 1 c with + | [(na,b,t)], c -> (na,t), c + | _ -> raise NoSubtacCoercion + in let rec coerce_application typ typ' c c' l l' = let len = Array.length l in let rec aux tele typ typ' i co = -(* (try trace (str "coerce_application.aux from " ++ (my_print_constr env x) ++ *) -(* str " to "++ my_print_constr env y *) -(* ++ str "in env:" ++ my_print_env env); *) -(* with _ -> ()); *) if i < len then let hdx = l.(i) and hdy = l'.(i) in try isevars := the_conv_x_leq env hdx hdy !isevars; - let (n, eqT, restT) = destProd typ in - let (n', eqT', restT') = destProd typ' in + let (n, eqT), restT = dest_prod typ in + let (n', eqT'), restT' = dest_prod typ' in aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co with Reduction.NotConvertible -> - let (n, eqT, restT) = destProd typ in - let (n', eqT', restT') = destProd typ' in + let (n, eqT), restT = dest_prod typ in + let (n', eqT'), restT' = dest_prod typ' in let _ = try isevars := the_conv_x_leq env eqT eqT' !isevars with Reduction.NotConvertible -> raise NoSubtacCoercion @@ -163,12 +153,12 @@ module Coercion = struct [| eqT; hdx; pred; x; hdy; evar|]) in aux (hdy :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) (fun x -> eq_app (co x)) else Some co - in aux [] typ typ' 0 (fun x -> x) + in + if isEvar c || isEvar c' then + (* Second-order unification needed. *) + raise NoSubtacCoercion; + aux [] typ typ' 0 (fun x -> x) in -(* (try trace (str "coerce' from " ++ (my_print_constr env x) ++ *) -(* str " to "++ my_print_constr env y *) -(* ++ str "in env:" ++ my_print_env env); *) -(* with _ -> ()); *) match (kind_of_term x, kind_of_term y) with | Sort s, Sort s' -> (match s, s' with @@ -179,13 +169,6 @@ module Coercion = struct | Prod (name, a, b), Prod (name', a', b') -> let name' = Name (Nameops.next_ident_away (id_of_string "x") (Termops.ids_of_context env)) in let env' = push_rel (name', None, a') env in - -(* let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in *) -(* let name'' = Name (Nameops.next_ident_away (id_of_string "x'") (Termops.ids_of_context env)) in *) -(* let env'' = push_rel (name'', Some (app_opt c1 (mkRel 1)), lift 1 a) env' in *) -(* let c2 = coerce_unify env'' (liftn 1 1 b) (lift 1 b') in *) -(* mkLetIn (name'', app_opt c1 (mkRel 1), (lift 1 a), *) - let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in (* env, x : a' |- c1 : lift 1 a' > lift 1 a *) let coec1 = app_opt c1 (mkRel 1) in @@ -295,7 +278,6 @@ module Coercion = struct and subset_coerce env isevars x y = match disc_subset x with Some (u, p) -> - (* trace (str "Inserting projection "); *) let c = coerce_unify env u y in let f x = app_opt c (mkApp ((Lazy.force sig_).proj1, @@ -423,7 +405,11 @@ module Coercion = struct isevars, { uj_val = app_opt ct j.uj_val; uj_type = typ' } - + let inh_coerce_to_prod loc env isevars t = + let typ = whd_betadeltaiota env (evars_of isevars) (snd t) in + let _, typ' = mu env isevars typ in + isevars, (fst t, typ') + let inh_coerce_to_fail env evd rigidonly v t c1 = if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t) then @@ -504,14 +490,13 @@ module Coercion = struct None -> 0, 0 | Some (init, cur) -> init, cur in - (* a little more effort to get products is needed *) - try let rels, rng = decompose_prod_n nabs t in + try + let rels, rng = Reductionops.decomp_n_prod env (evars_of isevars) nabs t in (* The final range free variables must have been replaced by evars, we accept only that evars in rng are applied to free vars. *) - if noccur_with_meta 0 (succ nabsinit) rng then ( -(* trace (str "No occur between 0 and " ++ int (succ nabsinit)); *) + if noccur_with_meta 1 (succ nabs) rng then ( let env', t, t' = - let env' = List.fold_right (fun (n, t) env -> push_rel (n, None, t) env) rels env in + let env' = push_rel_context rels env in env', rng, lift nabs t' in try @@ -523,6 +508,4 @@ module Coercion = struct error_cannot_coerce env' sigma (t, t')) else isevars with _ -> isevars -(* trace (str "decompose_prod_n failed"); *) -(* raise (Invalid_argument "Subtac_coercion.inh_conv_coerces_to") *) end diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index 5bff6ad1..a2f54b02 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -350,9 +350,27 @@ let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype = let push_named_context = List.fold_right push_named +let check_evars env initial_sigma evd c = + let sigma = evars_of evd in + let c = nf_evar sigma c in + let rec proc_rec c = + match kind_of_term c with + | Evar (evk,args) -> + assert (Evd.mem sigma evk); + if not (Evd.mem initial_sigma evk) then + let (loc,k) = evar_source evk evd in + (match k with + | QuestionMark _ -> () + | _ -> + let evi = nf_evar_info sigma (Evd.find sigma evk) in + Pretype_errors.error_unsolvable_implicit loc env sigma evi k None) + | _ -> iter_constr proc_rec c + in proc_rec c + let interp_recursive fixkind l boxed = let env = Global.env() in let fixl, ntnl = List.split l in + let kind = if fixkind <> Command.IsCoFixpoint then Fixpoint else CoFixpoint in let fixnames = List.map (fun fix -> fix.Command.fix_name) fixl in (* Interp arities allowing for unresolved types *) @@ -384,20 +402,17 @@ let interp_recursive fixkind l boxed = let rec_sign = nf_named_context_evar (evars_of evd) rec_sign in let recdefs = List.length rec_sign in -(* List.iter (check_evars env_rec Evd.empty evd) fixdefs; *) -(* List.iter (check_evars env Evd.empty evd) fixtypes; *) -(* check_mutuality env kind (List.combine fixnames fixdefs); *) + List.iter (check_evars env_rec Evd.empty evd) fixdefs; + List.iter (check_evars env Evd.empty evd) fixtypes; + Command.check_mutuality env kind (List.combine fixnames fixdefs); (* Russell-specific code *) (* Get the interesting evars, those that were not instanciated *) let isevars = Evd.undefined_evars evd in - trace (str "got undefined evars" ++ Evd.pr_evar_defs isevars); let evm = Evd.evars_of isevars in - trace (str "got the evm, recdefs is " ++ int recdefs); (* Solve remaining evars *) let rec collect_evars id def typ imps = - let _ = try trace (str "In collect evars, isevars is: " ++ Evd.pr_evar_defs isevars) with _ -> () in (* Generalize by the recursive prototypes *) let def = Termops.it_mkNamedLambda_or_LetIn def rec_sign diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli index 27520867..3a6a351b 100644 --- a/contrib/subtac/subtac_command.mli +++ b/contrib/subtac/subtac_command.mli @@ -42,6 +42,7 @@ val interp_binder : Evd.evar_defs ref -> Environ.env -> Names.name -> Topconstr.constr_expr -> Term.constr + val build_recursive : (fixpoint_expr * decl_notation) list -> bool -> unit diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index 55cdc7c4..a393e2c9 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -119,7 +119,7 @@ let from_prg : program_info ProgMap.t ref = ref ProgMap.empty let freeze () = !from_prg, !default_tactic_expr let unfreeze (v, t) = from_prg := v; set_default_tactic t let init () = - from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.tactics_call "obligations_tactic" []) + from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.tactics_call "obligation_tactic" []) let _ = Summary.declare_summary "program-tcc-table" @@ -442,6 +442,7 @@ and solve_obligation_by_tac prg obls i tac = true else false with + | Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s))) | Stdpp.Exc_located(_, Refiner.FailError (_, s)) | Refiner.FailError (_, s) -> user_err_loc (obl.obl_location, "solve_obligation", s) diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml index 0e987cf2..ad76bdeb 100644 --- a/contrib/subtac/subtac_pretyping.ml +++ b/contrib/subtac/subtac_pretyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_pretyping.ml 11047 2008-06-03 23:08:00Z msozeau $ *) +(* $Id: subtac_pretyping.ml 11282 2008-07-28 11:51:53Z msozeau $ *) open Global open Pp @@ -117,7 +117,6 @@ let env_with_binders env isevars l = in aux (env, []) l let subtac_process env isevars id bl c tycon = -(* let bl = Implicit_quantifiers.ctx_of_class_binders (vars_of_env env) cbl @ l in *) let c = Command.abstract_constr_expr c bl in let tycon = match tycon with @@ -132,12 +131,14 @@ let subtac_process env isevars id bl c tycon = let imps = Implicit_quantifiers.implicits_of_rawterm c in let coqc, ctyp = interp env isevars c tycon in let evm = non_instanciated_map env isevars (evars_of !isevars) in - evm, coqc, (match tycon with Some (None, c) -> c | _ -> ctyp), imps + let ty = nf_isevar !isevars (match tycon with Some (None, c) -> c | _ -> ctyp) in + evm, coqc, ty, imps open Subtac_obligations let subtac_proof kind env isevars id bl c tycon = let evm, coqc, coqt, imps = subtac_process env isevars id bl c tycon in - let evm = Subtac_utils.evars_of_term evm Evd.empty coqc in - let evars, def, ty = Eterm.eterm_obligations env id !isevars evm 0 coqc coqt in + let evm' = Subtac_utils.evars_of_term evm Evd.empty coqc in + let evm' = Subtac_utils.evars_of_term evm evm' coqt in + let evars, def, ty = Eterm.eterm_obligations env id !isevars evm' 0 coqc coqt in add_definition id def ty ~implicits:imps ~kind:kind evars diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index afa5817f..559b6ac1 100644 --- a/contrib/subtac/subtac_pretyping_F.ml +++ b/contrib/subtac/subtac_pretyping_F.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_pretyping_F.ml 11143 2008-06-18 15:52:42Z msozeau $ *) +(* $Id: subtac_pretyping_F.ml 11282 2008-07-28 11:51:53Z msozeau $ *) open Pp open Util @@ -246,6 +246,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) ctxtv vdef in evar_type_fixpoint loc env isevars names ftys vdefj; + let ftys = Array.map (nf_evar (evars_of !isevars)) ftys in + let fdefs = Array.map (fun x -> nf_evar (evars_of !isevars) (j_val x)) vdefj in let fixj = match fixkind with | RFix (vn,i) -> (* First, let's find the guard indexes. *) @@ -260,11 +262,11 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | None -> list_map_i (fun i _ -> i) 0 ctxtv.(i)) vn) in - let fixdecls = (names,ftys,Array.map j_val vdefj) in + let fixdecls = (names,ftys,fdefs) in let indexes = search_guard loc env possible_indexes fixdecls in make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | RCoFix i -> - let cofix = (i,(names,ftys,Array.map j_val vdefj)) in + let cofix = (i,(names,ftys,fdefs)) in (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e); make_judge (mkCoFix cofix) ftys.(i) in inh_conv_coerce_to_tycon loc env isevars fixj tycon @@ -273,13 +275,15 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct inh_conv_coerce_to_tycon loc env isevars (pretype_sort s) tycon | RApp (loc,f,args) -> - let length = List.length args in + let length = List.length args in let ftycon = - match tycon with - None -> None + if length > 0 then + match tycon with + | None -> None | Some (None, ty) -> mk_abstr_tycon length ty | Some (Some (init, cur), ty) -> Some (Some (length + init, length + cur), ty) + else tycon in let fj = pretype ftycon env isevars lvar f in let floc = loc_of_rawconstr f in @@ -291,23 +295,13 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let resty = whd_betadeltaiota env (evars_of !isevars) resj.uj_type in match kind_of_term resty with | Prod (na,c1,c2) -> - let hj = pretype (mk_tycon c1) env isevars lvar c in + Option.iter (fun ty -> isevars := + Coercion.inh_conv_coerces_to loc env !isevars resty ty) tycon; + let evd, (_, _, tycon) = split_tycon loc env !isevars tycon in + isevars := evd; + let hj = pretype (mk_tycon (nf_isevar !isevars c1)) env isevars lvar c in let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in let typ' = nf_isevar !isevars typ in - let tycon = - Option.map - (fun (abs, ty) -> - match abs with - None -> - isevars := Coercion.inh_conv_coerces_to loc env !isevars typ' - (abs, ty); - (abs, ty) - | Some (init, cur) -> - isevars := Coercion.inh_conv_coerces_to loc env !isevars typ' - (abs, ty); - (Some (init, pred cur), ty)) - tycon - in apply_rec env (n+1) { uj_val = nf_isevar !isevars value; uj_type = nf_isevar !isevars typ' } @@ -319,7 +313,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (join_loc floc argloc) env (evars_of !isevars) resj [hj] in - let ftycon = Option.map (lift_abstr_tycon_type (-1)) ftycon in let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj ftycon args) in let resj = match kind_of_term resj.uj_val with @@ -332,12 +325,22 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct inh_conv_coerce_to_tycon loc env isevars resj tycon | RLambda(loc,name,k,c1,c2) -> - let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon in + let tycon' = evd_comb1 + (fun evd tycon -> + match tycon with + | None -> evd, tycon + | Some ty -> + let evd, ty' = Coercion.inh_coerce_to_prod loc env evd ty in + evd, Some ty') + isevars tycon + in + let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon' in let dom_valcon = valcon_of_tycon dom in let j = pretype_type dom_valcon env isevars lvar c1 in let var = (name,None,j.utj_val) in let j' = pretype rng (push_rel var env) isevars lvar c2 in - judge_of_abstraction env name j j' + let resj = judge_of_abstraction env name j j' in + inh_conv_coerce_to_tycon loc env isevars resj tycon | RProd(loc,name,k,c1,c2) -> let j = pretype_type empty_valcon env isevars lvar c1 in diff --git a/contrib/subtac/test/ListsTest.v b/contrib/subtac/test/ListsTest.v index 3ceea173..05fc0803 100644 --- a/contrib/subtac/test/ListsTest.v +++ b/contrib/subtac/test/ListsTest.v @@ -1,5 +1,5 @@ (* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *) -Require Import Coq.subtac.Utils. +Require Import Coq.Program.Program. Require Import List. Set Implicit Arguments. @@ -7,7 +7,7 @@ Set Implicit Arguments. Section Accessors. Variable A : Set. - Program Definition myhd : forall { l : list A | length l <> 0 }, A := + Program Definition myhd : forall (l : list A | length l <> 0), A := fun l => match l with | nil => ! @@ -39,7 +39,7 @@ Section app. Next Obligation. intros. - destruct_call app ; subtac_simpl. + destruct_call app ; program_simpl. Defined. Program Lemma app_id_l : forall l : list A, l = nil ++ l. @@ -49,7 +49,7 @@ Section app. Program Lemma app_id_r : forall l : list A, l = l ++ nil. Proof. - induction l ; simpl ; auto. + induction l ; simpl in * ; auto. rewrite <- IHl ; auto. Qed. @@ -70,16 +70,24 @@ Section Nth. Next Obligation. Proof. - intros. - inversion H. + simpl in *. auto with arith. Defined. + Next Obligation. + Proof. + inversion H. + Qed. + Program Fixpoint nth' (l : list A) (n : nat | n < length l) { struct l } : A := match l, n with | hd :: _, 0 => hd | _ :: tl, S n' => nth' tl n' | nil, _ => ! end. + Next Obligation. + Proof. + simpl in *. auto with arith. + Defined. Next Obligation. Proof. diff --git a/contrib/subtac/test/take.v b/contrib/subtac/test/take.v index 87ab47d6..2e17959c 100644 --- a/contrib/subtac/test/take.v +++ b/contrib/subtac/test/take.v @@ -1,9 +1,12 @@ (* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *) Require Import JMeq. Require Import List. -Require Import Coq.subtac.Utils. +Require Import Program. Set Implicit Arguments. +Obligations Tactic := idtac. + +Print cons. Program Fixpoint take (A : Set) (l : list A) (n : nat | n <= length l) { struct l } : { l' : list A | length l' = n } := match n with @@ -16,21 +19,14 @@ Program Fixpoint take (A : Set) (l : list A) (n : nat | n <= length l) { struct end. Require Import Omega. - +Solve All Obligations. Next Obligation. - intros. - simpl in l0. - apply le_S_n ; exact l0. -Defined. - -Next Obligation. - intros. - destruct_call take ; subtac_simpl. + destruct_call take ; program_simpl. Defined. Next Obligation. intros. - inversion l0. + inversion H. Defined. diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4 index 9afd07a6..05be01bc 100644 --- a/contrib/xml/proofTree2Xml.ml4 +++ b/contrib/xml/proofTree2Xml.ml4 @@ -82,8 +82,7 @@ let first_word s = let string_of_prim_rule x = match x with | Proof_type.Intro _-> "Intro" - | Proof_type.Intro_replacing _-> "Intro_replacing" - | Proof_type.Cut (_,_,_) -> "Cut" + | Proof_type.Cut _ -> "Cut" | Proof_type.FixRule (_,_,_) -> "FixRule" | Proof_type.Cofix (_,_)-> "Cofix" | Proof_type.Refine _ -> "Refine" |