Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

ZArith + other : favor the use of modern names instead of compat nota…

…tions

 - For instance, refl_equal --> eq_refl
 - Npos, Zpos, Zneg now admit more uniform qualified aliases
   N.pos, Z.pos, Z.neg.
 - A new module BinInt.Pos2Z with results about injections from
   positive to Z
 - A result about Z.pow pushed in the generic layer
 - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l}
 - Using tactic Z.le_elim instead of Zle_lt_or_eq
 - Some cleanup in ring, field, micromega
   (use of "Equivalence", "Proper" ...)
 - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp)
 - In ZMake and ZMake, functor parameters are now named NN and ZZ
   instead of N and Z for avoiding confusions

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
commit fc2613e871dffffa788d90044a81598f671d0a3b 1 parent f93f073
letouzey authored
Showing with 5,779 additions and 6,911 deletions.
  1. +14 −14 doc/RecTutorial/RecTutorial.tex
  2. +7 −7 doc/RecTutorial/RecTutorial.v
  3. +8 −8 doc/faq/FAQ.tex
  4. +7 −7 doc/faq/interval_discr.v
  5. +1 −1  doc/refman/Classes.tex
  6. +1 −1  doc/refman/Natural.tex
  7. +1 −1  doc/refman/Omega.tex
  8. +1 −1  doc/refman/Polynom.tex
  9. +1 −1  doc/refman/Program.tex
  10. +1 −1  doc/refman/RefMan-coi.tex
  11. +7 −7 doc/refman/RefMan-gal.tex
  12. +20 −20 doc/refman/RefMan-lib.tex
  13. +3 −3 doc/refman/RefMan-ltac.tex
  14. +1 −1  doc/refman/RefMan-oth.tex
  15. +3 −3 doc/refman/RefMan-tacex.tex
  16. +3 −3 doc/refman/Setoid.tex
  17. +1 −1  interp/constrextern.ml
  18. +3 −3 plugins/cc/cctac.ml
  19. +3 −3 plugins/extraction/ExtrOcamlZBigInt.v
  20. +1 −1  plugins/extraction/ExtrOcamlZInt.v
  21. +37 −114 plugins/micromega/Env.v
  22. +420 −759 plugins/micromega/EnvRing.v
  23. +1 −1  plugins/micromega/MExtraction.v
  24. +3 −3 plugins/micromega/Psatz.v
  25. +4 −4 plugins/micromega/QMicromega.v
  26. +14 −14 plugins/micromega/RMicromega.v
  27. +21 −27 plugins/micromega/RingMicromega.v
  28. +7 −7 plugins/micromega/ZCoeff.v
  29. +102 −112 plugins/micromega/ZMicromega.v
  30. +12 −9 plugins/micromega/coq_micromega.ml
  31. +17 −17 plugins/nsatz/Nsatz.v
  32. +3 −3 plugins/omega/Omega.v
  33. +113 −153 plugins/omega/OmegaLemmas.v
  34. +173 −178 plugins/omega/PreOmega.v
  35. +30 −27 plugins/omega/coq_omega.ml
  36. +11 −12 plugins/ring/LegacyNArithRing.v
  37. +3 −3 plugins/ring/LegacyZArithRing.v
  38. +2 −4 plugins/ring/Ring_abstract.v
  39. +2 −4 plugins/ring/Ring_normalize.v
  40. +2 −4 plugins/ring/Setoid_ring_normalize.v
  41. +3 −3 plugins/ring/ring.ml
  42. +35 −58 plugins/romega/ReflOmegaCore.v
  43. +7 −7 plugins/rtauto/Bintree.v
  44. +1 −1  plugins/rtauto/refl_tauto.ml
  45. +4 −4 plugins/setoid_ring/ArithRing.v
  46. +31 −44 plugins/setoid_ring/BinList.v
  47. +12 −13 plugins/setoid_ring/Cring.v
  48. +2 −2 plugins/setoid_ring/Field_tac.v
  49. +84 −99 plugins/setoid_ring/Field_theory.v
  50. +17 −17 plugins/setoid_ring/InitialRing.v
  51. +2 −3 plugins/setoid_ring/Integral_domain.v
  52. +17 −16 plugins/setoid_ring/Ncring.v
  53. +21 −33 plugins/setoid_ring/Ncring_initial.v
  54. +36 −73 plugins/setoid_ring/Ncring_polynom.v
  55. +4 −4 plugins/setoid_ring/Ncring_tac.v
  56. +6 −6 plugins/setoid_ring/RealField.v
  57. +181 −375 plugins/setoid_ring/Ring_polynom.v
  58. +4 −3 plugins/setoid_ring/Ring_tac.v
  59. +129 −162 plugins/setoid_ring/Ring_theory.v
  60. +1 −1  plugins/setoid_ring/Rings_Z.v
  61. +2 −2 plugins/setoid_ring/ZArithRing.v
  62. +1 −1  tactics/tactics.ml
  63. +2 −2 test-suite/bugs/closed/shouldsucceed/1414.v
  64. +1 −1  test-suite/bugs/closed/shouldsucceed/1784.v
  65. +1 −1  test-suite/bugs/closed/shouldsucceed/1844.v
  66. +1 −1  test-suite/bugs/closed/shouldsucceed/1935.v
  67. +2 −2 test-suite/bugs/closed/shouldsucceed/2127.v
  68. +3 −3 test-suite/complexity/ring2.v
  69. +1 −1  test-suite/ideal-features/eapply_evar.v
  70. +5 −5 test-suite/micromega/example.v
  71. +9 −9 test-suite/micromega/square.v
  72. +13 −13 test-suite/success/Hints.v
  73. +2 −2 test-suite/success/MatchFail.v
  74. +8 −8 test-suite/success/OmegaPre.v
  75. +2 −2 test-suite/success/ProgramWf.v
  76. +8 −8 test-suite/success/ROmegaPre.v
  77. +5 −5 test-suite/success/RecTutorial.v
  78. +1 −1  test-suite/success/Scopes.v
  79. +3 −3 test-suite/success/apply.v
  80. +5 −5 test-suite/success/decl_mode.v
  81. +2 −2 test-suite/success/fix.v
  82. +1 −1  test-suite/success/searchabout.v
  83. +14 −14 test-suite/success/specialize.v
  84. +1 −1  test-suite/success/unicode_utf8.v
  85. +1 −1  theories/Arith/Compare_dec.v
  86. +1 −1  theories/Arith/Factorial.v
  87. +2 −2 theories/Bool/Bool.v
  88. +2 −2 theories/FSets/FSetBridge.v
  89. +4 −4 theories/FSets/FSetEqProperties.v
  90. +2 −4 theories/FSets/FSetFacts.v
  91. +1 −1  theories/FSets/FSetProperties.v
  92. +9 −9 theories/Init/Datatypes.v
  93. +4 −4 theories/Init/Logic_Type.v
  94. +1 −1  theories/Init/Notations.v
  95. +9 −9 theories/Init/Peano.v
  96. +13 −13 theories/Init/Specif.v
  97. +10 −19 theories/Lists/List.v
  98. +1 −1  theories/Lists/ListTactics.v
  99. +13 −14 theories/Lists/StreamMemo.v
  100. +7 −7 theories/Logic/ClassicalFacts.v
  101. +1 −1  theories/Logic/Classical_Prop.v
  102. +2 −2 theories/Logic/Diaconescu.v
  103. +6 −6 theories/Logic/EqdepFacts.v
  104. +12 −12 theories/Logic/Eqdep_dec.v
  105. +1 −1  theories/Logic/ProofIrrelevanceFacts.v
  106. +4 −4 theories/MSets/MSetEqProperties.v
  107. +2 −2 theories/MSets/MSetPositive.v
  108. +1 −1  theories/MSets/MSetProperties.v
  109. +1 −1  theories/MSets/MSetRBT.v
  110. +21 −21 theories/NArith/BinNat.v
  111. +46 −42 theories/NArith/BinNatDef.v
  112. +153 −288 theories/NArith/Ndec.v
  113. +91 −90 theories/NArith/Ndigits.v
  114. +27 −27 theories/NArith/Ndist.v
  115. +77 −84 theories/Numbers/BigNumPrelude.v
  116. +17 −27 theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
  117. +6 −6 theories/Numbers/Cyclic/Abstract/NZCyclic.v
  118. +24 −24 theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
  119. +55 −58 theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
  120. +14 −14 theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
  121. +135 −135 theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
  122. +39 −39 theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
  123. +92 −92 theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
  124. +43 −43 theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
  125. +193 −198 theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
  126. +12 −12 theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
  127. +1 −1  theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
  128. +297 −310 theories/Numbers/Cyclic/Int31/Cyclic31.v
  129. +8 −8 theories/Numbers/Cyclic/Int31/Int31.v
  130. +1 −1  theories/Numbers/Cyclic/Int31/Ring31.v
  131. +94 −95 theories/Numbers/Cyclic/ZModulo/ZModulo.v
  132. +1 −1  theories/Numbers/Integer/Abstract/ZBits.v
  133. +1 −1  theories/Numbers/Integer/Abstract/ZDivFloor.v
  134. +11 −0 theories/Numbers/Integer/Abstract/ZPow.v
  135. +4 −4 theories/Numbers/Integer/BigZ/BigZ.v
  136. +226 −226 theories/Numbers/Integer/BigZ/ZMake.v
  137. +1 −1  theories/Numbers/Integer/Binary/ZBinary.v
  138. +1 −1  theories/Numbers/Integer/NatPairs/ZNatPairs.v
  139. +2 −2 theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
  140. +1 −1  theories/Numbers/NatInt/NZAxioms.v
  141. +2 −2 theories/Numbers/NatInt/NZMulOrder.v
  142. +1 −1  theories/Numbers/Natural/Abstract/NBits.v
  143. +1 −1  theories/Numbers/Natural/BigN/BigN.v
  144. +176 −186 theories/Numbers/Natural/BigN/NMake.v
  145. +59 −59 theories/Numbers/Natural/BigN/Nbasic.v
  146. +2 −2 theories/Numbers/Natural/Binary/NBinary.v
  147. +4 −4 theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
  148. +4 −4 theories/Numbers/Rational/BigQ/BigQ.v
  149. +241 −242 theories/Numbers/Rational/BigQ/QMake.v
  150. +12 −11 theories/PArith/BinPos.v
  151. +10 −9 theories/PArith/Pnat.v
  152. +1 −1  theories/Program/Subset.v
  153. +101 −152 theories/QArith/QArith_base.v
  154. +12 −12 theories/QArith/Qabs.v
  155. +9 −9 theories/QArith/Qcanon.v
  156. +2 −2 theories/QArith/Qfield.v
  157. +35 −51 theories/QArith/Qpower.v
  158. +66 −98 theories/QArith/Qreduction.v
  159. +11 −11 theories/QArith/Qround.v
  160. +1 −1  theories/Reals/AltSeries.v
  161. +1 −1  theories/Reals/Exp_prop.v
  162. +38 −38 theories/Reals/RIneq.v
  163. +6 −6 theories/Reals/R_Ifp.v
  164. +1 −1  theories/Reals/Ranalysis2.v
  165. +2 −2 theories/Reals/Raxioms.v
  166. +2 −2 theories/Reals/Rbasic_fun.v
  167. +7 −7 theories/Reals/Rderiv.v
  168. +51 −55 theories/Reals/Rfunctions.v
  169. +1 −1  theories/Reals/RiemannInt_SF.v
  170. +2 −2 theories/Reals/Rlimit.v
  171. +3 −3 theories/Reals/Rpower.v
  172. +5 −5 theories/Reals/Rseries.v
  173. +1 −1  theories/Reals/Rsqrt_def.v
  174. +2 −2 theories/Reals/Rtopology.v
  175. +2 −2 theories/Reals/Rtrigo_alt.v
  176. +1 −1  theories/Reals/Rtrigo_calc.v
  177. +6 −6 theories/Reals/Rtrigo_def.v
  178. +5 −5 theories/Reals/Rtrigo_fun.v
  179. +2 −2 theories/Reals/Rtrigo_reg.v
  180. +5 −5 theories/Reals/SeqProp.v
  181. +1 −1  theories/Reals/Sqrt_reg.v
  182. +3 −3 theories/Relations/Relation_Operators.v
  183. +1 −1  theories/Sorting/PermutSetoid.v
  184. +6 −6 theories/Strings/Ascii.v
  185. +3 −3 theories/Structures/DecidableTypeEx.v
  186. +76 −84 theories/Structures/OrderedTypeEx.v
  187. +1 −1  theories/Unicode/Utf8.v
  188. +1 −1  theories/Wellfounded/Lexicographic_Product.v
  189. +408 −234 theories/ZArith/BinInt.v
  190. +129 −116 theories/ZArith/BinIntDef.v
  191. +8 −8 theories/ZArith/Int.v
  192. +5 −5 theories/ZArith/Wf_Z.v
  193. +29 −54 theories/ZArith/ZArith_dec.v
  194. +4 −4 theories/ZArith/Zabs.v
  195. +1 −1  theories/ZArith/Zbool.v
  196. +3 −3 theories/ZArith/Zcompare.v
  197. +3 −3 theories/ZArith/Zcomplements.v
  198. +15 −15 theories/ZArith/Zdigits.v
  199. +33 −33 theories/ZArith/Zdiv.v
  200. +2 −2 theories/ZArith/Zeven.v
  201. +108 −131 theories/ZArith/Zgcd_alt.v
  202. +47 −46 theories/ZArith/Zhints.v
  203. +29 −31 theories/ZArith/Zlogarithm.v
  204. +33 −84 theories/ZArith/Zmax.v
  205. +25 −63 theories/ZArith/Zmin.v
  206. +3 −2 theories/ZArith/Zmisc.v
  207. +32 −12 theories/ZArith/Znat.v
  208. +129 −151 theories/ZArith/Znumtheory.v
  209. +7 −5 theories/ZArith/Zorder.v
  210. +1 −1  theories/ZArith/Zpow_alt.v
  211. +1 −1  theories/ZArith/Zpow_def.v
  212. +5 −5 theories/ZArith/Zpow_facts.v
  213. +6 −6 theories/ZArith/Zpower.v
  214. +133 −216 theories/ZArith/Zquot.v
  215. +29 −30 theories/ZArith/Zsqrt_compat.v
  216. +8 −11 theories/ZArith/Zwf.v
