diff options
Diffstat (limited to 'contrib/ring')
| -rw-r--r-- | contrib/ring/LegacyArithRing.v (renamed from contrib/ring/ArithRing.v) | 11 | ||||
| -rw-r--r-- | contrib/ring/LegacyNArithRing.v (renamed from contrib/ring/NArithRing.v) | 10 | ||||
| -rw-r--r-- | contrib/ring/LegacyRing.v (renamed from contrib/ring/Ring.v) | 6 | ||||
| -rw-r--r-- | contrib/ring/LegacyRing_theory.v (renamed from contrib/ring/Ring_theory.v) | 20 | ||||
| -rw-r--r-- | contrib/ring/LegacyZArithRing.v (renamed from contrib/ring/ZArithRing.v) | 7 | ||||
| -rw-r--r-- | contrib/ring/Ring_abstract.v | 12 | ||||
| -rw-r--r-- | contrib/ring/Ring_normalize.v | 12 | ||||
| -rw-r--r-- | contrib/ring/g_ring.ml4 | 17 | ||||
| -rw-r--r-- | contrib/ring/quote.ml | 4 | ||||
| -rw-r--r-- | contrib/ring/ring.ml | 6 |
10 files changed, 55 insertions, 50 deletions
diff --git a/contrib/ring/ArithRing.v b/contrib/ring/LegacyArithRing.v index 68464c10..e062b731 100644 --- a/contrib/ring/ArithRing.v +++ b/contrib/ring/LegacyArithRing.v @@ -6,11 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ArithRing.v 6295 2004-11-12 16:40:39Z gregoire $ *) +(* $Id: LegacyArithRing.v 9179 2006-09-26 12:13:06Z barras $ *) (* 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/NArithRing.v b/contrib/ring/LegacyNArithRing.v index 878346ba..c689fc40 100644 --- a/contrib/ring/NArithRing.v +++ b/contrib/ring/LegacyNArithRing.v @@ -6,11 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: NArithRing.v 6295 2004-11-12 16:40:39Z gregoire $ *) +(* $Id: LegacyNArithRing.v 9179 2006-09-26 12:13:06Z barras $ *) (* 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.v b/contrib/ring/LegacyRing.v index 6572e79a..dc8635bd 100644 --- a/contrib/ring/Ring.v +++ b/contrib/ring/LegacyRing.v @@ -9,7 +9,7 @@ (* $Id: Ring.v 5920 2004-07-16 20:01:26Z herbelin $ *) Require Export Bool. -Require Export Ring_theory. +Require Export LegacyRing_theory. Require Export Quote. Require Export Ring_normalize. Require Export Ring_abstract. @@ -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/Ring_theory.v b/contrib/ring/LegacyRing_theory.v index 5536294e..5df927a6 100644 --- a/contrib/ring/Ring_theory.v +++ b/contrib/ring/LegacyRing_theory.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Ring_theory.v 5920 2004-07-16 20:01:26Z herbelin $ *) +(* $Id: LegacyRing_theory.v 9179 2006-09-26 12:13:06Z barras $ *) Require Export Bool. @@ -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/LegacyZArithRing.v index 3999b632..a410fbc5 100644 --- a/contrib/ring/ZArithRing.v +++ b/contrib/ring/LegacyZArithRing.v @@ -6,13 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ZArithRing.v 6295 2004-11-12 16:40:39Z gregoire $ *) +(* $Id: LegacyZArithRing.v 9181 2006-09-26 16:38:33Z barras $ *) (* Instantiation of the Ring tactic for the binary integers of ZArith *) -Require Export ArithRing. +Require Export LegacyArithRing. Require Export ZArith_base. Require Import Eqdep_dec. +Require Import LegacyRing. Unboxed Definition Zeq (x y:Z) := match (x ?= y)%Z with @@ -32,5 +33,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/Ring_abstract.v b/contrib/ring/Ring_abstract.v index c0818da8..115ed5ca 100644 --- a/contrib/ring/Ring_abstract.v +++ b/contrib/ring/Ring_abstract.v @@ -6,9 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Ring_abstract.v 6295 2004-11-12 16:40:39Z gregoire $ *) +(* $Id: Ring_abstract.v 9179 2006-09-26 12:13:06Z barras $ *) -Require Import Ring_theory. +Require Import LegacyRing_theory. Require Import Quote. Require Import Ring_normalize. @@ -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 7b40328a..4a082396 100644 --- a/contrib/ring/Ring_normalize.v +++ b/contrib/ring/Ring_normalize.v @@ -6,9 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Ring_normalize.v 6295 2004-11-12 16:40:39Z gregoire $ *) +(* $Id: Ring_normalize.v 9179 2006-09-26 12:13:06Z barras $ *) -Require Import Ring_theory. +Require Import LegacyRing_theory. Require Import Quote. Set Implicit Arguments. @@ -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/g_ring.ml4 b/contrib/ring/g_ring.ml4 index dccd1944..2f964988 100644 --- a/contrib/ring/g_ring.ml4 +++ b/contrib/ring/g_ring.ml4 @@ -8,13 +8,14 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: g_ring.ml4 7734 2005-12-26 14:06:51Z herbelin $ *) +(* $Id: g_ring.ml4 9178 2006-09-26 11:18:22Z barras $ *) 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 462e5ed8..e0a6cba3 100644 --- a/contrib/ring/quote.ml +++ b/contrib/ring/quote.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: quote.ml 7639 2005-12-02 10:01:15Z gregoire $ *) +(* $Id: quote.ml 9178 2006-09-26 11:18:22Z barras $ *) (* The `Quote' tactic *) @@ -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 5251dcc5..6b82b75b 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ring.ml 7837 2006-01-11 09:47:32Z herbelin $ *) +(* $Id: ring.ml 9179 2006-09-26 12:13:06Z barras $ *) (* ML part of the Ring tactic *) @@ -43,7 +43,7 @@ let ring_dir = ["Coq";"ring"] let setoids_dir = ["Coq";"Setoids"] let ring_constant = Coqlib.gen_constant_in_modules "Ring" - [ring_dir@["Ring_theory"]; + [ring_dir@["LegacyRing_theory"]; ring_dir@["Setoid_ring_theory"]; ring_dir@["Ring_normalize"]; ring_dir@["Ring_abstract"]; @@ -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, |