Crush.agda

open import Data.Nat.Base using (ℕ; zero; suc; _+_; _*_; _^_)
open import Data.Product using (_×_; _,_)
open import Function.Base using (_$_; _∘_)
open import Function.Definitions using (Injective)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; trans; sym; cong; refl; subst)

------------------------------------------------------------------------------------------
-- The "crush" function maps a pair of ℕ's to a single ℕ via prime factors 2 and 3.
------------------------------------------------------------------------------------------

ℕ² = ℕ × ℕ

crush : ℕ² → ℕ
crush (n , m) = 2 ^ n * 3 ^ m

-- Goal: prove the above function is injective. Proof at bottom of the file.
CrushInjective = Injective _≡_ _≡_ crush

private 
  import Data.Nat.Properties as NP
  import Data.Nat.Solver
  open import Relation.Nullary using (¬_)
  open import Relation.Nullary.Negation using (contradiction)

  -- Helpers used to prove CrushInjective

  record Odd n : Set where
    constructor odd
    field k : ℕ
          eq : n ≡ suc (2 * k)

  Even = ¬_ ∘ Odd

  3*-odd : ∀ {n} → Odd n → Odd (3 * n)
  3*-odd (odd k refl)
    = odd (1 + 3 * k)
    $ solve 1 (λ k → con 3 :* (con 1 :+ con 2 :* k) :=
                     con 1 :+ con 2 :* (con 1 :+ con 3 :* k))
        refl k
    where open Data.Nat.Solver.+-*-Solver

  3^-odd : ∀ n → Odd (3 ^ n)
  3^-odd zero = odd zero refl
  3^-odd (suc n) = 3*-odd $ 3^-odd n

  2*-even : ∀ n → Even (2 * n)
  2*-even n (odd k 2n≡1+2k) = contradiction 2n≡1+2k (NP.even≢odd n k)

  crush-injectiveˡ : ∀ n₁ m₁ n₂ m₂ → crush (n₁ , m₁) ≡ crush (n₂ , m₂) → n₁ ≡ n₂
  crush-injectiveˡ zero m₁ zero m₂ _ = refl
  crush-injectiveˡ zero m₁ (suc n₂) m₂ eq
    -- "2 ^ 0 * 3 ^ m = 3 ^ m"
    rewrite NP.*-identityˡ (3 ^ m₁)
    -- "2 ^ (suc n) * 3 ^ m" --> "2 * (2 ^ n * 3 ^ m)"
    rewrite NP.*-assoc 2 (2 ^ n₂) (3 ^ m₂)
    = contradiction (subst Odd eq (3^-odd m₁))
                    (2*-even (2 ^ n₂ * 3 ^ m₂))
  crush-injectiveˡ (suc n₁) m₁ zero m₂ eq
    rewrite NP.*-identityˡ (3 ^ m₂)
    rewrite NP.*-assoc 2 (2 ^ n₁) (3 ^ m₁)
    = contradiction (subst Odd (sym eq) (3^-odd m₂))
                    (2*-even (2 ^ n₁ * 3 ^ m₁))
  crush-injectiveˡ (suc n₁) m₁ (suc n₂) m₂ eq
    -- "2 ^ (suc n) * 3 ^ m" --> "2 * (2 ^ n * 3 ^ m)"
    rewrite NP.*-assoc 2 (2 ^ n₁) (3 ^ m₁)
    rewrite NP.*-assoc 2 (2 ^ n₂) (3 ^ m₂)
    = cong suc $ crush-injectiveˡ n₁ m₁ n₂ m₂ $ NP.*-cancelˡ-≡ 1 eq

  2^*-cancelˡ : ∀ n m₁ m₂ → 2 ^ n * m₁ ≡ 2 ^ n * m₂ → m₁ ≡ m₂
  2^*-cancelˡ zero m₁ m₂ eq = NP.+-cancelʳ-≡ m₁ m₂ eq
  2^*-cancelˡ (suc n) m₁ m₂ eq
    -- "2 ^ (suc n) * m" --> "2 ^ n * (2 * m)"
    rewrite NP.*-comm 2 (2 ^ n)
    rewrite NP.*-assoc (2 ^ n) 2 m₁
    rewrite NP.*-assoc (2 ^ n) 2 m₂
    = NP.*-cancelˡ-≡ 1 $ 2^*-cancelˡ n (2 * m₁) (2 * m₂) eq

  3*n≢1 : ∀ n → 3 * n ≢ 1
  3*n≢1 (suc n) eq
    rewrite NP.+-suc n (n + suc (n + 0))
    with eq
  ... | ()

  3^-injective : Injective _≡_ _≡_ (3 ^_)
  3^-injective {zero} {zero} 1≡1 = refl
  3^-injective {zero} {suc m} eq = contradiction (sym eq) (3*n≢1 (3 ^ m))
  3^-injective {suc n} {zero} eq = contradiction eq (3*n≢1 (3 ^ n))
  3^-injective {suc n} {suc m} eq = cong suc $ 3^-injective $ NP.*-cancelˡ-≡ 2 eq

  crush-injectiveʳ : ∀ n m₁ m₂ → crush (n , m₁) ≡ crush (n , m₂) → m₁ ≡ m₂
  crush-injectiveʳ n m₁ m₂ eq = 3^-injective $ 2^*-cancelˡ n (3 ^ m₁) (3 ^ m₂) eq

------------------------------------------------------------------------------------------
-- Proof of CrushInjective
------------------------------------------------------------------------------------------

crush-injective : CrushInjective
crush-injective {n₁ , m₁} {n₂ , m₂} eq with crush-injectiveˡ n₁ m₁ n₂ m₂ eq
crush-injective {n , m₁} {.n , m₂} eq | refl
  = cong (n ,_) $ crush-injectiveʳ n m₁ m₂ eq