From 81dd7a1db170d7d10d8a378cfd0719c2ded3f7df Mon Sep 17 00:00:00 2001 From: pottier Date: Tue, 22 Feb 2011 12:39:35 +0000 Subject: 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 --- plugins/setoid_ring/Ring2.v | 373 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 373 insertions(+) create mode 100644 plugins/setoid_ring/Ring2.v (limited to 'plugins/setoid_ring/Ring2.v') 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 *) +(* 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). -- cgit v1.2.3