I'm trying to prove (n : ℕ) → ∃[ m ] n * n ≡ 3 * m 2 → ⊥. Typically I would prove this by rewriting it in terms of congruence, and then splitting on each case. There doesn't seem to be a modular arithmetic module in agda-stdlib. How should I implement modular arithmetic or approach this kind of problem without modular arithmetic?

Edit: there has been discussion in the comments that is not quite precise enough to lead me to an answer, so in the hopes of clarifying what cannot fit in the word count I am dumping my various attempts at this problem, some of which inspired by things in the comments.

open Data.Nat.Divisibility.Core
open Data.Nat.Base
open Relation.Binary.Core
open Level using (0ℓ)
open Relation.Binary.PropositionalEquality
open Data.Empty
open Relation.Nullary
open Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax)
open Relation.Binary.PropositionalEquality.≡-Reasoning
open Data.Nat.Solver
open  -*-Solver

data Z/3 : (n : ℕ) → Set where
  Z/3₀ : (n : ℕ) → ∃[ m ] n ≡ 3 * m → Z/3 n
  Z/3₁ : (n : ℕ) → ∃[ m ] n ≡ 3 * m   1 → Z/3 n
  Z/3₂ : (n : ℕ) → ∃[ m ] n ≡ 3 * m   2 → Z/3 n

data _≋_ : Rel ℕ 0ℓ where
  3∣|a-b| : ∀ {a b : ℕ} → 3 ∣ ∣ a - b ∣ → a ≋ b

q' : {a : ℕ} → (2 ≋ ((a   3) * (a   3))) → (∃[ a' ] 2 ≋ (a' * a'))
q' = {!!}

qq : (n : ℕ) → Z/3 (n * n)
qq zero = Z/3₀ zero (zero , refl)
qq (suc zero) = Z/3₁ 1 (zero , refl)
qq (suc (suc zero)) = Z/3₁ 4 (1 , refl)
qq (suc (suc (suc n))) = Z/3₁ ((3   n) * (3   n)) ({!!} , {!!})

q'' : (n : ℕ) → ∃[ m ] n * n ≡ 3 * m   2 → ⊥
q'' zero (zero , ())
q'' zero (suc fst , ())
q'' (suc zero) (suc zero , ())
q'' (suc zero) (suc (suc fst) , ())
q'' (suc (suc zero)) (suc (suc (suc (suc zero))) , ())
q'' (suc (suc zero)) (suc (suc (suc (suc (suc fst)))) , ())
q'' (suc (suc (suc n))) (suc fst , snd) = q'' n ({!!} , {!!})

sq : {a : ℕ} → Z/3 a →  Z/3 (a * a)
sq (Z/3₀ n (m , p)) = Z/3₀ (n * n) (3 * m * m , q) where
  q =
    begin
      n * n
    ≡⟨ cong (λ e → e * n) p ⟩
      (3 * m) * n
    ≡⟨ cong (λ e → (3 * m) * e) p ⟩
      (3 * m) * (3 * m)
    ≡⟨ solve 1 (λ m' → (con 3 :* m') :* (con 3 :* m') := con 3 :* m' :* m' :  (con 3 :* m' :* m' :  (con 3 :* m' :* m' :  con zero))) refl m ⟩
      3 * m * m   (3 * m * m   (3 * m * m   zero))
    ∎
    -- (3 * b   1) * (3 * b   1)
    -- 9b^2   6b   1
    -- 3(3b^2   2b)  1
    -- (3 * b   2) * (3 * b   2)
    -- 9b^2   12b   4
    -- 3(3b^2 4b 1)   1
sq (Z/3₁ n (m , p)) = Z/3₁ (n * n) (3 * m * m   2 * m , q) where
  q =
    begin
      n * n
    ≡⟨ cong (λ e → e * n) p ⟩
      (3 * m   1) * n
    ≡⟨ cong (λ e → (3 * m   1) * e) p ⟩
      (3 * m   1) * (3 * m   1)
    ≡⟨ solve 1 (λ m' → (con 3 :* m' :  con 1) :* (con 3 :* m' :  con 1) := (m' :  (m' :  (m' :  con 0))) :* m' :  (m' :  (m' :  con 0)) :  ((m' :  (m' :  (m' :  con 0))) :* m' :  (m' :  (m' :  con 0)) :  ((m' :  (m' :  (m' :  con 0))) :* m' :  (m' :  (m' :  con 0)) :  con 0)) :  con 1 ) refl m ⟩
      (m   (m   (m   0))) * m   (m   (m   0))   ((m   (m   (m   0))) * m   (m   (m   0))   ((m   (m   (m   0))) * m   (m   (m   0))   0))   1
    ∎
sq (Z/3₂ n (m , p)) = Z/3₁ (n * n) (3 * m * m   4 * m   1 , {!!})

q : {a : ℕ} → ¬(2 ≋ (a * a))
q {zero} (3∣|a-b| (divides zero ()))
q {zero} (3∣|a-b| (divides (suc quotient) ()))
q {suc zero} (3∣|a-b| (divides zero ()))
q {suc zero} (3∣|a-b| (divides (suc quotient) ()))
q {suc (suc zero)} (3∣|a-b| (divides zero ()))
q {suc (suc zero)} (3∣|a-b| (divides (suc quotient) ()))
q {suc (suc (suc a))} (3∣|a-b| (divides (suc quotient) equality)) = {!!}

CodePudding user response：

Building on Mark's proof outline:

module SOMod where

open import Data.Empty
open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.DivMod
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Negation

open ≡-Reasoning

lemma : ∀ m n → (n * n) % 3 ≢ (3 * m   2) % 3
lemma m n p = contradiction ≡2 (≢2 n)
  where
  ≡2 : ((n % 3) * (n % 3)) % 3 ≡ 2
  ≡2 = begin
    ((n % 3) * (n % 3)) % 3 ≡˘⟨ %-distribˡ-* n n 3 ⟩
    (n * n) % 3             ≡⟨ p ⟩
    (3 * m   2) % 3         ≡⟨ cong (_% 3) ( -comm (3 * m) 2) ⟩
    (2   3 * m) % 3         ≡⟨ cong (λ # → (2   #) % 3) (*-comm 3 m) ⟩
    (2   m * 3) % 3         ≡⟨ [m kn]%n≡m%n 2 m 3 ⟩
    2 % 3                   ≡⟨⟩
    2                       ∎

  ≢2 : ∀ n → ((n % 3) * (n % 3)) % 3 ≢ 2
  ≢2 zero                = λ ()
  ≢2 (suc zero)          = λ ()
  ≢2 (suc (suc zero))    = λ ()
  ≢2 (suc (suc (suc n))) = ≢2 n

proof : ∀ n → ∃[ m ] n * n ≡ 3 * m   2 → ⊥
proof n (m , p) = contradiction (cong (_% 3) p) (lemma m n)