diff options
49 files changed, 1938 insertions, 910 deletions
@@ -2211,6 +2211,8 @@ tactics/termdn.cmx: lib/util.cmx kernel/term.cmx pretyping/rawterm.cmx \ pretyping/pattern.cmx library/nametab.cmx kernel/names.cmx \ library/nameops.cmx library/libnames.cmx tactics/dn.cmx \ tactics/termdn.cmi +test-suite/zarith.cmo: test-suite/zarith.cmi +test-suite/zarith.cmx: test-suite/zarith.cmi tools/coqdep.cmo: tools/coqdep_lexer.cmo config/coq_config.cmi tools/coqdep.cmx: tools/coqdep_lexer.cmx config/coq_config.cmx tools/gallina.cmo: tools/gallina_lexer.cmo @@ -3636,33 +3638,35 @@ contrib/rtauto/refl_tauto.cmx: lib/util.cmx pretyping/termops.cmx \ kernel/environ.cmx interp/coqlib.cmx kernel/closure.cmx \ contrib/rtauto/refl_tauto.cmi contrib/setoid_ring/newring.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ - pretyping/typing.cmi interp/topconstr.cmi kernel/term.cmi \ - tactics/tactics.cmi tactics/tacticals.cmi proofs/tacmach.cmi \ - tactics/tacinterp.cmi proofs/tacexpr.cmo library/summary.cmi \ - tactics/setoid_replace.cmi pretyping/retyping.cmi proofs/refiner.cmi \ - pretyping/reductionops.cmi pretyping/rawterm.cmi contrib/ring/quote.cmo \ - proofs/proof_type.cmi parsing/printer.cmi pretyping/pretyping.cmi \ - parsing/pptactic.cmi lib/pp.cmi parsing/pcoq.cmi library/nametab.cmi \ - kernel/names.cmi kernel/mod_subst.cmi library/libobject.cmi \ - library/libnames.cmi library/lib.cmi parsing/lexer.cmi library/global.cmi \ - interp/genarg.cmi pretyping/evd.cmi kernel/esubst.cmi kernel/environ.cmi \ - kernel/entries.cmi parsing/egrammar.cmi library/declare.cmi \ - library/decl_kinds.cmo interp/coqlib.cmi interp/constrintern.cmi \ - kernel/closure.cmi toplevel/cerrors.cmi + pretyping/typing.cmi kernel/typeops.cmi interp/topconstr.cmi \ + pretyping/termops.cmi kernel/term.cmi tactics/tactics.cmi \ + tactics/tacticals.cmi proofs/tacmach.cmi tactics/tacinterp.cmi \ + proofs/tacexpr.cmo library/summary.cmi tactics/setoid_replace.cmi \ + pretyping/retyping.cmi proofs/refiner.cmi pretyping/reductionops.cmi \ + pretyping/rawterm.cmi contrib/ring/quote.cmo proofs/proof_type.cmi \ + parsing/printer.cmi pretyping/pretyping.cmi parsing/pptactic.cmi \ + lib/pp.cmi parsing/pcoq.cmi library/nametab.cmi kernel/names.cmi \ + kernel/mod_subst.cmi library/libobject.cmi library/libnames.cmi \ + library/lib.cmi parsing/lexer.cmi library/global.cmi interp/genarg.cmi \ + pretyping/evd.cmi kernel/esubst.cmi kernel/environ.cmi kernel/entries.cmi \ + parsing/egrammar.cmi library/declare.cmi library/decl_kinds.cmo \ + interp/coqlib.cmi interp/constrintern.cmi kernel/closure.cmi \ + toplevel/cerrors.cmi contrib/setoid_ring/newring.cmx: toplevel/vernacinterp.cmx lib/util.cmx \ - pretyping/typing.cmx interp/topconstr.cmx kernel/term.cmx \ - tactics/tactics.cmx tactics/tacticals.cmx proofs/tacmach.cmx \ - tactics/tacinterp.cmx proofs/tacexpr.cmx library/summary.cmx \ - tactics/setoid_replace.cmx pretyping/retyping.cmx proofs/refiner.cmx \ - pretyping/reductionops.cmx pretyping/rawterm.cmx contrib/ring/quote.cmx \ - proofs/proof_type.cmx parsing/printer.cmx pretyping/pretyping.cmx \ - parsing/pptactic.cmx lib/pp.cmx parsing/pcoq.cmx library/nametab.cmx \ - kernel/names.cmx kernel/mod_subst.cmx library/libobject.cmx \ - library/libnames.cmx library/lib.cmx parsing/lexer.cmx library/global.cmx \ - interp/genarg.cmx pretyping/evd.cmx kernel/esubst.cmx kernel/environ.cmx \ - kernel/entries.cmx parsing/egrammar.cmx library/declare.cmx \ - library/decl_kinds.cmx interp/coqlib.cmx interp/constrintern.cmx \ - kernel/closure.cmx toplevel/cerrors.cmx + pretyping/typing.cmx kernel/typeops.cmx interp/topconstr.cmx \ + pretyping/termops.cmx kernel/term.cmx tactics/tactics.cmx \ + tactics/tacticals.cmx proofs/tacmach.cmx tactics/tacinterp.cmx \ + proofs/tacexpr.cmx library/summary.cmx tactics/setoid_replace.cmx \ + pretyping/retyping.cmx proofs/refiner.cmx pretyping/reductionops.cmx \ + pretyping/rawterm.cmx contrib/ring/quote.cmx proofs/proof_type.cmx \ + parsing/printer.cmx pretyping/pretyping.cmx parsing/pptactic.cmx \ + lib/pp.cmx parsing/pcoq.cmx library/nametab.cmx kernel/names.cmx \ + kernel/mod_subst.cmx library/libobject.cmx library/libnames.cmx \ + library/lib.cmx parsing/lexer.cmx library/global.cmx interp/genarg.cmx \ + pretyping/evd.cmx kernel/esubst.cmx kernel/environ.cmx kernel/entries.cmx \ + parsing/egrammar.cmx library/declare.cmx library/decl_kinds.cmx \ + interp/coqlib.cmx interp/constrintern.cmx kernel/closure.cmx \ + toplevel/cerrors.cmx contrib/subtac/context.cmo: kernel/term.cmi kernel/names.cmi \ contrib/subtac/context.cmi contrib/subtac/context.cmx: kernel/term.cmx kernel/names.cmx \ @@ -4201,7 +4205,7 @@ coq_memory.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \ /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/memory.h + /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_interp.h coq_values.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \ /usr/local/lib/ocaml/caml/mlvalues.h \ /usr/local/lib/ocaml/caml/compatibility.h \ @@ -4211,39 +4215,3 @@ coq_values.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \ /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \ /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ /usr/local/lib/ocaml/caml/alloc.h -coq_fix_code.d.o: kernel/byterun/coq_fix_code.c \ - /usr/local/lib/ocaml/caml/config.h \ - /usr/local/lib/ocaml/caml/compatibility.h \ - /usr/local/lib/ocaml/caml/misc.h /usr/local/lib/ocaml/caml/config.h \ - /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_instruct.h \ - kernel/byterun/coq_fix_code.h -coq_interp.d.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \ - /usr/local/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/caml/compatibility.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \ - kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \ - /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ - kernel/byterun/coq_jumptbl.h -coq_memory.d.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \ - /usr/local/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/caml/compatibility.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \ - kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ - kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \ - /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/memory.h -coq_values.d.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \ - /usr/local/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/caml/compatibility.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ - kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/fail.h \ - /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ - /usr/local/lib/ocaml/caml/alloc.h diff --git a/.depend.coq b/.depend.coq index 430003c5c..f8da6a192 100644 --- a/.depend.coq +++ b/.depend.coq @@ -38,7 +38,7 @@ theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/Rbase.vo theories theories/Reals/SplitAbsolu.vo: theories/Reals/SplitAbsolu.v theories/Reals/Rbasic_fun.vo theories/Reals/SplitRmult.vo: theories/Reals/SplitRmult.v theories/Reals/Rbase.vo theories/Reals/ArithProp.vo: theories/Reals/ArithProp.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Arith/Even.vo theories/Arith/Div2.vo contrib/setoid_ring/ArithRing.vo -theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v contrib/ring/LegacyArithRing.vo contrib/setoid_ring/ArithRing.vo theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/SplitAbsolu.vo theories/Reals/SplitRmult.vo theories/Reals/ArithProp.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo +theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v contrib/ring/LegacyArithRing.vo contrib/setoid_ring/ArithRing.vo theories/Reals/Rbase.vo theories/Reals/Rpow_def.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/SplitAbsolu.vo theories/Reals/SplitRmult.vo theories/Reals/ArithProp.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo theories/Reals/Rseries.vo: theories/Reals/Rseries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Logic/Classical.vo theories/Arith/Compare.vo theories/Reals/SeqProp.vo: theories/Reals/SeqProp.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Logic/Classical.vo theories/Arith/Max.vo theories/Reals/Rcomplete.vo: theories/Reals/Rcomplete.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Arith/Max.vo @@ -174,7 +174,7 @@ theories/ZArith/Zminmax.vo: theories/ZArith/Zminmax.v theories/ZArith/Zmin.vo th theories/ZArith/Zeven.vo: theories/ZArith/Zeven.v theories/ZArith/BinInt.vo theories/ZArith/Zhints.vo: theories/ZArith/Zhints.v theories/ZArith/BinInt.vo theories/ZArith/Zorder.vo theories/ZArith/Zmin.vo theories/ZArith/Zabs.vo theories/ZArith/Zcompare.vo theories/ZArith/Znat.vo theories/ZArith/auxiliary.vo theories/ZArith/Zmisc.vo theories/ZArith/Wf_Z.vo theories/ZArith/Zlogarithm.vo: theories/ZArith/Zlogarithm.v theories/ZArith/ZArith_base.vo contrib/omega/Omega.vo theories/ZArith/Zcomplements.vo theories/ZArith/Zpower.vo -theories/ZArith/Zpower.vo: theories/ZArith/Zpower.v theories/ZArith/ZArith_base.vo contrib/omega/Omega.vo theories/ZArith/Zcomplements.vo +theories/ZArith/Zpower.vo: theories/ZArith/Zpower.v theories/ZArith/ZArith_base.vo theories/ZArith/Zpow_def.vo contrib/omega/Omega.vo theories/ZArith/Zcomplements.vo theories/ZArith/Zcomplements.vo: theories/ZArith/Zcomplements.v contrib/setoid_ring/ZArithRing.vo theories/ZArith/ZArith_base.vo contrib/omega/Omega.vo theories/Arith/Wf_nat.vo theories/Lists/List.vo theories/ZArith/Zdiv.vo: theories/ZArith/Zdiv.v theories/ZArith/ZArith_base.vo theories/ZArith/Zbool.vo contrib/omega/Omega.vo contrib/setoid_ring/ZArithRing.vo theories/ZArith/Zcomplements.vo theories/ZArith/Zsqrt.vo: theories/ZArith/Zsqrt.v contrib/setoid_ring/ZArithRing.vo contrib/omega/Omega.vo theories/ZArith/ZArith_base.vo @@ -184,6 +184,7 @@ theories/ZArith/Zbool.vo: theories/ZArith/Zbool.v theories/ZArith/BinInt.vo theo theories/ZArith/Zbinary.vo: theories/ZArith/Zbinary.v theories/Bool/Bvector.vo theories/ZArith/ZArith.vo theories/ZArith/Zpower.vo contrib/omega/Omega.vo theories/ZArith/Znumtheory.vo: theories/ZArith/Znumtheory.v theories/ZArith/ZArith_base.vo contrib/setoid_ring/ZArithRing.vo theories/ZArith/Zcomplements.vo theories/ZArith/Zdiv.vo theories/NArith/Ndigits.vo theories/Arith/Wf_nat.vo theories/ZArith/Int.vo: theories/ZArith/Int.v theories/ZArith/ZArith.vo contrib/romega/ROmega.vo +theories/ZArith/Zpow_def.vo: theories/ZArith/Zpow_def.v theories/ZArith/ZArith_base.vo contrib/setoid_ring/Ring_theory.vo theories/Setoids/Setoid.vo: theories/Setoids/Setoid.v theories/Relations/Relation_Definitions.vo theories/Lists/MonoList.vo: theories/Lists/MonoList.v theories/Arith/Le.vo theories/Lists/ListSet.vo: theories/Lists/ListSet.v theories/Lists/List.vo @@ -284,7 +285,7 @@ theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/Rbase.vo theories theories/Reals/SplitAbsolu.vo: theories/Reals/SplitAbsolu.v theories/Reals/Rbasic_fun.vo theories/Reals/SplitRmult.vo: theories/Reals/SplitRmult.v theories/Reals/Rbase.vo theories/Reals/ArithProp.vo: theories/Reals/ArithProp.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Arith/Even.vo theories/Arith/Div2.vo contrib/setoid_ring/ArithRing.vo -theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v contrib/ring/LegacyArithRing.vo contrib/setoid_ring/ArithRing.vo theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/SplitAbsolu.vo theories/Reals/SplitRmult.vo theories/Reals/ArithProp.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo +theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v contrib/ring/LegacyArithRing.vo contrib/setoid_ring/ArithRing.vo theories/Reals/Rbase.vo theories/Reals/Rpow_def.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/SplitAbsolu.vo theories/Reals/SplitRmult.vo theories/Reals/ArithProp.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo theories/Reals/Rseries.vo: theories/Reals/Rseries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Logic/Classical.vo theories/Arith/Compare.vo theories/Reals/SeqProp.vo: theories/Reals/SeqProp.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Logic/Classical.vo theories/Arith/Max.vo theories/Reals/Rcomplete.vo: theories/Reals/Rcomplete.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Arith/Max.vo @@ -364,17 +365,17 @@ contrib/rtauto/Bintree.vo: contrib/rtauto/Bintree.v theories/Lists/List.vo theor contrib/rtauto/Rtauto.vo: contrib/rtauto/Rtauto.v theories/Lists/List.vo contrib/rtauto/Bintree.vo theories/Bool/Bool.vo theories/NArith/BinPos.vo contrib/recdef/Recdef.vo: contrib/recdef/Recdef.v theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo contrib/setoid_ring/BinList.vo: contrib/setoid_ring/BinList.v theories/NArith/BinPos.vo theories/Lists/List.vo theories/Lists/ListTactics.vo -contrib/setoid_ring/Ring_theory.vo: contrib/setoid_ring/Ring_theory.v theories/Setoids/Setoid.vo -contrib/setoid_ring/Ring_polynom.vo: contrib/setoid_ring/Ring_polynom.v theories/Setoids/Setoid.vo contrib/setoid_ring/BinList.vo theories/NArith/BinPos.vo theories/ZArith/BinInt.vo contrib/setoid_ring/Ring_theory.vo -contrib/setoid_ring/Ring_tac.vo: contrib/setoid_ring/Ring_tac.v theories/Setoids/Setoid.vo theories/NArith/BinPos.vo contrib/setoid_ring/Ring_polynom.vo contrib/setoid_ring/BinList.vo contrib/setoid_ring/newring.cmo +contrib/setoid_ring/Ring_theory.vo: contrib/setoid_ring/Ring_theory.v theories/Setoids/Setoid.vo theories/NArith/BinPos.vo theories/NArith/BinNat.vo +contrib/setoid_ring/Ring_polynom.vo: contrib/setoid_ring/Ring_polynom.v theories/Setoids/Setoid.vo contrib/setoid_ring/BinList.vo theories/NArith/BinPos.vo theories/NArith/BinNat.vo theories/ZArith/BinInt.vo contrib/setoid_ring/Ring_theory.vo +contrib/setoid_ring/Ring_tac.vo: contrib/setoid_ring/Ring_tac.v theories/Setoids/Setoid.vo theories/NArith/BinPos.vo contrib/setoid_ring/Ring_polynom.vo contrib/setoid_ring/BinList.vo contrib/setoid_ring/InitialRing.vo contrib/setoid_ring/newring.cmo contrib/setoid_ring/Ring_base.vo: contrib/setoid_ring/Ring_base.v contrib/setoid_ring/newring.cmo contrib/setoid_ring/Ring_theory.vo contrib/setoid_ring/Ring_tac.vo contrib/setoid_ring/InitialRing.vo -contrib/setoid_ring/InitialRing.vo: contrib/setoid_ring/InitialRing.v theories/ZArith/ZArith_base.vo theories/ZArith/BinInt.vo theories/NArith/BinNat.vo theories/Setoids/Setoid.vo contrib/setoid_ring/Ring_theory.vo contrib/setoid_ring/Ring_tac.vo contrib/setoid_ring/Ring_polynom.vo +contrib/setoid_ring/InitialRing.vo: contrib/setoid_ring/InitialRing.v theories/ZArith/ZArith_base.vo theories/ZArith/Zpow_def.vo theories/ZArith/BinInt.vo theories/NArith/BinNat.vo theories/Setoids/Setoid.vo contrib/setoid_ring/Ring_theory.vo contrib/setoid_ring/Ring_polynom.vo contrib/setoid_ring/Ring_equiv.vo: contrib/setoid_ring/Ring_equiv.v contrib/ring/Setoid_ring_theory.vo contrib/ring/LegacyRing_theory.vo contrib/setoid_ring/Ring_theory.vo -contrib/setoid_ring/Ring.vo: contrib/setoid_ring/Ring.v theories/Bool/Bool.vo contrib/setoid_ring/Ring_theory.vo contrib/setoid_ring/Ring_base.vo contrib/setoid_ring/Ring_tac.vo +contrib/setoid_ring/Ring.vo: contrib/setoid_ring/Ring.v theories/Bool/Bool.vo contrib/setoid_ring/Ring_theory.vo contrib/setoid_ring/Ring_base.vo contrib/setoid_ring/InitialRing.vo contrib/setoid_ring/Ring_tac.vo contrib/setoid_ring/ArithRing.vo: contrib/setoid_ring/ArithRing.v theories/Arith/Mult.vo contrib/setoid_ring/Ring.vo contrib/setoid_ring/NArithRing.vo: contrib/setoid_ring/NArithRing.v contrib/setoid_ring/Ring.vo theories/NArith/BinPos.vo theories/NArith/BinNat.vo -contrib/setoid_ring/ZArithRing.vo: contrib/setoid_ring/ZArithRing.v contrib/setoid_ring/Ring.vo theories/ZArith/ZArith_base.vo +contrib/setoid_ring/ZArithRing.vo: contrib/setoid_ring/ZArithRing.v contrib/setoid_ring/Ring.vo theories/ZArith/ZArith_base.vo theories/ZArith/Zpow_def.vo contrib/setoid_ring/Field_theory.vo: contrib/setoid_ring/Field_theory.v contrib/setoid_ring/Ring.vo theories/ZArith/ZArith_base.vo contrib/setoid_ring/Field_tac.vo: contrib/setoid_ring/Field_tac.v contrib/setoid_ring/Ring_tac.vo contrib/setoid_ring/BinList.vo contrib/setoid_ring/Ring_polynom.vo contrib/setoid_ring/InitialRing.vo contrib/setoid_ring/Field_theory.vo contrib/setoid_ring/Field.vo: contrib/setoid_ring/Field.v contrib/setoid_ring/Field_theory.vo contrib/setoid_ring/Field_tac.vo -contrib/setoid_ring/RealField.vo: contrib/setoid_ring/RealField.v theories/Reals/Raxioms.vo theories/Reals/Rdefinitions.vo contrib/setoid_ring/Ring.vo contrib/setoid_ring/Field.vo +contrib/setoid_ring/RealField.vo: contrib/setoid_ring/RealField.v theories/NArith/Nnat.vo contrib/setoid_ring/ArithRing.vo contrib/setoid_ring/Ring.vo contrib/setoid_ring/Field.vo theories/Reals/Rdefinitions.vo theories/Reals/Rpow_def.vo theories/Reals/Raxioms.vo @@ -225,7 +225,7 @@ ML4FILES +=\ contrib/omega/g_omega.ml4 \ contrib/romega/g_romega.ml4 contrib/ring/g_quote.ml4 \ contrib/ring/g_ring.ml4 contrib/dp/g_dp.ml4 \ - contrib/setoid_ring/newring.ml4 \ + contrib/setoid_ring/newring.ml4 \ contrib/field/field.ml4 contrib/fourier/g_fourier.ml4 \ contrib/extraction/g_extraction.ml4 contrib/xml/xmlentries.ml4 @@ -874,7 +874,8 @@ ZARITHVO=\ theories/ZArith/Zdiv.vo theories/ZArith/Zsqrt.vo \ theories/ZArith/Zwf.vo theories/ZArith/ZArith_base.vo \ theories/ZArith/Zbool.vo theories/ZArith/Zbinary.vo \ - theories/ZArith/Znumtheory.vo theories/ZArith/Int.vo + theories/ZArith/Znumtheory.vo theories/ZArith/Int.vo \ + theories/ZArith/Zpow_def.vo QARITHVO=\ theories/QArith/QArith_base.vo theories/QArith/Qreduction.vo \ @@ -1754,8 +1755,6 @@ depend: beforedepend dependp4 ml4filesml done # 5. We express dependencies of .o files $(CC) -MM $(CINCLUDES) kernel/byterun/*.c >> .depend - $(CC) -MM $(CINCLUDES) kernel/byterun/*.c | sed -e 's/\.o/.d.o/' >> \ - .depend # 6. Finally, we erase the generated .ml files rm -f $(ML4FILESML) # 7. Since .depend contains correct dependencies .depend.devel can be deleted diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli index b6cc55f61..ef1d095e2 100644 --- a/contrib/interface/ascent.mli +++ b/contrib/interface/ascent.mli @@ -642,6 +642,7 @@ and ct_TACTIC_COM = | CT_elim_type of ct_FORMULA | CT_exact of ct_FORMULA | CT_exact_no_check of ct_FORMULA + | CT_vm_cast_no_check of ct_FORMULA | CT_exists of ct_SPEC_LIST | CT_fail of ct_ID_OR_INT * ct_STRING_OPT | CT_first of ct_TACTIC_COM * ct_TACTIC_COM list diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml index fe227f995..166a0cbf6 100644 --- a/contrib/interface/vtp.ml +++ b/contrib/interface/vtp.ml @@ -1549,6 +1549,9 @@ and fTACTIC_COM = function | CT_exact_no_check(x1) -> fFORMULA x1; fNODE "exact_no_check" 1 +| CT_vm_cast_no_check(x1) -> + fFORMULA x1; + fNODE "vm_cast_no_check" 1 | CT_exists(x1) -> fSPEC_LIST x1; fNODE "exists" 1 diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 6c9e8239d..1d710ed3d 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1060,6 +1060,7 @@ and xlate_tac = | TacAssumption -> CT_assumption | TacExact c -> CT_exact (xlate_formula c) | TacExactNoCheck c -> CT_exact_no_check (xlate_formula c) + | TacVmCastNoCheck c -> CT_vm_cast_no_check (xlate_formula c) | TacDestructHyp (true, (_,id)) -> CT_cdhyp (xlate_ident id) | TacDestructHyp (false, (_,id)) -> CT_dhyp (xlate_ident id) | TacDestructConcl -> CT_dconcl diff --git a/contrib/setoid_ring/ArithRing.v b/contrib/setoid_ring/ArithRing.v index 334abb8b0..9015f3ce9 100644 --- a/contrib/setoid_ring/ArithRing.v +++ b/contrib/setoid_ring/ArithRing.v @@ -10,12 +10,6 @@ Require Import Mult. Require Export Ring. Set Implicit Arguments. -Ltac isnatcst t := - match t with - O => true - | S ?p => isnatcst p - | _ => false - end. Ltac natcst t := match isnatcst t with true => t @@ -50,7 +44,7 @@ Ltac natprering := Qed. -Unboxed Fixpoint nateq (n m:nat) {struct m} : bool := +Fixpoint nateq (n m:nat) {struct m} : bool := match n, m with | O, O => true | S n', S m' => nateq n' m' @@ -67,3 +61,6 @@ Qed. Add Ring natr : natSRth (decidable nateq_ok, constants [natcst], preprocess [natprering]). + + +(* Pourquoi on n'utilise pas N pour les calculs sur nat ???? *) diff --git a/contrib/setoid_ring/BinList.v b/contrib/setoid_ring/BinList.v index 0d0fe5a44..509020042 100644 --- a/contrib/setoid_ring/BinList.v +++ b/contrib/setoid_ring/BinList.v @@ -10,7 +10,7 @@ Set Implicit Arguments. Require Import BinPos. Require Export List. Require Export ListTactics. -Open Scope positive_scope. +Open Local Scope positive_scope. Section MakeBinList. Variable A : Type. @@ -89,3 +89,5 @@ Section MakeBinList. Qed. End MakeBinList. + + diff --git a/contrib/setoid_ring/Field_tac.v b/contrib/setoid_ring/Field_tac.v index 86df87c93..b2e693bc7 100644 --- a/contrib/setoid_ring/Field_tac.v +++ b/contrib/setoid_ring/Field_tac.v @@ -10,10 +10,10 @@ Require Import Ring_tac BinList Ring_polynom InitialRing. Require Export Field_theory. (* syntaxification *) - Ltac mkFieldexpr C Cst radd rmul rsub ropp rdiv rinv t fv := + Ltac mkFieldexpr C Cst CstPow radd rmul rsub ropp rdiv rinv rpow t fv := let rec mkP t := match Cst t with - | Ring_tac.NotConstant => + | InitialRing.NotConstant => match t with | (radd ?t1 ?t2) => let e1 := mkP t1 in @@ -31,6 +31,13 @@ Require Export Field_theory. let e2 := mkP t2 in constr:(FEdiv e1 e2) | (rinv ?t1) => let e1 := mkP t1 in constr:(FEinv e1) + | (rpow ?t1 ?n) => + match CstPow n with + | InitialRing.NotConstant => + let p := Find_at t fv in constr:(@FEX C p) + | ?c => let e1 := mkP t1 in constr:(FEpow e1 c) + end + | _ => let p := Find_at t fv in constr:(@FEX C p) end @@ -38,10 +45,10 @@ Require Export Field_theory. end in mkP t. -Ltac FFV Cst add mul sub opp div inv t fv := +Ltac FFV Cst CstPow add mul sub opp div inv pow t fv := let rec TFV t fv := match Cst t with - | Ring_tac.NotConstant => + | InitialRing.NotConstant => match t with | (add ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv) | (mul ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv) @@ -49,16 +56,24 @@ Ltac FFV Cst add mul sub opp div inv t fv := | (opp ?t1) => TFV t1 fv | (div ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv) | (inv ?t1) => TFV t1 fv + | (pow ?t1 ?n) => + match CstPow n with + | InitialRing.NotConstant => AddFvTail t fv + | _ => TFV t1 fv + end | _ => AddFvTail t fv end | _ => fv end in TFV t fv. -Ltac ParseFieldComponents lemma := +Ltac ParseFieldComponents lemma req := match type of lemma with - | context [@FEeval ?R ?rO ?add ?mul ?sub ?opp ?div ?inv ?C ?phi _ _] => - (fun f => f add mul sub opp div inv C) + | context [ + PCond _ _ _ _ _ _ _ _ _ _ _ -> + req (@FEeval ?R ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv + ?C ?phi ?Cpow ?Cp_phi ?rpow _ _) _ ] => + (fun f => f radd rmul rsub ropp rdiv rinv rpow C) | _ => fail 1 "field anomaly: bad correctness lemma (parse)" end. @@ -82,86 +97,138 @@ Ltac simpl_PCond req := fold_field_cond req. (* Rewriting (field_simplify) *) -Ltac Field_simplify lemma Cond_lemma req Cst_tac := - let Make_tac := - match type of lemma with - | forall l fe nfe, - _ = nfe -> - PCond _ _ _ _ _ _ _ _ _ -> - req (FEeval ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv (C:=?C) ?phi l fe) - _ => - let mkFV := FFV Cst_tac radd rmul rsub ropp rdiv rinv in - let mkFE := mkFieldexpr C Cst_tac radd rmul rsub ropp rdiv rinv in - let field_rw H := (protect_fv "field" in H; rewrite H) in - fun f rl => f mkFV mkFE field_rw lemma req rl; - try (apply Cond_lemma; simpl_PCond req) - | _ => fail 1 "field anomaly: bad correctness lemma (rewr)" - end in - Make_tac ReflexiveNormTactic. -(* Pb: second rewrite are applied to non-zero condition of first rewrite... *) - -Tactic Notation (at level 0) "field_simplify" constr_list(rl) := - field_lookup - (fun req cst_tac _ _ field_simplify_ok cond_ok pre post rl => - pre(); Field_simplify field_simplify_ok cond_ok req cst_tac rl; post()). - - -(* Generic form of field tactics *) -Ltac Field_Scheme FV_tac SYN_tac SIMPL_tac lemma Cond_lemma req := - let R := match type of req with ?R -> _ => R end in - let rec ParseExpr ilemma := - match type of ilemma with - forall nfe, ?fe = nfe -> _ => - (fun t => - let x := fresh "fld_expr" in - let H := fresh "norm_fld_expr" in - compute_assertion H x fe; - ParseExpr (ilemma x H) t; - try clear x H) - | _ => (fun t => t ilemma) - end in - let Main r1 r2 := - let fv := FV_tac r1 (@List.nil R) in - let fv := FV_tac r2 fv in - let fe1 := SYN_tac r1 fv in - let fe2 := SYN_tac r2 fv in - ParseExpr (lemma fv fe1 fe2) - ltac:(fun ilemma => - apply ilemma || fail "field anomaly: failed in applying lemma"; - [ SIMPL_tac | apply Cond_lemma; simpl_PCond req]) in - OnEquation req Main. +Ltac Field_norm_gen f Cst_tac Pow_tac lemma Cond_lemma req n lH rl := + let Main radd rmul rsub ropp rdiv rinv rpow C := + let mkFV := FV Cst_tac Pow_tac radd rmul rsub ropp rpow in + let mkPol := mkPolexpr C Cst_tac Pow_tac radd rmul rsub ropp rpow in + let mkFFV := FFV Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in + let mkFE := + mkFieldexpr C Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in + let fv := FV_hypo_tac mkFV req lH in + let simpl_field H := (protect_fv "field" in H;f H) in + let lemma_tac fv RW_tac := + let rr_lemma := fresh "f_rw_lemma" in + let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in + let vlpe := fresh "list_hyp" in + let vlmp := fresh "list_hyp_norm" in + let vlmp_eq := fresh "list_hyp_norm_eq" in + let prh := proofHyp_tac lH in + pose (vlpe := lpe); + match type of lemma with + | context [mk_monpol_list ?cO ?cI ?cadd ?cmul ?csub ?copp ?ceqb _] => + compute_assertion vlmp_eq vlmp + (mk_monpol_list cO cI cadd cmul csub copp ceqb vlpe); + (assert (rr_lemma := lemma n vlpe fv prh vlmp vlmp_eq) + || fail "type error when build the rewriting lemma"); + RW_tac rr_lemma; + try clear rr_lemma vlmp_eq vlmp vlpe + | _ => fail 1 "field_simplify anomaly: bad correctness lemma" + end in + ReflexiveRewriteTactic mkFFV mkFE simpl_field lemma_tac fv rl; + try (apply Cond_lemma; simpl_PCond req) in + ParseFieldComponents lemma req Main. + +Ltac Field_simplify_gen f := + fun req cst_tac pow_tac _ _ field_simplify_ok cond_ok pre post lH rl => + pre(); + Field_norm_gen f cst_tac pow_tac field_simplify_ok cond_ok req + ring_subst_niter lH rl; + post(). + +Ltac Field_simplify := Field_simplify_gen ltac:(fun H => rewrite H). +Ltac Field_simplify_in hyp:= + Field_simplify_gen ltac:(fun H => rewrite H in hyp). + +Tactic Notation (at level 0) + "field_simplify" constr_list(rl) := + field_lookup Field_simplify [] rl. + +Tactic Notation (at level 0) + "field_simplify" "[" constr_list(lH) "]" constr_list(rl) := + field_lookup Field_simplify [lH] rl. + +Tactic Notation (at level 0) + "field_simplify" constr_list(rl) "in" hyp(h) := + field_lookup (Field_simplify_in h) [] rl. + +Tactic Notation (at level 0) + "field_simplify" "[" constr_list(lH) "]" constr_list(rl) "in" hyp(h) := + field_lookup (Field_simplify_in h) [lH] rl. + + +(** Generic tactic for solving equations *) + +Ltac Field_Scheme Simpl_tac Cst_tac Pow_tac lemma Cond_lemma req n lH := + let Main radd rmul rsub ropp rdiv rinv rpow C := + let mkFV := FV Cst_tac Pow_tac radd rmul rsub ropp rpow in + let mkPol := mkPolexpr C Cst_tac Pow_tac radd rmul rsub ropp rpow in + let mkFFV := FFV Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in + let mkFE := + mkFieldexpr C Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in + let rec ParseExpr ilemma := + match type of ilemma with + forall nfe, ?fe = nfe -> _ => + (fun t => + let x := fresh "fld_expr" in + let H := fresh "norm_fld_expr" in + compute_assertion H x fe; + ParseExpr (ilemma x H) t; + try clear x H) + | _ => (fun t => t ilemma) + end in + let Main_eq t1 t2 := + let fv := FV_hypo_tac mkFV req lH in + let fv := mkFFV t1 fv in + let fv := mkFFV t2 fv in + let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in + let prh := proofHyp_tac lH in + let vlpe := fresh "list_hyp" in + let fe1 := mkFE t1 fv in + let fe2 := mkFE t2 fv in + pose (vlpe := lpe); + let nlemma := fresh "field_lemma" in + (assert (nlemma := lemma n fv vlpe fe1 fe2 prh) + || fail "field anomaly:failed to build lemma"); + ParseExpr nlemma + ltac:(fun ilemma => + apply ilemma + || fail "field anomaly: failed in applying lemma"; + [ Simpl_tac | apply Cond_lemma; simpl_PCond req]) in + OnEquation req Main_eq in + ParseFieldComponents lemma req Main. (* solve completely a field equation, leaving non-zero conditions to be proved (field) *) -Ltac Field lemma Cond_lemma req Cst_tac := - let Main radd rmul rsub ropp rdiv rinv C := - let mkFV := FFV Cst_tac radd rmul rsub ropp rdiv rinv in - let mkFE := mkFieldexpr C Cst_tac radd rmul rsub ropp rdiv rinv in - let Simpl := - vm_compute; reflexivity || fail "not a valid field equation" in - Field_Scheme mkFV mkFE Simpl lemma Cond_lemma req in - ParseFieldComponents lemma Main. +Ltac FIELD := + let Simpl := vm_compute; reflexivity || fail "not a valid field equation" in + fun req cst_tac pow_tac field_ok _ _ cond_ok pre post lH rl => + pre(); + Field_Scheme Simpl cst_tac pow_tac field_ok cond_ok req + Ring_tac.ring_subst_niter lH; + post(). + Tactic Notation (at level 0) "field" := - field_lookup - (fun req cst_tac field_ok _ _ cond_ok pre post rl => - pre(); Field field_ok cond_ok req cst_tac; post()). + field_lookup FIELD []. + +Tactic Notation (at level 0) "field" "[" constr_list(lH) "]" := + field_lookup FIELD [lH]. (* transforms a field equation to an equivalent (simplified) ring equation, and leaves non-zero conditions to be proved (field_simplify_eq) *) -Ltac Field_simplify_eq lemma Cond_lemma req Cst_tac := - let Main radd rmul rsub ropp rdiv rinv C := - let mkFV := FFV Cst_tac radd rmul rsub ropp rdiv rinv in - let mkFE := mkFieldexpr C Cst_tac radd rmul rsub ropp rdiv rinv in - let Simpl := (protect_fv "field") in - Field_Scheme mkFV mkFE Simpl lemma Cond_lemma req in - ParseFieldComponents lemma Main. - -Tactic Notation (at level 0) "field_simplify_eq" := - field_lookup - (fun req cst_tac _ field_simplify_eq_ok _ cond_ok pre post rl => - pre(); Field_simplify_eq field_simplify_eq_ok cond_ok req cst_tac; - post()). +Ltac FIELD_SIMPL := + let Simpl := (protect_fv "field") in + fun req cst_tac pow_tac _ field_simplify_eq_ok _ cond_ok pre post lH rl => + pre(); + Field_Scheme Simpl cst_tac pow_tac field_simplify_eq_ok cond_ok + req Ring_tac.ring_subst_niter lH; + post(). + +Tactic Notation (at level 0) "field_simplify_eq" := + field_lookup FIELD_SIMPL []. + +Tactic Notation (at level 0) "field_simplify_eq" "[" constr_list(lH) "]" := + field_lookup FIELD_SIMPL [lH]. (* Adding a new field *) @@ -179,22 +246,48 @@ Ltac coerce_to_almost_field set ext f := | semi_field_theory _ _ _ _ _ _ _ => constr:(SF2AF set f) end. -Ltac field_elements set ext fspec rk := +Ltac field_elements set ext fspec pspec sspec rk := let afth := coerce_to_almost_field set ext fspec in let rspec := ring_of_field fspec in - ring_elements set ext rspec rk - ltac:(fun arth ext_r morph f => f afth ext_r morph). - - -Ltac field_lemmas set ext inv_m fspec rk := - field_elements set ext fspec rk - ltac:(fun afth ext_r morph => - let field_ok := constr:(Field_correct set ext_r inv_m afth morph) in - let field_simpl_ok := - constr:(Pphi_dev_div_ok set ext_r inv_m afth morph) in - let field_simpl_eq_ok := - constr:(Field_simplify_eq_correct set ext_r inv_m afth morph) in - let cond1_ok := constr:(Pcond_simpl_gen set ext_r afth morph) in - let cond2_ok := constr:(Pcond_simpl_complete set ext_r afth morph) in - (fun f => f afth ext_r morph field_ok field_simpl_ok field_simpl_eq_ok - cond1_ok cond2_ok)). + ring_elements set ext rspec pspec sspec rk + ltac:(fun arth ext_r morph p_spec s_spec f => f afth ext_r morph p_spec s_spec). + +Ltac field_lemmas set ext inv_m fspec pspec sspec rk := + let simpl_eq_lemma := + match pspec with + | None => constr:(Field_simplify_eq_correct) + | Some _ => constr:(Field_simplify_eq_pow_correct) + end in + let rw_lemma := + match pspec with + | None => constr:(Field_rw_correct) + | Some _ => constr:(Field_rw_pow_correct) + end in + field_elements set ext fspec pspec sspec rk + ltac:(fun afth ext_r morph p_spec s_spec => + match p_spec with + | mkhypo ?pp_spec => match s_spec with + | mkhypo ?ss_spec => + let field_simpl_eq_ok := + constr:(simpl_eq_lemma _ _ _ _ _ _ _ _ _ _ + set ext_r inv_m afth + _ _ _ _ _ _ _ _ _ morph + _ _ _ pp_spec _ ss_spec) in + let field_simpl_ok := + constr:(rw_lemma _ _ _ _ _ _ _ _ _ _ + set ext_r inv_m afth + _ _ _ _ _ _ _ _ _ morph + _ _ _ pp_spec _ ss_spec) in + let field_ok := + constr:(Field_correct set ext_r inv_m afth morph pp_spec ss_spec) in + let cond1_ok := + constr:(Pcond_simpl_gen set ext_r afth morph pp_spec) in + let cond2_ok := + constr:(Pcond_simpl_complete set ext_r afth morph pp_spec) in + (fun f => + f afth ext_r morph field_ok field_simpl_ok field_simpl_eq_ok + cond1_ok cond2_ok) + | _ => fail 2 "bad sign specification" + end + | _ => fail 1 "bad power specification" + end). diff --git a/contrib/setoid_ring/Field_theory.v b/contrib/setoid_ring/Field_theory.v index f810859c3..3da183d5a 100644 --- a/contrib/setoid_ring/Field_theory.v +++ b/contrib/setoid_ring/Field_theory.v @@ -9,6 +9,7 @@ Require Ring. Import Ring_polynom Ring_tac Ring_theory InitialRing Setoid List. Require Import ZArith_base. +(*Require Import Omega.*) Set Implicit Arguments. Section MakeFieldPol. @@ -29,7 +30,7 @@ Section MakeFieldPol. Variable Rsth : Setoid_Theory R req. Variable Reqe : ring_eq_ext radd rmul ropp req. Variable SRinv_ext : forall p q, p == q -> / p == / q. - + (* Field properties *) Record almost_field_theory : Prop := mk_afield { AF_AR : almost_ring_theory rO rI radd rmul rsub ropp req; @@ -94,9 +95,20 @@ Hint Resolve (ARadd_0_l ARth) (ARadd_comm ARth) (ARadd_assoc ARth) (ARopp_mul_l ARth) (ARopp_add ARth) (ARsub_def ARth) . -Notation NPEeval := (PEeval rO radd rmul rsub ropp phi). -Notation Nnorm := (norm cO cI cadd cmul csub copp ceqb). -Notation NPphi_dev := (Pphi_dev rO rI radd rmul cO cI ceqb phi). + (* Power coefficients *) + Variable Cpow : Set. + Variable Cp_phi : N -> Cpow. + Variable rpow : R -> Cpow -> R. + Variable pow_th : power_theory rI rmul req Cp_phi rpow. + (* sign function *) + Variable get_sign : C -> option C. + Variable get_sign_spec : sign_theory ropp req phi get_sign. + +Notation NPEeval := (PEeval rO radd rmul rsub ropp phi Cp_phi rpow). +Notation Nnorm := (norm_subst cO cI cadd cmul csub copp ceqb). + +Notation NPphi_dev := (Pphi_dev rO rI radd rmul rsub ropp cO cI copp ceqb phi get_sign). +Notation NPphi_pow := (Pphi_pow rO rI radd rmul rsub ropp cO cI copp ceqb phi Cp_phi rpow get_sign). (* add abstract semi-ring to help with some proofs *) Add Ring Rring : (ARth_SRth ARth). @@ -105,7 +117,7 @@ Add Ring Rring : (ARth_SRth ARth). (* additional ring properties *) Lemma rsub_0_l : forall r, 0 - r == - r. -intros; rewrite (ARsub_def ARth) in |- *; ring. +intros; rewrite (ARsub_def ARth) in |- *;ring. Qed. Lemma rsub_0_r : forall r, r - 0 == r. @@ -352,6 +364,20 @@ intros H1; apply f_equal with ( f := xO ); auto. intros H1 H2; case H1; injection H2; auto. Qed. +Definition N_eq n1 n2 := + match n1, n2 with + | N0, N0 => true + | Npos p1, Npos p2 => positive_eq p1 p2 + | _, _ => false + end. + +Lemma N_eq_correct : forall n1 n2, if N_eq n1 n2 then n1 = n2 else n1 <> n2. +Proof. + intros [ |p1] [ |p2];simpl;trivial;try(intro H;discriminate H;fail). + assert (H:=positive_eq_correct p1 p2);destruct (positive_eq p1 p2); + [rewrite H;trivial | intro H1;injection H1;subst;apply H;trivial]. +Qed. + (* equality test *) Fixpoint PExpr_eq (e1 e2 : PExpr C) {struct e1} : bool := match e1, e2 with @@ -361,9 +387,25 @@ Fixpoint PExpr_eq (e1 e2 : PExpr C) {struct e1} : bool := | PEsub e3 e5, PEsub e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false | PEmul e3 e5, PEmul e4 e6 => if PExpr_eq e3 e4 then PExpr_eq e5 e6 else false | PEopp e3, PEopp e4 => PExpr_eq e3 e4 + | PEpow e3 n3, PEpow e4 n4 => if N_eq n3 n4 then PExpr_eq e3 e4 else false | _, _ => false end. +Add Morphism (pow_pos rmul) : pow_morph. +intros x y H p;induction p as [p IH| p IH|];simpl;auto;ring[IH]. +Qed. + +Add Morphism (pow_N rI rmul) : pow_N_morph. +intros x y H [|p];simpl;auto. apply pow_morph;trivial. +Qed. +(* +Lemma rpow_morph : forall x y n, x == y ->rpow x (Cp_phi n) == rpow y (Cp_phi n). +Proof. + intros; repeat rewrite pow_th.(rpow_pow_N). + destruct n;simpl. apply eq_refl. + induction p;simpl;try rewrite IHp;try rewrite H; apply eq_refl. +Qed. +*) Theorem PExpr_eq_semi_correct: forall l e1 e2, PExpr_eq e1 e2 = true -> NPEeval l e1 == NPEeval l e2. intros l e1; elim e1. @@ -387,6 +429,10 @@ intros e4 e6; generalize (rec1 e4); case (PExpr_eq e3 e4); intros e3 rec e2; (case e2; simpl; (try (intros; discriminate))). intros e4; generalize (rec e4); case (PExpr_eq e3 e4); (try (intros; discriminate)); auto. +intros e3 rec n3 e2;(case e2;simpl;(try (intros;discriminate))). +intros e4 n4;generalize (N_eq_correct n3 n4);destruct (N_eq n3 n4); +intros;try discriminate. +repeat rewrite pow_th.(rpow_pow_N);rewrite H;rewrite (rec _ H0);auto. Qed. (* add *) @@ -395,6 +441,7 @@ Definition NPEadd e1 e2 := PEc c1, PEc c2 => PEc (cadd c1 c2) | PEc c, _ => if ceqb c cO then e2 else PEadd e1 e2 | _, PEc c => if ceqb c cO then e1 else PEadd e1 e2 + (* Peut t'on factoriser ici ??? *) | _, _ => PEadd e1 e2 end. @@ -403,32 +450,64 @@ Theorem NPEadd_correct: Proof. intros l e1 e2. destruct e1; destruct e2; simpl in |- *; try reflexivity; try apply ceqb_rect; - try (intro eq_c; rewrite eq_c in |- *); simpl in |- *; - try rewrite (morph0 CRmorph) in |- *; try ring. -apply (morph_add CRmorph). + try (intro eq_c; rewrite eq_c in |- *); simpl in |- *;try apply eq_refl; + try ring [(morph0 CRmorph)]. + apply (morph_add CRmorph). +Qed. + +Definition NPEpow x n := + match n with + | N0 => PEc cI + | Npos p => + match x with + | PEc c => + if ceqb c cI then PEc cI else if ceqb c cO then PEc cO else PEc (pow_pos cmul c p) + | _ => PEpow x n + end + end. + +Theorem NPEpow_correct : forall l e n, + NPEeval l (NPEpow e n) == NPEeval l (PEpow e n). +Proof. + destruct n;simpl. + rewrite pow_th.(rpow_pow_N);simpl;auto. + destruct e;simpl;auto. + repeat apply ceqb_rect;simpl;intros;rewrite pow_th.(rpow_pow_N);simpl. + symmetry;induction p;simpl;trivial; ring [IHp H CRmorph.(morph1)]. + symmetry; induction p;simpl;trivial;ring [IHp CRmorph.(morph0)]. + induction p;simpl;auto;repeat rewrite CRmorph.(morph_mul);ring [IHp]. Qed. (* mul *) -Definition NPEmul x y := +Fixpoint NPEmul (x y : PExpr C) {struct x} : PExpr C := match x, y with PEc c1, PEc c2 => PEc (cmul c1 c2) | PEc c, _ => if ceqb c cI then y else if ceqb c cO then PEc cO else PEmul x y | _, PEc c => if ceqb c cI then x else if ceqb c cO then PEc cO else PEmul x y - | _, _ => PEmul x y + | PEpow e1 n1, PEpow e2 n2 => + if N_eq n1 n2 then NPEpow (NPEmul e1 e2) n1 else PEmul x y + | _, _ => PEmul x y end. - + +Lemma pow_pos_mul : forall x y p, pow_pos rmul (x * y) p == pow_pos rmul x p * pow_pos rmul y p. +induction p;simpl;auto;try ring [IHp]. +Qed. + Theorem NPEmul_correct : forall l e1 e2, NPEeval l (NPEmul e1 e2) == NPEeval l (PEmul e1 e2). -intros l e1 e2. -destruct e1; destruct e2; simpl in |- *; try reflexivity; +induction e1;destruct e2; simpl in |- *;try reflexivity; repeat apply ceqb_rect; - try (intro eq_c; rewrite eq_c in |- *); simpl in |- *; - try rewrite (morph0 CRmorph) in |- *; - try rewrite (morph1 CRmorph) in |- *; - try ring. -apply (morph_mul CRmorph). + try (intro eq_c; rewrite eq_c in |- *); simpl in |- *; try reflexivity; + try ring [(morph0 CRmorph) (morph1 CRmorph)]. + apply (morph_mul CRmorph). +assert (H:=N_eq_correct n n0);destruct (N_eq n n0). +rewrite NPEpow_correct. simpl. +repeat rewrite pow_th.(rpow_pow_N). +rewrite IHe1;rewrite <- H;destruct n;simpl;try ring. +apply pow_pos_mul. +simpl;auto. Qed. (* sub *) @@ -437,6 +516,7 @@ Definition NPEsub e1 e2 := PEc c1, PEc c2 => PEc (csub c1 c2) | PEc c, _ => if ceqb c cO then PEopp e2 else PEsub e1 e2 | _, PEc c => if ceqb c cO then e1 else PEsub e1 e2 + (* Peut-on factoriser ici *) | _, _ => PEsub e1 e2 end. @@ -467,6 +547,7 @@ Fixpoint PExpr_simp (e : PExpr C) : PExpr C := | PEmul e1 e2 => NPEmul (PExpr_simp e1) (PExpr_simp e2) | PEsub e1 e2 => NPEsub (PExpr_simp e1) (PExpr_simp e2) | PEopp e1 => NPEopp (PExpr_simp e1) + | PEpow e1 n1 => NPEpow (PExpr_simp e1) n1 | _ => e end. @@ -489,6 +570,10 @@ intros e1 He1. transitivity (NPEeval l (PEopp (PExpr_simp e1))); auto. apply NPEopp_correct. simpl; auto. +intros e1 He1 n;simpl. +rewrite NPEpow_correct;simpl. +repeat rewrite pow_th.(rpow_pow_N). +rewrite He1;auto. Qed. @@ -508,8 +593,9 @@ Inductive FExpr : Type := | FEmul: FExpr -> FExpr -> FExpr | FEopp: FExpr -> FExpr | FEinv: FExpr -> FExpr - | FEdiv: FExpr -> FExpr -> FExpr . - + | FEdiv: FExpr -> FExpr -> FExpr + | FEpow: FExpr -> N -> FExpr . + Fixpoint FEeval (l : list R) (pe : FExpr) {struct pe} : R := match pe with | FEc c => phi c @@ -520,6 +606,7 @@ Fixpoint FEeval (l : list R) (pe : FExpr) {struct pe} : R := | FEopp x => - FEeval l x | FEinv x => / FEeval l x | FEdiv x y => FEeval l x / FEeval l y + | FEpow x n => rpow (FEeval l x) (Cp_phi n) end. (* The result of the normalisation *) @@ -538,8 +625,8 @@ Record linear : Type := mk_linear { Fixpoint PCond (l : list R) (le : list (PExpr C)) {struct le} : Prop := match le with | nil => True - | e1 :: nil => ~ req (PEeval rO radd rmul rsub ropp phi l e1) rO - | e1 :: l1 => ~ req (PEeval rO radd rmul rsub ropp phi l e1) rO /\ PCond l l1 + | e1 :: nil => ~ req (NPEeval l e1) rO + | e1 :: l1 => ~ req (NPEeval l e1) rO /\ PCond l l1 end. Theorem PCond_cons_inv_l : @@ -584,66 +671,170 @@ Qed. ***************************************************************************) - -Fixpoint isIn (e1 e2: PExpr C) {struct e2}: option (PExpr C) := +Fixpoint isIn (e1:PExpr C) (p1:positive) + (e2:PExpr C) (p2:positive) {struct e2}: option (N * PExpr C) := match e2 with | PEmul e3 e4 => - match isIn e1 e3 with - Some e5 => Some (NPEmul e5 e4) - | None => match isIn e1 e4 with - | Some e5 => Some (NPEmul e3 e5) - | None => None - end + match isIn e1 p1 e3 p2 with + | Some (N0, e5) => Some (N0, NPEmul e5 (NPEpow e4 (Npos p2))) + | Some (Npos p, e5) => + match isIn e1 p e4 p2 with + | Some (n, e6) => Some (n, NPEmul e5 e6) + | None => Some (Npos p, NPEmul e5 (NPEpow e4 (Npos p2))) + end + | None => + match isIn e1 p1 e4 p2 with + | Some (n, e5) => Some (n,NPEmul (NPEpow e3 (Npos p2)) e5) + | None => None + end end + | PEpow e3 N0 => None + | PEpow e3 (Npos p3) => isIn e1 p1 e3 (Pmult p3 p2) | _ => - if PExpr_eq e1 e2 then Some (PEc cI) else None + if PExpr_eq e1 e2 then + match Zminus (Zpos p1) (Zpos p2) with + | Zpos p => Some (Npos p, PEc cI) + | Z0 => Some (N0, PEc cI) + | Zneg p => Some (N0, NPEpow e2 (Npos p)) + end + else None end. + + Definition ZtoN z := match z with Zpos p => Npos p | _ => N0 end. + Definition NtoZ n := match n with Npos p => Zpos p | _ => Z0 end. + + Notation pow_pos_plus := (Ring_theory.pow_pos_Pplus _ Rsth Reqe.(Rmul_ext) + ARth.(ARmul_comm) ARth.(ARmul_assoc)). + + Lemma isIn_correct_aux : forall l e1 e2 p1 p2, + match + (if PExpr_eq e1 e2 then + match Zminus (Zpos p1) (Zpos p2) with + | Zpos p => Some (Npos p, PEc cI) + | Z0 => Some (N0, PEc cI) + | Zneg p => Some (N0, NPEpow e2 (Npos p)) + end + else None) + with + | Some(n, e3) => + NPEeval l (PEpow e2 (Npos p2)) == + NPEeval l (PEmul (PEpow e1 (ZtoN (Zpos p1 - NtoZ n))) e3) /\ + (Zpos p1 > NtoZ n)%Z + | _ => True + end. +Proof. + intros l e1 e2 p1 p2; generalize (PExpr_eq_semi_correct l e1 e2); + case (PExpr_eq e1 e2); simpl; auto; intros H. + case_eq ((p1 ?= p2)%positive Eq);intros;simpl. + repeat rewrite pow_th.(rpow_pow_N);simpl. split. 2:refine (refl_equal _). + rewrite (Pcompare_Eq_eq _ _ H0). + rewrite H;[trivial | ring [ (morph1 CRmorph)]]. + fold (NPEpow e2 (Npos (p2 - p1))). + rewrite NPEpow_correct;simpl. + repeat rewrite pow_th.(rpow_pow_N);simpl. + rewrite H;trivial. split. 2:refine (refl_equal _). + rewrite <- pow_pos_plus; rewrite Pplus_minus;auto. apply ZC2;trivial. + repeat rewrite pow_th.(rpow_pow_N);simpl. + rewrite H;trivial. + change (ZtoN + match (p1 ?= p1 - p2)%positive Eq with + | Eq => 0 + | Lt => Zneg (p1 - p2 - p1) + | Gt => Zpos (p1 - (p1 - p2)) + end) with (ZtoN (Zpos p1 - Zpos (p1 -p2))). + replace (Zpos (p1 - p2)) with (Zpos p1 - Zpos p2)%Z. + split. + repeat rewrite Zth.(Rsub_def). rewrite (Ring_theory.Ropp_add Zsth Zeqe Zth). + rewrite Zplus_assoc. simpl. rewrite Pcompare_refl. simpl. + ring [ (morph1 CRmorph)]. + assert (Zpos p1 > 0 /\ Zpos p2 > 0)%Z. split;refine (refl_equal _). + apply Zplus_gt_reg_l with (Zpos p2). + rewrite Zplus_minus. change (Zpos p2 + Zpos p1 > 0 + Zpos p1)%Z. + apply Zplus_gt_compat_r. refine (refl_equal _). + simpl;rewrite H0;trivial. +Qed. + +Lemma pow_pos_pow_pos : forall x p1 p2, pow_pos rmul (pow_pos rmul x p1) p2 == pow_pos rmul x (p1*p2). +induction p1;simpl;intros;repeat rewrite pow_pos_mul;repeat rewrite pow_pos_plus;simpl. +ring [(IHp1 p2)]. ring [(IHp1 p2)]. auto. +Qed. -Theorem isIn_correct: forall l e1 e2, - match isIn e1 e2 with - (Some e3) => NPEeval l e2 == NPEeval l (NPEmul e1 e3) - | _ => True + +Theorem isIn_correct: forall l e1 p1 e2 p2, + match isIn e1 p1 e2 p2 with + | Some(n, e3) => + NPEeval l (PEpow e2 (Npos p2)) == + NPEeval l (PEmul (PEpow e1 (ZtoN (Zpos p1 - NtoZ n))) e3) /\ + (Zpos p1 > NtoZ n)%Z + | _ => True end. Proof. -intros l e1 e2; elim e2; simpl; auto. - intros c; - generalize (PExpr_eq_semi_correct l e1 (PEc c)); - case (PExpr_eq e1 (PEc c)); simpl; auto; intros H. - rewrite NPEmul_correct; simpl; auto. - rewrite H; auto; simpl. - rewrite (morph1 CRmorph); rewrite (ARmul_1_r Rsth ARth); auto. - intros p; - generalize (PExpr_eq_semi_correct l e1 (PEX C p)); - case (PExpr_eq e1 (PEX C p)); simpl; auto; intros H. - rewrite NPEmul_correct; simpl; auto. - rewrite H; auto; simpl. - rewrite (morph1 CRmorph); rewrite (ARmul_1_r Rsth ARth); auto. - intros p Hrec p1 Hrec1. - generalize (PExpr_eq_semi_correct l e1 (PEadd p p1)); - case (PExpr_eq e1 (PEadd p p1)); simpl; auto; intros H. - rewrite NPEmul_correct; simpl; auto. - rewrite H; auto; simpl. - rewrite (morph1 CRmorph); rewrite (ARmul_1_r Rsth ARth); auto. - intros p Hrec p1 Hrec1. - generalize (PExpr_eq_semi_correct l e1 (PEsub p p1)); - case (PExpr_eq e1 (PEsub p p1)); simpl; auto; intros H. - rewrite NPEmul_correct; simpl; auto. - rewrite H; auto; simpl. - rewrite (morph1 CRmorph); rewrite (ARmul_1_r Rsth ARth); auto. - intros p; case (isIn e1 p). - intros p2 Hrec p1 Hrec1. - rewrite Hrec; auto; simpl. - repeat (rewrite NPEmul_correct; simpl; auto). - intros _ p1; case (isIn e1 p1); auto. - intros p2 H; rewrite H. - repeat (rewrite NPEmul_correct; simpl; auto). - ring. - intros p; - generalize (PExpr_eq_semi_correct l e1 (PEopp p)); - case (PExpr_eq e1 (PEopp p)); simpl; auto; intros H. - rewrite NPEmul_correct; simpl; auto. - rewrite H; auto; simpl. - rewrite (morph1 CRmorph); rewrite (ARmul_1_r Rsth ARth); auto. +Opaque NPEpow. +intros l e1 p1 e2; generalize p1;clear p1;elim e2; intros; + try (refine (isIn_correct_aux l e1 _ p1 p2);fail);simpl isIn. +generalize (H p1 p2);clear H;destruct (isIn e1 p1 p p2). destruct p3. +destruct n. + simpl. rewrite NPEmul_correct. simpl; rewrite NPEpow_correct;simpl. + repeat rewrite pow_th.(rpow_pow_N);simpl. + rewrite pow_pos_mul;intros (H,H1);split;[ring[H]|trivial]. + generalize (H0 p4 p2);clear H0;destruct (isIn e1 p4 p0 p2). destruct p5. + destruct n;simpl. + rewrite NPEmul_correct;repeat rewrite pow_th.(rpow_pow_N);simpl. + intros (H1,H2) (H3,H4). + unfold Zgt in H2, H4;simpl in H2,H4. rewrite H4 in H3;simpl in H3. + rewrite pow_pos_mul. rewrite H1;rewrite H3. + assert (pow_pos rmul (NPEeval l e1) (p1 - p4) * NPEeval l p3 * + (pow_pos rmul (NPEeval l e1) p4 * NPEeval l p5) == + pow_pos rmul (NPEeval l e1) p4 * pow_pos rmul (NPEeval l e1) (p1 - p4) * + NPEeval l p3 *NPEeval l p5) by ring. rewrite H;clear H. + rewrite <- pow_pos_plus. rewrite Pplus_minus. + split. symmetry;apply ARth.(ARmul_assoc). refine (refl_equal _). trivial. + repeat rewrite pow_th.(rpow_pow_N);simpl. + intros (H1,H2) (H3,H4). + unfold Zgt in H2, H4;simpl in H2,H4. rewrite H4 in H3;simpl in H3. + rewrite H2 in H1;simpl in H1. + assert (Zpos p1 > Zpos p6)%Z. + apply Zgt_trans with (Zpos p4). exact H4. exact H2. + unfold Zgt in H;simpl in H;rewrite H. + split. 2:exact H. + rewrite pow_pos_mul. simpl;rewrite H1;rewrite H3. + assert (pow_pos rmul (NPEeval l e1) (p1 - p4) * NPEeval l p3 * + (pow_pos rmul (NPEeval l e1) (p4 - p6) * NPEeval l p5) == + pow_pos rmul (NPEeval l e1) (p1 - p4) * pow_pos rmul (NPEeval l e1) (p4 - p6) * + NPEeval l p3 * NPEeval l p5) by ring. rewrite H0;clear H0. + rewrite <- pow_pos_plus. + replace (p1 - p4 + (p4 - p6))%positive with (p1 - p6)%positive. + rewrite NPEmul_correct. simpl;ring. + assert + (Zpos p1 - Zpos p6 = Zpos p1 - Zpos p4 + (Zpos p4 - Zpos p6))%Z. + change ((Zpos p1 - Zpos p6)%Z = (Zpos p1 + (- Zpos p4) + (Zpos p4 +(- Zpos p6)))%Z). + rewrite <- Zplus_assoc. rewrite (Zplus_assoc (- Zpos p4)). + simpl. rewrite Pcompare_refl. reflexivity. + unfold Zminus, Zopp in H0. simpl in H0. + rewrite H2 in H0;rewrite H4 in H0;rewrite H in H0. inversion H0;trivial. + simpl. repeat rewrite pow_th.(rpow_pow_N). + intros H1 (H2,H3). unfold Zgt in H3;simpl in H3. rewrite H3 in H2;rewrite H3. + rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl. + simpl in H2. rewrite pow_th.(rpow_pow_N);simpl. + rewrite pow_pos_mul. split. ring [H2]. exact H3. + generalize (H0 p1 p2);clear H0;destruct (isIn e1 p1 p0 p2). destruct p3. + destruct n;simpl. rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl. + repeat rewrite pow_th.(rpow_pow_N);simpl. + intros (H1,H2);split;trivial. rewrite pow_pos_mul;ring [H1]. + rewrite NPEmul_correct;simpl;rewrite NPEpow_correct;simpl. + repeat rewrite pow_th.(rpow_pow_N);simpl. rewrite pow_pos_mul. + intros (H1, H2);rewrite H1;split. + unfold Zgt in H2;simpl in H2;rewrite H2;rewrite H2 in H1. + simpl in H1;ring [H1]. trivial. + trivial. + destruct n. trivial. + generalize (H p1 (p0*p2)%positive);clear H;destruct (isIn e1 p1 p (p0*p2)). destruct p3. + destruct n;simpl. repeat rewrite pow_th.(rpow_pow_N). simpl. + intros (H1,H2);split. rewrite pow_pos_pow_pos. trivial. trivial. + repeat rewrite pow_th.(rpow_pow_N). simpl. + intros (H1,H2);split;trivial. + rewrite pow_pos_pow_pos;trivial. + trivial. Qed. Record rsplit : Type := mk_rsplit { @@ -652,90 +843,94 @@ Record rsplit : Type := mk_rsplit { rsplit_right : PExpr C}. (* Stupid name clash *) -Let left := rsplit_left. -Let right := rsplit_right. -Let common := rsplit_common. +Notation left := rsplit_left. +Notation right := rsplit_right. +Notation common := rsplit_common. -Fixpoint split (e1 e2: PExpr C) {struct e1}: rsplit := +Fixpoint split_aux (e1: PExpr C) (p:positive) (e2:PExpr C) {struct e1}: rsplit := match e1 with | PEmul e3 e4 => - let r1 := split e3 e2 in - let r2 := split e4 (right r1) in + let r1 := split_aux e3 p e2 in + let r2 := split_aux e4 p (right r1) in mk_rsplit (NPEmul (left r1) (left r2)) (NPEmul (common r1) (common r2)) (right r2) + | PEpow e3 N0 => mk_rsplit (PEc cI) (PEc cI) e2 + | PEpow e3 (Npos p3) => split_aux e3 (Pmult p3 p) e2 | _ => - match isIn e1 e2 with - Some e3 => mk_rsplit (PEc cI) e1 e3 - | None => mk_rsplit e1 (PEc cI) e2 + match isIn e1 p e2 xH with + | Some (N0,e3) => mk_rsplit (PEc cI) (NPEpow e1 (Npos p)) e3 + | Some (Npos q, e3) => mk_rsplit (NPEpow e1 (Npos q)) (NPEpow e1 (Npos (p - q))) e3 + | None => mk_rsplit (NPEpow e1 (Npos p)) (PEc cI) e2 end end. -Theorem split_correct: forall l e1 e2, - NPEeval l e1 == NPEeval l (NPEmul (left (split e1 e2)) - (common (split e1 e2))) -/\ - NPEeval l e2 == NPEeval l (NPEmul (right (split e1 e2)) - (common (split e1 e2))). +Lemma split_aux_correct_1 : forall l e1 p e2, + let res := match isIn e1 p e2 xH with + | Some (N0,e3) => mk_rsplit (PEc cI) (NPEpow e1 (Npos p)) e3 + | Some (Npos q, e3) => mk_rsplit (NPEpow e1 (Npos q)) (NPEpow e1 (Npos (p - q))) e3 + | None => mk_rsplit (NPEpow e1 (Npos p)) (PEc cI) e2 + end in + NPEeval l (PEpow e1 (Npos p)) == NPEeval l (NPEmul (left res) (common res)) + /\ + NPEeval l e2 == NPEeval l (NPEmul (right res) (common res)). Proof. -intros l e1; elim e1; simpl; auto. - intros c e2; generalize (isIn_correct l (PEc c) e2); - case (isIn (PEc c) e2); auto; intros p; - [intros Hp1; rewrite Hp1 | idtac]; - simpl left; simpl common; simpl right; auto; - repeat rewrite NPEmul_correct; simpl; split; - try rewrite (morph1 CRmorph); ring. - intros p e2; generalize (isIn_correct l (PEX C p) e2); - case (isIn (PEX C p) e2); auto; intros p1; - [intros Hp1; rewrite Hp1 | idtac]; - simpl left; simpl common; simpl right; auto; - repeat rewrite NPEmul_correct; simpl; split; - try rewrite (morph1 CRmorph); ring. - intros p1 _ p2 _ e2; generalize (isIn_correct l (PEadd p1 p2) e2); - case (isIn (PEadd p1 p2) e2); auto; intros p; - [intros Hp1; rewrite Hp1 | idtac]; - simpl left; simpl common; simpl right; auto; - repeat rewrite NPEmul_correct; simpl; split; - try rewrite (morph1 CRmorph); ring. - intros p1 _ p2 _ e2; generalize (isIn_correct l (PEsub p1 p2) e2); - case (isIn (PEsub p1 p2) e2); auto; intros p; - [intros Hp1; rewrite Hp1 | idtac]; - simpl left; simpl common; simpl right; auto; - repeat rewrite NPEmul_correct; simpl; split; - try rewrite (morph1 CRmorph); ring. - intros p1 Hp1 p2 Hp2 e2. - repeat rewrite NPEmul_correct; simpl; split. - case (Hp1 e2); case (Hp2 (right (split p1 e2))). - intros tmp1 _ tmp2 _; rewrite tmp1; rewrite tmp2. - repeat rewrite NPEmul_correct; simpl. - ring. - case (Hp1 e2); case (Hp2 (right (split p1 e2))). - intros _ tmp1 _ tmp2; rewrite tmp2; - repeat rewrite NPEmul_correct; simpl. - rewrite tmp1. - repeat rewrite NPEmul_correct; simpl. - ring. - intros p _ e2; generalize (isIn_correct l (PEopp p) e2); - case (isIn (PEopp p) e2); auto; intros p1; - [intros Hp1; rewrite Hp1 | idtac]; - simpl left; simpl common; simpl right; auto; - repeat rewrite NPEmul_correct; simpl; split; - try rewrite (morph1 CRmorph); ring. + intros. unfold res;clear res; generalize (isIn_correct l e1 p e2 xH). + destruct (isIn e1 p e2 1). destruct p0. + Opaque NPEpow NPEmul. + destruct n;simpl; + (repeat rewrite NPEmul_correct;simpl; + repeat rewrite NPEpow_correct;simpl; + repeat rewrite pow_th.(rpow_pow_N);simpl). + intros (H, Hgt);split;try ring [H CRmorph.(morph1)]. + intros (H, Hgt). unfold Zgt in Hgt;simpl in Hgt;rewrite Hgt in H. + simpl in H;split;try ring [H]. + rewrite <- pow_pos_plus. rewrite Pplus_minus. reflexivity. trivial. + simpl;intros. repeat rewrite NPEmul_correct;simpl. + rewrite NPEpow_correct;simpl. split;ring [CRmorph.(morph1)]. Qed. +Theorem split_aux_correct: forall l e1 p e2, + NPEeval l (PEpow e1 (Npos p)) == + NPEeval l (NPEmul (left (split_aux e1 p e2)) (common (split_aux e1 p e2))) +/\ + NPEeval l e2 == NPEeval l (NPEmul (right (split_aux e1 p e2)) + (common (split_aux e1 p e2))). +Proof. +intros l; induction e1;intros k e2; try refine (split_aux_correct_1 l _ k e2);simpl. +generalize (IHe1_1 k e2); clear IHe1_1. +generalize (IHe1_2 k (rsplit_right (split_aux e1_1 k e2))); clear IHe1_2. +simpl. repeat (rewrite NPEmul_correct;simpl). +repeat rewrite pow_th.(rpow_pow_N);simpl. +intros (H1,H2) (H3,H4);split. +rewrite pow_pos_mul. rewrite H1;rewrite H3. ring. +rewrite H4;rewrite H2;ring. +destruct n;simpl. +split. repeat rewrite pow_th.(rpow_pow_N);simpl. +rewrite NPEmul_correct. simpl. + induction k;simpl;try ring [CRmorph.(morph1)]; ring [IHk CRmorph.(morph1)]. + rewrite NPEmul_correct;simpl. ring [CRmorph.(morph1)]. +generalize (IHe1 (p*k)%positive e2);clear IHe1;simpl. +repeat rewrite NPEmul_correct;simpl. +repeat rewrite pow_th.(rpow_pow_N);simpl. +rewrite pow_pos_pow_pos. intros [H1 H2];split;ring [H1 H2]. +Qed. +Definition split e1 e2 := split_aux e1 xH e2. + Theorem split_correct_l: forall l e1 e2, NPEeval l e1 == NPEeval l (NPEmul (left (split e1 e2)) (common (split e1 e2))). Proof. -intros l e1 e2; case (split_correct l e1 e2); auto. +intros l e1 e2; case (split_aux_correct l e1 xH e2);simpl. +rewrite pow_th.(rpow_pow_N);simpl;auto. Qed. Theorem split_correct_r: forall l e1 e2, NPEeval l e2 == NPEeval l (NPEmul (right (split e1 e2)) (common (split e1 e2))). Proof. -intros l e1 e2; case (split_correct l e1 e2); auto. +intros l e1 e2; case (split_aux_correct l e1 xH e2);simpl;auto. Qed. Fixpoint Fnorm (e : FExpr) : linear := @@ -777,6 +972,9 @@ Fixpoint Fnorm (e : FExpr) : linear := mk_linear (NPEmul (num x) (denum y)) (NPEmul (denum x) (num y)) (num y :: condition x ++ condition y) + | FEpow e1 n => + let x := Fnorm e1 in + mk_linear (NPEpow (num x) n) (NPEpow (denum x) n) (condition x) end. @@ -789,6 +987,18 @@ Eval compute (FEadd (FEinv (FEX xH%positive)) (FEinv (FEX (xO xH)%positive))))). *) + Lemma pow_pos_not_0 : forall x, ~x==0 -> forall p, ~pow_pos rmul x p == 0. +Proof. + induction p;simpl. + rewrite <- ARth.(ARmul_assoc). + intro Hp;assert (H1 := @rmul_reg_l _ (pow_pos rmul x p * pow_pos rmul x p) 0 H). + apply IHp. + rewrite (@rmul_reg_l _ (pow_pos rmul x p) 0 IHp). rewrite H1. rewrite Hp;ring. ring. + reflexivity. + intro Hp;apply IHp. rewrite (@rmul_reg_l _ (pow_pos rmul x p) 0 IHp). + rewrite Hp;ring. reflexivity. trivial. +Qed. + Theorem Pcond_Fnorm: forall l e, PCond l (condition (Fnorm e)) -> ~ NPEeval l (denum (Fnorm e)) == 0. @@ -849,6 +1059,11 @@ intros l e; elim e. specialize PCond_cons_inv_r with (1:=Hcond); intro Hcond1. apply PCond_app_inv_l with (1 := Hcond1). apply PCond_cons_inv_l with (1:=Hcond). + simpl;intros e1 Hrec1 n Hcond. + rewrite NPEpow_correct. + simpl;rewrite pow_th.(rpow_pow_N). + destruct n;simpl;intros. + apply AFth.(AF_1_neq_0). apply pow_pos_not_0;auto. Qed. Hint Resolve Pcond_Fnorm. @@ -928,6 +1143,22 @@ rewrite (He1 HH1); rewrite (He2 HH2). repeat rewrite NPEmul_correct;simpl. apply rdiv7; auto. apply PCond_cons_inv_l with ( 1 := HH ). + +intros e1 He1 n Hcond;assert (He1' := He1 Hcond);clear He1. +repeat rewrite NPEpow_correct;simpl;repeat rewrite pow_th.(rpow_pow_N). +rewrite He1';clear He1'. +destruct n;simpl. apply rdiv1. +generalize (NPEeval l (num (Fnorm e1))) (NPEeval l (denum (Fnorm e1))) + (Pcond_Fnorm _ _ Hcond). +intros r r0 Hdiff;induction p;simpl. +repeat (rewrite <- rdiv4;trivial). +intro Hp;apply (pow_pos_not_0 Hdiff p). rewrite (@rmul_reg_l _ (pow_pos rmul r0 p) 0 Hdiff). +rewrite Hp;ring. reflexivity. +apply pow_pos_not_0;trivial. apply pow_pos_not_0;trivial. +rewrite IHp;reflexivity. +rewrite <- rdiv4;trivial. apply pow_pos_not_0;trivial. apply pow_pos_not_0;trivial. +rewrite IHp;reflexivity. +reflexivity. Qed. Theorem Fnorm_crossproduct: @@ -951,16 +1182,19 @@ rewrite Fnorm_FEeval_PEeval in |- *. Qed. (* Correctness lemmas of reflexive tactics *) +Notation Ninterp_PElist := (interp_PElist rO radd rmul rsub ropp req phi Cp_phi rpow). +Notation Nmk_monpol_list := (mk_monpol_list cO cI cadd cmul csub copp ceqb). Theorem Fnorm_correct: - forall l fe, - Peq ceqb (Nnorm (num (Fnorm fe))) (Pc cO) = true -> - PCond l (condition (Fnorm fe)) -> FEeval l fe == 0. -intros l fe H H1; + forall n l lpe fe, + Ninterp_PElist l lpe -> + Peq ceqb (Nnorm n (Nmk_monpol_list lpe) (num (Fnorm fe))) (Pc cO) = true -> + PCond l (condition (Fnorm fe)) -> FEeval l fe == 0. +intros n l lpe fe Hlpe H H1; apply eq_trans with (1 := Fnorm_FEeval_PEeval l fe H1). apply rdiv8; auto. transitivity (NPEeval l (PEc cO)); auto. -apply (ring_correct Rsth Reqe ARth CRmorph); auto. +apply (ring_correct Rsth Reqe ARth CRmorph) with n lpe;trivial. simpl; apply (morph0 CRmorph); auto. Qed. @@ -969,31 +1203,50 @@ Qed. Definition display_linear l num den := NPphi_dev l num / NPphi_dev l den. -Theorem Pphi_dev_div_ok: - forall l fe nfe, - Fnorm fe = nfe -> - PCond l (condition nfe) -> - FEeval l fe == display_linear l (Nnorm (num nfe)) (Nnorm (denum nfe)). +Definition display_pow_linear l num den := + NPphi_pow l num / NPphi_pow l den. + +Theorem Field_rw_correct : + forall n lpe l, + Ninterp_PElist l lpe -> + forall lmp, Nmk_monpol_list lpe = lmp -> + forall fe nfe, Fnorm fe = nfe -> + PCond l (condition nfe) -> + FEeval l fe == display_linear l (Nnorm n lmp (num nfe)) (Nnorm n lmp (denum nfe)). Proof. - intros l fe nfe eq_nfe H; subst nfe. + intros n lpe l Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp. apply eq_trans with (1 := Fnorm_FEeval_PEeval _ _ H). unfold display_linear; apply SRdiv_ext; - apply (Pphi_dev_ok Rsth Reqe ARth CRmorph); reflexivity. + eapply (ring_rw_correct Rsth Reqe ARth CRmorph);eauto. +Qed. + +Theorem Field_rw_pow_correct : + forall n lpe l, + Ninterp_PElist l lpe -> + forall lmp, Nmk_monpol_list lpe = lmp -> + forall fe nfe, Fnorm fe = nfe -> + PCond l (condition nfe) -> + FEeval l fe == display_pow_linear l (Nnorm n lmp (num nfe)) (Nnorm n lmp (denum nfe)). +Proof. + intros n lpe l Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp. + apply eq_trans with (1 := Fnorm_FEeval_PEeval _ _ H). + unfold display_pow_linear; apply SRdiv_ext; + eapply (ring_rw_pow_correct Rsth Reqe ARth CRmorph);eauto. Qed. -(* solving a field equation *) Theorem Field_correct : - forall l fe1 fe2, + forall n l lpe fe1 fe2, Ninterp_PElist l lpe -> + forall lmp, Nmk_monpol_list lpe = lmp -> forall nfe1, Fnorm fe1 = nfe1 -> forall nfe2, Fnorm fe2 = nfe2 -> - Peq ceqb (Nnorm (PEmul (num nfe1) (denum nfe2))) - (Nnorm (PEmul (num nfe2) (denum nfe1))) = true -> + Peq ceqb (Nnorm n lmp (PEmul (num nfe1) (denum nfe2))) + (Nnorm n lmp (PEmul (num nfe2) (denum nfe1))) = true -> PCond l (condition nfe1 ++ condition nfe2) -> FEeval l fe1 == FEeval l fe2. Proof. -intros l fe1 fe2 nfe1 eq1 nfe2 eq2 Hnorm Hcond; subst nfe1 nfe2. +intros n l lpe fe1 fe2 Hlpe lmp eq_lmp nfe1 eq1 nfe2 eq2 Hnorm Hcond; subst nfe1 nfe2 lmp. apply Fnorm_crossproduct; trivial. -apply (ring_correct Rsth Reqe ARth CRmorph); trivial. +eapply (ring_correct Rsth Reqe ARth CRmorph); eauto. Qed. (* simplify a field equation : generate the crossproduct and simplify @@ -1002,42 +1255,98 @@ Theorem Field_simplify_eq_old_correct : forall l fe1 fe2 nfe1 nfe2, Fnorm fe1 = nfe1 -> Fnorm fe2 = nfe2 -> - NPphi_dev l (Nnorm (PEmul (num nfe1) (denum nfe2))) == - NPphi_dev l (Nnorm (PEmul (num nfe2) (denum nfe1))) -> + NPphi_dev l (Nnorm O nil (PEmul (num nfe1) (denum nfe2))) == + NPphi_dev l (Nnorm O nil (PEmul (num nfe2) (denum nfe1))) -> PCond l (condition nfe1 ++ condition nfe2) -> FEeval l fe1 == FEeval l fe2. Proof. intros l fe1 fe2 nfe1 nfe2 eq1 eq2 Hcrossprod Hcond; subst nfe1 nfe2. apply Fnorm_crossproduct; trivial. -rewrite (Pphi_dev_gen_ok Rsth Reqe ARth CRmorph) in |- *. -rewrite (Pphi_dev_gen_ok Rsth Reqe ARth CRmorph) in |- *. +match goal with + [ |- NPEeval l ?x == NPEeval l ?y] => + rewrite (ring_rw_correct Rsth Reqe ARth CRmorph pow_th get_sign_spec + O nil l I (refl_equal nil) x (refl_equal (Nnorm O nil x))); + rewrite (ring_rw_correct Rsth Reqe ARth CRmorph pow_th get_sign_spec + O nil l I (refl_equal nil) y (refl_equal (Nnorm O nil y))) + end. trivial. Qed. Theorem Field_simplify_eq_correct : - forall l fe1 fe2, + forall n l lpe fe1 fe2, + Ninterp_PElist l lpe -> + forall lmp, Nmk_monpol_list lpe = lmp -> + forall nfe1, Fnorm fe1 = nfe1 -> + forall nfe2, Fnorm fe2 = nfe2 -> + forall den, split (denum nfe1) (denum nfe2) = den -> + NPphi_dev l (Nnorm n lmp (PEmul (num nfe1) (right den))) == + NPphi_dev l (Nnorm n lmp (PEmul (num nfe2) (left den))) -> + PCond l (condition nfe1 ++ condition nfe2) -> + FEeval l fe1 == FEeval l fe2. +Proof. +intros n l lpe fe1 fe2 Hlpe lmp Hlmp nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond; + subst nfe1 nfe2 den lmp. +apply Fnorm_crossproduct; trivial. +simpl in |- *. +rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))) in |- *. +rewrite (split_correct_r l (denum (Fnorm fe1)) (denum (Fnorm fe2))) in |- *. +rewrite NPEmul_correct in |- *. +rewrite NPEmul_correct in |- *. +simpl in |- *. +repeat rewrite (ARmul_assoc ARth) in |- *. +rewrite <-( + let x := PEmul (num (Fnorm fe1)) + (rsplit_right (split (denum (Fnorm fe1)) (denum (Fnorm fe2)))) in +ring_rw_correct Rsth Reqe ARth CRmorph pow_th get_sign_spec n lpe l + Hlpe (refl_equal (Nmk_monpol_list lpe)) + x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod. +rewrite <-( + let x := (PEmul (num (Fnorm fe2)) + (rsplit_left + (split (denum (Fnorm fe1)) (denum (Fnorm fe2))))) in + ring_rw_correct Rsth Reqe ARth CRmorph pow_th get_sign_spec n lpe l + Hlpe (refl_equal (Nmk_monpol_list lpe)) + x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod. +simpl in Hcrossprod. +rewrite Hcrossprod in |- *. +reflexivity. +Qed. + +Theorem Field_simplify_eq_pow_correct : + forall n l lpe fe1 fe2, + Ninterp_PElist l lpe -> + forall lmp, Nmk_monpol_list lpe = lmp -> forall nfe1, Fnorm fe1 = nfe1 -> forall nfe2, Fnorm fe2 = nfe2 -> forall den, split (denum nfe1) (denum nfe2) = den -> - NPphi_dev l (Nnorm (PEmul (num nfe1) (right den))) == - NPphi_dev l (Nnorm (PEmul (num nfe2) (left den))) -> + NPphi_pow l (Nnorm n lmp (PEmul (num nfe1) (right den))) == + NPphi_pow l (Nnorm n lmp (PEmul (num nfe2) (left den))) -> PCond l (condition nfe1 ++ condition nfe2) -> FEeval l fe1 == FEeval l fe2. Proof. -intros l fe1 fe2 nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond; - subst nfe1 nfe2 den. +intros n l lpe fe1 fe2 Hlpe lmp Hlmp nfe1 eq1 nfe2 eq2 den eq3 Hcrossprod Hcond; + subst nfe1 nfe2 den lmp. apply Fnorm_crossproduct; trivial. simpl in |- *. -elim (split_correct l (denum (Fnorm fe1)) (denum (Fnorm fe2))); intros. -rewrite H in |- *. -rewrite H0 in |- *. -clear H H0. +rewrite (split_correct_l l (denum (Fnorm fe1)) (denum (Fnorm fe2))) in |- *. +rewrite (split_correct_r l (denum (Fnorm fe1)) (denum (Fnorm fe2))) in |- *. rewrite NPEmul_correct in |- *. rewrite NPEmul_correct in |- *. simpl in |- *. repeat rewrite (ARmul_assoc ARth) in |- *. -rewrite <- (Pphi_dev_gen_ok Rsth Reqe ARth CRmorph) in Hcrossprod. -rewrite <- (Pphi_dev_gen_ok Rsth Reqe ARth CRmorph) in Hcrossprod. +rewrite <-( + let x := PEmul (num (Fnorm fe1)) + (rsplit_right (split (denum (Fnorm fe1)) (denum (Fnorm fe2)))) in +ring_rw_pow_correct Rsth Reqe ARth CRmorph pow_th get_sign_spec n lpe l + Hlpe (refl_equal (Nmk_monpol_list lpe)) + x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod. +rewrite <-( + let x := (PEmul (num (Fnorm fe2)) + (rsplit_left + (split (denum (Fnorm fe1)) (denum (Fnorm fe2))))) in + ring_rw_pow_correct Rsth Reqe ARth CRmorph pow_th get_sign_spec n lpe l + Hlpe (refl_equal (Nmk_monpol_list lpe)) + x (refl_equal (Nnorm n (Nmk_monpol_list lpe) x))) in Hcrossprod. simpl in Hcrossprod. rewrite Hcrossprod in |- *. reflexivity. @@ -1100,7 +1409,7 @@ Fixpoint Fcons0 (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) := match l with nil => cons e nil | cons a l1 => - if Peq ceqb (Nnorm e) (Nnorm a) then l else cons a (Fcons0 e l1) + if Peq ceqb (Nnorm O nil e) (Nnorm O nil a) then l else cons a (Fcons0 e l1) end. Theorem PFcons0_fcons_inv: @@ -1108,8 +1417,8 @@ Theorem PFcons0_fcons_inv: intros l a l1; elim l1; simpl Fcons0; auto. simpl; auto. intros a0 l0. -generalize (ring_correct Rsth Reqe ARth CRmorph l a a0); - case (Peq ceqb (Nnorm a) (Nnorm a0)). +generalize (ring_correct Rsth Reqe ARth CRmorph pow_th O l nil a a0). simpl. + case (Peq ceqb (Nnorm O nil a) (Nnorm O nil a0)). intros H H0 H1; split; auto. rewrite H; auto. generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto. @@ -1125,6 +1434,7 @@ Qed. Fixpoint Fcons00 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) := match e with PEmul e1 e2 => Fcons00 e1 (Fcons00 e2 l) + | PEpow e1 _ => Fcons00 e1 l | _ => Fcons0 e l end. @@ -1137,9 +1447,12 @@ intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail). case (H0 _ H3); intros H4 H5; split; auto. simpl in |- *. apply field_is_integral_domain; trivial. + simpl;intros. rewrite pow_th.(rpow_pow_N). + destruct (H _ H0);split;auto. + destruct n;simpl. apply AFth.(AF_1_neq_0). + apply pow_pos_not_0;trivial. Qed. - Definition Pcond_simpl_gen := fcons_correct _ PFcons00_fcons_inv. @@ -1167,6 +1480,7 @@ Qed. Fixpoint Fcons1 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) := match e with PEmul e1 e2 => Fcons1 e1 (Fcons1 e2 l) + | PEpow e _ => Fcons1 e l | PEopp e => if ceqb (copp cI) cO then absurd_PCond else Fcons1 e l | PEc c => if ceqb c cO then absurd_PCond else l | _ => Fcons0 e l @@ -1196,6 +1510,9 @@ intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail). rewrite (morph1 CRmorph) in H0. rewrite (morph0 CRmorph) in H0. trivial. + intros;simpl. destruct (H _ H0);split;trivial. + rewrite pow_th.(rpow_pow_N). destruct n;simpl. + apply AFth.(AF_1_neq_0). apply pow_pos_not_0;trivial. Qed. Definition Fcons2 e l := Fcons1 (PExpr_simp e) l. @@ -1214,30 +1531,6 @@ Definition Pcond_simpl_complete := End Fcons_simpl. -Let Mpc := MPcond_map cO cI cadd cmul csub copp ceqb. -Let Mp := MPcond_dev rO rI radd rmul req cO cI ceqb phi. -Let Subst := PNSubstL cO cI cadd cmul ceqb. - -(* simplification + rewriting *) -Theorem Field_subst_correct : -forall l ul fe m n, - PCond l (Fapp Fcons00 (condition (Fnorm fe)) nil) -> - Mp (Mpc ul) l -> - Peq ceqb (Subst (Nnorm (num (Fnorm fe))) (Mpc ul) m n) (Pc cO) = true -> - FEeval l fe == 0. -intros l ul fe m n H H1 H2. -assert (H3 := (Pcond_simpl_gen _ _ H)). -apply eq_trans with (1 := Fnorm_FEeval_PEeval l fe - (Pcond_simpl_gen _ _ H)). -apply rdiv8; auto. -rewrite (PNSubstL_dev_ok Rsth Reqe ARth CRmorph m n - _ (num (Fnorm fe)) l H1). -rewrite <-(Ring_polynom.Pphi_Pphi_dev Rsth Reqe ARth CRmorph). -rewrite (fun x => Peq_ok Rsth Reqe CRmorph x (Pc cO)); auto. -simpl; apply (morph0 CRmorph); auto. -Qed. - - End AlmostField. Section FieldAndSemiField. diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v index 7df68cc05..a456f4779 100644 --- a/contrib/setoid_ring/InitialRing.v +++ b/contrib/setoid_ring/InitialRing.v @@ -7,16 +7,21 @@ (************************************************************************) Require Import ZArith_base. +Require Import Zpow_def. Require Import BinInt. Require Import BinNat. Require Import Setoid. Require Import Ring_theory. -Require Import Ring_tac. Require Import Ring_polynom. + Set Implicit Arguments. Import RingSyntax. + +(* An object to return when an expression is not recognized as a constant *) +Definition NotConstant := false. + (** Z is a ring and a setoid*) Lemma Zsth : Setoid_Theory Z (@eq Z). @@ -88,6 +93,21 @@ Section ZMORPHISM. | Zneg p => -(gen_phiPOS p) end. Notation "[ x ]" := (gen_phiZ x). + + Definition get_signZ z := + match z with + | Zneg p => Some (Zpos p) + | _ => None + end. + + Lemma get_signZ_th : sign_theory ropp req gen_phiZ get_signZ. + Proof. + constructor. + destruct c;intros;try discriminate. + injection H;clear H;intros H1;subst c'. + simpl;rrefl. + Qed. + Section ALMOST_RING. Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req. @@ -346,7 +366,8 @@ Section NMORPHISM. End NMORPHISM. (* syntaxification of constants in an abstract ring: - the inverse of gen_phiPOS *) + the inverse of gen_phiPOS + Why we do not reconnize only rI ?????? *) Ltac inv_gen_phi_pos rI add mul t := let rec inv_cst t := match t with @@ -396,65 +417,8 @@ End NMORPHISM. end end. -(* coefs = Z (abstract ring) *) -Module Zpol. - -Definition ring_gen_correct - R rO rI radd rmul rsub ropp req rSet req_th Rth := - @ring_correct R rO rI radd rmul rsub ropp req rSet req_th - (Rth_ARth rSet req_th Rth) - Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool - (@gen_phiZ R rO rI radd rmul ropp) - (gen_phiZ_morph rSet req_th Rth). - -Definition ring_rw_gen_correct - R rO rI radd rmul rsub ropp req rSet req_th Rth := - @Pphi_dev_ok R rO rI radd rmul rsub ropp req rSet req_th - (Rth_ARth rSet req_th Rth) - Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool - (@gen_phiZ R rO rI radd rmul ropp) - (gen_phiZ_morph rSet req_th Rth). - -Definition ring_gen_eq_correct R rO rI radd rmul rsub ropp Rth := - @ring_gen_correct - R rO rI radd rmul rsub ropp (@eq R) (Eqsth R) (Eq_ext _ _ _) Rth. - -Definition ring_rw_gen_eq_correct R rO rI radd rmul rsub ropp Rth := - @ring_rw_gen_correct - R rO rI radd rmul rsub ropp (@eq R) (Eqsth R) (Eq_ext _ _ _) Rth. - -End Zpol. - -(* coefs = N (abstract semi-ring) *) -Module Npol. - -Definition ring_gen_correct - R rO rI radd rmul req rSet req_th SRth := - @ring_correct R rO rI radd rmul (SRsub radd) (@SRopp R) req rSet - (SReqe_Reqe req_th) - (SRth_ARth rSet SRth) - N 0%N 1%N Nplus Nmult (SRsub Nplus) (@SRopp N) Neq_bool - (@gen_phiN R rO rI radd rmul) - (gen_phiN_morph rSet req_th SRth). - -Definition ring_rw_gen_correct - R rO rI radd rmul req rSet req_th SRth := - @Pphi_dev_ok R rO rI radd rmul (SRsub radd) (@SRopp R) req rSet - (SReqe_Reqe req_th) - (SRth_ARth rSet SRth) - N 0%N 1%N Nplus Nmult (SRsub Nplus) (@SRopp N) Neq_bool - (@gen_phiN R rO rI radd rmul) - (gen_phiN_morph rSet req_th SRth). - -Definition ring_gen_eq_correct R rO rI radd rmul SRth := - @ring_gen_correct - R rO rI radd rmul (@eq R) (Eqsth R) (Eq_s_ext _ _) SRth. - -Definition ring_rw_gen_eq_correct' R rO rI radd rmul SRth := - @ring_rw_gen_correct - R rO rI radd rmul (@eq R) (Eqsth R) (Eq_s_ext _ _) SRth. - -End Npol. +(* A simpl tactic reconninzing nothing *) + Ltac inv_morph_nothing t := constr:(NotConstant). Ltac coerce_to_almost_ring set ext rspec := @@ -481,7 +445,46 @@ Ltac abstract_ring_morphism set ext rspec := | _ => fail 1 "bad ring structure" end. -Ltac ring_elements set ext rspec rk := +Record hypo : Type := mkhypo { + hypo_type : Type; + hypo_proof : hypo_type + }. + +Ltac gen_ring_pow set arth pspec := + match pspec with + | None => + match type of arth with + | @almost_ring_theory ?R ?rO ?rI ?radd ?rmul ?rsub ?ropp ?req => + constr:(mkhypo (@pow_N_th R rI rmul req set)) + | _ => fail 1 "gen_ring_pow" + end + | Some ?t => constr:(t) + end. + +Ltac default_sign_spec morph := + match type of morph with + | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req + ?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceq_b ?phi => + constr:(mkhypo (@get_sign_None_th R ropp req C phi)) + | _ => fail 1 "ring anomaly : default_sign_spec" + end. + +Ltac gen_ring_sign set rspec morph sspec rk := + match sspec with + | None => + match rk with + | Abstract => + match type of rspec with + | @ring_theory ?R ?rO ?rI ?radd ?rmul ?rsub ?ropp ?req => + constr:(mkhypo (@get_signZ_th R rO rI radd rmul ropp req set)) + | _ => default_sign_spec morph + end + | _ => default_sign_spec morph + end + | Some ?t => constr:(t) + end. + +Ltac ring_elements set ext rspec pspec sspec rk := let arth := coerce_to_almost_ring set ext rspec in let ext_r := coerce_to_ring_ext ext in let morph := @@ -496,16 +499,78 @@ Ltac ring_elements set ext rspec rk := | @Morphism ?m => m | _ => fail 1 "ill-formed ring kind" end in - fun f => f arth ext_r morph. + let p_spec := gen_ring_pow set arth pspec in + let s_spec := gen_ring_sign set rspec morph sspec rk in + fun f => f arth ext_r morph p_spec s_spec. + (* Given a ring structure and the kind of morphism, returns 2 lemmas (one for ring, and one for ring_simplify). *) -Ltac ring_lemmas set ext rspec rk := - ring_elements set ext rspec rk - ltac:(fun arth ext_r morph => - let lemma1 := constr:(ring_correct set ext_r arth morph) in - let lemma2 := constr:(Pphi_dev_ok set ext_r arth morph) in - fun f => f arth ext_r morph lemma1 lemma2). +Ltac ring_lemmas set ext rspec pspec sspec rk := + let gen_lemma2 := + match pspec with + | None => constr:(ring_rw_correct) + | Some _ => constr:(ring_rw_pow_correct) + end in + ring_elements set ext rspec pspec sspec rk + ltac:(fun arth ext_r morph p_spec s_spec => + match p_spec with + | mkhypo ?pp_spec => + match s_spec with + | mkhypo ?ps_spec => + let lemma1 := + constr:(ring_correct set ext_r arth morph pp_spec) in + let lemma2 := + constr:(gen_lemma2 _ _ _ _ _ _ _ _ set ext_r arth + _ _ _ _ _ _ _ _ _ morph + _ _ _ pp_spec + _ ps_spec) in + fun f => f arth ext_r morph lemma1 lemma2 + | _ => fail 2 "bad sign specification" + end + | _ => fail 1 "bad power specification" + end). + +(* Tactic for constant *) +Ltac isnatcst t := + match t with + O => true + | S ?p => isnatcst p + | _ => false + end. + +Ltac isPcst t := + match t with + | xI ?p => isPcst p + | xO ?p => isPcst p + | xH => constr:true + (* nat -> positive *) + | P_of_succ_nat ?n => isnatcst n + | _ => false + end. + +Ltac isNcst t := + match t with + N0 => constr:true + | Npos ?p => isPcst p + | _ => constr:false + end. + +Ltac isZcst t := + match t with + Z0 => true + | Zpos ?p => isPcst p + | Zneg ?p => isPcst p + (* injection nat -> Z *) + | Z_of_nat ?n => isnatcst n + (* injection N -> Z *) + | Z_of_N ?n => isNcst n + (* *) + | _ => false + end. + + + diff --git a/contrib/setoid_ring/NArithRing.v b/contrib/setoid_ring/NArithRing.v index 0ddf7cfb7..ae067a8a2 100644 --- a/contrib/setoid_ring/NArithRing.v +++ b/contrib/setoid_ring/NArithRing.v @@ -12,18 +12,6 @@ Import InitialRing. Set Implicit Arguments. -Ltac isNcst t := - match t with - N0 => constr:true - | Npos ?p => isNcst p - | xI ?p => isNcst p - | xO ?p => isNcst p - | xH => constr:true - (* nat -> positive *) - | P_of_succ_nat ?n => isNcst n - (* *) - | _ => constr:false - end. Ltac Ncst t := match isNcst t with true => t diff --git a/contrib/setoid_ring/RealField.v b/contrib/setoid_ring/RealField.v index 13896123b..92fbc1b58 100644 --- a/contrib/setoid_ring/RealField.v +++ b/contrib/setoid_ring/RealField.v @@ -1,6 +1,9 @@ -Require Import Raxioms. -Require Import Rdefinitions. +Require Import Nnat. +Require Import ArithRing. Require Export Ring Field. +Require Import Rdefinitions. +Require Import Rpow_def. +Require Import Raxioms. Open Local Scope R_scope. @@ -102,4 +105,28 @@ Lemma Zeq_bool_complete : forall x y, Zeq_bool x y = true. Proof gen_phiZ_complete Rset Rext Rfield Rgen_phiPOS_not_0. -Add Field RField : Rfield (infinite Zeq_bool_complete). +Lemma Rdef_pow_add : forall (x:R) (n m:nat), pow x (n + m) = pow x n * pow x m. +Proof. + intros x n; elim n; simpl in |- *; auto with real. + intros n0 H' m; rewrite H'; auto with real. +Qed. + +Lemma R_power_theory : power_theory 1%R Rmult (eq (A:=R)) nat_of_N pow. +Proof. + constructor. destruct n. reflexivity. + simpl. induction p;simpl. + rewrite ZL6. rewrite Rdef_pow_add;rewrite IHp. symmetry; apply Rmult_assoc. + unfold nat_of_P;simpl;rewrite ZL6;rewrite Rdef_pow_add;rewrite IHp;trivial. + rewrite Rmult_comm;apply Rmult_1_l. +Qed. + +Ltac Rpow_tac t := + match isnatcst t with + | false => constr:(InitialRing.NotConstant) + | _ => constr:(N_of_nat t) + end. + +Add Field RField : Rfield (infinite Zeq_bool_complete, power_tac R_power_theory [Rpow_tac]). + + + diff --git a/contrib/setoid_ring/Ring.v b/contrib/setoid_ring/Ring.v index 167e026f6..1a4e1cc75 100644 --- a/contrib/setoid_ring/Ring.v +++ b/contrib/setoid_ring/Ring.v @@ -9,6 +9,7 @@ Require Import Bool. Require Export Ring_theory. Require Export Ring_base. +Require Export InitialRing. Require Export Ring_tac. Lemma BoolTheory : @@ -25,7 +26,7 @@ reflexivity. destruct x; reflexivity. Qed. -Unboxed Definition bool_eq (b1 b2:bool) := +Definition bool_eq (b1 b2:bool) := if b1 then b2 else negb b2. Lemma bool_eq_ok : forall b1 b2, bool_eq b1 b2 = true -> b1 = b2. diff --git a/contrib/setoid_ring/Ring_polynom.v b/contrib/setoid_ring/Ring_polynom.v index 7317ab212..f2c8a460c 100644 --- a/contrib/setoid_ring/Ring_polynom.v +++ b/contrib/setoid_ring/Ring_polynom.v @@ -1,5 +1,5 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 *) @@ -10,9 +10,11 @@ Set Implicit Arguments. Require Import Setoid. Require Import BinList. Require Import BinPos. +Require Import BinNat. Require Import BinInt. Require Export Ring_theory. +Open Local Scope positive_scope. Import RingSyntax. Section MakeRingPol. @@ -35,6 +37,12 @@ Section MakeRingPol. Variable CRmorph : ring_morph rO rI radd rmul rsub ropp req cO cI cadd cmul csub copp ceqb phi. + (* Power coefficients *) + Variable Cpow : Set. + Variable Cp_phi : N -> Cpow. + Variable rpow : R -> Cpow -> R. + Variable pow_th : power_theory rI rmul req Cp_phi rpow. + (* R notations *) Notation "0" := rO. Notation "1" := rI. @@ -113,12 +121,23 @@ Section MakeRingPol. | _ => Pinj j P end. + Definition mkPinj_pred j P:= + match j with + | xH => P + | xO j => Pinj (Pdouble_minus_one j) P + | xI j => Pinj (xO j) P + end. + Definition mkPX P i Q := match P with | Pc c => if c ?=! cO then mkPinj xH Q else PX P i Q | Pinj _ _ => PX P i Q | PX P' i' Q' => if Q' ?== P0 then PX P' (i' + i) Q else PX P i Q end. + + Definition mkXi i := PX P1 i P0. + + Definition mkX := mkXi 1. (** Opposite of addition *) @@ -323,6 +342,7 @@ Section MakeRingPol. end. Notation "P ** P'" := (Pmul P P'). + (** Monomial **) @@ -331,29 +351,29 @@ Section MakeRingPol. | zmon: positive -> Mon -> Mon | vmon: positive -> Mon -> Mon. - Fixpoint pow (x:R) (i:positive) {struct i}: R := - match i with - | xH => x - | xO i => let p := pow x i in p * p - | xI i => let p := pow x i in x * p * p - end. - Fixpoint Mphi(l:list R) (M: Mon) {struct M} : R := match M with mon0 => rI | zmon j M1 => Mphi (jump j l) M1 | vmon i M1 => let x := hd 0 l in - let xi := pow x i in + let xi := pow_pos rmul x i in (Mphi (tail l) M1) * xi end. - Definition zmon_pred j M := - match j with xH => M | _ => zmon (Ppred j) M end. - Definition mkZmon j M := match M with mon0 => mon0 | _ => zmon j M end. + Definition zmon_pred j M := + match j with xH => M | _ => mkZmon (Ppred j) M end. + + Definition mkVmon i M := + match M with + | mon0 => vmon i mon0 + | zmon j m => vmon i (zmon_pred j m) + | vmon i' m => vmon (i+i') m + end. + Fixpoint MFactor (P: Pol) (M: Mon) {struct P}: Pol * Pol := match P, M with _, mon0 => (Pc cO, P) @@ -434,7 +454,7 @@ Section MakeRingPol. | Pinj j Q => Pphi (jump j l) Q | PX P i Q => let x := hd 0 l in - let xi := pow x i in + let xi := pow_pos rmul x i in (Pphi l P) * xi + (Pphi (tail l) Q) end. @@ -469,26 +489,6 @@ Section MakeRingPol. rewrite Psucc_o_double_minus_one_eq_xO;trivial. simpl;trivial. Qed. - - Lemma pow_Psucc : forall x j, pow x (Psucc j) == x * pow x j. - Proof. - induction j;simpl;rsimpl. - rewrite IHj;rsimpl;mul_push x;rrefl. - Qed. - - Lemma pow_Pplus : forall x i j, pow x (i + j) == pow x i * pow 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 rewrite IHi. - rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite pow_Psucc. - simpl;rsimpl. - rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc. - repeat rewrite IHi;rsimpl. - rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite pow_Psucc; - simpl;rsimpl. - Qed. Lemma Peq_ok : forall P P', (P ?== P') = true -> forall l, P@l == P'@ l. @@ -523,8 +523,11 @@ Section MakeRingPol. rewrite <-jump_Pplus;rewrite Pplus_comm;rrefl. Qed. + Let pow_pos_Pplus := + pow_pos_Pplus rmul Rsth Reqe.(Rmul_ext) ARth.(ARmul_comm) ARth.(ARmul_assoc). + Lemma mkPX_ok : forall l P i Q, - (mkPX P i Q)@l == P@l*(pow (hd 0 l) i) + Q@(tail l). + (mkPX P i Q)@l == P@l*(pow_pos rmul (hd 0 l) i) + Q@(tail l). Proof. intros l P i Q;unfold mkPX. destruct P;try (simpl;rrefl). @@ -533,7 +536,7 @@ Section MakeRingPol. rewrite mkPinj_ok;rsimpl;simpl;rrefl. assert (H := @Peq_ok P3 P0);destruct (P3 ?== P0);simpl;try rrefl. rewrite (H (refl_equal true));trivial. - rewrite Pphi0;rewrite pow_Pplus;rsimpl. + rewrite Pphi0. rewrite pow_pos_Pplus;rsimpl. Qed. Ltac Esimpl := @@ -622,19 +625,19 @@ Section MakeRingPol. Esimpl2;add_push [c];rrefl. destruct p0;simpl;Esimpl2. rewrite IHP'2;simpl. - rsimpl;add_push (P'1@l * (pow (hd 0 l) p));rrefl. + rsimpl;add_push (P'1@l * (pow_pos rmul (hd 0 l) p));rrefl. rewrite IHP'2;simpl. - rewrite jump_Pdouble_minus_one;rsimpl;add_push (P'1@l * (pow (hd 0 l) p));rrefl. + rewrite jump_Pdouble_minus_one;rsimpl;add_push (P'1@l * (pow_pos rmul (hd 0 l) p));rrefl. rewrite IHP'2;rsimpl. add_push (P @ (tail l));rrefl. assert (H := ZPminus_spec p0 p);destruct (ZPminus p0 p);Esimpl2. rewrite IHP'1;rewrite IHP'2;rsimpl. add_push (P3 @ (tail l));rewrite H;rrefl. rewrite IHP'1;rewrite IHP'2;simpl;Esimpl. rewrite H;rewrite Pplus_comm. - rewrite pow_Pplus;rsimpl. + rewrite pow_pos_Pplus;rsimpl. add_push (P3 @ (tail l));rrefl. assert (forall P k l, - (PaddX Padd P'1 k P) @ l == P@l + P'1@l * pow (hd 0 l) k). + (PaddX Padd P'1 k P) @ l == P@l + P'1@l * pow_pos rmul (hd 0 l) k). induction P;simpl;intros;try apply (ARadd_comm ARth). destruct p2;simpl;try apply (ARadd_comm ARth). rewrite jump_Pdouble_minus_one;apply (ARadd_comm ARth). @@ -642,15 +645,15 @@ Section MakeRingPol. rewrite IHP'1;rsimpl; rewrite H1;add_push (P5 @ (tail l0));rrefl. rewrite IHP'1;simpl;Esimpl. rewrite H1;rewrite Pplus_comm. - rewrite pow_Pplus;simpl;Esimpl. + rewrite pow_pos_Pplus;simpl;Esimpl. add_push (P5 @ (tail l0));rrefl. rewrite IHP1;rewrite H1;rewrite Pplus_comm. - rewrite pow_Pplus;simpl;rsimpl. + rewrite pow_pos_Pplus;simpl;rsimpl. add_push (P5 @ (tail l0));rrefl. rewrite H0;rsimpl. add_push (P3 @ (tail l)). rewrite H;rewrite Pplus_comm. - rewrite IHP'2;rewrite pow_Pplus;rsimpl. + rewrite IHP'2;rewrite pow_pos_Pplus;rsimpl. add_push (P3 @ (tail l));rrefl. Qed. @@ -674,20 +677,20 @@ Section MakeRingPol. destruct P;simpl. repeat rewrite Popp_ok;Esimpl2;rsimpl;add_push [c];try rrefl. destruct p0;simpl;Esimpl2. - rewrite IHP'2;simpl;rsimpl;add_push (P'1@l * (pow (hd 0 l) p));trivial. + rewrite IHP'2;simpl;rsimpl;add_push (P'1@l * (pow_pos rmul (hd 0 l) p));trivial. add_push (P @ (jump p0 (jump p0 (tail l))));rrefl. rewrite IHP'2;simpl;rewrite jump_Pdouble_minus_one;rsimpl. - add_push (- (P'1 @ l * pow (hd 0 l) p));rrefl. + add_push (- (P'1 @ l * pow_pos rmul (hd 0 l) p));rrefl. rewrite IHP'2;rsimpl;add_push (P @ (tail l));rrefl. assert (H := ZPminus_spec p0 p);destruct (ZPminus p0 p);Esimpl2. rewrite IHP'1; rewrite IHP'2;rsimpl. add_push (P3 @ (tail l));rewrite H;rrefl. rewrite IHP'1; rewrite IHP'2;rsimpl;simpl;Esimpl. rewrite H;rewrite Pplus_comm. - rewrite pow_Pplus;rsimpl. + rewrite pow_pos_Pplus;rsimpl. add_push (P3 @ (tail l));rrefl. assert (forall P k l, - (PsubX Psub P'1 k P) @ l == P@l + - P'1@l * pow (hd 0 l) k). + (PsubX Psub P'1 k P) @ l == P@l + - P'1@l * pow_pos rmul (hd 0 l) k). induction P;simpl;intros. rewrite Popp_ok;rsimpl;apply (ARadd_comm ARth);trivial. destruct p2;simpl;rewrite Popp_ok;rsimpl. @@ -697,15 +700,15 @@ Section MakeRingPol. assert (H1 := ZPminus_spec p2 k);destruct (ZPminus p2 k);Esimpl2;rsimpl. rewrite IHP'1;rsimpl;add_push (P5 @ (tail l0));rewrite H1;rrefl. rewrite IHP'1;rewrite H1;rewrite Pplus_comm. - rewrite pow_Pplus;simpl;Esimpl. + rewrite pow_pos_Pplus;simpl;Esimpl. add_push (P5 @ (tail l0));rrefl. rewrite IHP1;rewrite H1;rewrite Pplus_comm. - rewrite pow_Pplus;simpl;rsimpl. + rewrite pow_pos_Pplus;simpl;rsimpl. add_push (P5 @ (tail l0));rrefl. rewrite H0;rsimpl. rewrite IHP'2;rsimpl;add_push (P3 @ (tail l)). rewrite H;rewrite Pplus_comm. - rewrite pow_Pplus;rsimpl. + rewrite pow_pos_Pplus;rsimpl. Qed. Lemma PmulI_ok : @@ -725,11 +728,11 @@ Section MakeRingPol. rewrite jump_Pplus;rewrite IHP;rrefl. destruct p0;Esimpl2. rewrite IHP1;rewrite IHP2;simpl;rsimpl. - mul_push (pow (hd 0 l) p);rrefl. + mul_push (pow_pos rmul (hd 0 l) p);rrefl. rewrite IHP1;rewrite IHP2;simpl;rsimpl. - mul_push (pow (hd 0 l) p); rewrite jump_Pdouble_minus_one;rrefl. + mul_push (pow_pos rmul (hd 0 l) p); rewrite jump_Pdouble_minus_one;rrefl. rewrite IHP1;simpl;rsimpl. - mul_push (pow (hd 0 l) p). + mul_push (pow_pos rmul (hd 0 l) p). rewrite H;rrefl. Qed. @@ -759,6 +762,22 @@ Section MakeRingPol. Mphi l (mkZmon j M) == Mphi l (zmon j M). intros M j l; case M; simpl; intros; rsimpl. Qed. + + Lemma zmon_pred_ok : forall M j l, + Mphi (tail l) (zmon_pred j M) == Mphi l (zmon j M). + Proof. + destruct j; simpl;intros auto; rsimpl. + rewrite mkZmon_ok;rsimpl. + rewrite mkZmon_ok;simpl. rewrite jump_Pdouble_minus_one; rsimpl. + Qed. + + Lemma mkVmon_ok : forall M i l, Mphi l (mkVmon i M) == Mphi l M*pow_pos rmul (hd 0 l) i. + Proof. + destruct M;simpl;intros;rsimpl. + rewrite zmon_pred_ok;simpl;rsimpl. + rewrite Pplus_comm;rewrite pow_pos_Pplus;rsimpl. + Qed. + Lemma Mphi_ok: forall P M l, let (Q,R) := MFactor P M in @@ -798,8 +817,7 @@ Section MakeRingPol. rewrite (ARadd_comm ARth); rsimpl. apply radd_ext; rsimpl. rewrite (ARadd_comm ARth); rsimpl. - case j; simpl; auto; try intros j1; rsimpl. - rewrite jump_Pdouble_minus_one; rsimpl. + rewrite zmon_pred_ok;rsimpl. intros j M1. case_eq ((i ?= j) Eq); intros He; simpl. rewrite (Pcompare_Eq_eq _ _ He). @@ -827,7 +845,7 @@ Section MakeRingPol. apply rmul_ext; rsimpl. rewrite (ARmul_comm ARth); rsimpl. apply rmul_ext; rsimpl. - rewrite <- pow_Pplus. + rewrite <- pow_pos_Pplus. rewrite (Pplus_minus _ _ (ZC2 _ _ He)); rsimpl. generalize (Hrec1 (mkZmon 1 M1) l); case (MFactor P2 (mkZmon 1 M1)); @@ -847,11 +865,10 @@ Section MakeRingPol. repeat (rewrite <-(ARmul_assoc ARth)). rewrite (ARmul_comm ARth (Q3@l)); rsimpl. apply rmul_ext; rsimpl. - rewrite <- pow_Pplus. + rewrite <- pow_pos_Pplus. rewrite (Pplus_minus _ _ He); rsimpl. Qed. - Lemma POneSubst_ok: forall P1 M1 P2 P3 l, POneSubst P1 M1 P2 = Some P3 -> Mphi l M1 == P2@l -> P1@l == P3@l. intros P2 M1 P3 P4 l; unfold POneSubst. @@ -947,47 +964,28 @@ Section MakeRingPol. | PEadd : PExpr -> PExpr -> PExpr | PEsub : PExpr -> PExpr -> PExpr | PEmul : PExpr -> PExpr -> PExpr - | PEopp : PExpr -> PExpr. + | PEopp : PExpr -> PExpr + | PEpow : PExpr -> N -> PExpr. - (** normalisation towards polynomials *) - - Definition X := (PX P1 xH P0). - - Definition mkX j := - match j with - | xH => X - | xO j => Pinj (Pdouble_minus_one j) X - | xI j => Pinj (xO j) X - end. - - Fixpoint norm (pe:PExpr) : Pol := - match pe with - | PEc c => Pc c - | PEX j => mkX j - | PEadd pe1 (PEopp pe2) => Psub (norm pe1) (norm pe2) - | PEadd (PEopp pe1) pe2 => Psub (norm pe2) (norm pe1) - | PEadd pe1 pe2 => Padd (norm pe1) (norm pe2) - | PEsub pe1 pe2 => Psub (norm pe1) (norm pe2) - | PEmul pe1 pe2 => Pmul (norm pe1) (norm pe2) - | PEopp pe1 => Popp (norm pe1) - end. + (** evaluation of polynomial expressions towards R *) + Definition mk_X j := mkPinj_pred j mkX. (** evaluation of polynomial expressions towards R *) - + Fixpoint PEeval (l:list R) (pe:PExpr) {struct pe} : R := - match pe with - | PEc c => phi c - | PEX j => nth 0 j l - | PEadd pe1 pe2 => (PEeval l pe1) + (PEeval l pe2) - | PEsub pe1 pe2 => (PEeval l pe1) - (PEeval l pe2) - | PEmul pe1 pe2 => (PEeval l pe1) * (PEeval l pe2) - | PEopp pe1 => - (PEeval l pe1) - end. + match pe with + | PEc c => phi c + | PEX j => nth 0 j l + | PEadd pe1 pe2 => (PEeval l pe1) + (PEeval l pe2) + | PEsub pe1 pe2 => (PEeval l pe1) - (PEeval l pe2) + | PEmul pe1 pe2 => (PEeval l pe1) * (PEeval l pe2) + | PEopp pe1 => - (PEeval l pe1) + | PEpow pe1 n => rpow (PEeval l pe1) (Cp_phi n) + end. (** Correctness proofs *) - - Lemma mkX_ok : forall p l, nth 0 p l == (mkX p) @ l. + Lemma mkX_ok : forall p l, nth 0 p l == (mk_X p) @ l. Proof. destruct p;simpl;intros;Esimpl;trivial. rewrite <-jump_tl;rewrite nth_jump;rrefl. @@ -995,238 +993,466 @@ Section MakeRingPol. rewrite nth_Pdouble_minus_one;rrefl. Qed. - Lemma norm_PEopp : forall l pe, (norm (PEopp pe))@l == -(norm pe)@l. - Proof. - intros;simpl;apply Popp_ok. - Qed. - Ltac Esimpl3 := repeat match goal with | |- context [(?P1 ++ ?P2)@?l] => rewrite (Padd_ok P2 P1 l) | |- context [(?P1 -- ?P2)@?l] => rewrite (Psub_ok P2 P1 l) - | |- context [(norm (PEopp ?pe))@?l] => rewrite (norm_PEopp l pe) - end;Esimpl2;try rrefl;try apply (ARadd_comm ARth). + end;Esimpl2;try rrefl;try apply (ARadd_comm ARth). + + (** Normalization and rewriting *) + + Section NORM_SUBST_REC. + Variable n : nat. + Variable lmp:list (Mon*Pol). + Let subst_l P := PNSubstL P lmp n n. + Let Pmul_subst P1 P2 := subst_l (Pmul P1 P2). + + Fixpoint norm_subst (pe:PExpr) : Pol := + match pe with + | PEc c => Pc c + | PEX j => subst_l (mk_X j) + | PEadd (PEopp pe1) pe2 => Psub (norm_subst pe2) (norm_subst pe1) + | PEadd pe1 (PEopp pe2) => + Psub (norm_subst pe1) (norm_subst pe2) + | PEadd pe1 pe2 => Padd (norm_subst pe1) (norm_subst pe2) + | PEsub pe1 pe2 => Psub (norm_subst pe1) (norm_subst pe2) + | PEmul pe1 pe2 => Pmul_subst (norm_subst pe1) (norm_subst pe2) + | PEopp pe1 => Popp (norm_subst pe1) + | PEpow pe1 n => pow_N P1 Pmul_subst (norm_subst pe1) n + end. - Lemma norm_ok : forall l pe, PEeval l pe == (norm pe)@l. + Lemma norm_subst_spec : + forall l pe, MPcond lmp l -> + PEeval l pe == (norm_subst pe)@l. + Proof. + intros;assert (subst_l_ok:forall P, (subst_l P)@l == P@l). + unfold subst_l;intros. + rewrite <- PNSubstL_ok;trivial. rrefl. + assert (Pms_ok:forall P1 P2, (Pmul_subst P1 P2)@l == P1@l*P2@l). + intros;unfold Pmul_subst;rewrite subst_l_ok;rewrite Pmul_ok;rrefl. + induction pe;simpl;Esimpl3. + rewrite subst_l_ok;apply mkX_ok. + rewrite IHpe1;rewrite IHpe2;destruct pe1;destruct pe2;Esimpl3. + rewrite IHpe1;rewrite IHpe2;rrefl. + rewrite Pms_ok;rewrite IHpe1;rewrite IHpe2;rrefl. + rewrite IHpe;rrefl. + rewrite pow_th.(rpow_pow_N). destruct n0;Esimpl3. + induction p;simpl;try rewrite IHp;try rewrite IHpe;repeat rewrite Pms_ok;rrefl. + Qed. + + End NORM_SUBST_REC. + + Fixpoint interp_PElist (l:list R) (lpe:list (PExpr*PExpr)) {struct lpe} : Prop := + match lpe with + | nil => True + | (me,pe)::lpe => + match lpe with + | nil => PEeval l me == PEeval l pe + | _ => PEeval l me == PEeval l pe /\ interp_PElist l lpe + end + end. + + Fixpoint mon_of_pol (P:Pol) : option Mon := + match P with + | Pc c => if (c ?=! cI) then Some mon0 else None + | Pinj j P => + match mon_of_pol P with + | None => None + | Some m => Some (mkZmon j m) + end + | PX P i Q => + if Peq Q P0 then + match mon_of_pol P with + | None => None + | Some m => Some (mkVmon i m) + end + else None + end. + + Fixpoint mk_monpol_list (lpe:list (PExpr * PExpr)) : list (Mon*Pol) := + match lpe with + | nil => nil + | (me,pe)::lpe => + match mon_of_pol (norm_subst 0 nil me) with + | None => mk_monpol_list lpe + | Some m => (m,norm_subst 0 nil pe):: mk_monpol_list lpe + end + end. + + Lemma mon_of_pol_ok : forall P m, mon_of_pol P = Some m -> + forall l, Mphi l m == P@l. + Proof. + induction P;simpl;intros;Esimpl. + assert (H1 := (morph_eq CRmorph) c cI). + destruct (c ?=! cI). + inversion H;rewrite H1;trivial;Esimpl. + discriminate. + generalize H;clear H;case_eq (mon_of_pol P);intros;try discriminate. + inversion H0. + rewrite mkZmon_ok;simpl;auto. + generalize H;clear H;change match P3 with + | Pc c => c ?=! cO + | Pinj _ _ => false + | PX _ _ _ => false + end with (P3 ?== P0). + assert (H := Peq_ok P3 P0). + destruct (P3 ?== P0). + case_eq (mon_of_pol P2);intros. + inversion H1. + rewrite mkVmon_ok;simpl. + rewrite H;trivial;Esimpl. rewrite IHP1;trivial;Esimpl. discriminate. + intros;discriminate. + Qed. + + Lemma interp_PElist_ok : forall l lpe, + interp_PElist l lpe -> MPcond (mk_monpol_list lpe) l. Proof. - induction pe;simpl;Esimpl3. - apply mkX_ok. - rewrite IHpe1;rewrite IHpe2; destruct pe1;destruct pe2;Esimpl3. - rewrite IHpe1;rewrite IHpe2;rrefl. - rewrite Pmul_ok;rewrite IHpe1;rewrite IHpe2;rrefl. - rewrite IHpe;rrefl. + induction lpe;simpl. trivial. + destruct a;simpl;intros. + assert (HH:=mon_of_pol_ok (norm_subst 0 nil p)); + destruct (mon_of_pol (norm_subst 0 nil p)). + split. + rewrite <- norm_subst_spec. exact I. + destruct lpe;try destruct H;rewrite <- H; + rewrite (norm_subst_spec 0 nil); try exact I;apply HH;trivial. + apply IHlpe. destruct lpe;simpl;trivial. destruct H. exact H0. + apply IHlpe. destruct lpe;simpl;trivial. destruct H. exact H0. Qed. - Lemma ring_correct : forall l pe1 pe2, - ((norm pe1) ?== (norm pe2)) = true -> (PEeval l pe1) == (PEeval l pe2). + Lemma norm_subst_ok : forall n l lpe pe, + interp_PElist l lpe -> + PEeval l pe == (norm_subst n (mk_monpol_list lpe) pe)@l. Proof. - intros l pe1 pe2 H. - repeat rewrite norm_ok. - apply (Peq_ok (norm pe1) (norm pe2) H l). - Qed. + intros;apply norm_subst_spec. apply interp_PElist_ok;trivial. + Qed. + + Lemma ring_correct : forall n l lpe pe1 pe2, + interp_PElist l lpe -> + (let lmp := mk_monpol_list lpe in + norm_subst n lmp pe1 ?== norm_subst n lmp pe2) = true -> + PEeval l pe1 == PEeval l pe2. + Proof. + simpl;intros. + do 2 (rewrite (norm_subst_ok n l lpe);trivial). + apply Peq_ok;trivial. + Qed. -(** Evaluation function avoiding parentheses *) - Fixpoint mkmult (r:R) (lm:list R) {struct lm}: R := - match lm with - | nil => r - | cons h t => mkmult (r*h) t - end. - - Definition mkadd_mult rP lm := - match lm with - | nil => rP + 1 - | cons h t => rP + mkmult h t - end. - Fixpoint powl (i:positive) (x:R) (l:list R) {struct i}: list R := - match i with - | xH => cons x l - | xO i => powl i x (powl i x l) - | xI i => powl i x (powl i x (cons x l)) - end. - - Fixpoint add_mult_dev (rP:R) (P:Pol) (fv lm:list R) {struct P} : R := - (* rP + P@l * lm *) + + (** Generic evaluation of polynomial towards R avoiding parenthesis *) + Variable get_sign : C -> option C. + Variable get_sign_spec : sign_theory ropp req phi get_sign. + + + Section EVALUATION. + + (* [mkpow x p] = x^p *) + Variable mkpow : R -> positive -> R. + (* [mkpow x p] = -(x^p) *) + Variable mkopp_pow : R -> positive -> R. + (* [mkmult_pow r x p] = r * x^p *) + Variable mkmult_pow : R -> R -> positive -> R. + + Fixpoint mkmult_rec (r:R) (lm:list (R*positive)) {struct lm}: R := + match lm with + | nil => r + | cons (x,p) t => mkmult_rec (mkmult_pow r x p) t + end. + + Definition mkmult1 lm := + match lm with + | nil => 1 + | cons (x,p) t => mkmult_rec (mkpow x p) t + end. + + Definition mkmultm1 lm := + match lm with + | nil => ropp rI + | cons (x,p) t => mkmult_rec (mkopp_pow x p) t + end. + + Definition mkmult_c_pos c lm := + if c ?=! cI then mkmult1 (rev' lm) + else mkmult_rec [c] (rev' lm). + + Definition mkmult_c c lm := + if c ?=! copp cI then mkmultm1 (rev' lm) + else mkmult_c_pos c lm. + + Definition mkadd_mult rP c lm := + match get_sign c with + | None => rP + mkmult_c_pos c lm + | Some c' => rP - mkmult_c_pos c' lm + end. + + Definition add_pow_list (r:R) n l := + match n with + | N0 => l + | Npos p => (r,p)::l + end. + + Fixpoint add_mult_dev + (rP:R) (P:Pol) (fv:list R) (n:N) (lm:list (R*positive)) {struct P} : R := + match P with + | Pc c => + let lm := add_pow_list (hd 0 fv) n lm in + mkadd_mult rP c lm + | Pinj j Q => + add_mult_dev rP Q (jump j fv) N0 (add_pow_list (hd 0 fv) n lm) + | PX P i Q => + let rP := add_mult_dev rP P fv (Nplus (Npos i) n) lm in + if Q ?== P0 then rP + else add_mult_dev rP Q (tail fv) N0 (add_pow_list (hd 0 fv) n lm) + end. + + Fixpoint mult_dev (P:Pol) (fv : list R) (n:N) + (lm:list (R*positive)) {struct P} : R := + (* P@l * (hd 0 l)^n * lm *) match P with - | Pc c => if c ?=! cI then mkadd_mult rP (rev' lm) - else mkadd_mult rP (cons [c] (rev' lm)) - | Pinj j Q => add_mult_dev rP Q (jump j fv) lm + | Pc c => mkmult_c c (add_pow_list (hd 0 fv) n lm) + | Pinj j Q => mult_dev Q (jump j fv) N0 (add_pow_list (hd 0 fv) n lm) | PX P i Q => - let rP := add_mult_dev rP P fv (powl i (hd 0 fv) lm) in - if Q ?== P0 then rP else add_mult_dev rP Q (tail fv) lm - end. + let rP := mult_dev P fv (Nplus (Npos i) n) lm in + if Q ?== P0 then rP + else + let lmq := add_pow_list (hd 0 fv) n lm in + add_mult_dev rP Q (tail fv) N0 lmq + end. + + Definition Pphi_avoid fv P := mult_dev P fv N0 nil. - Definition mkmult1 lm := - match lm with + Fixpoint r_list_pow (l:list (R*positive)) : R := + match l with | nil => rI - | cons h t => mkmult h t + | cons (r,p) l => pow_pos rmul r p * r_list_pow l end. - - Fixpoint mult_dev (P:Pol) (fv lm : list R) {struct P} : R := - (* P@l * lm *) - match P with - | Pc c => if c ?=! cI then mkmult1 (rev' lm) else mkmult [c] (rev' lm) - | Pinj j Q => mult_dev Q (jump j fv) lm - | PX P i Q => - let rP := mult_dev P fv (powl i (hd 0 fv) lm) in - if Q ?== P0 then rP else add_mult_dev rP Q (tail fv) lm - end. - Definition Pphi_dev fv P := mult_dev P fv nil. + Hypothesis mkpow_spec : forall r p, mkpow r p == pow_pos rmul r p. + Hypothesis mkopp_pow_spec : forall r p, mkopp_pow r p == - (pow_pos rmul r p). + Hypothesis mkmult_pow_spec : forall r x p, mkmult_pow r x p == r * pow_pos rmul x p. - Add Morphism mkmult : mkmult_ext. - intros r r0 eqr l;generalize l r r0 eqr;clear l r r0 eqr; - induction l;simpl;intros. - trivial. apply IHl; rewrite eqr;rrefl. - Qed. + Lemma mkmult_rec_ok : forall lm r, mkmult_rec r lm == r * r_list_pow lm. + Proof. + induction lm;intros;simpl;Esimpl. + destruct a as (x,p);Esimpl. + rewrite IHlm. rewrite mkmult_pow_spec. Esimpl. + Qed. - Lemma mul_mkmult : forall lm r1 r2, r1 * mkmult r2 lm == mkmult (r1*r2) lm. + Lemma mkmult1_ok : forall lm, mkmult1 lm == r_list_pow lm. Proof. - induction lm;simpl;intros;try rrefl. - rewrite IHlm. - setoid_replace (r1 * (r2 * a)) with (r1 * r2 * a);Esimpl. + destruct lm;simpl;Esimpl. + destruct p. rewrite mkmult_rec_ok;rewrite mkpow_spec;Esimpl. Qed. - Lemma mkmult1_mkmult : forall lm r, r * mkmult1 lm == mkmult r lm. + Lemma mkmultm1_ok : forall lm, mkmultm1 lm == - r_list_pow lm. Proof. - destruct lm;simpl;intros. Esimpl. - apply mul_mkmult. + destruct lm;simpl;Esimpl. + destruct p;rewrite mkmult_rec_ok. rewrite mkopp_pow_spec;Esimpl. Qed. - - Lemma mkmult1_mkmult_1 : forall lm, mkmult1 lm == mkmult 1 lm. + + Lemma r_list_pow_rev : forall l, r_list_pow (rev' l) == r_list_pow l. Proof. - intros;rewrite <- mkmult1_mkmult;Esimpl. + assert + (forall l lr : list (R * positive), r_list_pow (rev_append l lr) == r_list_pow lr * r_list_pow l). + induction l;intros;simpl;Esimpl. + destruct a;rewrite IHl;Esimpl. + rewrite (ARmul_comm ARth (pow_pos rmul r p)). rrefl. + intros;unfold rev'. rewrite H;simpl;Esimpl. + Qed. + + Lemma mkmult_c_pos_ok : forall c lm, mkmult_c_pos c lm == [c]* r_list_pow lm. + Proof. + intros;unfold mkmult_c_pos;simpl. + assert (H := (morph_eq CRmorph) c cI). + rewrite <- r_list_pow_rev; destruct (c ?=! cI). + rewrite H;trivial;Esimpl. + apply mkmult1_ok. apply mkmult_rec_ok. Qed. - Lemma mkmult_rev_append : forall lm l r, - mkmult r (rev_append lm l) == mkmult (mkmult r l) lm. + Lemma mkmult_c_ok : forall c lm, mkmult_c c lm == [c] * r_list_pow lm. Proof. - induction lm; simpl in |- *; intros. - rrefl. - rewrite IHlm; simpl in |- *. - repeat rewrite <- (ARmul_comm ARth a); rewrite <- mul_mkmult. - rrefl. + intros;unfold mkmult_c;simpl. + assert (H := (morph_eq CRmorph) c (copp cI)). + destruct (c ?=! copp cI). + rewrite <- r_list_pow_rev;rewrite H;trivial;Esimpl. + apply mkmultm1_ok. apply mkmult_c_pos_ok. Qed. - Lemma powl_mkmult_rev : forall p r x lm, - mkmult r (rev' (powl p x lm)) == mkmult (pow x p * r) (rev' lm). + Lemma mkadd_mult_ok : forall rP c lm, mkadd_mult rP c lm == rP + [c]*r_list_pow lm. Proof. - induction p;simpl;intros. - repeat rewrite IHp. - unfold rev';simpl. - repeat rewrite mkmult_rev_append. - simpl. - setoid_replace (pow x p * (pow x p * r) * x) - with (x * pow x p * pow x p * r);Esimpl. - mul_push x;rrefl. - repeat rewrite IHp. - setoid_replace (pow x p * (pow x p * r) ) - with (pow x p * pow x p * r);Esimpl. - unfold rev';simpl. repeat rewrite mkmult_rev_append;simpl. - rewrite (ARmul_comm ARth);rrefl. + intros;unfold mkadd_mult. + case_eq (get_sign c);intros. + rewrite (get_sign_spec.(sign_spec) _ H). + rewrite mkmult_c_pos_ok;Esimpl. + rewrite mkmult_c_pos_ok;Esimpl. Qed. - Lemma Pphi_add_mult_dev : forall P rP fv lm, - rP + P@fv * mkmult1 (rev' lm) == add_mult_dev rP P fv lm. + Lemma add_pow_list_ok : + forall r n l, r_list_pow (add_pow_list r n l) == pow_N rI rmul r n * r_list_pow l. Proof. - induction P;simpl;intros. - assert (H := (morph_eq CRmorph) c cI). - destruct (c ?=! cI). - rewrite (H (refl_equal true));rewrite (morph1 CRmorph);Esimpl. - destruct (rev' lm);Esimpl;rrefl. - rewrite mkmult1_mkmult;rrefl. - apply IHP. - replace (match P3 with + destruct n;simpl;intros;Esimpl. + Qed. + + Lemma add_mult_dev_ok : forall P rP fv n lm, + add_mult_dev rP P fv n lm == rP + P@fv*pow_N rI rmul (hd 0 fv) n * r_list_pow lm. + Proof. + induction P;simpl;intros. + rewrite mkadd_mult_ok. rewrite add_pow_list_ok; Esimpl. + rewrite IHP. simpl. rewrite add_pow_list_ok; Esimpl. + change (match P3 with | Pc c => c ?=! cO | Pinj _ _ => false | PX _ _ _ => false - end) with (Peq P3 P0);trivial. + end) with (Peq P3 P0). + change match n with + | N0 => Npos p + | Npos q => Npos (p + q) + end with (Nplus (Npos p) n);trivial. assert (H := Peq_ok P3 P0). destruct (P3 ?== P0). - rewrite (H (refl_equal true));simpl;Esimpl. - rewrite <- IHP1. - repeat rewrite mkmult1_mkmult_1. - rewrite powl_mkmult_rev. - rewrite <- mul_mkmult;Esimpl. - rewrite <- IHP2. - rewrite <- IHP1. - repeat rewrite mkmult1_mkmult_1. - rewrite powl_mkmult_rev. - rewrite <- mul_mkmult;Esimpl. + rewrite (H (refl_equal true)). + rewrite IHP1. destruct n;simpl;Esimpl;rewrite pow_pos_Pplus;Esimpl. + rewrite IHP2. + rewrite IHP1. destruct n;simpl;Esimpl;rewrite pow_pos_Pplus;Esimpl. Qed. - - Lemma Pphi_mult_dev : forall P fv lm, - P@fv * mkmult1 (rev' lm) == mult_dev P fv lm. + + Lemma mult_dev_ok : forall P fv n lm, + mult_dev P fv n lm == P@fv * pow_N rI rmul (hd 0 fv) n * r_list_pow lm. Proof. - induction P;simpl;intros. - assert (H := (morph_eq CRmorph) c cI). - destruct (c ?=! cI). - rewrite (H (refl_equal true));rewrite (morph1 CRmorph);Esimpl. - apply mkmult1_mkmult. - apply IHP. - replace (match P3 with + induction P;simpl;intros;Esimpl. + rewrite mkmult_c_ok;rewrite add_pow_list_ok;Esimpl. + rewrite IHP. simpl;rewrite add_pow_list_ok;Esimpl. + change (match P3 with | Pc c => c ?=! cO | Pinj _ _ => false | PX _ _ _ => false - end) with (Peq P3 P0);trivial. + end) with (Peq P3 P0). + change match n with + | N0 => Npos p + | Npos q => Npos (p + q) + end with (Nplus (Npos p) n);trivial. assert (H := Peq_ok P3 P0). - destruct (P3 ?== P0). - rewrite (H (refl_equal true));simpl;Esimpl. - rewrite <- IHP1. - repeat rewrite mkmult1_mkmult_1. - rewrite powl_mkmult_rev. - rewrite <- mul_mkmult;Esimpl. - rewrite <- Pphi_add_mult_dev. - rewrite <- IHP1. - repeat rewrite mkmult1_mkmult_1. - rewrite powl_mkmult_rev. - rewrite <- mul_mkmult;Esimpl. - Qed. + destruct (P3 ?== P0). + rewrite (H (refl_equal true)). + rewrite IHP1. destruct n;simpl;Esimpl;rewrite pow_pos_Pplus;Esimpl. + rewrite add_mult_dev_ok. rewrite IHP1; rewrite add_pow_list_ok. + destruct n;simpl;Esimpl;rewrite pow_pos_Pplus;Esimpl. + Qed. - Lemma Pphi_Pphi_dev : forall P l, P@l == Pphi_dev l P. - Proof. - unfold Pphi_dev;intros. - rewrite <- Pphi_mult_dev;simpl;Esimpl. + Lemma Pphi_avoid_ok : forall P fv, Pphi_avoid fv P == P@fv. + Proof. + unfold Pphi_avoid;intros;rewrite mult_dev_ok;simpl;Esimpl. Qed. - Lemma Pphi_dev_gen_ok : forall l pe, PEeval l pe == Pphi_dev l (norm pe). + End EVALUATION. + + Definition Pphi_pow := + let mkpow x p := + match p with xH => x | _ => rpow x (Cp_phi (Npos p)) end in + let mkopp_pow x p := ropp (mkpow x p) in + let mkmult_pow r x p := rmul r (mkpow x p) in + Pphi_avoid mkpow mkopp_pow mkmult_pow. + + Lemma local_mkpow_ok : + forall (r : R) (p : positive), + match p with + | xI _ => rpow r (Cp_phi (Npos p)) + | xO _ => rpow r (Cp_phi (Npos p)) + | 1 => r + end == pow_pos rmul r p. + Proof. intros r p;destruct p;try rewrite pow_th.(rpow_pow_N);reflexivity. Qed. + + Lemma Pphi_pow_ok : forall P fv, Pphi_pow fv P == P@fv. Proof. - intros l pe;rewrite <- Pphi_Pphi_dev;apply norm_ok. + unfold Pphi_pow;intros;apply Pphi_avoid_ok;intros;try rewrite local_mkpow_ok;rrefl. Qed. - Lemma Pphi_dev_ok : - forall l pe npe, norm pe = npe -> PEeval l pe == Pphi_dev l npe. + Lemma ring_rw_pow_correct : forall n lH l, + interp_PElist l lH -> + forall lmp, mk_monpol_list lH = lmp -> + forall pe npe, norm_subst n lmp pe = npe -> + PEeval l pe == Pphi_pow l npe. Proof. - intros l pe npe npe_eq; subst npe; apply Pphi_dev_gen_ok. - Qed. + intros n lH l H1 lmp Heq1 pe npe Heq2. + rewrite Pphi_pow_ok. rewrite <- Heq2;rewrite <- Heq1. + apply norm_subst_ok. trivial. + Qed. - Fixpoint MPcond_dev (LM1: list (Mon * Pol)) (l: list R) {struct LM1} : Prop := - match LM1 with - cons (M1,P2) LM2 => (Mphi l M1 == Pphi_dev l P2) /\ (MPcond_dev LM2 l) - | _ => True + Fixpoint mkmult_pow (r x:R) (p: positive) {struct p} : R := + match p with + | xH => r*x + | xO p => mkmult_pow (mkmult_pow r x p) x p + | xI p => mkmult_pow (mkmult_pow (r*x) x p) x p + end. + + Definition mkpow x p := + match p with + | xH => x + | xO p => mkmult_pow x x (Pdouble_minus_one p) + | xI p => mkmult_pow x x (xO p) end. - - Fixpoint MPcond_map (LM1: list (Mon * PExpr)): list (Mon * Pol) := - match LM1 with - cons (M1,P2) LM2 => cons (M1, norm P2) (MPcond_map LM2) - | _ => nil + + Definition mkopp_pow x p := + match p with + | xH => -x + | xO p => mkmult_pow (-x) x (Pdouble_minus_one p) + | xI p => mkmult_pow (-x) x (xO p) end. - Lemma MP_cond_dev_imp_MP_cond: forall LM1 l, - MPcond_dev LM1 l -> MPcond LM1 l. + Definition Pphi_dev := Pphi_avoid mkpow mkopp_pow mkmult_pow. + + Lemma mkmult_pow_ok : forall p r x, mkmult_pow r x p == r*pow_pos rmul x p. + Proof. + induction p;intros;simpl;Esimpl. + repeat rewrite IHp;Esimpl. + repeat rewrite IHp;Esimpl. + Qed. + + Lemma mkpow_ok : forall p x, mkpow x p == pow_pos rmul x p. + Proof. + destruct p;simpl;intros;Esimpl. + repeat rewrite mkmult_pow_ok;Esimpl. + rewrite mkmult_pow_ok;Esimpl. + pattern x at 1;replace x with (pow_pos rmul x 1). + rewrite <- pow_pos_Pplus. + rewrite <- Pplus_one_succ_l. + rewrite Psucc_o_double_minus_one_eq_xO. + simpl;Esimpl. + trivial. + Qed. + + Lemma mkopp_pow_ok : forall p x, mkopp_pow x p == - pow_pos rmul x p. + Proof. + destruct p;simpl;intros;Esimpl. + repeat rewrite mkmult_pow_ok;Esimpl. + rewrite mkmult_pow_ok;Esimpl. + pattern x at 1;replace x with (pow_pos rmul x 1). + rewrite <- pow_pos_Pplus. + rewrite <- Pplus_one_succ_l. + rewrite Psucc_o_double_minus_one_eq_xO. + simpl;Esimpl. + trivial. + Qed. + + Lemma Pphi_dev_ok : forall P fv, Pphi_dev fv P == P@fv. + Proof. + unfold Pphi_dev;intros;apply Pphi_avoid_ok. + intros;apply mkpow_ok. + intros;apply mkopp_pow_ok. + intros;apply mkmult_pow_ok. + Qed. + + Lemma ring_rw_correct : forall n lH l, + interp_PElist l lH -> + forall lmp, mk_monpol_list lH = lmp -> + forall pe npe, norm_subst n lmp pe = npe -> + PEeval l pe == Pphi_dev l npe. Proof. - intros LM1; elim LM1; simpl; auto. - intros (M2,P2) LM2 Hrec l [H1 H2]; split; auto. - rewrite H1; rewrite Pphi_Pphi_dev; rsimpl. + intros n lH l H1 lmp Heq1 pe npe Heq2. + rewrite Pphi_dev_ok. rewrite <- Heq2;rewrite <- Heq1. + apply norm_subst_ok. trivial. Qed. - Lemma PNSubstL_dev_ok: forall m n lm pe l, - let LM := MPcond_map lm in - MPcond_dev LM l -> PEeval l pe == Pphi_dev l (PNSubstL (norm pe) LM m n). - intros m n lm p3 l LM H. - rewrite <- Pphi_Pphi_dev; rewrite <- PNSubstL_ok; auto. - apply MP_cond_dev_imp_MP_cond; auto. - rewrite Pphi_Pphi_dev; apply Pphi_dev_ok; auto. - Qed. -End MakeRingPol. +End MakeRingPol. + diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v index 86684d939..d9d82aa0a 100644 --- a/contrib/setoid_ring/Ring_tac.v +++ b/contrib/setoid_ring/Ring_tac.v @@ -3,16 +3,18 @@ Require Import Setoid. Require Import BinPos. Require Import Ring_polynom. Require Import BinList. +Require Import InitialRing. Declare ML Module "newring". - + (* adds a definition id' on the normal form of t and an hypothesis id stating that t = id' (tries to produces a proof as small as possible) *) Ltac compute_assertion id id' t := let t' := eval vm_compute in t in - (pose (id' := t'); - assert (id : t = id'); - [exact_no_check (refl_equal id')|idtac]). + pose (id' := t'); + assert (id : t = id'); + [vm_cast_no_check (refl_equal id')|idtac]. +(* [exact_no_check (refl_equal id'<: t = id')|idtac]). *) (********************************************************************) (* Tacticals to build reflexive tactics *) @@ -45,29 +47,40 @@ Ltac ApplyLemmaThen lemma expr tac := clear H; OnMainSubgoal Heq ltac:(type of Heq) ltac:(tac Heq; clear Heq nexpr). +Ltac ApplyLemmaThenAndCont lemma expr tac CONT_tac cont_arg := + let npe := fresh "expr_nf" in + let H := fresh "eq_nf" in + let Heq := fresh "thm" in + let npe_spec := + match type of (lemma expr) with + forall npe, ?npe_spec = npe -> _ => npe_spec + | _ => fail 1 "ApplyLemmaThenAndCont: cannot find norm expression" + end in + (compute_assertion H npe npe_spec; + (assert (Heq:=lemma _ _ H) || fail "anomaly: failed to apply lemma"); + clear H; + OnMainSubgoal Heq ltac:(type of Heq) + ltac:(try tac Heq; clear Heq npe; CONT_tac cont_arg)). + (* General scheme of reflexive tactics using of correctness lemma that involves normalisation of one expression *) -Ltac ReflexiveNormTactic FV_tac SYN_tac MAIN_tac lemma2 req terms := - let R := match type of req with ?R -> _ => R end in - (* build the atom list *) - let val := list_fold_left FV_tac (@List.nil R) terms in - let lem := fresh "ring_lemma" in - pose (lem := lemma2 val) || fail "anomaly: ill-typed atom list"; - (* rewrite steps *) - list_iter - ltac:(fun term => - let expr := SYN_tac term val in - try ApplyLemmaThen lem expr MAIN_tac) - terms; - clear lem. + +Ltac ReflexiveRewriteTactic FV_tac SYN_tac MAIN_tac LEMMA_tac fv terms := + (* extend the atom list *) + let fv := list_fold_left FV_tac fv terms in + let RW_tac lemma := + let fcons term CONT_tac cont_arg := + let expr := SYN_tac term fv in + (ApplyLemmaThenAndCont lemma expr MAIN_tac CONT_tac cont_arg) in + (* rewrite steps *) + lazy_list_fold_right fcons ltac:(idtac) terms in + LEMMA_tac fv RW_tac. (********************************************************) -(* An object to return when an expression is not recognized as a constant *) -Definition NotConstant := false. - + (* Building the atom list of a ring expression *) -Ltac FV Cst add mul sub opp t fv := +Ltac FV Cst CstPow add mul sub opp pow t fv := let rec TFV t fv := match Cst t with | NotConstant => @@ -76,6 +89,11 @@ Ltac FV Cst add mul sub opp t fv := | (mul ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv) | (sub ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv) | (opp ?t1) => TFV t1 fv + | (pow ?t1 ?n) => + match CstPow n with + | InitialRing.NotConstant => AddFvTail t fv + | _ => TFV t1 fv + end | _ => AddFvTail t fv end | _ => fv @@ -83,10 +101,10 @@ Ltac FV Cst add mul sub opp t fv := in TFV t fv. (* syntaxification of ring expressions *) - Ltac mkPolexpr C Cst radd rmul rsub ropp t fv := +Ltac mkPolexpr C Cst CstPow radd rmul rsub ropp rpow t fv := let rec mkP t := match Cst t with - | NotConstant => + | InitialRing.NotConstant => match t with | (radd ?t1 ?t2) => let e1 := mkP t1 in @@ -99,6 +117,12 @@ Ltac FV Cst add mul sub opp t fv := let e2 := mkP t2 in constr:(PEsub e1 e2) | (ropp ?t1) => let e1 := mkP t1 in constr:(PEopp e1) + | (rpow ?t1 ?n) => + match CstPow n with + | InitialRing.NotConstant => + let p := Find_at t fv in constr:(PEX C p) + | ?c => let e1 := mkP t1 in constr:(PEpow e1 c) + end | _ => let p := Find_at t fv in constr:(PEX C p) end @@ -108,58 +132,140 @@ Ltac FV Cst add mul sub opp t fv := Ltac ParseRingComponents lemma := match type of lemma with - | context [@PEeval ?R ?rO ?add ?mul ?sub ?opp ?C ?phi _ _] => - (fun f => f R add mul sub opp C) + | context [@PEeval ?R ?rO ?add ?mul ?sub ?opp ?C ?phi ?Cpow ?powphi ?pow _ _] => + (fun f => f R add mul sub opp pow C) | _ => fail 1 "ring anomaly: bad correctness lemma (parse)" end. (* ring tactics *) -Ltac Ring Cst_tac lemma1 req := - let Main lhs rhs R radd rmul rsub ropp C := - let mkFV := FV Cst_tac radd rmul rsub ropp in - let mkPol := mkPolexpr C Cst_tac radd rmul rsub ropp in - let fv := mkFV lhs (@List.nil R) in +Ltac FV_hypo_tac mkFV req lH := + let R := match type of req with ?R -> _ => R end in + let FV_hypo_l_tac h := + match h with @mkhypo (req ?pe _) _ => mkFV pe end in + let FV_hypo_r_tac h := + match h with @mkhypo (req _ ?pe) _ => mkFV pe end in + let fv := list_fold_right FV_hypo_l_tac (@nil R) lH in + list_fold_right FV_hypo_r_tac fv lH. + +Ltac mkHyp_tac C req mkPE lH := + let mkHyp h res := + match h with + | @mkhypo (req ?r1 ?r2) _ => + let pe1 := mkPE r1 in + let pe2 := mkPE r2 in + constr:(cons (pe1,pe2) res) + | _ => fail "hypothesis is not a ring equality" + end in + list_fold_right mkHyp (@nil (PExpr C * PExpr C)) lH. + +Ltac proofHyp_tac lH := + let get_proof h := + match h with + | @mkhypo _ ?p => p + end in + let rec bh l := + match l with + | nil => constr:(I) + | cons ?h nil => get_proof h + | cons ?h ?tl => + let l := get_proof h in + let r := bh tl in + constr:(conj l r) + end in + bh lH. + +Definition ring_subst_niter := (10*10*10)%nat. + +Ltac Ring Cst_tac CstPow_tac lemma1 req n lH := + let Main lhs rhs R radd rmul rsub ropp rpow C := + let mkFV := FV Cst_tac CstPow_tac radd rmul rsub ropp rpow in + let mkPol := mkPolexpr C Cst_tac CstPow_tac radd rmul rsub ropp rpow in + let fv := FV_hypo_tac mkFV req lH in + let fv := mkFV lhs fv in let fv := mkFV rhs fv in check_fv fv; let pe1 := mkPol lhs fv in let pe2 := mkPol rhs fv in - apply (lemma1 fv pe1 pe2) || fail "typing error while applying ring"; - vm_compute; - exact (refl_equal true) || fail "not a valid ring equation" in + let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in + let vlpe := fresh "hyp_list" in + let vfv := fresh "fv_list" in + pose (vlpe := lpe); + pose (vfv := fv); + (apply (lemma1 n vfv vlpe pe1 pe2) + || fail "typing error while applying ring"); + [ ((let prh := proofHyp_tac lH in exact prh) + || idtac "can not automatically proof hypothesis : maybe a left member of a hypothesis is not a monomial") + | vm_compute; + (exact (refl_equal true) || fail "not a valid ring equation")] in ParseRingComponents lemma1 ltac:(OnEquation req Main). -Ltac Ring_norm_gen f Cst_tac lemma2 req rl := - let Main R add mul sub opp C := - let mkFV := FV Cst_tac add mul sub opp in - let mkPol := mkPolexpr C Cst_tac add mul sub opp in +Ltac Ring_norm_gen f Cst_tac CstPow_tac lemma2 req n lH rl := + let Main R add mul sub opp pow C := + let mkFV := FV Cst_tac CstPow_tac add mul sub opp pow in + let mkPol := mkPolexpr C Cst_tac CstPow_tac add mul sub opp pow in + let fv := FV_hypo_tac mkFV req lH in let simpl_ring H := (protect_fv "ring" in H; f H) in - ReflexiveNormTactic mkFV mkPol simpl_ring lemma2 req rl in + let lemma_tac fv RW_tac := + let rr_lemma := fresh "r_rw_lemma" in + let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in + let vlpe := fresh "list_hyp" in + let vlmp := fresh "list_hyp_norm" in + let vlmp_eq := fresh "list_hyp_norm_eq" in + let prh := proofHyp_tac lH in + pose (vlpe := lpe); + match type of lemma2 with + | context [mk_monpol_list ?cO ?cI ?cadd ?cmul ?csub ?copp ?ceqb _] => + compute_assertion vlmp_eq vlmp + (mk_monpol_list cO cI cadd cmul csub copp ceqb vlpe); + (assert (rr_lemma := lemma2 n vlpe fv prh vlmp vlmp_eq) + || fail "type error when build the rewriting lemma"); + RW_tac rr_lemma; + try clear rr_lemma vlmp_eq vlmp vlpe + | _ => fail 1 "ring_simplify anomaly: bad correctness lemma" + end in + ReflexiveRewriteTactic mkFV mkPol simpl_ring lemma_tac fv rl in ParseRingComponents lemma2 Main. -Ltac Ring_simplify := Ring_norm_gen ltac:(fun H => rewrite H). -Ltac Ring_simplify_in hyp := Ring_norm_gen ltac:(fun H => rewrite H in hyp). -Ltac Ring_nf Cst_tac lemma2 req rl f := - let on_rhs H := - match type of H with - | req _ ?rhs => clear H; f rhs - end in - Ring_norm_gen on_rhs Cst_tac lemma2 req rl. +Ltac Ring_gen pre post cst_tac pow_tac lemma1 req lH := + pre(); Ring cst_tac pow_tac lemma1 req ring_subst_niter lH. Tactic Notation (at level 0) "ring" := ring_lookup - (fun req sth ext morph arth cst_tac lemma1 lemma2 pre post rl => - pre(); Ring cst_tac lemma1 req). + (fun req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl => + Ring_gen pre post cst_tac pow_tac lemma1 req lH) []. -Tactic Notation (at level 0) "ring_simplify" constr_list(rl) := +Tactic Notation (at level 0) "ring" "[" constr_list(lH) "]" := ring_lookup - (fun req sth ext morph arth cst_tac lemma1 lemma2 pre post rl => - pre(); Ring_simplify cst_tac lemma2 req rl; post()) rl. + (fun req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl => + pre(); Ring_gen pre post cst_tac pow_tac lemma1 req lH) [lH]. -Tactic Notation (at level 0) "ring_simplify" constr_list(rl) "in" hyp(h) := - ring_lookup - (fun req sth ext morph arth cst_tac lemma1 lemma2 pre post rl => - pre(); Ring_simplify_in h cst_tac lemma2 req rl; post()) rl. +(* Simplification *) + + +Ltac Ring_simplify_gen f := + fun req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl => + pre(); + Ring_norm_gen f cst_tac pow_tac lemma2 req ring_subst_niter lH rl; + post(). + +Ltac Ring_simplify := Ring_simplify_gen ltac:(fun H => rewrite H). +Ltac Ring_simplify_in hyp:= Ring_simplify_gen ltac:(fun H => rewrite H in hyp). + + +Tactic Notation (at level 0) + "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) := + ring_lookup Ring_simplify [lH] rl. + +Tactic Notation (at level 0) + "ring_simplify" constr_list(rl) := + ring_lookup Ring_simplify [] rl. + +Tactic Notation (at level 0) + "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) "in" hyp(h):= + ring_lookup (Ring_simplify_in h) [lH] rl. + +Tactic Notation (at level 0) + "ring_simplify" constr_list(rl) "in" hyp(h):= + ring_lookup (Ring_simplify_in h) [] rl. -(* A simple macro tactic to be prefered to ring_simplify *) -Ltac ring_replace t1 t2 := replace t1 with t2 by ring. diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v index 2f7378eb0..dd63cf6d5 100644 --- a/contrib/setoid_ring/Ring_theory.v +++ b/contrib/setoid_ring/Ring_theory.v @@ -7,6 +7,9 @@ (************************************************************************) Require Import Setoid. +Require Import BinPos. +Require Import BinNat. + Set Implicit Arguments. Module RingSyntax. @@ -27,6 +30,71 @@ Reserved Notation "x == y" (at level 70, no associativity). End RingSyntax. Import RingSyntax. +Section Power. + Variable R:Type. + Variable rI : R. + Variable rmul : R -> R -> R. + Variable req : R -> R -> Prop. + Variable Rsth : Setoid_Theory R req. + Notation "x * y " := (rmul x y). + Notation "x == y" := (req x y). + + Hypothesis mul_ext : + forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 * y1 == x2 * y2. + Hypothesis mul_comm : forall x y, x * y == y * x. + Hypothesis mul_assoc : forall x y z, x * (y * z) == (x * y) * z. + Add Setoid R req Rsth as R_set_Power. + Add Morphism rmul : rmul_ext_Power. exact mul_ext. Qed. + + + Fixpoint pow_pos (x:R) (i:positive) {struct i}: R := + match i with + | xH => x + | xO i => let p := pow_pos x i in rmul p p + | xI i => let p := pow_pos x i in rmul (rmul x p) p + end. + + Lemma pow_pos_Psucc : forall x j, pow_pos x (Psucc j) == x * pow_pos x j. + Proof. + induction j;simpl. + rewrite IHj. + set (w:= x*pow_pos x j);unfold w at 2. + rewrite (mul_comm x (pow_pos x j));unfold w. + rewrite (mul_comm x (x * pow_pos x j * pow_pos x j)). + repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth). + repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth). + apply (Seq_refl _ _ Rsth). + 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 rewrite IHi. + rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite pow_pos_Psucc. + simpl;repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth). + rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc. + repeat rewrite IHi;rewrite mul_assoc. apply (Seq_refl _ _ Rsth). + rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;rewrite pow_pos_Psucc; + simpl. apply (Seq_refl _ _ Rsth). + Qed. + + Definition pow_N (x:R) (p:N) := + match p with + | N0 => rI + | 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; apply (Seq_refl _ _ Rsth). + Qed. + +End Power. + Section DEFINITIONS. Variable R : Type. Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R). @@ -126,6 +194,19 @@ Section DEFINITIONS. morph_opp : forall x, [-!x] == -[x]; morph_eq : forall x y, x?=!y = true -> [x] == [y] }. + + Section SIGN. + Variable get_sign : C -> option C. + Record sign_theory : Prop := mksign_th { + sign_spec : forall c c', get_sign c = Some c' -> [c] == - [c'] + }. + End SIGN. + + Definition get_sign_None (c:C) := @None C. + + Lemma get_sign_None_th : sign_theory get_sign_None. + Proof. constructor;intros;discriminate. Qed. + End MORPHISM. (** Identity is a morphism *) @@ -140,6 +221,20 @@ Section DEFINITIONS. try apply (Seq_refl _ _ Rsth);auto. Qed. + (** Specification of the power function *) + Section POWER. + Variable Cpow : Set. + Variable Cp_phi : N -> Cpow. + Variable rpow : R -> Cpow -> R. + + Record power_theory : Prop := mkpow_th { + rpow_pow_N : forall r n, req (rpow r (Cp_phi n)) (pow_N rI rmul r n) + }. + + End POWER. + + Definition pow_N_th := mkpow_th id_phi_N (pow_N rI rmul) (pow_N_pow_N rI rmul Rsth). + End DEFINITIONS. @@ -437,11 +532,12 @@ Qed. End ALMOST_RING. + Section AddRing. - Variable R : Type. +(* Variable R : Type. Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R). - Variable req : R -> R -> Prop. + Variable req : R -> R -> Prop. *) Inductive ring_kind : Type := | Abstract @@ -461,6 +557,7 @@ Inductive ring_kind : Type := (_ : ring_morph rO rI radd rmul rsub ropp req cO cI cadd cmul csub copp ceqb phi). + End AddRing. diff --git a/contrib/setoid_ring/ZArithRing.v b/contrib/setoid_ring/ZArithRing.v index 84b823d56..56367bc13 100644 --- a/contrib/setoid_ring/ZArithRing.v +++ b/contrib/setoid_ring/ZArithRing.v @@ -8,36 +8,53 @@ Require Export Ring. Require Import ZArith_base. +Require Import Zpow_def. + Import InitialRing. Set Implicit Arguments. -Ltac isZcst t := - match t with - Z0 => true - | Zpos ?p => isZcst p - | Zneg ?p => isZcst p - | xI ?p => isZcst p - | xO ?p => isZcst p - | xH => true - (* injection nat -> Z *) - | Z_of_nat ?n => isZcst n - | O => true - | S ?n => isZcst n - (* injection N -> Z *) - | Z_of_N ?n => isZcst n - | N0 => true - | Npos ?p => isZcst p - (* nat -> positive *) - | P_of_succ_nat ?n => isZcst n - (* *) - | _ => false - end. Ltac Zcst t := match isZcst t with true => t | _ => NotConstant end. +Ltac isZpow_coef t := + match t with + | Zpos ?p => isPcst p + | Z0 => true + | _ => false + end. + +Definition N_of_Z x := + match x with + | Zpos p => Npos p + | _ => N0 + end. + +Ltac Zpow_tac t := + match isZpow_coef t with + | true => constr:(N_of_Z t) + | _ => constr:(NotConstant) + end. + +Ltac Zpower_neg := + repeat match goal with + | [|- ?G] => + match G with + | context c [Zpower _ (Zneg _)] => + let t := context c [Z0] in + change t + end + end. + + Add Ring Zr : Zth - (decidable Zeqb_ok, constants [Zcst], preprocess [unfold Zsucc]). + (decidable Zeqb_ok, constants [Zcst], preprocess [Zpower_neg;unfold Zsucc], + power_tac Zpower_theory [Zpow_tac]). + + + + + diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index fd5411a2f..c22f1eb17 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -127,6 +127,12 @@ TACTIC EXTEND closed_term [ closed_term t l ] END ;; + +TACTIC EXTEND echo +| [ "echo" constr(t) ] -> + [ Pp.msg (Termops.print_constr t); Tacinterp.eval_tactic (TacId []) ] +END;; + (* let closed_term_ast l = TacFun([Some(id_of_string"t")], @@ -196,7 +202,8 @@ let constr_of = function let stdlib_modules = [["Coq";"Setoids";"Setoid"]; - ["Coq";"Lists";"List"] + ["Coq";"Lists";"List"]; + ["Coq";"Init";"Datatypes"] ] let coq_constant c = @@ -205,6 +212,8 @@ let coq_constant c = let coq_mk_Setoid = coq_constant "Build_Setoid_Theory" let coq_cons = coq_constant "cons" let coq_nil = coq_constant "nil" +let coq_None = coq_constant "None" +let coq_Some = coq_constant "Some" let lapp f args = mkApp(Lazy.force f,args) @@ -265,11 +274,18 @@ let coq_mk_seqe = my_constant "mk_seqe" let ltac_inv_morphZ = zltac"inv_gen_phiZ" let ltac_inv_morphN = zltac"inv_gen_phiN" - let coq_abstract = my_constant"Abstract" let coq_comp = my_constant"Computational" let coq_morph = my_constant"Morphism" +(* power function *) +let ltac_inv_morph_nothing = zltac"inv_morph_nothing" +let coq_pow_N_pow_N = my_constant "pow_N_pow_N" + +(* hypothesis *) +let coq_mkhypo = my_constant "mkhypo" +let coq_hypo = my_constant "hypo" + (* Equality: do not evaluate but make recursive call on both sides *) let map_with_eq arg_map c = let (req,_,_) = dest_rel c in @@ -283,10 +299,12 @@ let _ = add_map "ring" coq_nil, (function -1->Eval|_ -> Prot); (* Pphi_dev: evaluate polynomial and coef operations, protect ring operations and make recursive call on the var map *) - pol_cst "Pphi_dev", (function -1|6|7|8|9|11->Eval|10->Rec|_->Prot); + pol_cst "Pphi_dev", (function -1|8|9|10|11|12|13|15->Eval|14->Rec|_->Prot); + pol_cst "Pphi_pow", + (function -1|8|9|10|11|12|14|16|18->Eval|17->Rec|_->Prot); (* PEeval: evaluate morphism and polynomial, protect ring operations and make recursive call on the var map *) - pol_cst "PEeval", (function -1|7|9->Eval|8->Rec|_->Prot)]) + pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot)]) (****************************************************************************) (* Ring database *) @@ -299,6 +317,7 @@ type ring_info = ring_morph : constr; ring_th : constr; ring_cst_tac : glob_tactic_expr; + ring_pow_tac : glob_tactic_expr; ring_lemma1 : constr; ring_lemma2 : constr; ring_pre_tac : glob_tactic_expr; @@ -378,6 +397,7 @@ let subst_th (_,subst,th) = let thm1' = subst_mps subst th.ring_lemma1 in let thm2' = subst_mps subst th.ring_lemma2 in let tac'= subst_tactic subst th.ring_cst_tac in + let pow_tac'= subst_tactic subst th.ring_pow_tac in let pretac'= subst_tactic subst th.ring_pre_tac in let posttac'= subst_tactic subst th.ring_post_tac in if c' == th.ring_carrier && @@ -389,6 +409,7 @@ let subst_th (_,subst,th) = thm1' == th.ring_lemma1 && thm2' == th.ring_lemma2 && tac' == th.ring_cst_tac && + pow_tac' == th.ring_pow_tac && pretac' == th.ring_pre_tac && posttac' == th.ring_post_tac then th else @@ -399,6 +420,7 @@ let subst_th (_,subst,th) = ring_morph = morph'; ring_th = th'; ring_cst_tac = tac'; + ring_pow_tac = pow_tac'; ring_lemma1 = thm1'; ring_lemma2 = thm2'; ring_pre_tac = pretac'; @@ -532,14 +554,50 @@ let interp_cst_tac kind (zero,one,add,mul,opp) cst_tac = TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp])) | _ -> error"a tactic must be specified for an almost_ring") -let add_theory name rth eqth morphth cst_tac (pre,post) = +let make_hyp env c = + let t = (Typeops.typing env c).uj_type in + lapp coq_mkhypo [|t;c|] + +let make_hyp_list env lH = + let carrier = Lazy.force coq_hypo in + List.fold_right + (fun c l -> lapp coq_cons [|carrier; (make_hyp env c); l|]) lH + (lapp coq_nil [|carrier|]) + +let interp_power env pow = + let carrier = Lazy.force coq_hypo in + match pow with + | None -> + let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_nothing) in + (TacArg(TacCall(dummy_loc,t,[])), lapp coq_None [|carrier|]) + | Some (tac, spec) -> + let tac = + match tac with + | CstTac t -> Tacinterp.glob_tactic t + | Closed lc -> closed_term_ast (List.map Nametab.global lc) in + let spec = make_hyp env (ic spec) in + (tac, lapp coq_Some [|carrier; spec|]) + +let interp_sign env sign = + let carrier = Lazy.force coq_hypo in + match sign with + | None -> lapp coq_None [|carrier|] + | Some spec -> + let spec = make_hyp env (ic spec) in + lapp coq_Some [|carrier;spec|] + (* Same remark on ill-typed terms ... *) + +let add_theory name rth eqth morphth cst_tac (pre,post) power sign = let env = Global.env() in let sigma = Evd.empty in let (kind,r,zero,one,add,mul,sub,opp,req) = dest_ring env sigma rth in let (sth,ext) = build_setoid_params r add mul opp req eqth in + let (pow_tac, pspec) = interp_power env power in + let sspec = interp_sign env sign in let rk = reflect_coeff morphth in let params = - exec_tactic env 5 (zltac"ring_lemmas") (List.map carg[sth;ext;rth;rk]) in + exec_tactic env 5 (zltac "ring_lemmas") + (List.map carg[sth;ext;rth;pspec;sspec;rk]) in let lemma1 = constr_of params.(3) in let lemma2 = constr_of params.(4) in @@ -564,6 +622,7 @@ let add_theory name rth eqth morphth cst_tac (pre,post) = ring_morph = constr_of params.(2); ring_th = constr_of params.(0); ring_cst_tac = cst_tac; + ring_pow_tac = pow_tac; ring_lemma1 = lemma1; ring_lemma2 = lemma2; ring_pre_tac = pretac; @@ -576,6 +635,10 @@ type ring_mod = | Pre_tac of raw_tactic_expr | Post_tac of raw_tactic_expr | Setoid of Topconstr.constr_expr * Topconstr.constr_expr + | Pow_spec of cst_tac_spec * Topconstr.constr_expr + (* Syntaxification tactic , correctness lemma *) + | Sign_spec of Topconstr.constr_expr + VERNAC ARGUMENT EXTEND ring_mod | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational (ic eq_test)) ] @@ -586,6 +649,11 @@ VERNAC ARGUMENT EXTEND ring_mod | [ "preprocess" "[" tactic(pre) "]" ] -> [ Pre_tac pre ] | [ "postprocess" "[" tactic(post) "]" ] -> [ Post_tac post ] | [ "setoid" constr(sth) constr(ext) ] -> [ Setoid(sth,ext) ] + | [ "sign" constr(sign_spec) ] -> [ Sign_spec sign_spec ] + | [ "power" constr(pow_spec) "[" ne_global_list(l) "]" ] -> + [ Pow_spec (Closed l, pow_spec) ] + | [ "power_tac" constr(pow_spec) "[" tactic(cst_tac) "]" ] -> + [ Pow_spec (CstTac cst_tac, pow_spec) ] END let set_once s r v = @@ -597,19 +665,23 @@ let process_ring_mods l = let cst_tac = ref None in let pre = ref None in let post = ref None in + let sign = ref None in + let power = ref None in List.iter(function Ring_kind k -> set_once "ring kind" kind k | Const_tac t -> set_once "tactic recognizing constants" cst_tac t | Pre_tac t -> set_once "preprocess tactic" pre t | Post_tac t -> set_once "postprocess tactic" post t - | Setoid(sth,ext) -> set_once "setoid" set (ic sth,ic ext)) l; + | Setoid(sth,ext) -> set_once "setoid" set (ic sth,ic ext) + | Pow_spec(t,spec) -> set_once "power" power (t,spec) + | Sign_spec t -> set_once "sign" sign t) l; let k = match !kind with Some k -> k | None -> Abstract in - (k, !set, !cst_tac, !pre, !post) + (k, !set, !cst_tac, !pre, !post, !power, !sign) VERNAC COMMAND EXTEND AddSetoidRing | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods(l) ] -> - [ let (k,set,cst,pre,post) = process_ring_mods l in - add_theory id (ic t) set k cst (pre,post) ] + [ let (k,set,cst,pre,post,power,sign) = process_ring_mods l in + add_theory id (ic t) set k cst (pre,post) power sign ] END (*****************************************************************************) @@ -625,17 +697,20 @@ let make_term_list carrier rl gl = (fun x l -> lapp coq_cons [|carrier;x;l|]) rl (lapp coq_nil [|carrier|]) -let ring_lookup (f:glob_tactic_expr) rl gl = + +let ring_lookup (f:glob_tactic_expr) lH rl gl = let env = pf_env gl in let sigma = project gl in let e = find_ring_structure env sigma rl (pf_concl gl) None in let rl = carg (make_term_list e.ring_carrier rl gl) in + let lH = carg (make_hyp_list env lH) in let req = carg e.ring_req in let sth = carg e.ring_setoid in let ext = carg e.ring_ext in let morph = carg e.ring_morph in let th = carg e.ring_th in let cst_tac = Tacexp e.ring_cst_tac in + let pow_tac = Tacexp e.ring_pow_tac in let lemma1 = carg e.ring_lemma1 in let lemma2 = carg e.ring_lemma2 in let pretac = Tacexp(TacFun([None],e.ring_pre_tac)) in @@ -644,12 +719,16 @@ let ring_lookup (f:glob_tactic_expr) rl gl = (TacLetIn ([(dummy_loc,id_of_string"f"),None,Tacexp f], ltac_lcall "f" - [req;sth;ext;morph;th;cst_tac;lemma1;lemma2;pretac;posttac;rl])) gl + [req;sth;ext;morph;th;cst_tac;pow_tac; + lemma1;lemma2;pretac;posttac;lH;rl])) gl TACTIC EXTEND ring_lookup -| [ "ring_lookup" tactic(f) constr_list(l) ] -> [ ring_lookup (fst f) l ] +| [ "ring_lookup" tactic(f) "[" constr_list(lH) "]" constr_list(lr)] -> + [ring_lookup (fst f) lH lr] END + + (***********************************************************************) let new_field_path = @@ -666,14 +745,20 @@ let _ = add_map "field" (* display_linear: evaluate polynomials and coef operations, protect field operations and make recursive call on the var map *) my_constant "display_linear", - (function -1|7|8|9|10|12|13->Eval|11->Rec|_->Prot); - (* Pphi_dev: evaluate polynomial and coef operations, protect + (function -1|8|9|10|11|12|13|14|16|17->Eval|15->Rec|_->Prot); + my_constant "display_pow_linear", + (function -1|8|9|10|11|12|13|14|15|17|19|20->Eval|18->Rec|_->Prot); + (* Pphi_dev: evaluate polynomial and coef operations, protect ring operations and make recursive call on the var map *) - my_constant "Pphi_dev", (function -1|6|7|8|9|11->Eval|10->Rec|_->Prot); + pol_cst "Pphi_dev", (function -1|8|9|10|11|12|13|15->Eval|14->Rec|_->Prot); + pol_cst "Pphi_pow", + (function -1|8|9|10|11|12|14|16|18->Eval|17->Rec|_->Prot); (* PEeval: evaluate morphism and polynomial, protect ring operations and make recursive call on the var map *) - my_constant "FEeval", (function -1|9|11->Eval|10->Rec|_->Prot)]);; - + pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot); + (* FEeval: evaluate morphism, protect field + operations and make recursive call on the var map *) + my_constant "FEeval", (function -1|8|9|10|11|14->Eval|13->Rec|_->Prot)]);; let _ = add_map "field_cond" (map_with_eq @@ -681,7 +766,8 @@ let _ = add_map "field_cond" coq_nil, (function -1->Eval|_ -> Prot); (* PCond: evaluate morphism and denum list, protect ring operations and make recursive call on the var map *) - my_constant "PCond", (function -1|8|10->Eval|9->Rec|_->Prot)]);; + my_constant "PCond", (function -1|8|10|13->Eval|12->Rec|_->Prot)]);; +(* (function -1|8|10->Eval|9->Rec|_->Prot)]);;*) let afield_theory = my_constant "almost_field_theory" @@ -715,6 +801,7 @@ type field_info = { field_carrier : types; field_req : constr; field_cst_tac : glob_tactic_expr; + field_pow_tac : glob_tactic_expr; field_ok : constr; field_simpl_eq_ok : constr; field_simpl_ok : constr; @@ -798,6 +885,7 @@ let subst_th (_,subst,th) = let thm3' = subst_mps subst th.field_simpl_ok in let thm4' = subst_mps subst th.field_cond in let tac'= subst_tactic subst th.field_cst_tac in + let pow_tac' = subst_tactic subst th.field_pow_tac in let pretac'= subst_tactic subst th.field_pre_tac in let posttac'= subst_tactic subst th.field_post_tac in if c' == th.field_carrier && @@ -807,12 +895,14 @@ let subst_th (_,subst,th) = thm3' == th.field_simpl_ok && thm4' == th.field_cond && tac' == th.field_cst_tac && + pow_tac' == th.field_pow_tac && pretac' == th.field_pre_tac && posttac' == th.field_post_tac then th else { field_carrier = c'; field_req = eq'; field_cst_tac = tac'; + field_pow_tac = pow_tac'; field_ok = thm1'; field_simpl_eq_ok = thm2'; field_simpl_ok = thm3'; @@ -850,19 +940,21 @@ let default_field_equality r inv req = error "field inverse should be declared as a morphism" in inv_m.lem -let add_field_theory name fth eqth morphth cst_tac inj (pre,post) = +let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign = let env = Global.env() in let sigma = Evd.empty in let (kind,r,zero,one,add,mul,sub,opp,div,inv,req,rth) = dest_field env sigma fth in let (sth,ext) = build_setoid_params r add mul opp req eqth in let eqth = Some(sth,ext) in - let _ = add_theory name rth eqth morphth cst_tac (None,None) in + let _ = add_theory name rth eqth morphth cst_tac (None,None) power sign in + let (pow_tac, pspec) = interp_power env power in + let sspec = interp_sign env sign in let inv_m = default_field_equality r inv req in let rk = reflect_coeff morphth in let params = exec_tactic env 8 (field_ltac"field_lemmas") - (List.map carg[sth;ext;inv_m;fth;rk]) in + (List.map carg[sth;ext;inv_m;fth;pspec;sspec;rk]) in let lemma1 = constr_of params.(3) in let lemma2 = constr_of params.(4) in let lemma3 = constr_of params.(5) in @@ -889,6 +981,7 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) = { field_carrier = r; field_req = req; field_cst_tac = cst_tac; + field_pow_tac = pow_tac; field_ok = lemma1; field_simpl_eq_ok = lemma2; field_simpl_ok = lemma3; @@ -911,7 +1004,9 @@ let process_field_mods l = let cst_tac = ref None in let pre = ref None in let post = ref None in - let inj = ref None in + let inj = ref None in + let sign = ref None in + let power = ref None in List.iter(function Ring_mod(Ring_kind k) -> set_once "field kind" kind k | Ring_mod(Const_tac t) -> @@ -919,23 +1014,27 @@ let process_field_mods l = | Ring_mod(Pre_tac t) -> set_once "preprocess tactic" pre t | Ring_mod(Post_tac t) -> set_once "postprocess tactic" post t | Ring_mod(Setoid(sth,ext)) -> set_once "setoid" set (ic sth,ic ext) + | Ring_mod(Pow_spec(t,spec)) -> set_once "power" power (t,spec) + | Ring_mod(Sign_spec t) -> set_once "sign" sign t | Inject i -> set_once "infinite property" inj (ic i)) l; let k = match !kind with Some k -> k | None -> Abstract in - (k, !set, !inj, !cst_tac, !pre, !post) + (k, !set, !inj, !cst_tac, !pre, !post, !power, !sign) VERNAC COMMAND EXTEND AddSetoidField | [ "Add" "Field" ident(id) ":" constr(t) field_mods(l) ] -> - [ let (k,set,inj,cst_tac,pre,post) = process_field_mods l in - add_field_theory id (ic t) set k cst_tac inj (pre,post) ] + [ let (k,set,inj,cst_tac,pre,post,power,sign) = process_field_mods l in + add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign] END -let field_lookup (f:glob_tactic_expr) rl gl = +let field_lookup (f:glob_tactic_expr) lH rl gl = let env = pf_env gl in let sigma = project gl in let e = find_field_structure env sigma rl (pf_concl gl) None in let rl = carg (make_term_list e.field_carrier rl gl) in + let lH = carg (make_hyp_list env lH) in let req = carg e.field_req in let cst_tac = Tacexp e.field_cst_tac in + let pow_tac = Tacexp e.field_pow_tac in let field_ok = carg e.field_ok in let field_simpl_ok = carg e.field_simpl_ok in let field_simpl_eq_ok = carg e.field_simpl_eq_ok in @@ -946,9 +1045,10 @@ let field_lookup (f:glob_tactic_expr) rl gl = (TacLetIn ([(dummy_loc,id_of_string"f"),None,Tacexp f], ltac_lcall "f" - [req;cst_tac;field_ok;field_simpl_ok;field_simpl_eq_ok;cond_ok; - pretac;posttac;rl])) gl + [req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok;cond_ok; + pretac;posttac;lH;rl])) gl TACTIC EXTEND field_lookup -| [ "field_lookup" tactic(f) constr_list(l) ] -> [ field_lookup (fst f) l ] +| [ "field_lookup" tactic(f) "[" constr_list(lH) "]" constr_list(l) ] -> + [ field_lookup (fst f) lH l ] END diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 70648b44b..affcccb3a 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -10,11 +10,11 @@ #include <stdio.h> #include <stdlib.h> -#include "config.h" -#include "misc.h" -#include "mlvalues.h" -#include "fail.h" -#include "memory.h" +#include <config.h> +#include <misc.h> +#include <mlvalues.h> +#include <fail.h> +#include <memory.h> #include "coq_instruct.h" #include "coq_fix_code.h" diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h index 035d5b9b1..d1dac80fb 100644 --- a/kernel/byterun/coq_fix_code.h +++ b/kernel/byterun/coq_fix_code.h @@ -12,7 +12,7 @@ #ifndef _COQ_FIX_CODE_ #define _COQ_FIX_CODE_ -#include "mlvalues.h" +#include <mlvalues.h> void * coq_stat_alloc (asize_t sz); #ifdef THREADED_CODE diff --git a/kernel/byterun/coq_gc.h b/kernel/byterun/coq_gc.h index 2f0853264..ccccbe78d 100644 --- a/kernel/byterun/coq_gc.h +++ b/kernel/byterun/coq_gc.h @@ -10,8 +10,8 @@ #ifndef _COQ_CAML_GC_ #define _COQ_CAML_GC_ -#include "mlvalues.h" -#include "alloc.h" +#include <mlvalues.h> +#include <alloc.h> typedef void (*scanning_action) (value, value *); diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 0f91a7e3f..8f9c10e68 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -44,11 +44,7 @@ sp is a local copy of the global variable extern_sp. */ # ifdef DEBUG # define Next goto next_instr # else -# ifdef __ia64__ -# define Next goto *(void *)(coq_jumptbl_base + *((uint32 *) pc)++) -# else -# define Next goto *(void *)(coq_jumptbl_base + *pc++) -# endif +# define Next goto *(void *)(coq_jumptbl_base + *pc++) # endif #else # define Instruct(name) case name: diff --git a/kernel/byterun/coq_interp.h b/kernel/byterun/coq_interp.h index 76e689440..60865c32e 100644 --- a/kernel/byterun/coq_interp.h +++ b/kernel/byterun/coq_interp.h @@ -19,5 +19,9 @@ value coq_push_vstack(value stk); value coq_interprete_ml(value tcode, value a, value e, value ea); +value coq_interprete + (code_t coq_pc, value coq_accu, value coq_env, long coq_extra_args); + value coq_eval_tcode (value tcode, value e); + diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index bfcb6812c..913421087 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -14,6 +14,7 @@ #include "coq_instruct.h" #include "coq_fix_code.h" #include "coq_memory.h" +#include "coq_interp.h" /* stack */ @@ -264,9 +265,3 @@ value coq_set_drawinstr(value unit) return Val_unit; } - -value coq_print_pointer(value p) -{ - printf("pointer = %X\n", p); - return Val_unit; -} diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h index 0d866dc76..edd059488 100644 --- a/kernel/byterun/coq_memory.h +++ b/kernel/byterun/coq_memory.h @@ -11,11 +11,11 @@ #ifndef _COQ_MEMORY_ #define _COQ_MEMORY_ -#include "config.h" -#include "fail.h" -#include "misc.h" -#include "memory.h" -#include "mlvalues.h" +#include <config.h> +#include <fail.h> +#include <misc.h> +#include <memory.h> +#include <mlvalues.h> #define Coq_stack_size (4096 * sizeof(value)) diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c index 34b885e8f..007f61b27 100644 --- a/kernel/byterun/coq_values.c +++ b/kernel/byterun/coq_values.c @@ -13,7 +13,7 @@ #include "coq_instruct.h" #include "coq_memory.h" #include "coq_values.h" -#include "memory.h" +#include <memory.h> /* KIND OF VALUES */ #define Setup_for_gc diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index a5176f3f5..4c631fce3 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -11,8 +11,8 @@ #ifndef _COQ_VALUES_ #define _COQ_VALUES_ -#include "alloc.h" -#include "mlvalues.h" +#include <alloc.h> +#include <mlvalues.h> #define Default_tag 0 #define Accu_tag 0 diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 9066e46d9..fe428230a 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -106,3 +106,4 @@ val type_of_constant_knowing_parameters : (* Make a type polymorphic if an arity *) val make_polymorphic_if_arity : env -> types -> constant_type + diff --git a/kernel/vm.ml b/kernel/vm.ml index de9bd753a..131e8320f 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -469,8 +469,6 @@ let check_cofix vcf1 vcf2 = (current_cofix vcf1 = current_cofix vcf2) && (Obj.size (last (Obj.repr vcf1)) = Obj.size (last (Obj.repr vcf2))) -external print_point : Obj.t -> unit = "coq_print_pointer" - let reduce_cofix k vcf = let fc_typ = ((Obj.obj (last (Obj.repr vcf))) : tcode array) in let ndef = Array.length fc_typ in diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 9a4995c03..a76402e09 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -309,6 +309,7 @@ GEXTEND Gram | IDENT "assumption" -> TacAssumption | IDENT "exact"; c = constr -> TacExact c | IDENT "exact_no_check"; c = constr -> TacExactNoCheck c + | IDENT "vm_cast_no_check"; c = constr -> TacVmCastNoCheck c | IDENT "apply"; cl = constr_with_bindings -> TacApply cl | IDENT "elim"; cl = constr_with_bindings; el = OPT eliminator -> diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index ebf4b5ad1..495634512 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -652,6 +652,7 @@ and pr_atom1 = function | TacAssumption as t -> pr_atom0 t | TacExact c -> hov 1 (str "exact" ++ pr_constrarg c) | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c) + | TacVmCastNoCheck c -> hov 1 (str "vm_cast_no_check" ++ pr_constrarg c) | TacApply cb -> hov 1 (str "apply" ++ spc () ++ pr_with_bindings cb) | TacElim (cb,cbo) -> hov 1 (str "elim" ++ pr_arg pr_with_bindings cb ++ diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 70bc3f682..56dd32c55 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -271,6 +271,8 @@ let rec mlexpr_of_atomic_tactic = function <:expr< Tacexpr.TacExact $mlexpr_of_constr c$ >> | Tacexpr.TacExactNoCheck c -> <:expr< Tacexpr.TacExactNoCheck $mlexpr_of_constr c$ >> + | Tacexpr.TacVmCastNoCheck c -> + <:expr< Tacexpr.TacVmCastNoCheck $mlexpr_of_constr c$ >> | Tacexpr.TacApply cb -> <:expr< Tacexpr.TacApply $mlexpr_of_constr_with_binding cb$ >> | Tacexpr.TacElim (cb,cbo) -> diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index d7a9879be..b072e7cc3 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -121,6 +121,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacAssumption | TacExact of 'constr | TacExactNoCheck of 'constr + | TacVmCastNoCheck of 'constr | TacApply of 'constr with_bindings | TacElim of 'constr with_bindings * 'constr with_bindings option | TacElimType of 'constr diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 02792cb33..a940b5a0d 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -29,6 +29,8 @@ let h_intros_until x = abstract_tactic (TacIntrosUntil x) (intros_until x) let h_assumption = abstract_tactic TacAssumption assumption let h_exact c = abstract_tactic (TacExact c) (exact_check c) let h_exact_no_check c = abstract_tactic (TacExactNoCheck c) (exact_no_check c) +let h_vm_cast_no_check c = + abstract_tactic (TacVmCastNoCheck c) (vm_cast_no_check c) let h_apply cb = abstract_tactic (TacApply cb) (apply_with_bindings cb) let h_elim cb cbo = abstract_tactic (TacElim (cb,cbo)) (elim cb cbo) let h_elim_type c = abstract_tactic (TacElimType c) (elim_type c) diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 2823a53ad..bb1e4f423 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -30,6 +30,7 @@ val h_intros_until : quantified_hypothesis -> tactic val h_assumption : tactic val h_exact : constr -> tactic val h_exact_no_check : constr -> tactic +val h_vm_cast_no_check : constr -> tactic val h_apply : constr with_bindings -> tactic diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index ee70c326f..8eff3ccd9 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -626,6 +626,7 @@ let rec intern_atomic lf ist x = | TacAssumption -> TacAssumption | TacExact c -> TacExact (intern_constr ist c) | TacExactNoCheck c -> TacExactNoCheck (intern_constr ist c) + | TacVmCastNoCheck c -> TacVmCastNoCheck (intern_constr ist c) | TacApply cb -> TacApply (intern_constr_with_bindings ist cb) | TacElim (cb,cbo) -> TacElim (intern_constr_with_bindings ist cb, @@ -1992,6 +1993,7 @@ and interp_atomic ist gl = function | TacAssumption -> h_assumption | TacExact c -> h_exact (pf_interp_casted_constr ist gl c) | TacExactNoCheck c -> h_exact_no_check (pf_interp_constr ist gl c) + | TacVmCastNoCheck c -> h_vm_cast_no_check (pf_interp_constr ist gl c) | TacApply cb -> h_apply (interp_constr_with_bindings ist gl cb) | TacElim (cb,cbo) -> h_elim (interp_constr_with_bindings ist gl cb) @@ -2320,6 +2322,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacAssumption as x -> x | TacExact c -> TacExact (subst_rawconstr subst c) | TacExactNoCheck c -> TacExactNoCheck (subst_rawconstr subst c) + | TacVmCastNoCheck c -> TacVmCastNoCheck (subst_rawconstr subst c) | TacApply cb -> TacApply (subst_raw_with_bindings subst cb) | TacElim (cb,cbo) -> TacElim (subst_raw_with_bindings subst cb, diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f27d116e4..eba3fa4e4 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -629,6 +629,11 @@ let exact_check c gl = let exact_no_check = refine_no_check +let vm_cast_no_check c gl = + let concl = pf_concl gl in + refine_no_check (Term.mkCast(c,Term.VMcast,concl)) gl + + let exact_proof c gl = (* on experimente la synthese d'ise dans exact *) let c = Constrintern.interp_casted_constr (project gl) (pf_env gl) c (pf_concl gl) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index c1b8782b3..ac51f736c 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -106,6 +106,7 @@ val intros_pattern : identifier option -> intro_pattern_expr list -> tactic val assumption : tactic val exact_no_check : constr -> tactic +val vm_cast_no_check : constr -> tactic val exact_check : constr -> tactic val exact_proof : Topconstr.constr_expr -> tactic diff --git a/theories/Lists/ListTactics.v b/theories/Lists/ListTactics.v index 961101d65..233b40b88 100644 --- a/theories/Lists/ListTactics.v +++ b/theories/Lists/ListTactics.v @@ -17,6 +17,14 @@ Ltac list_fold_right fcons fnil l := | nil => fnil end. +Ltac lazy_list_fold_right fcons fnil l := + match l with + | (cons ?x ?tl) => + let cont := lazy_list_fold_right fcons fnil in + fcons x cont tl + | nil => fnil + end. + Ltac list_fold_left fcons fnil l := match l with | (cons ?x ?tl) => list_fold_left fcons ltac:(fcons x fnil) tl diff --git a/theories/QArith/Qring.v b/theories/QArith/Qring.v index 265851ec7..609e82b07 100644 --- a/theories/QArith/Qring.v +++ b/theories/QArith/Qring.v @@ -37,15 +37,15 @@ Proof. Qed. Ltac isQcst t := - let t := eval hnf in t in - match t with - Qmake ?n ?d => - match isZcst n with - true => isZcst d - | _ => false - end - | _ => false - end. + match t with + | inject_Z ?z => isZcst z + | Qmake ?n ?d => + match isZcst n with + true => isPcst d + | _ => false + end + | _ => false + end. Ltac Qcst t := match isQcst t with @@ -74,7 +74,7 @@ Let ex3 : forall x y z : Q, (x+y)+z == x+(y+z). Qed. Let ex4 : (inject_Z 1)+(inject_Z 1)==(inject_Z 2). - ring. + ring. Qed. Let ex5 : 1+1 == 2#1. diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v index a3dbca23d..eff4a6c3d 100644 --- a/theories/Reals/Cos_rel.v +++ b/theories/Reals/Cos_rel.v @@ -109,9 +109,10 @@ pose C (2 * S p) (S (2 * l)) * x ^ S (2 * l) * y ^ S (2 * (p - l))) p end). ring_simplify. +unfold Rminus. replace (* (- old ring compat *) - (-1 * + (- sum_f_R0 (fun k:nat => sum_f_R0 @@ -140,7 +141,6 @@ replace (fun l:nat => C (2 * S i) (S (2 * l)) * x ^ S (2 * l) * y ^ S (2 * (i - l))) i) with (sum_f_R0 (fun l:nat => Wn (S (2 * l))) i). -(*rewrite Rplus_comm.*) (* compatibility old ring... *) apply sum_decomposition. apply sum_eq; intros. unfold Wn in |- *. @@ -154,8 +154,7 @@ apply Rmult_eq_compat_l. replace (2 * S i - 2 * i0)%nat with (2 * (S i - i0))%nat. reflexivity. omega. -replace (sum_f_R0 sin_nnn (S n)) with (-1 * (-1 * sum_f_R0 sin_nnn (S n))). -(*replace (* compatibility old ring... *) +replace (- sum_f_R0 (fun k:nat => @@ -171,13 +170,13 @@ replace (sum_f_R0 sin_nnn (S n)) with (-1 * (-1 * sum_f_R0 sin_nnn (S n))). (fun p:nat => (-1) ^ p / INR (fact (2 * p + 1)) * x ^ (2 * p + 1) * ((-1) ^ (k - p) / INR (fact (2 * (k - p) + 1)) * - y ^ (2 * (k - p) + 1))) k) n);[idtac|ring].*) -apply Rmult_eq_compat_l. + y ^ (2 * (k - p) + 1))) k) n);[idtac|ring]. rewrite scal_sum. rewrite decomp_sum. replace (sin_nnn 0%nat) with 0. -rewrite Rmult_0_l; rewrite Rplus_0_l. -replace (pred (S n)) with n; [ idtac | reflexivity ]. +rewrite Rplus_0_l. +change (pred (S n)) with n. + (* replace (pred (S n)) with n; [ idtac | reflexivity ]. *) apply sum_eq; intros. rewrite Rmult_comm. unfold sin_nnn in |- *. @@ -185,8 +184,8 @@ rewrite scal_sum. rewrite scal_sum. apply sum_eq; intros. unfold Rdiv in |- *. -repeat rewrite Rmult_assoc. -rewrite (Rmult_comm (/ INR (fact (2 * S i)))). +(*repeat rewrite Rmult_assoc.*) +(* rewrite (Rmult_comm (/ INR (fact (2 * S i)))). *) repeat rewrite <- Rmult_assoc. rewrite <- (Rmult_comm (/ INR (fact (2 * S i)))). repeat rewrite <- Rmult_assoc. @@ -216,7 +215,7 @@ apply INR_fact_neq_0. apply INR_fact_neq_0. reflexivity. apply lt_O_Sn. -ring. +(* ring. *) apply sum_eq; intros. rewrite scal_sum. apply sum_eq; intros. diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v index 7077d1015..3447aa0e4 100644 --- a/theories/Reals/Rdefinitions.v +++ b/theories/Reals/Rdefinitions.v @@ -55,6 +55,8 @@ Definition Rminus (r1 r2:R) : R := (r1 + - r2)%R. (**********) Definition Rdiv (r1 r2:R) : R := (r1 * / r2)%R. +(**********) + Infix "-" := Rminus : R_scope. Infix "/" := Rdiv : R_scope. diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index f048faf53..ba7396ed6 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -19,6 +19,7 @@ Require Export LegacyArithRing. (* for ring_nat... *) Require Export ArithRing. Require Import Rbase. +Require Export Rpow_def. Require Export R_Ifp. Require Export Rbasic_fun. Require Export R_sqr. @@ -65,11 +66,6 @@ Qed. (** * Power *) (*******************************) (*********) -Boxed Fixpoint pow (r:R) (n:nat) {struct n} : R := - match n with - | O => 1 - | S n => r * pow r n - end. Infix "^" := pow : R_scope. diff --git a/theories/Reals/Rpow_def.v b/theories/Reals/Rpow_def.v new file mode 100644 index 000000000..5bdbb76b9 --- /dev/null +++ b/theories/Reals/Rpow_def.v @@ -0,0 +1,7 @@ +Require Import Rdefinitions. + +Fixpoint pow (r:R) (n:nat) {struct n} : R := + match n with + | O => R1 + | S n => Rmult r (pow r n) + end. diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index d05fd99cb..2adac468b 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -1580,10 +1580,14 @@ Lemma cos_eq_0_0 : Proof. intros x H; rewrite cos_sin in H; generalize (sin_eq_0_0 (PI / INR 2 + x) H); intro H2; elim H2; intros x0 H3; exists (x0 - Z_of_nat 1)%Z; - rewrite <- Z_R_minus; simpl; ring_simplify; -(* rewrite (Rmult_comm PI);*) (* old ring compat *) + rewrite <- Z_R_minus; simpl. +unfold INR in H3. field_simplify [(sym_eq H3)]. field. +(** + ring_simplify. + (* rewrite (Rmult_comm PI);*) (* old ring compat *) rewrite <- H3; simpl; - field; repeat split; discrR. + field;repeat split; discrR. +*) Qed. Lemma cos_eq_0_1 : diff --git a/theories/ZArith/Zpow_def.v b/theories/ZArith/Zpow_def.v new file mode 100644 index 000000000..dabd6ace1 --- /dev/null +++ b/theories/ZArith/Zpow_def.v @@ -0,0 +1,27 @@ +Require Import ZArith_base. +Require Import Ring_theory. + +Open Scope Z_scope. + +(** [Zpower_pos z n] is the n-th power of [z] when [n] is an binary + integer (type [positive]) and [z] a signed integer (type [Z]) *) +Definition Zpower_pos (z:Z) (n:positive) := iter_pos n Z (fun x:Z => z * x) 1. + +Definition Zpower (x y:Z) := + match y with + | Zpos p => Zpower_pos x p + | Z0 => 1 + | Zneg p => 0 + end. + +Lemma Zpower_theory : power_theory 1 Zmult (eq (A:=Z)) Z_of_N Zpower. +Proof. + constructor. intros. + destruct n;simpl;trivial. + unfold Zpower_pos. + assert (forall k, iter_pos p Z (fun x : Z => r * x) k = pow_pos Zmult r p*k). + induction p;simpl;intros;repeat rewrite IHp;trivial; + repeat rewrite Zmult_assoc;trivial. + rewrite H;rewrite Zmult_1_r;trivial. +Qed. + diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v index 248af0102..4e08c726e 100644 --- a/theories/ZArith/Zpower.v +++ b/theories/ZArith/Zpower.v @@ -9,6 +9,7 @@ (*i $Id$ i*) Require Import ZArith_base. +Require Export Zpow_def. Require Import Omega. Require Import Zcomplements. Open Local Scope Z_scope. @@ -35,11 +36,6 @@ Section section1. apply Zmult_assoc ]. Qed. - (** [Zpower_pos z n] is the n-th power of [z] when [n] is an binary - integer (type [positive]) and [z] a signed integer (type [Z]) *) - - Definition Zpower_pos (z:Z) (n:positive) := iter_pos n Z (fun x:Z => z * x) 1. - (** This theorem shows that powers of unary and binary integers are the same thing, modulo the function convert : [positive -> nat] *) @@ -66,13 +62,6 @@ Section section1. apply Zpower_nat_is_exp. Qed. - Definition Zpower (x y:Z) := - match y with - | Zpos p => Zpower_pos x p - | Z0 => 1 - | Zneg p => 0 - end. - Infix "^" := Zpower : Z_scope. Hint Immediate Zpower_nat_is_exp: zarith. @@ -382,4 +371,4 @@ Section power_div_with_rest. apply Zdiv_rest_proof with (q := a0) (r := b); assumption. Qed. -End power_div_with_rest.
\ No newline at end of file +End power_div_with_rest. diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v index 79fce8964..4a395e6f8 100644 --- a/theories/ZArith/Zsqrt.v +++ b/theories/ZArith/Zsqrt.v @@ -132,7 +132,7 @@ Definition Zsqrt : (fun r:Z => 0 = 0 * 0 + r /\ 0 * 0 <= 0 < (0 + 1) * (0 + 1)) 0 _) end); try omega. -split; [ omega | rewrite Heq; ring_simplify ((s + 1) * (s + 1)); omega ]. + split; [ omega | rewrite Heq; ring_simplify (s*s) ((s + 1) * (s + 1)); omega ]. Defined. (** Define a function of type Z->Z that computes the integer square root, |