Learning SSReflect by messing around with primes

Using Coq
1

Hi all. I’m currently trying to learn how to use SSReflect efficiently. Messing around with mersenne primes, I managed to prove that for any MP 2^n - 1, n is prime. But the path to get there was pretty rough. My formalization is here: perfect_numbers_rocq/primes.v at main · CharlesAverill/perfect_numbers_rocq · GitHub

The following questions are all of the form “I had to do X to accomplish Y, what is the official ssreflect way to accomplish Y?”

  1. Why the disconnect between eqb and eq? I’m aware one is a decision routine and the other is a relationship, so it’s strange that there is such an even mix of theorems that use one or the other, rather than all of ssrnat using just one (eq would be my expectation). My solution was to instantiate eqP and then invert it, but that just seems so clumsy for how often I had to do it.
  2. My proof is still very much in the standard Ltac style. One thing I notice is my comparatively-extensive use of destruct. This seems like it goes against the ssreflect philosophy, what’s the idiomatic way to accomplish case analysis succinctly?
  3. Same thing with replace/change in regards to expressions I would normally use lia for. Looking at the ssreflect sources, I never see idiomatic proofs use these
  4. The fact I can use bare bools as propositions seems strange. Breaks destruct/split as well which I’m not a fan of
  5. Generalizing/specializing theorems/assumptions?
  6. How come goal selectors get turned off? Seems like an overreach

If any of this is already a part of standard documentation I’ve missed, I would greatly appreciate a referral.

2

Well, I haven’t looked through your whole file, but let’s get started at least. A much more ssreflect idiomatic proof of your first lemma is:

Lemma eq_eqb_same_mod : forall a b m,
    (a = b %[mod m]) <-> (a == b %[mod m]).
Proof.
  by split => /eqP.
Qed.

The /eqP line utilizes the view mechanism of ssreflect, which is a core mechanic.

3

Here’s a bit more of the file.

From Coq Require Import ssreflect ssrfun ssrbool Zify.
From mathcomp Require Import eqtype ssrnat div prime zify.

Lemma eq_eqb_same_mod : forall a b m,
    (a = b %[mod m]) <-> (a == b %[mod m]).
Proof.
  by split => /eqP.
Qed.

Lemma subn_0_r : forall n,
    n - 0 = n.
Proof.
  by lia.
Qed.

Lemma pow2n_1_modsub1 : forall n,
    0 < n ->
    2^n == 1 %[mod 2^n - 1].
Proof.
  move=> n H.
  rewrite eqn_mod_dvd; auto using dvdnn.
  by lia.
Qed.

Lemma modnM : forall a b c d m,
    b <= a -> d <= c ->
    a == b %[mod m] ->
    c == d %[mod m] ->
    a * c == b * d %[mod m].
Proof.
  move=> a b c d m H H0.
  rewrite ? eqn_mod_dvd; auto using leq_mul => /dvdnP [] k H1 /dvdnP [] l H2.
  move: (subnK H) (subnK H0) H1 H2 => {2}<- {2}<- -> ->.
  apply /dvdnP.
  exists (d * k + b * l + k * l * m).
  by lia.
Qed.

Lemma pow_under_mod : forall k a b m,
    0 < k ->
    b <= a ->
    a == b %[mod m] -> a^k == b^k %[mod m].
Proof.
  elim; auto => - [] // ?? a b *.
  rewrite (expnS a) (expnS b).
  by apply modnM; rewrite ? leq_exp2r; auto.
Qed.

Lemma eq_refl_mod : forall n k,
    n = n %[mod k].
Proof.
  by lia.
Qed.

Lemma add_bs_mod : forall k x m,
    k <= x ->
    x == k %[mod m] -> x - k == 0 %[mod m].
Proof.
  move=> ????.
  by rewrite ? eqn_mod_dvd // subn_0_r.
Qed.

To answer some of your questions:

  1. Case analysis: Often you can use case or elim, or the tactical []. I used [] for case analysis in the proof of pow_under_mod, and for destructing an existential hypothesis in the proof of modnM.

  2. Replacing / changing part of an expression: You can do this using something like have ->: x = x + 0 by lia. But in idiomatic ssreflect you should really be trying to keep appropriate combinations of hypotheses and goals in your goal line at all times so that a single rewrite can deal with everything at once. See for example the second line of my proof of modnM or of add_bs_mod.

  1. To generalize a hypothesis H: move: H. To specialize a hypothesis H at 1: move: (H 1) => {}H.
1 Like
4

Here’s the complete file. I deleted any ultimately unneeded lemmas.

From mathcomp Require Import all_ssreflect eqtype ssrnat div prime zify.
Set Bullet Behavior "Strict Subproofs".

Lemma modnM : forall a b c d m : nat,
    b <= a -> d <= c -> a == b %[mod m] ->
    c == d %[mod m] -> a * c == b * d %[mod m].
Proof.
  move=> a b c d m Hba Hdc.
  rewrite ? eqn_mod_dvd; auto using leq_mul => /dvdnP [] k Hk /dvdnP [] l Hl.
  rewrite -(subnK Hba) -(subnK Hdc) Hk Hl.
  apply /dvdnP.
  exists (d * k + b * l + k * l * m).
  by lia.
Qed.

Lemma pow_under_mod : forall k a b m : nat,
    0 < k -> b <= a -> a == b %[mod m] -> a^k == b^k %[mod m].
Proof.
  elim; auto => - [] // n *.
  by rewrite ? (expnS^~ (n.+1)) modnM ? leq_exp2r; auto.
Qed.

(* n is the index of a mersenne prime *)
Definition mp (n : nat) : Prop := prime (2^n - 1).
#[global] Hint Unfold mp : core.

Example mersenne_prime_31 : mp 5.
Proof.
  auto.
Qed.

(* A mersenne prime's index must be prime *)
Lemma mp_n_impl_prime_n : forall n : nat, mp n -> prime n.
Proof.
  rewrite /mp => n Hmpn.
  apply /contraT => /primePn - [ | [] d /andP [] ?? /dvdnP [] x Hn];
                    first by do 2 (destruct n; auto).
  contradict Hmpn; apply /negP /primePn /or_intror.
  exists (2 ^ d - 1).
  - apply /andP; split.
    + by do 2 (destruct d; rewrite -? (addn2 d) ? expnD; try lia).
    + by rewrite ltn_sub2rE ? ltn_exp2l; auto using expn_gt0.
  - rewrite Hn -eqn_mod_dvd 1 ? mulnC ? expnM -1 ? {4}(exp1n x); try lia.
    by rewrite pow_under_mod ? eqn_mod_dvd; auto using dvdnn; lia.
Qed.
1 Like