From a5b631f7260e7d29defd8bd5c67db543742c9ecd Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 9 May 2016 17:40:04 +0200
Subject: congruence/univs: properly refresh (fix #4609)

In congruence, refresh universes including the Set/Prop ones so that
congruence works with cumulativity, not restricting itself to the
inferred types of terms that are manipulated but allowing them to be
used at more general types. This fixes bug #4609.
---
 plugins/cc/cctac.ml | 109 ++++++++++++++++++++++++++--------------------------
 1 file changed, 55 insertions(+), 54 deletions(-)

(limited to 'plugins')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index df4a7319ac..de555f0a7e 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -245,10 +245,10 @@ let build_projection intype outtype (cstr:pconstructor) special default gls=
 
 let _M =mkMeta
 
-let app_global f args k = 
+let app_global f args k =
   Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
 
-let new_app_global f args k = 
+let new_app_global f args k =
   Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
 
 let new_refine c = Proofview.V82.tactic (refine c)
@@ -258,7 +258,19 @@ let assert_before n c =
     let evm, _ = Tacmach.New.pf_apply type_of gl c in
       Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c)
   end
-    
+
+let refresh_type env evm ty =
+  Evarsolve.refresh_universes ~status:Evd.univ_flexible ~propset:true
+			      (Some false) env evm ty
+
+let refresh_universes ty k =
+  Proofview.Goal.enter begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let evm = Proofview.Goal.sigma gl in
+    let evm, ty = refresh_type env evm ty in
+    Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (k ty)
+  end
+
 let rec proof_tac p : unit Proofview.tactic =
   Proofview.Goal.nf_enter begin fun gl ->
   let type_of t = Tacmach.New.pf_unsafe_type_of gl t in
@@ -268,35 +280,31 @@ let rec proof_tac p : unit Proofview.tactic =
     | SymAx c ->
 	let l=constr_of_term p.p_lhs and
 	    r=constr_of_term p.p_rhs in
-        let typ = (* Termops.refresh_universes *) type_of l in
-        new_app_global _sym_eq [|typ;r;l;c|] exact_check
+	refresh_universes (type_of l) (fun typ ->
+        new_app_global _sym_eq [|typ;r;l;c|] exact_check)
     | Refl t ->
 	let lr = constr_of_term t in
-	let typ = (* Termops.refresh_universes *) type_of lr in
-        new_app_global _refl_equal [|typ;constr_of_term t|] exact_check
+	refresh_universes (type_of lr) (fun typ ->
+        new_app_global _refl_equal [|typ;constr_of_term t|] exact_check)
     | Trans (p1,p2)->
 	let t1 = constr_of_term p1.p_lhs and
 	    t2 = constr_of_term p1.p_rhs and
 	    t3 = constr_of_term p2.p_rhs in
-	let typ = (* Termops.refresh_universes *) (type_of t2) in
+	refresh_universes (type_of t2) (fun typ ->
 	let prf = new_app_global _trans_eq [|typ;t1;t2;t3;_M 1;_M 2|] in
-          Tacticals.New.tclTHENS (prf new_refine) [(proof_tac p1);(proof_tac p2)]
+          Tacticals.New.tclTHENS (prf new_refine) [(proof_tac p1);(proof_tac p2)])
     | Congr (p1,p2)->
 	let tf1=constr_of_term p1.p_lhs
 	and tx1=constr_of_term p2.p_lhs
 	and tf2=constr_of_term p1.p_rhs
 	and tx2=constr_of_term p2.p_rhs in
-	let typf = (* Termops.refresh_universes  *)(type_of tf1) in
-	let typx = (* Termops.refresh_universes *) (type_of tx1) in
-	let typfx = (* Termops.refresh_universes *) (type_of (mkApp (tf1,[|tx1|]))) in
+	refresh_universes (type_of tf1) (fun typf ->
+	refresh_universes (type_of tx1) (fun typx ->
+	refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx ->
         let id = Tacmach.New.of_old (fun gls -> pf_get_new_id (Id.of_string "f") gls) gl in
 	let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
-	let lemma1 =
-	  app_global _f_equal
-		[|typf;typfx;appx1;tf1;tf2;_M 1|] in
-	let lemma2=
-	  app_global _f_equal
-		[|typx;typfx;tf2;tx1;tx2;_M 1|] in
+	let lemma1 = app_global _f_equal [|typf;typfx;appx1;tf1;tf2;_M 1|] in
+	let lemma2 = app_global _f_equal [|typx;typfx;tf2;tx1;tx2;_M 1|] in
 	let prf =
 	  app_global _trans_eq
 		[|typfx;
@@ -310,53 +318,51 @@ let rec proof_tac p : unit Proofview.tactic =
 		reflexivity;
                 Tacticals.New.tclZEROMSG
 		    (Pp.str
-		       "I don't know how to handle dependent equality")]]
+		       "I don't know how to handle dependent equality")]])))
   | Inject (prf,cstr,nargs,argind) ->
 	 let ti=constr_of_term prf.p_lhs in
 	 let tj=constr_of_term prf.p_rhs in
 	 let default=constr_of_term p.p_lhs in
