aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/ring
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/ring')
-rw-r--r--contrib/ring/ArithRing.v9
-rw-r--r--contrib/ring/LegacyRing.v (renamed from contrib/ring/Ring.v)6
-rw-r--r--contrib/ring/NArithRing.v8
-rw-r--r--contrib/ring/Ring_abstract.v8
-rw-r--r--contrib/ring/Ring_normalize.v8
-rw-r--r--contrib/ring/Ring_theory.v18
-rw-r--r--contrib/ring/ZArithRing.v2
-rw-r--r--contrib/ring/g_ring.ml415
-rw-r--r--contrib/ring/quote.ml2
-rw-r--r--contrib/ring/ring.ml2
10 files changed, 41 insertions, 37 deletions
diff --git a/contrib/ring/ArithRing.v b/contrib/ring/ArithRing.v
index 0d42dabfd..959d66c74 100644
--- a/contrib/ring/ArithRing.v
+++ b/contrib/ring/ArithRing.v
@@ -10,7 +10,8 @@
(* Instantiation of the Ring tactic for the naturals of Arith $*)
-Require Export Ring.
+Require Import Bool.
+Require Export LegacyRing.
Require Export Arith.
Require Import Eqdep_dec.
@@ -36,12 +37,12 @@ Hint Resolve nateq_prop: arithring.
Definition NatTheory : Semi_Ring_Theory plus mult 1 0 nateq.
split; intros; auto with arith arithring.
- apply (fun n m p:nat => plus_reg_l m p n) with (n := n).
- trivial.
+(* apply (fun n m p:nat => plus_reg_l m p n) with (n := n).
+ trivial.*)
Defined.
-Add Semi Ring nat plus mult 1 0 nateq NatTheory [ 0 S ].
+Add Legacy Semi Ring nat plus mult 1 0 nateq NatTheory [ 0 S ].
Goal forall n:nat, S n = 1 + n.
intro; reflexivity.
diff --git a/contrib/ring/Ring.v b/contrib/ring/LegacyRing.v
index d0c2b7da3..667e24d53 100644
--- a/contrib/ring/Ring.v
+++ b/contrib/ring/LegacyRing.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: Ring.v 5920 2004-07-16 20:01:26Z herbelin $ *)
Require Export Bool.
Require Export Ring_theory.
@@ -32,5 +32,5 @@ destruct n; destruct m; destruct p; reflexivity.
destruct x; destruct y; reflexivity || simpl in |- *; tauto.
Defined.
-Add Ring bool xorb andb true false (fun b:bool => b) eqb BoolTheory
- [ true false ]. \ No newline at end of file
+Add Legacy Ring bool xorb andb true false (fun b:bool => b) eqb BoolTheory
+ [ true false ].
diff --git a/contrib/ring/NArithRing.v b/contrib/ring/NArithRing.v
index 41e3a7d7b..ee9fb3761 100644
--- a/contrib/ring/NArithRing.v
+++ b/contrib/ring/NArithRing.v
@@ -10,7 +10,8 @@
(* Instantiation of the Ring tactic for the binary natural numbers *)
-Require Export Ring.
+Require Import Bool.
+Require Export LegacyRing.
Require Export ZArith_base.
Require Import NArith.
Require Import Eqdep_dec.
@@ -37,8 +38,9 @@ Definition NTheory : Semi_Ring_Theory Nplus Nmult 1%N 0%N Neq.
apply Nmult_1_l.
apply Nmult_0_l.
apply Nmult_plus_distr_r.
- apply Nplus_reg_l.
+(* apply Nplus_reg_l.*)
apply Neq_prop.
Qed.
-Add Semi Ring N Nplus Nmult 1%N 0%N Neq NTheory [ Npos 0%N xO xI 1%positive ].
+Add Legacy Semi Ring
+ N Nplus Nmult 1%N 0%N Neq NTheory [ Npos 0%N xO xI 1%positive ].
diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v
index 5d5046393..574c24421 100644
--- a/contrib/ring/Ring_abstract.v
+++ b/contrib/ring/Ring_abstract.v
@@ -129,7 +129,7 @@ Hint Resolve (SR_mult_zero_left T).
Hint Resolve (SR_mult_zero_left2 T).
Hint Resolve (SR_distr_left T).
Hint Resolve (SR_distr_left2 T).
-Hint Resolve (SR_plus_reg_left T).
+(*Hint Resolve (SR_plus_reg_left T).*)
Hint Resolve (SR_plus_permute T).
Hint Resolve (SR_mult_permute T).
Hint Resolve (SR_distr_right T).
@@ -140,7 +140,7 @@ Hint Resolve (SR_plus_zero_right T).
Hint Resolve (SR_plus_zero_right2 T).
Hint Resolve (SR_mult_one_right T).
Hint Resolve (SR_mult_one_right2 T).
-Hint Resolve (SR_plus_reg_right T).
+(*Hint Resolve (SR_plus_reg_right T).*)
Hint Resolve refl_equal sym_equal trans_equal.
(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
Hint Immediate T.
@@ -439,7 +439,7 @@ Hint Resolve (Th_mult_zero_left T).
Hint Resolve (Th_mult_zero_left2 T).
Hint Resolve (Th_distr_left T).
Hint Resolve (Th_distr_left2 T).
-Hint Resolve (Th_plus_reg_left T).
+(*Hint Resolve (Th_plus_reg_left T).*)
Hint Resolve (Th_plus_permute T).
Hint Resolve (Th_mult_permute T).
Hint Resolve (Th_distr_right T).
@@ -449,7 +449,7 @@ Hint Resolve (Th_plus_zero_right T).
Hint Resolve (Th_plus_zero_right2 T).
Hint Resolve (Th_mult_one_right T).
Hint Resolve (Th_mult_one_right2 T).
-Hint Resolve (Th_plus_reg_right T).
+(*Hint Resolve (Th_plus_reg_right T).*)
Hint Resolve refl_equal sym_equal trans_equal.
(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
Hint Immediate T.
diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v
index bd22fa39a..6d0d05778 100644
--- a/contrib/ring/Ring_normalize.v
+++ b/contrib/ring/Ring_normalize.v
@@ -356,7 +356,7 @@ Hint Resolve (SR_mult_zero_left T).
Hint Resolve (SR_mult_zero_left2 T).
Hint Resolve (SR_distr_left T).
Hint Resolve (SR_distr_left2 T).
-Hint Resolve (SR_plus_reg_left T).
+(*Hint Resolve (SR_plus_reg_left T).*)
Hint Resolve (SR_plus_permute T).
Hint Resolve (SR_mult_permute T).
Hint Resolve (SR_distr_right T).
@@ -367,7 +367,7 @@ Hint Resolve (SR_plus_zero_right T).
Hint Resolve (SR_plus_zero_right2 T).
Hint Resolve (SR_mult_one_right T).
Hint Resolve (SR_mult_one_right2 T).
-Hint Resolve (SR_plus_reg_right T).
+(*Hint Resolve (SR_plus_reg_right T).*)
Hint Resolve refl_equal sym_equal trans_equal.
(* Hints Resolve refl_eqT sym_eqT trans_eqT. *)
Hint Immediate T.
@@ -785,7 +785,7 @@ Hint Resolve (Th_mult_zero_left T).
Hint Resolve (Th_mult_zero_left2 T).
Hint Resolve (Th_distr_left T).
Hint Resolve (Th_distr_left2 T).
-Hint Resolve (Th_plus_reg_left T).
+(*Hint Resolve (Th_plus_reg_left T).*)
Hint Resolve (Th_plus_permute T).
Hint Resolve (Th_mult_permute T).
Hint Resolve (Th_distr_right T).
@@ -796,7 +796,7 @@ Hint Resolve (Th_plus_zero_right T).
Hint Resolve (Th_plus_zero_right2 T).
Hint Resolve (Th_mult_one_right T).
Hint Resolve (Th_mult_one_right2 T).
-Hint Resolve (Th_plus_reg_right T).
+(*Hint Resolve (Th_plus_reg_right T).*)
Hint Resolve refl_equal sym_equal trans_equal.
(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
Hint Immediate T.
diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v
index 31cc274b2..192ff1f57 100644
--- a/contrib/ring/Ring_theory.v
+++ b/contrib/ring/Ring_theory.v
@@ -39,7 +39,7 @@ Record Semi_Ring_Theory : Prop :=
SR_mult_one_left : forall n:A, 1 * n = n;
SR_mult_zero_left : forall n:A, 0 * n = 0;
SR_distr_left : forall n m p:A, (n + m) * p = n * p + m * p;
- SR_plus_reg_left : forall n m p:A, n + m = n + p -> m = p;
+(* SR_plus_reg_left : forall n m p:A, n + m = n + p -> m = p;*)
SR_eq_prop : forall x y:A, Is_true (Aeq x y) -> x = y}.
Variable T : Semi_Ring_Theory.
@@ -52,10 +52,10 @@ Let plus_zero_left := SR_plus_zero_left T.
Let mult_one_left := SR_mult_one_left T.
Let mult_zero_left := SR_mult_zero_left T.
Let distr_left := SR_distr_left T.
-Let plus_reg_left := SR_plus_reg_left T.
+(*Let plus_reg_left := SR_plus_reg_left T.*)
Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left
- mult_one_left mult_zero_left distr_left plus_reg_left.
+ mult_one_left mult_zero_left distr_left (*plus_reg_left*).
(* Lemmas whose form is x=y are also provided in form y=x because Auto does
not symmetry *)
@@ -126,11 +126,11 @@ Qed.
Lemma SR_mult_one_right2 : forall n:A, n = n * 1.
intro; elim mult_comm; auto.
Qed.
-
+(*
Lemma SR_plus_reg_right : forall n m p:A, m + n = p + n -> m = p.
intros n m p; rewrite (plus_comm m n); rewrite (plus_comm p n); eauto.
Qed.
-
+*)
End Theory_of_semi_rings.
Section Theory_of_rings.
@@ -320,7 +320,7 @@ symmetry in |- *; apply Th_mult_opp_opp. Qed.
Lemma Th_opp_zero : - 0 = 0.
rewrite <- (plus_zero_left (- 0)).
auto. Qed.
-
+(*
Lemma Th_plus_reg_left : forall n m p:A, n + m = n + p -> m = p.
intros; generalize (f_equal (fun z => - n + z) H).
repeat rewrite plus_assoc.
@@ -336,7 +336,7 @@ rewrite (plus_comm n m).
rewrite (plus_comm n p).
auto.
Qed.
-
+*)
Lemma Th_distr_right : forall n m p:A, n * (m + p) = n * m + n * p.
intros.
repeat rewrite (mult_comm n).
@@ -349,7 +349,7 @@ Qed.
End Theory_of_rings.
-Hint Resolve Th_mult_zero_left Th_plus_reg_left: core.
+Hint Resolve Th_mult_zero_left (*Th_plus_reg_left*): core.
Unset Implicit Arguments.
@@ -373,4 +373,4 @@ End product_ring.
Section power_ring.
-End power_ring. \ No newline at end of file
+End power_ring.
diff --git a/contrib/ring/ZArithRing.v b/contrib/ring/ZArithRing.v
index 9324fb602..075431827 100644
--- a/contrib/ring/ZArithRing.v
+++ b/contrib/ring/ZArithRing.v
@@ -32,5 +32,5 @@ Definition ZTheory : Ring_Theory Zplus Zmult 1%Z 0%Z Zopp Zeq.
Qed.
(* NatConstants and NatTheory are defined in Ring_theory.v *)
-Add Ring Z Zplus Zmult 1%Z 0%Z Zopp Zeq ZTheory
+Add Legacy Ring Z Zplus Zmult 1%Z 0%Z Zopp Zeq ZTheory
[ Zpos Zneg 0%Z xO xI 1%positive ].
diff --git a/contrib/ring/g_ring.ml4 b/contrib/ring/g_ring.ml4
index 0cb86dfdd..5ca1bfced 100644
--- a/contrib/ring/g_ring.ml4
+++ b/contrib/ring/g_ring.ml4
@@ -12,9 +12,10 @@
open Quote
open Ring
+open Tacticals
TACTIC EXTEND ring
- [ "ring" constr_list(l) ] -> [ polynom l ]
+| [ "legacy" "ring" constr_list(l) ] -> [ polynom l ]
END
(* The vernac commands "Add Ring" and co *)
@@ -23,7 +24,7 @@ let cset_of_constrarg_list l =
List.fold_right ConstrSet.add (List.map constr_of l) ConstrSet.empty
VERNAC COMMAND EXTEND AddRing
- [ "Add" "Ring"
+ [ "Add" "Legacy" "Ring"
constr(a) constr(aplus) constr(amult) constr(aone) constr(azero)
constr(aopp) constr(aeq) constr(t) "[" ne_constr_list(l) "]" ]
-> [ add_theory true false false
@@ -40,7 +41,7 @@ VERNAC COMMAND EXTEND AddRing
(constr_of t)
(cset_of_constrarg_list l) ]
-| [ "Add" "Semi" "Ring"
+| [ "Add" "Legacy" "Semi" "Ring"
constr(a) constr(aplus) constr(amult) constr(aone) constr(azero)
constr(aeq) constr(t) "[" ne_constr_list(l) "]" ]
-> [ add_theory false false false
@@ -57,7 +58,7 @@ VERNAC COMMAND EXTEND AddRing
(constr_of t)
(cset_of_constrarg_list l) ]
-| [ "Add" "Abstract" "Ring"
+| [ "Add" "Legacy" "Abstract" "Ring"
constr(a) constr(aplus) constr(amult) constr(aone)
constr(azero) constr(aopp) constr(aeq) constr(t) ]
-> [ add_theory true true false
@@ -74,7 +75,7 @@ VERNAC COMMAND EXTEND AddRing
(constr_of t)
ConstrSet.empty ]
-| [ "Add" "Abstract" "Semi" "Ring"
+| [ "Add" "Legacy" "Abstract" "Semi" "Ring"
constr(a) constr(aplus) constr(amult) constr(aone)
constr(azero) constr(aeq) constr(t) ]
-> [ add_theory false true false
@@ -91,7 +92,7 @@ VERNAC COMMAND EXTEND AddRing
(constr_of t)
ConstrSet.empty ]
-| [ "Add" "Setoid" "Ring"
+| [ "Add" "Legacy" "Setoid" "Ring"
constr(a) constr(aequiv) constr(asetth) constr(aplus) constr(amult)
constr(aone) constr(azero) constr(aopp) constr(aeq) constr(pm)
constr(mm) constr(om) constr(t) "[" ne_constr_list(l) "]" ]
@@ -112,7 +113,7 @@ VERNAC COMMAND EXTEND AddRing
(constr_of t)
(cset_of_constrarg_list l) ]
-| [ "Add" "Semi" "Setoid" "Ring"
+| [ "Add" "Legacy" "Semi" "Setoid" "Ring"
constr(a) constr(aequiv) constr(asetth) constr(aplus)
constr(amult) constr(aone) constr(azero) constr(aeq)
constr(pm) constr(mm) constr(t) "[" ne_constr_list(l) "]" ]
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index 3b937c7a6..3c1645d47 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -298,7 +298,7 @@ let rec closed_under cset t =
(ConstrSet.mem t cset) or
(match (kind_of_term t) with
| Cast(c,_,_) -> closed_under cset c
- | App(f,l) -> closed_under cset f & array_for_all (closed_under cset) l
+ | App(f,l) -> closed_under cset f && array_for_all (closed_under cset) l
| _ -> false)
(*s [btree_of_array [| c1; c2; c3; c4; c5 |]] builds the complete
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 48e8763d5..1c5121ef6 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -885,7 +885,7 @@ let match_with_equiv c = match (kind_of_term c) with
| _ -> None
let polynom lc gl =
- Coqlib.check_required_library ["Coq";"ring";"Ring"];
+ Coqlib.check_required_library ["Coq";"ring";"LegacyRing"];
match lc with
(* If no argument is given, try to recognize either an equality or
a declared relation with arguments c1 ... cn,
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 18:31:20 +0000