Correct rebase on STM code. Thanks to E. Tassi for help on dealing with

latent universes. Now the universes in the type of a definition/lemma
are eagerly added to the environment so that later proofs can be checked
independently of the original (delegated) proof body.

- Fixed firstorder, ring to work correctly with universe polymorphism.
- Changed constr_of_global to raise an anomaly if side effects would be lost by
turning a polymorphic constant into a constr.
- Fix a non-termination issue in solve_evar_evar.
-

2 files changed, 67 insertions, 172 deletions

diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index 2b9dce1b0b..de308c2964 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -113,6 +113,28 @@ Lemma ceqb_spec c c' : BoolSpec ([c] == [c']) True (c =? c')%coef.
 Proof.
 generalize (CRmorph.(morph_eq) c c').
 destruct (c =? c')%coef; auto.
+<<<<<<< HEAD
+=======
+||||||| merged common ancestors
+destruct (c ?= c')%coef; auto.
+=======
+destruct (c ?= c')%coef; auto.
+<<<<<<< HEAD
+=======
+intros.
+generalize (fun h => X (morph_eq CRmorph _ _ h)).
+case (ceqb c1 c2); auto.
+>>>>>>> .merge_file_U4r9lJ
+>>>>>>> This commit adds full universe polymorphism and fast projections to Coq.
+||||||| merged common ancestors
+=======
+intros.
+generalize (fun h => X (morph_eq CRmorph _ _ h)).
+case (ceqb c1 c2); auto.
+>>>>>>> .merge_file_U4r9lJ
+=======
+>>>>>>> Correct rebase on STM code. Thanks to E. Tassi for help on dealing with
+>>>>>>> Correct rebase on STM code. Thanks to E. Tassi for help on dealing with
 Qed.
 
 (* Power coefficients : Cpow *)
@@ -279,6 +301,7 @@ apply radd_ext.
   [ ring | now rewrite rdiv_simpl ].
 Qed.
 
+<<<<<<< HEAD
 Theorem rdiv3 r1 r2 r3 r4 :
  ~ r2 == 0 ->
  ~ r4 == 0 ->
@@ -294,6 +317,8 @@ f_equiv.
 transitivity (r1 * r4 + - (r3 * r2)); auto.
 Qed.
 
+=======
+>>>>>>> Correct rebase on STM code. Thanks to E. Tassi for help on dealing with
 Theorem rdiv5 a b : - (a / b) == - a / b.
 Proof.
 now rewrite !rdiv_def, ropp_mul_l.
@@ -712,7 +737,6 @@ Fixpoint PEsimp (e : PExpr C) : PExpr C :=
   | _ => e
  end%poly.
 
-<<<<<<< .merge_file_5Z3Qpn
 Theorem PEsimp_ok e : (PEsimp e === e)%poly.
 Proof.
 induction e; simpl.
@@ -725,32 +749,6 @@ induction e; simpl.
 - rewrite NPEmul_ok. now f_equiv.
 - rewrite NPEopp_ok. now f_equiv.
 - rewrite NPEpow_ok. now f_equiv.
-=======
-Theorem PExpr_simp_correct:
- forall l e,  NPEeval l (PExpr_simp e) == NPEeval l e.
-clear eq_sym.
-intros l e; elim e; simpl; auto.
-intros e1 He1 e2 He2.
-transitivity (NPEeval l (PEadd (PExpr_simp e1) (PExpr_simp e2))); auto.
-apply NPEadd_correct.
-simpl; auto.
-intros e1 He1 e2 He2.
-transitivity (NPEeval l (PEsub (PExpr_simp e1) (PExpr_simp e2))). auto.
-apply NPEsub_correct.
-simpl; auto.
-intros e1 He1 e2 He2.
-transitivity (NPEeval l (PEmul (PExpr_simp e1) (PExpr_simp e2))); auto.
-apply NPEmul_correct.
-simpl; auto.
-intros e1 He1.
-transitivity (NPEeval l (PEopp (PExpr_simp e1))); auto.
-apply NPEopp_correct.
-simpl; auto.
-intros e1 He1 n;simpl.
-rewrite NPEpow_correct;simpl.
-repeat rewrite pow_th.(rpow_pow_N).
-rewrite He1;auto.
->>>>>>> .merge_file_U4r9lJ
 Qed.
 
 
@@ -1004,7 +1002,6 @@ Fixpoint split_aux e1 p e2 {struct e1}: rsplit :=
        end
   end%poly.
 
-<<<<<<< .merge_file_5Z3Qpn
 Lemma split_aux_ok1 e1 p e2 :
   (let res := match isIn e1 p e2 1 with
        | Some (N0,e3) => mk_rsplit 1 (e1 ^^ Npos p) e3
@@ -1015,20 +1012,6 @@ Lemma split_aux_ok1 e1 p e2 :
   e1 ^ Npos p === left res * common res
   /\ e2 === right res * common res)%poly.
 Proof.
-=======
-Lemma split_aux_correct_1 : forall l e1 p e2,
-  let res :=  match isIn e1 p e2 xH with
-       | Some (N0,e3) => mk_rsplit (PEc cI) (NPEpow e1 (Npos p)) e3
-       | Some (Npos q, e3) => mk_rsplit (NPEpow e1 (Npos q)) (NPEpow e1 (Npos (p - q))) e3
-       | None => mk_rsplit (NPEpow e1  (Npos p)) (PEc cI) e2
-       end in
-       NPEeval l (PEpow e1 (Npos p)) == NPEeval l (NPEmul (left res) (common res))
-   /\
-       NPEeval l e2 == NPEeval l (NPEmul (right res) (common res)).
-Proof.
- intros. unfold res. clear res; generalize (isIn_correct l e1 p e2 xH).
- destruct (isIn e1 p e2 1). destruct p0.
->>>>>>> .merge_file_U4r9lJ
  Opaque NPEpow NPEmul.
  intros. unfold res;clear res; generalize (isIn_ok e1 p e2 xH).
  destruct (isIn e1 p e2 1) as [([|p'],e')|]; simpl.
@@ -1148,7 +1131,6 @@ Eval compute
 Theorem Pcond_Fnorm l e :
  PCond l (condition (Fnorm e)) ->  ~ (denum (Fnorm e))@l == 0.
 Proof.
-<<<<<<< .merge_file_5Z3Qpn
 induction e; simpl condition; rewrite ?PCond_cons, ?PCond_app;
  simpl denum; intros (Hc1,Hc2) || intros Hc; rewrite ?NPEmul_ok.
 - simpl. rewrite phi_1; exact rI_neq_rO.
@@ -1171,93 +1153,6 @@ induction e; simpl condition; rewrite ?PCond_cons, ?PCond_app;
   + apply split_nz_r, Hc1.
 - rewrite NPEpow_ok. apply PEpow_nz, IHe, Hc.
 Qed.
-=======
- induction p;simpl.
-  intro Hp;assert (H1 := @rmul_reg_l _ (pow_pos rmul x p * pow_pos rmul x p) 0 H).
-  apply IHp.
-  rewrite (@rmul_reg_l _ (pow_pos rmul x p)  0 IHp).
-  reflexivity.
-  rewrite H1. ring. rewrite Hp;ring.
-  intro Hp;apply IHp. rewrite (@rmul_reg_l _ (pow_pos rmul x p)  0 IHp).
-  reflexivity. rewrite Hp;ring. trivial.
-Qed.
-
-Theorem Pcond_Fnorm:
- forall l e,
- PCond l (condition (Fnorm e)) ->  ~ NPEeval l ((Fnorm e).(denum)) == 0.
-intros l e; elim e.
- simpl; intros _ _; rewrite (morph1 CRmorph); exact rI_neq_rO.
- simpl; intros _ _; rewrite (morph1 CRmorph); exact rI_neq_rO.
- intros e1 Hrec1 e2 Hrec2 Hcond.
-   simpl in Hcond.
-   simpl @denum.
-   rewrite NPEmul_correct.
-   simpl.
-   apply field_is_integral_domain.
-   intros HH; case Hrec1; auto.
-     apply PCond_app_inv_l with (1 := Hcond).
-   rewrite (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2))).
-   rewrite NPEmul_correct; simpl; rewrite HH; ring.
-   intros HH; case Hrec2; auto.
-     apply PCond_app_inv_r with (1 := Hcond).
-   rewrite (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))); auto.
- intros e1 Hrec1 e2 Hrec2 Hcond.
-   simpl @condition in Hcond.
-   simpl @denum.
-   rewrite NPEmul_correct.
-   simpl.
-   apply field_is_integral_domain.
-   intros HH; case Hrec1; auto.
-     apply PCond_app_inv_l with (1 := Hcond).
-   rewrite (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2))).
-   rewrite NPEmul_correct; simpl; rewrite HH; ring.
-   intros HH; case Hrec2; auto.
-     apply PCond_app_inv_r with (1 := Hcond).
-   rewrite (split_correct_r l (denum (Fnorm e1)) (denum (Fnorm e2))); auto.
- intros e1 Hrec1 e2 Hrec2 Hcond.
-   simpl in Hcond.
-   simpl @denum.
-   rewrite NPEmul_correct.
-   simpl.
-   apply field_is_integral_domain.
-  intros HH; apply Hrec1.
-    apply PCond_app_inv_l with (1 := Hcond).
-    rewrite (split_correct_r l (num (Fnorm e2)) (denum (Fnorm e1))).
-    rewrite NPEmul_correct; simpl; rewrite HH; ring.
-  intros HH; apply Hrec2.
-    apply PCond_app_inv_r with (1 := Hcond).
-    rewrite (split_correct_r l (num (Fnorm e1)) (denum (Fnorm e2))).
-    rewrite NPEmul_correct; simpl; rewrite HH; ring.
- intros e1 Hrec1 Hcond.
-   simpl in Hcond.
-   simpl @denum.
-   auto.
- intros e1 Hrec1 Hcond.
-   simpl in Hcond.
-   simpl @denum.
-   apply PCond_cons_inv_l with (1:=Hcond).
- intros e1 Hrec1 e2 Hrec2 Hcond.
-   simpl in Hcond.
-   simpl @denum.
-   rewrite NPEmul_correct.
-   simpl.
-   apply field_is_integral_domain.
-    intros HH; apply Hrec1.
-    specialize PCond_cons_inv_r with (1:=Hcond); intro Hcond1.
-    apply PCond_app_inv_l with (1 := Hcond1).
-    rewrite (split_correct_l l (denum (Fnorm e1)) (denum (Fnorm e2))).
-    rewrite NPEmul_correct; simpl; rewrite HH; ring.
-    intros HH; apply PCond_cons_inv_l with (1:=Hcond).
-    rewrite (split_correct_r l (num (Fnorm e1)) (num (Fnorm e2))).
-    rewrite NPEmul_correct; simpl; rewrite HH; ring.
- simpl;intros e1 Hrec1 n Hcond.
-  rewrite NPEpow_correct.
-  simpl;rewrite pow_th.(rpow_pow_N).
-  destruct n;simpl;intros.
-  apply AFth.(AF_1_neq_0). apply pow_pos_not_0;auto.
-Qed.
-Hint Resolve Pcond_Fnorm.
->>>>>>> .merge_file_U4r9lJ
 
 
 (***************************************************************************
@@ -1648,21 +1543,11 @@ Hypothesis ceqb_complete : forall c1 c2, [c1] == [c2] -> ceqb c1 c2 = true.
 
 Lemma ceqb_spec' c1 c2 : Bool.reflect ([c1] == [c2]) (ceqb c1 c2).
 Proof.
-<<<<<<< .merge_file_5Z3Qpn
 assert (H := morph_eq CRmorph c1 c2).
 assert (H' := @ceqb_complete c1 c2).
 destruct (ceqb c1 c2); constructor.
 - now apply H.
 - intro E. specialize (H' E). discriminate.
-=======
-intros.
-generalize (fun h => X (morph_eq CRmorph _ _ h)).
-generalize (@ceqb_complete c1 c2).
-case (c1 ?=! c2); auto; intros.
-apply X0.
-red; intro.
-absurd (false = true); auto;  discriminate.
->>>>>>> .merge_file_U4r9lJ
 Qed.
 
 Fixpoint Fcons1 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) :=
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index ae05fbdc38..8df061870d 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -51,8 +51,17 @@ let tag_arg tag_rec map subs i c =
     | Prot -> mk_atom c
     | Rec -> if Int.equal i (-1) then mk_clos subs c else tag_rec c
 
+let global_head_of_constr c = 
+  let f, args = decompose_app c in
+    try global_of_constr f
+    with Not_found -> anomaly (str "global_head_of_constr")
+
+let global_of_constr_nofail c = 
+  try global_of_constr c
+  with Not_found -> VarRef (Id.of_string "dummy")
+
 let rec mk_clos_but f_map subs t =
-  match f_map t with
+  match f_map (global_of_constr_nofail t) with
     | Some map -> tag_arg (mk_clos_but f_map subs) map subs (-1) t
     | None ->
         (match kind_of_term t with
@@ -65,7 +74,7 @@ and mk_clos_app_but f_map subs f args n =
   else
     let fargs, args' = Array.chop n args in
     let f' = mkApp(f,fargs) in
-    match f_map f' with
+    match f_map (global_of_constr_nofail f') with
         Some map ->
           mk_clos_deep
             (fun s' -> unmark_arg (tag_arg (mk_clos_but f_map s') map s'))
@@ -74,7 +83,7 @@ and mk_clos_app_but f_map subs f args n =
       | None -> mk_clos_app_but f_map subs f args (n+1)
 
 let interp_map l t =
-  try Some(List.assoc_f eq_constr_nounivs t l) with Not_found -> None
+  try Some(List.assoc_f eq_gr t l) with Not_found -> None
 
 let protect_maps = ref String.Map.empty
 let add_map s m = protect_maps := String.Map.add s m !protect_maps
@@ -219,14 +228,12 @@ let coq_reference c =
   lazy (Coqlib.gen_reference_in_modules "Ring" stdlib_modules c)
 
 let coq_mk_Setoid = coq_constant "Build_Setoid_Theory"
-let coq_cons = coq_constant "cons"
-let coq_nil = coq_constant "nil"
-let coq_None = coq_constant "None"
-let coq_Some = coq_constant "Some"
+let coq_None = coq_reference "None"
+let coq_Some = coq_reference "Some"
 let coq_eq = coq_constant "eq"
 
-let coq_pcons = coq_reference "cons"
-let coq_pnil = coq_reference "nil"
+let coq_cons = coq_reference "cons"
+let coq_nil = coq_reference "nil"
 
 let lapp f args = mkApp(Lazy.force f,args)
 
@@ -274,7 +281,7 @@ let znew_ring_path =
 let zltac s =
   lazy(make_kn (MPfile znew_ring_path) DirPath.empty (Label.make s))
 
-let mk_cst l s = lazy (Coqlib.gen_constant "newring" l s);;
+let mk_cst l s = lazy (Coqlib.gen_reference "newring" l s);;
 let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;;
 
 (* Ring theory *)
@@ -319,9 +326,12 @@ let coq_hypo = my_reference "hypo"
 let map_with_eq arg_map c =
   let (req,_,_) = dest_rel c in
   interp_map
-    ((req,(function -1->Prot|_->Rec))::
+    ((global_head_of_constr req,(function -1->Prot|_->Rec))::
     List.map (fun (c,map) -> (Lazy.force c,map)) arg_map)
 
+let map_without_eq arg_map _ =
+  interp_map (List.map (fun (c,map) -> (Lazy.force c,map)) arg_map)
+
 let _ = add_map "ring"
   (map_with_eq
     [coq_cons,(function -1->Eval|2->Rec|_->Prot);
@@ -618,8 +628,8 @@ let make_hyp_list env evd lH =
   let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
   let l = 
     List.fold_right
-      (fun c l -> plapp evd coq_pcons [|carrier; (make_hyp env evd c); l|]) lH
-      (plapp evd coq_pnil [|carrier|])
+      (fun c l -> plapp evd coq_cons [|carrier; (make_hyp env evd c); l|]) lH
+      (plapp evd coq_nil [|carrier|])
   in 
   let l' = Typing.solve_evars env evd l in
     Evarutil.nf_evars_universes !evd l'
@@ -629,7 +639,7 @@ let interp_power env evd pow =
   match pow with
   | None ->
       let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morph_nothing) in
-      (TacArg(Loc.ghost,TacCall(Loc.ghost,t,[])), lapp coq_None [|carrier|])
+      (TacArg(Loc.ghost,TacCall(Loc.ghost,t,[])), plapp evd coq_None [|carrier|])
   | Some (tac, spec) ->
       let tac =
         match tac with
@@ -637,24 +647,24 @@ let interp_power env evd pow =
         | Closed lc ->
             closed_term_ast (List.map Smartlocate.global_with_alias lc) in
       let spec = make_hyp env evd (ic_unsafe spec) in
-      (tac, lapp coq_Some [|carrier; spec|])
+      (tac, plapp evd coq_Some [|carrier; spec|])
 
 let interp_sign env evd sign =
   let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
   match sign with
-  | None -> lapp coq_None [|carrier|]
+  | None -> plapp evd coq_None [|carrier|]
   | Some spec ->
       let spec = make_hyp env evd (ic_unsafe spec) in
-      lapp coq_Some [|carrier;spec|]
+      plapp evd coq_Some [|carrier;spec|]
        (* Same remark on ill-typed terms ... *)
 
 let interp_div env evd div =
   let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
   match div with
-  | None -> lapp coq_None [|carrier|]
+  | None -> plapp evd coq_None [|carrier|]
   | Some spec ->
       let spec = make_hyp env evd (ic_unsafe spec) in
-      lapp coq_Some [|carrier;spec|]
+      plapp evd coq_Some [|carrier;spec|]
        (* Same remark on ill-typed terms ... *)
 
 let add_theory name (sigma,rth) eqth morphth cst_tac (pre,post) power sign div =
@@ -788,8 +798,8 @@ let make_args_list rl t =
 
 let make_term_list env evd carrier rl =
   let l = List.fold_right
-    (fun x l -> plapp evd coq_pcons [|carrier;x;l|]) rl
-    (plapp evd coq_pnil [|carrier|])
+    (fun x l -> plapp evd coq_cons [|carrier;x;l|]) rl
+    (plapp evd coq_nil [|carrier|])
   in Typing.solve_evars env evd l
 
 let ltac_ring_structure e =
@@ -844,9 +854,9 @@ let _ = add_map "field"
     coq_nil, (function -1->Eval|_ -> Prot);
     (* display_linear: evaluate polynomials and coef operations, protect
        field operations and make recursive call on the var map *)
-    my_constant "display_linear",
+    my_reference "display_linear",
       (function -1|9|10|11|12|13|15|16->Eval|14->Rec|_->Prot);
-    my_constant "display_pow_linear",
+    my_reference "display_pow_linear",
      (function -1|9|10|11|12|13|14|16|18|19->Eval|17->Rec|_->Prot);
    (* Pphi_dev: evaluate polynomial and coef operations, protect
        ring operations and make recursive call on the var map *)
@@ -858,15 +868,15 @@ let _ = add_map "field"
     pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot);
     (* FEeval: evaluate morphism, protect field
        operations and make recursive call on the var map *)
-    my_constant "FEeval", (function -1|8|9|10|11|14->Eval|13->Rec|_->Prot)]);;
+    my_reference "FEeval", (function -1|8|9|10|11|14->Eval|13->Rec|_->Prot)]);;
 
 let _ = add_map "field_cond"
-  (map_with_eq
+  (map_without_eq
     [coq_cons,(function -1->Eval|2->Rec|_->Prot);
      coq_nil, (function -1->Eval|_ -> Prot);
     (* PCond: evaluate morphism and denum list, protect ring
        operations and make recursive call on the var map *)
-     my_constant "PCond", (function -1|9|11|14->Eval|13->Rec|_->Prot)]);;
+     my_reference "PCond", (function -1|9|11|14->Eval|13->Rec|_->Prot)]);;
 (*                       (function -1|9|11->Eval|10->Rec|_->Prot)]);;*)
 
 