-	 let intype = (* Termops.refresh_universes *) (type_of ti) in
-	 let outtype = (* Termops.refresh_universes *) (type_of default) in
 	 let special=mkRel (1+nargs-argind) in
-         let proj =
+	 refresh_universes (type_of ti) (fun intype ->
+         refresh_universes (type_of default) (fun outtype ->
+	 let proj =
            Tacmach.New.of_old (build_projection intype outtype cstr special default) gl
          in
 	 let injt=
            app_global _f_equal [|intype;outtype;proj;ti;tj;_M 1|] in
-	   Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf)
+	   Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf)))
   with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
   end
 
 let refute_tac c t1 t2 p =
   Proofview.Goal.nf_enter begin fun gl ->
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
-  let intype =
-    Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt1)) gl
-  in
-  let neweq= new_app_global _eq [|intype;tt1;tt2|] in
   let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
   let false_t=mkApp (c,[|mkVar hid|]) in
+  let k intype =
+    let neweq= new_app_global _eq [|intype;tt1;tt2|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
       [proof_tac p; simplest_elim false_t]
+  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt1) k
   end
 
 let refine_exact_check c gl =
   let evm, _ = pf_apply type_of gl c in
     Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl
 
-let convert_to_goal_tac c t1 t2 p = 
+let convert_to_goal_tac c t1 t2 p =
   Proofview.Goal.nf_enter begin fun gl ->
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
-  let sort =
-    Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt2)) gl
-  in
-  let neweq= new_app_global _eq [|sort;tt1;tt2|] in
-  let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in
-  let x = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
-  let identity=mkLambda (Name x,sort,mkRel 1) in
-  let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
+  let k sort =
+    let neweq= new_app_global _eq [|sort;tt1;tt2|] in
+    let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in
+    let x = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
+    let identity=mkLambda (Name x,sort,mkRel 1) in
+    let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name e)))
-      [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]
+			   [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]
+  in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k
   end
 
 let convert_to_hyp_tac c1 t1 c2 t2 p =
@@ -372,33 +378,28 @@ let convert_to_hyp_tac c1 t1 c2 t2 p =
 let discriminate_tac (cstr,u as cstru) p =
   Proofview.Goal.nf_enter begin fun gl ->
     let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
-    let intype =
-      Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls t1)) gl
-    in
+    let env = Proofview.Goal.env gl in
     let concl = Proofview.Goal.concl gl in
-    (* let evm,outsort = Evd.new_sort_variable Evd.univ_rigid (project gls) in  *)
-    (* let outsort = mkSort outsort in *)
     let xid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in
-    (* let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in *)
-    (* let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in *)
     let identity = Universes.constr_of_global (Lazy.force _I) in
-    (* let trivial=pf_unsafe_type_of gls identity in *)
     let trivial = Universes.constr_of_global (Lazy.force _True) in
-    let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Proofview.Goal.sigma gl) in 
+    let evm = Proofview.Goal.sigma gl in
+    let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl t1) in
+    let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm in
     let outtype = mkSort outtype in
-    let pred=mkLambda(Name xid,outtype,mkRel 1) in
+    let pred = mkLambda(Name xid,outtype,mkRel 1) in
     let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
     let proj = Tacmach.New.of_old (build_projection intype outtype cstru trivial concl) gl in
     let injt=app_global _f_equal
-                    [|intype;outtype;proj;t1;t2;mkVar hid|] in
+			[|intype;outtype;proj;t1;t2;mkVar hid|] in
     let endt k =
       injt (fun injt ->
-        app_global _eq_rect
-          [|outtype;trivial;pred;identity;concl;injt|] k) in
+            app_global _eq_rect
+		       [|outtype;trivial;pred;identity;concl;injt|] k) in
     let neweq=new_app_global _eq [|intype;t1;t2|] in
     Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm)
