diff options
| -rw-r--r-- | plugins/setoid_ring/Cring.v | 28 | ||||
| -rw-r--r-- | plugins/setoid_ring/Cring_tac.v | 15 | ||||
| -rw-r--r-- | plugins/setoid_ring/Ring2.v | 20 | ||||
| -rw-r--r-- | plugins/setoid_ring/Ring2_tac.v | 5 |
4 files changed, 38 insertions, 30 deletions
diff --git a/plugins/setoid_ring/Cring.v b/plugins/setoid_ring/Cring.v index 5ba016074..4058cd224 100644 --- a/plugins/setoid_ring/Cring.v +++ b/plugins/setoid_ring/Cring.v @@ -11,6 +11,7 @@ Require Import Setoid. Require Import BinPos. Require Import BinNat. +Require Export ZArith. Require Export Morphisms Setoid Bool. Require Import Algebra_syntax. Require Import Ring_theory. @@ -56,8 +57,13 @@ Instance opposite_cring`{R:Type}`{Rr:Cring R} : Opposite R := {opposite x := cring_opp x}. Instance equality_cring `{R:Type}`{Rr:Cring R} : Equality := {equality x y := cring_eq x y}. +Definition ZN(x:Z):= + match x with + Z0 => N0 + |Zpos p | Zneg p => Npos p +end. Instance power_cring {R:Type}{Rr:Cring R} : Power:= - {power x y := @Ring_theory.pow_N _ cring1 cring_mult x y}. + {power x y := @Ring_theory.pow_N _ cring1 cring_mult x (ZN y)}. Existing Instance cring_setoid. Existing Instance cring_plus_comp. @@ -87,28 +93,24 @@ Instance bracket_cring {C R:Type}`{Cr:Cring C} `{Rr:Cring R} {bracket x := cring_morphism_fun x}. (* Tactics for crings *) -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 cring_syntax1:forall (A:Type)(Ar:Cring A), (@cring_eq _ Ar) = equality. -intros. symmetry. simpl; etarefl. Qed. +intros. symmetry. simpl ; reflexivity. Qed. Lemma cring_syntax2:forall (A:Type)(Ar:Cring A), (@cring_plus _ Ar) = addition. -intros. symmetry. simpl; etarefl. Qed. +intros. symmetry. simpl; reflexivity. Qed. Lemma cring_syntax3:forall (A:Type)(Ar:Cring A), (@cring_mult _ Ar) = multiplication. -intros. symmetry. simpl; etarefl. Qed. +intros. symmetry. simpl; reflexivity. Qed. Lemma cring_syntax4:forall (A:Type)(Ar:Cring A), (@cring_sub _ Ar) = subtraction. -intros. symmetry. simpl; etarefl. Qed. +intros. symmetry. simpl; reflexivity. Qed. Lemma cring_syntax5:forall (A:Type)(Ar:Cring A), (@cring_opp _ Ar) = opposite. -intros. symmetry. simpl; etarefl. Qed. +intros. symmetry. simpl; reflexivity. Qed. Lemma cring_syntax6:forall (A:Type)(Ar:Cring A), (@cring0 _ Ar) = zero. -intros. symmetry. simpl; etarefl. Qed. +intros. symmetry. simpl; reflexivity. Qed. Lemma cring_syntax7:forall (A:Type)(Ar:Cring A), (@cring1 _ Ar) = one. -intros. symmetry. simpl; etarefl. Qed. +intros. symmetry. simpl; reflexivity. Qed. Lemma cring_syntax8:forall (A:Type)(Ar:Cring A)(B:Type)(Br:Cring B) (pM:@Cring_morphism A B Ar Br), (@cring_morphism_fun _ _ _ _ pM) = bracket. -intros. symmetry. simpl; etarefl. Qed. +intros. symmetry. simpl; reflexivity. Qed. Ltac set_cring_notations := repeat (rewrite cring_syntax1); diff --git a/plugins/setoid_ring/Cring_tac.v b/plugins/setoid_ring/Cring_tac.v index c83dd4e8d..8df45b56e 100644 --- a/plugins/setoid_ring/Cring_tac.v +++ b/plugins/setoid_ring/Cring_tac.v @@ -14,6 +14,7 @@ Require Import Znumtheory. Require Import Zdiv_def. Require Export Morphisms Setoid Bool. Require Import ZArith. +Open Scope Z_scope. Require Import Algebra_syntax. Require Import Ring_polynom. Require Export Cring. @@ -212,14 +213,18 @@ Variable R: Type. Variable Rr: Cring R. Existing Instance Rr. +Goal forall x y z:R, 3%Z * x * (2%Z * y * z) == 6%Z * (x * y) * z. +cring. +Qed. + (* reification: 0,7s sinon, le reste de la tactique donne le même temps que ring *) -Goal forall x y z t u :R, (x + y + z + t + u)^13%N == (u + t + z + y + x) ^13%N. +Goal forall x y z t u :R, (x + y + z + t + u)^13 == (u + t + z + y + x) ^13. Time cring. (*Finished transaction in 0. secs (0.410938u,0.s)*) Qed. (* -Goal forall x y z t u :R, (x + y + z + t + u)^16%N == (u + t + z + y + x) ^16%N. +Goal forall x y z t u :R, (x + y + z + t + u)^16 == (u + t + z + y + x) ^16. Time cring.(*Finished transaction in 1. secs (0.968852u,0.001s)*) Qed. *) @@ -237,6 +242,10 @@ Time ring.(*Finished transaction in 1. secs (0.914861u,0.s)*) Qed. *) +Goal forall x y z:R, 6*x^2 + y == y + 3*2*x^2 + 0 . +cring. +Qed. + (* Goal forall x y z:R, x + y == y + x + 0 . cring. @@ -246,7 +255,7 @@ Goal forall x y z:R, x * y * z == x * (y * z). cring. Qed. -Goal forall x y z:R, 3%Z * x * (2%Z * y * z) == 6%Z * (x * y) * z. +Goal forall x y z:R, 3 * x * (2%Z * y * z) == 6 * (x * y) * z. cring. Qed. diff --git a/plugins/setoid_ring/Ring2.v b/plugins/setoid_ring/Ring2.v index 30a6128f1..a28c1d4ea 100644 --- a/plugins/setoid_ring/Ring2.v +++ b/plugins/setoid_ring/Ring2.v @@ -85,28 +85,24 @@ Instance bracket_ring (C R:Type)`{Cr:Ring C} `{Rr:Ring 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. +intros. symmetry. simpl; reflexivity. Qed. Lemma ring_syntax2:forall (A:Type)(Ar:Ring A), (@ring_plus _ Ar) = addition. -intros. symmetry. simpl; etarefl. Qed. +intros. symmetry. simpl; reflexivity. Qed. Lemma ring_syntax3:forall (A:Type)(Ar:Ring A), (@ring_mult _ Ar) = multiplication. -intros. symmetry. simpl; etarefl. Qed. +intros. symmetry. simpl; reflexivity. Qed. Lemma ring_syntax4:forall (A:Type)(Ar:Ring A), (@ring_sub _ Ar) = subtraction. -intros. symmetry. simpl; etarefl. Qed. +intros. symmetry. simpl; reflexivity. Qed. Lemma ring_syntax5:forall (A:Type)(Ar:Ring A), (@ring_opp _ Ar) = opposite. -intros. symmetry. simpl; etarefl. Qed. +intros. symmetry. simpl; reflexivity. Qed. Lemma ring_syntax6:forall (A:Type)(Ar:Ring A), (@ring0 _ Ar) = zero. -intros. symmetry. simpl; etarefl. Qed. +intros. symmetry. simpl; reflexivity. Qed. Lemma ring_syntax7:forall (A:Type)(Ar:Ring A), (@ring1 _ Ar) = one. -intros. symmetry. simpl; etarefl. Qed. +intros. symmetry. simpl; reflexivity. 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. +intros. symmetry. simpl; reflexivity. Qed. Ltac set_ring_notations := repeat (rewrite ring_syntax1); diff --git a/plugins/setoid_ring/Ring2_tac.v b/plugins/setoid_ring/Ring2_tac.v index 1df1b8e73..15dad95e1 100644 --- a/plugins/setoid_ring/Ring2_tac.v +++ b/plugins/setoid_ring/Ring2_tac.v @@ -13,6 +13,7 @@ Require Import BinList. Require Import Znumtheory. Require Export Morphisms Setoid Bool. Require Import ZArith. +Open Scope Z_scope. Require Import Algebra_syntax. Require Export Ring2. Require Import Ring2_polynom. @@ -174,11 +175,11 @@ Goal forall x y z:R, x * y * z == x * (y * z). ring2. Qed. -Goal forall x y z:R, [3%Z]* x *([2%Z]* y * z) == [6%Z] * (x * y) * z. +Goal forall x y z:R, [3]* x *([2]* y * z) == [6] * (x * y) * z. ring2. Qed. -Goal forall x y z:R, 3%Z * x * (2%Z * y * z) == 6%Z * (x * y) * z. +Goal forall x y z:R, 3 * x * (2 * y * z) == 6 * (x * y) * z. ring2. Qed. |