anneaux commutatifs ou non, reification sans ml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13848 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 373 insertions, 0 deletions

diff --git a/plugins/setoid_ring/Ring2.v b/plugins/setoid_ring/Ring2.v
new file mode 100644
index 0000000000..30a6128f1f
--- /dev/null
+++ b/plugins/setoid_ring/Ring2.v
@@ -0,0 +1,373 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* non commutative rings *)
+
+Require Import Setoid.
+Require Import BinPos.
+Require Import BinNat.
+Require Export Morphisms Setoid Bool.
+Require Export Algebra_syntax.
+
+Set Implicit Arguments.
+
+Class Ring (R:Type) := {
+ ring0: R; ring1: R; 
+ ring_plus: R->R->R; ring_mult: R->R->R;
+ ring_sub:  R->R->R; ring_opp: R->R; 
+ ring_eq : R -> R -> Prop;
+ ring_setoid: Equivalence ring_eq;
+ ring_plus_comp: Proper (ring_eq==>ring_eq==>ring_eq) ring_plus;
+ ring_mult_comp: Proper (ring_eq==>ring_eq==>ring_eq) ring_mult;
+ ring_sub_comp: Proper (ring_eq==>ring_eq==>ring_eq) ring_sub;
+ ring_opp_comp: Proper (ring_eq==>ring_eq) ring_opp;
+
+ ring_add_0_l    : forall x, ring_eq (ring_plus ring0 x) x;
+ ring_add_comm    : forall x y, ring_eq (ring_plus x y) (ring_plus y x);
+ ring_add_assoc  : forall x y z, ring_eq (ring_plus x (ring_plus y z))
+                                         (ring_plus (ring_plus x y) z);
+ ring_mul_1_l    : forall x, ring_eq (ring_mult ring1 x) x;
+ ring_mul_1_r    : forall x, ring_eq (ring_mult x ring1) x;
+ ring_mul_assoc  : forall x y z, ring_eq (ring_mult x (ring_mult y z))
+                                         (ring_mult (ring_mult x y) z);
+ ring_distr_l    : forall x y z, ring_eq (ring_mult (ring_plus x y) z)
+                                   (ring_plus (ring_mult x z) (ring_mult y z));
+ ring_distr_r    : forall x y z, ring_eq (ring_mult z (ring_plus x y))
+                                  (ring_plus (ring_mult z x) (ring_mult z y));
+ ring_sub_def    : forall x y, ring_eq (ring_sub x y) (ring_plus x (ring_opp y));
+ ring_opp_def    : forall x, ring_eq (ring_plus x (ring_opp x)) ring0
+}.
+
+
+Instance zero_ring (R:Type)(Rr:Ring R) : Zero R := {zero := ring0}.
+Instance one_ring(R:Type)(Rr:Ring R) : One R := {one := ring1}.
+Instance addition_ring(R:Type)(Rr:Ring R) : Addition R :=
+  {addition x y := ring_plus x y}.
+Instance multiplication_ring(R:Type)(Rr:Ring R) : Multiplication:= 
+  {multiplication x y := ring_mult x y}.
+Instance subtraction_ring(R:Type)(Rr:Ring R) : Subtraction R :=
+  {subtraction x y := ring_sub x y}.
+Instance opposite_ring(R:Type)(Rr:Ring R) : Opposite R := 
+  {opposite x := ring_opp x}.
+Instance equality_ring(R:Type)(Rr:Ring R) : Equality :=
+  {equality x y := ring_eq x y}.
+
+Existing Instance ring_setoid.
+Existing Instance ring_plus_comp.
+Existing Instance ring_mult_comp.
+Existing Instance ring_sub_comp.
+Existing Instance ring_opp_comp.
+(** Interpretation morphisms definition*)
+
+Class Ring_morphism (C R:Type)`{Cr:Ring C} `{Rr:Ring R}:= {
+    ring_morphism_fun: C -> R;
+    ring_morphism0    : ring_morphism_fun 0 == 0;
+    ring_morphism1    : ring_morphism_fun 1 == 1;
+    ring_morphism_add : forall x y, ring_morphism_fun (x + y)
+                     == ring_morphism_fun x + ring_morphism_fun y;
+    ring_morphism_sub : forall x y, ring_morphism_fun (x - y)
+                     == ring_morphism_fun x - ring_morphism_fun y;
+    ring_morphism_mul : forall x y, ring_morphism_fun (x * y)
+                     == ring_morphism_fun x * ring_morphism_fun y;
+    ring_morphism_opp : forall x, ring_morphism_fun (-x)
+                          == -(ring_morphism_fun x);
+    ring_morphism_eq  : forall x y, x == y
+       -> ring_morphism_fun x == ring_morphism_fun y}.
+
+Instance bracket_ring (C R:Type)`{Cr:Ring C} `{Rr:Ring R}
+   `{phi:@Ring_morphism C R Cr Rr}
+  : Bracket C R  :=
+  {bracket x := ring_morphism_fun x}.
+
+(* Tactics for rings *)
+Axiom eta: forall (A B:Type) (f:A->B), (fun x:A => f x) = f.
+Axiom eta2: forall (A B C:Type) (f:A->B->C), (fun (x:A)(y:B) => f x y) = f.
+
+Ltac etarefl := try apply eta; try apply eta2; try reflexivity.
+
+Lemma ring_syntax1:forall (A:Type)(Ar:Ring A), (@ring_eq _ Ar) = equality.
+intros. symmetry. simpl; etarefl. Qed.
+Lemma ring_syntax2:forall (A:Type)(Ar:Ring A), (@ring_plus _ Ar) = addition.
+intros. symmetry. simpl; etarefl. Qed.
+Lemma ring_syntax3:forall (A:Type)(Ar:Ring A), (@ring_mult _ Ar) = multiplication.
+intros. symmetry. simpl; etarefl. Qed.
+Lemma ring_syntax4:forall (A:Type)(Ar:Ring A), (@ring_sub _ Ar) = subtraction.
+intros. symmetry. simpl; etarefl. Qed.
+Lemma ring_syntax5:forall (A:Type)(Ar:Ring A), (@ring_opp _ Ar) = opposite.
+intros. symmetry. simpl; etarefl. Qed.
+Lemma ring_syntax6:forall (A:Type)(Ar:Ring A), (@ring0 _ Ar) = zero.
+intros. symmetry. simpl; etarefl. Qed.
+Lemma ring_syntax7:forall (A:Type)(Ar:Ring A), (@ring1 _ Ar) = one.
+intros. symmetry. simpl; etarefl. Qed.
+Lemma ring_syntax8:forall (A:Type)(Ar:Ring A)(B:Type)(Br:Ring B)
+  (pM:@Ring_morphism A B Ar Br), (@ring_morphism_fun _ _ _ _ pM) = bracket.
+intros. symmetry. simpl; etarefl. Qed.
+
+Ltac set_ring_notations :=
+  repeat (rewrite ring_syntax1);
+  repeat (rewrite ring_syntax2);
+  repeat (rewrite ring_syntax3);
+  repeat (rewrite ring_syntax4);
+  repeat (rewrite ring_syntax5);
+  repeat (rewrite ring_syntax6);
+  repeat (rewrite ring_syntax7);
+  repeat (rewrite ring_syntax8).
+
+Ltac unset_ring_notations :=
+  unfold equality, equality_ring, addition, addition_ring,
+     multiplication, multiplication_ring, subtraction, subtraction_ring,
+     opposite, opposite_ring, one, one_ring, zero, zero_ring,
+     bracket, bracket_ring.
+
+Ltac ring_simpl := simpl; set_ring_notations.
+
+Ltac ring_rewrite H:=
+  generalize H;
+  let h := fresh "H" in
+  unset_ring_notations; intro h;
+  rewrite h; clear h;
+  set_ring_notations.
+
+Ltac ring_rewrite_rev H:=
+  generalize H;
+  let h := fresh "H" in
+  unset_ring_notations; intro h;
+  rewrite <- h; clear h;
+  set_ring_notations.
+
+Ltac rrefl := unset_ring_notations; reflexivity.
+
+Section Ring.
+
+Variable R: Type.
+Variable Rr: Ring R.
+
+(* Powers *)
+
+ Fixpoint pow_pos (x:R) (i:positive) {struct i}: R :=
+  match i with
+  | xH => x
+  | xO i => let p := pow_pos x i in p * p
+  | xI i => let p := pow_pos x i in x * (p * p)
+  end.
+Add Setoid R ring_eq ring_setoid as R_set_Power.
+ Add Morphism ring_mult : rmul_ext_Power. exact ring_mult_comp. Qed.
+
+ Lemma pow_pos_comm : forall x j,  x * pow_pos x j == pow_pos x j * x.
+induction j; ring_simpl. 
+ring_rewrite_rev ring_mul_assoc. ring_rewrite_rev ring_mul_assoc. 
+ring_rewrite_rev IHj. ring_rewrite (ring_mul_assoc (pow_pos x j) x (pow_pos x j)).
+ring_rewrite_rev IHj. ring_rewrite_rev ring_mul_assoc. rrefl.
+ring_rewrite_rev ring_mul_assoc. ring_rewrite_rev IHj.
+ring_rewrite ring_mul_assoc. ring_rewrite IHj.
+ring_rewrite_rev ring_mul_assoc. ring_rewrite IHj. rrefl. rrefl.
+Qed.
+
+ Lemma pow_pos_Psucc : forall x j, pow_pos x (Psucc j) == x * pow_pos x j.
+ Proof.
+  induction j; ring_simpl. 
+  ring_rewrite IHj. 
+ring_rewrite_rev (ring_mul_assoc x (pow_pos x j) (x * pow_pos x j)).
+ring_rewrite (ring_mul_assoc (pow_pos x j) x  (pow_pos x j)).
+  ring_rewrite_rev pow_pos_comm. unset_ring_notations.
+rewrite <- ring_mul_assoc. reflexivity.
+rrefl. rrefl.
+Qed.
+
+ Lemma pow_pos_Pplus : forall x i j, pow_pos x (i + j) == pow_pos x i * pow_pos x j.
+ Proof.
+  intro x;induction i;intros.
+  rewrite xI_succ_xO;rewrite Pplus_one_succ_r.
+  rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc.
+  repeat ring_rewrite IHi.
+  rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;
+  ring_rewrite pow_pos_Psucc.
+  ring_simpl;repeat ring_rewrite ring_mul_assoc. rrefl.
+  rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc.
+  repeat ring_rewrite IHi. ring_rewrite ring_mul_assoc. rrefl.
+  rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;ring_rewrite pow_pos_Psucc.
+   simpl. reflexivity. 
+ Qed.
+
+ Definition pow_N (x:R) (p:N) :=
+  match p with
+  | N0 => 1
+  | Npos p => pow_pos x p
+  end.
+
+ Definition id_phi_N (x:N) : N := x.
+
+ Lemma pow_N_pow_N : forall x n, pow_N x (id_phi_N n) == pow_N x n.
+ Proof.
+  intros; rrefl.
+ Qed.
+
+End Ring.
+
+
+
+
+Section Ring2.
+Variable R: Type.
+Variable Rr: Ring R.
+ (** Identity is a morphism *)
+ Definition IDphi (x:R) := x.
+ Lemma IDmorph : @Ring_morphism R R Rr Rr.
+ Proof.
+  apply (Build_Ring_morphism Rr Rr IDphi);intros;unfold IDphi; try rrefl. trivial.
+ Qed.
+
+Ltac ring_replace a b :=
+  unset_ring_notations; setoid_replace a with b; set_ring_notations.
+
+ (** rings are almost rings*)
+ Lemma ring_mul_0_l : forall x, 0 * x == 0.
+ Proof.
+  intro x. ring_replace (0*x) ((0+1)*x + -x). 
+  ring_rewrite ring_add_0_l. ring_rewrite ring_mul_1_l .
+  ring_rewrite ring_opp_def ;rrefl.
+  ring_rewrite ring_distr_l ;ring_rewrite ring_mul_1_l .
+  ring_rewrite_rev ring_add_assoc ; ring_rewrite ring_opp_def .
+  ring_rewrite ring_add_comm ; ring_rewrite ring_add_0_l ;rrefl.
+ Qed.
+
+ Lemma ring_mul_0_r : forall x, x * 0 == 0.
+ Proof.
+  intro x; ring_replace (x*0)  (x*(0+1) + -x).
+  ring_rewrite ring_add_0_l ; ring_rewrite ring_mul_1_r .
+  ring_rewrite ring_opp_def ;rrefl.
+
+  ring_rewrite ring_distr_r ;ring_rewrite ring_mul_1_r .
+  ring_rewrite_rev ring_add_assoc ; ring_rewrite ring_opp_def .
+  ring_rewrite ring_add_comm ; ring_rewrite ring_add_0_l ;rrefl.
+ Qed.
+
+ Lemma ring_opp_mul_l : forall x y, -(x * y) == -x * y.
+ Proof.
+  intros x y;ring_rewrite_rev (ring_add_0_l (- x * y)).
+  ring_rewrite ring_add_comm .
+  ring_rewrite_rev (ring_opp_def (x*y)).
+  ring_rewrite ring_add_assoc .
+  ring_rewrite_rev ring_distr_l.
+  ring_rewrite (ring_add_comm (-x));ring_rewrite ring_opp_def .
+  ring_rewrite ring_mul_0_l;ring_rewrite ring_add_0_l ;rrefl.
+ Qed.
+
+Lemma ring_opp_mul_r : forall x y, -(x * y) == x * -y.
+ Proof.
+  intros x y;ring_rewrite_rev (ring_add_0_l (x * - y)).
+  ring_rewrite ring_add_comm .
+  ring_rewrite_rev (ring_opp_def (x*y)).
+  ring_rewrite ring_add_assoc .
+  ring_rewrite_rev ring_distr_r .
+  ring_rewrite (ring_add_comm (-y));ring_rewrite ring_opp_def .
+  ring_rewrite ring_mul_0_r;ring_rewrite ring_add_0_l ;rrefl.
+ Qed.
+
+ Lemma ring_opp_add : forall x y, -(x + y) == -x + -y.
+ Proof.
+  intros x y;ring_rewrite_rev (ring_add_0_l  (-(x+y))).
+  ring_rewrite_rev (ring_opp_def  x).
+  ring_rewrite_rev (ring_add_0_l  (x + - x + - (x + y))).
+  ring_rewrite_rev (ring_opp_def  y).
+  ring_rewrite (ring_add_comm  x).
+  ring_rewrite (ring_add_comm  y).
+  ring_rewrite_rev (ring_add_assoc  (-y)).
+  ring_rewrite_rev (ring_add_assoc  (- x)).
+  ring_rewrite (ring_add_assoc   y).
+  ring_rewrite (ring_add_comm  y).
+  ring_rewrite_rev (ring_add_assoc   (- x)).
+  ring_rewrite (ring_add_assoc  y).
+  ring_rewrite (ring_add_comm  y);ring_rewrite ring_opp_def .
+  ring_rewrite (ring_add_comm  (-x) 0);ring_rewrite ring_add_0_l .
+  ring_rewrite ring_add_comm; rrefl.
+ Qed.
+
+ Lemma ring_opp_opp : forall x, - -x == x.
+ Proof.
+  intros x; ring_rewrite_rev (ring_add_0_l (- -x)).
+  ring_rewrite_rev (ring_opp_def x).
+  ring_rewrite_rev ring_add_assoc ; ring_rewrite ring_opp_def .
+  ring_rewrite (ring_add_comm  x); ring_rewrite ring_add_0_l . rrefl.
+ Qed.
+
+ Lemma ring_sub_ext :
+      forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 - y1 == x2 - y2.
+ Proof.
+  intros.
+  ring_replace (x1 - y1)  (x1 + -y1).
+  ring_replace (x2 - y2)  (x2 + -y2).
+  ring_rewrite H;ring_rewrite H0;rrefl.
+  ring_rewrite ring_sub_def. rrefl.
+  ring_rewrite ring_sub_def. rrefl.
+ Qed.
+
+ Ltac mring_rewrite :=
+   repeat first
+     [ ring_rewrite ring_add_0_l
+     | ring_rewrite_rev (ring_add_comm 0)
+     | ring_rewrite ring_mul_1_l
+     | ring_rewrite ring_mul_0_l
+     | ring_rewrite ring_distr_l
+     | rrefl
+     ].
+
+ Lemma ring_add_0_r : forall x, (x + 0) == x.
+ Proof. intros; mring_rewrite. Qed.
+
+ 
+ Lemma ring_add_assoc1 : forall x y z, (x + y) + z == (y + z) + x.
+ Proof.
+  intros;ring_rewrite_rev (ring_add_assoc x).
+  ring_rewrite (ring_add_comm x);rrefl.
+ Qed.
+
+ Lemma ring_add_assoc2 : forall x y z, (y + x) + z == (y + z) + x.
+ Proof.
+  intros; repeat ring_rewrite_rev ring_add_assoc.
+   ring_rewrite (ring_add_comm x); rrefl.
+ Qed.
+
+ Lemma ring_opp_zero : -0 == 0.
+ Proof.
+  ring_rewrite_rev (ring_mul_0_r 0). ring_rewrite ring_opp_mul_l.
+  repeat ring_rewrite ring_mul_0_r. rrefl.
+ Qed.
+
+End Ring2.
+
+(** Some simplification tactics*)
+Ltac gen_reflexivity := rrefl.
+ 
+Ltac gen_ring_rewrite :=
+  repeat first
+     [ rrefl
+     | progress ring_rewrite ring_opp_zero
+     | ring_rewrite ring_add_0_l
+     | ring_rewrite ring_add_0_r
+     | ring_rewrite ring_mul_1_l 
+     | ring_rewrite ring_mul_1_r
+     | ring_rewrite ring_mul_0_l 
+     | ring_rewrite ring_mul_0_r 
+     | ring_rewrite ring_distr_l 
+     | ring_rewrite ring_distr_r 
+     | ring_rewrite ring_add_assoc 
+     | ring_rewrite ring_mul_assoc
+     | progress ring_rewrite ring_opp_add 
+     | progress ring_rewrite ring_sub_def 
+     | progress ring_rewrite_rev ring_opp_mul_l 
+     | progress ring_rewrite_rev ring_opp_mul_r ].
+
+Ltac gen_add_push x :=
+set_ring_notations;
+repeat (match goal with
+  | |- context [(?y + x) + ?z] =>
+     progress ring_rewrite (@ring_add_assoc2 _ _ x y z)
+  | |- context [(x + ?y) + ?z] =>
+     progress ring_rewrite  (@ring_add_assoc1 _ _ x y z)
+  end).