Library PrimeGapS1.MaynardVerify.Def

From Stdlib Require Import ZArith List Lia.
From mathcomp Require Import ssreflect ssrbool ssrnat.
From PrimeGapS1 Require Import IntMat CharPoly Witness.
From PrimeGapS1 Require Import MaynardFactQ MaynardBasis MaynardSpec.

Import ListNotations.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.


Definition m1_num (i j : nat) : Z := fst (m1_num_den_at i j).
Definition m1_den (i j : nat) : Z := snd (m1_num_den_at i j).

Definition m2_num (i j : nat) : Z := fst (m2_num_den_at i j).
Definition m2_den (i j : nat) : Z := snd (m2_num_den_at i j).



Definition M1_entry_matchZ (i j : nat) : bool :=
  let p := m1_num_den_at i j in
  Z.eqb (BinInt.Z.mul (fst p) D_M1)
        (BinInt.Z.mul (mat_get M1_int i j) (snd p)).

Definition M2_entry_matchZ (i j : nat) : bool :=
  let p := m2_num_den_at i j in
  Z.eqb (BinInt.Z.mul (fst p) D_M2)
        (BinInt.Z.mul (mat_get M2_int i j) (snd p)).


Definition M2_check_rows (rows : list nat) : bool :=
  List.forallb
    (fun i ⇒ List.forallb (fun j ⇒ M2_entry_matchZ i j) (List.seq 0 42))
    rows.

Definition all_match_M1Z : bool :=
  List.forallb
    (fun i ⇒ List.forallb (fun j ⇒ M1_entry_matchZ i j) (List.seq 0 42))
    (List.seq 0 42).

Definition all_match_M2Z : bool := M2_check_rows (List.seq 0 42).


Lemma all_match_M1Z_true : all_match_M1Z = true.
Proof. vm_compute. reflexivity. Qed.


Lemma M1_entry_matchZ_E i j :
  M1_entry_matchZ i j
  = (m1_num i j × D_M1 =? mat_get M1_int i j × m1_den i j)%Z.
Proof. by []. Qed.

Lemma M2_entry_matchZ_E i j :
  M2_entry_matchZ i j
  = (m2_num i j × D_M2 =? mat_get M2_int i j × m2_den i j)%Z.
Proof. by []. Qed.


Opaque M1_entry_matchZ M2_entry_matchZ.


Lemma forallb_seq_in {n} {f : nat → bool} {i} :
  List.forallb f (List.seq 0 n) = true →
  (i < n)%nat → f i = true.
Proof.
  move⇒ H Hi.
  rewrite → List.forallb_forall in H.
  apply: H; apply: (proj2 (List.in_seq n 0 i)).
  by split; [apply: Nat.le_0_l | apply/ltP; exact: Hi].
Qed.


Lemma M1_entry_match_in_grid {i j} :
  (i < 42)%nat → (j < 42)%nat →
  M1_entry_matchZ i j = true.
Proof.
  move⇒ Hi Hj.
  have HM := all_match_M1Z_true.
  rewrite /all_match_M1Z in HM.
  have Hrow : forallb (M1_entry_matchZ i) (List.seq 0 42) = true
    := forallb_seq_in HM Hi.
  exact: forallb_seq_in Hrow Hj.
Qed.