primes - 如何在 Coq 中使用 Znumtheory 证明一个数是素数

Question

我正在尝试使用 Znumtheory 库证明一个数是素数。

在 Znum 理论中，素数是根据相对素数定义的:

  Inductive prime (p:Z) : Prop :=
      prime_intro :
      1 < p -> (forall n:Z, 1 <= n < p -> rel_prime n p) -> prime p.

所以为了证明 3 是素数，我应该将 prime_intro 应用于目标。这是我的尝试:

Theorem prime3 : prime 3.
Proof.
    apply prime_intro.

  - omega.
  - intros. 
    unfold rel_prime. apply Zis_gcd_intro.
    + apply Z.divide_1_l.
    + apply Z.divide_1_l.
    + intros. Abort.

我不知道如何使用假设 H : 1 <= n < 3上面写着 n是 1或 2 .我可以破坏它，申请 lt_eq_cases并再次破坏它，但我会被无用的 1 < n 卡住在第一种情况下。

我没想到看起来这么简单的东西会遇到困难。

Answer 1

我有一个@larsr 证明的变体。

Require Import ZArith.
Require Import Znumtheory.
Require Import Omega.

Theorem prime3 : prime 3.
Proof.
  constructor.
  - omega.
  - intros.
    assert (n = 1 \/ n = 2) as Ha by omega.
    destruct Ha; subst n; apply Zgcd_is_gcd.
Qed.

就像@larsr 的证明一样，我们证明1 < 3使用 omega然后证明 n=1或 n=2使用 omega再次。

证明rel_prime 1 3和 rel_prime 2 3根据 Zis_gcd 定义, 我们申请 Zgcd_is_gcd .这个引理指出计算 gcd足够的。这对于像 (1,3) 这样的具体输入来说是微不足道的。和 (2,3) .

编辑:我们可以推广这个结果，只使用 Gallina。我们定义一个 bool 函数is_prime我们证明是正确的 w.r.t.归纳规范prime .我想这可以以更优雅的方式完成，但我对与 Z 相关的所有引理感到困惑。 .此外，有些定义是不透明的，不能(至少直接)用于定义可计算函数。

Require Import ZArith.
Require Import Znumtheory.
Require Import Omega.
Require Import Bool.
Require Import Recdef.

(** [for_all] checks that [f] is true for any integer between 1 and [n] *)
Function for_all (f:Z->bool) n {measure Z.to_nat n}:=
  if n <=? 1 then true
  else f (n-1) && for_all f (n-1).
Proof.
  intros.
  apply Z.leb_nle in teq.
  apply Z2Nat.inj_lt. omega. omega. omega.
Defined.

Lemma for_all_spec : forall f n,
  for_all f n = true -> forall k, 1 <= k < n -> f k = true.
Proof.
  intros.
  assert (0 <= n) by omega.
  revert n H1 k H0 H.
  apply (natlike_ind (fun n => forall k : Z, 1 <= k < n ->
         for_all f n = true -> f k = true)); intros.
  - omega.
  - rewrite for_all_equation in H2.
    destruct (Z.leb_spec0 (Z.succ x) 1).
    + omega.
    + replace (Z.succ x - 1) with x in H2 by omega. apply andb_true_iff in H2.
      assert (k < x \/ k = x) by omega.
      destruct H3.
      * apply H0. omega. apply H2.
      * subst k. apply H2.
Qed.

Definition is_prime (p:Z) :=
  (1 <? p) && for_all (fun k => Z.gcd k p =? 1) p.

Theorem is_prime_correct : forall z, is_prime z = true -> prime z.
Proof.
  intros. unfold is_prime in H.
  apply andb_true_iff in H. destruct H as (H & H0).
  constructor.
  - apply Z.ltb_lt. assumption.
  - intros.
    apply for_all_spec with (k:=n) in H0; try assumption.
    unfold rel_prime. apply Z.eqb_eq in H0. rewrite <- H0.
    apply Zgcd_is_gcd.
Qed.

证明变得几乎和@Arthur 的一样简单。

Theorem prime113 : prime 113.
Proof.
  apply is_prime_correct; reflexivity.
Qed.