-      (Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
-        [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)])
+			  (Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
+      [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)])
   end
 
 (* wrap everything *)
@@ -482,7 +483,7 @@ let congruence_tac depth l =
    This isn't particularly related with congruence, apart from
    the fact that congruence is called internally.
 *)
-    
+
 let mk_eq f c1 c2 k =
   Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc ->
   Proofview.Goal.enter begin
@@ -495,7 +496,7 @@ let mk_eq f c1 c2 k =
     Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm))
 			  (k term)
     end)
-    
+
 let f_equal =
   Proofview.Goal.nf_enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
-- 
cgit v1.2.3


From ee8009e05d3e782ee6333d0054ee2fce5cda89a4 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 9 May 2016 17:43:59 +0200
Subject: congruence: remove casts of indexed terms

This fixes the end of bug #4069, provoked by a use
of unshelve refine which introduces a cast.
---
 plugins/cc/cctac.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index de555f0a7e..ba34d49bb0 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -80,8 +80,10 @@ let rec decompose_term env sigma t=
     | Proj (p, c) -> 
 	let canon_const kn = constant_of_kn (canonical_con kn) in 
 	let p' = Projection.map canon_const p in
-	  (Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c))
-    | _ ->if closed0 t then (Symb t) else raise Not_found
+	(Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c))
+    | _ ->
+       let t = strip_outer_cast t in
+       if closed0 t then Symb t else raise Not_found
 
 (* decompose equality in members and type *)
 open Globnames
-- 
cgit v1.2.3


From 71d4c435e42c24c21ae43f0ddcc7a71bee1009f5 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 9 May 2016 18:31:01 +0200
Subject: congruence: Restrict refreshing to Set

Because refreshing Prop is not semantics-preserving,
the new universe is >= Set, so cannot be minimized to Prop
afterwards.
---
 plugins/cc/cctac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index ba34d49bb0..c8d857b31f 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -262,7 +262,7 @@ let assert_before n c =
   end
 
 let refresh_type env evm ty =
-  Evarsolve.refresh_universes ~status:Evd.univ_flexible ~propset:true
+  Evarsolve.refresh_universes ~status:Evd.univ_flexible ~refreshset:true
 			      (Some false) env evm ty
 
 let refresh_universes ty k =
-- 
cgit v1.2.3


From a91bafa58710777506dc30afb1a0e2cc56b941c7 Mon Sep 17 00:00:00 2001
From: thery
Date: Tue, 5 Jul 2016 14:02:28 +0200
Subject: Bug fix : variable capture in ltac code of Nsatz

changing
set (x := val)
into
let x := fresh "x" in
set (x := val)
---
 plugins/nsatz/Nsatz.v | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'plugins')

diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v
index 3068b53470..b11d15e5ca 100644
--- a/plugins/nsatz/Nsatz.v
+++ b/plugins/nsatz/Nsatz.v
@@ -298,7 +298,9 @@ Ltac nsatz_call_n info nparam p rr lp kont :=
   match goal with
   | |- (?c::PEpow _ ?r::?lq0)::?lci0 = _ -> _ =>
     intros _;
+    let lci := fresh "lci" in
     set (lci:=lci0);
+    let lq := fresh "lq" in
     set (lq:=lq0);
     kont c rr lq lci
   end.
@@ -380,10 +382,13 @@ Ltac nsatz_generic radicalmax info lparam lvar :=
     end in 
 
   SplitPolyList ltac:(fun p lp =>
+    let p21 := fresh "p21" in
+    let lp21 := fresh "lp21" in
     set (p21:=p) ;
     set (lp21:=lp);
 (*    idtac "nparam:"; idtac nparam; idtac "p:"; idtac p; idtac "lp:"; idtac lp; *)
     nsatz_call radicalmax info nparam p lp ltac:(fun c r lq lci => 
+      let q := fresh "q" in
       set (q := PEmul c (PEpow p21 r)); 
       let Hg := fresh "Hg" in 
       assert (Hg:check lp21 q (lci,lq) = true); 
-- 
cgit v1.2.3


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(-)

(limited to 'plugins')

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(-)

(limited to 'plugins')

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