diff options
| -rw-r--r-- | theories/Ints/num/NMake.v | 26 | ||||
| -rw-r--r-- | theories/Ints/num/ZMake.v | 313 | ||||
| -rw-r--r-- | theories/Ints/num/genN.ml | 80 |
3 files changed, 378 insertions, 41 deletions
diff --git a/theories/Ints/num/NMake.v b/theories/Ints/num/NMake.v index 03402c53f..7ac69fb02 100644 --- a/theories/Ints/num/NMake.v +++ b/theories/Ints/num/NMake.v @@ -8,12 +8,12 @@ Require Import GenMul. Require Import GenDivn1. Require Import Wf_nat. - (***************************************************************) - (* *) - (* File automatically generated DO NOT EDIT *) - (* Constructors: 13 Generated Proofs: false *) - (* *) - (***************************************************************) +(***************************************************************) +(* *) +(* File automatically generated DO NOT EDIT *) +(* Constructors: 13 Generated Proofs: false *) +(* *) +(***************************************************************) Module Type W0Type. Parameter w : Set. @@ -212,7 +212,7 @@ Module Make (W0:W0Type). Admitted. - Theorem to_Z_pos: forall x, 0 <= [x]. + Theorem spec_pos: forall x, 0 <= [x]. Admitted. Section LevelAndIter. @@ -1729,7 +1729,7 @@ Module Make (W0:W0Type). end end. - Theorem succ_spec: forall n, [succ n] = [n] + 1. + Theorem spec_succ: forall n, [succ n] = [n] + 1. Admitted. (***************************************************************) @@ -1949,7 +1949,7 @@ Module Make (W0:W0Type). end end. - Let spec_pred: forall x, 0 < [x] -> [pred x] = [x] - 1. + Theorem spec_pred: forall x, 0 < [x] -> [pred x] = [x] - 1. Admitted. (***************************************************************) @@ -2912,7 +2912,7 @@ Admitted. Theorem spec_div_eucl: forall x y, 0 < [y] -> let (q,r) := div_eucl x y in - [q] = [x] / [y] /\ [r] = [x] mod [y]. + ([q], [r]) = Zdiv_eucl [x] [y]. Admitted. Definition div x y := fst (div_eucl x y). @@ -3460,5 +3460,11 @@ Admitted. if is_even x then [x] mod 2 = 0 else [x] mod 2 = 1. Admitted. + Theorem spec_0: [zero] = 0. + Admitted. + + Theorem spec_1: [one] = 1. + Admitted. + End Make. diff --git a/theories/Ints/num/ZMake.v b/theories/Ints/num/ZMake.v index f79b5478b..7fe5b1088 100644 --- a/theories/Ints/num/ZMake.v +++ b/theories/Ints/num/ZMake.v @@ -1,4 +1,8 @@ Require Import ZArith. +Require Import ZAux. +Require Import ZDivModAux. + +Open Scope Z_scope. Module Type NType. @@ -9,25 +13,79 @@ Module Type NType. Parameter of_N : N -> t. Parameter to_Z : t -> Z. + Parameter spec_pos: forall x, 0 <= to_Z x. + Parameter spec_0: to_Z zero = 0. + Parameter spec_1: to_Z one = 1. + Parameter spec_of_N: forall x, to_Z (of_N x) = Z_of_N x. Parameter compare : t -> t -> comparison. + + Parameter spec_compare: forall x y, + match compare x y with + Eq => to_Z x = to_Z y + | Lt => to_Z x < to_Z y + | Gt => to_Z x > to_Z y + end. + Parameter eq_bool : t -> t -> bool. + Parameter spec_eq_bool: forall x y, + if eq_bool x y then to_Z x = to_Z y else to_Z x <> to_Z y. + Parameter succ : t -> t. + + Parameter spec_succ: forall n, to_Z (succ n) = to_Z n + 1. + Parameter add : t -> t -> t. + + Parameter spec_add: forall x y, to_Z (add x y) = to_Z x + to_Z y. + Parameter pred : t -> t. + + Parameter spec_pred: forall x, 0 < to_Z x -> to_Z (pred x) = to_Z x - 1. + Parameter sub : t -> t -> t. + Parameter spec_sub: forall x y, to_Z y <= to_Z x -> + to_Z (sub x y) = to_Z x - to_Z y. + Parameter mul : t -> t -> t. + + Parameter spec_mul: forall x y, to_Z (mul x y) = to_Z x * to_Z y. + Parameter square : t -> t. + + Parameter spec_square: forall x, to_Z (square x) = to_Z x * to_Z x. + Parameter power_pos : t -> positive -> t. + + Parameter spec_power_pos: forall x n, to_Z (power_pos x n) = to_Z x ^ Zpos n. + Parameter sqrt : t -> t. + Parameter spec_sqrt: forall x, to_Z (sqrt x) ^ 2 <= to_Z x < (to_Z (sqrt x) + 1) ^ 2. + Parameter div_eucl : t -> t -> t * t. + + Parameter spec_div_eucl: forall x y, + 0 < to_Z y -> + let (q,r) := div_eucl x y in (to_Z q, to_Z r) = (Zdiv_eucl (to_Z x) (to_Z y)). + Parameter div : t -> t -> t. + + Parameter spec_div: forall x y, + 0 < to_Z y -> to_Z (div x y) = to_Z x / to_Z y. + Parameter modulo : t -> t -> t. + + Parameter spec_modulo: + forall x y, 0 < to_Z y -> to_Z (modulo x y) = to_Z x mod to_Z y. + Parameter gcd : t -> t -> t. + Parameter spec_gcd: forall a b, to_Z (gcd a b) = Zgcd (to_Z a) (to_Z b). + + End NType. Module Make (N:NType). @@ -55,6 +113,18 @@ Module Make (N:NType). | Neg nx => Zopp (N.to_Z nx) end. + Theorem spec_0: to_Z zero = 0. + exact N.spec_0. + Qed. + + Theorem spec_1: to_Z one = 1. + exact N.spec_1. + Qed. + + Theorem spec_m1: to_Z minus_one = -1. + simpl; rewrite N.spec_1; auto. + Qed. + Definition compare x y := match x, y with | Pos nx, Pos ny => N.compare nx ny @@ -71,12 +141,43 @@ Module Make (N:NType). | Neg nx, Neg ny => N.compare ny nx end. + + Theorem spec_compare: forall x y, + match compare x y with + Eq => to_Z x = to_Z y + | Lt => to_Z x < to_Z y + | Gt => to_Z x > to_Z y + end. + unfold compare, to_Z; intros x y; case x; case y; clear x y; + intros x y; auto; generalize (N.spec_pos x) (N.spec_pos y). + generalize (N.spec_compare y x); case N.compare; auto with zarith. + generalize (N.spec_compare y N.zero); case N.compare; + try rewrite N.spec_0; auto with zarith. + generalize (N.spec_compare x N.zero); case N.compare; + rewrite N.spec_0; auto with zarith. + generalize (N.spec_compare x N.zero); case N.compare; + rewrite N.spec_0; auto with zarith. + generalize (N.spec_compare N.zero y); case N.compare; + try rewrite N.spec_0; auto with zarith. + generalize (N.spec_compare N.zero x); case N.compare; + rewrite N.spec_0; auto with zarith. + generalize (N.spec_compare N.zero x); case N.compare; + rewrite N.spec_0; auto with zarith. + generalize (N.spec_compare x y); case N.compare; auto with zarith. + Qed. + Definition eq_bool x y := match compare x y with | Eq => true | _ => false end. + Theorem spec_eq_bool: forall x y, + if eq_bool x y then to_Z x = to_Z y else to_Z x <> to_Z y. + intros x y; unfold eq_bool; + generalize (spec_compare x y); case compare; auto with zarith. + Qed. + Definition cmp_sign x y := match x, y with | Pos nx, Neg ny => @@ -93,12 +194,22 @@ Module Make (N:NType). end. Definition abs x := Pos (to_N x). + + Theorem spec_abs: forall x, to_Z (abs x) = Zabs (to_Z x). + intros x; case x; clear x; intros x; assert (F:=N.spec_pos x). + simpl; rewrite Zabs_eq; auto. + simpl; rewrite Zabs_non_eq; simpl; auto with zarith. + Qed. Definition opp x := match x with | Pos nx => Neg nx | Neg nx => Pos nx end. + + Theorem spec_opp: forall x, to_Z (opp x) = - to_Z x. + intros x; case x; simpl; auto with zarith. + Qed. Definition succ x := match x with @@ -110,6 +221,16 @@ Module Make (N:NType). end end. + Theorem spec_succ: forall n, to_Z (succ n) = to_Z n + 1. + intros x; case x; clear x; intros x. + exact (N.spec_succ x). + simpl; generalize (N.spec_compare N.zero x); case N.compare; + rewrite N.spec_0; simpl. + intros HH; rewrite <- HH; rewrite N.spec_1; ring. + intros HH; rewrite N.spec_pred; auto with zarith. + generalize (N.spec_pos x); auto with zarith. + Qed. + Definition add x y := match x, y with | Pos nx, Pos ny => Pos (N.add nx ny) @@ -127,6 +248,20 @@ Module Make (N:NType). end | Neg nx, Neg ny => Neg (N.add nx ny) end. + + Theorem spec_add: forall x y, to_Z (add x y) = to_Z x + to_Z y. + unfold add, to_Z; intros [x | x] [y | y]. + exact (N.spec_add x y). + unfold zero; generalize (N.spec_compare x y); case N.compare. + rewrite N.spec_0; auto with zarith. + intros; rewrite N.spec_sub; try ring; auto with zarith. + intros; rewrite N.spec_sub; try ring; auto with zarith. + unfold zero; generalize (N.spec_compare x y); case N.compare. + rewrite N.spec_0; auto with zarith. + intros; rewrite N.spec_sub; try ring; auto with zarith. + intros; rewrite N.spec_sub; try ring; auto with zarith. + intros; rewrite N.spec_add; try ring; auto with zarith. + Qed. Definition pred x := match x with @@ -138,6 +273,15 @@ Module Make (N:NType). | Neg nx => Neg (N.succ nx) end. + Theorem spec_pred: forall x, to_Z (pred x) = to_Z x - 1. + unfold pred, to_Z, minus_one; intros [x | x]. + generalize (N.spec_compare N.zero x); case N.compare; + rewrite N.spec_0; try rewrite N.spec_1; auto with zarith. + intros H; exact (N.spec_pred _ H). + generalize (N.spec_pos x); auto with zarith. + rewrite N.spec_succ; ring. + Qed. + Definition sub x y := match x, y with | Pos nx, Pos ny => @@ -156,6 +300,20 @@ Module Make (N:NType). end end. + Theorem spec_sub: forall x y, to_Z (sub x y) = to_Z x - to_Z y. + unfold sub, to_Z; intros [x | x] [y | y]. + unfold zero; generalize (N.spec_compare x y); case N.compare. + rewrite N.spec_0; auto with zarith. + intros; rewrite N.spec_sub; try ring; auto with zarith. + intros; rewrite N.spec_sub; try ring; auto with zarith. + rewrite N.spec_add; ring. + rewrite N.spec_add; ring. + unfold zero; generalize (N.spec_compare x y); case N.compare. + rewrite N.spec_0; auto with zarith. + intros; rewrite N.spec_sub; try ring; auto with zarith. + intros; rewrite N.spec_sub; try ring; auto with zarith. + Qed. + Definition mul x y := match x, y with | Pos nx, Pos ny => Pos (N.mul nx ny) @@ -164,12 +322,21 @@ Module Make (N:NType). | Neg nx, Neg ny => Pos (N.mul nx ny) end. + + Theorem spec_mul: forall x y, to_Z (mul x y) = to_Z x * to_Z y. + unfold mul, to_Z; intros [x | x] [y | y]; rewrite N.spec_mul; ring. + Qed. + Definition square x := match x with | Pos nx => Pos (N.square nx) | Neg nx => Pos (N.square nx) end. + Theorem spec_square: forall x, to_Z (square x) = to_Z x * to_Z x. + unfold square, to_Z; intros [x | x]; rewrite N.spec_square; ring. + Qed. + Definition power_pos x p := match x with | Pos nx => Pos (N.power_pos nx p) @@ -181,12 +348,40 @@ Module Make (N:NType). end end. + Theorem spec_power_pos: forall x n, to_Z (power_pos x n) = to_Z x ^ Zpos n. + assert (F0: forall x, (-x)^2 = x^2). + intros x; rewrite Zpower_2; ring. + unfold power_pos, to_Z; intros [x | x] [p | p |]; + try rewrite N.spec_power_pos; try ring. + assert (F: 0 <= 2 * Zpos p). + assert (0 <= Zpos p); auto with zarith. + rewrite Zpos_xI; repeat rewrite Zpower_exp; auto with zarith. + repeat rewrite Zpower_mult; auto with zarith. + rewrite F0; ring. + assert (F: 0 <= 2 * Zpos p). + assert (0 <= Zpos p); auto with zarith. + rewrite Zpos_xO; repeat rewrite Zpower_exp; auto with zarith. + repeat rewrite Zpower_mult; auto with zarith. + rewrite F0; ring. + Qed. + Definition sqrt x := match x with | Pos nx => Pos (N.sqrt nx) | Neg nx => Neg N.zero end. + + Theorem spec_sqrt: forall x, 0 <= to_Z x -> + to_Z (sqrt x) ^ 2 <= to_Z x < (to_Z (sqrt x) + 1) ^ 2. + unfold to_Z, sqrt; intros [x | x] H. + exact (N.spec_sqrt x). + replace (N.to_Z x) with 0. + rewrite N.spec_0; simpl Zpower; unfold Zpower_pos, iter_pos; + auto with zarith. + generalize (N.spec_pos x); auto with zarith. + Qed. + Definition div_eucl x y := match x, y with | Pos nx, Pos ny => @@ -194,7 +389,10 @@ Module Make (N:NType). (Pos q, Pos r) | Pos nx, Neg ny => let (q, r) := N.div_eucl nx ny in - (Neg q, Pos r) + match N.compare N.zero r with + | Eq => (Neg q, zero) + | _ => (Neg (N.succ q), Neg (N.sub ny r)) + end | Neg nx, Pos ny => let (q, r) := N.div_eucl nx ny in match N.compare N.zero r with @@ -203,16 +401,114 @@ Module Make (N:NType). end | Neg nx, Neg ny => let (q, r) := N.div_eucl nx ny in - match N.compare N.zero r with - | Eq => (Pos q, zero) - | _ => (Pos (N.succ q), Pos (N.sub ny r)) - end + (Pos q, Neg r) end. + + Theorem spec_div_eucl: forall x y, + to_Z y <> 0 -> + let (q,r) := div_eucl x y in + (to_Z q, to_Z r) = Zdiv_eucl (to_Z x) (to_Z y). + unfold div_eucl, to_Z; intros [x | x] [y | y] H. + assert (H1: 0 < N.to_Z y). + generalize (N.spec_pos y); auto with zarith. + generalize (N.spec_div_eucl x y H1); case N.div_eucl; auto. + assert (HH: 0 < N.to_Z y). + generalize (N.spec_pos y); auto with zarith. + generalize (N.spec_div_eucl x y HH); case N.div_eucl; auto. + intros q r; generalize (N.spec_pos x) HH; unfold Zdiv_eucl; + case_eq (N.to_Z x); case_eq (N.to_Z y); + try (intros; apply False_ind; auto with zarith; fail). + intros p He1 He2 _ _ H1; injection H1; intros H2 H3. + generalize (N.spec_compare N.zero r); case N.compare; + unfold zero; rewrite N.spec_0; try rewrite H3; auto. + rewrite H2; intros; apply False_ind; auto with zarith. + rewrite H2; intros; apply False_ind; auto with zarith. + intros p _ _ _ H1; discriminate H1. + intros p He p1 He1 H1 _. + generalize (N.spec_compare N.zero r); case N.compare. + change (- Zpos p) with (Zneg p). + unfold zero; lazy zeta. + rewrite N.spec_0; intros H2; rewrite <- H2. + intros H3; rewrite <- H3; auto. + rewrite N.spec_0; intros H2. + change (- Zpos p) with (Zneg p); lazy iota beta. + intros H3; rewrite <- H3; auto. + rewrite N.spec_succ; rewrite N.spec_sub. + generalize H2; case (N.to_Z r). + intros; apply False_ind; auto with zarith. + intros p2 _; rewrite He; auto with zarith. + change (Zneg p) with (- (Zpos p)); apply f_equal2 with (f := @pair Z Z); ring. + intros p2 H4; discriminate H4. + assert (N.to_Z r = (Zpos p1 mod (Zpos p))). + unfold Zmod, Zdiv_eucl; rewrite <- H3; auto. + case (Z_mod_lt (Zpos p1) (Zpos p)); auto with zarith. + rewrite N.spec_0; intros H2; generalize (N.spec_pos r); + intros; apply False_ind; auto with zarith. + assert (HH: 0 < N.to_Z y). + generalize (N.spec_pos y); auto with zarith. + generalize (N.spec_div_eucl x y HH); case N.div_eucl; auto. + intros q r; generalize (N.spec_pos x) HH; unfold Zdiv_eucl; + case_eq (N.to_Z x); case_eq (N.to_Z y); + try (intros; apply False_ind; auto with zarith; fail). + intros p He1 He2 _ _ H1; injection H1; intros H2 H3. + generalize (N.spec_compare N.zero r); case N.compare; + unfold zero; rewrite N.spec_0; try rewrite H3; auto. + rewrite H2; intros; apply False_ind; auto with zarith. + rewrite H2; intros; apply False_ind; auto with zarith. + intros p _ _ _ H1; discriminate H1. + intros p He p1 He1 H1 _. + generalize (N.spec_compare N.zero r); case N.compare. + change (- Zpos p1) with (Zneg p1). + unfold zero; lazy zeta. + rewrite N.spec_0; intros H2; rewrite <- H2. + intros H3; rewrite <- H3; auto. + rewrite N.spec_0; intros H2. + change (- Zpos p1) with (Zneg p1); lazy iota beta. + intros H3; rewrite <- H3; auto. + rewrite N.spec_succ; rewrite N.spec_sub. + generalize H2; case (N.to_Z r). + intros; apply False_ind; auto with zarith. + intros p2 _; rewrite He; auto with zarith. + intros p2 H4; discriminate H4. + assert (N.to_Z r = (Zpos p1 mod (Zpos p))). + unfold Zmod, Zdiv_eucl; rewrite <- H3; auto. + case (Z_mod_lt (Zpos p1) (Zpos p)); auto with zarith. + rewrite N.spec_0; generalize (N.spec_pos r); intros; apply False_ind; auto with zarith. + assert (H1: 0 < N.to_Z y). + generalize (N.spec_pos y); auto with zarith. + generalize (N.spec_div_eucl x y H1); case N.div_eucl; auto. + intros q r; generalize (N.spec_pos x) H1; unfold Zdiv_eucl; + case_eq (N.to_Z x); case_eq (N.to_Z y); + try (intros; apply False_ind; auto with zarith; fail). + change (-0) with 0; lazy iota beta; auto. + intros p _ _ _ _ H2; injection H2. + intros H3 H4; rewrite H3; rewrite H4; auto. + intros p _ _ _ H2; discriminate H2. + intros p He p1 He1 _ _ H2. + change (- Zpos p1) with (Zneg p1); lazy iota beta. + change (- Zpos p) with (Zneg p); lazy iota beta. + rewrite <- H2; auto. + Qed. + Definition div x y := fst (div_eucl x y). + Definition spec_div: forall x y, + to_Z y <> 0 -> to_Z (div x y) = to_Z x / to_Z y. + intros x y H1; generalize (spec_div_eucl x y H1); unfold div, Zdiv. + case div_eucl; case Zdiv_eucl; simpl; auto. + intros q r q11 r1 H; injection H; auto. + Qed. + Definition modulo x y := snd (div_eucl x y). + Theorem spec_modulo: + forall x y, to_Z y <> 0 -> to_Z (modulo x y) = to_Z x mod to_Z y. + intros x y H1; generalize (spec_div_eucl x y H1); unfold modulo, Zmod. + case div_eucl; case Zdiv_eucl; simpl; auto. + intros q r q11 r1 H; injection H; auto. + Qed. + Definition gcd x y := match x, y with | Pos nx, Pos ny => Pos (N.gcd nx ny) @@ -221,4 +517,11 @@ Module Make (N:NType). | Neg nx, Neg ny => Pos (N.gcd nx ny) end. + Theorem spec_gcd: forall a b, to_Z (gcd a b) = Zgcd (to_Z a) (to_Z b). + unfold gcd, Zgcd, to_Z; intros [x | x] [y | y]; rewrite N.spec_gcd; unfold Zgcd; + auto; case N.to_Z; simpl; auto with zarith; + try rewrite Zabs_Zopp; auto; + case N.to_Z; simpl; auto with zarith. + Qed. + End Make. diff --git a/theories/Ints/num/genN.ml b/theories/Ints/num/genN.ml index 928a60402..936c61a65 100644 --- a/theories/Ints/num/genN.ml +++ b/theories/Ints/num/genN.ml @@ -44,12 +44,12 @@ let start_file post l = let print_Make () = let fmt = start_file "Make" [] in - fprintf fmt " (***************************************************************)\n"; - fprintf fmt " (* *)\n"; - fprintf fmt " (* File automatically generated DO NOT EDIT *)\n"; - fprintf fmt " (* Constructors: %i Generated Proofs: %b %s %s *)\n" size gen_proof (if size < 10 then " " else "") (if gen_proof then " " else ""); - fprintf fmt " (* *)\n"; - fprintf fmt " (***************************************************************)\n\n"; + fprintf fmt "(***************************************************************)\n"; + fprintf fmt "(* *)\n"; + fprintf fmt "(* File automatically generated DO NOT EDIT *)\n"; + fprintf fmt "(* Constructors: %i Generated Proofs: %b %s %s *)\n" size gen_proof (if size < 10 then " " else "") (if gen_proof then " " else ""); + fprintf fmt "(* *)\n"; + fprintf fmt "(***************************************************************)\n\n"; fprintf fmt "Module Type W0Type.\n"; @@ -138,6 +138,8 @@ let print_Make () = fprintf fmt " \n"; + + if gen_proof then begin fprintf fmt " (* Regular make op (no karatsuba) *)\n"; @@ -454,7 +456,7 @@ let print_Make () = - fprintf fmt " Theorem to_Z_pos: forall x, 0 <= [x].\n"; + fprintf fmt " Theorem spec_pos: forall x, 0 <= [x].\n"; if gen_proof then begin fprintf fmt " Proof.\n"; @@ -1022,7 +1024,7 @@ let print_Make () = fprintf fmt " end.\n"; fprintf fmt "\n"; - fprintf fmt " Theorem succ_spec: forall n, [succ n] = [n] + 1.\n"; + fprintf fmt " Theorem spec_succ: forall n, [succ n] = [n] + 1.\n"; if gen_proof then begin fprintf fmt " Proof.\n"; @@ -1157,7 +1159,7 @@ let print_Make () = fprintf fmt " end.\n"; fprintf fmt "\n"; - fprintf fmt " Let spec_pred: forall x, 0 < [x] -> [pred x] = [x] - 1.\n"; + fprintf fmt " Theorem spec_pred: forall x, 0 < [x] -> [pred x] = [x] - 1.\n"; if gen_proof then begin fprintf fmt " Proof.\n"; @@ -2039,7 +2041,7 @@ let print_Make () = fprintf fmt " Theorem spec_div_eucl: forall x y,\n"; fprintf fmt " 0 < [y] ->\n"; fprintf fmt " let (q,r) := div_eucl x y in\n"; - fprintf fmt " [q] = [x] / [y] /\\ [r] = [x] mod [y].\n"; + fprintf fmt " ([q], [r]) = Zdiv_eucl [x] [y].\n"; if gen_proof then begin fprintf fmt " Proof.\n"; @@ -2049,14 +2051,18 @@ let print_Make () = fprintf fmt " exact (spec_1 w0_spec).\n"; fprintf fmt " intros x y H; generalize (spec_compare x y);\n"; fprintf fmt " unfold div_eucl; case compare; try rewrite F0;\n"; - fprintf fmt " try rewrite F1; intros; try split; auto with zarith.\n"; - fprintf fmt " rewrite H0; apply sym_equal; apply Z_div_same; auto with zarith.\n"; - fprintf fmt " rewrite H0; apply sym_equal; apply Z_mod_same; auto with zarith.\n"; - fprintf fmt " apply sym_equal; apply ZDivModAux.Zdiv_lt_0.\n"; - fprintf fmt " generalize (to_Z_pos x); auto with zarith.\n"; - fprintf fmt " apply sym_equal; apply ZAux.Zmod_def_small; auto with zarith.\n"; - fprintf fmt " generalize (to_Z_pos x); auto with zarith.\n"; - fprintf fmt " apply (spec_div_gt x y); auto.\n"; + fprintf fmt " try rewrite F1; intros; auto with zarith.\n"; + fprintf fmt " rewrite H0; generalize (Z_div_same [y] (Zlt_gt _ _ H))\n"; + fprintf fmt " (Z_mod_same [y] (Zlt_gt _ _ H));\n"; + fprintf fmt " unfold Zdiv, Zmod; case Zdiv_eucl; intros; subst; auto.\n"; + fprintf fmt " assert (F2: 0 <= [x] < [y]).\n"; + fprintf fmt " generalize (spec_pos x); auto.\n"; + fprintf fmt " generalize (ZDivModAux.Zdiv_lt_0 _ _ F2)\n"; + fprintf fmt " (Zmod_def_small _ _ F2);\n"; + fprintf fmt " unfold Zdiv, Zmod; case Zdiv_eucl; intros; subst; auto.\n"; + fprintf fmt " generalize (spec_div_gt _ _ H0 H); auto.\n"; + fprintf fmt " unfold Zdiv, Zmod; case Zdiv_eucl; case div_gt.\n"; + fprintf fmt " intros a b c d (H1, H2); subst; auto.\n"; fprintf fmt " Qed.\n"; end else @@ -2073,7 +2079,8 @@ let print_Make () = fprintf fmt " Proof.\n"; fprintf fmt " intros x y H1; unfold div; generalize (spec_div_eucl x y H1);\n"; fprintf fmt " case div_eucl; simpl fst.\n"; - fprintf fmt " intros xx yy (H2, H3); auto with zarith.\n"; + fprintf fmt " intros xx yy; unfold Zdiv; case Zdiv_eucl; intros qq rr H; \n"; + fprintf fmt " injection H; auto.\n"; fprintf fmt " Qed.\n"; end else @@ -2202,7 +2209,7 @@ let print_Make () = fprintf fmt " try rewrite F1; intros; try split; auto with zarith.\n"; fprintf fmt " rewrite H0; apply sym_equal; apply Z_mod_same; auto with zarith.\n"; fprintf fmt " apply sym_equal; apply ZAux.Zmod_def_small; auto with zarith.\n"; - fprintf fmt " generalize (to_Z_pos x); auto with zarith.\n"; + fprintf fmt " generalize (spec_pos x); auto with zarith.\n"; fprintf fmt " apply spec_mod_gt; auto.\n"; fprintf fmt " Qed.\n"; end @@ -3122,10 +3129,10 @@ let print_Make () = begin fprintf fmt " Proof.\n"; fprintf fmt " intros x.\n"; - fprintf fmt " assert (F1:= to_Z_pos (head0 x)).\n"; + fprintf fmt " assert (F1:= spec_pos (head0 x)).\n"; fprintf fmt " assert (F2: 0 < Zpos (digits x)).\n"; fprintf fmt " red; auto.\n"; - fprintf fmt " case (Zle_lt_or_eq _ _ (to_Z_pos x)); intros HH.\n"; + fprintf fmt " case (Zle_lt_or_eq _ _ (spec_pos x)); intros HH.\n"; fprintf fmt " generalize HH; rewrite <- (spec_double_size x); intros HH1.\n"; fprintf fmt " case (spec_head0 x HH); intros _ HH2.\n"; fprintf fmt " case (spec_head0 _ HH1).\n"; @@ -3136,7 +3143,7 @@ let print_Make () = fprintf fmt " apply Zle_not_lt.\n"; fprintf fmt " apply Zmult_le_compat_r; auto with zarith.\n"; fprintf fmt " apply Zpower_le_monotone; auto; auto with zarith.\n"; - fprintf fmt " generalize (to_Z_pos (head0 (double_size x))); auto with zarith.\n"; + fprintf fmt " generalize (spec_pos (head0 (double_size x))); auto with zarith.\n"; fprintf fmt " assert (HH5: 2 ^[head0 x] <= 2 ^(Zpos (digits x) - 1)).\n"; fprintf fmt " case (Zle_lt_or_eq 1 [x]); auto with zarith; intros HH5.\n"; fprintf fmt " apply Zmult_le_reg_r with (2 ^ 1); auto with zarith.\n"; @@ -3182,10 +3189,10 @@ let print_Make () = fprintf fmt " intros x.\n"; fprintf fmt " assert (F: 0 < Zpos (digits x)).\n"; fprintf fmt " red; auto.\n"; - fprintf fmt " case (Zle_lt_or_eq _ _ (to_Z_pos (head0 (double_size x)))); auto; intros F0.\n"; - fprintf fmt " case (Zle_lt_or_eq _ _ (to_Z_pos (head0 x))); intros F1.\n"; + fprintf fmt " case (Zle_lt_or_eq _ _ (spec_pos (head0 (double_size x)))); auto; intros F0.\n"; + fprintf fmt " case (Zle_lt_or_eq _ _ (spec_pos (head0 x))); intros F1.\n"; fprintf fmt " apply Zlt_le_trans with (2 := (spec_double_size_head0 x)); auto with zarith.\n"; - fprintf fmt " case (Zle_lt_or_eq _ _ (to_Z_pos x)); intros F3.\n"; + fprintf fmt " case (Zle_lt_or_eq _ _ (spec_pos x)); intros F3.\n"; fprintf fmt " generalize F3; rewrite <- (spec_double_size x); intros F4.\n"; fprintf fmt " absurd (2 ^ (Zpos (xO (digits x)) - 1) < 2 ^ (Zpos (digits x))).\n"; fprintf fmt " apply Zle_not_lt.\n"; @@ -3352,6 +3359,27 @@ let print_Make () = fprintf fmt " Admitted.\n"; fprintf fmt "\n"; + fprintf fmt " Theorem spec_0: [zero] = 0.\n"; + if gen_proof then + begin + fprintf fmt " Proof.\n"; + fprintf fmt " exact (spec_0 w0_spec).\n"; + fprintf fmt " Qed.\n"; + end + else + fprintf fmt " Admitted.\n"; + fprintf fmt "\n"; + + fprintf fmt " Theorem spec_1: [one] = 1.\n"; + if gen_proof then + begin + fprintf fmt " Proof.\n"; + fprintf fmt " exact (spec_1 w0_spec).\n"; + fprintf fmt " Qed.\n"; + end + else + fprintf fmt " Admitted.\n"; + fprintf fmt "\n"; fprintf fmt "End Make.\n"; |