From abe34e282ee0a5f9cca3ea9f527b254388de2cf9 Mon Sep 17 00:00:00 2001 From: thery Date: Wed, 6 Jul 2016 10:01:49 +0200 Subject: Bug Fixes : 4851 4858 4880 for nsatz the function in_ideal of ideal.ml supposes the list of polynomials does not contain zero and is duplicate free. I force this invariant in the call of in_ideal in nsatz.ml4 the function clean_pol returns the reduced list plus a list of booleans that indicates which polynomials have been deleted the function expand_pol translates back the certificate of the reduced to list to the complete list thanks to the list of booleans. The fix is quadratic with respect to the input list which should be ok for reasonable usage of nsatz. If there is some performance issue we could improve the in_pol function. --- plugins/nsatz/nsatz.ml4 | 50 +++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 48 insertions(+), 2 deletions(-) diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4 index ced53d82f4..1230e64b93 100644 --- a/plugins/nsatz/nsatz.ml4 +++ b/plugins/nsatz/nsatz.ml4 @@ -472,6 +472,43 @@ let theoremedeszeros lpol p = open Ideal +(* Check if the polynomial p is in the list lp *) +let rec in_pol p lp = + match lp with + | [] -> false + | p1 :: lp1 -> if equal p p1 then true else in_pol p lp1 + +(* Remove zero polynomials and duplicates from the list of polynomials lp + Return (clp, lb) + where clp is the reduced list and lb is a list of booleans + that has the same size than lp and where true indicates an + element that has been removed + *) +let rec clean_pol lp = + match lp with + | [] -> [], [] + | p :: lp1 -> + let clp, lb = clean_pol lp1 in + if equal p zeroP || in_pol p clp then clp, true::lb + else p :: clp, false::lb + +(* Expand the list of polynomials lp putting zeros where the list of + booleans lb indicates there is a missing element + Warning: + the expansion is relative to the end of the list in reversed order + lp cannot have less elements than lb +*) +let expand_pol lb lp = + let rec aux lb lp = + match lb with + | [] -> lp + | true :: lb1 -> zeroP :: aux lb1 lp + | false :: lb1 -> + match lp with + [] -> assert false + | p :: lp1 -> p :: aux lb1 lp1 + in List.rev (aux lb (List.rev lp)) + let theoremedeszeros_termes lp = nvars:=0;(* mise a jour par term_pol_sparse *) List.iter set_nvars_term lp; @@ -522,20 +559,29 @@ let theoremedeszeros_termes lp = | [] -> assert false | p::lp1 -> let lpol = List.rev lp1 in + (* preprocessing : + we remove zero polynomials and duplicate that are not handled by in_ideal + lb is kept in order to fix the certificate in the post-processing + *) + let lpol, lb = clean_pol lpol in let (cert,lp0,p,_lct) = theoremedeszeros lpol p in info "cert ok\n"; let lc = cert.last_comb::List.rev cert.gb_comb in match remove_zeros (fun x -> equal x zeroP) lc with | [] -> assert false | (lq::lci) -> + (* post-processing : we apply the correction for the last line *) + let lq = expand_pol lb lq in (* lci commence par les nouveaux polynomes *) - let m= !nvars in + let m = !nvars in let c = pol_sparse_to_term m (polconst m cert.coef) in let r = Pow(Zero,cert.power) in let lci = List.rev lci in + (* post-processing we apply the correction for the other lines *) + let lci = List.map (expand_pol lb) lci in let lci = List.map (List.map (pol_sparse_to_term m)) lci in let lq = List.map (pol_sparse_to_term m) lq in - info ("number of parametres: "^string_of_int nparam^"\n"); + info ("number of parameters: "^string_of_int nparam^"\n"); info "term computed\n"; (c,r,lci,lq) ) -- cgit v1.2.3 From 8438b97aa5c8d8464ec7389f7992520e2c176ae6 Mon Sep 17 00:00:00 2001 From: thery Date: Wed, 6 Jul 2016 13:37:34 +0200 Subject: improved complexity in nsatz we use a hashtable to reduce the complexity of creating a duplicate-free list. --- plugins/nsatz/nsatz.ml4 | 25 +++++++++++++------------ 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4 index 1230e64b93..592fbce675 100644 --- a/plugins/nsatz/nsatz.ml4 +++ b/plugins/nsatz/nsatz.ml4 @@ -472,12 +472,6 @@ let theoremedeszeros lpol p = open Ideal -(* Check if the polynomial p is in the list lp *) -let rec in_pol p lp = - match lp with - | [] -> false - | p1 :: lp1 -> if equal p p1 then true else in_pol p lp1 - (* Remove zero polynomials and duplicates from the list of polynomials lp Return (clp, lb) where clp is the reduced list and lb is a list of booleans @@ -485,12 +479,19 @@ let rec in_pol p lp = element that has been removed *) let rec clean_pol lp = - match lp with - | [] -> [], [] - | p :: lp1 -> - let clp, lb = clean_pol lp1 in - if equal p zeroP || in_pol p clp then clp, true::lb - else p :: clp, false::lb + let t = Hashpol.create 12 in + let find p = try Hashpol.find t p + with + Not_found -> Hashpol.add t p true; false in + let rec aux lp = + match lp with + | [] -> [], [] + | p :: lp1 -> + let clp, lb = aux lp1 in + if equal p zeroP || find p then clp, true::lb + else + (p :: clp, false::lb) in + aux lp (* Expand the list of polynomials lp putting zeros where the list of booleans lb indicates there is a missing element -- cgit v1.2.3 From 2dc63a6f49ea30e175ead4603c93cda4b2bb889b Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 7 Jul 2016 08:32:36 +0200 Subject: Update COPYRIGHT. --- COPYRIGHT | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/COPYRIGHT b/COPYRIGHT index 006ce18f1d..301bc7a393 100644 --- a/COPYRIGHT +++ b/COPYRIGHT @@ -1,6 +1,6 @@ The Coq proof assistant -Copyright 1999-2015 The Coq development team, INRIA, CNRS, University +Copyright 1999-2016 The Coq development team, INRIA, CNRS, University Paris Sud, University Paris 7, Ecole Polytechnique. This product includes also software developed by -- cgit v1.2.3 From 1ef6104cf043ec839059cddfe530a81418a3d474 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 7 Jul 2016 13:45:32 +0200 Subject: Add test file for #4880. --- test-suite/bugs/closed/4880.v | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 test-suite/bugs/closed/4880.v diff --git a/test-suite/bugs/closed/4880.v b/test-suite/bugs/closed/4880.v new file mode 100644 index 0000000000..5569798d54 --- /dev/null +++ b/test-suite/bugs/closed/4880.v @@ -0,0 +1,11 @@ +Require Import Coq.Reals.Reals Coq.nsatz.Nsatz. +Local Open Scope R. + +Goal forall x y : R, + x*x = y * y -> + x*x = -y * -y -> + x*(x*x) = 0 -> (* The associativity does not actually matter, *) + (x*x)*x = 0. (* just otherwise [assumption] would solve the goal. *) +Proof. + nsatz. +Qed. -- cgit v1.2.3 From 88f4ca3d1798fc28f230f749665bcf48597accc3 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 7 Jul 2016 13:48:20 +0200 Subject: Test file for #4858. --- test-suite/bugs/closed/4858.v | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 test-suite/bugs/closed/4858.v diff --git a/test-suite/bugs/closed/4858.v b/test-suite/bugs/closed/4858.v new file mode 100644 index 0000000000..c04895a1bb --- /dev/null +++ b/test-suite/bugs/closed/4858.v @@ -0,0 +1,7 @@ +Require Import Nsatz. +Goal True. +nsatz_compute + (PEc 0%Z :: PEc (-1)%Z + :: PEpow (PEsub (PEX Z 2) (PEX Z 3)) 1 + :: PEsub (PEX Z 1) (PEX Z 1) :: nil). +Abort. -- cgit v1.2.3 From b0e81d65b85c1846a961196d70cd86ede2993c5b Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 8 Jul 2016 10:40:03 +0200 Subject: Update csdp.cache. --- test-suite/csdp.cache | Bin 79491 -> 79491 bytes 1 file changed, 0 insertions(+), 0 deletions(-) diff --git a/test-suite/csdp.cache b/test-suite/csdp.cache index 75dd38fde8..8e5708cf02 100644 Binary files a/test-suite/csdp.cache and b/test-suite/csdp.cache differ -- cgit v1.2.3 From e1661dc9a43b34526437e9bc3029e6320e09f899 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 8 Jul 2016 13:03:16 +0200 Subject: Fix test file for #4858. --- test-suite/bugs/closed/4858.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test-suite/bugs/closed/4858.v b/test-suite/bugs/closed/4858.v index c04895a1bb..a2fa93832a 100644 --- a/test-suite/bugs/closed/4858.v +++ b/test-suite/bugs/closed/4858.v @@ -1,6 +1,6 @@ Require Import Nsatz. Goal True. -nsatz_compute +try nsatz_compute (PEc 0%Z :: PEc (-1)%Z :: PEpow (PEsub (PEX Z 2) (PEX Z 3)) 1 :: PEsub (PEX Z 1) (PEX Z 1) :: nil). -- cgit v1.2.3 From 78063b84f46de33de8ad58f80e45a90fa290dcd6 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 8 Jul 2016 14:50:32 +0200 Subject: Add a few fixes in CHANGES that were forgotten. We should really automate the generation of the log of fixes for CHANGES. --- CHANGES | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/CHANGES b/CHANGES index 7d5691efe7..e7620dd4a8 100644 --- a/CHANGES +++ b/CHANGES @@ -20,6 +20,12 @@ Other bugfixes - #4818: "Admitted" fails due to undefined universe anomaly after calling "destruct" - #4823: remote counter: avoid thread race on sockets +- #4841: -verbose flag changed semantics in 8.5, is much harder to use +- #4851: [nsatz] cannot handle duplicated hypotheses +- #4858: Anomaly: Uncaught exception Failure("hd"). Please report. in variant + of nsatz +- #4880: [nsatz_compute] generates invalid certificates if given redundant + hypotheses - #4881: synchronizing "Declare Implicit Tactic" with backtrack. - #4882: anomaly with Declare Implicit Tactic on hole of type with evars - Fix use of "Declare Implicit Tactic" in refine. -- cgit v1.2.3 From 55d32c9a017853c2411f894a3ad1a946c628ba9c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 3 Jul 2016 11:36:05 +0200 Subject: Typo. --- theories/Logic/EqdepFacts.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 30e26c7c67..bd59159bb5 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -164,7 +164,7 @@ Proof. split; auto using eq_sig_eq_dep, eq_dep_eq_sig. Qed. -(** Dependent equality is equivalent tco a dependent pair of equalities *) +(** Dependent equality is equivalent to a dependent pair of equalities *) Set Implicit Arguments. -- cgit v1.2.3 From 65ba1b36df33a74998240a02fecc1fb80c3eeeee Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 13 Jul 2016 15:27:28 +0200 Subject: Fixing printing of evar name in an error message of instantiate. --- proofs/evar_refiner.ml | 2 +- test-suite/output/Errors.out | 2 ++ test-suite/output/Errors.v | 9 +++++++++ 3 files changed, 12 insertions(+), 1 deletion(-) diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 059ae54c9d..b6f2f69d29 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -56,7 +56,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = let loc = Glob_ops.loc_of_glob_constr rawc in user_err_loc (loc,"", str "Instance is not well-typed in the environment of " ++ - str (string_of_existential evk)) + pr_existential_key sigma evk ++ str ".") in define_and_solve_constraints evk typed_c env (evars_reset_evd sigma' sigma) diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out index 6354ad469e..8048deb0c0 100644 --- a/test-suite/output/Errors.out +++ b/test-suite/output/Errors.out @@ -5,3 +5,5 @@ Unable to unify "nat" with "True". The command has indeed failed with message: In nested Ltac calls to "f" and "apply x", last call failed. Unable to unify "nat" with "True". +The command has indeed failed with message: +Error: Instance is not well-typed in the environment of ?x diff --git a/test-suite/output/Errors.v b/test-suite/output/Errors.v index 352c87385f..424d24801c 100644 --- a/test-suite/output/Errors.v +++ b/test-suite/output/Errors.v @@ -16,3 +16,12 @@ Goal True. Fail simpl; apply 0. Fail simpl; f 0. Abort. + +(* Test instantiate error messages *) + +Goal forall T1 (P1 : T1 -> Type), sigT P1 -> sigT P1. +intros T1 P1 H1. +eexists ?[x]. +destruct H1 as [x1 H1]. +Fail instantiate (x:=projT1 x1). +Abort. -- cgit v1.2.3