More improvements of BigN, BigZ, BigQ:

 - ring/field: detection of constants for ring/field,
   detection of power, potential use of euclidean division.
 - for BigN and BigZ, x^n now takes a N as 2nd arg instead of a positive
 - mention that we can use (r)omega thanks to (ugly) BigN.zify, BigZ.zify.
   By the way, BigN.zify could still be improved (no insertion of positivity
   hyps yet, unlike the original zify).
 - debug of BigQ.qify (autorewrite was looping on spec_0).
 - for BigQ, start of a generic functor of properties QProperties.
 - BigQ now implements OrderedType, TotalOrder, and contains facts
   about min and max.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12681 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 14 insertions, 0 deletions

diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 6257e8e63..8240604c2 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -1780,6 +1780,20 @@ let _ =
   pp " intros; rewrite Zpower_1_r; auto.";
   pp " Qed.";
   pp "";
+
+  pr " Definition power x (n:N) := match n with";
+  pr "  | BinNat.N0 => one";
+  pr "  | BinNat.Npos p => power_pos x p";
+  pr " end.";
+  pr "";
+
+  pr " Theorem spec_power: forall x n, [power x n] = [x] ^ Z_of_N n.";
+  pa " Admitted.";
+  pp " Proof.";
+  pp " destruct n; simpl. apply (spec_1 w0_spec).";
+  pp " apply spec_power_pos.";
+  pp " Qed.";
+  pr "";
   pr "";
 
   pr " (***************************************************************)";