From 4aec8fda1161953cf929b4e282eea9b672ab4058 Mon Sep 17 00:00:00 2001 From: barras Date: Tue, 26 Sep 2006 12:13:06 +0000 Subject: commit de field + renommages git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9179 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/ring/ArithRing.v | 90 ---------- contrib/ring/LegacyArithRing.v | 90 ++++++++++ contrib/ring/LegacyNArithRing.v | 46 +++++ contrib/ring/LegacyRing.v | 2 +- contrib/ring/LegacyRing_theory.v | 376 +++++++++++++++++++++++++++++++++++++++ contrib/ring/LegacyZArithRing.v | 36 ++++ contrib/ring/NArithRing.v | 46 ----- contrib/ring/Ring_abstract.v | 2 +- contrib/ring/Ring_normalize.v | 2 +- contrib/ring/Ring_theory.v | 376 --------------------------------------- contrib/ring/ZArithRing.v | 36 ---- contrib/ring/ring.ml | 2 +- 12 files changed, 552 insertions(+), 552 deletions(-) delete mode 100644 contrib/ring/ArithRing.v create mode 100644 contrib/ring/LegacyArithRing.v create mode 100644 contrib/ring/LegacyNArithRing.v create mode 100644 contrib/ring/LegacyRing_theory.v create mode 100644 contrib/ring/LegacyZArithRing.v delete mode 100644 contrib/ring/NArithRing.v delete mode 100644 contrib/ring/Ring_theory.v delete mode 100644 contrib/ring/ZArithRing.v (limited to 'contrib/ring') diff --git a/contrib/ring/ArithRing.v b/contrib/ring/ArithRing.v deleted file mode 100644 index 959d66c749..0000000000 --- a/contrib/ring/ArithRing.v +++ /dev/null @@ -1,90 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* true - | S n', S m' => nateq n' m' - | _, _ => false - end. - -Lemma nateq_prop : forall n m:nat, Is_true (nateq n m) -> n = m. -Proof. - simple induction n; simple induction m; intros; try contradiction. - trivial. - unfold Is_true in H1. - rewrite (H n1 H1). - trivial. -Qed. - -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.*) -Defined. - - -Add Legacy Semi Ring nat plus mult 1 0 nateq NatTheory [ 0 S ]. - -Goal forall n:nat, S n = 1 + n. -intro; reflexivity. -Save S_to_plus_one. - -(* Replace all occurrences of (S exp) by (plus (S O) exp), except when - exp is already O and only for those occurrences than can be reached by going - down plus and mult operations *) -Ltac rewrite_S_to_plus_term t := - match constr:t with - | 1 => constr:1 - | (S ?X1) => - let t1 := rewrite_S_to_plus_term X1 in - constr:(1 + t1) - | (?X1 + ?X2) => - let t1 := rewrite_S_to_plus_term X1 - with t2 := rewrite_S_to_plus_term X2 in - constr:(t1 + t2) - | (?X1 * ?X2) => - let t1 := rewrite_S_to_plus_term X1 - with t2 := rewrite_S_to_plus_term X2 in - constr:(t1 * t2) - | _ => constr:t - end. - -(* Apply S_to_plus on both sides of an equality *) -Ltac rewrite_S_to_plus := - match goal with - | |- (?X1 = ?X2) => - try - let t1 := - (**) (**) - rewrite_S_to_plus_term X1 - with t2 := rewrite_S_to_plus_term X2 in - change (t1 = t2) in |- * - | |- (?X1 = ?X2) => - try - let t1 := - (**) (**) - rewrite_S_to_plus_term X1 - with t2 := rewrite_S_to_plus_term X2 in - change (t1 = t2) in |- * - end. - -Ltac ring_nat := rewrite_S_to_plus; ring. diff --git a/contrib/ring/LegacyArithRing.v b/contrib/ring/LegacyArithRing.v new file mode 100644 index 0000000000..959d66c749 --- /dev/null +++ b/contrib/ring/LegacyArithRing.v @@ -0,0 +1,90 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* true + | S n', S m' => nateq n' m' + | _, _ => false + end. + +Lemma nateq_prop : forall n m:nat, Is_true (nateq n m) -> n = m. +Proof. + simple induction n; simple induction m; intros; try contradiction. + trivial. + unfold Is_true in H1. + rewrite (H n1 H1). + trivial. +Qed. + +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.*) +Defined. + + +Add Legacy Semi Ring nat plus mult 1 0 nateq NatTheory [ 0 S ]. + +Goal forall n:nat, S n = 1 + n. +intro; reflexivity. +Save S_to_plus_one. + +(* Replace all occurrences of (S exp) by (plus (S O) exp), except when + exp is already O and only for those occurrences than can be reached by going + down plus and mult operations *) +Ltac rewrite_S_to_plus_term t := + match constr:t with + | 1 => constr:1 + | (S ?X1) => + let t1 := rewrite_S_to_plus_term X1 in + constr:(1 + t1) + | (?X1 + ?X2) => + let t1 := rewrite_S_to_plus_term X1 + with t2 := rewrite_S_to_plus_term X2 in + constr:(t1 + t2) + | (?X1 * ?X2) => + let t1 := rewrite_S_to_plus_term X1 + with t2 := rewrite_S_to_plus_term X2 in + constr:(t1 * t2) + | _ => constr:t + end. + +(* Apply S_to_plus on both sides of an equality *) +Ltac rewrite_S_to_plus := + match goal with + | |- (?X1 = ?X2) => + try + let t1 := + (**) (**) + rewrite_S_to_plus_term X1 + with t2 := rewrite_S_to_plus_term X2 in + change (t1 = t2) in |- * + | |- (?X1 = ?X2) => + try + let t1 := + (**) (**) + rewrite_S_to_plus_term X1 + with t2 := rewrite_S_to_plus_term X2 in + change (t1 = t2) in |- * + end. + +Ltac ring_nat := rewrite_S_to_plus; ring. diff --git a/contrib/ring/LegacyNArithRing.v b/contrib/ring/LegacyNArithRing.v new file mode 100644 index 0000000000..ee9fb37615 --- /dev/null +++ b/contrib/ring/LegacyNArithRing.v @@ -0,0 +1,46 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* true + | _ => false + end. + +Lemma Neq_prop : forall n m:N, Is_true (Neq n m) -> n = m. + intros n m H; unfold Neq in H. + apply Ncompare_Eq_eq. + destruct (n ?= m)%N; [ reflexivity | contradiction | contradiction ]. +Qed. + +Definition NTheory : Semi_Ring_Theory Nplus Nmult 1%N 0%N Neq. + split. + apply Nplus_comm. + apply Nplus_assoc. + apply Nmult_comm. + apply Nmult_assoc. + apply Nplus_0_l. + apply Nmult_1_l. + apply Nmult_0_l. + apply Nmult_plus_distr_r. +(* apply Nplus_reg_l.*) + apply Neq_prop. +Qed. + +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/LegacyRing.v b/contrib/ring/LegacyRing.v index 667e24d535..dc8635bdf9 100644 --- a/contrib/ring/LegacyRing.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. diff --git a/contrib/ring/LegacyRing_theory.v b/contrib/ring/LegacyRing_theory.v new file mode 100644 index 0000000000..192ff1f571 --- /dev/null +++ b/contrib/ring/LegacyRing_theory.v @@ -0,0 +1,376 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* A -> A. +Variable Amult : A -> A -> A. +Variable Aone : A. +Variable Azero : A. +(* There is also a "weakly decidable" equality on A. That means + that if (A_eq x y)=true then x=y but x=y can arise when + (A_eq x y)=false. On an abstract ring the function [x,y:A]false + is a good choice. The proof of A_eq_prop is in this case easy. *) +Variable Aeq : A -> A -> bool. + +Infix "+" := Aplus (at level 50, left associativity). +Infix "*" := Amult (at level 40, left associativity). +Notation "0" := Azero. +Notation "1" := Aone. + +Record Semi_Ring_Theory : Prop := + {SR_plus_comm : forall n m:A, n + m = m + n; + SR_plus_assoc : forall n m p:A, n + (m + p) = n + m + p; + SR_mult_comm : forall n m:A, n * m = m * n; + SR_mult_assoc : forall n m p:A, n * (m * p) = n * m * p; + SR_plus_zero_left : forall n:A, 0 + n = n; + 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_eq_prop : forall x y:A, Is_true (Aeq x y) -> x = y}. + +Variable T : Semi_Ring_Theory. + +Let plus_comm := SR_plus_comm T. +Let plus_assoc := SR_plus_assoc T. +Let mult_comm := SR_mult_comm T. +Let mult_assoc := SR_mult_assoc T. +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.*) + +Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_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 *) +Lemma SR_mult_assoc2 : forall n m p:A, n * m * p = n * (m * p). +symmetry in |- *; eauto. Qed. + +Lemma SR_plus_assoc2 : forall n m p:A, n + m + p = n + (m + p). +symmetry in |- *; eauto. Qed. + +Lemma SR_plus_zero_left2 : forall n:A, n = 0 + n. +symmetry in |- *; eauto. Qed. + +Lemma SR_mult_one_left2 : forall n:A, n = 1 * n. +symmetry in |- *; eauto. Qed. + +Lemma SR_mult_zero_left2 : forall n:A, 0 = 0 * n. +symmetry in |- *; eauto. Qed. + +Lemma SR_distr_left2 : forall n m p:A, n * p + m * p = (n + m) * p. +symmetry in |- *; eauto. Qed. + +Lemma SR_plus_permute : forall n m p:A, n + (m + p) = m + (n + p). +intros. +rewrite plus_assoc. +elim (plus_comm m n). +rewrite <- plus_assoc. +reflexivity. +Qed. + +Lemma SR_mult_permute : forall n m p:A, n * (m * p) = m * (n * p). +intros. +rewrite mult_assoc. +elim (mult_comm m n). +rewrite <- mult_assoc. +reflexivity. +Qed. + +Hint Resolve SR_plus_permute SR_mult_permute. + +Lemma SR_distr_right : forall n m p:A, n * (m + p) = n * m + n * p. +intros. +repeat rewrite (mult_comm n). +eauto. +Qed. + +Lemma SR_distr_right2 : forall n m p:A, n * m + n * p = n * (m + p). +symmetry in |- *; apply SR_distr_right. Qed. + +Lemma SR_mult_zero_right : forall n:A, n * 0 = 0. +intro; rewrite mult_comm; eauto. +Qed. + +Lemma SR_mult_zero_right2 : forall n:A, 0 = n * 0. +intro; rewrite mult_comm; eauto. +Qed. + +Lemma SR_plus_zero_right : forall n:A, n + 0 = n. +intro; rewrite plus_comm; eauto. +Qed. +Lemma SR_plus_zero_right2 : forall n:A, n = n + 0. +intro; rewrite plus_comm; eauto. +Qed. + +Lemma SR_mult_one_right : forall n:A, n * 1 = n. +intro; elim mult_comm; auto. +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. + +Variable A : Type. + +Variable Aplus : A -> A -> A. +Variable Amult : A -> A -> A. +Variable Aone : A. +Variable Azero : A. +Variable Aopp : A -> A. +Variable Aeq : A -> A -> bool. + +Infix "+" := Aplus (at level 50, left associativity). +Infix "*" := Amult (at level 40, left associativity). +Notation "0" := Azero. +Notation "1" := Aone. +Notation "- x" := (Aopp x). + +Record Ring_Theory : Prop := + {Th_plus_comm : forall n m:A, n + m = m + n; + Th_plus_assoc : forall n m p:A, n + (m + p) = n + m + p; + Th_mult_sym : forall n m:A, n * m = m * n; + Th_mult_assoc : forall n m p:A, n * (m * p) = n * m * p; + Th_plus_zero_left : forall n:A, 0 + n = n; + Th_mult_one_left : forall n:A, 1 * n = n; + Th_opp_def : forall n:A, n + - n = 0; + Th_distr_left : forall n m p:A, (n + m) * p = n * p + m * p; + Th_eq_prop : forall x y:A, Is_true (Aeq x y) -> x = y}. + +Variable T : Ring_Theory. + +Let plus_comm := Th_plus_comm T. +Let plus_assoc := Th_plus_assoc T. +Let mult_comm := Th_mult_sym T. +Let mult_assoc := Th_mult_assoc T. +Let plus_zero_left := Th_plus_zero_left T. +Let mult_one_left := Th_mult_one_left T. +Let opp_def := Th_opp_def T. +Let distr_left := Th_distr_left T. + +Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left + mult_one_left opp_def distr_left. + +(* Lemmas whose form is x=y are also provided in form y=x because Auto does + not symmetry *) +Lemma Th_mult_assoc2 : forall n m p:A, n * m * p = n * (m * p). +symmetry in |- *; eauto. Qed. + +Lemma Th_plus_assoc2 : forall n m p:A, n + m + p = n + (m + p). +symmetry in |- *; eauto. Qed. + +Lemma Th_plus_zero_left2 : forall n:A, n = 0 + n. +symmetry in |- *; eauto. Qed. + +Lemma Th_mult_one_left2 : forall n:A, n = 1 * n. +symmetry in |- *; eauto. Qed. + +Lemma Th_distr_left2 : forall n m p:A, n * p + m * p = (n + m) * p. +symmetry in |- *; eauto. Qed. + +Lemma Th_opp_def2 : forall n:A, 0 = n + - n. +symmetry in |- *; eauto. Qed. + +Lemma Th_plus_permute : forall n m p:A, n + (m + p) = m + (n + p). +intros. +rewrite plus_assoc. +elim (plus_comm m n). +rewrite <- plus_assoc. +reflexivity. +Qed. + +Lemma Th_mult_permute : forall n m p:A, n * (m * p) = m * (n * p). +intros. +rewrite mult_assoc. +elim (mult_comm m n). +rewrite <- mult_assoc. +reflexivity. +Qed. + +Hint Resolve Th_plus_permute Th_mult_permute. + +Lemma aux1 : forall a:A, a + a = a -> a = 0. +intros. +generalize (opp_def a). +pattern a at 1 in |- *. +rewrite <- H. +rewrite <- plus_assoc. +rewrite opp_def. +elim plus_comm. +rewrite plus_zero_left. +trivial. +Qed. + +Lemma Th_mult_zero_left : forall n:A, 0 * n = 0. +intros. +apply aux1. +rewrite <- distr_left. +rewrite plus_zero_left. +reflexivity. +Qed. +Hint Resolve Th_mult_zero_left. + +Lemma Th_mult_zero_left2 : forall n:A, 0 = 0 * n. +symmetry in |- *; eauto. Qed. + +Lemma aux2 : forall x y z:A, x + y = 0 -> x + z = 0 -> y = z. +intros. +rewrite <- (plus_zero_left y). +elim H0. +elim plus_assoc. +elim (plus_comm y z). +rewrite plus_assoc. +rewrite H. +rewrite plus_zero_left. +reflexivity. +Qed. + +Lemma Th_opp_mult_left : forall x y:A, - (x * y) = - x * y. +intros. +apply (aux2 (x:=(x * y))); + [ apply opp_def | rewrite <- distr_left; rewrite opp_def; auto ]. +Qed. +Hint Resolve Th_opp_mult_left. + +Lemma Th_opp_mult_left2 : forall x y:A, - x * y = - (x * y). +symmetry in |- *; eauto. Qed. + +Lemma Th_mult_zero_right : forall n:A, n * 0 = 0. +intro; elim mult_comm; eauto. +Qed. + +Lemma Th_mult_zero_right2 : forall n:A, 0 = n * 0. +intro; elim mult_comm; eauto. +Qed. + +Lemma Th_plus_zero_right : forall n:A, n + 0 = n. +intro; rewrite plus_comm; eauto. +Qed. + +Lemma Th_plus_zero_right2 : forall n:A, n = n + 0. +intro; rewrite plus_comm; eauto. +Qed. + +Lemma Th_mult_one_right : forall n:A, n * 1 = n. +intro; elim mult_comm; eauto. +Qed. + +Lemma Th_mult_one_right2 : forall n:A, n = n * 1. +intro; elim mult_comm; eauto. +Qed. + +Lemma Th_opp_mult_right : forall x y:A, - (x * y) = x * - y. +intros; do 2 rewrite (mult_comm x); auto. +Qed. + +Lemma Th_opp_mult_right2 : forall x y:A, x * - y = - (x * y). +intros; do 2 rewrite (mult_comm x); auto. +Qed. + +Lemma Th_plus_opp_opp : forall x y:A, - x + - y = - (x + y). +intros. +apply (aux2 (x:=(x + y))); + [ elim plus_assoc; rewrite (Th_plus_permute y (- x)); rewrite plus_assoc; + rewrite opp_def; rewrite plus_zero_left; auto + | auto ]. +Qed. + +Lemma Th_plus_permute_opp : forall n m p:A, - m + (n + p) = n + (- m + p). +eauto. Qed. + +Lemma Th_opp_opp : forall n:A, - - n = n. +intro; apply (aux2 (x:=(- n))); [ auto | elim plus_comm; auto ]. +Qed. +Hint Resolve Th_opp_opp. + +Lemma Th_opp_opp2 : forall n:A, n = - - n. +symmetry in |- *; eauto. Qed. + +Lemma Th_mult_opp_opp : forall x y:A, - x * - y = x * y. +intros; rewrite <- Th_opp_mult_left; rewrite <- Th_opp_mult_right; auto. +Qed. + +Lemma Th_mult_opp_opp2 : forall x y:A, x * y = - x * - y. +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. +rewrite (plus_comm (- n) n). +rewrite opp_def. +repeat rewrite Th_plus_zero_left; eauto. +Qed. + +Lemma Th_plus_reg_right : forall n m p:A, m + n = p + n -> m = p. +intros. +eapply Th_plus_reg_left with n. +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). +eauto. +Qed. + +Lemma Th_distr_right2 : forall n m p:A, n * m + n * p = n * (m + p). +symmetry in |- *; apply Th_distr_right. +Qed. + +End Theory_of_rings. + +Hint Resolve Th_mult_zero_left (*Th_plus_reg_left*): core. + +Unset Implicit Arguments. + +Definition Semi_Ring_Theory_of : + forall (A:Type) (Aplus Amult:A -> A -> A) (Aone Azero:A) + (Aopp:A -> A) (Aeq:A -> A -> bool), + Ring_Theory Aplus Amult Aone Azero Aopp Aeq -> + Semi_Ring_Theory Aplus Amult Aone Azero Aeq. +intros until 1; case H. +split; intros; simpl in |- *; eauto. +Defined. + +(* Every ring can be viewed as a semi-ring : this property will be used + in Abstract_polynom. *) +Coercion Semi_Ring_Theory_of : Ring_Theory >-> Semi_Ring_Theory. + + +Section product_ring. + +End product_ring. + +Section power_ring. + +End power_ring. diff --git a/contrib/ring/LegacyZArithRing.v b/contrib/ring/LegacyZArithRing.v new file mode 100644 index 0000000000..075431827c --- /dev/null +++ b/contrib/ring/LegacyZArithRing.v @@ -0,0 +1,36 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* true + | _ => false + end. + +Lemma Zeq_prop : forall x y:Z, Is_true (Zeq x y) -> x = y. + intros x y H; unfold Zeq in H. + apply Zcompare_Eq_eq. + destruct (x ?= y)%Z; [ reflexivity | contradiction | contradiction ]. +Qed. + +Definition ZTheory : Ring_Theory Zplus Zmult 1%Z 0%Z Zopp Zeq. + split; intros; eauto with zarith. + apply Zeq_prop; assumption. +Qed. + +(* NatConstants and NatTheory are defined in Ring_theory.v *) +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/NArithRing.v b/contrib/ring/NArithRing.v deleted file mode 100644 index ee9fb37615..0000000000 --- a/contrib/ring/NArithRing.v +++ /dev/null @@ -1,46 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* true - | _ => false - end. - -Lemma Neq_prop : forall n m:N, Is_true (Neq n m) -> n = m. - intros n m H; unfold Neq in H. - apply Ncompare_Eq_eq. - destruct (n ?= m)%N; [ reflexivity | contradiction | contradiction ]. -Qed. - -Definition NTheory : Semi_Ring_Theory Nplus Nmult 1%N 0%N Neq. - split. - apply Nplus_comm. - apply Nplus_assoc. - apply Nmult_comm. - apply Nmult_assoc. - apply Nplus_0_l. - apply Nmult_1_l. - apply Nmult_0_l. - apply Nmult_plus_distr_r. -(* apply Nplus_reg_l.*) - apply Neq_prop. -Qed. - -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 574c24421f..28de54e658 100644 --- a/contrib/ring/Ring_abstract.v +++ b/contrib/ring/Ring_abstract.v @@ -8,7 +8,7 @@ (* $Id$ *) -Require Import Ring_theory. +Require Import LegacyRing_theory. Require Import Quote. Require Import Ring_normalize. diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v index 6d0d057780..199ae75721 100644 --- a/contrib/ring/Ring_normalize.v +++ b/contrib/ring/Ring_normalize.v @@ -8,7 +8,7 @@ (* $Id$ *) -Require Import Ring_theory. +Require Import LegacyRing_theory. Require Import Quote. Set Implicit Arguments. diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v deleted file mode 100644 index 192ff1f571..0000000000 --- a/contrib/ring/Ring_theory.v +++ /dev/null @@ -1,376 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* A -> A. -Variable Amult : A -> A -> A. -Variable Aone : A. -Variable Azero : A. -(* There is also a "weakly decidable" equality on A. That means - that if (A_eq x y)=true then x=y but x=y can arise when - (A_eq x y)=false. On an abstract ring the function [x,y:A]false - is a good choice. The proof of A_eq_prop is in this case easy. *) -Variable Aeq : A -> A -> bool. - -Infix "+" := Aplus (at level 50, left associativity). -Infix "*" := Amult (at level 40, left associativity). -Notation "0" := Azero. -Notation "1" := Aone. - -Record Semi_Ring_Theory : Prop := - {SR_plus_comm : forall n m:A, n + m = m + n; - SR_plus_assoc : forall n m p:A, n + (m + p) = n + m + p; - SR_mult_comm : forall n m:A, n * m = m * n; - SR_mult_assoc : forall n m p:A, n * (m * p) = n * m * p; - SR_plus_zero_left : forall n:A, 0 + n = n; - 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_eq_prop : forall x y:A, Is_true (Aeq x y) -> x = y}. - -Variable T : Semi_Ring_Theory. - -Let plus_comm := SR_plus_comm T. -Let plus_assoc := SR_plus_assoc T. -Let mult_comm := SR_mult_comm T. -Let mult_assoc := SR_mult_assoc T. -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.*) - -Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_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 *) -Lemma SR_mult_assoc2 : forall n m p:A, n * m * p = n * (m * p). -symmetry in |- *; eauto. Qed. - -Lemma SR_plus_assoc2 : forall n m p:A, n + m + p = n + (m + p). -symmetry in |- *; eauto. Qed. - -Lemma SR_plus_zero_left2 : forall n:A, n = 0 + n. -symmetry in |- *; eauto. Qed. - -Lemma SR_mult_one_left2 : forall n:A, n = 1 * n. -symmetry in |- *; eauto. Qed. - -Lemma SR_mult_zero_left2 : forall n:A, 0 = 0 * n. -symmetry in |- *; eauto. Qed. - -Lemma SR_distr_left2 : forall n m p:A, n * p + m * p = (n + m) * p. -symmetry in |- *; eauto. Qed. - -Lemma SR_plus_permute : forall n m p:A, n + (m + p) = m + (n + p). -intros. -rewrite plus_assoc. -elim (plus_comm m n). -rewrite <- plus_assoc. -reflexivity. -Qed. - -Lemma SR_mult_permute : forall n m p:A, n * (m * p) = m * (n * p). -intros. -rewrite mult_assoc. -elim (mult_comm m n). -rewrite <- mult_assoc. -reflexivity. -Qed. - -Hint Resolve SR_plus_permute SR_mult_permute. - -Lemma SR_distr_right : forall n m p:A, n * (m + p) = n * m + n * p. -intros. -repeat rewrite (mult_comm n). -eauto. -Qed. - -Lemma SR_distr_right2 : forall n m p:A, n * m + n * p = n * (m + p). -symmetry in |- *; apply SR_distr_right. Qed. - -Lemma SR_mult_zero_right : forall n:A, n * 0 = 0. -intro; rewrite mult_comm; eauto. -Qed. - -Lemma SR_mult_zero_right2 : forall n:A, 0 = n * 0. -intro; rewrite mult_comm; eauto. -Qed. - -Lemma SR_plus_zero_right : forall n:A, n + 0 = n. -intro; rewrite plus_comm; eauto. -Qed. -Lemma SR_plus_zero_right2 : forall n:A, n = n + 0. -intro; rewrite plus_comm; eauto. -Qed. - -Lemma SR_mult_one_right : forall n:A, n * 1 = n. -intro; elim mult_comm; auto. -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. - -Variable A : Type. - -Variable Aplus : A -> A -> A. -Variable Amult : A -> A -> A. -Variable Aone : A. -Variable Azero : A. -Variable Aopp : A -> A. -Variable Aeq : A -> A -> bool. - -Infix "+" := Aplus (at level 50, left associativity). -Infix "*" := Amult (at level 40, left associativity). -Notation "0" := Azero. -Notation "1" := Aone. -Notation "- x" := (Aopp x). - -Record Ring_Theory : Prop := - {Th_plus_comm : forall n m:A, n + m = m + n; - Th_plus_assoc : forall n m p:A, n + (m + p) = n + m + p; - Th_mult_sym : forall n m:A, n * m = m * n; - Th_mult_assoc : forall n m p:A, n * (m * p) = n * m * p; - Th_plus_zero_left : forall n:A, 0 + n = n; - Th_mult_one_left : forall n:A, 1 * n = n; - Th_opp_def : forall n:A, n + - n = 0; - Th_distr_left : forall n m p:A, (n + m) * p = n * p + m * p; - Th_eq_prop : forall x y:A, Is_true (Aeq x y) -> x = y}. - -Variable T : Ring_Theory. - -Let plus_comm := Th_plus_comm T. -Let plus_assoc := Th_plus_assoc T. -Let mult_comm := Th_mult_sym T. -Let mult_assoc := Th_mult_assoc T. -Let plus_zero_left := Th_plus_zero_left T. -Let mult_one_left := Th_mult_one_left T. -Let opp_def := Th_opp_def T. -Let distr_left := Th_distr_left T. - -Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left - mult_one_left opp_def distr_left. - -(* Lemmas whose form is x=y are also provided in form y=x because Auto does - not symmetry *) -Lemma Th_mult_assoc2 : forall n m p:A, n * m * p = n * (m * p). -symmetry in |- *; eauto. Qed. - -Lemma Th_plus_assoc2 : forall n m p:A, n + m + p = n + (m + p). -symmetry in |- *; eauto. Qed. - -Lemma Th_plus_zero_left2 : forall n:A, n = 0 + n. -symmetry in |- *; eauto. Qed. - -Lemma Th_mult_one_left2 : forall n:A, n = 1 * n. -symmetry in |- *; eauto. Qed. - -Lemma Th_distr_left2 : forall n m p:A, n * p + m * p = (n + m) * p. -symmetry in |- *; eauto. Qed. - -Lemma Th_opp_def2 : forall n:A, 0 = n + - n. -symmetry in |- *; eauto. Qed. - -Lemma Th_plus_permute : forall n m p:A, n + (m + p) = m + (n + p). -intros. -rewrite plus_assoc. -elim (plus_comm m n). -rewrite <- plus_assoc. -reflexivity. -Qed. - -Lemma Th_mult_permute : forall n m p:A, n * (m * p) = m * (n * p). -intros. -rewrite mult_assoc. -elim (mult_comm m n). -rewrite <- mult_assoc. -reflexivity. -Qed. - -Hint Resolve Th_plus_permute Th_mult_permute. - -Lemma aux1 : forall a:A, a + a = a -> a = 0. -intros. -generalize (opp_def a). -pattern a at 1 in |- *. -rewrite <- H. -rewrite <- plus_assoc. -rewrite opp_def. -elim plus_comm. -rewrite plus_zero_left. -trivial. -Qed. - -Lemma Th_mult_zero_left : forall n:A, 0 * n = 0. -intros. -apply aux1. -rewrite <- distr_left. -rewrite plus_zero_left. -reflexivity. -Qed. -Hint Resolve Th_mult_zero_left. - -Lemma Th_mult_zero_left2 : forall n:A, 0 = 0 * n. -symmetry in |- *; eauto. Qed. - -Lemma aux2 : forall x y z:A, x + y = 0 -> x + z = 0 -> y = z. -intros. -rewrite <- (plus_zero_left y). -elim H0. -elim plus_assoc. -elim (plus_comm y z). -rewrite plus_assoc. -rewrite H. -rewrite plus_zero_left. -reflexivity. -Qed. - -Lemma Th_opp_mult_left : forall x y:A, - (x * y) = - x * y. -intros. -apply (aux2 (x:=(x * y))); - [ apply opp_def | rewrite <- distr_left; rewrite opp_def; auto ]. -Qed. -Hint Resolve Th_opp_mult_left. - -Lemma Th_opp_mult_left2 : forall x y:A, - x * y = - (x * y). -symmetry in |- *; eauto. Qed. - -Lemma Th_mult_zero_right : forall n:A, n * 0 = 0. -intro; elim mult_comm; eauto. -Qed. - -Lemma Th_mult_zero_right2 : forall n:A, 0 = n * 0. -intro; elim mult_comm; eauto. -Qed. - -Lemma Th_plus_zero_right : forall n:A, n + 0 = n. -intro; rewrite plus_comm; eauto. -Qed. - -Lemma Th_plus_zero_right2 : forall n:A, n = n + 0. -intro; rewrite plus_comm; eauto. -Qed. - -Lemma Th_mult_one_right : forall n:A, n * 1 = n. -intro; elim mult_comm; eauto. -Qed. - -Lemma Th_mult_one_right2 : forall n:A, n = n * 1. -intro; elim mult_comm; eauto. -Qed. - -Lemma Th_opp_mult_right : forall x y:A, - (x * y) = x * - y. -intros; do 2 rewrite (mult_comm x); auto. -Qed. - -Lemma Th_opp_mult_right2 : forall x y:A, x * - y = - (x * y). -intros; do 2 rewrite (mult_comm x); auto. -Qed. - -Lemma Th_plus_opp_opp : forall x y:A, - x + - y = - (x + y). -intros. -apply (aux2 (x:=(x + y))); - [ elim plus_assoc; rewrite (Th_plus_permute y (- x)); rewrite plus_assoc; - rewrite opp_def; rewrite plus_zero_left; auto - | auto ]. -Qed. - -Lemma Th_plus_permute_opp : forall n m p:A, - m + (n + p) = n + (- m + p). -eauto. Qed. - -Lemma Th_opp_opp : forall n:A, - - n = n. -intro; apply (aux2 (x:=(- n))); [ auto | elim plus_comm; auto ]. -Qed. -Hint Resolve Th_opp_opp. - -Lemma Th_opp_opp2 : forall n:A, n = - - n. -symmetry in |- *; eauto. Qed. - -Lemma Th_mult_opp_opp : forall x y:A, - x * - y = x * y. -intros; rewrite <- Th_opp_mult_left; rewrite <- Th_opp_mult_right; auto. -Qed. - -Lemma Th_mult_opp_opp2 : forall x y:A, x * y = - x * - y. -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. -rewrite (plus_comm (- n) n). -rewrite opp_def. -repeat rewrite Th_plus_zero_left; eauto. -Qed. - -Lemma Th_plus_reg_right : forall n m p:A, m + n = p + n -> m = p. -intros. -eapply Th_plus_reg_left with n. -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). -eauto. -Qed. - -Lemma Th_distr_right2 : forall n m p:A, n * m + n * p = n * (m + p). -symmetry in |- *; apply Th_distr_right. -Qed. - -End Theory_of_rings. - -Hint Resolve Th_mult_zero_left (*Th_plus_reg_left*): core. - -Unset Implicit Arguments. - -Definition Semi_Ring_Theory_of : - forall (A:Type) (Aplus Amult:A -> A -> A) (Aone Azero:A) - (Aopp:A -> A) (Aeq:A -> A -> bool), - Ring_Theory Aplus Amult Aone Azero Aopp Aeq -> - Semi_Ring_Theory Aplus Amult Aone Azero Aeq. -intros until 1; case H. -split; intros; simpl in |- *; eauto. -Defined. - -(* Every ring can be viewed as a semi-ring : this property will be used - in Abstract_polynom. *) -Coercion Semi_Ring_Theory_of : Ring_Theory >-> Semi_Ring_Theory. - - -Section product_ring. - -End product_ring. - -Section power_ring. - -End power_ring. diff --git a/contrib/ring/ZArithRing.v b/contrib/ring/ZArithRing.v deleted file mode 100644 index 075431827c..0000000000 --- a/contrib/ring/ZArithRing.v +++ /dev/null @@ -1,36 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* true - | _ => false - end. - -Lemma Zeq_prop : forall x y:Z, Is_true (Zeq x y) -> x = y. - intros x y H; unfold Zeq in H. - apply Zcompare_Eq_eq. - destruct (x ?= y)%Z; [ reflexivity | contradiction | contradiction ]. -Qed. - -Definition ZTheory : Ring_Theory Zplus Zmult 1%Z 0%Z Zopp Zeq. - split; intros; eauto with zarith. - apply Zeq_prop; assumption. -Qed. - -(* NatConstants and NatTheory are defined in Ring_theory.v *) -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.ml b/contrib/ring/ring.ml index 1c5121ef69..e81c9ddd5c 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -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"]; -- cgit v1.2.3