aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/firstorder/g_ground.ml43
-rw-r--r--plugins/firstorder/ground.ml3
-rw-r--r--plugins/firstorder/ground.mli2
-rw-r--r--plugins/firstorder/instances.ml27
-rw-r--r--plugins/firstorder/rules.ml42
-rw-r--r--plugins/firstorder/sequent.ml12
-rw-r--r--plugins/firstorder/sequent.mli4
-rw-r--r--plugins/funind/functional_principles_types.ml2
-rw-r--r--plugins/funind/g_indfun.ml42
-rw-r--r--plugins/funind/indfun.ml1
-rw-r--r--plugins/funind/indfun_common.ml2
-rw-r--r--plugins/funind/recdef.ml4
-rw-r--r--plugins/setoid_ring/Field_theory.v165
-rw-r--r--plugins/setoid_ring/newring.ml474
14 files changed, 121 insertions, 222 deletions
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 563148872..9ae8fcbf6 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -78,7 +78,8 @@ let gen_ground_tac flag taco ids bases gl=
| None-> snd (default_solver ()) in
let startseq gl=
let seq=empty_seq !ground_depth in
- extend_with_auto_hints bases (extend_with_ref_list ids seq gl) gl in
+ let seq,gl = extend_with_ref_list ids seq gl in
+ extend_with_auto_hints bases seq gl in
let result=ground_tac (Proofview.V82.of_tactic solver) startseq gl in
qflag:=backup;result
with reraise -> qflag:=backup;raise reraise
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index e0f4fa95f..3faf7f802 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -119,5 +119,6 @@ let ground_tac solver startseq gl=
end
with Heap.EmptyHeap->solver
end gl in
- wrap (List.length (pf_hyps gl)) true (toptac []) (startseq gl) gl
+ let seq, gl' = startseq gl in
+ wrap (List.length (pf_hyps gl)) true (toptac []) seq gl'
diff --git a/plugins/firstorder/ground.mli b/plugins/firstorder/ground.mli
index 8b2ba20c1..f4a6ff48a 100644
--- a/plugins/firstorder/ground.mli
+++ b/plugins/firstorder/ground.mli
@@ -7,5 +7,5 @@
(************************************************************************)
val ground_tac: Tacmach.tactic ->
- (Proof_type.goal Tacmach.sigma -> Sequent.t) -> Tacmach.tactic
+ (Proof_type.goal Tacmach.sigma -> Sequent.t * Proof_type.goal Tacmach.sigma) -> Tacmach.tactic
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index c6db6a49f..11b120c41 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -101,14 +101,12 @@ let dummy_constr=mkMeta (-1)
let dummy_bvid=Id.of_string "x"
-let constr_of_global = Universes.constr_of_global
-
-let mk_open_instance id gl m t=
+let mk_open_instance id idc gl m t=
let env=pf_env gl in
let evmap=Refiner.project gl in
let var_id=
if id==dummy_id then dummy_bvid else
- let typ=pf_type_of gl (constr_of_global id) in
+ let typ=pf_type_of gl idc in
(* since we know we will get a product,
reduction is not too expensive *)
let (nam,_,_)=destProd (whd_betadeltaiota env evmap typ) in
@@ -146,9 +144,10 @@ let left_instance_tac (inst,id) continue seq=
tclTHENS (Proofview.V82.of_tactic (cut dom))
[tclTHENLIST
[Proofview.V82.of_tactic introf;
+ pf_constr_of_global id (fun idc ->
(fun gls->generalize
- [mkApp(constr_of_global id,
- [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls);
+ [mkApp(idc,
+ [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls));
Proofview.V82.of_tactic introf;
tclSOLVE [wrap 1 false continue
(deepen (record (id,None) seq))]];
@@ -159,14 +158,16 @@ let left_instance_tac (inst,id) continue seq=
else
let special_generalize=
if m>0 then
- fun gl->
- let (rc,ot)= mk_open_instance id gl m t in
- let gt=
- it_mkLambda_or_LetIn
- (mkApp(constr_of_global id,[|ot|])) rc in
- generalize [gt] gl
+ pf_constr_of_global id (fun idc ->
+ fun gl->
+ let (rc,ot) = mk_open_instance id idc gl m t in
+ let gt=
+ it_mkLambda_or_LetIn
+ (mkApp(idc,[|ot|])) rc in
+ generalize [gt] gl)
else
- generalize [mkApp(constr_of_global id,[|t|])]
+ pf_constr_of_global id (fun idc ->
+ generalize [mkApp(idc,[|t|])])
in
tclTHENLIST
[special_generalize;
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 31a1e6cb0..996deb8c5 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -53,19 +53,19 @@ let clear_global=function
VarRef id->clear [id]
| _->tclIDTAC
-let constr_of_global = Universes.constr_of_global
(* connection rules *)
let axiom_tac t seq=
- try exact_no_check (constr_of_global (find_left t seq))
+ try pf_constr_of_global (find_left t seq) exact_no_check
with Not_found->tclFAIL 0 (Pp.str "No axiom link")
let ll_atom_tac a backtrack id continue seq=
tclIFTHENELSE
(try
tclTHENLIST
- [generalize [mkApp(constr_of_global id,
- [|constr_of_global (find_left a seq)|])];
+ [pf_constr_of_global (find_left a seq) (fun left ->
+ pf_constr_of_global id (fun id ->
+ generalize [mkApp(id, [|left|])]));
clear_global id;
Proofview.V82.of_tactic intro]
with Not_found->tclFAIL 0 (Pp.str "No link"))
@@ -92,7 +92,7 @@ let left_and_tac ind backtrack id continue seq gls=
let n=(construct_nhyps ind gls).(0) in
tclIFTHENELSE
(tclTHENLIST
- [Proofview.V82.of_tactic (simplest_elim (constr_of_global id));
+ [Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim);
clear_global id;
tclDO n (Proofview.V82.of_tactic intro)])
(wrap n false continue seq)
@@ -106,12 +106,12 @@ let left_or_tac ind backtrack id continue seq gls=
tclDO n (Proofview.V82.of_tactic intro);
wrap n false continue seq] in
tclIFTHENSVELSE
- (Proofview.V82.of_tactic (simplest_elim (constr_of_global id)))
+ (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim))
(Array.map f v)
backtrack gls
let left_false_tac id=
- Proofview.V82.of_tactic (simplest_elim (constr_of_global id))
+ Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim)
(* left arrow connective rules *)
@@ -120,29 +120,28 @@ let left_false_tac id=
let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl=
let rcs=ind_hyps 0 indu largs gl in
let vargs=Array.of_list largs in
- (* construire le terme H->B, le generaliser etc *)
- let myterm i=
+ (* construire le terme H->B, le generaliser etc *)
+ let myterm idc i=
let rc=rcs.(i) in
let p=List.length rc in
let cstr=mkApp ((mkConstructU ((ind,(i+1)),u)),vargs) in
let vars=Array.init p (fun j->mkRel (p-j)) in
let capply=mkApp ((lift p cstr),vars) in
- let head=mkApp ((lift p (constr_of_global id)),[|capply|]) in
- it_mkLambda_or_LetIn head rc in
+ let head=mkApp ((lift p idc),[|capply|]) in
+ it_mkLambda_or_LetIn head rc in
let lp=Array.length rcs in
- let newhyps=List.init lp myterm in
+ let newhyps idc =List.init lp (myterm idc) in
tclIFTHENELSE
(tclTHENLIST
- [generalize newhyps;
+ [pf_constr_of_global id (fun idc -> generalize (newhyps idc));
clear_global id;
tclDO lp (Proofview.V82.of_tactic intro)])
(wrap lp false continue seq) backtrack gl
let ll_arrow_tac a b c backtrack id continue seq=
let cc=mkProd(Anonymous,a,(lift 1 b)) in
- let d=mkLambda (Anonymous,b,
- mkApp ((constr_of_global id),
- [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
+ let d idc =mkLambda (Anonymous,b,
+ mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
tclORELSE
(tclTHENS (Proofview.V82.of_tactic (cut c))
[tclTHENLIST
@@ -150,9 +149,9 @@ let ll_arrow_tac a b c backtrack id continue seq=
clear_global id;
wrap 1 false continue seq];
tclTHENS (Proofview.V82.of_tactic (cut cc))
- [exact_no_check (constr_of_global id);
+ [pf_constr_of_global id exact_no_check;
tclTHENLIST
- [generalize [d];
+ [pf_constr_of_global id (fun idc -> generalize [d idc]);
clear_global id;
Proofview.V82.of_tactic introf;
Proofview.V82.of_tactic introf;
@@ -175,7 +174,7 @@ let forall_tac backtrack continue seq=
let left_exists_tac ind backtrack id continue seq gls=
let n=(construct_nhyps ind gls).(0) in
tclIFTHENELSE
- (Proofview.V82.of_tactic (simplest_elim (constr_of_global id)))
+ (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim))
(tclTHENLIST [clear_global id;
tclDO n (Proofview.V82.of_tactic intro);
(wrap (n-1) false continue seq)])
@@ -187,10 +186,11 @@ let ll_forall_tac prod backtrack id continue seq=
(tclTHENS (Proofview.V82.of_tactic (cut prod))
[tclTHENLIST
[Proofview.V82.of_tactic intro;
+ pf_constr_of_global id (fun idc ->
(fun gls->
let id0=pf_nth_hyp_id gls 1 in
- let term=mkApp((constr_of_global id),[|mkVar(id0)|]) in
- tclTHEN (generalize [term]) (clear [id0]) gls);
+ let term=mkApp(idc,[|mkVar(id0)|]) in
+ tclTHEN (generalize [term]) (clear [id0]) gls));
clear_global id;
Proofview.V82.of_tactic intro;
tclCOMPLETE (wrap 1 false continue (deepen seq))];
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index c0e5c7e58..43bb6dbbf 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -196,13 +196,13 @@ let expand_constructor_hints =
| gr ->
[gr])
-let extend_with_ref_list l seq gl=
+let extend_with_ref_list l seq gl =
let l = expand_constructor_hints l in
- let f gr seq=
- let c=Universes.constr_of_global gr in
+ let f gr (seq,gl) =
+ let gl, c = pf_eapply Evd.fresh_global gl gr in
let typ=(pf_type_of gl c) in
- add_formula Hyp gr typ seq gl in
- List.fold_right f l seq
+ (add_formula Hyp gr typ seq gl,gl) in
+ List.fold_right f l (seq,gl)
open Auto
@@ -227,7 +227,7 @@ let extend_with_auto_hints l seq gl=
error ("Firstorder: "^dbname^" : No such Hint database") in
Hint_db.iter g hdb in
List.iter h l;
- !seqref
+ !seqref, gl (*FIXME: forgetting about universes*)
let print_cmap map=
let print_entry c l s=
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 536ee7cc3..40aa169ab 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -54,9 +54,9 @@ val take_formula : t -> Formula.t * t
val empty_seq : int -> t
val extend_with_ref_list : global_reference list ->
- t -> Proof_type.goal sigma -> t
+ t -> Proof_type.goal sigma -> t * Proof_type.goal sigma
val extend_with_auto_hints : Auto.hint_db_name list ->
- t -> Proof_type.goal sigma -> t
+ t -> Proof_type.goal sigma -> t * Proof_type.goal sigma
val print_cmap: global_reference list CM.t -> Pp.std_ppcmds
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 88693c196..05cdd288c 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -645,7 +645,7 @@ let build_case_scheme fa =
(* Constrintern.global_reference id *)
(* in *)
let funs = (fun (_,f,_) ->
- try Universes.constr_of_global (Nametab.global f)
+ try Universes.unsafe_constr_of_global (Nametab.global f)
with Not_found ->
Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in
let first_fun,u = destConst funs in
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 3802aa365..90282fcf7 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -163,7 +163,7 @@ VERNAC COMMAND EXTEND Function
(Vernacexpr.VernacFixpoint(None, List.map snd recsl))
with
| Vernacexpr.VtSideff ids, _ when hard ->
- Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
+ Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids, false), VtLater)
| x -> x ]
-> [ do_generate_principle false (List.map snd recsl) ]
END
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index d98f824e8..d6ad5575b 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -181,6 +181,7 @@ let is_rec names =
let rec lookup names = function
| GVar(_,id) -> check_id id names
| GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> false
+ | GProj (loc, p, c) -> lookup names c
| GCast(_,b,_) -> lookup names b
| GProj _ -> error "GProj not handled"
| GRec _ -> error "GRec not handled"
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 8cccb0bed..5d9c226b7 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -166,7 +166,7 @@ let save with_clean id const (locality,_,kind) hook =
let cook_proof _ =
- let (id,(entry,strength)) = Pfedit.cook_proof () in
+ let (id,(entry,_,strength)) = Pfedit.cook_proof () in
(id,(entry,strength))
let get_proof_clean do_reduce =
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 96bf4c921..50e7507f4 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -75,7 +75,7 @@ let type_of_const t =
Const sp -> Typeops.type_of_constant (Global.env()) sp
|_ -> assert false
-let constr_of_global = Universes.constr_of_global
+let constr_of_global = Universes.unsafe_constr_of_global
let constant sl s = constr_of_global (find_reference sl s)
@@ -1016,7 +1016,7 @@ let compute_terminate_type nb_args func =
delayed_force nat,
(mkProd (Name k_id, delayed_force nat,
mkArrow cond result))))|])in
- let value = mkApp(delayed_force coq_sig,
+ let value = mkApp(constr_of_global (delayed_force coq_sig_ref),
[|b;
(mkLambda (Name v_id, b, nb_iter))|]) in
compose_prod rev_args value
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index 2b9dce1b0..de308c296 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 ae05fbdc3..8df061870 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)
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-22 13:36:40 +0000