Library PrimeGapS1.MaynardVerify

From Stdlib Require Import ZArith List Lia.
From mathcomp Require Import all_ssreflect all_algebra.

From PrimeGapS1.MaynardVerify Require Export Def.
From PrimeGapS1.MaynardVerify Require Import
  M2_0 M2_1 M2_2 M2_3 M2_4 M2_5.

Import ListNotations.


Lemma seq_split_42 :
  List.seq 0 42 =
    List.seq 0 7 ++ List.seq 7 7 ++ List.seq 14 7
    ++ List.seq 21 7 ++ List.seq 28 7 ++ List.seq 35 7.
Proof. vm_compute. reflexivity. Qed.

Lemma M2_check_rows_app : ∀ l1 l2 : list nat,
  M2_check_rows (l1 ++ l2) = M2_check_rows l1 && M2_check_rows l2.
Proof. intros l1 l2. apply List.forallb_app. Qed.


Lemma all_match_M2Z_true : all_match_M2Z = true.
Proof.
  unfold all_match_M2Z.
  rewrite seq_split_42.
  rewrite !M2_check_rows_app.
  rewrite M2_check_rows_0_6 M2_check_rows_7_13 M2_check_rows_14_20
          M2_check_rows_21_27 M2_check_rows_28_34 M2_check_rows_35_41.
  reflexivity.
Qed.

Opaque M1_entry_matchZ M2_entry_matchZ.

Lemma M2_entry_match_in_grid {i j} :
  (i < 42)%nat → (j < 42)%nat →
  M2_entry_matchZ i j = true.
Proof.
  move⇒ Hi Hj.
  have HM := all_match_M2Z_true.
  rewrite /all_match_M2Z /M2_check_rows in HM.
  have Hrow : forallb (M2_entry_matchZ i) (List.seq 0 42) = true
    := forallb_seq_in HM Hi.
  exact: forallb_seq_in Hrow Hj.
Qed.