在Coq中证明质数

Question

我有一个Coq函数，可以对素数进行分类。我将它导出到Haskell并进行测试;它工作正常。我想严格证明它确实对素数进行了分类，所以我试图证明以下定理isPrimeCorrect：

(************)
(* helper'' *)
(************)
Fixpoint helper' (p m n : nat) : bool :=
  match m with
  | 0 => false
  | 1 => false
  | S m' => (orb ((mult m n) =? p) (helper' p m' n))
  end.

(**********)
(* helper *)
(**********)
Fixpoint helper (p m : nat) : bool :=
  match m with
  | 0 => false
  | S m' => (orb ((mult m m) =? p) (orb (helper' p m' m) (helper p m')))
  end.

(***********)
(* isPrime *)
(***********)
Fixpoint isPrime (p : nat) : bool :=
  match p with
  | 0 => false
  | 1 => false
  | S p' => (negb (helper p p'))
  end.

(***********)
(* divides *)
(***********)
Definition divides (n p : nat) : Prop :=
  exists (m : nat), ((mult m n) = p).

(*********)
(* prime *)
(*********)
Definition prime (p : nat) : Prop :=
  (p > 1) /\ (forall (n : nat), ((divides n p) -> ((n = 1) \/ (n = p)))).

(*****************************)
(* isPrime correctness proof *)
(*****************************)
Theorem isPrimeCorrect: forall (p : nat),
  ((isPrime p) = true) <-> (prime p).

今天我在这个定理上花了好几个小时没有实际进展。实际上，我有点惊讶，因为我以前设法证明了相似的东西。任何提示/线索如何进行？

Answer 1

您必须明确地为每个帮助函数编写引理，这些函数完全表明您认为此函数为您所做的事情。例如，我试图为你的helper'函数做这个，我想出了以下引理：

Require Import Arith Psatz.

(************)
(* helper'' *)
(************)
Fixpoint helper' (p m n : nat) : bool :=
  match m with
  | 0 => false
  | 1 => false
  | S m' => (orb ((mult m n) =? p) (helper' p m' n))
  end.


Lemma helper'_correct :
  forall p m n,
    helper' p m n = true <-> exists k, (1 < k <= m /\ p = k * n).
Proof.
intros p; induction m as [ | m' IH]; intros n.
  split;[discriminate | ].
  intros [k [abs _]].
  lia.  (* Here the hypothesis abs has statement  1 <= k < 0 
            and lia recognizes that it is absurd. *)
destruct m' as [ | m''] eqn: E.
  split;[discriminate | intros [k [abs _]]; lia].
change (helper' p (S (S m'')) n) with (orb ((mult (S (S m'')) n) =? p)
                                    (helper' p (S m'') n)).
rewrite Bool.orb_true_iff.
split.
  intros [it | later].
    now exists (S (S m'')); split;[lia | symmetry; apply beq_nat_true ].
  rewrite IH in later; destruct later as [k [k1 k2]].
  exists k.
  (* here hypothesis k1 states 1 < k <= S m''
                     k2 states p = k * n
     and we need to prove 1 < k <= S (S m'') /\ p = k * n
     lia can do that automatically. *)
  lia.
intros [k [[k1 km] k2]].
apply le_lt_or_eq in km; rewrite or_comm in km; destruct km as [km | km].
  now left; rewrite <- km; rewrite Nat.eqb_eq, k2.
right; apply lt_n_Sm_le in km.
change (helper' p (S m'') n = true); rewrite IH.
exists k.
lia.
Qed.

显然，还应该有一种方法将qazxsw poi函数与qazxsw poi谓词联系起来。