diff options
Diffstat (limited to 'coqprime/num')
| -rw-r--r-- | coqprime/num/Lucas.v | 213 | ||||
| -rw-r--r-- | coqprime/num/MEll.v | 1228 | ||||
| -rw-r--r-- | coqprime/num/Mod_op.v | 1200 | ||||
| -rw-r--r-- | coqprime/num/NEll.v | 983 | ||||
| -rw-r--r-- | coqprime/num/Pock.v | 964 | ||||
| -rw-r--r-- | coqprime/num/W.v | 200 |
6 files changed, 0 insertions, 4788 deletions
diff --git a/coqprime/num/Lucas.v b/coqprime/num/Lucas.v deleted file mode 100644 index dfd3e8142..000000000 --- a/coqprime/num/Lucas.v +++ /dev/null @@ -1,213 +0,0 @@ - -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) - -Set Implicit Arguments. - -Require Import ZArith Znumtheory Zpow_facts. -Require Import CyclicAxioms DoubleCyclic BigN Cyclic31 Int31. -Require Import ZCAux. -Require Import W. -Require Import Mod_op. -Require Import LucasLehmer. -Require Import Coqprime.Bits. -Import CyclicAxioms DoubleType DoubleBase. - -Open Scope Z_scope. - -Section test. - -Variable w: Type. -Variable w_op: ZnZ.Ops w. -Variable op_spec: ZnZ.Specs w_op. -Variable p: positive. -Variable b: w. - -Notation "[| x |]" := - (ZnZ.to_Z x) (at level 0, x at level 99). - - -Hypothesis p_more_1: 2 < Zpos p. -Hypothesis b_p: [|b|] = 2 ^ Zpos p - 1. - -Lemma b_pos: 0 < [|b|]. -rewrite b_p; auto with zarith. -assert (2 ^ 0 < 2 ^ Zpos p); auto with zarith. -apply Zpower_lt_monotone; auto with zarith. -rewrite Zpower_0_r in H; auto with zarith. -Qed. - -Hint Resolve b_pos. - -Variable m_op: mod_op w. -Variable m_op_spec: mod_spec w_op b m_op. - -Let w2 := m_op.(add_mod) ZnZ.one ZnZ.one. - -Lemma w1_b: [|ZnZ.one|] = 1 mod [|b|]. -rewrite ZnZ.spec_1; simpl; auto. -rewrite Zmod_small; auto with zarith. -split; auto with zarith. -rewrite b_p. -assert (2 ^ 1 < 2 ^ Zpos p); auto with zarith. -apply Zpower_lt_monotone; auto with zarith. -rewrite Zpower_1_r in H; auto with zarith. -Qed. - -Lemma w2_b: [|w2|] = 2 mod [|b|]. -unfold w2; rewrite (add_mod_spec m_op_spec _ _ _ _ w1_b w1_b). -rewrite w1_b; rewrite <- Zplus_mod; auto with zarith. -Qed. - -Let w4 := m_op.(add_mod) w2 w2. - -Lemma w4_b: [|w4|] = 4 mod [|b|]. -unfold w4; rewrite (add_mod_spec m_op_spec _ _ _ _ w2_b w2_b). -rewrite w2_b; rewrite <- Zplus_mod; auto with zarith. -Qed. - -Let square_m2 := - let square := m_op.(square_mod) in - let sub := m_op.(sub_mod) in - fun x => sub (square x) w2. - -Definition lucastest := - ZnZ.to_Z (iter_pos (Pminus p 2) _ square_m2 w4). - -Theorem lucastest_aux_correct: - forall p1 z n, 0 <= n -> [|z|] = fst (s n) mod (2 ^ Zpos p - 1) -> - [|iter_pos p1 _ square_m2 z|] = fst (s (n + Zpos p1)) mod (2 ^ Zpos p - 1). -intros p1; pattern p1; apply Pind; simpl iter_pos; simpl s; clear p1. -intros z p1 Hp1 H. -unfold square_m2. -rewrite <- b_p in H. -generalize (square_mod_spec m_op_spec _ _ H); intros H1. -rewrite (sub_mod_spec m_op_spec _ _ _ _ H1 w2_b). -rewrite H1; rewrite w2_b; auto with zarith. -rewrite H; rewrite <- Zmult_mod; auto with zarith. -rewrite <- Zminus_mod; auto with zarith. -rewrite sn; simpl; auto with zarith. -rewrite b_p; auto. -intros p1 Rec w1 z Hz Hw1. -rewrite Pplus_one_succ_l; rewrite iter_pos_plus; - simpl iter_pos. -match goal with |- context[square_m2 ?X] => - set (tmp := X); unfold square_m2; unfold tmp; clear tmp -end. -generalize (Rec _ _ Hz Hw1); intros H1. -rewrite <- b_p in H1. -generalize (square_mod_spec m_op_spec _ _ H1); intros H2. -rewrite (sub_mod_spec m_op_spec _ _ _ _ H2 w2_b). -rewrite H2; rewrite w2_b; auto with zarith. -rewrite H1; rewrite <- Zmult_mod; auto with zarith. -rewrite <- Zminus_mod; auto with zarith. -replace (z + Zpos (1 + p1)) with ((z + Zpos p1) + 1); auto with zarith. -rewrite sn; simpl fst; try rewrite b_p; auto with zarith. -rewrite Zpos_plus_distr; auto with zarith. -Qed. - -Theorem lucastest_prop: lucastest = fst(s (Zpos p -2)) mod (2 ^ Zpos p - 1). -unfold lucastest. -assert (F: 0 <= 0); auto with zarith. -generalize (lucastest_aux_correct (p -2) w4 F); simpl Zplus; - rewrite Zpos_minus; auto with zarith. -rewrite Zmax_right; auto with zarith. -intros tmp; apply tmp; clear tmp. -rewrite <- b_p; simpl; exact w4_b. -Qed. - -Theorem lucastest_prop_cor: lucastest = 0 -> (2 ^ Zpos p - 1 | fst(s (Zpos p - 2)))%Z. -intros H. -apply Zmod_divide. -assert (H1: 2 ^ 1 < 2 ^ Zpos p); auto with zarith. -apply Zpower_lt_monotone; auto with zarith. -rewrite Zpower_1_r in H1; auto with zarith. -apply trans_equal with (2:= H); apply sym_equal; apply lucastest_prop; auto. -Qed. - -Theorem lucastest_prime: lucastest = 0 -> prime (2 ^ Zpos p - 1). -intros H1; case (prime_dec (2 ^ Zpos p - 1)); auto; intros H2. -case Zdivide_div_prime_le_square with (2 := H2). -assert (H3: 2 ^ 1 < 2 ^ Zpos p); auto with zarith. -apply Zpower_lt_monotone; auto with zarith. -rewrite Zpower_1_r in H3; auto with zarith. -intros q (H3, (H4, H5)). -contradict H5; apply Zlt_not_le. -generalize q_more_than_square; unfold Mp; intros tmp; apply tmp; - auto; clear tmp. -apply lucastest_prop_cor; auto. -case (Zle_lt_or_eq 2 q); auto. -apply prime_ge_2; auto. -intros H5; subst. -absurd (2 <= 1); auto with arith. -apply Zdivide_le; auto with zarith. -case H4; intros x Hx. -exists (2 ^ (Zpos p -1) - x). -rewrite Zmult_minus_distr_r; rewrite <- Hx; unfold Mp. -pattern 2 at 2; rewrite <- Zpower_1_r; rewrite <- Zpower_exp; auto with zarith. -replace (Zpos p - 1 + 1) with (Zpos p); auto with zarith. -Qed. - -End test. - -Definition znz_of_Z (w: Type) (op: ZnZ.Ops w) z := - match z with - | Zpos p => snd (ZnZ.of_pos p) - | _ => ZnZ.zero - end. - -Definition lucas p := - let op := cmk_op (Peano.pred (nat_of_P (get_height 31 p))) in - let b := znz_of_Z op (Zpower 2 (Zpos p) - 1) in - let zp := znz_of_Z op (Zpos p) in - let mod_op := mmake_mod_op op b zp in - lucastest op p mod_op. - -Theorem lucas_prime: - forall p, 2 < Zpos p -> lucas p = 0 -> prime (2 ^ Zpos p - 1). -unfold lucas; intros p Hp H. -match type of H with lucastest (cmk_op ?x) ?y ?z = _ => - set (w_op := (cmk_op x)); assert(A1: ZnZ.Specs w_op) -end. -unfold w_op; apply cmk_spec. -assert (F0: Zpos p <= Zpos (ZnZ.digits w_op)). -unfold w_op, base; rewrite (cmk_op_digits (Peano.pred (nat_of_P (get_height 31 p)))). -generalize (get_height_correct 31 p). -replace (Z_of_nat (Peano.pred (nat_of_P (get_height 31 p)))) with - ((Zpos (get_height 31 p) - 1) ); auto with zarith. -rewrite pred_of_minus; rewrite inj_minus1; auto with zarith. -rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto with zarith. -generalize (lt_O_nat_of_P (get_height 31 p)); auto with zarith. -assert (F1: ZnZ.to_Z (znz_of_Z w_op (2 ^ (Zpos p) - 1)) = 2 ^ (Zpos p) - 1). -assert (F1: 0 < 2 ^ (Zpos p) - 1). -assert (F2: 2 ^ 0 < 2 ^ (Zpos p)); auto with zarith. -apply Zpower_lt_monotone; auto with zarith. -rewrite Zpower_0_r in F2; auto with zarith. -case_eq (2 ^ (Zpos p) - 1); simpl ZnZ.to_Z. -intros HH; contradict F1; rewrite HH; auto with zarith. -2: intros p1 HH; contradict F1; rewrite HH; - apply Zle_not_lt; red; simpl; intros; discriminate. -intros p1 Hp1; apply ZnZ.of_pos_correct; auto. -rewrite <- Hp1. -unfold base. -apply Zlt_le_trans with (2 ^ (Zpos p)); auto with zarith. -apply Zpower_le_monotone; auto with zarith. -match type of H with lucastest (cmk_op ?x) ?y ?z = _ => - apply - (@lucastest_prime _ _ (cmk_spec x) p (znz_of_Z w_op (2 ^ Zpos p -1)) Hp F1 z) -end; auto with zarith; fold w_op. -eapply mmake_mod_spec with (p := p); auto with zarith. -unfold znz_of_Z; unfold znz_of_Z in F1; rewrite F1. -assert (F2: 2 ^ 1 < 2 ^ (Zpos p)); auto with zarith. -apply Zpower_lt_monotone; auto with zarith. -rewrite Zpower_1_r in F2; auto with zarith. -rewrite ZnZ.of_Z_correct; auto with zarith. -split; auto with zarith. -apply Zle_lt_trans with (1 := F0); auto with zarith. -unfold base; apply Zpower2_lt_lin; auto with zarith. -Qed. - diff --git a/coqprime/num/MEll.v b/coqprime/num/MEll.v deleted file mode 100644 index afcdf4146..000000000 --- a/coqprime/num/MEll.v +++ /dev/null @@ -1,1228 +0,0 @@ - -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) - - -Require Import ZArith Znumtheory Zpow_facts. -Require Import Int31 ZEll montgomery. - -Set Implicit Arguments. - -Open Scope Z_scope. - - -Record ex: Set := mkEx { - vN : positive; - vS : positive; - vR: List.list (positive * positive); - vA: Z; - vB: Z; - vx: Z; - vy: Z -}. - -Coercion Local Zpos : positive >-> Z. - -Record ex_spec (exx: ex): Prop := mkExS { - n2_div: ~(2 | exx.(vN)); - n_pos: 2 < exx.(vN); - lprime: - forall p : positive * positive, List.In p (vR exx) -> prime (fst p); - lbig: - 4 * vN exx < (Zmullp (vR exx) - 1) ^ 2; - inC: - vy exx ^ 2 mod vN exx = (vx exx ^ 3 + vA exx * vx exx + vB exx) mod vN exx -}. - -(* -Let is_even m := -Fixpoint invM_aux (n : nat) (m v: int31) : int31 := - match n with 0%nat => 0%int31 | S n => - if (iszero (Cyclic31.nshiftl 30 m)) then - lsl (invM_aux n (lsr m 1) v) 1 - else (1 lor (lsl (invM_aux n (lsr (m - v) 1) v) 1)) - end. - -Definition invM := invM_aux 31. - -Lemma invM_spec m v : - is_even v = false -> (v * (invM m v) = m)%int31. -Proof. admit. Qed. - -Inductive melt: Type := - mzero | mtriple: number -> number -> number -> melt. - -(* Montgomery version *) -Section MEll. - -Variable add_mod sub_mod mult_mod : number -> number -> number. - -Notation "x ++ y " := (add_mod x y). -Notation "x -- y" := (sub_mod x y) (at level 50, left associativity). -Notation "x ** y" := - (mult_mod x y) (at level 40, left associativity). -Notation "x ?= y" := (eq_num x y). - -Variable A c0 c2 c3 : number. - -Definition mdouble : number -> melt -> (melt * number):= - fun (sc: number) (p1: melt) => - match p1 with - mzero => (p1, sc) - | (mtriple x1 y1 z1) => - if (y1 ?= c0) then (mzero, z1 ** sc) else - (* we do 2p *) - let m' := c3 ** x1 ** x1 ++ A ** z1 ** z1 in - let l' := c2 ** y1 ** z1 in - let m'2 := m' ** m' in - let l'2 := l' ** l' in - let l'3 := l'2 ** l' in - let x3 := m'2 ** z1 -- c2 ** x1 ** l'2 in - (mtriple - (l' ** x3) - (l'2 ** (m' ** x1 -- y1 ** l') -- m' ** x3) - (z1 ** l'3), sc) - end. - -Definition madd := fun (sc : number) (p1 p2 : melt) => - match p1, p2 with - mzero, _ => (p2, sc) - | _ , mzero => (p1, sc) - | (mtriple x1 y1 z1), (mtriple x2 y2 z2) => - let d1 := x2 ** z1 in - let d2 := x1 ** z2 in - let l := d1 -- d2 in - let dl := d1 ++ d2 in - let m := y2 ** z1 -- y1 ** z2 in - if (l ?= c0) then - (* we have p1 = p2 o p1 = -p2 *) - if (m ?= c0) then - if (y1 ?= c0) then (mzero, z1 ** z2 ** sc) else - (* we do 2p *) - let m' := c3 ** x1 ** x1 ++ A ** z1 ** z1 in - let l' := c2 ** y1 ** z1 in - let m'2 := m' ** m' in - let l'2 := l' ** l' in - let l'3 := l'2 ** l' in - let x3 := m'2 ** z1 -- c2 ** x1 ** l'2 in - (mtriple - (l' ** x3) - (l'2 ** (m' ** x1 -- y1 ** l') -- m' ** x3) - (z1 ** l'3), z2 ** sc) - else (* p - p *) (mzero, m ** z1 ** z2 ** sc) - else - let l2 := l ** l in - let l3 := l2 ** l in - let m2 := m ** m in - let x3 := z1 ** z2 ** m2 -- l2 ** dl in - (mtriple (l ** x3) - (z2 ** l2 ** (m ** x1 -- y1 ** l) -- m ** x3) - (z1 ** z2 ** l3), sc) - end. - -Definition mopp p := - match p with mzero => p | (mtriple x1 y1 z1) => (mtriple x1 (c0 -- y1) z1) end. - -End MEll. - -*) - -(* - -Section Scal. - -Variable mdouble : number -> melt -> melt * number. -Variable madd : number -> melt -> melt -> melt * number. -Variable mopp : melt -> melt. - - -Fixpoint scalb (sc: number) (b:bool) (a: melt) (p: positive) {struct p}: - melt * number := - match p with - xH => if b then mdouble sc a else (a,sc) - | xO p1 => let (a1, sc1) := scalb sc false a p1 in - if b then - let (a2, sc2) := mdouble sc1 a1 in - madd sc2 a a2 - else mdouble sc1 a1 - | xI p1 => let (a1, sc1) := scalb sc true a p1 in - if b then mdouble sc1 a1 - else - let (a2, sc2) := mdouble sc1 a1 in - madd sc2 (mopp a) a2 - end. - -Definition scal sc a p := scalb sc false a p. - -Definition scal_list sc a l := - List.fold_left - (fun (asc: melt * number) p1 => let (a,sc) := asc in scal sc a p1) l (a,sc). - -Variable mult_mod : number -> number -> number. -Notation "x ** y" := - (mult_mod x y) (at level 40, left associativity). - -Variable c0 : number. - -Fixpoint scalL (sc : number) (a: melt) (l: List.list positive) {struct l} : - (melt * number) := - match l with - List.nil => (a,sc) - | List.cons n l1 => - let (a1, sc1) := scal sc a n in - let (a2, sc2) := scal_list sc1 a l1 in - match a2 with - mzero => (mzero, c0) - | mtriple _ _ z => scalL (sc2 ** z) a1 l1 - end - end. - -End Scal. - -Definition isM2 p := - match p with - xH => false -| xO _ => false -| _ => true -end. - -Definition ell_test (N S: positive) (l: List.list (positive * positive)) - (A B x y: Z) := - if isM2 N then - match (4 * N) ?= (ZEll.Zmullp l - 1) ^ 2 with - Lt => - match y ^ 2 mod N ?= (x ^ 3 + A * x + B) mod N with - Eq => - let M := positive_to_num N in - let m' := invM (0 - 1) (nhead M) in - let n := length M in - let e := encode M m' n in - let d := decode M m' n in - let add_mod := add_mod M in - let sub_mod := sub_mod M in - let mult_mod := reduce_mult_num M m' n in - let mA := e A in - let mB := e B in - let c0 := e 0 in - let c1 := e 1 in - let c2 := e 2 in - let c3 := e 3 in - let c4 := e 4 in - let c27 := e 27 in - let mdouble := mdouble add_mod sub_mod mult_mod mA c0 c2 c3 in - let madd := madd add_mod sub_mod mult_mod mA c0 c2 c3 in - let mopp := mopp sub_mod c0 in - let scal := scal mdouble madd mopp in - let scalL := scalL mdouble madd mopp mult_mod c0 in - let da := add_mod in - let dm := mult_mod in - let isc := (da (dm (dm (dm c4 mA) mA) mA) (dm (dm c27 mB) mB)) in - let a := mtriple (e x) (e y) c1 in - let (a1, sc1) := scal isc a S in - let (S1,R1) := ZEll.psplit l in - let (a2, sc2) := scal sc1 a1 S1 in - let (a3, sc3) := scalL sc2 a2 R1 in - match a3 with - mzero => if (Zeq_bool (Zgcd (d sc3) N) 1) then true - else false - | _ => false - end - | _ => false - end - | _ => false - end - else false. - -Time Eval vm_compute in (ell_test - 329719147332060395689499 - 8209062 - (List.cons (40165264598163841%positive,1%positive) List.nil) - (-94080) - 9834496 - 0 - 3136). - -Time Eval vm_compute in (ell_test - 1384435372850622112932804334308326689651568940268408537 - 13077052794 - (List.cons (105867537178241517538435987563198410444088809%positive, 1%positive) List.nil) - (-677530058123796416781392907869501000001421915645008494) - 0 - (- 169382514530949104195348226967375250000355478911252124) - 1045670343788723904542107880373576189650857982445904291 -). - -*) - -(* -Variable M : number. -Variable m' : int. - -Definition n := length M. -Definition e z := encode M m' n z. -Definition d z := decode M m' n z. - -Variable exx: ex. -Variable exxs: ex_spec exx. - -Definition S := exx.(vS). -Definition R := exx.(vR). -Definition A := e exx.(vA). -Definition B := e exx.(vB). -Definition xx := e exx.(vx). -Definition yy := e exx.(vy). -Definition c3 := e 3. -Definition c2 := e 2. -Definition c1 := e 1. -Definition c0 := e 0. - -Definition pp := mtriple xx yy c1. - -Notation "x ++ y " := (add_mod M x y). -Notation "x -- y" := (sub_mod M x y) (at level 50, left associativity). -Notation "x ** y" := - (reduce_mult_num M m' n x y) (at level 40, left associativity). -Notation "x ?= y" := (eq_num x y). - -Definition mdouble : number -> melt -> (melt * number):= - fun (sc: number) (p1: melt) => - match p1 with - mzero => (p1, sc) - | (mtriple x1 y1 z1) => - if (y1 ?= c0) then (mzero, z1 ** sc) else - (* we do 2p *) - let m' := c3 ** x1 ** x1 ++ A ** z1 ** z1 in - let l' := c2 ** y1 ** z1 in - let m'2 := m' ** m' in - let l'2 := l' ** l' in - let l'3 := l'2 ** l' in - let x3 := m'2 ** z1 -- c2 ** x1 ** l'2 in - (mtriple - (l' ** x3) - (l'2 ** (m' ** x1 -- y1 ** l') -- m' ** x3) - (z1 ** l'3), sc) - end. - -End MEll. - -Print mdouble. - -Definition Ex := mkEx 101 99 nil 10 3 4 5. - -Check ( - let v := Eval lazy compute in mdouble - in - -Check (fun exx: ex => nN (mkMOp exx)). - - -Definition e z := encode nn nn' nT ll z. -Definition d z := decode nn nn' nT ll z. - -} - -Lemma nEx : to_Z nN = to_Z (cons nn nT). -Proof. unfold nn, nT; case nN; auto. Qed. - -Definition nn' := invM (0 - 1) nn. - -Notation phi := Int31Op.to_Z. - -Lemma nn'_spec : phi (nn * nn') = wB - 1. -Proof. -unfold nn'; rewrite invM_spec. -rewrite sub_spec, to_Z_0, to_Z_1; simpl; auto. -admit. -Qed. - -Definition ll := length nN. - - -Inductive melt: Type := - mzero | mtriple: number -> number -> number -> melt. - -Definition pp := mtriple xx yy c1. - -Definition mplus x y : number := add_mod x y nN. -Definition msub x y : number := sub_mod x y nN. -Definition mmult x y : number := reduce_mult_num nn nn' nT x y ll. -Definition meq x y : bool := eq_num x y. - -Notation "x ++ y " := (mplus x y). -Notation "x -- y" := (msub x y) (at level 50, left associativity). -Notation "x ** y" := (mmult x y) (at level 40, left associativity). -Notation "x ?= y" := (meq x y). - -Definition mdouble: number -> melt -> (melt * number):= - fun (sc: number) (p1: melt) => - match p1 with - mzero => (p1, sc) - | (mtriple x1 y1 z1) => - if (y1 ?= c0) then (mzero, z1 ** sc) else - (* we do 2p *) - let m' := c3 ** x1 ** x1 ++ A ** z1 ** z1 in - let l' := c2 ** y1 ** z1 in - let m'2 := m' ** m' in - let l'2 := l' ** l' in - let l'3 := l'2 ** l' in - let x3 := m'2 ** z1 -- c2 ** x1 ** l'2 in - (mtriple - (l' ** x3) - (l'2 ** (m' ** x1 -- y1 ** l') -- m' ** x3) - (z1 ** l'3), sc) - end. - -Definition madd := fun (sc : number) (p1 p2 : melt) => - match p1, p2 with - mzero, _ => (p2, sc) - | _ , mzero => (p1, sc) - | (mtriple x1 y1 z1), (mtriple x2 y2 z2) => - let d1 := x2 ** z1 in - let d2 := x1 ** z2 in - let l := d1 -- d2 in - let dl := d1 ++ d2 in - let m := y2 ** z1 -- y1 ** z2 in - if (l ?= c0) then - (* we have p1 = p2 o p1 = -p2 *) - if (m ?= c0) then - if (y1 ?= c0) then (mzero, z1 ** z2 ** sc) else - (* we do 2p *) - let m' := c3 ** x1 ** x1 ++ A ** z1 ** z1 in - let l' := c2 ** y1 ** z1 in - let m'2 := m' ** m' in - let l'2 := l' ** l' in - let l'3 := l'2 ** l' in - let x3 := m'2 ** z1 -- c2 ** x1 ** l'2 in - (mtriple - (l' ** x3) - (l'2 ** (m' ** x1 -- y1 ** l') -- m' ** x3) - (z1 ** l'3), z2 ** sc) - else (* p - p *) (mzero, m ** z1 ** z2 ** sc) - else - let l2 := l ** l in - let l3 := l2 ** l in - let m2 := m ** m in - let x3 := z1 ** z2 ** m2 -- l2 ** dl in - (mtriple (l ** x3) - (z2 ** l2 ** (m ** x1 -- y1 ** l) -- m ** x3) - (z1 ** z2 ** l3), sc) - end. - -Definition mopp p := - match p with mzero => p | (mtriple x1 y1 z1) => (mtriple x1 (c0 -- y1) z1) end. - -Fixpoint scalb (sc: number) (b:bool) (a: melt) (p: positive) {struct p}: - melt * number := - match p with - xH => if b then mdouble sc a else (a,sc) - | xO p1 => let (a1, sc1) := scalb sc false a p1 in - if b then - let (a2, sc2) := mdouble sc1 a1 in - madd sc2 a a2 - else mdouble sc1 a1 - | xI p1 => let (a1, sc1) := scalb sc true a p1 in - if b then mdouble sc1 a1 - else - let (a2, sc2) := mdouble sc1 a1 in - madd sc2 (mopp a) a2 - end. - -Definition scal sc a p := scalb sc false a p. - -Definition scal_list sc a l := - List.fold_left - (fun (asc: melt * number) p1 => let (a,sc) := asc in scal sc a p1) l (a,sc). - -Fixpoint scalL (sc : number) (a: melt) (l: List.list positive) {struct l} : - (melt * number) := - match l with - List.nil => (a,sc) - | List.cons n l1 => - let (a1, sc1) := scal sc a n in - let (a2, sc2) := scal_list sc1 a l1 in - match a2 with - mzero => (mzero, c0) - | mtriple _ _ z => scalL (sc2 ** z) a1 l1 - end - end. - -Definition zpow sc p n := - let (p,sc') := scal sc p n in - (p, Zgcd (d sc') (exx.(vN))). - -Definition e2E n := - match n with - mzero => ZEll.nzero - | mtriple x1 y1 z1 => ntriple (d x1) (d y1) (d z1) - end. - -Definition wft t := d t = (d t) mod (to_Z nN). - -Lemma vN_pos : 0 < exx.(vN). -Proof. red; simpl; auto. Qed. - -Hint Resolve vN_pos. - -Lemma mplusz x y : wft x -> wft y -> - d (x ++ y) = nplus (exx.(vN)) (d x) (d y). -Proof. -intros Hx Hy. -unfold d, mplus, nplus. -(* -rewrite decode_encode_add. -rewrite (mop_spec.(add_mod_spec) _ _ _ _ Hx Hy); auto. -rewrite <- z2ZN; auto. -*) -admit. -Qed. - -Lemma mplusw x y : wft x -> wft y -> wft (x ++ y). -Proof. -intros Hx Hy. -unfold wft. -(* -pattern (z2Z (x ++ y)) at 2; rewrite (nplusz Hx Hy). -unfold ZEll.nplus; rewrite z2ZN. -rewrite Zmod_mod; auto. -apply (nplusz Hx Hy). -*) -admit. -Qed. - -Lemma msubz x y : wft x -> wft y -> - d (x -- y) = ZEll.nsub (vN exx) (d x) (d y). -Proof. -intros Hx Hy. -(* -unfold z2Z, nsub. -rewrite (mop_spec.(sub_mod_spec) _ _ _ _ Hx Hy); auto. -rewrite <- z2ZN; auto. -*) -admit. -Qed. - -Lemma msubw x y : wft x -> wft y -> wft (x -- y). -Proof. -intros Hx Hy. -unfold wft. -(* -pattern (z2Z (x -- y)) at 2; rewrite (nsubz Hx Hy). -unfold ZEll.nsub; rewrite z2ZN. -rewrite Zmod_mod; auto. -apply (nsubz Hx Hy). -*) -admit. -Qed. - -Lemma mmulz x y : wft x -> wft y -> - d (x ** y) = ZEll.nmul (vN exx) (d x) (d y). -Proof. -intros Hx Hy. -(* -unfold z2Z, nmul. -rewrite (mop_spec.(mul_mod_spec) _ _ _ _ Hx Hy); auto. -rewrite <- z2ZN; auto. -*) -admit. -Qed. - -Lemma mmulw x y : wft x -> wft y -> wft (x ** y). -Proof. -intros Hx Hy. -unfold wft. -(* -pattern (z2Z (x ** y)) at 2; rewrite (nmulz Hx Hy). -unfold ZEll.nmul; rewrite z2ZN. -rewrite Zmod_mod; auto. -apply (nmulz Hx Hy). -*) -admit. -Qed. - -Hint Resolve mmulw mplusw msubw. - - -Definition wfe p := match p with - mtriple x y z => wft x /\ wft y /\ wft z -| _ => True -end. - -Lemma dx x : d (e x) = x mod exx.(vN). -Proof. -(* -unfold Z2z; intros x. -generalize (Z_mod_lt x exx.(vN)). -case_eq (x mod exx.(vN)). -intros _ _. -simpl; unfold z2Z; rewrite ZnZ.spec_0; auto. -intros p Hp HH; case HH; auto with zarith; clear HH. -intros _ HH1. -case (ZnZ.spec_to_Z zN). -generalize z2ZN; unfold z2Z; intros HH; rewrite HH; auto. -intros _ H0. -set (v := ZnZ.of_pos p); generalize HH1. -rewrite (ZnZ.spec_of_pos p); fold v. -case (fst v). - simpl; auto. -intros p1 H1. -contradict H0; apply Zle_not_lt. -apply Zlt_le_weak; apply Zle_lt_trans with (2:= H1). -apply Zle_trans with (1 * base (ZnZ.digits op) + 0); auto with zarith. -apply Zplus_le_compat; auto. -apply Zmult_gt_0_le_compat_r; auto with zarith. - case (ZnZ.spec_to_Z (snd v)); auto with zarith. - case p1; red; simpl; intros; discriminate. - case (ZnZ.spec_to_Z (snd v)); auto with zarith. -intros p Hp; case (Z_mod_lt x exx.(vN)); auto with zarith. -rewrite Hp; intros HH; case HH; auto. -*) -admit. -Qed. - -Lemma dx1 x : d (e x) = d (e x) mod [nN]. -Proof. -(* -unfold Z2z; intros x. -generalize (Z_mod_lt x exx.(vN)). -case_eq (x mod exx.(vN)). -intros _ _. -simpl; unfold z2Z; rewrite ZnZ.spec_0; auto. -intros p H1 H2. -case (ZnZ.spec_to_Z zN). -generalize z2ZN; unfold z2Z; intros HH; rewrite HH; auto. -intros _ H0. -case H2; auto with zarith; clear H2; intros _ H2. -rewrite Zmod_small; auto. -set (v := ZnZ.of_pos p). -split. - case (ZnZ.spec_to_Z (snd v)); auto. -generalize H2; rewrite (ZnZ.spec_of_pos p); fold v. -case (fst v). - simpl; auto. -intros p1 H. -contradict H0; apply Zle_not_lt. -apply Zlt_le_weak; apply Zle_lt_trans with (2:= H). -apply Zle_trans with (1 * base (ZnZ.digits op) + 0); auto with zarith. -apply Zplus_le_compat; auto. -apply Zmult_gt_0_le_compat_r; auto with zarith. - case (ZnZ.spec_to_Z (snd v)); auto with zarith. - case p1; red; simpl; intros; discriminate. - case (ZnZ.spec_to_Z (snd v)); auto with zarith. -intros p Hp; case (Z_mod_lt x exx.(vN)); auto with zarith. -rewrite Hp; intros HH; case HH; auto. -*) -admit. -Qed. - -Lemma c0w : wft c0. -Proof. apply dx1. Qed. - -Lemma c2w : wft c2. -Proof. apply dx1. Qed. - -Lemma c3w : wft c3. -Proof. apply dx1. Qed. - -Lemma Aw : wft A. -Proof. apply dx1. Qed. - -Hint Resolve c0w c2w c3w Aw. - -Ltac nw := - repeat (apply mplusw || apply msubw || apply mmulw || apply c2w || - apply c3w || apply Aw); auto. - -Lemma madd_wf x y sc : - wfe x -> wfe y -> wft sc -> - wfe (fst (madd sc x y)) /\ wft (snd (madd sc x y)). -Proof. -destruct x as [ | x1 y1 z1]; auto. -destruct y as [ | x2 y2 z2]; auto. -(* - intros (wfx1,(wfy1, wfz1)) (wfx2,(wfy2, wfz2)) wfsc; - simpl; auto. - case meq. - 2: repeat split; simpl; nw. - case meq. - 2: repeat split; simpl; nw. - case meq. - repeat split; simpl; nw; auto. - repeat split; simpl; nw; auto. -*) -admit. -Qed. - -(* - - Lemma ztest: forall x y, - x ?= y =Zeq_bool (z2Z x) (z2Z y). - Proof. - intros x y. - unfold neq. - rewrite (ZnZ.spec_compare x y); case Zcompare_spec; intros HH; - match goal with H: context[x] |- _ => - generalize H; clear H; intros HH1 - end. - symmetry; apply GZnZ.Zeq_iok; auto. - case_eq (Zeq_bool (z2Z x) (z2Z y)); intros H1; auto; - generalize HH1; generalize (Zeq_bool_eq _ _ H1); unfold z2Z; - intros HH; rewrite HH; auto with zarith. - case_eq (Zeq_bool (z2Z x) (z2Z y)); intros H1; auto; - generalize HH1; generalize (Zeq_bool_eq _ _ H1); unfold z2Z; - intros HH; rewrite HH; auto with zarith. - Qed. - - Lemma zc0: z2Z c0 = 0. - Proof. - unfold z2Z, c0, z2Z; simpl. - generalize ZnZ.spec_0; auto. - Qed. - - -Ltac iftac t := - match t with - context[if ?x ?= ?y then _ else _] => - case_eq (x ?= y) - end. - -Ltac ftac := match goal with - |- context[?x = ?y] => (iftac x); - let H := fresh "tmp" in - (try rewrite ztest; try rewrite zc0; intros H; - repeat ((rewrite nmulz in H || rewrite nplusz in H || rewrite nsubz in H); auto); - try (rewrite H; clear H)) - end. - -Require Import Zmod. - -Lemma c2ww: forall x, ZEll.nmul (vN exx) 2 x = ZEll.nmul (vN exx) (z2Z c2) x. -intros x; unfold ZEll.nmul. -unfold c2; rewrite z2Zx; rewrite Zmodml; auto. -Qed. -Lemma c3ww: forall x, ZEll.nmul (vN exx) 3 x = ZEll.nmul (vN exx) (z2Z c3) x. -intros x; unfold ZEll.nmul. -unfold c3; rewrite z2Zx; rewrite Zmodml; auto. -Qed. - -Lemma Aww: forall x, ZEll.nmul (vN exx) exx.(vA) x = ZEll.nmul (vN exx) (z2Z A) x. -intros x; unfold ZEll.nmul. -unfold A; rewrite z2Zx; rewrite Zmodml; auto. -Qed. - -Lemma nadd_correct: forall x y sc, - wfe x -> wfe y -> wft sc -> - e2E (fst (nadd sc x y)) = fst (ZEll.nadd exx.(vN) exx.(vA) (z2Z sc) (e2E x) (e2E y) )/\ - z2Z (snd (nadd sc x y)) = snd (ZEll.nadd exx.(vN) exx.(vA) (z2Z sc) (e2E x) (e2E y)). -Proof. -intros x; case x; clear; auto. -intros x1 y1 z1 y; case y; clear; auto. - intros x2 y2 z2 sc (wfx1,(wfy1, wfz1)) (wfx2,(wfy2, wfz2)) wfsc; simpl. - ftac. - ftac. - ftac. - simpl; split; auto. - repeat ((rewrite nmulz || rewrite nplusz || rewrite nsubz); auto). - simpl; split; auto. - repeat ((rewrite nmulz || rewrite nplusz || rewrite nsubz|| - rewrite c2ww || rewrite c3ww || rewrite Aww); try nw; auto). - rewrite nmulz; auto. - simpl; split; auto. - repeat ((rewrite nmulz || rewrite nplusz || rewrite nsubz); auto). - simpl; split; auto. - repeat ((rewrite nmulz || rewrite nplusz || rewrite nsubz || - rewrite c2ww || rewrite c3ww || rewrite Aww); try nw; auto). - Qed. - - Lemma ndouble_wf: forall x sc, - wfe x -> wft sc -> - wfe (fst (ndouble sc x)) /\ wft (snd (ndouble sc x)). -Proof. -intros x; case x; clear; auto. -intros x1 y1 z1 sc (wfx1,(wfy1, wfz1)) wfsc; - simpl; auto. - repeat (case neq; repeat split; simpl; nw; auto). -Qed. - - -Lemma ndouble_correct: forall x sc, - wfe x -> wft sc -> - e2E (fst (ndouble sc x)) = fst (ZEll.ndouble exx.(vN) exx.(vA) (z2Z sc) (e2E x))/\ - z2Z (snd (ndouble sc x)) = snd (ZEll.ndouble exx.(vN) exx.(vA) (z2Z sc) (e2E x)). -Proof. -intros x; case x; clear; auto. - intros x1 y1 z1 sc (wfx1,(wfy1, wfz1)) wfsc; simpl. - ftac. - simpl; split; auto. - repeat ((rewrite nmulz || rewrite nplusz || rewrite nsubz); auto). - simpl; split; auto. - repeat ((rewrite nmulz || rewrite nplusz || rewrite nsubz || - rewrite c2ww || rewrite c3ww || rewrite Aww); try nw; auto). - Qed. - -Lemma nopp_wf: forall x, wfe x -> wfe (nopp x). -Proof. -intros x; case x; simpl nopp; auto. -intros x1 y1 z1 [H1 [H2 H3]]; repeat split; auto. -Qed. - -Lemma scalb_wf: forall n b x sc, - wfe x -> wft sc -> - wfe (fst (scalb sc b x n)) /\ wft (snd (scalb sc b x n)). -Proof. -intros n; elim n; unfold scalb; fold scalb; auto. - intros n1 Hrec b x sc H H1. - case (Hrec true x sc H H1). - case scalb; simpl fst; simpl snd. - intros a1 sc1 H2 H3. - case (ndouble_wf _ H2 H3); auto; - case ndouble; simpl fst; simpl snd; intros x2 sc2 H4 H5. - case b; auto. - case (nadd_wf _ _ (nopp_wf _ H) H4 H5); auto; - case ndouble; simpl fst; simpl snd; intros x2 sc2 H4 H5. - intros n1 Hrec b x sc H H1. - case (Hrec false x sc H H1). - case scalb; simpl fst; simpl snd. - intros a1 sc1 H2 H3. - case (ndouble_wf _ H2 H3); auto; - case ndouble; simpl fst; simpl snd; intros x2 sc2 H4 H5. - case b; auto. - case (nadd_wf _ _ H H4 H5); auto; - case ndouble; simpl fst; simpl snd; intros x2 sc2 H4 H5. -intros b x sc H H1; case b; auto. -case (ndouble_wf _ H H1); auto. -Qed. - - -Lemma scal_wf: forall n x sc, - wfe x -> wft sc -> - wfe (fst (scal sc x n)) /\ wft (snd (scal sc x n)). -Proof. -intros n; exact (scalb_wf n false). -Qed. - -Lemma nopp_correct: forall x, - wfe x -> e2E x = ZEll.nopp exx.(vN) (e2E (nopp x)). -Proof. -intros x; case x; simpl; auto. -intros x1 y1 z1 [H1 [H2 H3]]; apply f_equal3 with (f := ZEll.ntriple); auto. -rewrite nsubz; auto. -rewrite zc0. -unfold ZEll.nsub, ninv; simpl. -apply sym_equal. -rewrite <- (Z_mod_plus) with (b := -(-z2Z y1 /exx.(vN))); auto with zarith. -rewrite <- Zopp_mult_distr_l. -rewrite <- Zopp_plus_distr. -rewrite Zmult_comm; rewrite Zplus_comm. -rewrite <- Z_div_mod_eq; auto with zarith. -rewrite Zopp_involutive; rewrite <- z2ZN. -apply sym_equal; auto. -Qed. - -Lemma scalb_correct: forall n b x sc, - wfe x -> wft sc -> - e2E (fst (scalb sc b x n)) = fst (ZEll.scalb exx.(vN) exx.(vA) (z2Z sc) b (e2E x) n)/\ - z2Z (snd (scalb sc b x n)) = snd (ZEll.scalb exx.(vN) exx.(vA) (z2Z sc) b (e2E x) n). -Proof. -intros n; elim n; clear; auto. -intros p Hrec b x sc H1 H2. - case b; unfold scalb; fold scalb. - generalize (scalb_wf p true x H1 H2); - generalize (Hrec true _ _ H1 H2); case scalb; simpl. - case ZEll.scalb; intros r1 rc1; simpl. - intros a2 sc2 (H3, H4) (H5, H6); subst r1 rc1. - apply ndouble_correct; auto. - generalize (scalb_wf p true x H1 H2); - generalize (Hrec true _ _ H1 H2); case scalb; simpl. - case ZEll.scalb; intros r1 rc1; simpl. - intros a2 sc2 (H3, H4) (H5, H6); subst r1 rc1. - generalize (ndouble_wf _ H5 H6); - generalize (ndouble_correct _ H5 H6); case ndouble; simpl. - case ZEll.ndouble; intros r1 rc1; simpl. - intros a3 sc3 (H7,H8) (H9,H10); subst r1 rc1. - replace (ZEll.nopp (vN exx) (e2E x)) with - (e2E (nopp x)). - apply nadd_correct; auto. - generalize H1; case x; auto. - intros x1 y1 z1 [HH1 [HH2 HH3]]; split; auto. - rewrite nopp_correct; auto. - apply f_equal2 with (f := ZEll.nopp); auto. - generalize H1; case x; simpl; auto; clear x H1. - intros x1 y1 z1 [HH1 [HH2 HH3]]; - apply f_equal3 with (f := ZEll.ntriple); auto. - repeat rewrite nsubz; auto. - rewrite zc0. - unfold ZEll.nsub; simpl. - rewrite <- (Z_mod_plus) with (b := -(-z2Z y1 /exx.(vN))); auto with zarith. - rewrite <- Zopp_mult_distr_l. - rewrite <- Zopp_plus_distr. - rewrite Zmult_comm; rewrite Zplus_comm. - rewrite <- Z_div_mod_eq; auto with zarith. - rewrite Zopp_involutive; rewrite <- z2ZN. - apply sym_equal; auto. - generalize H1; case x; auto. - intros x1 y1 z1 [HH1 [HH2 HH3]]; split; auto. -intros p Hrec b x sc H1 H2. - case b; unfold scalb; fold scalb. - generalize (scalb_wf p false x H1 H2); - generalize (Hrec false _ _ H1 H2); case scalb; simpl. - case ZEll.scalb; intros r1 rc1; simpl. - intros a2 sc2 (H3, H4) (H5, H6); subst r1 rc1. - generalize (ndouble_wf _ H5 H6); - generalize (ndouble_correct _ H5 H6); case ndouble; simpl. - case ZEll.ndouble; intros r1 rc1; simpl. - intros a3 sc3 (H7,H8) (H9,H10); subst r1 rc1. - replace (ZEll.nopp (vN exx) (e2E x)) with - (e2E (nopp x)). - apply nadd_correct; auto. - rewrite nopp_correct; auto. - apply f_equal2 with (f := ZEll.nopp); auto. - generalize H1; case x; simpl; auto; clear x H1. - intros x1 y1 z1 [HH1 [HH2 HH3]]; - apply f_equal3 with (f := ZEll.ntriple); auto. - repeat rewrite nsubz; auto. - rewrite zc0. - unfold ZEll.nsub; simpl. - rewrite <- (Z_mod_plus) with (b := -(-z2Z y1 /exx.(vN))); auto with zarith. - rewrite <- Zopp_mult_distr_l. - rewrite <- Zopp_plus_distr. - rewrite Zmult_comm; rewrite Zplus_comm. - rewrite <- Z_div_mod_eq; auto with zarith. - rewrite Zopp_involutive; rewrite <- z2ZN. - apply sym_equal; auto. - generalize H1; case x; auto. - intros x1 y1 z1 [HH1 [HH2 HH3]]; split; auto. - generalize (scalb_wf p false x H1 H2); - generalize (Hrec false _ _ H1 H2); case scalb; simpl. - case ZEll.scalb; intros r1 rc1; simpl. - intros a2 sc2 (H3, H4) (H5, H6); subst r1 rc1. - apply ndouble_correct; auto. -intros b x sc H H1. -case b; simpl; auto. -apply ndouble_correct; auto. -Qed. - - -Lemma scal_correct: forall n x sc, - wfe x -> wft sc -> - e2E (fst (scal sc x n)) = fst (ZEll.scal exx.(vN) exx.(vA) (z2Z sc) (e2E x) n)/\ - z2Z (snd (scal sc x n)) = snd (ZEll.scal exx.(vN) exx.(vA) (z2Z sc) (e2E x) n). -Proof. -intros n; exact (scalb_correct n false). -Qed. - -Lemma scal_list_correct: forall l x sc, - wfe x -> wft sc -> - e2E (fst (scal_list sc x l)) = fst (ZEll.scal_list exx.(vN) exx.(vA) (z2Z sc) (e2E x) l)/\ - z2Z (snd (scal_list sc x l)) = snd (ZEll.scal_list exx.(vN) exx.(vA) (z2Z sc) (e2E x) l). -Proof. -intros l1; elim l1; simpl; auto. -unfold scal_list, ZEll.scal_list; simpl; intros a l2 Hrec x sc H1 H2. -generalize (scal_correct a _ H1 H2) (scal_wf a _ H1 H2); case scal. -case ZEll.scal; intros r1 rsc1; simpl. -simpl; intros a1 sc1 (H3, H4) (H5, H6); subst r1 rsc1; auto. -Qed. - -Lemma scal_list_wf: forall l x sc, - wfe x -> wft sc -> - wfe (fst (scal_list sc x l)) /\ wft (snd (scal_list sc x l)). -Proof. -intros l1; elim l1; simpl; auto. -unfold scal_list; intros a l Hrec x sc H1 H2; simpl. -generalize (@scal_wf a _ _ H1 H2); - case (scal sc x a); simpl; intros x1 sc1 [H3 H4]; auto. -Qed. - -Lemma scalL_wf: forall l x sc, - wfe x -> wft sc -> - wfe (fst (scalL sc x l)) /\ wft (snd (scalL sc x l)). -Proof. -intros l1; elim l1; simpl; auto. -intros a l2 Hrec x sc H1 H2. -generalize (scal_wf a _ H1 H2); case scal; simpl. -intros a1 sc1 (H3, H4); auto. -generalize (scal_list_wf l2 _ H1 H4); case scal_list; simpl. -intros a2 sc2; case a2; simpl; auto. -intros x1 y1 z1 ((V1, (V2, V3)), V4); apply Hrec; auto. -Qed. - -Lemma scalL_correct: forall l x sc, - wfe x -> wft sc -> - e2E (fst (scalL sc x l)) = fst (ZEll.scalL exx.(vN) exx.(vA) (z2Z sc) (e2E x) l)/\ - z2Z (snd (scalL sc x l)) = snd (ZEll.scalL exx.(vN) exx.(vA) (z2Z sc) (e2E x) l). -Proof. -intros l1; elim l1; simpl; auto. -intros a l2 Hrec x sc H1 H2. -generalize (scal_wf a _ H1 H2) (scal_correct a _ H1 H2); case scal; simpl. -case ZEll.scal; intros r1 rsc1; simpl. -intros a1 sc1 (H3, H4) (H5, H6); subst r1 rsc1. -generalize (scal_list_wf l2 _ H1 H4) (scal_list_correct l2 _ H1 H4); case scal_list; simpl. -case ZEll.scal_list; intros r1 rsc1; simpl. -intros a2 sc2 (H7, H8) (H9, H10); subst r1 rsc1. -generalize H7; clear H7; case a2; simpl; auto. -rewrite zc0; auto. -intros x1 y1 z1 (V1, (V2, V3)); auto. -generalize (nmulw H8 V3) (nmulz H8 V3); intros V4 V5; rewrite <- V5. -apply Hrec; auto. -Qed. - -Lemma f4 : wft (Z2z 4). -Proof. -red; apply z2Zx1. -Qed. - -Lemma f27 : wft (Z2z 27). -Proof. -red; apply z2Zx1. -Qed. - -Lemma Bw : wft B. -Proof. -red; unfold B; apply z2Zx1. -Qed. - -Hint Resolve f4 f27 Bw. - -Lemma mww: forall x y, ZEll.nmul (vN exx) (x mod (vN exx) ) y = ZEll.nmul (vN exx) x y. -intros x y; unfold ZEll.nmul; rewrite Zmodml; auto. -Qed. - -Lemma wwA: forall x, ZEll.nmul (vN exx) x exx.(vA) = ZEll.nmul (vN exx) x (z2Z A). -intros x; unfold ZEll.nmul. -unfold A; rewrite z2Zx; rewrite Zmodmr; auto. -Qed. - -Lemma wwB: forall x, ZEll.nmul (vN exx) x exx.(vB) = ZEll.nmul (vN exx) x (z2Z B). -intros x; unfold ZEll.nmul. -unfold B; rewrite z2Zx; rewrite Zmodmr; auto. -Qed. - - Lemma scalL_prime: - let a := ntriple (Z2z (exx.(vx))) (Z2z (exx.(vy))) c1 in - let isc := (Z2z 4) ** A ** A ** A ++ (Z2z 27) ** B ** B in - let (a1, sc1) := scal isc a exx.(vS) in - let (S1,R1) := psplit exx.(vR) in - let (a2, sc2) := scal sc1 a1 S1 in - let (a3, sc3) := scalL sc2 a2 R1 in - match a3 with - nzero => if (Zeq_bool (Zgcd (z2Z sc3) exx.(vN)) 1) then prime exx.(vN) - else True - | _ => True - end. - Proof. - intros a isc. - case_eq (scal isc a (vS exx)); intros a1 sc1 Ha1. - case_eq (psplit (vR exx)); intros S1 R1 HS1. - case_eq (scal sc1 a1 S1); intros a2 sc2 Ha2. - case_eq (scalL sc2 a2 R1); intros a3 sc3; case a3; auto. - intros Ha3; case_eq (Zeq_bool (Zgcd (z2Z sc3) (vN exx)) 1); auto. - intros H1. - assert (F0: - (vy exx mod vN exx) ^ 2 mod vN exx = - ((vx exx mod vN exx) ^ 3 + vA exx * (vx exx mod vN exx) + - vB exx) mod vN exx). - generalize exxs.(inC). - simpl; unfold Zpower_pos; simpl. - repeat rewrite Zmult_1_r. - intros HH. - match goal with |- ?t1 = ?t2 => rmod t1; auto end. - rewrite HH. - rewrite Zplus_mod; auto; symmetry; rewrite Zplus_mod; auto; symmetry. - apply f_equal2 with (f := Zmod); auto. - apply f_equal2 with (f := Zplus); auto. - rewrite Zplus_mod; auto; symmetry; rewrite Zplus_mod; auto; symmetry. - apply f_equal2 with (f := Zmod); auto. - apply f_equal2 with (f := Zplus); auto. - rewrite Zmult_mod; auto; symmetry; rewrite Zmult_mod; auto; symmetry. - apply f_equal2 with (f := Zmod); auto. - apply f_equal2 with (f := Zmult); auto. - rewrite Zmod_mod; auto. - match goal with |- ?t1 = ?t2 => rmod t2; auto end. - rewrite Zmult_mod; auto; symmetry; rewrite Zmult_mod; auto; symmetry. - apply f_equal2 with (f := Zmod); auto. - rewrite Zmod_mod; auto. - generalize (@ZEll.scalL_prime exx.(vN) - (exx.(vx) mod exx.(vN)) - (exx.(vy) mod exx.(vN)) - exx.(vA) - exx.(vB) - exxs.(n_pos) exxs.(n2_div) exx.(vR) - exxs.(lprime) exx.(vS) exxs.(lbig) F0); simpl. -generalize (@scal_wf (vS exx) a isc) (@scal_correct (vS exx) a isc). -unfold isc. -rewrite nplusz; auto; try nw; auto. -repeat rewrite nmulz; auto; try nw; auto. - repeat rewrite z2Zx. -repeat rewrite wwA || rewrite wwB|| rewrite mww. -replace (e2E a) with (ZEll.ntriple (vx exx mod vN exx) (vy exx mod vN exx) 1). -case ZEll.scal. -fold isc; rewrite HS1; rewrite Ha1; simpl; auto. -intros r1 rsc1 HH1 HH2. -case HH1; clear HH1. - unfold c1; repeat split; red; try apply z2Zx1. - unfold isc; nw. -case HH2; clear HH2. - unfold c1; repeat split; red; try apply z2Zx1. - unfold isc; nw. -intros U1 U2 W1 W2; subst r1 rsc1. -generalize (@scal_wf S1 a1 sc1) (@scal_correct S1 a1 sc1). -case ZEll.scal. -intros r1 rsc1 HH1 HH2. -case HH1; clear HH1; auto. -case HH2; clear HH2; auto. -rewrite Ha2; simpl. -intros U1 U2 W3 W4; subst r1 rsc1. -generalize (@scalL_wf R1 a2 sc2) (@scalL_correct R1 a2 sc2). -case ZEll.scalL. -intros n; case n; auto. -rewrite Ha3; simpl. -intros rsc1 HH1 HH2. -case HH1; clear HH1; auto. -case HH2; clear HH2; auto. -intros _ U2 _ W5; subst rsc1. -rewrite H1; auto. -intros x1 y1 z1 sc4; rewrite Ha3; simpl; auto. -intros _ HH; case HH; auto. -intros; discriminate. -unfold a; simpl. -unfold c1; repeat rewrite z2Zx. -rewrite (Zmod_small 1); auto. -generalize exxs.(n_pos). -auto with zarith. -Qed. -*) - -End NEll. - -Definition isM2 p := - match p with - xH => false -| xO _ => false -| _ => true -end. - -Lemma isM2_correct: forall p, - if isM2 p then ~(Zdivide 2 p) /\ 2 < p else True. -Proof. -intros p; case p; simpl; auto; clear p. -intros p1; split; auto. -intros HH; inversion_clear HH. -generalize H; rewrite Zmult_comm. -case x; simpl; intros; discriminate. -case p1; red; simpl; auto. -Qed. - -Definition ell_test (N S: positive) (l: List.list (positive * positive)) - (A B x y: Z) := - if isM2 N then - match (4 * N) ?= (ZEll.Zmullp l - 1) ^ 2 with - Lt => - match y ^ 2 mod N ?= (x ^ 3 + A * x + B) mod N with - Eq => - let ex := mkEx N S l A B x y in - let e2n := e ex in - let a := mtriple (e2n x) (e2n y) (e2n 1) in - let A := (e2n A) in - let B := (e2n B) in - let d4 := (e2n 4) in - let d27 := (e2n 27) in - let dN := nN ex in - let n := nn ex in - let n' := nn' ex in - let da := mplus ex in - let dm := mmult ex in - let isc := (da (dm (dm (dm d4 A) A) A) (dm (dm d27 B) B)) in - let (a1, sc1) := scal ex isc a S in - let (S1,R1) := ZEll.psplit l in - let (a2, sc2) := scal ex sc1 a1 S1 in - let (a3, sc3) := scalL ex sc2 a2 R1 in - match a3 with - mzero => if (Zeq_bool (Zgcd (d ex sc3) N) 1) then true - else false - | _ => false - end - | _ => false - end - | _ => false - end - else false. - -(* -Lemma Zcompare_correct: forall x y, - match x ?= y with Eq => x = y | Gt => x > y | Lt => x < y end. -Proof. -intros x y; unfold Zlt, Zgt; generalize (Zcompare_Eq_eq x y); case Zcompare; auto. -Qed. - -Lemma ell_test_correct: forall (N S: positive) (l: List.list (positive * positive)) - (A B x y: Z), - (forall p, List.In p l -> prime (fst p)) -> - if ell_test N S l A B x y then prime N else True. -intros N S1 l A1 B1 x y H; unfold ell_test. -generalize (isM2_correct N); case isM2; auto. -intros (H1, H2). -match goal with |- context[?x ?= ?y] => - generalize (Zcompare_correct x y); case Zcompare; auto -end; intros H3. -match goal with |- context[?x ?= ?y] => - generalize (Zcompare_correct x y); case Zcompare; auto -end; intros H4. -set (n := Peano.pred (nat_of_P (get_height 31 (plength N)))). -set (op := cmk_op n). -set (mop := make_mod_op op (ZnZ.of_Z N)). -set (exx := mkEx N S1 l A1 B1 x y). -set (op_spec := cmk_spec n). -assert (exxs: ex_spec exx). - constructor; auto. -assert (H0: N < base (ZnZ.digits op)). - apply Zlt_le_trans with (1 := plength_correct N). - unfold op, base. - rewrite cmk_op_digits. - apply Zpower_le_monotone; split; auto with zarith. - generalize (get_height_correct 31 (plength N)); unfold n. - set (p := plength N). - replace (Z_of_nat (Peano.pred (nat_of_P (get_height 31 p)))) with - ((Zpos (get_height 31 p) - 1) ); auto with zarith. - rewrite pred_of_minus; rewrite inj_minus1; auto with zarith. - rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto with zarith. - generalize (lt_O_nat_of_P (get_height 31 p)); auto with zarith. -assert (mspec: mod_spec op (zN exx op) mop). - unfold mop; apply make_mod_spec; auto. - rewrite ZnZ.of_Z_correct; auto with zarith. -generalize (@scalL_prime exx exxs _ op (cmk_spec n) mop mspec H0). -lazy zeta. -unfold c1, A, B, nplus, nmul; - simpl exx.(vA); simpl exx.(vB); simpl exx.(vx); simpl exx.(vy); - simpl exx.(vS); simpl exx.(vR); simpl exx.(vN). -case scal; intros a1 sc1. -case ZEll.psplit; intros S2 R2. -case scal; intros a2 sc2. -case scalL; intros a3 sc3. -case a3; auto. -case Zeq_bool; auto. -Qed. -*) - -Time Eval vm_compute in (ell_test - 329719147332060395689499 - 8209062 - (List.cons (40165264598163841%positive,1%positive) List.nil) - (-94080) - 9834496 - 0 - 3136). - - -Time Eval vm_compute in (ell_test - 1384435372850622112932804334308326689651568940268408537 - 13077052794 - (List.cons (105867537178241517538435987563198410444088809%positive, 1%positive) List.nil) - (-677530058123796416781392907869501000001421915645008494) - 0 - (- 169382514530949104195348226967375250000355478911252124) - 1045670343788723904542107880373576189650857982445904291 -). -*)
\ No newline at end of file diff --git a/coqprime/num/Mod_op.v b/coqprime/num/Mod_op.v deleted file mode 100644 index a8f25bd2d..000000000 --- a/coqprime/num/Mod_op.v +++ /dev/null @@ -1,1200 +0,0 @@ - -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) - -Set Implicit Arguments. - -Require Import DoubleBase DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv. -Require Import CyclicAxioms DoubleCyclic BigN Cyclic31. -Require Import ZArith ZCAux. -Import CyclicAxioms DoubleType DoubleBase. - -Theorem Zpos_pos: forall x, 0 < Zpos x. -red; simpl; auto. -Qed. -Hint Resolve Zpos_pos: zarith. - -Section Mod_op. - - Variable w : Type. - - Record mod_op : Type := mk_mod_op { - succ_mod : w -> w; - add_mod : w -> w -> w; - pred_mod : w -> w; - sub_mod : w -> w -> w; - mul_mod : w -> w -> w; - square_mod : w -> w; - power_mod : w -> positive -> w - }. - - Variable w_op : ZnZ.Ops w. - - Let w_digits := w_op.(ZnZ.digits). - Let w_zdigits := w_op.(ZnZ.zdigits). - Let w_to_Z := (@ZnZ.to_Z _ w_op). - Let w_of_pos := (@ZnZ.of_pos _ w_op). - Let w_head0 := (@ZnZ.head0 _ w_op). - Let w0 := (@ZnZ.zero _ w_op). - Let w1 := (@ZnZ.one _ w_op). - Let wBm1 := (@ZnZ.minus_one _ w_op). - - Let wWW := (@ZnZ.WW _ w_op). - Let wW0 := (@ZnZ.WO _ w_op). - Let w0W := (@ZnZ.OW _ w_op). - - Let w_compare := (@ZnZ.compare _ w_op). - Let w_opp_c := (@ZnZ.opp_c _ w_op). - Let w_opp := (@ZnZ.opp _ w_op). - Let w_opp_carry := (@ZnZ.opp_carry _ w_op). - - Let w_succ := (@ZnZ.succ _ w_op). - Let w_succ_c := (@ZnZ.succ_c _ w_op). - Let w_add_c := (@ZnZ.add_c _ w_op). - Let w_add_carry_c := (@ZnZ.add_carry_c _ w_op). - Let w_add := (@ZnZ.add _ w_op). - - - Let w_pred_c := (@ZnZ.pred_c _ w_op). - Let w_sub_c := (@ZnZ.sub_c _ w_op). - Let w_sub_carry := (@ZnZ.sub_carry _ w_op). - Let w_sub_carry_c := (@ZnZ.sub_carry_c _ w_op). - Let w_sub := (@ZnZ.sub _ w_op). - Let w_pred := (@ZnZ.pred _ w_op). - - Let w_mul_c := (@ZnZ.mul_c _ w_op). - Let w_mul := (@ZnZ.mul _ w_op). - Let w_square_c := (@ZnZ.square_c _ w_op). - - Let w_div21 := (@ZnZ.div21 _ w_op). - Let w_add_mul_div := (@ZnZ.add_mul_div _ w_op). - - Variable b : w. - (* b should be > 1 *) - Let n := w_head0 b. - - Let b2n := w_add_mul_div n b w0. - - Let bm1 := w_sub b w1. - - Let mb := w_opp b. - - Let wwb := WW w0 b. - - Let low x := match x with WW _ x => x | W0 => w0 end. - - Let w_add2 x y := match w_add_c x y with - C0 n => WW w0 n - |C1 n => WW w1 n - end. - Let ww_zdigits := w_add2 w_zdigits w_zdigits. - - Let ww_compare := - Eval lazy beta delta [ww_compare] in ww_compare w0 w_compare. - - Let ww_sub := - Eval lazy beta delta [ww_sub] in - ww_sub w0 wWW w_opp_c w_opp_carry w_sub_c w_opp w_sub w_sub_carry. - - Let ww_add_mul_div := - Eval lazy beta delta [ww_add_mul_div] in - ww_add_mul_div w0 wWW wW0 w0W - ww_compare w_add_mul_div - ww_sub w_zdigits low (w0W n). - - Let ww_lsl_n := - Eval lazy beta delta [ww_add_mul_div] in - fun ww => ww_add_mul_div ww W0. - - Let w_lsr_n w := - w_add_mul_div (w_sub w_zdigits n) w0 w. - - Open Scope Z_scope. - Notation "[| x |]" := - (@ZnZ.to_Z _ w_op x) (at level 0, x at level 99). - -Notation "[[ x ]]" := - (@ww_to_Z _ w_digits w_to_Z x) (at level 0, x at level 99). - - Section Mod_spec. - - Variable m_op : mod_op. - - Record mod_spec : Prop := mk_mod_spec { - succ_mod_spec : - forall w t, [|w|]= t mod [|b|] -> - [|succ_mod m_op w|] = ([|w|] + 1) mod [|b|]; - add_mod_spec : - forall w1 w2 t1 t2, [|w1|]= t1 mod [|b|] -> [|w2|]= t2 mod [|b|] -> - [|add_mod m_op w1 w2|] = ([|w1|] + [|w2|]) mod [|b|]; - pred_mod_spec : - forall w t, [|w|]= t mod [|b|] -> - [|pred_mod m_op w|] = ([|w|] - 1) mod [|b|]; - sub_mod_spec : - forall w1 w2 t1 t2, [|w1|]= t1 mod [|b|] -> [|w2|]= t2 mod [|b|] -> - [|sub_mod m_op w1 w2|] = ([|w1|] - [|w2|]) mod [|b|]; - mul_mod_spec : - forall w1 w2 t1 t2, [|w1|]= t1 mod [|b|] -> [|w2|]= t2 mod [|b|] -> - [|mul_mod m_op w1 w2|] = ([|w1|] * [|w2|]) mod [|b|]; - square_mod_spec : - forall w t, [|w|]= t mod [|b|] -> - [|square_mod m_op w|] = ([|w|] * [|w|]) mod [|b|]; - power_mod_spec : - forall w t p, [|w|]= t mod [|b|] -> - [|power_mod m_op w p|] = (Zpower_pos [|w|] p) mod [|b|] -(* - shift_spec : - forall w p, wf w -> - [|shift m_op w p|] = ([|w|] / (Zpower_pos 2 p)) mod [|b|]; - trunc_spec : - forall w p, wf w -> - [|power_mod m_op w p|] = ([|w1|] mod (Zpower_pos 2 p)) mod [|b|] -*) - }. - - End Mod_spec. - - Hypothesis b_pos: 1 < [|b|]. - Variable op_spec: ZnZ.Specs w_op. - - - Lemma Zpower_n: 0 < 2 ^ [|n|]. - apply Zpower_gt_0; auto with zarith. - case (ZnZ.spec_to_Z n); auto with zarith. - Qed. - - Hint Resolve Zpower_n Zmult_lt_0_compat Zpower_gt_0. - - Variable m_op : mod_op. - - Hint Rewrite - ZnZ.spec_0 - ZnZ.spec_1 - ZnZ.spec_m1 - ZnZ.spec_WW - ZnZ.spec_opp_c - ZnZ.spec_opp - ZnZ.spec_opp_carry - ZnZ.spec_succ_c - ZnZ.spec_add_c - ZnZ.spec_add_carry_c - ZnZ.spec_add - ZnZ.spec_pred_c - ZnZ.spec_sub_c - ZnZ.spec_sub_carry_c - ZnZ.spec_sub - ZnZ.spec_mul_c - ZnZ.spec_mul - : w_rewrite. - - Let _succ_mod x := - let res :=w_succ x in - match w_compare res b with - | Lt => res - | _ => w0 - end. - - Let split x := - match x with - | W0 => (w0,w0) - | WW h l => (h,l) - end. - - Let _w0_is_0: [|w0|] = 0. - unfold ZnZ.to_Z; rewrite <- ZnZ.spec_0; auto. - Qed. - - Let _w1_is_1: [|w1|] = 1. - unfold ZnZ.to_Z; rewrite <-ZnZ.spec_1; simpl; auto. - Qed. - - Theorem Zmod_plus_one: forall a1 b1, 0 < b1 -> (a1 + b1) mod b1 = a1 mod b1. - intros a1 b1 H; rewrite Zplus_mod; auto with zarith. - rewrite Z_mod_same; try rewrite Zplus_0_r; auto with zarith. - apply Zmod_mod; auto. - Qed. - - Theorem Zmod_minus_one: forall a1 b1, 0 < b1 -> (a1 - b1) mod b1 = a1 mod b1. - intros a1 b1 H; rewrite Zminus_mod; auto with zarith. - rewrite Z_mod_same; try rewrite Zminus_0_r; auto with zarith. - apply Zmod_mod; auto. - Qed. - - Lemma without_c_b: forall w2, [|w2|] < [|b|] -> - [|w_succ w2|] = [|w2|] + 1. - intros w2 H. - unfold w_succ;rewrite ZnZ.spec_succ. - rewrite Zmod_small;auto. - assert (HH := ZnZ.spec_to_Z w2). - assert (HH' := ZnZ.spec_to_Z b);auto with zarith. - Qed. - - Lemma _succ_mod_spec: forall w t, [|w|]= t mod [|b|] -> - [|_succ_mod w|] = ([|w|] + 1) mod [|b|]. - intros w2 t H; unfold _succ_mod, w_compare; simpl. - assert (F: [|w2|] < [|b|]). - case (Z_mod_lt t [|b|]); auto with zarith. - rewrite ZnZ.spec_compare; case Zcompare_spec; intros H1; - match goal with H: context[w_succ _] |- _ => - generalize H; clear H; rewrite (without_c_b _ F); intros H1; - auto with zarith - end. - rewrite H1, Z_mod_same, _w0_is_0; auto with zarith. - rewrite Zmod_small; auto with zarith. - case (ZnZ.spec_to_Z w2); auto with zarith. - Qed. - - Let _add_mod x y := - match w_add_c x y with - | C0 z => - match w_compare z b with - | Lt => z - | Eq => w0 - | Gt => w_sub z b - end - | C1 z => w_add mb z - end. - - Lemma _add_mod_correct: forall w1 w2, [|w1|] + [|w2|] < 2 * [|b|] -> - [|_add_mod w1 w2|] = ([|w1|] + [|w2|]) mod [|b|]. - intros w2 w3; unfold _add_mod, w_compare, w_add_c; intros H. - match goal with |- context[ZnZ.add_c ?x ?y] => - generalize (ZnZ.spec_add_c x y); unfold interp_carry; - case (ZnZ.add_c x y); autorewrite with w_rewrite - end; auto with zarith. - intros w4 H2. - rewrite ZnZ.spec_compare; case Zcompare_spec; intros H1; - match goal with H: context[b] |- _ => - generalize H; clear H; intros H1; rewrite <-H2; - auto with zarith - end. - rewrite H1, Z_mod_same; auto with zarith. - rewrite Zmod_small; auto with zarith. - case (ZnZ.spec_to_Z w4); auto with zarith. - assert (F1: 0 < [|w4|] - [|b|]); auto with zarith. - assert (F2: [|w4|] < [|b|] + [|b|]); auto with zarith. - autorewrite with w_rewrite; auto. - rewrite (fun x y => Zmod_small (x - y)); auto with zarith. - rewrite <- (Zmod_minus_one [|w4|]); auto with zarith. - apply sym_equal; apply Zmod_small; auto with zarith. - split; auto with zarith. - apply Zlt_trans with [|b|]; auto with zarith. - case (ZnZ.spec_to_Z b); unfold base; auto with zarith. - rewrite Zmult_1_l; intros w4 H2; rewrite <- H2. - unfold mb, w_add; rewrite ZnZ.spec_add; auto with zarith. - assert (F1: [|w4|] < [|b|]). - assert (F2: base (ZnZ.digits w_op) + [|w4|] < base (ZnZ.digits w_op) + [|b|]); - auto with zarith. - rewrite H2. - apply Zlt_trans with ([|b|] +[|b|]); auto with zarith. - apply Zplus_lt_compat_r; auto with zarith. - case (ZnZ.spec_to_Z b); auto with zarith. - assert (F2: [|b|] < base (ZnZ.digits w_op) + [|w4|]); auto with zarith. - apply Zlt_le_trans with (base (ZnZ.digits w_op)); auto with zarith. - case (ZnZ.spec_to_Z b); auto with zarith. - case (ZnZ.spec_to_Z w4); auto with zarith. - assert (F3: base (ZnZ.digits w_op) + [|w4|] < [|b|] + [|b|]); auto with zarith. - rewrite <- (fun x => Zmod_minus_one (base x + [|w4|])); auto with zarith. - rewrite (fun x y => Zmod_small (x - y)); auto with zarith. - unfold w_opp;rewrite (ZnZ.spec_opp b). - rewrite <- (fun x => Zmod_plus_one (-x)); auto with zarith. - rewrite (Zmod_small (- [|b|] + base (ZnZ.digits w_op)));auto with zarith. - 2 : assert (HHH := ZnZ.spec_to_Z b);auto with zarith. - repeat rewrite Zmod_small; auto with zarith. - Qed. - - Lemma _add_mod_spec: forall w1 w2 t1 t2, [|w1|] = t1 mod [|b|] -> [|w2|] = t2 mod [|b|] -> - [|_add_mod w1 w2|] = ([|w1|] + [|w2|]) mod [|b|]. - intros w2 w3 t1 t2 H H1. - apply _add_mod_correct; auto with zarith. - assert (F: [|w2|] < [|b|]). - case (Z_mod_lt t1 [|b|]); auto with zarith. - assert (F': [|w3|] < [|b|]). - case (Z_mod_lt t2 [|b|]); auto with zarith. - assert (tmp: forall x, 2 * x = x + x); auto with zarith. - Qed. - - Let _pred_mod x := - match w_compare w0 x with - | Eq => bm1 - | _ => w_pred x - end. - - Lemma _pred_mod_spec: forall w t, [|w|] = t mod [|b|] -> - [|_pred_mod w|] = ([|w|] - 1) mod [|b|]. - intros w2 t H; unfold _pred_mod, w_compare, bm1; simpl. - assert (F: [|w2|] < [|b|]). - case (Z_mod_lt t [|b|]); auto with zarith. - rewrite ZnZ.spec_compare; case Zcompare_spec; intros H1; - match goal with H: context[w2] |- _ => - generalize H; clear H; intros H1; autorewrite with w_rewrite; - auto with zarith - end; try rewrite _w0_is_0; try rewrite _w1_is_1; auto with zarith. - rewrite <- H1, _w0_is_0; simpl. - rewrite <- (Zmod_plus_one (-1)); auto with zarith. - repeat rewrite Zmod_small; auto with zarith. - case (ZnZ.spec_to_Z b); auto with zarith. - unfold w_pred;rewrite ZnZ.spec_pred; auto. - assert (HHH := ZnZ.spec_to_Z b);repeat rewrite Zmod_small;auto with - zarith. - intros;assert (HHH := ZnZ.spec_to_Z w2);auto with zarith. - Qed. - - Let _sub_mod x y := - match w_sub_c x y with - | C0 z => z - | C1 z => w_add z b - end. - - Lemma _sub_mod_spec: forall w1 w2 t1 t2, [|w1|] = t1 mod [|b|] -> [|w2|] = t2 mod [|b|] -> - [|_sub_mod w1 w2|] = ([|w1|] - [|w2|]) mod [|b|]. - intros w2 w3 t1 t2; unfold _sub_mod, w_compare, w_sub_c; intros H H1. - assert (F: [|w2|] < [|b|]). - case (Z_mod_lt t1 [|b|]); auto with zarith. - assert (F': [|w3|] < [|b|]). - case (Z_mod_lt t2 [|b|]); auto with zarith. - match goal with |- context[ZnZ.sub_c ?x ?y] => - generalize (ZnZ.spec_sub_c x y); unfold interp_carry; - case (ZnZ.sub_c x y); autorewrite with w_rewrite - end; auto with zarith. - intros w4 H2. - rewrite Zmod_small; auto with zarith. - split; auto with zarith. - rewrite <- H2; case (ZnZ.spec_to_Z w4); auto with zarith. - apply Zle_lt_trans with [|w2|]; auto with zarith. - case (ZnZ.spec_to_Z w3); auto with zarith. - intros w4 H2; rewrite <- H2. - unfold w_add; rewrite ZnZ.spec_add; auto with zarith. - case (ZnZ.spec_to_Z w4); intros F1 F2. - assert (F3: 0 <= - 1 * base (ZnZ.digits w_op) + [|w4|] + [|b|]); auto with zarith. - rewrite H2. - case (ZnZ.spec_to_Z w3); case (ZnZ.spec_to_Z w2); auto with zarith. - rewrite <- (fun x => Zmod_minus_one ([|w4|] + x)); auto with zarith. - rewrite <- (fun x y => Zmod_plus_one (-y + x)); auto with zarith. - repeat rewrite Zmod_small; auto with zarith. - case (ZnZ.spec_to_Z b); auto with zarith. - Qed. - - Let _mul_mod x y := - let xy := w_mul_c x y in - match ww_compare xy wwb with - | Lt => snd (split xy) - | Eq => w0 - | Gt => - let xy2n := ww_lsl_n xy in - let (h,l) := split xy2n in - let (q,r) := w_div21 h l b2n in - w_lsr_n r - end. - - Theorem high_zero:forall x, [[x]] < base w_digits -> [|fst (split x)|] = 0. - intros x; case x; simpl; auto. - intros xh xl H; case (Zle_lt_or_eq 0 [|xh|]); auto with zarith. - case (ZnZ.spec_to_Z xh); auto with zarith. - intros H1; contradict H; apply Zle_not_lt. - assert (HHHH := wB_pos w_digits). - unfold w_to_Z. - match goal with |- ?X <= ?Y + ?Z => - pattern X at 1; rewrite <- (Zmult_1_l X); auto with zarith; - apply Zle_trans with Y; auto with zarith - end. - case (ZnZ.spec_to_Z xl); auto with zarith. - Qed. - - Theorem n_spec: base (ZnZ.digits w_op) / 2 <= 2 ^ [|n|] * [|b|] - < base (ZnZ.digits w_op). - unfold n, w_head0; apply (ZnZ.spec_head0); auto with zarith. - Qed. - - Theorem b2n_spec: [|b2n|] = 2 ^ [|n|] * [|b|]. - unfold b2n, w_add_mul_div; case n_spec; intros Hp Hp1. - assert (F1: [|n|] < Zpos (ZnZ.digits w_op)). - case (Zle_or_lt (Zpos (ZnZ.digits w_op)) [|n|]); auto with zarith. - intros H1; contradict Hp1; apply Zle_not_lt; unfold base. - apply Zle_trans with (2 ^ [|n|] * 1); auto with zarith. - rewrite Zmult_1_r; apply Zpower_le_monotone; auto with zarith. - rewrite ZnZ.spec_add_mul_div; auto with zarith. - rewrite _w0_is_0; rewrite Zdiv_0_l; auto with zarith. - rewrite Zplus_0_r; rewrite Zmult_comm; apply Zmod_small; auto with zarith. - Qed. - - Theorem ww_lsl_n_spec: forall w, [[w]] < [|b|] * [|b|] -> - [[ww_lsl_n w]] = 2 ^ [|n|] * [[w]]. - intros w2 H; unfold ww_lsl_n. - case n_spec; intros Hp Hp1. - assert (F0: forall x, 2 * x = x + x); auto with zarith. - assert (F1: [|n|] < Zpos (ZnZ.digits w_op)). - case (Zle_or_lt (Zpos (ZnZ.digits w_op)) [|n|]); auto. - intros H1; contradict Hp1; apply Zle_not_lt; unfold base. - apply Zle_trans with (2 ^ [|n|] * 1); auto with zarith. - rewrite Zmult_1_r; apply Zpower_le_monotone; auto with zarith. - assert (F2: [|n|] < Zpos (xO (ZnZ.digits w_op))). - rewrite (Zpos_xO (ZnZ.digits w_op)); rewrite F0; auto with zarith. - pattern [|n|]; rewrite <- Zplus_0_r; auto with zarith. - apply Zplus_lt_compat; auto with zarith. - change - ([[DoubleLift.ww_add_mul_div w0 wWW wW0 w0W - ww_compare w_add_mul_div - ww_sub w_zdigits low (w0W n) w2 W0]] = 2 ^ [|n|] * [[w2]]). - rewrite (DoubleLift.spec_ww_add_mul_div ); auto with zarith. - 2: apply ZnZ.spec_to_Z; auto. - 2: refine (spec_ww_to_Z _ _ _); auto. - 2: apply ZnZ.spec_to_Z; auto. - 2: apply ZnZ.spec_WW; auto. - 2: apply ZnZ.spec_WO; auto. - 2: apply ZnZ.spec_OW; auto. - 2: refine (spec_ww_compare _ _ _ _ _ _ _); auto. - 2: apply ZnZ.spec_to_Z; auto. - 2: apply ZnZ.spec_compare; auto. - 2: apply ZnZ.spec_add_mul_div; auto. - 2: refine (spec_ww_sub _ _ _ _ _ _ _ _ _ _ - _ _ _ _ _ _ _ _ _ _ _); auto. - 2: apply ZnZ.spec_to_Z; auto. - 2: apply ZnZ.spec_WW; auto. - 2: apply ZnZ.spec_opp_c; auto. - 2: apply ZnZ.spec_opp; auto. - 2: apply ZnZ.spec_opp_carry; auto. - 2: apply ZnZ.spec_sub_c; auto. - 2: apply ZnZ.spec_sub; auto. - 2: apply ZnZ.spec_sub_carry; auto. - 2: apply ZnZ.spec_zdigits; auto. - replace ([[w0W n]]) with [|n|]. - change [[W0]] with 0. rewrite Zdiv_0_l; auto with zarith. - rewrite Zplus_0_r; rewrite Zmod_small; auto with zarith. - split; auto with zarith. - case spec_ww_to_Z with (w_digits := w_digits) (w_to_Z := w_to_Z) (x:=w2); auto with zarith. - apply ZnZ.spec_to_Z; auto. - apply Zlt_trans with ([|b|] * [|b|] * 2 ^ [|n|]); auto with zarith. - apply Zmult_lt_compat_r; auto with zarith. - rewrite <- Zmult_assoc. - unfold base; unfold base in Hp. - unfold ww_digits,w_digits;rewrite (Zpos_xO (ZnZ.digits w_op)); rewrite F0; auto with zarith. - rewrite Zpower_exp; auto with zarith. - apply Zmult_lt_compat; auto with zarith. - case (ZnZ.spec_to_Z b); auto with zarith. - split; auto with zarith. - rewrite Zmult_comm; auto with zarith. - unfold w_digits;auto with zarith. - generalize (ZnZ.spec_OW n). - unfold ww_to_Z, w_digits; auto. - intros x; case x; simpl. - unfold w_to_Z, w_digits, w0; rewrite ZnZ.spec_0; auto. - intros w3 w4; rewrite Zplus_comm. - rewrite Z_mod_plus; auto with zarith. - rewrite Zmod_small; auto with zarith. - case (ZnZ.spec_to_Z w4); auto with zarith. - unfold base; auto with zarith. - unfold ww_to_Z, w_digits, w_to_Z, w0W; auto. - rewrite ZnZ.spec_OW; auto with zarith. - Qed. - - Theorem w_lsr_n_spec: forall w, [|w|] < 2 ^ [|n|] * [|b|]-> - [|w_lsr_n w|] = [|w|] / 2 ^ [|n|]. - intros w2 H. - case (ZnZ.spec_to_Z w2); intros U1 U2. - unfold w_lsr_n, w_add_mul_div. - rewrite ZnZ.spec_add_mul_div; auto with zarith. - rewrite _w0_is_0; rewrite Zmult_0_l; auto with zarith. - rewrite Zplus_0_l. - autorewrite with w_rewrite; auto. - rewrite (fun x y => Zmod_small (x - y)); auto with zarith. - unfold w_zdigits; rewrite ZnZ.spec_zdigits; auto. - assert (tmp: forall p q, p - (p - q) = q); intros; try ring; - rewrite tmp; clear tmp; auto. - rewrite Zmod_small; auto with zarith. - split; auto with zarith. - apply Zle_lt_trans with (2 := U2); auto with zarith. - apply Zdiv_le_upper_bound; auto with zarith. - apply Zle_trans with ([|w2|] * (2 ^ 0)); auto with zarith. - simpl Zpower; rewrite Zmult_1_r; auto with zarith. - apply Zmult_le_compat_l; auto with zarith. - apply Zpower_le_monotone; auto with zarith. - case (ZnZ.spec_to_Z n); auto with zarith. - unfold n. - assert (HH: 0 < [|b|]); auto with zarith. - split. - case (Zle_or_lt [|w_head0 b|] [|w_zdigits|]); auto with zarith. - unfold w_zdigits; rewrite ZnZ.spec_zdigits; auto; intros H1. - case (ZnZ.spec_head0 b HH); intros _ H2; contradict H2. - apply Zle_not_lt; unfold base. - apply Zle_trans with (2^[|ZnZ.head0 b|] * 1); auto with zarith. - rewrite Zmult_1_r; apply Zpower_le_monotone; auto with zarith. - unfold w_zdigits; rewrite ZnZ.spec_zdigits; auto. - apply Zle_lt_trans with (Zpos (ZnZ.digits w_op)); auto with zarith. - case (ZnZ.spec_to_Z (w_head0 b)); auto with zarith. - unfold base; apply Zpower2_lt_lin; auto with zarith. - autorewrite with w_rewrite; auto. - rewrite Zmod_small; auto with zarith. - unfold w_zdigits; rewrite ZnZ.spec_zdigits; auto with zarith. - case (ZnZ.spec_to_Z n); auto with zarith. - unfold w_zdigits; rewrite ZnZ.spec_zdigits; auto. - split; auto with zarith. - case (Zle_or_lt [|n|] (Zpos (ZnZ.digits w_op))); auto with zarith; intros H1. - case (ZnZ.spec_head0 b); auto with zarith; intros _ H2. - contradict H2; apply Zle_not_lt; auto with zarith. - unfold base; apply Zle_trans with (2 ^ [|ZnZ.head0 b|] * 1); - auto with zarith. - rewrite Zmult_1_r; unfold base; apply Zpower_le_monotone; auto with zarith. - apply Zle_lt_trans with (Zpos (ZnZ.digits w_op)); auto with zarith. - case (ZnZ.spec_to_Z n); auto with zarith. - unfold base; apply Zpower2_lt_lin; auto with zarith. - Qed. - - Lemma split_correct: forall x, let (xh, xl) := split x in [[WW xh xl]] = [[x]]. - intros x; case x; simpl; unfold w0, w_to_Z;try rewrite ZnZ.spec_0; auto with zarith. - Qed. - - Lemma _mul_mod_spec: forall w1 w2 t1 t2, [|w1|] = t1 mod [|b|] -> [|w2|] = t2 mod [|b|] -> - [|_mul_mod w1 w2|] = ([|w1|] * [|w2|]) mod [|b|]. - intros w2 w3 t1 t2 H H1; unfold _mul_mod, wwb. - assert (F: [|w2|] < [|b|]). - case (Z_mod_lt t1 [|b|]); auto with zarith. - assert (F': [|w3|] < [|b|]). - case (Z_mod_lt t2 [|b|]); auto with zarith. - match goal with |- context[ww_compare ?x ?y] => - change (ww_compare x y) with (DoubleBase.ww_compare w0 w_compare x y) - end. - rewrite (@spec_ww_compare w w0 w_digits w_to_Z w_compare - ZnZ.spec_0 ZnZ.spec_to_Z ZnZ.spec_compare - (w_mul_c w2 w3) (WW w0 b)); case Zcompare_spec; intros H2; - match goal with H: context[w_mul_c] |- _ => - generalize H; clear H - end; try rewrite _w0_is_0; try rewrite !_w1_is_1; auto with zarith. - unfold w_mul_c, ww_to_Z, w_to_Z, w_digits; rewrite ZnZ.spec_mul_c; auto with zarith. - simpl; rewrite _w0_is_0, Zmult_0_l, Zplus_0_l. - intros H2; rewrite H2; simpl. - rewrite Z_mod_same; auto with zarith. - generalize (high_zero (w_mul_c w2 w3)). - unfold w_mul_c; generalize (ZnZ.spec_mul_c w2 w3); - case (ZnZ.mul_c w2 w3); simpl; auto with zarith. - intros H3 _ _; rewrite <- H3; autorewrite with w_rewrite; auto. -(* rewrite Zmod_small; auto with zarith. *) - intros w4 w5. - change (w_to_Z w0) with [|w0|]; rewrite _w0_is_0. - change (w_to_Z w4) with [|w4|]. - change (w_to_Z w5) with [|w5|]. - simpl. - intros H2 H3 H4. - assert (E1: [|w4|] = 0). - apply H3; auto with zarith. - apply Zlt_trans with (1 := H4). - case (ZnZ.spec_to_Z b); auto with zarith. - generalize H4 H2; rewrite E1; rewrite Zmult_0_l; rewrite Zplus_0_l; - clear H4 H2; intros H4 H2. - rewrite <- H2; rewrite Zmod_small; auto with zarith. - case (ZnZ.spec_to_Z w5); auto with zarith. - intros H2. - match goal with |- context[split ?x] => - generalize (split_correct x); - case (split x); auto with zarith - end. - assert (F1: [[w_mul_c w2 w3]] < [|b|] * [|b|]). - unfold w_to_Z, w_mul_c, ww_to_Z,w_digits; - rewrite ZnZ.spec_mul_c; auto with zarith. - apply Zmult_lt_compat; auto with zarith. - case (ZnZ.spec_to_Z w2); auto with zarith. - case (ZnZ.spec_to_Z w3); auto with zarith. - intros w4 w5; rewrite ww_lsl_n_spec; auto with zarith. - intros H3. - unfold w_div21; match goal with |- context[ZnZ.div21 ?y ?z ?t] => - generalize (ZnZ.spec_div21 y z t); - case (ZnZ.div21 y z t) - end. - rewrite b2n_spec; case (n_spec); auto. - intros H4 H5 w6 w7 H6. - case H6; auto with zarith. - case (Zle_or_lt (2 ^ [|n|] * [|b|]) [|w4|]); auto; intros H7. - match type of H3 with ?X = ?Y => - absurd (Y < X) - end. - apply Zle_not_lt; rewrite H3; auto with zarith. - simpl ww_to_Z. - match goal with |- ?X < ?Y + _ => - apply Zlt_le_trans with Y; auto with zarith - end. - apply Zlt_trans with (2 ^ [|n|] * ([|b|] * [|b|])); - auto with zarith. - apply Zmult_lt_compat_l; auto with zarith. - rewrite Zmult_assoc. - apply Zmult_lt_compat2; auto with zarith. - case (ZnZ.spec_to_Z b); auto with zarith. - case (ZnZ.spec_to_Z w5); unfold w_to_Z;auto with zarith. - clear H6; intros H7 H8. - rewrite w_lsr_n_spec; auto with zarith. - rewrite <- (Z_div_mult ([|w2|] * [|w3|]) (2 ^ [|n|])); - auto with zarith; rewrite Zmult_comm. - rewrite <- ZnZ.spec_mul_c; auto with zarith. - unfold w_mul_c in H3; unfold ww_to_Z in H3;simpl H3. - unfold w_digits,w_to_Z in H3. rewrite <- H3; simpl. - rewrite H7; rewrite (fun x => Zmult_comm (2 ^ x)); - rewrite Zmult_assoc; rewrite BigNumPrelude.Z_div_plus_l; auto with zarith. - rewrite Zplus_mod; auto with zarith. - rewrite Z_mod_mult; auto with zarith. - rewrite Zplus_0_l; auto with zarith. - rewrite Zmod_mod; auto with zarith. - rewrite Zmod_small; auto with zarith. - split; auto with zarith. - apply Zdiv_lt_upper_bound; auto with zarith. - rewrite Zmult_comm; auto with zarith. - Qed. - - Let _square_mod x := - let x2 := w_square_c x in - match ww_compare x2 wwb with - | Lt => snd (split x2) - | Eq => w0 - | Gt => - let x2_2n := ww_lsl_n x2 in - let (h,l) := split x2_2n in - let (q,r) := w_div21 h l b2n in - w_lsr_n r - end. - - Lemma _square_mod_spec: forall w t, [|w|] = t mod [|b|] -> - [|_square_mod w|] = ([|w|] * [|w|]) mod [|b|]. - intros w2 t2 H; unfold _square_mod, wwb. - assert (F: [|w2|] < [|b|]). - case (Z_mod_lt t2 [|b|]); auto with zarith. - match goal with |- context[ww_compare ?x ?y] => - change (ww_compare x y) with (DoubleBase.ww_compare w0 w_compare x y) - end. - rewrite (@spec_ww_compare w w0 w_digits w_to_Z w_compare - ZnZ.spec_0 ZnZ.spec_to_Z ZnZ.spec_compare); case Zcompare_spec; - intros H2; - match goal with H: context[w_square_c] |- _ => - generalize H; clear H - end; autorewrite with w_rewrite; try rewrite _w0_is_0; try rewrite !_w1_is_1; auto with zarith. - unfold w_square_c, ww_to_Z, w_to_Z, w_digits; rewrite ZnZ.spec_square_c; auto with zarith. - intros H2;rewrite H2; simpl. - rewrite _w0_is_0; simpl. - rewrite Z_mod_same; auto with zarith. - generalize (high_zero (w_square_c w2)). - unfold w_square_c; generalize (ZnZ.spec_square_c w2); - case (ZnZ.square_c w2); simpl; auto with zarith. - intros H3 _ _; rewrite <- H3; autorewrite with w_rewrite; auto. - intros w4 w5. - change (w_to_Z w0) with [|w0|]; rewrite _w0_is_0; simpl. - change (w_to_Z w4) with [|w4|]. - change (w_to_Z w5) with [|w5|]. - intros H2 H3 H4. - assert (E1: [|w4|] = 0). - apply H3; auto with zarith. - apply Zlt_trans with (1 := H4). - case (ZnZ.spec_to_Z b); auto with zarith. - generalize H4 H2; rewrite E1; rewrite Zmult_0_l; rewrite Zplus_0_l; - clear H4 H2; intros H4 H2. - rewrite <- H2; rewrite Zmod_small; auto with zarith. - case (ZnZ.spec_to_Z w5); auto with zarith. - intros H2. - match goal with |- context[split ?x] => - generalize (split_correct x); - case (split x); auto with zarith - end. - assert (F1: [[w_square_c w2]] < [|b|] * [|b|]). - unfold w_square_c, ww_to_Z, w_digits, w_to_Z. - rewrite ZnZ.spec_square_c; auto with zarith. - apply Zmult_lt_compat; auto with zarith. - case (ZnZ.spec_to_Z w2); auto with zarith. - case (ZnZ.spec_to_Z w2); auto with zarith. - intros w4 w5; rewrite ww_lsl_n_spec; auto with zarith. - intros H3. - unfold w_div21; match goal with |- context[ZnZ.div21 ?y ?z ?t] => - generalize (ZnZ.spec_div21 y z t); - case (ZnZ.div21 y z t) - end. - rewrite b2n_spec; case (n_spec); auto. - intros H4 H5 w6 w7 H6. - case H6; auto with zarith. - case (Zle_or_lt (2 ^ [|n|] * [|b|]) [|w4|]); auto; intros H7. - match type of H3 with ?X = ?Y => - absurd (Y < X) - end. - apply Zle_not_lt; rewrite H3; auto with zarith. - simpl ww_to_Z. - match goal with |- ?X < ?Y + _ => - apply Zlt_le_trans with Y; auto with zarith - end. - apply Zlt_trans with (2 ^ [|n|] * ([|b|] * [|b|])); - auto with zarith. - apply Zmult_lt_compat_l; auto with zarith. - rewrite Zmult_assoc. - apply Zmult_lt_compat2; auto with zarith. - case (ZnZ.spec_to_Z b); auto with zarith. - unfold w_to_Z,w_digits;case (ZnZ.spec_to_Z w5); auto with zarith. - clear H6; intros H7 H8. - rewrite w_lsr_n_spec; auto with zarith. - rewrite <- (Z_div_mult ([|w2|] * [|w2|]) (2 ^ [|n|])); - auto with zarith; rewrite Zmult_comm. - rewrite <- ZnZ.spec_square_c; auto with zarith. - unfold w_square_c, ww_to_Z in H3; unfold w_digits,w_to_Z in H3. - rewrite <- H3; simpl. - rewrite H7; rewrite (fun x => Zmult_comm (2 ^ x)); - rewrite Zmult_assoc; rewrite BigNumPrelude.Z_div_plus_l; auto with zarith. - rewrite Zplus_mod; auto with zarith. - rewrite Z_mod_mult; auto with zarith. - rewrite Zplus_0_l; auto with zarith. - rewrite Zmod_mod; auto with zarith. - rewrite Zmod_small; auto with zarith. - split; auto with zarith. - apply Zdiv_lt_upper_bound; auto with zarith. - rewrite Zmult_comm; auto with zarith. - Qed. - - Let _power_mod := - fix pow_mod (x:w) (p:positive) {struct p} : w := - match p with - | xH => x - | xO p' => - let pow := pow_mod x p' in - _square_mod pow - | xI p' => - let pow := pow_mod x p' in - _mul_mod (_square_mod pow) x - end. - - Lemma _power_mod_spec: forall w t p, [|w|] = t mod [|b|] -> - [|_power_mod w p|] = (Zpower_pos [|w|] p) mod [|b|]. - intros w2 t p; elim p; simpl; auto with zarith. - intros p' Rec H. - assert (F: [|w2|] < [|b|]). - case (Z_mod_lt t [|b|]); auto with zarith. - replace (xI p') with (p' + p' + 1)%positive. - repeat rewrite Zpower_pos_is_exp; auto with zarith. - pose (t1 := [|_power_mod w2 p'|]). - rewrite _mul_mod_spec with (t1 := t1 * t1) - (t2 := t); auto with zarith. - rewrite _square_mod_spec with (t := Zpower_pos [|w2|] p'); auto with zarith. - rewrite Rec; auto with zarith. - assert (tmp: forall p, Zpower_pos p 1 = p); try (rewrite tmp; clear tmp). - intros p1; unfold Zpower_pos; simpl; ring. - rewrite <- Zmult_mod; auto with zarith. - rewrite Zmult_mod; auto with zarith. - rewrite Zmod_mod; auto with zarith. - rewrite <- Zmult_mod; auto with zarith. - simpl; unfold t1; apply _square_mod_spec with (t := Zpower_pos [|w2|] p'); auto with zarith. - rewrite xI_succ_xO; rewrite <- Pplus_diag. - rewrite Pplus_one_succ_r; auto. - intros p' Rec H. - replace (xO p') with (p' + p')%positive. - repeat rewrite Zpower_pos_is_exp; auto with zarith. - rewrite _square_mod_spec with (t := Zpower_pos [|w2|] p'); auto with zarith. - rewrite Rec; auto with zarith. - rewrite <- Zmult_mod; auto with zarith. - rewrite <- Pplus_diag; auto. - intros H. - assert (tmp: forall p, Zpower_pos p 1 = p); try (rewrite tmp; clear tmp). - intros p1; unfold Zpower_pos; simpl; ring. - rewrite Zmod_small; auto with zarith. - assert (F: [|w2|] < [|b|]). - case (Z_mod_lt t [|b|]); auto with zarith. - case (ZnZ.spec_to_Z w2); auto with zarith. - Qed. - - Definition make_mod_op := - mk_mod_op - _succ_mod _add_mod - _pred_mod _sub_mod - _mul_mod _square_mod _power_mod. - - Definition make_mod_spec: mod_spec make_mod_op. - apply mk_mod_spec. - exact _succ_mod_spec. - exact _add_mod_spec. - exact _pred_mod_spec. - exact _sub_mod_spec. - exact _mul_mod_spec. - exact _square_mod_spec. - exact _power_mod_spec. - Defined. - -(*********** Mersenne special **********) - - Variable p: positive. - Variable zp: w. - - Hypothesis zp_b: [|zp|] = Zpos p. - Hypothesis p_lt_w_digits: Zpos p <= Zpos w_digits. - - Let p1 := Pminus (xO w_digits) p. - - Theorem p_p1: Zpos p + Zpos p1 = Zpos (xO w_digits). - unfold p1. - rewrite Zpos_minus; auto with zarith. - rewrite Zmax_right; auto with zarith. - rewrite Zpos_xO; auto with zarith. - assert (0 < Zpos w_digits); auto with zarith. - Qed. - - Let zp1 := ww_sub ww_zdigits (WW w0 zp). - - Let spec_add2: forall x y, - [[w_add2 x y]] = [|x|] + [|y|]. - unfold w_add2. - intros xh xl; generalize (ZnZ.spec_add_c xh xl). - unfold w_add_c; case ZnZ.add_c; unfold interp_carry; simpl ww_to_Z. - intros w2 Hw2; simpl; unfold w_to_Z; rewrite Hw2. - unfold w0; rewrite ZnZ.spec_0; simpl; auto with zarith. - intros w2; rewrite Zmult_1_l; simpl. - unfold w_to_Z, w1; rewrite ZnZ.spec_1; auto with zarith. - rewrite Zmult_1_l; auto. - Qed. - - Let spec_ww_digits: - [[ww_zdigits]] = Zpos (xO w_digits). - Proof. - unfold w_to_Z, ww_zdigits. - rewrite spec_add2. - unfold w_to_Z, w_zdigits, w_digits. - rewrite ZnZ.spec_zdigits; auto. - rewrite Zpos_xO; auto with zarith. - Qed. - - Let spec_ww_to_Z := (spec_ww_to_Z _ _ ZnZ.spec_to_Z). - Let spec_ww_compare := spec_ww_compare _ _ _ _ ZnZ.spec_0 - ZnZ.spec_to_Z ZnZ.spec_compare. - Let spec_ww_sub := - spec_ww_sub w0 zp wWW zp1 w_opp_c w_opp_carry - w_sub_c w_opp w_sub w_sub_carry w_digits w_to_Z - ZnZ.spec_0 - ZnZ.spec_to_Z - ZnZ.spec_WW - ZnZ.spec_opp_c - ZnZ.spec_opp - ZnZ.spec_opp_carry - ZnZ.spec_sub_c - ZnZ.spec_sub - ZnZ.spec_sub_carry. - - Theorem zp1_b: [[zp1]] = Zpos p1. - change ([[DoubleSub.ww_sub w0 wWW w_opp_c w_opp_carry w_sub_c w_opp w_sub - w_sub_carry ww_zdigits (WW w0 zp)]] = - Zpos p1). - rewrite spec_ww_sub; auto with zarith. - rewrite spec_ww_digits; simpl ww_to_Z. - change (w_to_Z w0) with [|w0|]. - unfold w0; rewrite ZnZ.spec_0; autorewrite with rm10; auto. - change (w_to_Z zp) with [|zp|]. - rewrite zp_b. - rewrite Zmod_small; auto with zarith. - rewrite <- p_p1; auto with zarith. - unfold ww_digits; split; auto with zarith. - rewrite <- p_p1; auto with zarith. - assert (0 < Zpos p1); auto with zarith. - apply Zle_lt_trans with (Zpos (xO w_digits)); auto with zarith. - assert (0 < Zpos p); auto with zarith. - unfold base; apply Zpower2_lt_lin; auto with zarith. - Qed. - - Hypothesis p_b: [|b|] = 2 ^ (Zpos p) - 1. - - - Let w_pos_mod := ZnZ.pos_mod. - - Let add_mul_div := - DoubleLift.ww_add_mul_div w0 wWW wW0 w0W - ww_compare w_add_mul_div - ww_sub w_zdigits low. - - Let _mmul_mod x y := - let xy := w_mul_c x y in - match xy with - W0 => w0 - | WW xh xl => - let xl1 := w_pos_mod zp xl in - match add_mul_div zp1 W0 xy with - W0 => match w_compare xl1 b with - | Lt => xl1 - | Eq => w0 - | Gt => w1 - end - | WW _ xl2 => _add_mod xl1 xl2 - end - end. - - Hint Unfold w_digits. - - Lemma WW_0: forall x y, [[WW x y]] = 0 -> [|x|] = 0 /\ [|y|] =0. - intros x y; simpl; case (ZnZ.spec_to_Z x); intros H1 H2; - case (ZnZ.spec_to_Z y); intros H3 H4 H5. - case Zle_lt_or_eq with (1 := H1); clear H1; intros H1; auto with zarith. - absurd (0 < [|x|] * base (ZnZ.digits w_op) + [|y|]); auto with zarith. - unfold w_to_Z, w_digits in H5;auto with zarith. - match goal with |- _ < ?X + _ => - apply Zlt_le_trans with X; auto with zarith - end. - case Zle_lt_or_eq with (1 := H3); clear H3; intros H3; auto with zarith. - absurd (0 < [|x|] * base (ZnZ.digits w_op) + [|y|]); auto with zarith. - unfold w_to_Z, w_digits in H5;auto with zarith. - rewrite <- H1; rewrite Zmult_0_l; auto with zarith. - Qed. - - Theorem WW0_is_0: [[W0]] = 0. - simpl; auto. - Qed. - Hint Rewrite WW0_is_0: w_rewrite. - - Theorem mmul_aux0: Zpos (xO w_digits) - Zpos p1 = Zpos p. - unfold w_digits. - apply trans_equal with (Zpos p + Zpos p1 - Zpos p1); auto with zarith. - rewrite p_p1; auto with zarith. - Qed. - - Theorem mmul_aux1: 2 ^ Zpos w_digits = - 2 ^ (Zpos w_digits - Zpos p) * 2 ^ Zpos p. - rewrite <- Zpower_exp; auto with zarith. - eq_tac; auto with zarith. - Qed. - - Theorem mmul_aux2:forall x, - x mod (2 ^ Zpos p - 1) = - ((x / 2 ^ Zpos p) + (x mod 2 ^ Zpos p)) mod (2 ^ Zpos p - 1). - intros x; pattern x at 1; rewrite Z_div_mod_eq with (b := 2 ^ Zpos p); auto with zarith. - match goal with |- (?X * ?Y + ?Z) mod (?X - 1) = ?T => - replace (X * Y + Z) with (Y * (X - 1) + (Y + Z)); try ring - end. - rewrite Zplus_mod; auto with zarith. - rewrite Z_mod_mult; auto with zarith. - rewrite Zplus_0_l. - rewrite Zmod_mod; auto with zarith. - Qed. - - Theorem mmul_aux3:forall xh xl, - [[WW xh xl]] mod (2 ^ Zpos p) = [|xl|] mod (2 ^ Zpos p). - intros xh xl; simpl ww_to_Z; unfold base. - rewrite Zplus_mod; auto with zarith. - generalize mmul_aux1; unfold w_digits; intros tmp; rewrite tmp; - clear tmp. - rewrite Zmult_assoc. - rewrite Z_mod_mult; auto with zarith. - rewrite Zplus_0_l; apply Zmod_mod; auto with zarith. - Qed. - - Let spec_low: forall x, - [|low x|] = [[x]] mod base w_digits. - intros x; case x; simpl low; auto with zarith. - intros xh xl; simpl. - rewrite Zplus_comm; rewrite Z_mod_plus; auto with zarith. - rewrite Zmod_small; auto with zarith. - case (ZnZ.spec_to_Z xl); auto with zarith. - unfold base; auto with zarith. - Qed. - - Theorem mmul_aux4:forall x, - [[x]] < [|b|] * 2 ^ Zpos p -> - match add_mul_div zp1 W0 x with - W0 => 0 - | WW _ xl2 => [|xl2|] - end = [[x]] / 2 ^ Zpos p. - intros x Hx. - assert (Hp: [[zp1]] <= Zpos (xO w_digits)); auto with zarith. - rewrite zp1_b; rewrite <- p_p1; auto with zarith. - assert (0 <= Zpos p); auto with zarith. - generalize (@DoubleLift.spec_ww_add_mul_div w w0 wWW wW0 w0W - ww_compare w_add_mul_div ww_sub w_digits w_zdigits low w_to_Z - ZnZ.spec_0 ZnZ.spec_to_Z spec_ww_to_Z - ZnZ.spec_WW ZnZ.spec_WO ZnZ.spec_OW - spec_ww_compare ZnZ.spec_add_mul_div spec_ww_sub - ZnZ.spec_zdigits spec_low W0 x zp1 Hp). - unfold add_mul_div; - case DoubleLift.ww_add_mul_div; autorewrite with w_rewrite; auto. - rewrite Zmult_0_l; rewrite Zplus_0_l. - rewrite zp1_b. - generalize mmul_aux0; unfold w_digits; intros tmp; rewrite tmp. - rewrite Zmod_small; auto with zarith. - split; auto with zarith. - apply Z_div_pos; auto with zarith. - case (spec_ww_to_Z x); auto with zarith. - unfold base. - apply Zdiv_lt_upper_bound; auto with zarith. - rewrite <- Zpower_exp; auto with zarith. - apply Zlt_le_trans with (base (ww_digits (ZnZ.digits w_op))); auto with zarith. - case (spec_ww_to_Z x); auto with zarith. - unfold base; apply Zpower_le_monotone; auto with zarith. - split; auto with zarith. - assert (0 < Zpos p); auto with zarith. - intros w2 w3; rewrite Zmult_0_l; rewrite Zplus_0_l. - rewrite zp1_b. - generalize mmul_aux0; unfold w_digits; intros tmp; rewrite tmp; - clear tmp. - simpl ww_to_Z; rewrite Zmod_small; auto with zarith. - intros H1; - generalize (high_zero (WW w2 w3)); unfold w_digits;intros tmp; - simpl fst in tmp; simpl ww_to_Z in tmp;auto with zarith. - unfold w_to_Z in *. - rewrite tmp in H1; auto with zarith. clear tmp. - simpl ww_to_Z; rewrite H1; apply Zdiv_lt_upper_bound; auto with zarith. - unfold base; rewrite <- Zpower_exp; auto with zarith. - apply Zlt_le_trans with (1 := Hx). - apply Zle_trans with (2 ^ Zpos p * 2 ^ Zpos p). - rewrite p_b; apply Zmult_le_compat_r; auto with zarith. - rewrite <- Zpower_exp; auto with zarith. - apply Zpower_le_monotone; auto with zarith. - split; auto with zarith. - apply Z_div_pos; auto with zarith. - case (spec_ww_to_Z x); auto with zarith. - unfold base. - apply Zdiv_lt_upper_bound; auto with zarith. - rewrite <- Zpower_exp; auto with zarith. - apply Zlt_le_trans with (base (ww_digits (ZnZ.digits w_op))); auto with zarith. - case (spec_ww_to_Z x); auto with zarith. - unfold base; apply Zpower_le_monotone; auto with zarith. - split; auto with zarith. - assert (0 < Zpos p); auto with zarith. - Qed. - - Theorem mmul_aux5:forall xh xl, - [[WW xh xl]] < [|b|] * 2 ^ Zpos p -> - let xl1 := w_pos_mod zp xl in - let r := - match add_mul_div zp1 W0 (WW xh xl) with - W0 => match w_compare xl1 b with - | Lt => xl1 - | Eq => w0 - | Gt => w1 - end - | WW _ xl2 => _add_mod xl1 xl2 - end in - [|r|] = [[WW xh xl]] mod [|b|]. - intros xh xl Hx xl1 r; unfold r; clear r. - generalize (mmul_aux4 _ Hx). - simpl ww_to_Z; rewrite p_b. - rewrite mmul_aux2. - assert (Hp: [[zp1]] <= Zpos (xO w_digits)); auto with zarith. - rewrite zp1_b; rewrite <- p_p1; auto with zarith. - assert (0 <= Zpos p); auto with zarith. - generalize (@DoubleLift.spec_ww_add_mul_div w w0 wWW wW0 w0W - ww_compare w_add_mul_div ww_sub w_digits w_zdigits low w_to_Z - ZnZ.spec_0 ZnZ.spec_to_Z spec_ww_to_Z - ZnZ.spec_WW ZnZ.spec_WO ZnZ.spec_OW - spec_ww_compare ZnZ.spec_add_mul_div spec_ww_sub - ZnZ.spec_zdigits spec_low W0 (WW xh xl) zp1 Hp). - unfold add_mul_div; - case DoubleLift.ww_add_mul_div; autorewrite with w_rewrite; auto. - rewrite Zmult_0_l; rewrite Zplus_0_l. - rewrite zp1_b. - generalize mmul_aux0; unfold w_digits; intros tmp; rewrite tmp; clear tmp. - intros H1 H2. - rewrite <- H2. - rewrite Zplus_0_l. - generalize mmul_aux3; simpl ww_to_Z; intros tmp; rewrite tmp; clear tmp; - auto with zarith. - unfold xl1; unfold w_pos_mod. - rewrite <- p_b; rewrite <- zp_b. - rewrite <- ZnZ.spec_pos_mod; auto with zarith. - unfold w_compare; rewrite ZnZ.spec_compare; - case Zcompare_spec; intros Hc; - match goal with H: context[b] |- _ => - generalize H; clear H - end; try rewrite _w0_is_0. - intros H3; rewrite H3. - rewrite Z_mod_same; auto with zarith. - intros H3; rewrite Zmod_small; auto with zarith. - case (ZnZ.spec_to_Z (ZnZ.pos_mod zp xl)); unfold w_to_Z; auto with zarith. - rewrite p_b; rewrite ZnZ.spec_pos_mod; auto with zarith. - intros H3; assert (HH: [|xl|] mod 2 ^ Zpos p = 2 ^ Zpos p). - apply Zle_antisym; auto with zarith. - case (Z_mod_lt ([|xl|]) (2 ^ Zpos p)); auto with zarith. - rewrite zp_b in H3; auto with zarith. - rewrite zp_b; rewrite HH. - rewrite <- Zmod_minus_one; auto with zarith. - rewrite _w1_is_1; rewrite Zmod_small; auto with zarith. - rewrite Zmult_0_l; rewrite Zplus_0_l. - rewrite zp1_b. - generalize mmul_aux0; unfold w_digits; intros tmp; rewrite tmp; clear tmp. - intros w2 w3 H1 H2; rewrite <- H2. - generalize mmul_aux3; simpl ww_to_Z; intros tmp; rewrite tmp; clear tmp; - auto with zarith. - rewrite <- p_b; rewrite <- zp_b. - rewrite <- ZnZ.spec_pos_mod; auto with zarith. - unfold xl1; unfold w_pos_mod. - rewrite Zplus_comm. - apply _add_mod_correct; auto with zarith. - assert (tmp: forall x, 2 * x = x + x); auto with zarith; - rewrite tmp; apply Zplus_le_lt_compat; clear tmp; auto with zarith. - rewrite ZnZ.spec_pos_mod; auto with zarith. - rewrite p_b; case (Z_mod_lt [|xl|] (2 ^ Zpos p)); auto with zarith. - rewrite zp_b; auto with zarith. - rewrite H2; apply Zdiv_lt_upper_bound; auto with zarith. - Qed. - - Lemma _mmul_mod_spec: forall w1 w2 t1 t2, [|w1|] = t1 mod [|b|] -> [|w2|] = t2 mod [|b|] -> - [|_mmul_mod w1 w2|] = ([|w1|] * [|w2|]) mod [|b|]. - intros w2 w3 t1 t2; unfold _mmul_mod, w_mul_c; intros H H1. - assert (F: [|w2|] < [|b|]). - case (Z_mod_lt t1 [|b|]); auto with zarith. - assert (F': [|w3|] < [|b|]). - case (Z_mod_lt t2 [|b|]); auto with zarith. - match goal with |- context[ZnZ.mul_c ?x ?y] => - generalize (ZnZ.spec_mul_c x y); unfold interp_carry; - case (ZnZ.mul_c x y); autorewrite with w_rewrite - end; auto with zarith. - simpl; intros H2; rewrite <- H2; rewrite Zmod_small; - auto with zarith. - intros w4 w5 H2. - rewrite mmul_aux5; auto with zarith. - rewrite <- H2; auto. - unfold ww_to_Z,w_digits,w_to_Z; rewrite H2. - apply Zmult_lt_compat; auto with zarith. - case (ZnZ.spec_to_Z w2); auto with zarith. - case (ZnZ.spec_to_Z w3); auto with zarith. - Qed. - - Let _msquare_mod x := - let xy := w_square_c x in - match xy with - W0 => w0 - | WW xh xl => - let xl1 := w_pos_mod zp xl in - match add_mul_div zp1 W0 xy with - W0 => match w_compare xl1 b with - | Lt => xl1 - | Eq => w0 - | Gt => w1 - end - | WW _ xl2 => _add_mod xl1 xl2 - end - end. - - Lemma _msquare_mod_spec: forall w1 t1, [|w1|] = t1 mod [|b|] -> - [|_msquare_mod w1|] = ([|w1|] * [|w1|]) mod [|b|]. - intros w2 t2; unfold _msquare_mod, w_square_c; intros H. - assert (F: [|w2|] < [|b|]). - case (Z_mod_lt t2 [|b|]); auto with zarith. - match goal with |- context[ZnZ.square_c ?x] => - generalize (ZnZ.spec_square_c x); unfold interp_carry; - case (ZnZ.square_c x); autorewrite with w_rewrite - end; auto with zarith. - simpl; intros H2; rewrite <- H2; rewrite Zmod_small; - auto with zarith. - intros w4 w5 H2. - rewrite mmul_aux5; auto with zarith. - unfold ww_to_Z, w_to_Z ,w_digits; rewrite <- H2; auto. - unfold ww_to_Z,w_to_Z ,w_digits; rewrite H2. - apply Zmult_lt_compat; auto with zarith. - case (ZnZ.spec_to_Z w2); auto with zarith. - case (ZnZ.spec_to_Z w2); auto with zarith. - Qed. - - Definition mmake_mod_op := - mk_mod_op - _succ_mod _add_mod - _pred_mod _sub_mod - _mmul_mod _msquare_mod _power_mod. - - Definition mmake_mod_spec: mod_spec mmake_mod_op. - apply mk_mod_spec. - exact _succ_mod_spec. - exact _add_mod_spec. - exact _pred_mod_spec. - exact _sub_mod_spec. - exact _mmul_mod_spec. - exact _msquare_mod_spec. - exact _power_mod_spec. - Defined. - -End Mod_op. - diff --git a/coqprime/num/NEll.v b/coqprime/num/NEll.v deleted file mode 100644 index 28dd63181..000000000 --- a/coqprime/num/NEll.v +++ /dev/null @@ -1,983 +0,0 @@ - -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) - - -Require Import ZArith Znumtheory Zpow_facts. -Require Import CyclicAxioms DoubleCyclic BigN Cyclic31 Int31. -Require Import W. -Require Import Mod_op. -Require Import ZEll. -Require Import Bits. -Import CyclicAxioms DoubleType DoubleBase. - - -Set Implicit Arguments. - -Open Scope Z_scope. - - -Record ex: Set := mkEx { - vN : positive; - vS : positive; - vR: List.list (positive * positive); - vA: Z; - vB: Z; - vx: Z; - vy: Z -}. - -Coercion Local Zpos : positive >-> Z. - -Record ex_spec (exx: ex): Prop := mkExS { - n2_div: ~(2 | exx.(vN)); - n_pos: 2 < exx.(vN); - lprime: - forall p : positive * positive, List.In p (vR exx) -> prime (fst p); - lbig: - 4 * vN exx < (Zmullp (vR exx) - 1) ^ 2; - inC: - vy exx ^ 2 mod vN exx = (vx exx ^ 3 + vA exx * vx exx + vB exx) mod vN exx -}. - -Section NEll. - -Variable exx: ex. -Variable exxs: ex_spec exx. - -Variable zZ: Type. -Variable op: ZnZ.Ops zZ. -Variable op_spec: ZnZ.Specs op. -Definition z2Z z := ZnZ.to_Z z. -Definition zN := snd (ZnZ.of_pos exx.(vN)). -Variable mop: mod_op zZ. -Variable mop_spec: mod_spec op zN mop. -Variable N_small: exx.(vN) < base (ZnZ.digits op). - -Lemma z2ZN: z2Z zN = exx.(vN). -apply (@ZnZ.of_Z_correct _ _ op_spec exx.(vN)); split; auto with zarith. -Qed. - -Definition Z2z z := - match z mod exx.(vN) with - | Zpos p => snd (ZnZ.of_pos p) - | _ => ZnZ.zero - end. - -Definition S := exx.(vS). -Definition R := exx.(vR). -Definition A := Z2z exx.(vA). -Definition B := Z2z exx.(vB). -Definition xx := Z2z exx.(vx). -Definition yy := Z2z exx.(vy). -Definition c3 := Z2z 3. -Definition c2 := Z2z 2. -Definition c1 := Z2z 1. -Definition c0 := Z2z 0. - -Inductive nelt: Type := - nzero | ntriple: zZ -> zZ -> zZ -> nelt. - -Definition pp := ntriple xx yy c1. - -Definition nplus x y := mop.(add_mod) x y. -Definition nmul x y := mop.(mul_mod) x y. -Definition nsub x y := mop.(sub_mod) x y. -Definition neq x y := match ZnZ.compare x y with Eq => true | _ => false end. - -Notation "x ++ y " := (nplus x y). -Notation "x -- y" := (nsub x y) (at level 50, left associativity). -Notation "x ** y" := (nmul x y) (at level 40, left associativity). -Notation "x ?= y" := (neq x y). - -Definition ndouble: zZ -> nelt -> (nelt * zZ):= fun (sc: zZ) (p1: nelt) => - match p1 with - nzero => (p1, sc) - | (ntriple x1 y1 z1) => - if (y1 ?= c0) then (nzero, z1 ** sc) else - (* we do 2p *) - let m' := c3 ** x1 ** x1 ++ A ** z1 ** z1 in - let l' := c2 ** y1 ** z1 in - let m'2 := m' ** m' in - let l'2 := l' ** l' in - let l'3 := l'2 ** l' in - let x3 := m'2 ** z1 -- c2 ** x1 ** l'2 in - (ntriple - (l' ** x3) - (l'2 ** (m' ** x1 -- y1 ** l') -- m' ** x3) - (z1 ** l'3), sc) - end. - - -Definition nadd := fun (sc: zZ) (p1 p2: nelt) => - match p1, p2 with - nzero, _ => (p2, sc) - | _ , nzero => (p1, sc) - | (ntriple x1 y1 z1), (ntriple x2 y2 z2) => - let d1 := x2 ** z1 in - let d2 := x1 ** z2 in - let l := d1 -- d2 in - let dl := d1 ++ d2 in - let m := y2 ** z1 -- y1 ** z2 in - if (l ?= c0) then - (* we have p1 = p2 o p1 = -p2 *) - if (m ?= c0) then - if (y1 ?= c0) then (nzero, z1 ** z2 ** sc) else - (* we do 2p *) - let m' := c3 ** x1 ** x1 ++ A ** z1 ** z1 in - let l' := c2 ** y1 ** z1 in - let m'2 := m' ** m' in - let l'2 := l' ** l' in - let l'3 := l'2 ** l' in - let x3 := m'2 ** z1 -- c2 ** x1 ** l'2 in - (ntriple - (l' ** x3) - (l'2 ** (m' ** x1 -- y1 ** l') -- m' ** x3) - (z1 ** l'3), z2 ** sc) - else (* p - p *) (nzero, m ** z1 ** z2 ** sc) - else - let l2 := l ** l in - let l3 := l2 ** l in - let m2 := m ** m in - let x3 := z1 ** z2 ** m2 -- l2 ** dl in - (ntriple (l ** x3) - (z2 ** l2 ** (m ** x1 -- y1 ** l) -- m ** x3) - (z1 ** z2 ** l3), sc) - end. - - -Definition nopp p := - match p with nzero => p | (ntriple x1 y1 z1) => (ntriple x1 (c0 -- y1) z1) end. - -Fixpoint scalb (sc: zZ) (b:bool) (a: nelt) (p: positive) {struct p}: - nelt * zZ := - match p with - xH => if b then ndouble sc a else (a,sc) - | xO p1 => let (a1, sc1) := scalb sc false a p1 in - if b then - let (a2, sc2) := ndouble sc1 a1 in - nadd sc2 a a2 - else ndouble sc1 a1 - | xI p1 => let (a1, sc1) := scalb sc true a p1 in - if b then ndouble sc1 a1 - else - let (a2, sc2) := ndouble sc1 a1 in - nadd sc2 (nopp a) a2 - end. - -Definition scal sc a p := scalb sc false a p. - - -Definition scal_list sc a l := - List.fold_left - (fun (asc: nelt * zZ) p1 => let (a,sc) := asc in scal sc a p1) l (a,sc). - -Fixpoint scalL (sc:zZ) (a: nelt) (l: List.list positive) {struct l}: (nelt * zZ) := - match l with - List.nil => (a,sc) - | List.cons n l1 => - let (a1, sc1) := scal sc a n in - let (a2, sc2) := scal_list sc1 a l1 in - match a2 with - nzero => (nzero, c0) - | ntriple _ _ z => scalL (sc2 ** z) a1 l1 - end - end. - -Definition zpow sc p n := - let (p,sc') := scal sc p n in - (p, ZnZ.to_Z (ZnZ.gcd sc' zN)). - -Definition e2E n := - match n with - nzero => ZEll.nzero - | ntriple x1 y1 z1 => ZEll.ntriple (z2Z x1) (z2Z y1) (z2Z z1) - end. - - -Definition wft t := z2Z t = (z2Z t) mod (z2Z zN). - -Lemma vN_pos: 0 < exx.(vN). -red; simpl; auto. -Qed. - -Hint Resolve vN_pos. - -Lemma nplusz: forall x y, wft x -> wft y -> - z2Z (x ++ y) = ZEll.nplus (vN exx) (z2Z x) (z2Z y). -Proof. -intros x y Hx Hy. -unfold z2Z, nplus. -rewrite (mop_spec.(add_mod_spec) _ _ _ _ Hx Hy); auto. -rewrite <- z2ZN; auto. -Qed. - -Lemma nplusw: forall x y, wft x -> wft y -> wft (x ++ y). -Proof. -intros x y Hx Hy. -unfold wft. -pattern (z2Z (x ++ y)) at 2; rewrite (nplusz Hx Hy). -unfold ZEll.nplus; rewrite z2ZN. -rewrite Zmod_mod; auto. -apply (nplusz Hx Hy). -Qed. - -Lemma nsubz: forall x y, wft x -> wft y -> - z2Z (x -- y) = ZEll.nsub (vN exx) (z2Z x) (z2Z y). -Proof. -intros x y Hx Hy. -unfold z2Z, nsub. -rewrite (mop_spec.(sub_mod_spec) _ _ _ _ Hx Hy); auto. -rewrite <- z2ZN; auto. -Qed. - -Lemma nsubw: forall x y, wft x -> wft y -> wft (x -- y). -Proof. -intros x y Hx Hy. -unfold wft. -pattern (z2Z (x -- y)) at 2; rewrite (nsubz Hx Hy). -unfold ZEll.nsub; rewrite z2ZN. -rewrite Zmod_mod; auto. -apply (nsubz Hx Hy). -Qed. - -Lemma nmulz: forall x y, wft x -> wft y -> - z2Z (x ** y) = ZEll.nmul (vN exx) (z2Z x) (z2Z y). -Proof. -intros x y Hx Hy. -unfold z2Z, nmul. -rewrite (mop_spec.(mul_mod_spec) _ _ _ _ Hx Hy); auto. -rewrite <- z2ZN; auto. -Qed. - -Lemma nmulw: forall x y, wft x -> wft y -> wft (x ** y). -Proof. -intros x y Hx Hy. -unfold wft. -pattern (z2Z (x ** y)) at 2; rewrite (nmulz Hx Hy). -unfold ZEll.nmul; rewrite z2ZN. -rewrite Zmod_mod; auto. -apply (nmulz Hx Hy). -Qed. - -Hint Resolve nmulw nplusw nsubw. - - -Definition wfe p := match p with - ntriple x y z => wft x /\ wft y /\ wft z -| _ => True -end. - -Lemma z2Zx: forall x, z2Z (Z2z x) = x mod exx.(vN). -unfold Z2z; intros x. -generalize (Z_mod_lt x exx.(vN)). -case_eq (x mod exx.(vN)). -intros _ _. -simpl; unfold z2Z; rewrite ZnZ.spec_0; auto. -intros p Hp HH; case HH; auto with zarith; clear HH. -intros _ HH1. -case (ZnZ.spec_to_Z zN). -generalize z2ZN; unfold z2Z; intros HH; rewrite HH; auto. -intros _ H0. -set (v := ZnZ.of_pos p); generalize HH1. -rewrite (ZnZ.spec_of_pos p); fold v. -case (fst v). - simpl; auto. -intros p1 H1. -contradict H0; apply Zle_not_lt. -apply Zlt_le_weak; apply Zle_lt_trans with (2:= H1). -apply Zle_trans with (1 * base (ZnZ.digits op) + 0); auto with zarith. -apply Zplus_le_compat; auto. -apply Zmult_gt_0_le_compat_r; auto with zarith. - case (ZnZ.spec_to_Z (snd v)); auto with zarith. - case p1; red; simpl; intros; discriminate. - case (ZnZ.spec_to_Z (snd v)); auto with zarith. -intros p Hp; case (Z_mod_lt x exx.(vN)); auto with zarith. -rewrite Hp; intros HH; case HH; auto. -Qed. - - -Lemma z2Zx1: forall x, z2Z (Z2z x) = z2Z (Z2z x) mod z2Z zN. -Proof. -unfold Z2z; intros x. -generalize (Z_mod_lt x exx.(vN)). -case_eq (x mod exx.(vN)). -intros _ _. -simpl; unfold z2Z; rewrite ZnZ.spec_0; auto. -intros p H1 H2. -case (ZnZ.spec_to_Z zN). -generalize z2ZN; unfold z2Z; intros HH; rewrite HH; auto. -intros _ H0. -case H2; auto with zarith; clear H2; intros _ H2. -rewrite Zmod_small; auto. -set (v := ZnZ.of_pos p). -split. - case (ZnZ.spec_to_Z (snd v)); auto. -generalize H2; rewrite (ZnZ.spec_of_pos p); fold v. -case (fst v). - simpl; auto. -intros p1 H. -contradict H0; apply Zle_not_lt. -apply Zlt_le_weak; apply Zle_lt_trans with (2:= H). -apply Zle_trans with (1 * base (ZnZ.digits op) + 0); auto with zarith. -apply Zplus_le_compat; auto. -apply Zmult_gt_0_le_compat_r; auto with zarith. - case (ZnZ.spec_to_Z (snd v)); auto with zarith. - case p1; red; simpl; intros; discriminate. - case (ZnZ.spec_to_Z (snd v)); auto with zarith. -intros p Hp; case (Z_mod_lt x exx.(vN)); auto with zarith. -rewrite Hp; intros HH; case HH; auto. -Qed. - - -Lemma c0w: wft c0. -Proof. -red; unfold c0; apply z2Zx1. -Qed. - -Lemma c2w: wft c2. -Proof. -red; unfold c2; apply z2Zx1. -Qed. - -Lemma c3w: wft c3. -Proof. -red; unfold c3; apply z2Zx1. -Qed. - -Lemma Aw: wft A. -Proof. -red; unfold A; apply z2Zx1. -Qed. - -Hint Resolve c0w c2w c3w Aw. - -Ltac nw := - repeat (apply nplusw || apply nsubw || apply nmulw || apply c2w || - apply c3w || apply Aw); auto. - - -Lemma nadd_wf: forall x y sc, - wfe x -> wfe y -> wft sc -> - wfe (fst (nadd sc x y)) /\ wft (snd (nadd sc x y)). -Proof. -intros x; case x; clear; auto. -intros x1 y1 z1 y; case y; clear; auto. - intros x2 y2 z2 sc (wfx1,(wfy1, wfz1)) (wfx2,(wfy2, wfz2)) wfsc; - simpl; auto. - case neq. - 2: repeat split; simpl; nw. - case neq. - 2: repeat split; simpl; nw. - case neq. - repeat split; simpl; nw; auto. - repeat split; simpl; nw; auto. -Qed. - - Lemma ztest: forall x y, - x ?= y =Zeq_bool (z2Z x) (z2Z y). - Proof. - intros x y. - unfold neq. - rewrite (ZnZ.spec_compare x y); case Zcompare_spec; intros HH; - match goal with H: context[x] |- _ => - generalize H; clear H; intros HH1 - end. - symmetry; apply GZnZ.Zeq_iok; auto. - case_eq (Zeq_bool (z2Z x) (z2Z y)); intros H1; auto; - generalize HH1; generalize (Zeq_bool_eq _ _ H1); unfold z2Z; - intros HH; rewrite HH; auto with zarith. - case_eq (Zeq_bool (z2Z x) (z2Z y)); intros H1; auto; - generalize HH1; generalize (Zeq_bool_eq _ _ H1); unfold z2Z; - intros HH; rewrite HH; auto with zarith. - Qed. - - Lemma zc0: z2Z c0 = 0. - Proof. - unfold z2Z, c0, z2Z; simpl. - generalize ZnZ.spec_0; auto. - Qed. - - -Ltac iftac t := - match t with - context[if ?x ?= ?y then _ else _] => - case_eq (x ?= y) - end. - -Ltac ftac := match goal with - |- context[?x = ?y] => (iftac x); - let H := fresh "tmp" in - (try rewrite ztest; try rewrite zc0; intros H; - repeat ((rewrite nmulz in H || rewrite nplusz in H || rewrite nsubz in H); auto); - try (rewrite H; clear H)) - end. - -Require Import Zmod. - -Lemma c2ww: forall x, ZEll.nmul (vN exx) 2 x = ZEll.nmul (vN exx) (z2Z c2) x. -intros x; unfold ZEll.nmul. -unfold c2; rewrite z2Zx; rewrite Zmodml; auto. -Qed. -Lemma c3ww: forall x, ZEll.nmul (vN exx) 3 x = ZEll.nmul (vN exx) (z2Z c3) x. -intros x; unfold ZEll.nmul. -unfold c3; rewrite z2Zx; rewrite Zmodml; auto. -Qed. - -Lemma Aww: forall x, ZEll.nmul (vN exx) exx.(vA) x = ZEll.nmul (vN exx) (z2Z A) x. -intros x; unfold ZEll.nmul. -unfold A; rewrite z2Zx; rewrite Zmodml; auto. -Qed. - -Lemma nadd_correct: forall x y sc, - wfe x -> wfe y -> wft sc -> - e2E (fst (nadd sc x y)) = fst (ZEll.nadd exx.(vN) exx.(vA) (z2Z sc) (e2E x) (e2E y) )/\ - z2Z (snd (nadd sc x y)) = snd (ZEll.nadd exx.(vN) exx.(vA) (z2Z sc) (e2E x) (e2E y)). -Proof. -intros x; case x; clear; auto. -intros x1 y1 z1 y; case y; clear; auto. - intros x2 y2 z2 sc (wfx1,(wfy1, wfz1)) (wfx2,(wfy2, wfz2)) wfsc; simpl. - ftac. - ftac. - ftac. - simpl; split; auto. - repeat ((rewrite nmulz || rewrite nplusz || rewrite nsubz); auto). - simpl; split; auto. - repeat ((rewrite nmulz || rewrite nplusz || rewrite nsubz|| - rewrite c2ww || rewrite c3ww || rewrite Aww); try nw; auto). - rewrite nmulz; auto. - simpl; split; auto. - repeat ((rewrite nmulz || rewrite nplusz || rewrite nsubz); auto). - simpl; split; auto. - repeat ((rewrite nmulz || rewrite nplusz || rewrite nsubz || - rewrite c2ww || rewrite c3ww || rewrite Aww); try nw; auto). - Qed. - - Lemma ndouble_wf: forall x sc, - wfe x -> wft sc -> - wfe (fst (ndouble sc x)) /\ wft (snd (ndouble sc x)). -Proof. -intros x; case x; clear; auto. -intros x1 y1 z1 sc (wfx1,(wfy1, wfz1)) wfsc; - simpl; auto. - repeat (case neq; repeat split; simpl; nw; auto). -Qed. - - -Lemma ndouble_correct: forall x sc, - wfe x -> wft sc -> - e2E (fst (ndouble sc x)) = fst (ZEll.ndouble exx.(vN) exx.(vA) (z2Z sc) (e2E x))/\ - z2Z (snd (ndouble sc x)) = snd (ZEll.ndouble exx.(vN) exx.(vA) (z2Z sc) (e2E x)). -Proof. -intros x; case x; clear; auto. - intros x1 y1 z1 sc (wfx1,(wfy1, wfz1)) wfsc; simpl. - ftac. - simpl; split; auto. - repeat ((rewrite nmulz || rewrite nplusz || rewrite nsubz); auto). - simpl; split; auto. - repeat ((rewrite nmulz || rewrite nplusz || rewrite nsubz || - rewrite c2ww || rewrite c3ww || rewrite Aww); try nw; auto). - Qed. - -Lemma nopp_wf: forall x, wfe x -> wfe (nopp x). -Proof. -intros x; case x; simpl nopp; auto. -intros x1 y1 z1 [H1 [H2 H3]]; repeat split; auto. -Qed. - -Lemma scalb_wf: forall n b x sc, - wfe x -> wft sc -> - wfe (fst (scalb sc b x n)) /\ wft (snd (scalb sc b x n)). -Proof. -intros n; elim n; unfold scalb; fold scalb; auto. - intros n1 Hrec b x sc H H1. - case (Hrec true x sc H H1). - case scalb; simpl fst; simpl snd. - intros a1 sc1 H2 H3. - case (ndouble_wf _ H2 H3); auto; - case ndouble; simpl fst; simpl snd; intros x2 sc2 H4 H5. - case b; auto. - case (nadd_wf _ _ (nopp_wf _ H) H4 H5); auto; - case ndouble; simpl fst; simpl snd; intros x2 sc2 H4 H5. - intros n1 Hrec b x sc H H1. - case (Hrec false x sc H H1). - case scalb; simpl fst; simpl snd. - intros a1 sc1 H2 H3. - case (ndouble_wf _ H2 H3); auto; - case ndouble; simpl fst; simpl snd; intros x2 sc2 H4 H5. - case b; auto. - case (nadd_wf _ _ H H4 H5); auto; - case ndouble; simpl fst; simpl snd; intros x2 sc2 H4 H5. -intros b x sc H H1; case b; auto. -case (ndouble_wf _ H H1); auto. -Qed. - - -Lemma scal_wf: forall n x sc, - wfe x -> wft sc -> - wfe (fst (scal sc x n)) /\ wft (snd (scal sc x n)). -Proof. -intros n; exact (scalb_wf n false). -Qed. - -Lemma nopp_correct: forall x, - wfe x -> e2E x = ZEll.nopp exx.(vN) (e2E (nopp x)). -Proof. -intros x; case x; simpl; auto. -intros x1 y1 z1 [H1 [H2 H3]]; apply f_equal3 with (f := ZEll.ntriple); auto. -rewrite nsubz; auto. -rewrite zc0. -unfold ZEll.nsub, ninv; simpl. -apply sym_equal. -rewrite <- (Z_mod_plus) with (b := -(-z2Z y1 /exx.(vN))); auto with zarith. -rewrite <- Zopp_mult_distr_l. -rewrite <- Zopp_plus_distr. -rewrite Zmult_comm; rewrite Zplus_comm. -rewrite <- Z_div_mod_eq; auto with zarith. -rewrite Zopp_involutive; rewrite <- z2ZN. -apply sym_equal; auto. -Qed. - -Lemma scalb_correct: forall n b x sc, - wfe x -> wft sc -> - e2E (fst (scalb sc b x n)) = fst (ZEll.scalb exx.(vN) exx.(vA) (z2Z sc) b (e2E x) n)/\ - z2Z (snd (scalb sc b x n)) = snd (ZEll.scalb exx.(vN) exx.(vA) (z2Z sc) b (e2E x) n). -Proof. -intros n; elim n; clear; auto. -intros p Hrec b x sc H1 H2. - case b; unfold scalb; fold scalb. - generalize (scalb_wf p true x H1 H2); - generalize (Hrec true _ _ H1 H2); case scalb; simpl. - case ZEll.scalb; intros r1 rc1; simpl. - intros a2 sc2 (H3, H4) (H5, H6); subst r1 rc1. - apply ndouble_correct; auto. - generalize (scalb_wf p true x H1 H2); - generalize (Hrec true _ _ H1 H2); case scalb; simpl. - case ZEll.scalb; intros r1 rc1; simpl. - intros a2 sc2 (H3, H4) (H5, H6); subst r1 rc1. - generalize (ndouble_wf _ H5 H6); - generalize (ndouble_correct _ H5 H6); case ndouble; simpl. - case ZEll.ndouble; intros r1 rc1; simpl. - intros a3 sc3 (H7,H8) (H9,H10); subst r1 rc1. - replace (ZEll.nopp (vN exx) (e2E x)) with - (e2E (nopp x)). - apply nadd_correct; auto. - generalize H1; case x; auto. - intros x1 y1 z1 [HH1 [HH2 HH3]]; split; auto. - rewrite nopp_correct; auto. - apply f_equal2 with (f := ZEll.nopp); auto. - generalize H1; case x; simpl; auto; clear x H1. - intros x1 y1 z1 [HH1 [HH2 HH3]]; - apply f_equal3 with (f := ZEll.ntriple); auto. - repeat rewrite nsubz; auto. - rewrite zc0. - unfold ZEll.nsub; simpl. - rewrite <- (Z_mod_plus) with (b := -(-z2Z y1 /exx.(vN))); auto with zarith. - rewrite <- Zopp_mult_distr_l. - rewrite <- Zopp_plus_distr. - rewrite Zmult_comm; rewrite Zplus_comm. - rewrite <- Z_div_mod_eq; auto with zarith. - rewrite Zopp_involutive; rewrite <- z2ZN. - apply sym_equal; auto. - generalize H1; case x; auto. - intros x1 y1 z1 [HH1 [HH2 HH3]]; split; auto. -intros p Hrec b x sc H1 H2. - case b; unfold scalb; fold scalb. - generalize (scalb_wf p false x H1 H2); - generalize (Hrec false _ _ H1 H2); case scalb; simpl. - case ZEll.scalb; intros r1 rc1; simpl. - intros a2 sc2 (H3, H4) (H5, H6); subst r1 rc1. - generalize (ndouble_wf _ H5 H6); - generalize (ndouble_correct _ H5 H6); case ndouble; simpl. - case ZEll.ndouble; intros r1 rc1; simpl. - intros a3 sc3 (H7,H8) (H9,H10); subst r1 rc1. - replace (ZEll.nopp (vN exx) (e2E x)) with - (e2E (nopp x)). - apply nadd_correct; auto. - rewrite nopp_correct; auto. - apply f_equal2 with (f := ZEll.nopp); auto. - generalize H1; case x; simpl; auto; clear x H1. - intros x1 y1 z1 [HH1 [HH2 HH3]]; - apply f_equal3 with (f := ZEll.ntriple); auto. - repeat rewrite nsubz; auto. - rewrite zc0. - unfold ZEll.nsub; simpl. - rewrite <- (Z_mod_plus) with (b := -(-z2Z y1 /exx.(vN))); auto with zarith. - rewrite <- Zopp_mult_distr_l. - rewrite <- Zopp_plus_distr. - rewrite Zmult_comm; rewrite Zplus_comm. - rewrite <- Z_div_mod_eq; auto with zarith. - rewrite Zopp_involutive; rewrite <- z2ZN. - apply sym_equal; auto. - generalize H1; case x; auto. - intros x1 y1 z1 [HH1 [HH2 HH3]]; split; auto. - generalize (scalb_wf p false x H1 H2); - generalize (Hrec false _ _ H1 H2); case scalb; simpl. - case ZEll.scalb; intros r1 rc1; simpl. - intros a2 sc2 (H3, H4) (H5, H6); subst r1 rc1. - apply ndouble_correct; auto. -intros b x sc H H1. -case b; simpl; auto. -apply ndouble_correct; auto. -Qed. - - -Lemma scal_correct: forall n x sc, - wfe x -> wft sc -> - e2E (fst (scal sc x n)) = fst (ZEll.scal exx.(vN) exx.(vA) (z2Z sc) (e2E x) n)/\ - z2Z (snd (scal sc x n)) = snd (ZEll.scal exx.(vN) exx.(vA) (z2Z sc) (e2E x) n). -Proof. -intros n; exact (scalb_correct n false). -Qed. - -Lemma scal_list_correct: forall l x sc, - wfe x -> wft sc -> - e2E (fst (scal_list sc x l)) = fst (ZEll.scal_list exx.(vN) exx.(vA) (z2Z sc) (e2E x) l)/\ - z2Z (snd (scal_list sc x l)) = snd (ZEll.scal_list exx.(vN) exx.(vA) (z2Z sc) (e2E x) l). -Proof. -intros l1; elim l1; simpl; auto. -unfold scal_list, ZEll.scal_list; simpl; intros a l2 Hrec x sc H1 H2. -generalize (scal_correct a _ H1 H2) (scal_wf a _ H1 H2); case scal. -case ZEll.scal; intros r1 rsc1; simpl. -simpl; intros a1 sc1 (H3, H4) (H5, H6); subst r1 rsc1; auto. -Qed. - -Lemma scal_list_wf: forall l x sc, - wfe x -> wft sc -> - wfe (fst (scal_list sc x l)) /\ wft (snd (scal_list sc x l)). -Proof. -intros l1; elim l1; simpl; auto. -unfold scal_list; intros a l Hrec x sc H1 H2; simpl. -generalize (@scal_wf a _ _ H1 H2); - case (scal sc x a); simpl; intros x1 sc1 [H3 H4]; auto. -Qed. - -Lemma scalL_wf: forall l x sc, - wfe x -> wft sc -> - wfe (fst (scalL sc x l)) /\ wft (snd (scalL sc x l)). -Proof. -intros l1; elim l1; simpl; auto. -intros a l2 Hrec x sc H1 H2. -generalize (scal_wf a _ H1 H2); case scal; simpl. -intros a1 sc1 (H3, H4); auto. -generalize (scal_list_wf l2 _ H1 H4); case scal_list; simpl. -intros a2 sc2; case a2; simpl; auto. -intros x1 y1 z1 ((V1, (V2, V3)), V4); apply Hrec; auto. -Qed. - -Lemma scalL_correct: forall l x sc, - wfe x -> wft sc -> - e2E (fst (scalL sc x l)) = fst (ZEll.scalL exx.(vN) exx.(vA) (z2Z sc) (e2E x) l)/\ - z2Z (snd (scalL sc x l)) = snd (ZEll.scalL exx.(vN) exx.(vA) (z2Z sc) (e2E x) l). -Proof. -intros l1; elim l1; simpl; auto. -intros a l2 Hrec x sc H1 H2. -generalize (scal_wf a _ H1 H2) (scal_correct a _ H1 H2); case scal; simpl. -case ZEll.scal; intros r1 rsc1; simpl. -intros a1 sc1 (H3, H4) (H5, H6); subst r1 rsc1. -generalize (scal_list_wf l2 _ H1 H4) (scal_list_correct l2 _ H1 H4); case scal_list; simpl. -case ZEll.scal_list; intros r1 rsc1; simpl. -intros a2 sc2 (H7, H8) (H9, H10); subst r1 rsc1. -generalize H7; clear H7; case a2; simpl; auto. -rewrite zc0; auto. -intros x1 y1 z1 (V1, (V2, V3)); auto. -generalize (nmulw H8 V3) (nmulz H8 V3); intros V4 V5; rewrite <- V5. -apply Hrec; auto. -Qed. - -Lemma f4 : wft (Z2z 4). -Proof. -red; apply z2Zx1. -Qed. - -Lemma f27 : wft (Z2z 27). -Proof. -red; apply z2Zx1. -Qed. - -Lemma Bw : wft B. -Proof. -red; unfold B; apply z2Zx1. -Qed. - -Hint Resolve f4 f27 Bw. - -Lemma mww: forall x y, ZEll.nmul (vN exx) (x mod (vN exx) ) y = ZEll.nmul (vN exx) x y. -intros x y; unfold ZEll.nmul; rewrite Zmodml; auto. -Qed. - -Lemma wwA: forall x, ZEll.nmul (vN exx) x exx.(vA) = ZEll.nmul (vN exx) x (z2Z A). -intros x; unfold ZEll.nmul. -unfold A; rewrite z2Zx; rewrite Zmodmr; auto. -Qed. - -Lemma wwB: forall x, ZEll.nmul (vN exx) x exx.(vB) = ZEll.nmul (vN exx) x (z2Z B). -intros x; unfold ZEll.nmul. -unfold B; rewrite z2Zx; rewrite Zmodmr; auto. -Qed. - - Lemma scalL_prime: - let a := ntriple (Z2z (exx.(vx))) (Z2z (exx.(vy))) c1 in - let isc := (Z2z 4) ** A ** A ** A ++ (Z2z 27) ** B ** B in - let (a1, sc1) := scal isc a exx.(vS) in - let (S1,R1) := psplit exx.(vR) in - let (a2, sc2) := scal sc1 a1 S1 in - let (a3, sc3) := scalL sc2 a2 R1 in - match a3 with - nzero => if (Zeq_bool (Zgcd (z2Z sc3) exx.(vN)) 1) then prime exx.(vN) - else True - | _ => True - end. - Proof. - intros a isc. - case_eq (scal isc a (vS exx)); intros a1 sc1 Ha1. - case_eq (psplit (vR exx)); intros S1 R1 HS1. - case_eq (scal sc1 a1 S1); intros a2 sc2 Ha2. - case_eq (scalL sc2 a2 R1); intros a3 sc3; case a3; auto. - intros Ha3; case_eq (Zeq_bool (Zgcd (z2Z sc3) (vN exx)) 1); auto. - intros H1. - assert (F0: - (vy exx mod vN exx) ^ 2 mod vN exx = - ((vx exx mod vN exx) ^ 3 + vA exx * (vx exx mod vN exx) + - vB exx) mod vN exx). - generalize exxs.(inC). - simpl; unfold Zpower_pos; simpl. - repeat rewrite Zmult_1_r. - intros HH. - match goal with |- ?t1 = ?t2 => rmod t1; auto end. - rewrite HH. - rewrite Zplus_mod; auto; symmetry; rewrite Zplus_mod; auto; symmetry. - apply f_equal2 with (f := Zmod); auto. - apply f_equal2 with (f := Zplus); auto. - rewrite Zplus_mod; auto; symmetry; rewrite Zplus_mod; auto; symmetry. - apply f_equal2 with (f := Zmod); auto. - apply f_equal2 with (f := Zplus); auto. - rewrite Zmult_mod; auto; symmetry; rewrite Zmult_mod; auto; symmetry. - apply f_equal2 with (f := Zmod); auto. - apply f_equal2 with (f := Zmult); auto. - rewrite Zmod_mod; auto. - match goal with |- ?t1 = ?t2 => rmod t2; auto end. - rewrite Zmult_mod; auto; symmetry; rewrite Zmult_mod; auto; symmetry. - apply f_equal2 with (f := Zmod); auto. - rewrite Zmod_mod; auto. - generalize (@ZEll.scalL_prime exx.(vN) - (exx.(vx) mod exx.(vN)) - (exx.(vy) mod exx.(vN)) - exx.(vA) - exx.(vB) - exxs.(n_pos) exxs.(n2_div) exx.(vR) - exxs.(lprime) exx.(vS) exxs.(lbig) F0); simpl. -generalize (@scal_wf (vS exx) a isc) (@scal_correct (vS exx) a isc). -unfold isc. -rewrite nplusz; auto; try nw; auto. -repeat rewrite nmulz; auto; try nw; auto. - repeat rewrite z2Zx. -repeat rewrite wwA || rewrite wwB|| rewrite mww. -replace (e2E a) with (ZEll.ntriple (vx exx mod vN exx) (vy exx mod vN exx) 1). -case ZEll.scal. -fold isc; rewrite HS1; rewrite Ha1; simpl; auto. -intros r1 rsc1 HH1 HH2. -case HH1; clear HH1. - unfold c1; repeat split; red; try apply z2Zx1. - unfold isc; nw. -case HH2; clear HH2. - unfold c1; repeat split; red; try apply z2Zx1. - unfold isc; nw. -intros U1 U2 W1 W2; subst r1 rsc1. -generalize (@scal_wf S1 a1 sc1) (@scal_correct S1 a1 sc1). -case ZEll.scal. -intros r1 rsc1 HH1 HH2. -case HH1; clear HH1; auto. -case HH2; clear HH2; auto. -rewrite Ha2; simpl. -intros U1 U2 W3 W4; subst r1 rsc1. -generalize (@scalL_wf R1 a2 sc2) (@scalL_correct R1 a2 sc2). -case ZEll.scalL. -intros n; case n; auto. -rewrite Ha3; simpl. -intros rsc1 HH1 HH2. -case HH1; clear HH1; auto. -case HH2; clear HH2; auto. -intros _ U2 _ W5; subst rsc1. -rewrite H1; auto. -intros x1 y1 z1 sc4; rewrite Ha3; simpl; auto. -intros _ HH; case HH; auto. -intros; discriminate. -unfold a; simpl. -unfold c1; repeat rewrite z2Zx. -rewrite (Zmod_small 1); auto. -generalize exxs.(n_pos). -auto with zarith. -Qed. - -End NEll. - -Fixpoint plength (p: positive) : positive := - match p with - xH => xH - | xO p1 => Psucc (plength p1) - | xI p1 => Psucc (plength p1) - end. - -Theorem plength_correct: forall p, (Zpos p < 2 ^ Zpos (plength p))%Z. -assert (F: (forall p, 2 ^ (Zpos (Psucc p)) = 2 * 2 ^ Zpos p)%Z). -intros p; replace (Zpos (Psucc p)) with (1 + Zpos p)%Z. -rewrite Zpower_exp; auto with zarith. -rewrite Zpos_succ_morphism; unfold Zsucc; auto with zarith. -intros p; elim p; simpl plength; auto. -intros p1 Hp1; rewrite F; repeat rewrite Zpos_xI. -assert (tmp: (forall p, 2 * p = p + p)%Z); - try repeat rewrite tmp; auto with zarith. -intros p1 Hp1; rewrite F; rewrite (Zpos_xO p1). -assert (tmp: (forall p, 2 * p = p + p)%Z); - try repeat rewrite tmp; auto with zarith. -rewrite Zpower_1_r; auto with zarith. -Qed. - -Theorem plength_pred_correct: forall p, (Zpos p <= 2 ^ Zpos (plength (Ppred p))) -%Z. -intros p; case (Psucc_pred p); intros H1. -subst; simpl plength. -rewrite Zpower_1_r; auto with zarith. -pattern p at 1; rewrite <- H1. -rewrite Zpos_succ_morphism; unfold Zsucc; auto with zarith. -generalize (plength_correct (Ppred p)); auto with zarith. -Qed. - -Definition pheight p := plength (Ppred (plength (Ppred p))). - -Theorem pheight_correct: forall p, (Zpos p <= 2 ^ (2 ^ (Zpos (pheight p))))%Z. -intros p; apply Zle_trans with (1 := (plength_pred_correct p)). -apply Zpower_le_monotone; auto with zarith. -split; auto with zarith. -unfold pheight; apply plength_pred_correct. -Qed. - -Definition isM2 p := - match p with - xH => false -| xO _ => false -| _ => true -end. - -Lemma isM2_correct: forall p, - if isM2 p then ~(Zdivide 2 p) /\ 2 < p else True. -Proof. -intros p; case p; simpl; auto; clear p. -intros p1; split; auto. -intros HH; inversion_clear HH. -generalize H; rewrite Zmult_comm. -case x; simpl; intros; discriminate. -case p1; red; simpl; auto. -Qed. - -Definition ell_test (N S: positive) (l: List.list (positive * positive)) - (A B x y: Z) := - let op := cmk_op (Peano.pred (nat_of_P (get_height 31 (plength N)))) in - let mop := make_mod_op op (ZnZ.of_Z N) in - if isM2 N then - match (4 * N) ?= (ZEll.Zmullp l - 1) ^ 2 with - Lt => - match y ^ 2 mod N ?= (x ^ 3 + A * x + B) mod N with - Eq => - let ex := mkEx N S l A B x y in - let a := ntriple (Z2z ex op x) (Z2z ex op y) (Z2z ex op 1) in - let A := (Z2z ex op A) in - let B := (Z2z ex op B) in - let d4 := (Z2z ex op 4) in - let d27 := (Z2z ex op 27) in - let da := mop.(add_mod) in - let dm := mop.(mul_mod) in - let isc := (da (dm (dm (dm d4 A) A) A) (dm (dm d27 B) B)) in - let (a1, sc1) := scal ex op mop isc a S in - let (S1,R1) := ZEll.psplit l in - let (a2, sc2) := scal ex op mop sc1 a1 S1 in - let (a3, sc3) := scalL ex op mop sc2 a2 R1 in - match a3 with - nzero => if (Zeq_bool (Zgcd (z2Z op sc3) N) 1) then true - else false - | _ => false - end - | _ => false - end - | _ => false - end - else false. - -Lemma Zcompare_correct: forall x y, - match x ?= y with Eq => x = y | Gt => x > y | Lt => x < y end. -Proof. -intros x y; unfold Zlt, Zgt; generalize (Zcompare_Eq_eq x y); case Zcompare; auto. -Qed. - -Lemma ell_test_correct: forall (N S: positive) (l: List.list (positive * positive)) - (A B x y: Z), - (forall p, List.In p l -> prime (fst p)) -> - if ell_test N S l A B x y then prime N else True. -intros N S1 l A1 B1 x y H; unfold ell_test. -generalize (isM2_correct N); case isM2; auto. -intros (H1, H2). -match goal with |- context[?x ?= ?y] => - generalize (Zcompare_correct x y); case Zcompare; auto -end; intros H3. -match goal with |- context[?x ?= ?y] => - generalize (Zcompare_correct x y); case Zcompare; auto -end; intros H4. -set (n := Peano.pred (nat_of_P (get_height 31 (plength N)))). -set (op := cmk_op n). -set (mop := make_mod_op op (ZnZ.of_Z N)). -set (exx := mkEx N S1 l A1 B1 x y). -set (op_spec := cmk_spec n). -assert (exxs: ex_spec exx). - constructor; auto. -assert (H0: N < base (ZnZ.digits op)). - apply Zlt_le_trans with (1 := plength_correct N). - unfold op, base. - rewrite cmk_op_digits. - apply Zpower_le_monotone; split; auto with zarith. - generalize (get_height_correct 31 (plength N)); unfold n. - set (p := plength N). - replace (Z_of_nat (Peano.pred (nat_of_P (get_height 31 p)))) with - ((Zpos (get_height 31 p) - 1) ); auto with zarith. - rewrite pred_of_minus; rewrite inj_minus1; auto with zarith. - rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto with zarith. - generalize (lt_O_nat_of_P (get_height 31 p)); auto with zarith. -assert (mspec: mod_spec op (zN exx op) mop). - unfold mop; apply make_mod_spec; auto. - rewrite ZnZ.of_Z_correct; auto with zarith. -generalize (@scalL_prime exx exxs _ op (cmk_spec n) mop mspec H0). -lazy zeta. -unfold c1, A, B, nplus, nmul; - simpl exx.(vA); simpl exx.(vB); simpl exx.(vx); simpl exx.(vy); - simpl exx.(vS); simpl exx.(vR); simpl exx.(vN). -case scal; intros a1 sc1. -case ZEll.psplit; intros S2 R2. -case scal; intros a2 sc2. -case scalL; intros a3 sc3. -case a3; auto. -case Zeq_bool; auto. -Qed. - -Time Eval vm_compute in (ell_test - 329719147332060395689499 - 8209062 - (List.cons (40165264598163841%positive,1%positive) List.nil) - (-94080) - 9834496 - 0 - 3136). - - -Time Eval vm_compute in (ell_test - 1384435372850622112932804334308326689651568940268408537 - 13077052794 - (List.cons (105867537178241517538435987563198410444088809%positive, 1%positive) List.nil) - (-677530058123796416781392907869501000001421915645008494) - 0 - (-169382514530949104195348226967375250000355478911252124) - 1045670343788723904542107880373576189650857982445904291 -). diff --git a/coqprime/num/Pock.v b/coqprime/num/Pock.v deleted file mode 100644 index 3b467af5a..000000000 --- a/coqprime/num/Pock.v +++ /dev/null @@ -1,964 +0,0 @@ - -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) - -Require Import List. -Require Import ZArith. -Require Import Zorder. -Require Import ZCAux. -Require Import LucasLehmer. -Require Import Pocklington. -Require Import ZArith Znumtheory Zpow_facts. -Require Import CyclicAxioms DoubleCyclic BigN Cyclic31 Int31. -Require Import Pmod. -Require Import Mod_op. -Require Import W. -Require Import Lucas. -Require Export PocklingtonCertificat. -Require Import NEll. -Import CyclicAxioms DoubleType DoubleBase List. - -Open Scope Z_scope. - -Section test. - -Variable w: Type. -Variable w_op: ZnZ.Ops w. -Variable op_spec: ZnZ.Specs w_op. -Variable p: positive. -Variable b: w. - -Notation "[| x |]" := - (ZnZ.to_Z x) (at level 0, x at level 99). - -Hypothesis b_pos: 0 < [|b|]. - -Variable m_op: mod_op w. -Variable m_op_spec: mod_spec w_op b m_op. - -Open Scope positive_scope. -Open Scope P_scope. - -Let pow := m_op.(power_mod). -Let times := m_op.(mul_mod). -Let pred:= m_op.(pred_mod). - -(* [fold_pow_mod a [q1,_;...;qn,_]] b = a ^(q1*...*qn) mod b *) -(* invariant a mod N = a *) -Definition fold_pow_mod (a: w) l := - fold_left - (fun a' (qp:positive*positive) => pow a' (fst qp)) - l a. - -Lemma fold_pow_mod_spec : forall l (a:w), - ([|a|] < [|b|])%Z -> [|fold_pow_mod a l|] = ([|a|]^(mkProd' l) mod [|b|])%Z. -intros l; unfold fold_pow_mod; elim l; simpl fold_left; simpl mkProd'; auto; clear l. -intros a H; rewrite Zpower_1_r; rewrite Zmod_small; auto with zarith. -case (ZnZ.spec_to_Z a); auto with zarith. -intros (p1, q1) l Rec a H. -case (ZnZ.spec_to_Z a); auto with zarith; intros U1 U2. -rewrite Rec. -rewrite m_op_spec.(power_mod_spec) with (t := [|a|]); auto with zarith. -rewrite <- Zpower_mod. -rewrite times_Zmult; rewrite Zpower_mult; auto with zarith. -apply Zle_lt_trans with (2 := H); auto with zarith. -rewrite Zmod_small; auto with zarith. -rewrite m_op_spec.(power_mod_spec) with (t := [|a|]); auto with zarith. -match goal with |- context[(?X mod ?Y)%Z] => - case (Z_mod_lt X Y); auto with zarith -end. -rewrite Zmod_small; auto with zarith. -Qed. - - -Fixpoint all_pow_mod (prod a: w) (l:dec_prime) {struct l}: w*w := - match l with - | nil => (prod,a) - | (q,_) :: l => - let m := pred (fold_pow_mod a l) in - all_pow_mod (times prod m) (pow a q) l - end. - - -Lemma snd_all_pow_mod : - forall l (prod a :w), ([|a|] < [|b|])%Z -> - [|snd (all_pow_mod prod a l)|] = ([|a|]^(mkProd' l) mod [|b|])%Z. -intros l; elim l; simpl all_pow_mod; simpl mkProd'; simpl snd; clear l. -intros _ a H; rewrite Zpower_1_r; auto with zarith. -rewrite Zmod_small; auto with zarith. -case (ZnZ.spec_to_Z a); auto with zarith. -intros (p1, q1) l Rec prod a H. -case (ZnZ.spec_to_Z a); auto with zarith; intros U1 U2. -rewrite Rec; auto with zarith. -rewrite m_op_spec.(power_mod_spec) with (t := [|a|]); auto with zarith. -rewrite <- Zpower_mod. -rewrite times_Zmult; rewrite Zpower_mult; auto with zarith. -apply Zle_lt_trans with (2 := H); auto with zarith. -rewrite Zmod_small; auto with zarith. -rewrite m_op_spec.(power_mod_spec) with (t := [|a|]); auto with zarith. -match goal with |- context[(?X mod ?Y)%Z] => - case (Z_mod_lt X Y); auto with zarith -end. -rewrite Zmod_small; auto with zarith. -Qed. - -Lemma fold_aux : forall a N l prod, - (fold_left - (fun (r : Z) (k : positive * positive) => - r * (a ^(N / fst k) - 1) mod [|b|]) l (prod mod [|b|]) mod [|b|] = - fold_left - (fun (r : Z) (k : positive * positive) => - r * (a^(N / fst k) - 1)) l prod mod [|b|])%Z. -induction l;simpl;intros. -rewrite Zmod_mod; auto with zarith. -rewrite <- IHl; auto with zarith. -rewrite Zmult_mod; auto with zarith. -rewrite Zmod_mod; auto with zarith. -rewrite <- Zmult_mod; auto with zarith. -Qed. - -Lemma fst_all_pow_mod : - forall l (a:w) (R:positive) (prod A :w), - [|prod|] = ([|prod|] mod [|b|])%Z -> - [|A|] = ([|a|]^R mod [|b|])%Z -> - [|fst (all_pow_mod prod A l)|] = - ((fold_left - (fun r (k:positive*positive) => - (r * ([|a|] ^ (R* mkProd' l / (fst k)) - 1))) l [|prod|]) mod [|b|])%Z. -intros l; elim l; simpl all_pow_mod; simpl fold_left; simpl fst; - auto with zarith; clear l. -intros (p1,q1) l Rec; simpl fst. -intros a R prod A H1 H2. -assert (F: (0 <= [|A|] < [|b|])%Z). -rewrite H2. -match goal with |- context[(?X mod ?Y)%Z] => - case (Z_mod_lt X Y); auto with zarith -end. -assert (F1: ((fun x => x = x mod [|b|])%Z [|fold_pow_mod A l|])). -rewrite Zmod_small; auto. -rewrite fold_pow_mod_spec; auto with zarith. -match goal with |- context[(?X mod ?Y)%Z] => - case (Z_mod_lt X Y); auto with zarith -end. -assert (F2: ((fun x => x = x mod [|b|])%Z [|pred (fold_pow_mod A l)|])). -rewrite Zmod_small; auto. -rewrite(fun x => m_op_spec.(pred_mod_spec) x [|x|]); - auto with zarith. -match goal with |- context[(?X mod ?Y)%Z] => - case (Z_mod_lt X Y); auto with zarith -end. -rewrite (Rec a (R * p1)%positive); auto with zarith. -rewrite(fun x y => m_op_spec.(mul_mod_spec) x y [|x|] [|y|]); - auto with zarith. -rewrite(fun x => m_op_spec.(pred_mod_spec) x [|x|]); - auto with zarith. -rewrite fold_pow_mod_spec; auto with zarith. -rewrite H2. -repeat rewrite Zpos_mult. -repeat rewrite times_Zmult. -repeat rewrite <- Zmult_assoc. -apply sym_equal; rewrite <- fold_aux; auto with zarith. -apply sym_equal; rewrite <- fold_aux; auto with zarith. -eq_tac; auto. -match goal with |- context[fold_left ?x _ _] => - apply f_equal2 with (f := fold_left x); auto with zarith -end. -rewrite Zmod_mod; auto with zarith. -rewrite (Zmult_comm R); repeat rewrite <- Zmult_assoc; - rewrite (Zmult_comm p1); rewrite Z_div_mult; auto with zarith. -repeat rewrite (Zmult_mod [|prod|]);auto with zmisc. -eq_tac; [idtac | eq_tac]; auto. -eq_tac; auto. -rewrite Zmod_mod; auto. -repeat rewrite (fun x => Zminus_mod x 1); auto with zarith. -eq_tac; auto; eq_tac; auto. -rewrite Zmult_comm; rewrite <- Zpower_mod; auto with zmisc. -rewrite Zpower_mult; auto with zarith. -rewrite Zmod_mod; auto with zarith. -rewrite Zmod_small; auto. -rewrite(fun x y => m_op_spec.(mul_mod_spec) x y [|x|] [|y|]); - auto with zarith. -match goal with |- context[(?X mod ?Y)%Z] => - case (Z_mod_lt X Y); auto with zarith -end. -rewrite(fun x => m_op_spec.(power_mod_spec) x [|x|]); - auto with zarith. -apply trans_equal with ([|A|] ^ p1 mod [|b|])%Z; auto. -rewrite H2. -rewrite Zpos_mult_morphism; rewrite Zpower_mult; auto with zarith. -rewrite <- Zpower_mod; auto with zarith. -rewrite Zmod_small; auto. -Qed. - - -Fixpoint pow_mod_pred (a:w) (l:dec_prime) {struct l} : w := - match l with - | nil => a - | (q, p)::l => - if (p ?= 1) then pow_mod_pred a l - else - let a' := iter_pos (Ppred p) _ (fun x => pow x q) a in - pow_mod_pred a' l - end. - -Lemma iter_pow_mod_spec : forall q p a, [|a|] = ([|a|] mod [|b|])%Z -> - ([|iter_pos p _ (fun x => pow x q) a|] = [|a|]^q^p mod [|b|])%Z. -intros q1 p1; elim p1; simpl iter_pos; clear p1. -intros p1 Rec a Ha. -rewrite(fun x => m_op_spec.(power_mod_spec) x [|x|]); - auto with zarith. -repeat rewrite Rec; auto with zarith. -match goal with |- (Zpower_pos ?X ?Y mod ?Z = _)%Z => - apply trans_equal with (X ^ Y mod Z)%Z; auto -end. -repeat rewrite <- Zpower_mod; auto with zmisc. -repeat rewrite <- Zpower_mult; auto with zmisc. -repeat rewrite <- Zpower_mod; auto with zmisc. -repeat rewrite <- Zpower_mult; auto with zarith zmisc. -eq_tac; auto. -eq_tac; auto. -rewrite Zpos_xI. -assert (tmp: forall x, (2 * x = x + x)%Z); auto with zarith; rewrite tmp; - clear tmp. -repeat rewrite Zpower_exp; auto with zarith. -rewrite Zpower_1_r; try ring; auto with misc. -rewrite Zmod_mod; auto with zarith. -rewrite Rec; auto with zmisc. -rewrite Zmod_mod; auto with zarith. -rewrite Rec; auto with zmisc. -rewrite Zmod_mod; auto with zarith. -intros p1 Rec a Ha. -repeat rewrite Rec; auto with zarith. -repeat rewrite <- Zpower_mod; auto with zmisc. -repeat rewrite <- Zpower_mult; auto with zmisc. -eq_tac; auto. -eq_tac; auto. -rewrite Zpos_xO. -assert (tmp: forall x, (2 * x = x + x)%Z); auto with zarith; rewrite tmp; - clear tmp. -repeat rewrite Zpower_exp; auto with zarith. -rewrite Zmod_mod; auto with zarith. -intros a Ha; rewrite Zpower_1_r; auto with zarith. -rewrite(fun x => m_op_spec.(power_mod_spec) x [|x|]); - auto with zarith. -Qed. - -Lemma pow_mod_pred_spec : forall l a, - ([|a|] = [|a|] mod [|b|] -> - [|pow_mod_pred a l|] = [|a|]^(mkProd_pred l) mod [|b|])%Z. -intros l; elim l; simpl pow_mod_pred; simpl mkProd_pred; clear l. -intros; rewrite Zpower_1_r; auto with zarith. -intros (p1,q1) l Rec a H; simpl snd; simpl fst. -case (q1 ?= 1)%P; auto with zarith. -rewrite Rec; auto. -rewrite iter_pow_mod_spec; auto with zarith. -rewrite times_Zmult; rewrite pow_Zpower. -rewrite <- Zpower_mod; auto with zarith. -rewrite Zpower_mult; auto with zarith. -rewrite Zmod_small; auto with zarith. -rewrite iter_pow_mod_spec; auto with zarith. -match goal with |- context[(?X mod ?Y)%Z] => - case (Z_mod_lt X Y); auto with zarith -end. -Qed. - -End test. - -Require Import Bits. - -Definition test_pock N a dec sqrt := - if (2 ?< N) then - let Nm1 := Ppred N in - let F1 := mkProd dec in - match (Nm1 / F1)%P with - | (Npos R1, N0) => - if is_odd R1 then - if is_even F1 then - if (1 ?< a) then - let (s,r') := (R1 / (xO F1))%P in - match r' with - | Npos r => - if (a ?< N) then - let op := cmk_op (Peano.pred (nat_of_P (get_height 31 (plength N)))) in - let wN := znz_of_Z op (Zpos N) in - let wa := znz_of_Z op (Zpos a) in - let w1 := znz_of_Z op 1 in - let mod_op := make_mod_op op wN in - let pow := mod_op.(power_mod) in - let ttimes := mod_op.(mul_mod) in - let pred:= mod_op.(pred_mod) in - let gcd:= ZnZ.gcd in - let A := pow_mod_pred _ mod_op (pow wa R1) dec in - match all_pow_mod _ mod_op w1 A dec with - | (p, aNm1) => - match ZnZ.to_Z aNm1 with - (Zpos xH) => - match ZnZ.to_Z (gcd p wN) with - (Zpos xH) => - if check_s_r s r sqrt then - (N ?< (times ((times ((xO F1)+r+1) F1) + r) F1) + 1) - else false - | _ => false - end - | _ => false - end - end else false - | _ => false - end - else false - else false - else false - | _=> false - end - else false. - -Lemma test_pock_correct : forall N a dec sqrt, - (forall k, In k dec -> prime (Zpos (fst k))) -> - test_pock N a dec sqrt = true -> - prime N. -unfold test_pock;intros N a dec sqrt H. -match goal with |- context[if ?x then _ else _] => - case_eq x; intros If1; auto -end. -2: intros; discriminate. -match goal with H: (?X ?< ?Y) = true |- _ => - generalize (is_lt_spec X Y); rewrite H; clear H; intros H -end. -generalize (div_eucl_spec (Ppred N) (mkProd dec)); - destruct ((Ppred N) / (mkProd dec))%P as (R1,n). -simpl fst; simpl snd; intros (H1, H2). -destruct R1 as [ |R1]. -intros; discriminate. -destruct n. -2: intros; discriminate. -match goal with |- context[if ?x then _ else _] => - case_eq x; intros If2; auto -end. -assert (If0: Zodd R1). -apply is_odd_Zodd; auto. -clear If2; rename If0 into If2. -2: intros; discriminate. -match goal with |- context[if ?x then _ else _] => - case_eq x; intros If3; auto -end. -assert (If0: Zeven (mkProd dec)). -apply is_even_Zeven; auto. -clear If3; rename If0 into If3. -2: intros; discriminate. -match goal with |- context[if ?x then _ else _] => - case_eq x; intros If4; auto -end. -match goal with H: (?X ?< ?Y) = true |- _ => - generalize (is_lt_spec X Y); rewrite H; clear H; intros H -end. -2: intros; discriminate. -generalize (div_eucl_spec R1 (xO (mkProd dec))); - destruct ((R1 / xO (mkProd dec))%P) as (s,r'); simpl fst; - simpl snd; intros (H3, H4). -destruct r' as [ |r]. -intros; discriminate. -match goal with |- context[if ?x then _ else _] => - case_eq x; intros If5; auto -end. -match goal with H: (?X ?< ?Y) = true |- _ => - generalize (is_lt_spec X Y); rewrite H; clear H; intros H -end. -2: intros; discriminate. -set (bb := Peano.pred (nat_of_P (get_height 31 (plength N)))). -set (w_op := cmk_op bb). -assert (op_spec: ZnZ.Specs w_op). -unfold bb, w_op; apply cmk_spec; auto. -assert (F0: N < DoubleType.base (ZnZ.digits w_op)). - apply Zlt_le_trans with (1 := plength_correct N). - unfold w_op, DoubleType.base. - rewrite cmk_op_digits. - apply Zpower_le_monotone; split; auto with zarith. - generalize (get_height_correct 31 (plength N)); unfold bb. - set (p := plength N). - replace (Z_of_nat (Peano.pred (nat_of_P (get_height 31 p)))) with - ((Zpos (get_height 31 p) - 1) ); auto with zarith. - rewrite pred_of_minus; rewrite inj_minus1; auto with zarith. - rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto with zarith. - generalize (lt_O_nat_of_P (get_height 31 p)); auto with zarith. -assert (F1: ZnZ.to_Z (ZnZ.of_Z N) = N). -rewrite ZnZ.of_Z_correct; auto with zarith. -assert (F2: 1 < ZnZ.to_Z (ZnZ.of_Z N)). -rewrite F1; auto with zarith. -assert (F3: 0 < ZnZ.to_Z (ZnZ.of_Z N)); auto with zarith. -assert (F4: ZnZ.to_Z (ZnZ.of_Z a) = a). -rewrite ZnZ.of_Z_correct; auto with zarith. -assert (F5: ZnZ.to_Z (ZnZ.of_Z 1) = 1). -rewrite ZnZ.of_Z_correct; auto with zarith. -assert (F6: N - 1 = (R1 * mkProd_pred dec)%positive * mkProd' dec). -rewrite Zpos_mult. -rewrite <- Zmult_assoc; rewrite mkProd_pred_mkProd; auto with zarith. -simpl in H1; rewrite Zpos_mult in H1; rewrite <- H1; rewrite Ppred_Zminus; - auto with zarith. -assert (m_spec: mod_spec w_op (znz_of_Z w_op N) - (make_mod_op w_op (znz_of_Z w_op N))). -apply make_mod_spec; auto with zarith. -match goal with |- context[all_pow_mod ?x ?y ?z ?t ?u] => - generalize (fst_all_pow_mod x w_op op_spec _ F3 _ m_spec - u (znz_of_Z w_op a) (R1*mkProd_pred dec) z t); - generalize (snd_all_pow_mod x w_op op_spec _ F3 _ m_spec u z t); - fold bb w_op; - case (all_pow_mod x y z t u); simpl fst; simpl snd -end. -intros prod aNm1; intros H5 H6. -case_eq (ZnZ.to_Z aNm1). -intros; discriminate. -2: intros; discriminate. -intros p; case p; clear p. -intros; discriminate. -intros; discriminate. -intros If6. -case_eq (ZnZ.to_Z (ZnZ.gcd prod (znz_of_Z w_op N))). -intros; discriminate. -2: intros; discriminate. -intros p; case p; clear p. -intros; discriminate. -intros; discriminate. -intros If7. -match goal with |- context[if ?x then _ else _] => - case_eq x; intros If8; auto -end. -2: intros; discriminate. -intros If9. -match goal with H: (?X ?< ?Y) = true |- _ => - generalize (is_lt_spec X Y); rewrite H; clear H; intros H -end. -assert (U1: N - 1 = mkProd dec * R1). -rewrite <- Ppred_Zminus in H1; auto with zarith. -rewrite H1; simpl. -repeat rewrite Zpos_mult; auto with zarith. -assert (HH:Z_of_N s = R1 / (2 * mkProd dec) /\ Zpos r = R1 mod (2 * mkProd dec)). -apply mod_unique with (2 * mkProd dec);auto with zarith. -apply Z_mod_lt; auto with zarith. -rewrite <- Z_div_mod_eq; auto with zarith. -rewrite H3. -rewrite (Zpos_xO (mkProd dec)). -simpl Z_of_N; ring. -case HH; clear HH; intros HH1 HH2. -apply PocklingtonExtra with (F1:=mkProd dec) (R1:=R1) (m:=1); - auto with zmisc zarith. -case (Zle_lt_or_eq 1 (mkProd dec)); auto with zarith. -simpl in H2; auto with zarith. -intros HH; contradict If3; rewrite <- HH. -apply Zodd_not_Zeven; red; auto. -intros p; case p; clear p. -intros HH; contradict HH. -apply not_prime_0. -2: intros p (V1, _); contradict V1; apply Zle_not_lt; red; simpl; intros; - discriminate. -intros p Hprime Hdec; exists (Zpos a);repeat split; auto with zarith. -apply trans_equal with (2 := If6). -rewrite H5. -rewrite pow_mod_pred_spec with (2 := m_spec); auto with zarith. -rewrite F1. -rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith. -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -rewrite F1; rewrite F4. -rewrite <- Zpower_mod; auto with zarith. -rewrite <- Zpower_mult; auto with zarith. -rewrite mkProd_pred_mkProd; auto with zarith. -rewrite U1; rewrite Zmult_comm. -rewrite Zpower_mult; auto with zarith. -rewrite <- Zpower_mod; auto with zarith. -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -rewrite F1; rewrite F4; rewrite Zmod_small; auto with zarith. -rewrite Zmod_small; auto with zarith. -rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith. -match goal with |- context[?X mod ?Y] => - case (Z_mod_lt X Y); auto with zarith -end. -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -rewrite F1; rewrite F4; rewrite Zmod_small; auto with zarith. -rewrite pow_mod_pred_spec with (2 := m_spec); auto with zarith. -match goal with |- context[?X mod ?Y] => - case (Z_mod_lt X Y); auto with zarith -end. -rewrite Zmod_small; auto with zarith. -rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith. -match goal with |- context[?X mod ?Y] => - case (Z_mod_lt X Y); auto with zarith -end. -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -rewrite F1; rewrite F4; rewrite Zmod_small; auto with zarith. -match type of H6 with _ -> _ -> ?X => - assert (tmp: X); [apply H6 | clear H6; rename tmp into H6]; - auto with zarith -end. -rewrite F1. -change (znz_of_Z w_op 1) with (ZnZ.of_Z 1). -rewrite F5; rewrite Zmod_small; auto with zarith. -rewrite pow_mod_pred_spec with (2 := m_spec); auto with zarith. -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -repeat (rewrite F1 || rewrite F4). -rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith. -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -repeat (rewrite F1 || rewrite F4). -rewrite Zpos_mult; rewrite <- Zpower_mod; auto with zarith. -rewrite Zpower_mult; auto with zarith. -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -repeat (rewrite F1 || rewrite F4). -rewrite Zmod_small; auto with zarith. -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -repeat (rewrite F1 || rewrite F4). -rewrite Zmod_small; auto with zarith. -rewrite (power_mod_spec m_spec) with (t := a); auto with zarith. -match goal with |- context[?X mod ?Y] => - case (Z_mod_lt X Y); auto with zarith -end. -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -repeat (rewrite F1 || rewrite F4); auto. -rewrite Zmod_small; auto with zarith. -change (znz_of_Z w_op N) with (ZnZ.of_Z N); auto. -auto with zarith. -change (znz_of_Z w_op a) with (ZnZ.of_Z a) in H6. -change (znz_of_Z w_op N) with (ZnZ.of_Z N) in H6. -change (znz_of_Z w_op 1) with (ZnZ.of_Z 1) in H6. -rewrite F5 in H6; rewrite F1 in H6; rewrite F4 in H6. -case in_mkProd_prime_div_in with (3 := Hdec); auto. -intros p1 Hp1. -rewrite <- F6 in H6. -apply Zis_gcd_gcd; auto with zarith. -change (rel_prime (a ^ ((N - 1) / p) - 1) N). -match type of H6 with _ = ?X mod _ => - apply rel_prime_div with (p := X); auto with zarith -end. -apply rel_prime_mod_rev; auto with zarith. -red. -pattern 1 at 4; rewrite <- If7; rewrite <- H6. -pattern N at 2; rewrite <- F1. -apply ZnZ.spec_gcd; auto with zarith. -assert (foldtmp: forall (A B: Set) (f: A -> B -> A) (P: A -> Prop) l a b, - In b l -> (forall x, P (f x b)) -> - (forall x y, P x -> P (f x y)) -> - P (fold_left f l a)). -assert (foldtmp0: forall (A B: Set) (f: A -> B -> A) (P: A -> Prop) l a, - P a -> - (forall x y, P x -> P (f x y)) -> - P (fold_left f l a)). -intros A B f P l; elim l; simpl; auto. -intros A B f P l; elim l; simpl; auto. -intros a1 b HH; case HH. -intros a1 l1 Rec a2 b [V|V] V1 V2; subst; auto. -apply foldtmp0; auto. -apply Rec with (b := b); auto with zarith. -match goal with |- context [fold_left ?f _ _] => - apply (foldtmp _ _ f (fun k => Zdivide (a ^ ((N - 1) / p) - 1) k)) - with (b := (p, p1)); auto with zarith -end. -rewrite <- HH2. -clear F0; match goal with H: ?X < ?Y |- ?X < ?Z => - replace Z with Y; auto -end. -repeat (rewrite Zpos_plus || rewrite Zpos_mult || rewrite times_Zmult). -rewrite Zpos_xO; ring. -rewrite <- HH1; rewrite <- HH2. -apply check_s_r_correct with sqrt; auto. -Qed. - -(* Simple version of pocklington for primo *) -Definition test_spock N a dec := - if (2 ?< N) then - let Nm1 := Ppred N in - let F1 := mkProd dec in - match (Nm1 / F1)%P with - | (Npos R1, N0) => - if (1 ?< a) then - if (a ?< N) then - if (N ?< F1 * F1) then - let op := cmk_op (Peano.pred (nat_of_P (get_height 31 (plength N)))) in - let wN := znz_of_Z op (Zpos N) in - let wa := znz_of_Z op (Zpos a) in - let w1 := znz_of_Z op 1 in - let mod_op := make_mod_op op wN in - let pow := mod_op.(power_mod) in - let ttimes := mod_op.(mul_mod) in - let pred:= mod_op.(pred_mod) in - let gcd:= ZnZ.gcd in - let A := pow_mod_pred _ mod_op (pow wa R1) dec in - match all_pow_mod _ mod_op w1 A dec with - | (p, aNm1) => - match ZnZ.to_Z aNm1 with - (Zpos xH) => - match ZnZ.to_Z (gcd p wN) with - (Zpos xH) => true - | _ => false - end - | _ => false - end - end else false - else false - else false - | _=> false - end - else false. - -Lemma test_spock_correct : forall N a dec, - (forall k, In k dec -> prime (Zpos (fst k))) -> - test_spock N a dec = true -> - prime N. -unfold test_spock;intros N a dec H. -match goal with |- context[if ?x then _ else _] => - case_eq x; intros If1; auto -end. -2: intros; discriminate. -match goal with H: (?X ?< ?Y) = true |- _ => - generalize (is_lt_spec X Y); rewrite H; clear H; intros H -end. -generalize (div_eucl_spec (Ppred N) (mkProd dec)); - destruct ((Ppred N) / (mkProd dec))%P as (R1,n). -simpl fst; simpl snd; intros (H1, H2). -destruct R1 as [ |R1]. -intros; discriminate. -destruct n. -2: intros; discriminate. -match goal with |- context[if ?x then _ else _] => - case_eq x; intros If2; auto -end. -match goal with H: (?X ?< ?Y) = true |- _ => - generalize (is_lt_spec X Y); rewrite H; clear H; intros H -end. -2: intros; discriminate. -(* -set (bb := pred (nat_of_P (get_height 31 (plength N)))). -set (w_op := cmk_op bb). -assert (op_spec: znz_spec w_op). -unfold bb, w_op; apply cmk_spec; auto. -assert (F0: N < Basic_type.base (znz_digits w_op)). - apply Zlt_le_trans with (1 := plength_correct N). - unfold w_op, Basic_type.base. - rewrite cmk_op_digits. - apply Zpower_le_monotone; split; auto with zarith. - generalize (get_height_correct 31 (plength N)); unfold bb. - set (p := plength N). - replace (Z_of_nat (pred (nat_of_P (get_height 31 p)))) with - ((Zpos (get_height 31 p) - 1) ); auto with zarith. - rewrite pred_of_minus; rewrite inj_minus1; auto with zarith. - rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto with zarith. - generalize (lt_O_nat_of_P (get_height 31 p)); auto with zarith. -*) -set (bb := Peano.pred (nat_of_P (get_height 31 (plength N)))). -set (w_op := cmk_op bb). -assert (op_spec: ZnZ.Specs w_op). -unfold bb, w_op; apply cmk_spec; auto. -match goal with |- context[if ?x then _ else _] => - case_eq x; intros If3; auto -end. -match goal with H: (?X ?< ?Y) = true |- _ => - generalize (is_lt_spec X Y); rewrite H; clear H; intros H -end. -match goal with |- context[if ?x then _ else _] => - case_eq x; intros If4; auto -end. -match goal with H: (?X ?< ?Y) = true |- _ => - generalize (is_lt_spec X Y); rewrite H; clear H; intros H -end. -assert (F0: N < DoubleType.base (ZnZ.digits w_op)). - apply Zlt_le_trans with (1 := plength_correct N). - unfold w_op, DoubleType.base. - rewrite cmk_op_digits. - apply Zpower_le_monotone; split; auto with zarith. - generalize (get_height_correct 31 (plength N)); unfold bb. - set (p := plength N). - replace (Z_of_nat (Peano.pred (nat_of_P (get_height 31 p)))) with - ((Zpos (get_height 31 p) - 1) ); auto with zarith. - rewrite pred_of_minus; rewrite inj_minus1; auto with zarith. - rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto with zarith. - generalize (lt_O_nat_of_P (get_height 31 p)); auto with zarith. -assert (F1: ZnZ.to_Z (ZnZ.of_Z N) = N). -rewrite ZnZ.of_Z_correct; auto with zarith. -assert (F2: 1 < ZnZ.to_Z (ZnZ.of_Z N)). -rewrite F1; auto with zarith. -assert (F3: 0 < ZnZ.to_Z (ZnZ.of_Z N)); auto with zarith. -assert (F4: ZnZ.to_Z (ZnZ.of_Z a) = a). -rewrite ZnZ.of_Z_correct; auto with zarith. -assert (F5: ZnZ.to_Z (ZnZ.of_Z 1) = 1). -rewrite ZnZ.of_Z_correct; auto with zarith. -assert (F6: N - 1 = (R1 * mkProd_pred dec)%positive * mkProd' dec). -rewrite Zpos_mult. -rewrite <- Zmult_assoc; rewrite mkProd_pred_mkProd; auto with zarith. -simpl in H1; rewrite Zpos_mult in H1; rewrite <- H1; rewrite Ppred_Zminus; - auto with zarith. -assert (m_spec: mod_spec w_op (znz_of_Z w_op N) - (make_mod_op w_op (znz_of_Z w_op N))). -apply make_mod_spec; auto with zarith. -match goal with |- context[all_pow_mod ?x ?y ?z ?t ?u] => - generalize (fst_all_pow_mod x w_op op_spec _ F3 _ m_spec - u (znz_of_Z w_op a) (R1*mkProd_pred dec) z t); - generalize (snd_all_pow_mod x w_op op_spec _ F3 _ m_spec u z t); - fold bb w_op; - case (all_pow_mod x y z t u); simpl fst; simpl snd -end. -2: intros; discriminate. -intros prod aNm1; intros H5 H6. -case_eq (ZnZ.to_Z aNm1). -intros; discriminate. -2: intros; discriminate. -intros p; case p; clear p. -intros; discriminate. -intros; discriminate. -intros If5. -case_eq (ZnZ.to_Z (ZnZ.gcd prod (znz_of_Z w_op N))). -intros; discriminate. -2: intros; discriminate. -intros p; case p; clear p. -intros; discriminate. -intros; discriminate. -intros If6 _. -assert (U1: N - 1 = mkProd dec * R1). -rewrite <- Ppred_Zminus in H1; auto with zarith. -rewrite H1; simpl. -repeat rewrite Zpos_mult; auto with zarith. -apply PocklingtonCorollary1 with (F1:=mkProd dec) (R1:=R1); - auto with zmisc zarith. -case (Zle_lt_or_eq 1 (mkProd dec)); auto with zarith. -simpl in H2; auto with zarith. -intros HH; contradict If4; rewrite Zpos_mult_morphism; - rewrite <- HH. -apply Zle_not_lt; auto with zarith. -intros p; case p; clear p. -intros HH; contradict HH. -apply not_prime_0. -2: intros p (V1, _); contradict V1; apply Zle_not_lt; red; simpl; intros; - discriminate. -intros p Hprime Hdec; exists (Zpos a);repeat split; auto with zarith. -apply trans_equal with (2 := If5). -rewrite H5. -rewrite pow_mod_pred_spec with (2 := m_spec); auto with zarith. -rewrite F1. -rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith. -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -rewrite F1; rewrite F4. -rewrite <- Zpower_mod; auto with zarith. -rewrite <- Zpower_mult; auto with zarith. -rewrite mkProd_pred_mkProd; auto with zarith. -rewrite U1; rewrite Zmult_comm. -rewrite Zpower_mult; auto with zarith. -rewrite <- Zpower_mod; auto with zarith. -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -rewrite F1; rewrite F4; rewrite Zmod_small; auto with zarith. -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -rewrite Zmod_small; auto with zarith. -rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith. -match goal with |- context[?X mod ?Y] => - case (Z_mod_lt X Y); auto with zarith -end. -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -rewrite F1; rewrite F4; rewrite Zmod_small; auto with zarith. -rewrite pow_mod_pred_spec with (2 := m_spec); auto with zarith. -match goal with |- context[?X mod ?Y] => - case (Z_mod_lt X Y); auto with zarith -end. -rewrite Zmod_small; auto with zarith. -rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith. -match goal with |- context[?X mod ?Y] => - case (Z_mod_lt X Y); auto with zarith -end. -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -rewrite F1; rewrite F4; rewrite Zmod_small; auto with zarith. -match type of H6 with _ -> _ -> ?X => - assert (tmp: X); [apply H6 | clear H6; rename tmp into H6]; - auto with zarith -end. -rewrite F1. -change (znz_of_Z w_op 1) with (ZnZ.of_Z 1). -rewrite F5; rewrite Zmod_small; auto with zarith. -rewrite pow_mod_pred_spec with (2 := m_spec); auto with zarith. -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -repeat (rewrite F1 || rewrite F4). -rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith. -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -repeat (rewrite F1 || rewrite F4). -rewrite Zpos_mult; rewrite <- Zpower_mod; auto with zarith. -rewrite Zpower_mult; auto with zarith. -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -repeat (rewrite F1 || rewrite F4). -rewrite Zmod_small; auto with zarith. -rewrite Zmod_small; auto with zarith. -rewrite m_spec.(power_mod_spec) with (t := a); auto with zarith. -match goal with |- context[?X mod ?Y] => - case (Z_mod_lt X Y); auto with zarith -end. -change (znz_of_Z w_op N) with (ZnZ.of_Z N). -change (znz_of_Z w_op a) with (ZnZ.of_Z a). -repeat (rewrite F1 || rewrite F4). -rewrite Zmod_small; auto with zarith. -change (znz_of_Z w_op N) with (ZnZ.of_Z N) in H6. -change (znz_of_Z w_op a) with (ZnZ.of_Z a) in H6. -change (znz_of_Z w_op 1) with (ZnZ.of_Z 1) in H6. -rewrite F5 in H6; rewrite F1 in H6; rewrite F4 in H6. -case in_mkProd_prime_div_in with (3 := Hdec); auto. -intros p1 Hp1. -rewrite <- F6 in H6. -apply Zis_gcd_gcd; auto with zarith. -change (rel_prime (a ^ ((N - 1) / p) - 1) N). -match type of H6 with _ = ?X mod _ => - apply rel_prime_div with (p := X); auto with zarith -end. -apply rel_prime_mod_rev; auto with zarith. -red. -pattern 1 at 4; rewrite <- If6; rewrite <- H6. -pattern N at 2; rewrite <- F1. -apply ZnZ.spec_gcd; auto with zarith. -assert (foldtmp: forall (A B: Set) (f: A -> B -> A) (P: A -> Prop) l a b, - In b l -> (forall x, P (f x b)) -> - (forall x y, P x -> P (f x y)) -> - P (fold_left f l a)). -assert (foldtmp0: forall (A B: Set) (f: A -> B -> A) (P: A -> Prop) l a, - P a -> - (forall x y, P x -> P (f x y)) -> - P (fold_left f l a)). -intros A B f P l; elim l; simpl; auto. -intros A B f P l; elim l; simpl; auto. -intros a1 b HH; case HH. -intros a1 l1 Rec a2 b [V|V] V1 V2; subst; auto. -apply foldtmp0; auto. -apply Rec with (b := b); auto with zarith. -match goal with |- context [fold_left ?f _ _] => - apply (foldtmp _ _ f (fun k => Zdivide (a ^ ((N - 1) / p) - 1) k)) - with (b := (p, p1)); auto with zarith -end. -intros; discriminate. -Qed. - -Fixpoint test_Certif (lc : Certif) : bool := - match lc with - | nil => true - | (Proof_certif _ _) :: lc => test_Certif lc - | (Lucas_certif n p) :: lc => - let xx := test_Certif lc in - if xx then - let yy := gt2 p in - if yy then - match p with - Zpos p1 => - let zz := Mp p in - match zz with - | Zpos n' => - if (n ?= n')%P then - let tt := lucas p1 in - match tt with - | Z0 => true - | _ => false - end - else false - | _ => false - end - | _ => false - end - else false - else false - | (Pock_certif n a dec sqrt) :: lc => - let xx := test_pock n a dec sqrt in - if xx then - let yy := all_in lc dec in - (if yy then test_Certif lc else false) - else false - | (SPock_certif n a dec) :: lc => - let xx :=test_spock n a dec in - if xx then - let yy := all_in lc dec in - (if yy then test_Certif lc else false) - else false - | (Ell_certif n ss l a b x y) :: lc => - let xx := ell_test n ss l a b x y in - if xx then - let yy := all_in lc l in - if yy then test_Certif lc else false - else false - end. - -Lemma test_Certif_In_Prime : - forall lc, test_Certif lc = true -> - forall c, In c lc -> prime (nprim c). -intros lc; elim lc; simpl; auto. -intros _ c H; case H. -intros a; case a; simpl; clear a lc. -intros N p l Rec H c [H1 | H1]; subst; auto with arith. -intros n p l; case (test_Certif l); auto with zarith. -2: intros; discriminate. -intros H H1 c [H2 | H2]; subst; auto with arith. -simpl nprim. -generalize H1; clear H1. -case_eq (gt2 p). -2: intros; discriminate. -case p; clear p; try (intros; discriminate; fail). -unfold gt2; intros p H1. -match goal with H: (?X ?< ?Y) = true |- _ => - generalize (is_lt_spec X Y); rewrite H; clear H; intros H -end. -unfold Mp; case_eq (2 ^ p -1); try (intros; discriminate; fail). -intros p1 Hp1. -case_eq (n ?= p1)%P; try rewrite <- Hp1. -2: intros; discriminate. -intros H2. -match goal with H: (?X ?= ?Y)%P = true |- _ => - generalize (is_eq_eq _ _ H); clear H; intros H -end. -generalize (lucas_prime H1); rewrite Hp1; rewrite <- H2. -case (lucas p); try (intros; discriminate; fail); auto. -intros N a d p l H. -generalize (test_pock_correct N a d p). -case (test_pock N a d p); auto. -2: intros; discriminate. -generalize (all_in_In l d). -case (all_in l d). -2: intros; discriminate. -intros H1 H2 H3 c [H4 | H4]; subst; simpl; auto. -apply H2; auto. -intros k Hk. -case H1 with (2 := Hk); auto. -intros x (Hx1, Hx2); rewrite Hx2; auto. -intros N a d l H. -generalize (test_spock_correct N a d). -case test_spock; auto. -2: intros; discriminate. -generalize (all_in_In l d). -case (all_in l d). -2: intros; discriminate. -intros H1 H2 H3 c [H4 | H4]; subst; simpl; auto. -apply H2; auto. -intros k Hk. -case H1 with (2 := Hk); auto. -intros x (Hx1, Hx2); rewrite Hx2; auto. -intros N S l A B x y l1. -generalize (all_in_In l1 l). -generalize (ell_test_correct N S l A B x y). -case ell_test. -case all_in; auto. -intros H1 H2 H3 H4 c [H5 | H5]; try subst c; simpl; auto. -apply H1. -intros p Hp; case (H2 (refl_equal true) p); auto. -intros x1 (Hx1, Hx2); rewrite Hx2; auto. -intros; discriminate. -intros; discriminate. -Qed. - -Lemma Pocklington_refl : - forall c lc, test_Certif (c::lc) = true -> prime (nprim c). -Proof. - intros c lc Heq;apply test_Certif_In_Prime with (c::lc);trivial;simpl;auto. -Qed. - diff --git a/coqprime/num/W.v b/coqprime/num/W.v deleted file mode 100644 index d26e2657e..000000000 --- a/coqprime/num/W.v +++ /dev/null @@ -1,200 +0,0 @@ - -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) - -Set Implicit Arguments. -Require Import CyclicAxioms DoubleCyclic BigN Cyclic31 Int31. -Require Import ZArith ZCAux. - -(* ** Type of words ** *) - - -(* Make the words *) - -Definition mk_word: forall (w: Type) (n:nat), Type. -fix 2. -intros w n; case n; simpl. -exact int31. -intros n1; exact (zn2z (mk_word w n1)). -Defined. - -(* Make the op *) -Fixpoint mk_op (w : Type) (op : ZnZ.Ops w) (n : nat) {struct n} : - ZnZ.Ops (word w n) := - match n return (ZnZ.Ops (word w n)) with - | O => op - | S n1 => mk_zn2z_ops_karatsuba (mk_op op n1) - end. - -Theorem mk_op_digits: forall w (op: ZnZ.Ops w) n, - (Zpos (ZnZ.digits (mk_op op n)) = 2 ^ Z_of_nat n * Zpos (ZnZ.digits op))%Z. -intros w op n; elim n; simpl mk_op; auto; clear n. -intros n Rec; simpl ZnZ.digits. -rewrite Zpos_xO; rewrite Rec. -rewrite Zmult_assoc; apply f_equal2 with (f := Zmult); auto. -rewrite inj_S; unfold Zsucc; rewrite Zplus_comm. -rewrite Zpower_exp; auto with zarith. -Qed. - -Theorem digits_pos: forall w (op: ZnZ.Ops w) n, - (1 < Zpos (ZnZ.digits op) -> 1 < Zpos (ZnZ.digits (mk_op op n)))%Z. -intros w op n H. -rewrite mk_op_digits. -rewrite <- (Zmult_1_r 1). -apply Zle_lt_trans with (2 ^ (Z_of_nat n) * 1)%Z. -apply Zmult_le_compat_r; auto with zarith. -rewrite <- (Zpower_0_r 2). -apply Zpower_le_monotone; auto with zarith. -apply Zmult_lt_compat_l; auto with zarith. -Qed. - -Fixpoint mk_spec (w : Type) (op : ZnZ.Ops w) (op_spec : ZnZ.Specs op) - (H: (1 < Zpos (ZnZ.digits op))%Z) (n : nat) - {struct n} : ZnZ.Specs (mk_op op n) := - match n return (ZnZ.Specs (mk_op op n)) with - | O => op_spec - | S n1 => - @mk_zn2z_specs_karatsuba (word w n1) (mk_op op n1) - (* (digits_pos op n1 H) *) (mk_spec op_spec H n1) - end. - -(* ** Operators ** *) -Definition w31_1_op := mk_zn2z_ops int31_ops. -Definition w31_2_op := mk_zn2z_ops w31_1_op. -Definition w31_3_op := mk_zn2z_ops w31_2_op. -Definition w31_4_op := mk_zn2z_ops_karatsuba w31_3_op. -Definition w31_5_op := mk_zn2z_ops_karatsuba w31_4_op. -Definition w31_6_op := mk_zn2z_ops_karatsuba w31_5_op. -Definition w31_7_op := mk_zn2z_ops_karatsuba w31_6_op. -Definition w31_8_op := mk_zn2z_ops_karatsuba w31_7_op. -Definition w31_9_op := mk_zn2z_ops_karatsuba w31_8_op. -Definition w31_10_op := mk_zn2z_ops_karatsuba w31_9_op. -Definition w31_11_op := mk_zn2z_ops_karatsuba w31_10_op. -Definition w31_12_op := mk_zn2z_ops_karatsuba w31_11_op. -Definition w31_13_op := mk_zn2z_ops_karatsuba w31_12_op. -Definition w31_14_op := mk_zn2z_ops_karatsuba w31_13_op. - -Definition cmk_op: forall (n: nat), ZnZ.Ops (word int31 n). -intros n; case n; clear n. -exact int31_ops. -intros n; case n; clear n. -exact w31_1_op. -intros n; case n; clear n. -exact w31_2_op. -intros n; case n; clear n. -exact w31_3_op. -intros n; case n; clear n. -exact w31_4_op. -intros n; case n; clear n. -exact w31_5_op. -intros n; case n; clear n. -exact w31_6_op. -intros n; case n; clear n. -exact w31_7_op. -intros n; case n; clear n. -exact w31_8_op. -intros n; case n; clear n. -exact w31_9_op. -intros n; case n; clear n. -exact w31_10_op. -intros n; case n; clear n. -exact w31_11_op. -intros n; case n; clear n. -exact w31_12_op. -intros n; case n; clear n. -exact w31_13_op. -intros n; case n; clear n. -exact w31_14_op. -intros n. -match goal with |- context[S ?X] => - exact (mk_op int31_ops (S X)) -end. -Defined. - -Definition cmk_spec: forall n, ZnZ.Specs (cmk_op n). -assert (S1: ZnZ.Specs w31_1_op). -unfold w31_1_op; apply mk_zn2z_specs; auto with zarith. -exact int31_specs. -assert (S2: ZnZ.Specs w31_2_op). -unfold w31_2_op; apply mk_zn2z_specs; auto with zarith. -assert (S3: ZnZ.Specs w31_3_op). -unfold w31_3_op; apply mk_zn2z_specs; auto with zarith. -assert (S4: ZnZ.Specs w31_4_op). -unfold w31_4_op; apply mk_zn2z_specs_karatsuba; auto with zarith. -assert (S5: ZnZ.Specs w31_5_op). -unfold w31_5_op; apply mk_zn2z_specs_karatsuba; auto with zarith. -assert (S6: ZnZ.Specs w31_6_op). -unfold w31_6_op; apply mk_zn2z_specs_karatsuba; auto with zarith. -assert (S7: ZnZ.Specs w31_7_op). -unfold w31_7_op; apply mk_zn2z_specs_karatsuba; auto with zarith. -assert (S8: ZnZ.Specs w31_8_op). -unfold w31_8_op; apply mk_zn2z_specs_karatsuba; auto with zarith. -assert (S9: ZnZ.Specs w31_9_op). -unfold w31_9_op; apply mk_zn2z_specs_karatsuba; auto with zarith. -assert (S10: ZnZ.Specs w31_10_op). -unfold w31_10_op; apply mk_zn2z_specs_karatsuba; auto with zarith. -assert (S11: ZnZ.Specs w31_11_op). -unfold w31_11_op; apply mk_zn2z_specs_karatsuba; auto with zarith. -assert (S12: ZnZ.Specs w31_12_op). -unfold w31_12_op; apply mk_zn2z_specs_karatsuba; auto with zarith. -assert (S13: ZnZ.Specs w31_13_op). -unfold w31_13_op; apply mk_zn2z_specs_karatsuba; auto with zarith. -assert (S14: ZnZ.Specs w31_14_op). -unfold w31_14_op; apply mk_zn2z_specs_karatsuba; auto with zarith. -intros n; case n; clear n. -exact int31_specs. -intros n; case n; clear n. -exact S1. -intros n; case n; clear n. -exact S2. -intros n; case n; clear n. -exact S3. -intros n; case n; clear n. -exact S4. -intros n; case n; clear n. -exact S5. -intros n; case n; clear n. -exact S6. -intros n; case n; clear n. -exact S7. -intros n; case n; clear n. -exact S8. -intros n; case n; clear n. -exact S9. -intros n; case n; clear n. -exact S10. -intros n; case n; clear n. -exact S11. -intros n; case n; clear n. -exact S12. -intros n; case n; clear n. -exact S13. -intros n; case n; clear n. -exact S14. -intro n. -simpl cmk_op. -repeat match goal with |- ZnZ.Specs - (mk_zn2z_ops_karatsuba ?X) => - generalize (@mk_zn2z_specs_karatsuba _ X); intros tmp; - apply tmp; clear tmp; auto with zarith -end. -(* -apply digits_pos. -*) -auto with zarith. -apply mk_spec. -exact int31_specs. -auto with zarith. -Defined. - - -Theorem cmk_op_digits: forall n, - (Zpos (ZnZ.digits (cmk_op n)) = 2 ^ (Z_of_nat n) * 31)%Z. -do 15 (intros n; case n; clear n; [try reflexivity | idtac]). -intros n; unfold cmk_op; lazy beta. -rewrite mk_op_digits; auto. -Qed. |