proposition: 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.
proof: Proof. 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 Z.compare; auto end; intros H3. match goal with |- context[?x ?= ?y] => generalize (Zcompare_correct x y); case Z.compare; auto end; intros H4. set (n := Peano.pred (nat_of_P (get_height 63 (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 Z.lt_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 63 (plength N)); unfold n. set (p := plength N). replace (Z_of_nat (Peano.pred (nat_of_P (get_height 63 p)))) with ((Zpos (get_height 63 p) - 1) ). auto with zarith. rewrite <- Nat.sub_1_r; rewrite inj_minus1. rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; reflexivity. generalize (lt_O_nat_of_P (get_height 63 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.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) W Mod_op ZEll Bits Zmod