Доказательство простых чисел в Coq - PullRequest
Новая
       13

Доказательство простых чисел в Coq

1 голос
/ 06 апреля 2019

У меня есть функция 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).

Я потратил много часов на эту теорему сегодня без реального прогресса.На самом деле, я был немного удивлен, насколько это сложно, так как раньше мне удавалось доказать довольно похожие вещи.Любые подсказки / подсказки, как поступить?

1 Ответ

2 голосов
/ 09 апреля 2019

Вы должны явно написать леммы для каждой из вспомогательных функций, в которых точно указано, что, по вашему мнению, эта функция делает для вас.Например, я попытался сделать это для вашей 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.

Очевидно, что также должен быть способ связать функцию helper с divides предикат.

...