diff options
Diffstat (limited to 'contrib/setoid_ring/Ring_theory.v')
| -rw-r--r-- | contrib/setoid_ring/Ring_theory.v | 504 |
1 files changed, 504 insertions, 0 deletions
diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v new file mode 100644 index 00000000..2f7378eb --- /dev/null +++ b/contrib/setoid_ring/Ring_theory.v @@ -0,0 +1,504 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import Setoid. +Set Implicit Arguments. + +Module RingSyntax. +Reserved Notation "x ?=! y" (at level 70, no associativity). +Reserved Notation "x +! y " (at level 50, left associativity). +Reserved Notation "x -! y" (at level 50, left associativity). +Reserved Notation "x *! y" (at level 40, left associativity). +Reserved Notation "-! x" (at level 35, right associativity). + +Reserved Notation "[ x ]" (at level 1, no associativity). + +Reserved Notation "x ?== y" (at level 70, no associativity). +Reserved Notation "x -- y" (at level 50, left associativity). +Reserved Notation "x ** y" (at level 40, left associativity). +Reserved Notation "-- x" (at level 35, right associativity). + +Reserved Notation "x == y" (at level 70, no associativity). +End RingSyntax. +Import RingSyntax. + +Section DEFINITIONS. + Variable R : Type. + Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R). + Variable req : R -> R -> Prop. + Notation "0" := rO. Notation "1" := rI. + Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y). + Notation "x - y " := (rsub x y). Notation "- x" := (ropp x). + Notation "x == y" := (req x y). + + (** Semi Ring *) + Record semi_ring_theory : Prop := mk_srt { + SRadd_0_l : forall n, 0 + n == n; + SRadd_comm : forall n m, n + m == m + n ; + SRadd_assoc : forall n m p, n + (m + p) == (n + m) + p; + SRmul_1_l : forall n, 1*n == n; + SRmul_0_l : forall n, 0*n == 0; + SRmul_comm : forall n m, n*m == m*n; + SRmul_assoc : forall n m p, n*(m*p) == (n*m)*p; + SRdistr_l : forall n m p, (n + m)*p == n*p + m*p + }. + + (** Almost Ring *) +(*Almost ring are no ring : Ropp_def is missing **) + Record almost_ring_theory : Prop := mk_art { + ARadd_0_l : forall x, 0 + x == x; + ARadd_comm : forall x y, x + y == y + x; + ARadd_assoc : forall x y z, x + (y + z) == (x + y) + z; + ARmul_1_l : forall x, 1 * x == x; + ARmul_0_l : forall x, 0 * x == 0; + ARmul_comm : forall x y, x * y == y * x; + ARmul_assoc : forall x y z, x * (y * z) == (x * y) * z; + ARdistr_l : forall x y z, (x + y) * z == (x * z) + (y * z); + ARopp_mul_l : forall x y, -(x * y) == -x * y; + ARopp_add : forall x y, -(x + y) == -x + -y; + ARsub_def : forall x y, x - y == x + -y + }. + + (** Ring *) + Record ring_theory : Prop := mk_rt { + Radd_0_l : forall x, 0 + x == x; + Radd_comm : forall x y, x + y == y + x; + Radd_assoc : forall x y z, x + (y + z) == (x + y) + z; + Rmul_1_l : forall x, 1 * x == x; + Rmul_comm : forall x y, x * y == y * x; + Rmul_assoc : forall x y z, x * (y * z) == (x * y) * z; + Rdistr_l : forall x y z, (x + y) * z == (x * z) + (y * z); + Rsub_def : forall x y, x - y == x + -y; + Ropp_def : forall x, x + (- x) == 0 + }. + + (** Equality is extensional *) + + Record sring_eq_ext : Prop := mk_seqe { + (* SRing operators are compatible with equality *) + SRadd_ext : + forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 + y1 == x2 + y2; + SRmul_ext : + forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 * y1 == x2 * y2 + }. + + Record ring_eq_ext : Prop := mk_reqe { + (* Ring operators are compatible with equality *) + Radd_ext : + forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 + y1 == x2 + y2; + Rmul_ext : + forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 * y1 == x2 * y2; + Ropp_ext : forall x1 x2, x1 == x2 -> -x1 == -x2 + }. + + (** Interpretation morphisms definition*) + Section MORPHISM. + Variable C:Type. + Variable (cO cI : C) (cadd cmul csub : C->C->C) (copp : C->C). + Variable ceqb : C->C->bool. + (* [phi] est un morphisme de [C] dans [R] *) + Variable phi : C -> R. + Notation "x +! y" := (cadd x y). Notation "x -! y " := (csub x y). + Notation "x *! y " := (cmul x y). Notation "-! x" := (copp x). + Notation "x ?=! y" := (ceqb x y). Notation "[ x ]" := (phi x). + +(*for semi rings*) + Record semi_morph : Prop := mkRmorph { + Smorph0 : [cO] == 0; + Smorph1 : [cI] == 1; + Smorph_add : forall x y, [x +! y] == [x]+[y]; + Smorph_mul : forall x y, [x *! y] == [x]*[y]; + Smorph_eq : forall x y, x?=!y = true -> [x] == [y] + }. + +(* for rings*) + Record ring_morph : Prop := mkmorph { + morph0 : [cO] == 0; + morph1 : [cI] == 1; + morph_add : forall x y, [x +! y] == [x]+[y]; + morph_sub : forall x y, [x -! y] == [x]-[y]; + morph_mul : forall x y, [x *! y] == [x]*[y]; + morph_opp : forall x, [-!x] == -[x]; + morph_eq : forall x y, x?=!y = true -> [x] == [y] + }. + End MORPHISM. + + (** Identity is a morphism *) + Variable Rsth : Setoid_Theory R req. + Add Setoid R req Rsth as R_setoid1. + Variable reqb : R->R->bool. + Hypothesis morph_req : forall x y, (reqb x y) = true -> x == y. + Definition IDphi (x:R) := x. + Lemma IDmorph : ring_morph rO rI radd rmul rsub ropp reqb IDphi. + Proof. + apply (mkmorph rO rI radd rmul rsub ropp reqb IDphi);intros;unfold IDphi; + try apply (Seq_refl _ _ Rsth);auto. + Qed. + +End DEFINITIONS. + + + +Section ALMOST_RING. + Variable R : Type. + Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R). + Variable req : R -> R -> Prop. + Notation "0" := rO. Notation "1" := rI. + Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y). + Notation "x - y " := (rsub x y). Notation "- x" := (ropp x). + Notation "x == y" := (req x y). + + (** Leibniz equality leads to a setoid theory and is extensional*) + Lemma Eqsth : Setoid_Theory R (@eq R). + Proof. constructor;intros;subst;trivial. Qed. + + Lemma Eq_s_ext : sring_eq_ext radd rmul (@eq R). + Proof. constructor;intros;subst;trivial. Qed. + + Lemma Eq_ext : ring_eq_ext radd rmul ropp (@eq R). + Proof. constructor;intros;subst;trivial. Qed. + + Variable Rsth : Setoid_Theory R req. + Add Setoid R req Rsth as R_setoid2. + Ltac sreflexivity := apply (Seq_refl _ _ Rsth). + + Section SEMI_RING. + Variable SReqe : sring_eq_ext radd rmul req. + Add Morphism radd : radd_ext1. exact (SRadd_ext SReqe). Qed. + Add Morphism rmul : rmul_ext1. exact (SRmul_ext SReqe). Qed. + Variable SRth : semi_ring_theory 0 1 radd rmul req. + + (** Every semi ring can be seen as an almost ring, by taking : + -x = x and x - y = x + y *) + Definition SRopp (x:R) := x. Notation "- x" := (SRopp x). + + Definition SRsub x y := x + -y. Notation "x - y " := (SRsub x y). + + Lemma SRopp_ext : forall x y, x == y -> -x == -y. + Proof. intros x y H;exact H. Qed. + + Lemma SReqe_Reqe : ring_eq_ext radd rmul SRopp req. + Proof. + constructor. exact (SRadd_ext SReqe). exact (SRmul_ext SReqe). + exact SRopp_ext. + Qed. + + Lemma SRopp_mul_l : forall x y, -(x * y) == -x * y. + Proof. intros;sreflexivity. Qed. + + Lemma SRopp_add : forall x y, -(x + y) == -x + -y. + Proof. intros;sreflexivity. Qed. + + + Lemma SRsub_def : forall x y, x - y == x + -y. + Proof. intros;sreflexivity. Qed. + + Lemma SRth_ARth : almost_ring_theory 0 1 radd rmul SRsub SRopp req. + Proof (mk_art 0 1 radd rmul SRsub SRopp req + (SRadd_0_l SRth) (SRadd_comm SRth) (SRadd_assoc SRth) + (SRmul_1_l SRth) (SRmul_0_l SRth) + (SRmul_comm SRth) (SRmul_assoc SRth) (SRdistr_l SRth) + SRopp_mul_l SRopp_add SRsub_def). + + (** Identity morphism for semi-ring equipped with their almost-ring structure*) + Variable reqb : R->R->bool. + + Hypothesis morph_req : forall x y, (reqb x y) = true -> x == y. + + Definition SRIDmorph : ring_morph 0 1 radd rmul SRsub SRopp req + 0 1 radd rmul SRsub SRopp reqb (@IDphi R). + Proof. + apply mkmorph;intros;try sreflexivity. unfold IDphi;auto. + Qed. + + (* a semi_morph can be extended to a ring_morph for the almost_ring derived + from a semi_ring, provided the ring is a setoid (we only need + reflexivity) *) + Variable C : Type. + Variable (cO cI : C) (cadd cmul: C->C->C). + Variable (ceqb : C -> C -> bool). + Variable phi : C -> R. + Variable Smorph : semi_morph rO rI radd rmul req cO cI cadd cmul ceqb phi. + + Lemma SRmorph_Rmorph : + ring_morph rO rI radd rmul SRsub SRopp req + cO cI cadd cmul cadd (fun x => x) ceqb phi. + Proof. + case Smorph; intros; constructor; auto. + unfold SRopp in |- *; intros. + setoid_reflexivity. + Qed. + + End SEMI_RING. + + Variable Reqe : ring_eq_ext radd rmul ropp req. + Add Morphism radd : radd_ext2. exact (Radd_ext Reqe). Qed. + Add Morphism rmul : rmul_ext2. exact (Rmul_ext Reqe). Qed. + Add Morphism ropp : ropp_ext2. exact (Ropp_ext Reqe). Qed. + + Section RING. + Variable Rth : ring_theory 0 1 radd rmul rsub ropp req. + + (** Rings are almost rings*) + Lemma Rmul_0_l : forall x, 0 * x == 0. + Proof. + intro x; setoid_replace (0*x) with ((0+1)*x + -x). + rewrite (Radd_0_l Rth); rewrite (Rmul_1_l Rth). + rewrite (Ropp_def Rth);sreflexivity. + + rewrite (Rdistr_l Rth);rewrite (Rmul_1_l Rth). + rewrite <- (Radd_assoc Rth); rewrite (Ropp_def Rth). + rewrite (Radd_comm Rth); rewrite (Radd_0_l Rth);sreflexivity. + Qed. + + Lemma Ropp_mul_l : forall x y, -(x * y) == -x * y. + Proof. + intros x y;rewrite <-(Radd_0_l Rth (- x * y)). + rewrite (Radd_comm Rth). + rewrite <-(Ropp_def Rth (x*y)). + rewrite (Radd_assoc Rth). + rewrite <- (Rdistr_l Rth). + rewrite (Rth.(Radd_comm) (-x));rewrite (Ropp_def Rth). + rewrite Rmul_0_l;rewrite (Radd_0_l Rth);sreflexivity. + Qed. + + Lemma Ropp_add : forall x y, -(x + y) == -x + -y. + Proof. + intros x y;rewrite <- ((Radd_0_l Rth) (-(x+y))). + rewrite <- ((Ropp_def Rth) x). + rewrite <- ((Radd_0_l Rth) (x + - x + - (x + y))). + rewrite <- ((Ropp_def Rth) y). + rewrite ((Radd_comm Rth) x). + rewrite ((Radd_comm Rth) y). + rewrite <- ((Radd_assoc Rth) (-y)). + rewrite <- ((Radd_assoc Rth) (- x)). + rewrite ((Radd_assoc Rth) y). + rewrite ((Radd_comm Rth) y). + rewrite <- ((Radd_assoc Rth) (- x)). + rewrite ((Radd_assoc Rth) y). + rewrite ((Radd_comm Rth) y);rewrite (Ropp_def Rth). + rewrite ((Radd_comm Rth) (-x) 0);rewrite (Radd_0_l Rth). + apply (Radd_comm Rth). + Qed. + + Lemma Ropp_opp : forall x, - -x == x. + Proof. + intros x; rewrite <- (Radd_0_l Rth (- -x)). + rewrite <- (Ropp_def Rth x). + rewrite <- (Radd_assoc Rth); rewrite (Ropp_def Rth). + rewrite ((Radd_comm Rth) x);apply (Radd_0_l Rth). + Qed. + + Lemma Rth_ARth : almost_ring_theory 0 1 radd rmul rsub ropp req. + Proof + (mk_art 0 1 radd rmul rsub ropp req (Radd_0_l Rth) (Radd_comm Rth) (Radd_assoc Rth) + (Rmul_1_l Rth) Rmul_0_l (Rmul_comm Rth) (Rmul_assoc Rth) (Rdistr_l Rth) + Ropp_mul_l Ropp_add (Rsub_def Rth)). + + (** Every semi morphism between two rings is a morphism*) + Variable C : Type. + Variable (cO cI : C) (cadd cmul csub: C->C->C) (copp : C -> C). + Variable (ceq : C -> C -> Prop) (ceqb : C -> C -> bool). + Variable phi : C -> R. + Notation "x +! y" := (cadd x y). Notation "x *! y " := (cmul x y). + Notation "x -! y " := (csub x y). Notation "-! x" := (copp x). + Notation "x ?=! y" := (ceqb x y). Notation "[ x ]" := (phi x). + Variable Csth : Setoid_Theory C ceq. + Variable Ceqe : ring_eq_ext cadd cmul copp ceq. + Add Setoid C ceq Csth as C_setoid. + Add Morphism cadd : cadd_ext. exact (Radd_ext Ceqe). Qed. + Add Morphism cmul : cmul_ext. exact (Rmul_ext Ceqe). Qed. + Add Morphism copp : copp_ext. exact (Ropp_ext Ceqe). Qed. + Variable Cth : ring_theory cO cI cadd cmul csub copp ceq. + Variable Smorph : semi_morph 0 1 radd rmul req cO cI cadd cmul ceqb phi. + Variable phi_ext : forall x y, ceq x y -> [x] == [y]. + Add Morphism phi : phi_ext1. exact phi_ext. Qed. + Lemma Smorph_opp : forall x, [-!x] == -[x]. + Proof. + intros x;rewrite <- (Rth.(Radd_0_l) [-!x]). + rewrite <- ((Ropp_def Rth) [x]). + rewrite ((Radd_comm Rth) [x]). + rewrite <- (Radd_assoc Rth). + rewrite <- (Smorph_add Smorph). + rewrite (Ropp_def Cth). + rewrite (Smorph0 Smorph). + rewrite (Radd_comm Rth (-[x])). + apply (Radd_0_l Rth);sreflexivity. + Qed. + + Lemma Smorph_sub : forall x y, [x -! y] == [x] - [y]. + Proof. + intros x y; rewrite (Rsub_def Cth);rewrite (Rsub_def Rth). + rewrite (Smorph_add Smorph);rewrite Smorph_opp;sreflexivity. + Qed. + + Lemma Smorph_morph : ring_morph 0 1 radd rmul rsub ropp req + cO cI cadd cmul csub copp ceqb phi. + Proof + (mkmorph 0 1 radd rmul rsub ropp req cO cI cadd cmul csub copp ceqb phi + (Smorph0 Smorph) (Smorph1 Smorph) + (Smorph_add Smorph) Smorph_sub (Smorph_mul Smorph) Smorph_opp + (Smorph_eq Smorph)). + + End RING. + + (** Usefull lemmas on almost ring *) + Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req. + + Lemma ARth_SRth : semi_ring_theory 0 1 radd rmul req. +Proof. +elim ARth; intros. +constructor; trivial. +Qed. + + Lemma ARsub_ext : + forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 - y1 == x2 - y2. + Proof. + intros. + setoid_replace (x1 - y1) with (x1 + -y1). + setoid_replace (x2 - y2) with (x2 + -y2). + rewrite H;rewrite H0;sreflexivity. + apply (ARsub_def ARth). + apply (ARsub_def ARth). + Qed. + Add Morphism rsub : rsub_ext. exact ARsub_ext. Qed. + + Ltac mrewrite := + repeat first + [ rewrite (ARadd_0_l ARth) + | rewrite <- ((ARadd_comm ARth) 0) + | rewrite (ARmul_1_l ARth) + | rewrite <- ((ARmul_comm ARth) 1) + | rewrite (ARmul_0_l ARth) + | rewrite <- ((ARmul_comm ARth) 0) + | rewrite (ARdistr_l ARth) + | sreflexivity + | match goal with + | |- context [?z * (?x + ?y)] => rewrite ((ARmul_comm ARth) z (x+y)) + end]. + + Lemma ARadd_0_r : forall x, (x + 0) == x. + Proof. intros; mrewrite. Qed. + + Lemma ARmul_1_r : forall x, x * 1 == x. + Proof. intros;mrewrite. Qed. + + Lemma ARmul_0_r : forall x, x * 0 == 0. + Proof. intros;mrewrite. Qed. + + Lemma ARdistr_r : forall x y z, z * (x + y) == z*x + z*y. + Proof. + intros;mrewrite. + repeat rewrite (ARth.(ARmul_comm) z);sreflexivity. + Qed. + + Lemma ARadd_assoc1 : forall x y z, (x + y) + z == (y + z) + x. + Proof. + intros;rewrite <-(ARth.(ARadd_assoc) x). + rewrite (ARth.(ARadd_comm) x);sreflexivity. + Qed. + + Lemma ARadd_assoc2 : forall x y z, (y + x) + z == (y + z) + x. + Proof. + intros; repeat rewrite <- (ARadd_assoc ARth); + rewrite ((ARadd_comm ARth) x); sreflexivity. + Qed. + + Lemma ARmul_assoc1 : forall x y z, (x * y) * z == (y * z) * x. + Proof. + intros;rewrite <-((ARmul_assoc ARth) x). + rewrite ((ARmul_comm ARth) x);sreflexivity. + Qed. + + Lemma ARmul_assoc2 : forall x y z, (y * x) * z == (y * z) * x. + Proof. + intros; repeat rewrite <- (ARmul_assoc ARth); + rewrite ((ARmul_comm ARth) x); sreflexivity. + Qed. + + Lemma ARopp_mul_r : forall x y, - (x * y) == x * -y. + Proof. + intros;rewrite ((ARmul_comm ARth) x y); + rewrite (ARopp_mul_l ARth); apply (ARmul_comm ARth). + Qed. + + Lemma ARopp_zero : -0 == 0. + Proof. + rewrite <- (ARmul_0_r 0); rewrite (ARopp_mul_l ARth). + repeat rewrite ARmul_0_r; sreflexivity. + Qed. + + + +End ALMOST_RING. + +Section AddRing. + + Variable R : Type. + Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R). + Variable req : R -> R -> Prop. + +Inductive ring_kind : Type := +| Abstract +| Computational + (R:Type) + (req : R -> R -> Prop) + (reqb : R -> R -> bool) + (_ : forall x y, (reqb x y) = true -> req x y) +| Morphism + (R : Type) + (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R) + (req : R -> R -> Prop) + (C : Type) + (cO cI : C) (cadd cmul csub : C->C->C) (copp : C->C) + (ceqb : C->C->bool) + phi + (_ : ring_morph rO rI radd rmul rsub ropp req + cO cI cadd cmul csub copp ceqb phi). + +End AddRing. + + +(** Some simplification tactics*) +Ltac gen_reflexivity Rsth := apply (Seq_refl _ _ Rsth). + +Ltac gen_srewrite O I add mul sub opp eq Rsth Reqe ARth := + repeat first + [ gen_reflexivity Rsth + | progress rewrite (ARopp_zero Rsth Reqe ARth) + | rewrite (ARadd_0_l ARth) + | rewrite (ARadd_0_r Rsth ARth) + | rewrite (ARmul_1_l ARth) + | rewrite (ARmul_1_r Rsth ARth) + | rewrite (ARmul_0_l ARth) + | rewrite (ARmul_0_r Rsth ARth) + | rewrite (ARdistr_l ARth) + | rewrite (ARdistr_r Rsth Reqe ARth) + | rewrite (ARadd_assoc ARth) + | rewrite (ARmul_assoc ARth) + | progress rewrite (ARopp_add ARth) + | progress rewrite (ARsub_def ARth) + | progress rewrite <- (ARopp_mul_l ARth) + | progress rewrite <- (ARopp_mul_r Rsth Reqe ARth) ]. + +Ltac gen_add_push add Rsth Reqe ARth x := + repeat (match goal with + | |- context [add (add ?y x) ?z] => + progress rewrite (ARadd_assoc2 Rsth Reqe ARth x y z) + | |- context [add (add x ?y) ?z] => + progress rewrite (ARadd_assoc1 Rsth ARth x y z) + end). + +Ltac gen_mul_push mul Rsth Reqe ARth x := + repeat (match goal with + | |- context [mul (mul ?y x) ?z] => + progress rewrite (ARmul_assoc2 Rsth Reqe ARth x y z) + | |- context [mul (mul x ?y) ?z] => + progress rewrite (ARmul_assoc1 Rsth ARth x y z) + end). + |