{-# OPTIONS --cubical-compatible -WnoUnsupportedIndexedMatch --safe #-}

open import Level
open import Algebra.Bundles
open import Relation.Unary hiding (∅)
open import Data.Sum
open import Data.Product
open import Function.Base
import Data.Nat as Nat
import Data.Nat.Properties
import Relation.Binary.PropositionalEquality as PE
import Relation.Binary.Reasoning.Setoid
open import Data.List hiding (sum)
open import Data.List.Properties hiding (sum-++)
open import Data.List.Relation.Unary.All
open import Data.List.Relation.Unary.All.Properties
import Data.List.Relation.Binary.Pointwise as PW

module Krull.Base (R… : CommutativeRing 0ℓ 0ℓ) where

open CommutativeRing R… renaming (Carrier to R)
open Relation.Binary.Reasoning.Setoid setoid
open import Algebra.Definitions.RawSemiring (Algebra.Bundles.Semiring.rawSemiring semiring) using (_^_)
⊥ : Set
⊥ = 1# ≈ 0#

infix  ¬_
¬_ : Set → Set
¬_ P = P → ⊥

∅ : Pred R 0ℓ
∅ = λ _ → ⊥

contraposition : {A B : Set} → (A → B) → (¬ B → ¬ A)
contraposition f k x = k (f x)

data comprehension-syntax {X : Set} (F : Pred X 0ℓ) (P : X → Set) : Pred X 0ℓ where
  In : {x : X} → F x → P x → comprehension-syntax F P x

syntax comprehension-syntax A (λ x → B) = ｛ x ∶ A ∣ B ｝

-- ⟨ M ⟩ is the ideal generated by M
data ⟨_⟩ (M : Pred R 0ℓ) : Pred R 0ℓ where
  Base   : {x : R} → M x → ⟨ M ⟩ x
  Zero   : ⟨ M ⟩ 0#
  Sum    : {a b : R} → ⟨ M ⟩ a → ⟨ M ⟩ b → ⟨ M ⟩ (a + b)
  Magnet : {r a : R} → ⟨ M ⟩ a → ⟨ M ⟩ (r * a)
  Eq     : {a b : R} → a ≈ b → ⟨ M ⟩ a → ⟨ M ⟩ b

⟨⟩-monotone : {M N : Pred R 0ℓ} → M ⊆ N → ⟨ M ⟩ ⊆ ⟨ N ⟩
⟨⟩-monotone i (Base x)   = Base (i x)
⟨⟩-monotone i Zero       = Zero
⟨⟩-monotone i (Sum e f)  = Sum (⟨⟩-monotone i e) (⟨⟩-monotone i f)
⟨⟩-monotone i (Magnet e) = Magnet (⟨⟩-monotone i e)
⟨⟩-monotone i (Eq p e)   = Eq p (⟨⟩-monotone i e)

⟨⟩-idempotent : {M : Pred R 0ℓ} → ⟨ ⟨ M ⟩ ⟩ ⊆ ⟨ M ⟩
⟨⟩-idempotent (Base p)   = p
⟨⟩-idempotent Zero       = Zero
⟨⟩-idempotent (Sum e f)  = Sum (⟨⟩-idempotent e) (⟨⟩-idempotent f)
⟨⟩-idempotent (Magnet e) = Magnet (⟨⟩-idempotent e)
⟨⟩-idempotent (Eq p e)   = Eq p (⟨⟩-idempotent e)

⟨∅⟩-trivial : {x : R} → x ∈ ⟨ ∅ ⟩ → x ≈ 0#
⟨∅⟩-trivial {x} (Base a)  = begin
  x      ≈˘⟨ *-identityˡ x ⟩
  1# * x ≈⟨ *-congʳ a ⟩
  0# * x ≈⟨ zeroˡ x ⟩
  0#     ∎
⟨∅⟩-trivial Zero      = refl
⟨∅⟩-trivial {x} (Sum p q) = begin
  x       ≈⟨ +-cong (⟨∅⟩-trivial p) (⟨∅⟩-trivial q) ⟩
  0# + 0# ≈⟨ +-identityˡ 0# ⟩
  0#      ∎
⟨∅⟩-trivial {x} (Magnet p)  = begin
  x      ≈⟨ *-congˡ (⟨∅⟩-trivial p) ⟩
  _ * 0# ≈⟨ zeroʳ _ ⟩
  0#     ∎
⟨∅⟩-trivial (Eq q p) = trans (sym q) (⟨∅⟩-trivial p)

⟨⟩-union₀ : {M N : Pred R 0ℓ} {a : R} → a ∈ ⟨ M ∪ N ⟩ → a ∈ ⟨ M ⟩ ⊎ Satisfiable N
⟨⟩-union₀ (Base (inj₁ x)) = inj₁ (Base x)
⟨⟩-union₀ (Base (inj₂ p)) = inj₂ (_ , p)
⟨⟩-union₀ Zero = inj₁ Zero
⟨⟩-union₀ (Sum p q) with ⟨⟩-union₀ p with ⟨⟩-union₀ q
... | inj₁ x | inj₁ x₁ = inj₁ (Sum x x₁)
... | inj₁ x | inj₂ y = inj₂ y
... | inj₂ y | q' = inj₂ y
⟨⟩-union₀ (Magnet p) with ⟨⟩-union₀ p
... | inj₁ x = inj₁ (Magnet x)
... | inj₂ y = inj₂ y
⟨⟩-union₀ (Eq x p) with ⟨⟩-union₀ p
... | inj₁ x₁ = inj₁ (Eq x x₁)
... | inj₂ y = inj₂ y

module _ (G : Nat.ℕ → Pred R 0ℓ) (increasing : {n m : Nat.ℕ} → n Nat.≤ m → G n ⊆ G m) where
  ⟨⟩-compact : {a : R} → (a ∈ ⟨ ⋃[ n ∶ Nat.ℕ ] G n ⟩) → Σ[ n ∈ Nat.ℕ ] a ∈ ⟨ G n ⟩
  ⟨⟩-compact (Base (n , p)) = n , Base p
  ⟨⟩-compact Zero = Nat.zero , Zero
  ⟨⟩-compact (Sum p q) with ⟨⟩-compact p with ⟨⟩-compact q
  ... | n , p' | m , q' = (n Nat.⊔ m) , (Sum (⟨⟩-monotone (increasing (Data.Nat.Properties.m≤m⊔n n m)) p') (⟨⟩-monotone (increasing (Data.Nat.Properties.m≤n⊔m n m)) q'))
  ⟨⟩-compact (Magnet p) with ⟨⟩-compact p
  ... | n , p' = n , Magnet p'
  ⟨⟩-compact (Eq x p) with ⟨⟩-compact p
  ... | n , p' = n , Eq x p'

image : {X Y : Set} (f : X → Y) (R : Pred X 0ℓ) → Pred Y 0ℓ
image f R y = Σ[ x ∈ _ ] y PE.≡ f x × x ∈ R

⟨⟩-mult : {M : Pred R 0ℓ} {a : R} (r : R) → a ∈ ⟨ M ⟩ → r * a ∈ ⟨ image (r *_) M ⟩
⟨⟩-mult r (Base p)       = Base (_ , PE.refl , p)
⟨⟩-mult r Zero           = Eq (sym (zeroʳ r)) Zero
⟨⟩-mult r (Sum e f)      = Eq (sym (distribˡ r _ _)) (Sum (⟨⟩-mult r e) (⟨⟩-mult r f))
⟨⟩-mult {a = a} r (Magnet {z} {w} e) = Eq (trans (sym (*-assoc z r w)) (trans (*-congʳ (*-comm z r)) (*-assoc r z w))) (Magnet {_} {z} (⟨⟩-mult r e))
⟨⟩-mult r (Eq p e)       = Eq (*-congˡ p) (⟨⟩-mult r e)

≡⇒≈ : {a b : R} → a PE.≡ b → a ≈ b
≡⇒≈ PE.refl = refl

neg-one-times : (x : R) → (- 1#) * x ≈ - x
neg-one-times x = begin
  (- 1#) * x             ≈˘⟨ +-identityʳ _ ⟩
  (- 1#) * x + 0#        ≈˘⟨ +-congˡ (-‿inverseʳ x) ⟩
  (- 1#) * x + (x - x)   ≈˘⟨ +-assoc _ x (- x) ⟩
  ((- 1#) * x + x) - x   ≈˘⟨ +-congʳ (+-congˡ (*-identityˡ x)) ⟩
  ((- 1#) * x + 1# * x) - x ≈˘⟨ +-congʳ (distribʳ x (- 1#) 1#) ⟩
  ((- 1#) + 1#) * x - x  ≈⟨ +-congʳ (*-congʳ (-‿inverseˡ 1#)) ⟩
  0# * x - x             ≈⟨ +-congʳ (zeroˡ x) ⟩
  0# - x                 ≈⟨ +-identityˡ (- x) ⟩
  - x                    ∎


-- The following two definitions are only required for the generic
-- prime ideal, not for the maximal ideal construction described in
-- the paper.
√ : Pred R 0ℓ → Pred R 0ℓ
√ M x = Σ[ n ∈ Nat.ℕ ] x ^ n ∈ M

^-* : (x : R) (n m : Nat.ℕ) → x ^ n * x ^ m ≈ x ^ (n Nat.+ m)
^-* x Nat.zero    m = *-identityˡ (x ^ m)
^-* x (Nat.suc n) m = trans (*-assoc x (x ^ n) (x ^ m)) (*-congˡ (^-* x n m))

-- The following definition of the Jacobson radical of an ideal is only required for Forcing.Maximal.
Jac : Pred R 0ℓ → Pred R 0ℓ
Jac M x = (u : R) → ∃[ v ] (1# - u * x) * v - 1# ∈ ⟨ M ⟩

Jac-inflationary : (M : Pred R 0ℓ) → M ⊆ Jac M
Jac-inflationary M {x} x∈M u = 1# , Eq (sym eq) (Eq (neg-one-times (u * x)) (Magnet {r = - 1#} (Magnet {r = u} (Base x∈M))))
  where
  eq : (1# - u * x) * 1# - 1# ≈ - (u * x)
  eq = begin
    (1# - u * x) * 1# - 1#  ≈⟨ +-congʳ (*-identityʳ _) ⟩
    (1# - u * x) - 1#       ≈⟨ +-assoc 1# (- (u * x)) (- 1#) ⟩
    1# + (- (u * x) + - 1#) ≈⟨ +-congˡ (+-comm _ _) ⟩
    1# + (- 1# + - (u * x)) ≈˘⟨ +-assoc 1# (- 1#) _ ⟩
    (1# + - 1#) + - (u * x) ≈⟨ +-congʳ (-‿inverseʳ 1#) ⟩
    0# + - (u * x)          ≈⟨ +-identityˡ _ ⟩
    - (u * x)               ∎

module _ (I : Pred R 0ℓ) (x : R) where
  ideal-decompose : {a : R} → a ∈ ⟨ I ∪ ｛ x ｝ ⟩ → Σ[ u ∈ R ] Σ[ s ∈ R ] (a ≈ u + s * x) × u ∈ ⟨ I ⟩
  ideal-decompose (Base (inj₁ i)) = _ , 0# , trans (sym (+-identityʳ _)) (+-congˡ (sym (zeroˡ x))) , Base i
  ideal-decompose (Base (inj₂ PE.refl)) = 0# , 1# , (trans (sym (+-identityˡ x)) (+-congˡ (sym (*-identityˡ x)))) , Zero
  ideal-decompose Zero = 0# , 0# , trans (sym (+-identityˡ 0#)) (+-congˡ (sym (zeroˡ x))) , Zero
  ideal-decompose (Sum p q) with ideal-decompose p | ideal-decompose q
  ... | u₁ , s₁ , eq₁ , m₁ | u₂ , s₂ , eq₂ , m₂ =
    (u₁ + u₂) , (s₁ + s₂) , trans (+-cong eq₁ eq₂) eq , Sum m₁ m₂
    where
    eq =
      begin
        (u₁ + s₁ * x) + (u₂ + s₂ * x)
      ≈⟨ +-assoc u₁ (s₁ * x) (u₂ + s₂ * x) ⟩
        u₁ + (s₁ * x + (u₂ + s₂ * x))
      ≈⟨ +-congˡ (sym (+-assoc (s₁ * x) u₂ (s₂ * x))) ⟩
        u₁ + (((s₁ * x) + u₂) + (s₂ * x))
      ≈⟨ +-congˡ (+-congʳ (+-comm _ _)) ⟩
        u₁ + ((u₂ + (s₁ * x)) + (s₂ * x))
      ≈⟨ +-congˡ (+-assoc u₂ (s₁ * x) (s₂ * x)) ⟩
        u₁ + (u₂ + (s₁ * x + s₂ * x))
      ≈⟨ +-congˡ (+-congˡ (sym (distribʳ x s₁ s₂))) ⟩
        u₁ + (u₂ + ((s₁ + s₂) * x))
      ≈˘⟨ +-assoc u₁ u₂ ((s₁ + s₂) * x) ⟩
        (u₁ + u₂) + ((s₁ + s₂) * x)
      ∎
  ideal-decompose (Magnet {r} p) with ideal-decompose p
  ... | u , s , eq , m = r * u , r * s , trans (*-congˡ eq) (trans (distribˡ r u (s * x)) (+-congˡ (sym (*-assoc r s x)))) , Magnet m
  ideal-decompose (Eq eq q) with ideal-decompose q
  ... | u , s , eq' , m = u , s , trans (sym eq) eq' , m

inverse-unique : (x y : R) → x + y ≈ 0# → y ≈ - x
inverse-unique x y h = begin
  y              ≈˘⟨ +-identityˡ y ⟩
  0# + y         ≈˘⟨ +-congʳ (-‿inverseˡ x) ⟩
  (- x + x) + y  ≈⟨ +-assoc (- x) x y ⟩
  - x + (x + y)  ≈⟨ +-congˡ h ⟩
  - x + 0#       ≈⟨ +-identityʳ (- x) ⟩
  - x            ∎

double-neg : (x : R) → - (- x) ≈ x
double-neg x = sym (inverse-unique (- x) x (-‿inverseˡ x))

neg-distrib-+ : (a b : R) → - (a + b) ≈ (- a) + (- b)
neg-distrib-+ a b = sym (inverse-unique (a + b) ((- a) + (- b)) lemma)
  where
  lemma : (a + b) + ((- a) + (- b)) ≈ 0#
  lemma = begin
    (a + b) + ((- a) + (- b))  ≈⟨ +-assoc a b ((- a) + (- b)) ⟩
    a + (b + ((- a) + (- b)))  ≈˘⟨ +-congˡ (+-assoc b (- a) (- b)) ⟩
    a + ((b + (- a)) + (- b))  ≈⟨ +-congˡ (+-congʳ (+-comm b (- a))) ⟩
    a + (((- a) + b) + (- b))  ≈⟨ +-congˡ (+-assoc (- a) b (- b)) ⟩
    a + ((- a) + (b + (- b)))  ≈⟨ +-congˡ (+-congˡ (-‿inverseʳ b)) ⟩
    a + ((- a) + 0#)           ≈⟨ +-congˡ (+-identityʳ (- a)) ⟩
    a + (- a)                  ≈⟨ -‿inverseʳ a ⟩
    0#                         ∎

neg-distribʳ-* : (a b : R) → a * (- b) ≈ - (a * b)
neg-distribʳ-* a b = begin
  a * (- b)         ≈˘⟨ *-congˡ (neg-one-times b) ⟩
  a * ((- 1#) * b)  ≈˘⟨ *-assoc a (- 1#) b ⟩
  (a * (- 1#)) * b  ≈⟨ *-congʳ (*-comm a (- 1#)) ⟩
  ((- 1#) * a) * b  ≈⟨ *-assoc (- 1#) a b ⟩
  (- 1#) * (a * b)  ≈⟨ neg-one-times (a * b) ⟩
  - (a * b)         ∎

sub-distribʳ : (a b c : R) → (a - b) * c ≈ a * c - b * c
sub-distribʳ a b c = begin
  (a - b) * c              ≈⟨ distribʳ c a (- b) ⟩
  a * c + (- b) * c        ≈˘⟨ +-congˡ (*-congʳ (neg-one-times b)) ⟩
  a * c + (- 1# * b) * c   ≈⟨ +-congˡ (*-assoc (- 1#) b c) ⟩
  a * c + (- 1#) * (b * c) ≈⟨ +-congˡ (neg-one-times (b * c)) ⟩
  a * c - b * c        ∎

+-cancelˡ-to-sub : (a b c : R) → a ≈ b + c → c ≈ a - b
+-cancelˡ-to-sub a b c h = begin
  c                ≈˘⟨ +-identityˡ c ⟩
  0# + c           ≈˘⟨ +-congʳ (-‿inverseˡ b) ⟩
  (- b + b) + c    ≈⟨ +-assoc (- b) b c ⟩
  - b + (b + c)    ≈˘⟨ +-congˡ h ⟩
  - b + a          ≈⟨ +-comm (- b) a ⟩
  a - b            ∎


-- None of the following functions and results are used in the rest of this
-- project, but they seemed to be a worthwhile addition for future developments.

sum : List R → R
sum []       = 0#
sum (a ∷ as) = a + sum as

sum-++ : (xs ys : List R) → sum (xs ++ ys) ≈ sum xs + sum ys
sum-++ []       ys = sym (+-identityˡ (sum ys))
sum-++ (x ∷ xs) ys = trans (+-congˡ (sum-++ xs ys)) (sym (+-assoc x (sum xs) (sum ys)))

sum-*ˡ : (a : R) (xs : List R) → sum (Data.List.map (a *_) xs) ≈ a * sum xs
sum-*ˡ a []       = sym (zeroʳ a)
sum-*ˡ a (x ∷ xs) = trans (+-congˡ (sum-*ˡ a xs)) (sym (distribˡ a x (sum xs)))

sum-*ʳ : (a : R) (xs : List R) → sum (Data.List.map (_* a) xs) ≈ sum xs * a
sum-*ʳ a []       = sym (zeroˡ a)
sum-*ʳ a (x ∷ xs) = trans (+-congˡ (sum-*ʳ a xs)) (sym (distribʳ a x (sum xs)))

zipped : List (R × R) → List R
zipped = Data.List.map (λ (a , b) → a * b)

weighted-sum : List (R × R) → R
weighted-sum ps = sum (zipped ps)

zipped-* : (r : R) (ps : List (R × R)) → PW.Pointwise _≈_ (zipped (Data.List.map (λ (a , b) → r * a , b) ps)) (Data.List.map (r *_) (zipped ps))
zipped-* r []             = PW.[]
zipped-* r ((a , b) ∷ ps) = *-assoc r a b PW.∷ zipped-* r ps

sum-pointwise : (xs ys : List R) → PW.Pointwise _≈_ xs ys → sum xs ≈ sum ys
sum-pointwise []       []       PW.[]        = refl
sum-pointwise (x ∷ xs) (y ∷ ys) (x≈y PW.∷ k) = +-cong x≈y (sum-pointwise xs ys k)

⟨⟩-canon : {M : Pred R 0ℓ} {a : R} → a ∈ ⟨ M ⟩ → Σ[ ps ∈ List (R × R) ] weighted-sum ps ≈ a × All (M ∘ proj₂) ps
⟨⟩-canon {a = a} (Base p) = (1# , a) ∷ [] , trans (+-identityʳ (1# * a)) (*-identityˡ a) , (p ∷ [])
⟨⟩-canon Zero = [] , (refl , [])
⟨⟩-canon (Sum e f) with ⟨⟩-canon e | ⟨⟩-canon f
... | ps , eq , ms | ps' , eq' , ms' = ps ++ ps' , trans (≡⇒≈ (PE.cong sum (map-++ (uncurry _*_) ps ps'))) (trans (sum-++ (zipped ps) (zipped ps')) (+-cong eq eq')) , ++⁺ ms ms'
⟨⟩-canon (Magnet {r} e) with ⟨⟩-canon e
... | ps , eq , ms = Data.List.map (λ (a , b) → r * a , b) ps , trans (sum-pointwise _ _ (zipped-* r ps)) (trans (sum-*ˡ r (zipped ps)) (*-congˡ eq)) , map⁺ ms
⟨⟩-canon (Eq p e) with ⟨⟩-canon e
... | ps , eq , ms = ps , trans eq p , ms

⟨⟩-canon-reverse : {M : Pred R 0ℓ} (ps : List (R × R)) → All (M ∘ proj₂) ps → weighted-sum ps ∈ ⟨ M ⟩
⟨⟩-canon-reverse []             qs       = Zero
⟨⟩-canon-reverse ((a , b) ∷ ps) (q ∷ qs) = Sum (Magnet (Base q)) (⟨⟩-canon-reverse ps qs)

module _ {M N : Pred R 0ℓ} where
  private
    go : (ps : List (R × R)) → All ((M ∪ N) ∘ proj₂) ps → Σ[ x ∈ R ] Σ[ y ∈ R ] weighted-sum ps ≈ x + y × x ∈ ⟨ M ⟩ × y ∈ ⟨ N ⟩
    go []             []            = 0# , 0# , sym (+-identityˡ 0#) , Zero , Zero
    go ((a , b) ∷ ps) (inj₁ q ∷ ms) with go ps ms
    ... | x , y , eq , e , f = a * b + x , y , trans (+-congˡ eq) (sym (+-assoc (a * b) x y)) , Sum (Magnet (Base q)) e , f
    go ((a , b) ∷ ps) (inj₂ q ∷ ms) with go ps ms
    ... | x , y , eq , e , f = x , a * b + y , trans (+-congˡ eq) (trans (+-comm (a * b) (x + y)) (trans (+-assoc x y (a * b)) (+-congˡ (+-comm y (a * b))))) , e , Sum (Magnet (Base q)) f

  ⟨⟩-union : {a : R} → a ∈ ⟨ M ∪ N ⟩ → Σ[ x ∈ R ] Σ[ y ∈ R ] a ≈ x + y × x ∈ ⟨ M ⟩ × y ∈ ⟨ N ⟩
  ⟨⟩-union e with ⟨⟩-canon e
  ... | ps , eq , ms with go ps ms
  ... | x , y , eq' , e , f = x , y , trans (sym eq) eq' , e , f