From 518a1dc079ec7295e6b0a85f379512110dd453db Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 29 May 2025 23:04:17 -0400 Subject: [PATCH 1/2] Clean up subcomponent dependencies of lia --- .../stdlib-subcomponents/default.nix | 28 +- doc/changelog/01-changed/150-early-lia.rst | 8 + doc/changelog/02-added/150-early-lia.rst | 12 + doc/changelog/04-removed/150-early-lia.rst | 9 + doc/changelog/05-deprecated/150-early-lia.rst | 23 + doc/stdlib/depends.dot | 28 +- doc/stdlib/hidden-files | 9 +- doc/stdlib/index-list.html.template | 227 ++- test-suite/bugs/bug_15043.v | 8 +- test-suite/bugs/bug_4187.v | 3 +- test-suite/bugs/bug_4456.v | 9 +- test-suite/output/MExtraction.out | 1586 ++++++++--------- theories/All/All.v | 1 + theories/Arith/Compare.v | 4 +- theories/Logic/ChoiceFacts.v | 2 - theories/Make.compat | 2 + theories/{Make.zarith-base => Make.integers} | 41 +- theories/Make.lia | 2 +- theories/Make.narith-base | 10 - theories/{Make.arith-base => Make.naturals} | 0 theories/Make.positive | 9 - theories/Make.ring | 4 - theories/Make.zarith | 22 + theories/Numbers/Cyclic/Int63/Sint63.v | 2 +- theories/Numbers/DecimalFacts.v | 7 +- theories/Numbers/DecimalN.v | 2 +- theories/Numbers/DecimalNat.v | 8 +- theories/Numbers/DecimalPos.v | 13 +- theories/Numbers/DecimalZ.v | 6 +- theories/Numbers/HexadecimalFacts.v | 7 +- theories/Numbers/HexadecimalN.v | 2 +- theories/Numbers/HexadecimalNat.v | 8 +- theories/Numbers/HexadecimalPos.v | 13 +- theories/Numbers/HexadecimalZ.v | 6 +- theories/QArith/Qround.v | 2 +- theories/Strings/BinaryString.v | 5 +- theories/Strings/HexString.v | 5 +- theories/Strings/OctalString.v | 5 +- theories/Strings/String.v | 3 +- theories/ZArith/BinInt.v | 9 + theories/ZArith/ZArith_dec.v | 1 - theories/ZArith/ZModOffset.v | 4 +- theories/ZArith/Zbitwise.v | 2 +- theories/ZArith/Zcong.v | 12 +- theories/ZArith/Zdiv.v | 28 +- theories/ZArith/Zdiv_facts.v | 4 +- theories/ZArith/Zpow_def.v | 1 + theories/ZArith/Zquot.v | 2 +- theories/ZArith/auxiliary.v | 5 - theories/Zmod/Bits.v | 16 +- theories/Zmod/ZmodBase.v | 14 +- theories/Zmod/ZstarBase.v | 6 +- theories/extraction/ExtrHaskellNatInt.v | 1 - theories/extraction/ExtrHaskellNatInteger.v | 1 - theories/extraction/ExtrHaskellNatNum.v | 2 +- theories/extraction/ExtrHaskellZInt.v | 2 +- theories/extraction/ExtrHaskellZInteger.v | 2 +- theories/extraction/ExtrHaskellZNum.v | 2 +- theories/extraction/ExtrOcamlIntConv.v | 2 +- theories/extraction/ExtrOcamlNatBigInt.v | 2 +- theories/extraction/ExtrOcamlNatInt.v | 2 +- theories/extraction/ExtrOcamlZBigInt.v | 2 +- theories/extraction/ExtrOcamlZInt.v | 2 +- theories/micromega/Lia.v | 5 +- theories/micromega/RingMicromega.v | 2 +- theories/micromega/SatDivMod.v | 42 + theories/micromega/ZMicromega.v | 770 +++----- theories/micromega/ZifyInst.v | 10 +- theories/micromega/ZifyN.v | 25 +- theories/micromega/ZifyNat.v | 26 +- theories/omega/PreOmega.v | 2 +- theories/setoid_ring/Field_tac.v | 4 +- theories/setoid_ring/Field_theory.v | 15 +- theories/setoid_ring/ZArithRing.v | 12 +- 74 files changed, 1455 insertions(+), 1723 deletions(-) create mode 100644 doc/changelog/01-changed/150-early-lia.rst create mode 100644 doc/changelog/02-added/150-early-lia.rst create mode 100644 doc/changelog/04-removed/150-early-lia.rst create mode 100644 doc/changelog/05-deprecated/150-early-lia.rst rename theories/{Make.zarith-base => Make.integers} (57%) delete mode 100644 theories/Make.narith-base rename theories/{Make.arith-base => Make.naturals} (100%) delete mode 100644 theories/Make.positive create mode 100644 theories/micromega/SatDivMod.v diff --git a/.nix/rocq-overlays/stdlib-subcomponents/default.nix b/.nix/rocq-overlays/stdlib-subcomponents/default.nix index 907c7fc270..a5904ba1aa 100644 --- a/.nix/rocq-overlays/stdlib-subcomponents/default.nix +++ b/.nix/rocq-overlays/stdlib-subcomponents/default.nix @@ -14,23 +14,21 @@ let "classes" = [ "program" "relations" ]; "bool" = [ "classes" ]; "structures" = [ "bool" ]; - "arith-base" = [ "structures" ]; - "positive" = [ "arith-base" ]; + "naturals" = [ "structures" ]; "narith" = [ "ring" ]; - "zarith-base" = [ "narith-base" ]; - "narith-base" = [ "positive" ]; - "lists" = [ "arith-base" ]; - "ring" = [ "zarith-base" "lists" ]; + "integers" = [ "naturals" ]; + "lists" = [ "naturals" ]; + "ring" = [ "integers" "lists" ]; "arith" = [ "ring" ]; - "strings" = [ "arith" ]; - "lia" = [ "arith" "narith" ]; + "strings" = [ "integers" "lists" ]; + "lia" = [ "ring" ]; "zarith" = [ "lia" ]; "zmod" = [ "zarith" "sorting" "field" ]; - "qarith-base" = [ "ring" ]; - "field" = [ "zarith" ]; + "qarith-base" = [ "zarith" ]; + "field" = [ "ring" ]; "lqa" = [ "field" "qarith-base" ]; "qarith" = [ "lqa" ]; - "classical-logic" = [ "arith" ]; + "classical-logic" = [ "naturals" ]; "sets" = [ "classical-logic" ]; "vectors" = [ "lists" ]; "sorting" = [ "lia" "sets" ]; @@ -41,12 +39,12 @@ let "primitive-array" = [ "primitive-int" ]; "primitive-string" = [ "primitive-int" "orders-ex" ]; "reals" = [ "qarith" "classical-logic" "vectors" ]; - "fmaps-fsets-msets" = [ "orders-ex" "zarith" ]; - "extraction" = [ "primitive-string" "primitive-array" "primitive-floats" ]; - "funind" = [ "arith-base" ]; + "fmaps-fsets-msets" = [ "orders-ex" "zarith" "arith" ]; + "extraction" = [ "zarith" "primitive-string" "primitive-array" "primitive-floats" ]; + "funind" = [ "naturals" ]; "wellfounded" = [ "lists" ]; "streams" = [ "logic" ]; - "rtauto" = [ "positive" "lists" ]; + "rtauto" = [ "integers" "lists" ]; "compat" = [ "rtauto" "fmaps-fsets-msets" "funind" "extraction" "reals" "zmod" "wellfounded" "streams" ]; "all" = [ "compat" ]; }; diff --git a/doc/changelog/01-changed/150-early-lia.rst b/doc/changelog/01-changed/150-early-lia.rst new file mode 100644 index 0000000000..cd0bed6a6c --- /dev/null +++ b/doc/changelog/01-changed/150-early-lia.rst @@ -0,0 +1,8 @@ +- Internal dependencies between about 50 stdlib files + + + To diagnose a failing qualified reference use + `From Stdlib Require All. Locate My.Qualified.reference.` + Then add a Require command for the appropriately granular containing file + (`#150 `_, + by Andres Erbsen). + diff --git a/doc/changelog/02-added/150-early-lia.rst b/doc/changelog/02-added/150-early-lia.rst new file mode 100644 index 0000000000..b947179a36 --- /dev/null +++ b/doc/changelog/02-added/150-early-lia.rst @@ -0,0 +1,12 @@ +- in `ZArithRing` + + + Added `Zpower_theory` to replace the now-deprecated one in `Zpow_def` + (`#150 `_, + by Andres Erbsen). + +- in `BinInt` + + + Added lemmas `div_eucl_0_r`, `mod_0_r`, `div_0_r` + (`#150 `_, + by Andres Erbsen). + diff --git a/doc/changelog/04-removed/150-early-lia.rst b/doc/changelog/04-removed/150-early-lia.rst new file mode 100644 index 0000000000..1679901de2 --- /dev/null +++ b/doc/changelog/04-removed/150-early-lia.rst @@ -0,0 +1,9 @@ +- in `ZMicromega` + + + Support for `EnumProof`s in `ZChecker`. + The `lia` plugin does not generate such proofs anymore. + If you have a different certificate generator that targets the same + checker, please open an issue + (`#150 `_, + by Andres Erbsen). + diff --git a/doc/changelog/05-deprecated/150-early-lia.rst b/doc/changelog/05-deprecated/150-early-lia.rst new file mode 100644 index 0000000000..33d1f3908e --- /dev/null +++ b/doc/changelog/05-deprecated/150-early-lia.rst @@ -0,0 +1,23 @@ +- in `ZMicromega` + + + Internal tactics `flatten_bool` and `inv`, definitions `EnumProof`, `isZ0`, + `bdepth`, `vars`, and lemmas `eq_le_iff`, `isZ0_0`, `isZ0_0`, `isZ0_n0`, + `isZ0_n0`, `eq_true_iff_eq`, `max_var_le`, `max_var_correct`, + `max_var_nformulae_correct_aux`, `max_var_nformalae_correct`, + `ltof_bdepth_split_l`, `ltof_bdepth_split_r` + (`#150 `_, + by Andres Erbsen). + +- in `ZMicromega` + + + Misplaced lemma `Zpower_theory`, with replacement in `ZArithRing` + (`#150 `_, + by Andres Erbsen). + +- in `Div` + + + Lemmas `Zmod_0_r` and `Zdiv_0_r` in favor of `BinInt.Z.mod_0_r` and + `BinInt.Z.div_0_r` + (`#150 `_, + by Andres Erbsen). + diff --git a/doc/stdlib/depends.dot b/doc/stdlib/depends.dot index bc634f8962..f1b0f9ccb9 100644 --- a/doc/stdlib/depends.dot +++ b/doc/stdlib/depends.dot @@ -12,31 +12,31 @@ digraph stdlib_deps { classes -> relations; program -> "corelib-wrapper"; program -> logic; - strings -> arith; + strings -> integers; + strings -> lists; reals -> qarith; reals -> vectors; reals -> "classical-logic"; - "arith-base" -> structures; + naturals -> structures; + integers -> naturals; zarith -> lia; zmod -> zarith; zmod -> sorting; zmod -> field; qarith -> lqa; - positive -> "arith-base"; narith -> ring; ring -> lists; - ring -> "zarith-base"; + ring -> integers; arith -> ring; structures -> bool; - "narith-base" -> positive; - lists -> "arith-base"; - "zarith-base" -> "narith-base"; + lists -> naturals; "primitive-int" -> zarith; "primitive-int" -> unicode; - lia -> narith; - lia -> arith; + lia -> ring; "fmaps-fsets-msets" -> zarith; + "fmaps-fsets-msets" -> arith; "fmaps-fsets-msets" -> "orders-ex"; + "orders-ex" -> narith; "orders-ex" -> strings; "orders-ex" -> sorting; sets -> "classical-logic"; @@ -48,22 +48,22 @@ digraph stdlib_deps { "primitive-string" -> "primitive-int"; "primitive-string" -> "orders-ex"; vectors -> lists; - field -> zarith; + field -> ring; lqa -> field; lqa -> "qarith-base"; - "qarith-base" -> ring; - "classical-logic" -> arith; + "qarith-base" -> zarith; + "classical-logic" -> naturals; + extraction -> "zarith"; extraction -> "primitive-string"; extraction -> "primitive-floats"; extraction -> "primitive-array"; "primitive-array" -> "primitive-int"; streams -> logic; - funind -> "arith-base"; + funind -> naturals; compat -> zmod; compat -> reals; compat -> "fmaps-fsets-msets"; compat -> wellfounded; - compat -> "primitive-string"; compat -> extraction; compat -> streams; compat -> funind; diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index 125d78c26f..6deb34c1f5 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -33,8 +33,6 @@ theories/micromega/Env.v theories/micromega/EnvRing.v theories/micromega/Fourier.v theories/micromega/Fourier_util.v -theories/micromega/Lia.v -theories/micromega/Lqa.v theories/micromega/Lra.v theories/micromega/OrderedRing.v theories/micromega/Psatz.v @@ -51,8 +49,7 @@ theories/micromega/ZifyInst.v theories/micromega/ZifyBool.v theories/micromega/ZifyUint63.v theories/micromega/ZifySint63.v -theories/micromega/ZifyNat.v -theories/micromega/ZifyN.v +theories/micromega/SatDivMod.v theories/micromega/ZifyComparison.v theories/micromega/ZifyClasses.v theories/micromega/ZifyPow.v @@ -66,7 +63,6 @@ theories/setoid_ring/Algebra_syntax.v theories/setoid_ring/ArithRing.v theories/setoid_ring/BinList.v theories/setoid_ring/Cring.v -theories/setoid_ring/Field.v theories/setoid_ring/Field_tac.v theories/setoid_ring/Field_theory.v theories/setoid_ring/InitialRing.v @@ -77,7 +73,6 @@ theories/setoid_ring/Ncring_initial.v theories/setoid_ring/Ncring_polynom.v theories/setoid_ring/Ncring_tac.v theories/setoid_ring/RealField.v -theories/setoid_ring/Ring.v theories/setoid_ring/Ring_base.v theories/setoid_ring/Ring_polynom.v theories/setoid_ring/Ring_tac.v @@ -163,3 +158,5 @@ theories/ssr/ssrfun.v theories/ssr/ssrsetoid.v theories/ssr/ssrunder.v theories/ssrmatching/ssrmatching.v +theories/NArith/NArith_base.v +theories/ZArith/ZArith_base.v diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 0a844101c0..c83587818d 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -96,11 +96,8 @@ through the From Stdlib Require Import command.

theories/Structures/GenericMinMax.v -
Arith-base: - Basic Peano Arithmetic. - Everything can be loaded with From Stdlib Require Import Arith_base. - To enjoy the ring and lia automatic tactic, you additionally need to load - arith below, using From Stdlib Require Import Arith Lia. +
Natural Numbers: + Definitions and basic theory of Peano Arithmetic.
theories/Arith/PeanoNat.v @@ -175,27 +172,15 @@ through the From Stdlib Require Import command.

theories/Streams/StreamMemo.v
-
PArith: - Binary representation of positive integers for effective computation. - You may also want narith and zarith below for N and Z - built on top of positive. -
-
- theories/Numbers/AltBinNotations.v - theories/PArith/BinPosDef.v - theories/PArith/BinPos.v - theories/PArith/Pnat.v - theories/PArith/POrderedType.v - (theories/PArith/PArith.v) -
- -
NArith-base: - Binary natural numbers. - Everything can be loaded with From Stdlib Require Import NArith_base. - To enjoy the ring automatic tactic, you need to load - narith below, using From Stdlib Require Import NArith. +
Integers: + Integers: binary constructions (including natural and positive numbers) and basic properties. + Look at ZArith below for more theory with the ring + and lia tactics.
+ theories/ZArith/BinIntDef.v + theories/ZArith/BinInt.v + theories/ZArith/Znat.v theories/NArith/BinNatDef.v theories/NArith/BinNat.v theories/NArith/Nnat.v @@ -203,20 +188,11 @@ through the From Stdlib Require Import command.

theories/NArith/Ndiv_def.v theories/NArith/Ngcd_def.v theories/NArith/Nsqrt_def.v - (theories/NArith/NArith_base.v) -
- -
NArith: - Binary natural numbers -
-
- (theories/NArith/NArith.v) -
- -
ZArith-base: - Basic binary integers -
-
+ theories/PArith/BinPosDef.v + theories/PArith/BinPos.v + theories/PArith/Pnat.v + theories/PArith/POrderedType.v + (theories/PArith/PArith.v) theories/Numbers/Integer/Abstract/ZAdd.v theories/Numbers/Integer/Abstract/ZAddOrder.v theories/Numbers/Integer/Abstract/ZAxioms.v @@ -234,69 +210,61 @@ through the From Stdlib Require Import command.

theories/Numbers/Integer/Abstract/ZProperties.v theories/Numbers/Integer/Abstract/ZDivFloor.v theories/Numbers/Integer/Abstract/ZDivTrunc.v - theories/ZArith/BinIntDef.v - theories/ZArith/BinInt.v - theories/ZArith/Zorder.v - theories/ZArith/Zcompare.v - theories/ZArith/Znat.v - theories/ZArith/Zmin.v - theories/ZArith/Zmax.v - theories/ZArith/Zminmax.v - theories/ZArith/Zabs.v - theories/ZArith/Zeven.v - theories/ZArith/auxiliary.v - theories/ZArith/ZArith_dec.v - theories/ZArith/Zbool.v - theories/ZArith/Zmisc.v - theories/ZArith/Wf_Z.v - theories/ZArith/Zhints.v - (theories/ZArith/ZArith_base.v) - theories/ZArith/Zpow_alt.v - theories/ZArith/Int.v
Ring: Ring tactic.
- theories/ZArith/Zcomplements.v - theories/ZArith/Zpow_def.v - theories/ZArith/Zdiv.v - theories/ZArith/Znumtheory.v - theories/ZArith/Zdivisibility.v - theories/ZArith/Zcong.v + theories/setoid_ring/Ring.v
-
Arith: - Basic Peano arithmetic +
Linear Integer Arithmetic: + Decision procedure and reductons to it: + From Stdlib Require Import Lia.
- (theories/Arith/Arith.v) + theories/micromega/Lia.v + theories/micromega/ZifyNat.v + theories/micromega/ZifyN.v
ZArith: - Binary encoding of integers. - This binary encoding was initially developped to enable effective - computations, compared to the unary encoding of nat. Proofs were then added - making the types usable for mathematical proofs, although this was not - the initial intent. If even-more efficient computations are needed, look - at the primitive-int package below for 63 bits machine arithmetic - or the coq-bignums package for arbitrary precision machine arithmetic. - Everything can be imported with From Stdlib Require Import ZArith. - Also contains the migromega tactic that can be loaded with - From Stdlib Require Import Lia. + Proofs about integers, including arithmetic and basic number-theoretic properties. + Commonly used modules can be imported with From Stdlib Require Import ZArith.
- theories/ZArith/Zpower.v - theories/ZArith/Zquot.v (theories/ZArith/ZArith.v) + theories/ZArith/Int.v + theories/ZArith/Wf_Z.v + theories/ZArith/ZArith_dec.v + theories/ZArith/ZModOffset.v + theories/ZArith/Zabs.v + theories/ZArith/Zbitwise.v + theories/ZArith/Zbool.v + theories/ZArith/Zcompare.v + theories/ZArith/Zcomplements.v + theories/ZArith/Zcong.v + theories/ZArith/Zdiv.v + theories/ZArith/Zdiv_facts.v + theories/ZArith/Zdivisibility.v + theories/ZArith/Zeven.v theories/ZArith/Zgcd_alt.v theories/ZArith/Zwf.v + theories/ZArith/Zhints.v + theories/ZArith/Zmax.v + theories/ZArith/Zmin.v + theories/ZArith/Zminmax.v + theories/ZArith/Zmisc.v + theories/ZArith/Znumtheory.v + theories/ZArith/Zorder.v + theories/ZArith/Zpow_alt.v + theories/ZArith/Zpow_def.v theories/ZArith/Zpow_facts.v - theories/ZArith/Zdiv_facts.v - theories/ZArith/Zbitwise.v - theories/ZArith/ZModOffset.v + theories/ZArith/Zpower.v + theories/ZArith/Zquot.v theories/ZArith/ZNsatz.v + theories/ZArith/auxiliary.v theories/Numbers/DecimalFacts.v theories/Numbers/DecimalNat.v theories/Numbers/DecimalPos.v @@ -309,6 +277,13 @@ through the From Stdlib Require Import command.

theories/Numbers/HexadecimalZ.v
+
Field: + Field tactic. +
+ theories/setoid_ring/Field.v +
+
+
Zmod and Zstar: Modular arithmetic -- integers modulo another integer -- including machine words (bitvectors) and the multiplicative group of integers modulo another @@ -325,6 +300,46 @@ through the From Stdlib Require Import command.

(theories/Zmod/ZmodInv.v) +
QArith-base: + Early development of binary rational numbers leading up to lqa. + Look at QArith below for more functionalities with the field + and lqa tactics. +
+
+ theories/QArith/QArith_base.v + theories/QArith/Qreduction.v + theories/QArith/QOrderedType.v + theories/QArith/Qminmax.v +
+ +
Linear Rational Arithmetic: + Decision procedure +
+ theories/micromega/Lqa.v +
+
+ +
QArith: + Rational numbers, including canonical (Qc) and non-canonical (Q) + constructions on top of binary Integers as well as + basic theory. Alternative definitions are available in coq-mathcomp-algebra + (unary rat and theory) or coq-bignums (machine-integer construction) and + coq-coqeal (refinements linking both). +
+
+ theories/QArith/QArith.v + theories/QArith/Qabs.v + theories/QArith/Qcabs.v + theories/QArith/Qcanon.v + theories/QArith/Qfield.v + theories/QArith/Qpower.v + theories/QArith/Qring.v + theories/QArith/Qround.v + theories/QArith/QNsatz.v + theories/Numbers/DecimalQ.v + theories/Numbers/HexadecimalQ.v +
+
Unicode: Unicode-based alternative notations
@@ -334,9 +349,10 @@ through the From Stdlib Require Import command.

Primitive Integers: - Interface for hardware integers (63 rather than 64 bits due to OCaml - garbage collector). This enables very efficient arithmetic, for developing - tactics for proofs by reflection for instance. + Interface and axioms for OCaml integers (63 rather than 64 bits due to + OCaml garbage collector). This enables more efficient arithmetic, for + developing tactics for proofs by reflection for instance. The coq-bignums + package implements arbitrary-precision machine arithmetic on top of Uint63.
theories/Numbers/Cyclic/Abstract/CyclicAxioms.v @@ -491,48 +507,18 @@ through the From Stdlib Require Import command.

theories/Strings/PString.v
-
QArith-base: - Basic binary rational numbers. - Look at qarith below for more functionalities with the field - and Lqa tactics. -
-
- theories/QArith/QArith_base.v - theories/QArith/Qreduction.v - theories/QArith/QOrderedType.v - theories/QArith/Qminmax.v -
- -
Field: - Field tactic. +
NArith: + Wrapper for binary natural numbers (from Integers) and the associated (semi)ring tactc.
- theories/QArith/Qpower.v - theories/QArith/Qring.v - theories/QArith/Qfield.v - theories/QArith/Qcanon.v - theories/QArith/Qround.v + (theories/NArith/NArith.v)
-
QArith: - Binary rational numbers, made on top of zarith. - Those enable effective computations in arbitrary precision exact rational - arithmetic. Those rationals are known to be difficult to use for - mathematical proofs because there is no canonical representation - (2/3 and 4/6 are not equal for instance). For even more efficient - computation, look at the coq-bignums package which uses machine integers. - For mathematical proofs, the rat type of the coq-mathcomp-algebra package - are much more comfortable, although they don't enjoy efficient computation - (coq-coqeal offers a refinement with coq-bignums that enables to enjoy - both aspects). +
Arith: + Wrapper for Peano natural numbers (from Naturals) and the associated (semi)ring tactc.
- theories/QArith/Qabs.v - (theories/QArith/QArith.v) - theories/QArith/Qcabs.v - theories/QArith/QNsatz.v - theories/Numbers/DecimalQ.v - theories/Numbers/HexadecimalQ.v + (theories/Arith/Arith.v)
Reals: @@ -716,6 +702,7 @@ through the From Stdlib Require Import command.

theories/Compat/AdmitAxiom.v + theories/Numbers/AltBinNotations.v theories/Compat/Stdlib818.v
diff --git a/test-suite/bugs/bug_15043.v b/test-suite/bugs/bug_15043.v index e68cb597f2..324c270814 100644 --- a/test-suite/bugs/bug_15043.v +++ b/test-suite/bugs/bug_15043.v @@ -9,16 +9,12 @@ Abort. End ShortExample. + Module OriginalReport. Axiom proof_admitted : False. Tactic Notation "admit" := abstract case proof_admitted. -From Stdlib Require Psatz. -From Stdlib Require Utf8. - -Import Arith. -Import Psatz. -Import Stdlib.Unicode.Utf8. +From Stdlib Require Import Arith Psatz Utf8. Fixpoint log3_iter down_counter log_up_counter up_counter dist_next := match down_counter with diff --git a/test-suite/bugs/bug_4187.v b/test-suite/bugs/bug_4187.v index 58e782f4af..20a2c62e04 100644 --- a/test-suite/bugs/bug_4187.v +++ b/test-suite/bugs/bug_4187.v @@ -7,7 +7,8 @@ Axiom proof_admitted : False. Tactic Notation "admit" := case proof_admitted. From Stdlib Require Import List. From Stdlib Require Import Setoid. -From Stdlib Require Import BinNat. +From Stdlib Require Import BinNat . +From Stdlib Require Compare_dec Wf_nat. From Stdlib Require Import Sumbool. Global Set Implicit Arguments. Global Generalizable All Variables. diff --git a/test-suite/bugs/bug_4456.v b/test-suite/bugs/bug_4456.v index 1560a3c946..5ee7e53ddc 100644 --- a/test-suite/bugs/bug_4456.v +++ b/test-suite/bugs/bug_4456.v @@ -8,13 +8,10 @@ Axiom proof_admitted : False. Tactic Notation "admit" := case proof_admitted. -From Stdlib Require Program. -From Stdlib Require String. -From Stdlib Require Lia. +From Stdlib Require Import Program String Arith Lia List. Module Export Fiat_DOT_Common. Module Export Fiat. Module Common. -Import Stdlib.Lists.List. Export Program. Global Set Implicit Arguments. @@ -110,8 +107,6 @@ Module Export Fiat. Module Export Parsers. Module Export ContextFreeGrammar. Module Export Core. -Import Stdlib.Strings.String. -Import Stdlib.Lists.List. Export Fiat.Parsers.StringLike.Core. Section cfg. @@ -489,8 +484,6 @@ Defined. End app. Import Stdlib.Lists.List. -Import Arith. -Import Lia. Import Fiat_DOT_Common.Fiat.Common. Import Fiat.Parsers.ContextFreeGrammar.Valid. Local Open Scope string_like_scope. diff --git a/test-suite/output/MExtraction.out b/test-suite/output/MExtraction.out index 7a08d63147..a1ab5d3224 100644 --- a/test-suite/output/MExtraction.out +++ b/test-suite/output/MExtraction.out @@ -438,13 +438,6 @@ module N = | S n' -> Npos (Pos.of_succ_nat n') end -(** val pow_pos : ('a1 -> 'a1 -> 'a1) -> 'a1 -> positive -> 'a1 **) - -let rec pow_pos rmul x = function -| XI i0 -> let p = pow_pos rmul x i0 in rmul x (rmul p p) -| XO i0 -> let p = pow_pos rmul x i0 in rmul p p -| XH -> x - module Z = struct (** val double : z -> z **) @@ -690,752 +683,374 @@ module Z = | Zneg b0 -> Zpos (Coq_Pos.gcd a0 b0)) end -type 'c pExpr = -| PEc of 'c -| PEX of positive -| PEadd of 'c pExpr * 'c pExpr -| PEsub of 'c pExpr * 'c pExpr -| PEmul of 'c pExpr * 'c pExpr -| PEopp of 'c pExpr -| PEpow of 'c pExpr * n +(** val pow_pos0 : ('a1 -> 'a1 -> 'a1) -> 'a1 -> positive -> 'a1 **) -type 'c pol = -| Pc of 'c -| Pinj of positive * 'c pol -| PX of 'c pol * positive * 'c pol +let rec pow_pos0 rmul x = function +| XI i0 -> let p = pow_pos0 rmul x i0 in rmul x (rmul p p) +| XO i0 -> let p = pow_pos0 rmul x i0 in rmul p p +| XH -> x -(** val p0 : 'a1 -> 'a1 pol **) +type kind = +| IsProp +| IsBool -let p0 cO = - Pc cO +type 'a trace = +| Null +| Push of 'a * 'a trace +| Merge of 'a trace * 'a trace -(** val p1 : 'a1 -> 'a1 pol **) +type ('tA, 'tX, 'aA, 'aF) gFormula = +| TT of kind +| FF of kind +| X of kind * 'tX +| A of kind * 'tA * 'aA +| AND of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula +| OR of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula +| NOT of kind * ('tA, 'tX, 'aA, 'aF) gFormula +| IMPL of kind * ('tA, 'tX, 'aA, 'aF) gFormula * 'aF option + * ('tA, 'tX, 'aA, 'aF) gFormula +| IFF of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula +| EQ of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula -let p1 cI = - Pc cI +(** val mapX : + (kind -> 'a2 -> 'a2) -> kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> ('a1, + 'a2, 'a3, 'a4) gFormula **) -(** val peq : ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> bool **) +let rec mapX f _ = function +| X (k0, x) -> X (k0, (f k0 x)) +| AND (k0, f1, f2) -> AND (k0, (mapX f k0 f1), (mapX f k0 f2)) +| OR (k0, f1, f2) -> OR (k0, (mapX f k0 f1), (mapX f k0 f2)) +| NOT (k0, f1) -> NOT (k0, (mapX f k0 f1)) +| IMPL (k0, f1, o, f2) -> IMPL (k0, (mapX f k0 f1), o, (mapX f k0 f2)) +| IFF (k0, f1, f2) -> IFF (k0, (mapX f k0 f1), (mapX f k0 f2)) +| EQ (f1, f2) -> EQ ((mapX f IsBool f1), (mapX f IsBool f2)) +| x -> x -let rec peq ceqb p p' = - match p with - | Pc c -> (match p' with - | Pc c' -> ceqb c c' - | _ -> false) - | Pinj (j, q0) -> - (match p' with - | Pinj (j', q') -> - (match Coq_Pos.compare j j' with - | Eq -> peq ceqb q0 q' - | _ -> false) - | _ -> false) - | PX (p2, i, q0) -> - (match p' with - | PX (p'0, i', q') -> - (match Coq_Pos.compare i i' with - | Eq -> if peq ceqb p2 p'0 then peq ceqb q0 q' else false - | _ -> false) - | _ -> false) +(** val foldA : + ('a5 -> 'a3 -> 'a5) -> kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a5 -> 'a5 **) -(** val mkPinj : positive -> 'a1 pol -> 'a1 pol **) +let rec foldA f _ f0 acc = + match f0 with + | A (_, _, an) -> f acc an + | AND (k0, f1, f2) -> foldA f k0 f1 (foldA f k0 f2 acc) + | OR (k0, f1, f2) -> foldA f k0 f1 (foldA f k0 f2 acc) + | NOT (k0, f1) -> foldA f k0 f1 acc + | IMPL (k0, f1, _, f2) -> foldA f k0 f1 (foldA f k0 f2 acc) + | IFF (k0, f1, f2) -> foldA f k0 f1 (foldA f k0 f2 acc) + | EQ (f1, f2) -> foldA f IsBool f1 (foldA f IsBool f2 acc) + | _ -> acc -let mkPinj j p = match p with -| Pc _ -> p -| Pinj (j', q0) -> Pinj ((Coq_Pos.add j j'), q0) -| PX (_, _, _) -> Pinj (j, p) +(** val cons_id : 'a1 option -> 'a1 list -> 'a1 list **) -(** val mkPinj_pred : positive -> 'a1 pol -> 'a1 pol **) +let cons_id id l = + match id with + | Some id0 -> id0::l + | None -> l -let mkPinj_pred j p = - match j with - | XI j0 -> Pinj ((XO j0), p) - | XO j0 -> Pinj ((Coq_Pos.pred_double j0), p) - | XH -> p +(** val ids_of_formula : kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a4 list **) -(** val mkPX : - 'a1 -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **) +let rec ids_of_formula _ = function +| IMPL (k0, _, id, f') -> cons_id id (ids_of_formula k0 f') +| _ -> [] -let mkPX cO ceqb p i q0 = - match p with - | Pc c -> if ceqb c cO then mkPinj XH q0 else PX (p, i, q0) - | Pinj (_, _) -> PX (p, i, q0) - | PX (p', i', q') -> - if peq ceqb q' (p0 cO) - then PX (p', (Coq_Pos.add i' i), q0) - else PX (p, i, q0) +(** val collect_annot : kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a3 list **) -(** val mkXi : 'a1 -> 'a1 -> positive -> 'a1 pol **) +let rec collect_annot _ = function +| A (_, _, a) -> a::[] +| AND (k0, f1, f2) -> app (collect_annot k0 f1) (collect_annot k0 f2) +| OR (k0, f1, f2) -> app (collect_annot k0 f1) (collect_annot k0 f2) +| NOT (k0, f0) -> collect_annot k0 f0 +| IMPL (k0, f1, _, f2) -> app (collect_annot k0 f1) (collect_annot k0 f2) +| IFF (k0, f1, f2) -> app (collect_annot k0 f1) (collect_annot k0 f2) +| EQ (f1, f2) -> app (collect_annot IsBool f1) (collect_annot IsBool f2) +| _ -> [] -let mkXi cO cI i = - PX ((p1 cI), i, (p0 cO)) +type rtyp = __ -(** val mkX : 'a1 -> 'a1 -> 'a1 pol **) +type eKind = __ -let mkX cO cI = - mkXi cO cI XH +type 'a bFormula = ('a, eKind, unit0, unit0) gFormula -(** val popp : ('a1 -> 'a1) -> 'a1 pol -> 'a1 pol **) +(** val map_bformula : + kind -> ('a1 -> 'a2) -> ('a1, 'a3, 'a4, 'a5) gFormula -> ('a2, 'a3, 'a4, + 'a5) gFormula **) -let rec popp copp = function -| Pc c -> Pc (copp c) -| Pinj (j, q0) -> Pinj (j, (popp copp q0)) -| PX (p2, i, q0) -> PX ((popp copp p2), i, (popp copp q0)) +let rec map_bformula _ fct = function +| TT k -> TT k +| FF k -> FF k +| X (k, p) -> X (k, p) +| A (k, a, t0) -> A (k, (fct a), t0) +| AND (k0, f1, f2) -> + AND (k0, (map_bformula k0 fct f1), (map_bformula k0 fct f2)) +| OR (k0, f1, f2) -> + OR (k0, (map_bformula k0 fct f1), (map_bformula k0 fct f2)) +| NOT (k0, f0) -> NOT (k0, (map_bformula k0 fct f0)) +| IMPL (k0, f1, a, f2) -> + IMPL (k0, (map_bformula k0 fct f1), a, (map_bformula k0 fct f2)) +| IFF (k0, f1, f2) -> + IFF (k0, (map_bformula k0 fct f1), (map_bformula k0 fct f2)) +| EQ (f1, f2) -> + EQ ((map_bformula IsBool fct f1), (map_bformula IsBool fct f2)) -(** val paddC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol **) +type ('x, 'annot) clause = ('x * 'annot) list -let rec paddC cadd p c = - match p with - | Pc c1 -> Pc (cadd c1 c) - | Pinj (j, q0) -> Pinj (j, (paddC cadd q0 c)) - | PX (p2, i, q0) -> PX (p2, i, (paddC cadd q0 c)) +type ('x, 'annot) cnf = ('x, 'annot) clause list -(** val psubC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol **) +(** val cnf_tt : ('a1, 'a2) cnf **) -let rec psubC csub p c = - match p with - | Pc c1 -> Pc (csub c1 c) - | Pinj (j, q0) -> Pinj (j, (psubC csub q0 c)) - | PX (p2, i, q0) -> PX (p2, i, (psubC csub q0 c)) +let cnf_tt = + [] -(** val paddI : - ('a1 -> 'a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> - positive -> 'a1 pol -> 'a1 pol **) +(** val cnf_ff : ('a1, 'a2) cnf **) -let rec paddI cadd pop q0 j = function -| Pc c -> mkPinj j (paddC cadd q0 c) -| Pinj (j', q') -> - (match Z.pos_sub j' j with - | Z0 -> mkPinj j (pop q' q0) - | Zpos k -> mkPinj j (pop (Pinj (k, q')) q0) - | Zneg k -> mkPinj j' (paddI cadd pop q0 k q')) -| PX (p2, i, q') -> - (match j with - | XI j0 -> PX (p2, i, (paddI cadd pop q0 (XO j0) q')) - | XO j0 -> PX (p2, i, (paddI cadd pop q0 (Coq_Pos.pred_double j0) q')) - | XH -> PX (p2, i, (pop q' q0))) +let cnf_ff = + []::[] -(** val psubI : - ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> - 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **) +(** val add_term : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) + clause -> ('a1, 'a2) clause option **) -let rec psubI cadd copp pop q0 j = function -| Pc c -> mkPinj j (paddC cadd (popp copp q0) c) -| Pinj (j', q') -> - (match Z.pos_sub j' j with - | Z0 -> mkPinj j (pop q' q0) - | Zpos k -> mkPinj j (pop (Pinj (k, q')) q0) - | Zneg k -> mkPinj j' (psubI cadd copp pop q0 k q')) -| PX (p2, i, q') -> - (match j with - | XI j0 -> PX (p2, i, (psubI cadd copp pop q0 (XO j0) q')) - | XO j0 -> PX (p2, i, (psubI cadd copp pop q0 (Coq_Pos.pred_double j0) q')) - | XH -> PX (p2, i, (pop q' q0))) +let rec add_term unsat deduce t0 = function +| [] -> + (match deduce (fst t0) (fst t0) with + | Some u -> if unsat u then None else Some (t0::[]) + | None -> Some (t0::[])) +| t'::cl0 -> + (match deduce (fst t0) (fst t') with + | Some u -> + if unsat u + then None + else (match add_term unsat deduce t0 cl0 with + | Some cl' -> Some (t'::cl') + | None -> None) + | None -> + (match add_term unsat deduce t0 cl0 with + | Some cl' -> Some (t'::cl') + | None -> None)) -(** val paddX : - 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol - -> positive -> 'a1 pol -> 'a1 pol **) +(** val or_clause : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, + 'a2) clause -> ('a1, 'a2) clause option **) -let rec paddX cO ceqb pop p' i' p = match p with -| Pc _ -> PX (p', i', p) -| Pinj (j, q') -> - (match j with - | XI j0 -> PX (p', i', (Pinj ((XO j0), q'))) - | XO j0 -> PX (p', i', (Pinj ((Coq_Pos.pred_double j0), q'))) - | XH -> PX (p', i', q')) -| PX (p2, i, q') -> - (match Z.pos_sub i i' with - | Z0 -> mkPX cO ceqb (pop p2 p') i q' - | Zpos k -> mkPX cO ceqb (pop (PX (p2, k, (p0 cO))) p') i' q' - | Zneg k -> mkPX cO ceqb (paddX cO ceqb pop p' k p2) i q') +let rec or_clause unsat deduce cl1 cl2 = + match cl1 with + | [] -> Some cl2 + | t0::cl -> + (match add_term unsat deduce t0 cl2 with + | Some cl' -> or_clause unsat deduce cl cl' + | None -> None) -(** val psubX : - 'a1 -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 - pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **) +(** val xor_clause_cnf : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, + 'a2) cnf -> ('a1, 'a2) cnf **) -let rec psubX cO copp ceqb pop p' i' p = match p with -| Pc _ -> PX ((popp copp p'), i', p) -| Pinj (j, q') -> - (match j with - | XI j0 -> PX ((popp copp p'), i', (Pinj ((XO j0), q'))) - | XO j0 -> PX ((popp copp p'), i', (Pinj ((Coq_Pos.pred_double j0), q'))) - | XH -> PX ((popp copp p'), i', q')) -| PX (p2, i, q') -> - (match Z.pos_sub i i' with - | Z0 -> mkPX cO ceqb (pop p2 p') i q' - | Zpos k -> mkPX cO ceqb (pop (PX (p2, k, (p0 cO))) p') i' q' - | Zneg k -> mkPX cO ceqb (psubX cO copp ceqb pop p' k p2) i q') +let xor_clause_cnf unsat deduce t0 f = + fold_left (fun acc e -> + match or_clause unsat deduce t0 e with + | Some cl -> cl::acc + | None -> acc) f [] -(** val padd : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol - -> 'a1 pol **) +(** val or_clause_cnf : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, + 'a2) cnf -> ('a1, 'a2) cnf **) -let rec padd cO cadd ceqb p = function -| Pc c' -> paddC cadd p c' -| Pinj (j', q') -> paddI cadd (padd cO cadd ceqb) q' j' p -| PX (p'0, i', q') -> - (match p with - | Pc c -> PX (p'0, i', (paddC cadd q' c)) - | Pinj (j, q0) -> - (match j with - | XI j0 -> PX (p'0, i', (padd cO cadd ceqb (Pinj ((XO j0), q0)) q')) - | XO j0 -> - PX (p'0, i', - (padd cO cadd ceqb (Pinj ((Coq_Pos.pred_double j0), q0)) q')) - | XH -> PX (p'0, i', (padd cO cadd ceqb q0 q'))) - | PX (p2, i, q0) -> - (match Z.pos_sub i i' with - | Z0 -> - mkPX cO ceqb (padd cO cadd ceqb p2 p'0) i (padd cO cadd ceqb q0 q') - | Zpos k -> - mkPX cO ceqb (padd cO cadd ceqb (PX (p2, k, (p0 cO))) p'0) i' - (padd cO cadd ceqb q0 q') - | Zneg k -> - mkPX cO ceqb (paddX cO ceqb (padd cO cadd ceqb) p'0 k p2) i - (padd cO cadd ceqb q0 q'))) +let or_clause_cnf unsat deduce t0 f = + match t0 with + | [] -> f + | _::_ -> xor_clause_cnf unsat deduce t0 f -(** val psub : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 - -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) +(** val or_cnf : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, + 'a2) cnf -> ('a1, 'a2) cnf **) -let rec psub cO cadd csub copp ceqb p = function -| Pc c' -> psubC csub p c' -| Pinj (j', q') -> psubI cadd copp (psub cO cadd csub copp ceqb) q' j' p -| PX (p'0, i', q') -> - (match p with - | Pc c -> PX ((popp copp p'0), i', (paddC cadd (popp copp q') c)) - | Pinj (j, q0) -> - (match j with - | XI j0 -> - PX ((popp copp p'0), i', - (psub cO cadd csub copp ceqb (Pinj ((XO j0), q0)) q')) - | XO j0 -> - PX ((popp copp p'0), i', - (psub cO cadd csub copp ceqb (Pinj ((Coq_Pos.pred_double j0), q0)) - q')) - | XH -> PX ((popp copp p'0), i', (psub cO cadd csub copp ceqb q0 q'))) - | PX (p2, i, q0) -> - (match Z.pos_sub i i' with - | Z0 -> - mkPX cO ceqb (psub cO cadd csub copp ceqb p2 p'0) i - (psub cO cadd csub copp ceqb q0 q') - | Zpos k -> - mkPX cO ceqb (psub cO cadd csub copp ceqb (PX (p2, k, (p0 cO))) p'0) - i' (psub cO cadd csub copp ceqb q0 q') - | Zneg k -> - mkPX cO ceqb - (psubX cO copp ceqb (psub cO cadd csub copp ceqb) p'0 k p2) i - (psub cO cadd csub copp ceqb q0 q'))) +let rec or_cnf unsat deduce f f' = + match f with + | [] -> cnf_tt + | e::rst -> + rev_append (or_cnf unsat deduce rst f') (or_clause_cnf unsat deduce e f') -(** val pmulC_aux : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> - 'a1 pol **) +(** val and_cnf : ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf **) -let rec pmulC_aux cO cmul ceqb p c = - match p with - | Pc c' -> Pc (cmul c' c) - | Pinj (j, q0) -> mkPinj j (pmulC_aux cO cmul ceqb q0 c) - | PX (p2, i, q0) -> - mkPX cO ceqb (pmulC_aux cO cmul ceqb p2 c) i (pmulC_aux cO cmul ceqb q0 c) +let and_cnf = + rev_append -(** val pmulC : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> - 'a1 -> 'a1 pol **) +type ('term, 'annot, 'tX, 'aF) tFormula = ('term, 'tX, 'annot, 'aF) gFormula -let pmulC cO cI cmul ceqb p c = - if ceqb c cO - then p0 cO - else if ceqb c cI then p else pmulC_aux cO cmul ceqb p c +(** val is_cnf_tt : ('a1, 'a2) cnf -> bool **) -(** val pmulI : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> - 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **) +let is_cnf_tt = function +| [] -> true +| _::_ -> false -let rec pmulI cO cI cmul ceqb pmul0 q0 j = function -| Pc c -> mkPinj j (pmulC cO cI cmul ceqb q0 c) -| Pinj (j', q') -> - (match Z.pos_sub j' j with - | Z0 -> mkPinj j (pmul0 q' q0) - | Zpos k -> mkPinj j (pmul0 (Pinj (k, q')) q0) - | Zneg k -> mkPinj j' (pmulI cO cI cmul ceqb pmul0 q0 k q')) -| PX (p', i', q') -> - (match j with - | XI j' -> - mkPX cO ceqb (pmulI cO cI cmul ceqb pmul0 q0 j p') i' - (pmulI cO cI cmul ceqb pmul0 q0 (XO j') q') - | XO j' -> - mkPX cO ceqb (pmulI cO cI cmul ceqb pmul0 q0 j p') i' - (pmulI cO cI cmul ceqb pmul0 q0 (Coq_Pos.pred_double j') q') - | XH -> - mkPX cO ceqb (pmulI cO cI cmul ceqb pmul0 q0 XH p') i' (pmul0 q' q0)) +(** val is_cnf_ff : ('a1, 'a2) cnf -> bool **) -(** val pmul : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) +let is_cnf_ff = function +| [] -> false +| c0::l -> + (match c0 with + | [] -> (match l with + | [] -> true + | _::_ -> false) + | _::_ -> false) -let rec pmul cO cI cadd cmul ceqb p p'' = match p'' with -| Pc c -> pmulC cO cI cmul ceqb p c -| Pinj (j', q') -> pmulI cO cI cmul ceqb (pmul cO cI cadd cmul ceqb) q' j' p -| PX (p', i', q') -> - (match p with - | Pc c -> pmulC cO cI cmul ceqb p'' c - | Pinj (j, q0) -> - let qQ' = - match j with - | XI j0 -> pmul cO cI cadd cmul ceqb (Pinj ((XO j0), q0)) q' - | XO j0 -> - pmul cO cI cadd cmul ceqb (Pinj ((Coq_Pos.pred_double j0), q0)) q' - | XH -> pmul cO cI cadd cmul ceqb q0 q' - in - mkPX cO ceqb (pmul cO cI cadd cmul ceqb p p') i' qQ' - | PX (p2, i, q0) -> - let qQ' = pmul cO cI cadd cmul ceqb q0 q' in - let pQ' = pmulI cO cI cmul ceqb (pmul cO cI cadd cmul ceqb) q' XH p2 in - let qP' = pmul cO cI cadd cmul ceqb (mkPinj XH q0) p' in - let pP' = pmul cO cI cadd cmul ceqb p2 p' in - padd cO cadd ceqb - (mkPX cO ceqb (padd cO cadd ceqb (mkPX cO ceqb pP' i (p0 cO)) qP') i' - (p0 cO)) - (mkPX cO ceqb pQ' i qQ')) +(** val and_cnf_opt : ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf **) -(** val psquare : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> bool) -> 'a1 pol -> 'a1 pol **) +let and_cnf_opt f1 f2 = + if if is_cnf_ff f1 then true else is_cnf_ff f2 + then cnf_ff + else if is_cnf_tt f2 then f1 else and_cnf f1 f2 -let rec psquare cO cI cadd cmul ceqb = function -| Pc c -> Pc (cmul c c) -| Pinj (j, q0) -> Pinj (j, (psquare cO cI cadd cmul ceqb q0)) -| PX (p2, i, q0) -> - let twoPQ = - pmul cO cI cadd cmul ceqb p2 - (mkPinj XH (pmulC cO cI cmul ceqb q0 (cadd cI cI))) - in - let q2 = psquare cO cI cadd cmul ceqb q0 in - let p3 = psquare cO cI cadd cmul ceqb p2 in - mkPX cO ceqb (padd cO cadd ceqb (mkPX cO ceqb p3 i (p0 cO)) twoPQ) i q2 +(** val or_cnf_opt : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, + 'a2) cnf -> ('a1, 'a2) cnf **) -(** val mk_X : 'a1 -> 'a1 -> positive -> 'a1 pol **) +let or_cnf_opt unsat deduce f1 f2 = + if if is_cnf_tt f1 then true else is_cnf_tt f2 + then cnf_tt + else if is_cnf_ff f2 then f1 else or_cnf unsat deduce f1 f2 -let mk_X cO cI j = - mkPinj_pred j (mkX cO cI) +(** val mk_and : + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, + 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3, + 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf **) -(** val ppow_pos : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> 'a1 pol -> positive -> 'a1 - pol **) +let mk_and unsat deduce rEC k pol0 f1 f2 = + if pol0 + then and_cnf_opt (rEC pol0 k f1) (rEC pol0 k f2) + else or_cnf_opt unsat deduce (rEC pol0 k f1) (rEC pol0 k f2) -let rec ppow_pos cO cI cadd cmul ceqb subst_l res p = function -| XI p3 -> - subst_l - (pmul cO cI cadd cmul ceqb - (ppow_pos cO cI cadd cmul ceqb subst_l - (ppow_pos cO cI cadd cmul ceqb subst_l res p p3) p p3) - p) -| XO p3 -> - ppow_pos cO cI cadd cmul ceqb subst_l - (ppow_pos cO cI cadd cmul ceqb subst_l res p p3) p p3 -| XH -> subst_l (pmul cO cI cadd cmul ceqb res p) +(** val mk_or : + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, + 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3, + 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf **) -(** val ppow_N : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> n -> 'a1 pol **) +let mk_or unsat deduce rEC k pol0 f1 f2 = + if pol0 + then or_cnf_opt unsat deduce (rEC pol0 k f1) (rEC pol0 k f2) + else and_cnf_opt (rEC pol0 k f1) (rEC pol0 k f2) -let ppow_N cO cI cadd cmul ceqb subst_l p = function -| N0 -> p1 cI -| Npos p2 -> ppow_pos cO cI cadd cmul ceqb subst_l (p1 cI) p p2 +(** val mk_impl : + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, + 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3, + 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf **) -(** val norm_aux : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 - -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol **) +let mk_impl unsat deduce rEC k pol0 f1 f2 = + if pol0 + then or_cnf_opt unsat deduce (rEC (negb pol0) k f1) (rEC pol0 k f2) + else and_cnf_opt (rEC (negb pol0) k f1) (rEC pol0 k f2) -let rec norm_aux cO cI cadd cmul csub copp ceqb = function -| PEc c -> Pc c -| PEX j -> mk_X cO cI j -| PEadd (pe1, pe2) -> - (match pe1 with - | PEopp pe3 -> - psub cO cadd csub copp ceqb - (norm_aux cO cI cadd cmul csub copp ceqb pe2) - (norm_aux cO cI cadd cmul csub copp ceqb pe3) - | _ -> - (match pe2 with - | PEopp pe3 -> - psub cO cadd csub copp ceqb - (norm_aux cO cI cadd cmul csub copp ceqb pe1) - (norm_aux cO cI cadd cmul csub copp ceqb pe3) - | _ -> - padd cO cadd ceqb (norm_aux cO cI cadd cmul csub copp ceqb pe1) - (norm_aux cO cI cadd cmul csub copp ceqb pe2))) -| PEsub (pe1, pe2) -> - psub cO cadd csub copp ceqb (norm_aux cO cI cadd cmul csub copp ceqb pe1) - (norm_aux cO cI cadd cmul csub copp ceqb pe2) -| PEmul (pe1, pe2) -> - pmul cO cI cadd cmul ceqb (norm_aux cO cI cadd cmul csub copp ceqb pe1) - (norm_aux cO cI cadd cmul csub copp ceqb pe2) -| PEopp pe1 -> popp copp (norm_aux cO cI cadd cmul csub copp ceqb pe1) -| PEpow (pe1, n0) -> - ppow_N cO cI cadd cmul ceqb (fun p -> p) - (norm_aux cO cI cadd cmul csub copp ceqb pe1) n0 - -type kind = -| IsProp -| IsBool - -type 'a trace = -| Null -| Push of 'a * 'a trace -| Merge of 'a trace * 'a trace - -type ('tA, 'tX, 'aA, 'aF) gFormula = -| TT of kind -| FF of kind -| X of kind * 'tX -| A of kind * 'tA * 'aA -| AND of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula -| OR of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula -| NOT of kind * ('tA, 'tX, 'aA, 'aF) gFormula -| IMPL of kind * ('tA, 'tX, 'aA, 'aF) gFormula * 'aF option - * ('tA, 'tX, 'aA, 'aF) gFormula -| IFF of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula -| EQ of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula - -(** val mapX : - (kind -> 'a2 -> 'a2) -> kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> ('a1, - 'a2, 'a3, 'a4) gFormula **) - -let rec mapX f _ = function -| X (k0, x) -> X (k0, (f k0 x)) -| AND (k0, f1, f2) -> AND (k0, (mapX f k0 f1), (mapX f k0 f2)) -| OR (k0, f1, f2) -> OR (k0, (mapX f k0 f1), (mapX f k0 f2)) -| NOT (k0, f1) -> NOT (k0, (mapX f k0 f1)) -| IMPL (k0, f1, o, f2) -> IMPL (k0, (mapX f k0 f1), o, (mapX f k0 f2)) -| IFF (k0, f1, f2) -> IFF (k0, (mapX f k0 f1), (mapX f k0 f2)) -| EQ (f1, f2) -> EQ ((mapX f IsBool f1), (mapX f IsBool f2)) -| x -> x - -(** val foldA : - ('a5 -> 'a3 -> 'a5) -> kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a5 -> 'a5 **) - -let rec foldA f _ f0 acc = - match f0 with - | A (_, _, an) -> f acc an - | AND (k0, f1, f2) -> foldA f k0 f1 (foldA f k0 f2 acc) - | OR (k0, f1, f2) -> foldA f k0 f1 (foldA f k0 f2 acc) - | NOT (k0, f1) -> foldA f k0 f1 acc - | IMPL (k0, f1, _, f2) -> foldA f k0 f1 (foldA f k0 f2 acc) - | IFF (k0, f1, f2) -> foldA f k0 f1 (foldA f k0 f2 acc) - | EQ (f1, f2) -> foldA f IsBool f1 (foldA f IsBool f2 acc) - | _ -> acc - -(** val cons_id : 'a1 option -> 'a1 list -> 'a1 list **) - -let cons_id id l = - match id with - | Some id0 -> id0::l - | None -> l - -(** val ids_of_formula : kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a4 list **) - -let rec ids_of_formula _ = function -| IMPL (k0, _, id, f') -> cons_id id (ids_of_formula k0 f') -| _ -> [] - -(** val collect_annot : kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a3 list **) - -let rec collect_annot _ = function -| A (_, _, a) -> a::[] -| AND (k0, f1, f2) -> app (collect_annot k0 f1) (collect_annot k0 f2) -| OR (k0, f1, f2) -> app (collect_annot k0 f1) (collect_annot k0 f2) -| NOT (k0, f0) -> collect_annot k0 f0 -| IMPL (k0, f1, _, f2) -> app (collect_annot k0 f1) (collect_annot k0 f2) -| IFF (k0, f1, f2) -> app (collect_annot k0 f1) (collect_annot k0 f2) -| EQ (f1, f2) -> app (collect_annot IsBool f1) (collect_annot IsBool f2) -| _ -> [] - -type rtyp = __ - -type eKind = __ - -type 'a bFormula = ('a, eKind, unit0, unit0) gFormula - -(** val map_bformula : - kind -> ('a1 -> 'a2) -> ('a1, 'a3, 'a4, 'a5) gFormula -> ('a2, 'a3, 'a4, - 'a5) gFormula **) - -let rec map_bformula _ fct = function -| TT k -> TT k -| FF k -> FF k -| X (k, p) -> X (k, p) -| A (k, a, t0) -> A (k, (fct a), t0) -| AND (k0, f1, f2) -> - AND (k0, (map_bformula k0 fct f1), (map_bformula k0 fct f2)) -| OR (k0, f1, f2) -> - OR (k0, (map_bformula k0 fct f1), (map_bformula k0 fct f2)) -| NOT (k0, f0) -> NOT (k0, (map_bformula k0 fct f0)) -| IMPL (k0, f1, a, f2) -> - IMPL (k0, (map_bformula k0 fct f1), a, (map_bformula k0 fct f2)) -| IFF (k0, f1, f2) -> - IFF (k0, (map_bformula k0 fct f1), (map_bformula k0 fct f2)) -| EQ (f1, f2) -> - EQ ((map_bformula IsBool fct f1), (map_bformula IsBool fct f2)) - -type ('x, 'annot) clause = ('x * 'annot) list +(** val mk_iff : + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, + 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3, + 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf **) -type ('x, 'annot) cnf = ('x, 'annot) clause list +let mk_iff unsat deduce rEC k pol0 f1 f2 = + or_cnf_opt unsat deduce + (and_cnf_opt (rEC (negb pol0) k f1) (rEC false k f2)) + (and_cnf_opt (rEC pol0 k f1) (rEC true k f2)) -(** val cnf_tt : ('a1, 'a2) cnf **) +(** val is_bool : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> bool option **) -let cnf_tt = - [] +let is_bool _ = function +| TT _ -> Some true +| FF _ -> Some false +| _ -> None -(** val cnf_ff : ('a1, 'a2) cnf **) +(** val xcnf : + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) + cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> kind -> ('a1, 'a3, 'a4, + 'a5) tFormula -> ('a2, 'a3) cnf **) -let cnf_ff = - []::[] +let rec xcnf unsat deduce normalise1 negate0 pol0 _ = function +| TT _ -> if pol0 then cnf_tt else cnf_ff +| FF _ -> if pol0 then cnf_ff else cnf_tt +| X (_, _) -> cnf_ff +| A (_, x, t0) -> if pol0 then normalise1 x t0 else negate0 x t0 +| AND (k0, e1, e2) -> + mk_and unsat deduce (fun x x0 x1 -> + xcnf unsat deduce normalise1 negate0 x x0 x1) k0 pol0 e1 e2 +| OR (k0, e1, e2) -> + mk_or unsat deduce (fun x x0 x1 -> + xcnf unsat deduce normalise1 negate0 x x0 x1) k0 pol0 e1 e2 +| NOT (k0, e) -> xcnf unsat deduce normalise1 negate0 (negb pol0) k0 e +| IMPL (k0, e1, _, e2) -> + mk_impl unsat deduce (fun x x0 x1 -> + xcnf unsat deduce normalise1 negate0 x x0 x1) k0 pol0 e1 e2 +| IFF (k0, e1, e2) -> + (match is_bool k0 e2 with + | Some isb -> + xcnf unsat deduce normalise1 negate0 (if isb then pol0 else negb pol0) + k0 e1 + | None -> + mk_iff unsat deduce (fun x x0 x1 -> + xcnf unsat deduce normalise1 negate0 x x0 x1) k0 pol0 e1 e2) +| EQ (e1, e2) -> + (match is_bool IsBool e2 with + | Some isb -> + xcnf unsat deduce normalise1 negate0 (if isb then pol0 else negb pol0) + IsBool e1 + | None -> + mk_iff unsat deduce (fun x x0 x1 -> + xcnf unsat deduce normalise1 negate0 x x0 x1) IsBool pol0 e1 e2) -(** val add_term : +(** val radd_term : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) - clause -> ('a1, 'a2) clause option **) + clause -> (('a1, 'a2) clause, 'a2 trace) sum **) -let rec add_term unsat deduce t0 = function +let rec radd_term unsat deduce t0 = function | [] -> (match deduce (fst t0) (fst t0) with - | Some u -> if unsat u then None else Some (t0::[]) - | None -> Some (t0::[])) + | Some u -> if unsat u then Inr (Push ((snd t0), Null)) else Inl (t0::[]) + | None -> Inl (t0::[])) | t'::cl0 -> (match deduce (fst t0) (fst t') with | Some u -> if unsat u - then None - else (match add_term unsat deduce t0 cl0 with - | Some cl' -> Some (t'::cl') - | None -> None) + then Inr (Push ((snd t0), (Push ((snd t'), Null)))) + else (match radd_term unsat deduce t0 cl0 with + | Inl cl' -> Inl (t'::cl') + | Inr l -> Inr l) | None -> - (match add_term unsat deduce t0 cl0 with - | Some cl' -> Some (t'::cl') - | None -> None)) + (match radd_term unsat deduce t0 cl0 with + | Inl cl' -> Inl (t'::cl') + | Inr l -> Inr l)) -(** val or_clause : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, - 'a2) clause -> ('a1, 'a2) clause option **) +(** val ror_clause : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, + 'a2) clause -> (('a1, 'a2) clause, 'a2 trace) sum **) -let rec or_clause unsat deduce cl1 cl2 = +let rec ror_clause unsat deduce cl1 cl2 = match cl1 with - | [] -> Some cl2 + | [] -> Inl cl2 | t0::cl -> - (match add_term unsat deduce t0 cl2 with - | Some cl' -> or_clause unsat deduce cl cl' - | None -> None) + (match radd_term unsat deduce t0 cl2 with + | Inl cl' -> ror_clause unsat deduce cl cl' + | Inr l -> Inr l) -(** val xor_clause_cnf : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, - 'a2) cnf -> ('a1, 'a2) cnf **) +(** val xror_clause_cnf : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, + 'a2) clause list -> ('a1, 'a2) clause list * 'a2 trace **) -let xor_clause_cnf unsat deduce t0 f = - fold_left (fun acc e -> - match or_clause unsat deduce t0 e with - | Some cl -> cl::acc - | None -> acc) f [] +let xror_clause_cnf unsat deduce t0 f = + fold_left (fun pat e -> + let acc,tg = pat in + (match ror_clause unsat deduce t0 e with + | Inl cl -> (cl::acc),tg + | Inr l -> acc,(Merge (tg, l)))) + f ([],Null) -(** val or_clause_cnf : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, - 'a2) cnf -> ('a1, 'a2) cnf **) +(** val ror_clause_cnf : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, + 'a2) clause list -> ('a1, 'a2) clause list * 'a2 trace **) -let or_clause_cnf unsat deduce t0 f = +let ror_clause_cnf unsat deduce t0 f = match t0 with - | [] -> f - | _::_ -> xor_clause_cnf unsat deduce t0 f + | [] -> f,Null + | _::_ -> xror_clause_cnf unsat deduce t0 f -(** val or_cnf : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, - 'a2) cnf -> ('a1, 'a2) cnf **) - -let rec or_cnf unsat deduce f f' = - match f with - | [] -> cnf_tt - | e::rst -> - rev_append (or_cnf unsat deduce rst f') (or_clause_cnf unsat deduce e f') - -(** val and_cnf : ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf **) - -let and_cnf = - rev_append - -type ('term, 'annot, 'tX, 'aF) tFormula = ('term, 'tX, 'annot, 'aF) gFormula - -(** val is_cnf_tt : ('a1, 'a2) cnf -> bool **) - -let is_cnf_tt = function -| [] -> true -| _::_ -> false - -(** val is_cnf_ff : ('a1, 'a2) cnf -> bool **) - -let is_cnf_ff = function -| [] -> false -| c0::l -> - (match c0 with - | [] -> (match l with - | [] -> true - | _::_ -> false) - | _::_ -> false) - -(** val and_cnf_opt : ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf **) - -let and_cnf_opt f1 f2 = - if if is_cnf_ff f1 then true else is_cnf_ff f2 - then cnf_ff - else if is_cnf_tt f2 then f1 else and_cnf f1 f2 - -(** val or_cnf_opt : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, - 'a2) cnf -> ('a1, 'a2) cnf **) - -let or_cnf_opt unsat deduce f1 f2 = - if if is_cnf_tt f1 then true else is_cnf_tt f2 - then cnf_tt - else if is_cnf_ff f2 then f1 else or_cnf unsat deduce f1 f2 - -(** val mk_and : - ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, - 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3, - 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf **) - -let mk_and unsat deduce rEC k pol0 f1 f2 = - if pol0 - then and_cnf_opt (rEC pol0 k f1) (rEC pol0 k f2) - else or_cnf_opt unsat deduce (rEC pol0 k f1) (rEC pol0 k f2) - -(** val mk_or : - ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, - 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3, - 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf **) - -let mk_or unsat deduce rEC k pol0 f1 f2 = - if pol0 - then or_cnf_opt unsat deduce (rEC pol0 k f1) (rEC pol0 k f2) - else and_cnf_opt (rEC pol0 k f1) (rEC pol0 k f2) - -(** val mk_impl : - ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, - 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3, - 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf **) - -let mk_impl unsat deduce rEC k pol0 f1 f2 = - if pol0 - then or_cnf_opt unsat deduce (rEC (negb pol0) k f1) (rEC pol0 k f2) - else and_cnf_opt (rEC (negb pol0) k f1) (rEC pol0 k f2) - -(** val mk_iff : - ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, - 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3, - 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf **) - -let mk_iff unsat deduce rEC k pol0 f1 f2 = - or_cnf_opt unsat deduce - (and_cnf_opt (rEC (negb pol0) k f1) (rEC false k f2)) - (and_cnf_opt (rEC pol0 k f1) (rEC true k f2)) - -(** val is_bool : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> bool option **) - -let is_bool _ = function -| TT _ -> Some true -| FF _ -> Some false -| _ -> None - -(** val xcnf : - ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) - cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> kind -> ('a1, 'a3, 'a4, - 'a5) tFormula -> ('a2, 'a3) cnf **) - -let rec xcnf unsat deduce normalise1 negate0 pol0 _ = function -| TT _ -> if pol0 then cnf_tt else cnf_ff -| FF _ -> if pol0 then cnf_ff else cnf_tt -| X (_, _) -> cnf_ff -| A (_, x, t0) -> if pol0 then normalise1 x t0 else negate0 x t0 -| AND (k0, e1, e2) -> - mk_and unsat deduce (fun x x0 x1 -> - xcnf unsat deduce normalise1 negate0 x x0 x1) k0 pol0 e1 e2 -| OR (k0, e1, e2) -> - mk_or unsat deduce (fun x x0 x1 -> - xcnf unsat deduce normalise1 negate0 x x0 x1) k0 pol0 e1 e2 -| NOT (k0, e) -> xcnf unsat deduce normalise1 negate0 (negb pol0) k0 e -| IMPL (k0, e1, _, e2) -> - mk_impl unsat deduce (fun x x0 x1 -> - xcnf unsat deduce normalise1 negate0 x x0 x1) k0 pol0 e1 e2 -| IFF (k0, e1, e2) -> - (match is_bool k0 e2 with - | Some isb -> - xcnf unsat deduce normalise1 negate0 (if isb then pol0 else negb pol0) - k0 e1 - | None -> - mk_iff unsat deduce (fun x x0 x1 -> - xcnf unsat deduce normalise1 negate0 x x0 x1) k0 pol0 e1 e2) -| EQ (e1, e2) -> - (match is_bool IsBool e2 with - | Some isb -> - xcnf unsat deduce normalise1 negate0 (if isb then pol0 else negb pol0) - IsBool e1 - | None -> - mk_iff unsat deduce (fun x x0 x1 -> - xcnf unsat deduce normalise1 negate0 x x0 x1) IsBool pol0 e1 e2) - -(** val radd_term : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) - clause -> (('a1, 'a2) clause, 'a2 trace) sum **) - -let rec radd_term unsat deduce t0 = function -| [] -> - (match deduce (fst t0) (fst t0) with - | Some u -> if unsat u then Inr (Push ((snd t0), Null)) else Inl (t0::[]) - | None -> Inl (t0::[])) -| t'::cl0 -> - (match deduce (fst t0) (fst t') with - | Some u -> - if unsat u - then Inr (Push ((snd t0), (Push ((snd t'), Null)))) - else (match radd_term unsat deduce t0 cl0 with - | Inl cl' -> Inl (t'::cl') - | Inr l -> Inr l) - | None -> - (match radd_term unsat deduce t0 cl0 with - | Inl cl' -> Inl (t'::cl') - | Inr l -> Inr l)) - -(** val ror_clause : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, - 'a2) clause -> (('a1, 'a2) clause, 'a2 trace) sum **) - -let rec ror_clause unsat deduce cl1 cl2 = - match cl1 with - | [] -> Inl cl2 - | t0::cl -> - (match radd_term unsat deduce t0 cl2 with - | Inl cl' -> ror_clause unsat deduce cl cl' - | Inr l -> Inr l) - -(** val xror_clause_cnf : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, - 'a2) clause list -> ('a1, 'a2) clause list * 'a2 trace **) - -let xror_clause_cnf unsat deduce t0 f = - fold_left (fun pat e -> - let acc,tg = pat in - (match ror_clause unsat deduce t0 e with - | Inl cl -> (cl::acc),tg - | Inr l -> acc,(Merge (tg, l)))) - f ([],Null) - -(** val ror_clause_cnf : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, - 'a2) clause list -> ('a1, 'a2) clause list * 'a2 trace **) - -let ror_clause_cnf unsat deduce t0 f = - match t0 with - | [] -> f,Null - | _::_ -> xror_clause_cnf unsat deduce t0 f - -(** val ror_cnf : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause list -> - ('a1, 'a2) clause list -> ('a1, 'a2) cnf * 'a2 trace **) +(** val ror_cnf : + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause list -> + ('a1, 'a2) clause list -> ('a1, 'a2) cnf * 'a2 trace **) let rec ror_cnf unsat deduce f f' = match f with @@ -1677,117 +1292,502 @@ let abst_and to_constr rEC pol0 k f1 f2 = else abs_or to_constr k (rEC pol0 k f1) (rEC pol0 k f2) (fun x x0 x1 -> AND (x, x0, x1)) -(** val abst_or : - ('a1, 'a2, 'a3) to_constrT -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) - tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> kind -> ('a1, 'a2, - 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, - 'a4) tFormula **) +(** val abst_or : + ('a1, 'a2, 'a3) to_constrT -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) + tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> kind -> ('a1, 'a2, + 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, + 'a4) tFormula **) + +let abst_or to_constr rEC pol0 k f1 f2 = + if pol0 + then abs_or to_constr k (rEC pol0 k f1) (rEC pol0 k f2) (fun x x0 x1 -> OR + (x, x0, x1)) + else abs_and to_constr k (rEC pol0 k f1) (rEC pol0 k f2) (fun x x0 x1 -> OR + (x, x0, x1)) + +(** val abst_impl : + ('a1, 'a2, 'a3) to_constrT -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) + tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> 'a4 option -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> + ('a1, 'a2, 'a3, 'a4) tFormula **) + +let abst_impl to_constr rEC pol0 o k f1 f2 = + if pol0 + then abs_or to_constr k (rEC (negb pol0) k f1) (rEC pol0 k f2) (mk_arrow o) + else abs_and to_constr k (rEC (negb pol0) k f1) (rEC pol0 k f2) (mk_arrow o) + +(** val or_is_X : + kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> + bool **) + +let or_is_X k f1 f2 = + match is_X k f1 with + | Some _ -> true + | None -> (match is_X k f2 with + | Some _ -> true + | None -> false) + +(** val abs_iff : + ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> + ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, + 'a2, 'a3, 'a4) tFormula -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, + 'a2, 'a3, 'a4) tFormula **) + +let abs_iff to_constr k nf1 ff2 f1 tf2 r def = + if (&&) (or_is_X k nf1 ff2) (or_is_X k f1 tf2) + then X (r, (aformula to_constr r def)) + else def + +(** val abst_iff : + ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> (bool -> kind -> ('a1, + 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> kind + -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> + ('a1, 'a2, 'a3, 'a4) tFormula **) + +let abst_iff to_constr needA rEC pol0 k f1 f2 = + abs_iff to_constr k (rEC (negb pol0) k f1) (rEC false k f2) (rEC pol0 k f1) + (rEC true k f2) k (IFF (k, (abst_simpl to_constr needA k f1), + (abst_simpl to_constr needA k f2))) + +(** val abst_eq : + ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> (bool -> kind -> ('a1, + 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> + ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, + 'a2, 'a3, 'a4) tFormula **) + +let abst_eq to_constr needA rEC pol0 f1 f2 = + abs_iff to_constr IsBool (rEC (negb pol0) IsBool f1) (rEC false IsBool f2) + (rEC pol0 IsBool f1) (rEC true IsBool f2) IsProp (EQ + ((abst_simpl to_constr needA IsBool f1), + (abst_simpl to_constr needA IsBool f2))) + +(** val abst_form : + ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> bool -> kind -> ('a1, 'a2, + 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula **) + +let rec abst_form to_constr needA pol0 _ = function +| TT k -> if pol0 then TT k else X (k, (to_constr.mkTT k)) +| FF k -> if pol0 then X (k, (to_constr.mkFF k)) else FF k +| X (k, p) -> X (k, p) +| A (k, x, t0) -> + if needA t0 then A (k, x, t0) else X (k, (to_constr.mkA k x t0)) +| AND (k0, f1, f2) -> + abst_and to_constr (abst_form to_constr needA) pol0 k0 f1 f2 +| OR (k0, f1, f2) -> + abst_or to_constr (abst_form to_constr needA) pol0 k0 f1 f2 +| NOT (k0, f0) -> + abs_not to_constr k0 (abst_form to_constr needA (negb pol0) k0 f0) + (fun x x0 -> NOT (x, x0)) +| IMPL (k0, f1, o, f2) -> + abst_impl to_constr (abst_form to_constr needA) pol0 o k0 f1 f2 +| IFF (k0, f1, f2) -> + abst_iff to_constr needA (abst_form to_constr needA) pol0 k0 f1 f2 +| EQ (f1, f2) -> + abst_eq to_constr needA (abst_form to_constr needA) pol0 f1 f2 + +(** val cnf_checker : + (('a1 * 'a2) list -> 'a3 -> bool) -> ('a1, 'a2) cnf -> 'a3 list -> bool **) + +let rec cnf_checker checker f l = + match f with + | [] -> true + | e::f0 -> + (match l with + | [] -> false + | c::l0 -> if checker e c then cnf_checker checker f0 l0 else false) + +(** val tauto_checker : + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) + cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> (('a2 * 'a3) list -> 'a4 -> + bool) -> ('a1, rtyp, 'a3, unit0) gFormula -> 'a4 list -> bool **) + +let tauto_checker unsat deduce normalise1 negate0 checker f w = + cnf_checker checker (xcnf unsat deduce normalise1 negate0 true IsProp f) w + +type 'c pExpr = +| PEc of 'c +| PEX of positive +| PEadd of 'c pExpr * 'c pExpr +| PEsub of 'c pExpr * 'c pExpr +| PEmul of 'c pExpr * 'c pExpr +| PEopp of 'c pExpr +| PEpow of 'c pExpr * n + +type 'c pol = +| Pc of 'c +| Pinj of positive * 'c pol +| PX of 'c pol * positive * 'c pol + +(** val p0 : 'a1 -> 'a1 pol **) + +let p0 cO = + Pc cO + +(** val p1 : 'a1 -> 'a1 pol **) + +let p1 cI = + Pc cI + +(** val peq : ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> bool **) + +let rec peq ceqb p p' = + match p with + | Pc c -> (match p' with + | Pc c' -> ceqb c c' + | _ -> false) + | Pinj (j, q0) -> + (match p' with + | Pinj (j', q') -> + (match Coq_Pos.compare j j' with + | Eq -> peq ceqb q0 q' + | _ -> false) + | _ -> false) + | PX (p2, i, q0) -> + (match p' with + | PX (p'0, i', q') -> + (match Coq_Pos.compare i i' with + | Eq -> if peq ceqb p2 p'0 then peq ceqb q0 q' else false + | _ -> false) + | _ -> false) + +(** val mkPinj : positive -> 'a1 pol -> 'a1 pol **) + +let mkPinj j p = match p with +| Pc _ -> p +| Pinj (j', q0) -> Pinj ((Coq_Pos.add j j'), q0) +| PX (_, _, _) -> Pinj (j, p) + +(** val mkPinj_pred : positive -> 'a1 pol -> 'a1 pol **) + +let mkPinj_pred j p = + match j with + | XI j0 -> Pinj ((XO j0), p) + | XO j0 -> Pinj ((Coq_Pos.pred_double j0), p) + | XH -> p + +(** val mkPX : + 'a1 -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **) + +let mkPX cO ceqb p i q0 = + match p with + | Pc c -> if ceqb c cO then mkPinj XH q0 else PX (p, i, q0) + | Pinj (_, _) -> PX (p, i, q0) + | PX (p', i', q') -> + if peq ceqb q' (p0 cO) + then PX (p', (Coq_Pos.add i' i), q0) + else PX (p, i, q0) + +(** val mkXi : 'a1 -> 'a1 -> positive -> 'a1 pol **) + +let mkXi cO cI i = + PX ((p1 cI), i, (p0 cO)) + +(** val mkX : 'a1 -> 'a1 -> 'a1 pol **) + +let mkX cO cI = + mkXi cO cI XH + +(** val popp : ('a1 -> 'a1) -> 'a1 pol -> 'a1 pol **) + +let rec popp copp = function +| Pc c -> Pc (copp c) +| Pinj (j, q0) -> Pinj (j, (popp copp q0)) +| PX (p2, i, q0) -> PX ((popp copp p2), i, (popp copp q0)) + +(** val paddC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol **) + +let rec paddC cadd p c = + match p with + | Pc c1 -> Pc (cadd c1 c) + | Pinj (j, q0) -> Pinj (j, (paddC cadd q0 c)) + | PX (p2, i, q0) -> PX (p2, i, (paddC cadd q0 c)) + +(** val psubC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol **) + +let rec psubC csub p c = + match p with + | Pc c1 -> Pc (csub c1 c) + | Pinj (j, q0) -> Pinj (j, (psubC csub q0 c)) + | PX (p2, i, q0) -> PX (p2, i, (psubC csub q0 c)) + +(** val paddI : + ('a1 -> 'a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> + positive -> 'a1 pol -> 'a1 pol **) + +let rec paddI cadd pop q0 j = function +| Pc c -> mkPinj j (paddC cadd q0 c) +| Pinj (j', q') -> + (match Z.pos_sub j' j with + | Z0 -> mkPinj j (pop q' q0) + | Zpos k -> mkPinj j (pop (Pinj (k, q')) q0) + | Zneg k -> mkPinj j' (paddI cadd pop q0 k q')) +| PX (p2, i, q') -> + (match j with + | XI j0 -> PX (p2, i, (paddI cadd pop q0 (XO j0) q')) + | XO j0 -> PX (p2, i, (paddI cadd pop q0 (Coq_Pos.pred_double j0) q')) + | XH -> PX (p2, i, (pop q' q0))) + +(** val psubI : + ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> + 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **) + +let rec psubI cadd copp pop q0 j = function +| Pc c -> mkPinj j (paddC cadd (popp copp q0) c) +| Pinj (j', q') -> + (match Z.pos_sub j' j with + | Z0 -> mkPinj j (pop q' q0) + | Zpos k -> mkPinj j (pop (Pinj (k, q')) q0) + | Zneg k -> mkPinj j' (psubI cadd copp pop q0 k q')) +| PX (p2, i, q') -> + (match j with + | XI j0 -> PX (p2, i, (psubI cadd copp pop q0 (XO j0) q')) + | XO j0 -> PX (p2, i, (psubI cadd copp pop q0 (Coq_Pos.pred_double j0) q')) + | XH -> PX (p2, i, (pop q' q0))) + +(** val paddX : + 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol + -> positive -> 'a1 pol -> 'a1 pol **) + +let rec paddX cO ceqb pop p' i' p = match p with +| Pc _ -> PX (p', i', p) +| Pinj (j, q') -> + (match j with + | XI j0 -> PX (p', i', (Pinj ((XO j0), q'))) + | XO j0 -> PX (p', i', (Pinj ((Coq_Pos.pred_double j0), q'))) + | XH -> PX (p', i', q')) +| PX (p2, i, q') -> + (match Z.pos_sub i i' with + | Z0 -> mkPX cO ceqb (pop p2 p') i q' + | Zpos k -> mkPX cO ceqb (pop (PX (p2, k, (p0 cO))) p') i' q' + | Zneg k -> mkPX cO ceqb (paddX cO ceqb pop p' k p2) i q') + +(** val psubX : + 'a1 -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 + pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **) + +let rec psubX cO copp ceqb pop p' i' p = match p with +| Pc _ -> PX ((popp copp p'), i', p) +| Pinj (j, q') -> + (match j with + | XI j0 -> PX ((popp copp p'), i', (Pinj ((XO j0), q'))) + | XO j0 -> PX ((popp copp p'), i', (Pinj ((Coq_Pos.pred_double j0), q'))) + | XH -> PX ((popp copp p'), i', q')) +| PX (p2, i, q') -> + (match Z.pos_sub i i' with + | Z0 -> mkPX cO ceqb (pop p2 p') i q' + | Zpos k -> mkPX cO ceqb (pop (PX (p2, k, (p0 cO))) p') i' q' + | Zneg k -> mkPX cO ceqb (psubX cO copp ceqb pop p' k p2) i q') + +(** val padd : + 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol + -> 'a1 pol **) + +let rec padd cO cadd ceqb p = function +| Pc c' -> paddC cadd p c' +| Pinj (j', q') -> paddI cadd (padd cO cadd ceqb) q' j' p +| PX (p'0, i', q') -> + (match p with + | Pc c -> PX (p'0, i', (paddC cadd q' c)) + | Pinj (j, q0) -> + (match j with + | XI j0 -> PX (p'0, i', (padd cO cadd ceqb (Pinj ((XO j0), q0)) q')) + | XO j0 -> + PX (p'0, i', + (padd cO cadd ceqb (Pinj ((Coq_Pos.pred_double j0), q0)) q')) + | XH -> PX (p'0, i', (padd cO cadd ceqb q0 q'))) + | PX (p2, i, q0) -> + (match Z.pos_sub i i' with + | Z0 -> + mkPX cO ceqb (padd cO cadd ceqb p2 p'0) i (padd cO cadd ceqb q0 q') + | Zpos k -> + mkPX cO ceqb (padd cO cadd ceqb (PX (p2, k, (p0 cO))) p'0) i' + (padd cO cadd ceqb q0 q') + | Zneg k -> + mkPX cO ceqb (paddX cO ceqb (padd cO cadd ceqb) p'0 k p2) i + (padd cO cadd ceqb q0 q'))) + +(** val psub : + 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 + -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) + +let rec psub cO cadd csub copp ceqb p = function +| Pc c' -> psubC csub p c' +| Pinj (j', q') -> psubI cadd copp (psub cO cadd csub copp ceqb) q' j' p +| PX (p'0, i', q') -> + (match p with + | Pc c -> PX ((popp copp p'0), i', (paddC cadd (popp copp q') c)) + | Pinj (j, q0) -> + (match j with + | XI j0 -> + PX ((popp copp p'0), i', + (psub cO cadd csub copp ceqb (Pinj ((XO j0), q0)) q')) + | XO j0 -> + PX ((popp copp p'0), i', + (psub cO cadd csub copp ceqb (Pinj ((Coq_Pos.pred_double j0), q0)) + q')) + | XH -> PX ((popp copp p'0), i', (psub cO cadd csub copp ceqb q0 q'))) + | PX (p2, i, q0) -> + (match Z.pos_sub i i' with + | Z0 -> + mkPX cO ceqb (psub cO cadd csub copp ceqb p2 p'0) i + (psub cO cadd csub copp ceqb q0 q') + | Zpos k -> + mkPX cO ceqb (psub cO cadd csub copp ceqb (PX (p2, k, (p0 cO))) p'0) + i' (psub cO cadd csub copp ceqb q0 q') + | Zneg k -> + mkPX cO ceqb + (psubX cO copp ceqb (psub cO cadd csub copp ceqb) p'0 k p2) i + (psub cO cadd csub copp ceqb q0 q'))) + +(** val pmulC_aux : + 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> + 'a1 pol **) -let abst_or to_constr rEC pol0 k f1 f2 = - if pol0 - then abs_or to_constr k (rEC pol0 k f1) (rEC pol0 k f2) (fun x x0 x1 -> OR - (x, x0, x1)) - else abs_and to_constr k (rEC pol0 k f1) (rEC pol0 k f2) (fun x x0 x1 -> OR - (x, x0, x1)) +let rec pmulC_aux cO cmul ceqb p c = + match p with + | Pc c' -> Pc (cmul c' c) + | Pinj (j, q0) -> mkPinj j (pmulC_aux cO cmul ceqb q0 c) + | PX (p2, i, q0) -> + mkPX cO ceqb (pmulC_aux cO cmul ceqb p2 c) i (pmulC_aux cO cmul ceqb q0 c) -(** val abst_impl : - ('a1, 'a2, 'a3) to_constrT -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) - tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> 'a4 option -> kind - -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> - ('a1, 'a2, 'a3, 'a4) tFormula **) +(** val pmulC : + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> + 'a1 -> 'a1 pol **) -let abst_impl to_constr rEC pol0 o k f1 f2 = - if pol0 - then abs_or to_constr k (rEC (negb pol0) k f1) (rEC pol0 k f2) (mk_arrow o) - else abs_and to_constr k (rEC (negb pol0) k f1) (rEC pol0 k f2) (mk_arrow o) +let pmulC cO cI cmul ceqb p c = + if ceqb c cO + then p0 cO + else if ceqb c cI then p else pmulC_aux cO cmul ceqb p c -(** val or_is_X : - kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> - bool **) +(** val pmulI : + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> + 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol **) -let or_is_X k f1 f2 = - match is_X k f1 with - | Some _ -> true - | None -> (match is_X k f2 with - | Some _ -> true - | None -> false) +let rec pmulI cO cI cmul ceqb pmul0 q0 j = function +| Pc c -> mkPinj j (pmulC cO cI cmul ceqb q0 c) +| Pinj (j', q') -> + (match Z.pos_sub j' j with + | Z0 -> mkPinj j (pmul0 q' q0) + | Zpos k -> mkPinj j (pmul0 (Pinj (k, q')) q0) + | Zneg k -> mkPinj j' (pmulI cO cI cmul ceqb pmul0 q0 k q')) +| PX (p', i', q') -> + (match j with + | XI j' -> + mkPX cO ceqb (pmulI cO cI cmul ceqb pmul0 q0 j p') i' + (pmulI cO cI cmul ceqb pmul0 q0 (XO j') q') + | XO j' -> + mkPX cO ceqb (pmulI cO cI cmul ceqb pmul0 q0 j p') i' + (pmulI cO cI cmul ceqb pmul0 q0 (Coq_Pos.pred_double j') q') + | XH -> + mkPX cO ceqb (pmulI cO cI cmul ceqb pmul0 q0 XH p') i' (pmul0 q' q0)) -(** val abs_iff : - ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> - ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, - 'a2, 'a3, 'a4) tFormula -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, - 'a2, 'a3, 'a4) tFormula **) +(** val pmul : + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 + -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) -let abs_iff to_constr k nf1 ff2 f1 tf2 r def = - if (&&) (or_is_X k nf1 ff2) (or_is_X k f1 tf2) - then X (r, (aformula to_constr r def)) - else def +let rec pmul cO cI cadd cmul ceqb p p'' = match p'' with +| Pc c -> pmulC cO cI cmul ceqb p c +| Pinj (j', q') -> pmulI cO cI cmul ceqb (pmul cO cI cadd cmul ceqb) q' j' p +| PX (p', i', q') -> + (match p with + | Pc c -> pmulC cO cI cmul ceqb p'' c + | Pinj (j, q0) -> + let qQ' = + match j with + | XI j0 -> pmul cO cI cadd cmul ceqb (Pinj ((XO j0), q0)) q' + | XO j0 -> + pmul cO cI cadd cmul ceqb (Pinj ((Coq_Pos.pred_double j0), q0)) q' + | XH -> pmul cO cI cadd cmul ceqb q0 q' + in + mkPX cO ceqb (pmul cO cI cadd cmul ceqb p p') i' qQ' + | PX (p2, i, q0) -> + let qQ' = pmul cO cI cadd cmul ceqb q0 q' in + let pQ' = pmulI cO cI cmul ceqb (pmul cO cI cadd cmul ceqb) q' XH p2 in + let qP' = pmul cO cI cadd cmul ceqb (mkPinj XH q0) p' in + let pP' = pmul cO cI cadd cmul ceqb p2 p' in + padd cO cadd ceqb + (mkPX cO ceqb (padd cO cadd ceqb (mkPX cO ceqb pP' i (p0 cO)) qP') i' + (p0 cO)) + (mkPX cO ceqb pQ' i qQ')) -(** val abst_iff : - ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> (bool -> kind -> ('a1, - 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> kind - -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> - ('a1, 'a2, 'a3, 'a4) tFormula **) +(** val psquare : + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 + -> bool) -> 'a1 pol -> 'a1 pol **) -let abst_iff to_constr needA rEC pol0 k f1 f2 = - abs_iff to_constr k (rEC (negb pol0) k f1) (rEC false k f2) (rEC pol0 k f1) - (rEC true k f2) k (IFF (k, (abst_simpl to_constr needA k f1), - (abst_simpl to_constr needA k f2))) +let rec psquare cO cI cadd cmul ceqb = function +| Pc c -> Pc (cmul c c) +| Pinj (j, q0) -> Pinj (j, (psquare cO cI cadd cmul ceqb q0)) +| PX (p2, i, q0) -> + let twoPQ = + pmul cO cI cadd cmul ceqb p2 + (mkPinj XH (pmulC cO cI cmul ceqb q0 (cadd cI cI))) + in + let q2 = psquare cO cI cadd cmul ceqb q0 in + let p3 = psquare cO cI cadd cmul ceqb p2 in + mkPX cO ceqb (padd cO cadd ceqb (mkPX cO ceqb p3 i (p0 cO)) twoPQ) i q2 -(** val abst_eq : - ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> (bool -> kind -> ('a1, - 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> - ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, - 'a2, 'a3, 'a4) tFormula **) +(** val mk_X : 'a1 -> 'a1 -> positive -> 'a1 pol **) -let abst_eq to_constr needA rEC pol0 f1 f2 = - abs_iff to_constr IsBool (rEC (negb pol0) IsBool f1) (rEC false IsBool f2) - (rEC pol0 IsBool f1) (rEC true IsBool f2) IsProp (EQ - ((abst_simpl to_constr needA IsBool f1), - (abst_simpl to_constr needA IsBool f2))) +let mk_X cO cI j = + mkPinj_pred j (mkX cO cI) -(** val abst_form : - ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> bool -> kind -> ('a1, 'a2, - 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula **) +(** val ppow_pos : + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 + -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> 'a1 pol -> positive -> 'a1 + pol **) -let rec abst_form to_constr needA pol0 _ = function -| TT k -> if pol0 then TT k else X (k, (to_constr.mkTT k)) -| FF k -> if pol0 then X (k, (to_constr.mkFF k)) else FF k -| X (k, p) -> X (k, p) -| A (k, x, t0) -> - if needA t0 then A (k, x, t0) else X (k, (to_constr.mkA k x t0)) -| AND (k0, f1, f2) -> - abst_and to_constr (abst_form to_constr needA) pol0 k0 f1 f2 -| OR (k0, f1, f2) -> - abst_or to_constr (abst_form to_constr needA) pol0 k0 f1 f2 -| NOT (k0, f0) -> - abs_not to_constr k0 (abst_form to_constr needA (negb pol0) k0 f0) - (fun x x0 -> NOT (x, x0)) -| IMPL (k0, f1, o, f2) -> - abst_impl to_constr (abst_form to_constr needA) pol0 o k0 f1 f2 -| IFF (k0, f1, f2) -> - abst_iff to_constr needA (abst_form to_constr needA) pol0 k0 f1 f2 -| EQ (f1, f2) -> - abst_eq to_constr needA (abst_form to_constr needA) pol0 f1 f2 +let rec ppow_pos cO cI cadd cmul ceqb subst_l res p = function +| XI p3 -> + subst_l + (pmul cO cI cadd cmul ceqb + (ppow_pos cO cI cadd cmul ceqb subst_l + (ppow_pos cO cI cadd cmul ceqb subst_l res p p3) p p3) + p) +| XO p3 -> + ppow_pos cO cI cadd cmul ceqb subst_l + (ppow_pos cO cI cadd cmul ceqb subst_l res p p3) p p3 +| XH -> subst_l (pmul cO cI cadd cmul ceqb res p) -(** val cnf_checker : - (('a1 * 'a2) list -> 'a3 -> bool) -> ('a1, 'a2) cnf -> 'a3 list -> bool **) +(** val ppow_N : + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 + -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> n -> 'a1 pol **) -let rec cnf_checker checker f l = - match f with - | [] -> true - | e::f0 -> - (match l with - | [] -> false - | c::l0 -> if checker e c then cnf_checker checker f0 l0 else false) +let ppow_N cO cI cadd cmul ceqb subst_l p = function +| N0 -> p1 cI +| Npos p2 -> ppow_pos cO cI cadd cmul ceqb subst_l (p1 cI) p p2 -(** val tauto_checker : - ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) - cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> (('a2 * 'a3) list -> 'a4 -> - bool) -> ('a1, rtyp, 'a3, unit0) gFormula -> 'a4 list -> bool **) +(** val norm_aux : + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 + -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol **) -let tauto_checker unsat deduce normalise1 negate0 checker f w = - cnf_checker checker (xcnf unsat deduce normalise1 negate0 true IsProp f) w +let rec norm_aux cO cI cadd cmul csub copp ceqb = function +| PEc c -> Pc c +| PEX j -> mk_X cO cI j +| PEadd (pe1, pe2) -> + (match pe1 with + | PEopp pe3 -> + psub cO cadd csub copp ceqb + (norm_aux cO cI cadd cmul csub copp ceqb pe2) + (norm_aux cO cI cadd cmul csub copp ceqb pe3) + | _ -> + (match pe2 with + | PEopp pe3 -> + psub cO cadd csub copp ceqb + (norm_aux cO cI cadd cmul csub copp ceqb pe1) + (norm_aux cO cI cadd cmul csub copp ceqb pe3) + | _ -> + padd cO cadd ceqb (norm_aux cO cI cadd cmul csub copp ceqb pe1) + (norm_aux cO cI cadd cmul csub copp ceqb pe2))) +| PEsub (pe1, pe2) -> + psub cO cadd csub copp ceqb (norm_aux cO cI cadd cmul csub copp ceqb pe1) + (norm_aux cO cI cadd cmul csub copp ceqb pe2) +| PEmul (pe1, pe2) -> + pmul cO cI cadd cmul ceqb (norm_aux cO cI cadd cmul csub copp ceqb pe1) + (norm_aux cO cI cadd cmul csub copp ceqb pe2) +| PEopp pe1 -> popp copp (norm_aux cO cI cadd cmul csub copp ceqb pe1) +| PEpow (pe1, n0) -> + ppow_N cO cI cadd cmul ceqb (fun p -> p) + (norm_aux cO cI cadd cmul csub copp ceqb pe1) n0 (** val cneqb : ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool **) @@ -2308,7 +2308,7 @@ type zArithProof = | RatProof of zWitness * zArithProof | CutProof of zWitness * zArithProof | SplitProof of z polC * zArithProof * zArithProof -| EnumProof of zWitness * zWitness * zArithProof list +| Deprecated_EnumProof of zWitness * zWitness * zArithProof list | ExProof of positive * zArithProof (** val zgcdM : z -> z -> z **) @@ -2361,26 +2361,11 @@ let genCuttingPlane = function let nformula_of_cutting_plane = function | e_z,o -> let e,z0 = e_z in (padd1 e (Pc z0)),o -(** val is_pol_Z0 : z polC -> bool **) - -let is_pol_Z0 = function -| Pc z0 -> (match z0 with - | Z0 -> true - | _ -> false) -| _ -> false - (** val eval_Psatz0 : z nFormula list -> zWitness -> z nFormula option **) let eval_Psatz0 = eval_Psatz Z0 (Zpos XH) Z.add Z.mul Z.eqb Z.leb -(** val valid_cut_sign : op1 -> bool **) - -let valid_cut_sign = function -| Equal -> true -| NonStrict -> true -| _ -> false - (** val bound_var : positive -> z formula **) let bound_var v = @@ -2407,7 +2392,6 @@ let max_var_nformulae l = (** val zChecker : z nFormula list -> zArithProof -> bool **) let rec zChecker l = function -| DoneProof -> false | RatProof (w, pf0) -> (match eval_Psatz0 l w with | Some f -> if zunsat f then true else zChecker (f::l) pf0 @@ -2428,33 +2412,6 @@ let rec zChecker l = function (zChecker ((nformula_of_cutting_plane cp2)::l) pf2) | None -> false) | None -> false) -| EnumProof (w1, w2, pf0) -> - (match eval_Psatz0 l w1 with - | Some f1 -> - (match eval_Psatz0 l w2 with - | Some f2 -> - (match genCuttingPlane f1 with - | Some p -> - let p2,op3 = p in - let e1,z1 = p2 in - (match genCuttingPlane f2 with - | Some p3 -> - let p4,op4 = p3 in - let e2,z2 = p4 in - if (&&) ((&&) (valid_cut_sign op3) (valid_cut_sign op4)) - (is_pol_Z0 (padd1 e1 e2)) - then let rec label pfs lb ub = - match pfs with - | [] -> Z.gtb lb ub - | pf1::rsr -> - (&&) (zChecker (((psub1 e1 (Pc lb)),Equal)::l) pf1) - (label rsr (Z.add lb (Zpos XH)) ub) - in label pf0 (Z.opp z1) z2 - else false - | None -> true) - | None -> true) - | None -> false) - | None -> false) | ExProof (x, prf) -> let fr = max_var_nformulae l in if Coq_Pos.leb x fr @@ -2465,6 +2422,7 @@ let rec zChecker l = function let post = xnnormalise (bound_var t0) in zChecker (nfx::(posz::(post::l))) prf else false +| _ -> false (** val zTautoChecker : z formula bFormula -> zArithProof list -> bool **) @@ -2516,7 +2474,7 @@ let qinv x = (** val qpower_positive : q -> positive -> q **) let qpower_positive = - pow_pos qmult + pow_pos0 qmult (** val qpower : q -> z -> q **) diff --git a/theories/All/All.v b/theories/All/All.v index e7f515f684..86cfe1d745 100644 --- a/theories/All/All.v +++ b/theories/All/All.v @@ -63,6 +63,7 @@ From Stdlib Require Export micromega.ZifyComparison. From Stdlib Require Export micromega.ZifyInst. From Stdlib Require Export micromega.ZifyN. From Stdlib Require Export micromega.ZifyNat. +From Stdlib Require Export micromega.SatDivMod. From Stdlib Require Export micromega.ZifyPow. From Stdlib Require Export micromega.ZifySint63. From Stdlib Require Export micromega.ZifyUint63. diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v index a2908d5b81..f88b2d6fdc 100644 --- a/theories/Arith/Compare.v +++ b/theories/Arith/Compare.v @@ -16,9 +16,7 @@ Notation not_eq_sym := not_eq_sym (only parsing). Implicit Types m n p q : nat. -From Stdlib Require Import Arith_base. -From Stdlib Require Import Peano_dec. -From Stdlib Require Import Compare_dec. +From Stdlib Require Import PeanoNat Compare_dec. Definition le_or_le_S := le_le_S_dec. diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index cf485849b4..38028e057f 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -946,8 +946,6 @@ Qed. (** * Choice => Dependent choice => Countable choice *) (* The implications below are standard *) -From Stdlib Require Import Arith. - Theorem functional_choice_imp_functional_dependent_choice : FunctionalChoice -> FunctionalDependentChoice. Proof. diff --git a/theories/Make.compat b/theories/Make.compat index ec446b2501..4339a823ff 100644 --- a/theories/Make.compat +++ b/theories/Make.compat @@ -1,6 +1,8 @@ Compat/_All/AdmitAxiom.v Compat/_All/Stdlib818.v Reals/_Compat/Nsatz.v +Numbers/_Compat/AltBinNotations.v -Q Reals/_Compat Stdlib.Reals +-Q Numbers/_Compat Stdlib.Numbers -Q Compat/_All Stdlib.Compat diff --git a/theories/Make.zarith-base b/theories/Make.integers similarity index 57% rename from theories/Make.zarith-base rename to theories/Make.integers index 78fd933bce..5fad59eb43 100644 --- a/theories/Make.zarith-base +++ b/theories/Make.integers @@ -16,26 +16,25 @@ Numbers/Integer/Abstract/ZLt.v Numbers/Integer/Abstract/ZLcm.v Numbers/Integer/Abstract/ZBase.v Numbers/Integer/Abstract/ZBits.v -ZArith/_Base/BinIntDef.v -ZArith/_Base/BinInt.v -ZArith/_Base/Zcompare.v -ZArith/_Base/Zorder.v -ZArith/_Base/Zminmax.v -ZArith/_Base/Zmin.v -ZArith/_Base/Zmax.v -ZArith/_Base/Znat.v -ZArith/_Base/ZArith_dec.v -ZArith/_Base/Zabs.v -ZArith/_Base/auxiliary.v -ZArith/_Base/Zbool.v -ZArith/_Base/Zmisc.v -ZArith/_Base/Wf_Z.v -ZArith/_Base/Zhints.v -ZArith/_Base/ZArith_base.v -ZArith/_Base/Zeven.v -ZArith/_Base/Zpow_alt.v -ZArith/_Base/Zeuclid.v -ZArith/_Base/Int.v +PArith/Pnat.v +PArith/POrderedType.v +PArith/BinPos.v +PArith/PArith.v +PArith/BinPosDef.v +NArith/_integers/BinNatDef.v +NArith/_integers/BinNat.v +NArith/_integers/Nnat.v +NArith/_integers/Ndiv_def.v +NArith/_integers/Ndec.v +NArith/_integers/Ngcd_def.v +NArith/_integers/Nsqrt_def.v +NArith/_integers/NArith_base.v +ZArith/_integers/BinIntDef.v +ZArith/_integers/BinInt.v +ZArith/_integers/Znat.v -Q Numbers/Integer/Abstract Stdlib.Numbers.Integer.Abstract --Q ZArith/_Base Stdlib.ZArith +-Q PArith Stdlib.PArith +-Q ZArith/_integers Stdlib.ZArith +-Q NArith/_integers Stdlib.NArith +-Q Numbers/_integers Stdlib.Numbers diff --git a/theories/Make.lia b/theories/Make.lia index 5effe945ae..6b8731fceb 100644 --- a/theories/Make.lia +++ b/theories/Make.lia @@ -8,12 +8,12 @@ micromega/_Lia/ZifyPow.v micromega/_Lia/ZifyBool.v micromega/_Lia/Zify.v micromega/_Lia/ZifyInst.v +micromega/_Lia/SatDivMod.v micromega/_Lia/DeclConstantZ.v micromega/_Lia/OrderedRing.v micromega/_Lia/Tauto.v micromega/_Lia/Env.v micromega/_Lia/Refl.v -micromega/_Lia/ZArith_hints.v micromega/_Lia/ZMicromega.v micromega/_Lia/EnvRing.v micromega/_Lia/Lia.v diff --git a/theories/Make.narith-base b/theories/Make.narith-base deleted file mode 100644 index 49e2b187cb..0000000000 --- a/theories/Make.narith-base +++ /dev/null @@ -1,10 +0,0 @@ -NArith/_Base/BinNatDef.v -NArith/_Base/BinNat.v -NArith/_Base/Nnat.v -NArith/_Base/Ndiv_def.v -NArith/_Base/Ndec.v -NArith/_Base/Ngcd_def.v -NArith/_Base/Nsqrt_def.v -NArith/_Base/NArith_base.v - --Q NArith/_Base Stdlib.NArith diff --git a/theories/Make.arith-base b/theories/Make.naturals similarity index 100% rename from theories/Make.arith-base rename to theories/Make.naturals diff --git a/theories/Make.positive b/theories/Make.positive deleted file mode 100644 index f0672e975c..0000000000 --- a/theories/Make.positive +++ /dev/null @@ -1,9 +0,0 @@ -Numbers/_positive/AltBinNotations.v -PArith/Pnat.v -PArith/POrderedType.v -PArith/BinPos.v -PArith/PArith.v -PArith/BinPosDef.v - --Q Numbers/_positive Stdlib.Numbers --Q PArith Stdlib.PArith diff --git a/theories/Make.ring b/theories/Make.ring index 5821fbb2c0..bac481aa75 100644 --- a/theories/Make.ring +++ b/theories/Make.ring @@ -1,6 +1,3 @@ -ZArith/_Ring/Zpow_def.v -ZArith/_Ring/Zcomplements.v -ZArith/_Ring/Zdiv.v setoid_ring/_Ring/Ncring_polynom.v setoid_ring/_Ring/Rings_Z.v setoid_ring/_Ring/Ncring_initial.v @@ -21,6 +18,5 @@ setoid_ring/_Ring/NArithRing.v setoid_ring/_Ring/Ring_theory.v nsatz/NsatzTactic.v --Q ZArith/_Ring Stdlib.ZArith -Q setoid_ring/_Ring Stdlib.setoid_ring -Q nsatz Stdlib.nsatz diff --git a/theories/Make.zarith b/theories/Make.zarith index 97f9ee8bd6..685374cfc2 100644 --- a/theories/Make.zarith +++ b/theories/Make.zarith @@ -12,6 +12,9 @@ ZArith/_All/Zdivisibility.v ZArith/_All/Zcong.v ZArith/_All/Znumtheory.v ZArith/_All/ZNsatz.v +ZArith/_All/Zpow_def.v +ZArith/_All/Zcomplements.v +ZArith/_All/Zdiv.v Numbers/Integer/Binary/ZBinary.v Numbers/Integer/NatPairs/ZNatPairs.v Numbers/_ZArith/DecimalN.v @@ -27,8 +30,27 @@ Numbers/_ZArith/HexadecimalPos.v btauto/Algebra.v btauto/Reflect.v btauto/Btauto.v +ZArith/_All/Zcompare.v +ZArith/_All/Zorder.v +ZArith/_All/Zminmax.v +ZArith/_All/Zmin.v +ZArith/_All/Zmax.v +ZArith/_All/ZArith_dec.v +ZArith/_All/Zabs.v +ZArith/_All/auxiliary.v +ZArith/_All/Zbool.v +ZArith/_All/Zmisc.v +ZArith/_All/Wf_Z.v +ZArith/_All/Zhints.v +ZArith/_All/ZArith_base.v +ZArith/_All/Zeven.v +ZArith/_All/Zpow_alt.v +ZArith/_All/Zeuclid.v +ZArith/_All/Int.v +micromega/_ZArith/ZArith_hints.v -Q ZArith/_All Stdlib.ZArith +-Q micromega/_ZArith Stdlib.micromega -Q Numbers/Natural/Binary Stdlib.Numbers.Natural.Binary -Q Numbers/Integer/Binary Stdlib.Numbers.Integer.Binary -Q Numbers/Integer/NatPairs Stdlib.Numbers.Integer.NatPairs diff --git a/theories/Numbers/Cyclic/Int63/Sint63.v b/theories/Numbers/Cyclic/Int63/Sint63.v index d60b6c5d92..8de84ef871 100644 --- a/theories/Numbers/Cyclic/Int63/Sint63.v +++ b/theories/Numbers/Cyclic/Int63/Sint63.v @@ -411,7 +411,7 @@ Proof. intros ltn0. apply to_Z_inj. rewrite asr_spec, Z.pow_neg_r by assumption. - now rewrite Zdiv_0_r. + now rewrite Z.div_0_r. Qed. Lemma asr_1 (n : int) : (1 >> n)%sint63 = (n =? 0)%sint63. diff --git a/theories/Numbers/DecimalFacts.v b/theories/Numbers/DecimalFacts.v index 37a2de21e6..b468b415f7 100644 --- a/theories/Numbers/DecimalFacts.v +++ b/theories/Numbers/DecimalFacts.v @@ -10,7 +10,7 @@ (** * DecimalFacts : some facts about Decimal numbers *) -From Stdlib Require Import Decimal Arith ZArith. +From Stdlib Require Import PeanoNat List Decimal. Variant digits := d0 | d1 | d2 | d3 | d4 | d5 | d6 | d7 | d8 | d9. @@ -184,10 +184,7 @@ Lemma nb_digits_del_head_sub d n : Proof. rewrite !nb_digits_spec; intro Hn. rewrite del_head_spec_small; [|now apply Nat.le_sub_l]. - rewrite List.length_skipn, <-(Nat2Z.id (_ - _)). - rewrite Nat2Z.inj_sub; [|now apply Nat.le_sub_l]. - rewrite (Nat2Z.inj_sub _ _ Hn). - rewrite Z.sub_sub_distr, Z.sub_diag; apply Nat2Z.id. + rewrite List.length_skipn, Nat.sub_sub_distr, Nat.sub_diag; trivial. Qed. Lemma unorm_D0 u : unorm (D0 u) = unorm u. diff --git a/theories/Numbers/DecimalN.v b/theories/Numbers/DecimalN.v index 5114313d44..f046178608 100644 --- a/theories/Numbers/DecimalN.v +++ b/theories/Numbers/DecimalN.v @@ -13,7 +13,7 @@ Proofs that conversions between decimal numbers and [N] are bijections *) -From Stdlib Require Import Decimal DecimalFacts DecimalPos PArith NArith. +From Stdlib Require Import Decimal DecimalFacts DecimalPos BinPos BinNat. Module Unsigned. diff --git a/theories/Numbers/DecimalNat.v b/theories/Numbers/DecimalNat.v index bdca24d984..a964f97433 100644 --- a/theories/Numbers/DecimalNat.v +++ b/theories/Numbers/DecimalNat.v @@ -13,7 +13,7 @@ Proofs that conversions between decimal numbers and [nat] are bijections. *) -From Stdlib Require Import Decimal DecimalFacts Arith. +From Stdlib Require Import Decimal DecimalFacts PeanoNat. Module Unsigned. @@ -142,7 +142,7 @@ Proof. [ simpl; now rewrite Nat.mul_1_r | .. ]; unfold rev; simpl revapp; rewrite 2 IHd; rewrite <- Nat.add_assoc; f_equal; simpl_of_lu; simpl of_lu; - rewrite Nat.pow_succ_r'; ring. + rewrite ?Nat.pow_succ_r', ?Nat.mul_assoc, ?Nat.mul_add_distr_r, ?(Nat.mul_comm 10); trivial. Qed. Lemma of_uint_acc_spec n d : @@ -152,8 +152,8 @@ Proof. simpl Nat.of_uint_acc; rewrite ?Nat.tail_mul_spec, ?IHd; simpl rev; simpl usize; rewrite ?Nat.pow_succ_r'; [ simpl; now rewrite Nat.mul_1_r | .. ]; - unfold rev at 2; simpl revapp; rewrite of_lu_revapp; - simpl of_lu; ring. + unfold rev at 2; simpl revapp; rewrite of_lu_revapp; simpl of_lu; + rewrite ?Nat.mul_assoc, <-?Nat.add_assoc, <-?Nat.mul_add_distr_r, ?(Nat.mul_comm _ 10); trivial. Qed. Lemma of_uint_alt d : Nat.of_uint d = of_lu (rev d). diff --git a/theories/Numbers/DecimalPos.v b/theories/Numbers/DecimalPos.v index 983cbb2394..4e69b92ded 100644 --- a/theories/Numbers/DecimalPos.v +++ b/theories/Numbers/DecimalPos.v @@ -13,7 +13,7 @@ Proofs that conversions between decimal numbers and [positive] are bijections. *) -From Stdlib Require Import Decimal DecimalFacts PArith NArith NArithRing. +From Stdlib Require Import Decimal DecimalFacts BinPos BinNat Nnat. Module Unsigned. @@ -91,7 +91,7 @@ Proof. induction d; simpl; intro d'; [ now rewrite N.mul_1_r | .. ]; unfold rev; simpl revapp; rewrite 2 IHd; rewrite <- N.add_assoc; f_equal; simpl_of_lu; simpl of_lu; - rewrite N.pow_succ_r'; ring. + rewrite N.pow_succ_r', ?N.mul_assoc, ?(N.mul_comm 10), ?Nmult_plus_distr_r; trivial. Qed. Definition Nadd n p := @@ -121,14 +121,14 @@ Proof. rewrite N.pow_succ_r'; unfold rev; simpl revapp; try rewrite of_lu_revapp; simpl of_lu; rewrite of_uint_acc_eqn by easy; simpl tl; simpl hd; - rewrite IHd, Nadd_simpl; ring. + rewrite IHd, Nadd_simpl, ?N.mul_assoc, <-?N.add_assoc, ?(N.mul_comm 10), ?Nmult_plus_distr_r; trivial. Qed. Lemma of_uint_alt d : Pos.of_uint d = of_lu (rev d). Proof. induction d; simpl; trivial; unfold rev; simpl revapp; rewrite of_lu_revapp; simpl of_lu; try apply of_uint_acc_rev. - rewrite IHd. ring. + rewrite IHd, N.add_0_r; trivial. Qed. Lemma of_lu_rev d : Pos.of_uint (rev d) = of_lu d. @@ -143,7 +143,8 @@ Proof. rewrite N.double_spec, N.succ_double_spec. induction d; try destruct IHd as (IH1,IH2); simpl Little.double; simpl Little.succ_double; - repeat (simpl_of_lu; rewrite ?IH1, ?IH2); split; reflexivity || ring. + repeat (simpl_of_lu; rewrite ?IH1, ?IH2); split; + rewrite ?(N.add_comm _ 1), ?Nmult_plus_distr_l, ?N.add_assoc, ?N.mul_assoc; trivial. Qed. Lemma of_lu_double d : @@ -339,7 +340,7 @@ Proof. revert IHu. set (t := _ u); case t; clear t; intros u0 n H. rewrite of_lu_eqn; unfold hd, tl. - rewrite N.add_0_l, H, Nat2N.inj_succ, N.pow_succ_r'; ring. + rewrite N.add_0_l, H, Nat2N.inj_succ, N.pow_succ_r', ?(N.mul_comm 10), N.mul_assoc; trivial. Qed. End Unsigned. diff --git a/theories/Numbers/DecimalZ.v b/theories/Numbers/DecimalZ.v index 785ff496bd..259ec08ffa 100644 --- a/theories/Numbers/DecimalZ.v +++ b/theories/Numbers/DecimalZ.v @@ -13,7 +13,7 @@ Proofs that conversions between decimal numbers and [Z] are bijections. *) -From Stdlib Require Import Decimal DecimalFacts DecimalPos DecimalN ZArith. +From Stdlib Require Import Decimal DecimalFacts DecimalPos DecimalN BinNat BinInt Znat. Lemma of_to (z:Z) : Z.of_int (Z.to_int z) = z. Proof. @@ -93,7 +93,7 @@ Proof. induction n; [now simpl; rewrite N.mul_1_r|]. rewrite !Unsigned.nat_iter_S, <-IHn. simpl Unsigned.usize; rewrite N.pow_succ_r'. - rewrite !N2Z.inj_mul; simpl Z.of_N; ring. + rewrite !N2Z.inj_mul; simpl Z.of_N; rewrite ?Z.mul_assoc, ?(Z.mul_comm 10); trivial. Qed. Lemma of_int_iter_D0 d n : @@ -102,7 +102,7 @@ Proof. case d; clear d; intro d; simpl. - now rewrite of_uint_iter_D0. - rewrite of_uint_iter_D0; induction n; [now simpl|]. - rewrite !Unsigned.nat_iter_S, <-IHn; ring. + rewrite !Unsigned.nat_iter_S, <-IHn, ?Z.mul_opp_r; trivial. Qed. Lemma nztail_to_uint_pow10 n : diff --git a/theories/Numbers/HexadecimalFacts.v b/theories/Numbers/HexadecimalFacts.v index a263718ebe..d7e9c5a70b 100644 --- a/theories/Numbers/HexadecimalFacts.v +++ b/theories/Numbers/HexadecimalFacts.v @@ -10,7 +10,7 @@ (** * HexadecimalFacts : some facts about Hexadecimal numbers *) -From Stdlib Require Import Hexadecimal Arith ZArith. +From Stdlib Require Import PeanoNat List Hexadecimal. Variant digits := | d0 | d1 | d2 | d3 | d4 | d5 | d6 | d7 | d8 | d9 @@ -198,10 +198,7 @@ Lemma nb_digits_del_head_sub d n : Proof. rewrite !nb_digits_spec; intro Hn. rewrite del_head_spec_small; [|now apply Nat.le_sub_l]. - rewrite List.length_skipn, <-(Nat2Z.id (_ - _)). - rewrite Nat2Z.inj_sub; [|now apply Nat.le_sub_l]. - rewrite (Nat2Z.inj_sub _ _ Hn). - rewrite Z.sub_sub_distr, Z.sub_diag; apply Nat2Z.id. + rewrite List.length_skipn, Nat.sub_sub_distr, Nat.sub_diag; trivial. Qed. Lemma unorm_D0 u : unorm (D0 u) = unorm u. diff --git a/theories/Numbers/HexadecimalN.v b/theories/Numbers/HexadecimalN.v index 4eb1daf0f6..87590fa94f 100644 --- a/theories/Numbers/HexadecimalN.v +++ b/theories/Numbers/HexadecimalN.v @@ -13,7 +13,7 @@ Proofs that conversions between hexadecimal numbers and [N] are bijections *) -From Stdlib Require Import Hexadecimal HexadecimalFacts HexadecimalPos PArith NArith. +From Stdlib Require Import Hexadecimal HexadecimalFacts HexadecimalPos BinPos BinNat. Module Unsigned. diff --git a/theories/Numbers/HexadecimalNat.v b/theories/Numbers/HexadecimalNat.v index 47d64f25c3..0ec2cee0bf 100644 --- a/theories/Numbers/HexadecimalNat.v +++ b/theories/Numbers/HexadecimalNat.v @@ -13,7 +13,7 @@ Proofs that conversions between hexadecimal numbers and [nat] are bijections. *) -From Stdlib Require Import Hexadecimal HexadecimalFacts Arith. +From Stdlib Require Import Hexadecimal HexadecimalFacts PeanoNat. Module Unsigned. @@ -161,7 +161,7 @@ Proof. [ simpl; now rewrite Nat.mul_1_r | .. ]; unfold rev; simpl revapp; rewrite 2 IHd; rewrite <- Nat.add_assoc; f_equal; simpl_of_lu; simpl of_lu; - rewrite Nat.pow_succ_r'; ring. + rewrite ?Nat.pow_succ_r', ?Nat.mul_assoc, ?Nat.mul_add_distr_r, ?(Nat.mul_comm 16); trivial. Qed. Lemma of_uint_acc_spec n d : @@ -171,8 +171,8 @@ Proof. simpl Nat.of_hex_uint_acc; rewrite ?Nat.tail_mul_spec, ?IHd; simpl rev; simpl usize; rewrite ?Nat.pow_succ_r'; [ simpl; now rewrite Nat.mul_1_r | .. ]; - unfold rev at 2; simpl revapp; rewrite of_lu_revapp; - simpl of_lu; ring. + unfold rev at 2; simpl revapp; rewrite of_lu_revapp; simpl of_lu; + rewrite ?Nat.mul_assoc, <-?Nat.add_assoc, <-?Nat.mul_add_distr_r, ?(Nat.mul_comm _ 16); trivial. Qed. Lemma of_uint_alt d : Nat.of_hex_uint d = of_lu (rev d). diff --git a/theories/Numbers/HexadecimalPos.v b/theories/Numbers/HexadecimalPos.v index c95cc7d5fa..f1035a1dc0 100644 --- a/theories/Numbers/HexadecimalPos.v +++ b/theories/Numbers/HexadecimalPos.v @@ -13,7 +13,7 @@ Proofs that conversions between hexadecimal numbers and [positive] are bijections. *) -From Stdlib Require Import Hexadecimal HexadecimalFacts PArith NArith NArithRing. +From Stdlib Require Import Hexadecimal HexadecimalFacts BinPos BinNat Nnat. Module Unsigned. @@ -110,7 +110,7 @@ Proof. induction d; simpl; intro d'; [ now rewrite N.mul_1_r | .. ]; unfold rev; simpl revapp; rewrite 2 IHd; rewrite <- N.add_assoc; f_equal; simpl_of_lu; simpl of_lu; - rewrite N.pow_succ_r'; ring. + rewrite N.pow_succ_r', ?N.mul_assoc, ?(N.mul_comm 16), ?Nmult_plus_distr_r; trivial. Qed. Definition Nadd n p := @@ -140,14 +140,14 @@ Proof. rewrite N.pow_succ_r'; unfold rev; simpl revapp; try rewrite of_lu_revapp; simpl of_lu; rewrite of_uint_acc_eqn by easy; simpl tl; simpl hd; - rewrite IHd, Nadd_simpl; ring. + rewrite IHd, Nadd_simpl, ?N.mul_assoc, <-?N.add_assoc, ?(N.mul_comm 16), ?Nmult_plus_distr_r; trivial. Qed. Lemma of_uint_alt d : Pos.of_hex_uint d = of_lu (rev d). Proof. induction d; simpl; trivial; unfold rev; simpl revapp; rewrite of_lu_revapp; simpl of_lu; try apply of_uint_acc_rev. - rewrite IHd. ring. + rewrite IHd, N.add_0_r; trivial. Qed. Lemma of_lu_rev d : Pos.of_hex_uint (rev d) = of_lu d. @@ -162,7 +162,8 @@ Proof. rewrite N.double_spec, N.succ_double_spec. induction d; try destruct IHd as (IH1,IH2); simpl Little.double; simpl Little.succ_double; - repeat (simpl_of_lu; rewrite ?IH1, ?IH2); split; reflexivity || ring. + repeat (simpl_of_lu; rewrite ?IH1, ?IH2); split; + rewrite ?(N.add_comm _ 1), ?Nmult_plus_distr_l, ?N.add_assoc, ?N.mul_assoc; trivial. Qed. Lemma of_lu_double d : @@ -360,7 +361,7 @@ Proof. revert IHu. set (t := _ u); case t; clear t; intros u0 n H. rewrite of_lu_eqn; unfold hd, tl. - rewrite N.add_0_l, H, Nat2N.inj_succ, N.pow_succ_r'; ring. + rewrite N.add_0_l, H, Nat2N.inj_succ, N.pow_succ_r', ?N.mul_assoc, ?(N.mul_comm 16); trivial. Qed. Definition double d := rev (Little.double (rev d)). diff --git a/theories/Numbers/HexadecimalZ.v b/theories/Numbers/HexadecimalZ.v index a70506fc26..e95ac90d11 100644 --- a/theories/Numbers/HexadecimalZ.v +++ b/theories/Numbers/HexadecimalZ.v @@ -13,7 +13,7 @@ Proofs that conversions between hexadecimal numbers and [Z] are bijections. *) -From Stdlib Require Import Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalN ZArith. +From Stdlib Require Import Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalN BinNat BinInt Znat. Lemma of_to (z:Z) : Z.of_hex_int (Z.to_hex_int z) = z. Proof. @@ -94,7 +94,7 @@ Proof. induction n; [now simpl; rewrite N.mul_1_r|]. rewrite !Unsigned.nat_iter_S, <-IHn. simpl Unsigned.usize; rewrite N.pow_succ_r'. - rewrite !N2Z.inj_mul; simpl Z.of_N; ring. + rewrite !N2Z.inj_mul, ?Z.mul_assoc, ?(Z.mul_comm 16); trivial. Qed. Lemma of_hex_int_iter_D0 d n : @@ -104,7 +104,7 @@ Proof. case d; clear d; intro d; simpl. - now rewrite of_hex_uint_iter_D0. - rewrite of_hex_uint_iter_D0; induction n; [now simpl|]. - rewrite !Unsigned.nat_iter_S, <-IHn; ring. + rewrite !Unsigned.nat_iter_S, <-IHn, ?Z.mul_opp_r; trivial. Qed. Definition double d := diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v index 06bff84ac7..cb65d2d2e2 100644 --- a/theories/QArith/Qround.v +++ b/theories/QArith/Qround.v @@ -142,7 +142,7 @@ Lemma Zdiv_Qdiv (n m: Z): (n / m)%Z = Qfloor (n / m). Proof. unfold Qfloor. intros. simpl. destruct m as [ | | p]; simpl. - - now rewrite Zdiv_0_r, Z.mul_0_r. + - now rewrite Z.div_0_r, Z.mul_0_r. - now rewrite Z.mul_1_r. - rewrite <- Z.opp_eq_mul_m1. rewrite <- (Z.opp_involutive (Zpos p)). diff --git a/theories/Strings/BinaryString.v b/theories/Strings/BinaryString.v index ad65b90ecb..674d36dc0d 100644 --- a/theories/Strings/BinaryString.v +++ b/theories/Strings/BinaryString.v @@ -9,10 +9,7 @@ (************************************************************************) From Stdlib Require Import Ascii String. -From Stdlib Require Import BinNums. -Import BinNatDef. -Import BinIntDef. -Import BinPosDef. +From Stdlib Require Import BinNatDef BinIntDef BinPosDef. Local Open Scope positive_scope. Local Open Scope string_scope. diff --git a/theories/Strings/HexString.v b/theories/Strings/HexString.v index 7770565f87..41ecc5be86 100644 --- a/theories/Strings/HexString.v +++ b/theories/Strings/HexString.v @@ -9,10 +9,7 @@ (************************************************************************) From Stdlib Require Import Ascii String. -From Stdlib Require Import BinNums. -Import BinNatDef. -Import BinIntDef. -Import BinPosDef. +From Stdlib Require Import BinNatDef BinIntDef BinPosDef. Local Open Scope positive_scope. Local Open Scope string_scope. diff --git a/theories/Strings/OctalString.v b/theories/Strings/OctalString.v index 477a7de0bb..ba48cdd7bc 100644 --- a/theories/Strings/OctalString.v +++ b/theories/Strings/OctalString.v @@ -9,10 +9,7 @@ (************************************************************************) From Stdlib Require Import Ascii String. -From Stdlib Require Import BinNums. -Import BinNatDef. -Import BinIntDef. -Import BinPosDef. +From Stdlib Require Import BinNatDef BinIntDef BinPosDef. Local Open Scope positive_scope. Local Open Scope string_scope. diff --git a/theories/Strings/String.v b/theories/Strings/String.v index 47d0cc669e..db82023578 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -12,7 +12,8 @@ (** Contributed by Laurent Théry (INRIA); Adapted to Coq V8 by the Coq Development Team *) -From Stdlib Require Import Arith. +From Stdlib Require Import List. +From Stdlib Require Import PeanoNat. From Stdlib Require Import Ascii. From Stdlib Require Import Bool. From Stdlib.Strings Require Import Byte. diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index bbea730c23..1389926f87 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -679,6 +679,15 @@ Qed. (** ** Correctness proofs for Trunc division *) +Lemma div_eucl_0_r a : Z.div_eucl a 0 = (0, a). +Proof. case a; trivial. Qed. + +Lemma mod_0_r a : a mod 0 = a. +Proof. case a; trivial. Qed. + +Lemma div_0_r a : a/0 = 0. +Proof. case a; trivial. Qed. + Lemma pos_div_eucl_eq a b : 0 < b -> let (q, r) := pos_div_eucl a b in pos a = q * b + r. Proof. diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v index 9ab96ccd2a..c08ad1b06a 100644 --- a/theories/ZArith/ZArith_dec.v +++ b/theories/ZArith/ZArith_dec.v @@ -12,7 +12,6 @@ From Stdlib Require Import Sumbool. From Stdlib Require Import BinInt. From Stdlib Require Import Zorder. -From Stdlib Require Import Zcompare. Local Open Scope Z_scope. (* begin hide *) diff --git a/theories/ZArith/ZModOffset.v b/theories/ZArith/ZModOffset.v index 491c221033..9496b25353 100644 --- a/theories/ZArith/ZModOffset.v +++ b/theories/ZArith/ZModOffset.v @@ -28,7 +28,7 @@ Lemma omod_small_iff d a b : (d <= a < d+b \/ b = 0 \/ d+b < a <= d) <-> Z.omodulo d a b = a. Proof. cbv [Z.omodulo]; case (Z.eq_dec b 0) as [->|]; - rewrite ?Zmod_0_r; try pose proof Z.mod_small_iff (a-d) b; lia. + rewrite ?Z.mod_0_r; try pose proof Z.mod_small_iff (a-d) b; lia. Qed. Lemma omod_small d a b : d <= a < d+b -> Z.omodulo d a b = a. @@ -188,7 +188,7 @@ Qed. Lemma smod_complement a b h (H : b = 2*h) : Z.smodulo a b / h = - (Z.modulo a b / h). Proof. - destruct (Z.eqb_spec h 0); [subst; rewrite ?Zdiv_0_r; trivial|]; rewrite <-smod_mod. + destruct (Z.eqb_spec h 0); [subst; rewrite ?Z.div_0_r; trivial|]; rewrite <-smod_mod. specialize (Z.mod_bound_or a b); generalize (a mod b); clear a; intros a **. pose proof Z.div_smod a b ltac:(lia). progress replace (Z.quot b 2) with h in * diff --git a/theories/ZArith/Zbitwise.v b/theories/ZArith/Zbitwise.v index 3dbe79011d..a8a0a80005 100644 --- a/theories/ZArith/Zbitwise.v +++ b/theories/ZArith/Zbitwise.v @@ -1,4 +1,4 @@ -From Stdlib Require Import BinInt Lia Btauto. Local Open Scope Z_scope. +From Stdlib Require Import BinInt Wf_Z Lia Btauto. Local Open Scope Z_scope. Import (ltac.notations) BinInt.Z. Module Z. diff --git a/theories/ZArith/Zcong.v b/theories/ZArith/Zcong.v index f3c965bbbd..429072ffac 100644 --- a/theories/ZArith/Zcong.v +++ b/theories/ZArith/Zcong.v @@ -25,7 +25,7 @@ Proof. case (Z.eqb_spec a 0) as [->|nz]; trivial. cbv [invmod]; destruct Z.extgcd as [[u v]g] eqn:H. eapply Z.extgcd_correct in H; case H as [[]]; subst; cbn [fst snd]. - rewrite ?Zmod_0_r, ?Z.mul_0_r, ?Z.add_0_r in *. + rewrite ?Z.mod_0_r, ?Z.mul_0_r, ?Z.add_0_r in *. rewrite Z.gcd_0_r, <-Z.sgn_abs, (Z.mul_comm u) in H. eapply Z.mul_cancel_l; eauto. Qed. @@ -33,7 +33,7 @@ Qed. Lemma invmod_ok a m : invmod a m * a mod m = Z.gcd a m mod m. Proof. case (Z.eqb_spec m 0) as [->|nz]. - { rewrite invmod_0_r, ?Zmod_0_r, ?Z.gcd_0_r, <-?Z.sgn_abs; apply Z.mul_comm. } + { rewrite invmod_0_r, ?Z.mod_0_r, ?Z.gcd_0_r, <-?Z.sgn_abs; apply Z.mul_comm. } cbv [invmod]; destruct Z.extgcd as [[u v]g] eqn:H. eapply Z.extgcd_correct in H; case H as [[]]; subst; cbn [fst snd]. rewrite Z.gcd_mod, Z.gcd_comm in H by trivial; rewrite <-H. @@ -66,7 +66,7 @@ Qed. Lemma invmod_mod_l a m : invmod (a mod m) m = invmod a m. Proof. - case (Z.eq_dec m 0) as [->|]; [rewrite Zmod_0_r; trivial|]. + case (Z.eq_dec m 0) as [->|]; [rewrite Z.mod_0_r; trivial|]. cbv [invmod]. rewrite Zmod_mod; trivial. Qed. @@ -100,7 +100,7 @@ Proof. cbv [combinecong Z.lcm] in *; case (Z.extgcd m1 m2) as [[a b] d] eqn:E. eapply Z.extgcd_correct in E; case E as [E D]; rewrite D in *; repeat case Z.eq_dec as []; - rewrite ?e0, ?Zdiv_0_r, ?Z.mul_0_r, ?Zmod_0_r; auto using Zmod_mod. + rewrite ?e0, ?Z.div_0_r, ?Z.mul_0_r, ?Z.mod_0_r; auto using Zmod_mod. Qed. Lemma combinecong_sound m1 m2 r1 r2 (H : r1 mod Z.gcd m1 m2 = r2 mod Z.gcd m1 m2) @@ -112,7 +112,7 @@ Proof. change (Z.abs _) with (Z.lcm m1 m2). destruct (Z.eq_dec (Z.gcd m1 m2) 0) in *. { apply Z.gcd_eq_0 in e; case e as []; subst. - case Z.eq_dec; rewrite ?Zmod_0_r in *; cbn in *; intuition congruence. } + case Z.eq_dec; rewrite ?Z.mod_0_r in *; cbn in *; intuition congruence. } case Z.eq_dec as []; try congruence. rewrite 2 Z.mod_mod_divide by auto using Z.divide_lcm_l, Z.divide_lcm_r. apply Z.cong_iff_0, Z.mod_divide in H; trivial; rewrite <-D in *; clear D. @@ -142,7 +142,7 @@ Proof. revert H1 H2; case (combinecong_sound m1 m2 r1 r2 H) as [<- <-]; intros. rewrite <-mod_combinecong_lcm. remember (combinecong _ _ _ _) as b. case (Z.eq_dec m1 0) as [->|]; case (Z.eq_dec m2 0) as [->|]; - rewrite ?Zmod_0_r in *; try congruence. + rewrite ?Z.mod_0_r in *; try congruence. apply Z.cong_iff_ex in H1, H2; case H1 as [s H1]; case H2 as [r H2]. assert (s*m1/Z.gcd m1 m2 = r*m2/Z.gcd m1 m2) by congruence. rewrite !Z.divide_div_mul_exact in * by diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 8b45e9ae15..4061472a98 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -182,6 +182,7 @@ Proof. intros a; destruct a; simpl; auto. Qed. +#[deprecated(use=Z.mod_0_r, since="9.1")] Lemma Zmod_0_r: forall a, a mod 0 = a. Proof. intros a; destruct a; simpl; auto. @@ -192,6 +193,7 @@ Proof. intros a; destruct a; simpl; auto. Qed. +#[deprecated(use=Z.div_0_r, since="9.1")] Lemma Zdiv_0_r: forall a, a/0 = 0. Proof. intros a; destruct a; simpl; auto. @@ -199,7 +201,7 @@ Qed. Ltac zero_or_not a := destruct (Z.eq_dec a 0); - [subst; rewrite ?Zmod_0_l, ?Zdiv_0_l, ?Zmod_0_r, ?Zdiv_0_r; + [subst; rewrite ?Zmod_0_l, ?Zdiv_0_l, ?Z.mod_0_r, ?Z.div_0_r; auto with zarith|]. Lemma Zmod_1_r: forall a, a mod 1 = 0. @@ -209,7 +211,7 @@ Lemma Zdiv_1_r: forall a, a/1 = a. Proof. intros a. zero_or_not a. apply Z.div_1_r. Qed. #[global] -Hint Resolve Zmod_0_l Zmod_0_r Zdiv_0_l Zdiv_0_r Zdiv_1_r Zmod_1_r +Hint Resolve Zmod_0_l Z.mod_0_r Zdiv_0_l Z.div_0_r Zdiv_1_r Zmod_1_r : zarith. Lemma Zdiv_1_l: forall a, 1 < a -> 1/a = 0. @@ -246,14 +248,14 @@ Qed. Lemma Z_div_nonneg_nonneg : forall a b, 0 <= a -> 0 <= b -> 0 <= a / b. Proof. - intros a b. destruct b; intros; now (rewrite Zdiv_0_r + apply Z_div_pos). + intros a b. destruct b; intros; now (rewrite Z.div_0_r + apply Z_div_pos). Qed. (* Modulo for a non-negative divisor is non-negative. *) Lemma Z_mod_nonneg_nonneg : forall a b, 0 <= a -> 0 <= b -> 0 <= a mod b. Proof. - destruct b; intros; now (rewrite Zmod_0_r + apply Z_mod_lt). + destruct b; intros; now (rewrite Z.mod_0_r + apply Z_mod_lt). Qed. (** As soon as the divisor is greater or equal than 2, @@ -740,7 +742,7 @@ Proof. zero_or_not b; [|rewrite Z.mod_small_iff]; intuition idtac. Qed. Lemma gcd_mod_l a b : Z.gcd (a mod b) b = Z.gcd a b. Proof. case (Z.eqb_spec b 0) as [->|]; - rewrite ?Zmod_0_r, ?Z.gcd_mod, Z.gcd_comm; trivial. + rewrite ?Z.mod_0_r, ?Z.gcd_mod, Z.gcd_comm; trivial. Qed. Lemma gcd_mod_r a b : Z.gcd a (b mod a) = Z.gcd a b. @@ -749,7 +751,7 @@ Proof. rewrite Z.gcd_comm, Z.gcd_mod_l, Z.gcd_comm; trivial. Qed. Lemma mod_pow_l a b c : (a mod c)^b mod c = ((a ^ b) mod c). Proof. destruct (Z.ltb_spec b 0) as [|Hb]. { rewrite !Z.pow_neg_r; trivial. } - destruct (Z.eqb_spec c 0) as [|Hc]. { subst. rewrite !Zmod_0_r; trivial. } + destruct (Z.eqb_spec c 0) as [|Hc]. { subst. rewrite !Z.mod_0_r; trivial. } generalize dependent b; eapply Wf_Z.natlike_ind; trivial; intros x Hx IH. rewrite !Z.pow_succ_r, <-Z.mul_mod_idemp_r, IH, Z.mul_mod_idemp_l, Z.mul_mod_idemp_r; trivial. Qed. @@ -757,7 +759,7 @@ Qed. Lemma cong_iff_0 a b m : a mod m = b mod m <-> (a - b) mod m = 0. Proof. case (Z.eq_dec m 0) as [->|Hm]. - { rewrite ?Zmod_0_r; rewrite Z.sub_move_0_r; reflexivity. } + { rewrite ?Z.mod_0_r; rewrite Z.sub_move_0_r; reflexivity. } split; intros H. { rewrite Zminus_mod, H, Z.sub_diag, Z.mod_0_l; trivial. } apply Zmod_divides in H; trivial; case H as [c H]. assert (b = a + (-c) * m) as ->; rewrite ?Z.mod_add; trivial. @@ -767,16 +769,16 @@ Qed. Lemma cong_iff_ex a b m : a mod m = b mod m <-> exists n, a - b = n * m. Proof. destruct (Z.eq_dec m 0) as [->|]. - { rewrite !Zmod_0_r. setoid_rewrite Z.mul_0_r. setoid_rewrite Z.sub_move_0_r. + { rewrite !Z.mod_0_r. setoid_rewrite Z.mul_0_r. setoid_rewrite Z.sub_move_0_r. firstorder idtac. } { rewrite cong_iff_0, Z.mod_divide by trivial; reflexivity. } Qed. Lemma mod_mod_divide a b c : (c | b) -> (a mod b) mod c = a mod c. Proof. - destruct (Z.eqb_spec b 0); subst. { rewrite Zmod_0_r; trivial. } + destruct (Z.eqb_spec b 0); subst. { rewrite Z.mod_0_r; trivial. } inversion_clear 1; subst. - destruct (Z.eqb_spec c 0); subst. { rewrite Z.mul_0_r, 2Zmod_0_r; trivial. } + destruct (Z.eqb_spec c 0); subst. { rewrite Z.mul_0_r, 2Z.mod_0_r; trivial. } apply cong_iff_ex; eexists (- x * (a/(x*c))); rewrite Z.mod_eq by auto. ring_simplify; trivial. Qed. @@ -788,7 +790,7 @@ Proof. { rewrite !Z_mod_zero_opp_full; trivial. } rewrite Z_mod_nz_opp_full by trivial. rewrite <-Zminus_mod_idemp_r. - case (Z.eq_dec b 0) as [->|]; [rewrite Zmod_0_r; ring|]. + case (Z.eq_dec b 0) as [->|]; [rewrite Z.mod_0_r; ring|]. rewrite <-Z.mod_add with (b:=1) by trivial. change 0 with (0 mod b); f_equal; ring. Qed. @@ -805,7 +807,7 @@ Proof. rewrite <-(mod_mod_opp_r a (-b)), Z.opp_involutive; trivial. Qed. Lemma mod_mod_abs_r a b : (a mod Z.abs b) mod b = a mod b. Proof. case b as []; cbn [Z.abs]. - { rewrite ?Zmod_0_r; trivial. } + { rewrite ?Z.mod_0_r; trivial. } { apply Z.mod_mod; inversion 1. } { rewrite <-Pos2Z.opp_pos. apply mod_opp_r_mod. } Qed. @@ -813,7 +815,7 @@ Qed. Lemma mod_abs_r_mod a b : (a mod b) mod Z.abs b = a mod Z.abs b. Proof. case b as []; cbn [Z.abs]. - { rewrite ?Zmod_0_r; trivial. } + { rewrite ?Z.mod_0_r; trivial. } { apply Z.mod_mod; inversion 1. } { rewrite <-Pos2Z.opp_pos. apply mod_mod_opp_r. } Qed. diff --git a/theories/ZArith/Zdiv_facts.v b/theories/ZArith/Zdiv_facts.v index 4b1a9b7279..9938cc2c44 100644 --- a/theories/ZArith/Zdiv_facts.v +++ b/theories/ZArith/Zdiv_facts.v @@ -16,7 +16,7 @@ Module Z. Lemma diveq_iff c a b : (b = 0 /\ c = 0 \/ c*b <= a < c*b + b \/ c*b + b < a <= c*b) <-> a/b = c. Proof. - destruct (Z.eqb_spec b 0); [subst; rewrite Zdiv_0_r; intuition lia|]. + destruct (Z.eqb_spec b 0); [subst; rewrite Z.div_0_r; intuition lia|]. rewrite <-(Z.sub_move_0_r (_/_)), <-(Z.add_opp_r (_/_)). rewrite <-Z.div_add, Z.div_small_iff; lia. Qed. @@ -24,7 +24,7 @@ Qed. Lemma mod_diveq_iff c a b : (b = 0 \/ c*b <= a < c*b + b \/ c*b + b < a <= c*b) <-> a mod b = a-b*c. Proof. - destruct (Z.eqb_spec b 0); [subst; rewrite Zmod_0_r; intuition lia|]. + destruct (Z.eqb_spec b 0); [subst; rewrite Z.mod_0_r; intuition lia|]. rewrite Z.mod_eq by trivial; pose proof diveq_iff c a b; nia. Qed. diff --git a/theories/ZArith/Zpow_def.v b/theories/ZArith/Zpow_def.v index 940fea467e..1975f7badd 100644 --- a/theories/ZArith/Zpow_def.v +++ b/theories/ZArith/Zpow_def.v @@ -23,6 +23,7 @@ Notation Zpower_succ_r := Z.pow_succ_r (only parsing). Notation Zpower_neg_r := Z.pow_neg_r (only parsing). Notation Zpower_Ppow := Pos2Z.inj_pow (only parsing). +#[deprecated(since="9.1", note="Use setoid_ring.ZArithRing.Zpower_theory")] Lemma Zpower_theory : power_theory 1 Z.mul (@eq Z) Z.of_N Z.pow. Proof. constructor. intros z n. diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v index aea05b2fe0..57533ff1a8 100644 --- a/theories/ZArith/Zquot.v +++ b/theories/ZArith/Zquot.v @@ -419,7 +419,7 @@ Theorem Zquot_Zdiv_pos : forall a b, 0 <= a -> 0 <= b -> Proof. intros a b Ha Hb. Z.le_elim Hb. - generalize (Zquotrem_Zdiv_eucl_pos a b Ha Hb); intuition. - - subst; now rewrite Zquot_0_r, Zdiv_0_r. + - subst; now rewrite Zquot_0_r, Z.div_0_r. Qed. Theorem Zrem_Zmod_pos : forall a b, 0 <= a -> 0 < b -> diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v index 8c1ea509c8..107ecfd36e 100644 --- a/theories/ZArith/auxiliary.v +++ b/theories/ZArith/auxiliary.v @@ -11,12 +11,7 @@ (** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) -From Stdlib Require Export Arith_base. From Stdlib Require Import BinInt. -From Stdlib Require Import Zorder. -From Stdlib Require Import Decidable. -From Stdlib Require Import Peano_dec. -From Stdlib Require Export Compare_dec. Local Open Scope Z_scope. diff --git a/theories/Zmod/Bits.v b/theories/Zmod/Bits.v index 2c2c659087..92bdd5eb12 100644 --- a/theories/Zmod/Bits.v +++ b/theories/Zmod/Bits.v @@ -87,7 +87,7 @@ Proof. rewrite of_Z_inj. trivial. Qed. Lemma mod_to_Z [n] (x : bits n) : to_Z x mod 2^n = to_Z x. Proof. - case (Z.ltb_spec n 0) as []. { rewrite Z.pow_neg_r at 2 by trivial. apply Zmod_0_r. } + case (Z.ltb_spec n 0) as []. { rewrite Z.pow_neg_r at 2 by trivial. apply Z.mod_0_r. } rewrite Z.mod_small; auto using to_Z_range. Qed. @@ -250,7 +250,7 @@ Proof. apply unsigned_and_small. lia. Qed. Lemma unsigned_or [n] (x y : bits n) : to_Z (or x y) = Z.lor x y. Proof. cbv [or]; rewrite to_Z_of_Z. - case (Z.ltb_spec n 0) as []. { rewrite Z.pow_neg_r at 3 by trivial; apply Zmod_0_r. } + case (Z.ltb_spec n 0) as []. { rewrite Z.pow_neg_r at 3 by trivial; apply Z.mod_0_r. } apply Z.bits_inj; intros i; destruct (Z.ltb_spec i n); repeat rewrite ?Z.lor_spec, ?Z.mod_pow2_bits_low, ?Z.mod_pow2_bits_high, ?testbit_high by lia; trivial. Qed. @@ -259,7 +259,7 @@ Notation to_Z_or := unsigned_or (only parsing). Lemma unsigned_xor [n] (x y : bits n) : to_Z (xor x y) = Z.lxor x y. Proof. cbv [xor]; rewrite to_Z_of_Z. - case (Z.ltb_spec n 0) as []. { rewrite Z.pow_neg_r at 3 by trivial; apply Zmod_0_r. } + case (Z.ltb_spec n 0) as []. { rewrite Z.pow_neg_r at 3 by trivial; apply Z.mod_0_r. } apply Z.bits_inj; intros i; destruct (Z.ltb_spec i n); repeat rewrite ?Z.lxor_spec, ?Z.mod_pow2_bits_low, ?Z.mod_pow2_bits_high, ?testbit_high by lia; trivial. Qed. @@ -291,7 +291,7 @@ Proof. ?Z.ones_spec_high, ?Z.ones_spec_low, ?testbit_high, ?Z.ones_neg, ?Z.bits_m1 by lia; trivial; try lia. - rewrite (Z.pow_neg_r 2 n) at 2 by lia; rewrite Zmod_0_r. + rewrite (Z.pow_neg_r 2 n) at 2 by lia; rewrite Z.mod_0_r. repeat rewrite ?Z.pow_neg_r (* does not work...*) , ?Z.mod_pow2_bits_low, ?Z.mod_pow2_bits_high, ?Z.lnot_spec, ?Z.mod_pow2_bits_low, ?Z.mod_pow2_bits_high, ?Z.ldiff_spec, @@ -323,8 +323,8 @@ Proof. ?Z.mod_pow2_bits_low, ?Z.mod_pow2_bits_high, ?Z.testbit_ones, ?(proj2 (Z.ltb_lt _ _)), (proj2 (Z.leb_le _ _)), ?(proj2 (Z.ltb_nlt _ _)) by lia; trivial. - rewrite (Z.pow_neg_r 2 n) at 2 by lia; rewrite Zmod_0_r. - rewrite (Z.pow_neg_r 2 n) at 1 by lia; rewrite Zmod_0_r. + rewrite (Z.pow_neg_r 2 n) at 2 by lia; rewrite Z.mod_0_r. + rewrite (Z.pow_neg_r 2 n) at 1 by lia; rewrite Z.mod_0_r. repeat rewrite ?Z.pow_neg_r (* does not work...*) , ?Z.mod_pow2_bits_low, ?Z.mod_pow2_bits_high, ?Z.lnot_spec, ?Z.mod_pow2_bits_low, ?Z.mod_pow2_bits_high, ?Z.ldiff_spec, @@ -350,7 +350,7 @@ Lemma unsigned_app [n m] a b (Hn : 0 <= n) (Hm : 0 <= m) : to_Z (@app n m a b) = Z.lor a (Z.shiftl b n). Proof. cbv [app]. rewrite to_Z_of_Z, Z.shiftl_mul_pow2; trivial. - case (Z.ltb_spec (n+m) 0) as []. { rewrite (Z.pow_neg_r 2 (_+_)), Zmod_0_r; lia. } + case (Z.ltb_spec (n+m) 0) as []. { rewrite (Z.pow_neg_r 2 (_+_)), Z.mod_0_r; lia. } apply Z.mod_small. rewrite Z.pow_add_r by lia. (* lor <= add *) @@ -367,7 +367,7 @@ Notation to_Z_firstn := unsigned_firstn (only parsing). Lemma unsigned_skipn [n m] a (Hn : 0 <= n) : to_Z (@skipn n m a) = a/2^n. Proof. cbv [skipn]; rewrite to_Z_of_Z, Z.shiftr_div_pow2 by trivial. - case (Z.ltb_spec m n) as []. { rewrite (Z.pow_neg_r 2 (_-_)), Zmod_0_r; lia. } + case (Z.ltb_spec m n) as []. { rewrite (Z.pow_neg_r 2 (_-_)), Z.mod_0_r; lia. } pose proof to_Z_range a ltac:(lia). apply Z.mod_small; split. { Z.div_mod_to_equations; nia. } apply Zdiv_lt_upper_bound; [lia|]. diff --git a/theories/Zmod/ZmodBase.v b/theories/Zmod/ZmodBase.v index 1a9f587600..9e30955578 100644 --- a/theories/Zmod/ZmodBase.v +++ b/theories/Zmod/ZmodBase.v @@ -111,7 +111,7 @@ Proof. rewrite of_Z_inj_abs. split. { split. - { intros ->. rewrite !Zmod_0_r in H; apply H; inversion 1. } + { intros ->. rewrite !Z.mod_0_r in H; apply H; inversion 1. } { intros. subst. specialize (H ltac:(lia)). rewrite ?Z.abs_eq in * by lia; trivial. } } { intros [A B] ?. @@ -583,7 +583,7 @@ Proof. rewrite to_Z_of_small_Z; cycle 1; f_equal. { apply Z.mod_id_iff; case Z.eqb eqn:?; Z.to_euclidean_division_equations; nia. } destruct m as [|m|m]; cbn [Z.sgn Z.opp]; intuition try lia. - { case Z.eqb; rewrite Zmod_0_r, ?Z.add_0_r; trivial. } + { case Z.eqb; rewrite Z.mod_0_r, ?Z.add_0_r; trivial. } { case Z.eqb eqn:?; [|rewrite Z.mod_small]; Z.to_euclidean_division_equations; nia. } case (Z.eqb_spec (Z.sgn (x/y)) 1) as []; trivial. rewrite (Z.mod_diveq (-1)); Z.to_euclidean_division_equations; nia. @@ -596,7 +596,7 @@ Proof. rewrite to_Z_udiv by trivial. pose proof unsigned_range x. pose proof unsigned_range y. - destruct m as [|m|m]; [apply Zmod_0_r| |lia]. + destruct m as [|m|m]; [apply Z.mod_0_r| |lia]. apply Z.mod_small; Z.to_euclidean_division_equations; nia. Qed. Notation to_Z_udiv_nonneg := unsigned_udiv_nonneg (only parsing). @@ -623,7 +623,7 @@ Proof. Qed. Lemma umod_0_r [m] x : @umod m x zero = x. -Proof. apply to_Z_inj; rewrite unsigned_umod, unsigned_0, Zmod_0_r; trivial. Qed. +Proof. apply to_Z_inj; rewrite unsigned_umod, unsigned_0, Z.mod_0_r; trivial. Qed. Lemma signed_squot [m] x y : @signed m (squot x y) = Z.smodulo (if signed y =? 0 then -1 else signed x ÷ signed y) m. @@ -696,7 +696,7 @@ Notation to_Z_and := unsigned_and (only parsing). Lemma unsigned_and_small [m] (Hm : 0 <= m) x y : @to_Z m (and x y) = Z.land x y. Proof. rewrite to_Z_and. - case (Z.eqb_spec m 0) as [->|]; auto using Zmod_0_r. + case (Z.eqb_spec m 0) as [->|]; auto using Z.mod_0_r. apply Z.mod_small. pose proof to_Z_range x; pose proof to_Z_range y. pose proof N.land_le_l (Z.to_N x) (Z.to_N y). @@ -712,7 +712,7 @@ Notation to_Z_ndn := unsigned_ndn (only parsing). Lemma unsigned_ndn_small [m] x y (Hm : 0 <= m) : @to_Z m (ndn x y) = Z.ldiff x y. Proof. rewrite to_Z_ndn. - case (Z.eqb_spec m 0) as [->|]; auto using Zmod_0_r. + case (Z.eqb_spec m 0) as [->|]; auto using Z.mod_0_r. apply Z.mod_small. pose proof to_Z_range x; pose proof to_Z_range y. pose proof N.ldiff_le_l (Z.to_N x) (Z.to_N y). @@ -730,7 +730,7 @@ Notation to_Z_slu := unsigned_slu (only parsing). Lemma unsigned_sru [m] x n (Hn : 0 <= n) : @to_Z m (sru x n) = Z.shiftr x n. Proof. cbv [sru]; rewrite to_Z_of_Z. - case (Z.eqb_spec m 0) as [->|]; auto using Zmod_0_r. + case (Z.eqb_spec m 0) as [->|]; auto using Z.mod_0_r. apply Z.mod_id_iff; pose proof (to_Z_range x). rewrite Z.shiftr_div_pow2; Z.to_euclidean_division_equations; nia. Qed. diff --git a/theories/Zmod/ZstarBase.v b/theories/Zmod/ZstarBase.v index 969baafcea..d621a58d2c 100644 --- a/theories/Zmod/ZstarBase.v +++ b/theories/Zmod/ZstarBase.v @@ -280,7 +280,7 @@ Lemma mul_cancel_l [m] (a b c : Zstar m) (H : mul a b = mul a c) : b = c. Proof. case (Z.eq_dec m 0) as [->|]; trivial. { apply (f_equal (fun x => unsigned (to_Zmod x))) in H. - rewrite !to_Zmod_mul, !to_Z_mul, !Zmod_0_r in H. + rewrite !to_Zmod_mul, !to_Z_mul, !Z.mod_0_r in H. eapply to_Zmod_inj, to_Z_inj, Z.mul_cancel_l; eauto. pose proof to_Zmod_range a; rewrite Z.coprime_0_r_iff in *; lia. } apply (f_equal (fun x => mul (inv a) x)) in H. @@ -440,7 +440,7 @@ Proof. case (Z.eqb_spec m 0) as [->|]. 2:rewrite inv_mul, !mul_assoc, mul_inv_same_r, mul_1_l by lia; trivial. apply to_Zmod_inj, to_Z_inj. - repeat rewrite ?to_Zmod_inv, ?to_Zmod_mul, ?to_Z_mul, ?to_Z_inv, ?to_Zmod_pow, ?to_Z_pow, ?Zmod_0_r, ?Z.invmod_0_r. + repeat rewrite ?to_Zmod_inv, ?to_Zmod_mul, ?to_Z_mul, ?to_Z_inv, ?to_Zmod_pow, ?to_Z_pow, ?Z.mod_0_r, ?Z.invmod_0_r. rewrite Z.sgn_mul. assert (to_Z x = 1 \/ to_Z x = -1) as [->| ->] by (rewrite Z.coprime_0_r_iff in H; lia). all : cbn [Z.sgn]; lia. @@ -534,7 +534,7 @@ Proof. case Z.eqb_spec; intros. { subst m; rewrite Z.coprime_0_r_iff in H; cbv [In]. rewrite <-2to_Zmod_inj_iff, !to_Zmod_opp, !to_Zmod_1. - rewrite <-2unsigned_inj_iff, !unsigned_opp, !unsigned_1_neg, Zmod_0_r; lia. } + rewrite <-2unsigned_inj_iff, !unsigned_opp, !unsigned_1_neg, Z.mod_0_r; lia. } rewrite in_of_Zmod_filter. auto using in_elements. Qed. diff --git a/theories/extraction/ExtrHaskellNatInt.v b/theories/extraction/ExtrHaskellNatInt.v index b811933122..1298301a3a 100644 --- a/theories/extraction/ExtrHaskellNatInt.v +++ b/theories/extraction/ExtrHaskellNatInt.v @@ -2,7 +2,6 @@ From Stdlib Require Extraction. -From Stdlib Require Import Arith. From Stdlib Require Import ExtrHaskellNatNum. (** diff --git a/theories/extraction/ExtrHaskellNatInteger.v b/theories/extraction/ExtrHaskellNatInteger.v index 0f3371e1e0..8cc1d90cbc 100644 --- a/theories/extraction/ExtrHaskellNatInteger.v +++ b/theories/extraction/ExtrHaskellNatInteger.v @@ -2,7 +2,6 @@ From Stdlib Require Extraction. -From Stdlib Require Import Arith. From Stdlib Require Import ExtrHaskellNatNum. (** diff --git a/theories/extraction/ExtrHaskellNatNum.v b/theories/extraction/ExtrHaskellNatNum.v index c5ccc0cead..bab4669a7b 100644 --- a/theories/extraction/ExtrHaskellNatNum.v +++ b/theories/extraction/ExtrHaskellNatNum.v @@ -8,7 +8,7 @@ From Stdlib Require Extraction. -From Stdlib Require Import Arith. +From Stdlib Require Import PeanoNat Peano_dec Compare_dec. From Stdlib Require Import EqNat. Extract Inlined Constant Nat.add => "(Prelude.+)". diff --git a/theories/extraction/ExtrHaskellZInt.v b/theories/extraction/ExtrHaskellZInt.v index a85c93ef76..a0ac2e57a0 100644 --- a/theories/extraction/ExtrHaskellZInt.v +++ b/theories/extraction/ExtrHaskellZInt.v @@ -2,7 +2,7 @@ From Stdlib Require Extraction. -From Stdlib Require Import ZArith. +From Stdlib Require Import BinInt. From Stdlib Require Import ExtrHaskellZNum. (** diff --git a/theories/extraction/ExtrHaskellZInteger.v b/theories/extraction/ExtrHaskellZInteger.v index 377ac7db4d..7844e88cb4 100644 --- a/theories/extraction/ExtrHaskellZInteger.v +++ b/theories/extraction/ExtrHaskellZInteger.v @@ -2,7 +2,7 @@ From Stdlib Require Extraction. -From Stdlib Require Import ZArith. +From Stdlib Require Import BinInt. From Stdlib Require Import ExtrHaskellZNum. (** Disclaimer: trying to obtain efficient certified programs diff --git a/theories/extraction/ExtrHaskellZNum.v b/theories/extraction/ExtrHaskellZNum.v index bdb6c7d5ad..cd72c38b4d 100644 --- a/theories/extraction/ExtrHaskellZNum.v +++ b/theories/extraction/ExtrHaskellZNum.v @@ -8,7 +8,7 @@ From Stdlib Require Extraction. -From Stdlib Require Import ZArith. +From Stdlib Require Import BinInt ZArith_dec. From Stdlib Require Import EqNat. Extract Inlined Constant Z.add => "(Prelude.+)". diff --git a/theories/extraction/ExtrOcamlIntConv.v b/theories/extraction/ExtrOcamlIntConv.v index 4a1d0202a7..f6a228f94e 100644 --- a/theories/extraction/ExtrOcamlIntConv.v +++ b/theories/extraction/ExtrOcamlIntConv.v @@ -14,7 +14,7 @@ From Stdlib Require Extraction. -From Stdlib Require Import Arith ZArith. +From Stdlib Require Import PeanoNat BinInt. Parameter int : Type. Parameter int_zero : int. diff --git a/theories/extraction/ExtrOcamlNatBigInt.v b/theories/extraction/ExtrOcamlNatBigInt.v index ae0d786d54..64a286207f 100644 --- a/theories/extraction/ExtrOcamlNatBigInt.v +++ b/theories/extraction/ExtrOcamlNatBigInt.v @@ -12,7 +12,7 @@ From Stdlib Require Extraction. -From Stdlib Require Import Arith EqNat Euclid. +From Stdlib Require Import PeanoNat Peano_dec EqNat Euclid. From Stdlib Require Import ExtrOcamlBasic. (** NB: The extracted code depends on [zarith] package. *) diff --git a/theories/extraction/ExtrOcamlNatInt.v b/theories/extraction/ExtrOcamlNatInt.v index c92842a562..0bc8753c9b 100644 --- a/theories/extraction/ExtrOcamlNatInt.v +++ b/theories/extraction/ExtrOcamlNatInt.v @@ -12,7 +12,7 @@ From Stdlib Require Extraction. -From Stdlib Require Import Arith EqNat Euclid. +From Stdlib Require Import PeanoNat Peano_dec EqNat Euclid. From Stdlib Require Import ExtrOcamlBasic. (** Disclaimer: trying to obtain efficient certified programs diff --git a/theories/extraction/ExtrOcamlZBigInt.v b/theories/extraction/ExtrOcamlZBigInt.v index f2c67ce425..8f13a895dd 100644 --- a/theories/extraction/ExtrOcamlZBigInt.v +++ b/theories/extraction/ExtrOcamlZBigInt.v @@ -12,7 +12,7 @@ From Stdlib Require Extraction. -From Stdlib Require Import ZArith NArith. +From Stdlib Require Import BinInt BinNat. From Stdlib Require Import ExtrOcamlBasic. Extraction Blacklist Z Big_int_Z. diff --git a/theories/extraction/ExtrOcamlZInt.v b/theories/extraction/ExtrOcamlZInt.v index 934caa2af0..4c3ee0d89b 100644 --- a/theories/extraction/ExtrOcamlZInt.v +++ b/theories/extraction/ExtrOcamlZInt.v @@ -12,7 +12,7 @@ From Stdlib Require Extraction. -From Stdlib Require Import ZArith NArith. +From Stdlib Require Import BinNat BinInt. From Stdlib Require Import ExtrOcamlBasic. (** Disclaimer: trying to obtain efficient certified programs diff --git a/theories/micromega/Lia.v b/theories/micromega/Lia.v index e268cef643..7ea3ecac5b 100644 --- a/theories/micromega/Lia.v +++ b/theories/micromega/Lia.v @@ -14,9 +14,8 @@ (* *) (************************************************************************) -From Stdlib Require Import PreOmega ZMicromega RingMicromega VarMap DeclConstantZ. -From Stdlib Require Import BinNums. -From Stdlib.micromega Require Tauto. +From Stdlib Require Import BinInt. +From Stdlib.micromega Require Import Tauto VarMap ZMicromega Zify. Declare ML Module "rocq-runtime.plugins.micromega_core". Declare ML Module "rocq-runtime.plugins.micromega". diff --git a/theories/micromega/RingMicromega.v b/theories/micromega/RingMicromega.v index c5eea752e3..629d8014c4 100644 --- a/theories/micromega/RingMicromega.v +++ b/theories/micromega/RingMicromega.v @@ -11,7 +11,7 @@ (************************************************************************) From Stdlib Require Import PeanoNat. -From Stdlib Require Import BinPos BinNat. +From Stdlib Require Import BinPos BinNat NArithRing. From Stdlib Require Import Relation_Definitions. From Stdlib Require Import Setoid. From Stdlib Require Import Ring. diff --git a/theories/micromega/SatDivMod.v b/theories/micromega/SatDivMod.v new file mode 100644 index 0000000000..871527d9be --- /dev/null +++ b/theories/micromega/SatDivMod.v @@ -0,0 +1,42 @@ +From Stdlib Require Import BinInt. +From Stdlib.micromega Require Import ZifyClasses ZifyInst. + +#[local] Open Scope Z_scope. + +#[local] +Lemma Z_div_nonneg_nonneg a b : 0 <= a -> 0 <= b -> 0 <= a / b. +Proof. + intros H; pose proof Z.div_pos a b H. + case (Z.ltb_spec 0 b); auto. + intros A B; rewrite (Z.le_antisymm _ _ A B). + case a; cbv; congruence. +Qed. + +#[local] +Lemma Z_mod_nonneg_nonneg a b : 0 <= a -> 0 <= b -> 0 <= a mod b. +Proof. + case (Z.ltb_spec 0 b); intros. + { apply Z.mod_pos_bound; trivial. } + rewrite <-(Z.le_antisymm 0 b); trivial. + case a in *; cbv in *; congruence. +Qed. + +#[global] +Instance SatDiv : Saturate Z.div := + {| + PArg1 := fun x => 0 <= x; + PArg2 := fun y => 0 <= y; + PRes := fun _ _ r => 0 <= r; + SatOk := Z_div_nonneg_nonneg + |}. +Add Zify Saturate SatDiv. + +#[global] +Instance SatMod : Saturate Z.modulo := + {| + PArg1 := fun x => 0 <= x; + PArg2 := fun y => 0 <= y; + PRes := fun _ _ r => 0 <= r; + SatOk := Z_mod_nonneg_nonneg + |}. +Add Zify Saturate SatMod. diff --git a/theories/micromega/ZMicromega.v b/theories/micromega/ZMicromega.v index a609f4b456..c5ecc87ede 100644 --- a/theories/micromega/ZMicromega.v +++ b/theories/micromega/ZMicromega.v @@ -15,26 +15,23 @@ (************************************************************************) -From Stdlib Require Import List. -From Stdlib Require Import Bool. -From Stdlib Require Import OrderedRing. -From Stdlib Require Import RingMicromega. -From Stdlib Require Import ZArithRing. -From Stdlib Require Import ZCoeff. -From Stdlib Require Import Refl. -From Stdlib Require Import BinInt. -From Stdlib Require InitialRing. -From Stdlib.micromega Require Import Tauto. +From Stdlib Require Import Bool List BinInt. +From Stdlib.setoid_ring Require Import ZArithRing. +From Stdlib.micromega Require Import Refl Tauto OrderedRing RingMicromega EnvRing VarMap. + Local Open Scope Z_scope. +#[deprecated(since="9.1")] Ltac flatten_bool := repeat match goal with [ id : (_ && _)%bool = true |- _ ] => destruct (andb_prop _ _ id); clear id | [ id : (_ || _)%bool = true |- _ ] => destruct (orb_prop _ _ id); clear id end. +#[deprecated(since="9.1")] Ltac inv H := inversion H ; try subst ; clear H. +#[deprecated(since="9.1")] Lemma eq_le_iff : forall x, 0 = x <-> (0 <= x /\ x <= 0). Proof. intros. @@ -68,8 +65,6 @@ Qed. -From Stdlib Require Import EnvRing. - Lemma Zsor : SOR 0 1 Z.add Z.mul Z.sub Z.opp (@eq Z) Z.le Z.lt. Proof. constructor ; intros ; subst; try reflexivity. @@ -506,7 +501,6 @@ Definition ZweakTautoChecker (w: list ZWitness) (f : BFormula (Formula Z) Tauto. (* To get a complete checker, the proof format has to be enriched *) -From Stdlib Require Import Zdiv. Local Open Scope Z_scope. Definition ceiling (a b:Z) : Z := @@ -517,43 +511,30 @@ Definition ceiling (a b:Z) : Z := end. -Lemma Zdivide_ceiling : forall a b, (b | a) -> ceiling a b = Z.div a b. +Lemma Zdivide_ceiling a b : (b | a) -> ceiling a b = Z.div a b. Proof. - unfold ceiling. - intros a b H. - assert (mod0_divide : forall a b, (b | a) -> a mod b = 0). - { intros ? ? (?,->); apply Z_mod_mult. } - apply mod0_divide in H. - case_eq (Z.div_eucl a b). - intros z z0 H0. - change z with (fst (z,z0)). - rewrite <- H0. - change (fst (Z.div_eucl a b)) with (Z.div a b). - change z0 with (snd (z,z0)). - rewrite <- H0. - change (snd (Z.div_eucl a b)) with (Z.modulo a b). - rewrite H. - reflexivity. + intros [d ->]. + case (Z.eqb_spec b 0) as [->|]. + { cbv [ceiling]; rewrite Z.div_eucl_0_r, Z.div_0_r, Z.mul_0_r; trivial. } + specialize (Z.mod_mul d b ltac:(trivial)). + cbv [Z.div Z.modulo ceiling]. + destruct Z.div_eucl; intros ->; trivial. Qed. Lemma narrow_interval_lower_bound a b x : a > 0 -> a * x >= b -> x >= ceiling b a. Proof. - rewrite !Z.ge_le_iff. - unfold ceiling. - intros Ha H. - generalize (Z_div_mod b a Ha). - destruct (Z.div_eucl b a) as (q,r). intros (->,(H1,H2)). - destruct r as [|r|r]. - - rewrite Z.add_0_r in H. - apply Z.mul_le_mono_pos_l in H; auto with zarith. - - assert (0 < Z.pos r) by easy. - rewrite Z.add_1_r, Z.le_succ_l. - apply Z.mul_lt_mono_pos_l with a. - + auto using Z.gt_lt. - + eapply Z.lt_le_trans. 2: eassumption. - now apply Z.lt_add_pos_r. - - now elim H1. + rewrite !Z.ge_le_iff, Z.gt_lt_iff; intros Ha Hb. + generalize (Z.div_mod b a ltac:(intros ->; inversion Ha)). + generalize (Z.mul_div_le b a Ha). + generalize (Z.mod_pos_bound b a Ha). + cbv [Z.modulo Z.div ceiling]; destruct Z.div_eucl as [q r]; intros [Hr ?] **. + assert (q <= x). { eapply Z.mul_le_mono_pos_l, Z.le_trans; eauto. } + destruct r as [|r|?]; [assumption| |contradiction (Hr eq_refl)]. + rewrite Z.add_1_r, Z.le_succ_l. + eapply Z.mul_lt_mono_pos_l; [apply Ha|]. + eapply Z.lt_le_trans; [|apply Hb]. + subst b; apply Z.lt_add_pos_r, eq_refl. Qed. (** NB: narrow_interval_upper_bound is Zdiv.Zdiv_le_lower_bound *) @@ -563,10 +544,12 @@ Inductive ZArithProof := | RatProof : ZWitness -> ZArithProof -> ZArithProof | CutProof : ZWitness -> ZArithProof -> ZArithProof | SplitProof : PolC Z -> ZArithProof -> ZArithProof -> ZArithProof -| EnumProof : ZWitness -> ZWitness -> list ZArithProof -> ZArithProof +| deprecated_EnumProof : ZWitness -> ZWitness -> list ZArithProof -> ZArithProof | ExProof : positive -> ZArithProof -> ZArithProof (*ExProof x : exists z t, x = z - t /\ z >= 0 /\ t >= 0 *) . +#[deprecated(since="9.1")] +Notation EnumProof := deprecated_EnumProof (only parsing). Register ZArithProof as micromega.ZArithProof.type. @@ -574,7 +557,6 @@ Register DoneProof as micromega.ZArithProof.DoneProof. Register RatProof as micromega.ZArithProof.RatProof. Register CutProof as micromega.ZArithProof.CutProof. Register SplitProof as micromega.ZArithProof.SplitProof. -Register EnumProof as micromega.ZArithProof.EnumProof. Register ExProof as micromega.ZArithProof.ExProof. @@ -584,22 +566,27 @@ Register ExProof as micromega.ZArithProof.ExProof. - a is the gcd of the other coefficient. *) -Definition isZ0 (x:Z) := +Definition deprecated_isZ0 (x:Z) := match x with | Z0 => true | _ => false end. -Lemma isZ0_0 : forall x, isZ0 x = true <-> x = 0. +#[deprecated(since="9.1")] +Lemma isZ0_0 : forall x, deprecated_isZ0 x = true <-> x = 0. Proof. intros x; destruct x ; simpl ; intuition congruence. Qed. -Lemma isZ0_n0 : forall x, isZ0 x = false <-> x <> 0. +#[deprecated(since="9.1")] +Lemma isZ0_n0 : forall x, deprecated_isZ0 x = false <-> x <> 0. Proof. intros x; destruct x ; simpl ; intuition congruence. Qed. +#[deprecated(since="9.1")] +Notation isZ0 := deprecated_isZ0 (only parsing). + Definition ZgcdM (x y : Z) := Z.max (Z.gcd x y) 1. @@ -702,7 +689,7 @@ Proof. simpl in H0. inversion H0 ; subst; clear H0. apply IHp ; auto. - simpl. intros a b H H0. - inv H0. + inversion_clear H0. constructor. + apply Zdivide_pol_Zdivide with (1:= (ltac:(assumption) : Zdivide_pol a p)). apply Z.gcd_divide_l. @@ -722,7 +709,7 @@ Proof. simpl in H. inversion H ; subst; clear H. apply IHp ; auto. - simpl. intros ? H. - inv H. + inversion_clear H. constructor. + auto. + apply IHp2 ; assumption. @@ -734,7 +721,7 @@ Lemma Zgcd_pol_div : forall p g c, Proof. intros p; induction p as [c|? ? IHp|p1 IHp1 ? p3 IHp2]; simpl. - (* Pc *) - intros ? ? H. inv H. + intros ? ? H. inversion_clear H. constructor. exists 0. now ring. - (* Pinj *) @@ -743,7 +730,7 @@ Proof. - (* PX *) intros g c. case_eq (Zgcd_pol p1) ; case_eq (Zgcd_pol p3) ; intros z z0 H z1 z2 H0 H1. - inv H1. + inversion H1; subst; clear H1. unfold ZgcdM at 1. destruct (Z.max_spec (Z.gcd (ZgcdM z1 z2) z) 1) as [HH1 | HH1]; cycle 1; destruct HH1 as [HH1 HH1'] ; rewrite HH1'. @@ -850,13 +837,6 @@ Definition mk_eq_pos (x : positive) (y:positive) (t : positive) : Formula Z := Build_Formula (PEX x) OpEq (PEsub (PEX y) (PEX t)). -Fixpoint vars (jmp : positive) (p : Pol Z) : list positive := - match p with - | Pc c => nil - | Pinj j p => vars (Pos.add j jmp) p - | PX p j q => jmp::(vars jmp p)++vars (Pos.succ jmp) q - end. - Fixpoint max_var (jmp : positive) (p : Pol Z) : positive := match p with | Pc _ => jmp @@ -878,48 +858,6 @@ Proof. Qed. -Lemma max_var_le : forall p v, - (v <= max_var v p)%positive. -Proof. - intros p; induction p as [?|p ? IHp|? IHp1 ? ? IHp2]; simpl. - - intros. - apply Pos.le_refl. - - intros v. - specialize (IHp (p+v)%positive). - eapply Pos.le_trans ; eauto. - assert (xH + v <= p + v)%positive. - { apply Pos.add_le_mono. - - apply Pos.le_1_l. - - apply Pos.le_refl. - } - eapply Pos.le_trans ; eauto. - apply pos_le_add. - - intros v. - apply Pos.max_case_strong;intros ; auto. - specialize (IHp2 (Pos.succ v)%positive). - eapply Pos.le_trans ; eauto. -Qed. - -Lemma max_var_correct : forall p j v, - In v (vars j p) -> Pos.le v (max_var j p). -Proof. - intros p; induction p; simpl. - - tauto. - - auto. - - intros j v H. - rewrite in_app_iff in H. - destruct H as [H |[ H | H]]. - + subst. - apply Pos.max_case_strong;intros ; auto. - * apply max_var_le. - * eapply Pos.le_trans ; eauto. - apply max_var_le. - + apply Pos.max_case_strong;intros ; auto. - eapply Pos.le_trans ; eauto. - + apply Pos.max_case_strong;intros ; auto. - eapply Pos.le_trans ; eauto. -Qed. - Definition max_var_nformulae (l : list (NFormula Z)) := List.fold_left (fun acc f => Pos.max acc (max_var xH (fst f))) l xH. @@ -951,39 +889,8 @@ Section MaxVar. unfold F. apply Pos.max_le_compat_r; auto. Qed. - - - - - Lemma max_var_nformulae_correct_aux : forall l p o v, - In (p,o) l -> In v (vars xH p) -> Pos.le v (fold_left F l 1)%positive. - Proof. - intros l p o v H H0. - generalize 1%positive as acc. - revert p o v H H0. - induction l as [|a l IHl]. - - simpl. tauto. - - simpl. - intros p o v H H0 ?. - destruct H ; subst. - + unfold F at 2. - simpl. - apply max_var_correct in H0. - apply max_var_nformulae_mono_aux. - apply Pos.max_case_strong;intros ; auto. - eapply Pos.le_trans ; eauto. - + eapply IHl ; eauto. - Qed. - End MaxVar. -Lemma max_var_nformalae_correct : forall l p o v, - In (p,o) l -> In v (vars xH p) -> Pos.le v (max_var_nformulae l)%positive. -Proof. - intros l p o v. - apply max_var_nformulae_correct_aux. -Qed. - Fixpoint max_var_psatz (w : Psatz Z) : positive := match w with @@ -1000,7 +907,7 @@ Fixpoint max_var_prf (w : ZArithProof) : positive := | DoneProof => xH | RatProof w pf | CutProof w pf => Pos.max (max_var_psatz w) (max_var_prf pf) | SplitProof p pf1 pf2 => Pos.max (max_var xH p) (Pos.max (max_var_prf pf1) (max_var_prf pf1)) - | EnumProof w1 w2 l => List.fold_left + | deprecated_EnumProof w1 w2 l => List.fold_left (fun acc prf => Pos.max acc (max_var_prf prf)) l (Pos.max (max_var_psatz w1) (max_var_psatz w2)) | ExProof _ pf => max_var_prf pf @@ -1044,91 +951,9 @@ Fixpoint ZChecker (l:list (NFormula Z)) (pf : ZArithProof) {struct pf} : bool let post := xnnormalise (bound_var t) in ZChecker (nfx::posz::post::l) prf else false - | EnumProof w1 w2 pf => - match eval_Psatz l w1 , eval_Psatz l w2 with - | Some f1 , Some f2 => - match genCuttingPlane f1 , genCuttingPlane f2 with - |Some (e1,z1,op1) , Some (e2,z2,op2) => - if (valid_cut_sign op1 && valid_cut_sign op2 && is_pol_Z0 (padd e1 e2)) - then - (fix label (pfs:list ZArithProof) := - fun lb ub => - match pfs with - | nil => if Z.gtb lb ub then true else false - | pf::rsr => andb (ZChecker ((psub e1 (Pc lb), Equal) :: l) pf) (label rsr (Z.add lb 1%Z) ub) - end) pf (Z.opp z1) z2 - else false - | _ , _ => true - end - | _ , _ => false - end + | deprecated_EnumProof w1 w2 pf => false (* no longer used *) end. - - -Fixpoint bdepth (pf : ZArithProof) : nat := - match pf with - | DoneProof => O - | RatProof _ p => S (bdepth p) - | CutProof _ p => S (bdepth p) - | SplitProof _ p1 p2 => S (Nat.max (bdepth p1) (bdepth p2)) - | EnumProof _ _ l => S (List.fold_right (fun pf x => Nat.max (bdepth pf) x) O l) - | ExProof _ p => S (bdepth p) - end. - -From Stdlib Require Import PeanoNat Wf_nat. - -Lemma in_bdepth : forall l a b y, In y l -> ltof ZArithProof bdepth y (EnumProof a b l). -Proof. - intros l; induction l as [|a l IHl]. - - (* nil *) - simpl. - tauto. - - (* cons *) - simpl. - intros a0 b y H. - destruct H as [H|H]. - + subst. - unfold ltof. - simpl. - generalize ( (fold_right - (fun (pf : ZArithProof) (x : nat) => Nat.max (bdepth pf) x) 0%nat l)). - intros. - generalize (bdepth y) ; intros. - rewrite Nat.lt_succ_r. apply Nat.le_max_l. - + generalize (IHl a0 b y H). - unfold ltof. - simpl. - generalize ( (fold_right (fun (pf : ZArithProof) (x : nat) => Nat.max (bdepth pf) x) 0%nat - l)). - intros. - eapply Nat.lt_le_trans. - * eassumption. - * rewrite <- Nat.succ_le_mono. - apply Nat.le_max_r. -Qed. - -Lemma ltof_bdepth_split_l : - forall p pf1 pf2, - ltof ZArithProof bdepth pf1 (SplitProof p pf1 pf2). -Proof. - intros. - unfold ltof. simpl. - rewrite Nat.lt_succ_r. - apply Nat.le_max_l. -Qed. - -Lemma ltof_bdepth_split_r : - forall p pf1 pf2, - ltof ZArithProof bdepth pf2 (SplitProof p pf1 pf2). -Proof. - intros. - unfold ltof. simpl. - rewrite Nat.lt_succ_r. - apply Nat.le_max_r. -Qed. - - Lemma eval_Psatz_sound : forall env w l f', make_conj (eval_nformula env) l -> eval_Psatz l w = Some f' -> eval_nformula env f'. @@ -1155,7 +980,7 @@ Proof. case_eq (Zgcd_pol e) ; intros g c0. case Z.gtb_spec. - intros H0 H1 H2. - inv H2. + inversion_clear H2. change (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x)) with eval_pol in *. apply (Zgcd_pol_correct_lt _ env) in H1. 2: auto using Z.gt_lt. apply Z.le_add_le_sub_l, Z.ge_le; rewrite Z.add_0_r. @@ -1183,7 +1008,7 @@ Proof. case_eq (Z.gtb g 0 && (negb (Z.eqb c 0) && negb (Z.eqb (Z.gcd g c) g))) ; [discriminate|]. case_eq (makeCuttingPlane e). intros ? ? H H0 H1 H2 H3. - inv H3. + inversion H3; subst; clear H3. unfold makeCuttingPlane in H. rewrite H1 in H. revert H. @@ -1194,7 +1019,7 @@ Proof. rewrite Zgcd_pol_correct_lt with (1:= H1) in H2. 2: auto using Z.gt_lt. unfold nformula_of_cutting_plane. change (eval_pol env (padd e' (Pc z)) = 0). - inv H3. + inversion_clear H3. rewrite eval_pol_add. set (x:=eval_pol env (Zdiv_pol (PsubC Z.sub e c) g)) in *; clearbody x. simpl. @@ -1218,14 +1043,14 @@ Proof. ++ now rewrite Z.add_move_0_r in H2. + intros H H3. unfold nformula_of_cutting_plane. - inv H3. + inversion H3; subst; clear H3. change (eval_pol env (padd e' (Pc 0)) = 0). rewrite eval_pol_add. simpl. now rewrite Z.add_0_r. - (* NonEqual *) intros ? H H0. - inv H0. + inversion_clear H0. unfold eval_nformula in *. unfold RingMicromega.eval_nformula in *. unfold nformula_of_cutting_plane. @@ -1236,7 +1061,7 @@ Proof. intros p; destruct p as [[e' z] op]. case_eq (makeCuttingPlane (PsubC Z.sub e 1)). intros ? ? H H0 H1. - inv H1. + inversion H1; subst; clear H1. apply (makeCuttingPlane_ns_sound env) with (2:= H). simpl in *. rewrite (RingMicromega.PsubC_ok Zsor ZSORaddon). @@ -1245,7 +1070,7 @@ Proof. intros p; destruct p as [[e' z] op]. case_eq (makeCuttingPlane e). intros ? ? H H0 H1. - inv H1. + inversion H1; subst; clear H1. apply (makeCuttingPlane_ns_sound env) with (2:= H). assumption. Qed. @@ -1260,17 +1085,10 @@ Proof. - case_eq (Zgcd_pol p) ; intros g c. case_eq (Z.gtb g 0 && (negb (Z.eqb c 0) && negb (Z.eqb (Z.gcd g c) g))). + intros H H0 H1 H2. - flatten_bool. - match goal with [ H' : (g >? 0) = true |- ?G ] => rename H' into H3 end. - match goal with [ H' : negb (Z.eqb c 0) = true |- ?G ] => rename H' into H end. - match goal with [ H' : negb (Z.eqb (Z.gcd g c) g) = true |- ?G ] => rename H' into H5 end. - rewrite negb_true_iff in H5. - apply Z.eqb_neq in H5. - rewrite Z.gtb_lt in H3. - rewrite negb_true_iff in H. - apply Z.eqb_neq in H. + rewrite !andb_true_iff, !negb_true_iff in H. + case H as (?%Z.gtb_lt & ?%Z.eqb_neq & H5%Z.eqb_neq). change (eval_pol env p = 0) in H2. - rewrite Zgcd_pol_correct_lt with (1:= H0) in H2. 2: auto using Z.gt_lt. + rewrite Zgcd_pol_correct_lt with (1:= H0) in H2 by auto using Z.gt_lt. set (x:=eval_pol env (Zdiv_pol (PsubC Z.sub p c) g)) in *; clearbody x. contradict H5. apply Z.add_move_0_l in H2; subst c. @@ -1438,6 +1256,7 @@ Proof. Qed. +#[deprecated(since="9.1")] Lemma eq_true_iff_eq : forall b1 b2 : bool, (b1 = true <-> b2 = true) <-> b1 = b2. Proof. @@ -1453,282 +1272,68 @@ Proof. apply Z.le_ge_cases. Qed. +Local Lemma Private_Pos_neq_lt a b : Pos.lt a b -> a <> b. +Proof. intros H ->. apply (Pos.lt_irrefl _ H). Qed. +Local Lemma Private_Pos_neq_le_lt a b c : Pos.le a b -> Pos.lt b c -> a <> c. +Proof. intros; eapply Private_Pos_neq_lt; eauto using Pos.le_lt_trans. Qed. +Local Hint Resolve Private_Pos_neq_lt Private_Pos_neq_le_lt Pos.lt_trans: core. +Local Hint Resolve Pos.lt_succ_diag_r Z.le_ge Z.le_refl Z.lt_le_incl : core. Lemma ZChecker_sound : forall w l, ZChecker l w = true -> forall env, make_impl (eval_nformula env) l False. Proof. - intros w; induction w as [w H] using (well_founded_ind (well_founded_ltof _ bdepth)). - destruct w as [ | w pf | w pf | p pf1 pf2 | w1 w2 pf | x pf]. - - (* DoneProof *) - simpl. discriminate. - - (* RatProof *) - simpl. - intros l. case_eq (eval_Psatz l w) ; [| discriminate]. - intros f Hf. - case_eq (Zunsat f). - + intros H0 ? ?. - apply (checker_nf_sound Zsor ZSORaddon l w). - unfold check_normalised_formulas. unfold eval_Psatz in Hf. rewrite Hf. - unfold Zunsat in H0. assumption. - + intros H0 H1 env. - assert (make_impl (eval_nformula env) (f::l) False) as H2. - { apply H with (2:= H1). - unfold ltof. - simpl. - auto with arith. - } - destruct f. - rewrite <- make_conj_impl in H2. - rewrite make_conj_cons in H2. - rewrite <- make_conj_impl. - intro. - apply H2. - split ; auto. - apply eval_Psatz_sound with (2:= Hf) ; assumption. - - (* CutProof *) - simpl. - intros l. - case_eq (eval_Psatz l w) ; [ | discriminate]. - intros f' Hlc. - case_eq (genCuttingPlane f'). - + intros p H0 H1 env. - assert (make_impl (eval_nformula env) (nformula_of_cutting_plane p::l) False) as H2. - { eapply (H pf) ; auto. - unfold ltof. - simpl. - auto with arith. - } - rewrite <- make_conj_impl in H2. - rewrite make_conj_cons in H2. - rewrite <- make_conj_impl. - intro. - apply H2. - split ; auto. - apply (eval_Psatz_sound env) in Hlc. - * apply cutting_plane_sound with (1:= Hlc) (2:= H0). - * auto. - + (* genCuttingPlane = None *) - intros H0 H1 env. - rewrite <- make_conj_impl. - intros H2. - apply eval_Psatz_sound with (2:= Hlc) in H2. - apply genCuttingPlaneNone with (2:= H2) ; auto. - - (* SplitProof *) - intros l. - cbn - [genCuttingPlane]. - case_eq (genCuttingPlane (p, NonStrict)) ; [| discriminate]. - case_eq (genCuttingPlane (popp p, NonStrict)) ; [| discriminate]. - intros cp1 GCP1 cp2 GCP2 ZC1 env. - flatten_bool. - match goal with [ H' : ZChecker _ pf1 = true |- _ ] => rename H' into H0 end. - match goal with [ H' : ZChecker _ pf2 = true |- _ ] => rename H' into H1 end. + setoid_rewrite <-make_conj_impl. + induction w as [ | | | | p | x ]; cbn [ZChecker]; intros ?l E env HX. + { (* DoneProof *) discriminate. } + { (* RatProof *) + destruct eval_Psatz as [f'|] eqn:Hlc in E; [|discriminate]; + eapply eval_Psatz_sound in Hlc; eauto. + destruct Zunsat eqn:Hus in E. { eapply Zunsat_sound in Hus; eauto. } + eapply IHw; try apply E; try apply le_n. + rewrite make_conj_cons; eauto. } + { (* CutProof *) + destruct eval_Psatz as [f'|] eqn:Hlc in E; [|discriminate]; + eapply eval_Psatz_sound in Hlc; eauto. + destruct genCuttingPlane eqn:Hcp in E; [|eauto using genCuttingPlaneNone]; + eapply cutting_plane_sound in Hcp; eauto. + eapply IHw; try apply E; try apply le_n. + rewrite make_conj_cons; eauto. } + { (* SplitProof *) + destruct genCuttingPlane eqn:Hcp1 in E; [|discriminate]. + destruct genCuttingPlane eqn:Hcp2 in E; [|discriminate]; + apply andb_true_iff in E; destruct E as [El Er]. destruct (eval_nformula_split env p). - + apply (fun H' ck => H _ H' _ ck env) in H0. - * rewrite <- make_conj_impl in *. - intro ; apply H0. - rewrite make_conj_cons. split; auto. - apply (cutting_plane_sound _ (p,NonStrict)) ; auto. - * apply ltof_bdepth_split_l. - + apply (fun H' ck => H _ H' _ ck env) in H1. - * rewrite <- make_conj_impl in *. - intro ; apply H1. - rewrite make_conj_cons. split; auto. - apply (cutting_plane_sound _ (popp p,NonStrict)) ; auto. - * apply ltof_bdepth_split_r. - - (* EnumProof *) - intros l. - simpl. - case_eq (eval_Psatz l w1) ; [ | discriminate]. - case_eq (eval_Psatz l w2) ; [ | discriminate]. - intros f1 Hf1 f2 Hf2. - case_eq (genCuttingPlane f2). - + intros p; destruct p as [ [p1 z1] op1]. - case_eq (genCuttingPlane f1). - * intros p; destruct p as [ [p2 z2] op2]. - case_eq (valid_cut_sign op1 && valid_cut_sign op2 && is_pol_Z0 (padd p1 p2)). - -- intros Hcond. - flatten_bool. - match goal with [ H1 : is_pol_Z0 (padd p1 p2) = true |- _ ] => rename H1 into HZ0 end. - match goal with [ H2 : valid_cut_sign op1 = true |- _ ] => rename H2 into Hop1 end. - match goal with [ H3 : valid_cut_sign op2 = true |- _ ] => rename H3 into Hop2 end. - intros HCutL HCutR Hfix env. - (* get the bounds of the enum *) - rewrite <- make_conj_impl. - intro H0. - assert (-z1 <= eval_pol env p1 <= z2) as H1. { - split. - - apply (eval_Psatz_sound env) in Hf2 ; auto. - apply cutting_plane_sound with (1:= Hf2) in HCutR. - unfold nformula_of_cutting_plane in HCutR. - unfold eval_nformula in HCutR. - unfold RingMicromega.eval_nformula in HCutR. - change (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x)) with eval_pol in HCutR. - unfold eval_op1 in HCutR. - destruct op1 ; simpl in Hop1 ; try discriminate; - rewrite eval_pol_add in HCutR; simpl in HCutR. - + rewrite Z.add_move_0_l in HCutR; rewrite HCutR, Z.opp_involutive; reflexivity. - + now apply Z.le_sub_le_add_r in HCutR. - (**) - - apply (fun H => is_pol_Z0_eval_pol _ H env) in HZ0. - rewrite eval_pol_add, Z.add_move_r, Z.sub_0_l in HZ0. - rewrite HZ0. - apply (eval_Psatz_sound env) in Hf1 ; auto. - apply cutting_plane_sound with (1:= Hf1) in HCutL. - unfold nformula_of_cutting_plane in HCutL. - unfold eval_nformula in HCutL. - unfold RingMicromega.eval_nformula in HCutL. - change (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x)) with eval_pol in HCutL. - unfold eval_op1 in HCutL. - rewrite eval_pol_add in HCutL. simpl in HCutL. - destruct op2 ; simpl in Hop2 ; try discriminate. - + rewrite Z.add_move_r, Z.sub_0_l in HCutL. - now rewrite HCutL, Z.opp_involutive. - + now rewrite <- Z.le_sub_le_add_l in HCutL. - } - revert Hfix. - match goal with - | |- context[?F pf (-z1) z2 = true] => set (FF := F) - end. - intros Hfix. - assert (HH :forall x, -z1 <= x <= z2 -> exists pr, - (In pr pf /\ - ZChecker ((PsubC Z.sub p1 x,Equal) :: l) pr = true)%Z). { - clear HZ0 Hop1 Hop2 HCutL HCutR H0 H1. - revert Hfix. - generalize (-z1). clear z1. intro z1. - revert z1 z2. - induction pf as [|a pf IHpf];simpl ;intros z1 z2 Hfix x **. - - revert Hfix. - now case (Z.gtb_spec); [ | easy ]; intros LT; elim (Zorder.Zlt_not_le _ _ LT); transitivity x. - - flatten_bool. - match goal with [ H' : _ <= x <= _ |- _ ] => rename H' into H0 end. - match goal with [ H' : FF pf (z1 + 1) z2 = true |- _ ] => rename H' into H2 end. - destruct (ZArith_dec.Z_le_lt_eq_dec _ _ (proj1 H0)) as [ LT | -> ]. - 2: exists a; auto. - rewrite <- Z.le_succ_l in LT. - assert (LE: (Z.succ z1 <= x <= z2)%Z) by intuition. - elim IHpf with (2:=H2) (3:= LE). - + intros x0 ?. - exists x0 ; split;tauto. - + intros until 1. - apply H ; auto. - cbv [ltof] in *. - cbn [bdepth] in *. - eauto using Nat.lt_le_trans, le_n_S, Nat.le_max_r. - } - (*/asser *) - destruct (HH _ H1) as [pr [Hin Hcheker]]. - assert (make_impl (eval_nformula env) ((PsubC Z.sub p1 (eval_pol env p1),Equal) :: l) False) as H2. { - eapply (H pr) ;auto. - apply in_bdepth ; auto. - } - rewrite <- make_conj_impl in H2. - apply H2. - rewrite make_conj_cons. - split ;auto. - unfold eval_nformula. - unfold RingMicromega.eval_nformula. - simpl. - rewrite (RingMicromega.PsubC_ok Zsor ZSORaddon). - unfold eval_pol. ring. - -- discriminate. - * (* No cutting plane *) - intros H0 H1 H2 env. - rewrite <- make_conj_impl. - intros H3. - apply eval_Psatz_sound with (2:= Hf1) in H3. - apply genCuttingPlaneNone with (2:= H3) ; auto. - + (* No Cutting plane (bis) *) - intros H0 H1 env. - rewrite <- make_conj_impl. - intros H2. - apply eval_Psatz_sound with (2:= Hf2) in H2. - apply genCuttingPlaneNone with (2:= H2) ; auto. - - intros l. - unfold ZChecker. - fold ZChecker. - set (fr := (max_var_nformulae l)%positive). - set (z1 := (Pos.succ fr)) in *. - set (t1 := (Pos.succ z1)) in *. - destruct (x <=? fr)%positive eqn:LE ; [|congruence]. - intros H0 env. - set (env':= fun v => if Pos.eqb v z1 - then if Z.leb (env x) 0 then 0 else env x - else if Pos.eqb v t1 - then if Z.leb (env x) 0 then -(env x) else 0 - else env v). - apply (fun H' ck => H _ H' _ ck env') in H0. - + rewrite <- make_conj_impl in *. - intro H1. - rewrite !make_conj_cons in H0. - apply H0 ; repeat split. - * - apply eval_nformula_mk_eq_pos. - unfold env'. - rewrite! Pos.eqb_refl. - replace (x=?z1)%positive with false. - 1:replace (x=?t1)%positive with false. - 1:replace (t1=?z1)%positive with false. - 1:destruct (env x <=? 0); ring. - { unfold t1. - symmetry; apply not_true_iff_false; rewrite Pos.eqb_eq; symmetry; apply Pos.succ_discr. - } - { - unfold t1, z1. - symmetry; apply not_true_iff_false; rewrite Pos.eqb_eq; intros ->. - apply Pos.leb_le, Pos.lt_succ_r in LE; rewrite <-?Pos.succ_lt_mono in *. - pose proof Pos.lt_not_add_l fr 1; rewrite Pos.add_1_r in *; contradiction. - } - { - unfold z1. - symmetry; apply not_true_iff_false; rewrite Pos.eqb_eq; intros ->. - apply Pos.leb_le, Pos.lt_succ_r in LE; rewrite <-?Pos.succ_lt_mono in *. - case (Pos.lt_irrefl _ LE). - } - * - apply eval_nformula_bound_var. - unfold env'. - rewrite! Pos.eqb_refl. - destruct (env x <=? 0) eqn:EQ. - -- compute. congruence. - -- rewrite Z.leb_gt in EQ. - apply Z.ge_le_iff, Z.lt_le_incl; trivial. - * - apply eval_nformula_bound_var. - unfold env'. - rewrite! Pos.eqb_refl. - replace (t1 =? z1)%positive with false. - -- destruct (env x <=? 0) eqn:EQ. - ++ rewrite Z.leb_le in EQ. - apply Z.ge_le_iff. rewrite Z.opp_le_mono, Z.opp_involutive; trivial. - ++ compute; congruence. - -- unfold t1. - clear. - symmetry; apply not_true_iff_false; rewrite Pos.eqb_eq; symmetry; apply Pos.succ_discr. - * - rewrite (agree_env_eval_nformulae _ env') in H1;auto. - unfold agree_env; intros x0 H2. - unfold env'. - replace (x0 =? z1)%positive with false. - 1:replace (x0 =? t1)%positive with false. - 1:reflexivity. - { - unfold t1, z1. - symmetry; apply not_true_iff_false; rewrite Pos.eqb_eq; intros ->. - apply Pos.lt_succ_r in H2; rewrite <-?Pos.succ_lt_mono in *. - pose proof Pos.lt_not_add_l (max_var_nformulae l) 1; rewrite Pos.add_1_r in *; contradiction. - } - { - unfold z1, fr in *. - symmetry; apply not_true_iff_false; rewrite Pos.eqb_eq; intros ->. - apply Pos.lt_succ_r in H2; rewrite <-?Pos.succ_lt_mono in *. - case (Pos.lt_irrefl _ H2). - } - + unfold ltof. - simpl. - apply Nat.lt_succ_diag_r. + { eapply IHw1 in El; auto. + eapply cutting_plane_sound in Hcp1; eauto. + rewrite make_conj_cons; eauto. } + { eapply IHw2 in Er; auto. + eapply cutting_plane_sound in Hcp2; eauto. + rewrite make_conj_cons; eauto. } } + { (* EnumProof *) inversion E. } + { (* ExProof *) + destruct (Pos.leb_spec x (max_var_nformulae l)); [|discriminate]. + let fr := constr:((max_var_nformulae l)%positive) in + let z1 := constr:(Pos.succ fr) in + let t1 := constr:(Pos.succ z1) in + let env':= constr:(fun v => + if Pos.eqb v z1 then if Z.leb (env x) 0 then 0 else env x + else if Pos.eqb v t1 then if Z.leb (env x) 0 then -(env x) else 0 + else env v) in + eapply IHw; try eapply E; try apply PeanoNat.Nat.lt_succ_diag_r; instantiate (1:=env'). + rewrite !make_conj_cons; repeat split; cycle -1. + { rewrite agree_env_eval_nformulae in HX; eauto; []; intros ? ?. + erewrite !(proj2 (Pos.eqb_neq _ _ )); eauto. } + { apply eval_nformula_mk_eq_pos. + rewrite !Pos.eqb_refl, !(proj2 (Pos.eqb_neq _ _ )) by (eauto || symmetry; eauto). + case Z.leb; auto using Z.sub_0_r, Z.sub_opp_r. } + { apply eval_nformula_bound_var. + rewrite !Pos.eqb_refl; case Z.leb_spec; intros EQ; auto. } + { apply eval_nformula_bound_var. + rewrite !Pos.eqb_refl, !(proj2 (Pos.eqb_neq _ _ )) by (eauto || symmetry; eauto). + case Z.leb_spec; intros; auto. + apply Z.le_ge, Z.opp_nonneg_nonpos; auto. } } Qed. Definition ZTautoChecker (f : BFormula (Formula Z) Tauto.isProp) (w: list ZArithProof): bool := @@ -1736,39 +1341,27 @@ Definition ZTautoChecker (f : BFormula (Formula Z) Tauto.isProp) (w: list ZArit Lemma ZTautoChecker_sound : forall f w, ZTautoChecker f w = true -> forall env, eval_bf (Zeval_formula env) f. Proof. - intros f w. - unfold ZTautoChecker. apply (tauto_checker_sound _ _ _ _ eval_nformula). - - apply Zeval_nformula_dec. - - intros t ? env. - unfold eval_nformula. unfold RingMicromega.eval_nformula. - destruct t. - apply (check_inconsistent_sound Zsor ZSORaddon) ; auto. - - unfold Zdeduce. intros ? ? ? H **. revert H. - apply (nformula_plus_nformula_correct Zsor ZSORaddon); auto. - - - intros ? ? ? ? H. - rewrite normalise_correct in H. - rewrite Zeval_formula_compat; auto. - - - intros ? ? ? ? H. - rewrite negate_correct in H ; auto. - rewrite Tauto.hold_eNOT. - rewrite Zeval_formula_compat; auto. - - intros t w0. - unfold eval_tt. - intros H env. - rewrite (make_impl_map (eval_nformula env)). - + eapply ZChecker_sound; eauto. - + tauto. + { apply Zeval_nformula_dec. } + { intros [] ? ?; apply (check_inconsistent_sound Zsor ZSORaddon) ; auto. } + { intros * H **; revert H. + apply (nformula_plus_nformula_correct Zsor ZSORaddon); auto. } + { intros * H. rewrite normalise_correct in H. apply Zeval_formula_compat, H. } + { intros * H. rewrite negate_correct in H. + rewrite Tauto.hold_eNOT, Zeval_formula_compat; auto. } + { intros * H env. + rewrite (make_impl_map (eval_nformula env)) by reflexivity. + eapply ZChecker_sound, H. } Qed. + + Fixpoint xhyps_of_pt (base:nat) (acc : list nat) (pt:ZArithProof) : list nat := match pt with | DoneProof => acc | RatProof c pt => xhyps_of_pt (S base ) (xhyps_of_psatz base acc c) pt | CutProof c pt => xhyps_of_pt (S base ) (xhyps_of_psatz base acc c) pt | SplitProof p pt1 pt2 => xhyps_of_pt (S base) (xhyps_of_pt (S base) acc pt1) pt2 - | EnumProof c1 c2 l => + | deprecated_EnumProof c1 c2 l => let acc := xhyps_of_psatz base (xhyps_of_psatz base acc c2) c1 in List.fold_left (xhyps_of_pt (S base)) l acc | ExProof _ pt => xhyps_of_pt (S (S (S base ))) acc pt @@ -1782,8 +1375,6 @@ Open Scope Z_scope. Definition make_impl := Refl.make_impl. Definition make_conj := Refl.make_conj. -From Stdlib Require VarMap. - (*Definition varmap_type := VarMap.t Z. *) Definition env := PolEnv Z. Definition node := @VarMap.Branch Z. @@ -1799,3 +1390,122 @@ Definition prod_pos_nat := prod positive nat. #[deprecated(use=Z.to_N, since="9.0")] Notation n_of_Z := Z.to_N (only parsing). + +Require Import PeanoNat Wf_nat. + +#[deprecated(since="9.1")] +Fixpoint vars (jmp : positive) (p : Pol Z) : list positive := + match p with + | Pc c => nil + | Pinj j p => vars (Pos.add j jmp) p + | PX p j q => jmp::(vars jmp p)++vars (Pos.succ jmp) q + end. + +#[deprecated(since="9.1")] +Lemma max_var_le : forall p v, + (v <= max_var v p)%positive. +Proof. + intros p; induction p as [?|p ? IHp|? IHp1 ? ? IHp2]; simpl. + - intros. + apply Pos.le_refl. + - intros v. + specialize (IHp (p+v)%positive). + eapply Pos.le_trans ; eauto. + assert (xH + v <= p + v)%positive. + { apply Pos.add_le_mono. + - apply Pos.le_1_l. + - apply Pos.le_refl. + } + eapply Pos.le_trans ; eauto. + apply pos_le_add. + - intros v. + apply Pos.max_case_strong;intros ; auto. + specialize (IHp2 (Pos.succ v)%positive). + eapply Pos.le_trans ; eauto. +Qed. + +Local Set Warnings "-deprecated". + +#[deprecated(since="9.1")] +Lemma max_var_correct : forall p j v, + In v (vars j p) -> Pos.le v (max_var j p). +Proof. + intros p; induction p; simpl. + - tauto. + - auto. + - intros j v H. + rewrite in_app_iff in H. + destruct H as [H |[ H | H]]. + + subst. + apply Pos.max_case_strong;intros ; auto. + * apply max_var_le. + * eapply Pos.le_trans ; eauto. + apply max_var_le. + + apply Pos.max_case_strong;intros ; auto. + eapply Pos.le_trans ; eauto. + + apply Pos.max_case_strong;intros ; auto. + eapply Pos.le_trans ; eauto. +Qed. + +#[deprecated(since="9.1")] +Lemma max_var_nformulae_correct_aux : forall l p o v, + In (p,o) l -> In v (vars xH p) -> Pos.le v (fold_left F l 1)%positive. +Proof. +intros l p o v H H0. +generalize 1%positive as acc. +revert p o v H H0. +induction l as [|a l IHl]. +- simpl. tauto. +- simpl. + intros p o v H H0 ?. + destruct H ; subst. + + unfold F at 2. + simpl. + apply max_var_correct in H0. + apply max_var_nformulae_mono_aux. + apply Pos.max_case_strong;intros ; auto. + eapply Pos.le_trans ; eauto. + + eapply IHl ; eauto. +Qed. + +#[deprecated(since="9.1")] +Lemma max_var_nformalae_correct : forall l p o v, + In (p,o) l -> In v (vars xH p) -> Pos.le v (max_var_nformulae l)%positive. +Proof. + intros l p o v. + apply max_var_nformulae_correct_aux. +Qed. + + +#[deprecated(since="9.1")] +Fixpoint bdepth (pf : ZArithProof) : nat := +match pf with + | DoneProof => O + | RatProof _ p => S (bdepth p) + | CutProof _ p => S (bdepth p) + | SplitProof _ p1 p2 => S (Nat.max (bdepth p1) (bdepth p2)) + | EnumProof _ _ l => S (List.fold_right (fun pf x => Nat.max (bdepth pf) x) O l) + | ExProof _ p => S (bdepth p) +end. + +#[deprecated(since="9.1")] +Lemma ltof_bdepth_split_l : + forall p pf1 pf2, + ltof ZArithProof bdepth pf1 (SplitProof p pf1 pf2). +Proof. + intros. + unfold ltof. simpl. + rewrite Nat.lt_succ_r. + apply Nat.le_max_l. +Qed. + +#[deprecated(since="9.1")] +Lemma ltof_bdepth_split_r : + forall p pf1 pf2, + ltof ZArithProof bdepth pf2 (SplitProof p pf1 pf2). +Proof. + intros. + unfold ltof. simpl. + rewrite Nat.lt_succ_r. + apply Nat.le_max_r. +Qed. diff --git a/theories/micromega/ZifyInst.v b/theories/micromega/ZifyInst.v index a6f066fe8c..5bbb375aa4 100644 --- a/theories/micromega/ZifyInst.v +++ b/theories/micromega/ZifyInst.v @@ -12,7 +12,7 @@ Each instance is registered using a Add 'class' 'name_of_instance'. *) -From Stdlib Require Import Arith BinInt BinNat Zeven Znat Nnat. +From Stdlib Require Import BinInt BinNat Znat Nnat. From Stdlib Require Import ZifyClasses. Declare ML Module "rocq-runtime.plugins.zify". Local Open Scope Z_scope. @@ -581,9 +581,15 @@ Instance Op_Z_div2 : UnOp Z.div2 := { TUOp x := x / 2 ; TUOpInj := Z.div2_div }. Add Zify UnOp Op_Z_div2. +Local Lemma Zquot2_quot n : Z.quot2 n = n ÷ 2. +Proof. + rewrite Z.quot_div, Z.mul_1_r, <-Z.div2_div by inversion 1. + case n; trivial; induction p; trivial. +Qed. + #[global] Instance Op_Z_quot2 : UnOp Z.quot2 := - { TUOp x := Z.quot x 2 ; TUOpInj := Zeven.Zquot2_quot }. + { TUOp x := Z.quot x 2 ; TUOpInj := Zquot2_quot }. Add Zify UnOp Op_Z_quot2. Lemma of_nat_to_nat_eq x : Z.of_nat (Z.to_nat x) = Z.max 0 x. diff --git a/theories/micromega/ZifyN.v b/theories/micromega/ZifyN.v index 69a06d23c3..6b22d6882f 100644 --- a/theories/micromega/ZifyN.v +++ b/theories/micromega/ZifyN.v @@ -10,8 +10,8 @@ (* Instances of [ZifyClasses] for dealing with advanced [N] operators. *) -From Stdlib Require Import BinNat BinInt Znat Zdiv. -From Stdlib Require Import ZifyClasses ZifyInst Zify. +From Stdlib Require Import BinNat BinInt Znat. +From Stdlib.micromega Require Import ZifyClasses ZifyInst Zify SatDivMod. Ltac zify_convert_to_euclidean_division_equations_flag ::= constr:(true). @@ -35,7 +35,26 @@ Instance Op_N_pow : BinOp N.pow := {| TBOp := Z.pow ; TBOpInj := N2Z.inj_pow|}. Add Zify BinOp Op_N_pow. -#[local] Open Scope Z_scope. +#[local] +Open Scope Z_scope. + +#[local] +Lemma Z_div_nonneg_nonneg a b : 0 <= a -> 0 <= b -> 0 <= a / b. +Proof. + intros H; pose proof Z.div_pos a b H. + case (Z.ltb_spec 0 b); auto. + intros A B; rewrite (Z.le_antisymm _ _ A B). + case a; cbv; congruence. +Qed. + +#[local] +Lemma Z_mod_nonneg_nonneg a b : 0 <= a -> 0 <= b -> 0 <= a mod b. +Proof. + case (Z.ltb_spec 0 b); intros. + { apply Z.mod_pos_bound; trivial. } + rewrite <-(Z.le_antisymm 0 b); trivial. + case a in *; cbv in *; congruence. +Qed. #[global] Instance SatDiv : Saturate Z.div := diff --git a/theories/micromega/ZifyNat.v b/theories/micromega/ZifyNat.v index 6c32015ed2..ea752a3ab4 100644 --- a/theories/micromega/ZifyNat.v +++ b/theories/micromega/ZifyNat.v @@ -10,8 +10,8 @@ (* Instances of [ZifyClasses] for dealing with advanced [nat] operators. *) -From Stdlib Require Import BinInt Znat Zdiv. -From Stdlib Require Import ZifyClasses ZifyInst Zify. +From Stdlib Require Import BinInt Znat. +From Stdlib.micromega Require Import ZifyClasses ZifyInst Zify SatDivMod. Ltac zify_convert_to_euclidean_division_equations_flag ::= constr:(true). @@ -34,25 +34,3 @@ Add Zify BinOp Op_div. Instance Op_pow : BinOp Nat.pow := {| TBOp := Z.pow ; TBOpInj := Nat2Z.inj_pow |}. Add Zify BinOp Op_pow. - -#[local] Open Scope Z_scope. - -#[global] -Instance SatDiv : Saturate Z.div := - {| - PArg1 := fun x => 0 <= x; - PArg2 := fun y => 0 <= y; - PRes := fun _ _ r => 0 <= r; - SatOk := Z_div_nonneg_nonneg - |}. -Add Zify Saturate SatDiv. - -#[global] -Instance SatMod : Saturate Z.modulo := - {| - PArg1 := fun x => 0 <= x; - PArg2 := fun y => 0 <= y; - PRes := fun _ _ r => 0 <= r; - SatOk := Z_mod_nonneg_nonneg - |}. -Add Zify Saturate SatMod. diff --git a/theories/omega/PreOmega.v b/theories/omega/PreOmega.v index a887994cff..530d085488 100644 --- a/theories/omega/PreOmega.v +++ b/theories/omega/PreOmega.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -From Stdlib Require Import Arith BinInt BinNat Znat Nnat. +From Stdlib Require Import BinInt BinNat Znat Nnat. Local Open Scope Z_scope. diff --git a/theories/setoid_ring/Field_tac.v b/theories/setoid_ring/Field_tac.v index 3b9f9ae59f..4416eba3ef 100644 --- a/theories/setoid_ring/Field_tac.v +++ b/theories/setoid_ring/Field_tac.v @@ -8,8 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -From Stdlib Require Import Ring_tac BinList Ring_polynom InitialRing. -From Stdlib Require Export Field_theory. +From Stdlib.setoid_ring Require Import Ring_tac BinList Ring_polynom InitialRing Field_theory. +Export Field_theory. (* syntaxification *) (* We do not assume that Cst recognizes the rO and rI terms as constants, as *) diff --git a/theories/setoid_ring/Field_theory.v b/theories/setoid_ring/Field_theory.v index ea8df5921e..97db79b77c 100644 --- a/theories/setoid_ring/Field_theory.v +++ b/theories/setoid_ring/Field_theory.v @@ -8,11 +8,10 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -From Stdlib Require Ring. -Import Ring_polynom Ring_tac Ring_theory InitialRing Setoid List Morphisms. +From Corelib Require Import RelationClasses Setoid Morphisms. From Stdlib Require Import BinNat BinInt. +From Stdlib.setoid_ring Require Import Ring_base Ring_polynom Ring_tac Ring_theory InitialRing. Set Implicit Arguments. -(* Set Universe Polymorphism. *) Section MakeFieldPol. @@ -778,24 +777,24 @@ 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 (e1 @ l) rO - | e1 :: l1 => ~ req (e1 @ l) rO /\ PCond l l1 + | cons e1 nil => ~ req (e1 @ l) rO + | cons e1 l1 => ~ req (e1 @ l) rO /\ PCond l l1 end. Theorem PCond_cons l a l1 : - PCond l (a :: l1) <-> ~ a @ l == 0 /\ PCond l l1. + PCond l (cons a l1) <-> ~ a @ l == 0 /\ PCond l l1. Proof. destruct l1. - simpl. split; [split|destruct 1]; trivial. - reflexivity. Qed. -Theorem PCond_cons_inv_l l a l1 : PCond l (a::l1) -> ~ a @ l == 0. +Theorem PCond_cons_inv_l l a l1 : PCond l (cons a l1) -> ~ a @ l == 0. Proof. rewrite PCond_cons. now destruct 1. Qed. -Theorem PCond_cons_inv_r l a l1 : PCond l (a :: l1) -> PCond l l1. +Theorem PCond_cons_inv_r l a l1 : PCond l (cons a l1) -> PCond l l1. Proof. rewrite PCond_cons. now destruct 1. Qed. diff --git a/theories/setoid_ring/ZArithRing.v b/theories/setoid_ring/ZArithRing.v index 54255c8b91..1407b03c1e 100644 --- a/theories/setoid_ring/ZArithRing.v +++ b/theories/setoid_ring/ZArithRing.v @@ -8,9 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -From Stdlib Require Export Ring. From Stdlib Require Import BinInt. -From Stdlib Require Import Zpow_def. +From Stdlib.setoid_ring Require Export Ring. Import InitialRing. @@ -50,6 +49,15 @@ Ltac Zpower_neg := Local Lemma Private_proj1_eqb_eq x y : Z.eqb x y = true -> x = y. Proof. apply Z.eqb_eq. Qed. +Lemma Zpower_theory : power_theory 1%Z Z.mul (@eq Z) Z.of_N Z.pow. +Proof. + constructor. intros z n. + destruct n as [|p];simpl;trivial. + unfold Z.pow_pos. + rewrite <- (Z.mul_1_r (pow_pos _ _ _)). generalize 1%Z. + induction p as [p IHp|p IHp|]; simpl; intros; rewrite ?IHp, ?Z.mul_assoc; trivial. +Qed. + Add Ring Zr : Zth (decidable Private_proj1_eqb_eq, constants [Zcst], preprocess [Zpower_neg;unfold Z.succ], power_tac Zpower_theory [Zpow_tac], From c0f8ee33fbcce68fbce4ba06909874f3bc833c59 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 12 Jun 2025 11:29:09 -0400 Subject: [PATCH 2/2] [CI] Add overlay --- .nix/config.nix | 1 + 1 file changed, 1 insertion(+) diff --git a/.nix/config.nix b/.nix/config.nix index 06a3619a3e..8b3c732353 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -216,6 +216,7 @@ with builtins; with (import {}).lib; # for a complete list of Coq packages available in Nix # * : is such that this will use the branch # from https://github.com// + vst.override.version = "andres-erbsen:use-RelationClasses"; }; common-bundles = { bignums.override.version = "master";