@@ -875,9 +885,9 @@ let _ = Redexpr.declare_reduction "simpl_field_expr"
 
 
 
-let afield_theory = my_constant "almost_field_theory"
-let field_theory = my_constant "field_theory"
-let sfield_theory = my_constant "semi_field_theory"
+let afield_theory = my_reference "almost_field_theory"
+let field_theory = my_reference "field_theory"
+let sfield_theory = my_reference "semi_field_theory"
 let af_ar = my_reference"AF_AR"
 let f_r = my_reference"F_R"
 let sf_sr = my_reference"SF_SR"
@@ -885,18 +895,18 @@ let dest_field env evd th_spec =
   let th_typ = Retyping.get_type_of env !evd th_spec in
   match kind_of_term th_typ with
     | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|])
-        when eq_constr_nounivs f (Lazy.force afield_theory) ->
+        when is_global (Lazy.force afield_theory) f ->
         let rth = plapp evd af_ar
           [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in
         (None,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth)
     | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|])
-        when eq_constr_nounivs f (Lazy.force field_theory) ->
+        when is_global (Lazy.force field_theory) f ->
         let rth =
           plapp evd f_r
             [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in
         (Some false,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth)
     | App(f,[|r;zero;one;add;mul;div;inv;req|])
-        when eq_constr_nounivs f (Lazy.force sfield_theory) ->
+        when is_global (Lazy.force sfield_theory) f ->
         let rth = plapp evd sf_sr
           [|r;zero;one;add;mul;div;inv;req;th_spec|] in
         (Some true,r,zero,one,add,mul,None,None,div,inv,req,rth)