View
28 doc/RecTutorial/RecTutorial.tex
@@ -560,11 +560,11 @@ \subsection{The propositional equality type.} \label{equality}
\begin{alltt}
Print eq.
\it{} Inductive eq (A : Type) (x : A) : A \arrow{} Prop :=
- refl_equal : x = x
+ eq_refl : x = x
For eq: Argument A is implicit
-For refl_equal: Argument A is implicit
+For eq_refl: Argument A is implicit
For eq: Argument scopes are [type_scope _ _]
-For refl_equal: Argument scopes are [type_scope _]
+For eq_refl: Argument scopes are [type_scope _]
\end{alltt}
Notice also that the first parameter $A$ of \texttt{eq} has type
@@ -581,15 +581,15 @@ \subsection{The propositional equality type.} \label{equality}
reflexivity.
Qed.
-Lemma eq_proof_proof : refl_equal (2*6) = refl_equal (3*4).
+Lemma eq_proof_proof : eq_refl (2*6) = eq_refl (3*4).
Proof.
reflexivity.
Qed.
Print eq_proof_proof.
\it eq_proof_proof =
-refl_equal (refl_equal (3 * 4))
- : refl_equal (2 * 6) = refl_equal (3 * 4)
+eq_refl (eq_refl (3 * 4))
+ : eq_refl (2 * 6) = eq_refl (3 * 4)
\tt
Lemma eq_lt_le : ( 2 < 4) = (3 {\coqle} 4).
@@ -942,10 +942,10 @@ \subsubsection{Example: strong specification of the predecessor function.}
\textbf{| O {\funarrow}}
exist (fun m : nat {\funarrow} 0 = 0 {\coqand} m = 0 {\coqor} 0 = S m) 0
(or_introl (0 = 1)
- (conj (refl_equal 0) (refl_equal 0)))
+ (conj (eq_refl 0) (eq_refl 0)))
\textbf{| S n0 {\funarrow}}
exist (fun m : nat {\funarrow} S n0 = 0 {\coqand} m = 0 {\coqor} S n0 = S m) n0
- (or_intror (S n0 = 0 {\coqand} n0 = 0) (refl_equal (S n0)))
+ (or_intror (S n0 = 0 {\coqand} n0 = 0) (eq_refl (S n0)))
\textbf{end} : {\prodsym} n : nat, \textbf{pred_spec n}
\end{alltt}
@@ -1084,7 +1084,7 @@ \subsubsection{The Equality Type}
\begin{alltt}
fun H : Q a {\funarrow}
match \(\pi\) in (_ = y) return Q y with
- refl_equal {\funarrow} H
+ eq_refl {\funarrow} H
end
\end{alltt}
Notice the header of the \texttt{match} construct.
@@ -1552,13 +1552,13 @@ \subsubsection*{Remark} In this case, the construction of a non-terminating
\begin{alltt}
Definition isingle l := inode l (fun i {\funarrow} ileaf).
-Definition t1 := inode 0 (fun n {\funarrow} isingle (Z_of_nat n)).
+Definition t1 := inode 0 (fun n {\funarrow} isingle (Z.of_nat n)).
Definition t2 :=
inode 0
(fun n : nat {\funarrow}
- inode (Z_of_nat n)
- (fun p {\funarrow} isingle (Z_of_nat (n*p)))).
+ inode (Z.of_nat n)
+ (fun p {\funarrow} isingle (Z.of_nat (n*p)))).
\end{alltt}
@@ -1572,7 +1572,7 @@ \subsubsection*{Remark} In this case, the construction of a non-terminating
Inductive itree_le : itree{\arrow} itree {\arrow} Prop :=
| le_leaf : {\prodsym} t, itree_le ileaf t
| le_node : {\prodsym} l l' s s',
- Zle l l' {\arrow}
+ Z.le l l' {\arrow}
({\prodsym} i, {\exsym} j:nat, itree_le (s i) (s' j)){\arrow}
itree_le (inode l s) (inode l' s').
@@ -1597,7 +1597,7 @@ \subsubsection*{Remark} In this case, the construction of a non-terminating
Inductive itree_le' : itree{\arrow} itree {\arrow} Prop :=
| le_leaf' : {\prodsym} t, itree_le' ileaf t
| le_node' : {\prodsym} l l' s s' g,
- Zle l l' {\arrow}
+ Z.le l l' {\arrow}
({\prodsym} i, itree_le' (s i) (s' (g i))) {\arrow}
itree_le' (inode l s) (inode l' s').
View
14 doc/RecTutorial/RecTutorial.v
@@ -83,7 +83,7 @@ Proof.
Qed.
Print eq_3_3.
-Lemma eq_proof_proof : refl_equal (2*6) = refl_equal (3*4).
+Lemma eq_proof_proof : eq_refl (2*6) = eq_refl (3*4).
Proof.
reflexivity.
Qed.
@@ -241,7 +241,7 @@ Section equality_elimination.
(Q : A -> Type).
Check (fun H : Q a =>
match p in (eq _ y) return Q y with
- refl_equal => H
+ eq_refl => H
end).
End equality_elimination.
@@ -377,18 +377,18 @@ Inductive itree : Set :=
Definition isingle l := inode l (fun i => ileaf).
-Definition t1 := inode 0 (fun n => isingle (Z_of_nat (2*n))).
+Definition t1 := inode 0 (fun n => isingle (Z.of_nat (2*n))).
Definition t2 := inode 0
(fun n : nat =>
- inode (Z_of_nat n)
- (fun p => isingle (Z_of_nat (n*p)))).
+ inode (Z.of_nat n)
+ (fun p => isingle (Z.of_nat (n*p)))).
Inductive itree_le : itree-> itree -> Prop :=
| le_leaf : forall t, itree_le ileaf t
| le_node : forall l l' s s',
- Zle l l' ->
+ Z.le l l' ->
(forall i, exists j:nat, itree_le (s i) (s' j)) ->
itree_le (inode l s) (inode l' s').
@@ -423,7 +423,7 @@ Qed.
Inductive itree_le' : itree-> itree -> Prop :=
| le_leaf' : forall t, itree_le' ileaf t
| le_node' : forall l l' s s' g,
- Zle l l' ->
+ Z.le l l' ->
(forall i, itree_le' (s i) (s' (g i))) ->
itree_le' (inode l s) (inode l' s').
View
16 doc/faq/FAQ.tex
@@ -545,7 +545,7 @@ \subsection{Axioms}
\begin{coq_example*}
Axiom Streicher_K :
forall (A:Type) (x:A) (P: x=x -> Prop),
- P (refl_equal x) -> forall p: x=x, P p.
+ P (eq_refl x) -> forall p: x=x, P p.
\end{coq_example*}
In the general case, axiom $K$ is an independent statement of the
@@ -563,7 +563,7 @@ \subsection{Axioms}
Axiom $K$ is also equivalent to {\em Uniqueness of Reflexive Identity Proofs} \cite{HofStr98}
\begin{coq_example*}
-Axiom UIP_refl : forall (A:Set) (x:A) (p: x=x), p = refl_equal x.
+Axiom UIP_refl : forall (A:Set) (x:A) (p: x=x), p = eq_refl x.
\end{coq_example*}
Axiom $K$ is also equivalent to
@@ -2108,7 +2108,7 @@ \section{Case studies}
Require Import Eqdep_dec.
Require Import Peano_dec.
Theorem K_nat :
- forall (x:nat) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
+ forall (x:nat) (P:x = x -> Prop), P (eq_refl x) -> forall p:x = x, P p.
Proof.
intros; apply K_dec_set with (p := p).
apply eq_nat_dec.
@@ -2139,16 +2139,16 @@ \section{Case studies}
Proof.
induction p using le_ind'; intro q.
replace (le_n n) with
- (eq_rect _ (fun n0 => n <= n0) (le_n n) _ (refl_equal n)).
+ (eq_rect _ (fun n0 => n <= n0) (le_n n) _ eq_refl).
2:reflexivity.
- generalize (refl_equal n).
+ generalize (eq_refl n).
pattern n at 2 4 6 10, q; case q; [intro | intros m l e].
rewrite <- eq_rect_eq_nat; trivial.
contradiction (le_Sn_n m); rewrite <- e; assumption.
replace (le_S n m p) with
- (eq_rect _ (fun n0 => n <= n0) (le_S n m p) _ (refl_equal (S m))).
+ (eq_rect _ (fun n0 => n <= n0) (le_S n m p) _ eq_refl).
2:reflexivity.
- generalize (refl_equal (S m)).
+ generalize (eq_refl (S m)).
pattern (S m) at 1 3 4 6, q; case q; [intro Heq | intros m0 l HeqS].
contradiction (le_Sn_n m); rewrite Heq; assumption.
injection HeqS; intro Heq; generalize l HeqS.
@@ -2536,7 +2536,7 @@ \section{Troubleshooting}
Lemma example_show_existentials : forall a b c:nat, a=b -> b=c -> a=c.
Proof.
intros.
-eapply trans_equal.
+eapply eq_trans.
Show Existentials.
eassumption.
assumption.
View
14 doc/faq/interval_discr.v
@@ -32,16 +32,16 @@ Theorem le_uniqueness_proof : forall (n m : nat) (p q : n <= m), p = q.
Proof.
induction p using le_ind'; intro q.
replace (le_n n) with
- (eq_rect _ (fun n0 => n <= n0) (le_n n) _ (refl_equal n)).
+ (eq_rect _ (fun n0 => n <= n0) (le_n n) _ eq_refl).
2:reflexivity.
- generalize (refl_equal n).
+ generalize (eq_refl n).
pattern n at 2 4 6 10, q; case q; [intro | intros m l e].
rewrite <- eq_rect_eq_nat; trivial.
contradiction (le_Sn_n m); rewrite <- e; assumption.
replace (le_S n m p) with
- (eq_rect _ (fun n0 => n <= n0) (le_S n m p) _ (refl_equal (S m))).
+ (eq_rect _ (fun n0 => n <= n0) (le_S n m p) _ eq_refl).
2:reflexivity.
- generalize (refl_equal (S m)).
+ generalize (eq_refl (S m)).
pattern (S m) at 1 3 4 6, q; case q; [intro Heq | intros m0 l HeqS].
contradiction (le_Sn_n m); rewrite Heq; assumption.
injection HeqS; intro Heq; generalize l HeqS.
@@ -216,7 +216,7 @@ Lemma inj_restrict :
Proof.
intros A f x y z Hfinj Hneqx Hfy Hfx Heq.
assert (f z <> f x).
- apply sym_not_eq.
+ apply not_eq_sym.
intro Heqf.
apply Hneqx.
apply Hfinj.
@@ -292,7 +292,7 @@ destruct (le_lt_dec (f xSn) (f y)) as [Hlefy|Hgefy].
assert (Heq : x = y).
apply Hfinj.
assert (f xSn <> f y).
- apply sym_not_eq.
+ apply not_eq_sym.
intro Heqf.
apply Hneqy.
apply Hfinj.
@@ -302,7 +302,7 @@ assert (Heq : x = y).
apply le_O_n.
apply le_neq_lt; assumption.
assert (f xSn <> f x).
- apply sym_not_eq.
+ apply not_eq_sym.
intro Heqf.
apply Hneqx.
apply Hfinj.
View
2  doc/refman/Classes.tex
@@ -71,7 +71,7 @@
Instance unit_EqDec : EqDec unit :=
{ eqb x y := true ;
eqb_leibniz x y H :=
- match x, y return x = y with tt, tt => refl_equal tt end }.
+ match x, y return x = y with tt, tt => eq_refl tt end }.
\end{coq_example*}
If one does not give all the members in the \texttt{Instance}
View
2  doc/refman/Natural.tex
@@ -158,7 +158,7 @@ \subsubsection*{Implicit proof constructors}
By default, the proposition (or predicate) constructors
\verb=conj=, \verb=or_introl=, \verb=or_intror=, \verb=ex_intro=,
-\verb=exT_intro=, \verb=refl_equal=, \verb=refl_eqT= and \verb=exist=
+\verb=eq_refl= and \verb=exist=
\noindent are declared implicit. Note that declaring implicit the
constructor of a datatype (i.e. an inductive type of type \verb=Set=)
View
2  doc/refman/Omega.tex
@@ -51,7 +51,7 @@
and in expressions of type \verb=Z=, {\tt omega} recognizes
\begin{quote}
-\verb!+, -, *, Zsucc!, and constants.
+\verb!+, -, *, Z.succ!, and constants.
\end{quote}
All expressions of type \verb=nat= or \verb=Z= not built on these
View
2  doc/refman/Polynom.tex
@@ -927,7 +927,7 @@ \subsection{\tt Add Legacy Field
Goal forall x y z:Z, x + 3 + y + y * z = x + 3 + y + z * y.
\end{coq_example}
\begin{coq_example*}
-intros; rewrite (Zmult_comm y z); reflexivity.
+intros; rewrite (Z.mul_comm y z); reflexivity.
Save toto.
\end{coq_example*}
\begin{coq_example}
View
2  doc/refman/Program.tex
@@ -53,7 +53,7 @@
(match x as y return (x = y -> _) with
| 0 => fun H : x = 0 -> t
| S n => fun H : x = S n -> u
- end) (refl_equal n).
+ end) (eq_refl n).
\end{coq_example*}
This permits to get the proper equalities in the context of proof
View
2  doc/refman/RefMan-coi.tex
@@ -277,7 +277,7 @@ \section{Reasoning about infinite objects}
definition.
\begin{coq_example}
CoFixpoint eqproof (s1 s2:Stream A) : EqSt s1 (conc s1 s2) :=
- eqst s1 (conc s1 s2) (refl_equal (hd A (conc s1 s2)))
+ eqst s1 (conc s1 s2) (eq_refl (hd A (conc s1 s2)))
(eqproof (tl A s1) s2).
\end{coq_example}
\begin{coq_eval}
View
14 doc/refman/RefMan-gal.tex
@@ -566,16 +566,16 @@ \subsection{Definition by case analysis
For instance, in the following example:
\begin{coq_example*}
Inductive bool : Type := true : bool | false : bool.
-Inductive eq (A:Type) (x:A) : A -> Prop := refl_equal : eq A x x.
+Inductive eq (A:Type) (x:A) : A -> Prop := eq_refl : eq A x x.
Inductive or (A:Prop) (B:Prop) : Prop :=
| or_introl : A -> or A B
| or_intror : B -> or A B.
Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false)
:= match b as x return or (eq bool x true) (eq bool x false) with
| true => or_introl (eq bool true true) (eq bool true false)
- (refl_equal bool true)
+ (eq_refl bool true)
| false => or_intror (eq bool false true) (eq bool false false)
- (refl_equal bool false)
+ (eq_refl bool false)
end.
\end{coq_example*}
the branches have respective types {\tt or (eq bool true true) (eq
@@ -591,9 +591,9 @@ \subsection{Definition by case analysis
Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false)
:= match b return or (eq bool b true) (eq bool b false) with
| true => or_introl (eq bool true true) (eq bool true false)
- (refl_equal bool true)
+ (eq_refl bool true)
| false => or_intror (eq bool false true) (eq bool false false)
- (refl_equal bool false)
+ (eq_refl bool false)
end.
\end{coq_example*}
@@ -621,9 +621,9 @@ \subsection{Definition by case analysis
For instance, in the following example:
\begin{coq_example*}
-Definition sym_equal (A:Type) (x y:A) (H:eq A x y) : eq A y x :=
+Definition eq_sym (A:Type) (x y:A) (H:eq A x y) : eq A y x :=
match H in eq _ _ z return eq A z x with
- | refl_equal => refl_equal A x
+ | eq_refl => eq_refl A x
end.
\end{coq_example*}
the type of the branch has type {\tt eq~A~x~x} because the third
View
40 doc/refman/RefMan-lib.tex
@@ -220,11 +220,11 @@
equivalent to Leibniz' equality.
\ttindex{eq}
-\ttindex{refl\_equal}
+\ttindex{eq\_refl}
\begin{coq_example*}
Inductive eq (A:Type) (x:A) : A -> Prop :=
- refl_equal : eq A x x.
+ eq_refl : eq A x x.
\end{coq_example*}
\subsubsection[Lemmas]{Lemmas\label{PreludeLemmas}}
@@ -239,8 +239,8 @@
\begin{coq_eval}
Abort.
\end{coq_eval}
-\ttindex{sym\_eq}
-\ttindex{trans\_eq}
+\ttindex{eq\_sym}
+\ttindex{eq\_trans}
\ttindex{f\_equal}
\ttindex{sym\_not\_eq}
\begin{coq_example*}
@@ -248,10 +248,10 @@
Variables A B : Type.
Variable f : A -> B.
Variables x y z : A.
-Theorem sym_eq : x = y -> y = x.
-Theorem trans_eq : x = y -> y = z -> x = z.
+Theorem eq_sym : x = y -> y = x.
+Theorem eq_trans : x = y -> y = z -> x = z.
Theorem f_equal : x = y -> f x = f y.
-Theorem sym_not_eq : x <> y -> y <> x.
+Theorem not_eq_sym : x <> y -> y <> x.
\end{coq_example*}
\begin{coq_eval}
Abort.
@@ -280,7 +280,7 @@
\end{coq_eval}
%Abort (for now predefined eq_rect)
\begin{coq_example*}
-Hint Immediate sym_eq sym_not_eq : core.
+Hint Immediate eq_sym not_eq_sym : core.
\end{coq_example*}
\ttindex{f\_equal$i$}
@@ -864,22 +864,22 @@ \subsection{Survey}
\begin{tabular}{l|l|l|l}
Notation & Interpretation & Precedence & Associativity\\
\hline
-\verb!_ < _! & {\tt Zlt} &&\\
-\verb!x <= y! & {\tt Zle} &&\\
-\verb!_ > _! & {\tt Zgt} &&\\
-\verb!x >= y! & {\tt Zge} &&\\
+\verb!_ < _! & {\tt Z.lt} &&\\
+\verb!x <= y! & {\tt Z.le} &&\\
+\verb!_ > _! & {\tt Z.gt} &&\\
+\verb!x >= y! & {\tt Z.ge} &&\\
\verb!x < y < z! & {\tt x < y \verb!/\! y < z} &&\\
\verb!x < y <= z! & {\tt x < y \verb!/\! y <= z} &&\\
\verb!x <= y < z! & {\tt x <= y \verb!/\! y < z} &&\\
\verb!x <= y <= z! & {\tt x <= y \verb!/\! y <= z} &&\\
-\verb!_ ?= _! & {\tt Zcompare} & 70 & no\\
-\verb!_ + _! & {\tt Zplus} &&\\
-\verb!_ - _! & {\tt Zminus} &&\\
-\verb!_ * _! & {\tt Zmult} &&\\
-\verb!_ / _! & {\tt Zdiv} &&\\
-\verb!_ mod _! & {\tt Zmod} & 40 & no \\
-\verb!- _! & {\tt Zopp} &&\\
-\verb!_ ^ _! & {\tt Zpower} &&\\
+\verb!_ ?= _! & {\tt Z.compare} & 70 & no\\
+\verb!_ + _! & {\tt Z.add} &&\\
+\verb!_ - _! & {\tt Z.sub} &&\\
+\verb!_ * _! & {\tt Z.mul} &&\\
+\verb!_ / _! & {\tt Z.div} &&\\
+\verb!_ mod _! & {\tt Z.modulo} & 40 & no \\
+\verb!- _! & {\tt Z.opp} &&\\
+\verb!_ ^ _! & {\tt Z.pow} &&\\
\end{tabular}
\end{center}
\caption{Definition of the scope for integer arithmetics ({\tt Z\_scope})}
View
6 doc/refman/RefMan-ltac.tex
@@ -607,7 +607,7 @@ \subsubsection{Application}
match x with
context f [S ?X] =>
idtac X; (* To display the evaluation order *)
- assert (p := refl_equal 1 : X=1); (* To filter the case X=1 *)
+ assert (p := eq_refl 1 : X=1); (* To filter the case X=1 *)
let x:= context f[O] in assert (x=O) (* To observe the context *)
end.
Goal True.
@@ -1205,7 +1205,7 @@ \subsection{Deciding type isomorphisms}
Axiom AL_unit : (unit -> A) = A.
Lemma Cons : B = C -> A * B = A * C.
Proof.
-intro Heq; rewrite Heq; apply refl_equal.
+intro Heq; rewrite Heq; reflexivity.
Qed.
End Iso_axioms.
\end{coq_example*}
@@ -1272,7 +1272,7 @@ \subsection{Deciding type isomorphisms}
\begin{coq_example}
Ltac DoCompare n :=
match goal with
- | [ |- (?A = ?A) ] => apply refl_equal
+ | [ |- (?A = ?A) ] => reflexivity
| [ |- (?A * ?B = ?A * ?C) ] =>
apply Cons; let newn := Length B in DoCompare newn
| [ |- (?A * ?B = ?C) ] =>
View
2  doc/refman/RefMan-oth.tex
@@ -266,7 +266,7 @@ \section{Requests to the environment}
Require Import ZArith.
\end{coq_example*}
\begin{coq_example}
-SearchAbout Zmult Zplus "distr".
+SearchAbout Z.mul Z.add "distr".
SearchAbout "+"%Z "*"%Z "distr" -positive -Prop.
SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas.
\end{coq_example}
View
6 doc/refman/RefMan-tacex.tex
@@ -1129,7 +1129,7 @@ \subsection{About the cardinality of the set of natural numbers}
elim (Hy 0); elim (Hy 1); elim (Hy 2); intros;
match goal with
| [_:(?a = ?b),_:(?a = ?c) |- _ ] =>
- cut (b = c); [ discriminate | apply trans_equal with a; auto ]
+ cut (b = c); [ discriminate | transitivity a; auto ]
end.
Qed.
\end{coq_example*}
@@ -1379,7 +1379,7 @@ \subsection{Deciding type isomorphisms}
Axiom AL_unit : (unit -> A) = A.
Lemma Cons : B = C -> A * B = A * C.
Proof.
-intro Heq; rewrite Heq; apply refl_equal.
+intro Heq; rewrite Heq; reflexivity.
Qed.
End Iso_axioms.
\end{coq_example*}
@@ -1439,7 +1439,7 @@ \subsection{Deciding type isomorphisms}
\begin{coq_example}
Ltac DoCompare n :=
match goal with
- | [ |- (?A = ?A) ] => apply refl_equal
+ | [ |- (?A = ?A) ] => reflexivity
| [ |- (?A * ?B = ?A * ?C) ] =>
apply Cons; let newn := Length B in
DoCompare newn
View
6 doc/refman/Setoid.tex
@@ -371,9 +371,9 @@
\begin{cscexample}[Covariance and contravariance]
Suppose that division over real numbers has been defined as a
-morphism of signature \texttt{Zdiv: Zlt ++> Zlt -{}-> Zlt} (i.e.
-\texttt{Zdiv} is increasing in its first argument, but decreasing on the
-second one). Let \texttt{<} denotes \texttt{Zlt}.
+morphism of signature \texttt{Z.div: Z.lt ++> Z.lt -{}-> Z.lt} (i.e.
+\texttt{Z.div} is increasing in its first argument, but decreasing on the
+second one). Let \texttt{<} denotes \texttt{Z.lt}.
Under the hypothesis \texttt{H: x < y} we have
\texttt{k < x / y -> k < x / x}, but not
\texttt{k < y / x -> k < x / x}.
View
2  interp/constrextern.ml
@@ -321,7 +321,7 @@ let make_notation_gen loc ntn mknot mkprim destprim l =
if has_curly_brackets ntn
then expand_curly_brackets loc mknot ntn l
else match ntn,List.map destprim l with
- (* Special case to avoid writing "- 3" for e.g. (Zopp 3) *)
+ (* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *)
| "- _", [Some (Numeral p)] when Bigint.is_strictly_pos p ->
mknot (loc,ntn,([mknot (loc,"( _ )",l)]))
| _ ->
View
6 plugins/cc/cctac.ml
@@ -34,11 +34,11 @@ let _f_equal = constant ["Init";"Logic"] "f_equal"
let _eq_rect = constant ["Init";"Logic"] "eq_rect"
-let _refl_equal = constant ["Init";"Logic"] "refl_equal"
+let _refl_equal = constant ["Init";"Logic"] "eq_refl"
-let _sym_eq = constant ["Init";"Logic"] "sym_eq"
+let _sym_eq = constant ["Init";"Logic"] "eq_sym"
-let _trans_eq = constant ["Init";"Logic"] "trans_eq"
+let _trans_eq = constant ["Init";"Logic"] "eq_trans"
let _eq = constant ["Init";"Logic"] "eq"
View
6 plugins/extraction/ExtrOcamlZBigInt.v
@@ -75,13 +75,13 @@ Extract Constant Z.compare => "Big.compare_case Eq Lt Gt".
Extract Constant Z.of_N => "fun p -> p".
Extract Constant Z.abs_N => "Big.abs".
-(** Zdiv and Zmod are quite complex to define in terms of (/) and (mod).
+(** Z.div and Z.modulo are quite complex to define in terms of (/) and (mod).
For the moment we don't even try *)
(** Test:
Require Import ZArith NArith.
Extraction "/tmp/test.ml"
- Pplus Ppred Pminus Pmult Pcompare Npred Nminus Ndiv Nmod Ncompare
- Zplus Zmult BinInt.Zcompare Z_of_N Zabs_N Zdiv.Zdiv Zmod.
+ Pos.add Pos.pred Pos.sub Pos.mul Pos.compare N.pred N.sub N.div N.modulo N.compare
+ Z.add Z.mul Z.compare Z.of_N Z.abs_N Z.div Z.modulo.
*)
View
2  plugins/extraction/ExtrOcamlZInt.v
@@ -74,7 +74,7 @@ Extract Constant Z.compare =>
Extract Constant Z.of_N => "fun p -> p".
Extract Constant Z.abs_N => "abs".
-(** Zdiv and Zmod are quite complex to define in terms of (/) and (mod).
+(** Z.div and Z.modulo are quite complex to define in terms of (/) and (mod).
For the moment we don't even try *)
View
151 plugins/micromega/Env.v
@@ -12,10 +12,9 @@
(* *)
(************************************************************************)
-Require Import ZArith.
-Require Import Coq.Arith.Max.
-Require Import List.
+Require Import BinInt List.
Set Implicit Arguments.
+Local Open Scope positive_scope.
Section S.
@@ -23,154 +22,78 @@ Section S.
Definition Env := positive -> D.
- Definition jump (j:positive) (e:Env) := fun x => e (Pplus x j).
+ Definition jump (j:positive) (e:Env) := fun x => e (x+j).
- Definition nth (n:positive) (e : Env ) := e n.
+ Definition nth (n:positive) (e:Env) := e n.
- Definition hd (x:D) (e: Env) := nth xH e.
+ Definition hd (e:Env) := nth 1 e.
- Definition tail (e: Env) := jump xH e.
+ Definition tail (e:Env) := jump 1 e.
- Lemma psucc : forall p, (match p with
- | xI y' => xO (Psucc y')
- | xO y' => xI y'
- | 1%positive => 2%positive
- end) = (p+1)%positive.
+ Lemma jump_add i j l x : jump (i + j) l x = jump i (jump j l) x.
Proof.
- destruct p.
- auto with zarith.
- rewrite xI_succ_xO.
- auto with zarith.
- reflexivity.
+ unfold jump. f_equal. apply Pos.add_assoc.
Qed.
- Lemma jump_Pplus : forall i j l,
- forall x, jump (i + j) l x = jump i (jump j l) x.
- Proof.
- unfold jump.
- intros.
- rewrite Pplus_assoc.
- reflexivity.
- Qed.
-
- Lemma jump_simpl : forall p l,
- forall x, jump p l x =
+ Lemma jump_simpl p l x :
+ jump p l x =
match p with
| xH => tail l x
| xO p => jump p (jump p l) x
| xI p => jump p (jump p (tail l)) x
end.
Proof.
- destruct p ; unfold tail ; intros ; repeat rewrite <- jump_Pplus.
- (* xI p = p + p + 1 *)
- rewrite xI_succ_xO.
- rewrite Pplus_diag.
- rewrite <- Pplus_one_succ_r.
- reflexivity.
- (* xO p = p + p *)
- rewrite Pplus_diag.
- reflexivity.
- reflexivity.
+ destruct p; unfold tail; rewrite <- ?jump_add; f_equal;
+ now rewrite Pos.add_diag.
Qed.
- Ltac jump_s :=
- repeat
- match goal with
- | |- context [jump xH ?e] => rewrite (jump_simpl xH)
- | |- context [jump (xO ?p) ?e] => rewrite (jump_simpl (xO p))
- | |- context [jump (xI ?p) ?e] => rewrite (jump_simpl (xI p))
- end.
-
- Lemma jump_tl : forall j l, forall x, tail (jump j l) x = jump j (tail l) x.
+ Lemma jump_tl j l x : tail (jump j l) x = jump j (tail l) x.
Proof.
- unfold tail.
- intros.
- repeat rewrite <- jump_Pplus.
- rewrite Pplus_comm.
- reflexivity.
+ unfold tail. rewrite <- !jump_add. f_equal. apply Pos.add_comm.
Qed.
- Lemma jump_Psucc : forall j l,
- forall x, (jump (Psucc j) l x) = (jump 1 (jump j l) x).
+ Lemma jump_succ j l x : jump (Pos.succ j) l x = jump 1 (jump j l) x.
Proof.
- intros.
- rewrite <- jump_Pplus.
- rewrite Pplus_one_succ_r.
- rewrite Pplus_comm.
- reflexivity.
+ rewrite <- jump_add. f_equal. symmetry. apply Pos.add_1_l.
Qed.
- Lemma jump_Pdouble_minus_one : forall i l,
- forall x, (jump (Pdouble_minus_one i) (tail l)) x = (jump i (jump i l)) x.
+ Lemma jump_pred_double i l x :
+ jump (Pos.pred_double i) (tail l) x = jump i (jump i l) x.
Proof.
- unfold tail.
- intros.
- repeat rewrite <- jump_Pplus.
- rewrite <- Pplus_one_succ_r.
- rewrite Psucc_o_double_minus_one_eq_xO.
- rewrite Pplus_diag.
- reflexivity.
+ unfold tail. rewrite <- !jump_add. f_equal.
+ now rewrite Pos.add_1_r, Pos.succ_pred_double, Pos.add_diag.
Qed.
- Lemma jump_x0_tail : forall p l, forall x, jump (xO p) (tail l) x = jump (xI p) l x.
- Proof.
- intros.
- unfold jump.
- unfold tail.
- unfold jump.
- rewrite <- Pplus_assoc.
- simpl.
- reflexivity.
- Qed.
-
- Lemma nth_spec : forall p l x,
+ Lemma nth_spec p l :
nth p l =
match p with
- | xH => hd x l
+ | xH => hd l
| xO p => nth p (jump p l)
| xI p => nth p (jump p (tail l))
end.
Proof.
- unfold nth.
- destruct p.
- intros.
- unfold jump, tail.
- unfold jump.
- rewrite Pplus_diag.
- rewrite xI_succ_xO.
- simpl.
- reflexivity.
- unfold jump.
- rewrite Pplus_diag.
- reflexivity.
- unfold hd.
- unfold nth.
- reflexivity.
+ unfold hd, nth, tail, jump.
+ destruct p; f_equal; now rewrite Pos.add_diag.
Qed.
-
- Lemma nth_jump : forall p l x, nth p (tail l) = hd x (jump p l).
+ Lemma nth_jump p l : nth p (tail l) = hd (jump p l).
Proof.
- unfold tail.
- unfold hd.
- unfold jump.
- unfold nth.
- intros.
- rewrite Pplus_comm.
- reflexivity.
+ unfold hd, nth, tail, jump. f_equal. apply Pos.add_comm.
Qed.
- Lemma nth_Pdouble_minus_one :
- forall p l, nth (Pdouble_minus_one p) (tail l) = nth p (jump p l).
+ Lemma nth_pred_double p l :
+ nth (Pos.pred_double p) (tail l) = nth p (jump p l).
Proof.
- intros.
- unfold tail.
- unfold nth, jump.
- rewrite Pplus_diag.
- rewrite <- Psucc_o_double_minus_one_eq_xO.
- rewrite Pplus_one_succ_r.
- reflexivity.
+ unfold nth, tail, jump. f_equal.
+ now rewrite Pos.add_1_r, Pos.succ_pred_double, Pos.add_diag.
Qed.
End S.
+Ltac jump_simpl :=
+ repeat
+ match goal with
+ | |- appcontext [jump xH] => rewrite (jump_simpl xH)
+ | |- appcontext [jump (xO ?p)] => rewrite (jump_simpl (xO p))
+ | |- appcontext [jump (xI ?p)] => rewrite (jump_simpl (xI p))
+ end.
View
1,179 plugins/micromega/EnvRing.v
@@ -11,15 +11,10 @@
Set Implicit Arguments.
-Require Import Setoid.
-Require Import BinList.
-Require Import Env.
-Require Import BinPos.
-Require Import BinNat.
-Require Import BinInt.
+Require Import Setoid Morphisms Env BinPos BinNat BinInt.
Require Export Ring_theory.
-Open Local Scope positive_scope.
+Local Open Scope positive_scope.
Import RingSyntax.
Section MakeRingPol.
@@ -30,7 +25,7 @@ Section MakeRingPol.
Variable req : R -> R -> Prop.
(* Ring properties *)
- Variable Rsth : Setoid_Theory R req.
+ Variable Rsth : Equivalence req.
Variable Reqe : ring_eq_ext radd rmul ropp req.
Variable ARth : almost_ring_theory rO rI radd rmul rsub ropp req.
@@ -42,35 +37,55 @@ Section MakeRingPol.
Variable CRmorph : ring_morph rO rI radd rmul rsub ropp req
cO cI cadd cmul csub copp ceqb phi.
- (* Power coefficients *)
+ (* Power coefficients *)
Variable Cpow : Type.
Variable Cp_phi : N -> Cpow.
Variable rpow : R -> Cpow -> R.
Variable pow_th : power_theory rI rmul req Cp_phi rpow.
-
(* R notations *)
Notation "0" := rO. Notation "1" := rI.
- Notation "x + y" := (radd x y). Notation "x * y " := (rmul x y).
- Notation "x - y " := (rsub x y). Notation "- x" := (ropp x).
- Notation "x == y" := (req x y).
+ Infix "+" := radd. Infix "*" := rmul.
+ Infix "-" := rsub. Notation "- x" := (ropp x).
+ Infix "==" := req.
+ Infix "^" := (pow_pos rmul).
(* C notations *)
- Notation "x +! y" := (cadd x y). Notation "x *! y " := (cmul x y).
- Notation "x -! y " := (csub x y). Notation "-! x" := (copp x).
- Notation " x ?=! y" := (ceqb x y). Notation "[ x ]" := (phi x).
-
- (* Usefull tactics *)
- Add Setoid R req Rsth as R_set1.
- Ltac rrefl := gen_reflexivity Rsth.
- Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed.
- Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed.
- Add Morphism ropp : ropp_ext. exact (Ropp_ext Reqe). Qed.
- Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed.
+ Infix "+!" := cadd. Infix "*!" := cmul.
+ Infix "-! " := csub. Notation "-! x" := (copp x).
+ Infix "?=!" := ceqb. Notation "[ x ]" := (phi x).
+
+ (* Useful tactics *)
+ Add Morphism radd : radd_ext. exact (Radd_ext Reqe). Qed.
+ Add Morphism rmul : rmul_ext. exact (Rmul_ext Reqe). Qed.
+ Add Morphism ropp : ropp_ext. exact (Ropp_ext Reqe). Qed.
+ Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed.
Ltac rsimpl := gen_srewrite Rsth Reqe ARth.
+
Ltac add_push := gen_add_push radd Rsth Reqe ARth.
Ltac mul_push := gen_mul_push rmul Rsth Reqe ARth.
+ Ltac add_permut_rec t :=
+ match t with
+ | ?x + ?y => add_permut_rec y || add_permut_rec x
+ | _ => add_push t; apply (Radd_ext Reqe); [|reflexivity]
+ end.
+
+ Ltac add_permut :=
+ repeat (reflexivity ||
+ match goal with |- ?t == _ => add_permut_rec t end).
+
+ Ltac mul_permut_rec t :=
+ match t with
+ | ?x * ?y => mul_permut_rec y || mul_permut_rec x
+ | _ => mul_push t; apply (Rmul_ext Reqe); [|reflexivity]
+ end.
+
+ Ltac mul_permut :=
+ repeat (reflexivity ||
+ match goal with |- ?t == _ => mul_permut_rec t end).
+
+
(* Definition of multivariable polynomials with coefficients in C :
Type [Pol] represents [X1 ... Xn].
The representation is Horner's where a [n] variable polynomial
@@ -117,19 +132,19 @@ Section MakeRingPol.
| _, _ => false
end.
- Notation " P ?== P' " := (Peq P P').
+ Infix "?==" := Peq.
Definition mkPinj j P :=
match P with
| Pc _ => P
- | Pinj j' Q => Pinj ((j + j'):positive) Q
+ | Pinj j' Q => Pinj (j + j') Q
| _ => Pinj j P
end.
Definition mkPinj_pred j P:=
match j with
| xH => P
- | xO j => Pinj (Pdouble_minus_one j) P
+ | xO j => Pinj (Pos.pred_double j) P
| xI j => Pinj (xO j) P
end.
@@ -157,14 +172,14 @@ Section MakeRingPol.
(** Addition et subtraction *)
- Fixpoint PaddC (P:Pol) (c:C) {struct P} : Pol :=
+ Fixpoint PaddC (P:Pol) (c:C) : Pol :=
match P with
| Pc c1 => Pc (c1 +! c)
| Pinj j Q => Pinj j (PaddC Q c)
| PX P i Q => PX P i (PaddC Q c)
end.
- Fixpoint PsubC (P:Pol) (c:C) {struct P} : Pol :=
+ Fixpoint PsubC (P:Pol) (c:C) : Pol :=
match P with
| Pc c1 => Pc (c1 -! c)
| Pinj j Q => Pinj j (PsubC Q c)
@@ -176,11 +191,11 @@ Section MakeRingPol.
Variable Pop : Pol -> Pol -> Pol.
Variable Q : Pol.
- Fixpoint PaddI (j:positive) (P:Pol){struct P} : Pol :=
+ Fixpoint PaddI (j:positive) (P:Pol) : Pol :=
match P with
| Pc c => mkPinj j (PaddC Q c)
| Pinj j' Q' =>
- match ZPminus j' j with
+ match Z.pos_sub j' j with
| Zpos k => mkPinj j (Pop (Pinj k Q') Q)
| Z0 => mkPinj j (Pop Q' Q)
| Zneg k => mkPinj j' (PaddI k Q')
@@ -188,16 +203,16 @@ Section MakeRingPol.
| PX P i Q' =>
match j with
| xH => PX P i (Pop Q' Q)
- | xO j => PX P i (PaddI (Pdouble_minus_one j) Q')
+ | xO j => PX P i (PaddI (Pos.pred_double j) Q')
| xI j => PX P i (PaddI (xO j) Q')
end
end.
- Fixpoint PsubI (j:positive) (P:Pol){struct P} : Pol :=
+ Fixpoint PsubI (j:positive) (P:Pol) : Pol :=
match P with
| Pc c => mkPinj j (PaddC (--Q) c)
| Pinj j' Q' =>
- match ZPminus j' j with
+ match Z.pos_sub j' j with
| Zpos k => mkPinj j (Pop (Pinj k Q') Q)
| Z0 => mkPinj j (Pop Q' Q)
| Zneg k => mkPinj j' (PsubI k Q')
@@ -205,41 +220,41 @@ Section MakeRingPol.
| PX P i Q' =>
match j with
| xH => PX P i (Pop Q' Q)
- | xO j => PX P i (PsubI (Pdouble_minus_one j) Q')
+ | xO j => PX P i (PsubI (Pos.pred_double j) Q')
| xI j => PX P i (PsubI (xO j) Q')
end
end.
Variable P' : Pol.
- Fixpoint PaddX (i':positive) (P:Pol) {struct P} : Pol :=
+ Fixpoint PaddX (i':positive) (P:Pol) : Pol :=
match P with
| Pc c => PX P' i' P
| Pinj j Q' =>
match j with
| xH => PX P' i' Q'
- | xO j => PX P' i' (Pinj (Pdouble_minus_one j) Q')
+ | xO j => PX P' i' (Pinj (Pos.pred_double j) Q')
| xI j => PX P' i' (Pinj (xO j) Q')
end
| PX P i Q' =>
- match ZPminus i i' with
+ match Z.pos_sub i i' with
| Zpos k => mkPX (Pop (PX P k P0) P') i' Q'
| Z0 => mkPX (Pop P P') i Q'
| Zneg k => mkPX (PaddX k P) i Q'
end
end.
- Fixpoint PsubX (i':positive) (P:Pol) {struct P} : Pol :=
+ Fixpoint PsubX (i':positive) (P:Pol) : Pol :=
match P with
| Pc c => PX (--P') i' P
| Pinj j Q' =>
match j with
| xH => PX (--P') i' Q'
- | xO j => PX (--P') i' (Pinj (Pdouble_minus_one j) Q')
+ | xO j => PX (--P') i' (Pinj (Pos.pred_double j) Q')
| xI j => PX (--P') i' (Pinj (xO j) Q')
end
| PX P i Q' =>
- match ZPminus i i' with
+ match Z.pos_sub i i' with
| Zpos k => mkPX (Pop (PX P k P0) P') i' Q'
| Z0 => mkPX (Pop P P') i Q'
| Zneg k => mkPX (PsubX k P) i Q'
@@ -259,18 +274,18 @@ Section MakeRingPol.
| Pinj j Q =>
match j with
| xH => PX P' i' (Padd Q Q')
- | xO j => PX P' i' (Padd (Pinj (Pdouble_minus_one j) Q) Q')
+ | xO j => PX P' i' (Padd (Pinj (Pos.pred_double j) Q) Q')
| xI j => PX P' i' (Padd (Pinj (xO j) Q) Q')
end
| PX P i Q =>
- match ZPminus i i' with
+ match Z.pos_sub i i' with
| Zpos k => mkPX (Padd (PX P k P0) P') i' (Padd Q Q')
| Z0 => mkPX (Padd P P') i (Padd Q Q')
| Zneg k => mkPX (PaddX Padd P' k P) i (Padd Q Q')
end
end
end.
- Notation "P ++ P'" := (Padd P P').
+ Infix "++" := Padd.
Fixpoint Psub (P P': Pol) {struct P'} : Pol :=
match P' with
@@ -282,22 +297,22 @@ Section MakeRingPol.
| Pinj j Q =>
match j with
| xH => PX (--P') i' (Psub Q Q')
- | xO j => PX (--P') i' (Psub (Pinj (Pdouble_minus_one j) Q) Q')
+ | xO j => PX (--P') i' (Psub (Pinj (Pos.pred_double j) Q) Q')
| xI j => PX (--P') i' (Psub (Pinj (xO j) Q) Q')
end
| PX P i Q =>
- match ZPminus i i' with
+ match Z.pos_sub i i' with
| Zpos k => mkPX (Psub (PX P k P0) P') i' (Psub Q Q')
| Z0 => mkPX (Psub P P') i (Psub Q Q')
| Zneg k => mkPX (PsubX Psub P' k P) i (Psub Q Q')
end
end
end.
- Notation "P -- P'" := (Psub P P').
+ Infix "--" := Psub.
(** Multiplication *)
- Fixpoint PmulC_aux (P:Pol) (c:C) {struct P} : Pol :=
+ Fixpoint PmulC_aux (P:Pol) (c:C) : Pol :=
match P with
| Pc c' => Pc (c' *! c)
| Pinj j Q => mkPinj j (PmulC_aux Q c)
@@ -311,11 +326,11 @@ Section MakeRingPol.
Section PmulI.
Variable Pmul : Pol -> Pol -> Pol.
Variable Q : Pol.
- Fixpoint PmulI (j:positive) (P:Pol) {struct P} : Pol :=
+ Fixpoint PmulI (j:positive) (P:Pol) : Pol :=
match P with
| Pc c => mkPinj j (PmulC Q c)
| Pinj j' Q' =>
- match ZPminus j' j with
+ match Z.pos_sub j' j with
| Zpos k => mkPinj j (Pmul (Pinj k Q') Q)
| Z0 => mkPinj j (Pmul Q' Q)
| Zneg k => mkPinj j' (PmulI k Q')
@@ -323,13 +338,12 @@ Section MakeRingPol.
| PX P' i' Q' =>
match j with
| xH => mkPX (PmulI xH P') i' (Pmul Q' Q)
- | xO j' => mkPX (PmulI j P') i' (PmulI (Pdouble_minus_one j') Q')
+ | xO j' => mkPX (PmulI j P') i' (PmulI (Pos.pred_double j') Q')
| xI j' => mkPX (PmulI j P') i' (PmulI (xO j') Q')
end
end.
End PmulI.
-(* A symmetric version of the multiplication *)
Fixpoint Pmul (P P'' : Pol) {struct P''} : Pol :=
match P'' with
@@ -342,7 +356,7 @@ Section MakeRingPol.
let QQ' :=
match j with
| xH => Pmul Q Q'
- | xO j => Pmul (Pinj (Pdouble_minus_one j) Q) Q'
+ | xO j => Pmul (Pinj (Pos.pred_double j) Q) Q'
| xI j => Pmul (Pinj (xO j) Q) Q'
end in
mkPX (Pmul P P') i' QQ'
@@ -355,25 +369,7 @@ Section MakeRingPol.
end
end.
-(* Non symmetric *)
-(*
- Fixpoint Pmul_aux (P P' : Pol) {struct P'} : Pol :=
- match P' with
- | Pc c' => PmulC P c'
- | Pinj j' Q' => PmulI Pmul_aux Q' j' P
- | PX P' i' Q' =>
- (mkPX (Pmul_aux P P') i' P0) ++ (PmulI Pmul_aux Q' xH P)
- end.
-
- Definition Pmul P P' :=
- match P with
- | Pc c => PmulC P' c
- | Pinj j Q => PmulI Pmul_aux Q j P'
- | PX P i Q =>
- (mkPX (Pmul_aux P P') i P0) ++ (PmulI Pmul_aux Q xH P')
- end.
-*)
- Notation "P ** P'" := (Pmul P P').
+ Infix "**" := Pmul.
Fixpoint Psquare (P:Pol) : Pol :=
match P with
@@ -388,26 +384,35 @@ Section MakeRingPol.
(** Monomial **)
+ (** A monomial is X1^k1...Xi^ki. Its representation
+ is a simplified version of the polynomial representation:
+
+ - [mon0] correspond to the polynom [P1].
+ - [(zmon j M)] corresponds to [(Pinj j ...)],
+ i.e. skip j variable indices.
+ - [(vmon i M)] is X^i*M with X the current variable,
+ its corresponds to (PX P1 i ...)]
+ *)
+
Inductive Mon: Set :=
- mon0: Mon
+ | mon0: Mon
| zmon: positive -> Mon -> Mon
| vmon: positive -> Mon -> Mon.
- Fixpoint Mphi(l:Env R) (M: Mon) {struct M} : R :=
+ Fixpoint Mphi (l:Env R)(M: Mon) : R :=
match M with
- mon0 => rI
- | zmon j M1 => Mphi (jump j l) M1
- | vmon i M1 =>
- let x := hd 0 l in
- let xi := pow_pos rmul x i in
- (Mphi (tail l) M1) * xi
+ | mon0 => rI
+ | zmon j M1 => Mphi (jump j l) M1
+ | vmon i M1 => Mphi (tail l) M1 * (hd l) ^ i
end.
+ Notation "M @@ l" := (Mphi l M) (at level 10, no associativity).
+
Definition mkZmon j M :=
match M with mon0 => mon0 | _ => zmon j M end.
Definition zmon_pred j M :=
- match j with xH => M | _ => mkZmon (Ppred j) M end.
+ match j with xH => M | _ => mkZmon (Pos.pred j) M end.
Definition mkVmon i M :=
match M with
@@ -416,7 +421,7 @@ Section MakeRingPol.
| vmon i' m => vmon (i+i') m
end.
- Fixpoint MFactor (P: Pol) (M: Mon) {struct P}: Pol * Pol :=
+ Fixpoint MFactor (P: Pol) (M: Mon) : Pol * Pol :=
match P, M with
_, mon0 => (Pc cO, P)
| Pc _, _ => (P, Pc cO)
@@ -453,7 +458,7 @@ Section MakeRingPol.
| _ => Some (Padd Q1 (Pmul P2 R1))
end.
- Fixpoint PNSubst1 (P1: Pol) (M1: Mon) (P2: Pol) (n: nat) {struct n}: Pol :=
+ Fixpoint PNSubst1 (P1: Pol) (M1: Mon) (P2: Pol) (n: nat) : Pol :=
match POneSubst P1 M1 P2 with
Some P3 => match n with S n1 => PNSubst1 P3 M1 P2 n1 | _ => P3 end
| _ => P1
@@ -465,14 +470,13 @@ Section MakeRingPol.
| _ => None
end.
- Fixpoint PSubstL1 (P1: Pol) (LM1: list (Mon * Pol)) (n: nat) {struct LM1}:
- Pol :=
+ Fixpoint PSubstL1 (P1: Pol) (LM1: list (Mon * Pol)) (n: nat) : Pol :=
match LM1 with
cons (M1,P2) LM2 => PSubstL1 (PNSubst1 P1 M1 P2 n) LM2 n
| _ => P1
end.
- Fixpoint PSubstL (P1: Pol) (LM1: list (Mon * Pol)) (n: nat) {struct LM1}: option Pol :=
+ Fixpoint PSubstL (P1: Pol) (LM1: list (Mon * Pol)) (n: nat) : option Pol :=
match LM1 with
cons (M1,P2) LM2 =>
match PNSubst P1 M1 P2 n with
@@ -482,7 +486,7 @@ Section MakeRingPol.
| _ => None
end.
- Fixpoint PNSubstL (P1: Pol) (LM1: list (Mon * Pol)) (m n: nat) {struct m}: Pol :=
+ Fixpoint PNSubstL (P1: Pol) (LM1: list (Mon * Pol)) (m n: nat) : Pol :=
match PSubstL P1 LM1 n with
Some P3 => match m with S m1 => PNSubstL P3 LM1 m1 n | _ => P3 end
| _ => P1
@@ -490,146 +494,112 @@ Section MakeRingPol.
(** Evaluation of a polynomial towards R *)
- Fixpoint Pphi(l:Env R) (P:Pol) {struct P} : R :=
+ Fixpoint Pphi(l:Env R) (P:Pol) : R :=
match P with
| Pc c => [c]
| Pinj j Q => Pphi (jump j l) Q
- | PX P i Q =>
- let x := hd 0 l in
- let xi := pow_pos rmul x i in
- (Pphi l P) * xi + (Pphi (tail l) Q)
+ | PX P i Q => Pphi l P * (hd l) ^ i + Pphi (tail l) Q
end.
Reserved Notation "P @ l " (at level 10, no associativity).
Notation "P @ l " := (Pphi l P).
+
(** Proofs *)
- Lemma ZPminus_spec : forall x y,
- match ZPminus x y with
- | Z0 => x = y
- | Zpos k => x = (y + k)%positive
- | Zneg k => y = (x + k)%positive
+
+ Ltac destr_pos_sub :=
+ match goal with |- context [Z.pos_sub ?x ?y] =>
+ generalize (Z.pos_sub_discr x y); destruct (Z.pos_sub x y)
end.
+
+ Lemma Peq_ok P P' : (P ?== P') = true -> forall l, P@l == P'@ l.
+ Proof.
+ revert P';induction P;destruct P';simpl; intros H l; try easy.
+ - now apply (morph_eq CRmorph).
+ - destruct (Pos.compare_spec p p0); [ subst | easy | easy ].
+ now rewrite IHP.
+ - specialize (IHP1 P'1); specialize (IHP2 P'2).
+ destruct (Pos.compare_spec p p0); [ subst | easy | easy ].
+ destruct (P2 ?== P'1); [|easy].
+ rewrite H in *.
+ now rewrite IHP1, IHP2.
+ Qed.
+
+ Lemma Peq_spec P P' :
+ BoolSpec (forall l, P@l == P'@l) True (P ?== P').
Proof.
- induction x;destruct y.
- replace (ZPminus (xI x) (xI y)) with (Zdouble (ZPminus x y));trivial.
- assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble;rewrite H;trivial.
- replace (ZPminus (xI x) (xO y)) with (Zdouble_plus_one (ZPminus x y));trivial.
- assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble_plus_one;rewrite H;trivial.
- apply Pplus_xI_double_minus_one.
- simpl;trivial.
- replace (ZPminus (xO x) (xI y)) with (Zdouble_minus_one (ZPminus x y));trivial.
- assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble_minus_one;rewrite H;trivial.
- apply Pplus_xI_double_minus_one.
- replace (ZPminus (xO x) (xO y)) with (Zdouble (ZPminus x y));trivial.
- assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble;rewrite H;trivial.
- replace (ZPminus (xO x) xH) with (Zpos (Pdouble_minus_one x));trivial.
- rewrite <- Pplus_one_succ_l.
- rewrite Psucc_o_double_minus_one_eq_xO;trivial.
- replace (ZPminus xH (xI y)) with (Zneg (xO y));trivial.
- replace (ZPminus xH (xO y)) with (Zneg (Pdouble_minus_one y));trivial.
- rewrite <- Pplus_one_succ_l.
- rewrite Psucc_o_double_minus_one_eq_xO;trivial.
- simpl;trivial.
+ generalize (Peq_ok P P'). destruct (P ?== P'); auto.
Qed.
- Lemma Peq_ok : forall P P',
- (P ?== P') = true -> forall l, P@l == P'@ l.
+ Lemma Pphi0 l : P0@l == 0.
Proof.
- induction P;destruct P';simpl;intros;try discriminate;trivial.
- apply (morph_eq CRmorph);trivial.
- assert (H1 := Pos.compare_eq p p0); destruct (p ?= p0);
- try discriminate H.
- rewrite (IHP P' H); rewrite H1;trivial;rrefl.
- assert (H1 := Pos.compare_eq p p0); destruct (p ?= p0);
- try discriminate H.
- rewrite H1;trivial. clear H1.
- assert (H1 := IHP1 P'1);assert (H2 := IHP2 P'2);
- destruct (P2 ?== P'1);[destruct (P3 ?== P'2); [idtac|discriminate H]
- |discriminate H].
- rewrite (H1 H);rewrite (H2 H);rrefl.
+ simpl;apply (morph0 CRmorph).
Qed.
- Lemma Pphi0 : forall l, P0@l == 0.
+ Lemma Pphi1 l : P1@l == 1.
Proof.
- intros;simpl;apply (morph0 CRmorph).
+ simpl;apply (morph1 CRmorph).
Qed.
-Lemma env_morph : forall p e1 e2, (forall x, e1 x = e2 x) ->
- p @ e1 = p @ e2.
+Lemma env_morph p e1 e2 :
+ (forall x, e1 x = e2 x) -> p @ e1 = p @ e2.
Proof.
- induction p ; simpl.
- reflexivity.
- intros.
- apply IHp.
- intros.
- unfold jump.
- apply H.
- intros.
- rewrite (IHp1 e1 e2) ; auto.
- rewrite (IHp2 (tail e1) (tail e2)) ; auto.
- unfold hd. unfold nth. rewrite H. reflexivity.
- unfold tail. unfold jump. intros ; apply H.
+ revert e1 e2. induction p ; simpl.
+ - reflexivity.
+ - intros e1 e2 EQ. apply IHp. intros. apply EQ.
+ - intros e1 e2 EQ. f_equal; [f_equal|].
+ + now apply IHp1.
+ + f_equal. apply EQ.
+ + apply IHp2. intros; apply EQ.
Qed.
-Lemma Pjump_Pplus : forall P i j l, P @ (jump (i + j) l ) = P @ (jump j (jump i l)).
+Lemma Pjump_add P i j l :
+ P @ (jump (i + j) l) = P @ (jump j (jump i l)).
Proof.
- intros. apply env_morph. intros. rewrite <- jump_Pplus.
- rewrite Pplus_comm.
- reflexivity.
+ apply env_morph. intros. rewrite <- jump_add. f_equal.
+ apply Pos.add_comm.
Qed.
-Lemma Pjump_xO_tail : forall P p l,
+Lemma Pjump_xO_tail P p l :
P @ (jump (xO p) (tail l)) = P @ (jump (xI p) l).
Proof.
- intros.
- apply env_morph.
- intros.
- rewrite (@jump_simpl R (xI p)).
- rewrite (@jump_simpl R (xO p)).
- reflexivity.
+ apply env_morph. intros. now jump_simpl.
Qed.
-Lemma Pjump_Pdouble_minus_one : forall P p l,
- P @ (jump (Pdouble_minus_one p) (tail l)) = P @ (jump (xO p) l).
+Lemma Pjump_pred_double P p l :
+ P @ (jump (Pos.pred_double p) (tail l)) = P @ (jump (xO p) l).
Proof.
- intros.
- apply env_morph.
- intros.
- rewrite jump_Pdouble_minus_one.
- rewrite (@jump_simpl R (xO p)).
- reflexivity.
+ apply env_morph. intros.
+ rewrite jump_pred_double. now jump_simpl.
Qed.
-
-
- Lemma Pphi1 : forall l, P1@l == 1.
+ Lemma mkPinj_ok j l P : (mkPinj j P)@l == P@(jump j l).
Proof.
- intros;simpl;apply (morph1 CRmorph).
+ destruct P;simpl;rsimpl.
+ now rewrite Pjump_add.
Qed.
- Lemma mkPinj_ok : forall j l P, (mkPinj j P)@l == P@(jump j l).
+ Lemma pow_pos_add x i j : x^(j + i) == x^i * x^j.
Proof.
- intros j l p;destruct p;simpl;rsimpl.
- rewrite Pjump_Pplus.
- reflexivity.
+ rewrite Pos.add_comm.
+ apply (pow_pos_add Rsth Reqe.(Rmul_ext) ARth.(ARmul_assoc)).
Qed.
- Let pow_pos_Pplus :=
- pow_pos_Pplus rmul Rsth Reqe.(Rmul_ext) ARth.(ARmul_comm) ARth.(ARmul_assoc).
-
- Lemma mkPX_ok : forall l P i Q,
- (mkPX P i Q)@l == P@l*(pow_pos rmul (hd 0 l) i) + Q@(tail l).
+ Lemma ceqb_spec c c' : BoolSpec ([c] == [c']) True (c ?=! c').
Proof.
- intros l P i Q;unfold mkPX.
- destruct P;try (simpl;rrefl).
- assert (H := morph_eq CRmorph c cO);destruct (c ?=! cO);simpl;try rrefl.
- rewrite (H (refl_equal true));rewrite (morph0 CRmorph).
- rewrite mkPinj_ok;rsimpl;simpl;rrefl.
- assert (H := @Peq_ok P3 P0);destruct (P3 ?== P0);simpl;try rrefl.
- rewrite (H (refl_equal true));trivial.
- rewrite Pphi0. rewrite pow_pos_Pplus;rsimpl.
+ generalize (morph_eq CRmorph c c').
+ destruct (c ?=! c'); auto.
Qed.
+ Lemma mkPX_ok l P i Q :
+ (mkPX P i Q)@l == P@l * (hd l)^i + Q@(tail l).
+ Proof.
+ unfold mkPX. destruct P.
+ - case ceqb_spec; intros H; simpl; try reflexivity.
+ rewrite H, (morph0 CRmorph), mkPinj_ok; rsimpl.
+ - reflexivity.
+ - case Peq_spec; intros H; simpl; try reflexivity.
+ rewrite H, Pphi0, Pos.add_comm, pow_pos_add; rsimpl.
+ Qed.
Ltac Esimpl :=
repeat (progress (
@@ -647,43 +617,42 @@ Qed.
end));
rsimpl; simpl.
- Lemma PaddC_ok : forall c P l, (PaddC P c)@l == P@l + [c].
+ Lemma PaddC_ok c P l : (PaddC P c)@l == P@l + [c].
Proof.
- induction P;simpl;intros;Esimpl;trivial.
+ revert l;induction P;simpl;intros;Esimpl;trivial.
rewrite IHP2;rsimpl.
Qed.
- Lemma PsubC_ok : forall c P l, (PsubC P c)@l == P@l - [c].
+ Lemma PsubC_ok c P l : (PsubC P c)@l == P@l - [c].
Proof.
- induction P;simpl;intros.
- Esimpl.
- rewrite IHP;rsimpl.
- rewrite IHP2;rsimpl.
+ revert l;induction P;simpl;intros.
+ - Esimpl.
+ - rewrite IHP;rsimpl.
+ - rewrite IHP2;rsimpl.
Qed.
- Lemma PmulC_aux_ok : forall c P l, (PmulC_aux P c)@l == P@l * [c].
+ Lemma PmulC_aux_ok c P l : (PmulC_aux P c)@l == P@l * [c].
Proof.
- induction P;simpl;intros;Esimpl;trivial.
- rewrite IHP1;rewrite IHP2;rsimpl.
- mul_push ([c]);rrefl.
+ revert l;induction P;simpl;intros;Esimpl;trivial.
+ rewrite IHP1, IHP2;rsimpl. add_permut. mul_permut.
Qed.
- Lemma PmulC_ok : forall c P l, (PmulC P c)@l == P@l * [c].
+ Lemma PmulC_ok c P l : (PmulC P c)@l == P@l * [c].
Proof.
- intros c P l; unfold PmulC.
- assert (H:= morph_eq CRmorph c cO);destruct (c ?=! cO).
- rewrite (H (refl_equal true));Esimpl.
- assert (H1:= morph_eq CRmorph c cI);destruct (c ?=! cI).
- rewrite (H1 (refl_equal true));Esimpl.
- apply PmulC_aux_ok.
+ unfold PmulC.
+ case ceqb_spec; intros H.
+ - rewrite H; Esimpl.
+ - case ceqb_spec; intros H'.
+ + rewrite H'; Esimpl.
+ + apply PmulC_aux_ok.
Qed.
- Lemma Popp_ok : forall P l, (--P)@l == - P@l.
+ Lemma Popp_ok P l : (--P)@l == - P@l.
Proof.
- induction P;simpl;intros.
- Esimpl.
- apply IHP.
- rewrite IHP1;rewrite IHP2;rsimpl.
+ revert l;induction P;simpl;intros.
+ - Esimpl.
+ - apply IHP.
+ - rewrite IHP1, IHP2;rsimpl.
Qed.
Ltac Esimpl2 :=
@@ -696,520 +665,273 @@ Qed.
| |- context [(--?P)@?l] => rewrite (Popp_ok P l)
end)); Esimpl.
-
-
-
- Lemma Padd_ok : forall P' P l, (P ++ P')@l == P@l + P'@l.
- Proof.
- induction P';simpl;intros;Esimpl2.
- generalize P p l;clear P p l.
- induction P;simpl;intros.
- Esimpl2;apply (ARadd_comm ARth).
- assert (H := ZPminus_spec p p0);destruct (ZPminus p p0).
- rewrite H;Esimpl. rewrite IHP';rrefl.
- rewrite H;Esimpl. rewrite IHP';Esimpl.
- rewrite Pjump_Pplus. rrefl.
- rewrite H;Esimpl. rewrite IHP.
- rewrite Pjump_Pplus. rrefl.
- destruct p0;simpl.
- rewrite IHP2;simpl. rsimpl.
- rewrite Pjump_xO_tail. Esimpl.
- rewrite IHP2;simpl.
- rewrite Pjump_Pdouble_minus_one.
- rsimpl.
- rewrite IHP'.
- rsimpl.
- destruct P;simpl.
- Esimpl2;add_push [c];rrefl.
- destruct p0;simpl;Esimpl2.
- rewrite IHP'2;simpl.
- rewrite Pjump_xO_tail.
- rsimpl;add_push (P'1@l * (pow_pos rmul (hd 0 l) p));rrefl.
- rewrite IHP'2;simpl.
- rewrite Pjump_Pdouble_minus_one. rsimpl.
- add_push (P'1@l * (pow_pos rmul (hd 0 l) p));rrefl.
- rewrite IHP'2;rsimpl.
- unfold tail.
- add_push (P @ (jump 1 l));rrefl.
- assert (H := ZPminus_spec p0 p);destruct (ZPminus p0 p);Esimpl2.
- rewrite IHP'1;rewrite IHP'2;rsimpl.
- add_push (P3 @ (tail l));rewrite H;rrefl.
- rewrite IHP'1;rewrite IHP'2;simpl;Esimpl.
- rewrite H;rewrite Pplus_comm.
- rewrite pow_pos_Pplus;rsimpl.
- add_push (P3 @ (tail l));rrefl.
- assert (forall P k l,
- (PaddX Padd P'1 k P) @ l == P@l + P'1@l * pow_pos rmul (hd 0 l) k).
- induction P;simpl;intros;try apply (ARadd_comm ARth).
- destruct p2; simpl; try apply (ARadd_comm ARth).
- rewrite Pjump_xO_tail.
- apply (ARadd_comm ARth).
- rewrite Pjump_Pdouble_minus_one.
- apply (ARadd_comm ARth).
- assert (H1 := ZPminus_spec p2 k);destruct (ZPminus p2 k);Esimpl2.
- rewrite IHP'1;rsimpl; rewrite H1;add_push (P5 @ (tail l0));rrefl.
- rewrite IHP'1;simpl;Esimpl.
- rewrite H1;rewrite Pplus_comm.
- rewrite pow_pos_Pplus;simpl;Esimpl.
- add_push (P5 @ (tail l0));rrefl.
- rewrite IHP1;rewrite H1;rewrite Pplus_comm.
- rewrite pow_pos_Pplus;simpl;rsimpl.
- add_push (P5 @ (tail l0));rrefl.
- rewrite H0;rsimpl.
- add_push (P3 @ (tail l)).
- rewrite H;rewrite Pplus_comm.
- rewrite IHP'2;rewrite pow_pos_Pplus;rsimpl.
- add_push (P3 @ (tail l));rrefl.
- Qed.
-
- Lemma Psub_ok : forall P' P l, (P -- P')@l == P@l - P'@l.
+ Lemma PaddX_ok P' P k l :
+ (forall P l, (P++P')@l == P@l + P'@l) ->
+ (PaddX Padd P' k P) @ l == P@l + P'@l * (hd l)^k.
Proof.
- induction P';simpl;intros;Esimpl2;trivial.
- generalize P p l;clear P p l.
- induction P;simpl;intros.
- Esimpl2;apply (ARadd_comm ARth).
- assert (H := ZPminus_spec p p0);destruct (ZPminus p p0).
- rewrite H;Esimpl. rewrite IHP';rsimpl.
- rewrite H;Esimpl. rewrite IHP';Esimpl.
- rewrite <- Pjump_Pplus;rewrite Pplus_comm;rrefl.
- rewrite H;Esimpl. rewrite IHP.
- rewrite <- Pjump_Pplus;rewrite Pplus_comm;rrefl.
- destruct p0;simpl.
- rewrite IHP2;simpl; try rewrite Pjump_xO_tail ; rsimpl.
- rewrite IHP2;simpl.
- rewrite Pjump_Pdouble_minus_one;rsimpl.
- unfold tail ; rsimpl.
- rewrite IHP';rsimpl.
- destruct P;simpl.
- repeat rewrite Popp_ok;Esimpl2;rsimpl;add_push [c];try rrefl.
- destruct p0;simpl;Esimpl2.
- rewrite IHP'2;simpl;rsimpl;add_push (P'1@l * (pow_pos rmul (hd 0 l) p));trivial.
- rewrite Pjump_xO_tail.
- add_push (P @ ((jump (xI p0) l)));rrefl.
- rewrite IHP'2;simpl;rewrite Pjump_Pdouble_minus_one;rsimpl.
- add_push (- (P'1 @ l * pow_pos rmul (hd 0 l) p));rrefl.
- unfold tail.
- rewrite IHP'2;rsimpl;add_push (P @ (jump 1 l));rrefl.
- assert (H := ZPminus_spec p0 p);destruct (ZPminus p0 p);Esimpl2.
- rewrite IHP'1; rewrite IHP'2;rsimpl.
- add_push (P3 @ (tail l));rewrite H;rrefl.
- rewrite IHP'1; rewrite IHP'2;rsimpl;simpl;Esimpl.
- rewrite H;rewrite Pplus_comm.
- rewrite pow_pos_Pplus;rsimpl.
- add_push (P3 @ (tail l));rrefl.
- assert (forall P k l,
- (PsubX Psub P'1 k P) @ l == P@l + - P'1@l * pow_pos rmul (hd 0 l) k).
- induction P;simpl;intros.
- rewrite Popp_ok;rsimpl;apply (ARadd_comm ARth);trivial.
- destruct p2;simpl; rewrite Popp_ok;rsimpl.
- rewrite Pjump_xO_tail.
- apply (ARadd_comm ARth);trivial.
- rewrite Pjump_Pdouble_minus_one.
- apply (ARadd_comm ARth);trivial.
- apply (ARadd_comm ARth);trivial.
- assert (H1 := ZPminus_spec p2 k);destruct (ZPminus p2 k);Esimpl2;rsimpl.
- rewrite IHP'1;rsimpl;add_push (P5 @ (tail l0));rewrite H1;rrefl.
- rewrite IHP'1;rewrite H1;rewrite Pplus_comm.
- rewrite pow_pos_Pplus;simpl;Esimpl.
- add_push (P5 @ (tail l0));rrefl.
- rewrite IHP1;rewrite H1;rewrite Pplus_comm.
- rewrite pow_pos_Pplus;simpl;rsimpl.
- add_push (P5 @ (tail l0));rrefl.
- rewrite H0;rsimpl.
- rewrite IHP'2;rsimpl;add_push (P3 @ (tail l)).
- rewrite H;rewrite Pplus_comm.
- rewrite pow_pos_Pplus;rsimpl.
+ intros IHP'.
+ revert k l. induction P;simpl;intros.
+ - add_permut.
+ - destruct p; simpl;
+ rewrite ?Pjump_xO_tail, ?Pjump_pred_double; add_permut.
+ - destr_pos_sub; intros ->;Esimpl2.
+ + rewrite IHP';rsimpl. add_permut.
+ + rewrite IHP', pow_pos_add;simpl;Esimpl. add_permut.
+ + rewrite IHP1, pow_pos_add;rsimpl. add_permut.
Qed.
-(* Proof for the symmetric version *)
- Lemma PmulI_ok :
- forall P',
- (forall (P : Pol) (l : Env R), (Pmul P P') @ l == P @ l * P' @ l) ->
- forall (P : Pol) (p : positive) (l : Env R),
- (PmulI Pmul P' p P) @ l == P @ l * P' @ (jump p l).
+ Lemma Padd_ok P' P l : (P ++ P')@l == P@l + P'@l.
Proof.
- induction P;simpl;intros.
- Esimpl2;apply (ARmul_comm ARth).
- assert (H1 := ZPminus_spec p p0);destruct (ZPminus p p0);Esimpl2.
- rewrite H1; rewrite H;rrefl.
- rewrite H1; rewrite H.
- rewrite Pjump_Pplus;simpl;rrefl.
- rewrite H1.
- rewrite Pjump_Pplus;rewrite IHP;rrefl.
- destruct p0;Esimpl2.
- rewrite IHP1;rewrite IHP2;rsimpl.
- rewrite Pjump_xO_tail.
- mul_push (pow_pos rmul (hd 0 l) p);rrefl.
- rewrite IHP1;rewrite IHP2;simpl;rsimpl.
- mul_push (pow_pos rmul (hd 0 l) p); rewrite Pjump_Pdouble_minus_one.
- rrefl.
- rewrite IHP1;simpl;rsimpl.
- mul_push (pow_pos rmul (hd 0 l) p).
- rewrite H;rrefl.
+ revert P l; induction P';simpl;intros;Esimpl2.
+ - revert p l; induction P;simpl;intros.
+ + Esimpl2; add_permut.
+ + destr_pos_sub; intros ->;Esimpl.
+ * now rewrite IHP'.
+ * rewrite IHP';Esimpl. now rewrite Pjump_add.
+ * rewrite IHP. now rewrite Pjump_add.
+ + destruct p0;simpl.
+ * rewrite IHP2;simpl. rsimpl. rewrite Pjump_xO_tail. Esimpl.
+ * rewrite IHP2;simpl. rewrite Pjump_pred_double. rsimpl.
+ * rewrite IHP'. rsimpl.
+ - destruct P;simpl.
+ + Esimpl2. add_permut.
+ + destruct p0;simpl;Esimpl2; rewrite IHP'2; simpl.
+ * rewrite Pjump_xO_tail. rsimpl. add_permut.
+ * rewrite Pjump_pred_double. rsimpl. add_permut.
+ * rsimpl. unfold tail. add_permut.
+ + destr_pos_sub; intros ->; Esimpl2.
+ * rewrite IHP'1, IHP'2;rsimpl. add_permut.
+ * rewrite IHP'1, IHP'2;simpl;Esimpl.
+ rewrite pow_pos_add;rsimpl. add_permut.
+ * rewrite PaddX_ok by trivial; rsimpl.
+ rewrite IHP'2, pow_pos_add; rsimpl. add_permut.
Qed.
-(*
- Lemma PmulI_ok :
- forall P',
- (forall (P : Pol) (l : list R), (Pmul_aux P P') @ l == P @ l * P' @ l) ->
- forall (P : Pol) (p : positive) (l : list R),
- (PmulI Pmul_aux P' p P) @ l == P @ l * P' @ (jump p l).
+ Lemma PsubX_ok P' P k l :
+ (forall P l, (P--P')@l == P@l - P'@l) ->
+ (PsubX Psub P' k P) @ l == P@l - P'@l * (hd l)^k.
Proof.
- induction P;simpl;intros.
- Esimpl2;apply (ARmul_comm ARth).
- assert (H1 := ZPminus_spec p p0);destruct (ZPminus p p0);Esimpl2.
- rewrite H1; rewrite H;rrefl.
- rewrite H1; rewrite H.
- rewrite Pplus_comm.
- rewrite jump_Pplus;simpl;rrefl.
- rewrite H1;rewrite Pplus_comm.
- rewrite jump_Pplus;rewrite IHP;rrefl.
- destruct p0;Esimpl2.
- rewrite IHP1;rewrite IHP2;simpl;rsimpl.
- mul_push (pow_pos rmul (hd 0 l) p);rrefl.
- rewrite IHP1;rewrite IHP2;simpl;rsimpl.
- mul_push (pow_pos rmul (hd 0 l) p); rewrite jump_Pdouble_minus_one;rrefl.
- rewrite IHP1;simpl;rsimpl.
- mul_push (pow_pos rmul (hd 0 l) p).
- rewrite H;rrefl.
+ intros IHP'.
+ revert k l. induction P;simpl;intros.
+ - rewrite Popp_ok;rsimpl; add_permut.
+ - destruct p; simpl;
+ rewrite Popp_ok;rsimpl;
+ rewrite ?Pjump_xO_tail, ?Pjump_pred_double; add_permut.
+ - destr_pos_sub; intros ->; Esimpl2; rsimpl.
+ + rewrite IHP';rsimpl. add_permut.
+ + rewrite IHP', pow_pos_add;simpl;Esimpl. add_permut.
+ + rewrite IHP1, pow_pos_add;rsimpl. add_permut.
Qed.
- Lemma Pmul_aux_ok : forall P' P l,(Pmul_aux P P')@l == P@l * P'@l.
+ Lemma Psub_ok P' P l : (P -- P')@l == P@l - P'@l.
Proof.
- induction P';simpl;intros.
- Esimpl2;trivial.
- apply PmulI_ok;trivial.
- rewrite Padd_ok;Esimpl2.
- rewrite (PmulI_ok P'2 IHP'2). rewrite IHP'1. rrefl.
+ revert P l; induction P';simpl;intros;Esimpl2.
+ - revert p l; induction P;simpl;intros.
+ + Esimpl2; add_permut.
+ + destr_pos_sub; intros ->;Esimpl.
+ * rewrite IHP';rsimpl.
+ * rewrite IHP';Esimpl. now rewrite Pjump_add.
+ * rewrite IHP. now rewrite Pjump_add.
+ + destruct p0;simpl.
+ * rewrite IHP2;simpl. rsimpl. rewrite Pjump_xO_tail. Esimpl.
+ * rewrite IHP2;simpl. rewrite Pjump_pred_double. rsimpl.
+ * rewrite IHP'. rsimpl.
+ - destruct P;simpl.
+ + Esimpl2; add_permut.
+ + destruct p0;simpl;Esimpl2; rewrite IHP'2; simpl.
+ * rewrite Pjump_xO_tail. rsimpl. add_permut.
+ * rewrite Pjump_pred_double. rsimpl. add_permut.
+ * rsimpl. unfold tail. add_permut.
+ + destr_pos_sub; intros ->; Esimpl2.
+ * rewrite IHP'1, IHP'2;rsimpl. add_permut.
+ * rewrite IHP'1, IHP'2;simpl;Esimpl.
+ rewrite pow_pos_add;rsimpl. add_permut.
+ * rewrite PsubX_ok by trivial;rsimpl.
+ rewrite IHP'2, pow_pos_add;rsimpl. add_permut.
Qed.
-*)
-(* Proof for the symmetric version *)
- Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
+ Lemma PmulI_ok P' :
+ (forall P l, (Pmul P P') @ l == P @ l * P' @ l) ->
+ forall P p l, (PmulI Pmul P' p P) @ l == P @ l * P' @ (jump p l).
Proof.
- intros P P';generalize P;clear P;induction P';simpl;intros.
- apply PmulC_ok. apply PmulI_ok;trivial.
- destruct P.
- rewrite (ARmul_comm ARth);Esimpl2;Esimpl2.
- Esimpl2. rewrite IHP'1;Esimpl2.
- assert (match p0 with
- | xI j => Pinj (xO j) P ** P'2
- | xO j => Pinj (Pdouble_minus_one j) P ** P'2
- | 1 => P ** P'2
- end @ (tail l) == P @ (jump p0 l) * P'2 @ (tail l)).
- destruct p0;rewrite IHP'2;Esimpl.
- rewrite Pjump_xO_tail. reflexivity.
- rewrite Pjump_Pdouble_minus_one;Esimpl.
- rewrite H;Esimpl.
- rewrite Padd_ok; Esimpl2. rewrite Padd_ok; Esimpl2.
- repeat (rewrite IHP'1 || rewrite IHP'2);simpl.
- rewrite PmulI_ok;trivial.
- unfold tail.
- mul_push (P'1@l). simpl. mul_push (P'2 @ (jump 1 l)). Esimpl.
+ intros IHP'.
+ induction P;simpl;intros.
+ - Esimpl2; mul_permut.
+ - destr_pos_sub; intros ->;Esimpl2.
+ + now rewrite IHP'.
+ + now rewrite IHP', Pjump_add.
+ + now rewrite IHP, Pjump_add.
+ - destruct p0;Esimpl2; rewrite ?IHP1, ?IHP2; rsimpl.
+ + rewrite Pjump_xO_tail. f_equiv. mul_permut.
+ + rewrite Pjump_pred_double. f_equiv. mul_permut.
+ + rewrite IHP'. f_equiv. mul_permut.
Qed.
-(*
-Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
+ Lemma Pmul_ok P P' l : (P**P')@l == P@l * P'@l.
Proof.
- destruct P;simpl;intros.
- Esimpl2;apply (ARmul_comm ARth).
- rewrite (PmulI_ok P (Pmul_aux_ok P)).
- apply (ARmul_comm ARth).
- rewrite Padd_ok; Esimpl2.
- rewrite (PmulI_ok P3 (Pmul_aux_ok P3));trivial.
- rewrite Pmul_aux_ok;mul_push (P' @ l).
- rewrite (ARmul_comm ARth (P' @ l));rrefl.
+ revert P l;induction P';simpl;intros.
+ - apply PmulC_ok.
+ - apply PmulI_ok;trivial.
+ - destruct P.
+ + rewrite (ARmul_comm ARth). Esimpl2; Esimpl2.
+ + Esimpl2. rewrite IHP'1;Esimpl2. f_equiv.
+ destruct p0;rewrite IHP'2;Esimpl.
+ * now rewrite Pjump_xO_tail.
+ * rewrite Pjump_pred_double; Esimpl.
+ + rewrite Padd_ok, !mkPX_ok, Padd_ok, !mkPX_ok,
+ !IHP'1, !IHP'2, PmulI_ok; trivial. Esimpl2.
+ unfold tail.
+ add_permut; f_equiv; mul_permut.
Qed.
-*)
- Lemma Psquare_ok : forall P l, (Psquare P)@l == P@l * P@l.
+ Lemma Psquare_ok P l : (Psquare P)@l == P@l * P@l.
Proof.
- induction P;simpl;intros;Esimpl2.
- apply IHP. rewrite Padd_ok. rewrite Pmul_ok;Esimpl2.
- rewrite IHP1;rewrite IHP2.
- mul_push (pow_pos rmul (hd 0 l) p). mul_push (P2@l).
- rrefl.
+ revert l;induction P;simpl;intros;Esimpl2.
+ - apply IHP.
+ - rewrite Padd_ok, Pmul_ok;Esimpl2.
+ rewrite IHP1, IHP2.
+ mul_push ((hd l)^p). now mul_push (P2@l).
Qed.
- Lemma Mphi_morph : forall P env env', (forall x, env x = env' x ) ->
- Mphi env P = Mphi env' P.
+ Lemma Mphi_morph M e1 e2 :
+ (forall x, e1 x = e2 x) -> M @@ e1 = M @@ e2.
Proof.
- induction P ; simpl.
- reflexivity.
- intros.
- apply IHP.
- intros.
- unfold jump.
- apply H.
- (**)
- intros.
- replace (Mphi (tail env) P) with (Mphi (tail env') P).
- unfold hd. unfold nth.
- rewrite H.
- reflexivity.
- apply IHP.
- unfold tail,jump.
- intros. symmetry. apply H.
+ revert e1 e2; induction M; simpl; intros e1 e2 EQ; trivial.
+ - apply IHM. intros; apply EQ.
+ - f_equal.
+ * apply IHM. intros; apply EQ.
+ * f_equal. apply EQ.
Qed.
-Lemma Mjump_xO_tail : forall M p l,
- Mphi (jump (xO p) (tail l)) M = Mphi (jump (xI p) l) M.
+Lemma Mjump_xO_tail M p l :
+ M @@ (jump (xO p) (tail l)) = M @@ (jump (xI p) l).
Proof.
- intros.
- apply Mphi_morph.
- intros.
- rewrite (@jump_simpl R (xI p)).
- rewrite (@jump_simpl R (xO p)).
- reflexivity.
+ apply Mphi_morph. intros. now jump_simpl.
Qed.
-Lemma Mjump_Pdouble_minus_one : forall M p l,
- Mphi (jump (Pdouble_minus_one p) (tail l)) M = Mphi (jump (xO p) l) M.
+Lemma Mjump_pred_double M p l :
+ M @@ (jump (Pos.pred_double p) (tail l)) = M @@ (jump (xO p) l).
Proof.
- intros.
- apply Mphi_morph.
- intros.
- rewrite jump_Pdouble_minus_one.
- rewrite (@jump_simpl R (xO p)).
- reflexivity.
+ apply Mphi_morph. intros.
+ rewrite jump_pred_double. now jump_simpl.