diff options
| -rw-r--r-- | Makefile.build | 2 | ||||
| -rw-r--r-- | Makefile.common | 6 | ||||
| -rw-r--r-- | plugins/pluginsbyte.itarget | 1 | ||||
| -rw-r--r-- | plugins/pluginsdyn.itarget | 1 | ||||
| -rw-r--r-- | plugins/pluginsopt.itarget | 1 | ||||
| -rw-r--r-- | plugins/pluginsvo.itarget | 1 | ||||
| -rw-r--r-- | plugins/setoid_ring/Cring.v | 8 | ||||
| -rw-r--r-- | plugins/setoid_ring/Cring_tac.v | 15 | ||||
| -rw-r--r-- | plugins/setoid_ring/vo.itarget | 2 |
9 files changed, 29 insertions, 8 deletions
diff --git a/Makefile.build b/Makefile.build index d14152842..aa8a391c3 100644 --- a/Makefile.build +++ b/Makefile.build @@ -436,7 +436,7 @@ plugins: $(PLUGINSVO) omega: $(OMEGAVO) $(OMEGACMA) $(ROMEGAVO) $(ROMEGACMA) micromega: $(MICROMEGAVO) $(MICROMEGACMA) $(CSDPCERT) ring: $(RINGVO) $(RINGCMA) -setoid_ring: $(NEWRINGVO) $(NEWRINGCMA) +setoid_ring: $(NEWRINGVO) $(NEWRINGCMA) $(NCRINGVO) $(NCRINGCMA) nsatz: $(NSATZVO) $(NSATZCMA) dp: $(DPCMA) xml: $(XMLVO) $(XMLCMA) diff --git a/Makefile.common b/Makefile.common index fa76dac60..a564d0e6a 100644 --- a/Makefile.common +++ b/Makefile.common @@ -171,6 +171,7 @@ MICROMEGACMA:=plugins/micromega/micromega_plugin.cma QUOTECMA:=plugins/quote/quote_plugin.cma RINGCMA:=plugins/ring/ring_plugin.cma NEWRINGCMA:=plugins/setoid_ring/newring_plugin.cma +NCRINGCMA:=plugins/setoid_ring/ncring_plugin.cma NSATZCMA:=plugins/nsatz/nsatz_plugin.cma DPCMA:=plugins/dp/dp_plugin.cma FIELDCMA:=plugins/field/field_plugin.cma @@ -192,7 +193,7 @@ OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \ DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cma PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \ - $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(DPCMA) $(FIELDCMA) \ + $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(NCRINGCMA)$(DPCMA) $(FIELDCMA) \ $(FOURIERCMA) $(EXTRACTIONCMA) $(XMLCMA) \ $(CCCMA) $(FOCMA) $(SUBTACCMA) $(RTAUTOCMA) \ $(FUNINDCMA) $(NSATZCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA) @@ -305,6 +306,7 @@ QUOTEVO:=$(call cat_vo_itarget, plugins/quote) RINGVO:=$(call cat_vo_itarget, plugins/ring) FIELDVO:=$(call cat_vo_itarget, plugins/field) NEWRINGVO:=$(call cat_vo_itarget, plugins/setoid_ring) +NCRINGVO:=$(call cat_vo_itarget, plugins/setoid_ring) NSATZVO:=$(call cat_vo_itarget, plugins/nsatz) FOURIERVO:=$(call cat_vo_itarget, plugins/fourier) FUNINDVO:=$(call cat_vo_itarget, plugins/funind) @@ -316,7 +318,7 @@ CCVO:= PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \ $(XMLVO) $(FOURIERVO) $(CCVO) $(FUNINDVO) \ - $(RTAUTOVO) $(NEWRINGVO) $(DPVO) $(QUOTEVO) \ + $(RTAUTOVO) $(NEWRINGVO) $(NCRINGVO)$(DPVO) $(QUOTEVO) \ $(NSATZVO) $(EXTRACTIONVO) ALLVO:= $(THEORIESVO) $(PLUGINSVO) diff --git a/plugins/pluginsbyte.itarget b/plugins/pluginsbyte.itarget index 04cbdccb0..402d22d1b 100644 --- a/plugins/pluginsbyte.itarget +++ b/plugins/pluginsbyte.itarget @@ -13,6 +13,7 @@ xml/xml_plugin.cma subtac/subtac_plugin.cma ring/ring_plugin.cma cc/cc_plugin.cma +ncring/ncring_plugin.cma nsatz/nsatz_plugin.cma funind/recdef_plugin.cma syntax/ascii_syntax_plugin.cma diff --git a/plugins/pluginsdyn.itarget b/plugins/pluginsdyn.itarget index bbadfe696..c7c855336 100644 --- a/plugins/pluginsdyn.itarget +++ b/plugins/pluginsdyn.itarget @@ -13,6 +13,7 @@ xml/xml_plugin.cmxs subtac/subtac_plugin.cmxs ring/ring_plugin.cmxs cc/cc_plugin.cmxs +ncring/ncring_plugin.cmxs nsatz/nsatz_plugin.cmxs funind/recdef_plugin.cmxs syntax/ascii_syntax_plugin.cmxs diff --git a/plugins/pluginsopt.itarget b/plugins/pluginsopt.itarget index 74b3f5275..84ba2c6d7 100644 --- a/plugins/pluginsopt.itarget +++ b/plugins/pluginsopt.itarget @@ -13,6 +13,7 @@ xml/xml_plugin.cmxa subtac/subtac_plugin.cmxa ring/ring_plugin.cmxa cc/cc_plugin.cmxa +ncring/ncring_plugin.cmxa nsatz/nsatz_plugin.cmxa funind/recdef_plugin.cmxa syntax/ascii_syntax_plugin.cmxa diff --git a/plugins/pluginsvo.itarget b/plugins/pluginsvo.itarget index db56534c9..421178f40 100644 --- a/plugins/pluginsvo.itarget +++ b/plugins/pluginsvo.itarget @@ -2,6 +2,7 @@ dp/vo.otarget field/vo.otarget fourier/vo.otarget funind/vo.otarget +ncring/vo.otarget nsatz/vo.otarget micromega/vo.otarget omega/vo.otarget diff --git a/plugins/setoid_ring/Cring.v b/plugins/setoid_ring/Cring.v index 5ba016074..46064385a 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. 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/vo.itarget b/plugins/setoid_ring/vo.itarget index cccd21855..c4a21fd6a 100644 --- a/plugins/setoid_ring/vo.itarget +++ b/plugins/setoid_ring/vo.itarget @@ -20,4 +20,4 @@ Cring_tac.vo Ring2.vo Ring2_polynom.vo Ring2_initial.vo -Ring2_tac.vo
\ No newline at end of file +Ring2_tac.vo |