(* reflection-primes.v *)
(* Przykłady zaczerpnięte z Coq'Art *)

Require Export Zdiv.
Check Zdiv_eucl.
Check Z_div_mod.
Check Zmod.

Axiom verify_divide : forall m p : nat, 0 < m -> 0 < p -> (exists q : nat, m = q * p) -> 
  Zmod (Z_of_nat m) (Z_of_nat p) = 0%Z.

Axiom divisor_smaller : forall m p : nat, 0 < m -> forall q : nat, m = q*p -> q <= m.

Fixpoint check_range (v : Z) (r : nat) (sr : Z) {struct r} : bool :=
  match r with
  | O => true
  | S r' => match (v mod sr)%Z with
                 | Z0 => false
                 | _ => check_range v r' (Zpred sr)
                 end
  end.

Definition check_primality (n : nat) :=
  check_range (Z_of_nat n) (pred (pred( n))) (Z_of_nat (pred n)).

(*
Time Eval compute in (check_primarility 2333).
Time Eval compute in (check_primarility 2300).
*)

Axiom check_range_correct :
  forall (v : Z) (r : nat) (rz : Z), 
  (0 < v)%Z -> Z_of_nat (S r) = rz -> check_range v r rz = true -> 
  ~(exists k : nat, k <= S r /\ k <> 1 /\ exists q : nat, Zabs_nat v = q*k).

Axiom check_correct : 
  forall p : nat, 0 < p -> check_primality p = true -> 
  ~(exists k : nat, k <> 1 /\ k <> p /\ exists q : nat, p = q * k).

(*
Theorem prime_2333 : 
  ~(exists k : nat, k <> 1 /\ k <> 2333 /\ exists q : nat, 2333 = q*k).
Time apply check_correct; auto with arith.
Time Qed.
*)

(* EOF *)