From 8b3728b68ea21e0cfedfc4eff7fa15830e84bdf1 Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Wed, 20 Jan 2016 15:54:08 -0500 Subject: Import coqprime; use it to prove Euler's criterion. --- coqprime/num/Lucas.v | 213 +++++++++ coqprime/num/MEll.v | 1228 +++++++++++++++++++++++++++++++++++++++++++++++++ coqprime/num/Mod_op.v | 1200 +++++++++++++++++++++++++++++++++++++++++++++++ coqprime/num/NEll.v | 983 +++++++++++++++++++++++++++++++++++++++ coqprime/num/Pock.v | 964 ++++++++++++++++++++++++++++++++++++++ coqprime/num/W.v | 200 ++++++++ 6 files changed, 4788 insertions(+) create mode 100644 coqprime/num/Lucas.v create mode 100644 coqprime/num/MEll.v create mode 100644 coqprime/num/Mod_op.v create mode 100644 coqprime/num/NEll.v create mode 100644 coqprime/num/Pock.v create mode 100644 coqprime/num/W.v (limited to 'coqprime/num') diff --git a/coqprime/num/Lucas.v b/coqprime/num/Lucas.v new file mode 100644 index 000000000..f969dc106 --- /dev/null +++ b/coqprime/num/Lucas.v @@ -0,0 +1,213 @@ + +(*************************************************************) +(* 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 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 new file mode 100644 index 000000000..afcdf4146 --- /dev/null +++ b/coqprime/num/MEll.v @@ -0,0 +1,1228 @@ + +(*************************************************************) +(* 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 new file mode 100644 index 000000000..a8f25bd2d --- /dev/null +++ b/coqprime/num/Mod_op.v @@ -0,0 +1,1200 @@ + +(*************************************************************) +(* 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 new file mode 100644 index 000000000..28dd63181 --- /dev/null +++ b/coqprime/num/NEll.v @@ -0,0 +1,983 @@ + +(*************************************************************) +(* 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 new file mode 100644 index 000000000..3b467af5a --- /dev/null +++ b/coqprime/num/Pock.v @@ -0,0 +1,964 @@ + +(*************************************************************) +(* 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 new file mode 100644 index 000000000..d26e2657e --- /dev/null +++ b/coqprime/num/W.v @@ -0,0 +1,200 @@ + +(*************************************************************) +(* 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. -- cgit v1.2.3