summaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2008-08-08 13:18:42 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2008-08-08 13:18:42 +0200
commit870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch)
tree0c647056de1832cf1dba5ba58758b9121418e4be /contrib
parenta0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff)
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'contrib')
-rw-r--r--contrib/extraction/modutil.ml75
-rw-r--r--contrib/extraction/table.ml3
-rw-r--r--contrib/extraction/table.mli3
-rw-r--r--contrib/firstorder/sequent.ml4
-rw-r--r--contrib/funind/functional_principles_proofs.ml12
-rw-r--r--contrib/funind/g_indfun.ml414
-rw-r--r--contrib/funind/indfun.ml2
-rw-r--r--contrib/funind/invfun.ml10
-rw-r--r--contrib/funind/recdef.ml4
-rw-r--r--contrib/interface/blast.ml30
-rw-r--r--contrib/interface/depends.ml18
-rw-r--r--contrib/interface/pbp.ml22
-rw-r--r--contrib/interface/showproof.ml4
-rw-r--r--contrib/interface/xlate.ml93
-rw-r--r--contrib/micromega/Psatz.v (renamed from contrib/micromega/Micromegatac.v)42
-rw-r--r--contrib/micromega/QMicromega.v72
-rw-r--r--contrib/micromega/RMicromega.v36
-rw-r--r--contrib/micromega/ZMicromega.v11
-rw-r--r--contrib/micromega/certificate.ml342
-rw-r--r--contrib/micromega/coq_micromega.ml334
-rw-r--r--contrib/micromega/csdpcert.ml158
-rw-r--r--contrib/micromega/g_micromega.ml439
-rw-r--r--contrib/romega/ROmega.v1
-rw-r--r--contrib/romega/ReflOmegaCore.v3
-rw-r--r--contrib/setoid_ring/Field_theory.v1
-rw-r--r--contrib/setoid_ring/InitialRing.v10
-rw-r--r--contrib/setoid_ring/Ring_theory.v2
-rw-r--r--contrib/setoid_ring/ZArithRing.v2
-rw-r--r--contrib/setoid_ring/newring.ml415
-rw-r--r--contrib/subtac/g_subtac.ml46
-rw-r--r--contrib/subtac/subtac.ml5
-rw-r--r--contrib/subtac/subtac_cases.ml8
-rw-r--r--contrib/subtac/subtac_classes.ml43
-rw-r--r--contrib/subtac/subtac_classes.mli10
-rw-r--r--contrib/subtac/subtac_coercion.ml65
-rw-r--r--contrib/subtac/subtac_command.ml27
-rw-r--r--contrib/subtac/subtac_command.mli1
-rw-r--r--contrib/subtac/subtac_obligations.ml3
-rw-r--r--contrib/subtac/subtac_pretyping.ml11
-rw-r--r--contrib/subtac/subtac_pretyping_F.ml51
-rw-r--r--contrib/subtac/test/ListsTest.v20
-rw-r--r--contrib/subtac/test/take.v18
-rw-r--r--contrib/xml/proofTree2Xml.ml43
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"