diff options
Diffstat (limited to 'theories/Numbers/Natural/BigN/NMake_gen.ml')
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml | 24 |
1 files changed, 16 insertions, 8 deletions
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 9e4e88c5..6de77e0a 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -138,8 +138,6 @@ pr pr ""; pr " Definition t := t'."; pr ""; - pr " Bind Scope abstract_scope with t t'."; - pr ""; pr " (** * A generic toolbox for building and deconstructing [t] *)"; pr ""; @@ -234,7 +232,7 @@ pr | S n1 => mk_zn2z_ops (nmake_op ww ww_op n1) end. - Let eval n m := ZnZ.to_Z (Ops:=nmake_op _ (dom_op n) m). + Definition eval n m := ZnZ.to_Z (Ops:=nmake_op _ (dom_op n) m). Theorem nmake_op_S: forall ww (w_op: ZnZ.Ops ww) x, nmake_op _ w_op (S x) = mk_zn2z_ops (nmake_op _ w_op x). @@ -326,8 +324,13 @@ pr " Lemma spec_zeron : forall n, ZnZ.to_Z (zeron n) = 0%%Z. Proof. - do_size (destruct n; [exact ZnZ.spec_0|]). - destruct n; auto. simpl. rewrite make_op_S. exact ZnZ.spec_0. + do_size (destruct n; + [match goal with + |- @eq Z (_ (zeron ?n)) _ => + apply (ZnZ.spec_0 (Specs:=dom_spec n)) + end|]). + destruct n; auto. simpl. rewrite make_op_S. fold word. + apply (ZnZ.spec_0 (Specs:=wn_spec (SizePlus 0))). Qed. (** * Digits *) @@ -533,7 +536,7 @@ pr " for i = 0 to size-1 do let pattern = (iter_str (size+1-i) "(S ") ^ "_" ^ (iter_str (size+1-i) ")") in pr -" Let mk_t_%iw m := Eval cbv beta zeta iota delta [ mk_t plus ] in +" Definition mk_t_%iw m := Eval cbv beta zeta iota delta [ mk_t plus ] in match m return word w%i (S m) -> t with | %s as p => mk_t_w %i (S p) | p => mk_t (%i+p) @@ -542,7 +545,7 @@ pr done; pr -" Let mk_t_w' n : forall m, word (dom_t n) (S m) -> t := +" Definition mk_t_w' n : forall m, word (dom_t n) (S m) -> t := match n return (forall m, word (dom_t n) (S m) -> t) with"; for i = 0 to size-1 do pr " | %i => mk_t_%iw" i i done; pr @@ -958,6 +961,11 @@ pr " end."; pr ""; pr " Ltac unfold_red := unfold reduce, %s." (iter_name 1 size "reduce_" ","); +pr ""; +for i = 0 to size do +pr " Declare Equivalent Keys reduce reduce_%i." i; +done; +pr " Declare Equivalent Keys reduce_n reduce_%i." (size + 1); pr " Ltac solve_red := |